In reply to MLearner:
If you wanted to formally verify a rr arbiter with any number of requestors, then you don’t need to model it like above.
Instead, you can define ‘fairness’ across any 2 requestors. You let the fv tool choose any 2 random requestors. Intuitively I feel that any fairness bug can be reproduced by a failing trace using 2 requestors. So my simple-minded solution would be to use the assertion as described by Harry Foster
p_fairness: assert property(@(posedge clk) disable iff (reset)
not(req1 ##1(!gnt1 throughout gnt2[->2])));