The second capstone takes the round-robin arbiter from the arbiters article from a list of specification rules to a full proof. It adds what that article left out: covers that show every behavior is reachable, a measured worst-case wait, and a proof of every property for every cycle. Along the way it shows that some designs need no helper invariants at all, only the right induction depth.
10 min read | Intermediate
What You'll Learn
- Assemble the complete property set for an arbiter, with assumptions and covers
- Measure the worst-case wait with a cover and a bound
- Prove safety and fairness for every cycle with k-induction
- Write the sign-off status of the block
The Plan
| ID | Rule | Kind |
|---|---|---|
| A1 | At most one grant per cycle | assert, safety |
| A2 | A grant only goes to a requester that asked in the previous cycle | assert, safety |
| A3 | Every requester is granted within 4 cycles of asking | assert, bounded liveness |
| M1 | A request is held until it is granted | assume |
| C1 | Requester 3 is granted | cover |
| C2 | All four request in the same cycle | cover |
| C3 | A requester waits the full 4 cycles | cover |
The design is the fixed arbiter: the pointer stores the index of the requester that was granted, and the search starts after it.
Milestone 1: Bounded Check and Covers
All assertions pass at depth 10. The covers, as meant-to-fail checks on the lab engine:
- C1 fails at step 2: requester 3 asks in step 1 and is granted in step 2.
- C2 fails at step 1: all four can ask at once.
- C3 fails at step 5: a requester can wait exactly 4 cycles.
C3 matters most. Together with A3 it says that the bound of 4 is tight: it is reached, and never exceeded. Lowering the bound in A3 to 3 makes the assertion fail, which confirms it from the other side.
Quick Check
Q: Why is the cover C3 needed if A3 already passes with a bound of 4?
Show Answer
A3 alone could pass vacuously, for example if an over-constraint prevented any waiting. C3 shows that a 4-cycle wait really happens, so the bound in A3 is exercised at its limit.
Milestone 2: The Proof
In prove mode, k-induction returns UNKNOWN for k = 1 to 4 and PASS from k = 5:
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.
No helper invariants were needed. With k = 5, the step looks at five consecutive good cycles, and that is enough to rule out the unreachable states: wait counters and pointer values that cannot coexist for five cycles without breaking a property. The PDR engine also proves all properties. For the arbiter, the right induction depth was all it took; the FIFO capstone needed helpers. Which case applies depends on how long unreachable states can mimic reachable ones.
Quick Check
Q: Why does a larger k help here, when it did not help for the lockstep counters in Chapter 6?
Show Answer
Here every unreachable start state breaks a property within a few cycles, so five good cycles in a row are only possible from states that behave like reachable ones. The lockstep counters had unreachable states that could stay good forever, by holding still, so no k excluded them.
Milestone 3: Status
| ID | Status | Evidence |
|---|---|---|
| A1, A2, A3 | Proven | k-induction, k = 5; PDR |
| M1 | Assumption | to be proven on each requester |
| C1, C2, C3 | Reached | steps 2, 1 and 5 |
The worst-case wait of 4 cycles is now a proven fact that can go into the specification and into the performance model of the system.
Running It in ChipVerify Lab
The example contains the fixed arbiter with all assertions and the hold assumption, and the three covers as commented meant-to-fail checks. Run it as is, then uncomment the covers one at a time.
Common Mistakes
Mistake #1: Proving fairness without the tight-bound cover
A fairness bound that is never reached may be too loose, or vacuous. Cover the bound itself.
Mistake #2: Reaching for helpers before trying a larger k
For many control blocks a modest induction depth is enough. Try k up to the length of the longest internal sequence before writing helpers.
Mistake #3: Forgetting the assumption in the status
The proof holds under M1. The report must say so, and M1 must be checked on the requesters or in simulation.
Practice Exercise
Challenge: Close the Arbiter
Open the example. Run it, then run each cover. Change the fairness bound to 3 and run again. Finally, put the pointer bug from the arbiters article back (last <= 2'd0 on every grant) and see which milestone catches it.
Hint
The pointer bug turns the arbiter into a fixed-priority one. Which assertion depends on the order of grants?
Solution
All assertions pass; the covers fail at steps 2, 1 and 5. With a bound of 3 the fairness assertion fails at step 5. With the pointer bug, fairness fails at step 6 in the bounded check, before any proof is attempted: milestone 1 catches it. The safety rules still pass, as in the arbiters article.
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
- The arbiter's plan: two safety rules, bounded fairness, a hold assumption, and three covers.
- The covers showed every behavior is reachable, including the 4-cycle worst-case wait.
- k-induction proved all properties from k = 5, with no helper invariants; PDR proved them too.
- The worst-case wait of 4 cycles is a proven property of the block.
