You are the formal owner for a small chip block: a FIFO, a handshake bridge, four control registers, an arbiter, a pipelined pair, and a counter. The designs carry 16 planted faults. The lab is symptoms first: the brief gives symptoms, the design listings show each variant as a visible BUG == line (read those last, after the trace), each stage lesson gives inputs, a deliverable and a pass criterion, and the causes, the killing properties and the fixes are in the Solutions topic after stage 4. Every stage produces rows in a results ledger that cite the runs they rest on, and the lab ends with a signoff check that prints one line only when everything agrees. The section has 32 pages and takes roughly seven focused sessions, one per topic, in the order below.
Topic | Lessons | After it you can... |
|---|---|---|
2 | State the deliverables, the rubric and the ledger checks. | |
3 | Prove storage safety, find five FIFO and three bridge faults, and judge an input rule. | |
3 | Prove a register map from its table, bound an arbiter, and check pairs and a chain. | |
3 | Prove latency, a retimed twin, and a scoped ECO. | |
3 | Find the helper that closes an induction, and run the manifest. | |
8 | Check every cause, killing property, step and fix, and read the reference ledger and its single PASS line. | |
2 | Rerun a proof locally and extend the lab. |
Suggested order: the brief, stages 1 to 4, then Solutions, then the appendix. Do not start a stage until the package of the previous one passes the engine; do not open Solutions before stage 4, and compare each lesson of it with your own table. The appendix maps the proofs onto a local flow you can rerun.
The results ledger: each stage files rows that cite typed runs, the engine checks them, and the final manifest prints its line only when all rows agree.