Hardware interview practice
How SVA disable iff Handles Reset
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?
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
Concise answer
The answer and the key reason
Deeper explanation
Work through the implementation and tradeoffs
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.
What to remember
- Reset aborts the live attempt
- Abort is neither pass nor fail
- New attempts begin after reset
Practice the complete prompt