A scoreboard models the whole queue inside the proof: 32 memory bits and pointers for this FIFO, hopeless at real sizes. The cheaper answer follows one word: pick a slot freely, remember what was written there, and check the word when the slot is read. Job of this lesson: show the free constant and the tracker, the ordering fault only it finds, and the wrong form that only fits a one-deep buffer.
A free constant is a value the tool picks once and keeps, so it stands for every value at once. The FIFO file declares a free slot tslot, a copy of it one cycle old and an assumption that the two are equal (a clocked stability assumption lags a step and leaks at the last step). A tracker latches the written word into td, raises tv, and clears it on the read. While the followed slot is at the read pointer, rdata must equal td. The tracker adds 2 + 1 + 8 = 11 flip-flops to the 32 memory bits.
The proof is complete at k = 2 with the helper a_tracked (memory slot equals shadow while followed). Without the helper the induction step starts from a state where another word sits in the followed slot and fails.
// 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.
// 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 named in the header, 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: prove 6 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));
// 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 named in the header, 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
endmoduleTwo faults only the tracked item sees. The first is the stuck data bit: one push of a word with bit 7 set, then a read, and a_data fails at step 2 (depth 3); every count property passes. The second reorders after a wrap: the write of slot 3 is redirected into slot 2, so the first three words are right and the order breaks once the write pointer wraps:
// formal: bmc 3 expect fail slang top sync_fifo define BUG=5
`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 named in the header, 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 6 expect fail 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 == 2'd3) ? 2'd2 : 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 named in the header, 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
endmoduleThe reorder fails a_data and a_tracked at step 5 (depth 6); depth 5 passes. Now the wrong form from the sentence "the word read is the word written": comparing rdata with the data written in the previous cycle. It only fits a one-deep buffer and fails on the good FIFO at step 4 (depth 5):
// formal: bmc 8 expect fail 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));
// 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 named in the header, 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);
// the wrong form of "read returns what was written": the previous write, which only fits a one-deep buffer
always @(posedge clk) if (!init && !$past(rst)) a_data_wrong: assert (!($past(pop) && !$past(empty)) || rdata == $past(wdata));
`endif
endmodule// not-run: the failing form, shown in the block above as real code
// a_data_wrong: assert (!($past(pop) && !$past(empty)) || rdata == $past(wdata));
// Right form: compare rdata with the shadow td of the followed slot, never with $past(wdata).The tracked value is free and never driven; the reviewer checks the wire-plus-old-copy idiom.
The shadow is latched from the design's own write data, so the check compares an output with a remembered input.
Data independence is written down: the queue moves words without looking at them. Any control path that reads data breaks the argument.
The helper that ties the shadow to the memory is proved, and a mutant (stuck bit, reorder) fails the property.
Confirm the tracker follows one item: tv rises only on a tracked write and falls only on a tracked read. Plant a stuck bit and a reorder and confirm each fails. If the property fails on the good design, check the free-constant idiom first: an undriven register looks exactly like a design bug.
a_data does. Why?From any state with count in range the next count is in range, so count properties are inductive alone. The induction step for a_data may start with a different word in the followed slot, which only the helper rules out.