$past, $rose, $fell and $stable

Many rules compare now with before: a flag that was set must still be set, a value may only change after a write, an output rises only after a request. SVA has a small family of functions for this, the sampled value functions $past, $rose, $fell, $stable and $changed. This article explains each one, uses them on a sticky error flag with a real bug, and shows the first-cycle trap that catches almost every beginner.

9 min read | Beginner to Intermediate

What You'll Learn

• Use $past, $rose, $fell, $stable and $changed in properties
• Look several cycles back with $past(x, n)
• Write "stays until" and "changes only after" rules for a register
• Avoid the first-cycle trap, where a check compares with a cycle that never existed

The Sampled Value Functions

Each function compares the value of an expression at the current clock edge with its value at an earlier edge. "Value" here means the sampled value, the one just before the edge, as for every concurrent assertion.

Two details are worth remembering. $rose and $fell look only at the lowest bit, so on a vector $rose(count) means "bit 0 of count went from 0 to 1", which is rarely what you want. Use $changed or compare with $past for vectors. And $past takes an optional third argument, a gating condition: $past(x, 1, en) is the value of x at the last clock edge where en was true.

The Design: a Sticky Error Flag

Many blocks report errors through a sticky flag: a single error pulse sets it, and it stays set until software clears it. That way an error is not lost when software reads the status late. Here is one with a bug:

module sticky (input clk, input rst, input err, input clr, output reg flag);
  always @(posedge clk)
    if (rst)      flag <= 1'b0;
    else if (clr) flag <= 1'b0;
    else          flag <= err;                    // bug: should be "else if (err) flag <= 1'b1;"
endmodule

The last line copies err into the flag instead of setting it. The flag follows the error pulse and forgets it one cycle later. In a simulation where err stays high for a while, or where software reads the flag at the right moment, this goes unnoticed.

Properties That Look Back

Three rules describe a sticky flag:

// once set, the flag stays set until a clear
a_hold: assert property (@(posedge clk) disable iff (rst) flag && !clr |=> flag);
// the flag only rises after an error
a_rise: assert property (@(posedge clk) disable iff (rst) $rose(flag) |-> $past(err));
// the flag only falls after a clear
a_fall: assert property (@(posedge clk) disable iff (rst) $fell(flag) |-> $past(clr));

Each rule says something different. a_hold is about keeping the value. a_rise and a_fall say what is allowed to cause a change. Together they pin down the behavior without restating the RTL. Notice that a_hold uses |=> to look forward one cycle, while a_rise uses $past to look back. Both forms describe a relation between two neighboring cycles. You pick whichever reads more naturally.

Running It in ChipVerify Lab

The lab engine reads $past, $rose, $fell and $stable inside clocked blocks. The forward-looking |=> becomes a backward look with $past: "if the flag was set and there was no clear in the previous cycle, the flag is set now".

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // once set, it stays set until clr or rst
  always @(posedge clk) if (!init && $past(flag) && !$past(clr) && !$past(rst)) assert (flag);
  // it only rises after an err
  always @(posedge clk) if (!init && $rose(flag)) assert ($past(err));
  // it only falls after clr or rst
  always @(posedge clk) if (!init && $fell(flag)) assert ($past(clr) || $past(rst));
`endif

The run fails at step 4:

An error pulse in step 1 sets the flag in step 2. In step 2 there is no error and no clear, so the flag should stay set, but in step 3 it is 0 again. Both a_hold and a_fall fail on this trace. With the fix, else if (err) flag <= 1'b1;, all three pass.

The First-Cycle Trap

Look again at the lab form of a_hold. It starts with !init. Remove it, so that the check also runs in the first cycle, and run the fixed design. It fails at step 1, and the waveform shows nothing wrong at all: reset in step 0, every signal 0, no error, no clear.

The reason is the cycle before step 0. A clocked assertion in the lab is evaluated at a clock edge and reported in the step after it, as the earlier chapters showed. The failure reported in step 1 comes from the very first clock edge, and at that edge $past refers to a cycle before step 0. That cycle never existed. The tool may choose any values for it, and it chooses ones that break the rule: a flag that "was" set with no clear and no reset. The waveform cannot show them, because they are not part of the trace.

The same problem exists in SVA. In the first clock tick, a sampled value function compares with the default value of the signal, which is X for a 4-state logic. The usual protection is disable iff (rst) together with a reset in the first cycle, so the check is off until there is a real history. In the lab form, the init register does the same job.

Whenever a counterexample fails in step 0 or 1 and the trace looks innocent, suspect a $past that reaches before the start.

Common Mistakes

always @(posedge clk) if (!init && !$past(rst) && $past(err) && !$past(clr)) assert (flag);