ELEC 7770 Advanced VLSI Design Spring 2012 VerificationVLSI Realization ProcessOrigin of “Debugging”Verification and TestingDefinitionsWhat is Being Verified?Avoiding Interpretation ErrorMethods of VerificationEquivalence CheckingCompare Two CircuitsAre Graphs Isomorphic? NO.Are Boolean Functions Identical? YES.Model CheckingSymbolic SimulationSimulation: TestbenchTestbenchSlide 17Slide 18ATPG 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 TheoremClaude E. Shannon (1916-2001)Shannon’s LegacyTheoremExpansion 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 Ordered BDD (ROBDD)ROBDDsReduction: OBDD to ROBDDProperties of ROBDDELEC 7770ELEC 7770Advanced VLSI DesignAdvanced VLSI DesignSpring 2012Spring 2012VerificationVerificationVishwani 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_Spr12/course.htmlhttp://www.eng.auburn.edu/~vagrawal/COURSE/E7770_Spr12/course.html Spring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)11VLSI Realization ProcessVLSI Realization ProcessSpring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)22Determine requirementsWrite specificationsDesign synthesis and VerificationFabricationManufacturing testChips to customerCustomer’s needTest developmentDesignManufactureOrigin of “Debugging”Origin of “Debugging”Spring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)33D. 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).Verification and TestingVerification and TestingSpring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)44SpecificationTestingManufacturingVerificationHardware designSilicon50-70% cost 30-50% costDefinitionsDefinitions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 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)55What 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?Spring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)66SpecificationInterpretationRTL codingVerificationJ. Bergeron, Writing Testbenches: Functional VerificationOf HDL Models, Springer, 2000.Avoiding Interpretation ErrorAvoiding Interpretation ErrorUse redundancyUse redundancySpring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)77SpecificationInterpretationRTL codingVerificationInterpretationMethods 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 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)88Equivalence 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 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)99Compare Two CircuitsCompare Two CircuitsAre graphs isomorphic?Are graphs isomorphic?Are Boolean functions identical?Are Boolean functions identical?Are timing behaviors identical?Are timing behaviors identical?Spring 2012, Jan 23 . .Spring 2012, Jan 23 . .ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design