Strong and #-# of SVA

[Orimitsu]

Thanks @ben2 ,

I understand that #-#, #=# don’t have meaning of implication unlike |->, |=>. Therefore, the check is done at every clock. A few articles says no vacuous pass with followed-by operator, #-#, #=#. But they are NOT implication property. So, check is done at every clock unless there is implication before them. Therefore, no vacuous pass in that sense. I misunderstood it and I thought strong attribute can be applied with #-#. I guess the person who created the following post made the same misunderstanding as me.

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

Hey All , I am having some trouble understanding why we would use the implication operator which can lead to vacuous passess when instead we have the ollowed by operator in SVA ? Isn’t the whole point of adding an assertion is to check for both antecedent & consequents to be satisfied in the assertion? Why is implication still used ? EDIT: I think I should also add on to the point that this is specifically in a properly where we check for the antecdent to be true to evaluate the consequent sho…

Usually, #-# is used to combine two properties as follows.

A |-> B #-# C |-> D

And, I think this is equivalent to the following two properties.

A |-> B
A ##0 B ##0 C |-> D

In this sense, followed-by operators are different from simple concatenation of implication.

A |-> B |-> C |-> D

is equal to

A |-> B
A ##0 B |-> C
A ##0 B ##0 C |-> D

I believe my understanding is correct now.