2. SVA Guide - Concurrent Assertions
The protocol checker had 47 assertions and a perfect record: three months of regressions, zero failures. During a coverage review, someone added cover property directives mirroring each assertion's antecedent — and 41 of the 47 covers never hit. The assertions weren't passing; they were vacuously passing. A clock-enable refactor months earlier had disconnected the qualifier signal, every antecedent evaluated false forever, and forty-one checks had been politely reporting "true" about nothing at all. The bug they existed to catch shipped in the meantime.
Concurrent assertions are the most powerful checking construct SystemVerilog has — a little declarative language for describing behavior over time — and they have two failure modes that produce silent green: vacuous passes and weak properties that cannot fail. This post rebuilds the guide around using the power and closing both trapdoors: correct implication semantics (with diagrams that actually differ this time), the sequence operators real checkers need, local variables for data integrity, and a ladder down into strong properties, formal, and the checker construct.
|-> with ##2, |=> with ##1) described the same timing, defeating the comparison, and its signal-stability pattern misbehaved on the cycle valid rises. Both are corrected below.The Three-Layer Language
Concurrent assertions are structured like a small language, and keeping the layers straight prevents most syntax confusion:
flowchart TD
S["SEQUENCE — a pattern over cycles
req ##[1:3] ack"] --> P["PROPERTY — sequences + implication,
clock, disable iff"]
P --> D["DIRECTIVE — what to do with it:
assert / cover / assume"]
style S fill:#e0f2fe,stroke:#0284c7
style P fill:#fef3c7,stroke:#d97706
style D fill:#d1fae5,stroke:#059669
sequence req_ack_seq;
req ##[1:3] ack; // pattern: ack 1-3 cycles after req
endsequence
property req_ack_prop;
@(posedge clk) disable iff (reset) // context: clock + abort condition
$rose(req) |-> req_ack_seq;
endproperty
assert property (req_ack_prop) else $error("req without timely ack");
cover property (req_ack_prop); // and prove it actually fires — see below
req in a debugger at the edge and see 1 while the assertion saw 0, nothing is broken: the assertion is evaluating the pre-edge snapshot. Half of all "my assertion is lying to me" debug sessions end at this sentence.Implication: |-> vs |=>, Drawn Correctly
Implication is "if antecedent matched, consequent must hold." The two flavors differ by exactly one cycle — so here is the same consequent under each, one cycle apart:
Overlapping |->: consequent starts the same cycle
property grant_same_cycle;
@(posedge clk) req |-> gnt; // gnt must be high in the SAME sample as req
endproperty
{ "signal": [
{ "name": "clk", "wave": "p......" },
{ "name": "req", "wave": "0.10...", "node": "..a" },
{ "name": "gnt", "wave": "0.10...", "node": "..b" }
], "edge": ["a-b same sample"], "head": { "text": "req |-> gnt : checked at the req sample itself" }, "config": { "hscale": 1.5 } }
Non-overlapping |=>: consequent starts the next cycle
property grant_next_cycle;
@(posedge clk) req |=> gnt; // gnt must be high one sample AFTER req
endproperty
{ "signal": [
{ "name": "clk", "wave": "p......" },
{ "name": "req", "wave": "0.10...", "node": "..a" },
{ "name": "gnt", "wave": "0..10..", "node": "...b" }
], "edge": ["a-b next sample"], "head": { "text": "req |=> gnt : checked one sample later" }, "config": { "hscale": 1.5 } }
The algebra to remember: a |=> b ≡ a |-> ##1 b. Everything else about the two operators is identical — including the part that matters most: if the antecedent never matches, neither operator checks anything. That's a vacuous pass, and it reports as success.
Repetition: [*n], [->n], [=n] — the Interview Trap Explained
| Operator | Name | Meaning |
|---|---|---|
busy[*3] | Consecutive | busy true 3 cycles in a row |
ack[->3] | Goto | 3 (possibly scattered) occurrences of ack; sequence endpoint lands on the cycle of the 3rd ack |
ack[=3] | Non-consecutive | 3 scattered occurrences, and then any number of additional non-ack cycles may pass before the next sequence element |
The goto/non-consecutive distinction — usually hand-waved, always asked in interviews — is about where the sequence ends. Use goto when the next thing must happen immediately at the Nth occurrence; use [=n] when the next thing merely happens sometime after:
// "On the 4th beat (the cycle it occurs), last must be high":
property burst_last_on_4th;
@(posedge clk) $rose(burst_start) |-> (beat_valid[->4]) ##0 last_beat;
endproperty
// "After 4 beats have occurred (whenever), eventually done rises":
property burst_then_done;
@(posedge clk) $rose(burst_start) |-> (beat_valid[=4]) ##1 done;
endproperty
The Sequence Operators Real Checkers Need
The 2016 version stopped at delays and repetition. Production protocol checkers lean on four more:
// throughout — a condition must HOLD during an entire sequence:
property no_abort_during_burst;
@(posedge clk) $rose(start) |->
(!abort) throughout (beat[->4] ##0 last);
endproperty
// within — one sequence must fit inside another's window:
property ack_within_grant_window;
@(posedge clk) $rose(gnt) |->
($rose(ack) ##0 1'b1) within (gnt[*1:8]);
endproperty
// intersect — both sequences match, SAME start, SAME length:
property done_exactly_when_count_hits;
@(posedge clk) $rose(go) |->
(count_q == 0)[->1] intersect (1'b1[*1:16]);
endproperty
// first_match — prune a multi-match sequence to its earliest match:
sequence first_ack;
first_match(##[1:16] ack);
endsequence
throughout alone eliminates a whole class of clumsy hand-rolled state: "valid must stay high until ready" — valid throughout (ready[->1]) — instead of auxiliary flags maintained in an always block next to the assertion.
Local Variables: Checking Data, Not Just Handshakes
Everything so far checks control signals. The step up to real verification power is checking that the right data came back — which requires capturing a value when a sequence starts and comparing it when the sequence ends. That's what sequence local variables do:
// Every read response must return the data written to that address
property write_then_read_returns_data;
logic [31:0] a, d; // local variables
@(posedge clk) disable iff (reset)
($rose(wr_en), a = wr_addr, d = wr_data) // capture at write
##1 ($rose(rd_en) && rd_addr == a) [->1] // next read to same address
|=> (rd_data == d); // must return captured data
endproperty
assert property (write_then_read_returns_data);
Two things make local variables special. First, the capture happens at the sequence position where the assignment is attached — (expr, var = val) — not at some global moment. Second, and this is the part that makes them viable for pipelined protocols: every evaluation attempt gets its own copy. Ten overlapping writes in flight means ten concurrent attempts, each carrying its own captured a and d, each matching its own response. You get a pipelined data-integrity checker in six lines that would take a queue-managing always block forty.
Signal Stability, Done Right
The 2016 version's stability pattern (valid |-> $stable(data)[*1:$] ##1 !valid) misfires on the cycle valid rises: $stable(data) compares against the previous cycle — when the data was legitimately changing into place. The clean formulation checks stability only from the second valid cycle onward:
// While valid STAYS high, data must not change:
property data_stable_while_valid;
@(posedge clk) disable iff (reset)
valid && $past(valid) |-> $stable(data);
endproperty
One cycle of antecedent (valid now and last cycle), one cycle of check. No unbounded repetition, no off-by-one at the rising edge, and it fails on exactly the cycle the data glitched — not at some distant sequence endpoint.
The Two Trapdoors to Silent Green
Trapdoor 1 — Vacuous passes
If the antecedent never matches, the assertion passes without checking anything — the cold open's forty-one zombies. The discipline that prevents it costs one line per assertion:
assert property (p_req_ack) else $error("...");
cover property (@(posedge clk) $rose(req)); // prove the antecedent LIVES
Review the cover counts at regression end (most tools also have a vacuity-reporting option — turn it on). An assertion whose antecedent cover is zero isn't a passing check; it's a dead one.
Trapdoor 2 — Weak properties that cannot fail
This one is nastier because even non-vacuous assertions are affected: req |-> ##[0:$] ack — "eventually ack" — is a weak property. If ack simply never arrives, the attempt is still pending at end of simulation, and a pending weak property does not fail. The assertion literally cannot report the bug it was written for. Fixes, in order of preference:
// Best: bound it — protocols have timeouts; encode them
property req_ack_bounded;
@(posedge clk) disable iff (reset) $rose(req) |-> ##[1:64] ack;
endproperty
// When genuinely unbounded: use a STRONG operator — pending at end-of-sim = FAIL
property req_ack_strong;
@(posedge clk) disable iff (reset) $rose(req) |-> s_eventually ack;
endproperty
Binding a Checker to RTL
bind attaches assertions to a design without touching its source — the mechanism VIP protocol checkers ride in on (see Understanding VIP). The APB example, with every port now earning its keep:
module apb_protocol_checker (input logic clk, psel, penable, pready);
// Setup phase: first cycle of psel has penable low
property apb_setup; @(posedge clk) $rose(psel) |-> !penable; endproperty
// Access phase follows setup immediately
property apb_access; @(posedge clk) (psel && !penable) |=> penable; endproperty
// Slave must answer: pready within 16 cycles of access phase
property apb_ready; @(posedge clk) $rose(psel && penable) |-> ##[0:15] pready; endproperty
// Signals hold until the transfer completes
property apb_hold; @(posedge clk) (psel && penable && !pready) |=> penable; endproperty
assert property (apb_setup) else $error("APB: penable high in setup phase");
assert property (apb_access) else $error("APB: access phase did not follow setup");
assert property (apb_ready) else $error("APB: slave never asserted pready");
assert property (apb_hold) else $error("APB: penable dropped mid-transfer");
cover property (@(posedge clk) $rose(psel)); // the checker is alive
endmodule
bind apb_master apb_protocol_checker chk (
.clk(pclk), .psel(psel), .penable(penable), .pready(pready)
);
Common Mistakes
- Assertions with no paired cover. Green means "checked and held" only if the antecedent fired. Prove it fired.
- Unbounded
##[0:$]in an assert. Weak semantics — it can never fail. Bound it or go strong (s_eventually). $stable/$pastat the start of a window. They look one cycle back — on the first cycle of a burst that's the pre-burst value. Qualify with$past(valid)-style guards.- Logic in
disable iff. It's an asynchronous abort evaluated continuously, not a sampled condition — keep it to reset-like signals only, or attempts die at moments you never intended. - Confusing
[->n]and[=n]. Goto pins the endpoint to the Nth occurrence;[=n]lets trailing cycles pass. Concatenating##0 xafter[=n]rarely means what you hoped. - Free-running assertions on un-reset signals. The first samples after time zero see Xs; gate with
disable iff (!rst_done)or you open every regression with noise failures.
Interview Corner
Q:|-> vs |=> in one sentence, plus the identity connecting them?
A: Overlapping |-> starts checking the consequent in the same sample where the antecedent matched; non-overlapping |=> starts one sample later; and a |=> b is exactly a |-> ##1 b.
assert property (req |-> ##[0:$] ack) never fail, and what do you do about it?
A: Unbounded delay makes it a weak property: if ack never comes, the attempt is still pending at end of simulation, and pending weak attempts don't fail. Bound the window to the protocol's real timeout, or use a strong operator like s_eventually, whose pending attempts do fail at end of sim.
A: When the antecedent doesn't match, the implication is trivially true — the tool reports a pass though nothing was checked. Detection is structural: pair every assert with a cover on its antecedent and treat zero cover hits as a broken check, plus enable the simulator's vacuity reporting. An assertion nobody has ever seen fail or cover is not evidence of correctness; it's evidence of disconnection.
Q: How do local variables in sequences handle five overlapping transactions?A: Each evaluation attempt spawns with its own private copy of the sequence's local variables — five in-flight transactions means five concurrent attempts, each carrying the address/data it captured at its own start and each matching its own completion. That per-attempt storage is what makes SVA viable for pipelined data-integrity checks, not just handshakes.
Beyond the Basics: Advanced → Expert
Level 1 — The assert/cover contract as methodology
Scale the pairing discipline from habit to structure: every property file ships assert + antecedent-cover + a "did the interesting thing happen" cover (not just $rose(req) but req ##[1:64] ack completing). At regression end, three numbers per checker — failures, vacuity rate, cover hits — go in the report next to coverage. A protocol checker is itself a DUT: the covers are its coverage model, and the error-injection tests that force each assertion to fire (see the VIP post's Level 2) are its regression.
Level 2 — Weak vs strong, systematically
The ##[0:$] trapdoor is one instance of a general axis: SVA properties are weak by default (pending = pass at end of sim), and 1800-2012 added the strong family — s_eventually, s_until, s_nexttime, and strong(seq) — where pending = fail. The engineering rule: safety properties ("nothing bad happens") are naturally weak and bounded; liveness properties ("something good eventually happens") are only meaningful strong or bounded. Audit any checker library by grepping for $] inside asserts: each hit is either a missing bound, a missing s_, or a check that has never been able to fail.
Level 3 — The checker construct: assertions with their own state
When a check needs bookkeeping (an expected-occupancy counter, a mode shadow register), the usual move is an always block beside the assertions — unencapsulated, unreusable. SystemVerilog's checker...endchecker (1800-2009) exists for exactly this: a container that packages assertions plus the auxiliary modeling they need, instantiable in modules and procedural contexts, bindable like a module:
checker fifo_occupancy_check (input logic clk, rst_n, push, pop, input int unsigned DEPTH);
int unsigned count = 0;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) count <= 0;
else count <= count + (push && !pop) - (pop && !push);
assert property (@(posedge clk) disable iff (!rst_n)
!(push && count == DEPTH)) else $error("push to full FIFO");
assert property (@(posedge clk) disable iff (!rst_n)
!(pop && count == 0)) else $error("pop from empty FIFO");
endchecker
Almost nobody uses checkers; almost everybody hand-rolls what checkers provide. Being the person on the team who knows this construct is a cheap superpower.
Level 4 — The same properties, under a formal engine
Everything in this post is also the input language of formal property verification — with the directives changing roles. In simulation, assume property is a constraint documented; under formal, it prunes the state space (garbage assumptions = vacuous proofs, the formal twin of Trapdoor 1). assert becomes a proof obligation over all reachable behavior — a full proof is exhaustive in a way no regression is; a bounded proof ("holds for 40 cycles from reset") is a weaker but still potent claim. cover becomes reachability: the engine hands you a witness trace showing how a scenario can occur, which is also the fastest protocol-understanding tool ever shipped. The practical entry point: take your bound checker module, add input assumptions for the legal stimulus space, and run the same file under a formal tool — bugs in the checker itself surface within minutes, which is why formal teams say "formal verifies your assertions before it verifies your design."
Level 5 — Assertion cost and the simulation budget
Every attempt of every property is a lightweight thread; unbounded windows and long [*m:n] ranges multiply them. The expensive shape: an antecedent that matches every cycle feeding an unbounded consequent — thousands of concurrent attempts, each holding local-variable state. Mitigations, in order: tighten antecedents ($rose(req) spawns per-event; bare req spawns per-cycle of a held request), bound every window to the protocol timeout, use first_match to kill redundant matches, and when a check genuinely wants transaction-lifetime state across thousands of cycles — move it to the scoreboard, which is the right tool for long-horizon bookkeeping (the layered-checking table in the VIP post). Profile before guessing: most simulators report per-assertion attempt counts and time; the top three lines of that report usually contain one property doing 90% of the damage.
Key Takeaways
- Three layers: sequences (patterns) → properties (context) → directives (assert/cover/assume). Sampling is preponed — assertions see pre-edge values.
a |=> b≡a |-> ##1 b; goto[->n]pins the endpoint,[=n]doesn't.throughout/within/intersect/local variables are where real checkers live.- Two roads to silent green: vacuous passes (pair every assert with a cover) and weak unbounded properties (bound them or use
s_eventually). - Encapsulate stateful checks in
checkerconstructs; bind checkers to RTL; feed the same properties to formal, where assume/assert/cover swap into constraint/proof/reachability. - Assertions have a runtime budget: tight antecedents, bounded windows,
first_match— and move long-horizon bookkeeping to the scoreboard.
Comments (0)
Leave a Comment