Overview
Bounded model checking (BMC) is a hardware and software verification technique that limits its analysis to a fixed number of execution steps. Rather than exploring the full reachable state space, BMC checks whether any counterexample to a property exists within a finite bound [arxiv:0710.4629].
How BMC Works
In the hardware setting, BMC works by unrolling a bounded number of circuit steps into one large SMT query. The unrolled query is then passed to an SMT solver such as Z3, and satisfiability of the query corresponds to the existence of a counterexample within the chosen bound [1].
Because BMC reduces model checking to a sequence of satisfiability problems, the formulation of those problems is typically expressed in SMT-LIB, the standard interchange format for SMT solvers. This makes BMC tightly coupled with advances in SMT solver technology, in particular solvers like Z3 [007d4713-fff9-457f-963a-ee09c3491124, 91532559-482e-4d7c-96dd-390c79237ffc].
SAT- and QBF-Based Variants
Classical BMC algorithms encode the unrolled transition relation as a propositional formula and check it with a SAT solver. While effective, this encoding can suffer from a potential memory explosion because the transition relation must be repeatedly unrolled [arxiv:0710.4629].
An alternative formulation uses Quantified Boolean Formulae (QBF), which can represent BMC instances more succinctly because it avoids the explicit unrolling of the transition relation. QBF-based BMC has not been as widely adopted, historically because of the lack of efficient general-purpose QBF decision procedures, and specialized decision procedures have been developed to evaluate it on industrial benchmarks [arxiv:0710.4629].
Tool Support
SymbiYosys is a popular open-source hardware verification front-end that supports several solver backends. Several of its backends, including the built-in Yosys-SMTBMC engine, verify properties using BMC, passing the resulting SMT queries to a backend solver [1]. SymbiYosys also relies on the Yosys synthesis suite, which it shares with other push-button verification systems [2].
A foundational reference for the technique is Biere's chapter "Bounded Model Checking" in the Handbook of Satisfiability (volume 185 of Frontiers in Artificial Intelligence and Applications, 2009) [2].
Optimizations and Counterexample Discovery
Because BMC scales with the unrolling bound, a number of techniques have been proposed to reduce the cost of finding counterexamples. One approach adapts ideas from software testing by running BMC in parallel over versions of the system in which features have been randomly disabled. Adding such constraints to the BMC problem can shrink the verification instance and dramatically decrease the time required to find a counterexample; if no counterexample is found, the partial verification results are still useful in practice [arxiv:1610.08020].
Limitations Inherited From the Encoding
BMC, as implemented in tools such as SymbiYosys, encodes execution directly into the solver query. This makes such implementations less effective than symbolic-execution-based approaches for reasoning across many cycles of execution [1]. Additionally, because BMC only checks a finite bound, it cannot on its own establish unbounded correctness; complementary techniques such as property-directed reachability and k-induction are typically required to extend its guarantees [2].