A liveness violation is an infinite trace, and no finite report can print infinity. What the engine reports instead is a lasso: a finite stem from reset into a loop that repeats forever, with the loop marked. Reading that shape, stem plus loop, is the liveness analogue of reading a bounded trace, and misreading it as a finite failure sends the fix to the wrong place.
The buggy arbiter never advances its pointer when requester 0 wins, so with all four requesters persistent the pointer sticks at 3 and requester 0 is granted every cycle while 1 to 3 wait forever. The lasso is a one-state loop: a stem of reset and the first grant, then the pointer equal to 3 repeating with the same grant. Why can a bounded check not refute true liveness? Because no finite prefix refutes an eventually property: whatever finite prefix you show, it can be extended by an infinite continuation in which the requester is served, so the property is not yet violated. Only the infinite loop violates it. Bounded response is a different property: requester 1 waits at most 3 cycles has bad prefixes, namely any prefix in which requester 1 has waited 4 cycles, and that is a safety property a bounded run can refute. That is why the runnable check below finds the starvation at depth 6 while it says nothing about eventually.
The loop-length arithmetic generalises the point. A design with 5 state bits has at most 32 distinct states, so any run of 33 states repeats one (a pigeonhole argument), and a liveness engine searches for the repeat rather than the violation.
With helpers removed so the bounded-wait property speaks instead of the helper, the buggy design passes at depth 5 and fails at depth 6: requester 1 has waited 4 cycles at step 5. The cycle table marks the loop: from step 1 the pointer never moves and the grant never changes, which is the finite face of the infinite violation. The script finds the same lasso on an explicit model of the arbiter under constant contention, all four requesting in every cycle, which restates the design's pointer rule rather than reading the RTL: the good design cycles through all four grants, the buggy design self-loops with only grant 0, and the injected claim that the good design starves is caught because its loop serves everyone.
// 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
endmoduleStep | Last | Grant | Requester 1 waited | Note |
|---|---|---|---|---|
0 | any | - | - | Power-up with reset forced high; nothing is checked |
1 | 3 | 0001 | 0 | First cycle after reset: all four request, requester 0 first. Loop starts here |
2 | 3 | 0001 | 1 | Pointer fails to advance: the same state repeats |
3 | 3 | 0001 | 2 | Loop: same state, same grant |
4 | 3 | 0001 | 3 | At the bound, still waiting |
5 | 3 | 0001 | 4 | Bound of 3 broken: the bounded-wait property fails here |
How to read it: one slot is one step, counted from the first step after reset, so slot 1 is step 1. req is 0xf, all four requesters, in every slot. last, the pointer, stays at 3 and grant stays at 1, requester 0, in every slot. same_state, high when the pointer and the grant equal those of the step before, is low in step 1, where the step before is the reset step, and high from step 2 on: that is the loop. wt1, the wait counter of requester 1, counts 0, 1, 2, 3, 4, 5. bound_ok, the check that the wait is at most 3, is high through step 4, where the wait is 3, and drops in step 5, where the wait reaches 4: the step the table marks. Step 6 repeats the same state with a wait of 5.
def succ(last, buggy):
g = (last + 1) % 4 # all four request: grant is next in rotation
if buggy and g == 0:
return last # pointer fails to advance on requester 0
return g
def find_lasso(succ, init):
path, pos = [], {}
s = init
while s not in pos:
pos[s] = len(path)
path.append(s)
s = succ(s)
return path[:pos[s]], path[pos[s]:]
def grants(last):
return {(last + 1) % 4}
def starves(loop, victim):
return all(victim not in grants(s) for s in loop)
# an explicit model of the arbiter under constant contention (all four request every cycle)
_, good_loop = find_lasso(lambda s: succ(s, False), 3)
assert sorted(good_loop) == [0, 1, 2, 3], good_loop
assert not any(starves(good_loop, v) for v in (0, 1, 2, 3))
_, bad_loop = find_lasso(lambda s: succ(s, True), 3)
assert bad_loop == [3], bad_loop
assert starves(bad_loop, 1) and starves(bad_loop, 2) and starves(bad_loop, 3)
# the bounded-response form HAS a bad prefix: after 4 steps the victim has waited 4 > 3 cycles on the buggy rule
def wait_of(victim, steps, buggy):
last, w = 3, 0
for _ in range(steps):
g, last = (last + 1) % 4, succ(last, buggy)
w = 0 if g == victim else w + 1
return w
assert wait_of(1, 4, True) == 4 # bounded wait broken: a finite prefix refutes the safety form
assert wait_of(1, 4, False) == 2 # the good rule stays within the bound over the same four steps
# injected variant: claiming the good design starves requester 1
caught = False
try:
assert starves(good_loop, 1)
except AssertionError:
caught = True
assert caught, "lasso check missed the served requester"
print("PASS: buggy lasso is [3] starving 1..3; good lasso serves all")Liveness counterexamples are drawn as stem plus marked loop, never as a flat trace.
Deadlock, livelock and starvation are named precisely: here, starvation of 1 to 3 while 0 is served.
The loop is checked against the design: a loop the design cannot repeat is a modelling artefact, not a violation.
Confirm a reported lasso by replaying the stem in simulation and checking the loop state repeats with identical signals: if the second lap differs, the loop is not real. Then confirm the fix breaks the loop rather than shortening the stem: the pointer must advance on every grant, which the good design's four-state cycle demonstrates.
Loop: the state repeats identically, so it repeats forever. The stem is the reset and the first cycle; everything from step 1 on is the infinite violation, and the fix must move the pointer, not the reset sequence.