Q&A: Sampled Values & $past

Q: The waveform shows the signal high at the failure time, but the assertion says it was low. Who is right?

Direct answer: both — they are reporting different samples . The assertion evaluated preponed values: the signal as it was immediately before the clock edge. The waveform cursor parked on the edge shows the value after the same-edge NBA update. If the signal rose at that very edge, the viewer shows 1 while the assertion correctly used 0. The debugging rule: for any signal that transitions on the failing edge, the assertion saw the pre-transition value — read the waveform one sample to the left.

ack rises exactly at edge N; property: $rose(req) |-> ##2 ack

  viewer at edge N      : ack = 1   "why did it fail?!"
  assertion at edge N   : ack = 0   (preponed, pre-edge value)

      N-1        N
  ____________/■■■■■■■   ← ack
              ↑edge
  assertion samples HERE (just left of the edge)

  The DUT was one cycle late; the viewer's post-edge rendering
  disguised it. Many tools draw a separate 'sampled' row or
  assertion-debug track — use it instead of eyeballing edges.

Follow-up: 'How do you make this class of confusion go away for the team?'

• Turn on the simulator's assertion-debug view, which displays the sampled values per attempt — argue from those, never from raw cursor reads.

• In logs, print $sampled(sig) in action blocks so the message itself shows what the assertion saw.

• Train the one-sample-left rule explicitly during failure triage reviews.

Junior vs senior answer

• Junior: 'the waveform must be wrong' or 'add ##1 until it passes' — patching symptoms.

• Senior: names preponed sampling as the mechanism, gives the one-sample-left rule, and points at sampled-value debug tracks and $sampled in messages as the workflow fix.

Q: What does $rose do on a multi-bit signal?

Direct answer: $rose(expr) looks only at the LSB of the expression: true when the LSB changed to 1 from 0 (or from X/Z). For a vector, every bit except bit 0 is ignored — $rose(data_bus) answers 'did data_bus[0] rise', which is almost never the intended question. Intended-meaning replacements: bus became nonzero — (data_bus != 0) && ($past(data_bus) == 0); bus changed at all — $changed(data_bus); a specific flag rose — $rose(data_bus[7]).

cycle      :   0       1
counter    :   8'h00   8'h02      ← clearly "rose" informally

$rose(counter): LSB 0→0  → FALSE.  Assertion using it never fires.
(counter != 0) && ($past(counter)==0) → TRUE — what was meant.

Worse trap: counter 8'h01 → 8'h03: LSB 1→1, $rose false again;
but 8'h02 → 8'h01 makes $rose TRUE while the value DECREASED.

Follow-up: 'And $fell / $stable / $changed on vectors?'

$fell mirrors $rose (LSB to 0). $stable and $changed compare the whole vector — they are the vector-safe pair. The asymmetry (edge functions LSB-only, stability functions whole-vector) is the exact trivia being probed; volunteering it ends the question.

Junior vs senior answer

• Junior: assumes $rose means 'the value increased' or 'became nonzero'.

• Senior: LSB rule, the three intended-meaning rewrites, and the whole-vector contrast with $stable/$changed.

Q: What does $past return in the first cycles of simulation?

Direct answer: before $past(sig, N) has N sampling events of history, it returns the default initial value of the signal's type — X for 4-state logic, 0 for 2-state. Consequences: comparisons against early $past are comparisons against X; X == anything evaluates to X, an X antecedent does not match (vacuous), and an X consequent is typically reported as undetermined/failing depending on tool settings. Net effect: early-cycle attempts behave erratically and non-portably unless you gate the property until history exists .

// warm-up gate: counter suppresses attempts until $past is valid
logic [1:0] hist;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) hist <= '0;
  else if (hist != 2) hist <= hist + 1;

a_delayed_eq: assert property (
  @(posedge clk) disable iff (!rst_n)
  (hist == 2) |-> (dout == $past(din, 2)));

// long reset? disable iff often covers the warm-up implicitly —
// but say you are RELYING on that, or the review will ask.

Follow-up: 'Does disable iff fix the startup problem on its own?'

Only if reset is asserted for at least N sampled cycles at time zero AND $past's history window lies entirely inside reset — common, but an assumption. Mid-sim X injection, gated clocks, or short resets break it. The explicit warm-up term documents the requirement instead of inheriting it silently.

Junior vs senior answer

• Junior: 'it returns X at the start' — true, stops before consequences.

• Senior: default-initial-value rule, the X-comparison vacuity cascade, the explicit warm-up gate, and the limits of leaning on disable iff.

Q: What is the 4th argument of $past — the gating expression?

Direct answer: $past(expr, N, , gate) returns expr from the Nth-most-recent sampling event where gate was true — it rewinds through qualifying cycles only, skipping cycles where gate was false. This is the native tool for valid-gated pipelines and enabled datapaths: 'the input from three valid beats ago' is $past(din, 3, , vld), with no hand-built shift register. (The third argument slot is an expression-clocking field, normally left empty — hence the double comma.)

cycle :  0   1   2   3   4   5   6
vld   :  0   1   0   1   1   0   1
din   :  -   A   -   B   C   -   D

standing at cycle 6:
  $past(din, 1)          = din@5 = garbage  (ungated: raw cycle)
  $past(din, 1, , vld)   = C   (last vld beat before 6: cycle 4)
  $past(din, 3, , vld)   = A   (3rd-last vld beat: cycle 1)

One argument replaces a queue, a write pointer, and three
off-by-one bugs.

Follow-up: 'Pitfalls of the gated form?'

• Fewer than N gated events so far → same default-initial-value problem; warm up on a count of gate events, not raw cycles.

• The gate is sampled like everything else — preponed; a same-edge gate transition uses the pre-edge gate value.

• Empty third argument is required syntax for the common case — the double comma trips people at the whiteboard; write it deliberately.

Junior vs senior answer

• Junior: hand-builds a shift register with valid enables in aux code.

• Senior: $past gating argument, the gated warm-up subtlety, and when aux modeling is still better (complex flow control, multi-clock).

Q: How do $rose, $stable, and $onehot behave around X?

Direct answer: three different contracts. $rose — true on a transition to 1 from 0, X, or Z; so an X-to-1 wake-up after reset reads as a rise — an edge you may not consider real. $stable — sampled-value equality using 4-state comparison; X-to-X counts as stable , so a bus stuck at X sails through stability checks. $onehot — with X/Z bits present the result is not a clean true; the check is effectively undetermined and, in an assertion context, will not give you the crisp failure you expect. The umbrella rule: none of these functions raise an alarm about X itself — X-detection must be explicit, via $isunknown.

cycle :  0   1   2
sig   :  X   1   1      $rose @1 : TRUE  (X→1 counts as a rise!)
bus   :  XX  XX  XX     $stable @1, @2 : TRUE (X==X — "stable" garbage)
state :  0X10 ...       $onehot @0 : not a clean TRUE/FALSE

A dead, all-X design can pass rise-checks at wake-up and
stability checks forever. Only $isunknown makes X loud.

Follow-up: 'So what is the standing X-strategy in an assertion bind file?'

• Dedicated X-assertions on every control signal and qualified datapath: valid |-> !$isunknown(data), continuous !$isunknown on controls out of reset.

• Treat the sampled-value functions as value-logic only; never rely on them to flag unknowns.

• In formal, start from X-free initial states or add X-checks as proof obligations — X-optimism in the model can hide the same class of bugs.

Junior vs senior answer

• Junior: 'X makes assertions fail' — backwards in the dangerous cases: X makes them vacuous or falsely stable.

• Senior: per-function contracts (X→1 rise, X==X stable, undetermined onehot) and the explicit-$isunknown strategy that follows.

Key takeaways

• Assertions argue from preponed samples — one sample left of the waveform cursor on transitioning signals.

• $rose/$fell are LSB-only; $stable/$changed are whole-vector — the asymmetry is the interview question.

• $past needs history: gate with a warm-up count, and use its gating argument instead of hand-built shift registers.

Common pitfalls

• Debugging from the waveform cursor instead of the sampled-value track — chasing a one-cycle ghost.

• $rose on a counter or bus — silently checks bit 0 only.

• Trusting $stable through X — a stuck-at-X bus is 'stable'; only $isunknown reports it.