Advanced SVA: Sequences and Properties
Multi-cycle behavior, implication, and avoiding vacuous pass
Basic assertions checked single conditions and a simple "request then ack" rule. Advanced SystemVerilog Assertions describe behavior that unfolds over many cycles, with overlap, repetition, and precise timing. A sequence is a temporal pattern: ## advances clock cycles, [*n] repeats the preceding expression for n consecutive cycles, and [->n] waits for its n-th occurrence.
Sequence and implication operators
| Syntax | Meaning |
|---|---|
| a ##1 b | b is true the cycle after a |
| a ##[1:3] b | b is true 1 to 3 cycles after a |
| a [*3] | a holds for 3 consecutive cycles |
| a [->2] | a is true on its 2nd occurrence (goto repeat) |
| p |-> q | Overlapping: q starts the cycle p completes |
| p |=> q | Non-overlapping: q starts the next cycle (same as p |-> ##1 q) |
// On a read, addr must stay stable for 2 cycles, then valid must rise
// within 1 to 4 cycles and the returned data must not contain X/Z.
property read_xfer;
@(posedge clk) disable iff (!rst_n)
(start && rd) |=> (addr == $past(addr)) [*2]
##[1:4] valid && !$isunknown(data);
endproperty
assert property (read_xfer) else $error("read protocol violated");- disable iff (!rst_n) - abandon any in-progress check while reset is asserted, so reset cannot cause spurious failures.
- $past(addr) - the value of addr one clock earlier, used here to assert stability.
- $isunknown(data) - true if any bit of data is X or Z, the correct way to forbid unknowns.
To check that a response matches the request that caused it, a property must remember a value sampled at one point and compare it later. A local variable, declared inside the property, captures a value in the antecedent (here t = tag) and uses it in the consequent.
property tag_match;
bit [3:0] t;
@(posedge clk) (req, t = tag) |-> ##[1:8] (rsp && rsp_tag == t);
endproperty
assert property (tag_match);Pair every assert property with a cover property on the same antecedent. The assert proves the rule is never broken; the cover proves the rule was actually exercised. Without the cover you cannot tell a genuine pass from a vacuous one, where the antecedent simply never fired and the property passed by doing nothing.
Vacuous pass is the silent killer of assertion-based verification. If start && rd never occurs, read_xfer reports pass forever while testing nothing. Watch the assertion coverage, not just the pass count, and remember that |-> and |=> only constrain the consequent when the antecedent matches, so an antecedent that is too narrow makes a strong-looking property meaningless.