Verifying one or more properties of a design using SAT-based BMC
AssigneeFujitsu Limited
InventorMukul R. Prasad
Life of this patent
Estimating the term…
Abstract
In one embodiment, a method for satisfiability (SAT)-based bounded model checking (BMC) includes isolating information learned from a first iteration of an SAT-based BMC process and applying the isolated information from the first iteration of the SAT-based BMC process to a second iteration of the SAT-based BMC process subsequent to the first iteration.
Claims12
Logic for circuit verification, the logic encoded in one or more media for execution using one or more processors and when executed operable to:
- access a logic-level description of a circuit generated from a register transfer (RI)-level description of the circuit;
- apply logic optimization to the logic-level description to simplify the logic-level description for satisfiability (SAT)-based bounded model checking (BMC) of the circuit using the logic-level description to generate a simplified logic-level description;
- verify the circuit by (i) performing a first iteration of a SAT-based BMC process on the simplified logic-level description;
- (ii) isolating information learned from the first iteration of the SAT-based BMC process;
- and (iii) applying the isolated information from the first iteration of the SAT-based BMC to a second iteration of the SAT-based BMC process subsequent to the first iteration;
- and
- communicate the results of the circuit verification to a user.
Logic for circuit design verification, the logic encoded in one or more media for execution using one or more processors and when executed operable to:
- receive the design of a circuit;
- determine a variable order for an iteration of a satisfiability (SAT)-based bounded model checking (BMC) process according to a variable-ordering algorithm specific to BMC;
- verify the circuit design by:
- (i) performing a first iteration of the SAT-based BMC process on the circuit design;
- (ii) isolating information learned from a the first iteration of the SAT-based BMC process;
- and (iii) applying the isolated information from the first iteration of the SAT-based BMC process to a second iteration of the SAT-based BMC process subsequent to the first iteration;
- and
- communicating the results of the circuit verification to a user.
Dependencies are inferred from the claim text.