Assertions (SVA)

SystemVerilog Assertions (SVA) express temporal/protocol correctness properties directly in the language, and check them continuously during simulation (and can be reused, largely unchanged, in formal verification).

Immediate vs. concurrent assertions

Immediate assertions check a condition at the instant they execute — procedural, like an if:

always_comb begin
  a_no_x_addr: assert (!$isunknown(addr)) else $error("addr has X/Z bits");
end

Concurrent assertions check a temporal property, sampled on every clock edge, and can span multiple cycles:

property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:4] ack;
endproperty
a_req_ack: assert property (p_req_ack)
  else $error("ack did not follow req within 4 cycles");

Immediate assertions are for "this combinational condition must hold right now." Concurrent assertions are for "this sequence of events must hold over time" — the overwhelming majority of real protocol-correctness checks (handshakes, latency bounds, ordering) need concurrent assertions, not immediate ones.

Reading the operators

• |-> (overlapping implication): if the antecedent holds this cycle, the consequent must hold starting the same cycle.
• |=> (non-overlapping implication): consequent must hold starting the next cycle.
• ##N: delay of exactly N cycles.
• ##[N:M]: delay of somewhere between N and M cycles (bounded — unbounded ##[N:$] is legal but expensive in simulation and often disallowed/warned-on for formal).

// "if req is high this cycle, valid must be high exactly 2 cycles later"
req |-> ##2 valid;

// "if req is high this cycle, ack must go high within 1 to 4 cycles"
req |-> ##[1:4] ack;

|-> vs |=> is a frequent off-by-one bug source

Writing req |-> ack (same-cycle) when you meant "ack the cycle after req" (req |=> ack) is one of the most common SVA authoring mistakes — it silently changes what's being checked rather than causing an error, since both are syntactically valid. Simulate a known-good trace and confirm the assertion actually fires/doesn't-fire when expected before trusting it in a full regression.

disable iff and reset

Almost every concurrent assertion needs disable iff (!rst_n) (or equivalent) — without it, the assertion is also evaluated during reset, when signals are typically in an undefined or transitional state, producing false failures that have nothing to do with real DUT behavior. This is the single most common reason a "flaky" assertion turns out not to be flaky at all — it's failing on every reset, and nobody noticed because the failures were dismissed as noise.

Sequences as reusable building blocks

sequence seq_valid_data;
  valid ##0 !$isunknown(data);
endsequence

property p_valid_no_x;
  @(posedge clk) disable iff (!rst_n)
  seq_valid_data;
endproperty
assert property (p_valid_no_x);

Factoring shared temporal patterns into named sequences (not just properties) pays off quickly once a protocol checker has more than 3-4 properties — the same handshake/timing pattern usually recurs across many properties, and a bug fixed once in a shared sequence fixes every property that uses it.

Where these checks live

Protocol assertions are typically bound into the DUT (or a bus-functional interface) via a bind statement rather than hand-instantiated inside every testbench that uses that interface — one assertion set, reusable across every test and every level of integration that includes the same interface, without modifying the DUT/interface source itself:

bind axi_if axi_protocol_checker u_axi_chk (.clk(clk), .awvalid(awvalid), /* ... */);