system-verilog - SVA: 含意 (|=>) とシーケンスの使用?

Question

|=>SystemVerilog アサーション プロパティは、含意演算子とシーケンスを使用して構築できます##1

例えば ​​：

property P1;
  @(posedge clk)
    A ##1 B |=> C ##1 D;
endproperty

上記ではA ##1 B、有効化シーケンス (前件) および実現シーケンス (後件) として使用しましたC ##1 D。

次のように書き換えられなかった理由がわかりません。

property P2;
  @(posedge clk)
    A ##1 B ##1 C ##1 D;
endproperty

|=>シーケンスよりも含意を選択するのはいつ、そしてなぜ##1ですか?

Answer 1

上記のプロパティはシーケンス パスと同じですが、失敗条件は一致しません。

それらがすべて 1 の場合A ##1 B ##1 C ##1 D;、A ##1 B |=> C ##1 D;真です。

A が 1 の場合、残りの 0 は次のようになります。

A ##1 B ##1 C ##1 D;失敗し、A ##1 B |=> C ##1 D;合格します。

後者は、有効化シーケンスの条件が満たされていないため、失敗とは見なされません。