[SVA] 4. system function と control task

SVA で使えるシステムファンクションとコントロールタスクの基本的な記述方法についてまとめます。省略している箇所も多々ありますので、詳細については IEEE Std 1800-2017 を参照ください。

Sampled value system functions

信号の変化や値の取得を行うシステムファンクション群です。

$sampled ( <信号> )	信号値を取得
$rose ( <信号> )	立ち上がりの判定
$fell ( <信号> )	立ち下がりの判定
$stable ( <信号> )	無変化の判定
$changed ( <信号> )	変化の判定
$past ( <信号> [, <遡るクロック数>])	過去の信号値を取得

$sampled は値を取得するだけです。存在理由がよく分かりません。
$rose, $fell, $stable, $changed は1つ前のクロックエッジ時の値とを比較して判定します。x, z も変化の対象になります。例えば、$fell は x → 0 や z → 0 の変化にも反応します。
$past は指定したサイクル数分遡って値を取得することができます。<遡るクロック数> を省略した場合は 1 と見なされます。

■ サンプル

  /* a と b が同じタイミングで立ち上がること */
  property p1;
    @(posedge clock)  $rose(a) |-> $rose(b);
  endproperty

  SVA_P1 : assert property(p1);

  /* a が 0 のとき b が変化しないこと */
  property p1;
    @(posedge clock)  ~a |=> $stable(b);
  endproperty

  SVA_P1 : assert property(p1);

↑具体的には AXI4 interface の Ready 信号が落ちているときに Data が変化しないこと等の使い方ができます。

  /* a の立下りを検出したとき 1 サイクル前の b の値が 0 であること */
  property p1;
    @(posedge clock)  $fell(a) |-> $past(b, 1) == 0;
  endproperty

  SVA_P1 : assert property(p1);

Bit vector system functions

多ビット信号の状態や、x, z を含むかどうかを判定するシステムファンクション群です。

$countbits ( <信号>, <値>)	指定した値（0、1、x、z）の数を取得
$countones ( <信号> )	1 の数を取得
$onehot ( <信号> )	信号がワンホットであることを判定
$onehot0 ( <信号> )	信号がワンホットもしくは ALL 0 であること判定
$isunknown ( <信号> )	信号に x，z を含むかどうかを判定

■サンプル


  /* a [3:0] に含まれる 1 の数が 2つ以下であること */
  property p1;
    @(posedge clock)  $countbits(a[3:0], 1) <= 2;
  endproperty

  SVA_P1 : assert property(p1);

Assertion control tasks

アサーションの有効/無効をコントロールするタスク群です。module 内で initial や task 等で記載することが多いかと思います。

$asserton [(<階層の深さ> [, <基準階層>])]	アサーションを有効化
$assertoff [(<階層の深さ> [, <基準階層>])]	アサーションを無効化
$assertkill [(<階層の深さ> [, <基準階層>])]	アサーションを無効化 (強制終了)

<階層の深さ> は 0 と 0 以外で意味合いが異なります。
0　　：基準階層以下を全て
0以外：基準階層以下から指定した深さまで (1 設定時は基準階層のみ)
<階層の深さ> を省略した場合は 0 となります。
<基準階層> は省略した場合は最上位階層(テストベンチのトップ階層)となります。

VCS を使っている人は $dumpvars や $fsdbDumpvars と同じ使い方と思っていただければ大丈夫だと思います。(多分...)

Assertion control tasks には $asserton, $assertoff, $assertkill の他にも以下のようなタスクがありますが省略します。

$assertpasson

$assertpassoff

$assertfailon

$assertfailoff

$assertnonvacuouson

$assertvacuousoff

$assertcontrol

■サンプル
initial で $assertoff を使う場合を例として、図を使って説明します。グレーになっている箇所が無効化対象のモジュールになります。

  initial  $assertoff();　// 最上位階層以下の階層を全て無効化

$assertoff(0);　または　$assertoff(0, top);　としても同じ結果となります。
　　↓

  initial  $assertoff(1);  // 最上位階層から 1階層無効化

　　↓

  initial  $assertoff(2);  // 最上位階層から 2階層無効化

　　↓

  initial  $assertoff(0, top.aaa);  // top.aaa 以下の階層を全て無効化

　　↓

  initial  $assertoff(1, top.aaa);  // top.aaa から 1 階層無効化

　　↓

また、特定のアサーションのみを指定したい場合は、以下のように設定します。

  initial  $assertoff(0, top.aaa.bbb.<ラベル名>);

平凡なる好奇

2019年6月15日土曜日