Sampled-Value Edge Cases

The mismatch every engineer hits once

Sooner or later you will stare at a waveform where req and gnt are clearly both high at a clock edge — and the assertion req |-> gnt failed on that very edge. The waveform is not lying and neither is the assertion: the waveform viewer shows values after the NBA updates of that timestep, while the assertion sampled both signals in the Preponed region — the values from just before the edge. If gnt was set by a flop on this same edge, the assertion saw the old gnt = 0.

Why the waveform and the assertion disagree

  tick            :    1         2         3
  clk             :  __┌──┐______┌──┐______┌──┐__
  req (actual)    :  ____┌─────────────┐__________   set by flop AT tick 1
  gnt (actual)    :  ______________┌────────┐______  set by flop AT tick 2

  what the viewer shows at tick 2:  req=1, gnt=1   (post-NBA values)
  what the assertion samples at 2:  req=1, gnt=0   (Preponed: pre-edge)

  assert property (@(posedge clk) req |-> gnt);
  tick 2 attempt: antecedent req=1, consequent gnt=0 → FAIL
  tick 3 attempt: req=1, gnt=1 → PASS

  Rule of thumb: an assertion at tick N sees the world as it was
  at the END of tick N-1. Add ##1 or use $past-style thinking when
  the response is produced by a flop on the same edge.

The practical fixes: write the property to match flop timing (req |-> ##1 gnt when gnt is registered), or debug with the simulator's assertion-debug view which displays sampled values rather than post-update values. Never “fix” it by moving the assertion to negedge without understanding what you changed — you just created a half-cycle timing assumption.

Sampled functions in procedural code

The sampled value functions are not restricted to properties. You can call them inside always blocks, tasks, and checkers — but outside an assertion there is no inferred clock, so you must pass the clocking event explicitly . A common use is debug instrumentation: print a message on the sampled rise of a signal so the printout aligns exactly with what concurrent assertions see, instead of with delta-cycle-sensitive procedural timing.

// Procedural use: explicit clocking argument is REQUIRED
always @(posedge clk) begin
  if ($rose(err_irq, @(posedge clk)))
    $display("[%0t] err_irq rose (sampled view)", $time);

  if (!$stable(cfg_reg, @(posedge clk)) && busy)
    $error("cfg moved while busy: %h -> %h",
           $past(cfg_reg, 1, , @(posedge clk)), cfg_reg);
end

// In a property, the clock is inferred from the property clock:
assert property (@(posedge clk) busy |-> $stable(cfg_reg));

Note the empty argument slot in $past(cfg_reg, 1, , @(posedge clk)) — the gating expression position is skipped to supply the clocking event as the fourth argument. Tools accept the event in properties too, which becomes essential in multi-clock checkers (covered in the clock-and-gating lesson).

$sampled: pinning a value inside action blocks

$sampled(expr) returns the Preponed-region value of expr at the current tick. Inside a property it is redundant — every expression is already evaluated on sampled values. Its real job is in action blocks : the pass/fail statements of an assertion execute in the Reactive region, after NBA updates, so naively printing a signal there shows the post-edge value — not the value the assertion actually tested. Wrapping the signal in $sampled in the action block reports the value that participated in the check.

assert property (@(posedge clk) disable iff (!rst_n)
  req |-> gnt)
else begin
  // WRONG: gnt here is the Reactive-region (post-update) value —
  // it may read 1 even though the assertion failed on gnt==0.
  $error("req without gnt: gnt=%b (post-edge, misleading)", gnt);

  // RIGHT: report the value the assertion actually evaluated
  $error("req without gnt: sampled gnt=%b", $sampled(gnt));
end

Region timeline within one clock tick (simplified)

  Preponed ──► Active(blocking) ──► NBA ──► Observed ──► Reactive
     │                                          │            │
     │ assertion INPUTS sampled here            │            │
     │                                assertions EVALUATE    │
     │                                                action blocks RUN
     │                                                       │
     └── $sampled(sig) in an action block retrieves ─────────┘
         this Preponed value, not the current one

Glitch invisibility — feature, not bug

Because assertions consume only one snapshot per clocking event, anything that happens strictly between ticks — combinational glitches, hazard pulses, zero-width spikes — is invisible. For synchronous protocol rules this is exactly right: a glitch that no flop captures is functionally harmless, and assertions firing on it would be noise. But it means SVA on a clocked property is the wrong tool for genuinely asynchronous requirements: detecting glitches on a clock mux, verifying combinational pulse widths, or CDC pulse-synchronizer correctness. Those need different machinery — @(edge) event-based procedural checks, dedicated CDC tools, or assertions clocked on a faster sampling clock.

// This will NEVER fire for a glitch between posedges, by design:
assert property (@(posedge clk) !glitchy_enable_conflict);

// Procedural watchdog for an async requirement (use sparingly):
always @(set_a or set_b)
  if (set_a && set_b)
    $error("async conflict: set_a and set_b overlapped at %0t", $time);

Interview angle

The flagship question: “the waveform shows the signal high at the edge but the assertion failed — why?” Answer with regions: inputs sampled in Preponed (pre-edge), viewer shows post-NBA values; if the consequent is produced by a flop on the same edge, the assertion is one cycle ahead of the waveform. Follow-ups to be ready for: what $sampled is for (truthful action-block messages), whether sampled functions work in procedural code (yes, with an explicit clocking event), and “can SVA catch a glitch?” — no, on a clocked property, and you should explain why that is usually correct and what to use instead when it is not.

Key takeaways

• Assertion inputs are sampled in the Preponed region — the value just BEFORE the clock edge.

• Waveform viewers show post-NBA values; expect a one-cycle apparent skew on flop-driven consequents.

• Sampled functions work procedurally if you pass the clocking event explicitly.

• $sampled in action blocks reports the value the assertion actually tested, not the post-edge value.

• Clocked assertions cannot see inter-tick glitches — use other techniques for async requirements.

Common pitfalls

• Debugging an assertion against the waveform's post-edge values — chasing a failure that is correct.

• Printing raw signals in action blocks — Reactive-region values mislead; wrap them in $sampled.

• Calling $rose in an always block without the clocking argument — compile error or wrong inferred clock.

• Moving an assertion to negedge to make a mismatch 'go away' — hides a real timing relationship.

• Relying on a clocked assertion to catch combinational glitches or async pulse overlaps — it cannot.