Engines, run strategy and bounded proofs

Engine strategy

• Covers and bug hunting: BMC-style engines, possibly with simulation-guided "jumps" deep into the state space.
• Proofs: PDR/IC3 and k-induction; give them helper invariants.
• Small deep FSMs: BDD-based reachability can still win.
• Run engines in parallel and let the fastest finish; most tools do this by default.
• Prove helpers first, then use them as assumptions for the harder properties (tools often automate this).

When a bounded proof is enough

A bounded proof to depth N is convincing when you can show that N is large enough to reach every relevant behaviour:

1. Write covers for the deepest important scenarios (full FIFO with wrapped pointers, longest arbitration wait, every FSM state and transition).
2. Note the depth at which each is hit.
3. If all are hit well within N (rule of thumb: N at least twice the deepest cover), document the argument in the signoff report.

Chapter takeaways