Some proofs do not close on budget, and the project still needs an answer. The honest answer is inconclusive, bounded to N, with the evidence that bounds it: the deepest bound run, the covers that show the bound is exercised, and the reason the full proof stays out of reach. That verdict ships; a bounded pass filed as a proof does not. This lesson makes the stopping decision explicit and states what the last resort, a tightening assumption, must carry to be signable.
Effort is budgeted like any engineering resource: a time box per property, a review at each box, and a stopping rule written before the run. When the box expires with the proof still open, the verdict is inconclusive with attachments: the outcome table below names the next action for each case. There are exactly three outcomes, and the last two rows of the table are the third in two forms, with a bound and without one. The FIFO triple beneath is the worked decision, taken at a budget review before anyone has found the helper that the previous topic teaches: induction without the helper stays open to depth 12, the bounded run to 20 is clean, and every cover is reached by depth 8. The control machine has a diameter of 7 transitions, so depth 9 reaches every control state and depth 20 revisits them; the data array is not covered by that argument. The filed verdict is inconclusive, bounded to 20, with data integrity open for want of its helper, and the covers as activity evidence. A tightening assumption is the last resort after that filing, and it must carry four things: the exact statement, the justification for why the excluded behaviour cannot occur, an owner who defends it, and a review that discharges it against the neighbour or the specification.
// 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.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
// ---- data integrity by tracked-slot abstraction (one free slot, one shadow value) ----
// free constant: (* anyconst *) alone is not honoured by the front end, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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; // the tracked slot holds a value we are watching
reg [7:0] td; // the value that should be there
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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
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: bmc 20 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
// ---- data integrity by tracked-slot abstraction (one free slot, one shadow value) ----
// free constant: (* anyconst *) alone is not honoured by the front end, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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; // the tracked slot holds a value we are watching
reg [7:0] td; // the value that should be there
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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
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: cover 8 expect reached slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
// ---- data integrity by tracked-slot abstraction (one free slot, one shadow value) ----
// free constant: (* anyconst *) alone is not honoured by the front end, so the
// value is also assumed equal to its one-cycle-old copy (works in both front ends;
// a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
(* 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; // the tracked slot holds a value we are watching
reg [7:0] td; // the value that should be there
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);
// helper invariant needed for the induction step of a_data
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
// ---- covers: the properties are not vacuous ----
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
endmoduleOutcome | Meaning | Next action |
|---|---|---|
Proven | Base and step pass on the stated model | File with vacuity and mutation evidence |
Counterexample | A concrete trace breaks it | Classify: design bug, missing assumption, artefact |
Inconclusive, bounded to N | Clean to N, open beyond | Justify the bound or strengthen; file N |
Inconclusive, open | No bound and no proof | Reduce, split, budget more, or assume last with review |
No verdict reads proven unless base and step both passed on the filed model and assumptions.
Every bounded verdict prints N with its justification: diameter, recurrence, or induction elsewhere.
Every assumption carries its statement, justification, owner and discharging review; waivers reference proofs, not hopes.
Reconfirm an inconclusive filing by rerunning its three attachments on the final design revision: the bound, the covers and the open proof. If the revision moved any of them, the filing is stale and the decision is remade. A proof result tied to its source revision is the only one signoff reads; the bounded-signoff topic states the full checklist this lesson feeds.
Inconclusive, bounded to 20, with the bound, the covers and the reason induction stays open. Then either budget another round with a named tactic or propose the last-resort assumption with its owner and justification.