Each interface in this topic gets a complete ruleset. A ruleset pairs safety rules with bounded liveness, X-safety and cover points.
Family | Safety core | Liveness and cover |
|---|---|---|
Handshake (valid/ready, req/ack) | Offers held until accepted; payload stable | Bounded accept window; back-to-back and stall covers |
Storage (FIFO) | No overflow or underflow; count matches pointers | Full-to-empty drain cover; pointer-wrap cover |
Control (FSM, pulses, interrupts) | Legal arcs only; one-hot encoding; mutex | Bounded exit from busy states; arc covers |
Datapath (pipelines, credits) | Gated-latency equality; stall freezes stages | In-order retirement; credit bound and conservation |
Lesson | Ruleset |
|---|---|
Stability, X-safety, bounded acceptance and covers. | |
Hold, ack window, one pulse per request, spacing. | |
Legality, count and pointer math, data integrity. | |
Encoding, legal arcs, bounded exit, reset, covers. | |
Gated latency, stall hold, ordering, credit bound. |
Proof that the checker ever ran. Covers record back-to-back transfers, stalls, drains and rare arcs across the regression. A ruleset with no hits proves nothing about the design.