Simulation shows a design working; this section proves it, one application at a time. Every lesson takes the same shape: a table or a small property set that is the source of truth, a runnable proof over all inputs and all reachable states, a failing partner that shows the proof can catch a real bug, and the counterexample read cycle by cycle. The designs are the running ones: the chain of pipeline, FIFO and handshake stage carries the connectivity proof, the register block carries the register proofs, the arbiter and a two-stage chain carry the progress proofs, and the FIFO, handshake stage and pipeline carry the data-integrity sets. Where no running design shows the point, a small lesson-local module is named in its lesson and used only there.
Topic | What it covers | After it you can... |
|---|---|---|
A connection table proved structurally for every mode, with generated checks | Write a connectivity table, generate its checks, and read a wrong-row counterexample. | |
Reset values, read-only bits, write-1-to-clear and access timing from a register table | Prove a register map from its table, including the hardware-set race. | |
Three distinct progress failures, bounded grants, fairness documented as a register | Tell the three apart, prove bounded progress, and state what fairness you assumed. | |
What two-state formal can and cannot say about X, proved with two-copy harnesses | Prove reset determinism and say exactly what an X question still needs. | |
Full property sets for the FIFO, the handshake stage and the pipeline | Write a complete safety set with ordering, conservation and latency. | |
Information flow, dead-state analysis, and where formal sits in CDC, low-power and CPU flows | Scope what a proof does and does not show, and point each neighbour flow at its owner. |
Suggested order: top to bottom. Modules that carry a name such as chain_top or chain2 belong to their topic only: each lesson that uses one says where it is defined. Connectivity first, because its table-driven method is reused by the register topic; registers next, because every block has them; progress and X in either order after that; the datapath sets after the handshake and pipeline behaviour is familiar; the scoping lesson last, because it tells you when to stop. Each lesson states its result exactly: proven for this model under these assumptions, a counterexample at a named cycle, or inconclusive with what is missing.
Connectivity from the table, the register set from the map, and reset determinism. They catch wiring, decoding and reset bugs that simulation finds late, and each is cheap to prove.