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.

How BMC Works

In the hardware setting, BMC works by unrolling a bounded number of circuit steps into one large SMT query. The unrolled query is then passed to an SMT solver, and satisfiability of the query corresponds to the existence of a counterexample within the chosen bound. µArchiFI formalizes this as Algorithm 1 (BMC_Concretizing), which initializes a formula φ with the initial state s₀, then iteratively appends the transition relation φ ← φ ∧ (sᵢ = T(sᵢ₋₁, xᵢ₋₁)) until either the property φ is reached at some step i (in which case a counterexample path is returned) or the bound is reached.

Because BMC reduces model checking to a sequence of satisfiability problems, the formulation of those problems is typically expressed in SMT-LIB, the standard interchange format for SMT solvers. This makes BMC tightly coupled with advances in SMT solver technology. For example, the EPEX processor-verification pipeline uses CBMC to translate a C description of an ISA into an SMT-LIB v2.0 instance, which is then handed to Z3. µArchiFI likewise emits the faulty transition system in SMT-LIB or BTOR2 format for consumption by external model checkers.

SAT- and QBF-Based Variants

Classical BMC algorithms encode the unrolled transition relation as a propositional formula and check it with a SAT solver. While effective, this encoding can suffer from a potential memory explosion because the transition relation must be repeatedly unrolled. The µArchiFI paper notes that solving the unrolled formula φ "suffers from the increasing number of variables and clauses" as more transitions are added.

An alternative formulation uses Quantified Boolean Formulae (QBF), which can represent BMC instances more succinctly because it avoids the explicit unrolling of the transition relation. QBF-based BMC has not been as widely adopted, historically because of the lack of efficient general-purpose QBF decision procedures, and specialized decision procedures have been developed to evaluate it on real-life industrial benchmarks.

BMC as a Source of SAT Instances

BMC of circuits is a common source of CNF SAT benchmarks used to evaluate auxiliary SAT-based tools. In the experimental evaluation of the UniGen near-uniform SAT witness generator, the public-domain benchmarks included bit-blasted versions of constraints arising in bounded model checking of circuits (used in prior work [5] of that paper), alongside bit-blasted SMTLib benchmarks, constraints from automated program synthesis, and ISCAS89 circuits with parity conditions on randomly chosen subsets of outputs and next-state variables. This positions BMC-derived CNFs as a standard workload for assessing SAT sampling techniques such as UniGen, which is intended for evaluating BMC among other applications.

BMC and State-Space Explosion

State-space explosion is an inherent problem of model checking: analyzing an entire system exhaustively is computationally expensive and may be impractical for large systems. BMC is used as an alternative precisely because it can reduce the state space effectively. It is considered an acceptable and popular technique for two main reasons:

• Efficiency: it reduces the state space by examining only a finite prefix of execution traces, rather than exploring the full reachable state space.
• Scalability: scaling model checking to large designs remains a challenge, and BMC has been found promising in finding deep vulnerabilities in industrial designs and scales well with size.

It might be argued that since BMC cannot cover the whole state space, it cannot guarantee completeness; however, researchers have shown that completeness can be guaranteed with an appropriate threshold, so that an Undetermined result is acceptable in many cases. The µArchiFI paper similarly justifies bounded over unbounded verification for fault-injection analysis because, while unbounded techniques prove the property in the general case, the data dependencies and transient nature of faults make them ill-suited to the fault-injection problem.

Tool Support

riscv-formal is a formal verification framework for RISC-V cores. It supports both bounded and unbounded model checking: the RISCV_FORMAL_CHECK_CYCLE macro defines the cycle number in which checks are performed, and "for bounded model checking, this should be the solver depth," while the separate RISCV_FORMAL_UNBOUNDED macro is used to indicate that unbounded model checking is being used. Other riscv-formal macros (such as RISCV_FORMAL_FAIRNESS for liveness/hang checks and RISCV_FORMAL_RESET_CYCLES for the reset length) configure the surrounding testbench that the bounded or unbounded model checker exercises.

SymbiYosys is a popular open-source hardware verification front-end that supports several solver backends. Several of its backends, including the built-in Yosys-SMTBMC engine, verify properties using BMC, passing the resulting SMT queries to a backend solver. SymbiYosys also relies on the Yosys synthesis suite, which it shares with other push-button verification systems. µArchiFI's modeling and fault-injection passes are likewise integrated into the Yosys toolchain, and µArchiFI uses the SystemVerilog Assertion subset supported by Yosys to encode the attacker's goal into the hardware design.

A foundational reference for the technique is Biere's chapter "Bounded Model Checking" in the Handbook of Satisfiability (volume 185 of Frontiers in Artificial Intelligence and Applications, 2009). The origin of BMC as a symbolic model checking technique without BDDs is the seminal paper "Symbolic model checking without BDDs" by Biere, Cimatti, Clarke, and Zhu (1999).

CBMC is a model checker for C programs that compiles bounded unwinding of a C program into an SMT-LIB instance suitable for backend solvers such as Z3. CBMC converts C programs into logical models expressed in SMT-LIB and discharges assertions about the C program using existing SAT/SMT solvers; when an assertion fails, CBMC produces a trace of a program execution that causes the failure, from which input values and the corresponding output can be extracted.

PONO is an SMT-based model checker that µArchiFI invokes as one of several external verification backends on the emitted transition system. In µArchiFI's fault-injection experiments on RISC-V use cases, PONO was reported to be faster than the alternatives on the fault-free model-checking problem of Use Case I and was able to solve fault-injected variants of all three use cases where some other tools timed out.

µArchiFI is an open-source tool dedicated to the formal modeling and verification of microarchitecture-level fault injections and their effects on hardware/software systems. µArchiFI models the system under attack as a transition system M_F = (S, S₀, X, T), with S₀ describing possible software execution paths and X controlling the attacker's fault-injection choices, and reduces fault-injection security to a BMC reachability problem with bound k. A path (s₀, …, s_k) in this transition system allows an attacker to identify both the fault-injection instance and the software execution trace that satisfies the attacker goal φ.

UniGen is a near-uniform SAT witness generator whose experimental evaluation explicitly uses bit-blasted BMC-of-circuits CNF instances (together with SMTLib, program-synthesis, and ISCAS89 benchmarks) as part of its public benchmark suite, making BMC a representative input workload for the tool.

BMC for HW/SW Co-Verification

BMC is used for hardware/software co-verification of embedded systems. 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 the same authors extend the analysis in "Analyzing functional coverage in bounded model checking" (IEEE Trans. on CAD, 27(7):1305–1314, 2008), which is cited in the stimulus-generation literature as a treatment of functional coverage analysis in BMC. Both works are cited as prior art on coverage analysis in BMC.

BMC for SEU Reliability Evaluation

BMC has been applied to evaluate the reliability of hardware against Single Event Upsets (SEUs). In the SEU-evaluation workflow applied to the RISC-V Ibex core, the formal method exhaustively searches the state space and the full fault list for faults that may cause Silent Data Corruptions (SDCs), crashes, or hangs. Compared to fault injection, the advantages of this approach are exhaustive search and backward tracing of faults, while the inherent limitation is state-space explosion, which cannot be avoided in complex designs. The workflow classifies faults according to their effects: faults whose corresponding assertion is Proven are deemed safe SEUs, while faults whose assertion is Failure yield a counterexample and are deemed crucial SEUs (vulnerable bits).

Because BMC only explores a bounded prefix of execution, there is a trade-off between the permitted model-checking time and the number of Undetermined results: with a longer bounded model-checking time, the number of Undetermined results can be minimized, but reducing that number to zero requires an indeterminate amount of time, which is unlikely to be worthwhile. Future work in this line includes extending the method from SEUs to Double Event Upsets and investigating approaches to mitigate state-space explosion.

Use Inside Symbolic Quick Error Detection (SQED)

Symbolic Quick Error Detection (SQED), the symbolic pre-silicon form of Quick Error Detection (QED), uses BMC as its underlying engine when checking that two executions of an instruction sequence, fed matching inputs, produce matching outputs. In practice this means performing a single-instruction BMC check for every instruction on the core. SQED imposes practical restrictions on this check, such as splitting the register file in half so that one half holds the original instructions and the other holds the duplicated sequence, which prevents tests from using the full register range.

BMC for Equivalence Checking and Test-Suite Generation

BMC underlies equivalence checking of two C programs by unwinding both programs for a bounded number of steps and asserting their outputs are equal across all non-deterministic inputs; when the assertion fails, the BMC counterexample yields input values that distinguish the implementations. This equivalence-checking use of BMC is the engine of mutation-based test-suite generation pipelines in which a mutation engine produces buggy variants of a formal (executable) semantics expressed as C, and a bounded model checker compares each variant to the original semantics. When the two are not equivalent, the counterexample is added to the test suite as a distinguishing input–output pair, and the resulting inputs can be used to drive an oracle that produces expected outputs.

This pattern has been applied to instruction-set semantics — for example, NVIDIA's PTX — where the semantics of an instruction such as add.rm.ftz.sat.f32 is written as a C program and buggy mutants are checked for equivalence with the original using CBMC. Equivalence checking is undecidable in general, but several properties of instruction-set semantics make it tractable in practice: the semantics are usually simple, perform bitwise manipulations on fixed-size inputs, and any loops are almost always bounded, so that the problem reduces to checking the equivalence of small, straight-line programs.

In mutation-and-equivalence pipelines, only mutants that pass all existing tests and survive move on to the equivalence-checking stage, after which the mutation score — the number of killed mutations divided by the total number of mutations — measures the effectiveness of the existing test suite, with values close to 1.0 indicating high resilience to detecting bugs. The mutants themselves can be generated in a single invocation and then tested in parallel as a collection of independent tasks. Because BMC only explores bounded traces, the check typically ranges over all possible (non-deterministic) values of uninitialized inputs in the equivalence harness, ensuring that the assertion holds across the full input domain supported by the semantics.

Optimizations and Counterexample Discovery

Because BMC scales with the unrolling bound, a number of techniques have been proposed to reduce the cost of finding counterexamples. One approach adapts ideas from software testing by running BMC in parallel over versions of the system in which features have been randomly disabled. Adding such constraints to the BMC problem can shrink the verification instance and dramatically decrease the time required to find a counterexample; if no counterexample is found, the partial verification results are still useful in practice.

The µArchiFI paper introduces two complementary state-space reduction techniques that both add terms and clauses to the unrolled BMC formula:

• Sandboxing restricts the Program Counter (PC) to a range of values that a static analysis (e.g., an objdump-like tool) can derive from the binary, eliminating software execution paths that cannot occur under fault injection. In µArchiFI, sandboxing is implemented by constraining the PC of the decode stage of in-order processors. Adding such a global constraint, however, may lose the k-completeness of the bounded verification procedure; sandboxing is therefore recommended for vulnerability exploration rather than for proving robustness.
• Concretization splits the unrolled formula φ into sub-formulas encoding different software execution paths. µArchiFI's BMC_Concretizing procedure (Algorithm 1) first runs BMC up to a concretization depth m, then enumerates possible PC values returned by the SMT solver up to a limit L, running a separate bounded verification for each concretized PC up to bound k. If the PC enumeration is incomplete, the remaining paths are encoded in a single follow-up BMC call.

Space-Efficient QBF-Based BMC

Because classical SAT-based BMC requires repeatedly unrolling the transition relation and can therefore suffer from a potential memory explosion, an alternative approach encodes BMC instances as Quantified Boolean Formulae (QBF), allowing an exponentially more succinct representation because no explicit unrolling of the transition relation is required. QBF-based BMC has historically been limited by the lack of efficient decision procedures, but specialized QBF decision procedures tailored for BMC have been developed and evaluated against general-purpose SAT and QBF solvers on real-life industrial benchmarks.

Limitations Inherited From the Encoding

BMC, as implemented in tools such as SymbiYosys, encodes execution directly into the solver query. This makes such implementations less effective than symbolic-execution-based approaches for reasoning across many cycles of execution. Additionally, because BMC only checks a finite bound, it cannot on its own establish unbounded correctness; complementary techniques such as property-directed reachability and k-induction are typically required to extend its guarantees. The riscv-formal framework provides a parallel RISCV_FORMAL_UNBOUNDED configuration alongside its bounded mode to support such complementary analyses. SQED inherits these scalability considerations, and the EPEX authors observe that formal approaches in general—while able to provide correctness guarantees—are significantly harder to use than simulation-based methods and should be complemented by simulation-based verification.

In the fault-injection setting, µArchiFI explicitly justifies choosing bounded over unbounded verification: unbounded techniques prove the property in the general case, but the data dependencies and transient nature of faults make them ill-suited to the fault-injection problem. µArchiFI's experimental evaluation reports that, on the same RISC-V use cases, PONO was generally faster than Yosys-BMC and BTORMC on fault-free verification and was the only solver able to solve fault-injected variants of all three use cases within the time budget, while BTORMC timed out on the fault-injected Use Case II. In the SEU-evaluation setting, state-space explosion is acknowledged as an inherent problem of formal verification and a key limitation when applying BMC to complex designs.