Overview
Binary Decision Diagrams (BDDs) are compact, canonical graph-based encodings of Boolean functions that have become a cornerstone of formal hardware verification, symbolic model checking, logic synthesis, and reactive synthesis. A BDD represents a Boolean function by recursively Shannon-expanding over its input variables and sharing isomorphic sub-graphs, yielding a reduced ordered binary decision diagram (ROBDD) that is canonical for a given variable ordering. This canonicality enables efficient equivalence checking, satisfiability analysis of combinational and sequential circuits, and symbolic image computations in unbounded model checking.
Use in Circuit Verification
Verification is a central task in circuit design, and most general-purpose formal methods exhibit exponential worst-case behavior. Research on Polynomial Circuit Verification using BDDs [arXiv:2104.03024] shows that for circuits with specific structural properties—such as tree-like circuits, or circuits built from multiplexers that are themselves derived from BDDs—complete formal verification can be carried out in polynomial time and space. This result is significant because it identifies a structurally characterized class of circuits for which BDD-based verification escapes the typical exponential blow-up.
The general pattern in BDD-based verification is:
- Encode the circuit's Boolean behavior as a BDD (or a set of BDDs).
- Encode the specification property also as a BDD.
- Apply canonical graph algorithms (e.g., ROBDD equivalence, satisfiability via reachability of the
1-terminal) to check whether the circuit satisfies the property.
When the circuit's BDD size is polynomially bounded, these operations remain tractable, enabling complete rather than bounded verification.
BDDs in Symbolic (State-based) Model Checking
State-based model checking methods reason at the level of sets of states using BDDs for Boolean subformulas and Presburger arithmetic solvers for integer-level subformulas. Given a transition relation T(C, X, C′, X′) over control states C and datapath variables X, and a state set represented as a disjunction of state-disjuncts D_ρ(C, X), symbolic state traversal proceeds by repeated image computations:
Img(D_ρ) = (∃ C, X . T ∧ D_ρ)(X/X′, C/C′)
until a fixpoint is reached [f0a2cbf0]. A frontier set F of unexplored state-disjuncts divides the reachable state space into explored and unexplored parts; the basic frontier-update lemma states that if F is a frontier with respect to an error set B_Err and B_Err ∩ D = ∅, then F \ {D} ∪ {Img(D)} is also a frontier [f0a2cbf0].
State-based methods perform well when state sets have compact representations, but can suffer from memory explosion; stateless methods (e.g., SAT/SMT-based BMC) avoid explicit state-set manipulation at the cost of time-intensive reasoning [cb99461e].
Hybrid Model Checking (HMC)
The HMC framework interleaves state traversal (ST) and path-based reasoning (PR) using a memory bound to switch from ST to PR and a depth/time bound to switch back, repeatedly switching between the two modes to avoid blow-up within any single method. Large frontier state sets are partitioned dynamically based on the number of linear equations (for Presburger arithmetic) and BDD nodes, and ranked to favor processing of states more likely to reach errors [cb99461e]. HMC's highlights include:
- A divide-and-conquer procedure to compute frontier states and represent them efficiently.
- For terminating programs, exhaustive coverage despite not storing the entire reachable state set.
- Abstract interpretation to over-approximate states backward-reachable from error states in k steps.
- Control-state reachability to build simplified transition relations on-the-fly.
The HMC implementation represents and simplifies Boolean formulas using the CUDD library, and Presburger arithmetic formulas using the Omega library [f0a2cbf0].
Polynomial Formal Verification (PFV) Using BDDs
BDDs are the underlying data structure for Polynomial Formal Verification (PFV), a class of techniques that aim to bound verification complexity using BDD-based representations and related symbolic structures. As described in the RISC-V testability survey (hal-05579640):
"Polynomial formal verification using BDD-based techniques" — PFV [9d367313]
PFV is listed among hardware–software co-verification techniques alongside symbolic co-simulation, FERIVer, and the riscv-formal framework. Within RISC-V verification flows, PFV provides mathematical guarantees of correctness that complement dynamic, simulation-based testing.
Concrete RISC-V Deployments
The survey of RISC-V processor verification (d-nb.info/1375027034/34, Journal of Electronic Testing, 2025) catalogs several concrete applications of BDD-based PFV to RISC-V cores:
| Processor | Method | Verification time / notes | Ref |
|---|---|---|---|
| RISC-V RV32I processor (Tomasulo, precise/nested interrupts) | Polynomial formal verification based on BDDs; ITE (If–Then–Else) operator used to compute the results of logic operations in BDDs | Listed limitations: "Complexity of BDDs"; benefits: "Simplify complexity of CPU verification; fast and use little memory" | [61] |
| RV32I-based MicroRV32 (multi-cycle sequential) | Polynomial Formal Verification using BDD and equivalence checking; SYSSIM used to verify the sequential multi-cycle processor | Complete verification of the multi-cycle processor achieved; ALU verification time ≈ 200 ns; "Efficient and low cost" | [55] |
These entries show two distinct application patterns:
- Logic-level BDDs with the ITE operator — the If–Then–Else operator is the fundamental recursive combinator on BDDs (it computes
ITE(f, g, h) = (f ∧ g) ∨ (¬f ∧ h)) and is used to build the logical operation results for verification [a81afbab]. - Sequential multi-cycle verification — SYSSIM is used together with BDD equivalence checking on MicroRV32 to verify the full sequential processor [a81afbab].
The cited benefits—"fast and use little memory", "simplify complexity of CPU verification", "efficient and low cost"—directly motivate BDD/PFV despite the acknowledged "Complexity of BDDs" limitation.
BDDs in Reactive Synthesis
Beyond verification, BDDs have historically been the dominant representation for synthesizing reactive systems from declarative specifications. However, BDD-based synthesis inherits the well-known scalability issues of BDD representations. The work on Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications [arXiv:1604.06204] explicitly notes:
"Existing approaches to synthesize reactive systems from declarative specifications mostly rely on Binary Decision Diagrams (BDDs), inheriting their scalability issues."
To address this, the paper proposes algorithms based on SAT solvers, QBF solvers, and Effectively Propositional Logic (EPR), using techniques such as query learning, templates, EPR reduction, QBF certification, interpolation, and parallelization. The approach outperforms a naive BDD-based tool and is competitive with a highly optimized BDD-based tool, winning two medals in the SyntComp competition. This demonstrates that while BDDs remain a strong baseline for synthesis, alternative symbolic representations can surpass them in scalability.
Practical Considerations
| Aspect | BDD-based approach | Notes |
|---|---|---|
| Canonicality | Yes (for ROBDD with fixed variable order) | Enables cheap equivalence checks |
| Worst-case size | Exponential in number of variables | Variable ordering strongly affects size |
| Best-case size | Polynomial for tree-like / multiplexer-derived circuits | Basis for PFV polynomial guarantees |
| Core operator | ITE (If–Then–Else) | Used to compose BDD-encoded logic results |
| Underlying engine for | Image/pre-image computation in state-based model checking | Works alongside Presburger arithmetic for integer variables |
| Primary use cases | Verification, model checking, synthesis | RISC-V RV32I/MicroRV32 verification, HMC, reactive synthesis |
| Example tooling | SYSSIM, riscv-formal (complementary), CUDD |
SYSSIM used for sequential multi-cycle PFV; CUDD for Boolean manipulation in HMC |
| Scalability bottleneck | BDD blow-up on unstructured problems | Motivates SAT/QBF/EPR-based alternatives and hybrid ST/PR approaches |
Related Techniques
- Polynomial Formal Verification (PFV) — uses BDDs and related structures to bound verification complexity; demonstrated on multi-cycle RISC-V cores such as RV32I (ITE-based) and MicroRV32 (SYSSIM-based).
- Symbolic co-simulation / co-verification — integrates symbolic execution engines (e.g., KLEE) with ISS–RTL co-simulation, often complementary to BDD-based PFV.
riscv-formal— open framework using the RISC-V Formal Interface (RVFI) for property checking, often combined with BDD-based or simulation-based methods in hybrid flows.- SAT / QBF / EPR solvers — alternatives that overcome BDD scalability issues in synthesis, as shown in safety-specification reactive synthesis.
- Hybrid Model Checking (HMC) — interleaves BDD/Presburger-based state traversal with SAT/SMT-based path reasoning to combine their complementary strengths.
- CUDD Library — the standard BDD package used to represent and simplify Boolean formulas in symbolic verification frameworks such as HMC.
Summary
BDDs provide a canonical, symbolic representation of Boolean functions that makes them a natural engine for formal hardware verification, symbolic model checking, and reactive synthesis. In state-based model checking they underpin image/pre-image computations over state sets, and combined with Presburger arithmetic they support hybrid model-checking frameworks (e.g., HMC) implemented on top of libraries such as CUDD. For circuit classes with favorable structure—such as tree-like circuits and multiplexer-based circuits derived from BDDs—BDD-based verification, and Polynomial Formal Verification in particular, achieves polynomial complexity. These methods have been concretely demonstrated on multi-cycle RISC-V cores covering both combinational and sequential logic, including the RV32I core (with ITE-based BDD composition) and the MicroRV32 core (verified sequentially via SYSSIM with BDD equivalence checking). In domains such as reactive synthesis, however, BDDs face scalability limitations, motivating the development of SAT-, QBF-, and EPR-based alternatives that can outperform BDD-based tools on large specifications.