Reset & X-Checking Drills

Drill 1 — outputs hold reset values during reset

Problem

Interviewer: 'While reset is asserted, valid must be low and state must be IDLE. Careful — most candidates write a property that can never fire.'

Think it through

• The trap: disable iff (!rst_n) KILLS attempts while reset is low — adding it here aborts the very check you are writing. Reset-value properties must NOT carry the usual disable clause.

• Active-low rst_n: the in-reset condition is !rst_n. Plain overlapped implication, no temporal depth.

• If reset is asynchronous, the assertion still samples at the clock — pin-level async behavior between edges is out of SVA's reach; say so.

// NOTE: deliberately NO disable iff here
a_reset_values: assert property (
  @(posedge clk) !rst_n |-> (!valid && (state == IDLE)));

PASS trace                          FAIL trace
cycle :  0  1  2  3  4              cycle :  0  1  2  3  4
rst_n :  0  0  0  1  1              rst_n :  0  0  0  1  1
valid :  0  0  0  0  1              valid :  0  1  0  0  1
state :  I  I  I  I  R              state :  I  I  I  I  R

cycles 0-2 in reset: valid low,     valid pops high at cycle 1
state IDLE → PASS                   DURING reset → FAIL at 1.
                                    (with disable iff (!rst_n)
                                    this bug is INVISIBLE)

Common wrong answers

• disable iff (!rst_n) ... !rst_n |-> ... — the property self-disables; it can never report. The single most common reset-drill error.

• Checking only at $fell(rst_n) — verifies the entry cycle, not the whole reset duration.

• Mixing polarities — rst_n |-> reset-values checks during NORMAL operation. Write the polarity down before the property.

Drill 2 — no X on control signals after reset deasserts

Problem

Interviewer: 'Once reset deasserts, the control bundle (valid, ready, state) must never be X or Z. Both the one-shot check at the deassert edge and the continuous version, please.'

// One-shot: first post-reset cycle is clean
a_no_x_at_exit: assert property (
  @(posedge clk)
  $rose(rst_n) |=> !$isunknown({valid, ready, state}));

// Continuous: clean on every out-of-reset cycle
a_no_x_ever: assert property (
  @(posedge clk) disable iff (!rst_n)
  !$isunknown({valid, ready, state}));

Think it through + waveform

• $isunknown(expr) is true if ANY bit is X or Z — concatenate the bundle and check once.

• The one-shot uses |=> : at the $rose(rst_n) cycle itself, flops are still emerging from reset; the contract starts the following cycle. Defend the choice.

• The continuous form uses disable iff legitimately (we WANT it silent during reset) — contrast with Drill 1 where the same clause was fatal.

FAIL trace
cycle :  0  1  2  3  4
rst_n :  0  0  1  1  1
valid :  0  0  0  X  0     ← un-reset flop wakes up at 3

a_no_x_ever: attempt at cycle 3 sees $isunknown true → FAIL at 3.
Classic root cause: a flop missing from the reset tree, visible
only because the X-check made it loud.

Common wrong answers

• (valid !== 1'bx) — element-by-element !== checks miss Z and get verbose; $isunknown on the concatenation is the idiom.

• Checking X during reset too — many designs legally float pre-reset; scoping to post-reset keeps signal-to-noise high.

• Relying on implicit X-propagation through comparisons elsewhere — X == anything is X, which makes ordinary assertions VACUOUSLY pass, not fail. Explicit $isunknown checks are the only reliable X net.

Drill 3 — busy deasserts within N cycles of reset assertion

Problem

Interviewer: 'When reset asserts mid-operation, the busy flag must clear within 4 cycles. Note which clock domain and which disable clause you use.'

// Triggered BY reset assertion — so again, no disable iff (!rst_n)
a_busy_clears: assert property (
  @(posedge clk)
  $fell(rst_n) |-> ##[0:4] !busy);

PASS trace                          FAIL trace
cycle :  0  1  2  3  4  5           cycle :  0  1  2  3  4  5
rst_n :  1  0  0  0  0  0           rst_n :  1  0  0  0  0  0
busy  :  1  1  1  0  0  0           busy  :  1  1  1  1  1  1

fall@1; busy low by cycle 3         busy still high at 5 = fall+4
(within fall+4) → PASS              window [0:4] exhausted → FAIL.

Think it through + common wrong answers

• The property RUNS during reset, so disable iff (!rst_n) would abort it instantly — same lesson as Drill 1, now with a temporal window.

• ##[0:4] includes the assert-cycle itself: a design that clears busy combinationally on reset passes at offset 0.

• Wrong: $rose(rst) on an active-low rst_n — polarity slips are endemic in this family; one trace drawing catches them.

• If the clock can stop during reset (gated clocks), a clocked property cannot count — flag the assumption that clk keeps running.

Drill 4 — bus must be known when valid

Problem

Interviewer: 'Whenever valid is high, the 64-bit data bus must contain no X or Z bits. When valid is low we don't care. One property.'

a_data_known: assert property (
  @(posedge clk) disable iff (!rst_n)
  valid |-> !$isunknown(data));

Think it through + common wrong answers

• Qualification IS the spec: unqualified !$isunknown(data) fails on every idle cycle of a bus that legally floats between beats.

• This pattern (valid-qualified known-ness) is the cheapest, highest-yield X-check in any interface bind file — say that; it shows methodology awareness.

• Wrong: valid |-> (data !== 64'bx) — !== against all-X only detects the ALL-X pattern... actually data !== 64'bx is true unless every bit is X; one X bit among knowns slips through. $isunknown is per-bit. This subtlety is a favorite follow-up.

• Wrong: ^data === 1'bx as the check — works (XOR-reduce goes X if any bit is X/Z), but inverted logic and Z-handling subtleties make it a worse answer than the purpose-built function.

Drill 5 — first transaction only after init done

Problem

Interviewer: 'After reset deasserts, the block runs an init sequence and raises init_done. No valid may appear before init_done. Give me the invariant form AND the sequence form, and say which you'd ship.'

// Form 1: invariant — ship this one
a_no_valid_pre_init: assert property (
  @(posedge clk) disable iff (!rst_n)
  !init_done |-> !valid);

// Form 2: sequence form anchored at reset exit
property p_valid_waits;
  @(posedge clk)
  $rose(rst_n) |-> (!valid) until_with init_done;
endproperty
a_valid_waits: assert property (p_valid_waits);

FAIL trace (premature valid)
cycle    :  0  1  2  3  4  5
rst_n    :  0  1  1  1  1  1
init_done:  0  0  0  0  1  1
valid    :  0  0  1  0  0  1

Form 1: cycle 2 has !init_done && valid → FAIL at 2.
Form 2: window opens at rise@1; !valid must hold through
        cycle 4 (until_with) — violated at 2 → FAIL at 2.
valid at 5 (after init_done) is legal in both forms.

Think it through + common wrong answers

• Both forms catch the bug, but Form 1 is stateless, re-arms automatically if init_done ever drops (re-init), and survives mid-sim resets without anchoring logic. Prefer invariants whenever the spec allows.

• Form 2's until_with assumes valid may legally rise IN the init_done cycle; if not, use until — extract that detail from the spec aloud.

• Wrong: $rose(rst_n) |-> ##[1:$] init_done ##1 valid — over-constrains: demands a valid eventually appears, which the spec never required, and (weakly) checks nothing about EARLY valids.

Key takeaways

• Properties that CHECK reset behavior must not carry disable iff on that same reset — the clause silently kills them.

• $isunknown over a concatenation is the X-check idiom; !== comparisons against all-X literals miss partial-X buses.

• Prefer stateless invariants (!init_done |-> !valid) over anchored sequences when both express the spec — they re-arm for free.

Common pitfalls

• disable iff (!rst_n) on an in-reset check — the most common reset-family error in interviews and in real bind files.

• X never fails ordinary comparisons — X == X is X, implications go vacuous; only explicit $isunknown makes X loud.

• Polarity slips between rst, rst_n, $rose, $fell — draw the trace before writing the edge function.

• Assuming the clock runs during reset — gated-clock designs make clocked reset checks blind; state the assumption.