bounded model checking

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, reducing model checking to a sequence of satisfiability queries discharged to SAT, QBF, or SMT solvers. It is used in hardware verification frameworks such as riscv-formal and SymbiYosys, in C program model checkers such as CBMC, in specialized workflows for HW/SW co-verification, fault injection, and SEU reliability evaluation, and as a source of SAT benchmarks used to evaluate SAT sampling tools. Application areas include equivalence checking of mutated C-based instruction-set semantics for test-suite generation.

First seen 6/9/2026

Last seen 9/7/2026

Evidence 19 chunks

Wiki v8

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. 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.

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). 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.

READ FULL ARTICLE →

NEIGHBORHOOD

3 nodes · 2 edges

graph · bounded model checking · depth=1

RELATIONSHIPS

14 connections

CBMC ← implements 100% 3e

CBMC implements bounded model checking for C programs.

μARCHIFI ← uses 100% 2e

μARCHIFI uses bounded model checking for verification.

Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking ← uses 100% 2e

The paper uses bounded model checking to check equivalence between original and mutated semantics.

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.

UniGen ← evaluates 90% 1e

UniGen was experimentally evaluated on benchmarks from bounded model checking.

riscv-formal ← implements 90% 1e

riscv-formal supports bounded model checking via the RISCV_FORMAL_CHECK_CYCLE macro.

On Parallel Scalable Uniform SAT Witness Generation ← uses 100% 1e

The paper uses constraints from bounded model checking as evaluation benchmarks.

HW/SW Co-Verification using Bounded Model Checking (Große et al., 2006) ← uses 95% 1e

The HW/SW Co-Verification paper uses bounded model checking as its core technique.

state-space explosion mentions → 90% 1e

Bounded Model Checking is used to address the state space explosion problem.

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.

LINKED ENTITIES

2 links

Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking USES Extracted graph relationship

CBMC IMPLEMENTS Extracted graph relationship

CITATIONS

11 sources

11 citations — click to expand

[1] BMC checks whether any counterexample to a property exists within a finite bound, reducing model checking to a sequence of satisfiability queries discharged to SAT/SMT solvers. Minimal Stimuli Generation in Simulation-based Verification

[2] BMC works by unrolling a bounded number of circuit steps into one large SMT query whose satisfiability corresponds to the existence of a counterexample within the chosen bound. Defining macros - RISC-V Formal documentation

[3] CBMC is a bounded model checker for C programs that converts C programs into logical models expressed in SMT-LIB and discharges assertions using SAT/SMT solvers, producing a counterexample trace when an assertion fails. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking

[4] riscv-formal supports bounded model checking via the RISCV_FORMAL_CHECK_CYCLE macro (defining the cycle number in which checks are performed, equal to the solver depth) and unbounded model checking via the separate RISCV_FORMAL_UNBOUNDED macro. Defining macros - RISC-V Formal documentation

[5] BMC-of-circuits CNF instances (together with SMTLib, program-synthesis, and ISCAS89 benchmarks) are used in the UniGen experimental evaluation as standard SAT-sampling workloads. Balancing Scalability and Uniformity in SAT Witness Generator

[6] BMC underlies the equivalence-checking stage of mutation-based test-suite generation pipelines by comparing mutated and original C semantics and yielding counterexamples whose input/output pairs are added to the test suite. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking

[7] Equivalence checking is undecidable in general, but instruction-set semantics are usually simple, perform bitwise manipulations on fixed-size inputs, and any loops are almost always bounded, reducing the problem to checking equivalence of small, straight-line programs. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking

[8] In mutation-based test-suite generation, the mutation score (killed mutations divided by total mutations) measures the effectiveness of the existing test suite, with values close to 1.0 indicating high resilience to detecting bugs; mutants are generated in a single invocation and tested in parallel. Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking

[9] Große, Kühne, and Drechsler apply BMC in HW/SW Co-Verification of Embedded Systems using Bounded Model Checking (ACM Great Lakes Symposium on VLSI, 2006) and in Analyzing functional coverage in bounded model checking (IEEE Trans. on CAD, 27(7):1305–1314, 2008). Minimal Stimuli Generation in Simulation-based Verification

[10] BMC is widely used in HW/SW co-verification, fault injection, and SEU reliability evaluation, and is popular because it reduces state-space exploration to a finite prefix while scaling well to large industrial designs. Minimal Stimuli Generation in Simulation-based Verification

[11] The origin of BMC as a symbolic model checking technique without BDDs is Biere, Cimatti, Clarke, and Zhu, 'Symbolic model checking without BDDs' (TACAS, 1999). Minimal Stimuli Generation in Simulation-based Verification