How do SAT and BDD verify RTL to gate netlist equivalence?

Formal equivalence checking ensures that a synthesized gate-level netlist implements the exact same logical behavior as the original register-transfer-level (RTL) design. Rather than relying on simulation, which can only test a fraction of possible input combinations, formal methods mathematically prove or disprove equivalence across all inputs. Boolean Satisfiability (SAT) solvers and Binary Decision Diagrams (BDDs) are the two foundational engines that power this verification process in classical computing.

Constructing the Miter Circuit

Before either a SAT solver or a BDD can be applied, the verification tool must frame equivalence as a single Boolean problem. Both the RTL design and the gate netlist are converted into combinational logic networks by matching their state-holding elements, such as flip-flops and latches, through a process called sequential-to-combinational reduction.

Once the inputs and registers are aligned, the two circuits are combined into a miter circuit. For corresponding outputs \(f_{\text{RTL}}(x)\) and \(f_{\text{gate}}(x)\) over input vector \(x = (x_1, x_2, \dots, x_n)\), the miter computes their exclusive-OR:

\[M(x) = f_{\text{RTL}}(x) \oplus f_{\text{gate}}(x)\]

If the two designs are functionally equivalent, then \(M(x) = 0\) for all possible input assignments. If there exists even a single input vector \(x^*\) such that \(M(x^*) = 1\), the designs are not equivalent, and \(x^*\) serves as a counterexample.

Verification with Binary Decision Diagrams

A Binary Decision Diagram, specifically a Reduced Ordered Binary Decision Diagram (ROBDD), is a canonical directed acyclic graph representation of a Boolean function. Given a fixed variable ordering, every Boolean function has a unique ROBDD.

The construction of a BDD relies on Shannon expansion, which decomposes a function \(f\) around a variable \(x_i\):

\[f = x_i \cdot f_{x_i=1} + \overline{x_i} \cdot f_{x_i=0}\]

By recursively applying Shannon expansion and merging isomorphic subgraphs while eliminating redundant nodes, the verifier builds canonical representations for both \(f_{\text{RTL}}\) and \(f_{\text{gate}}\).

Because ROBDDs are canonical, equivalence checking becomes a constant-time pointer comparison: if the root nodes of the two BDDs are identical, the circuits are equivalent. Alternatively, building the BDD for the miter \(M(x)\) yields the constant \(0\) node if and only if the designs match.

The primary limitation of BDDs is memory explosion. For certain functions, such as integer multipliers, the size of the BDD grows exponentially with the number of input bits regardless of the variable ordering chosen.

Verification with Boolean Satisfiability Solvers

Boolean Satisfiability (SAT) solvers approach the miter circuit as a search problem rather than a canonical representation problem. The miter circuit is translated into Conjunctive Normal Form (CNF) using the Tseitin transformation, which introduces auxiliary variables for internal gates to keep the formula size linear in the size of the circuit.

A CNF formula is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals:

\[\Phi = \bigwedge_{j=1}^{m} \left( \bigvee_{k} l_{j,k} \right)\]

The SAT solver then searches for an assignment to the variables that makes \(M(x) = 1\) (satisfiable). Modern solvers use Conflict-Driven Clause Learning (CDCL), which combines:

• Unit propagation to deduce forced variable assignments.
• Backtracking search to explore the decision tree.
• Conflict analysis to learn new clauses that prevent repeating dead-end search paths.

If the solver proves that \(\Phi\) is unsatisfiable (UNSAT), no input can make the outputs differ, proving equivalence. If it finds a satisfying assignment (SAT), the input values directly provide a counterexample demonstrating the bug.

Combining SAT and BDDs in Practice

In industrial equivalence checkers, SAT solvers and BDDs are rarely used in isolation. Instead, they are combined in hybrid frameworks that leverage the strengths of both engines:

• Structural hashing and sweeping: The tool identifies potentially equivalent internal nodes (cutpoints) between the RTL and netlist using random simulation.
• BDD-based local equivalence: Small, localized cones of logic are proved equivalent using BDDs, which handle XOR-heavy and symmetric logic efficiently.
• SAT-based global solving: When BDDs grow too large, the tool switches to a CDCL SAT solver, which excels at navigating large, deep circuits with minimal memory overhead.

By partitioning the miter at verified internal cutpoints and alternating between BDDs and SAT solvers, modern formal verification tools can prove equivalence for designs containing millions of gates.