Binary Decision Diagram
ConceptA Binary Decision Diagram (BDD) is a directed acyclic graph representation of a Boolean function. In the evidence here, ordered and reduced BDDs are treated as canonical representations: variables appear at most once per root-to-terminal path and in the same order on all paths, while isomorphic subgraphs and redundant nodes are removed. BDDs are used in the SystemC Verification Library for constraint representation and constraint-based randomization, in RISC-V processor formal verification workflows, in knowledge compilation variants such as OAODD, and in logic minimization for DSOPs.
First seen 6/14/2026
Last seen 7/13/2026
Evidence 8 chunks
Wiki v2
WIKI
Definition
A Binary Decision Diagram (BDD) represents a Boolean function as a directed acyclic graph. In the SCV constraint-solving paper, each BDD node carries out a Shannon decomposition of a Boolean function (f : B^n \rightarrow B) [1]. In the RISC-V verification survey, BDDs used for verification are described as directed graphs with no cycles, with each node having two edges representing 0 and 1 [2].
Ordered, reduced, and canonical form
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
7 connectionsThe SCV library uses BDDs as the basic data structure to represent constraints.
The paper analyzes BDDs as the basic data structure used in the SCV to represent constraints.
BDDs can be shown using complement edges to represent both a function and its complement.
scv_expression stores the BDD representation of constraints.
The BDD weighting algorithm operates on BDD nodes to compute probabilities.
BDD-based verification directly uses Binary Decision Diagrams.
BDDs are the core data structure used in polynomial formal verification.
LINKED ENTITIES
5 linksSystemC Verification Library USES Extracted graph relationship
BDD Weighting Algorithm USES Extracted graph relationship
scv_expression USES Extracted graph relationship
Improvements for Constraint Solving in the SystemC Verification Library USES Extracted graph relationship
Complement Edges in BDD USES Extracted graph relationship
CITATIONS
14 sources14 citations — click to expand
[1] A BDD represents a Boolean function as a directed acyclic graph whose nodes perform Shannon decomposition, and verification BDD nodes have 0/1 edges. Improvements for Constraint Solving in the SystemC Verification Library; Survey of Verification of RISC-V Processors
[2] Ordered BDDs encounter each variable at most once per path and in the same order on all paths; reduced BDDs remove isomorphic subgraphs and redundant nodes; reduced ordered BDDs are canonical. Improvements for Constraint Solving in the SystemC Verification Library
[3] Complement edges allow representing a function and its complement by the same node by modifying the edge pointing to that node. Improvements for Constraint Solving in the SystemC Verification Library
[4] The SCV library includes an integrated BDD-based constraint solver, and SCV constraints are represented internally by BDDs for their characteristic functions using CUDD. Improvements for Constraint Solving in the SystemC Verification Library
[5] SCV constraint solving traverses the BDD from the root to the 1-terminal, and the resulting path determines variable values for a constraint solution. Improvements for Constraint Solving in the SystemC Verification Library
[6] scv_expression represents constraint expressions as expression trees, while scv_expr stores the BDD representation and maps bit operators to BDD synthesis operations such as BDD-AND. Improvements for Constraint Solving in the SystemC Verification Library
[7] The SCV improvements added bitwise AND, bitwise OR, bitwise NOT, bit-select, and slice-select operators for constraints. Improvements for Constraint Solving in the SystemC Verification Library
[8] Naive 50/50 BDD traversal can produce non-uniform constraint solutions because sub-BDDs can contain different numbers of paths to the 1-terminal. Improvements for Constraint Solving in the SystemC Verification Library
[9] The SCV weighting algorithm computes weights and probabilities for BDD nodes so generated values are uniformly distributed among constraint solutions. Improvements for Constraint Solving in the SystemC Verification Library
[10] The original SCV solver failed to update probabilities after BDD simplification, and the redesign recomputed weights and probabilities after simplification with tighter integration between weighting and BDD synthesis. Improvements for Constraint Solving in the SystemC Verification Library
[11] BDD-based RISC-V verification faces size-growth and golden-reference-model challenges, addressed by divide-and-conquer, partial simulation, symbolic simulation, piecewise reference BDD generation, and equivalence checking; the RV32I case reported 16 minutes. Survey of Verification of RISC-V Processors - Springer Nature
[12] For MicroRV32, BDDs using the SYMSIM tool verified extracted functionalities across Fetch, Control, Execute/ALU, and Decode and Extension Unit stages, with 200 ms reported for ALU verification. Survey of Verification of RISC-V Processors - Springer Nature
[13] OAODD extends OBDD with AND-vertices and OR-vertices for knowledge compilation and supports conversions, polynomial-time logical operations, and compilation from negative normal form formulas. Ordered {AND, OR}-Decomposition and Binary-Decision Diagram
[14] BDDs have been used for DSOP minimization with implicit term representation, faster handling of large circuits than explicit techniques, and quality dependence on variable ordering. On an optimization technique using Binary Decision Diagram