Bounded Model Checking
ConceptBounded model checking (BMC) is a formal verification technique that checks whether a system violates a property within a bounded number of execution steps by unrolling those steps into a single satisfiability query and discharging it to an SAT or SMT solver. It underlies the verification backends of open-source hardware tools such as SymbiYosys and has been the subject of optimization work targeting memory usage and counterexample discovery.
First seen 6/9/2026
Last seen 6/9/2026
Evidence 2 chunks
Wiki v1
WIKI
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
NEIGHBORHOOD
3 nodes · 2 edgesgraph · bounded model checking · depth=1
RELATIONSHIPS
2 connectionsSymbiYosys uses bounded model checking via its Yosys-SMTBMC backend.
Bounded model checking unrolls circuit steps into an SMT query using SMT-LIB encoding.
LINKED ENTITIES
2 linksCITATIONS
8 sources8 citations — click to expand
[1] BMC unrolls a bounded number of circuit steps into one large SMT query, which is then passed to an SMT solver such as Z3 to determine satisfiability. rtlv: push-button verification of software on hardware
[2] SymbiYosys is a popular open-source hardware verification tool, and several of its backends (including Yosys-SMTBMC) verify properties using bounded model checking. rtlv: push-button verification of software on hardware
[3] A canonical reference for BMC is A. Biere, 'Bounded Model Checking,' in the Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, 2009. rtlv: push-button verification of software on hardware
[4] Z3 is an efficient SMT solver used in verification toolchains. rtlv: push-button verification of software on hardware
[5] Traditional SAT-based BMC can suffer from a potential memory-explosion problem because the transition relation is unrolled. Space-Efficient Bounded Model Checking
[6] QBF-based BMC can represent formulae more succinctly because it avoids unrolling the transition relation, but its adoption has been limited by the lack of efficient QBF decision procedures. Space-Efficient Bounded Model Checking
[7] Randomly disabling features and running BMC in parallel over the resulting variants can shrink the verification problem and speed up counterexample discovery, while still providing useful partial verification results when no counterexample is found. Bounded Model Checking and Feature Omission Diversity
[8] BMC encodings that pass execution directly to the solver query are less effective than symbolic-execution-based approaches for reasoning about many cycles of execution. rtlv: push-button verification of software on hardware