Formal Property Verification (FPV) Basics
Bring up a complete FPV environment for a small periodic timer: covers, assumptions, assertions, running the tool and debugging counterexamples.
What you will learn
- Follow the FPV loop: covers → assumptions → assertions → run → debug → refine.
- Set up clocks, reset and a formal wrapper for a block.
- Decide whether a counterexample is a design bug, a property bug or a missing assumption.
- Explain how FPV differs from simulation in practice.
Lessons
- 4.1The FPV loopThe iterative workflow behind every formal property verification effort.
- 4.2The example: a periodic timerSpecification and RTL for the block we will verify.
- 4.3Bringing up the environmentCompile, clocks and reset, and the formal wrapper.
- 4.4Covers first: does the environment work?Write covers for the behaviours you expect to see.
- 4.5Adding assumptions and assertionsTurn the spec into properties and get the first results.
- 4.6Debugging counterexamplesA repeatable triage process for failing assertions.
- 4.7How FPV differs from simulation in practiceFree inputs, all values, internal constraints and different debug habits.
- ✎Chapter quiz (4 questions)