Patent ID: 8527922

Claim:
A computer-implemented method for performing proof-based abstraction via a computing device, the method comprising: receiving an input containing a candidate netlist (N 1 ), a target (T 1 ), and a number, K, of cycles of interest, wherein K is an integer number that represents a number of cycles that are required to be analyzed for the proof-based abstraction; in response to receiving the inputs, building, by a processor of the computing device, an inductively unrolled netlist, utilizing random, symbolic initial values, for K cycles; providing the unrolled netlist with a first initial value constraint to a satisfiability (SAT) solver where the first initial value constraint is empty; receiving a result of the SAT solver; determining whether the result of the SAT solver is satisfiable; in response to the result of the SAT solver not being satisfiable, performing an abstraction on the netlist and outputting the abstraction; and in response to the result of the SAT solver being satisfiable, performing one of: (a) outputting a valid counterexample of the original netlist; and (b) lazily adding initial value constraints to avoid spurious counterexamples.