system-verilog - SVA中的暗示（->）和##0有什么区别？

Question

以下陈述之间的细微差别是什么

a -> b对比a ##0 b

在 SVA（SystemVerilog 断言）中？

Answer 1

您必须检查的第一件事是单个蕴涵运算符的语法，即a |-> b.

在 SystemVerilog 断言中有两个表达式。

1. a ##0 b
2. a |-> b

实际上，它在表达上看起来很相似。这个表达式的第一个是检查a是否断言（1）和在 0 个时钟周期之后b断言（1）与否。第二个表达式是在断言（1）b时检查是否（打开）断言，a然后在同一姿势b上断言（1）或不断言。

现在，实际上，当验证工程师编写这种断言时，他们会处理以下事情。

1. a ##0 b：在此表达式中，如果a未断言，则表示失败。

何时a断言（1）并且在同一时间戳b上未断言，则也显示失败。

2. a |-> b：在此表达式中，如果a已断言b且未断言，则将显示失败。

如果a未断言，则不会检查是否b已断言。这种行为不同于a ##0 b.

如果您应用不同的输入数据，那么您可以看到该表达式a ##0 b会给您带来比a |-> b. 上面已经解释了相同的原因。

还要注意的另一件事是“蕴涵构造只能与属性定义一起使用。它不能在序列中使用。”

谢谢，

阿舒托什

Answer 2

您的问题说明了蕴涵运算符( |->) 的重要性。这个例子使用了一个隐含运算符并且很有用：

a -> b意思是“如果a是真的那么b应该是true”（有用）。

这不会而且通常不是很有用：

a ##0 b意思是“a并且b在任何时候都应该是正确的”（不是很有用）。

https://www.edaplayground.com/x/47iN