Fairness Assumptions for Progress Proofs

On this page

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

Why it matters

A progress proof without fairness assumes nothing about the environment: the downstream may stall for ever, and the proof fails on an infinite stall the design cannot prevent. A proof with a careless assumption can do worse: it passes because the assumption quietly forbids the behaviour that would expose the bug. Fairness is the line between the two, and it belongs in a register with an owner, not in a comment.

The core idea

Assume only on the environment's choices, never on the design's outputs: the downstream may stall but not for ever, the requester may pause but the proof states what it keeps. Bound the assumption with a number derived like any other bound, document assumption, bound, owner and where it is checked, in one register, and check it twice: a cover shows the assumption still allows real traffic, and simulation shows the assumed behaviour actually occurs. The assumption used here is a bound on consecutive stalls, which is a safety constraint, stronger than fairness in the infinitely-often sense; true liveness would need the weaker constraint and a liveness engine. A constraint on a design output, or one so strong it excludes the victim, hides starvation by construction.

Assumption	Environment signal	Bound	Owner	Checked by
downstream holds a beat for at most two consecutive stalled cycles (two-stage chain and the crossing check)	`out_ready` (and `dst_ready`)	2 cycles	downstream block owner	stall cover, an assertion on the downstream block, a bench test
arbiter requesters	none	none: the bound of 3 needs no assumption	-	contention cover shows full contention is reachable

Worked example: the assumption still allows traffic, and what it is for

The two-stage chain from the previous lesson carries the documented stall bound. The cover run shows the assumption still allows real traffic: a beat flows through, and a two-cycle stall followed by a drain is reachable. The second block removes the assumption altogether: the correct chain then fails its progress bound, because the downstream may stall for ever. That failure is why the assumption exists, and it is the same bound the previous lesson derived, so it must be written down and owned:

chain2.sv

// formal: cover 10 expect reached slang top chain2
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

chain2.sv

// formal: bmc 12 expect fail slang top chain2 define FAIR=2
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

Step	in_valid	v1	v2	age	Outcome
1	1	0	0	0	beat accepted
2	1	1	0	0	beat moves to stage 2
3	0	0	1	1	downstream stalled
4	1	0	1	2	still stalled
5	0	1	1	3	still stalled
6	1	1	1	4	counterexample: `p_age` fails, the downstream never drains

Worked example: the too-strong version

Two over-strong forms show how the same cover catches them. First, assume the downstream is always ready: the progress proof passes, but the two-cycle stall cover is not reached within 10. That is inconclusive on its own, and here the reason is known: the assumption removed the stalls. The proof is true and tells you nothing about stalled traffic:

chain2.sv

// formal: prove 4 expect pass slang top chain2 define FAIR=1
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

chain2.sv

// formal: cover 10 expect fail slang top chain2 define FAIR=1
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

Second, on the arbiter, an assumption that looks like fairness but is exclusion: requester 3 never requests. The cover for the grant of requester 3 is not reached within 6, and a cover not reached within a bound is inconclusive. Here the reason can be proved, not only suspected: a grant implies a request (a_no_phantom in the arbiter lesson is inductive), so with the request removed the grant is impossible, and the assertion that grant 3 never happens is proven. The assumption removed the victim instead of bounding the environment. Without the assumption the same assertion fails, because requester 3 is granted in the open arbiter:

rr_arbiter.sv

// formal: cover 6 expect fail slang top arbiter_closed
`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

module arbiter_closed #(parameter EXCLUDE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  rr_arbiter u_arb (.clk(clk), .rst(rst), .req(req), .grant(grant));

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init && EXCLUDE != 0) assume (!req[3]);   // looks like fairness, is exclusion

  always @(*) if (!init) begin
    a_g3_never:  assert (!grant[3]);
    c_g3_served: cover (grant[3]);
  end
`endif
endmodule

rr_arbiter.sv

// formal: prove 4 expect pass slang top arbiter_closed
`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

module arbiter_closed #(parameter EXCLUDE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  rr_arbiter u_arb (.clk(clk), .rst(rst), .req(req), .grant(grant));

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init && EXCLUDE != 0) assume (!req[3]);   // looks like fairness, is exclusion

  always @(*) if (!init) begin
    a_g3_never:  assert (!grant[3]);
    c_g3_served: cover (grant[3]);
  end
`endif
endmodule

rr_arbiter.sv

// formal: bmc 6 expect fail slang top arbiter_closed define EXCLUDE=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

module arbiter_closed #(parameter EXCLUDE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  rr_arbiter u_arb (.clk(clk), .rst(rst), .req(req), .grant(grant));

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init && EXCLUDE != 0) assume (!req[3]);   // looks like fairness, is exclusion

  always @(*) if (!init) begin
    a_g3_never:  assert (!grant[3]);
    c_g3_served: cover (grant[3]);
  end
`endif
endmodule

The open arbiter, with no assumption at all, reaches every grant and full contention, which is why its register row says none:

rr_arbiter.sv

// formal: cover 6 expect reached slang top arbiter_open
`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

module arbiter_open (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  rr_arbiter u_arb (.clk(clk), .rst(rst), .req(req), .grant(grant));

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    c_any_grant:   cover (|grant);
    c_all_contend: cover (req == 4'b1111);
    c_g3_served:   cover (grant[3]);
  end
`endif
endmodule

What the review looks for

Every fairness assumption names the environment signal it constrains, never a design output.
The register lists bound, owner and check location, and each entry has a reachable cover.
A too-strong assumption is detectable: excluding a requester or a stall empties its covers, which fail signoff.
The register says which bounds are safety constraints and what true liveness would still need.

Verify and debug

Read the assumption list before the proof result: an assumption on a design output invalidates the proof regardless of the verdict. Then read the covers: an assumption that empties a cover has excluded behaviour, not bounded it. Confirm each fairness assumption in simulation with a test that exercises the bounded behaviour, and assert it on the neighbour. The assumption background is in the property-development lessons.

Check yourself An assumption says the downstream stalls at most two cycles. The cover for a four-cycle stall is unreachable. Is the proof stronger or weaker?

Neither yet: the assumption may legitimately exclude four-cycle stalls, but only if the neighbour guarantees two. Find that guarantee as an assertion on the neighbour, or the proof rests on an undischarged promise.

Navigate

Why it matters

The core idea

Worked example: the assumption still allows traffic, and what it is for

Worked example: the too-strong version

What the review looks for

Verify and debug

Related topics

Fairness Assumptions for Progress Proofs

Why it matters

The core idea

Worked example: the assumption still allows traffic, and what it is for

Worked example: the too-strong version

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: the assumption still allows traffic, and what it is for

Worked example: the too-strong version

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: the assumption still allows traffic, and what it is for

Worked example: the too-strong version

What the review looks for

Verify and debug

Related topics

Up next