Hardware Design Verification: Simulation and Formal Method-Based Approaches

Chapter 8. Decision Diagrams, Equivalence Checking, and Symbolic Simulation

Chapter Highlights

• Binary decision diagrams

• Decision diagram variants

• Decision diagram-based equivalence checking

• Boolean satisfiability

• 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 ...