パイプライントランザクションを処理するためのSVAシーケンスのサポートコードの回避

Question

次のようなプロトコルがあります。 fillからreqマスターセット一度、スレーブrsp介して4つの転送信号を送る。

この全体のトランザクションのアンSVA配列が（スレーブtransサイクル間idleサイクルを挿入することができると仮定して）次のようになります。

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

ここで、マスタがリクエストをパイプラインで送信できるとします。これは、4つのtransサイクルが行われる前に、次fillを開始するために許可されていることを意味する：

上からSVAシーケンスが、助けにはなりません秒fillのために、誤って4 transに一致するように起こっているので、最後にtransを「フローティング」のままにします。前のfillのものがマッチした後で初めて、transサイクルのマッチングを開始する必要があります。

シーケンスでは、単一の評価ではグローバル情報が利用できません。基本的には、別のインスタンスが実行されていることを知る必要があります。私はこれを実装すると考えることができる唯一の方法は、いくつかのRTLのサポートコードを使用している：上記のコードは、トランザクションの進行中trans_ongoingビットを上げ、クロック・サイクルでtrans_doneパルスすべき

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 

ときfillための最後のtrans送信されます。

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

：（。。私はそれをテストしていないので、私がすべきと言うが、これはポイントではありませんのは、それが動作することを仮定します）

はこのような何かを持って、一つはするシーケンスを書き換えることができ

これはうまくいくはずですが、私はサポートコードが必要であるという事実について特に興奮していません。その中には多くの冗長性があります。なぜなら、私は基本的に、トランザクションとパイプラインの仕組みの良いチャンクを再記述したからです。それも簡単に再利用できません。 sequenceはパッケージに入れて他の場所にインポートすることができます。サポートコードは一部のモジュールにのみ配置して再利用できますが、シーケンスを格納するパッケージとは異なる論理エンティティです。

質問はここにあります：サポートコードの必要を避けながらパイプラインバージョンのシーケンスを書き込む方法はありますか？

Answer 1

トランスの開始前に常にrspがアイドル状態にあるようです。 RSPのidleが一定値であり、transはなることはありませんという値である場合は、使用することができます：パイプラインが1〜3段階をサポートしている場合

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

は、上記の動作するはずです。

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 

FYI：これを完全にテストする時間はありませんでした。それは少なくとも正しい方向にあなたを得る必要があります。

---

---

私はもう少し実験やお好みに合わせてよりかもしれない解決策を見つけました。サポートコードはありません。

trans[->4]の等価物は、配列で(!trans[*] ##1 trans)[*4]16.9.2 § IEEE Std 1800-2012当たり繰り返しです。したがって、ローカル変数を使用して、展開されたフォームで新しい塗りつぶし要求を検出できます。それは新しいアサーションスレッドを毎回起動しますので、記載されていない別の修飾子がない限り、次の順序

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();を使用することはできません。代わりにexpectステートメントを使用すると、プロパティの評価を待つことができます（IEEE Std 1800-2012 § 16.17 Expectステートメント）。私はあなたのhttps://www.edaplayground.com/x/5QLs

Answer 2

次の2つのアサーションを使用して、1つの可能な解決策を達成できます。第一の画像については

- 第二の画像については

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

-

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

1つの問題は、連続がある場合にせずに、要求を「埋める」の連続した4（各サイクルで要求を「埋める」ということです2番目のアサーションは、各 "fill"リクエストに対して "trans"サイクルを計算しません（代わりに、2番目の "trans"サイクル自体でのみ完了します）。

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