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 | Path |
|---|---|---|
Stability, X-safety, bounded acceptance and covers. | Required | |
Hold, ack window, one pulse per request, spacing. | Recommended | |
Legality, count and pointer math, data integrity. | Recommended | |
Encoding, legal arcs, bounded exit, reset, covers. | Optional | |
Gated latency, stall hold, ordering, credit bound. | Optional | |
The course project's assertions in one runnable checker with planted bugs. | Optional |
Required lessons are the core first pass for writing working assertions. Recommended lessons are worth reading for most learners once the first pass works. Optional lessons are reference, specialist material or revision, and you can come back to them when a project needs them.
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.