gnt ##1 ack

The most common SVA misconception, is the way engineers tend to interpretate the delay (##) operator.
Consider the following assertions:

a_gnt_delay_ack : assert property ( @(posedge clk) gnt ##1 ack );
a_gnt_delay_ack_imp1 : assert property ( @(posedge clk) gnt ##1 ack -> 1);
a_gnt_imply_ack : assert property ( @(posedge clk) gnt => ack );

The following image show how they function in a certain scenario:

The image shows that @ 740 a_gnt_delay_ack fail. The reason is that the simulator holds 2 "threads" of this assertion at time 740. The first thread started at time 720, and it ended with great success. The second thread started at time 740, and immidiately ended with failiure (since gnt == 0 at 740). The assertion result is build from a "superposition" of all active threads at the given time. And since assertion mechanism was built to detect failures, the assertion result is fail.

The assertion, a_gnt_delay_ack_imp1, is useful only to illustrate how the 2 threads are handled, when they appear in the antecedent part on an implication construct. The image shows success @ 740. The reason is that here the 2 threads cause a success of the property. The first thread, cause a real success. The second thread cause a vacuous success.

The assertion a_gnt_imply_ack, implements the "most reasonable intent". One clock after gnt is up, expect ack to be 1.