A bounded run answers a narrow question: is there a violation within N steps of reset? Everything in this topic follows from taking that question literally. You will unroll a design by hand, derive depths from reset length plus trigger length plus latency plus one, watch a late bug hide below its bound and appear above it, and learn the rule that settles every argument about disagreeing runs: on the same model, a counterexample always wins.
Lesson | After it you can... |
|---|---|
Write out what a bounded check asks the solver and price it in clauses. | |
Derive a depth from the design instead of guessing one. | |
Report bounded to N honestly and show the bug it misses. | |
Settle a disagreeing-runs argument by listing what differed. |
Suggested order: top to bottom. Unrolling first, because depth means nothing until you see the copies. Depth choice second, because it uses the unrolling picture. The invisible-bug lesson third, because it motivates the depth rules. The wins-every-time rule last, because it generalises the whole topic beyond depth to assumptions and reset.
A bounded pass says no violation within N steps of reset; a proof says no violation in any reachable state. The first is a statement about the search, the second about the design.