Simulation shows the protocol working on the cases it tried; formal methods prove the property on all cases within the stated assumptions. For handshakes and FIFO pointers the state space is small enough that proof is practical, which makes it the strongest evidence in a signoff review, provided the assumptions are written down and themselves reviewed.
Property | What the proof covers | Typical bound or scope |
|---|---|---|
No lost or duplicated pulse | Every source event yields exactly one destination event | All spacings down to the stated minimum gap |
Handshake data integrity | Captured word equals the offered word on every transfer | All phase alignments of the two clocks |
FIFO no overflow or underflow | Writes never exceed depth, reads never precede writes | All pointer and flag combinations reachable from reset |
Deadlock freedom | Every offered transfer eventually completes | With the fairness assumption that both clocks keep running |
Clock behaviour: both clocks run within their specified ranges for the whole proof. A stopped or gated clock is outside the proof unless modelled.
Reset behaviour: the proof starts from the reset state the design actually reaches, with both sides reset together as the reset lesson requires.
Single-step pointers: Gray pointers advance by one only; jumps are excluded by assumption and must be excluded by design too.
Synchroniser abstraction: the proof typically treats the synchroniser as a bounded-latency delay (settling within N cycles), not as a metastable element. Metastability itself is argued separately (see the next lessons).
Environment discipline: the source obeys the spacing or stability rules; the proof shows the protocol correct given a disciplined environment, and the assertions lesson shows the environment checked.
That the real source actually holds data stable: the assumption needs its own assertion (the data-stability checker of the previous lesson) bound in simulation.