Binary Decision Diagrams (BDDs)

Concept

Binary Decision Diagrams (BDDs) are canonical, directed-acyclic-graph representations of Boolean functions that serve as a foundational data structure in formal hardware verification, symbolic model checking, and reactive synthesis. Reduced ordered BDDs (ROBDDs) enable efficient equivalence checking, image computation, and satisfiability analysis. BDDs underpin Polynomial Formal Verification (PFV), which achieves polynomial-time, polynomial-space verification for circuits with favorable structure (e.g., tree-like or multiplexer-derived circuits), and have been demonstrated on RISC-V cores such as RV32I and MicroRV32. State-based model checking uses BDDs together with Presburger arithmetic to compute reachable state sets via image/pre-image operations, and BDDs are the canonical data structure used by libraries such as CUDD for representing and simplifying Boolean formulas in hybrid model-checking frameworks.

First seen 6/6/2026

Last seen 7/30/2026

Evidence 6 chunks

Wiki v3

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

5 connections

Polynomial Formal Verification (PFV) ← uses 95% 2e

PFV uses Binary Decision Diagrams and related structures for formal verification.

Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking ← uses 100% 2e

The paper uses BDDs for Boolean formula representation.

formal verification ← uses 93% 1e

Binary Decision Diagrams are used in polynomial formal verification for RISC-V processors.

State-based Model Checking ← uses 100% 1e

State-based model checking uses BDDs for Boolean level reasoning.

CUDD Library ← implements 100% 1e

CUDD library implements BDD operations.

LINKED ENTITIES

3 links

State-based Model Checking USES Extracted graph relationship

Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking USES Extracted graph relationship

CUDD Library IMPLEMENTS Extracted graph relationship

CITATIONS

11 sources

11 citations — click to expand

[1] Verification is one of the central tasks during circuit design; for circuits with specific structural properties (tree-like circuits, multiplexer-derived circuits) complete formal verification based on BDDs can be carried out in polynomial time and space. Polynomial Circuit Verification using BDDs

[2] In state-based model checking, BDDs are used for Boolean-level reasoning and Presburger arithmetic solvers for integer-level reasoning; image computations Img(D_ρ) = (∃ C, X . T ∧ D_ρ)(X/X′, C/C′) drive symbolic state traversal toward a fixpoint. Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking

[3] If F is a frontier set with respect to error states B_Err and B_Err ∩ D = ∅, then F \ {D} ∪ {Img(D)} is also a frontier set. Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking

[4] State-based model checking methods (BDDs, Presburger arithmetic) perform well when state sets have compact representations but suffer from memory explosion; stateless methods (SAT/SMT-based BMC) avoid explicit state-set manipulation but involve time-intensive computations. Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking

[5] HMC interleaves state traversal (ST) and path-based reasoning (PR), switching from ST to PR via a memory bound and back via a depth/time bound; large frontier state sets are partitioned by number of Presburger linear equations and BDD nodes. Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking

[6] The HMC implementation uses CUDD to represent and simplify Boolean formulas and the Omega library to represent and simplify Presburger arithmetic formulas. Efficient State Space Exploration: Interleaving Stateless and State-based Model Checking

[7] PFV (Polynomial Formal Verification using BDD-based techniques) is listed among hardware–software co-verification techniques alongside symbolic co-simulation, FERIVer, and riscv-formal in the RISC-V testability survey. Towards Reliable and Secure RISC-V Systems: Survey of Testability and ...

[8] RISC-V RV32I (Tomasulo, precise/nested interrupts) was verified using polynomial formal verification based on BDDs with the ITE (If–Then–Else) operator used to compute the results of logic operations; limitations include "Complexity of BDDs"; benefits are "Simplify complexity of CPU verification; fast and use little memory". Survey of Verification of RISC-V Processors

[9] The RV32I-based MicroRV32 (multi-cycle sequential) was verified using Polynomial Formal Verification with BDD and equivalence checking together with SYSSIM, achieving complete verification of the multi-cycle processor; ALU verification time ≈ 200 ns; benefits cited as "Efficient and low cost". Survey of Verification of RISC-V Processors

[10] Existing approaches to synthesize reactive systems from declarative specifications mostly rely on BDDs, inheriting their scalability issues. Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications

[11] SAT/QBF/EPR-based reactive synthesis algorithms (query learning, templates, EPR reduction, QBF certification, interpolation, parallelization) outperform a simple BDD-based tool and are competitive with a highly optimized one; the approach won two medals in SyntComp. Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications