// 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