In reply to hisingh:
(a) When you negate a property, you switch its strength. (16.12.3 Negation property). Since the consequent is now strong, an incomplete property fails. To get the behavior you expected, write it as
@( posedge clk ) $rose( req ) |=> not strong (!ack[*1:$] ##1 $rose( req ) ) ;
(b) There are two assertion attempts, one starting at time 5, and the other starting at time 45. There is no strength involved in the first attempt, all tools agree it should fail. But since the second attempt begins on the last clock cycle and you are using non overlapping implication, the consequent never begins evaluations, so it is incomplete.
We normally recommend only using the overlapping implication to avoid confusion and writ the property as
@( posedge clk ) $rose( req ) |-> not strong((##1 !ack[*1:$] ##1 $rose( req ) ) ;
If you add a pass message to the assert statement
a_property : assert property ( strictly1ack ) $info(“pass”,$time); else $error(" TIME : %2t STRICTLY1ACK FAIL " , $time , ) ;
You see that the tool that printed the passing message for the cover directive does not print a passing message for the assert directive. That is a contradiction and incorrect behavior.