11Implementation Verification:Equivalence CheckingProfs. Kurt Keutzer & Sanjit SeshiaEECSUC BerkeleyWith thanks to Srinivas Devadas, MITKeutzer & Seshia2Design ProcessDesign: specify and enter the design intentImplement:refine the design through all phasesVerify:verify the correctness of design and implementation2Keutzer & Seshia3Implementation VerificationRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignIs the implementationconsistentwith the originaldesign intent?Is what I implementedwhat Iwanted?absq01dclkabsq01dclkKeutzer & Seshia4Design VerificationRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignspecificationIs the designconsistentwith the originalspecification?Is what I think I wantwhat I really want?3Keutzer & Seshia5Manufacture Verification (Test)RTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignIs the manufacturedcircuitconsistentwith the implemented design?Did theybuildwhat Iwanted?absq01dclkabsq01dclkKeutzer & Seshia6Impl. Verification for ASIC’s by SimulationRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignApply gate-level simulation at each step to verify functionality:• 0-1 behavior on regression test setand timing:• maximum delay of circuit across critical pathsabsq01dclkabsq01dclkASICsignoff4Keutzer & Seshia7Advantages of gate-level simulation– verifies timing and functionality simultaneously– approach well understood by designersDisadvantages of gate-level simulation?Simulationdriver(vectors)Simulationmonitor(yes/no)andspeedSoftware Simulationabsq01dclkKeutzer & Seshia8Advantages of gate-level simulation– verifies timing and functionality simultaneously– approach well understood by designersDisadvantages of gate-level simulation?– computationally intensive - only ~10 clock cycles of 100K gate design per 1 CPU second– incomplete - results only as good as your vector set - easy to overlook incorrect timing/behaviorSimulationdriver(vectors)Simulationmonitor(yes/no)andspeedSoftware Simulationabsq01dclk5Keutzer & Seshia9Alternative – “Static Sign-off”RTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignabsq01dclkabsq01dclkASICsignoffUse static analysis techniques to verify: functionality:• formal equivalence-checking techniquesand timing:• use static timing analysis –discussed earlier in the semester, but don’t forget about false paths!Keutzer & Seshia10Problem: RTL to RTL VerificationAfter verification RTL may still be modified– RTL level improvements for :• performance• power• area• testabilityNeed to verify that new RTL is correctSpecification Implementation6Keutzer & Seshia11Problem: RTL to Gates VerificationVerify the gate level implementation is consistent with the RTL level designErrors may have occurred due to– synthesis (heaven forbid!!)– manual interventionHDL Design ImplementationKeutzer & Seshia12Problem: Gates to Gates VerificationVerify the modified gate level implementation is consistent with the RTL level designErrors may have occurred due to– Incorrect synthesis or module generation (heaven forbid!!)– Test insertion– Scan chain reordering– Clock tree synthesis– Post layout “tweaks”Netlist Implementation7Keutzer & Seshia13Problem: Layout to Gates Verification (LVS)Verify the modified gate level implementation is consistent with the RTL level designErrors may have occurred due to– Errors in physical design tools– Manual changes in layoutVerification is primarily graphical or ``topological’’netlist physical layoutKeutzer & Seshia15This Lecture• Solving the “Gates-to-Gates” verification problem– Special case: when only combinational parts differ• Binary Decision Diagrams (BDDs)– A very, very useful data structure!– Many applications, in EDA and elsewhere8Keutzer & Seshia16Solving Gates to Gates VerificationclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogic``specification’’implementationKeutzer & Seshia17Extract combinational portionscomparecombinationalportions``spec’’Flip-flopsCombinationalLogicinputsoutputs``implementation’’Flip-flopsCombinationalLogicinputsoutputs9Keutzer & Seshia18Combinational Equivalence CheckingGiven:• Combinational circuits C1 and C2(Boolean functions B1 and B2) How can we prove that C1 is/isn’t equivalent to C2, in a reasonable amount of time? Keutzer & Seshia19Combinational Equivalence CheckingPresumes equivalence-relation given (or discovered) between sequential circuitsApproaches– Boolean satisfiability (SAT)– Set-theoretic approaches (used in 2-level examples)– Symbolic simulation – Structural techniques• graph isomorphism– Canonical forms - BDD’s and variants– Test-oriented methodsThese techniques form the foundation of modern equivalence checking/implementation verification10Keutzer & Seshia202-level circuitsNow, treating F and G as sets of cubes we can check if)()()( FGGFGF→•→⇔⇔)()( GFGF ∨∧∨⇔1)()( ⇔∪∩∪ GFGFWhich is feasible for most 2-level circuits/SOP expressionsWorked well in the Espresso era – doesn’t generalize to multilevel Keutzer & Seshia21Multilevel: Structural MethodsCombinational circuit 1unmapped circuit 1unmapped circuit 2Combinational circuit 2Compare them as graphs.Is this tough or easy to solve algorithmically?11Keutzer & Seshia22Structural MethodsCombinational circuit 1unmapped circuit 1unmapped circuit 2Combinational circuit 2Looks tough – graph isomorphismTurns out to be easy – DAGsIf this returns “Equivalent”, are the ckts equivalent? How about when it returns “Not Equivalent”?Keutzer & Seshia23More powerful: TestingGiven two single-output circuits A and BAre A and B equivalent can be posed as: Is there a test for F s-a-0?If F s-a-0 is redundant, A ≡≡≡≡ B else test vector produces different outputs for Aand B.x2Bx4x1x3Axs-a-012Keutzer & Seshia24Boolean Satisfiability (SAT) Againabcdefghi1hfift = 1?This time ask whether there is an input on which Circuit 1 and Circuit 2 differ? This time we don’t expect one!Circuit 1Circuit 2 –Any structural simularities (found earlier)are sharedKeutzer & Seshia25Looking at the Problem AfreshPrimary Inputs, Register and Black Box Outputsspec implementationCOMPARE0 or