Stage 2 covers the control surface: four registers with write-1-to-clear and read-only behaviour, and the arbiter that shares the datapath. The register work is table-driven: each row of the map becomes properties. The arbiter work is bound-driven: you derive the wait limit, then prove it. The stage ends with pair proofs, two copies of one design for reset determinism, and a chain whose connections come from a table. The causes of the faults are in the Solutions topic after stage 4.
Lesson | After it you can... |
|---|---|
Turn the register map into a property set, check it is complete, and find three planted faults. | |
Derive the wait bound with a model, prove it, and find three planted faults. | |
Prove two-copy reset determinism and a table-driven chain, each with a failing partner. |
Suggested order: top to bottom. Registers first, because their proofs need no helpers; the arbiter next, because its helpers preview stage 4; pairs last, because they reuse the designs of stages 1 and 2.
Every combination of register values is reachable by writes and set pulses, so the induction step never starts in an unreachable state. Helpers repair unreachable-state leakage; here there is none.