Bounds and induction are where precise vocabulary pays: bounded to N, proven, and inconclusive are three different claims, and panels fail candidates who merge them. This drill fixes the engine vocabulary. Each answer is two sentences; the trap column names the merge being fished for.
Question | Short answer | Trap | Teaching lesson |
|---|---|---|---|
What does a bounded PASS mean? | No counterexample exists within the stated depth. It proves nothing unbounded and becomes signoff-grade only with a bound justification. | Calling it a proof without the justification. | |
How do you choose a BMC depth? | At least reset plus trigger length plus worst-case latency plus 1, or a diameter argument. The decade-counter wrap bug needs depth 11: depth 10 passes and proves nothing. | One step short of the bug. | |
Base case versus induction step? | The base checks the first k states from reset; the step assumes any k consecutive states satisfy the property and checks the next. A pass needs both to the same k. | Raising k while the base covers fewer steps. | |
What is a counterexample to induction? | A step failure starting from an arbitrary state, possibly unreachable from reset. It indicts the invariant, not the design, until replayed from reset. | Fixing RTL for an unreachable-state trace. | |
When does raising k help? | When the property is inductive but needs a longer window to force the relation, as the retimed miter does at k of 3. When the step fails across a range of k, no k closes it. | Raising k instead of adding an invariant. | |
What makes a good helper invariant? | A true property tying state elements together, proved as an assertion, that excludes the unreachable states breaking the step. Pointer-equals-pointer-difference is the classic shape. | Assuming the helper instead of proving it. | |
Counterexample always wins: what does that mean? | A bounded counterexample on a model beats any unbounded pass claim on the same model, assumptions and reset. An apparent conflict means the models differed. | Overruling a trace with a second tool's pass. | |
What is inconclusive? | Undetermined: bound reached, time-out, or a failed induction step with a passing base. It demands a justified bound, a longer run, or a stronger proof, never a waiver by silence. | Counting not-failed as proven. | |
BMC versus k-induction versus IC3: when which? | BMC for bugs within reach and for bound arguments; k-induction for invariants with small helpers; IC3-style engines for deep properties where lemmas must be discovered. Diagnose cone, depth and engine progress first. | Naming engines without the selection rule. | |
What is the diameter argument? | The longest shortest path between reachable states: a bound at or beyond it sees every behaviour. The 4-entry FIFO control machine has diameter 7 transitions from reset. | Quoting a depth without the machine it covers. | |
Why do sampled-history properties need k of at least 2? | They judge the present against the previous cycle, so the step needs two consecutive states to check the relation. On the FIFO, bridge, register block and counter the transition properties close at 2; the pipeline's latency property looks three cycles back and needs 3. | Proving them at k of 1 and filing the pass. | |
A proof times out. First three reads? | Cone size per property, depth reached versus the bound the behaviour needs, and whether the engine is progressing or stuck. Then reduce, split, strengthen, in that order. | Tightening assumptions first. |
Inconclusive with a spurious counterexample to induction: strengthen with a helper invariant that excludes that state, and prove the helper as an assertion.