Checklists describe; packages convince. This lesson fills every checklist line for the FIFO with real runs: the full property set proven, every trigger covered, an assumption register, three mutants killed, the overflow mutant caught only at depth 7, and a ledger gate that fails when any item is removed. The depths and steps are the ones the runs below produce.
One module text, five runs. The text is the FIFO with its property set plus a small wrapper that adds the antecedent covers of the push, pop and overflow checks. The full proof closes at k equal to 2, and k equal to 1 leaves the induction step open. All covers are reached within depth 6. The overflow mutant passes at depth 6 and fails at depth 7. Each result is quoted for the same text, so a reviewer replaying the package compares like with like.
Run 1 proves every assertion of the FIFO, including the data check with its helper. The proof header asks for a bound of 2 and an induction step of 2.
// formal: prove 2 expect pass slang top sync_fifo_signoff
`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));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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
module sync_fifo_signoff #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop
);
wire [7:0] rdata;
wire full, empty;
wire [2:0] count;
sync_fifo #(.BUG(BUG), .HELPER(HELPER)) dut (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(pop), .rdata(rdata), .full(full), .empty(empty), .count(count));
`ifdef FORMAL
reg winit = 1'b1;
always @(posedge clk) winit <= 1'b0;
// antecedent covers: push alone, pop alone, push into a full FIFO (push and pop together is c_both)
always @(*) if (!winit) begin
c_push_only: cover (push && !pop && !full);
c_pop_only: cover (pop && !push && !empty);
c_push_full: cover (push && !pop && full);
end
`endif
endmoduleRun 2 is the failing partner of the bound: with k equal to 1 the base case passes and the induction step does not, because four of the properties read one cycle back. The result is unproven, not a pass.
// formal: prove 1 expect unproven slang top sync_fifo_signoff
`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));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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
module sync_fifo_signoff #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop
);
wire [7:0] rdata;
wire full, empty;
wire [2:0] count;
sync_fifo #(.BUG(BUG), .HELPER(HELPER)) dut (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(pop), .rdata(rdata), .full(full), .empty(empty), .count(count));
`ifdef FORMAL
reg winit = 1'b1;
always @(posedge clk) winit <= 1'b0;
// antecedent covers: push alone, pop alone, push into a full FIFO (push and pop together is c_both)
always @(*) if (!winit) begin
c_push_only: cover (push && !pop && !full);
c_pop_only: cover (pop && !push && !empty);
c_push_full: cover (push && !pop && full);
end
`endif
endmoduleRun 3 reaches every cover of the module: six in all: the three original ones (full, empty after use, joint push and pop) and the three antecedent covers of the wrapper. Depth 6 is the smallest depth at which all are reached, because the full state is first reached at step 5.
// formal: cover 6 expect reached slang top sync_fifo_signoff
`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));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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
module sync_fifo_signoff #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop
);
wire [7:0] rdata;
wire full, empty;
wire [2:0] count;
sync_fifo #(.BUG(BUG), .HELPER(HELPER)) dut (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(pop), .rdata(rdata), .full(full), .empty(empty), .count(count));
`ifdef FORMAL
reg winit = 1'b1;
always @(posedge clk) winit <= 1'b0;
// antecedent covers: push alone, pop alone, push into a full FIFO (push and pop together is c_both)
always @(*) if (!winit) begin
c_push_only: cover (push && !pop && !full);
c_pop_only: cover (pop && !push && !empty);
c_push_full: cover (push && !pop && full);
end
`endif
endmoduleRuns 4 and 5 are the mutant that needs the full depth: a missing full check. Bounded to 6 the proof set sees nothing; bounded to 7 it fails.
// formal: bmc 6 expect pass slang top sync_fifo_signoff define BUG=1
`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));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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
module sync_fifo_signoff #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop
);
wire [7:0] rdata;
wire full, empty;
wire [2:0] count;
sync_fifo #(.BUG(BUG), .HELPER(HELPER)) dut (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(pop), .rdata(rdata), .full(full), .empty(empty), .count(count));
`ifdef FORMAL
reg winit = 1'b1;
always @(posedge clk) winit <= 1'b0;
// antecedent covers: push alone, pop alone, push into a full FIFO (push and pop together is c_both)
always @(*) if (!winit) begin
c_push_only: cover (push && !pop && !full);
c_pop_only: cover (pop && !push && !empty);
c_push_full: cover (push && !pop && full);
end
`endif
endmodule// formal: bmc 7 expect fail slang top sync_fifo_signoff define BUG=1
`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));
// helper invariant: occupancy equals pointer distance (mod 4) unless full
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 the proof header selects, so the
// value is also assumed equal to its one-cycle-old copy (works with either front end;
// 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
module sync_fifo_signoff #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop
);
wire [7:0] rdata;
wire full, empty;
wire [2:0] count;
sync_fifo #(.BUG(BUG), .HELPER(HELPER)) dut (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
.pop(pop), .rdata(rdata), .full(full), .empty(empty), .count(count));
`ifdef FORMAL
reg winit = 1'b1;
always @(posedge clk) winit <= 1'b0;
// antecedent covers: push alone, pop alone, push into a full FIFO (push and pop together is c_both)
always @(*) if (!winit) begin
c_push_only: cover (push && !pop && !full);
c_pop_only: cover (pop && !push && !empty);
c_push_full: cover (push && !pop && full);
end
`endif
endmoduleProperty group | Run | Result quoted | Trigger cover |
|---|---|---|---|
Range, flags, exclusivity, pointer consistency (four checks) | Run 1, k equal to 2 | Proven for this model under these assumptions. | None needed: no antecedent. |
Push, pop, ignored overflow, joint push and pop (four checks) | Run 1, k equal to 2 | Proven for this model under these assumptions. | c_push_only, c_pop_only, c_push_full, c_both: all reached in run 3. |
Data integrity by tracked slot, with its helper (two checks) | Run 1, k equal to 2 | Proven; the helper is proven in the same run. | c_empty_after_use reached in run 3. |
Covers (six) | Run 3, depth 6 | Reached. Not labelled proven: a cover is reached, not proven. | Witnesses read. |
Assumption | Rule it models | Discharge |
|---|---|---|
Reset is asserted at step 0 | Power-up is followed by a reset before the FIFO is used. | Reset sequencing is checked at integration; without it the proof would start from an arbitrary state, where the good design fails its range check. |
The tracked slot is one fixed slot | The data check follows the same slot at every step. | A proof device, not an environment rule: justified by data independence, because the FIFO moves words without looking at them. |
None on push, pop or write data | The inputs are free. | Nothing to discharge: no environment rule was assumed. |
Mutant | Fault | Killed by | Evidence |
|---|---|---|---|
BUG 1 | Push accepted when full. | Range check, at depth 7. | Runs 4 and 5 above. |
BUG 2 | Pop accepted when empty. | Range check, at depth 3. | The run in the mutation lesson. |
BUG 5 | Write data bit 7 stuck at 0. | Data check, at depth 3. | The run in the mutation lesson. |
Mutation score: 3 of 3 killed, for this declared mutant set. The other two planted faults are not run in this lesson; a real package would use a larger set. The bound for the overflow mutant is justified by the sum from the bound lessons: reset 1, five pushes (four fill the FIFO and the fifth overflows), latency 0, plus 1 gives 7, and runs 4 and 5 show 7 is the edge, not a round number.
The script assembles the package ledger. A property is proven, a cover is reached, a mutant is killed: three vocabularies for three kinds of row, and a cover labelled proven is rejected. It fails the package six ways before the clean ledger passes.
# the FIFO package gate: completeness over the assembled ledger
ALLOWED = {"property": ("proven", "counterexample", "inconclusive"),
"cover": ("reached", "inconclusive", "unreachable"), "mutant": ("killed", "survived")}
GOOD = {"property": "proven", "cover": "reached", "mutant": "killed"}
PROPS = ["a_range", "a_flags", "a_not_both", "a_ptr", "a_push_inc", "a_pop_dec",
"a_ovf_ign", "a_both", "a_data", "a_tracked"]
COVERS = ["c_full", "c_both", "c_empty_after_use", "c_push_only", "c_pop_only", "c_push_full"]
MUTANTS = ["BUG1", "BUG2", "BUG5"]
TRIGGER = {"a_push_inc": "c_push_only", "a_pop_dec": "c_pop_only",
"a_ovf_ign": "c_push_full", "a_both": "c_both"}
DERIVED = 1 + 5 + 0 + 1 # reset + five pushes + latency + 1
def package(h):
rows = [{"kind": "property", "id": i, "status": "proven", "hash": h} for i in PROPS]
rows += [{"kind": "cover", "id": i, "status": "reached", "hash": h} for i in COVERS]
return rows + [{"kind": "mutant", "id": i, "status": "killed", "hash": h} for i in MUTANTS]
def gate(rows, register, current, depth_run):
faults, have = [], {(r["kind"], r["id"]) for r in rows}
for kind, ids in (("property", PROPS), ("cover", COVERS), ("mutant", MUTANTS)):
faults += ["missing " + kind + ": " + i for i in ids if (kind, i) not in have]
faults += [p + ": trigger cover " + c + " absent" for p, c in TRIGGER.items() if ("cover", c) not in have]
for r in rows:
if r["status"] not in ALLOWED[r["kind"]]:
faults.append(r["id"] + ": " + r["status"] + " is not a status for a " + r["kind"])
elif r["status"] != GOOD[r["kind"]]:
faults.append(r["id"] + ": " + r["status"])
if r["hash"] != current:
faults.append(r["id"] + ": stale")
faults += ["assumption " + a["id"] + ": no discharge" for a in register if not a["discharge"]]
return faults + (["bound below derived minimum 7"] if depth_run < DERIVED else [])
reg = [{"id": "rst-step-0", "discharge": "reset sequencing at integration"},
{"id": "tslot-const", "discharge": "data independence of the FIFO"}]
ok = package("a41f")
assert gate(ok, reg, "a41f", 7) == []
assert gate([r for r in ok if r["id"] != "c_push_full"], reg, "a41f", 7) == [
"missing cover: c_push_full", "a_ovf_ign: trigger cover c_push_full absent"]
assert gate([dict(r, status="proven") if r["id"] == "c_full" else r for r in ok], reg, "a41f", 7) == [
"c_full: proven is not a status for a cover"]
assert gate([dict(r, status="survived") if r["id"] == "BUG5" else r for r in ok], reg, "a41f", 7) == ["BUG5: survived"]
assert gate(ok, [reg[0], dict(reg[1], discharge="")], "a41f", 7) == ["assumption tslot-const: no discharge"]
assert gate(ok, reg, "a41f", 6) == ["bound below derived minimum 7"]
assert gate(ok, reg, "b002", 7) == [r["id"] + ": stale" for r in ok]
print("PASS: full package ships; each removed or mislabelled item fails with its own message")Every checklist line resolves to a run or a script result above, with the bound and the step stated.
Every trigger has its antecedent cover in the same text as the proof; the covers are reached, never called proven.
The mutant row is present and load-bearing: depth 7 is defended by the sum and by the pass at 6 and fail at 7.
Removing any row fails the gate; the package is complete by construction, not by inspection.
Replay the package on a clean checkout: fresh sources, hash recomputed, all five runs giving their expected result, gate passing. Then mutate one line of the FIFO and confirm exactly one gate row changes meaning: a proof fails or a new survivor appears. A package where a source change breaks nothing is either perfectly robust or not connected to the sources; the hash check distinguishes the two.
Not signed off. The gate compares against the current hash, so a uniform mismatch fails every row as stale. Update the sources or rerun; never edit the hashes by hand.