Without a liveness mode, eventually must still be checked somehow, and there are two working answers, both of which end in a safety property. A counter: if the waiter has not been served within N cycles, fail. A saved state: remember a state, and fail if the design returns to it with the waiter never served in between. Either turns an infinite obligation into something a safety engine proves or refutes. The price differs: the counter needs a bound and the saved state needs a copy of the state.
The counter construction adds a waiting counter per requester, reset when the requester stops requesting or is granted, and asserts it never exceeds N. On the good arbiter N equal to 3 is exact: a persistent requester waits at most 3 cycles and is granted in the fourth, so the bound is tight and no legitimate case fails; N equal to 2 fails on the good design, because a wait of 3 is legitimate. The saved-state construction is the exact one. A free input chooses, once, a moment to copy the state into a shadow register and set a saved flag; from then on the construction records whether the waiter was served and whether every fairness constraint held; the safety property says the saved state never recurs with the waiter unserved and every fairness constraint met inside the loop. The last condition matters: a loop that the environment's fairness forbids is not a violation. The construction doubles the state bits and needs fairness bookkeeping, and the result is an ordinary safety property, so a safety engine can run it. What this course's flow lacks is a liveness mode, not the ability to run the saved-state check; it does not include the construction, so it is shown as concept.
// not-run: the saved-state construction needs a shadow copy of the state and fairness flags; shown as concept
// shadow registers: saved_state, saved_valid, served_since_save, fair_ok_since_save
// free input "save": once, copy the state into saved_state and set saved_valid
// every later cycle: served_since_save |= victim_granted; fair_ok_since_save &= every_fairness_constraint_held
// safety property: !(saved_valid && state == saved_state && !served_since_save && fair_ok_since_save)
// a violation is a lasso: the stem reaches the save point, the loop returns to itThe good design proves the wait bounds outright: the first run is the counter form with N equal to 3, tight against the 3-cycle worst wait. The second run tightens the bound to 2: the contention cover reaches a wait of 3 at step 4, so a legitimate case breaks the too-short bound at depth 5, which is the price of choosing N by feel. The buggy design breaks the bound of 3 at depth 6 in the previous lesson. The script then does the saved-state construction explicitly on the arbiter model: it searches the product of the design state, a saved copy and a served flag for the bad state, finding a path on the buggy pointer rule and none on the good one. Dropping the served flag turns the good design into a false alarm, which shows the flag is load-bearing.
// 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 fail slang top rr_arbiter 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
// a bound of 2 is too short: a wait of 3 is legitimate (it is reached at step 4)
always @(*) if (!init) a_tight: assert (wt3 <= 3'd2);
`endif
endmodulefrom collections import deque
VICTIM = 1
def step(last, buggy):
g = (last + 1) % 4 # all four request every cycle: the grant is the next in rotation
new_last = last if (buggy and g == 0) else g
return g, new_last
def search(buggy, track_served=True):
"""Reachability of the saved-state safety violation in the product (state, saved copy, served flag)."""
start = (3, None, False)
parent = {start: None}
queue = deque([start])
while queue:
cur = queue.popleft()
last, saved, served = cur
if saved is None:
n = (last, last, False) # the free save move: copy the state, no time passes
if n not in parent:
parent[n] = cur
queue.append(n)
g, nl = step(last, buggy)
served2 = (served or g == VICTIM) if track_served else False
n = (nl, saved, served2)
if saved is not None and nl == saved and not served2:
path = [n, cur] # back in the saved state with the victim never served: a lasso
while parent[path[-1]] is not None:
path.append(parent[path[-1]])
return list(reversed(path))
if n not in parent:
parent[n] = cur
queue.append(n)
return None
assert search(True) is not None # the buggy pointer rule: a loop with requester 1 never served
assert search(False) is None # the good rule: every loop serves requester 1
# injected data: without the served flag the good design raises a false alarm
assert search(False, track_served=False) is not None
# the counter form on the same model: worst wait of the victim over 8 steps
def worst_wait(buggy, steps=8):
last, w, worst = 3, 0, 0
for _ in range(steps):
g, last = step(last, buggy)
w = 0 if g == VICTIM else w + 1
worst = max(worst, w)
return worst
assert worst_wait(False) == 3 and worst_wait(True) == 8
caught = False
try:
assert worst_wait(True) <= 3
except AssertionError:
caught = True
assert caught, "counter check missed the bound violation"
print("PASS: saved-state search finds the starvation loop on the buggy rule only; counter form agrees")Form | Gains | Costs |
|---|---|---|
Counter with bound N | Runs in the course flow; states the latency | Needs N justified; a legitimate slow case fails if N is short; a too-long N passes a sluggish design |
Saved-state loop detector | No bound: the exact liveness check | Doubles the state bits and needs fairness bookkeeping; a safety property, so a safety engine runs it; not part of this flow |
The bound N is derived from worst latency plus the assumed stall bound, never rounded.
The maximum-latency case has a cover proving the bound is reachable, not just satisfiable.
The saved-state form lists its fairness flags: a loop counts only if every fairness constraint held inside it.
Tune N from the covers: the contention cover reaches wait 3 at step 4 on the good arbiter, so N equal to 3 is reachable and tight. If the counter fails on the good design, N is short of a legitimate case: lengthen it to the measured worst case plus the stall bound. If it passes on a sluggish design, the bound exceeds what the specification tolerates: shorten it to the specified latency.
The run passes but the specification fails: the bound exceeds what is tolerated. Shorten N to the specified latency plus the stall bound and rerun; a pass at 7 is evidence about 7, not about 4.