Stability, Pulse & Glitch Checks

Rules about shape, not sequence

This family checks the shape of signals over a window: values that must not move during an operation, pulses that must be exactly or at-least-or-at-most so wide, signal pairs that must never overlap, and levels that must persist until consumed. The star operator here is throughout: expr throughout seq requires the boolean expr to hold at every tick that seq spans — the natural phrasing for “X stays true for the whole duration of Y.”

// Config frozen across the whole transaction window.
// Window: from start pulse to the cycle done asserts.
property p_cfg_frozen;
  @(posedge clk) disable iff (!rst_n)
    $rose(start) |->
      $stable(cfg) throughout (##1 (!done) [*0:$] ##1 done);
endproperty
a_cfg_frozen: assert property (p_cfg_frozen);

// Equivalent cycle-local phrasing — often easier to debug, because
// it fails AT the offending cycle instead of at window end:
a_cfg_frozen_local: assert property (@(posedge clk) disable iff (!rst_n)
  busy |-> $stable(cfg));

throughout window: cfg must hold from start to done

  tick  :   1     2     3     4     5     6
  start :   0     1     0     0     0     0
  busy  :   0     1     1     1     1     0
  done  :   0     0     0     0     1     0
  cfg   :   C0    C0    C0    C1    C1    C1
                              ^
  attempt @2 ($rose(start)): $stable(cfg) must hold every tick the
  window spans (3..5). Tick 4: cfg C0→C1, $stable false → FAIL.
  The cycle-local form (busy |-> $stable(cfg)) also fails @4 — and
  pinpoints the tick directly, which is why many teams prefer it
  whenever a level like busy delimits the window.

Pulse-width discipline

Three distinct requirements hide under “pulse width,” and each gets its own idiom. Exactly one cycle: a rise is followed immediately by a fall. Minimum width: after a rise, the signal holds for at least N cycles. Maximum width: after a rise, a fall arrives within N cycles. Note these are clocked-sample rules — sub-cycle glitches between ticks are invisible to all of them (sampled-values edge-cases lesson); what you are policing is cycle-granular pulse discipline.

// Exactly one cycle wide (e.g. a kick/strobe signal)
a_pulse_1cyc: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(kick) |-> ##1 !kick)
  else $error("kick wider than 1 cycle");

// Minimum width: hold at least MIN cycles after rising
a_pulse_min: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req_pulse) |-> req_pulse [*MIN])
  else $error("pulse narrower than MIN");

// Maximum width: fall within MAX cycles of rising
a_pulse_max: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req_pulse) |-> ##[1:MAX] !req_pulse)
  else $error("pulse wider than MAX");

// Min AND max together: width in [MIN:MAX]
a_pulse_band: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req_pulse) |-> (req_pulse [*MIN] ##[0:MAX-MIN] !req_pulse));

Pulse-width band [MIN=2 : MAX=4] — three candidate pulses

  tick    :   1    2    3    4    5    6    7    8    9
  pulse A :   0    1    0    0    0    0    0    0    0   width 1
  pulse B :   0    0    0    1    1    1    0    0    0   width 3
  pulse C :   0    0    0    0    0    0    1    1    1   width ≥3...

  A: $rose@2 → need pulse[*2] from tick 2 → tick 3 sampled 0 → FAIL
  B: $rose@4 → pulse holds 4,5 (=[*2]) then ##[0:2] !pulse:
     tick 6 sampled 0 → PASS (width 3 inside band)
  C: if it holds through tick 11, the [*2] ##[0:2] window expires
     with no 0 observed → FAIL at tick 10 (wider than MAX=4)

Mutual exclusion and interrupt persistence

// Mutually exclusive controls: never both high in the same cycle
a_mutex: assert property (@(posedge clk) disable iff (!rst_n)
  !(wr_en && rd_en))
  else $error("simultaneous wr_en/rd_en");

// N-way version: at most one of a control bundle (idle allowed)
a_mutex_n: assert property (@(posedge clk) disable iff (!rst_n)
  $onehot0({mode_a, mode_b, mode_c, mode_d}));

// Interrupt held until serviced: once irq rises it must stay
// asserted until the service strobe; only then may it drop.
a_irq_held: assert property (@(posedge clk) disable iff (!rst_n)
  irq && !service |-> ##1 irq)
  else $error("irq dropped before service");

// And irq must actually clear promptly once serviced
a_irq_clears: assert property (@(posedge clk) disable iff (!rst_n)
  irq && service |-> ##[1:2] !irq)
  else $error("irq stuck after service");

Interrupt persistence: drop-before-service is the bug

  tick    :   1    2    3    4    5    6
  irq     :   0    1    1    0    0    0     ← drops at 4
  service :   0    0    0    0    1    0        but service is at 5

  a_irq_held attempt @3: irq&&!service → need irq@4 → sampled 0
  → FAIL@4: the CPU will read the pending-register and find nothing.
  This "wiggling interrupt" bug is invisible to directed tests that
  always service quickly — the assertion catches it on any stimulus.

  Healthy trace: irq 1 1 1 1 0 / service 0 0 0 1 0 → held to service,
  cleared within 2 → both assertions pass.

Note the persistence rule is the same hold-until-consumed skeleton as valid/ready's valid && !ready |-> ##1 valid and req/ack's hold rule — one structural pattern, three protocols. Recognizing these skeletons is what lets you improvise correct assertions for a protocol you have never seen.

Interview angle

Two prompts dominate. “Assert that config does not change during a transaction” — give the cycle-local busy |-> $stable(cfg) if a level delimits the window, and the throughout form when only start/end events exist; mention that the local form pinpoints the offending cycle while throughout reports at window end. “Assert a one-cycle pulse” — $rose(p) |-> ##1 !p, then expect the escalation to min/max bands and produce the [*MIN] ##[0:MAX-MIN] composition. The differentiating remark: clocked pulse checks are blind to sub-cycle glitches — say it before they ask. For mutual exclusion of N signals, reach for $onehot0 on a concatenation rather than N² pairwise rules.

Key takeaways

• throughout pins a condition across a sequence's whole span — the idiom for protected windows.

• Prefer cycle-local stability (busy |-> $stable) when a level delimits the window — better failure locality.

• Pulse discipline: ##1 !p for exact-one; [*MIN] for floors; ##[1:MAX] !p for ceilings; compose for bands.

• $onehot0 on a concatenation does N-way mutual exclusion in one assertion.

• Hold-until-consumed is one skeleton shared by irq/valid/req rules — learn patterns, not instances.

Common pitfalls

• throughout failures report at window end — harder to localize than per-cycle stability checks.

• Asserting $stable(cfg) on the same tick as $rose(start) — compares against the pre-start value.

• Believing a pulse-width assertion catches glitches between clock edges — sampling makes them invisible.

• N(N-1)/2 pairwise mutex assertions when $onehot0 of the concat does it in one.

• Interrupt rules without the clears-after-service half — a stuck-high irq passes the persistence rule forever.