During reset, most signals are in an undefined or transitioning state — and if an assertion happens to be partway through a multi-cycle check exactly when reset asserts, it can report a failure that has nothing to do with a genuine protocol violation. disable iff exists specifically to prevent this.
11 min read | Intermediate Level
What You'll Learn
- What
disable iffdoes, and where it's placed within a property - Why gating a property's antecedent isn't enough to protect an already-in-progress check
- How
disable iffcan abort a check that already started before the disable condition became true - Why
disable iffis used almost exclusively for reset, rather than arbitrary conditions
Syntax
disable iff is placed right after the clocking event, before the rest of the property expression:
property p_name;
@(posedge clk) disable iff (condition) antecedent |-> consequent;
endproperty
assert property (p_name);
When condition becomes true at any point during the property's evaluation — not just at the moment a new attempt would start — that specific attempt is aborted immediately. It's neither counted as a pass nor a fail; it simply stops being evaluated.
Why Gating the Antecedent Isn't Enough
It might seem like ANDing the reset condition into the antecedent itself — !rst && req |-> ##2 gnt — would achieve the same protection. It doesn't, and the reason matters: that only controls whether a new attempt is allowed to start. It has no effect on a check that already started one or more cycles earlier and is still waiting to resolve. disable iff is different: it can reach back and abort an already in-flight check the moment its condition becomes true, regardless of how far into its own evaluation window that check already was.
A Concrete Example: Aborting a Check Mid-Flight
Take a simple property: whenever req is seen, gnt must follow exactly 2 cycles later.
// Without disable iff - vulnerable to a spurious failure if reset
// happens to occur while a check is already in progress
property p_no_disable;
@(posedge clk) req |-> ##2 gnt;
endproperty
assert property (p_no_disable);
Now suppose the following happens: req is high at cycle 1, starting a check that needs gnt to be high at cycle 3. But at cycle 2, reset asserts — and by cycle 3, gnt is low, as it typically would be during or right after a reset.
Without disable iff, the check that started at cycle 1 has no way to know reset happened partway through — it simply evaluates whether gnt is high at cycle 3, finds it isn't, and reports a failure. This is a spurious failure: nothing about the actual protocol was violated, reset just happened to land in the middle of an in-flight check.
Adding disable iff fixes this:
// With disable iff - the in-flight check from cycle 1 is safely
// aborted the moment rst goes high at cycle 2
property p_with_disable;
@(posedge clk) disable iff (rst) req |-> ##2 gnt;
endproperty
assert property (p_with_disable);
With this version, the moment rst goes high at cycle 2 — while the check started at cycle 1 is still waiting to resolve at cycle 3 — that check is aborted immediately. No pass, no fail. Whatever gnt happens to be doing at cycle 3 no longer matters, because the relevant attempt was already called off a cycle earlier.
Quick Check
Q: If reset instead asserted at cycle 3 (the exact cycle gnt is being checked), rather than cycle 2, would disable iff (rst) still prevent a spurious failure?
Show Answer
Yes. disable iff checks its condition continuously throughout the property's evaluation, not just at a fixed point — if rst becomes true at the exact cycle the consequent would otherwise be checked, the attempt is still aborted before that check can produce a false failure.
Where Is disable iff Used?
Almost every concurrent assertion in a real testbench includes disable iff (!rst_n) (or the active-high equivalent), tied to the design's own reset signal. It's rare to see a production assertion without one, since reset periods are exactly when signals are least reliable and most likely to produce a spurious failure if left unguarded.
Common Beginner Mistakes
Mistake #1: Gating the antecedent instead of using disable iff
As explained above, !rst && req |-> ... only prevents new attempts from starting — it does nothing for a check already in progress when reset asserts. Why? This gap is exactly what produces spurious failures during reset if disable iff isn't used instead.
Mistake #2: Forgetting disable iff entirely
As the worked example shows, an assertion with no reset handling at all can report a completely misleading failure the moment reset happens to interrupt an in-flight check. Why? A spurious, reset-induced failure wastes debug time chasing something that was never a real bug — almost every real assertion needs this protection.
Mistake #3: Placing disable iff in the wrong position
disable iff belongs right after the clocking event and before the rest of the property expression — not anywhere else in the property. Why? This ordering is part of the required property syntax; placing it elsewhere is a syntax error, not just a style preference.
Mistake #4: Using disable iff for something other than reset
While technically legal to use with any condition, disable iff is used almost exclusively for reset in practice. Why? Its whole purpose is suppressing checks during a period when the design's own signals are known to be unreliable — using it to silence an assertion under some other arbitrary condition usually signals the property itself needs rethinking, not that disable iff is the right tool.
Practice Exercise
Challenge: Add disable iff to a Data-Stability Check
Write a property that checks: whenever valid is high and ready is low, data must stay stable (unchanged) on the following cycle. Include disable iff tied to an active-low reset signal rst_n.
Hint
Use $stable(data) as the consequent, and remember disable iff goes right after the clocking event, before the rest of the property.
Solution
property p_data_stable;
@(posedge clk) disable iff (!rst_n)
(valid && !ready) |=> $stable(data);
endproperty
assert property (p_data_stable);
Without disable iff (!rst_n), a reset happening to occur right as data is being checked for stability could easily produce a spurious failure — reset typically forces data to a known value, which would look exactly like an unexpected change to $stable() if the check weren't safely aborted first.
Summary
In this tutorial, you learned:
disable iff (condition)aborts a property's evaluation the moment its condition becomes true, reporting neither a pass nor a fail- It's placed immediately after the clocking event, before the rest of the property expression
- Gating the antecedent alone only prevents new attempts from starting — it can't abort a check already in progress, which is exactly what
disable iffcan do - Its condition is checked continuously throughout a property's evaluation, not just once at the start
disable iffis used almost universally for reset, since that's when a design's signals are least trustworthy
