Formal Verification · All levels
SystemVerilog Assertions (SVA): Tricky Q&A
Senior interview and review questions for SystemVerilog Assertions (SVA).
Section Q&A bank
Use these drills after completing all topics in SystemVerilog Assertions (SVA). Answer with requirement context, mechanism proof, artifact, owner, and signoff decision.
When does `a |-> b` fail differently from `a |=> b`, and why does it matter for handshakes?
[INT][FORMAL][SVA-ASSERTIONS]
Q: When does `a |-> b` fail differently from `a |=> b`, and why does it matter for handshakes?
A:
They differ at the start point of the consequent. `|->` checks `b` in the same sampled cycle as `a`, while `|=>` shifts consequent evaluation by one cycle. If a protocol allows ready one cycle after valid, using `|->` can create false failures; if the protocol requires same-cycle backpressure handling, using `|=>` can hide a real timing bug.
FOLLOW-UP TRAP: Treating `|->` and `|=>` as interchangeable implication syntax with no timing impact.Why can a liveness property appear to pass in formal even though simulation shows no progress?
[INT][FORMAL][SVA-ASSERTIONS]
Q: Why can a liveness property appear to pass in formal even though simulation shows no progress?
A:
A weak eventuality can pass vacuously on finite prefixes or under unconstrained environments where the trigger is avoided. You often need strong eventuality (`strong(##[1:$] done)`) plus explicit fairness assumptions to force meaningful progress obligations and prevent trivial proofs.
FOLLOW-UP TRAP: Assuming any 'eventually' formulation automatically proves real forward progress.What common reset mistake makes SVA failures noisy and misleading at startup?
[INT][FORMAL][SVA-ASSERTIONS]
Q: What common reset mistake makes SVA failures noisy and misleading at startup?
A:
Omitting or mis-scoping `disable iff` causes assertions to evaluate during reset deassertion turbulence, unknown states, or uninitialized control paths. This produces failures unrelated to functional behavior and can mask true post-reset issues by drowning regressions in startup noise.
FOLLOW-UP TRAP: Believing reset handling is optional if the design reaches steady state quickly.A property never fails and never hits cover; what is the most likely root cause?
[INT][FORMAL][SVA-ASSERTIONS]
Q: A property never fails and never hits cover; what is the most likely root cause?
A:
The antecedent is never true at sampled clock boundaries (or is over-constrained), so the assertion is vacuous. First debug trigger reachability with `cover property`, check clock/reset sampling alignment, and inspect assumptions/constraints before concluding the design is correct.
FOLLOW-UP TRAP: Interpreting a non-failing assertion as proof of correctness without vacuity analysis.Q&A drill guide
REQUIREMENT -> PROPERTY -> EVIDENCE -> OWNER ACTION -> RESIDUAL RISKSketch while answering
SVA INTENT CHAIN
timing contract -> sequence composition -> property implication -> sampled failure traceCommon traps
Confirm antecedent trigger at sampled clock edges.
Verify implication operator matches protocol timing contract.
Split monolithic properties into stage-local checks.
Key takeaways
Tie each proof claim to assumption boundaries and reachability evidence.
Prefer minimal reversible fixes and preserve legal behavior visibility.
Common pitfalls
Treating runtime reduction as proof-quality improvement without audits.
Declaring closure while critical covers remain unreachable.
Using broad waivers instead of first-divergence root-cause ownership.