ModelSim/QuestaSim SystemVerilogアサーションのすすめ

2024/08/30

ModelSim DE/QuestaSimではSystemVerilogアサーションが標準機能として使用可能です。標準機能のため追加費用なしで使用することができます。ここではそのメリットと実行方法を説明します。

本ブログの内容はModelSim DEやQuestaSim、また、Questa Intel FPGA Edition, Questa Intel FPGA Starter Editionなどでもご利用いただけます。SystemVerilogを使用するためVerilog言語が扱えるライセンスが必要となり、VHDL単言語ライセンスではご使用できませんのでご注意ください。

ModelSim簡易チュートリアル
【アサーション編】
の詳細を見る

アサーションとは

SystemVerilogアサーションは、デザインの入出力ポートや内部信号にアサーションを監視モニターとして挿入し、
シミュレーション中に仕様と異なる異常動作検出、または正常動作の確認、さらに人手による波形目視確認を自動化する
便利な検証手法です。

波形の目視確認では、同一の確認内容を場合によっては数十カ所にわたり人手で確認を行わなくてはならず、そのため多くの時間を費やし、確認ミスも起こりやすくなります。アサーションを使用することで、これらの確認作業を自動化し、
さらに確認ミスを防止することもできます。

【アサーション記述例】

リセット解除後、リクエスト信号reqがアサートされると2～4クロックサイクル後にアクノリッジackがアサートされる。

左右にスクロールしてご覧ください

p_reqack_chk: assert property( @(posedge clk) disable iff( ~rst_n )
	req |-> ##[*2:4] ack );

p_reqack_chk:	アサーションラベル名、FAIL時のログにこの名称が表示されるまた、波形ダンプや波形表示で使用する名称となる
assert property();	プロパティ（アサーション）記述
@(posedge clk)	各信号のサンプリング、Waitカウントするクロック通常はreq,ack信号と同期するクロックを指定
disable iff(~rst_n)	アサーションチェック除外指定。rst_nが‘0’の時チェック除外 disable ifでなくdisable iffであることに注意
req	Verilog/SystemVerilogと同じ解釈でreq==1’b1と同じ意味
\|->	インプリケーション、左辺が成立すると同じサイクルで右辺を評価通常左辺がトリガとなり右辺がチェック内容となる
##[*2:4]	Waitクロックサイクル指定、この場合は2～4クロックサイクル
ack	ack==1’b1と同じ意味

リクエストのアサートに対し2～4クロックサイクル以内でアクノリッジが返される場合、アサーションはPASS（仕様通りの動作）となり、2～4クロックサイクル以内にアクノリッジが返されない場合はFAILとなります。結果はシミュレーションログファイルにシミュレーション時刻とFAILしたアサーション名が生成されます。また、波形ダンプを行っている場合には波形ウィンドウにフェイルマークが赤色で表示されます。

アサーションのメリット

監視モニター（アサーション）を挿入し波形目視を自動化
アサーションがシミュレーション実行中、常に仕様通りの正しい動作をしているか監視します。
そのためシミュレーション後に波形の目視チェックを行う必要がありません。
不具合検出の漏れを防止
デザイン内部に記述されたアサーションが不具合を検出しFAILすることで、デザイントップの出力ポートに伝播しない内部の不具合も見逃すことがなくなります。
不具合検出、原因解析の時間を短縮
デザイン内部に記述されたアサーションがFAILした場合、アサーションから回路のfan-inを即座に探査できます。
デザイントップの出力ポートから探査する場合と比較し、短時間で原因箇所にたどり着けます。
不具合修正後の確認時間を短縮
不具合修正後、再度同じアサーションを用いてシミュレーションを行うことで、不具合修正の確認を自動で容易に実行できます。
デザインの仕様が明確になる
アサーションを記述するには緻密な仕様が必要です。そのため仕様の正確な理解と確認がアサーション記述前に必要となります。仕様が曖昧な場合はこの時点で確認が行えるので、仕様確認の過程で不具合を見つける効果もあります。

アサーション記述方法

アサーションは仕様を基に記述します。仕様から直接アサーションを記述するとミスが入りやすくなります。
そのため、まずは記述を行うアサーションを日本語など文章化することをお勧めします。文章をまとめる過程で自分が理解していない仕様の詳細に気づく効果もあります。

1）アサーション記述箇所の抽出と文章化

アサーションをどこに挿入するか悩む方も多いと思います。先に記載した通りアサーションは波形目視を自動化することが主な目的の一つとなるので、「シミュレーション実行後、どの信号をどのように波形で確認しますか」と考えるとよいでしょう。

例えば、以下のUART送信ブロックの場合を想定すると次のようになります。

リセット実行時の確認	iRSTがアサートされるとoSERIALが1になる iRSTがアサートされるとoBUSYが0になる
STARTビット送出	iWENがアサートされoBUSYが0のとき、1クロックサイクル後sSERIALが0になる
8ビット送信データ	スタートビット送出後、LSB側から1ビットずつ8クロック連続で送信
STOPビット送出	iWENがアサートされoBUSYが0のとき、9クロックサイクル後sSERIALが1になる

今回の例ではテストベンチでシリアル変換される8ビットデータの期待値照合は、Verilog記述で行っているため
アサーション記述は行いません。

2）アサーション記述

アサーション記述箇所の文章が完成したらアサーションを記述します。
明確に仕様を加味した文章を事前に書くことで、誰でも簡単にアサーション記述が行えます。

左右にスクロールしてご覧ください

// iRSTがアサートされるとoSERIALが1になる（oSERIALリセット）
p_reset_oSERIAL: assert property( @(posedge iCLK)
    iRST |-> ##1 oSERIAL==1'b1 );

// iRSTがアサートされるとoBUSYが0になる（oBUSYリセット）
p_reset_oBUSY: assert property( @(posedge iCLK)
    iRST |-> ## 1 oBUSY==1'b0 );

// iWENがアサートされoBUSYが0のとき、1クロックサイクル後sSERIALが0になる
//STARTビット送出
p_start_bit: assert property( @(posedge iCLK) disable iff( iRST )
    iWEN & ~oBUSY |-> ##1 oSERIAL==1'b0 );

// iWENがアサートされoBUSYが0のとき、9クロックサイクル後sSERIALが1になる
//STOPビット送出
p_end_bit: assert property( @(posedge iCLK) disable iff( iRST )
    iWEN & ~oBUSY |-> ##9 oSERIAL==1'b1 );

アサーション記述を行うファイルはいくつか種類があります。

テストベンチがVerilog/SystemVerilogの場合はテストベンチに記述
- テストベンチにアサーションを直接記述し、変数は階層参照を使用
- ModelSim/QuestaSimでは下位階層がVHDLでもVerilog/SystemVerilogテストベンチから階層参照が可能
- 簡単に記述ができるメリットがある
独立したmodule内にアサーションを記述し、そのmoduleをbind文で検証対象のmoduleに設定
- テストベンチがVHDLの場合はこの方法のみ
- テストベンチがVerilog/SystemVerilogでも利用でき、言語依存がなく再利用がしやすい
- 記述に少し手間がかかるデメリットがある

今回は最も簡単なテストベンチにアサーション記述を行います。
そのため各信号はテストベンチトップからの階層表記を使用して記述します。

以下、記述例となります。

左右にスクロールしてご覧ください

module tb;
//Signal Declaration
logic iCLK;
logic iRST;
	:
//DUT instance
    dut U_0( … );
	:
//Test Pattern Generator
    initial iCLK=0; always #50 iCLK=~iCLK;
	:
//SystemVerilog Assertion
p_reset_oSERIAL: assert property( @(posedge U_0.iCLK)
        U_0.iRST |-> ##1 U_0.oSERIAL==1'b1 );
p_reset_oBUSY: assert property( @(posedge U_0.iCLK)
        U_0.iRST |-> ## 1 U_0.oBUSY==1'b0 );
p_start_bit: assert property( @(posedge U_0.iCLK) disable iff( U_0.iRST )
        U_0.iWEN & ~U_0.oBUSY |-> ##1 U_0.oSERIAL==1'b0 );
p_end_bit: assert property( @(posedge U_0.iCLK) disable iff( U_0.iRST )
        U_0.iWEN & ~U_0.oBUSY |-> ##9 U_0.oSERIAL==1'b1 );
endmodule

シミュレーション実行方法

コンパイルは通常通り実行します。ただしアサーション記述を行ったファイルのファイルタイプが.vの場合、.svに変更して実行ください。

シミュレーション実行にはオプション設定が必要な場合があります。
ModelSim/QuestaSimともにデフォルトではアサーションがPASSしたカウントを取集しません。
（FAILカウントは収集します）
アサーションが正しく動いたか確認したい場合や何回アサーションが実行されたかを正確に確認したい場合には、
シミュレーション実行時にオプション指定を行います。

メインメニューからSimulation > Start Simulationを選択し、Designタブで通常通りテストベンチトップを指定します。
次にOthersタブのEnable assertion debugをクリックし、Other Vsim Options欄に-assertdebugを入力しOKボタンを押してシミュレータを起動します。

シミュレータが起動したら各アサーションの波形登録を行います。
メインウインドからView > Assertionを選択しアサーションウインドを開き、読み込まれたアサーションを選択し、
マウス右クリックで波形を登録します。

必要に応じてその他デザイン、テストベンチのポートや信号を波形登録します。

アサーション結果解析

シミュレーション実行し終了したら解析を行います。波形登録されたアサーションは関連する信号をグループ化して表示し、パス、フェイルをマーカで表示します。

アサーションウインにはPASSカウント、FAILカウントが表示され何回アサーションが実行されたかを確認することができます。FAILしたアサーションは赤字で表示されます。

アサーションがFAILした場合、メッセージがTranscriptに生成されます。そのメッセージをダブルクリックすると波形ウィンドウでカーソルがFAILした時刻を指し示します。またメッセージにはアサーションのどのExpressionでFAILしたが表示されます。

ModelSim簡易チュートリアル【アサーション編】ダウンロード

今回の記事の作成に使用したModelSim DE/QuestaSim用SystemVerilogアサーションの実行サンプルと、今回紹介できなかったBIND文を使用したサンプルも入れました。
またチュートリアルではModelSimを使った具体的な実行手順とデバッグ機能の使用方法も含まれています。
ご興味ございましたら以下からダウンロードください。

ModelSim簡易チュートリアル
【アサーション編】
の詳細を見る