[SVA] 1. SystemVerilog アサーション

SVA (SystemVerilog Assertion) は論理回路の検証手法の一つです。
SVA を使う主な目的としては「目視による確認漏れを減らす」や「バグの早期発見」だと思いますが、その辺りの話は放り投げて、記述方法についてを数回に分けてまとめたいと思います。

私は基本的なことしか書けないので、詳細について知りたい方は IEEE Std 1800-2017 を参照してください。(私はあまり読みたくないです。1300ページ超えてますし...)

今回は SVA の構文について。SVA には即時アサーション (Immediate assertion) と並列アサーション (Concurrent assertion) があります。

即時アサーション

即時アサーションは、記述したタイミングでのみチェックを行い、指定した条件を満たさなかった場合に発火します。記述できる場所は module, program, class 等です。(他にもあるのかな？) always, task, function initial, final 文などで使います。

即時アサーションの構文は以下になります。else の前で改行していますが、しなくてもいいです。

　<ラベル> : assert ( <条件> ) <処理1>;
             else              <処理2>;

条件 を満たしている場合(アサーションOK)は 処理1 が実行され、条件 を満たさなかった場合(アサーションNG)は 処理2 が実行されます。
処理1/2 は、システムタスク $fatal, $error, $warning, $info を使ってメッセージを出力させるのが一般的なようです。しかし、検証環境が UVM であれば `uvm_fatal, `uvm_error `uvm_info 等を使った方が個人的にはいいと思います。(私は省略するか $display を使うことが多いです。)

ラベル, 処理1/2, else は省略できますが、ラベルはシミュレーションログのチェック時に判別し易くなるので、個人的には省略しない方がいいと思います。また、処理1 のみを省略した場合は ; も消す必要があるので注意してください。

　<ラベル> : assert ( <条件> );

  <ラベル> : assert ( <条件> )
             else <処理2>;

処理が複数ある場合は begin - end で括ってください。

　<ラベル> : assert ( <条件> ) begin
                                 <処理1>;
                                 <処理2>;
                               end
                               else begin
                                 <処理3>;
                                 <処理4>;
                               end

■ サンプル

以下の例では、シミュレーション開始から 10us 後に信号 a の状態をチェックします。信号 a が 0, x, z の場合に発火します。

  initial begin
    #10us;
    sva_state : assert (a) $info ("[SVA INFO ] OK");
                else       $error("[SVA ERROR] NG");
  end

always_comb (または always @(*)) と組み合わせることで、モジュール間の信号接続チェック等にも使えます。

  always_comb begin
    sva_connect : assert (top.xxx.a === top.yyy.a);
  end

並列アサーション

並列アサーションについてですが、単純に SystemVerilog アサーションといえばこちらを指すことが多いです。即時アサーションとは違い、シミュレーションと並行してクロックエッジを契機にチェックを行います。記述できる場所は module, program, interface 等です。class は無理かも。
並列アサーションは、シーケンス(sequence) とプロパティ(property) を組み合わせて記述します。

シーケンスには信号の振る舞いを記述します。
プロパティにはシーケンスの因果関係を記述します。

シーケンスとプロパティの構文は以下になります。

　sequence <シーケンス名> (<引数>);
    ...;
  endsequence

  property <プロパティ名> (<引数>);
    @(posedge clock)  <シーケンス>;
  endproperty

  property <プロパティ名> (<引数>);
    @(posedge clock)  <シーケンス> |=> <シーケンス>;
  endproperty

posedge は negedge でもいいです。信号に遅延が挿入されていて思うように動かない場合は negedge を使いましょう。
プロパティ内の |=> は1サイクル後を表します。同タイミングを表したい場合は |-> になります。シーケンスとプロパティの詳細については後日まとめたいと思います。

また、プロパティはそれだけでは機能せず assert でプロパティを指定することで有効になります。ラベル, 処理1/2, else については、即時アサーションの時と同様に省略できます。

　<ラベル> : assert ( <プロパティ名> ) <処理1>;
             else                      <処理2>;

■ サンプル

簡単な例として a という信号が1サイクルのパルスであることをチェックするアサーションを記載します。(サンプルとして適切ではない気もしますが...)


  // シーケンス
  //--------------------------
  /* a = 0 の 1サイクル後に a = 1 (立ち上がり検出) */
  sequence s1;
    (a == 0) ##1 (a == 1);
  endsequence

  /* a = 0 */
  sequence s2;
    a == 0;
  endsequence

  // プロパティ
  //--------------------------
  /* s1 を満たした次のサイクルで s2 を満たすこと */
  property p1;
    @(posedge clock)  s1 |=> s2;
  endproperty

  // プロパティを有効にする
  //--------------------------
  SVA_P1 : assert property(p1);

シーケンスの記述はプロパティ内でも使えますので、下記のようにプロパティだけで記述することもできます。


  // プロパティ
  //--------------------------
  /* a = 1 を満たした次のサイクルで a = 0 を満たすこと */
  property p1;
    @(posedge clock)  (a == 0) ##1 (a == 1) |=> (a == 0);
  endproperty


  // プロパティを有効にする
  //--------------------------
  SVA_P1 : assert property(p1);

また、システムタスクを使用すると分かりやすくなります。$rose は立ち上がりの判定をし、$fell は立下りの判定をします。アサーションでよく使うシステムタスクについても後日まとめたいと思います。


  // プロパティ
  //--------------------------
  /* a の立ち上がりを検出した次のサイクルで a が立ち下がること */
  property p1;
    @(posedge clock)  $rose(a) |=> $fell(a);
  endproperty


  // プロパティを有効にする
  //--------------------------
  SVA_P1 : assert property(p1);

波形で確認すると以下のようになります。

また、クロックを negedge にすると波形は以下のようになります。

私は negedge の方がタイミングがはっきりするので好きです。デルタ遅延でハマる心配もないですし。

おまけ

$fatal, $error, $warning, $info について。[] 内は省略可能です。シミュレータによるのかもしれませんが、$fatal は発火した時点でシミュレーションが終わるので注意が必要です。

　$fatal   [ ( finish_number [, list_of_arguments ] ) ] ;
  $error   [ ( [ list_of_arguments ] ) ] ;
  $warning [ ( [ list_of_arguments ] ) ] ;
  $info    [ ( [ list_of_arguments ] ) ] ;

  finish_number = 0 | 1 | 2

平凡なる好奇

2019年6月7日金曜日