System verilog assertion for round robin arbiter

HI Ben,

https://verificationacademy.com/forums/systemverilog/round-robin-assertion

I went through above link, thanks for the detailed info.

My query : After REQ, GNT should be asserted in the next clock cycle (REQ |=> GNT)

Now, REQ1 and REQ2 asserted in the same clock cycle.
So, GNT1 will come at 2nd clock cycle and GNT2 will come in 3rd clock cycle.
After GNT1 going low, GNT2 must be asserted

ap_grnt1_after2: assert property(@(posedge clk)
REQ1 |=> GNT1 |=> !GNT1 && GNT2;
endproperty

May I know my code is fine or does it requires any modification?

In reply to Mahesh K:
I don’t have the time to review this, it was too long ago.
I also wrote a paper that might be useful to you.
9. SVA for statistical analysis of a weighted work-conserving
prioritized round-robin arbiter
SystemVerilog can perform statistical analysis of computer systems, though it is rarely used in this
manner. That kind of performance analysis is very important because it reaffirms the needed
system-level requirements.

http://systemverilog.us/vf/arbiterv422.sv

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.