2

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

ここに画像の説明を入力

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

req == fill ##1 (trans [->1]) [*4];

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

ここに画像の説明を入力

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

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

int num_trans_seen;
bit trans_ongoing;
bit trans_done;
bit trans_queued;

always @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    num_trans_seen;
    trans_ongoing <= 0;
    trans_done <= 0;
    trans_queued <= 0;
  end
  else begin
    if (trans_ongoing)
      if (num_trans_seen == 3 && req == trans) begin
        trans_done <= 1;
        if (req == fill || trans_queued)
          trans_queued <= 0;
        else
          trans_ongoing <= 0;
        num_trans_seen == 0;
      end
    else
      if (trans_queued) begin
        trans_queued <= 0;
        trans_ongoing <= 1;
      end

    if (trans_done)
      trans_done <= 0;
  end

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

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

req == fill ##0 (trans_ongoing ##0 trans_done [->1]) [*0:1]
  ##1 (trans [->1]) [*4];

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

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

4

2 に答える 2

1

トランスが開始する前に、rsp は常にアイドル状態になっているようです。rsp'sidleが定数値であり、trans決して変わらない値である場合は、次を使用できます。

req == fill ##0 (rsp==idle)[->1] ##1 trans[*4];

上記は、パイプラインが 1 ～ 3 ステージをサポートする場合に機能するはずです。

4 つ以上の深いパイプラインの場合、補助コードが必要だと思います。アサーションの成功/失敗ブロックを使用して、完了のカウントを無効にすることができますtrans。これにより、追加の RTL を記述する必要がなくなります。プロパティのローカル変数を使用して、塗りつぶしのカウント値をサンプリングできます。サンプリングされた値は、予想されるトランス パターンのサンプリングを開始するための基準として使用されます。

int fill_req;
int trans_rsp;
always @(posedge clk, negedge rst_n) begin
  if(!rst_n) begin
    fill_req <= '0;
    trans_rsp <= '0;
  end
  else begin
    if(req == fill) begin
      fill_req <= fill_req + 1; // Non-blocking to prevent risk of race condition
    end
  end
end

property fill_trans();
  int id;
  @(posedge clk) disable iff(!rst_n)
  (req == fill, id = fill_req) |-> (rsp==idle && id==trans_rsp)[->1] ##1 trans[*4];
endproperty

assert property (fill_trans()) begin
  // SUCCESS
  trans_rsp <= trans_rsp + 1; // Non-blocking to prevent risk of race condition
end
else begin
  // FAIL
  // trans_rsp <= trans_rsp + 1; // Optional for supporting pass after fail
  $error("...");
end

参考までに: これを完全にテストする時間がありませんでした。少なくとも正しい方向に進むはずです。

もう少し実験して、あなたの好みに合った解決策を見つけました。サポートコードはありません。

に相当するのtrans[->4]は(!trans[*] ##1 trans)[*4]、IEEE Std 1800-2012 § 16.9.2 Repetition in sequenceです。したがって、ローカル変数を使用して、展開されたフォームで新しい入力リクエストを検出できます。たとえば、次のシーケンス

sequence fill_trans;
  int cnt;                                // local variable
  @(posedge clk)
  (req==FILL,cnt=4) ##1 (                 // initial request set to 4
    (rsp!=TRANS,cnt+=4*(req==FILL))[*]    // add 4 if new request
    ##1 (rsp==TRANS,cnt+=4*(req==FILL)-1) // add 4 if new request, always minus 1
  )[*] ##1 (cnt==0);                      // sequence ends when cnt is zero
endsequence

assert property();言及されていない別の修飾子がない限り、fill リクエストがあるたびに新しいアサーション スレッドを開始するため、typ. を使用することはできません。代わりにexpect、プロパティの評価を待機できるステートメントを使用します ( IEEE Std 1800-2012 § 16.17 Expect ステートメント)。

always @(posedge clk) begin
  if(req==FILL) begin
    expect(fill_trans);
  end
end

https://www.edaplayground.com/x/5QLsをテストするために、記述動作を再作成してみました

于 2016-08-31T03:22:38.690 に答える
0

考えられる解決策の 1 つは、以下の 2 つのアサーションで実現できます。

1枚目の画像の場合 -

(req == fill) && (rsp == idle) |=> ((rsp == trans)[->1])[*4]

2枚目の画像の場合 -

(req == fill) && (rsp == trans) |=> ((rsp == trans)[->1])[*0:4] ##1 (rsp == idle) ##1 ((rsp == trans)[->1])[*4]

1 つの問題は、各サイクルで継続的な「フィル」リクエストがある場合 (中間の「アイドル」なしで連続した 4 つの「フィル」リクエスト)、2 番目のアサーションが各「フィル」リクエストの「トランス」サイクルを計算しないことです (代わりに「トランス」サイクル自体の 2 番目のセットでのみ完了します)。

現在のところ、特定のバグのアサーションを変更できませんでした。

于 2016-08-30T16:57:35.780 に答える