A system test hangs: one client stops getting served while the other runs fine. The trace is offered as a deadlock. The candidate must decide what it is, because the three progress failures have different shapes, proofs and fixes, and treating starvation as deadlock prescribes the wrong cure.
Job of this lesson: define the three precisely, separate structural cycles from temporal absence of progress, prove a bounded progress property, and show the starvation counterexample and its fix on a two-client arbiter and on the running four-requester arbiter.
Trap | What the candidate does | Why it fails |
|---|---|---|
Call every hang a deadlock | Proposes breaking a dependency cycle. | No cycle here: one client is served forever while the other waits. That is starvation, fixed in the arbiter, not the fabric. |
Prove 'eventually' with no fairness and no engine | Asserts every request is eventually granted. | The unbounded form needs fairness on environment choices and a lasso engine; without them it cannot be refuted or proved. The bounded form below needs neither. |
Put fairness on the design | Assumes the grant arrives to prove the grant arrives. | Fairness constrains environment choices only, never design outputs; assuming the answer forces the pass and hides the starvation. |
Deadlock means no progress is possible: a cycle of waits where each party holds what the next needs, argued on the dependency graph. Livelock means activity without completion. Starvation means one requester is never served while others are. Deadlock needs a structural argument plus a progress property, livelock a completion measure, starvation a bounded wait per requester. A liveness counterexample is a lasso. The bounded form replaces eventually with within N, a safety property whose window comes from the requester count and the service quantum.
The design is a 2-client round robin with a wait counter for client 1: consecutive cycles it requests without being granted. By the formula below a client waits at most 1 cycle, so the property is wait at most 1, beside a one-hot check on the grant logic. The good design is proved, induction step included. The starvation variant freezes the turn update whenever client 0 wins; the double-grant variant makes the one-hot check fail, so that check can fail too.
// formal: prove 8 expect pass slang top tiny_arb
`define FORMAL
// Lesson-local demo: 2-client round-robin arbiter with a wait bound of 1 for client 1.
module tiny_arb #(parameter BUG = 0) (
input wire clk, input wire rst, input wire [1:0] req, output wire [1:0] gnt
);
reg turn;
assign gnt[0] = req[0] && (turn == 1'b0 || !req[1]);
assign gnt[1] = req[1] && (turn == 1'b1 || !req[0] || BUG == 2);
always @(posedge clk) begin
if (rst) turn <= 1'b0;
else if (gnt[0] && !(BUG == 1)) turn <= 1'b1;
else if (gnt[1]) turn <= 1'b0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] w1;
always @(posedge clk) begin
if (rst) w1 <= 3'd0;
else if (!req[1] || gnt[1]) w1 <= 3'd0;
else w1 <= w1 + 3'd1;
end
always @(*) if (!init) begin
a_onehot: assert (gnt != 2'b11);
a_bounded: assert (w1 <= 3'd1);
end
always @(posedge clk) if (!init) c_both: cover (req == 2'b11);
`endif
endmodule// formal: bmc 3 expect pass slang top tiny_arb define BUG=1
`define FORMAL
// Lesson-local demo: 2-client round-robin arbiter with a wait bound of 1 for client 1.
module tiny_arb #(parameter BUG = 0) (
input wire clk, input wire rst, input wire [1:0] req, output wire [1:0] gnt
);
reg turn;
assign gnt[0] = req[0] && (turn == 1'b0 || !req[1]);
assign gnt[1] = req[1] && (turn == 1'b1 || !req[0] || BUG == 2);
always @(posedge clk) begin
if (rst) turn <= 1'b0;
else if (gnt[0] && !(BUG == 1)) turn <= 1'b1;
else if (gnt[1]) turn <= 1'b0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] w1;
always @(posedge clk) begin
if (rst) w1 <= 3'd0;
else if (!req[1] || gnt[1]) w1 <= 3'd0;
else w1 <= w1 + 3'd1;
end
always @(*) if (!init) begin
a_onehot: assert (gnt != 2'b11);
a_bounded: assert (w1 <= 3'd1);
end
always @(posedge clk) if (!init) c_both: cover (req == 2'b11);
`endif
endmodule// formal: bmc 4 expect fail slang top tiny_arb define BUG=1
`define FORMAL
// Lesson-local demo: 2-client round-robin arbiter with a wait bound of 1 for client 1.
module tiny_arb #(parameter BUG = 0) (
input wire clk, input wire rst, input wire [1:0] req, output wire [1:0] gnt
);
reg turn;
assign gnt[0] = req[0] && (turn == 1'b0 || !req[1]);
assign gnt[1] = req[1] && (turn == 1'b1 || !req[0] || BUG == 2);
always @(posedge clk) begin
if (rst) turn <= 1'b0;
else if (gnt[0] && !(BUG == 1)) turn <= 1'b1;
else if (gnt[1]) turn <= 1'b0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] w1;
always @(posedge clk) begin
if (rst) w1 <= 3'd0;
else if (!req[1] || gnt[1]) w1 <= 3'd0;
else w1 <= w1 + 3'd1;
end
always @(*) if (!init) begin
a_onehot: assert (gnt != 2'b11);
a_bounded: assert (w1 <= 3'd1);
end
always @(posedge clk) if (!init) c_both: cover (req == 2'b11);
`endif
endmodule// formal: bmc 2 expect fail slang top tiny_arb define BUG=2
`define FORMAL
// Lesson-local demo: 2-client round-robin arbiter with a wait bound of 1 for client 1.
module tiny_arb #(parameter BUG = 0) (
input wire clk, input wire rst, input wire [1:0] req, output wire [1:0] gnt
);
reg turn;
assign gnt[0] = req[0] && (turn == 1'b0 || !req[1]);
assign gnt[1] = req[1] && (turn == 1'b1 || !req[0] || BUG == 2);
always @(posedge clk) begin
if (rst) turn <= 1'b0;
else if (gnt[0] && !(BUG == 1)) turn <= 1'b1;
else if (gnt[1]) turn <= 1'b0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] w1;
always @(posedge clk) begin
if (rst) w1 <= 3'd0;
else if (!req[1] || gnt[1]) w1 <= 3'd0;
else w1 <= w1 + 3'd1;
end
always @(*) if (!init) begin
a_onehot: assert (gnt != 2'b11);
a_bounded: assert (w1 <= 3'd1);
end
always @(posedge clk) if (!init) c_both: cover (req == 2'b11);
`endif
endmodule// formal: cover 3 expect reached slang top tiny_arb
`define FORMAL
// Lesson-local demo: 2-client round-robin arbiter with a wait bound of 1 for client 1.
module tiny_arb #(parameter BUG = 0) (
input wire clk, input wire rst, input wire [1:0] req, output wire [1:0] gnt
);
reg turn;
assign gnt[0] = req[0] && (turn == 1'b0 || !req[1]);
assign gnt[1] = req[1] && (turn == 1'b1 || !req[0] || BUG == 2);
always @(posedge clk) begin
if (rst) turn <= 1'b0;
else if (gnt[0] && !(BUG == 1)) turn <= 1'b1;
else if (gnt[1]) turn <= 1'b0;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [2:0] w1;
always @(posedge clk) begin
if (rst) w1 <= 3'd0;
else if (!req[1] || gnt[1]) w1 <= 3'd0;
else w1 <= w1 + 3'd1;
end
always @(*) if (!init) begin
a_onehot: assert (gnt != 2'b11);
a_bounded: assert (w1 <= 3'd1);
end
always @(posedge clk) if (!init) c_both: cover (req == 2'b11);
`endif
endmoduleStep | req | gnt | turn | wait of client 1 | Bound of 1 |
|---|---|---|---|---|---|
0 | reset | - | 0 | 0 | not checked |
1 | 11 | 01 | 0 | 0 | holds |
2 | 11 | 01 | 0 (frozen) | 1 | holds |
3 | 11 | 01 | 0 (frozen) | 2 | breaks |
Both clients ask from step 1; client 0 wins every cycle and the turn never moves, so the wait reads 0, 1, 2 and breaks the bound at step 3 (depth 4; depth 3 passes). This is starvation: client 0 is served throughout, there is no cycle of waits, and no fabric change helps. Root cause: the pointer update is skipped when client 0 wins. Fix: advance it on every grant. The cover for both clients requesting together is not reached at depth 2 (inconclusive on its own) and is reached at depth 3.
On the four-requester arbiter the property is wait at most 3: a continuously requesting requester is granted in the fourth cycle. It needs no assumption on the requesters, because a grant is given whenever any request exists and the wait counter restarts when a request drops; fairness appears only for the unbounded form (fairness assumptions for progress proofs). The starvation mutant, pointer not advanced when requester 0 wins, passes at depth 5 and fails at depth 6 with the helpers off. The contention cover is reached at depth 5; not reached within 4 is inconclusive.
// 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 5 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);
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 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
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: cover 4 expect fail 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: cover 5 expect reached 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
endmoduleThe window is derived, not chosen. For a round robin over N requesters with one grant per cycle, a continuously requesting client waits at most N minus 1 times the quantum: every other client is served at most once before the turn returns. N of 2 gives 1, the bound above; N of 4 gives 3, the running arbiter.
def worst_wait(requesters, quantum=1):
assert requesters >= 2, "a single requester never waits"
assert quantum >= 1, "service quantum is at least one cycle"
return (requesters - 1) * quantum
assert worst_wait(4) == 3, worst_wait(4)
assert worst_wait(2) == 1, worst_wait(2)
# The failing variant: the same call with a wrong requester count gives a different window.
try:
assert worst_wait(3) == 3
raise SystemExit("accepted the window of a four-requester arbiter for three requesters")
except AssertionError:
pass
print("PASS: 2 requesters wait at most 1 cycle, 4 requesters at most 3")A strong answer draws the dependency graph first and reports it acyclic, then reads who is served, which names starvation. It derives the window, says the bounded form needs no fairness while the unbounded form would, and closes with the fix plus the rerun: bound proved, cover reached, mutant caught.
Dimension | Strong (3 to 4) | Weak (0 to 2) |
|---|---|---|
Assumption | Bounded form: none; unbounded form: fairness on the environment only. | No statement, or fairness on the grant. |
Mechanism | Wait counter read cycle by cycle to step 3. | The trace is a deadlock because nothing finished. |
Trade-off | Bounded safety form versus true liveness with a lasso engine. | Eventually asserted with no engine behind it. |
Evidence | Failing step plus worst-case cover plus the passing fix. | The passing fix alone. |
Separate livelock from starvation on the served set: if transactions start but none completes, find the completion measure that never advances; if one client is served while another waits, it is starvation and the arbiter owns the fix.