Two engineers can both say “the FIFO is proven” and mean different things: a bounded check to depth 20, or a full proof under stated assumptions. The design may be fine; the claims are about different models. This lab makes the model part of the deliverable: every result carries its design, bound, assumptions, run and revision.
Stage lessons give inputs, a deliverable, a pass criterion and a hint ladder, and never name a cause. The design listings carry a BUG switch that selects a variant; its lines are the answer, so run a variant by header and read the trace first. Causes, killing properties and fixes are in the Solutions topic after stage 4.
Each design carries five obligations: prove its safety properties, reach its covers, justify every bounded result, register every assumption with the rows that discharge it, and make every planted fault fail a named property.
Design | Prove | Cover | Bounded claim needs |
|---|---|---|---|
FIFO | Occupancy, flags, no loss, order | Full, push with pop, tracked read | Depth 9: farthest state at step 8 |
Bridge | Conservation, holds, word integrity | Stall, skid, blocked input, flow | Depth 4: deepest cover at step 3 |
Registers | Reset, read-write, clear, read-only, isolation | Clear, both bits, set with clear | Depth 3: deepest cover at step 2 |
Arbiter | One-hot, no phantom, work, wait bound 3 | Each grant, contention, idle | Depth 5: contention at step 4 |
Pipeline, twin | Latency 3, reset zero, equal outputs | Non-zero result | Depth 5: first result at step 4 |
Counter | Range, pulse, step, hold | Nine, pulse, wrap | Depth 15: wrap at step 14 |
The minima apply to bounded results and covers. A full proof is filed with the depth and window it ran at.
A property set per design, each property shown failing on a planted fault or a mutant you write.
A harness: reset at step 0, free tracked constants, and an assumption register.
A results ledger: one row per obligation, citing the run it rests on.
A mutation table: each planted fault, the property that kills it, and the failing step.
A signoff package: bound justifications, discharged assumptions, waivers with owner and expiry, and the final manifest.
Bar | Pass | Fail |
|---|---|---|
Properties | Every property fails on a fault or mutant. | A property that cannot fail. |
Bounds | Every bounded result has a depth and a reason tied to a cover step. | A bare depth, or “proven” from a bounded run. |
Assumptions | Each is registered and names the rows that discharge it. | An open or unregistered assumption. |
Mutants | Every planted fault killed in a counterexample row. | A survivor, or a kill no run shows. |
Freshness | Every row names its revision. | A result from an older revision. |
There are 16 planted faults. The names W1, W2 and so on are the BUG values 1, 2 and so on of each design. Finding the cause from the trace is the graded skill.
Design | Variant | Symptom |
|---|---|---|
FIFO | W1 | Occupancy exceeds the depth; the oldest word is lost. |
FIFO | W2 | Occupancy shows an impossible wrapped value. |
FIFO | W3 | The full flag asserts early; capacity is lost. |
FIFO | W4 | Occupancy drifts away from the pointers. |
FIFO | W5 | Words come out with one bit cleared. |
Bridge | W1 | A word is lost under backpressure. |
Bridge | W2 | The output valid drops without a transfer. |
Bridge | W3 | The stalled output word changes. |
Registers | W1 | Writing 1 to a status bit sets it. |
Registers | W2 | The read-only ID register accepts writes. |
Registers | W3 | A data register wakes with the wrong value. |
Arbiter | W1 | One requester hogs the grant. |
Arbiter | W2 | Two grants assert in the same cycle. |
Arbiter | W3 | A grant asserts with no request present. |
Pipeline twin | W1 | Twin outputs disagree for some operand values only. |
Counter | W1 | The terminal pulse arrives one count late. |
Rules: every check must be able to fail; a bounded result carries a bound and a reason (“bounded to N”); results are proven, counterexample or inconclusive; no result outlives its revision.
A counterexample at the failing depth. The passing depth was “bounded to N”, never a proof.
Bounds, twice: the depth is below the minimum of 9, and a bounded claim carries no written reason. The engine reports both complaints.