以下陈述之间的细微差别是什么
a -> b对比a ##0 b
在 SVA（SystemVerilog 断言）中？
问问题
4188 次
2 回答
2
您必须检查的第一件事是单个蕴涵运算符的语法，即a |-> b.
在 SystemVerilog 断言中有两个表达式。
a ##0 ba |-> b
实际上，它在表达上看起来很相似。这个表达式的第一个是检查a是否断言（1）和在 0 个时钟周期之后b断言（1）与否。第二个表达式是在断言（1）b时检查是否（打开）断言，a然后在同一姿势b上断言（1）或不断言。
现在，实际上，当验证工程师编写这种断言时，他们会处理以下事情。
a ##0 b：在此表达式中，如果a未断言，则表示失败。
何时a断言（1）并且在同一时间戳b上未断言，则也显示失败。
a |-> b：在此表达式中，如果a已断言b且未断言，则将显示失败。
如果a未断言，则不会检查是否b已断言。这种行为不同于a ##0 b.
如果您应用不同的输入数据，那么您可以看到该表达式a ##0 b会给您带来比a |-> b. 上面已经解释了相同的原因。
还要注意的另一件事是“蕴涵构造只能与属性定义一起使用。它不能在序列中使用。”
谢谢，
阿舒托什
于 2016-08-28T08:23:55.563 回答
1
您的问题说明了蕴涵运算符( |->) 的重要性。这个例子使用了一个隐含运算符并且很有用：
a -> b意思是“如果a是真的那么b应该是true”（有用）。
这不会而且通常不是很有用：
a ##0 b意思是“a并且b在任何时候都应该是正确的”（不是很有用）。
于 2016-08-28T08:27:53.340 回答