When the induction step fails from an unreachable state, the property is true but not inductive: it does not say enough about the state for the step to work. The fix is to add helper properties that describe the reachable states more precisely. Each helper is itself proven, so it adds no risk, and together they make the induction go through. This article strengthens the lockstep proof with one helper and shows a general method for finding helpers.
9 min read | Intermediate
What You'll Learn
- Explain what it means for a property to be inductive
- Derive a helper invariant from an induction counterexample
- Complete the lockstep proof with one helper and k = 1
- Use a method for finding helpers in larger designs
Inductive Properties
A set of properties is inductive if, from any state where all of them hold, the next state also satisfies all of them. The lockstep property done_a == done_b is true in every reachable state, but it is not inductive: the state a = 8, b = 0 satisfies it and leads to a state that does not.
Strengthening means adding properties until the set is inductive. The added ones are usually called helper invariants or lemmas. They are proven along with the original property, so they cannot make the proof wrong. A false helper simply fails the base case.
Finding the Helper From the Trace
The induction counterexample of the previous article started with a = 6 and b = 14. Ask: which simple relation holds after reset and is broken here? The answer for two copies of the same counter is obvious: a equals b.
a_agree: assert property (@(posedge clk) disable iff (rst) done_a == done_b);
a_same: assert property (@(posedge clk) disable iff (rst) a == b); // helper
Now the step must start from a state where both hold. With a equal to b, both counters compute the same next value, so they stay equal, and their done outputs agree. The set is inductive with k = 1. In prove mode:
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for basecase SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for induction SBY [run] summary: successful proof by k-induction. SBY [run] DONE (PASS, rc=0)
The helper does more than complete the proof. It states the real design intent, "the two copies are identical", which is stronger and more useful than the original property.
Quick Check
Q: Could a wrong helper, one that is false in some reachable state, make the proof pass incorrectly?
Show Answer
No. Every helper is an assertion, so it is checked in the base case and in the step like the original property. A false helper fails, either as a real counterexample from reset or in the step. Helpers must be assertions, never assumptions.
A Method for Finding Helpers
- Run the proof. If the step fails, read the start state of the induction trace.
- Compare it with what you know about reachable states: which relation between registers holds after reset and is broken in the trace?
- Write that relation as an assertion. Check it with a bounded run first: if it fails from reset, it is wrong.
- Run the proof again with the new assertion. Repeat until the step passes.
Typical helpers relate registers that encode the same information in different ways:
- Two copies of the same value:
a == b. - A count and the pointers of a FIFO:
count == wptr - rptr, with care for the full case. - A state machine and the counter or flags it controls: "in IDLE, the timer is 0".
- A register and its legal range:
q <= 9for a decimal digit. - A valid bit and the data it guards in a pipeline.
The last one is often the cheapest: for the decimal counter, the property q != 11 failed the step from the unreachable value 10, and the range helper q <= 9 rules out 10 to 15 at once.
Quick Check
Q: A FIFO proof fails the step from a state with count = 3 and wptr equal to rptr. What helper would you try?
Show Answer
A relation between the count and the pointers, such as count == wptr - rptr modulo the depth, together with a rule for the full case where the pointers are equal and the count is the full size.
Running It in ChipVerify Lab
In the lab form, the step assumes and asserts the whole set of properties, original and helper:
`ifdef FORMAL
// induction step in the lab: start anywhere, never reset
always @(*) assume (!rst);
reg [7:0] step = 8'd0;
always @(posedge clk) step <= step + 8'd1;
// the properties hold in the first K steps ...
always @(*) if (step < 8'd1) assume (done_a == done_b && a == b);
// ... and must still hold in step K
always @(*) if (step == 8'd1) assert (done_a == done_b && a == b);
`endif
It passes at depth 2. Together with a normal bounded run from reset that asserts both properties, which also passes, this is a full proof that the lockstep copies always agree.
Common Mistakes
Mistake #1: Adding a helper as an assumption
An assumed helper is never checked. If it is wrong, it removes reachable states and the "proof" is worthless. Helpers are assertions.
Mistake #2: Writing helpers that restate the RTL
A helper should describe a relation between state elements, not copy a line of the design. "a equals b" is a fact about the design; "next a is a + 1" is the design.
Mistake #3: Adding many helpers at once
Add one helper at a time and rerun. Otherwise you do not know which one fixed the step, and you keep helpers that are not needed.
Practice Exercise
Challenge: Strengthen the Decimal Counter
Open the example, which runs the lockstep step with the helper and passes. Then write the induction step for the decimal counter from the induction article, with the property q != 4'd11, and strengthen it so the step passes with K = 1.
Hint
The step failed from q = 10. Which helper rules out every value the counter can never take?
Solution
always @(*) if (step < 8'd1) assume (q != 4'd11 && q <= 4'd9);
always @(*) if (step == 8'd1) assert (q != 4'd11 && q <= 4'd9);
With the range helper q <= 9, the step starts only from 0 to 9 and passes. The helper also makes the original property redundant, since a value of at most 9 is never 11. That is common: the helper is often the more useful property.
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 property can be true and still not inductive. The induction step then fails from unreachable states.
- Strengthening adds helper invariants, proven like any assertion, until the set is inductive.
- Find helpers from the induction trace: which relation holds after reset but is broken at the start of the trace?
- The lockstep proof needed one helper,
a == b, and then passed with k = 1. - Helpers are assertions, never assumptions, and they often state the design intent better than the original property.
