You need to be more specific what you mean by “when req is present” and
“gnt should come”. Usually this means when the signal first gets asserted or rises (if active high).
It is a bad coding style to use an implication operator in cover-s - for the exact reason as you’ve experienced, these are called vacuous successes in SVA and a cover usually does not differentiate between vacuous and non-vacuous. For cover - 2 approaches:
Your simulator may already do this internally, check for flags
Rewrite without implication operator, just use ##4 in your example
Here, 1 and 2 are performing the same functionality.
2nd may not be required in this context.
In general, when to write cover property.
For example, If it is FIFO, then “buffer can get FULL and then empty again”. For this requirement, I can use cover instead of assert since FULL followed by EMPTY involves many write operations followed by read, so basically when there is some sequence is involved, we will choose “cover” instead of “assert”.
In this Arbiter example, I was not able to think where “cover” can be used becuase I do not see any sequence. If possible, can you give one best example for cover in any generic arbiter.