An SVA check reports clean passes in dashboard summaries, yet silicon-like stress traces reveal protocol behavior that should violate intent under burst corner conditions.
The signal you would look at: High assertion pass rate paired with low antecedent hit coverage in failing workload classes.
Whether you know that a pass can be vacuous, and what evidence separates a real pass from an empty one.
Whether you can find the reason an antecedent never fires: reset masking, a wrong sampled value, or a trigger that is an event, not a level.
Whether you propose the guard (a cover property on the antecedent), not just a rewrite.
Follow these steps in order. The order matters: each step narrows the search so that the next one is cheap.
Ask for the antecedent hit count for the failing workload. A pass count with a zero or tiny hit count is the first red flag.
Write the cover property for the antecedent and look at whether it is ever hit in the burst traffic.
If it is never hit, find why: is the antecedent an event ($rose, $fell) that cannot happen on the sampled values, is disable iff aborting the attempt, or is a vector $rose looking only at its least significant bit?
If it is hit, check overlapping attempts: one response can satisfy several attempts, so a green log does not prove every request was answered.
Fix the property or the stimulus, show the assertion now fails on the known-bad trace, and keep the cover property in the signoff list.
A model transcript of the first part of the round. Do not memorise the words; copy the order of the moves.
Interviewer: The dashboard says the grant assertion passed a million times, and silicon still showed a missing grant. What is your first question?
Candidate: How many of those passes were non-vacuous? I want the antecedent hit count, or I add a cover property on the antecedent and rerun the failing workload.
Interviewer: The cover property never hits in the burst test.
Candidate: Then every attempt passed vacuously. I would check what the antecedent is: if it uses $rose on a vector, it only looks at the least significant bit, and if it is an event it will not fire when the signal stays high.
Interviewer: It is $rose(req) and in the burst traffic req stays high.
Candidate: Right, $rose is an event, it fires on the transition only. A level condition would have started an attempt every cycle. I would change the trigger to match the protocol rule, and then confirm the property now fails on the known-bad trace.
Interviewer: What if the cover hits but you still miss bugs?
Candidate: Then I check disable iff and overlapping attempts. A reset glitch can abort the attempt, and one grant can satisfy two overlapping requests, so the log is green while a request goes unanswered.
Interviewer: What do you put in signoff?
Candidate: Assertion status together with the cover property for each antecedent, so a pass only counts when the property was actually exercised.Treating pass counts as proof of behavior without checking antecedent activation.
Using overly restrictive disable conditions that prevent property engagement.
Closing signoff on assertion status alone instead of correlating with cover properties.
Forgetting that $rose and $fell are events, so a signal that stays high starts no attempt.
Work these cold, with the timer, before you rehearse the conversation.