Lab: properties for a round-robin arbiter

// rr_arbiter.sv — N-way round-robin arbiter, combinational grant
module rr_arbiter #(
  parameter int N = 4
) (
  input  logic         clk,
  input  logic         rst,
  input  logic [N-1:0] req,
  output logic [N-1:0] gnt
);
  localparam int PW = (N > 1) ? $clog2(N) : 1;
  logic [PW-1:0] ptr;                    // requester with the highest priority

  // Grant the first requester at or after ptr (wrapping around)
  always_comb begin
    gnt = '0;
    for (int k = N - 1; k >= 0; k--) begin   // lowest k wins: last assignment sticks
      if (req[(int'(ptr) + k) % N]) begin
        gnt = '0;
        gnt[(int'(ptr) + k) % N] = 1'b1;
      end
    end
  end

  // After a grant, the requester just after the winner gets top priority
  always_ff @(posedge clk) begin
    if (rst) begin
      ptr <= '0;
    end else begin
      for (int i = 0; i < N; i++)
        if (gnt[i]) ptr <= PW'((i + 1) % N);
    end
  end
endmodule

// rr_arbiter_fv.sv — formal wrapper with assumptions, assertions and covers
module rr_arbiter_fv #(
  parameter int N = 4
) (
  input logic         clk,
  input logic         rst,
  input logic [N-1:0] req
);
  logic [N-1:0] gnt;
  rr_arbiter #(.N(N)) dut (.*);

  initial assume (rst);                       // traces start in reset
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // ---------------------------------------------------------- environment
  for (genvar i = 0; i < N; i++) begin : g_env
    // (5) a pending request is held until granted
    m_req_held: assume property (req[i] && !gnt[i] |=> req[i]);
  end

  // ---------------------------------------------------------- checks
  a_onehot:        assert property ($onehot0(gnt));                 // (1)
  a_work_conserve: assert property (|req |-> |gnt);                 // (3)

  for (genvar i = 0; i < N; i++) begin : g_chk
    a_gnt_has_req: assert property (gnt[i] |-> req[i]);             // (2)
    a_fair:        assert property (req[i] |-> ##[0:N-1] gnt[i]);   // (4)

    // ---------------------------------------------------------- covers
    c_gnt:         cover property (gnt[i]);                          // (6)
    c_wait_max:    cover property ((req[i] && !gnt[i]) [*N-1] ##1 gnt[i]);
  end

  c_back_to_back:  cover property (gnt[0] ##1 gnt[1]);
endmodule

# rr_arbiter.sby
[tasks]
prove
cover

[options]
prove: mode prove
cover: mode cover
depth 12

[engines]
prove: abc pdr
cover: smtbmc

[script]
read -formal rr_arbiter.sv rr_arbiter_fv.sv
prep -top rr_arbiter_fv

[files]
rr_arbiter.sv
rr_arbiter_fv.sv