// SVA form of the properties (used by commercial formal tools):
//   a_onehot: assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
//   a_fair3:  assert property (@(posedge clk) disable iff (rst) req[3] |-> ##[0:4] gnt[3]);
//   m_hold3:  assume property (@(posedge clk) disable iff (rst) req[3] && !gnt[3] |=> req[3]);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module rr_arb (input clk, input rst, input [3:0] req, output reg [3:0] gnt);
  // round-robin arbiter: after a grant, the next requester in order has the highest priority
  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

`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
endmodule