【发布时间】：2016-08-28 07:10:10
【问题描述】：
以下语句之间的细微差别是什么
a -> b 与 a ##0 b
在 SVA（SystemVerilog 断言）中？
【问题讨论】：
标签： system-verilog system-verilog-assertions
【发布时间】：2016-08-28 07:10:10
【问题描述】：
您必须检查的第一件事是a |-> b 的单个蕴涵运算符的语法。
在 SystemVerilog 断言中有两个表达式。
a ##0 ba |-> b
实际上，它看起来像一个类似的表达方式。这个表达式的第一个是检查a 是否被断言(1) 并且在0 个时钟周期之后b 是否被断言(1)。第二个表达式是检查b 在断言a 时是否（打开）断言（1）然后在相同的姿势b 是否断言（1）。
现在，实际上，当验证工程师编写此类断言时，他们会处理以下事情。
-
a ##0 b：在这个表达式中，如果a没有被断言，那么它显示失败。
当a 被断言(1) 并且在同一时间戳b 未被断言时，也会显示失败。
-
a |-> b：在这个表达式中，如果a被断言并且b未被断言，那么它将显示失败。
如果a 没有被断言，那么它不会检查b 是否被断言。这种行为与a ##0 b 不同。
如果您应用不同的输入数据，那么您会看到 表达式a ##0 b 会比a |-> b 给您带来更多的失败。上面已经解释了相同的原因。
还有一点需要注意的是“蕴含构造只能与属性定义一起使用。它不能在序列中使用。”
谢谢，
阿苏托什
【讨论】：
您的问题说明了蕴涵运算符 (|->) 的重要性。这个例子使用了一个隐含运算符并且很有用：
a -> b 表示“如果a 为真，则b 应为true”（有用）。
这不是而且通常不是很有用：
a ##0 b 表示“a 和 b 在任何时候都应该为真”（不是很有用）。
【讨论】：