Every liveness proof smuggles in an assumption about the environment: without one, the environment can stall forever and every eventually fails. Fairness states that assumption precisely. Weak fairness says a request that stays enabled continuously is eventually taken; strong fairness says a request enabled infinitely often is taken infinitely often. The arbiter needs neither as an assumption, because a grant follows any request in the same cycle, but the notions decide every liveness review, so this lesson evaluates them on traces where they differ and then writes the bounded form of the environment's promise as a runnable assumption.
Consider one requester over a looping trace. Weak fairness is violated only by a loop where the requester is enabled in every state and never granted: continuous hunger with no service. Strong fairness is violated by any loop where the requester is enabled in at least one state per lap and never granted: intermittent hunger with no service. Strong implies weak, not the reverse: a trace that enables the requester every other lap and never grants it satisfies weak fairness and breaks strong. Fairness constrains the environment's choices only, never design outputs: assuming the design grants is assuming the conclusion.
The runnable form in this flow is a bounded promise about the environment's input. The monitor below counts how long a request has waited for the environment's ready. Without an assumption the environment may stall for ever, and the bound on the wait fails; with the assumption that ready is high after at most 3 stalled cycles, the same bound is proven. The assumption mentions only the two input signals and the counter built from them. The cover shows it is not vacuous: a wait of 3 stalled cycles is reachable. The arbiter, by contrast, needs no assumption at all, which the last block of the lesson shows.
// formal: bmc 6 expect fail slang top wait_bound define FAIR=0
`define FORMAL
// wait_bound: request/ready monitor (lesson-local module). The environment drives req and ready.
// waited counts consecutive cycles in which req was high and ready low.
// FAIR = 1 adds the environment contract "ready arrives within 3 stalled cycles" as an assumption
// on the two input signals; FAIR = 0 leaves the environment free to stall for ever.
module wait_bound #(parameter FAIR = 1) (
input wire clk,
input wire rst,
input wire req,
input wire ready,
output reg [3:0] waited
);
always @(posedge clk) begin
if (rst || !req || ready) waited <= 4'd0;
else if (waited != 4'd15) waited <= waited + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// bounded fairness on the ENVIRONMENT: after 3 stalled cycles, ready must be high
generate if (FAIR) begin : g_fair
always @(*) if (!init) u_fair: assume (waited < 4'd3 || ready);
end endgenerate
// the safety form of "a request is eventually accepted": nobody waits longer than 3 cycles
always @(*) if (!init) a_wait: assert (waited <= 4'd3);
// the assumption is not vacuous: a wait of 3 stalled cycles is reachable
always @(*) if (!init) c_wait3: cover (waited == 4'd3);
`endif
endmoduleNo environment contract: the environment holds ready low, the wait grows past 3, and the bound fails at depth 6 (it passes at depth 5, when the fourth stalled cycle has not yet been counted). This is a missing fairness assumption, not a design bug.
// formal: prove 4 expect pass slang top wait_bound define FAIR=1
`define FORMAL
// wait_bound: request/ready monitor (lesson-local module). The environment drives req and ready.
// waited counts consecutive cycles in which req was high and ready low.
// FAIR = 1 adds the environment contract "ready arrives within 3 stalled cycles" as an assumption
// on the two input signals; FAIR = 0 leaves the environment free to stall for ever.
module wait_bound #(parameter FAIR = 1) (
input wire clk,
input wire rst,
input wire req,
input wire ready,
output reg [3:0] waited
);
always @(posedge clk) begin
if (rst || !req || ready) waited <= 4'd0;
else if (waited != 4'd15) waited <= waited + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// bounded fairness on the ENVIRONMENT: after 3 stalled cycles, ready must be high
generate if (FAIR) begin : g_fair
always @(*) if (!init) u_fair: assume (waited < 4'd3 || ready);
end endgenerate
// the safety form of "a request is eventually accepted": nobody waits longer than 3 cycles
always @(*) if (!init) a_wait: assert (waited <= 4'd3);
// the assumption is not vacuous: a wait of 3 stalled cycles is reachable
always @(*) if (!init) c_wait3: cover (waited == 4'd3);
`endif
endmoduleWith ready promised within 3 stalled cycles, the bound is proven for every environment that keeps the promise. Read this result honestly: the module contains only a monitor, so the assumption waited < 3 || ready and the assertion waited <= 3 are the same statement one cycle apart. The pass shows that the promise is consistent with the bound and that the bound is not met without it; it says nothing yet about a design. The design that needs the promise is the handshake chain in Progress in a Handshake Chain, where the same promise bounds a real stage. The promise is bounded, so it is a safety assumption, and it implies weak fairness for ready while a request is pending.
// formal: cover 5 expect reached slang top wait_bound define FAIR=1
`define FORMAL
// wait_bound: request/ready monitor (lesson-local module). The environment drives req and ready.
// waited counts consecutive cycles in which req was high and ready low.
// FAIR = 1 adds the environment contract "ready arrives within 3 stalled cycles" as an assumption
// on the two input signals; FAIR = 0 leaves the environment free to stall for ever.
module wait_bound #(parameter FAIR = 1) (
input wire clk,
input wire rst,
input wire req,
input wire ready,
output reg [3:0] waited
);
always @(posedge clk) begin
if (rst || !req || ready) waited <= 4'd0;
else if (waited != 4'd15) waited <= waited + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// bounded fairness on the ENVIRONMENT: after 3 stalled cycles, ready must be high
generate if (FAIR) begin : g_fair
always @(*) if (!init) u_fair: assume (waited < 4'd3 || ready);
end endgenerate
// the safety form of "a request is eventually accepted": nobody waits longer than 3 cycles
always @(*) if (!init) a_wait: assert (waited <= 4'd3);
// the assumption is not vacuous: a wait of 3 stalled cycles is reachable
always @(*) if (!init) c_wait3: cover (waited == 4'd3);
`endif
endmoduleThe wait of 3 stalled cycles is reached within depth 5, so the assumption allows the interesting behaviour and is not vacuous.
// 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
endmoduleThe arbiter proves its bounded wait with no assumption on the requesters: a grant follows any request in the same cycle and the pointer moves toward every waiter, so a persistent requester waits at most 3 cycles.
The script evaluates both notions on three looping traces for one requester: always enabled and always granted, enabled every other lap and never granted, and never enabled. The middle trace is the interesting one: weak fairness holds, strong fails. The injected check confirms that claiming strong fairness on the starving trace is caught.
def weak_holds(loop, i):
enabled_all = all(i in s["enabled"] for s in loop)
taken = any(i in s["taken"] for s in loop)
return (not enabled_all) or taken
def strong_holds(loop, i):
enabled_some = any(i in s["enabled"] for s in loop)
taken = any(i in s["taken"] for s in loop)
return (not enabled_some) or taken
granted = [{"enabled": {1}, "taken": {1}}]
starving = [{"enabled": {1}, "taken": set()},
{"enabled": set(), "taken": set()}]
idle = [{"enabled": set(), "taken": set()}]
hungry = [{"enabled": {1}, "taken": set()}]
assert weak_holds(granted, 1) and strong_holds(granted, 1)
assert weak_holds(starving, 1) and not strong_holds(starving, 1)
assert weak_holds(idle, 1) and strong_holds(idle, 1)
assert not weak_holds(hungry, 1) and not strong_holds(hungry, 1)
# injected variant: claiming strong fairness on the starving trace
caught = False
try:
assert strong_holds(starving, 1)
except AssertionError:
caught = True
assert caught, "fairness check missed the starving trace"
print("PASS: weak holds on intermittent hunger, strong fails; false claim caught")Loop shape | Weak | Strong |
|---|---|---|
Always enabled, always taken | Holds | Holds |
Enabled every other lap, never taken | Holds | Fails |
Continuously enabled, never taken | Fails | Fails |
Every liveness-adjacent claim names its fairness, weak or strong, and the bound that replaces it.
Fairness constrains environment choices only: no assumption touches a design output.
Bounded substitutes state the environment stall bound they assume, with a cover that the bound is reachable.
Recheck any fairness assumption by asking who controls the signal: if the design drives it, the assumption is forbidden and the proof is circular. If the environment drives it, confirm the bound is reachable with a cover, as above, then confirm the proof fails when the assumption is removed on a design that needs it, as the first block does.
Strong: the requester is enabled infinitely often and never taken. Weak holds, because enablement is not continuous. A proof that needs this trace ruled out needs strong fairness on the environment.