A passing property can be a lie with a straight face. The trigger never fires, the environment never offers the interesting case, or the check compares a signal with itself, and the report still says pass. This topic makes every pass earn its keep: each implication gets a cover of its trigger, each cover gets a witness trace that you read, and any required scenario that cannot be reached fails sign-off outright. The running examples are the four-requester arbiter and the skid-buffer bridge, plus one dead trigger that passes and is caught.
Lesson | After it you can... |
|---|---|
Pair every implication with a trigger cover and read the witness cycle by cycle. | |
Spot a strangled environment from its silent covers and repair the harness. | |
Word the three cover outcomes correctly and prove unreachability when you claim it. | |
Catch a check that cannot fail by mutating the design and the property. |
Suggested order: top to bottom. Antecedent covers first, because they are the habit everything else builds on; over-constraint next, because it is the commonest reason covers go quiet; the bounded-miss wording next, because it stops a quiet cover being misread; mutation last, because it catches the vacuity that covers alone miss.
No. The check never fired, so the design could be arbitrarily broken in the covered behaviour. Treat the pair as a failure of the verification, not as evidence.