はじめに

前回のアサーション記事はプロパティの中身の話でした。今日はアサーションの実行まわりの話を書きます。

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

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

GitHub - systemverilog-assertion - simple-req-ack

登場人物

前回のアサーションでは以下の4人が登場します。

DUT（dut.sv）･･･検証対象のデザインです。
アサーション（sva_req_ack.sv）･･･プロパティを書いてアサートします。
バインダー（binder.sv）･･･別ファイルに書いたアサーションを検証対象の信号にバインドします。
テストベンチ（bench.sv）･･･ DUTに刺激を与えます。

以下、簡単に紹介します。

DUT（dut.sv）

仕様は、reqが1パルス入力されると2サイクル後ackを1パルス返します。記述がヘボいのは気にしないことにします。

module dut (
    input  clk,
    input  rst_n,

    input  req,
    output ack
);
    logic req_ff, ack_ff;

    always_ff @(negedge rst_n, posedge clk)
        if (!rst_n)
            req_ff <= '0;
        else
            if (req_ff)
                req_ff <= '0;
            else
                req_ff <= req;

    always_ff @(negedge rst_n, posedge clk)
        if (!rst_n)
            ack_ff <= '0;
        else
        if (ack_ff)
            ack_ff <= '0;
        else
        if (req_ff)
            ack_ff <= '1;

    assign ack = ack_ff;

endmodule

アサーション（sva_req_ack.sv）

今回のチェッカーです。4つに似たようなプロパティを用意してアサートしています。

module sva_req_ack(input clk, rst_n, req, ack);

    // 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

    // ASSERT PROPERTY
    assert_sva_req_ack1 : assert property( sva_req_ack1(clk, rst_n, req, ack) );
    assert_sva_req_ack2 : assert property( sva_req_ack2(clk, rst_n, req, ack) );
    assert_sva_req_ack3 : assert property( sva_req_ack3(clk, rst_n, req, ack) );
    assert_sva_req_ack4 : assert property( sva_req_ack4(clk, rst_n, req, ack) );

endmodule

バインダー（binder.sv）

アサーションを接続（bind）するための記述です。sva_req_ack.svを使うのでincludeしています。
bindの文法はこんな感じのようです。

bind [アサーションを接続信号を含むmodule名] [アサーションのmodule名] [アサーションのインスタンス名] (ポート接続)

バインダーでポート宣言しない方法もありと思います。今回はポート未接続なWarningがいやだったのでポート宣言しています。

`include "sva_req_ack.sv"

module binder(input clk, rst_n, req, ack);
    // bind [BIND_TARGET] [ASSERTION_NAME] [INSTANCE_NAME_OF_ASSERTION]
    bind bench sva_req_ack i_sva_req_ack(
        // .PORT_OF_ASSERTION(PORT_OF_TARGET)
        .clk(clk),
        .rst_n(rst_n),
        .req(req),
        .ack(ack)
    );
endmodule

テストベンチ（bench.sv)

テストベンチです。DUTとバインダーをインスタンスしています。その他クロック、リセット、シナリオのtaskでできています。

`include "dut.sv"
`include "binder.sv"

module bench #(
    parameter CLK_PERIOD=10,
    parameter RESET_CYCLE=5,
    parameter RESET_ACTIVE=0
);

    logic clk, rst_n;
    logic req, ack;

    // DUT
    dut i_dut( .clk(clk), .rst_n(rst_n), .req(req), .ack(ack) );
    // Instantiate Binder 
    binder i_binder( .clk(clk), .rst_n(rst_n), .req(req), .ack(ack) );

    // TASKs
    task clk_gen();
        clk = 0;
        forever #(CLK_PERIOD/2) clk=!clk;
    endtask

    task rst_gen();
        rst_n = RESET_ACTIVE;
        repeat(RESET_CYCLE) @(posedge clk);
        rst_n <= !RESET_ACTIVE;
        forever @(posedge clk);
    endtask

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

        repeat(5) @(posedge clk);
            req = 1;
        repeat(1) @(posedge clk);
            req = 0;
        repeat(5) @(posedge clk);
    endtask

    initial begin
        fork 
            rst_gen();  // forever
            clk_gen();  // forever
            scenario();
        join_any
        $finish;
    end

endmodule

実行してみる。

みんな大好きMentorのシミュレータで実行するためのコマンドはこのようになります。

vlog *.sv

# Add -assertdebug to use assertion

vsim bench -voptargs=+acc -assertdebug

# Enable Assertion Thread View (ATV) to specify assertion
#   -enable    ... Turn on assertion thread viewing 
#   -asserts   ... Turn on assertion thread viewing for only assertion
#              (not coverage)
#   -recursive ... Assertion is turned on recursivly from PATH.
#   PATH       ... "/*", Assertion is in effect on this layer specifed by PATH.

atv log -enable -asserts -recursive /*
## To open the Assertion Window:
## View -> Coverage -> Assertions

ポイントは、

vsimコマンドに-assertdebugを追加してアサーションを有効にします。
atv（Assertion Thread View）コマンドを有効にします。
- -enable で有効化
- -asserts でATVを（カバレッジでなくて）アサーションに使います
- PATHを-recursiveで指示することで、PATH以下の階層でアサーションを有効にします。
GUI上でアサーション結果を見るためにAssertion Windowを開きます。
- メニューの View - Coverage - Assertions から開けます。

なお、vlib と run -all はお好みでお願いします。

今日はここまで

正直、自分はアサーション全然やったことがないのでして、SVAを超絶実践されている方面の方々から多大なご批判を受けそうな内容でありますが、そこは寛容にお願いしたいところであります。
次回は、今回書いている4つの似たようなプロパティについて考えられれば、と思っています。

カミは死んだ

Paper Is Dead ... osz

SVA - アサーション実行してみる？