Q011FreeDesign Verification
How SVA disable iff Handles Reset
Question
A request is sampled high, but rst_n goes low before the next edge where gnt would be checked. What happens to that pending assertion attempt?
Code to inspect
assert property (@(posedge clk) disable iff (!rst_n) req |=> gnt);Answer choices
- A. It fails because gnt was not checked
- B. It passes nonvacuously
- C. It is asynchronously disabled and produces neither pass nor failure for that attempt
- D. It remains pending until rst_n rises
Short answer
The pending attempt is canceled as soon as `rst_n` becomes low. It is not counted as a pass or failure and does not wait to resume. `disable iff` acts independently of the assertion’s sampling edge, so reset between edges still aborts it.
Why this reasoning works
When `req` is sampled high, the nonoverlapped implication creates an obligation to examine `gnt` at the following rising edge. Before that check arrives, `!rst_n` becomes true. The disable condition terminates the live property evaluation, removing the outstanding obligation rather than evaluating a missing grant as a failure for that attempt.
This behavior differs from placing reset only inside a clocked antecedent, which samples reset at assertion events. It is useful when reset should invalidate in-flight protocol checks immediately. Once reset is released, future clock edges may launch new attempts, but the canceled attempt is gone; it is neither paused nor restarted.
Interview takeaways
- Reset aborts the live attempt
- Abort is neither pass nor fail
- New attempts begin after reset