US 8,527,922 B1 · Method and system for optimal counterexample-guided proof-based abstraction

Abstract

A computer-implemented method includes receiving an input containing a candidate netlist, a target, and a number, K, of cycles of interest, where K represents a number of cycles required to be analyzed for the proof-based abstraction. In response to receiving the inputs, a computing device builds an inductively unrolled netlist, utilizing random, symbolic initial values, for K cycles and provides the unrolled netlist with a first initial value constraint to a satisfiability (SAT) solver, with the first initial value constraint empty. The method includes determining whether a result of the SAT solver is satisfiable, and in response to the result not being satisfiable, performing an abstraction on the netlist and outputting the abstraction. However, in response to the result being satisfiable, the method includes performing one of: (a) outputting a valid counterexample of the original netlist; and (b) lazily adding initial value constraints to avoid spurious counterexamples.

Claims23

Dependent claims

A computer-implemented method for performing proof-based abstraction via a computing device, the method comprising:

receiving an input containing a candidate netlist (N1), a target (T1), 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.

7 more elements

A computing device for performing proof-based abstraction, the computing device comprising a processor, an input device, an output device, and a memory with program code that is executed by the processor to cause the computing device to:

receive an input containing a candidate netlist (N1), a target (T1), 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, build an inductively unrolled netlist, utilizing random, symbolic initial values, for K cycles;
provide the unrolled netlist with a first initial value constraint to a satisfiability (SAT) solver where the first initial value constraint is empty;
receive a result of the SAT solver;
determine whether the result of the SAT solver is satisfiable;
in response to the result of the SAT solver not being satisfiable, perform an abstraction on the netlist and outputting the abstraction;
and
in response to the result of the SAT solver being satisfiable, perform one of:
(a) outputting a valid counterexample of the original netlist;
and (b) lazily adding initial value constraints to avoid spurious counterexamples.

7 more elements

A computer program product for performing proof-based abstraction, the computer program product comprising:

a computer readable device;
and
program code on the computer readable device, which program code is configured to be executed by a processor within a computing device to cause the computing device to:
receive an input containing a candidate netlist (N1), a target (T1), 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, build an inductively unrolled netlist, utilizing random, symbolic initial values, for K cycles;
provide the unrolled netlist with a first initial value constraint to a satisfiability (SAT) solver where the first initial value constraint is empty;
receive a result of the SAT solver;
determine whether the result of the SAT solver is satisfiable;
in response to the result of the SAT solver not being satisfiable, perform an abstraction on the netlist and outputting the abstraction;
and
in response to the result of the SAT solver being satisfiable, perform one of:
(a) outputting a valid counterexample of the original netlist;
and (b) lazily adding initial value constraints to avoid spurious counterexamples.

10 more elements

Dependencies are inferred from the claim text.

Method and system for optimal counterexample-guided proof-based abstraction

Life of this patent

Method and system for optimal counterexample-guided proof-based abstraction

Life of this patent

Abstract

Claims23