An Arbiter: Exclusion, Rotation and Fairness

Prove a round-robin arbiter safe, catch a starvation bug with a bounded fairness property, and see why the proof needs k = 6.

Lesson: F8.2
Time: 20 min
Runs on: SymbiYosys
Check: 5 questions

A four-way round-robin arbiter had a clever pointer update: skip the next requester if it was idle last cycle. Every grant was one-hot and every grant went to a requester, so no single-cycle check ever fired. A requester that raised its request at the wrong moment waited a whole extra round, again and again. The random bench reported "gnt[1]: hit".

Spec sentence	Kind	The bench line	Measured
At most one grant	safety	`assert($onehot0(gnt))`	in the k = 2 proof, 0.5 s
No grant without a request	safety	`assert((gnt & ~req) == 0)`	same proof
The pointer moves past the granted index	safety (rotation)	`if (gnt_q != 0) assert(ptr == ptr_exp)`	BUG_SKIP: FAIL at reported step 3
A held request is granted within four cycles	bounded fairness (safety)	`assert(wait3 < 4)`, one counter per requester	BUG_SKIP: FAIL at reported step 6
A held request is eventually granted	liveness	`req[i] \|-> s_eventually gnt[i]`	drawn below; live mode is not run on this site yet

rr4: four requesters, combinational grant to the first requester at or after ptr. One assumption: a request stays up until it is granted.

Four Sentences, Two Kinds

The Pointer Map, and the Arrow the Bug AddsEach node is a value of ptr. A grant to requester i moves ptr to i + 1. BUG_SKIP adds the dashed jump: past i + 1 when that requester was idle last cycle.

data: where the transaction goes

Read the diagram as text

ptr = 0: grant to 0 moves it to 1
ptr = 1: grant to 1 moves it to 2
ptr = 2: grant to 2 moves it to 3
ptr = 3: grant to 3 moves it to 0
BUG_SKIP at step 1: grant to 0 jumps ptr to 2; requester 1 has just raised its request

ptr = 0 → ptr = 1: gnt 0
ptr = 1 → ptr = 2: gnt 1
ptr = 2 → ptr = 3: gnt 2
ptr = 3 → ptr = 0: gnt 3
BUG_SKIP at step 1 → ptr = 2: the extra arrow

The rotation property allows only the four solid arrows. The measured trace walks the extra one first.

Mutual exclusion and no grant without a request are one-cycle facts. Rotation says the pointer moves only along the solid arrows. Fairness says a requester that keeps asking is served within one round.

Fairness is a promise about the future, so it needs a promise from the environment too: a request stays up until it is granted (F1.3). Without that assumption a requester may give up, and no grant is owed.

Bounded Fairness Finds the Skip

Requester 1 waits a whole round

Measured with smtbmc yices: FAIL at reported step 6, 0.5 s. Requester 1 asks from step 1 and is granted only after the three others.

The bounded form counts the cycles a held request has waited and asserts the count stays under four. It is safety: it fails on a finite trace with a step number, and bmc runs it. Here it fails at reported step 6. The rotation property fails earlier, at step 3, and names the bad update directly.

Keep both. Rotation is about the implementation and debugs fast; fairness is the spec and survives a redesign of the pointer.

Liveness, and Why the Bound Is a Choice

The Same Bug at Two Depths of MeaningLeft: the bounded property fails on a finite trace. Right: a liveness counterexample is a loop that repeats forever without the grant. Drawing, not a measured trace.

Read the diagram as text

Finite prefix: reset, then requester 1 raises req
Bounded FAIL: four cycles without a grant: a step number
Lasso: a round of grants to the others, repeated forever
Liveness FAIL: no step number: the loop never ends

Finite prefix → Bounded FAIL
Finite prefix → Lasso
Lasso → Liveness FAIL: repeats forever

F3.7 runs liveness by the same rules. On this site the bounded form is what the labs run.

The liveness form, req[i] |-> s_eventually gnt[i] (A3.1), states the spec without a number. A design that grants in five cycles meets it and fails the bounded form. A real tool adds three rules. Give a live job one obligation and no safety asserts. Run s_eventually 1'b0 under the same assumptions first: it must FAIL, or a PASS may be vacuous.

Closing the Proof

Run on the fixed rr4	Measured result
Exclusion, no grant without request, rotation; prove, `smtbmc yices`	Prove PASS (k = 2), 0.5 s
Plus bounded fairness, prove k = 2	UNKNOWN at k = 2 (base case passed, induction step failed), 0.5 s
Plus bounded fairness, prove k = 4	UNKNOWN at k = 4 (base case passed, induction step failed), 0.5 s
Plus bounded fairness, prove k = 6	Prove PASS (k = 6), 0.5 s
All four, `abc pdr`	Prove PASS (abc pdr), 0.6 s
Bounded fairness only, bmc depth 20	BMC PASS to depth 20, 0.6 s

rr4 has 6 flops: ptr and last cycle's requests. The wait counters live in the bench.

The wait counters are bench state. In an induction start they may hold any value, so a short window can begin with a counter at 3 that no reset reaches. Six steps of history push that start out of reach. PDR finds the bound by itself (F2.5).

Asked in Interviews

Question	Answer
How do you write "every request is eventually granted"?	`s_eventually` in a liveness job with the hold assumption, or a bounded form in bmc when the spec gives a bound.
What is the fairness assumption here?	A requester holds its request until granted. Without it the environment can withdraw forever and no grant is owed.
How does formal find starvation?	A finite trace for the bounded form; a lasso, a loop that repeats forever, for the liveness form.

Try It

The lab task: bmc, depth 20. The twins switch the bug, the property set and the mode.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top rr4
[files]
design.sv

The property set in concurrent SVA, one line per requester where it says i. The lab runs the Imm form below.

assume property (@(posedge clk) disable iff (rst) req[i] && !gnt[i] |=> req[i]);
assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
assert property (@(posedge clk) disable iff (rst) (gnt & ~req) == 0);
assert property (@(posedge clk) disable iff (rst) gnt[i] |=> ptr == i + 1);
assert property (@(posedge clk) disable iff (rst) req[i] && !gnt[i] |-> ##[0:3] gnt[i]);

The bench as the engine runs it: registered copies stand in for $past.

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The requesters' promise: a request stays up until it is granted.
  reg [3:0] gnt_q = 0;
  always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
  reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0;   // cycles each request has waited
  always @(posedge clk) begin
    gnt_q <= rst ? 4'd0 : gnt;
    wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
    wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
    wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
    wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
  end
  reg [1:0] ptr_exp = 0;                  // where the pointer must go: past the last grant
  always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
  reg [3:0] f_seen = 0;
  always @(posedge clk) f_seen <= rst ? 4'd0 : f_seen | gnt;
  always @(posedge clk) if (!rst) begin
    assert($onehot0(gnt));                         // at most one grant
    assert((gnt & ~req) == 0);                     // no grant without a request
    if (gnt_q != 0) assert(ptr == ptr_exp);        // rotation: past the granted index
    assert(wait0 < 4 && wait1 < 4 && wait2 < 4 && wait3 < 4);   // granted within four cycles
    c_g0: cover(gnt[0]);
    c_g1: cover(gnt[1]);
    c_g2: cover(gnt[2]);
    c_g3: cover(gnt[3]);
    c_round: cover(f_seen == 4'hF && req == 4'hF);
  end

Covers
Run the cover twin. Every grant is reached at step 2; a full round at step 6.
The bug
Run as loaded: FAIL at reported step 6. Find the step where ptr jumps by two.
Fix and prove
Make the update idx + 2'd1, then prove all four properties at k = 2, 4 and 6. Which k closes?

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module rr4(input clk, rst, input [3:0] req, output reg [3:0] gnt);
  reg [1:0] ptr = 0;
  reg [3:0] req_q = 0;                    // last cycle's requests
  reg [1:0] idx;                          // the granted index
  integer i;
  always @(*) begin
    gnt = 0; idx = 0;
    for (i = 3; i >= 0; i = i - 1)        // the lowest offset from ptr wins
      if (req[ptr + i[1:0]]) begin gnt = 4'b0001 << (ptr + i[1:0]); idx = ptr + i[1:0]; end
  end
  always @(posedge clk)
    if (rst) begin ptr <= 0; req_q <= 0; end
    else begin
      req_q <= req;
      if (gnt != 0) ptr <= req_q[idx + 2'd1] ? idx + 2'd1 : idx + 2'd2;   // bug: skips a requester idle last cycle
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The requesters' promise: a request stays up until it is granted.
  reg [3:0] gnt_q = 0;
  always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
  reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0;   // cycles each request has waited
  always @(posedge clk) begin
    gnt_q <= rst ? 4'd0 : gnt;
    wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
    wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
    wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
    wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
  end
  reg [1:0] ptr_exp = 0;                  // where the pointer must go: past the last grant
  always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
  always @(posedge clk) if (!rst) begin
    assert(wait0 < 4 && wait1 < 4 && wait2 < 4 && wait3 < 4);   // granted within four cycles
  end
`endif
endmodule

Check Yourself

Predict the outputrr4 with BUG_SKIP, the hold assumption on, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0, only the bounded-fairness property. The verdict is:

module rr4(input clk, rst, input [3:0] req, output reg [3:0] gnt);
  reg [1:0] ptr = 0;
  reg [3:0] req_q = 0;                    // last cycle's requests
  reg [1:0] idx;                          // the granted index
  integer i;
  always @(*) begin
    gnt = 0; idx = 0;
    for (i = 3; i >= 0; i = i - 1)        // the lowest offset from ptr wins
      if (req[ptr + i[1:0]]) begin gnt = 4'b0001 << (ptr + i[1:0]); idx = ptr + i[1:0]; end
  end
  always @(posedge clk)
    if (rst) begin ptr <= 0; req_q <= 0; end
    else begin
      req_q <= req;
      if (gnt != 0) ptr <= req_q[idx + 2'd1] ? idx + 2'd1 : idx + 2'd2;   // bug: skips a requester idle last cycle
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The requesters' promise: a request stays up until it is granted.
  reg [3:0] gnt_q = 0;
  always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
  reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0;   // cycles each request has waited
  always @(posedge clk) begin
    gnt_q <= rst ? 4'd0 : gnt;
    wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
    wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
    wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
    wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
  end
  reg [1:0] ptr_exp = 0;                  // where the pointer must go: past the last grant
  always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
  always @(posedge clk) if (!rst) begin
    assert(wait0 < 4 && wait1 < 4 && wait2 < 4 && wait3 < 4);   // granted within four cycles
  end
`endif
endmodule

Predict the outputThe fixed rr4, all four properties, mode prove, k = 4, smtbmc yices. The verdict is:

module rr4(input clk, rst, input [3:0] req, output reg [3:0] gnt);
  reg [1:0] ptr = 0;
  reg [3:0] req_q = 0;                    // last cycle's requests
  reg [1:0] idx;                          // the granted index
  integer i;
  always @(*) begin
    gnt = 0; idx = 0;
    for (i = 3; i >= 0; i = i - 1)        // the lowest offset from ptr wins
      if (req[ptr + i[1:0]]) begin gnt = 4'b0001 << (ptr + i[1:0]); idx = ptr + i[1:0]; end
  end
  always @(posedge clk)
    if (rst) begin ptr <= 0; req_q <= 0; end
    else begin
      req_q <= req;
      if (gnt != 0) ptr <= idx + 2'd1;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The requesters' promise: a request stays up until it is granted.
  reg [3:0] gnt_q = 0;
  always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
  reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0;   // cycles each request has waited
  always @(posedge clk) begin
    gnt_q <= rst ? 4'd0 : gnt;
    wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
    wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
    wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
    wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
  end
  reg [1:0] ptr_exp = 0;                  // where the pointer must go: past the last grant
  always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
  always @(posedge clk) if (!rst) begin
    assert($onehot0(gnt));                         // at most one grant
    assert((gnt & ~req) == 0);                     // no grant without a request
    if (gnt_q != 0) assert(ptr == ptr_exp);        // rotation: past the granted index
    assert(wait0 < 4 && wait1 < 4 && wait2 < 4 && wait3 < 4);   // granted within four cycles
  end
`endif
endmodule

ConceptWhy does the bounded fairness property not replace the liveness property?

Liveness always runs faster than bmc on the same arbiter, so it is preferred.It fixes a bound the spec may not state: a five-cycle grant meets the spec and fails it.The bounded form needs no assumption about how the requesters behave.Bounded properties cannot fail on a correct design, so they prove nothing at all.

ConceptA team runs mode live with the $onehot0(gnt) assert in the same job. What goes wrong?

Exclusion becomes a liveness property and now needs a fairness assumption of its own.The tool refuses the job outright, because a live job needs at least two obligations.The live mode treats the safety assert as an assumption, so exclusion is no longer checked.The job runs both checks correctly and reports the two verdicts separately in one log.

Read the waveformIn the BUG_SKIP trace, which requester is passed over, and in which step does the pointer jump?