A reviewed structure is necessary but not sufficient: verification must show the protocol behaves under stall, back-pressure, rate mismatch and reset, and that the checks themselves have teeth. This topic collects the assertion patterns, the formal arguments, the coverage checklist and the metastability-injection technique that together make that case.
Lesson | After it you can... |
|---|---|
Write runnable checkers for pulse, handshake and FIFO protocols. | |
Say what formal proves for crossings and what it assumes. | |
Plan stall, back-pressure and rate-mismatch scenarios. | |
Inject capture-window randomness and read the result honestly. |
Suggested order: read the four lessons in page order; the spacing rules and FIFO flags lessons supply the properties these checks pin down.
Nothing: it never violated the gap, so a missing or broken guard would pass the same test. Proof needs a negative test that breaks the rule on purpose.