Data Structures for Formal Verification of Circuit Designs

Abstract:

We address the problem of logic verification, for both combinational and sequential logic. We discuss the Binary Decision Diagram (or BDD) as a means to represent boolean functions. This representation is canonical with respect to the variable ordering and is usually compact. We present an O(n23n)
algorithm for finding the optimal variable ordering for a BDD, and compare it to a brute-force method and to heuristic approaches. We introduce a data structure called the projective BDD which is not canonical but can be more compact than the BDD. We address the problem of verifying multiplier
circuits using this structure. Finally, we present a form of deterministic finite automation called the nDFA, and apply it to the problem of sequential logic verification.