SAT-Based Bounded Model Checking

Bounded Model Checking (BMC) has been gaining ground as a falsification engine, mainly due to its improved scalability compared to other formal techniques. In BMC, the focus is on finding counterexamples (bugs) of a bounded length

k

. For a given design and correctness property, the problem is translated effectively to a propositional formula such that the formula is true if and only if a counterexample of length

k

exists [66, 67]. Such a translation basically involves unrolling the circuit of the transition relation for the required number of time frames as illustrated in Figure 5.1 (with

k

=

d

). Essentially,

d

copies of circuit are made and then clauses are built at each time frame for the unrolled circuit and the property to be checked, which is then fed to a SAT-solver. In practice, the bound

k

can be increased incrementally to find the shortest counterexample. A separate reasoning is needed to ensure completeness when no counterexample can be found up to a certain bound [66, 67]. However, with increasing depth the problem size, comprising the unrolled circuit and translated property, grows linearly [111] with the size of the model, thereby the making the Boolean reasoning increasingly difficult for large bounds, in general. The standard translation for these properties is

monolithic

, i.e., the entire propositional formula is generated for a given

k

and then the formula is checked for satisfiability using a standard SAT solver.