8.6. Summary of Key Concepts

Try these first

1. 1.

   What is formal verification?

   Hint

   Think about the role of mathematics in checking designs.

2. 2.

   Name one technique used in formal verification.

   Hint

   There are several key techniques we discussed.

3. 3.

   Which of the following methods compares RTL designs to gate-level netlists?

   • Property Checking
   • Model Checking
   • Equivalence Checking

   Hint

   Think about the verification steps after design transformation.

4. 4.

   True or False: Property checking ensures that designs work under some conditions.

   • True
   • False

   Hint

   Reflect on the meaning of exhaustive verification.

5. 5.

   Design a fictitious RTL circuit and identify potential properties to check using property checking. Explain how you would use model checking to explore possible states.

   Hint

   Consider all timing scenarios and state transitions.

6. 6.

   Discuss how abstraction can help mitigate the state explosion problem in formal verification. Provide an example of a design where you might implement abstraction.

   Hint

   Think about what elements are necessary for verification and which can be simplified.