Bounded model checking finds bugs, but it never proves that there are none beyond its depth. For sign-off on a critical block, teams want more: a statement that a property holds in every cycle, forever. This chapter shows how formal tools give that statement with induction, why induction sometimes fails on a correct design, and how to fix it by adding the right helper properties.
A pass from a bounded check reads like good news, but its meaning is narrow: no input sequence of up to k cycles breaks the property. Everything beyond cycle k is unchecked. This article explains what separates a bounded pass from a proof, when a bounded pass is already enough, and the two ways a formal tool can reach a real proof.
7 min read | Intermediate
What You'll Learn
- State exactly what a bounded pass guarantees and what it does not
- Explain when a bounded check is complete, using the reachability diameter
- Name the two routes to a full proof: complete BMC and induction
- Report formal results with the right status: proven, bounded or failed
What a Bounded Pass Says
The chapters so far showed many bounded passes that hid bugs. The mod-60 counter passed at depth 62 and failed at 63. The watchdog passed at depth 100 and wrapped after 1024 cycles. Nothing in the passing runs warned about the bug.
A bounded pass covers the green box: all states the design can reach within the depth. The property may still fail in a state further away. To prove it, a tool has to cover every reachable state, at any distance from reset.
Route 1: Complete BMC
If the depth is larger than the reachability diameter, the longest shortest path from reset to any state, the green box is the whole outer box. Then a bounded check of an invariant is a proof. The choosing a depth article introduced the diameter.
This route works for small control blocks whose every state is reachable in a few cycles: an arbiter, a short state machine, a handshake controller. It does not work for anything with a large counter, a deep FIFO or a big memory, because their diameters run into the thousands or billions. Tools also rarely know the diameter, so in practice this route is an argument you make by hand.
Quick Check
Q: A 3-state machine with no counters passes all its invariants at depth 10. Is that a proof?
Show Answer
Very likely, yes. Every state of such a machine is reachable within a few cycles, so the diameter is far below 10. Make the argument explicit, or confirm it with an induction proof.
Route 2: Induction
Induction proves a property without walking the paths at all. It shows two things:
- Base case: the property holds in the first k cycles after reset. This is an ordinary bounded check.
- Induction step: from any k consecutive states in which the property holds, wherever they are, the next state also satisfies it.
Together these cover every cycle, however far from reset. The step does not care how a state was reached, so a counter of a billion states is no harder than a counter of ten. The induction article explains it in detail.
For the decimal counter of this chapter's example, a mod-10 counter with the rule q <= 9, SymbiYosys in prove mode reports:
SBY [run] engine_0.basecase: ## 0:00:00 Status: passed SBY [run] engine_0.induction: ## 0:00:00 Trying induction in step 1.. SBY [run] engine_0.induction: ## 0:00:00 Trying induction in step 0.. SBY [run] engine_0.induction: ## 0:00:00 Temporal induction successful. SBY [run] summary: successful proof by k-induction. SBY [run] DONE (PASS, rc=0)
That is a proof for every cycle, from a run that took less than a second.
Reporting Results Honestly
A formal report should give every property one of these statuses:
- Proven: holds in every cycle, by induction or another complete method.
- Bounded: holds up to depth k, with k stated. Useful, but not a proof.
- Failed: a real counterexample from reset exists.
- Vacuous or unreachable: passes because its trigger never happens. A finding, not a pass.
Calling a bounded pass "proven" is the most common way formal results are oversold. Chapter 10 returns to reporting.
Quick Check
Q: A report lists 40 assertions as "pass" after runs at depth 20. What is missing?
Show Answer
The status should say "bounded at depth 20", unless each assertion was also proven by induction. The report should also list the covers, to show the assertions are not vacuous.
Running It in ChipVerify Lab
The lab panel runs bounded checks, so every lab result is a bounded pass or a failure. The example below is the mod-10 counter with the rule q <= 9, which passes at any depth. Its formal block also contains, commented out, the induction step written in a form the lab can run. The proofs in practice article explains that form.
Common Mistakes
Mistake #1: Calling a bounded pass a proof
A pass at depth k covers k cycles. Report it as bounded unless the depth exceeds the diameter or an induction proof exists.
Mistake #2: Raising the depth to "get closer" to a proof
For a design with a large state space, no affordable depth comes close to the diameter. Induction is the tool for a proof, not a bigger depth.
Mistake #3: Forgetting that a proof is only as good as its assumptions
Induction proves the property under the assumptions you wrote. An over-constraint makes the proof as hollow as it makes a bounded pass.
Practice Exercise
Challenge: Bounded or Proven?
This is a pencil and paper exercise, with the example for checking. For each case, say whether the result is a proof, a bounded pass, or neither: (1) the mod-10 counter, rule q <= 9, passes at depth 12; (2) the watchdog, rule "tout stays high", passes at depth 100; (3) the mod-10 counter, rule q <= 9, passes in prove mode.
Hint
Compare each depth with the number of cycles the design needs to reach all of its states.
Solution
(1) A proof by complete BMC: the counter reaches all its states within 10 cycles after reset, so depth 12 covers them all. (2) A bounded pass only: the watchdog needs over 1000 cycles to reach its high counts, and in fact it has a bug there. (3) A proof by induction.
Open the ready-made example in the lab and run the formal check from the formal panel. The free tier allows a depth of up to 10 cycles, and PRO allows up to 100.
Summary
- A bounded pass covers the states reachable within the depth and nothing beyond.
- If the depth exceeds the reachability diameter, a bounded check of an invariant is complete, which works for small control blocks.
- Induction proves a property for every cycle with a base case and an induction step, independent of how deep the state space is.
- The mod-10 counter rule
q <= 9was proven by k-induction in under a second. - Report every property as proven, bounded with its depth, failed, or vacuous.
