The most dangerous assumption in formal work is the one that assumes the conclusion: fairness placed on the design's own output. Assume the grant arrives and the starving arbiter passes, because the solver is forbidden from exploring the very behaviour the property should check. The report is clean and means nothing. This lesson runs the trap, shows the cover that exposes it, and states the review rule that catches it every time.
Fairness may only constrain the environment's choices: the requesters keep requesting, the downstream accepts within M cycles. The moment an assumption touches a design output, the tool prunes the design instead of the environment, and the property holds in the pruned model while the silicon starves. Below, the buggy arbiter is given the assumption that a requester that has waited three cycles is granted, written for each requester on the grant output. The bounded-wait proof now passes, although the same design fails at depth 6 without the assumption. The exposing question is a cover on the situation the bound must forbid: requester 1 has waited 3 cycles and is not granted. Without the assumption the cover is reached; with it, it is not reached within 8, which in general is only inconclusive but here is explained by the assumption's own text: it contradicts the cover.
// formal: prove 6 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
// ASSUMPTION ON A DESIGN OUTPUT (wrong): a requester that has waited three cycles is granted
always @(*) if (!init) begin
u_fair0: assume (!(req[0] && wt0 == 3'd3) || grant[0]);
u_fair1: assume (!(req[1] && wt1 == 3'd3) || grant[1]);
u_fair2: assume (!(req[2] && wt2 == 3'd3) || grant[2]);
u_fair3: assume (!(req[3] && wt3 == 3'd3) || grant[3]);
end
`endif
endmoduleA pass on the buggy design: base case and induction step both hold, because every trace in which a requester starves is excluded by the assumption on grant. The verdict is correct for the pruned model and says nothing about the design.
// formal: cover 8 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
// ASSUMPTION ON A DESIGN OUTPUT (wrong): a requester that has waited three cycles is granted
always @(*) if (!init) begin
u_fair0: assume (!(req[0] && wt0 == 3'd3) || grant[0]);
u_fair1: assume (!(req[1] && wt1 == 3'd3) || grant[1]);
u_fair2: assume (!(req[2] && wt2 == 3'd3) || grant[2]);
u_fair3: assume (!(req[3] && wt3 == 3'd3) || grant[3]);
end
// the situation the bound must forbid: requester 1 has waited 3 cycles and is not granted
always @(*) if (!init) c_starve: cover (req[1] && wt1 == 3'd3 && !grant[1]);
`endif
endmoduleThe cover of the forbidden situation is not reached within 8: inconclusive in general, and here explained, since the assumption requires the grant in exactly that situation.
// formal: cover 6 expect reached 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
// the situation the bound must forbid: requester 1 has waited 3 cycles and is not granted
always @(*) if (!init) c_starve: cover (req[1] && wt1 == 3'd3 && !grant[1]);
`endif
endmoduleThe same cover without the assumption is reached within depth 6: requester 1 waits 3 cycles and is not granted. The only difference between the two cover runs is the assumption on the output, and the first lesson of the section says what that means: different model, different answer.
Run | Assumption | Question asked | Answer |
|---|---|---|---|
Buggy arbiter, bounded wait, depth 6 | None | Wait at most 3? | Counterexample at step 5 (previous lesson) |
Buggy arbiter, prove 6 | Grant after 3 waited cycles, on the output | Wait at most 3? | Passes: false pass |
Buggy arbiter, cover 8 | The same | Can requester 1 wait 3 and not be granted? | Not reached: inconclusive, explained by the assumption |
Buggy arbiter, cover 6 | None | The same | Reached: the situation exists |
No assumption in the list constrains a design output: every assumption names an input or a documented cut point.
Every bounded pass states its depth next to the verdict, so a too-short bound reads as narrow, not clean.
The situation the bound forbids has a cover, and the cover is reachable without the assumptions of the proof that uses it.
Audit assumptions by signal direction: list every assume, mark who drives the signal, and delete or move any that the design drives. Then rerun the proof without the suspect assumption and at a deeper bound: if a pass turns into a counterexample, the assumption was hiding the bug. A proof that survives assumption review plus a cover of the forbidden situation plus a design mutation is the only one filed as proven.
Only if something outside the design guarantees it, which nothing can: the grant is the design's own output. Restate the assumption on the environment, bound it, cover it, and watch the proof fail on the starving design as it should.