SystemVerilog：暗示操作员与 |->

Question

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

来自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 等形式验证工具结合使用非常常见。

谁能帮帮我？

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);

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

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

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

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

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

Answer 2

我试过了，显然|-> 不允许用于属性（仅用于序列和布尔表达式）。这是我尝试过的：

  property a_and_b;
    @(posedge clk)
    a && b;
  endproperty

  property a_and_c;
    @(posedge clk)
    a && c;
  endproperty

使用|-> 的第一个表单无法编译：

// this doesn't compile
assert property(a_and_b |-> a_and_c);

使用implies 的第二种形式确实可以编译：

// this does compile
assert property(a_and_b implies a_and_c);

语义方面，它与|-> 运算符一样。当a_and_b 失败时，断言空洞地通过。如果a_and_b 成功但b_and_c 没有成功，则发出失败。