Arbiters

An arbiter decides who may use a shared resource next. Its rules are short and precise, which makes it an ideal block for formal: at most one grant, no grant without a request, and every requester served within a bounded time. The last rule is where round-robin arbiters fail, because the bug only shows under a particular pattern of competing requests. This article checks a 4-requester round-robin arbiter and finds a pointer bug that starves one requester.

9 min read | Intermediate

What You'll Learn

• Write the three standard arbiter properties: mutual exclusion, validity and fairness
• Express fairness as a bounded wait with a fairness assumption on the requesters
• Find a round-robin pointer bug that starves a requester
• Measure the worst-case wait of a correct arbiter

Standard Arbiter Properties

// mutual exclusion: at most one grant
a_onehot: assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
// validity: a grant only goes to a requester that asked
a_valid:  assert property (@(posedge clk) disable iff (rst) ##1 (gnt & ~$past(req)) == 4'b0000);
// fairness: a waiting requester is served within 4 cycles (one property per requester)
a_fair3:  assert property (@(posedge clk) disable iff (rst) req[3] |-> ##[0:4] gnt[3]);
// fairness needs well-behaved requesters: a request is held until granted
m_hold3:  assume property (@(posedge clk) disable iff (rst) req[3] && !gnt[3] |=> req[3]);

Mutual exclusion and validity are safety rules from the invariants article. Fairness is a bounded liveness rule from the safety and liveness article. It needs the hold assumption: a requester that gives up cannot complain about not being served.

The Design: a Round-Robin Arbiter

A round-robin arbiter remembers the last requester it granted and searches the others in order, starting after that one. That way every requester gets a turn:

module rr_arb (input clk, input rst, input [3:0] req, output reg [3:0] gnt);
  reg [1:0] last;                       // index of the last granted requester
  reg [3:0] nxt;
  integer i;
  always @(*) begin
    nxt = 4'b0000;
    for (i = 3; i >= 1; i = i - 1)      // search last+1, last+2, last+3, then last itself
      if (req[(last + i) % 4]) nxt = 4'b0001 << ((last + i) % 4);
    if (nxt == 4'b0000 && req[last]) nxt = 4'b0001 << last;
  end
  always @(posedge clk)
    if (rst) begin
      gnt <= 4'b0000; last <= 2'd3;
    end else begin
      gnt <= nxt;
      if (nxt != 4'b0000) last <= 2'd0;   // bug: should remember the index of the grant
    end
endmodule

The loop runs from i = 3 down to 1, so the last match it finds is the nearest requester after last, which wins. The bug is in the pointer update: it always stores 0 instead of the requester that was granted. The search therefore always starts at requester 1, and the arbiter behaves like a fixed-priority arbiter with the order 1, 2, 3, 0.

Running It in ChipVerify Lab

In the lab form, a helper counter per requester measures how long it has waited:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // requests are held until granted
  genvar k;
  generate for (k = 0; k < 4; k = k + 1) begin : hold
    always @(posedge clk) if (!init && !$past(rst) && $past(req[k]) && !gnt[k]) assume (req[k]);
  end endgenerate
  // at most one grant, and only to a requester that asked
  always @(*) if (!init) assert ($onehot0(gnt));
  always @(posedge clk) if (!init && !$past(rst)) assert ((gnt & ~$past(req)) == 4'b0000);
  // fairness: every requester is served within 4 cycles of asking
  reg [2:0] w0 = 0, w1 = 0, w2 = 0, w3 = 0;
  always @(posedge clk) begin
    w0 <= (rst || gnt[0] || !req[0]) ? 3'd0 : w0 + 3'd1;
    w1 <= (rst || gnt[1] || !req[1]) ? 3'd0 : w1 + 3'd1;
    w2 <= (rst || gnt[2] || !req[2]) ? 3'd0 : w2 + 3'd1;
    w3 <= (rst || gnt[3] || !req[3]) ? 3'd0 : w3 + 3'd1;
  end
  always @(*) if (!init) assert (w0 <= 3'd4 && w1 <= 3'd4 && w2 <= 3'd4 && w3 <= 3'd4);
`endif

The run fails at step 6:

Requester 3 asks from step 1. The tool keeps requesters 1 and 2 busy with new requests. Because the pointer never moves, they always come first in the search, and requester 3 is granted only in step 6, five cycles after asking. The two safety rules hold in this trace: the bug is only visible through fairness.

The Fix and the Worst Case

The pointer must store the index of the granted requester:

if (nxt[0]) last <= 2'd0;
if (nxt[1]) last <= 2'd1;
if (nxt[2]) last <= 2'd2;
if (nxt[3]) last <= 2'd3;

With the fix, the run passes at depth 12. Lowering the bound in the fairness assertion measures the real worst case: a bound of 3 fails, so a requester of this arbiter can wait 4 cycles, one for each requester ahead of it in the round plus the registered grant. That number belongs in the specification of the block.

Common Mistakes