Lesson 3.3 · SystemVerilog Assertions Essentials

Concurrent assertions, clocks and sampling

A concurrent assertion is evaluated at clock edges and can describe behaviour across many cycles. Its general shape:

shape of a concurrent assertion

label: assert property ( @(posedge clk) disable iff (rst)  <property_expression> );

Sampling: what value does the assertion see?

Concurrent assertions use the value each signal had just before the clock edge — formally, in the Preponed region of the time step. That is exactly the value a flip-flop clocked on the same edge would capture. If a signal changes right at the edge, the assertion sees the old value.

At the edge that starts cycle 1, valid is rising — but the assertion samples the value before the edge (0). It first sees valid = 1 at the edge that starts cycle 2.

Sampled-value functions

Function	True / returns…	Typical use
`$past(x)`, `$past(x, n)`	Value of x one (or n) clock ticks ago	Compare with history: `out == $past(in)`
`$rose(x)`	LSB of x went 0 → 1 since the last tick	Detect a request start
`$fell(x)`	LSB of x went 1 → 0 since the last tick	Detect end of busy
`$stable(x)`	x unchanged since the last tick	Data held while waiting
`$changed(x)`	x changed since the last tick	Detect updates
`$onehot(x)` / `$onehot0(x)`	Exactly one bit / at most one bit set	Grants, selects, FSM encodings
`$countones(x)`	Number of 1 bits	Population limits
`$isunknown(x)`	Any bit is X or Z	X-checks in simulation / X-prop apps

using sampled-value functions

// Data must not change while a transfer is stalled
a_data_stable: assert property (@(posedge clk) disable iff (rst)
                 valid && !ready |=> $stable(data));

// A pipeline stage delays its input by exactly two cycles
a_two_stage:   assert property (@(posedge clk) disable iff (rst)
                 out == $past(in, 2));

Default clocking and disable iff

Repeating @(posedge clk) disable iff (rst) in every property is noisy. Declare defaults once per module:

defaults

default clocking cb @(posedge clk); endclocking
default disable iff (rst);

// Now properties are short and readable
a_onehot_gnt: assert property ($onehot0(gnt));
a_gnt_req:    assert property (|gnt |-> |(gnt & req));

disable iff (rst) means: while rst is high, any evaluation in progress is discarded (neither pass nor fail). It is asynchronous to the property's clock — it takes effect as soon as rst is seen.