The last chapter is practice. Each project uses the method of the whole tutorial on a complete design: write the properties from a short specification, run, read the counterexamples, fix, and prove what can be proven. Start with the bug hunt, then work through the three capstones, and finish with the checklist and the interview questions.
Five small designs, five specifications, five bugs. Each bug can be found with a single well-chosen property. The designs come without properties: your job is to read the specification, write the one property that captures it, and let the formal tool find the bug. The solutions give one property per design, verified on the lab engine, and the step at which it fails.
10 min read | Intermediate
What You'll Learn
- Turn a one-sentence specification into a property
- Choose between an invariant, a $past rule and a sequence for each case
- Read five short counterexamples and fix the RTL
- Check that each fixed design passes
How to Work
Open the example: it contains five files, one per design, each with an empty `ifdef FORMAL block that already has the reset assumption. For each design:
- Set the top module in the formal panel.
- Write one assertion in place of the comment, from the specification below.
- Run at depth 10. Read the counterexample, find the bug, fix it, and run again.
Write each property in the lab form, using $past, $countones and the other functions from Chapter 3. The key line of each design is shown below; the bug is in it, but it is the property that must prove it.
Design 1: Gray Counter
Specification: a 4-bit counter whose output gray is Gray-coded: consecutive output values differ in exactly one bit.
assign gray = bin ^ (bin << 1);
Quick Check
Q: Which function makes "differ in exactly one bit" a one-line property?
Show Answer
$countones(gray ^ $past(gray)) == 1: the XOR of two values has a 1 in every bit that differs, and $countones counts them. Apply it only when the value changed.
Design 2: Byte With Parity
Specification: the block registers a byte q together with a parity bit p so that the nine bits always have even parity.
else begin q <= d; p <= ^d[6:0]; end
Design 3: Rising Edge Detector
Specification: rise is high for exactly the cycles in which in is high and was low in the previous cycle.
assign rise = in ^ in_d;
Design 4: Saturating Up/Down Counter
Specification: the counter counts up on up and down on dn, and stays at 15 and at 0 instead of wrapping.
else if (up && !dn && q != 4'd15) q <= q + 4'd1;
else if (dn && !up) q <= q - 4'd1;
Design 5: One-Shot
Specification: each rising edge of trig produces exactly one one-cycle pulse, even if trig stays high.
trig_d <= trig;
pulse <= trig;
Quick Check
Q: For the one-shot, which single property catches a pulse that is too long, without saying anything about trig?
Show Answer
"The pulse is never high in two consecutive cycles": !(pulse && $past(pulse)). It follows from "one-cycle pulse" alone.
Running It in ChipVerify Lab
All five designs are in one example. Their files are independent; the top module you select decides which one is checked.
Common Mistakes
Mistake #1: Copying the RTL into the property
rise == (in ^ $past(in)) passes on the buggy edge detector. Write the specification, not the code.
Mistake #2: Forgetting the reset guards on $past
Each property that looks back needs !init and usually !$past(rst), or it fails in the first cycles for no reason.
Practice Exercise
Challenge: Five Bugs, Five Properties
Work through all five designs. For each, write one property, find the bug, fix it, and run again.
Hint
Designs 1 and 5 need $past on the output, design 2 needs only the current values, designs 3 and 4 need $past on the inputs or the count.
Solution
// 1. Gray counter: fails at step 3. Fix: bin ^ (bin >> 1)
always @(posedge clk) if (!init && !$past(rst) && gray != $past(gray)) assert ($countones(gray ^ $past(gray)) == 1);
// 2. Parity: fails at step 2. Fix: p <= ^d
always @(*) if (!init) assert (^{q, p} == 1'b0);
// 3. Edge detector: fails at step 3. Fix: rise = in & ~in_d
always @(posedge clk) if (!init && !$past(rst)) assert (rise == (in && !$past(in)));
// 4. Up/down counter: fails at step 3. Fix: else if (dn && !up && q != 4'd0)
always @(posedge clk) if (!init && !$past(rst) && $past(q) == 4'd0 && $past(dn && !up)) assert (q == 4'd0);
// 5. One-shot: fails at step 4. Fix: pulse <= trig && !trig_d
always @(posedge clk) if (!init && !$past(rst)) assert (!(pulse && $past(pulse)));
All five fixed designs pass at depth 10. In SVA, design 3 is assert property (@(posedge clk) disable iff (rst) rise == $rose(in));, and design 5 is assert property (@(posedge clk) disable iff (rst) pulse |=> !pulse);.
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
- Each of the five bugs was found by one property written from a one-sentence specification.
- Invariants (parity),
$pastrules (edge, saturation, one-shot) and bit counting (Gray code) cover most small blocks. - All five counterexamples appeared within 4 steps; small blocks rarely need deep checks.
- Write the specification, not the RTL, and guard every look back.
