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.
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. 3. The method of claim 1 , wherein the abstracted logic includes a multiplexor.