SVA : Property is a tautology

In reply to ben@SystemVerilog.us:

@sharvil11 and Ben Cohen
Thanks for the solution.

I have one query here. If a req doesn’t get grant at end of simulation, it will be flagged as failure.
But how will a formal tool treat this case ? Can it fail this property and provide a trace because it can still be said that grant may occur in future.

Regards,
Vivek