1

次のステートメントの微妙な違いは何ですか

a -> b対a ##0 b

SVA (SystemVerilog アサーション) で?

4

2 に答える 2

2

最初に確認する必要があるのは、単一の含意演算子の構文ですa |-> b。

SystemVerilog アサーションには 2 つの式があります。

  1. a ##0 b
  2. a |-> b

実は、表情が似ています。この式の最初のチェックaは asserted(1) で、0 クロック サイクル後にbasserted(1) かどうかをチェックします。2 番目の式は、bis (on) asserted がaasserted(1) の場合にチェックされ、次に同じ posedgebが asserted(1) であるかどうかがチェックされます。

実際、検証エンジニアがこの種のアサーションを書くとき、彼らは次のことを処理します。

  1. a ##0 b:この式aで がアサートされていない場合、失敗を示します。

がアサートされている場合a(1) で、同じタイム スタンプbがアサートされていない場合も失敗を示します。

  1. a |-> b: この式では、aがアサートされ、 がアサートされbていない場合、失敗が表示されます。

がアサートされていない場合aは、アサートされているかどうかをチェックbしません。この動作は とは異なりa ##0 bます。

異なる入力データを適用すると、式a ##0 bがより多くの失敗をもたらすことa |-> bがわかります。同じ理由はすでに上で説明されています。

もう 1 つ注意すべき点は、「含意構文はプロパティ定義でのみ使用できます。シーケンスでは使用できません」です。

ありがとう、

アシュトシュ

于 2016-08-28T08:23:55.563 に答える
1

あなたの質問は、含意演算子( |->) の重要性を示しています。この例では、含意演算子を使用しており、便利です。

a -> ba「が true のb場合true」 (便利)を意味します。

これは役に立ちませんし、通常はあまり役に立ちません:

a ##0 b「常に真である必要があります」aを意味bします (あまり役に立ちません)。

https://www.edaplayground.com/x/47iN

于 2016-08-28T08:27:53.340 に答える