Bounded Model Check

Concept

Bounded Model Check (BMC) is a formal verification technique that checks whether a finite-state transition system satisfies a property by exploring executions up to a configurable depth bound. It is widely used in hardware verification tools, including the riscv-formal framework for verifying ISA compliance of RISC-V processors.

First seen 6/7/2026

Last seen 6/7/2026

Evidence 3 chunks

Wiki v1

WIKI

Bounded Model Check

Bounded Model Check (BMC) is a formal verification technique in which a system model and a property are translated into a formula whose satisfiability corresponds to the existence of a counterexample within a bounded number of execution steps. Unlike unbounded model checking, which seeks to prove properties for all possible executions, BMC limits its search to executions of length up to a chosen bound, known as the depth or k.

General approach

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

1 connections

riscv-formal ← uses 97% 1e

riscv-formal supports setting up tests as bounded model checks

LINKED ENTITIES

1 links

riscv-formal USES Extracted graph relationship

CITATIONS

11 sources

11 citations — click to expand

[1] Bounded Model Checking uses SAT methods to check the satisfiability of Boolean formulae obtained by unrolling the transition relation of the system up to a bound. Space-Efficient Bounded Model Checking

[2] BMC can be formulated using Quantified Boolean Formulae (QBF), which can give an exponentially more succinct representation because no unrolling of the transition relation is required. Space-Efficient Bounded Model Checking

[3] Bounded Model Checking has been applied to software models expressed in first-order relational modelling languages such as Alloy, including for the verification of reactive behaviour specified in temporal logic. Bounded Model Checking of Temporal Formulas with Alloy

[4] In riscv-formal, the `[options]` section of the `genchecks.py` config supports a `mode` option that can be set to `bmc` (Bounded Model Check, the default) or `prove` (unbounded verification). Verification procedure - RISC-V Formal documentation

[5] Many riscv-formal tests, depending on the strength of safety properties in the core, may be set up as bounded model checks or as unbounded verification tasks. Verification procedure - RISC-V Formal documentation

[6] In riscv-formal, the `csrw` and `csr_ill` checks take a single depth value, the maximum depth of the Bounded Model Checker; `csrc_*` checks take two values (reset cycles and BMC depth); the `[depth]` section is required for a check to run. Verification procedure - RISC-V Formal documentation

[7] The riscv-formal Liveness check uses a BMC: it assumes an instruction is retired at a configurable trigger point in the middle of the bounded model check and verifies that the next instruction is also retired within the BMC span. Verification procedure - RISC-V Formal documentation

[8] The riscv-formal Uniqueness check uses a BMC parameterised by reset cycles, trigger depth, and execution depth, to ensure that no two instructions with the same `rvfi_order` are retired. Verification procedure - RISC-V Formal documentation

[9] The riscv-formal Faults, Cover, and Causality (`causal`, `causal_mem`, `causal_io`) checks are each parameterised as bounded model checks with reset-cycles and execution-depth values; the Cover check additionally collects bounds information and can produce witness traces. Verification procedure - RISC-V Formal documentation

[10] The riscv-formal `cover` check is a formal check using `cover()` SystemVerilog statements for various RVFI events or sequences of events; it is a BMC whose purpose is to collect data about the required bounds to reach certain states, which can then be used to set the bounds of the other bounded model checks, and to create witness traces. Verification procedure - RISC-V Formal documentation

[11] The riscv-formal `bus_imem` standard bus check is implemented using a single-word read-only unconstrained memory abstraction, parameterised as a bounded model check with reset cycles and execution depth. Verification procedure - RISC-V Formal documentation