Reaching back N samples

$past(expr) returns the value expr had at the previous tick of the property's clock; $past(expr, N) reaches N ticks back. Conceptually the simulator keeps a shift register of snapshots per $past call, advanced once per clocking event. This is the natural tool for backward-looking checks: instead of “when input arrives, output must appear later” (forward, needs a thread waiting N cycles), you write “when output appears, it must equal what the input was N cycles ago” — a single-cycle check with no open threads.

The full signature is $past(expr, N, gating_expr, @(posedge clk)). The third argument is the most under-taught feature in SVA: when gating_expr is supplied, the internal shift register only advances on ticks where the gate is true. $past(din, 2, vld) therefore means “the value of din at the second-most-recent tick where vld was high” — exactly what an elastic, valid-qualified pipeline needs.

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

// Registered output: classic one-liner
assert property (@(posedge clk) disable iff (!rst_n)
  dout == $past(din));

// Fixed-latency pipeline, latency parameterized
localparam int LAT = 4;
assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (out_data == $past(in_data, LAT)));

// Gated $past: compare against the last GATED sample, not the last tick
assert property (@(posedge clk) disable iff (!rst_n)
  pop |-> (rd_data == $past(wr_data, 1, push)));

Cycle-by-cycle: plain and gated $past

Plain $past(din) vs $past(din, 2)

  tick            :   1    2    3    4    5    6
  din  (sampled)  :   A    B    C    D    E    F
  $past(din)      :   x    A    B    C    D    E
  $past(din, 2)   :   x    x    A    B    C    D
                      ^    ^
                      └────┴── history not filled yet → default value

Gated $past: $past(din, 1, vld) advances only when vld=1

  tick            :   1    2    3    4    5    6    7
  vld  (sampled)  :   0    1    0    0    1    0    1
  din  (sampled)  :   ?    B    ?    ?    E    ?    G
  gated history   :   []   [B]  [B]  [B]  [E]  [E]  [G]
  $past(din,1,vld):   x    x    B    B    B    E    E

  tick 5: gate is high, so AFTER this tick the stored value becomes E,
          but the value RETURNED at tick 5 is still B (the previous
          gated sample). $past looks strictly backward.
  ticks 3,4: gate low → history frozen → still returns B.

Note the subtlety at tick 5 above: on a tick where the gate is high, $past(expr, 1, gate) still returns the previous gated sample — the current tick's value enters the history only for future ticks. Getting this off-by-one right is the difference between a FIFO check that works and one that compares an element with itself.

The first N cycles: default values and guards

Before the history fills — the first N ticks after simulation start (and after any disable iff reset, depending on tool) — $past returns the default value of the expression's type: X for 4-state logic, 0 for 2-state types like int or bit. The 4-state case is survivable because a comparison with X is false and the assertion simply fails visibly (or is reset-gated). The 2-state case is the silent killer: $past(count) of an int returns a perfectly legal-looking 0, and a check like count == $past(count) + 1 can pass or fail for the wrong reason on cycle 1.

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

// Guard the start-up window explicitly with a cycle counter ...
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 == $past(in, LAT)));

// ... or let the antecedent provide the guard naturally:
// out_valid cannot be high until LAT cycles after the first in_valid,
// so the $past history is always filled when the consequent runs.
assert property (@(posedge clk) disable iff (!rst_n)
  out_valid |-> (out_data == $past(in_data, LAT)));

Where $past may appear

$past is legal in both the antecedent and the consequent, but the idiomatic placement is the consequent: trigger on the effect and reach back to the cause. Antecedent $past is occasionally useful — e.g. ($past(state) == IDLE && state == BUSY) |-> ... to key off a specific transition — but a backward-looking antecedent is usually expressible more clearly with $rose/$fell or a sequence. Remember the value $past returns is always relative to the tick at which that particular expression is evaluated — in a |-> ##2 (b == $past(c)), the $past(c) is c's value one tick before the consequent tick, i.e. one tick after the antecedent matched.

Worked example: registered output with enable

1
2
3
4
5
6
7
8
9
10

// DUT behavior: q <= (en) ? d : q;  on posedge clk
// Two assertions cover both branches completely.

// 1. When enabled last cycle, q took d's old value
assert property (@(posedge clk) disable iff (!rst_n)
  $past(en) |-> (q == $past(d)));

// 2. When not enabled last cycle, q held
assert property (@(posedge clk) disable iff (!rst_n)
  !$past(en) |-> $stable(q));

tick           :   1    2    3    4    5
  en  (sampled)  :   1    0    1    1    0
  d   (sampled)  :   A    B    C    D    E
  q   (sampled)  :   ?    A    A    C    D

  tick 2: $past(en)=1 → check q==$past(d) → A==A  PASS
  tick 3: $past(en)=0 → check $stable(q)  → A==A  PASS
  tick 4: $past(en)=1 → check q==$past(d) → C==C  PASS
  tick 5: $past(en)=1 → check q==$past(d) → D==D  PASS

  Why $past(en) and not en: q visible at tick N was decided by
  en and d at tick N-1. The assertion must reach back to the
  cause, not test the current-cycle enable.

Interview angle

Three reliable questions. “What does $past return on the first cycle?” — type default: X for logic, 0 for 2-state, and explain why the 2-state case is dangerous. “Check that a pipeline output equals its input N cycles earlier when only some cycles carry data” — that is the gated form, $past(in_data, N, in_valid), and you should mention the off-by-one (current gated tick is not yet in the history). “Forward or backward style for a latency check?” — backward (out_valid |-> out == $past(in, LAT)) is cheaper: no multi-cycle threads, failure reported at the cycle of the bad output.

Key takeaways

• $past(expr, N) returns the sampled value N clock ticks back — a per-call snapshot shift register.

• The gating argument makes the history advance only on qualifying ticks — the key to valid-qualified pipelines.

• Before the history fills, $past returns the type default: X for 4-state, 0 for 2-state — guard cycle 1..N.

• Backward-looking checks (effect |-> equals $past(cause)) beat forward threads for fixed-latency rules.

• On a gated tick, $past(e,1,gate) still returns the previous gated sample, not the current one.

Common pitfalls

• $past of a 2-state expression on early cycles returns 0 silently — checks pass or fail for the wrong reason.

• Forgetting that $past inside ##N consequents is relative to the consequent's tick, not the antecedent's.

• Using $past(in, N) on an elastic pipeline — bubbles shift the alignment; you needed the gated form.

• Assuming $past history survives a disable iff reset identically on all tools — re-guard after reset.

• Comparing q to $past(d) gated on en instead of $past(en) — off-by-one against the flop's actual cause.