11Implementation Verification:Equivalence CheckingProf. Kurt KeutzerEECSUC BerkeleyWith thanks to Srinivas Devadas, MITKurt Keutzer 2Design ProcessDesign: specify and enter the design intentImplement:refine the design through all phasesVerify:verify the correctness of design and implementation2Kurt Keutzer 3Design VerificationRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignspecificationIs the designconsistentwith the originalspecification?Is what I think I wantwhat I really want?Kurt Keutzer 4Implementation VerificationRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignIs the implementationconsistentwith the originaldesign intent?Is what I implementedwhat Iwanted?absq01dclkabsq01dclk3Kurt Keutzer 5Manufacture Verification (Test)RTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignIs the manufacturedcircuitconsistentwith the implemented design?Did theybuildwhat Iwanted?absq01dclkabsq01dclkKurt Keutzer 6Implementation verification for ASIC’sRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/modulegeneratorsphysicaldesignlayoutmanualdesignApply gate-level simulation (‘‘the golden simulator’’) at each step to verify functionality:• 0-1 behavior on regression test setand timing:• maximum delay of circuit across critical pathsabsq01dclkabsq01dclkASICsignoff4Kurt Keutzer 7Advantages of gate-level simulation– verifies timing and functionality simultaneously– approach well understood by designersDisadvantages of gate-level simulation?Simulationdriver(vectors)Simulationmonitor(yes/no)andspeedSoftware Simulationabsq01dclkKurt Keutzer 8Advantages of gate-level simulation– verifies timing and functionality simultaneously– approach well understood by designersDisadvantages of gate-level simulation?– computationally intensive - only 1 - 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 Simulationabsq01dclk5Kurt Keutzer 9Alternative - Static Sign-offRTLSynthesisHDLnetlistlogicoptimizationnetlistLibrary/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!Kurt Keutzer 10Problem: 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 Implementation6Kurt Keutzer 11Problem: 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 ImplementationKurt Keutzer 12Problem: 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 Implementation7Kurt Keutzer 13Problem: 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 layoutKurt Keutzer 14Solving Layout to Gates Verification (LVS)Extract gate level models from physical levelGraphically compare extracted model against gate-level schematic (layout versus schematic)Flag any discrepanciesnetlist physical layout8Kurt Keutzer 15Solving Gates to Gates VerificationclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogicclkCombinationallogic``specification’’implementationKurt Keutzer 16Extract combinational portionscomparecombinationalportions``spec’’Flip-flopsCombinationalLogicinputsoutputs``implementation’’Flip-flopsCombinationalLogicinputsoutputs9Kurt Keutzer 17Combinational Equivalence CheckingGiven combination circuits C1 and C2/(Boolean functions B1 and B2) how can we practically prove that C1 is equivalent to C2?Kurt Keutzer 18Combinational Equivalence CheckingPresumes equivalence-relation given (or discovered) between sequential circuitsApproaches– Reasoning in the propositional calculus/Satisfiability– Set-theoretic approaches (used in 2-level examples)– Symbolic simulation (used in 2-level examples)– Symbolic manipulation• graph isomorphism• structural reductions– Canonical forms - BDD’s and variants– Test-oriented methods• static, dynamic learningThese techniques form the foundation of modern equivalence checking/implementation verification10Kurt Keutzer 192-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 expressions/DNF formulasWorked well in the espresso era – doesn’t generalize to multilevel Kurt Keutzer 20Multilevel: Structural MethodsCombinational circuit 1unmapped circuit 1unmapped circuit 2Combinational circuit 2Compare them as graphsLooks tough – why?Turns out to be easy – why?11Kurt Keutzer 21Structural MethodsCombinational circuit 1unmapped circuit 1unmapped circuit 2Combinational circuit 2Compare them as graphsLooks tough – graph isomorphismTurns out to be easy – DAGsThis helps but runs out of gas soon.Kurt Keutzer 22More 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-012Kurt Keutzer 23SAT 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 sharedKurt Keutzer 24More powerful: Comparison MitrePrimary Inputs, Register and Black Box Outputsspec implementationCOMPARE0 or 113Kurt Keutzer 25Canonical Forms: Binary Decision TreeDo not have to store