system-verilog - SystemVerilog : implies operator vs. |->

Question

最近的问题出现在通常的蕴涵运算符( |-> )和 implies 之间的区别是什么SystemVerilog 中的运算符。不幸的是，我还没有找到明确的答案。但是，我收集了以下信息:
来自 SystemVerilog LRM 1800-2012 :

§ 16.12.7 隐含和 iff 属性:

property_expr1 implies property_expr2
A property of this form evaluates to true if, and only if, either property_expr1 evaluates to false or property_expr2 evaluates to true.

§ F.3.4.3.2 派生 bool 运算符:

p1 implies p2 ≡ (not p1 or p2)

§ F.3.4.3.4 派生条件运算符:

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

但是，LRM 并没有真正指出实际差异是什么。我假设他们在错误前因(成功与空洞的成功)的情况下的评估不同，但我找不到这个假设的任何来源或证据。而且，我知道implies运算符与 OneSpin 等形式验证工具结合使用非常常见。
有人可以帮我吗？
P.S.:似乎在以下书中有这个问题的答案:SystemVerilog Assertions Handbook, 3rd Edition。但是 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);

两个蕴涵运算符只是具有不同的证明行为。属性(property)p1将通过 a ##1 b 的匹配触发并将寻找匹配的 c在与 b 相同的时钟周期内.然而，属性(property)p2由 a ##1 b 触发并将检查 c 的匹配项在a的时钟周期内.这意味着属性将通过以下场景:

属性 p1 通过而 p2 失败:

属性 p2 通过而 p1 失败:


可以在 SystemVerilog LRM 中找到此行为的提示。定义的替换是:

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

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