2020年8月16日日曜日

verilog : Vivado で SVA(アサーション) を試す

目的:

Vivado で SVA を使用してみる。

結果:

Vivado で SVA 並列アサーション を記述し、アサーションができることを確認した。
  • 2021/11/4 追記
    とくに問題なくアサーションできている。
  • 2020/10/16 追記
    前回から30日以上経過しているが、アサーション結果表示できている。
  • 2020/09/04 追記
    再実行で アサーションの表示が また 出力されるようになった。
    先日、Windows版の vivado を Update したが、この影響か ?
  • 2020/08/29 追記
    再実行したところ、アサーションの表示が 出力されない。
    WEB PACK ではサポートされず、30日間無償評価で使用できていたと思われる。
但し、
  1.  property に 引数 を付けるとエラー が発生する。
  2. アサーションの結果は 波形には表示されない。
  3. アサーションの結果は Fail 時 のみ ログ, ディスプレイ に表示される。
    ( 特に処理の記述を行わない場合 )
となる。
以下のパターンで試しただけなので、他にも注意点があるかもしれないし、上の点も 設定, 記述方法等があるかもしれないが、SVA は使用可能。
(尚、波形への表示案については「Vivado で SVA(アサーション) を試す 2」を参照。)

SVA 適用手順:

Vivado の コマンドラインでのシミュレーション環境 をベースに SVA を適用した。
( SVA 適用後の サンプルは こちら を参照。)
  1. ディレクトリ構成
    アサーション格納用として assertion ディレクトリを作成
  2. アサーション用ファイルの作成
    アサーション用ファイルとして
    1. SVA ファイル ( アサーション記述のモジュール )
    2. bind ファイル ( SVA のモジュールを rtl に接続する記述 )
    3. bind リスト ( bind ファイルを インクルードする為の リスト )
    を作成する。
  3. bind ファイルのインクルード
    テストベンチに 上 の bind リスト を インクルードする。
  4. プロジェクトファイル (vlog.prj) 修正
    vlog.prj に SVA ファイル を追加する。
以上で、SVA　が適用される。

SVA 適用例:

SVA 適用例を以下に示す。
  1. テストベンチ ( Vivado の コマンドラインでのシミュレーション環境からの差分 )
      end

// include test patteern  ------------
`include "tp.sv"

// include assertion bind list -------
`include "./assertion/bind.list"


endmodule

  2. bind リスト
    `include "./assertion/bind_sva.sv"
    bind ファイルのインクルード文を記述する。
    　
  3. bind ファイル 
    bind testbench.i_plsgen sva_1 i_sva_1(
  .clk    (clk),
  .clr    (clr),
  .start  (pls_start),
  .en     (plsen),
  .outpls (output_pls)
) ;

bind testbench.i_plsgen sva_2 i_sva_2(
  .clk    (clk),
  .clr    (clr),
  .start  (pls_start),
  .en     (plsen),
  .outpls (output_pls)
) ;
    ここでは、 ２つのアサーションファイルをバインドしている。
    それぞれ RTL (i_plsgen) にバインド
    testbench には バインドできない ?
    　
  4. SVA ファイル
    アサーションファイルを以下に示す。
    尚、アサーションの適不適は不問とする。
    ( RTL は パルス生成回路 )
    // -----------------------------------------------------
//   Sample module
//
//   Module Name : sva_1
//   Version     : 0.00
// -----------------------------------------------------

module sva_1 ( clk, clr, start, en, outpls) ;
  input clk ;
  input clr ;
  input start ;
  input en ;
  input outpls ;

  // sequence description ----------------
  sequence S1 ;
    outpls[*4] ##1 !outpls[*5] ;
  endsequence

  // property description ---------------
  property p_test1 ;
    @(posedge clk ) disable iff(clr)
      $rose(start) |-> ##1 S1[*6] ;
  endproperty

  // assertion description
  a_test1 : assert property ( p_test1 ) ;

  endmodule
    sva_1 は、 start 信号の立ち上がりの次クロックから、"H 4サイクル, L 5サイクル"のシーケンスを 6回繰り返すことをチェックする。
    　
    // -----------------------------------------------------
//   Sample module
//
//   Module Name : sva_2
//   Version     : 0.00
// -----------------------------------------------------

module sva_2 ( clk, clr, start, en, outpls) ;
  input clk ;
  input clr ;
  input start ;
  input en ;
  input outpls ;

  // sequence description ----------------
  sequence S1 ;
    outpls[*4] ##1 !outpls[*5] ;
  endsequence

  // property description ---------------
  property p_test2 ;
    @(posedge clk ) disable iff(clr)
      $rose(start) |-> ##1 S1[*6] |-> ##1 $fell(en) ;
  endproperty

  // assertion description ---------------
  a_test2 : assert property ( p_test2 ) ;

  endmodule
    sva_2 は、 start 信号の立ち上がりの次クロックから、"H 4サイクル, L 5サイクル"のシーケンスを 6回繰り返した後、次サイクルで en が 立ち下がることをチェックする。
    尚、sva_1, sva_2 の 2ファイルに分ける必要は無いが (通常は 1つのファイル(モジュール) に a_test1 と a_test2 の 両方を記述する) 、サンプルの為 2つのファイルに分けている。
    　　
  5. プロジェクトファイル (vlog.prj) 
    verilog xil_defaultlib  \
"./rtl/plsgen.v" \
"./rtl/D_CNT.v" \

sv xil_defaultlib  \
"./testbench/testbench.sv" \
"./testbench/param.sv" \
"./assertion/sva_1.sv" \
"./assertion/sva_2.sv" \

verilog xil_defaultlib "/tools/Xilinx/Vivado/2020.1/data/verilog/src/glbl.v"
    プロジェクトファイルに sva_1.sv, sva_2.sv を追加する。
     

SVA 適用結果:

SVA 適用後の シミュレーション実行結果を以下に示す。
****** xsim v2020.1 (64-bit)
  **** SW Build 2902540 on Wed May 27 19:54:35 MDT 2020
  **** IP Build 2902112 on Wed May 27 22:43:36 MDT 2020
    ** Copyright 1986-2020 Xilinx, Inc. All Rights Reserved.

source xsim.dir/test_1/xsim_script.tcl
# xsim {test_1} -autoloadwcfg -runall
Vivado Simulator 2020.1
Time resolution is 1 ps
run -all
ERROR: Assertion failed.
Time: 1140 ns Started: 220 ns Scope: /testbench/i_plsgen/i_sva_1 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_1.sv Line:28
ERROR: Assertion failed.
Time: 3580 ns Started: 2480 ns Scope: /testbench/i_plsgen/i_sva_2 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_2.sv Line:28
$finish called at time : 3841 ns : File "/mnt/d/UserData/hobby/logic/study/test3/testbench/tp.sv" Line 42
exit
INFO: [Common 17-206] Exiting xsim at Sun Aug 16 15:08:32 2020...
この時の波形

テストパターンは、3回 パルスを生成。
1回目は "H" 4 クロック, "L" 5クロック を 5回繰り返し
　6回目の"H" が無い為、a_test1 が Fail
　a_test2 は 6回目 の "H" が無く 前提部が不成立の為、発火しない。(Fail しない)
2回目は H4 クロック, L5クロック を 6回繰り返し
　a_test1, a_test2 共に 発火し、Pass。

3回目は H4 クロック, L5クロック を 7回繰り返し
　6回目の "H" がある為、a_test1 は発火し、Pass
　6回目の "H"→"L" の後 7回目が開始し、en (plsen) が 立ち下がらない為、Fail
期待通り、1回目, 3回目 のパルス生成で Fail し、エラー出力されている。

発火確認:

上の結果では、Fail した場合は ERROR 表示されるが、Fail しない場合は 何も表示されない。
この為、Pass したのか 発火しなかったのかの区別がつかない。
発火した場合に表示する様に SVA ファイルを修正してみる。
  // assertion description
  a_test1 : assert property ( p_test1 ) $display("a_test1 : OK") ;

  endmodule

  // assertion description ---------------
  a_test2 : assert property ( p_test2 ) $display("a_test2 : OK") ;

  endmodule
assert文 に 処理 ($display 等) を追加する。
処理追加後の結果は下の通り。

****** xsim v2020.1 (64-bit)
  **** SW Build 2902540 on Wed May 27 19:54:35 MDT 2020
  **** IP Build 2902112 on Wed May 27 22:43:36 MDT 2020
    ** Copyright 1986-2020 Xilinx, Inc. All Rights Reserved.

source xsim.dir/test_1/xsim_script.tcl
# xsim {test_1} -autoloadwcfg -runall
Vivado Simulator 2020.1
Time resolution is 1 ps
run -all
ERROR: Assertion failed.
Time: 1140 ns Started: 220 ns Scope: /testbench/i_plsgen/i_sva_1 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_1.sv Line:28

Time: 2340 ns Started: 1260 ns Scope: /testbench/i_plsgen/i_sva_1 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_1.sv Line:28
a_test1 : OK

Time: 2360 ns Started: 1260 ns Scope: /testbench/i_plsgen/i_sva_2 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_2.sv Line:28
a_test2 : OK

Time: 3560 ns Started: 2480 ns Scope: /testbench/i_plsgen/i_sva_1 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_1.sv Line:28
a_test1 : OK
ERROR: Assertion failed.
Time: 3580 ns Started: 2480 ns Scope: /testbench/i_plsgen/i_sva_2 File: /mnt/d/UserData/hobby/logic/study/test3/assertion/sva_2.sv Line:28
$finish called at time : 3841 ns : File "/mnt/d/UserData/hobby/logic/study/test3/testbench/tp.sv" Line 42
exit
INFO: [Common 17-206] Exiting xsim at Sun Aug 16 16:19:29 2020...

実行結果は、
1回目 (started: 220nS) は a_test1 Fail し、a_test2 は発火なし。
2回目 (started: 1260nS) は a_test1, a_test2 共に発火し、Fail なし。
3回目 (Started: 2480nS) は a_test1 は発火して Failなし, a_test2 は Fail。
となり、発火したことを確認できる。

できれば、波形に 表示されるといいのだが、、、
　→　表示案 : Vivado で SVA(アサーション) を試す 2　

時刻:

0 件のコメント:

コメントを投稿

登録: コメントの投稿 (Atom)