Spartan-3A Starter KitでCMOSカメラ・ディスプレイ回路でのOVLアサーション１

”Spartan-3A Starter KitでCMOSカメラ・ディスプレイ回路６（シミュレーション２）”でVerilogで書いたアサーションをOVLに書きなおしてみたいという希望を書いたが、実際にOVLアサーションに書きなおしてみることにした。
OVLについては、私のブログのまとめサイトのアサーション事始めを参照のこと。
AccelleraのOVL(Open Verification Library)のダウンロードサイトに行くと、Ver.2.5が出ていたので、これをダンロードしてから始めると良いと思う。

まずはVGA_Display_Controllerから、VerilogアサーションをOVLに変更してみる。ここでのアサーションは下のように非同期FIFOのoverflowとunderflowを検出するアサーションだ。

    // アサーション
    // synthesis translate_off
    always @ (posedge clk_ddr2) begin
        if (reset_ddr2)
            ;
        else begin
            if (afifo_overflow) begin 
                $display("%m: at time %t ERROR : FIFOがフルなのにライトした",$time);
                $stop;
            end
        end
    end
    always @(posedge clk_cam) begin
        if (reset_cam)
            ;
        else begin
            if (afifo_underflow) begin
                $display("%m: at time %t ERROR : FIFOが空なのにリードした",$time);
                $stop;
            end
        end
    end
    // synthesis translate_on

これを、OVLに変更するために、ovl_never を使用し、以下のように変更した。

// synthesis translate_off
`include "std_ovl_defines.h" // std_ovl_defines.hをインクルード
// synthesis translate_on

...............

    // synthesis translate_off
    wire [`OVL_FIRE_WIDTH-1:0] fire_overflow, fire_underflow; // fire用の信号を定義
    // synthesis translate_on

    ...............
    
    // synthesis translate_off
    ovl_never #(
        `OVL_ERROR,            // severity_level
        `OVL_ASSERT,        // property_type
        "ERROR : FIFOがフルなのにライトした", // msg
        `OVL_COVER_DEFAULT,    // coverage_level
        `OVL_POSEDGE,        // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK    // gating_type
    ) afifo_overflow_assertion (
        clk_ddr2,
        reset_ddr2,
        1'b1,
        afifo_overflow,
        fire_overflow
    );
        
    ovl_never #(
        `OVL_ERROR,            // severity_level
        `OVL_ASSERT,        // property_type
        "ERROR : FIFOが空なのにリードした", // msg
        `OVL_COVER_DEFAULT,    // coverage_level
        `OVL_POSEDGE,        // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK    // gating_type
    ) afifo_underflow_assertion (
        clk_cam,
        reset_cam,
        1'b1,
        afifo_underflow,
        fire_underflow
    );
    // synthesis translate_on

最初にstd_ovl_defines.hをインクルードする。次にfire用の信号を宣言する。その次にovl_neverを書いた。”OVL（Open Verification Library）を試してみる７(OVLチェッカの概要）”を引用する。

ovl_never : test_exprが決して真にならないことをチェックする。例えば、サイコロの値をdice_cntとすると、test_exprはdice_cnt>6と表される。dice_cntが7以上になればアサーション・エラーとなる

詳しくは（OVLの使い方や値の意味は）、OVLをダウンロードして、解凍したファイルのstd_ovl\docs\pdfdocsの下のovl_lrm.pdf(Accellera Standard OVL V2 Library Reference Manual)を見てもらうとわかると思う。

最初のパラメータ (severity_level) の`OVL_ERRORは、重要性のレベルでアサーションエラーだとERRORを出力する。“severity level”には、OVL_FATAL、OVL_ERROR、OVL_WARNING、OVL_INFOがあるそうだ(Accellera Standard OVL V2 Library Reference Manual参照、以下略)。

2番目 (property_type) の`OVL_ASSERTは、assertやassumeのプロパティだ。OVL_ASSERTはX/Zのチェックを含んだassert。OVL_ASSERT_2STATEは、X/Zのチェックを無視したassert。後は、OVL_ASSUME、OVL_ASSUME_2STATE がある。

3番目 (msg) は、アサーションエラーの時のメッセージ。

4番目 (coverage_level) は、coverage_level。`OVL_COVER_DEFAULTは、std_ovl_defines.hで OVL_COVER_BASICと定義されている。これをOVL_COVER_CORNERにすると、ovl_rangeで、min値とmax値になったときに”OVL_COVER_POINT : OVL_RANGE ”が表示される。
OVL_COVER_SANITY はチェックしている値が変化したときに、”OVL_COVER_POINT : OVL_RANGE ”が表示される。
後は、OVL_COVER_STATISTIC、OVL_COVER_NONE、OVL_COVER_ALL がある。

5番目 (clock_edge) は、クロックエッジで立ち上がりでチェックするか（OVL_POSEDGE）、立ち上がりでチェックするか（OVL_NEGEDGE）。

6番目 (reset_polarity) は、リセットの極性。アクティブハイ（OVL_ACTIVE_HIGH）か、アクテイブロー（OVL_ACTIVE_LOW）

7番目 (gating_type) は、enableに対してどう振舞うかを表す。OVL_GATE_CLOCKの場合はenableがFALSEの場合はチェックを停止し、なにもしない。カウンタや初期値は変更されない。
OVL_GATE_NONEの場合はenableを無視する。OVL_GATE_RESETの場合はenableがFALSEの場合はリセットする。

今度は信号の方で、最初の clk_cam は、アサーションのためのクロック。

2番目の reset_cam は同期リセット。

3番目の 1'b1 は、enableで、パラメータの7番目のgating_typeに関連する。

4番目の afifo_overflow は、チェックの条件だ。ここがTUREになると、パラメータの3番目のメッセージが出力される。

5番目の fire_overflow は、3ビット幅のfireで、ビット0はアサーションが失敗した時に1になる。ビット1はX/Zチェックが失敗した時に1になる。ビット2はCoverイベントがあったときに1になる。

さて、OVLをシミュレーションしてみよう。”OVL（Open Verification Library）を試してみる２（Veritakを使用する）”で行ったように、Defineが必要になる。

-Define OVL_VERILOG
-Define OVL_INIT_MSG
-Define OVL_COVER_ON
-Define OVL_ASSERT_ON
-Define OVL_MAX_REPORT_ERROR=1

上に示すDefineを行った。このうち必須なのは、OVL_ASSERT_ONとOVL_COVER_ONかな？
次に、std_ovl フォルダをincludeフォルダとして登録した。ライブラリフォルダとしても登録した。

-include_dir ../../../../OVL/std_ovl
-lib_dir ../../../../OVL/std_ovl

OVL Ver.2であれば、

-lib_ext vlib

は必要ない。
これで準備OKなので、Veritak-Basic Ver.3.80Dで、コンパイルしてシミュレーションしてみた。下がその結果だ。


2つのfireは、ずっと発火しないまま、つまりエラーがでない状況だ。これは良いことなのだが、fireが発火するシミュレーションが、”OVL（Open Verification Library）を試してみる４（OVL_range）”にあるので参照のこと。