Concurrent Assertions

Immediate Assertions check a condition at one instant — the moment the assert statement executes. Many real hardware rules aren't instantaneous at all: "if a request is asserted, the grant must arrive within 4 cycles," or "valid and ready must never both glitch in the same cycle a reset is asserted." Checking a rule like that by hand means writing a small state machine just to track it — exactly the kind of repetitive, error-prone testbench code SystemVerilog Assertions (SVA) exist to eliminate.

assert property: the basic shape

property valid_implies_ready;
    @(posedge clk)
    valid |-> ready;
endproperty

assert property (valid_implies_ready)
else $error("valid asserted without ready");

A property is a temporal expression — evaluated relative to a clock (@(posedge clk) here), not at one instant. |-> is the implication operator: "if the left side is true this cycle, the right side must also be true this cycle" (a same-cycle implication; the double-arrow form |=> checks the right side one cycle later instead — covered below). assert property (...) continuously checks the property, cycle after cycle, for as long as the simulation runs — not a one-time check like an immediate assertion, but a standing rule the design must never violate.

$rose and $fell: detecting edges on any signal

property grant_after_request;
    @(posedge clk)
    $rose(request) |-> ##[1:4] grant;
endproperty

assert property (grant_after_request);

$rose(signal) is true exactly on the cycle a signal transitions from 0 to 1 (rising edge, on any signal — not just a clock); $fell(signal) is the mirror for 1-to-0. ##[1:4] is a cycle-delay range — "somewhere between 1 and 4 cycles later." Read the whole property as: "whenever request rises, grant must become true somewhere in the next 1 to 4 cycles" — exactly the kind of multi-cycle rule an immediate assertion has no way to express at all, and that a hand-written checker would need its own small counter and state machine to track.

Sequences: naming a reusable temporal pattern

sequence req_then_ack;
    @(posedge clk)
    req ##1 ack;
endsequence

property req_ack_no_double_ack;
    req_then_ack |-> ##1 !ack;
endproperty

assert property (req_ack_no_double_ack);

A sequence names a temporal pattern (req, followed one cycle later by ack) so it can be reused across multiple properties without re-writing the pattern each time — the same motivation as naming any other reusable piece of logic. Properties are usually built out of one or more named sequences plus the boolean/implication logic connecting them, exactly as req_ack_no_double_ack reuses req_then_ack above.

##1 vs. |=>: same-cycle vs. next-cycle implication

Operator	Checks the consequent
|->	In the same cycle as the antecedent
|=>	One cycle after the antecedent (shorthand for |-> ##1)

property no_immediate_reread;
    @(posedge clk)
    write |=> !read;    // one cycle after a write, read must be low
endproperty

This distinction matters constantly in real protocol checking — a handshake signal that must respond in the same cycle it's requested needs |->; one that's only allowed to respond starting the next cycle needs |=>, and using the wrong one either falsely fails a legitimate design or lets a real protocol violation through undetected.

disable iff and $past: surviving reset, and reasoning about a prior cycle

property counts_up_while_enabled;
    @(posedge clk) disable iff (reset)
    enable |=> q == $past(q) + 1;
endproperty

assert property (counts_up_while_enabled);

Right after @(posedge clk) and before the property's actual body, disable iff (reset) tells the checker to skip evaluating the property entirely on any cycle where reset is true — without it, a property would keep evaluating through reset too, and since most signals are still settling into their known reset values (or briefly X) during that window, a property that's perfectly correct once the design is running can spuriously fail before reset even finishes. $past(expr) reaches back and returns expr's value from the previous clock cycle (the property's own clocking event, here @(posedge clk)) — counts_up_while_enabled above reads as "whenever enable was true, q this cycle must equal q from last cycle plus one." $past isn't limited to one cycle back either: a second argument, $past(expr, N), reaches back N cycles instead of the default of 1.

throughout and intersect: relating a condition to a whole sequence

property busy_holds_during_transfer;
    @(posedge clk)
    req |-> (busy throughout (##[1:3] ack));
endproperty

sequence early_done;
    ##[1:3] done;
endsequence

sequence late_done;
    ##[2:4] done;
endsequence

property done_lands_in_overlap;
    @(posedge clk)
    req |-> (early_done intersect late_done);
endproperty

Two more operators combine a plain condition with a sequence's timing: throughout requires a boolean expression (busy above) to stay true for the entire duration of another sequence (##[1:3] ack), not just at its start or end — the whole expression only matches if busy never drops during that window. intersect requires two sequences (both starting at the same cycle) to each match and end on the exact same cycle as each other — above, early_done intersect late_done only matches on a done landing in cycles 2 or 3, the overlap of [1:3] and [2:4]; unlike a plain and, which only needs both sequences to eventually match without caring whether they finish together, intersect is the tighter check for "these two timing windows must actually agree."

Why concurrent assertions matter for verification specifically

A well-written set of concurrent assertions catches protocol violations at the exact cycle they occur, with the exact signal values involved — dramatically faster to debug than noticing, several cycles later, that a scoreboard's final output comparison came back wrong and then working backward through a waveform to find where things actually went wrong. This is also the basis of assertion-based verification (ABV) as a complementary strategy to the scoreboard-based checking Testbench covers — assertions catch protocol/timing bugs close to their source; a scoreboard catches whether the DUT's overall functional behavior was correct. Real verification environments use both, not one instead of the other.

What's next

Assertions check that behavior is correct. The next page covers a related but different question: functional coverage — tracking what's actually been exercised by a test, independent of whether it passed or failed, using covergroup and coverpoint.