2

私はアサーション ベースの検証の初心者であり、それが適切に行われる方法を学ぼうとしています。systemverilog + assertions に関する構造と技術的な詳細に関する多くの情報を見つけましたが、現実の世界で物事が実際にどのように行われるかについてのある種の「クックブック」資料をまだ見つけていません。

質問と制約:

  • デザインには、 data、valid、およびid入力を含むデータ入力バスがあります。
  • 1データ「パッケージ」は3サンプル
  • チャネルnの後には、チャネルn+1からのデータが常に存在します。
    • チャネル ID は、最大の ID が送信された後にラップされます
  • データ バイト間に任意の数の clk ティックを含めることができます

  • 以下は、チャネル ID を使用した単純でうまくいけば正しいタイミング図です。

    ここに画像の説明を入力

では、最小限のコードでこれを行うにはどうすればよいでしょうか。素敵できれい。以前は、データを駆動するダミーの Verilog モジュールを作成しました。しかし、仮定プロパティを使用してチャネル ID を制約することはできますが、それ以外の場合は、正式なツールが私の設計にブレーキをかけようとする自由な手は残しておいてください。

スターター向けのシンプルなテンプレートは次のとおりです。

data_in : assume property (
  <data with some ID>[=3]
  |=>
  <data with the next id after any clk tick>
);

問題は、上記のような仮定/アサーションがすべてのデータサンプルでトリガーされ、時間的に重複する並列スレッドを作成する傾向があることだと思います。

4

4 に答える 4

2

あなたが正式な検証方法論について話していると信じています。

フォーマル検証の場合、刺激を駆動するモジュールを構築する必要はありません。しかし、その代わりに、刺激はツール自体によって駆動され、想定プロパティを使用してツールを誘導して、正当な刺激を生成することができます。

仮定を何も提供しない場合、ツールは任意のランダム データを操作してアサーションを評価できます。この場合、誤った改ざんが発生する可能性があります。このシナリオは「制約下」として知られています。

同様に、仮定が多すぎると、正当な入力の組み合わせを見逃す可能性があります。このシナリオは、「過剰な制約」として知られています。

したがって、正確な仮定を提供することは非常に重要です。

あなたの場合、仮定は次のようになります。

property channel_change;
  // To check the next consecutive ID, after data transfer
  @(posedge clk)
  (id) throughout (valid [=3]) |=> valid && (id == $past(id) + 1)
endproperty

assume property (channel_change);

Formal Verification Methodology の詳細については、私のブログにアクセスしてください: What is Formal Verification? [1/2] &正式認証とは? [2/2]

于 2016-07-22T17:26:06.437 に答える
1

あなたが提供した例は重複していません。同じ ID を持つ 3 つのサンプルの後、次の ID を持つ別のデータ サンプルが来ると、結果が一致し、プロパティ全体が保持されます。

試行錯誤を繰り返すことは、とにかく現実です。ツールは常に、すべてのクロック サイクルで (アサートまたは想定された) プロパティを評価して、一致が可能かどうかを判断します。そうであると判断した場合は、新しい試行を開始します。そうでない場合は、次に進みます。試みが試合で終わるかどうかはわからないので、「すでに試みられている間はこのアサーションを考慮しようとしないでください」と言う方法はありません。

あなたが描いたような波を見ると、3 つのサンプルの間にプロパティを評価する必要がないことがすぐにわかりますが、それは単に全体像を見ることができるからです。これは、未来を見ることができるツールに似ています。

具体的な質問に移りますが、制約がすべてを語っているわけではありません。同じ ID を持つ 3 つのサンプルが来ると、次のサンプルの ID をインクリメントする必要があることを示しているだけです。ここでは、サンプルが 3 個のパケットで提供されなければならないということは何もありません。次のようなものが必要です。

assume property (
  sample_with_some_id_came |->
    came_out_of_reset_and_no_samples_were_sent.triggered or
      one_or_two_samples_with_same_id_sent_after_reset.triggered or
      three_samples_with_the_previous_id_sent.triggered
);

また、同じ ID を持つ 3 つのサンプルの後には常に次のサンプルが必要であると言うので、あなたの想定がある種の「無限の」動作を引き起こさないかどうかもわかりません。

于 2016-07-22T13:21:35.840 に答える