ELEC 7770 Advanced VLSI Design Spring 2008 VerificationVLSI Realization ProcessOrigin of “Debugging”Verification and TestingDefinitionsWhat is Being Verified?Avoiding Interpretation ErrorMethods of VerificationEquivalence CheckingCompare Two CircuitsModel CheckingSymbolic SimulationSimulation: TestbenchTestbenchSlide 15Slide 16ATPG Approach (Miter)Difficulties with MiterA Heuristic ApproachExample Circuit C1Example Circuit C2C1 ≡ C2C2’: Erroneous Implementation of C2Incorrect Result: C1 ≡ C2’Additional SafeguardProbabilistic EquivalenceSimplest ExampleProbability of Wrong DecisionCalculation of Signal ProbabilityReferences on Signal ProbabilityMore on Equivalence CheckingMethods of Equivalence CheckingShannon’s Expansion TheoremTheoremExpansion About Two InputsBinary Decision TreeBinary Decision DiagramsBinary Decision DiagramOrdered Binary Decision Diagram (OBDD)OBDD With Different Input OrderingEvaluating Function from OBDDCannot Compare Two CircuitsOBDD Graph IsomorphismReduced Order BDD (ROBDD)ROBDDsReduction: OBDD to ROBDDProperties of ROBDDSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)11ELEC 7770ELEC 7770Advanced VLSI DesignAdvanced VLSI DesignSpring 2008Spring 2008VerificationVerificationVishwani D. AgrawalVishwani D. AgrawalJames J. Danaher ProfessorJames J. Danaher ProfessorECE Department, Auburn UniversityECE Department, Auburn UniversityAuburn, AL 36849Auburn, AL [email protected]@eng.auburn.eduhttp://www.eng.auburn.edu/~vagrawal/COURSE/E7770_Spr078/course.htmlhttp://www.eng.auburn.edu/~vagrawal/COURSE/E7770_Spr078/course.htmlSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)22VLSI Realization ProcessVLSI Realization ProcessDetermine requirementsWrite specificationsDesign synthesis and VerificationFabricationManufacturing testChips to customerCustomer’s needTest developmentDesignManufactureSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)33Origin of “Debugging”Origin of “Debugging”D. Gizopoulos (Editor), Advances in Electronic Testing: Challenges and Methodologies, Springer, 2006, Chapter 3, “Silicon Debug,” by D. Josephson and B. Gottlieb.Thomas Edison wrote in a letter in 1878: “It has been just so in all of my inventions. The first step is an intuition, and comes with a burst, then difficulties arise—this thing gives out and [it is] then that “Bugs” — as such little faults and difficulties are called — show themselves and months of intense watching, study and labor are requisite before commercial success or failure is certainly reached.” An interesting example of “debugging” was in 1945 when a computer failure was traced down to a moth that was caught in a relay between contacts (Figure 3-1).Spring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)44Verification and TestingVerification and TestingSpecificationTestingManufacturingVerificationHardware designSilicon50-70% cost 30-50% costSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)55DefinitionsDefinitionsVerification: Predictive analysis to ensure that the Verification: Predictive analysis to ensure that the synthesized design, when manufactured, will synthesized design, when manufactured, will perform the given I/O function.perform the given I/O function.Alternative Definition: Verification is a process used Alternative Definition: Verification is a process used to demonstrate the functional correctness of a to demonstrate the functional correctness of a design.design.Spring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)66What is Being Verified?What is Being Verified?Given a set of specification,Given a set of specification,Does the design do what was specified?Does the design do what was specified?SpecificationInterpretationRTL codingVerificationJ. Bergeron, Writing Testbenches: Functional VerificationOf HDL Models, Springer, 2000.Spring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)77Avoiding Interpretation ErrorAvoiding Interpretation ErrorUse redundancyUse redundancySpecificationInterpretationRTL codingVerificationInterpretationSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)88Methods of VerificationMethods of VerificationSimulation: Verify input-output behavior for Simulation: Verify input-output behavior for selected cases.selected cases.Formal verification: Exhaustively verify input-Formal verification: Exhaustively verify input-output behavior:output behavior:Equivalence checkingEquivalence checkingModel checkingModel checkingSymbolic simulationSymbolic simulationSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)99Equivalence CheckingEquivalence CheckingLogic equivalence: Two circuits implement Logic equivalence: Two circuits implement identical Boolean function.identical Boolean function.Logic and temporal equivalence: Two finite state Logic and temporal equivalence: Two finite state machines have identical input-output behavior machines have identical input-output behavior (machine equivalence).(machine equivalence).Topological equivalence: Two netlists are Topological equivalence: Two netlists are identical (graph isomorphism).identical (graph isomorphism).Reference: S.-Y. Hwang and K.-T. Cheng, Reference: S.-Y. Hwang and K.-T. Cheng, Formal Equivalence Checking and Design Formal Equivalence Checking and Design DebuggingDebugging, Springer, 1998., Springer, 1998.Spring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1010Compare Two CircuitsCompare Two CircuitsGraphs isomorphic?Graphs isomorphic?Boolean functions identical?Boolean functions identical?Timing behaviors identical?Timing behaviors identical? a c b a c b f fSpring 08, Jan 22 . .Spring 08, Jan 22 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1111Model CheckingModel