Bounded Model Checking

Bounded Model Checking (BMC) is a SAT-based formal-verification technique. The cited source describes SAT-based methods as a robust solution in formal verification and identifies SAT-based BMC as a prominent technique; it also states that successive performance improvements made BMC suitable for formal verification of larger-scale designs.

Verification model

The source presents the verification setting using a synchronous circuit modeled as a finite-state machine:

M = (I, S, S0, Δ, Λ, O)

where I is the input alphabet, O is the output alphabet, S is a finite set of states, S0 is the set of initial states, Λ is the output function, and Δ is the next-state function. The transition relation is given as:

T(s, s′) = ∃x ∈ B^n : s′ ≡ Δ(x, s)

This model provides the basis for SAT-based bounded reasoning over state transitions.

SAT-based bounded checking

For safety properties of the form f = AG(φ), the cited material explains that the property can be translated into a Boolean function [[f]]t that checks validity at a time point t. The translation is defined so that a satisfying assignment of [[f]]t corresponds to a counterexample of φ. The resulting Boolean function depends on inputs, outputs, and states within a bounded time interval [0, c].

In the interval-property-checking formulation presented alongside the BMC discussion, counterexamples are searched by solving a SAT instance that unrolls the transition relation across a bounded interval and connects it to one instantiation of the property formula:

∧ T(st+i, st+i+1) ∧ [[f]]t, for i = 0 ... c.

Relationship to interval property checking

The cited source explicitly contrasts interval property checking (IPC) with original BMC. It states that IPC uses an arbitrary starting state, whereas original BMC uses the initial state. Under IPC, a property that holds from an arbitrary state also holds from any reachable state, enabling exhaustive verification for that property. The same passage notes that IPC can produce false negatives when counterexamples start in unreachable states, and that invariants are added to restrict the starting state.