Pulse & Stability Drills

Drill 1 — signal high for exactly one cycle

Problem

Interviewer: 'irq must always be a single-cycle pulse. Assert it.'

Think it through

• 'Exactly one cycle' decomposes into: if it rose, it must be low the next cycle. The rise edge is the natural trigger.

• $rose(irq) |=> !irq is the whole answer. Resist the urge to add operators.

• The level form (irq |=> !irq) happens to behave identically for genuine pulses, but the failure REPORTING differs on a stuck-high bug: the level form fails every cycle, the edge form fails once. Once is what you want in a log.

a_irq_one_cycle: assert property (
  @(posedge clk) disable iff (!rst_n)
  $rose(irq) |=> !irq)
  else $error("irq wider than one cycle");

PASS trace                          FAIL trace
cycle :  0  1  2  3  4              cycle :  0  1  2  3  4
irq   :  0  1  0  0  1              irq   :  0  1  1  0  0

Rises at 1 and 4; low the           Rise at 1; irq still high at 2.
following cycle each time → PASS    FAIL reported at cycle 2, once.

Variation — pulse must also occur (cover, not assert)

// The assert alone passes vacuously if irq never fires.
// Pair it with a cover so the testbench proves the pulse happened:
c_irq_seen: cover property (@(posedge clk) $rose(irq));

Common wrong answers

• $rose(irq) |-> !irq — same-cycle check: $rose means irq IS high this cycle, so this is a contradiction that fails on every legal pulse.

• irq ##1 !irq as a bare property — a sequence used as a property only checks the first attempt cycle; you wanted an implication.

• Adding ##1 $fell(irq) on top of |=> !irq — redundant; !irq next cycle IS the fall. Over-engineering reads as not understanding.

Drill 2 — pulse width between MIN and MAX cycles

Problem

Interviewer: 'busy must stay high at least 2 and at most 4 cycles. Write the assertion, and walk me through why your upper bound actually works.'

Think it through

• Anchor on the rise. From the rise, busy must repeat high 2 to 4 times total, then be low.

• busy[*2:4] alone does NOT enforce the max: a 6-cycle pulse contains a 4-cycle match, so the consequent would succeed. The ##1 !busy terminator is what makes the max real.

• Consequent (busy[*2:4] ##1 !busy) has up to 3 ways to match; an assert needs only one to succeed — exactly the semantics we want.

property p_busy_width_2_4;
  @(posedge clk) disable iff (!rst_n)
  $rose(busy) |-> busy[*2:4] ##1 !busy;
endproperty
a_busy_width: assert property (p_busy_width_2_4);

PASS trace (width 3)                FAIL trace (width 5)
cycle :  0  1  2  3  4  5           cycle :  0  1  2  3  4  5  6
busy  :  0  1  1  1  0  0           busy  :  0  1  1  1  1  1  0

Rise at 1. busy[*3] = cycles        Rise at 1. Threads try widths
1,2,3 then !busy at 4.              2,3,4 — each demands !busy next
The [*3] thread matches → PASS      (at 3,4,5) and busy is still high.
                                    All threads dead → FAIL at cycle 5.

FAIL trace (width 1):  busy = 0 1 0 ...
busy[*2] needs cycles 1 AND 2 high; cycle 2 is low → FAIL at cycle 2.

Variation — minimum width only

// 'busy high at least 2 cycles' — no terminator needed:
a_busy_min2: assert property (
  @(posedge clk) disable iff (!rst_n)
  $rose(busy) |-> busy[*2]);
// Equivalently: $rose(busy) |=> busy;

Common wrong answers

• $rose(busy) |-> busy[*2:4] — silently drops the max bound; the most common error on this drill, and interviewers probe for it specifically.

• $rose(busy) |=> busy[*2:4] ##1 !busy — the |=> skips the rise cycle, so the count is off by one: this accepts widths 3..5.

• not (busy[*5]) as the max check — workable ('never 5 consecutive high'), but then the min check is separate; fine if you SAY it covers only the max.

Drill 3 — data stable while enable is high

Problem

Interviewer: 'While en is asserted, data must not change. data may change in the same cycle en rises. Assert it.'

Think it through

• $stable(data) compares this cycle's sampled value to last cycle's. So the obligation applies on cycles where en is high NOW and was ALSO high LAST cycle — the second-and-later cycles of an en window.

• en && $past(en) |-> $stable(data) encodes precisely that, and naturally allows data to change in the rise cycle.

• The sequence form en ##1 en |-> $stable(data) is identical; use whichever you can defend.

a_data_stable: assert property (
  @(posedge clk) disable iff (!rst_n)
  (en && $past(en)) |-> $stable(data));

PASS trace                          FAIL trace
cycle :  0    1    2    3    4      cycle :  0    1    2    3    4
en    :  0    1    1    1    0      en    :  0    1    1    1    0
data  :  AA   55   55   55   77     data  :  AA   55   55   66   77

data changes at 1 (rise cycle —     data changes at cycle 3 while
allowed) and at 4 (en low —         en was high at 2 and 3.
allowed). Cycles 2,3: stable        $stable(data) false at 3 → FAIL.
→ PASS

Variation — stable through the whole window, throughout-style

// 'From en rise to en fall, data frozen at its rise-cycle value'
// Local variable captures the value at the rise:
property p_data_frozen;
  logic [7:0] d0;
  @(posedge clk) disable iff (!rst_n)
  ($rose(en), d0 = data) |=> (data == d0) until !en;
endproperty
// Stronger than $stable: catches change-and-change-back glitches
// that return to a DIFFERENT value than the rise-cycle snapshot.

Common wrong answers

• en |-> $stable(data) — fires on the rise cycle too, where $stable compares against the pre-en value. Legal setup changes now fail.

• $rose(en) |-> $stable(data) until $fell(en) — $stable on the rise cycle again; also until's exclusive endpoint needs justifying.

• $past(en) without pairing it with en — checks one cycle too long, into the cycle after en falls.

Drill 4 — no glitch between transactions (stability window)

Problem

Interviewer: 'After valid drops, the data bus must hold its last value until the next valid. Glitches between transactions have been corrupting a downstream latch. Write the check.'

Think it through

• Window opens at $fell(valid), closes when valid returns. Inside the window data must be $stable every cycle.

• Weak until is the honest choice in simulation: if no new valid ever comes, the window runs to end-of-sim and passes — acceptable.

• data may change WITH the new valid, so the window must exclude the arrival cycle: plain until (exclusive) is exactly right here.

property p_no_glitch;
  @(posedge clk) disable iff (!rst_n)
  $fell(valid) |=> $stable(data) until valid;
endproperty
a_no_glitch: assert property (p_no_glitch);

PASS trace                          FAIL trace
cycle :  0    1    2    3    4      cycle :  0    1    2    3    4
valid :  1    0    0    0    1      valid :  1    0    0    0    1
data  :  AA   AA   AA   AA   BB     data  :  AA   AA   CC   AA   BB

valid falls at 1; window 2..3.      Glitch: data flips to CC at 2.
$stable holds at 2 and 3; data      $stable(data) false at 2 → FAIL.
changes at 4 WITH valid → PASS

Common wrong answers

• until_with valid — demands stability INTO the new-valid cycle, failing the legal data change that rides in with valid.

• $fell(valid) |-> $stable(data) until valid — |-> starts in the fall cycle, where data still legally holds the last beat... usually passes, but the off-by-one reasoning is wrong; |=> states the intent.

• Asserting $stable(data) whenever !valid as a plain invariant (!valid |-> $stable(data)) — also fails the first idle cycle after a data change aligned with the last valid beat. Trace it before claiming equivalence.

Drill 5 — two signals never both high

Problem

Interviewer: 'rd_en and wr_en must be mutually exclusive. One line.'

a_mutex: assert property (
  @(posedge clk) disable iff (!rst_n) !(rd_en && wr_en));

// Scales to N signals:
a_mutex_n: assert property (
  @(posedge clk) disable iff (!rst_n) $onehot0({rd_en, wr_en, er_en}));

Think it through + common wrong answers

• Pure combinational invariant — no implication, no delays. Writing rd_en |-> !wr_en works but passes vacuously every idle cycle; the direct boolean is cleaner and the vacuity question disappears.

• $onehot0 allows all-zeros; $onehot would demand exactly one high every cycle — a different (and here wrong) spec.

• This is a sampled check: a sub-cycle combinational glitch between clock edges is invisible to SVA. Saying that unprompted is a senior marker.

Key takeaways

• Pulse-width max bounds need a terminator (##1 !sig) — repetition ranges alone only enforce the minimum.

• $stable compares against the previous sample — exclude window-opening cycles from stability obligations (en && $past(en)).

• until excludes the closing event's cycle, until_with includes it; glitch-window drills hinge on that single choice.

Common pitfalls

• busy[*2:4] without ##1 !busy — max bound silently unenforced; long pulses pass.

• $rose(x) |-> !x — same-cycle contradiction; |-> overlaps, the rise cycle has x high.

• Stability asserted from the rise cycle — $stable compares into the pre-window past and fails legal setup changes.

• Treating $onehot0 and $onehot as interchangeable — all-idle cycles fail under $onehot.