Sampled Functions with Clock & Gating Arguments

Overriding the inferred clock

Inside a property, every sampled value function inherits the property's clocking event. All of them also accept an explicit clocking event argument that overrides the inherited one: $rose(sig, @(posedge clk2)) asks whether sig rose between the two most recent clk2 ticks — even if the surrounding property is clocked on clk1. This is occasionally necessary in multi-clock checkers, but treat it as a sharp tool: the function's answer is now aligned to a different time base than the rest of the property, and the combined expression only means something if you can state precisely which tick of which clock each term refers to.

// Property clocked on clk_a, but one term sampled against clk_b
property p_cfg_frozen_during_fast_burst;
  @(posedge clk_a) disable iff (!rst_n)
    burst_active |-> $stable(cfg_reg, @(posedge clk_b));
endproperty
assert property (p_cfg_frozen_during_fast_burst);

// Cleaner alternative when the whole rule lives in one domain:
// move the entire property onto that domain's clock instead.
assert property (@(posedge clk_b) disable iff (!rst_n)
  burst_active_sync_b |-> $stable(cfg_reg));

The second form is almost always preferable: synchronize the qualifier into the target domain and keep one time base per property. Reserve explicit per-function clocks for checkers that genuinely must correlate two domains in one expression.

The valid-qualified pipeline — full worked example

The single most useful gated-$past pattern: a pipeline where data advances only on valid cycles (bubbles are legal), and the check is “when a result emerges, it equals the input from N valid beats ago — not N clock ticks ago.” Plain $past(in, N) breaks the moment a bubble enters; $past(in, N, in_vld) advances its history only on qualifying beats and stays aligned through any stall pattern.

// 3-deep valid-qualified pipeline (bubbles allowed, no backpressure)
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
);
  // count valid beats so the first DEPTH outputs are not checked
  // against unfilled $past history
  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) |->
      (out_data == $past(in_data, DEPTH, in_vld)));

  // valid conservation: every input beat eventually emerges in order
  // (bounded form — see liveness discussion in protocol lessons)
  assert property (@(posedge clk) disable iff (!rst_n)
    in_vld |-> ##[1:32] out_vld);
endmodule

DEPTH=3, bubbles at ticks 3 and 5 — gated history stays aligned

  tick                    :  1   2   3   4   5   6   7   8
  in_vld   (sampled)      :  1   1   0   1   0   1   1   1
  in_data  (sampled)      :  A   B   -   C   -   D   E   F
  gated history (newest→) : [A] [BA] [BA][CBA][CBA][DCB][EDC][FED]
  out_vld  (sampled)      :  0   0   0   1   0   1   1   1
  out_data (sampled)      :  -   -   -   A   -   B   C   D
  $past(in,3,in_vld)      :  x   x   x   A   A   B   C   D
  check at out_vld ticks  :          → A==A    B==B C==C D==D  all PASS

  With UNGATED $past(in_data,3):
  tick 6 returns in_data from tick 3 — a bubble ('-') → spurious FAIL.

Gated $past in multi-rate designs

A related pattern appears when a block runs at a decimated rate: an enable strobe tick_en fires every K cycles of the fast clock, and registers update only on strobed cycles. Rules about “the previous value” mean “the previous strobed value” — exactly the gating argument again. The same idea checks accumulators, decimation filters, and slow control registers living in a fast domain.

// Accumulator updates only on tick_en (every K fast-clock cycles)
// Rule: on each strobed cycle, acc grew by exactly sample_in
assert property (@(posedge clk_fast) disable iff (!rst_n)
  tick_en && !first_tick |->
    (acc == $past(acc, 1, tick_en) + $past(sample_in, 1, tick_en)));

// Between strobes the accumulator must hold
assert property (@(posedge clk_fast) disable iff (!rst_n)
  !tick_en |-> $stable(acc));

K=3 decimation: acc updates only where tick_en=1

  fast tick      :  1   2   3   4   5   6   7   8   9
  tick_en        :  1   0   0   1   0   0   1   0   0
  sample_in      :  5   .   .   7   .   .   2   .   .
  acc (sampled)  :  0   5   5   5  12  12  12  14  14
                        └────┘       └────┘
                       $stable(acc) holds on every !tick_en tick
  at tick 4: $past(acc,1,tick_en)=0? No — careful: at tick 4 the
  previous GATED tick is 1, where acc sampled 0 and sample_in 5...
  but acc visible AT tick 4 is still 5 (update lands after the edge).
  This is why the check fires at the strobe AFTER the update is
  visible — align your check to when the effect is sampled.

That last waveform note is deliberate: multi-rate $past checks have two off-by-one hazards stacked (flop visibility delay plus gated-history advance). Always draw the tick table before trusting the assertion — and expect an interviewer to make you do exactly that.

CDC-flavored caution

Explicit clock arguments make it syntactically easy to mix domains in one expression — and semantically treacherous. $past(sig_from_domA, 1, , @(posedge clk_b)) samples an asynchronous signal on clk_b: in real hardware that crossing can metastabilize, and in simulation the race resolves arbitrarily, so the assertion may pass in RTL sim and have no silicon meaning. Assertions do not synchronize signals; they sample them. For CDC rules, assert within each domain (e.g. “req toggles only when ack quiet” on the source side; “synchronized req is stable for one destination cycle” on the destination side) and leave crossing-correctness proofs to CDC tools.

Interview angle

Expect: “a pipeline only moves on valid — how do you check N-cycle latency?” The expected answer is the gated form $past(in, N, in_vld) plus the guard for the first N valid beats; bonus points for the tick-table off-by-one (gated history advances after the gated tick). “Can you sample a signal from another clock domain in an assertion?” — syntactically yes via the clocking argument, but say why you would not: no synchronization, sim-only determinism, assert per-domain instead. Drawing the bubble waveform from this lesson on a whiteboard is the strongest possible answer format.

Key takeaways

• Every sampled value function accepts an explicit clocking event that overrides the property clock.

• $past(in, N, valid) measures N qualifying beats, not N ticks — the elastic-pipeline workhorse.

• Guard the first N gated beats: the gated history needs N qualifying samples before it is meaningful.

• In multi-rate checks, stack the flop-visibility delay on top of the gated-history advance — draw the ticks.

• Mixing clock domains in one expression is legal syntax and unreliable semantics — assert per domain.

Common pitfalls

• Ungated $past on an elastic pipeline — first bubble misaligns the comparison forever after.

• Checking out_data on the first DEPTH valid beats — gated history unfilled, X or default compares.

• Assuming $past(e,1,gate) on a gated tick returns the current value — it returns the previous gated one.

• Cross-domain sampling via @(posedge other_clk) arguments — race-dependent, meaningless for silicon.

• Forgetting the empty-argument comma when passing a clock with no gate: $past(e, 1, , @(posedge clk)).