Skip to content
STIMSMITH

Bounded Model Checking

Concept

Bounded Model Checking (BMC) is a hardware and software formal verification technique that restricts analysis to a fixed number of execution steps. It reduces the model-checking problem to a sequence of satisfiability queries discharged to SAT, QBF, or SMT solvers, and is widely used in hardware verification (Yosys-SMTBMC, SymbiYosys), in software model checkers such as CBMC, and in fault-injection and SEU reliability frameworks such as µArchiFI and the Ibex-based evaluation of Single Event Upsets. BMC mitigates the state-space explosion that limits exhaustive model checking, can effectively reduce the state space and scale to large industrial designs, and although it only covers a bounded trace, completeness can be guaranteed with an appropriate threshold so that 'Undetermined' results are often acceptable.

First seen 6/9/2026
Last seen 7/10/2026
Evidence 11 chunks
Wiki v4

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]. In the µArchiFI fault-injection workflow, the BMC bound k is fixed according to the length of the longest program execution trace plus a small safety margin (e.g., a 10-percent increment) to capture possible modifications in the control flow induced by faults [1].

The result of a BMC run can be one of three outcomes: Proven (the assertion is fully proved), Failure (the model checker produces a counterexample), or Undetermined / Bounded Proven (the tool cannot prove or disprove the assertion within the bounded trace or time) [2]. When a counterexample is produced by µArchiFI's external model checker, a VCD file reports precisely where the fault is injected and when the attacker's goal is reached, although understanding the propagation of the fault and its consequences still requires further analysis [3].

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

9 connections
μARCHIFI ← uses 100% 2e
μARCHIFI uses bounded model checking for verification.
Symbolic Quick Error Detection ← uses 100% 1e
SQED leverages bounded model checking for its formal verification checks.
SMT-LIB uses → 85% 1e
Bounded model checking unrolls circuit steps into an SMT query using SMT-LIB encoding.
CBMC ← implements 90% 1e
CBMC is a bounded model checking tool used to transform C programs into SMT-lib instances.
SMT Solver uses → 95% 1e
Bounded model checking uses an SMT solver to enumerate models.
PONO ← uses 95% 1e
PONO is an SMT-based model checker used for bounded model checking.
Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core ← uses 95% 1e
Bounded Model Checking is used as an alternative to full model checking to handle state explosion.
SymbiYosys ← implements 100% 1e
SymbiYosys uses bounded model checking via its Yosys-SMTBMC backend.
state-space explosion mentions → 90% 1e
Bounded Model Checking is used to address the state space explosion problem.

LINKED ENTITIES

2 links
Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core USES Extracted graph relationship
state-space explosion MENTIONS Extracted graph relationship

CITATIONS

11 sources
11 citations — click to expand
[1] BMC reduces model checking to satisfiability queries and can suffer from a potential memory explosion because the transition relation must be repeatedly unrolled. Space-Efficient Bounded Model Checking
[2] Running BMC in parallel over versions of the system in which features have been randomly disabled can shrink the verification instance and dramatically decrease the time required to find a counterexample. Bounded Model Checking and Feature Omission Diversity
[3] In µArchiFI, the BMC bound k is fixed according to the longest program execution trace plus a 10-percent increment to capture possible modifications in the control flow induced by faults. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[4] µArchiFI introduces the BMC_Concretizing algorithm, which initializes φ with the initial state s₀ and iteratively appends the transition relation until the property is reached or the bound is reached. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[5] State-space explosion is an inherent problem of model checking; BMC can reduce the state space effectively and is considered acceptable and popular because of efficiency and scalability to industrial designs. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[6] Although BMC cannot cover the whole state space, completeness can be guaranteed with an appropriate threshold, so 'Undetermined' is an acceptable result in many cases. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[7] The µArchiFI paper explicitly justifies bounded over unbounded verification because the data dependencies and transient nature of faults make unbounded techniques ill-suited to the fault-injection problem. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[8] µArchiFI's experimental evaluation reports PONO was generally faster than Yosys-BMC and BTORMC on fault-free verification and the only solver able to solve fault-injected variants of all three use cases within the time budget, while BTORMC timed out on Use Case II. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[9] A formal method applying bounded model checking to the RISC-V Ibex core can exhaustively search the state space and the full fault list for SEUs that cause SDCs, crashes, or hangs; the inherent limitation is state-space explosion in complex designs. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[10] There is a trade-off between permitted model-checking time and the number of Undetermined results: increasing the bounded model-checking time can reduce Undetermined results, but reducing them to zero requires an indeterminate amount of time that is unlikely to be worthwhile. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core
[11] EPEX uses CBMC to translate a C description of an ISA into an SMT-LIB v2.0 instance, which is then handed to Z3 for BMC-style verification. EPEX: Processor Verification by Equivalent Program Execution