It is the week before tape-out review. A proof of no-overflow on a FIFO-like block with a large depth parameter has been running since yesterday: no pass, no counterexample, depth climbing slowly, memory climbing faster. The engineer owns the signoff row for this block and must walk into the review with either a proof or an honest status.
Job of this lesson: show the ordered response: diagnose first, then reduce, split, and strengthen; justify any abstraction; report bounded to N meanwhile; and treat tightening assumptions as the last resort with a written exception.
Trap | What the candidate does | Why it fails |
|---|---|---|
Tighten assumptions until it converges | Adds input rules to shrink the search. | The proof passes on a pruned design; the shipped behaviour was never checked. Assumptions are the last resort and need a written justification. |
Call the bounded run a proof | Reports depth 40 with no failure as proven. | A bounded run alone proves nothing unbounded; the bug may sit one step further out, as the decade-counter wrap bug does at depth 11. |
Raise k until the step passes | Increases the induction length blindly. | A property that is not inductive never closes however large k grows; the repair is an invariant, and the base must cover the same k. |
Non-convergence is diagnosed, not guessed at. First read the numbers: the cone size per property, the depth reached, the state bits, and whether the run is computing or stuck. A cone holding the full memory says the property sees too much; a depth stuck below the wrap length says the bound cannot reach the behaviour; a failing induction step says the property is not inductive. Each reading points at a different repair, in this order: reduce the model, split the obligation, strengthen the proof. Only when all three are exhausted may an assumption be tightened, and then it is filed as a written exception with an owner, not as tuning.
The running design is the 4-entry FIFO: 39 state bits, of which the proof-relevant control is small, and the data-integrity property closes at induction depth 2 only with its helper invariant. Without the helper the base case passes and the step fails for every k up to 12: the step starts in states where the tracked memory word disagrees with the shadow value, states no reset sequence reaches. The unproven run is inconclusive, not a design bug, and one true invariant closes it.
// formal: prove 12 expect unproven slang top sync_fifo define HELPER=0
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule// formal: prove 4 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmoduleThe first run reports base passed and induction failed: undetermined, and the lesson states it as such. The second run differs by one generate flag, the helper asserting that the tracked slot holds the shadow value, and the whole property set closes. Root cause of the non-convergence: the data property is not inductive on its own. Fix: prove the helper as an assertion, never as an assumption.
Parameter reduction is priced, not hoped for. The calculator below sizes a FIFO proof: state bits, steps to fill and steps to wrap, for the small model that converges and the large one that does not. The 39 bits and the fill step 5 are measured on the 4-entry FIFO; the wrap steps are a derived illustration (two laps of the pointers), not a run. The large model is then reported as bounded to its justified depth while the small model carries the inductive proof, bridged by data independence: the FIFO moves words without looking at them.
def fifo_size(entries):
import math
ptr = max(1, math.ceil(math.log2(entries)))
count_bits = math.ceil(math.log2(entries + 1))
state_bits = entries * 8 + 2 * ptr + count_bits
fill_steps = 1 + entries # one reset step plus one push per entry
wrap_steps = 1 + 2 * entries + 1 # derived, not measured: two laps of the pointers, then one check
return state_bits, fill_steps, wrap_steps
small = fifo_size(4)
assert small == (39, 5, 10), small
large = fifo_size(64)
assert large == (531, 65, 130), large
assert 2 ** 531 > 10 ** 150, "large state space must dwarf enumeration"
# The failing variant: the same call with the wrong size gives different figures.
try:
assert fifo_size(3) == small
raise SystemExit("accepted the figures of a 3-entry FIFO for a 4-entry one")
except AssertionError:
pass
print("PASS: 4-entry model is 39 bits filling at step 5; 64-entry is 531 bits filling at step 65")A strong answer opens with the three numbers: cone size, depth reached, state bits, and names what each rules out. It then walks the order without skipping: the small parameter that converges, the invariant that closes the step, the abstraction and its justification, the interim bounded status with its rule, and the written exception if an assumption was touched at all.
Dimension | Strong (3 to 4) | Weak (0 to 2) |
|---|---|---|
Assumption | Every tightened rule filed as an exception with an owner. | Assumptions added silently to converge. |
Mechanism | Unproven step read as non-inductive; helper proved as assertion. | Step failure read as a design bug. |
Trade-off | Small parameter plus abstraction costed against full-depth brute force. | One more k, one more night of runtime. |
Evidence | Passing induction plus bounded-to-N interim with its rule. | A bounded run filed as a proof. |
Nothing about k: a step failing across a range of k values signals a non-inductive property, so add a helper invariant that ties the state elements together and prove it as an assertion.