A swapped pair of bits between two blocks passes every block-level testbench and fails in the system. Connectivity proof exists for exactly that bug: it checks, structurally and for all input values, that every destination sees its specified source. This topic proves the helper chain of pipeline into FIFO into handshake stage from a six-row table, generates the checks from the table so the table stays the source of truth, and reads the counterexamples that a wrong row and three wiring faults produce.
Lesson | After it you can... |
|---|---|
Write a connection table, generate its proof block, run the proof, and see a table typo fail it. | |
Prove each connection in its mode and catch a link that is live outside it. | |
Read a truncation, a swap and a missing tie-off, and decide whether the table or the wiring is wrong. |
Suggested order: top to bottom. The first lesson builds the method on the chain, the second adds modes, and the third is the debug guide you will actually open when a check fails. The structural lint view of the same tables lives in the SoC course.
Hand-written checks drift from the intent: the table is reviewed and the checks are derived, so a wrong row is one typo in one place and the proof names it. A hand-written set can also silently miss a signal.