4

|->最近、通常の含意演算子 ( ) とimpliesSystemVerilogの演算子の違いは何かという疑問が持ち上がりました。残念ながら、私はまだ明確な答えを見つけることができませんでした。ただし、次の情報を収集しました。

SystemVerilog LRM 1800-2012から:

  • § 16.12.7 Implies および 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

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

を使用する 2 番目の形式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 に答える