Stage 1 covers the two storage designs: the FIFO that must never lose or reorder a word, and the bridge stage that must never lose a word under backpressure. Both are safety work and close in full with helper assertions. Each lesson gives you the design, the property set already written, a deliverable and a pass criterion; the causes of the eight planted faults are in the Solutions topic after stage 4.
Lesson | After it you can... |
|---|---|
Prove the FIFO set, locate five planted faults by counterexample, and file the rows. | |
Prove the bridge with every input free, and judge a proposed input rule. | |
Build the mutation table, find survivors under reduced property sets, and file the covers. |
Suggested order: top to bottom. The FIFO lesson fixes the ledger habit; the bridge lesson adds the assumption register; the covers lesson tests both. Do not start stage 2 until your stage 1 package passes the engine.
Both designs close in full with their helper assertions, so a bounded row would be an unfinished proof. Bounded rows appear only where a lab argument justifies them.