ELEC 7770 Advanced VLSI Design Spring 2007 Logic EquivalenceEquivalence CheckingCompare Two CircuitsATPG 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 CheckingSpring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)11ELEC 7770ELEC 7770Advanced VLSI DesignAdvanced VLSI DesignSpring 2007Spring 2007Logic EquivalenceLogic EquivalenceVishwani 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_Spr07http://www.eng.auburn.edu/~vagrawal/COURSE/E7770_Spr07Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)22Equivalence CheckingEquivalence CheckingDefinition: Establishing that two circuits are Definition: Establishing that two circuits are functionally equivalent.functionally equivalent.Applications:Applications:Verify that a design is identical to specification.Verify that a design is identical to specification.Verify that synthesis did not change the function.Verify that synthesis did not change the function.Verify that corrections made to a design did not create Verify that corrections made to a design did not create new errors.new errors.Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)33Compare 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 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)44ATPG Approach (Miter)ATPG Approach (Miter)Redundancy of a stuck-at-0 fault, checked by ATPG, establishes equivalence of the corresponding output pair.If the fault is detectable, its tests are used to diagnose the differences.Circuit 1(Verified design)Circuit 2(Sythesized or modified design) stuck-at-0stuck-at-0Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)55Difficulties with MiterDifficulties with MiterATPG is NP-completeATPG is NP-completeWhen circuits are equivalent, proving When circuits are equivalent, proving redundancy of faults is computationally redundancy of faults is computationally expensive.expensive.When circuits are different, test vectors are When circuits are different, test vectors are quickly found, but diagnosis is difficult.quickly found, but diagnosis is difficult.Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)66A Heuristic ApproachA Heuristic ApproachDerive V1, test vectors for all faults in C1.Derive V1, test vectors for all faults in C1.Derive V2, test vectors for all faults in C2.Derive V2, test vectors for all faults in C2.If the combined set, V1+V2, produces the same If the combined set, V1+V2, produces the same outputs from the two circuits, then they are outputs from the two circuits, then they are probablyprobably equivalent. equivalent.Reference: V. D. Agrawal, “Choice of Tests for Reference: V. D. Agrawal, “Choice of Tests for Logic Verification and Equivalence Checking and Logic Verification and Equivalence Checking and the Use of Fault Simulation,” Proc. 13the Use of Fault Simulation,” Proc. 13thth International Conf. VLSI Design, January 2000, International Conf. VLSI Design, January 2000, pp. 306-311.pp. 306-311.Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)77Example Circuit C1Example Circuit C1 x1 x2 x3 x4 C1C1 = x1 x3 x4 + x2 x3 + x2 x41 1 11 1 1 11 x3 x2 x4 x1TestsSpring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)88Example Circuit C2Example Circuit C2 x1 x2 x3 x4 C2C2 = x1 x3 x4 + x2 x3 + x2 x41 1 11 1 1 11 x3 x2 x4 x1TestsSpring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)99C1 C1 ≡≡ C2 C21 1 11 1 1 11 x3 x2 x4 x1Tests1 1 11 1 1 11 x3 x2 x4 x1TestsC1C2Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1010C2’: Erroneous Implementation of C2C2’: Erroneous Implementation of C2 x1 x2 x3 x4 C2’C2 = x1 x3 x4 + x2 x3 + x2 x41 1 11 1 11 x3 x2 x4 x1TestsC2’ = x1 x2 x3 x4 + x2 x3 + x2 x4 minterm deletedSpring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1111Incorrect Result: C1 Incorrect Result: C1 ≡ ≡ C2’C2’C1 = x1 x3 x4 + x2 x3 + x2 x41 1 11 1 11 x3 x2 x4 x1TestsC2’ = x1 x2 x3 x4 + x2 x3 + x2 x4 minterm deleted1 1 11 1 1 11 x3 x2 x4 x1TestsSpring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1212Additional SafeguardAdditional SafeguardSimulate V1+V2 for equivalence:Output always 0No single fault on PI’s detectedStill not perfectC1(Verified design)C2(Sythesized or modified design) s-a-0s-a-10Spring 07, Feb 8Spring 07, Feb 8ELEC 7770: Advanced VLSI Design (Agrawal)ELEC 7770: Advanced VLSI Design (Agrawal)1313Probabilistic EquivalenceProbabilistic EquivalenceConsider two Boolean functions F and G of the same set Consider two Boolean functions F and G of the same set of input variables {X1, . . . , Xn}.of input variables {X1, . . . , Xn}.Let f = Prob(F=1), g = Prob(G=1), xi = Prob(Xi=1)Let f = Prob(F=1), g = Prob(G=1), xi = Prob(Xi=1)For any arbitrarily given values of xi, if f = g, then F and G For any arbitrarily given values of xi, if f = g, then F and G are equivalent with probability 1.are equivalent with probability 1.References:References:J. Jain, J. Bittner, D. S. Fussell and J. A. Abraham, “Probabilistic J. Jain, J. Bittner, D. S. Fussell and J. A. Abraham, “Probabilistic Verification of Boolean Functions,” Formal Methods in System