The specification says every requester is served fairly. The proof engineer writes eventually and the flow cannot run it. The working replacement is a bound: a continuously requesting requester waits at most three cycles, granted on the fourth. That number is not chosen; it falls out of the rotation, and this lesson's one job is to write the rule with its counter, justify the bound, and show what goes wrong when the bound is guessed too small or too large.
Bounded response is safety: a wait longer than N cycles is a finite bad prefix, so a bounded run can refute it and an induction can prove it. The rule needs a counter per requester that counts consecutive unanswered cycles and resets on grant or on the request dropping. The bound is the worst honest latency plus the assumed stall bound: here the arbiter grants combinationally whenever any request exists, so the worst wait is the three other grants ahead in rotation, and no stall assumption is needed at all.
Two comments are mandatory on every such rule. The property says within N cycles, never eventually: the words state which side of the line the rule is on. And the bound says where it came from: rotation depth plus environment stall bound, not a round number.
// not-run: implication and delay operators are not accepted by this front end
// general textbook form, a registered grant: req |-> ##[1:N] gnt // within N cycles, safety
// this arbiter's grant is combinational, so the window starts in the request cycle and a
// continuously waiting requester is granted within the first four cycles:
// assert property (not ((req[i] && !grant[i]) [*4])); // never four consecutive waiting cycles
// counter form used below: wt[i] counts consecutive waiting cycles; the rule is wt[i] <= 3The arbiter carries four wait counters, one per requester, and four bounded-response checks against them. The listing is the running arbiter with two lesson-local parameters: BOUND, the wait bound the checks use (3 for the specified design), and SLOW, a deliberately slow variant used below. On the correct design the full proof passes:
// 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).
// Lesson-local parameters: BOUND is the wait bound the checks use (3 for the specified design);
// SLOW=1 builds a deliberately slow variant that grants only every second cycle.
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1, parameter BOUND = 3, parameter SLOW = 0) (
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)}};
reg phase; // SLOW only: grants happen in every second cycle
always @(posedge clk) phase <= rst ? 1'b0 : !phase;
assign grant = (g_hi | g_lo) & {4{(SLOW == 0) || phase}};
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 (4 bits)
reg [3:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 4'd0; wt1 <= 4'd0; wt2 <= 4'd0; wt3 <= 4'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 4'd1 : 4'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 4'd1 : 4'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 4'd1 : 4'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 4'd1 : 4'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 (SLOW != 0 || !(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= BOUND);
a_wt1: assert (wt1 <= BOUND);
a_wt2: assert (wt2 <= BOUND);
a_wt3: assert (wt3 <= BOUND);
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 + {2'b0, ahead(2'd0)} <= 4'd3);
h_wt1: assert (wt1 + {2'b0, ahead(2'd1)} <= 4'd3);
h_wt2: assert (wt2 + {2'b0, ahead(2'd2)} <= 4'd3);
h_wt3: assert (wt3 + {2'b0, ahead(2'd3)} <= 4'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 == 4'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleThe mutant stops advancing the pointer when requester 0 wins, so 0 hogs the arbiter and the rest starve. Step 0 is the reset step; the bounded waits fail at the first wait of four cycles. The run with the helper invariants off fails at depth 6; the solver names a_wt3 and a_wt2. The table follows requester 3 in a constructed trace that exhibits the same failure, not the solver's own:
// 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).
// Lesson-local parameters: BOUND is the wait bound the checks use (3 for the specified design);
// SLOW=1 builds a deliberately slow variant that grants only every second cycle.
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1, parameter BOUND = 3, parameter SLOW = 0) (
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)}};
reg phase; // SLOW only: grants happen in every second cycle
always @(posedge clk) phase <= rst ? 1'b0 : !phase;
assign grant = (g_hi | g_lo) & {4{(SLOW == 0) || phase}};
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 (4 bits)
reg [3:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 4'd0; wt1 <= 4'd0; wt2 <= 4'd0; wt3 <= 4'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 4'd1 : 4'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 4'd1 : 4'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 4'd1 : 4'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 4'd1 : 4'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 (SLOW != 0 || !(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= BOUND);
a_wt1: assert (wt1 <= BOUND);
a_wt2: assert (wt2 <= BOUND);
a_wt3: assert (wt3 <= BOUND);
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 + {2'b0, ahead(2'd0)} <= 4'd3);
h_wt1: assert (wt1 + {2'b0, ahead(2'd1)} <= 4'd3);
h_wt2: assert (wt2 + {2'b0, ahead(2'd2)} <= 4'd3);
h_wt3: assert (wt3 + {2'b0, ahead(2'd3)} <= 4'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 == 4'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleStep | req | last | grant | Wait counter of requester 3, as seen in that step |
|---|---|---|---|---|
1 | 1111 | 3 | 0001 | 0 (the request starts). |
2 | 1111 | 3 | 0001 | 1. |
3 | 1111 | 3 | 0001 | 2. |
4 | 1111 | 3 | 0001 | 3, the bound. |
5 | 1111 | 3 | 0001 | 4: the bounded wait fails here. |
The bound is a claim about the specification, so a wrong bound misleads in both directions. Too small: on the correct arbiter a bound of 2 is exceeded by a legal four-way rotation, and the proof reports a counterexample that is not a design bug:
// formal: bmc 8 expect fail slang top rr_arbiter define BOUND=2
`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).
// Lesson-local parameters: BOUND is the wait bound the checks use (3 for the specified design);
// SLOW=1 builds a deliberately slow variant that grants only every second cycle.
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1, parameter BOUND = 3, parameter SLOW = 0) (
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)}};
reg phase; // SLOW only: grants happen in every second cycle
always @(posedge clk) phase <= rst ? 1'b0 : !phase;
assign grant = (g_hi | g_lo) & {4{(SLOW == 0) || phase}};
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 (4 bits)
reg [3:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 4'd0; wt1 <= 4'd0; wt2 <= 4'd0; wt3 <= 4'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 4'd1 : 4'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 4'd1 : 4'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 4'd1 : 4'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 4'd1 : 4'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 (SLOW != 0 || !(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= BOUND);
a_wt1: assert (wt1 <= BOUND);
a_wt2: assert (wt2 <= BOUND);
a_wt3: assert (wt3 <= BOUND);
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 + {2'b0, ahead(2'd0)} <= 4'd3);
h_wt1: assert (wt1 + {2'b0, ahead(2'd1)} <= 4'd3);
h_wt2: assert (wt2 + {2'b0, ahead(2'd2)} <= 4'd3);
h_wt3: assert (wt3 + {2'b0, ahead(2'd3)} <= 4'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 == 4'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleToo large: the slow variant grants only in every second cycle. With the specified bound of 3 it fails, which is the right answer for a design that breaks its specification. With a bound of 7 the same slow design passes, because 7 is the longest wait it produces: bounded to depth 14, and blind to the slowness the specified three would catch.
// formal: bmc 12 expect fail slang top rr_arbiter define SLOW=1 define HELPER=0 define BOUND=3
`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).
// Lesson-local parameters: BOUND is the wait bound the checks use (3 for the specified design);
// SLOW=1 builds a deliberately slow variant that grants only every second cycle.
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1, parameter BOUND = 3, parameter SLOW = 0) (
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)}};
reg phase; // SLOW only: grants happen in every second cycle
always @(posedge clk) phase <= rst ? 1'b0 : !phase;
assign grant = (g_hi | g_lo) & {4{(SLOW == 0) || phase}};
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 (4 bits)
reg [3:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 4'd0; wt1 <= 4'd0; wt2 <= 4'd0; wt3 <= 4'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 4'd1 : 4'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 4'd1 : 4'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 4'd1 : 4'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 4'd1 : 4'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 (SLOW != 0 || !(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= BOUND);
a_wt1: assert (wt1 <= BOUND);
a_wt2: assert (wt2 <= BOUND);
a_wt3: assert (wt3 <= BOUND);
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 + {2'b0, ahead(2'd0)} <= 4'd3);
h_wt1: assert (wt1 + {2'b0, ahead(2'd1)} <= 4'd3);
h_wt2: assert (wt2 + {2'b0, ahead(2'd2)} <= 4'd3);
h_wt3: assert (wt3 + {2'b0, ahead(2'd3)} <= 4'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 == 4'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmodule// formal: bmc 14 expect pass slang top rr_arbiter define SLOW=1 define HELPER=0 define BOUND=7
`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).
// Lesson-local parameters: BOUND is the wait bound the checks use (3 for the specified design);
// SLOW=1 builds a deliberately slow variant that grants only every second cycle.
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1, parameter BOUND = 3, parameter SLOW = 0) (
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)}};
reg phase; // SLOW only: grants happen in every second cycle
always @(posedge clk) phase <= rst ? 1'b0 : !phase;
assign grant = (g_hi | g_lo) & {4{(SLOW == 0) || phase}};
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 (4 bits)
reg [3:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 4'd0; wt1 <= 4'd0; wt2 <= 4'd0; wt3 <= 4'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 4'd1 : 4'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 4'd1 : 4'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 4'd1 : 4'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 4'd1 : 4'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 (SLOW != 0 || !(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= BOUND);
a_wt1: assert (wt1 <= BOUND);
a_wt2: assert (wt2 <= BOUND);
a_wt3: assert (wt3 <= BOUND);
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 + {2'b0, ahead(2'd0)} <= 4'd3);
h_wt1: assert (wt1 + {2'b0, ahead(2'd1)} <= 4'd3);
h_wt2: assert (wt2 + {2'b0, ahead(2'd2)} <= 4'd3);
h_wt3: assert (wt3 + {2'b0, ahead(2'd3)} <= 4'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 == 4'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleHow to read it: one slot is one step, counted from the first step after reset, and req is 0xf in every slot. On the correct arbiter grant_good rotates 1, 2, 4, 8, so wt3_good, the wait counter of requester 3, counts 0, 1, 2, 3 and returns to 0 in step 5, the step after its grant: its longest wait is 3 and ok_good stays high. On the starving mutant grant_bug is 1 in every step, wt3_bug counts 0 to 7, and ok_bug drops in step 5, where the wait reaches 4: the step the cycle table marks as the failure.
The bound arithmetic is worth automating. The script below models the rotation, measures the longest wait of the correct and the slow design, derives the specified bound from the number of requesters, and classifies each bound against each design; its numbers are the ones in the table. It rejects negative inputs, and its classifications are asserted both ways:
def window(worst_latency, stall_bound):
if worst_latency < 0 or stall_bound < 0:
raise ValueError("latencies and stall bounds are counts, never negative")
return worst_latency + stall_bound
def worst_wait(n, slow=False, cycles=60):
"""All n requesters request in every cycle; the slow variant grants only in every second cycle."""
last, wait, worst = n - 1, [0] * n, 0
for t in range(cycles):
grant = (last + 1) % n if (not slow or t % 2 == 1) else None
wait = [0 if i == grant else w + 1 for i, w in enumerate(wait)]
worst = max(worst, *wait)
if grant is not None:
last = grant
return worst
def judge(bound, worst, spec):
if worst > bound:
return "false failure" if bound < spec else "real failure"
return "passes but hides a slow design" if worst > spec else "passes"
spec = window(4 - 1, 0) # four requesters: three grants ahead, no stall bound
good, slow = worst_wait(4), worst_wait(4, slow=True)
assert (spec, good, slow) == (3, 3, 7) # the proof blocks use bound 3; the slow variant needs 7
assert judge(3, good, spec) == "passes"
assert judge(2, good, spec) == "false failure" # N too small: a legal design fails
assert judge(3, slow, spec) == "real failure" # the specified N catches the slow design
assert judge(7, slow, spec) == "passes but hides a slow design" # N too large lets it through
assert window(4, 3) == 7 # illustrative registered grant: latency 4, stall bound 3
try:
window(-1, 0)
raise SystemExit("FAIL: a negative latency was accepted")
except ValueError:
pass
print("PASS: window 3 for four requesters; too small fails the good design, too large hides the slow one")The property says within N cycles in its comment, and N carries its derivation: rotation depth here, latency plus stall bound in general.
A window too small is a false failure, not a bug: a bound of 2 fails a legal four-way rotation, so the bound is argued before the run, not fitted to it.
A window too large is a hidden slowness: the review asks which design the bound would reject, and the slow variant above is that design.
The starvation mutant fails exactly at N plus 1: a wait of four with a bound of three, which is what makes the counterexample readable.
Read a bounded-response failure as a count: how many consecutive unanswered cycles, and which grants went to others meanwhile? A count above the rotation depth means the pointer is stuck. A count within depth but above the window means the window is wrong: lengthen it with its derivation, never to quiet one trace.
The step-five wait: the helper is an invariant about the pointer, and it breaks earlier because it watches the cause. An invariant failing is not yet a requirement failing, which is why both are reported and read in that order.