Advanced SVA: Sequences and Properties

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

// 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);