disable iff & Reset Handling

What disable iff actually does

disable iff (expr) is the property-layer reset gate. Its semantics are asynchronous abort : whenever the disable expression is true — checked continuously, with current values, not sampled values — every in-flight attempt of that property is killed immediately, with no pass and no fail recorded, and no new attempt produces a result while the condition holds. Aborted attempts simply vanish from the statistics (most tools count them as "disabled"). This is exactly what you want across reset: a handshake that was mid-window when reset hit is neither a failure nor a pass — it is void.

// The canonical pattern — active-low async reset
property p_req_ack;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack;
endproperty
ap_req_ack: assert property (p_req_ack)
  else $error("ack window violated");

IN-FLIGHT ATTEMPTS DURING RESET — req |-> ##[1:3] ack, disable iff (!rst_n)

  clk    : T0    T1    T2    T3    T4    T5    T6
  rst_n  : 1     1     1     0     0     1     1
                             └──reset──┘
  req    : 0     1     0     0     0     0     1
  ack    : 0     0     0     0     0     0     0

  attempt@T1: req=1 → waiting for ack in window [T2..T4]
                T2: ack=0, thread alive
                T3: rst_n goes 0 → ATTEMPT KILLED (no fail!) ☒
  attempt@T3, @T4: disabled while rst_n=0 → no result
  attempt@T6: req=1 → fresh attempt, full window [T7..T9] — reset
              left no residue; the property starts clean.

  Without disable iff: attempt@T1 would FAIL at T4 — a false failure
  caused by reset, not by the design.

Two semantic details that matter: the disable expression is evaluated asynchronously with current values (it does not wait for a clock edge — a mid-cycle reset pulse still aborts), and it resets the whole property including any local variables. It is legal only at the property layer — never inside a sequence.

Sync vs async reset in assertions

disable iff's async-abort semantics pair naturally with asynchronous resets. For a fully synchronous reset, async abort is usually still acceptable — killing attempts a fraction of a cycle early is rarely observable — but if you need strictly clock-aligned gating (for example, the spec defines behavior in the very cycle reset asserts), gate the antecedent instead, or combine both styles.

// Style 1: async abort — standard, works for async or sync reset
property p_async_gate;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack;
endproperty

// Style 2: sampled (clock-aligned) gating in the antecedent —
// uses SAMPLED rst_n, attempt simply never starts during reset
property p_sync_gate;
  @(posedge clk)
  (rst_n && req) |-> ##[1:3] ack;
endproperty
// Caveat: an attempt started BEFORE reset keeps running into reset —
// style 2 alone does NOT kill in-flight attempts.

// Style 3: belt and braces — gate new attempts AND abort in-flight ones
property p_both;
  @(posedge clk) disable iff (!rst_n)
  (rst_n && req) |-> ##[1:3] ack;
endproperty

WHY STYLE 2 ALONE IS NOT ENOUGH

  clk    : T0    T1    T2    T3    T4
  rst_n  : 1     1     0     0     1
  req    : 1     0     0     0     0
  ack    : 0     0     0     0     0

  Style 2 (antecedent gate only):
    attempt@T0: (rst_n && req)=1 → window [T1..T3] →
                ack never comes → FAILS at T3, DURING reset ✗ false fail
  Style 1/3 (disable iff):
    attempt@T0 aborted the moment rst_n drops at T2 → void ☒  correct

Reset gating patterns for real environments

Beyond a single rst_n

// Compound disable: hardware reset OR test-controlled assertion-off window
bit assertions_off;   // TB can set around error-injection scenarios

property p_gated (sequence s_check);
  @(posedge clk) disable iff (!rst_n || assertions_off)
  s_check;
endproperty

// Post-reset settling: require N clean cycles after deassertion before
// the antecedent can engage (some IP is allowed to misbehave briefly)
logic [2:0] rst_done_sr;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) rst_done_sr <= '0;
  else        rst_done_sr <= {rst_done_sr[1:0], 1'b1};
wire rst_settled = rst_done_sr[2];   // 3 cycles after deassert

ap_after_settle: assert property (@(posedge clk) disable iff (!rst_n)
  (rst_settled && req) |-> ##[1:3] ack);

• Use the same reset polarity and signal the RTL uses — a checker on the wrong reset tree creates phantom failures during partial resets.

• TB-controlled disable bits (assertions_off) beat $assertoff for surgical scope: one property, one window, self-documenting.

• For multi-domain designs, each property's disable iff should use the reset of the clock domain it checks.

• Also assert reset behavior itself: e.g. outputs quiet during reset — a property whose ANTECEDENT is reset, which therefore must NOT be disabled by it.

// Checking behavior DURING reset — do NOT disable iff on the same reset!
ap_quiet_in_reset: assert property (@(posedge clk)
  !rst_n |-> (!valid && !req))
  else $error("interface not quiet during reset");

The double-gating mistake

The most common reset bug in assertion code is gating the same property twice with opposite tools : disable iff for abort plus putting reset inside the temporal logic — or worse, gating with sampled reset inside the expression while disable iff uses current values. The two gates disagree for one cycle around each reset edge, producing heisen-failures that appear only with specific reset timing.

DOUBLE GATING — why it breaks at the deassert edge

  property: disable iff (!rst_n)  (rst_n && req) |-> ##1 ack;
                current-value gate  sampled-value gate

  clk    : T0    T1    T2
  rst_n  : 0     1     1      ← deasserts between T0 and T1 (async)
  req    : 0     1     0

  At T1: disable iff sees rst_n=1 (current)  → property ARMED
         antecedent samples rst_n... PREPONED value at T1 = may be 0!
         → (rst_n && req) = 0 → vacuous pass — silently skipped a
           cycle the spec says must be checked. With the opposite
           timing skew it instead double-checks. One reset, two gates,
           two clocks-worth of ambiguity.

  RULE: one property, ONE reset gate. disable iff for abort semantics;
  antecedent gating only when you specifically need sampled alignment —
  and if you truly need both (style 3), understand the edge-cycle gap.

Interview angle

"How do assertions handle reset?" is guaranteed in any SVA interview round. Model answer: disable iff at the property layer; it evaluates its expression asynchronously with current values and aborts all in-flight attempts without recording pass or fail; attempts restart cleanly after deassertion. Then volunteer the distinction between aborting in-flight attempts (disable iff) and preventing new ones (antecedent gating).

• Trap question: "What happens to an attempt that was mid-window when reset asserted?" — aborted, neither pass nor fail; without disable iff it would falsely fail.

• Trap question: "Is the disable iff expression sampled like other signals?" — No: current values, asynchronous; this is THE asymmetry interviewers fish for.

• Trap question: "Write an assertion that the bus is quiet during reset." — antecedent is reset itself; candidates who reflexively add disable iff (!rst_n) disable their own check.

• Follow-up: "disable iff vs $assertoff?" — disable iff is per-property, declarative, formal-friendly; $assertoff is a procedural system-task sledgehammer for sim control.

Key takeaways

• disable iff aborts every in-flight attempt asynchronously, with current (unsampled) values; aborted attempts record nothing.

• Antecedent gating prevents new attempts but cannot kill in-flight ones — across reset you generally need disable iff.

• Use the reset of the domain you are checking, and consider post-reset settling windows for IP that needs them.

• Properties about reset behavior itself must not be disabled by that same reset.

• One property, one gate — mixing current-value disable iff with sampled in-expression reset creates one-cycle heisenbugs.

Common pitfalls

• No disable iff at all — every reset event sprays false failures from aborted handshakes.

• disable iff (rst_n) with wrong polarity — property is disabled the entire test, passes vacuously forever, dashboards stay green.

• Double gating with mismatched sampling (current vs preponed) — failures that only reproduce with particular reset alignment.

• Putting disable iff inside a sequence — illegal; it is property-layer only.

• Forgetting local variables are also cleared on abort — state you hoped to carry across reset is gone by design.