A FIFO proof at two entries passed and the shipped, larger FIFO failed: its pointers were one bit wide. Small sizes hide index-width and wrap faults, and a bounded run needs more steps as the size grows. Job of this lesson: four sweeps, each with its fault: the depth a bounded run needs, a pointer-width fault, a non-power-of-two size, and a mode that only a cover reveals; then the symmetry argument and the fault that breaks it.
Two numbers are easy to confuse. The parameter is the design's own size; the depth is the proof's bound. A bounded run to depth D sees faults that need D steps, so a larger FIFO needs a larger depth: the sweep below measures it. Sizes are chosen to differ in what could go wrong: a power of two and not, one and more than one pointer bit, every mode that changes behaviour.
An occupancy model (count only) with the fault "push accepted when full" fails the range check. The first failing depth for N entries is N + 3: a reset step, N pushes to fill, one attempt and one step to see the count. The script below finds these depths by breadth-first search for every size in the table, and the runs confirm three of them, N = 2, 4 and 16, each with one depth less passing:
N | 2 | 3 | 4 | 5 | 8 | 16 |
|---|---|---|---|---|---|---|
First failing depth | 5 | 6 | 7 | 8 | 11 | 19 |
// formal: bmc 4 expect pass slang top pf define BUG=1 define N=2
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmodule// formal: bmc 5 expect fail slang top pf define BUG=1 define N=2
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmodule// formal: bmc 6 expect pass slang top pf define BUG=1 define N=4
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmodule// formal: bmc 7 expect fail slang top pf define BUG=1 define N=4
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmodule// formal: bmc 18 expect pass slang top pf define BUG=1 define N=16
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmodule// formal: bmc 19 expect fail slang top pf define BUG=1 define N=16
`define FORMAL
module pf #(parameter N = 4, parameter BUG = 0) (input wire clk, input wire rst, input wire push, input wire pop, output reg [7:0] count);
wire full = (count == N);
wire empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) if (rst) count <= 0; else count <= count + do_push - do_pop;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= N);
`endif
endmoduleCounting "reset, sixteen pushes, one more" gives 18 steps, numbered 0 to 17. The bad count is visible one step later, at step 18, so the run needs depth 19.
from collections import deque
# Breadth-first search of the occupancy machine with the fault "a push is accepted when full".
measured = {2: 5, 3: 6, 4: 7, 5: 8, 8: 11, 16: 19} # the table; the runs above confirm N = 2, 4 and 16
def first_fail_depth(n):
seen, q = {0}, deque([(0, 1)]) # occupancy 0 at step 1 (step 0 is the reset step)
while q:
c, step = q.popleft()
if c > n:
return step + 1 # the bad count exists at this step; the run needs one more depth
for push, pop in ((0, 0), (1, 0), (0, 1), (1, 1)):
nxt = c + push - (1 if pop and c > 0 else 0) # the fault: the push is not blocked by a full FIFO
if nxt not in seen:
seen.add(nxt)
q.append((nxt, step + 1))
return None
assert all(first_fail_depth(n) == d for n, d in measured.items())
assert all(d == n + 3 for n, d in measured.items())
assert measured[16] == (1 + 16 + 1) + 1 # 18 steps up to the attempt (0 to 17), plus the step that shows it
assert first_fail_depth(16) != 2 * 16 + 3 # twice the size is not the bound for this fault
print("PASS: first failing depth is N + 3 for N = 2, 3, 4, 5, 8, 16 (19 for sixteen entries)")A lesson-local FIFO control model keeps pointers and occupancy in an N-entry FIFO and checks that the write pointer equals the read pointer plus the occupancy, modulo N. Three faults, each present only at some sizes or modes:
Fault | Passes at | Fails at |
|---|---|---|
Pointers one bit wide | N = 2, depth 8 and induction | N = 3, step 3 |
Pointers wrap by overflow | N = 4 (power of two) | N = 5, step 6 |
Overwrite mode: read pointer not moved | Drop mode, any size | Overwrite mode, step 6 |
// formal: prove 8 expect pass slang top pfw define N=2 define BUG=1
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: bmc 4 expect fail slang top pfw define N=3 define BUG=1
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: bmc 8 expect pass slang top pfw define N=4 define BUG=2
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: bmc 7 expect fail slang top pfw define N=5 define BUG=2
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: prove 6 expect pass slang top pfw define N=4 define BUG=3
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: bmc 7 expect fail slang top pfw define N=4 define MODE=1 define BUG=3
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmoduleThe third pair is the mode trap: the default mode proves while the overwrite mode, which the default proof never enters, fails (depth 6 passes). The covers settle which mode a run exercised: the overwrite cover is not reached in the default mode, by construction, and reached in the overwrite mode:
// formal: cover 8 expect fail slang top pfw define N=4 define MODE=0
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmodule// formal: cover 8 expect reached slang top pfw define N=4 define MODE=1
`define FORMAL
// pfw: the control of an N-entry FIFO (pointers and occupancy, no data). MODE 0 drops a push into a full FIFO,
// MODE 1 lets it overwrite the oldest word. BUG: 1 pointers are one bit wide whatever N is, 2 pointers wrap by
// natural overflow (right only when N is a power of two), 3 in MODE 1 the overwrite does not move the read pointer.
module pfw #(parameter N = 4, parameter MODE = 0, parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire pop
);
localparam PW = (BUG == 1) ? 1 : $clog2(N);
reg [PW-1:0] wptr, rptr;
reg [7:0] count;
wire full = (count == N);
wire empty = (count == 0);
wire ovr = (MODE == 1) && push && full; // push into a full FIFO that overwrites the oldest word
wire do_push = push && (!full || ovr);
wire do_pop = (pop && !empty) || ovr;
function [PW-1:0] nxt(input [PW-1:0] p);
nxt = (BUG == 2) ? (p + 1'b1) : ((p == N - 1) ? {PW{1'b0}} : (p + 1'b1));
endfunction
always @(posedge clk) begin
if (rst) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (do_push) wptr <= nxt(wptr);
if (do_pop && !(BUG == 3 && ovr)) rptr <= nxt(rptr);
count <= count + do_push - 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 <= N);
a_ptr: assert ((rptr + count) % N == wptr); // write pointer = read pointer + occupancy, modulo N
// helper for the induction step: a pointer never leaves 0 to N-1 (trivial when N is a power of two)
if (HELPER) h_ptr_range: assert (wptr < N && rptr < N);
c_full: cover (full);
c_ovr: cover (ovr); // only the overwrite mode can reach this
end
`endif
endmoduleThe round-robin arbiter treats the four requesters alike by rotation. To prove the bounded-wait rule for one requester and argue rotation carries it to the others, the argument needs a fault that breaks it: the pointer is not moved when requester 0 wins, so requester 0 is always served. With the rule kept for requester 0 only, the proof passes to depth 12; kept for requester 1 only, it fails at step 5 (depth 5 passes). The full set proves on the good arbiter:
// formal: prove 4 expect pass slang top rr_arbiter
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant
);
reg [1:0] last;
// requests strictly after `last` in rotation order (higher priority part)
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest; // lowest set bit, one-hot (0 if none)
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// wt[i]: consecutive cycles requester i has requested without being granted
reg [2:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
end
end
always @(*) if (!init) begin
a_onehot0: assert ((grant & (grant - 4'd1)) == 4'd0); // at most one grant
a_no_phantom: assert ((grant & ~req) == 4'd0); // grant implies request
a_work_cons: assert (!(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= 3'd3);
a_wt1: assert (wt1 <= 3'd3);
a_wt2: assert (wt2 <= 3'd3);
a_wt3: assert (wt3 <= 3'd3);
end
// helper invariants for the induction step of the wait bounds: waited cycles plus the
// requesters still ahead in rotation order never exceed 3
function [1:0] ahead; // how many grants can still precede requester i
input [1:0] i;
ahead = i - last - 2'd1; // 0..3 (mod 4)
endfunction
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
end
end endgenerate
// covers
always @(*) if (!init) begin
c_g0: cover (grant[0]);
c_g1: cover (grant[1]);
c_g2: cover (grant[2]);
c_g3: cover (grant[3]);
c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmodule// formal: bmc 12 expect pass slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant
);
reg [1:0] last;
// requests strictly after `last` in rotation order (higher priority part)
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest; // lowest set bit, one-hot (0 if none)
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// wt[i]: consecutive cycles requester i has requested without being granted
reg [2:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
end
end
always @(*) if (!init) begin
a_onehot0: assert ((grant & (grant - 4'd1)) == 4'd0); // at most one grant
a_no_phantom: assert ((grant & ~req) == 4'd0); // grant implies request
a_work_cons: assert (!(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= 3'd3);
c_wt1: cover (wt1 > 3'd3);
c_wt2: cover (wt2 > 3'd3);
c_wt3: cover (wt3 > 3'd3);
end
// helper invariants for the induction step of the wait bounds: waited cycles plus the
// requesters still ahead in rotation order never exceed 3
function [1:0] ahead; // how many grants can still precede requester i
input [1:0] i;
ahead = i - last - 2'd1; // 0..3 (mod 4)
endfunction
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
end
end endgenerate
// covers
always @(*) if (!init) begin
c_g0: cover (grant[0]);
c_g1: cover (grant[1]);
c_g2: cover (grant[2]);
c_g3: cover (grant[3]);
c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmodule// formal: bmc 6 expect fail slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant
);
reg [1:0] last;
// requests strictly after `last` in rotation order (higher priority part)
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest; // lowest set bit, one-hot (0 if none)
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// wt[i]: consecutive cycles requester i has requested without being granted
reg [2:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
end
end
always @(*) if (!init) begin
a_onehot0: assert ((grant & (grant - 4'd1)) == 4'd0); // at most one grant
a_no_phantom: assert ((grant & ~req) == 4'd0); // grant implies request
a_work_cons: assert (!(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
c_wt0: cover (wt0 > 3'd3);
a_wt1: assert (wt1 <= 3'd3);
c_wt2: cover (wt2 > 3'd3);
c_wt3: cover (wt3 > 3'd3);
end
// helper invariants for the induction step of the wait bounds: waited cycles plus the
// requesters still ahead in rotation order never exceed 3
function [1:0] ahead; // how many grants can still precede requester i
input [1:0] i;
ahead = i - last - 2'd1; // 0..3 (mod 4)
endfunction
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
end
end endgenerate
// covers
always @(*) if (!init) begin
c_g0: cover (grant[0]);
c_g1: cover (grant[1]);
c_g2: cover (grant[2]);
c_g3: cover (grant[3]);
c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleThe sweep lists sizes and modes, with the smallest size that shows each fault, and a non-power-of-two size.
The bound is justified for each size: the formula and the run; no depth is quoted that was not run.
Every mode has a cover that is reached in it; a symmetry claim comes with the fault that breaks it.
Read the size at which a fault first appears and the depth at which it fails. A failure at fewer steps than N + 3 for the occupancy fault is a different fault, not a faster version of the same one. When a mode passes, run its cover before believing it: the overwrite cover is not reached in the default mode and is reached in the overwrite mode, so the default proof never entered the behaviour that fails. One size below the first failing depth passes: run it, so the depth in the report is a measurement.
With two entries one pointer bit indexes both slots and wraps correctly. With three entries the pointer cannot reach slot 2, so the write pointer disagrees with the read pointer plus occupancy.