問題タブ [system-verilog-assertions]

次のポーズエッジが完了してから 4 サイクル後に req が高くなるというアサーションを書きたいと思います。私にとって、リセット時の完了はすでに高いです。完了の次のポーズエッジでリクエストを高くするにはどうすればよいですか。assert property {$rose(done) |-> ##4 req}しかし、なぜそれが機能しないのかわかりません。誰でも助けてもらえますか？

私はsystemverilogとSVAを初めて使用し、prbsジェネレーターのアサーションを作成して、特定の配列（logic [6:0]）を127クロックサイクル後の同じ配列と比較しようとしています。問題は、配列の比較に役立つとわかった演算子は同時実行を許可せず、同時実行を許可する演算子はビットのみで動作することです。

私がやりたかったことを例示しようとすると、次のようになります。

SystemVerilog Assertions (SVA) で、なぜ使用するのか:

悪い考えですか？それは含意の空虚な成功の側面によるものですか (つまり、a真でない場合)?

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

a -> b対a ##0 b

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

次のようなプロトコルがあるとします。マスターが に設定reqされるfillと、スレーブは を介し​​て 4 つの転送を通知しrspます。

このトランザクション全体の SVA シーケンスは次のようになります (スレーブがidleサイクル間にtransサイクルを挿入できると仮定)。

ここで、マスターがリクエストのパイプライン処理を許可されているとします。これはfill、4transサイクルが完了する前に次のサイクルを開始できることを意味します。

上記の SVA シーケンスは役に立ちません。2 番目はfill4 サイクルと誤って一致transし、最後のtrans「フローティング」のままになるからです。trans前のサイクルが一致した後にのみ、一致するサイクルを開始する必要がありfillます。

シーケンスには、単一の評価では利用できないグローバル情報が必要です。基本的に、別のインスタンスが実行されていることを知る必要があります。これを実装する唯一の方法は、RTL サポート コードを使用することです。

上記のコードは、トランザクションの進行中にビットを上げ、aの最後のトランザクションが送信されたときにクロック サイクルtrans_ongoingでパルスします。(私はそれをテストしていないのですべきだと言いますが、これはポイントではありません。それが機能すると仮定しましょう。)trans_donetransfill

このようなものがあると、シーケンスを次のように書き換えることができます。

これで問題なく動作するはずですが、サポート コードが必要であるという事実に特に感心しているわけではありません。基本的に、トランザクションとは何か、パイプラインがどのように機能するかについてかなりの部分を再説明したため、これには多くの冗長性があります。また、再利用も容易ではありません。をパッケージに入れて、別のsequence場所にインポートできます。サポート コードは、一部のモジュールに配置して再利用することしかできませんが、シーケンスを格納するパッケージとは異なる論理エンティティです。

ここでの問題は、サポート コードを必要とせずにパイプライン化されたバージョンのシーケンスを記述する方法はないかということです。

と の 2 つのプロパティが与えられた場合、とP1 = (R1 or R2) |-> Pはシーケンスではプロパティですが、は と同等であると言うのは正しいですか?P2 = (R1 |-> P) or (R2 |-> P)R1R2PP1P2

LRM の附属書 F のタイト充足可能性とニュートラル充足可能性の定義に基づいて計算を行ったところ、同等であることがわかりました。(どこかで間違いを犯す可能性を排除したくありません。)

シミュレーション ツールでこの 2 つが異なる方法で処理されているのを見たことがあるので、質問します。

SystemVerilog アサーションを勉強しています。Valid-ack仕様を確認するためにSVAを適用しました。スペックは以下の通りです。

valid が駆動される (0 から 1) 場合、ack が駆動される (1) まで、valid は 1 に等しい必要があります。ack がディアサートされると (1 から 0)、valid もディアサートされます (1 から 0)。

この仕様を確認するために、2 つのプロパティ (pr1 と pr2) を書きました。以下のリンクから SVA コードを確認できます。 https://www.edaplayground.com/x/5gHd

2 つのプロパティがまったく同じように機能することを期待していました。ただし、pr2 は期待どおりに機能しません (valid は 1 に等しいが ack は 50ns で 0 に等しいため、50ns でアサーションが失敗する可能性があると予想していました)。

波形： https ://www.edaplayground.com/w/x/u5

pr2 (50ns) で何が間違っていますか?

よろしくお願いします、

triggeredシーケンスのプロパティを使用するアサーションがいくつかあります。これは、「X が発生した場合、Y は過去に発生したに違いない」という形式のプロパティをチェックするのに役立ちます。

簡単な例を見てみましょう：

3 つの信号 、および が与えられaたb場合、3 サイクル前に High であり、2 サイクル前に High であった場合にのみc、cHigh になることが許可されます。これは、このプロパティを満たすトレースです。ab

cこれを確認できるようにするには、 aが有効なポイントで一致するヘルパー (クロック付き) シーケンスが必要です。

次に、このシーケンスをアサーションで使用できます。

このアサーションはほとんどの場合問題なく機能しますが、リセットを処理するときはうまくいかなくなります。

と の間のクロック サイクルで正確にアクティブになるリセット信号もあるとしbますc。

この場合の素朴なアプローチは、アサーションの外側、default disable iff節の内側にリセット認識を実装することです。

cリセットは の前にアクティブだったので、前にa ##1 b発生した はカウントされず、アサーションが失敗することが予想されます。ただし、シーケンスの評価はリセットとは無関係であるため、これは起こりません。

この動作を実現するには、シーケンスをリセット対応にする必要があります。

アサーションはリセット対応バージョンを使用する必要があります。

two_cycles...リセットの発生によりシーケンスが一致しないため、2 番目のアサーションは実際に失敗します。

これは明らかに機能しますが、より多くの労力が必要であり、スコープごとに制御するのではなく、リセットをシーケンス/プロパティの不可欠な部分にする必要があります。この場合、を使用することに近いリセット認識を実現する他の方法はありますdisable iffか?

既に宣言されているプロパティがすべてのクロック サイクルで false かどうかをアサートする方法はありますか?

例えば、

status[idx]req[idx]との両方が高い場合にのみ、高くする必要がありますenable[idx]。

私が欲しいのは、上記のネガティブシナリオチェッカーです。つまり、または のいずれかがローstatusの場合、 がハイになることはありません。reqenable

私は以下を試しましたが、vcsは以下のコンパイルエラーを出します

エラー - [PIWDOAACS] 'disable iff' が誤って使用されました

「disable iff」を含むプロパティ インスタンスは、「assert」、「assume」、および「cover」ステートメントでのみ使用できます。プロパティ p_RiseIntDischeck は、このコンテキストではインスタンス化されない場合があります。

seq_aすでに宣言されておりseq_b、他のアサーションに使用されています。これらのシーケンスを再利用し、上記のケースのネガティブ シナリオ チェッカーを作成するための最良/推奨の方法は何ですか?