SystemVerilog：隐含运算符与|->

Question

最近出现了一个问题，通常的隐含运算符（|->）和impliesSystemVerilog中的运算符之间有什么区别。不幸的是我找不到一个明确的答案。但是，我收集了以下信息：

从SystemVerilog LRM 1800-2012：

• 第16.12.7节隐含和iff属性：

  property_expr1 implies property_expr2
  仅当property_expr1的值为false或property_expr2的值为true时，此形式的属性的值为true。

• §F.3.4.3.2 派生布尔运算符：

  p1 implies p2 ≡ (not p1 or p2)

• §F.3.4.3.4 派生的条件运算符：

  (if(b) P) ≡ (b |-> P)

但是，LRM并未真正指出实际的区别是什么。我假设在错误的先行情况下（成功与空前成功），它们的评估有所不同，但是我无法找到此假设的任何来源或证据。此外，我知道implies操作员与OneSpin等正式验证工具结合使用非常普遍。

有人可以帮我吗？

PS：似乎在下一本书中对此问题有一个答案：SystemVerilog断言手册，第三版。但是155美元对我来说太过分了，只是为了得到这个问题的答案:)

Answer 1

我认为甚至还有更大的不同。假设我们有以下示例：

property p1;
  @ (posedge clk) 
  a ##1 b |-> c;
endproperty

property p2;
  @ (posedge clk) 
  a ##1 b implies c;
endproperty

assert property (p1);
assert property (p2);

两个蕴涵运算符只是具有不同的证明行为。属性p1将通过匹配触发，a ##1 b并c在与相同的时钟滴答中寻找匹配b。但是，属性p2由触发，a ##1 b并将c在的时钟周期内检查是否匹配a。这意味着这些属性将在以下情况下通过：

属性p1通过而p2失败： 属性p2通过而p1失败：

在SystemVerilog LRM中可以找到有关此行为的提示。定义的替换为：

(if(b) P) = (b |-> P)
p1 implies p2 = (not p1 or p2)

因此，总而言之，如果使用隐含运算符，则定义多循环操作将变得更加容易，因为前提和结果具有相同的评估起点。