はじめに

今回はsimple-req-ackのアサーションに対して、これまでと異なるテストベクタをくべてその振る舞いの違いを見てみます。

なお、ソースコードはGitHubにあります。

このブログで扱うソースコードはできるだけGitHubにあげていきます。ライセンスなどご確認頂いた上でお好きにお使い下さい。今回のコードはこちらになります。

GitHub - systemverilog-assertion - simple-req-ack2

DUT仕様おさらい（dut.sv）

DUT仕様は、reqが1パルス入力されると2サイクル後ackを1パルス返すものでした。

プロパティおさらい（sva_req_ack.sv）

DUT仕様を確認するために似たような4つのプロパティを用意していました。

sva_req_ack1 ･･･ Highレベルを確認
sva_req_ack2 ･･･ Highへの立ち上がりを確認
sva_req_ack3 ･･･立ち上がりと立ち下がりを確認
sva_req_ack4 ･･･立ち上がりとレベルと立ち下がりを互いの信号関係を踏まえ確認

プロパティだけ抜粋しておきます。

 // PROPERTY 
    property sva_req_ack1 (clk, rst_n, req, ack);
        @(posedge clk) disable iff(!rst_n)
        req |-> ##2 ack;
    endproperty

    property sva_req_ack2 (clk, rst_n, req, ack);
        @(posedge clk) disable iff(!rst_n)
        $rose(req) |-> ##2 $rose(ack);
    endproperty

    property sva_req_ack3 (clk, rst_n, req, ack);
        @(posedge clk) disable iff(!rst_n)
        $rose(req) |-> ##1 $fell(req) ##1 $rose(ack) ##1 $fell(ack);
    endproperty

    property sva_req_ack4 (clk, rst_n, req, ack);
        @(posedge clk) disable iff(!rst_n)
        $rose(req) |->
            !ack ##1 ($fell(req) & !ack) ##1 ($rose(ack) & !req) ##1 ($fell(ack) & !req);
    endproperty

今回のテスト（bench.sv）

やっと本題です。今回は1パルスのreqに加えて、2サイクルのreqパルスと5サイクルのreqパルスをくべてみます。シナリオ箇所だけ抜粋します。

 task scenario();
        req = 0;
        @(posedge rst_n)

        // 1st. req as 1 cycle pulse.
        repeat(5) @(posedge clk);
            req = 1;
        repeat(1) @(posedge clk);
            req = 0;
        repeat(3) @(posedge clk);

        // 2nd. req as 2 cycle pulse.
            req = 1;
        repeat(2) @(posedge clk);  // 2 cycles
            req = 0;
        repeat(3) @(posedge clk);

        // 3rd. req as 5 cycle pulse.
            req = 1;
        repeat(5) @(posedge clk);  // 5 cycles
            req = 0;
        repeat(5) @(posedge clk);
    endtask

実行結果

波形はこのようになります。

f:id:hassyy:20150804212402p:plain

今回は2サイクルのreqパルスと5サイクルのreqパルスは期待しない動作なのでアサーションがFail（ファイア）することを期待します。おおかたよさそうですが、残念ながら2番目のプロパティ（sva_req_ack2:立ち上がりだけ）はしれっとPassしてしまいました。その他のプロパティについては、1番目（sva_req_ack1：Highレベル）はNGを検出していますが、複数回ファイアしています。また、3番目（sva_req_ack3:立ち上がりと立ち下がり）と4番目（sva_req_ack4：全部）は、最初のNGでのみファイアしています。
NGを検出した上で、どのプロパティがよいかは...自分は最小限のファイアが好みです。余計なファイアがないほうがデバッグしやすいので。ですがどれが良いかは一概には言えないと思います。丁寧なプロパティは場合によってはCPUリソースやメモリ食いかもしれませんし...何を検出するためプロパティを書くか、に依存すると思っています。

今日はここまで

ここ数回SVAについてどうでもいい内容を書いてみました。次は、UVM1.2も動き出すようですしまたUVM Cookbookに戻ろうかなと思っています。ですが座学だけだとつまらないのでUVMのサンプルでも作ってみようかなと思っています。

カミは死んだ

Paper Is Dead ... osz

SVA - アサーションFireさせてみた。