Patent Document ID: 7996803
Application ID: 12362513

Base Claim:
1. A method for sequential equivalence checking of two netlists, the method comprising: a processor executing program instructions to perform the functions of: (a) receiving a first netlist and a second netlist of an original model, wherein each netlist of the first netlist and the second netlists includes at least one representation of one or more hardware registers coupling a plurality of gates; (b) determining, from netlists of the original model, logic to be abstracted; (c) determining a condition for functional consistency; (d) creating an abstract model by replacing the logic with abstracted logic using one or more uninterpreted functions; (e) performing one or more functions on the abstract model; (f) determining whether or not a counterexample is obtained from said performing the one or more functions on the abstract model; (g) if a counter example is not obtained, determining whether or not a proof is complete; (h) if the proof is complete, reporting that the proof is complete; (i) if the proof is not complete, repeating the method from step (e) using another function on the abstract model, wherein said another function is different from any one or more functions previously used in performing step (e); (j) if a counter example is obtained, determining whether or not the counter example can be transferred onto the original model; (k) if the counter example can be transferred onto the original model, reporting that the counter example can be transferred onto the original model and reporting the counter example; and (l) if the counter example can not be transferred onto the original model: refining the abstraction; and repeating the method from step (e) with the abstract model including the refined abstraction.

---

Claim 4:
4. The method of claim 1 , wherein said determining, from the original model, the logic to be abstracted includes one or more of: determining a first register in the first netlist and a corresponding second register in the second list; determining a first next-state function of the first register; and determining a second next-state function of the second register.