Arbiter Grant Latency Proof

On this page

Part 5 of 10, lesson 9 of 20Formal ApplicationsAll levels

Why it matters

A round-robin arbiter looks fair by construction until a pointer update is gated by one requester and everyone else starves. The symptom is a throughput collapse under a specific traffic mix that directed tests never hit, because they never hold all four requesters high while the pointer sticks. The bounded-wait property catches it: a continuously requesting requester must wait at most three cycles, one fewer than the requester count.

The core idea

Three property families share the work. One-hot and no-grant-without-request are combinational and close at once. Work conservation, some request implies some grant, needs no environment assumption here because a grant is given in the same cycle as any request, so the pointer always moves toward every waiter. The bounded-wait family counts consecutive unserved cycles per requester and bounds each counter at three. Helpers relate each wait counter to the requesters still ahead in rotation order, which closes the induction at once; without them the step needs a window of four.

Worked example: the window arithmetic

The window comes from the specification, not from tuning: with four requesters and a one-cycle grant, a waiter can be preceded by at most the other three, so the bound is three. The calculator below derives it and shows that a smaller window fails legitimately slow traffic while the specified window holds:

example.py

def window(n_requesters, quantum, stall_bound):
    return (n_requesters - 1) * quantum + stall_bound

assert window(4, 1, 0) == 3
assert window(4, 1, 2) == 5

def waits(patterns, n=4):
    # illustrative rotating-priority model: after a grant the pointer moves past the winner
    ptr, wait, seen = 0, [0] * n, []
    for req in patterns:
        win = next((k for k in ((ptr + i) % n for i in range(n)) if req >> k & 1), None)
        for k in range(n):
            if req >> k & 1 and k != win: wait[k] += 1
            elif k == win: seen.append(wait[k]); wait[k] = 0; ptr = (k + 1) % n
            else: wait[k] = 0
    return seen

waits_seen = waits([0b1111] * 12 + [0b1010, 0b0110, 0b1111, 0b1001, 0b1111, 0b1111])
assert max(waits_seen) == window(4, 1, 0), waits_seen
assert all(w <= window(4, 1, 0) for w in waits_seen)
too_small = 2
assert any(w > too_small for w in waits_seen)
print("PASS: window 3 from (4-1)*1+0, waits computed from the model; window 2 would fail legitimate traffic")

Worked example: the proof and its starvation partners

The full arbiter property set proves whole with helpers, with no assumption on the requesters. The first partner freezes the pointer whenever requester 0 wins, so requester 0 is served forever and the other three starve. With the helpers present, the helper invariant already fails at step 2, which teaches a useful distinction: an invariant failing is not yet a requirement failing, but it points at the same root cause:

rr_arbiter.sv

// formal: prove 4 expect pass slang top rr_arbiter
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

rr_arbiter.sv

// formal: bmc 3 expect fail slang top rr_arbiter define BUG=1
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

The requirement itself, the bounded wait, is seen without the helpers. Read the trace as waits: all four request from the first step, requester 0 wins every cycle, and the victims' counters climb past the bound at step 5. The bound of 3 is met exactly at step 4, so a run bounded to 5 (steps 0 to 4) passes and a run bounded to 6 fails. A bounded run one step short of the bug would have said nothing wrong:

Step	req	grant	wt1	Outcome
1	1111	0001	0	requester 0 wins, pointer stuck
2	1111	0001	1	victims waiting
3	1111	0001	2	still waiting
4	1111	0001	3	at the bound
5	1111	0001	4	counterexample: bound exceeded

rr_arbiter.sv

// formal: bmc 5 expect pass slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

rr_arbiter.sv

// formal: bmc 6 expect fail slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

Root cause: the pointer update does not advance when requester 0 wins, so rotation stops. Fix the update to advance on every grant. The window arithmetic above says why the bound is three and not two: three is derived from the requester count, and the calculator shows a smaller window failing traffic the specification allows.

The helper claim is also run. Without the helpers the induction step fails at depth 3 and closes at depth 4, which is why the property alone needs a window of four; the bounded check passes either way:

rr_arbiter.sv

// formal: prove 3 expect unproven slang top rr_arbiter define HELPER=0
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

rr_arbiter.sv

// formal: prove 4 expect pass slang top rr_arbiter define HELPER=0
`define FORMAL
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;

  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;
    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);

  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);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    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

  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  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

  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

What the review looks for

The bound is derived from requester count and service quantum, not tuned until the proof passes.
The no-assumption claim is justified: grants are combinational in requests, so no requester behaviour is assumed.
Helper invariants are proved alongside, never assumed: each appears as an assertion in the same run.

Verify and debug

A wait-bound failure first asks who else requested: with no contention the bound is trivially met, so the trace must show contention. Then read the pointer: a pointer that stops advancing names the logic bug. A failure only without helpers at a smaller window is a proof-strength issue, not a design bug, and the helper family is the fix.

Check yourself Requester 1 waits three cycles while requesters 2 and 3 are served, then is granted. Does the bound hold?

Yes: three is the bound, met exactly. The bound counts the worst legitimate case, three other grants first, not the average. Only a fourth waiting cycle would fail.

Navigate

Why it matters

The core idea

Worked example: the window arithmetic

Worked example: the proof and its starvation partners

What the review looks for

Verify and debug

Related topics

Arbiter Grant Latency Proof

Why it matters

The core idea

Worked example: the window arithmetic

Worked example: the proof and its starvation partners

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: the window arithmetic

Worked example: the proof and its starvation partners

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: the window arithmetic

Worked example: the proof and its starvation partners

What the review looks for

Verify and debug

Related topics

Up next