Scaling up and reaching signoff
With DEPTH = 4 everything proves in seconds. Signoff means covering the configurations the project will actually use.
Growing the configuration
- Run the same wrapper for DEPTH = 8, 16, 32 (WIDTH = 2 for data, WIDTH = 1 for control-only runs).
- If a proof becomes inconclusive, look at which assertion and how deep the bounded proof got.
- Use helper invariants that relate state variables, e.g.
count == wptr - rptr(mod DEPTH, with a full/empty distinction).
Justifying a bounded proof
Sometimes a bounded result is acceptable. The argument must show that the bound reaches every relevant state. For a FIFO, every combination of count and pointer offset is reachable within about 2 × DEPTH cycles from reset (fill, partially drain, refill to wrap the pointers). If covers for "full with pointers wrapped" and "tracked item at maximum depth" are hit well within the bound, a bounded proof to, say, 4 × DEPTH cycles is a defensible signoff for many teams. Document the argument; do not just quote a number.
The signoff report
Keep it short and factual:
- Configurations proven, tool and version, run time.
- Assertions: proven / bounded (with depth and justification).
- Assumptions: list, source in spec, where each is checked (none for this FIFO).
- Covers: all hit, maximum trace length.
- Quality: mutation results, COI/proof-core coverage, open waivers.
Chapter 11 expands this into a project-level signoff methodology.