Clocks and sampling

Properties are checked only at the clock

A concurrent assertion names a clocking event, usually @(posedge clk). The property is evaluated at each such event and nowhere else, so a pulse that rises and falls between two edges is invisible to it. In the example below, a 3 ns pulse on err between the edges at 35 and 45 never fails !err, while an always @(posedge err) block counts it.

Writing the clock in every assertion is repetitive. A default clocking cb @(posedge clk); endclocking declaration in the module lets later assertions leave it out.

Sampled values

An assertion does not read signals at the moment it is evaluated. It reads their sampled values: the values from the Preponed region, before anything has changed in the time step of the edge. That is the same view a #1step clocking block gives, as Module 6 showed.

Because the samples are taken before any process runs, the result never depends on process order. Even a testbench that writes a signal at the edge with a blocking assignment gives the same sampled value on every simulator.

One time step, region by region

Reading a waveform the way an assertion does

1. Find the edge

   Locate the rising edge of the assertion's clock that you are interested in.

2. Look just left of it

   Read each signal's value immediately before the edge. A value that changes exactly at the edge counts as its old value.

3. Compare with the previous edge

   For $rose, $fell, $stable and $past, repeat the same reading at the edge before, and compare the two samples.

Many waveform viewers draw a change at an edge on top of the edge, which invites reading the new value. Zoom in, or move the cursor slightly left of the edge, before deciding what an assertion saw.

Why assertions cannot race

Module 6 showed a monitor in an always block reading a signal at the same edge where another process writes it, with no defined order. A concurrent assertion has no such problem, because its samples are taken before any process of that time step runs.

That makes assertions a reliable second opinion when a monitor and a waveform disagree. If the assertion and the monitor report different values for the same edge, the monitor is reading at the wrong moment.

Comparing edges: $rose, $fell, $stable, $changed

Sampled value functions compare a signal's sample at this edge with its sample at the previous edge. $rose(x) is true when the sample went from 0 to 1, $fell(x) when it went from 1 to 0, $stable(x) when it did not change, and $changed(x) when it did.

They work on whole vectors too: $stable(rdata) is true when every bit matches the previous sample. For $rose and $fell, only the least significant bit counts.

These functions are how most rules about change are written. The rule "data does not move during a stall" becomes rvalid && !rready |=> $stable(rdata).

$past, and the first edges

$past(x) returns the sample of x at the previous edge, and $past(x, n) the sample n edges back. It lets a property compare with an older value directly, as in rdata == $past(rdata).

At the start of simulation there may not be n earlier edges. Then $past returns the value the variable was declared with, such as the 1 in logic rready = 1;, not a value later written by an initial block. $rose and $fell at the first edge compare with the same declared value. Simulators do not all agree on these early values, so start such checks only after reset.

Checks that use $past should therefore start only after reset, or after enough edges, so that they never compare with a value nobody intended.

Printing what the assertion saw

Action blocks run later in the time step than the sampling, so a signal printed there may already hold a newer value. At 15 in the example, the fail message shows rready as 1 while the rule used 0. Print $sampled(x) to show the value the assertion actually used.

Try it

rready was written right after the edge at 5, so the fall is seen at 15. By the time the fail action runs at 15, the testbench has already written 1, which is why now and sampled differ. rdata was written between edges, so its changes appear at the very next edges, 45 and 55.

At 45, two edges back is before the first change, so $past(rdata, 2) returns the declared value 10. The err pulse came and went between two edges: counted once, never seen by no_err. Change #3 to #6, so the pulse covers the edge at 45, and predict which rule reports.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic v = 0;
  r: assert property (@(posedge clk) !$rose(v))
    else $display("rose seen at %0t", $time);
  initial begin
    @(posedge clk); v = 1;               // written at the edge at t=5
    #30 $finish;
  end
endmodule

rvalid && !rready |=> rdata == $past(rdata)

rvalid && !rready |-> $stable(rdata)

rvalid && !rready |=> !$changed(rdata)

rvalid && !rready |=> $stable(rdata)