SVA System Functions

SystemVerilog provides built-in system functions to easily detect signal edges and sample values from the past. These are essential for writing concise assertions.

Sampled Values (The Concept)

In concurrent assertions, values are sampled in the Preponed region (right before the clock edge). This avoids race conditions. SVA functions like $rose work on these sampled values.

Edge Detection

$rose(expr): Returns true if LSB of expr went from 0 to 1.
$fell(expr): Returns true if LSB of expr went from 1 to 0.
$stable(expr): Returns true if value hasn't changed from previous clock.

// "If Write Enable rises, then Valid must be High"
$rose(wr_en) |-> valid;

// "Address must remain stable while Request is high"
req |-> $stable(addr);

Past Values ($past)

$past(expr, N) returns the value of expression expr from N clock cycles ago.

// "Data Out now must equal Data In from 2 cycles ago (Pipeline check)"
data_out == $past(data_in, 2);

Note: $past is useful but expensive in formal verification as it increases state depth. Use it judiciously.

Common Interview Questions

Q: What region are SVA variables sampled in?

Preponed Region. This is the very beginning of the time slot, before any events (active region) occur. It ensures assertions check values before they change on the active clock edge.

Q: Does $rose check for 0->1 or X->1?

$rose specifically checks if the LSB changed to 1 from any non-1 value (0, X, or Z). However, usually we care about 0->1.

Previous Temporal Operators Next Assertion Binding