Hardware Design Verification: Simulation and Formal Method-Based Approaches

Chapter 9. Model Checking and Symbolic Computation

Chapter Highlights

• Properties, specifications, and logic

• Property checking

• Symbolic computation and model checking

• Symbolic CTL model checking

• Computational improvements

• Using model-checking tools

Checking equivalence between two circuits, proving or disproving that the two circuits are functionally equivalent, is one aspect of formal verification. If two circuits are sequential and the mapping between their states is not available, the techniques we discussed earlier fail, and model-checking techniques are required. In general, model checking is required when verifying partial and abstract specifications. Modeling checking, the main subject of formal verification, deals with more general problems ...