Why is using NOT with implication a bad idea in SVA?

2
votes

In SystemVerilog Assertions (SVA), why is using:

not (a |-> b)

a bad idea? Is it due to the vacuous success aspect of the implication (i.e., when a is not true)?

2
system-verilogsystem-verilog-assertions

2 Answers

0
votes

Yes. Due to the vacuous passes, if a is false your property will not hold.

0
votes

This statement would work only if a is true. If a is false then the assertion will return true irrespective of what the value of b is.