A formal tool is a perfect adversary. It drives every input of your block in every possible way, including ways that the rest of the chip never would. Some of the failures it reports are real bugs, and some are inputs that cannot happen. This chapter is about telling the two apart: describing the environment with assumptions, starting from reset, and making sure the assumptions do not hide the bugs you are looking for.
When a formal check fails, the first question is not "where is the bug?" but "can this input really happen?". A block is designed for the neighbors it has, and it may rely on promises they make: a select signal that is always one-hot, a response that only follows a request. This article shows why the tool ignores those promises until you write them down, and how an assumption does that.
8 min read | Beginner to Intermediate
What You'll Learn
- Explain why a formal tool explores inputs that the real system never produces
- Decide whether a counterexample shows a bug or an impossible input
- Write an assumption that describes a promise of the environment
- Choose the weakest assumption that makes a correct design pass
The Tool Knows Nothing About the Neighbors
In simulation, a testbench drives the inputs, and it usually drives them the way the real neighbors would. A formal tool has no testbench. Every input of the top module is free: in every cycle the tool may give it any value. That is the source of its power, because it tries the strange input sequences that nobody thought of. It is also the source of false failures, because some of those sequences are impossible in the real chip.
The tool cannot know which sequences are impossible. That knowledge lives in the specification of the neighbor blocks, and you have to write it down as assumptions.
The Design: an AND-OR Multiplexer
A common way to build a fast multiplexer is to AND each input with its select bit and OR the results. It is smaller than a chain of priority logic, and it is correct as long as exactly one select bit is high:
module onehot_mux (input [3:0] sel, input [7:0] d0, input [7:0] d1, input [7:0] d2, input [7:0] d3,
output [7:0] y);
assign y = ({8{sel[0]}} & d0) | ({8{sel[1]}} & d1) | ({8{sel[2]}} & d2) | ({8{sel[3]}} & d3);
endmodule
The block that drives sel comes from a one-hot state machine, so sel always has exactly one bit set. The rule for the multiplexer: the output is the selected input.
always_comb begin
if (sel[0]) a_y0: assert (y == d0);
if (sel[1]) a_y1: assert (y == d1);
if (sel[2]) a_y2: assert (y == d2);
if (sel[3]) a_y3: assert (y == d3);
end
The First Run: a False Failure
Without any assumption, the run fails in the first step:
The tool chose sel = 1001: two inputs selected at once. The output is the OR of d0 and d3, which is not d0. The counterexample is correct as a statement about the logic. But sel = 1001 cannot happen, because its driver is one-hot. The design is fine, the check is missing a fact about the environment.
Quick Check
Q: A counterexample relies on an input value that the neighbor block can never produce. Is it a bug?
Show Answer
Not in the design under check. It shows that the check is missing an assumption about the neighbor. Before adding the assumption, confirm from the specification of the neighbor that the input really is impossible.
Adding the Assumption
An assumption tells the tool to consider only inputs that satisfy it. For the multiplexer:
m_sel: assume property (@(posedge clk) $onehot(sel));
The multiplexer itself has no clock, so in a purely combinational check the immediate form inside always_comb is used, assume ($onehot(sel));. With the assumption, the run passes: for every one-hot select and every data value, the output is the selected input.
Bug or Impossible Input?
Every counterexample needs this decision, and getting it wrong is costly either way. Treat a real bug as an impossible input and you hide it with an assumption. Treat an impossible input as a bug and you change a correct design. Some questions that help:
- Which input values or sequences does the counterexample rely on?
- Does the specification of the neighbor rule them out, in writing?
- Is the neighbor checked to keep that promise, by its own assertion or by a simulation check?
- Could a later version of the chip use the block with a different neighbor?
If the promise is written in the specification and the neighbor keeps it, add the assumption. If not, the block should probably handle the input, and the counterexample is a bug. For the multiplexer, a designer who cannot rely on one-hot selects would use a priority multiplexer instead.
Keep Assumptions Weak
An assumption should say exactly what the neighbor promises and nothing more. A stronger assumption removes more input sequences, and every sequence it removes is one the tool no longer checks. For the multiplexer, even $onehot0(sel), which also allows "nothing selected", is enough for the check to pass. If the driver can really be idle with no select bit set, that weaker assumption is the right one, because it keeps the idle case in the search.
The over-constraining article shows what happens when an assumption is too strong.
Quick Check
Q: Both $onehot(sel) and $onehot0(sel) make the multiplexer check pass. Which one checks more?
Show Answer
$onehot0(sel). It allows every input that $onehot allows, plus the all-zero select. A weaker assumption leaves more input sequences in the search.
Running It in ChipVerify Lab
The lab reads immediate assume and assert statements and $onehot:
`ifdef FORMAL
// the block that drives sel always selects exactly one input
always @(*) assume ($onehot(sel));
// the output is the selected input
always @(*) if (sel[0]) assert (y == d0);
always @(*) if (sel[1]) assert (y == d1);
always @(*) if (sel[2]) assert (y == d2);
always @(*) if (sel[3]) assert (y == d3);
`endif
Run the example as it is and it passes. Comment out the assume line and run again to see the false failure.
Common Mistakes
Mistake #1: Adding an assumption to make a failure go away
An assumption must come from the specification of the environment, not from the counterexample. If you cannot point to the sentence that promises it, the counterexample may be a real bug.
Mistake #2: Assuming more than the neighbor promises
Every extra restriction removes inputs from the search. Assume exactly what is promised, as weakly as possible.
Mistake #3: Constraining outputs of the design
Assumptions describe inputs coming from the environment. An assumption on an output or an internal signal of the design forces the design to behave and hides its bugs. If a rule is about the design, it is an assertion.
Practice Exercise
Challenge: How Weak Can It Be?
Open the example, remove the assumption, and run to see the false failure. Then try these assumptions one at a time and predict the result before each run: $onehot0(sel), and $countones(sel) <= 2.
Hint
The AND-OR multiplexer is wrong only when two or more select bits are high.
Solution
$onehot0(sel) passes: with no select bit set, none of the assertions is triggered, and with one bit set the output is correct. $countones(sel) <= 2 fails in step 0, because it still allows two select bits at once. The weakest assumption that works is "at most one select bit", which is exactly the property the AND-OR structure needs.
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
- Every input of the design under check is free in formal: the tool tries values the real neighbors never produce.
- A counterexample that relies on an impossible input shows a missing assumption, not a design bug.
- An assumption describes a promise of the environment and must come from its specification.
- Assume as little as possible:
$onehot0(sel)was enough for the multiplexer, and checks more than$onehot(sel). - Never assume anything about the outputs or internal signals of the design under check.
