A verification team runs a million cycles of random traffic with every assertion passing and declares the interface clean. On silicon, under one unusual traffic pattern, a request never gets its response. No assertion fired because no assertion could: in every finite simulation, "the response has not come yet" looks exactly like "the response will never come". The team had checked that nothing bad happened. Nobody had checked that something good eventually did.
What kinds of property does a protocol have, and why are some so much harder to check?
The obvious approach is to write a check for every rule and run lots of simulation. That works for rules whose violation shows up at a moment in time: data changed while stalled, a credit count went negative. It cannot work for rules that promise something will happen eventually, because a simulation always ends, and at the end the promise might still be about to be kept.
Safety | Liveness | |
|---|---|---|
Says | Nothing bad ever happens | Something good eventually happens |
Violated by | A finite trace: you can point at the cycle it went wrong | Only an infinite trace: no finite trace proves it was broken |
Protocol examples | Data stable while stalled; credits never negative; never more than N outstanding; a response matches a request | Every request gets a response; a stalled transfer completes; every requester is eventually granted; the link eventually trains |
Checked by | Assertions in simulation; formal tools | Formal tools; or turned into a bounded safety check |
Every property is a combination of the two (fact T29). Deadlock, livelock and starvation (Part 9) are all liveness failures, which is exactly why they escape simulation-based testing.
Bound it: "every request gets a response within 1,000 cycles" is a safety property, violated at cycle 1,001. Choose the bound from the design's worst case, not from typical latency.
Check at the end of a test: after traffic stops and the design drains, nothing may be outstanding. A hang shows up as leftovers.
Prove it formally: formal tools can check true liveness ("eventually") or show a trace that loops for ever (lesson 15.7).
Watch for fairness assumptions: "eventually granted" usually holds only if the partner eventually becomes ready; state those assumptions explicitly.
// snippet: a liveness rule made bounded (and so checkable in simulation)
// Every request (req) receives a response (rsp) within MAX_LAT cycles.
assert property (@(posedge clk) disable iff (!rst_n)
req |-> ##[1:MAX_LAT] rsp);The bounded form catches hangs and also unexpectedly slow responses; the bound itself becomes part of the specification.
Protocol | Liveness promise | How it is bounded |
|---|---|---|
AXI | A transfer eventually completes once the handshake rules are followed (facts A1 to A3) | Not bounded by the protocol; systems add timeouts |
PCI Express | A non-posted request gets a completion | Completion timeout ranges in Device Control 2 (fact P29) |
DCLink | Every packet is eventually acknowledged | Replay timer (step 9) |
The opening silicon hang (illustrative) was a starvation case: one requester was always beaten by a higher-priority one under a particular traffic mix. Adding a bounded-response assertion (every request granted within 64 cycles) to the random simulation found it in a few hours; a formal run on the arbiter then proved the corrected version could not starve.
Safety: a violation happens at a specific cycle and a finite trace shows it.
After traffic stops and the design should have drained, anything still outstanding proves something never completed.
Safety: nothing bad happens, violated at a cycle you can point to. Liveness: something good eventually happens.
Simulation catches safety violations; liveness needs a bound, an end-of-test drain check, or a formal proof.
Deadlock and starvation are liveness failures; give every liveness rule a checking plan.