SystemVerilog Assertion (SVA) のノウハウまとめ
随時更新予定です。
目次
SystemVerilog Assertion (SVA) とは
SVAは論理回路の検証手法
- 自動検証によるヒューマンエラー削減
- 仕様変更による影響範囲の確認
- 検証エビデンスとして明確
SVAの仕様詳細は以下SystemVerilogの仕様書を参照
SVA簡易実装例:
- Signal_A がアサートされてから 4 cycle以内に Signal_B がアサートを確認
SystemVerilog:
bind TB sva_module u_sva_module();
`define DUT_PATH TB.top
module sva_module();
localparam N = 4;
property p_A_to_B_within_N(
logic clk
, logic rstn
, logic sig_a
, logic sig_b
);
@(posedge clk) disable iff (!rstn)
$rose(sig_a) |-> ##[1:N] $rose(sig_b);
endproperty
assert property (p_A_to_B_within_N (
.clk (`DUT_PATH.clk)
, .rstn (`DUT_PATH.rstn)
, .sig_a (`DUT_PATH.Signal_A)
, .sig_b (`DUT_PATH.Signal_B)
))
else $error("Signal_B did not assert within %0d cycles after Signal_A", N);
endmodule並列アサーション
- 時系列のパターンを記載するシーケンス部分をプロパティとして定義することで記述 (上の例)
- シミュレーションと並行して、クロックエッジ（もしくは他信号のエッジ）をトリガーに条件をチェックを実施
即時アサーション
アサーションを有効にしている間チェックされ続ける並列アサーションと違い、コード中に記述した特定のタイミングでのみチェック
記載例：
initial begin
#100us;
sva_state : assert (TB.top.Block_A.y === TB.top.Block_B.y) $info ("[SVA] OK");
else $error("[SVA] ERROR");
end次のようにalways_combを使って記載することで「信号の接続検証」も可能
always_comb begin
sva_connect : assert (TB.top.yyy.y === TB.top.xxx.y);
endSVAチェック可能な代表条件
SVAで使用される演算子
プロパティ演算子
遅延
繰り返し
その他演算子
ended メソッド
あるシーケンスAと、あるシーケンスBに順序関係がある場合、endedメソッドを使用して片方のシーケンスAの終了を待って、もう片方のシーケンスBの開始条件を定義できる。
例：
Writeアクセスのシーケンスが完了してから、Readアクセスのシーケンスへ移行
// Write Check シーケンス
sequence write_seq;
wr_req ##[1:2] wr_ack;
endsequence
// Read Check シーケンス
sequence read_seq;
rd_req ##[1:3] (rd_valid && rdata == wdata);
endsequence
// Writeが完了してからRead条件の確認
property write_then_read_check;
@(posedge clk)
write_seq.ended |-> read_seq;
endpropertytriggered メソッド
シーケンスが成立したイベントを検出して、次のシーケンスの確認を実施
例：
Req/Ackのイベントが発生したことを確認して、Responceの確認へ移行
// Req-Ack 成立
sequence req_seq;
req ##1 ack;
endsequence
// Responce Check
property resp_check;
@(posedge clk)
req_seq.triggered |-> ##[1:5] resp;
endproperty
strong メソッド
シーケンスの完了を必ず保障するための演算子として用います。評価途中でSimulationが終了した場合もErrorを発火させることが可能例：
// req が起きたら ack が"必ず"成立する
assert property (@posedge clk req |-> strong(##1 ack));Assertion関連システムタスク
重大度のレベルとメッセージ出力
失敗の重大度を示すメッセージと、指定したテキストを表示します。主に次のような情報がLogに出力されます。
- アサーション名
- アサーションの実装されている階層
- アサーションの実装されているファイル名、行番号
- アサーションによるチェックの行われたシミュレーション時間
$fatalが呼び出されると、暗黙的に$finishが呼び出されて処理が終了します。
SVAの有効無効切り替え制御
SystemVerilogのシステムタスク ON/OFF
使用例：
$asserton (<階層の深さ>, <基準階層>)
基準階層：
- 階層で指定する場合 : (top.assertのように階層指定)
- 特定アサーションのみ指定する場合 : 階層＋ラベル名を指定
階層の深さ：
- 基準階層以下全て：0
- 基準階層以下から指定した深さ：0以外
SVAの応用記述
シーケンスに対応した命令実行
(シーケンス, 命令分) のように記載することで、あるシーケンス成立時に特定の命令を付与することが可能です。
実装例：
// シーケンスに対応した命令実行
property prop_sequence_example;
($rose(req), $display("Detect assert Req")) |-> ##1 (ack, $display("Detect req ##1 ack"));
endpropertyプロパティ内で変数の宣言
プロパティの宣言内で、変数を宣言することが可能です。外部に宣言した変数をプロパティ内部で参照することはできないため、そのような場合には、引数として値を引き込む必要があります。
下記では、t_reqという変数を時間の保存用として宣言しています。
実装例：
// プロパティ内で変数宣言
property req_ack_within_time;
realtime t_req;
@(posedge clk)
// req発生時に時刻保存
(req, t_req = $realtime)
// ackが来たとき時間差チェック
|-> ##[0:$] (ack && ($realtime - t_req <= 100ns));
endproperty参考：
