4

|->最近出现了一个问题，通常的蕴涵运算符 ( ) 和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 Assertions Handbook, 3rd Edition。但是仅仅为了得到这个问题的答案，155 美元对我来说有点太多了 :)

4

2 回答 2

5

我认为还有一个更显着的区别。假设我们有以下示例：

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寻找匹配。但是，属性由 触发并将在 的时钟周期内检查是否匹配。这意味着属性将在以下情况下通过：cbp2a ##1 bca

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

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

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

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

于 2014-07-31T13:02:56.543 回答
2

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

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

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

第一种形式 using|->不编译：

// 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没有成功，则发出失败。

于 2014-07-23T14:44:11.367 回答