Decision Diagrams, Equivalence Checking, and Symbolic Simulation
A fundamental problem in formal verification is determining whether two Boolean functions are functionally equivalent. A case in point is to determine whether a circuit, after timing optimization, retains the same functionality. Logical equivalence can be done on either combinational functions or sequential functions. Determining even combinational equivalence can be hard, such as deciding whether is equivalent to . The second expression can be obtained from the first expression by shifting the complementation operation to the other literal of each cube. Although somewhat counterintuitive, these two expressions are functionally equivalent. Sequential equivalence is concerned with determining whether two sequential machines are functionally equivalent. One way to do this is based on combinational equivalence. First we minimize the two machines to eliminate redundant states, then we map their states based on one-to-one correspondence, and finally we decide whether their next-state functions are combinationally equivalent. The problem of combinational equivalence is a focus of this chapter.
A brute-force method to determine combinational equivalence is to expand the combinational functions in minterm form and compare them term by term. The minterm representation has the property that two equivalent Boolean functions have identical minterm expressions. This property in general is called canonicity of representation. A representation having the property is a canonical representation. In addition to minterm representation, maxterm and truth table are also canonical representations. One way to decide whether two functions are equivalent is to represent them in a canonical form. If their forms are identical, they are equivalent; otherwise, they are not equivalent. However, this method runs into the problem of exponential size, because the number of minterms or maxterms of a function can be exponential with respect to the number of variables.
The sum-of-products representation is more compact than minterm representation, but it does not reveal readily functional equivalence or unequivalence. As demonstrated by our previous example, the two functions have a completely different appearance, even though they are functionally equivalent. Thus, a second desirable property of a representation, besides canonicity, is compactness. Sum-of-products is more compact than truth table representation.
An ideal representation should be both canonical and compact. Because logical equivalence is an NP-complete problem, it is likely that all canonical representations are exponential in size in the worst case. However, a canonical representation is still useful if its size for many practical functions is reasonable. In this chapter we will look at BDDs as a representation of Boolean functions. Then we will examine how BDDs are used in determining functional equivalence. As an alternative to BDDs in checking equivalence, we will study SAT. Finally, we will examine symbolic simulation, to which BDDs and SAT are applicable.