Overview

Ordered Binary Decision Diagrams (BDDs) are referenced in the provided sources as a Boolean method that can be applied once verification conditions have been reduced to propositional logic. In the processor-verification setting, formulas in the logic of equality with uninterpreted functions (EUF) are reduced to propositional formulas so that Boolean methods such as BDDs and SAT checkers can be used.

Use in processor verification

The cited processor-verification work uses EUF as an abstraction for data manipulation in processor correctness proofs. It states that reducing EUF formulas to propositional formulas enables the use of BDDs and Boolean satisfiability checkers for verification. The same source also reports simplifications based on the observation that many equations appear only in positive form, allowing the verification method to restrict attention to "maximally diverse" interpretations of function symbols. Experimental results in that paper are reported as demonstrating efficiency on pipelined-processor verification using the Burch-and-Dill method.

Use in BDD-based SAT solving

Public context also describes SAT solvers based on BDDs, especially solvers capable of generating proofs of unsatisfiability. In particular, a 2023 note reports that for the pigeonhole problem in the standard direct encoding, a BDD-based bucket-elimination approach can generate polynomial-time unsatisfiability proofs when different variable orderings are used for the BDDs and for the buckets. The same note reports experimental scaling of approximately (O(n^5)) for these proofs, while using the same variable ordering for both BDDs and buckets leads to exponential scaling.