An assertion often needs to compare what a signal is doing now with what it did at an earlier clock edge. Did a request become high? Did data change? Does an output match an input from three cycles ago?

SystemVerilog provides sampled value functions to express these checks directly. This tutorial explains their timing, shows practical assertions, and demonstrates why a passing assertion can still miss a design bug.

$rose function

If there is a change in the least significant bit (LSB) of an expression from 0 or x or z (previous clocking event value) to 1, then the $rose function returns true, otherwise returns false.

Syntax:

$rose (expression, <clocking_event>)

To understand the importance of $rose, let’s understand how it is used for a design requirement.

The clock may be supplied explicitly or inferred from the assertion or procedural context.

Previous sample	Current sample	`$rose`
0	1	1
X or Z	1	1
1	1	0
1	0	0
0	X or Z	0

Design specification

For a request sampled at C1, ‘ready’ should become high exactly 3 clock cycles later ( i.e. ‘ready’ must remain low at C1, C2, and C3, then become high at C4)

Figure 1: Expected response: request at C1, response at C4.

First, consider a property that checks only the value of ready:

property prop;
  @(posedge clk) disable iff (!rst_n)
    req |-> ##3 ready;
endproperty

ap_ready: assert property (prop);

|-> starts the consequent at the same clock as the request. ##3 then advances three clocks, from C1 to C4.

Signal / case	C1	C2	C3	C4
`req`	1	0	0	0
Correct `ready`	0	0	0	1
Early `ready`, held high	0	1	1	1

Both cases pass because ready is high at C4. The property does not check when it first became high.

If there is a bug in RTL and ready is asserted before 3 clock cycles.

The above property will not capture this RTL defect. So, $rose(ready) is used to capture such a bug.

Figure 2: Early assertion that remains high: the level check misses the violation.

Replacing ready with $rose(ready) requires a sampled rising transition at C4:

property prop;
  @(posedge clk) disable iff (!rst_n)
    req |-> ##3 $rose(ready);
endproperty

ap_ready: assert property (prop);

This version detects the early-held-high case. Since ready is 1 at both C3 and C4, $rose(ready) is 0 at C4, and the assertion attempt fails.

However, it still does not prohibit an earlier pulse:

Signal	C1	C2	C3	C4
`req`	1	0	0	0
`ready`	0	1	0	1
Observation	Request	Early pulse	Low again	Rises again

Figure 3: Early pulse followed by another rise: even the $rose check passes.

The request attempt passes at C4: ready was 0 at C3 and is 1 at C4. The early pulse at C2 is not constrained by this property.

$rose compares consecutive samples. It does not mean “the first rise since the request.”

To enforce the complete specification, explicitly require the earlier low values:

property prop;
  @(posedge clk) disable iff (!rst_n)
    req |-> (!ready)[*3] ##1 ready;
endproperty

ap_ready: assert property (prop);

(!ready)[*3] requires three consecutive low samples at C1, C2, and C3. ##1 ready then requires a high sample at C4. Both early-assertion cases fail at C2.

An additional $rose(ready) at C4 is unnecessary because the sequence already requires 0 at C3 and 1 at C4.

`ready` samples at C1–C4	`##3 ready`	`##3 $rose(ready)`	(!ready)[*3] ##1 ready;
`0 0 0 1`	Pass	Pass	Pass
`0 1 1 1`	Pass	Fail	Fail
`0 1 0 1`	Pass	Pass	Fail
`0 0 0 0`	Fail	Fail	Fail

If ready is unrestricted at C1 and must be low only at C2 and C3, use req |-> ##1 (!ready)[*2] ##1 ready instead.

Choosing the request trigger: req starts an attempt on every clock where it is high. Use $rose(req) if a new request is defined by its sampled rising transition. A complete protocol may also need checks for unsolicited responses and response width.

Example in procedural block

always @(posedge clk) begin
  if ($rose(ack))
    $display("ack has a sampled rising transition");
end

The function infers posedge clk as its sampling clock and compares the current ack sample with the previous one. It does not monitor every asynchronous edge on ack.

Example for continuous assignment

wire ack_rose;
assign ack_rose = $rose(ack, @(posedge clk));

The explicit clock defines the samples used by $rose. This expression reports a sampled transition; it is not an asynchronous edge detector.

Difference between @posedge and $rose

@(posedge <signal>) is an event operator (blocking). Used to trigger procedural blocks (e.g., always @(posedge clk)). It suspends execution until a rising edge (0/X/Z->1 transition) occurs on the specified signal.

Event-based
Triggers exactly at the transition

$rose(<signal>) is a system function (sampled). Used inside SystemVerilog Assertions (assert property) or Coverage (cover property). $rose returns true if the least significant bit (0/X/Z) of the expression changed to 1. Otherwise, it returns false

Sampled function
Evaluated only at clocking events
Requires two samples

When to Use Which

Use @posedge to implement RTL logic or trigger procedural blocks in simulation.
Use $rose() when you want to check or detect that an edge occurred (e.g., checking requirements in formal verification, assertions, and functional coverage).

$fell function

If there is a change in the least significant bit (LSB) of an expression from 1 or x or z (previous clocking event value) to 0, then the $fell function returns true, otherwise returns false.

Syntax:

$fell (expression, <clocking_event>)

Design specification

If the signal reset goes low (means reset is removed) then data should not be X or Z

Figure 4: Reset release at C2: $fell(reset) triggers the data-knownness check.

property prop;
  @(posedge clk)
    $fell(reset) |-> !$isunknown(data);
endproperty

ap_data_on_release: assert property (prop);

For active-high reset, 1-to-0 means release. For active-low reset rst_n, 0-to-1 means release, so use $rose(rst_n) instead.

In Figure 4, reset is 1 at C1 and 0 at C2, so $fell(reset) is 1 at C2. The data sample at C2 is 8'h3C, which contains no X/Z, and the check passes. Data may be X at C1 because this property checks only the release event. The later change to 8'hA5 is also allowed; no data-stability requirement was specified.

As defined above, X-to-0 and Z-to-0 also make $fell true. If the requirement permits only a known 1-to-0 reset release, use ($past(reset) === 1'b1 && reset === 1'b0) as the antecedent and ensure valid history.

The property checks data at the clock that detects release. If the specification allows one additional clock, use |=>. A clock-sampled check does not test data at the asynchronous instant reset changes.

Example in procedural block

always @(posedge clk) data = $fell(reset)? 0: x;

Example for continuous assignment

assign out = $fell(in1 & in2, @posedge clk);

$stable function

If there is no change in the value of an expression from the previous clocking event value then the $stable function returns true, otherwise returns false.

Syntax:

$stable (expression, <clocking_event>)

Example: Whenever valid is sampled high, wdata must equal its value at the previous clock sample.

property prop;
  @(posedge clk) disable iff (!rst_n)
    valid |-> $stable(wdata);
endproperty

ap_stable_wdata: assert property (prop);

If valid is high at C2, this compares wdata(C2) with wdata(C1). It does not impose a next-clock requirement. It also constrains the first cycle where valid becomes high, so use it only if the data must already have been present at the preceding sample.

For a different requirement—hold a stalled transfer through the next clock—write:

ap_hold_when_stalled: assert property (
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> (valid && $stable(wdata))
);

A stall at C1 requires valid to remain high at C2 and wdata(C2) to equal wdata(C1). Repeated stalls extend the check through the acceptance clock. The choice between |-> and |=> follows the timing requirement.

Example in procedural block

always @(posedge clk) begin
  if(!($stable(data) && valid)) $display("data is not stable when valid is high");
end

Note:

Both $rose and $fell function only consider the LSB bit of an expression. So, it is better to use a single-bit signal.
The clocking event is optional to use.
If clocking event is not used then
a. Derived from a clocking event used in an assertion.
b. Inferred clock from procedural block

$past function

The $past() function is used to sample/ return the value of an expression or signal for the given number of clock cycles in the past.

Syntax:

$past(<expression>, <number_of_cycles>, <gating_expression>, <clock_event>);

The default value for the number of clock cycles is 1 if not specified.
The gating expression is an optional expression for the clocking event.
A clocking event is also an optional event. It will infer an assertion or property clocking event if it is not specified.

Design specification

For a request, ready should be asserted after 3 clock cycles. In another way, req should be set 3 clock cycles before ready is asserted.

property prop;
  @(posedge clk) disable iff (!rst_n)
    $rose(ready) |-> $past(req, 3);
endproperty

ap_response_has_request: assert property (prop);

A rise at C4 checks req at C1.

This is a backward check: it asks whether a response had an earlier request. It is not equivalent to req |-> ##3 $rose(ready), which requires a future response for each request. If a request receives no response, only the forward check detects that missing response.

Example in procedural block

The previous cycle value of the req signal is used in the below example.

always @(posedge clk) begin
  out <= ack & $past(req);
end

$onehot

The $onehot returns true if a single bit of an expression/ signal is high, otherwise for an expression/ signal has x or z value, $onehot will fail.

Syntax:

$onehot(<expression>)

Design requirement

To read data from SRAM, there can be multiple requests from various sources. There can be only one done signal along with a ready signal.

property prop;
  @posedge(clk) disable iff (rst) ready |-> $onehot(done)
endproperty

Whenever ready is high at the same cycle, the done signal should have at least one bit to be high.

$onehot0

The $onehot0 returns true if at most one bit of an expression/ signal is high (i.e. all bits are 0 or at least one bit is 1) otherwise for an expression/signal that has x or z value, $onehot0 will fail.

Syntax:

$onehot0(<expression>)

$isunknown

The $isunknown returns true if any bit of an expression or signal is x or z.

Syntax:

$isunknown(<expression>)

Example: When en bit is set, addr and data signal should not have x or z value.

property prop;
  @(posedge clk) disable iff (!rst_n)
    en |-> !$isunknown({addr, data});
endproperty

ap_transfer_known: assert property (prop);

The concatenation checks both buses. This property does not require them to be known when en is low.

If en itself must always be known, add a separate check:

ap_enable_known: assert property (
  @(posedge clk) disable iff (!rst_n) !$isunknown(en)
);

Use four-state types such as logic to retain X/Z values. A two-state bit cannot represent them.

Value	`$onehot`	`$onehot0`	`$isunknown`
`4'b0000`	0	1	0
`4'b0100`	1	1	0
`4'b0101`	0	0	0
`4'b0x01`	1	1	1
`4'b0x00`	0	1	1

$countones

The $countones returns the count of ones in an expression.

Syntax:

$countones(<expression>)

Example 1

$countones(8'b1010_1100) // Returns 4
$countones(4'b1x0z)     // Returns 1

Example 2: For an error in the transaction, the data[3:0] signal value is expected to be 4‘hF. Below assertion checks all bit sets in case, an error is detected.

property prop;
  @(posedge clk) disable iff (!rst_n)
    (valid && error) |-> ($countones(data[3:0]) == 4);
endproperty

ap_error_data: assert property (prop);

The width matters: counting four 1 bits in exactly four positions requires every position to be 1, so this particular check also excludes X/Z from data[3:0]. For this requirement, the direct expression data[3:0] == 4'hF is an equally clear alternative.

Note: countones do not count x or z values in an expression.

$assertoff(), $asserton(), $assertkill()

To have global control over assertions at instance or module level, $assertoff(), $asserton() and $assertkill() is used.

$assertoff() – It is used to turn off assertions temporarily at the module or instance level.

$assertkill() – It is used to kill currently executing assertions.

$asserton() is by default set that keeps assertion enabled by default. The $asserton can also be called after assertoff() or $assertkill() to enable assertion once again.

Syntax:

$assertoff(level, <list of modules/ instance/ assertion_identifier>);
$assertkill(level, <list of modules/ instance/ assertion_identifier>);
$asserton(level, <list of modules/ instance/ assertion_identifier>);

where, The level represents up to what level of hierarchy from module or instance assertion can be turned on/ off.

assertion _identifier represents a label used with assert or property.

level = 0: This turns on/off assertions at all levels below the current instance or module.

….

level = n: This turn on/off assertions at ‘n’ hierarchical levels below the current instance or module.

Example: Generally assertions are turned off when reset is asserted as shown below.

module control_assertion();
  Initial begin
    @(posedge rst) $assertoff(0, tb_top.DUT); // To disable assertion for all levels on active high reset
    @(negedge rst) $asserton(0, tb_top.DUT);  // To enable assertion for all levels on active high reset
  end
endmodule