Writing the FPV plan
A good FPV plan fits on one or two pages and is reviewed by the designer and the verification lead. It has four parts.
1. Goals and scope
Signoff of sync_fifo for all legal parameter values used in the project (WIDTH 8–64, DEPTH 4–32).
Simulation will only run integration tests at the next level up.
2. Requirements → properties
| Req | Property | Type |
|---|---|---|
| R1 push stores data unless full | a_count_inc, data integrity check | assertion |
| R1 push while full is dropped | a_full_drop | assertion |
| R2 pop removes oldest unless empty | a_count_dec, data integrity check | assertion |
| R3 order and data preserved | a_data_order (tracked item) | assertion |
| R4 count / full / empty consistent | a_count_range, a_count_hold, a_flags | assertion |
| — | reach full, empty after full, push+pop when full, pointer wrap | covers |
3. Complexity strategy
- Data independence: the FIFO never inspects data values, so its control behaviour does not depend on
WIDTH. Prove control properties with WIDTH = 1 and data integrity with WIDTH = 2 or larger. (Argued informally here; a design that branches on data would need full width.) - Depth: start with DEPTH = 4, then 8, 16, 32. If larger depths become inconclusive, use the bounded-depth argument below or a pointer abstraction (Chapter 10).
4. Quality checks and exit criteria
- All assertions proven for each configuration; all covers reachable.
- No vacuous assertions; every assumption reviewed (this plan needs none on inputs — a strong result).
- Mutation run: every injected control bug detected by at least one assertion.
- COI coverage: every flop in the design is in the cone of at least one assertion.