はじめに

このエントリは結構前に書いたのですが内容が中途半端で意味不明だったので保留していたものです。が、ネタが無いので公開しておきます...

今更ですがSystemVerilogのスタディをコツコツはじめました。今回は、みんな大好きSVA（SystemVerilogAssertion）についてメモします。

SVAを構成する品々

SVAは、論理式（Boolean）、または、論理式を時系列に記述したシーケンス（Sequence）をプロパティ（Property）とし、assertディレクティブ（Directive）でアサーション化するものです（日本語、変ですね...osz）。内訳はこんな感じです。

SVAの静的な条件式です。Verilogの論理式で記述します。

Boolean（またはSequence）を時系列に組み合わせたものです。 [] (中カッコ)を使ってシーケンスの繰り返しを表現します。

	メモ
[*N]	N回の連続な繰り返し
[*M:N]	M回以上、N回以下の繰り返し
[=N]	N回の非連続な繰り返し。最後の事象発生後に事象が発生しない期間が続いてもよい
[->N]	N回の非連続な繰り返しで、最後の事象発生で終了

Sequence（Boolean）の因果関係を組み合わせてアサーションで確認したい条件式を作成します。

不思議な矢印（|=>、|->：Implication）を使ってアサーションの開始条件と、その後に期待する事後条件を書きます。

Implicationには2種類あります。

Implication	メモ
SEQ_A \|=> SEQ_B	SEQ_A成立の1サイクル後のSEQ_Bが発生する
SEQ_A \|-> SEQ_B	SEQ_A成立と同じサイクルでSEQ_Bが発生する

また、プロパティに記述するシーケンスの動作クロックの指定や名前を指定した部品化ができます。

property p_req_ack_done;
    @(posedge clk) req ##[*1:5] ack |=> done;
endproperty

またパラメータ化ができます。

property p_req_ack_done_param（req_param, ack_param, done_param）;
    @(posedge clk) req_param ##[*1:5] ack_param |=> done_param;
endproperty

property記述はassertすることで実際のアサーション記述になります。

assert property @(posedge clk) req ##[*1:5] ack |=> done;

またはラベル名を付けたり、プロパティ名の指定もできます。

label_if : assert property (p_req_ack_done);

パラメータ化したプロパティの場合はこんなです。

label_if_param : assert property (p_req_ack_done_parm(req, ack, done));

アサーションはmodule内に記述して実行します。アサーションの記述形態は以下のようになるでしょか。

BIND記述はこんな感じです：

bind DUTモジュール名 アサーショモジュール名 バインド時のインスタンス名(接続)

コードだとこんな感じでしょうか（いろいろry）。

bind i_dut assert_module i_a_if1(.req(req), .ack(ack), .done(done));

SVAアサーションの概要をメモしました。次回は具体例な記述など書いてみたいと思っています。きっと無理だな...osz