Control proofs say the pointers are right; data proofs say the bytes are right. This topic writes the full safety set for each of the three datapath designs: occupancy, flags and pointer consistency plus a tracked-slot integrity property for the FIFO, stability and conservation plus tracked-word integrity for the handshake stage, and the three-cycle latency rule for the pipeline. Each set is proved whole, each mutant is killed by its named property, and the table in each lesson says which property catches which bug class.
Lesson | After it you can... |
|---|---|
Prove occupancy, flags, pointers and slot integrity, and say what depth each needs. | |
Prove stability, conservation and integrity across backpressure. | |
Prove fixed latency with history registers and reuse the set for equivalence. |
Suggested order: top to bottom. The FIFO set is the richest and introduces the tracked slot; the bridge set reuses the tracking idea on a skid; the pipeline set introduces input history, which the equivalence section reuses for its alignment argument. Prove each set at the depth its lesson states, and induction where the lesson shows the helper.
The tracked-item integrity property: control counts words, only the tag check follows values. Add the tracked slot or word with its helper invariant, and mutate the data path to confirm it fails.