system-verilog - 为什么在 SVA 中使用 NOT 暗示是一个坏主意？

Question

在 SystemVerilog 断言 (SVA) 中，为什么使用：

not (a |-> b)

一个坏主意？是否是由于暗示的成功方面的空洞（即，何时a不正确）？

Answer 1

是的。由于空的通行证，如果a是假的，你的财产将不会持有。

Answer 2

只有当 a 为真时，此语句才有效。如果 a 为假，则无论 b 的值是什么，断言都将返回真。