問題タブ [system-verilog-assertions]

非同期リセットを使用した広告フリップフロップの簡単な例を見てみましょう。

q は、クロックの次のエッジで d で更新する必要があります。これは、単純な含意演算子アサーションで記述できます。

ただし、アサーションでリセット動作をキャプチャする方法。私はいくつかをフォローしようとしました

これらのアサーションは両方とも失敗します。最初の次のポーズエッジがないためだと思いますか?

パスしますが、フリー ランニング クロックが必要で、クロックの 2 つのエッジ間でアサートされます (最初の意図した動作ではありません)。

私の理解では、これは正しい即時アサーションですが、波形ビューアーでこれが成功または失敗することはわかりません。さらに、最後のタイプのアサーションについてはカバーを書くことができないと思います。

以下のようにプロパティをチェックするSVアサーションがあります

以下のような主張があります。

ここでのシナリオは、前件が真であり、後件が 1 ～ 100 クロック サイクルの間でチェックされるというものです。前例の後、クロック ゲーティングによりクロックがしばらく停止し、その後、クロックは再びカチカチと動き始めます。信号my_prio[rx_prio]は、クロック ゲーティングの後、100 クロック サイクル以内に再びアサートされます。しかし、私はまだアサーションの失敗を取得します。

失敗の問題を理解することができません。アサーション チェック間のクロック ゲーティングに問題はありますか? または他の理由の失敗？ありがとう。

以下に示すように、アサーションのシーケンスで絶対遅延を指定することは可能ですか?

これは確かにコンパイルされません。しかし、クロックサイクルではなく遅延のアサーションを書きたいときに、そのような状況に対処する方法を知りたかっただけですか?

例: 2 つのクロック間のスキュー関係をチェックするアサーションを書きたいですか? スキューがたとえば 5 ps を超えたときにアサーションを起動するように指定するにはどうすればよいですか?

「clk」の立ち上がりエッジで信号が遷移する場合にのみ起動するアサーションを作成しようとしています。私は自分のアイデアをテストするために以下のコードを書きました

上記のコードは、VCS で次の出力を返します。

「d」が時間 150 まで安定していたのに、時間 100 でアサーションが発生したのはなぜですか?

私は以下のようなSVプロパティを持っています:

以下のような主張があります。

上記のプロパティには、チェック全体でアサートされるべきではない信号s_ofがあります。しかし、ここでのシナリオは、この信号s_ofが含意演算子の結果の間にアサートされているということです。したがって、結果ステートメント中にシグナルs_ofがアサートされた場合でも、チェックを無効にする必要があります。これを達成する方法はありますか？

ありがとう。

|->最近、通常の含意演算子 ( ) と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 ドルは私には少し多すぎます :)

私は Verilog の初心者です (もちろん SystemVerilog も)。その機能をテストする RTL モジュールがあります。モジュールを再利用できるように、刺激を適用してから観察するのではなく、アサーションを使用してそれを実行しようとしていました..

とにかく、私の主張は次のようになります。

この場合、read_enable_pulseモジュール内部の信号があり、

バインドせずにテストベンチレベルから見たいと思います（方法も正確にはわかりません）。

testbenchmodule.mymodule.read_enable_pulse階層をくぐる場所に入れてみましread_enable_pulseたがうまくいかないようです..

誰でもこれを行う方法を知ることができますか?