[SVA] 5. その他

SVA (SystemVerilog Assertion) の基本的な記述方法について、前回までの内容を見ていただければなんとなく理解していただけるのではないかと思います。高位合成が流行るにつれてSVAを使う機会がどうなっていくのか私には想像できませんが、あと数年は使うことになるのではないでしょうか。

今回の記事は SVA に関連あるけど、知らなくてもおそらく問題ない内容となっています。

並列アサーションの記述方法

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

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

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

上記が並列アサーションの基本形だとは思うのですが、私は sequence は使わずにシーケンスの構文を property 内に記述することがほとんどですし、assert 内にプロパティの構文を記述する場合もあります。
完全に好みの話になるのですが、、、
「(A = 1) の条件を満たすとき、次のクロックエッジで (B=1) となること」
を例として色々な記述方法について紹介したいと思います。
(sequence や、assert の <処理> については今回は触れません。)

まずは、上にも書いた assert 内でプロパティ構文を使用する方法。1行で書けるので見た目はスッキリします。

SVA_P1: assert property (@(posedge clock)  A |=> B);

property に名前を付けて assert の外に出すと以下のようになります。プロパティ名は p1 としてみました。

property p1;
  @(posedge clock)  A |=> B;
endproperty

SVA_P1: assert property( p1 );

property は引数を与えることも可能ですので、同じチェック内容が複数ある場合は以下のようにすると記述量を抑えることができます。最もよく見かける構成だと思います。引数の型やbit幅は不要です。

property p1 (clock, a, b);
  @(posedge clock)  a |=> b;
endproperty

SVA_P1: assert property( p1(CLOCK1, A1, B1) );
SVA_P2: assert property( p1(CLOCK2, A2, B2) );
...

こちらはあまり見かけませんが always を使用して property 内のクロックエッジ記述を外に出すこともできます。

property p1 (a, b);
  a |=> b;
endproperty

always @(posedge CLOCK1) begin
  SVA_P1: assert property( p1(A1, B1) );
  ...
end

always @(posedge CLOCK2) begin
  SVA_P2: assert property( p1(A2, B2) );
  ...
end

信号の参照方法

SVA を interface に記述する場合は、interface 内の信号を使用すると思いますが、module に記述する場合は他の module で使用している信号を参照すると思います。参照の仕方は主に以下の3つになるのではないでしょうか。
　1. 信号のパスを直接指定
　2. wire で一旦別の信号に繋げて使用
　3. bind を使用

1 の信号のパスを直接指定する方法は、以下のようになります。階層が深い場合は信号毎に改行しないと見にくいかもしれません。

property p1;
  @(posedge clock)  A |=> B;
endproperty

SVA_P1: assert property( p1(top.dut.CLOCK, top.dut.A, top.dut.B) );

また、階層が深い場合は define を使用してパスを置き換えると見やすくなります。今回の例では階層が浅いので見た目はあまり変わりませんが top.dut を D_DUT に置き換えると以下のようになります。

`define D_DUT  top.dut

property p1;
  @(posedge clock)  A |=> B;
endproperty

SVA_P1: assert property( p1(`D_DUT.CLOCK, `D_DUT.A, `D_DUT.B) );

2 のwire で一旦別の信号に繋げて使用する方法は、以下のようになります。(logic ではなく敢えて wire)

wire CLOCK = top.dut.CLOCK;
wire A     = top.dut.A;
wire B     = top.dut.B;

property p1;
  @(posedge clock)  A |=> B;
endproperty

SVA_P1: assert property( p1(CLOCK, A, B) );

3 の bind を使用する方法についてですが、上の2つの方法と比べると少しだけ複雑かもしれません。bind はアサーション以外でも使えますが、私はあまり好きではないのでほとんど使いません。

bind は別に用意したモジュールを、既存の module の下に外から無理矢理インスタンスさせる機能です。
以下の画像の例ですと、bbb という bind 用のモジュールを作っておいて、それを aaa モジュールの下に bind させています。※太字がモジュール名で () 内はインスタンス名になります。

bind の指定は以下のようになります。
bind <対象モジュール名>:<対象パス> <bindモジュール名> <bindインスタンス名> (<接続>);

bbb.sv
module bbb
 (
  input  clock,
  input  a,
  input  b
  );

  property p1;
    @(posedge clock)  A |=> B;
  endproperty

  SVA_P1: assert property( p1(CLOCK, A, B) );

endmodule

// bind 処理
bind  aaa:top.dut  bbb  dut_bind (.*);

<接続> は上記のように (.*) として省略できますが、必要であればモジュールをインスタンスする時の要領で接続してください。