verilog : SVA による検証概要

目的:

SVA の概要について 理解した内容を 記す

SVA とは:

System Verilog Assertion の略。
System Verilog の アサーション記述言語。
内部論理の期待動作の検知 や 禁止動作を監視する。
 ( 期待通りに動作しない場合等を検出する )

SVA 適用手順:

SVA を適用するには、以下の記述を行う。

1. SVA ファイル記述
   SVA 用のモジュールを作成する。
   SVAは、通常のRTL内にも記述できるが、
   
   1. ifdef などで合成時に無視できるようにする必要がある。
   2. module が system veerilog として扱われるため、RTL に system verilog の記述が混ざっても検証時には気づけない。 
      ( RTL を verilog で記述する場合 )
   等の注意が必要な為、SVA用のモジュールにした方が良いと感じる。
2. bind ファイル記述
   SVA ファイル を RTL の信号 に紐づける。
   SVA ファイルで 直接 RTLの信号を記述することもできるが、bind ファイルを 使用することで複数の信号に同じ SVA を適用できる。

SVA ファイルの記述:

SVA のファイルは、通常の module と同様に作成する。
但し、output ポートは無い。(必要無い)
SVA の module には、
　通常の rtl 記述
　property 記述
　assertion 記述
 を行う。
例 : sva_test.sv

module sva_test ( clk, rst_n, sig1, sig2) ;
  input clk ;
  input rst_n ;
  input sig1 ;
  input sig2 ;

  // property 記述
  property p_test1(x, y) ;
    @(posedge clk ) disable iff(~rst_n)
        $rose(x) |-> ##1 fell(y) ;
  endproperty

  // assertion 記述
  a_test1 : assert property ( p_test1 ( sig1, sig2) ) ;

endmodule

property 記述 と assertion 記述 を １つ にして

a_test1 : assert property (
    @(posedge clk ) disable iff(rst)
        $rose(sig1) |-> ##1 fell(sig2)
) ;

の様にも記述できるが、property 記述 と assertion 記述 を 分けると、1つのproperty 記述を 複数の asertion 記述で使用できる。

property 記述 については、SVA の property 記述概要 を参照

bind ファイルの記述:

アサーションの バインディングは 以下の様に行う。
 bind <bind先モジュール名> <アサーションモジュール名>  <インスタンス名> (
   ポート 接続 記述
) ;
例

bind DUT sva_test  sva_test1 (
  .clk    (clock),
  .rst_n (reset_n) ,
  .sig1   (signal_1) ,
  .sig2   (signal_2) ,
) ;