N samples back

$past(expr) returns the value sampled on the previous clocking event. $past(expr, N) reaches N events back, as if each call owned a shift register of snapshots.

That shape suits backward-looking checks. Instead of opening a thread that waits N cycles for an output, trigger on the output and reach back to the input.

The full signature is $past(expr, N, gate, clock). The gate is third and the clock is fourth: $past(din, 2, vld) advances only on ticks where vld holds.

Standardize on the three-argument gated form. The double-comma form $past(e, 1, , @(posedge clk)) exists only to pass an explicit clock with no gate.

On a gated tick, $past(e, 1, gate) still returns the previous gated sample. The current tick enters the history only for future ticks.

Read down any column: at edge 4, $past(data, 2) is d2, the sample from edge 2. The x slots at the start are why a $past check needs a guard for its first N cycles.

Guard the first N cycles

Before the history fills, $past returns the default sampled value: the declaration initializer if there is one, otherwise the type default (X for 4-state logic, 0 for 2-state types such as int or bit).

The 2-state case is the silent one. A legal-looking 0 can satisfy a check for the wrong reason on cycle 1, so guard the start-up window explicitly.

1
2
3
4
5
6
7

// snippet
bit [3:0] cycles_since_rst;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) cycles_since_rst <= '0;
  else if (!(&cycles_since_rst)) cycles_since_rst <= cycles_since_rst + 1;
assert property (@(posedge clk) disable iff (!rst_n)
  (cycles_since_rst >= LAT) |-> (out_data == $past(in_data, LAT)));

A cleaner guard comes free when the consequent cannot fire early. If out_valid cannot rise until LAT beats after the first input, the history is always filled when the check runs.

Place $past in the consequent and trigger on the effect. A $past inside a delayed consequent is relative to the consequent tick, not the antecedent tick.

Pipelines that move on valid

An elastic pipeline advances only on qualifying beats. The gated form keeps the comparison aligned through any stall pattern, where the ungated form fails on the first bubble.

The listing below is not run in this course's checks because Verilator 5.048 does not support $past with a gate argument. The bench at the end of this lesson keeps the same history with two flops that advance only on valid, which every simulator runs.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

// not-run: Verilator 5.048 does not support $past with a gate argument
module pipe_check #(int DEPTH = 3) (
  input logic clk, rst_n,
  input logic in_vld,  input logic [31:0] in_data,
  input logic out_vld, input logic [31:0] out_data
);
  int unsigned vld_beats;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) vld_beats <= 0;
    else if (in_vld) vld_beats <= vld_beats + 1;
  assert property (@(posedge clk) disable iff (!rst_n)
    (out_vld && vld_beats >= DEPTH - 1) |->
      (out_data == $past(in_data, DEPTH - 1, in_vld)));
endmodule

A three-stage pipe that moves on valid shows, on each valid beat, the input from two gated beats before the current one. That is $past(in_data, DEPTH - 1, in_vld), because the current gated tick is not yet in the history. Idle slots never enter it.

• Slot 0: valid beat with a; out_data still 0, history holds one beat.

• Slot 1: valid beat with b; out_data still 0, history holds two beats.

• Slot 2: bubble; out_data still 0, history frozen.

• Slot 3: valid beat with c; out_data a, two gated beats before c.

• Slot 4: bubble; out_data back to 0, output lane idle.

• Slot 5: valid beat with d; out_data b.

• Slot 6: valid beat with e; out_data c.

Testbench

The bench checks the elastic pipe from the diagram twice: against a valid-gated history kept by two flops, and against the ungated $past(in_data, 2). Then it plants a pipe that shifts on bubbles too.

1
2
3
4
5
6
7
8
9
10
11
12
13

// A three-stage pipe that moves only on valid: out_data is the input from
// two valid beats before the current one, as in the diagram.
module vpipe3 (
  input  logic clk, rst_n, in_vld, bug,
  input  logic [7:0] in_data,
  output logic [7:0] out_data
);
  logic [7:0] h0, h1;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin h0 <= 0; h1 <= 0; end
    else if (in_vld || bug) begin h0 <= in_data; h1 <= h0; end   // bug: shifts on a bubble too
  assign out_data = h1;
endmodule

correct pipe, 6 valid beats and 3 bubbles: gated check 0 failures, ungated $past 3
planted bug, the pipe shifts on bubbles: gated check 3 failures
PASS: the valid-gated history stayed aligned through bubbles and caught the pipe that shifted on them

Related topics

• Edges between snapshots

• Assembling real checks