FC2カウンター FPGAの部屋 アサーション事始め
FC2ブログ

FPGAやCPLDの話題やFPGA用のツールの話題などです。 マニアックです。 日記も書きます。

FPGAの部屋

FPGAの部屋の有用と思われるコンテンツのまとめサイトを作りました。Xilinx ISEの初心者の方には、FPGAリテラシーおよびチュートリアルのページをお勧めいたします。

OVL(Open Verification Library)を試してみる6(ovl_next, ovl_frame その2)

OVL(Open Verification Library)を試してみる5(ovl_next, ovl_frame その1)”の続き。

さて、request とacknowledge の関係をVerilogでコーディングしてみた。req0, ta0, ack0 とreq1, ta1, ack1 の信号のグループがある。req_start0の1パルスをreq0を生成するステートマシン(req_sm.v)が受けると、req0信号をアサートする。req0は応答が帰ってくるまでアサートし続ける。ack0を出力するステートマシン(ack_sm.v)は、バックエンドの回路からのta0のアサートを確認して、ack0をアサートする。ack0がアサートされると、req0はディアサートされる、といったような制御をする。タイミングチャートを下に示す。
OVL_req_ack_1_100318.png

req_start1, req1, ta1, ack1の関係もreq0などの関係と同様とする。今回は間違いやすくするために、ack_sm.v はreq0,req1を同時に受けて、ack0, ack1を返すステートマシンとする(ta0, ta1も2つ同時に受ける)。それにわざと間違いを入れておいた(思いもよらない間違いも入っていたが。。。)。実際に作るときは、ack0, ack1のステートマシンを分けて、2つのステートマシンで処理する。しかし、仕様で同様の状態になってしまうケースもあることから、OVLを使用したアサーションの例として作成した。

req_sm.v を下に示す。

// OVLテスト用req_sm.v
// req_start 信号を受けると、reqを1にアサートする。ackを受け取るとreqを0にディアサートする

`default_nettype none

module req_sm (
    input wire    clk,
    input wire    reset,
    input wire    req_start,
    input wire    ack,
    output reg    req
);
    
    parameter [1:0]    idle_req        = 2'b01,
                    assert_req    = 2'b10;
    
    reg [1:0] cs_req;
    
    always @(posedge clk) begin
        if (reset) begin
            cs_req <= idle_req;
            req <= 1'b0;
        end else begin
            case (cs_req)
                idle_req : 
                    if (req_start) begin
                        cs_req <= assert_req;
                        req <= 1'b1;
                    end
                assert_req :
                    if (ack) begin
                        cs_req <= idle_req;
                        req <= 1'b0;
                    end
            endcase
        end
    end
endmodule

`default_nettype wire


次に、ack_sm.v を示す。

// OVLテスト用 ack_sm.v
// 2つのreqを管理して、reqがアサートされている状態で、taがアサートされるとackを返す

`default_nettype none

module ack_sm (
    input wire    clk,
    input wire    reset,
    input wire    req0,
    input wire    req1,
    input wire    ta0, // Transfer Acknowledge
    input wire    ta1, // Transfer Acknowledge 
    output reg    ack0,
    output reg    ack1
);
    
    parameter [6:0]    idle_req         = 7'b0000001,    // 最初のidle 状態
                    assert_req0        = 7'b0000010,    // req0だけがアサートされている
                    assert_req1        = 7'b0000100,    // req1だけがアサートされている
                    assert_req01    = 7'b0001000,
                    req0_ack        = 7'b0010000,
                    req1_ack        = 7'b0100000,
                    req01_ack        = 7'b1000000;
    reg [6:0] cs_main;
    
    always @(posedge clk) begin
        if (reset) begin
            cs_main <= idle_req;
            ack0 <= 1'b0; ack1 <= 1'b0;
        end else begin
            case (cs_main)
                idle_req : begin
                    if (req0) begin
                        cs_main <= assert_req0;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end else if (req1) begin
                        cs_main <= assert_req1;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end
                end
                assert_req0 : begin
                    if (req1) begin
                        cs_main <= assert_req01;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end else if (ta0) begin
                        cs_main <= req0_ack;
                        ack0 <= 1'b1; ack1 <= 1'b0;
                    end
                end
                assert_req1 : begin
                    if (req0) begin
                        cs_main <= assert_req01;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end else if (ta1) begin
                        cs_main <= req1_ack;
                        ack0 <= 1'b0; ack1 <= 1'b1;
                    end
                end
                assert_req01 : begin
                    if (ta0 & ~ta1) begin
                        cs_main <= req0_ack;
                        ack0 <= 1'b1; ack1 <= 1'b0;
                    end else if (~ta0 & ta1) begin
                        cs_main <= req1_ack;
                        ack0 <= 1'b0; ack1 <= 1'b1;
                    end else if (ta0 & ta1) begin
                        cs_main <= req01_ack;
                        ack0 <= 1'b1; ack1 <= 1'b1;
                    end
                end
                req0_ack : begin
                    if (req1) begin
                        cs_main <= assert_req1;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end else begin
                        cs_main <= idle_req;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end
                end
                req1_ack : begin
                    if (req0) begin
                        cs_main <= assert_req0;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end else begin
                        cs_main <= idle_req;
                        ack0 <= 1'b0; ack1 <= 1'b0;
                    end
                end
                req01_ack : begin
                    cs_main <= idle_req;
                    ack0 <= 1'b0; ack1 <= 1'b0;
                end
            endcase
        end
    end
endmodule

`default_nettype wire


わざと間違いを入れてある。しかし、ack0, ack1を別々のステートマシンでやった方が、相当簡単になる。2つ一緒にやるのは難しい。
次は、OVLの入ったテストベンチを示す。req_sm.v は2つインスタンスを作っている。ack_sm.v は1つインスタンスしている。

// tb_req_ack.v

`default_nettype none
`timescale 1ns / 10ps

`include "std_ovl_defines.h"

module tb_req_ack;
    reg clk;
    reg reset;
    reg req_start0, req_start1;
    wire req0, req1;
    wire ack0, ack1;
    reg ta0, ta1;
    wire [`OVL_FIRE_WIDTH-1:0] fire_ta0_ack0_as, fire_ta1_ack1_as;
    wire [`OVL_FIRE_WIDTH-1:0] fire_req0_ack0_as, fire_req1_ack1_as;

    parameter CLK_PERIOD = 20;
    
    // 50MHzクロック
    always begin
       #(CLK_PERIOD/2)    clk = 1'b1 ;
       #(CLK_PERIOD/2)    clk = 1'b0 ;
    end
    
    // reset
    initial begin
            reset = 1'b1;
        #100    reset = 1'b0;
    end
    
    req_sm req_sm0 (
        .clk(clk),
        .reset(reset),
        .req_start(req_start0),
        .ack(ack0),
        .req(req0)
    );
    req_sm req_sm1 (
        .clk(clk),
        .reset(reset),
        .req_start(req_start1),
        .ack(ack1),
        .req(req1)
    );
    
    ack_sm ack_sm_i (
        .clk(clk),
        .reset(reset),
        .req0(req0),
        .req1(req1),
        .ta0(ta0),
        .ta1(ta1),
        .ack0(ack0),
        .ack1(ack1)
    );
    
    // req_start0とta0の関係を生成する
    initial begin
        req_start0 <= 1'b0;
        ta0 <= 1'b0;
        @(negedge reset); // リセットが0になるのを待つ
        #100;
        REQ_START_TA0(3'd1);
        REQ_START_TA0(3'd2);
        REQ_START_TA0(3'd3);
        REQ_START_TA0(3'd2);
        REQ_START_TA0(3'd1);
        REQ_START_TA0(3'd3);
        REQ_START_TA0(3'd2);
        #200    $stop;
    end
    
    // req_start1とta1の関係を生成する
    initial begin
        req_start1 <= 1'b0;
        ta1 <= 1'b0;
        @(negedge reset); // リセットが0になるのを待つ
        #100;
        REQ_START_TA1(3'd2);
        REQ_START_TA1(3'd1);
        REQ_START_TA1(3'd2);
        REQ_START_TA1(3'd3);
        REQ_START_TA1(3'd3);
        REQ_START_TA1(3'd1);
        REQ_START_TA1(3'd2);
    end
    
    // task REQ_START_TA0
    task REQ_START_TA0;
        input [2:0] loop_count;
        

        begin :REQ_START_TA0_PROCESS
            integer i;            
            
            @(posedge clk); // clkの立ち上がりまでwait
            #1 ; // 遅延を挟んで
            req_start0 = 1'b1;
            @(posedge clk); // clkの立ち上がりまでwait
            #1; // 遅延を挟んで
            req_start0 = 1'b0;
            
            for(i=loop_count; i>0; i=i-1) begin
                @(posedge clk);
                #1;
            end
            ta0 = 1'b1;
            @(posedge clk); // clkの立ち上がりまでwait
            #1 ; // 遅延を挟んで
            ta0 = 1'b0;
        end
    endtask
    
    // task REQ_START_TA1
    task REQ_START_TA1;
        input [2:0] loop_count;
        

        begin :REQ_START_TA1_PROCESS
            integer i;        
            
            @(posedge clk); // clkの立ち上がりまでwait
            #1 ; // 遅延を挟んで
            req_start1 = 1'b1;
            @(posedge clk); // clkの立ち上がりまでwait
            #1; // 遅延を挟んで
            req_start1 = 1'b0;
            
            for(i=loop_count; i>0; i=i-1) begin
                @(posedge clk);
                #1;
            end
            ta1 = 1'b1;
            @(posedge clk); // clkの立ち上がりまでwait
            #1 ; // 遅延を挟んで
            ta1 = 1'b0;
        end
    endtask
    
    // アサーション
    // ta0がアサートされた次のクロックでack0がアサートされる
    ovl_next #(
        `OVL_ERROR,            // severity_level
        1,                    // num_cks(1クロック後にアサート)
        1,                    // check_overlapping (off)
        1,                    // check_missing_start (on)
        `OVL_ASSERT,        // property_type
        // "ERROR: ta0がアサートされた次のクロックでack0がアサートされていない",
        "ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted.",
        `OVL_COVER_BASIC,    // coverage_level
        `OVL_POSEDGE,        // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) ta0_ack0_assertion (
        clk,
        reset,
        1'b1,                // enable
        ta0,                // start event
        ack0,                // test_expr
        fire_ta0_ack0_as    // fire
    );
    
    // ta1がアサートされた次のクロックでack1がアサートされる
    ovl_next #(
        `OVL_ERROR,            // severity_level
        1,                    // num_cks(1クロック後にアサート)
        1,                    // check_overlapping (off)
        1,                    // check_missing_start (on)
        `OVL_ASSERT,        // property_type
        // "ERROR: ta1がアサートされた次のクロックでack1がアサートされていない",
        "ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted.",
        `OVL_COVER_BASIC,    // coverage_level
        `OVL_POSEDGE,        // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) ta1_ack1_assertion (
        clk,
        reset,
        1'b1,                // enable
        ta1,                // start event
        ack1,                // test_expr
        fire_ta1_ack1_as    // fire
    );
    
    // req0アサートされた後で、ack0 が2~4クロックの間に1になる
    ovl_frame #(
        `OVL_ERROR,                // severity_level
        2,                        // min_cks
        4,                        // max_cks
        `OVL_IGNORE_NEW_START,    // action_on_new_start
        `OVL_ASSERT,            // property_type
        // "ERROR: req0がアサートされた後の2~4クロック後にack0が1にならない",
        "ERROR: ack0 isn't asserted after 2-4 clocks after req0 was asserted.",
        `OVL_COVER_BASIC,        // coverage_level
        `OVL_POSEDGE,            // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) req0_ack0_assertion (
        clk,
        reset,
        1'b1,                // enable
        req0,                // start event
        ack0,                // test_expr
        fire_req0_ack0_as    // fire
    );
        
    // req1アサートされた後で、ack1 が2~4クロックの間に1になる
    ovl_frame #(
        `OVL_ERROR,                // severity_level
        2,                        // min_cks
        4,                        // max_cks
        `OVL_IGNORE_NEW_START,    // action_on_new_start
        `OVL_ASSERT,            // property_type
        // "ERROR: req1がアサートされた後の2~4クロック後にack1が1にならない",
        "ERROR: ack1 isn't asserted after 2-4 clocks after req1 was asserted.",
        `OVL_COVER_BASIC,        // coverage_level
        `OVL_POSEDGE,            // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) req1_ack1_assertion (
        clk,
        reset,
        1'b1,                // enable
        req1,                // start event
        ack1,                // test_expr
        fire_req1_ack1_as    // fire
    );
        
endmodule

`default_nettype wire


Veritakの場合には日本語のメッセージを活かしてある。
さて、Veritakを起動して、プロジェクトを作成してシミュレーションしてみた。
下にVeritakのプロジェクトの様子を示す。define値を設定している。今回はOVL_V1のassert_... を使用してないので、.vlibは使用しない。
OVL_req_ack_2_100318.png

次にシミュレーション結果を下の図に示す。
OVL_req_ack_3_100318.png

黒い縦線のところでack0 がアサートされていないのがわかる。これに対応するovl_nextのエラーメッセージを下に示す。

OVL_ERROR : OVL_NEXT : ERROR: ta0がアサートされた次のクロックでack0がアサートされていない : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 29000 : tb_req_ack.ta0_ack0_assertion.ovl_error_t


これは、fire信号、[2:0]fire_ta0_ack0_as でも確認することができる。値の4はカバーなので、1がアサーション・エラーを示す値となる。
次に、ovl_frame の方だが、330nsec の時点で、アサーション・エラーとなっている。メッセージを下に示す。

OVL_ERROR : OVL_FRAME : ERROR: req0がアサートされた後の2~4クロック後にack0が1にならない : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 33000 : tb_req_ack.req0_ack0_assertion.ovl_error_t


こちらのfire信号、fire_req0_ack0_asは0のままだった。ドライバ記述部に飛んで、記述を見てみたが、すべて0となっていた。ovl_frame のfire はOVLのバージョン2.4ではサポートされていないようだ。

ovl_next とovl_frame アサーションを使用して、波形の自動チェックができることがわかった。エラーが出たらアサーションが止まるようにしておくと良いかもしれない(severity_levelにOVL_ERRORのかわりにOVL_FATALを記述する)。

最後に、ModelSimでもやってみたので、図を下に示す。
OVL_req_ack_4_100318.png
  1. 2010年03月18日 05:20 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

OVL(Open Verification Library)を試してみる5(ovl_next, ovl_frame その1)

今回は、ovl_nextとovl_frameを試してみる。今回は例を作るのに時間がかかってしまった。良い例(とはなっていないかもしれないが?)を作るのは大変だと思った。
ovl_nextは、reqの次にackが来るというように、Aという信号がアサートされた後の確定したクロック後にBという信号がアサートされるというアサーションだ。例を見てみよう。下に示したのが実際に書いたovl_nextの記述。

    // ta0がアサートされた次のクロックでack0がアサートされる
    ovl_next #(
        `OVL_ERROR,            // severity_level
        1,                    // num_cks(1クロック後にアサート)
        1,                    // check_overlapping (off)
        1,                    // check_missing_start (on)
        `OVL_ASSERT,        // property_type
        "ERROR: ta0がアサートされた次のクロックでack0がアサートされていない",
        `OVL_COVER_BASIC,    // coverage_level
        `OVL_POSEDGE,        // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) ta0_ack0_assertion (
        clk,
        reset,
        1'b1,                // enable
        ta0,                // start event
        ack0,                // test_expr
        fire_ta0_ack0_as    // fire
    );


これはta0がアサートされていから1クロック後に必ずack0がアサートされるということを示したovl_nextのアサーションだ。もし、複雑なRTLコードの2つの信号間に、同じクロック期間でアサートされる関係がある時には、このようなアサーションを設計者が入れておけば、あとでRTLコードを読む人へのメッセージともなることだろう?(どっかで、聞いた?、見た?言葉)

次にovl_frameだが、これはovl_nextはA, B信号間のクロック数は確定している必要がある。ovl_frameは、Aがアサートされてから、最小何クロックから最大何クロックまでにBがアサートされれば良いというアサーションになる。下に例を示す。

    // req0アサートされた後で、ack0 が2~4クロックの間に1になる
    ovl_frame #(
        `OVL_ERROR,                // severity_level
        2,                        // min_cks
        4,                        // max_cks
        `OVL_IGNORE_NEW_START,    // action_on_new_start
        `OVL_ASSERT,            // property_type
        "ERROR: req0がアサートされた後の2~4クロック後にack0が1にならない",
        `OVL_COVER_BASIC,        // coverage_level
        `OVL_POSEDGE,            // clock_edge
        `OVL_ACTIVE_HIGH,    // reset_polarity
        `OVL_GATE_CLOCK        // gating_type
    ) req0_ack0_assertion (
        clk,
        reset,
        1'b1,                // enable
        req0,                // start event
        ack0,                // test_expr
        fire_req0_ack0_as    // fire
    );


OVL_IGNORE_NEW_STARTを定義してあるので、Aの信号req0はパルスではなくて、アサートされ続ける信号でも問題ない。
次は、実際に例を作って、結果を見てみることにする。(もう作って、やってありますが。。。)

参考文献:Accellera Standard OVL V2 Library Reference Manual Software Version 2.4 March 2009
  1. 2010年03月17日 05:25 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

OVL(Open Verification Library)を試してみる4(OVL_range)

今回は、今までのassert_range をOVL V2のovl_range に書き換えてみようと思う。なお、std_ovl/docs/pdfdocs/ovl_lrm.pdf (Accellera Standard OVL V2 Library Reference Manual) を参考にしている。
まずは、OVL V1のassert_rangeは今までやってきた通り。

   assert_range #(
                  /*severity_level*/`OVL_FATAL, 
                  /*width*/ 4, 
                  /*min  */ 0, 
                  /*max  */ 9, 
                  /*property_type */`OVL_ASSERT, 
                  /*msg*/ "The counter arrived at invalid range.", 
                  /*coverage_level*/`OVL_COVER_CORNER)
     counter_checker_inst (
                           .clk(ICLK), 
                           .reset_n(~IRST), 
                           .test_expr(OCOUT));


次に、OVL V2のovl_range で書き換えた例を示す。なお、このovl_range は論理合成可能だそうだ。

   ovl_range #(
                `OVL_FATAL,         // severity_level
                4,                     // width
                0,                     // min
                9,                     // max
                `OVL_ASSERT,         // property_type
                "The counter arrived at invalid range.", 
                `OVL_COVER_CORNER,    // coverage_level
                `OVL_POSEDGE,        // clock edge
                `OVL_ACTIVE_HIGH,    // reset_polarity
                `OVL_GATE_CLOCK)    // gating type
     counter_checker_inst (
                .clock(ICLK), 
                .reset(IRST), 
                .enable(1'b1),
                .test_expr(OCOUT),
                .fire(fire)
    );


パラメータでは、clock edge、reset_polarity、gating typeが増えている。ポートではenableとfire が増えている。
fire の定義は、 wire [`OVL_FIRE_WIDTH-1:0] fire; で、OVL_FIRE_WIDTHは3だ。fire[0] は、アサーションの失敗した時に1になる。fire[1] はX/Zチェックが失敗した時に1になる(X/ZチェックはXやZになったときだろうか?)。fire[2] はカバー・イベントがあった時に1になるそうだ。つまり今は、OVL_COVER_CORNERにしているので、コーナーの時、つまりOCONTが0と9の時に1になるのだと思われる。
この修正後にシミュレーションをしてみた結果を下に示す。
OVL_sample_7_100312.png

コーナーの値0と9の次のクロックでfire[2]が1となるのがわかる。
次に、coverage_levelをOVL_COVER_BASICとしてコーナーの値でカバーを出さないようにして、max値を8として、わざとアサーションを失敗させてみよう。これでシミュレーションしてみたのが下の図。
OVL_sample_8_100312.png

235ステップ目でOCOUTが9となって、アサーションを失敗して、OVL_FATALになったので、335ステップ目でfinish している。ここで、severity_levelをOVL_ERRORにして再度シミュレーションを行うと、OCOUTが9になったときにfire[0] が1となる。
OVL_sample_9_100312.png

severity_levelがOVL_FATALの時に、アサーションが失敗した時からシミュレーションが終了するまでの時間は、グローバルのマクロ、OVL_RUNTIME_AFTER_FATALで設定することができる。デフォルト値は100だ。
  1. 2010年03月13日 13:16 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

OVL(Open Verification Library)を試してみる3(アサーションの説明)

はじめの一歩-テストベンチ-”に書かれているassert_range アサーションはある信号の値が自分の意図する範囲に入っているのかを確認するアサーションだ。アサーションとは、検証する必要のある設計意図としての動作、つまりプロパティに対する記述分だそうだ。(アサーションベース設計、原書2版、第1章はじめに、4ページより引用)つまりRTLで動作を記述するのだが、RTLではいろいろなステートマシンやその他のカウンタやロジックなどが複雑にからみ合って記述する必要がある場合がある。その信号だけを考えてみよう。その場合に、その信号は例えば4ビットのバイナリなんだけど、10進数を表していて、取りうる値の範囲は0~9までという設計だったとしよう。多分、このRTLコードには、間違いは少ないと思うが、その信号のプロパティとしての値の範囲は0~9ということを検証しようとする。そのときに使えるのがアサーションということになる。アサーション記述言語には、OVL、PSL、SystemVerilogアサーションの3つが有名らしいが、そのうちのPSL、SystemVerilogアサーションは対応するシミュレーターが必要となる。OVLはライブラリとしてコンパイルすれば、どのシミュレーターでもアサーションを記述することができる。
これまで、アサーション記述言語のことを書いてきたが、Verilogでもアサーションを書くことができる。例えば、キャラクタ描画テスト回路のFIFOのoverflow, underflowが出ているかどうかを見るために、シミュレーション限定でVerilogコードによるアサーションを書いてあった。本来、FIFOのoverflow, underflowは起こらないように制御するものであるが、制御コードのバグによって起こってしまう場合がある。アサーションによってそれを監視していれば、起こった時にすぐわかるわけだ。それが分からないと、なかなかデバックが難しくなったりする。下に示すのは、ビットマップVGAコントローラに使用した非同期FIFOのアサーションだ。この非同期FIFOには、underflow, overflow端子を生成しておいたので、それがアサートされるかどうかをチェックしている。

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


ちょっと日本語になっているのが微妙ですが、Veritak用ということで。。。
これだけだが、これでunderflowやoverflowを検出できてずいぶんと助かった。
さて、OVL V1でこれをやろうとすると、assrt_neverを使うのだろう。上のVerilogアサーションと等価に書くには、下のように書けば良いと思う。

    // アサーション
    // synthesis translate_off
    assert_never #(`OVL_FATAL, 0, "ERROR : FIFOが空なのにリードした") fifo_underflow_assertion(clk_ddr2, ~reset_ddr2, afifo_underflow);
    assert_never #(`OVL_FATAL, 0, "ERROR : FIFOがフルなのにライトした") fifo_overflow_assertion(clk_ddr2, ~reset_ddr2, afifo_overflow);
    // synthesis translate_on


上の記述は確かめていないので、動くかどうかわかりません。あくまでもイメージということでお願いします。(動かなかったら教えてください)
というわけで、数行に渡っていたVerilogのアサーションがOVL V1を使うと、1行で書くことができる。こんな簡単なアサーションだけではなく、例えば、requestとackの関係はassert_nextによって検証することができる。

次はassert_で表されるOVL V1のアサーションをovl_で始まるOVL V2のアサーションに書き換えてみる。OVL V2は、機能が拡張されていて、OVL V1を含んでいるそうだ。

  1. 2010年03月11日 23:17 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

OVL(Open Verification Library)を試してみる2(Veritakを使用する)

前回はModelSimでOVLを使用したが、今度はVeritakでもOVLを使えるかどうかを試してみた。
まずは、Veritakを起動してovl_sampleというプロジェクトを生成する。(私のブログのVeritakのチュートリアルを参照
ovl_sampleのコマンドファイルのcomplie.f を下に引用させて頂く。

ovl_example/sim/compile.f-------------------------------------
 1    +define+OVL_ASSERT_ON
 2    +define+OVL_COVER_ON
 3    +define+OVL_MAX_REPORT_ERROR=1
 4    +define+OVL_INIT_MSG
 5    +libext+.v+.vlib
 6    -y ../std_ovl
 7    +incdir+../std_ovl
 8    +incdir+../tb
 9    ../tb/top.v
10    +incdir+../rtl
11    ../rtl/decimal_counter.v
----------------------------------------------------------- 


complie.fの記述を参考に、Veritakのプロジェクトにファイルを追加する。ここでコンパイルするファイルは../tb/top.vと../rtl/decimal_counter.vだ。
Add Include Dirボタンで、インクルードするフォルダを指定する。7の+incdir+../std_ov だけで良さそうだ。
Add Lib Dirボタンで、ライブラリのあるフォルダを指定する。6番の-y ../std_ovlがライブラリを指定するフォルダで、5番の+libext+.v+.vlibで、ライブラリとして指定するファイルの拡張子を決定する。この機能はVeritakのこのマニアルによると、Add Lib Extボタンで追加出来るそうなのだけれど、Veritakのプロジェクトの設定画面にそのボタンが無い。Veritak BasicにはなくてProの機能なのだろうか?
define はどこで追加すると言うと、Def/Plus/Top のテキストボックスに書いて、Add Defineボタンをクリックするとdefineが適用されるらしい。compile.f の1,2,3,4番のdefineを入力した。
OVL_sample_3_100310.png

これでSave Projectボタンをクリックして、Exitボタンをクリックし、Load Verilogプロジェクトした。その結果、counter_checker_instモジュールが見つからないというエラーが出てしまった。counter_checker_instモジュールの実体は、assert_rangeなので、assert_range.vlibがライブラリとして定義出来ないのが、まずいようだ。
OVL_sample_4_100310.png

Veritakのサポートに聞いてみることにする。
(2010/03/11:追記)
Veritakのサポートに連絡したところ、早速、Add Lib Extボタンを追加して頂いた。たっくさんありがとうございました。Veritakのバージョンは3.77Eだ。
Add Lib Extボタンでvlibもライブラリとして解釈される。vlibを追加した。
OVL_sample_5_100310.png

タックさんに教えて頂いたのだが、このままシミュレーションをスタートすると、ずっとシミュレーションをやり続けてしまう。そこで、500nsecで終了するように設定する。シミュレーションメニューからRun Lengthを選択すると、ダイアログが出る。ダイアログで、Enter Time Integerに500ns を入力し、Enableをチェックした。これで500nsec シミュレーション後に停止するようだ。
シミュレーション後の様子を下図に示す。無事にシミュレーションすることができた。
OVL_sample_6_100311.png
  1. 2010年03月10日 05:51 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0

OVL(Open Verification Library)を試してみる1

次は、”OVL(Open Verification Library)フリーな検証ライブラリの話題”を見ながら、OVLを試してみようと思う。OVLはVerilogやVHDLでアサーションを利用できるライブラリだ。今までやってきたDPI-Cを使用するテストベンチはSystemVerilogの環境でないと動作しない。SystemVerilogのアサーションも約二年前にセミナを受けてきたが、Questaがないので使用できない。やはり、普段使っている言語でアサーションを簡単にかければ、デバック効率が格段に上がるのでは?と思う。デバックも何千という波形を見て、動作しているかどうかを人間が判定していると、自分が注目している動作は動作していても、他の注目していない部分がおかしくなっていることがある。その異常な動作が、すぐには他のところに波及せずに、大分シミュレーション時間が経過してから、他の部分に異常な動作となって現れる場合がある。そこで異常動作がわかっても、原因を追求するのが、難しい場合がある。その時に、最初に異常な動作が現れた最初の段階で、おかしいよと言ってくれるとデバックがとても助かる。アサーションにはそんな、チェッカーの役割を期待している。例えば、FIFOのオーバフーロー、アンダーフローをチェックするアサーションをVerilogで書いただけでも、相当便利だ。FIFOはオーバフーロー、アンダーフローを起こさないように、制御するはずなので、制御ロジックが不良なのが1発で分る。と言った訳でOVLをやってみたいと思った。
まずは”入手とインストール”を見ながら、OVLをダウンロードする。現在のバージョンは2.4だった。

(2013/06/27:追記)現在のOVL Ver. 2.7 の入手先は、”License and Statement of Use of Accellera System Initiative's Open Verification Library”です。そのWebページの”Accept agreement and proceed to download OVL.”をクリックするとダウンロード出来ます。

はじめの一歩”を参考に、ovl_example.zipをダウンロードして展開した。ovl_example/std_ovl にダウンロードしたOVL(std_ovl フォルダの内容)をコピーする。
OVLのアサーションは、tbフォルダのtop.vに書いてあるassert_rangeが使われている(はじめの一歩-テストベンチ-)。これは、アサーションベース設計、原書2版(たぶん、この本が唯一日本語で書かれているOVLの本だと思うんだけど?)の394~395ページに書かれている。それによると、assert_rangeアサーションは回路の中で、カウンタやステートマシンの値が適切な範囲にあることを保証するアサーションだそうだ。
さて、前回まで使ってきた。ModelSim AE 6.5bを起動する。”はじめの一歩”にはプロジェクトを作成することは書いていないが、前回のavalon_bfm_sim プロジェクトに上書きしても何なので、ovl_sampleプロジェクトを作成する。作成するフォルダは、ovl_example\sim とする。
FileメニューからNew -> Project... を選んで、ovl_sampleプロジェクトを作成する。ここでModelSimのキャプチャ図を貼ろうと思ったのだが、PrintScreenしておいたはずの図がなくなってしまったので省略。
OVL_sample_1_100309.png

Transcriptペインで、do all.do を実行する。するとシミュレーションがスタートした。
OVL_sample_2_100309.png

あっさりと出来ました。ログを下に示す。

do all.do
# ** Warning: (vlib-34) Library already exists at "work".
# Model Technology ModelSim ALTERA vlog 6.5b Compiler 2009.10 Oct 1 2009
# -- Compiling module clkgen
# -- Compiling module control
# -- Compiling module top
# -- Compiling module decimal_counter
# -- Scanning library directory '../std_ovl'
# -- Compiling module assert_range
#
# Top level modules:
# top
# vsim -do wave.do -l transcript.log -c top
# Loading work.top
# Loading work.clkgen
# Loading work.control
# Loading work.decimal_counter
# Loading work.assert_range
# do wave.do
# OVL_NOTE: V2.4: ASSERT_RANGE initialized @ top.counter_checker_inst.ovl_init_msg_t Severity: 0, Message: The counter arrived at invalid range.
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 105 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 115 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 125 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_max covered : time 235 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 245 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 255 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_max covered : time 415 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 425 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 435 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 445 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 455 : top.counter_checker_inst.ovl_cover_t
# OVL_COVER_POINT : ASSERT_RANGE : test_expr_at_min covered : time 465 : top.counter_checker_inst.ovl_cover_t



  1. 2010年03月09日 05:52 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:2

PS/2キーボードインターフェース用テストベンチ(task使用)のアサーション($timeformat)

たっくさんから $timeformat を教えてもらったので、もう一度、PS/2キーボードインターフェース用テストベンチを書き直した。
$timeformatの説明はこのページにあるので、詳しくはこのページを見てください。
PS/2インターフェースなので、単位はusec 、小数点以下は3桁、つまり nsec まで表示とした。

$timeformat(-6, 3, "usec", 4);


PS/2プロトコルで送ったコードとPS/2インターフェース回路で受けたコードが合わないときに表示するデータに時刻を追加した。

if (scandata != input_code) begin
    $display("Error!!!  %t, input_code = %h, scandata = %h"
        ,$time, input_code, scandata);
    $stop;
end


テストベンチの全コードを下に示す。

// ps2read_tb.v

`default_nettype none
`timescale 1ns / 100ps

module ps2read_tb;

    parameter CYCLE=20;

    reg clk, reset, ps2clk, ps2data;
    wire [7:0] scandata;
    reg [7:0] testcode;
    
    ps2read ps2read_inst (
        .clk(clk),
        .reset(reset),
        .ps2clk(ps2clk),
        .ps2data(ps2data),
        .scandata(scandata)
    );
    
    initial begin
        clk <= 1'b1;
    end
    always #(CYCLE/2)
        clk <= ~clk;
    
    initial begin
        $timeformat(-6, 3, "usec", 4);
        
        reset <= 1'b1;
        ps2clk <= 1'b1;
        ps2data <= 1'b1;
        
        #80; // リセット
        reset <= 1'b0; // リセット解除
        
        PS2_SigGen(8'h1C);
        PS2_SigGen(8'h32);
        
        #500;
        $stop;
    end
    
    task PS2_SigGen;
        input [7:0] input_code;
        integer i;
        begin
            ps2clk <= 1'b1;
            ps2data <= 1'b0; // Stop bit
            
            #40000;
            ps2clk <= 1'b0; // 立ち下がりエッジ
            #40000;
            
            for(i=0; i<=7; i=i+1) begin
                ps2clk <= 1'b1; // 立ち上がりエッジ
                ps2data <= input_code[i]; // シリアルデータ出力
                
                #40000;
                ps2clk <= 1'b0; // 立下りエッジ
                #40000;
            end
        
            ps2clk <= 1'b1;
            ps2data <= !(^input_code);
        
            #40000;
            ps2clk <= 1'b0; // 立ち下がりエッジ
            #40000;
        
            ps2clk <= 1'b1;
            ps2data <= 1'b1; // Stop bit
        
            #40000;
            ps2clk <= 1'b0; // 立ち下がりエッジ
            
            if (scandata != input_code) begin
                $display("Error!!!  %t, input_code = %h, scandata = %h"
                    ,$time, input_code, scandata);
                $stop;
            end
            
            #40000;
            ps2clk <= 1'b1; // 1に戻す
        end
    endtask
endmodule


更にわざとエラーが出るように、if 文の中を == に書き換えて Veritak でシミュレーションしてみた。
keyboard_verilog_5_071015.png

黄色の枠で囲んだところが、わざとエラーが出るようにしたところ。
ピンクの枠で囲んでいるのがエラーメッセージだ。840.080 usec でエラーが出ている。
今のところ、コードが合っているのは当たり前なのだが、PS/2インターフェース回路を後で修正したときに、意図せずに間違ったデータが出たときに教えてくれるというわけだ。
PS/2インターフェース回路などでは間違うことはないかもしれないが、たとえばPCI-Xインターフェース回路で、”Aという信号をアサートしたら、何クロック以内にBという信号をアサートする必要がある”というルールをVerilogコードまたはPSLなどで書いておく。そうすると、回路を修正していく過程で、修正する項目しかwave波形表示ウインドウで注目していなくても、それらのルールに合致しているということが自動的に証明されるはずである。
これは結構重要で、あっちを修正したはずが、こっちがだめになったということが良くある。これをwave画面上で気がつけばよいが、実際にやってみるまで気がつかないということが良くある。
もっと怖いのは、たまたまそのシステムでは大丈夫だが、ほかのシステムでテストしたときにだめということになり、あわててしまうこともある。なるべく、決まったルールはシミュレーション上で自動的に判別できたほうが良いと思う。そうでないとwave波形を見る目が血走ってぐったり疲れてしまう。心の健康のためにもアサーションを導入しようという気持ちだ。(半分冗談、こうゆう時にいまどきのブロガーは(笑)と入れるのだろうか?)
  1. 2007年10月15日 06:06 |
  2. アサーション事始め
  3. | トラックバック:0
  4. | コメント:0