BDD-Based Verification

Core Idea

BDD-based verification uses Binary Decision Diagrams — compact canonical representations of Boolean functions — to perform symbolic model checking. Instead of enumerating individual states, the model checker represents entire sets of states as BDDs and computes transitions, reachability, and fixed points using BDD operations. This enables verification of systems with billions of reachable states, far beyond what explicit-state enumeration can handle. BDD-based symbolic model checking, pioneered by McMillan, Burch, and Clarke in the early 1990s, was the breakthrough that made model checking practical for hardware verification.

Explainer

Explicit-state model checking enumerates states one by one, storing each in a hash table and exploring successors. This is intuitive but hits a hard wall: a system with n Boolean state variables has 2ⁿ possible states, and storing each individually is infeasible for n beyond roughly 30-40. Symbolic model checking overcomes this by representing sets of states as Boolean functions and manipulating them using Binary Decision Diagrams (BDDs) — a data structure that compactly represents Boolean functions as directed acyclic graphs with shared substructure.

A Reduced Ordered BDD (ROBDD) represents a Boolean function f(x1, ..., xn) as a DAG where each internal node tests a variable and branches to two children based on the variable's value. Two crucial properties make BDDs useful: they are canonical (given a fixed variable ordering, two equivalent functions have identical BDDs, making equality checking trivial) and they are often compact (structured functions arising in practice typically have polynomial-size BDDs even when the truth table is exponential). Set operations on state sets translate to BDD operations: union is Boolean OR, intersection is AND, complement is NOT, and all are computed in polynomial time relative to BDD sizes.

The key operation in symbolic model checking is image computation: given the current set of reachable states (a BDD) and the transition relation (a BDD over current-state and next-state variables), compute the set of all possible successor states. This uses existential quantification — "there exists a current state in the reachable set from which the transition leads to next-state s'" — implemented as a BDD operation called relational product. Starting from the initial states, the algorithm iterates image computation until a fixed point where no new states are discovered. The entire reachable state set is now captured in a single BDD, which can be intersected with the negation of the specification to find violations.

The Achilles' heel of BDDs is variable ordering sensitivity. The same Boolean function can be polynomial-sized under one variable ordering and exponential under another. The canonical example: x1*y1 XOR x2*y2 XOR ... XOR xn*yn has O(n) nodes with interleaved ordering but O(2ⁿ) with separated ordering. Finding the optimal ordering is NP-hard, so tools use heuristic dynamic variable reordering (sifting algorithms that swap adjacent variables to reduce BDD size during computation). Good ordering heuristics are often the difference between a verification completing in seconds and running out of memory.

BDD-based model checking was the breakthrough that made formal verification practical for hardware design. In the early 1990s, McMillan, Burch, and Clarke showed that BDD-based techniques could verify circuits with 10²⁰ or more states — far beyond explicit enumeration. The technique proved particularly effective for control-intensive hardware (cache coherence protocols, bus arbiters, pipeline controllers) where state sets have regular structure that BDDs exploit. More recently, SAT-based bounded model checking has complemented BDD-based methods: it unrolls the transition relation for a bounded number of steps and checks satisfiability using SAT solvers, which are sometimes more effective for datapath-heavy designs where BDDs blow up. Modern verification flows typically use both approaches.