Almost every panel asks the same three probes on every property: what did you assume, what if the trigger never fires, and how do you know the pass is real. This drill makes those answers automatic. Each answer is two sentences; the trap column names the mistake being fished for.
Question | Short answer | Trap | Teaching lesson |
|---|---|---|---|
Assume or assert: how do you decide? | Assume on primary inputs what the neighbour owes you; assert on outputs what you owe. Every assume is discharged as an assertion on the neighbour or at integration. | Asserting on inputs, which fails on legal traffic. | |
What is over-constraint? | Assumptions that together exclude behaviour the design must handle, so properties pass on a pruned model. Found by unreached activity covers and by a mutant the harness no longer catches. | Calling it a design bug instead of a harness bug. | |
What is vacuity? | The antecedent or trigger is never true, so an implication-style property passes without checking anything. A weak sequence that never completes is not vacuous, it is unfinished. | Confusing weak semantics with vacuity. | |
How do you prove a pass is not vacuous? | Reach the antecedent cover of every implication-style property and an activity cover for the environment, then mutate the design and watch each property fail. | Quoting the passing report as its own evidence. | |
What does a cover not reached within N mean? | Inconclusive: nothing about reachability is decided. Only an engine-proved unreachable is unreachable. | Filing a bound miss as proven unreachable. | |
What is mutation testing of a harness? | Inject one bug per property class and require each property to fail at a stated step. A property that survives its mutant cannot protect the design. | Mutating only the easy paths. | |
What can reset gating hide? | Two gates, two blind spots. The gate disable iff hides an output that is wrong only while reset is asserted; the history guard skips the cycle after reset and hides a wrong reset value that run mode overwrites. Keep an explicit reset-state check per reset-valued output. | Trusting a gated pass on reset values. | |
What breaks assume-guarantee soundness? | An assumption about a removed block that is never proved as an assertion on that block, or a circular pair with no induction-on-time argument. | Assuming the contract instead of proving it. | |
Where do black-box outputs come from? | They are free: any value at any cycle until a documented contract constrains them. Passing proofs stay valid; spurious failures are cured by contracts, never by blind tightening. | Treating a spurious failure as a design bug. | |
How do you port simulation constraints to formal? | Input-side checks become assumes only when the neighbour guarantees them; the same rule asserted in the bench stays an assert at the boundary. Usage rules nobody owes become covers, not assumes. | Assuming the whole testbench. | |
What belongs in an assumption register? | Each assume with its owner, the neighbour assertion discharging it, and the runs it constrains. Reviewed at signoff, rerun on every RTL change. | An undocumented list in one engineer's directory. | |
A block proves instantly. First move? | Read the cover column, then the cone, then the assumption list. An instant proof is the signature of vacuity, a disconnected property, or reset held for ever. | Celebrating the speed. |
That the harness constrains more than it checks: each undischarged assume is a behaviour the proof never examined, and the panel will ask for the owner of every line.