Why can't we use followed by instead of implication operator in SVA as the default operator?

[Orimitsu]

Hi @pkumar16 ,
followed-by operators #-#, #=# don’t mean implication. That is, signals’ behavior is evaluated at each cycle unless implication operators are added before them. Moreover, they don’t have strong attribute. Refer to the following post.

Strong and #-# of SVA

Hi, Please help. I am confused with #-# operator of SVA. I thought the following two properties were equal. // strong usage $rose(s1) |-> strong(##[0:$] ##0 $rose(s2)) // #-# operator usage $rose(s1) #-# ##[0:$] ##0 $rose(s2) However, it looks it is not correct. The following tests were applied to these properties. # === TEST 1 : ________________ # s1 : ______________| _____ # s2 : _________________________| # === TEST 2 : _______________ # s1 : ___…