A formal tool answers "is there any input sequence that breaks this rule?" without trying the sequences one by one. This article shows how. It explains bounded model checking, the method used by ChipVerify Lab, by building it up in steps: copy the design once for every clock cycle, connect the copies through the registers, and hand the whole thing to a solver. No mathematics is needed to follow it.
9 min read | Beginner to Intermediate
What You'll Learn
- Explain how a design is unrolled into one copy per clock cycle
- Describe the question that the solver answers
- Read the progress messages of a SymbiYosys run
- Explain what the depth of a bounded check means, and why a bug can hide beyond it
From a Design to a Puzzle
The article about state and reachability described a design as a loop: the next state is a function of the current state and the inputs. A formal tool turns that loop into a puzzle that a solver can work on. The trick is to stop thinking of time as a loop and to write it out, cycle after cycle.
Unrolling in Time
Take the logic of the design, the part between the registers. Make one copy of it for clock cycle 0, one for cycle 1, one for cycle 2, and so on, up to some cycle k. Connect them: the register outputs of one copy are the register inputs of the next. The inputs of each copy are left free, which means the solver may give them any value. The properties are attached to every copy:
The result is one large piece of combinational logic. It has no clock and no time any more, just inputs on the left and assertion outputs at every step. This is called unrolling the design, and each copy is often called a step or a frame.
The Question for the Solver
Now the formal tool asks the solver a single question about that large piece of logic:
Is there any value for all the free inputs, in steps 0 to k, such that some assertion is false in some step?
A solver is a program that answers questions of this kind. The common ones are SAT solvers, which work on single bits, and SMT solvers, which also understand words and arithmetic, such as a 32-bit comparison. Bitwuzla, boolector and z3, the solvers in ChipVerify Lab, are SMT solvers. They are very good at this: they do not try the input values one by one, but use reasoning rules to rule out whole groups of values at once.
There are two possible answers:
- Yes, here is one. The values that the solver chose are the counterexample. The tool turns them into a waveform.
- No, there is none. No sequence of inputs of that length can break an assertion. The property passes up to that depth.
This method is called bounded model checking, BMC. The word bounded refers to the k: the check covers every input sequence of up to k + 1 cycles, but says nothing about longer ones.
Quick Check
Q: In the unrolled design, why does a register not need a clock any more?
Show Answer
Each clock edge has become a connection between two copies of the logic. The value that a register would store on the edge is simply passed from one copy to the next, so time is represented by the chain of copies.
Watching It Happen
SymbiYosys prints its progress step by step. This is the start of the run of the correct 0-to-5 counter from the first article, on the lab engine with the bitwuzla solver and a depth of 10:
engine_0: ## 0:00:00 Solver: bitwuzla engine_0: ## 0:00:00 Checking assumptions in step 0.. engine_0: ## 0:00:00 Checking assertions in step 0.. engine_0: ## 0:00:00 Checking assumptions in step 1.. engine_0: ## 0:00:00 Checking assertions in step 1.. ... engine_0: ## 0:00:00 Checking assertions in step 9.. engine_0: ## 0:00:00 Status: passed DONE (PASS, rc=0)
The tool adds one step at a time. For each step it checks that the assumptions can be met, and then asks the solver whether an assertion can fail in that step. With a depth of 10 it checks steps 0 to 9, and the counter passes.
For the counter with the wrong wrap value, the same run stops early:
engine_0: ## 0:00:00 BMC failed! engine_0: ## 0:00:00 Assert failed in mod6: mod6_bug.sv:9.36-9.54 engine_0: ## 0:00:00 Writing trace to VCD file: engine_0/trace.vcd summary: failed assertion mod6._witness_.check_assert_mod6_bug_sv_9_10 at mod6_bug.sv:9.36-9.54 step 8 DONE (FAIL, rc=2)
The tool names the assertion by its file and line, says in which step it failed, and writes the counterexample as a VCD file. That file is the waveform that the lab displays.
The Depth Matters
The depth is how many steps the tool unrolls. It is a limit on how far in time the search looks. The buggy counter shows it clearly. Its bad value appears after a reset and six counts, and the tool reports the failure at step 8. On the lab engine:
| Depth | Steps checked | Result |
|---|---|---|
| 8 | 0 to 7 | PASS, the bug is too far away |
| 9 | 0 to 8 | FAIL, counterexample at step 8 |
A pass at depth 8 does not mean the counter is correct. It means no failure exists in the first 8 steps. A bug that needs more cycles to appear stays hidden. A counter that counts to 1,000 before it goes wrong needs a depth of more than 1,000. That is why the depth must be chosen with the design in mind, and why there are methods that prove a property for every length. Chapter 5 and Chapter 6 cover both.
Quick Check
Q: A BMC run with a depth of 20 passes. A bug in the design needs 35 cycles after reset to appear. Will the run find it?
Show Answer
No. The run only looks at the first 20 steps, so the bug is beyond its reach. It needs a depth larger than 35, or a full proof method.
Why the Work Grows With the Depth
Every extra step adds another copy of the design for the solver to reason about. A deeper check is therefore a bigger puzzle, and it takes longer. The growth is not always gentle: a design with wide arithmetic or many registers can become slow after a few dozen steps. This is one reason why the free tier of the lab allows 10 steps and PRO allows 100, and why formal works best on blocks of moderate size.
Running It in ChipVerify Lab
In the lab, the depth is set with the slider of the formal panel, and the solver with the engine selector. The progress messages above are what the lab log shows during a run. The example of this article is the buggy counter of the first article, so you can try the depth yourself.
Common Mistakes
Mistake #1: Reading a bounded pass as a proof
A pass from BMC holds only up to the depth. Always know how many cycles your design needs to reach its interesting states, and choose the depth accordingly.
Mistake #2: Setting the depth as high as possible by default
A very deep run can be slow or time out, and it does not help if the bug lies within a few cycles. Start with a small depth, look at the result, and increase it with a reason.
Practice Exercise
Challenge: Find the Smallest Depth
Open the buggy counter in ChipVerify Lab. Run the formal check with a depth of 5, then 8, then 9, then 10. Note which runs fail. What is the smallest depth that finds the bug, and why that number?
Hint
Count the cycles the counterexample needs: one for the reset, then the counts from 0 up to the bad value, then the check of that value at the next clock edge.
Solution
Depths 5 and 8 pass, and depths 9 and 10 fail with the failure at step 8. The smallest depth is 9, because the tool must check step 8, and a depth of 9 covers steps 0 to 8. The counter needs a reset step and six counts before it holds 6, and the assertion sees that value at the following clock edge.
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
- Bounded model checking unrolls the design: one copy of the logic for each clock cycle, connected through the registers.
- The inputs of every step are free. The solver searches for values that make an assertion false in some step.
- If it finds them, they are the counterexample. If not, the property holds for every input sequence up to the depth.
- SymbiYosys checks one step after the other and reports the step of a failure. The buggy counter fails at step 8, so it needs a depth of at least 9.
- A bounded pass is not a proof for longer runs, and a deeper check costs more time.
