Procedural code detects an edge as an event. @(posedge req) fires the instant req transitions, at any point in time.
$rose(req) is a comparison of two snapshots. It is true when the current sample of bit 0 is 1 and the previous sample was not 1.
$fell is the mirror image on falling values. $stable(v) compares the whole vector against its previous sample, and $changed(v) is its exact negation.
// snippet
assert property (@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] $rose(gnt));
assert property (@(posedge clk) disable iff (!rst_n)
busy |-> $stable(cfg_reg));
assert property (@(posedge clk) disable iff (!rst_n)
$changed(data_bus) |-> valid);The rose lane pulses only on the slot where req newly reads 1. The fell lane pulses only where it newly reads 0.
Slot 0: req 0 with no earlier sample, so rose 0 and fell 0.
Slot 1: req still 0, so both lanes stay 0.
Slot 2: req 1 after 0, so rose 1.
Slot 3: req still 1, so rose 0: high is not rising.
Slot 4: req still 1, so rose 0.
Slot 5: req 0 after 1, so fell 1.
Slot 6: req still 0, so fell 0.
Slot 7: req 1 after 0, so rose 1.
A multi-bit argument to $rose silently watches only bit 0. $rose(data_bus) is true when data_bus[0] went to 1, which is almost never the intent.
For vectors, say what is meant. $changed(data_bus) catches any movement, and $rose(|data_bus) means the bus became non-zero.
Previous to current | $rose | $fell | $stable | $changed |
|---|---|---|---|---|
0 to 1 | 1 | 0 | 0 | 1 |
1 to 0 | 0 | 1 | 0 | 1 |
X to 1 | 1 | 0 | 0 | 1 |
X to 0 | 0 | 1 | 0 | 1 |
Z to 1 | 1 | 0 | 0 | 1 |
0 to X | 0 | 0 | 0 | 1 |
1 to X | 0 | 0 | 0 | 1 |
X to X | 0 | 0 | 1 | 0 |
1 to 1 | 0 | 0 | 1 | 0 |
0 to 0 | 0 | 0 | 1 | 0 |
Four-state values follow the same rule. A snapshot pair ending in 1 with a non-1 predecessor counts as a rise, including X to 1.
At the first tick, the previous value is the default sampled value: the declaration initializer, or the type default when there is none (X for uninitialized logic, 0 for bit). $stable and $rose there compare against that default, so gate start-up with disable iff or a warm-up qualifier.
// bad-example
assert property (@(posedge clk) $rose(data_bus) |-> valid);// snippet
assert property (@(posedge clk) $changed(data_bus) |-> valid);
assert property (@(posedge clk) $rose(|data_bus) |-> valid);data_bus goes from 0x04 to 0x00. Does $rose(data_bus) fire?No. Bit 0 was 0 in both samples. $changed(data_bus) fires, and $fell(|data_bus) reports the bus returning to zero.
A level antecedent matches every cycle the level holds. If req stays high for 5 cycles, req |-> ... spawns 5 overlapping attempts.
An edge antecedent matches once per event. $rose(req) |-> ... spawns one attempt, which is the intent for most request rules.
Stimulus | Level antecedent | Edge antecedent |
|---|---|---|
| Attempts at 2, 3, 4; two of them fail | One attempt at tick 2; it passes |
Rule holds while | Correct: the obligation renews each cycle | Wrong: only the rising cycle is checked |
Pulses that live entirely between clock ticks are invisible to every sampled value function. Neither snapshot captures them, so no edge is reported.
That blindness is correct for synchronous rules: a glitch no flop captures is harmless. Asynchronous needs, such as glitch detection, need event-based checks instead.
The edge form $rose(req) |-> ... with one attempt. The level form opens two extra attempts that expire without their own grant.
The bench counts real $rose, $fell and $changed covers over the 8-beat trace from the diagram, then moves a bus one bit at a time, then holds a request for three ticks under a level and an edge antecedent.
$rose(bus) fire? And $changed(bus)?$rose once: it looks at bit 0 only, which rises on 02 to 03. $changed three times: every step changed some bit.
module tb_edge_funcs;
logic clk = 0;
always #5 clk = ~clk;
logic sig = 0, req = 0, gnt = 0;
logic [7:0] bus = 8'h00;
int rises = 0, falls = 0, changes = 0, bus_rises = 0, bus_changes = 0, level_fails = 0, edge_fails = 0;
cp_rose: cover property (@(posedge clk) $rose(sig)) rises++;
cp_fell: cover property (@(posedge clk) $fell(sig)) falls++;
cp_changed: cover property (@(posedge clk) $changed(sig)) changes++;
// On a vector, $rose looks at bit 0 only; $changed looks at every bit.
cp_bus_rose: cover property (@(posedge clk) $rose(bus)) bus_rises++;
cp_bus_changed: cover property (@(posedge clk) $changed(bus)) bus_changes++;
// One request held for 3 ticks, one grant: level versus edge antecedent.
ap_level: assert property (@(posedge clk) req |-> ##2 gnt) else level_fails++;
ap_edge: assert property (@(posedge clk) $rose(req) |-> ##2 gnt) else edge_fails++;
initial begin
// sig over 8 beats: high on beats 2, 3, 4 and 7, as in the diagram.
for (int t = 0; t < 8; t++) begin
sig = (t == 2 || t == 3 || t == 4 || t == 7);
@(negedge clk);
end
sig = 0;
repeat (2) @(negedge clk);
$display("sig: %0d rises, %0d falls, %0d changes", rises, falls, changes);
bus = 8'h02; @(negedge clk); // only bit 1 moves
bus = 8'h03; @(negedge clk); // bit 0 rises
bus = 8'h00; @(negedge clk);
repeat (2) @(negedge clk);
$display("bus 00 -> 02 -> 03 -> 00: $rose(bus) %0d, $changed(bus) %0d", bus_rises, bus_changes);
req = 1; repeat (2) @(negedge clk); // req held for 3 ticks ...
gnt = 1; @(negedge clk); // ... with the grant on the third
req = 0; gnt = 0;
repeat (4) @(negedge clk);
$display("req held 3 ticks, gnt on the 3rd: level antecedent %0d failures, edge antecedent %0d", level_fails, edge_fails);
if (rises != 2 || falls != 2 || changes != 4 || bus_rises != 1 || bus_changes != 3 || level_fails != 2 || edge_fails != 0)
$fatal(1, "FAIL: %0d %0d %0d %0d %0d %0d %0d", rises, falls, changes, bus_rises, bus_changes, level_fails, edge_fails);
$display("PASS: edges counted between snapshots, $rose(bus) saw bit 0 only, and the level antecedent failed twice where the edge passed");
$finish;
end
endmodulesig: 2 rises, 2 falls, 4 changes
bus 00 -> 02 -> 03 -> 00: $rose(bus) 1, $changed(bus) 3
req held 3 ticks, gnt on the 3rd: level antecedent 2 failures, edge antecedent 0
PASS: edges counted between snapshots, $rose(bus) saw bit 0 only, and the level antecedent failed twice where the edge passedRun with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.