In reply to foxtrot:
WHy do you think that the following will not work?
assert property (@(posedge clk) req |-> s_eventually gnt);
Also, when you say gnt comes at positive duty cycle, you mean in the middle of a cycle. But will it miss the clk sampling @(posedge clk)? If so, you’ll need to latch the gnt so that it can be sampled.
Note that the following solution could work.
assert property (@(posedge clk) req |-> @ (posedge gnt) 1'b1);
In general, SVA is used with clocking event s sampling data. The above uses the gnt as a clocking event; it is an unusual solution.
Ben