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 | Path | What it covers |
|---|---|---|
Optional | accept_on, reject_on and their sync forms, how they differ from disable iff, and an unrolled rewrite that runs here. | |
Optional | Properties that instantiate themselves, the four LRM restrictions, and when recursion beats repetition. | |
Recommended | let helpers, parameterized properties and one checker library bound to two different DUTs. | |
Required | Matching responses to requests by ID under out-of-order traffic, and the table rules local variables cannot express. | |
Recommended | assume and restrict, safety versus liveness, s_eventually, and habits that let a formal tool use your assertions. |
Path says how much of each lesson a first pass needs. Required: core for this topic, read it. Recommended: most learners should read it. Optional: reference, specialist or revision material; skip it on a first pass and return when you need it.
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.