SVA for checking fairness of Round-Robin Arbiter

In reply to imajeeth:

I think this is not a scalable solution. In my case, there were 16 requestors. Here was my approach:
1 - Assume that req[15:0] and gnt[15:0] is vector of request and grant signals.
2 - Check these properties:
a - $onehot0(gnt)
b - gnt [i] |-> req [i] in which i was generated by “generate” statement from 0 to 15 for all requestors.
c - Developed a function called rr_scheme in which updated the “pivot” (if req[i] & gnt[i] then pivot = i) and returned the expected gnt vector (in my case, expected gnt = the very first req[i] with i > pivot or very first req[i] from req[0] if there was no req[i] with i > pivot). The last assertion compared gnt with rr_scheme returned.

Sorry that I don’t have the code right now.