Round robin assertion

Hey Ben thanks for taking time to reply.
Just to make sure we both are in same page and understanding same. I still feel that my code works good for round robin.

To clarify any confusion in the problem, i will write it down below,

Problem statement:
Even though i have considered 16 variables in my solution for understanding purpose lets consider 4 variable round robin arbitrator,
A = req[0], B = req[1], C = req[2], D = req[3]
grant should be cyclic: A → B → C → D → A . . .
if all the request is preset then grant follows above order, if not then it will grant the next available request in the cyclic order i.e if C - request is absent then it will follow this order, A → B → D → A → . .

Here we also assume that we give only 1-grant clk tick to serve the request.
So for the above problem i feel my solution will work and i don’t think we need to keep a track of request and grant sequence in round-robin fashion.
In my solution, variable ‘i’ will keep a track of request in order and ‘j’ will track the grant, i don’t think we need to keep a track of previous grant in this case.

Please correct me if i’m missing out anything.

Or any good example in which my solution fails will be good to get a better solution and cover the corner cases

assert property
        (
          @posedge clk
          (gnt[i] && req[j]) |=> (gnt[j] && !req[j]) // Sorry i had made a mistake !req[j] variable which i have corrected
        )