Part 4 taught the SVA operators one by one. This topic covers what senior engineers are asked to own: properties that end early on purpose, properties that carry state through recursion, assertion libraries shared by many blocks, ID tracking under outstanding traffic, and assertions a formal tool can prove.
The free simulator here (Verilator 5.048 with --assert) runs only part of SVA. Each lesson tells you what ran, what did not, and how the meaning was checked instead: against the IEEE 1800 text, with a trace table, or with an equivalent check that does run.
WHERE EACH LESSON SITS
property ends early on an event ......... abort operators (accept_on, reject_on, sync_*)
property carries state cycle to cycle .... recursive properties
one rule, many blocks .................... let + parameterized properties + bind
one rule, many transactions in flight .... local variables (one copy per attempt)
one rule, proved instead of simulated .... formal-ready assertions (assume, liveness)Lesson | What it covers |
|---|---|
accept_on, reject_on and their sync forms, how they differ from disable iff, and an unrolled rewrite that runs here. | |
Properties that instantiate themselves, the four LRM restrictions, and when recursion beats repetition. | |
let helpers, parameterized properties and one checker library bound to two different DUTs. | |
Matching responses to requests by ID under out-of-order traffic, and the table rules local variables cannot express. | |
assume and restrict, safety versus liveness, s_eventually, and habits that let a formal tool use your assertions. |
These results come from small directed tests run while writing this topic. Other tools and later versions differ, so treat the table as a map of this site's runnable examples, not as a statement about SVA.
Construct | Result with verilator --assert |
|---|---|
accept_on, reject_on, sync_accept_on, sync_reject_on | Rejected: "Unsupported" |
Recursive property | Rejected: "Unsupported: Recursive property call" |
s_eventually, s_until, s_until_with, s_nexttime, s_always, nexttime, always, eventually[ ], strong( ), weak( ) | Rejected: "Unsupported" |
until, until_with, implies, assume, restrict, let, checker | Compiled; until gave correct results on our traces |
| Correct on our traces |
| Wrong verdicts on our traces |
| Missed failures: when b held for the first repetition and dropped on the second, no failure was reported. The written-out |
Local variables in properties | Compiled, but the value was not held: the check used the signal's current value |
Several attempts failing in the same cycle | Action block ran once, so counts are per cycle, not per attempt |
No. Several constructs in the table compile and still give wrong verdicts. Before trusting a new construct in a tool, run a short directed trace where you know the answer, including one that must fail.