Skip to content
STIMSMITH

Bounded Model Check

Concept WIKI v1 · 6/7/2026

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.

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

In its classical formulation, BMC unrolls the transition relation of the system for k steps and asks a SAT solver whether the resulting formula, conjoined with the negated property, is satisfiable. A satisfying assignment corresponds to a concrete counterexample trace of length at most k; if the formula is unsatisfiable, no counterexample exists within that bound (but the property may still be violated at greater depths).

BMC can also be formulated in terms of Quantified Boolean Formulae (QBF). QBF-based encodings can yield exponentially more succinct formulae than the unrolled transition-relation approach, at the cost of requiring an efficient QBF decision procedure. Industrial benchmarks have been used to compare SAT-based, general-purpose-QBF, and special-purpose QBF approaches in BMC.

Beyond hardware, BMC has been applied to software models expressed in first-order relational modelling languages such as Alloy, where it can be combined with temporal logic to specify and verify reactive behaviour.

Use in riscv-formal

The riscv-formal framework uses Bounded Model Checking as one of its two primary solver modes. The verification mode is selected in the [options] section of the genchecks.py configuration file:

Option Value Description
mode bmc Bounded Model Check (default).
mode prove Unbounded verification.

For most riscv-formal checks, a [depth] section specifies the parameters of the BMC run. The interpretation of the depth values depends on the check:

  • Two values (e.g. csrw, csr_ill, csrc_*, cover, bus_imem, causal*, faults): the first value is the number of cycles to hold reset for, and the second value is the maximum execution depth of the BMC.
  • Three values (e.g. liveness, uniqueness): the first value is the reset-cycles count, the second is the trigger depth at which an instruction is required to be retired, and the third is the execution depth of the BMC span.

Checks typically run as BMC

The following riscv-formal checks are commonly configured as bounded model checks. The choice between BMC and unbounded verification depends on factors such as the strength of safety properties present in the core, the overall complexity of the design, and the verification requirements of the application.

  • Instruction and CSR checks — csrw (CSR read/write instruction behaviour), csr_ill (illegal CSR access), and the csrc_* consistency checks (csrc_const, csrc_zero, csrc_hpm, csrc_any).
  • Causality checks — causal, causal_mem, and causal_io, which verify that out-of-order retirement preserves causality for registers, memory, and I/O memory respectively. The I/O memory region is selected via the RISCV_FORMAL_IOADDR(addr) macro.
  • Liveness check — Ensures the core never freezes, by requiring that an instruction retired at a configurable trigger depth is followed by a later-retired instruction within the BMC span. Bounded fairness constraints may need to be added to the design for this check to succeed.
  • Uniqueness check — Ensures that no two instructions with the same rvfi_order are retired.
  • Faults check — Verifies that dynamically occurring memory faults are handled correctly, using the RISCV_FORMAL_MEM_FAULT macro and the rvfi_mem_fault* signals.
  • Cover check — A BMC that uses cover() SystemVerilog statements to collect data about the bounds required to reach certain states, helping to set bounds for the other bounded model checks. It can also be used to produce witness traces, for instance to examine the conditions under which a specific CSR bit goes high.
  • Standard bus checks — E.g. the bus_imem instruction-bus memory check, which adds a single-word, read-only, unconstrained memory abstraction.

Role of the Cover check

The cover check has a special role in the riscv-formal workflow. Because BMC results are only valid up to the configured depth, the user must pick bounds large enough to expose interesting behaviour. The cover check is run as a BMC whose purpose is to discover the depths at which various RVFI events and event sequences become reachable. These discovered bounds can then be transferred to the other checks so that their BMCs are not only correct but also meaningful.

See also

  • riscv-formal — A verification framework that uses Bounded Model Checking (among other techniques) for ISA-compliance checking of RISC-V cores.

LINKED ENTITIES

1 links
riscv-formal USES

CITATIONS

11 sources
11 citations
[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