Techniques for performing conditional sequential equivalence checking of an integrated circuit logic design
View Patent ↗A technique for conditional sequential equivalence checking of logic designs embodied in netlists includes creating an equivalence-checking netlist over a first netlist and a second netlist. The conditional sequential equivalence checking includes conditions under which equivalences of the first and second netlists are checked. The technique derives a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set and attempts to prove that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate. The candidate conditional equivalence invariants that cannot be proven accurate are removed from the set of candidate conditional equivalence invariants. The candidate conditional equivalence invariants that have been proven accurate are recorded as a set of conditional equivalence invariants. Finally, the conditional sequential equivalence checking of the equivalence-checking netlist is completed using the set of conditional equivalence invariants that are recorded.
1. A method for conditional sequential equivalence checking of logic designs embodied in netlists using a data processing system, comprising:
creating, using the data processing system, an equivalence-checking netlist over a first netlist and a second netlist, wherein the first netlist is associated with a first logic design and the second netlist is associated with a second logic design, and wherein the conditional sequential equivalence checking includes conditions under which equivalences of the first and second netlists are checked;
deriving, using the data processing system, a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set;
attempting to prove, using the data processing system, that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate;
removing, using the data processing system, candidate conditional equivalence invariants that cannot be proven accurate from the set of candidate conditional equivalence invariants;
recording, using the data processing system, the candidate conditional equivalence invariants that have been proven accurate as a set of conditional equivalence invariants; and
completing, using the data processing system, the conditional sequential equivalence checking of the equivalence-checking netlist using the recorded set of conditional equivalence invariants.
2. The method of claim 1 , wherein the removing employs under-approximate analysis to falsify invalid ones of the candidate conditional equivalence invariants.
3. The method of claim 2 , wherein the removing employs random simulation, a hardware accelerator, or formal/semi-formal search techniques to falsify invalid ones of the candidate conditional equivalence invariants.
4. The method of claim 1 , wherein the equivalence-checking netlist is binary valued.
5. The method of claim 1 , wherein the equivalence-checking netlist is ternary valued.
6. The method of claim 1 , further comprising:
determining gates that are effective conditions for correlated-gate pairs based on toggle and mismatch activities of the candidate conditional equivalence invariants and the correlated-gate pairs.
7. The method of claim 1 , further comprising:
subsetting the set of candidate conditional equivalence invariants through structural analysis.
8. The method of claim 7 , wherein the structural analysis is based on fan-in overlap between a correlated-gate pair.
9. The method of claim 1 , further comprising:
subsetting the set of candidate conditional equivalence invariants through semantic analysis.
10. A computer program product embodied on a computer readable storage device and including code for conditional sequential equivalence checking of logic designs embodied in netlists, the code, when executed, causing a data processing system to:
create an equivalence-checking netlist over a first netlist and a second netlist, wherein the first netlist is associated with a first logic design and the second netlist is associated with a second logic design, and wherein the conditional sequential equivalence checking includes conditions under which equivalences of the first and second netlists are checked;
derive a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set;
attempt to prove that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate;
remove candidate conditional equivalence invariants that cannot be proven accurate from the set of candidate conditional equivalence invariants;
record the candidate conditional equivalence invariants that have been proven accurate as a set of conditional equivalence invariants; and
complete the conditional sequential equivalence checking of the equivalence-checking netlist using the recorded set of conditional equivalence invariants, wherein the equivalence-checking netlist is stored in the data processing system following the completion of the conditional sequential equivalence checking.
11. The computer program product of claim 10 , wherein the removing employs under-approximate analysis to falsify invalid ones of the candidate conditional equivalence invariants.
12. The computer program product of claim 11 , wherein the removing employs random simulation, a hardware accelerator, or formal/semi-formal search techniques to falsify invalid ones of the candidate conditional equivalence invariants.
13. The computer program product of claim 10 , wherein the equivalence-checking netlist is binary valued.
14. The computer program product of claim 10 , wherein the equivalence-checking netlist is ternary valued.
15. The computer program product of claim 10 , wherein the code, when executed, is further configured to cause the data processing system to:
determine gates that are effective conditions for correlated-gate pairs based on toggle and mismatch activities of the candidate conditional equivalence invariants and the correlated-gate pairs.
16. The computer program product of claim 10 , wherein the code, when executed, is further configured to cause the data processing system to:
subset the set of candidate conditional equivalence invariants through structural analysis.
17. The computer program product of claim 16 , wherein the structural analysis is based on fan-in overlap between a correlated-gate pair.
18. The computer program product of claim 10 , wherein the code, when executed, is further configured to cause the data processing system to:
subset the set of candidate conditional equivalence invariants through semantic analysis.
19. A data processing system configured to perform conditional sequential equivalence checking of logic designs embodied in netlists, the data processing system comprising:
a memory subsystem; and
one or more processors coupled to the memory subsystem, wherein the one or more processors are configured to:
create an equivalence-checking netlist over a first netlist and a second netlist, wherein the first netlist is associated with a first logic design and the second netlist is associated with a second logic design, and wherein the conditional sequential equivalence checking includes conditions under which equivalences of the first and second netlists are checked;
derive a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set;
attempt to prove that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate;
remove candidate conditional equivalence invariants that cannot be proven accurate from the set of candidate conditional equivalence invariants;
record the candidate conditional equivalence invariants that have been proven accurate as a set of conditional equivalence invariants; and
complete the conditional sequential equivalence checking of the equivalence-checking netlist using the recorded set of conditional equivalence invariants, wherein the equivalence-checking netlist is stored in the data processing system following the completion of the conditional sequential equivalence checking.
20. The data processing system of claim 19 , wherein the one or more processors are further configured to:
partition the set of candidate conditional equivalence invariants into subsets, wherein conditional equivalence is applicable between correlated gates in the first and second netlists when neither of the correlated gates in one of the subsets is tristated.