Patent Document ID: 20110093824
Application ID: 12580373
Patent Flag: 0

Claim One:
1. A method for conditional sequential equivalence checking of logic designs embodied in netlists using a data processing system, comprising: creating 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 a set of candidate conditional equivalence invariants for each correlated gate in a correlated gate pair set; attempting to prove that each candidate conditional equivalence invariant in the set of candidate conditional equivalence invariants is accurate; removing candidate conditional equivalence invariants that cannot be proven accurate from the set of candidate conditional equivalence invariants; recording the candidate conditional equivalence invariants that have been proven accurate as a set of conditional equivalence invariants; and completing the conditional sequential equivalence checking of the equivalence-checking netlist using the recorded set of conditional equivalence invariants.