FPV for Bug Hunting and Signoff
Build a complete, reviewable FPV plan for a synchronous FIFO: goals, property set, end-to-end data checking with a tracked item, complexity staging and quality checks.
What you will learn
- Choose between bug-hunting and signoff goals and plan accordingly.
- Write a verification plan: requirements, properties, complexity strategy and exit criteria.
- Check end-to-end data integrity cheaply with a tracked (symbolic) item.
- Apply quality checks: covers, vacuity, mutation and cone-of-influence coverage.
Lessons
- 6.1Bug hunting or signoff?Two goals, two levels of rigour.
- 6.2The example: a synchronous FIFOA parameterised first-word-fall-through FIFO.
- 6.3Writing the FPV planRequirements, properties, complexity strategy and exit criteria in one page.
- 6.4End-to-end data checking with a tracked itemLet the tool pick one arbitrary entry and follow it through the FIFO.
- 6.5Quality checks: is the proof worth anything?Covers, vacuity, over-constraint checks, mutation and COI coverage.
- 6.6Scaling up and reaching signoffGrow the configuration, handle inconclusive results and write the signoff report.
- ✎Chapter quiz (4 questions)