Properties and implication
Most assertions follow the pattern "whenever X happens, Y must follow". SVA expresses this with the implication operators. The left side is the antecedent, the right side the consequent.
| Operator | Name | Consequent starts… |
|---|---|---|
A |-> B | overlapping | in the same tick the antecedent match ends |
A |=> B | non-overlapping | one tick after the antecedent match ends (same as A |-> ##1 B) |
Vacuous success
An implication whose antecedent never matches is vacuously true. In the waveform above, the property is also evaluated at cycles 0, 2, 3 — the antecedent is false there, so those attempts pass vacuously. That is intended. But if the antecedent can never be true — because of a typo, a wrong polarity, or an over-constraining assumption — the assertion is proven while checking nothing.
// Typo: the antecedent is a contradiction - it can never be true
a_oops: assert property (req && !req |=> gnt); // "proven", checks nothing
// Defence: cover the antecedent of every important implication
c_ante: cover property (req && !gnt);Most formal tools also report vacuity automatically. Read those reports — they are among the most valuable output a tool gives you.
Useful property operators
| Operator | Meaning |
|---|---|
not P | P does not hold |
P and Q, P or Q | Property conjunction / disjunction |
if (c) P else Q | Conditional property |
P until Q | P holds on every tick until Q (Q may never come — weak) |
P s_until Q | Same, but Q must eventually come (strong) |
s_eventually P | P must hold at some future tick (liveness) |
always P | P holds on every tick from now on |
Safety versus liveness
A safety property says something bad never happens; any violation has a finite counterexample (e.g. two grants at once). A liveness property says something good eventually happens (e.g. every request is eventually granted); a violation is an infinite trace where the good thing never happens. Formal tools show liveness counterexamples as a loop: a prefix followed by a cycle of states that repeats forever.
// Liveness: every request is eventually granted
a_live: assert property (req |-> s_eventually gnt);
// Bounded safety alternative: granted within 8 ticks (often easier to prove, and more precise)
a_bounded: assert property (req |-> ##[0:7] gnt);