Q082FreeDesign Verification
SVA Overlapped vs. Nonoverlapped Implication
Question
For the one-cycle antecedent a, which property is cycle-equivalent to the property shown?
Code to inspect
assert property (@(posedge clk) a |=> b);Answer choices
- A. a |-> b
- B. a throughout b
- C. a |-> ##2 b
- D. a |-> ##1 b
Short answer
For this one-cycle antecedent, `a |=> b` is cycle-equivalent to `a |-> ##1 b`. Nonoverlapped implication checks the consequent on the sampled edge after `a`; overlapped implication plus an explicit one-cycle delay reaches that same edge.
Why this reasoning works
An assertion attempt begins when `a` is true at a rising-edge sample. With `|=>`, evaluation of `b` starts at the next sampling event, so `b` must be true one clock later. The operator describes clocked sequence timing, not a delay measured in simulator time units.
In `a |-> ##1 b`, the overlapped operator places the consequent sequence at the antecedent endpoint, and `##1` advances the actual `b` test by one sampled clock. The two formulations therefore align for the shown Boolean antecedent. Neither `throughout` nor an undelayed overlapped implication expresses that next-cycle requirement. Both use the same property clock.
Interview takeaways
- `|=>` starts next cycle
- `|->` starts at the endpoint
- `##1` adds one sampled clock