Hardware Design Verification: Simulation and Formal Method-Based Approaches

Chapter 7. Formal Verification Preliminaries

Chapter Highlights

• Sets and operations

• Relation, partition, partially ordered set, and lattice

• Boolean functions and representations

• Boolean functional operators

• Finite-state automata and languages

Simulation-based verification relies much on one’s ability to generate vectors to explore corner cases. In reality, two major problems exist. First, it is almost impossible, especially in large designs, to consider all possible test scenarios and, as a result, bugs arise from scenarios that were never anticipated. Second, even if one could enumerate all the possible corner cases in a design, it must be done intelligently so that the computation time to verify them all is realistic. Formal verification is a ...