The FPV loop

Formal property verification (FPV) means proving SVA assertions on RTL with a model checker. Regardless of the tool or the block, the work follows the same loop:

Two things about this loop surprise people coming from simulation:

• Covers come first. Before trusting any "proven" result, you want evidence that the environment allows the interesting behaviour. Covers are cheap to write and quick to run.
• Failures are welcome. Early counterexamples mostly reveal missing assumptions and misunderstood spec details. Each one teaches you something about the design.

In this chapter we will walk the loop once, end to end, on a small but realistic block.