Bug hunting or signoff?
When verification engineers run FPV on a block, they usually have one of two goals:
| Bug hunting FPV | Signoff FPV | |
|---|---|---|
| Question | "Can formal find bugs simulation missed?" | "Can formal replace simulation for this block?" |
| Property set | Targeted at risky areas | Complete with respect to the spec |
| Assumptions | Whatever keeps traces legal | Minimal, reviewed, each one justified (and ideally asserted elsewhere) |
| Inconclusive results | Acceptable | Must be justified (bounded depth argument) or resolved |
| Quality checks | Light | Mandatory: coverage, vacuity, mutation, reviews |
| Effort | Days to a couple of weeks | Several weeks for a typical block |
Bug hunting is a great first step; many teams start there and evolve into signoff once the environment is mature. Either way, the work starts with a plan.