SVA(SystemVerilog Assertion)での可変遅延および連続繰り返し(##N, [*N])

■ はじめに

SVAでは遅延や連続繰り返しは##3や[*3]の様に表される。これら遅延および連続値は固定である必要があり、これらの値を可変にした以下の様なプロパティはN.Gである。

可変の遅延および連続値（SVA的にN.Gな記述）

property prop_variable_delay(N);
  $rose(a) |-> ##N $rose(b)  ; // Illegal in SVA
endproperty

property prop_variable_repeat(N);
  $rose(a) |-> a[*N] $rose(b); // Illegal in SVA
endproperty

ところが、この可変の遅延および繰り返しを可能にする方法がある。
先に結論を書くと以下の様に、サイクル毎のカウント値を内部変数に保持して、その値を参照するのである。

可変イベントチェック（信号bが必ず来る事を期待）

sequence seq_delay(D); // D >= 0, D = N
   int cnt;
   (1, cnt=0) ##0 first_match((1, cnt++)[+] ##0 (cnt == D+1));
endsequence

sequence seq_repeat(R,a); // R >= 1, R = N + 1
   int cnt;
   (1, cnt=0) ##0 first_match((a, cnt++)[+] ##0 (cnt == R));
endsequence

property prop_variable_delay(N);
   $rose(a) |-> seq_delay(N)    ##0 $rose(b);
endproperty

property prop_variable_repeat(N);
   $rose(a) |-> seq_repeat(N+1,a) ##0 $rose(b);
endproperty

可変のイベント期間チェック（信号bが必ずしも立たない場合を許容）

property prop_variable_delay(N);
   int cnt;
 //($rose(a), cnt=0) ##0 first_match((1, cnt += !b)[+] ##0 $rose(b)) |-> (cnt == N);
   ($rose(a), cnt=0) ##0 ( (1, cnt += !b)[+] intersect b[->1]      ) |-> (cnt >= N) ;
endproperty

property prop_variable_repeat(N);
   int cnt;
 //($rose(a), cnt=0) ##0 first_match((a, cnt += !b)[+] ##0 $rose(b)) |-> (cnt == N);
   ($rose(a), cnt=0) ##0 ( (a, cnt += !b)[+] intersect b[->1]      ) |-> (cnt == N) ;
endproperty

以下順に説明を書いて行く。

■ シーケンスの後の命令実行

SVAでは(<sequence>, <execute line>)の様にシーケンスを括弧でくくるとそのシーケンスの後に命令文を実行できる。

シーケンスの後に命令実行

property prop_sequence_exe;
  ($rose(a), $display("Rose of a is detected!!!")) |-> ##0 (b ##1 c, $display(" b ##1 c is detected!!!"));  
endproperty

この例では$display()で$rose(a)およびb ##1 cのシーケンスが成立した時にメッセージを表示するようにした。当然自分で定義したfunction等も実行できる。メッセージ表示や値の代入等を定義した物を用意しておけばデバッグに便利である。
因みに実行する命令文は複数持つこともでき、その場合(<sequence>, <execute line 1>, <execute line 2>, ...)と,で繋げていく。

■ プロパティの内部変数

そして、SVAではpropertyの中に内部変数を持つことができる。シーケンス終了時にその変数へ値を代入する事により、とある時点での値の保持しておく事ができる。なので以下の様に、ある時点での信号の値を保持しておいて、数クロック後にその保持した値が現れる事をチェックするプロパティを書く事ができる。

内部ローカル変数を使用

property prop_local_val;
  int val;
  @(posedge clk) (en, val = in_d) |-> ##100 out_d == val;  
endproperty

この例ではenが1であると言うシーケンスの時にvalと言うローカル変数にval = in_dでin_dの値を保持すると言う命令を実行している。そしてその100サイクル後にout_dにそのvalに保持されていたin_dの値が現れる事を期待している。
同様なpropertyを$past(in_d,100)の様に$past()を使っても書けるが、長い遅延に$past()を使うのはよろしくない。

■ 内部変数のカウント

以上のシーケンス終了時の命令実行とプロパティ内部変数を使う事により可変の遅延および繰り返しができるようになる。実行命令として内部変数をとある時点「まで」カウントするようにする。そして、そのカウント値が指定した値になっている事を期待するようなシーケンス或いはプロパティを作る。以下はそのプロパティの具体例。
良く知られているが、「～まで」を表現するSVAシーケンスはこの例の様に<seq_1>[*1:$] ##1 <seq_2>或いは<seq_1>[*0:$] ##1 <seq_2>の様に表現される。

遅延および繰り返しが可変のSVAプロパティ

//------- Variable Delay --------------------
//                |<===== N =====>|
//                |_             _|
// a     : _______|1 2 3     . . N|__
//                 ^...............*
//                 0
//                 + + +     + + +
// cnt             1 2     . . . N N
property prop_variable_delay(a, N);
   int cnt;
   ($rose(a), cnt=0) |-> (1, cnt++)[*1:$] ##1 !a ##0 (cnt == N);
endproperty

//------- Variable Repetion -----------------
//                |<===== N =====>|
//                |______   ______|
// a     : _______|1 2 3     . . N|__
//                 ^...............*
//                 0
//                 + + +     + + +
// cnt             1 2     . . . N N
property prop_variable_repeat(a, N);
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt++)[*1:$] ##1 !a ##0 (cnt == N);
endproperty

これらはaが立ち上がった後、aが下がる「まで」cntをカウントアップしている。そしてその時点でのcntの値がNで指定した値になっている事を期待している。

ここで示したプロパティは繰り返し回数Nが1以上である必要がある。なので上記のプロパティはN>0が保証されている場合のみに使用できる。
信号がaの一つのみの場合はaが立ち上がればaが下がるのは必ずその次のサイクル以降なのでNは必ず1以上と言える。

N ==1（終了シーケンス重なりなし）

//    (N == 1)     __
// a     : _______|1 |__
//                 ^..*
//                 0
//                 +
// cnt   :         1  1

■ N=0の場合も含める

aとは別のbと言う信号があり、2つの信号の間の立ち上がりをチェックしたい様な場合、aが立ち上がったと同時にbが立ち上がる、つまりN=0の場合が有り得る。

２つの信号の場合（N == 0が有り得る）

//                 ______   _________
// a     : _______|^
//                 <----- N -----> __
// b     :        ________________|*
//                 ^...............*

//    (N == 1)     _____
// a     : _______|^
//                  1 __
// b     :        ___|*
//                 ^..*

//    (N == 0)     __
// a     : _______|^
//                0__
// b     :      __|*
//                 *

N=0も含めたい場合には「～まで」の条件に付けた##1を##0にしてaの繰り返しにbの立ち上がりを含める必要がある。そしてb==1となった際にcntがカウントされないようにcnt += !b、でインクリメントする必要がある。

N == 0も含む可変繰り返し１(cnt += !bでインクリメント）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |______   _____|__
// a     : _______|1 2 3    . . N __ 
// b     :         ______   _____|*
//       :         ^..............*
//                 0
//                 + + +    + + + 
// cnt   :         1 2 3  . . . N N
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt+=!b)[*1:$] ##0 $rose(b) ##0 (cnt == N);
endproperty

或いはインクリメントはc++のままで、cntの最後の値にNではなく、N+1や>Nを期待する方法もある。

N == 0も含む可変繰り返し２（cnt == N+1を期待）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |______   _____|__
// a     : _______|1 2 3    . . N __ 
// b     :         ______   _____|*
//       :         ^..............*
//                 0
//                 + + +    + + + +
// cnt   :         1 2 3  . . . N N+1
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt == N+1);
 //($rose(a), cnt=0) |-> (a, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt >  N  );
endproperty

他には初期化を-1に調整して最後bの立ち上がりの時点でcnt==Nを期待するように調整でも良い。

N == 0も含む可変繰り返し３（（cnt = -1で初期化）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |______   _____|__
// a     : _______|1 2 3    . . N __ 
// b     :         ______   _____|*
//                 ^..............*
//                -1
//                 + + +      + + +
// cnt   :         0 1 2      . . N
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose, cnt=-1) |-> (a, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt == N);
endproperty

aの可変連続ではなく、必ず成立を意味する1の可変連続にすると可変遅延となる。1の1回連続は遅延0(##0)と同じ。

N == 0も含む可変遅延１（cnt += !b）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |__            |
// a     : _______|1 2 3    . . N __ 
// b     :      _________   _____|*
//                 ^..............*
//                 0
//                 + + +      + + 
// cnt   :         1 2 3      . N N
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose(a), cnt=0) |-> (1, cnt+=!b)[*1:$] ##0 $rose(b) ##0 (cnt == N);
endproperty

N == 0も含む可変遅延２（cnt == N+1）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |__            |
// a     : _______|1 2 3    . . N __ 
// b     :      _________   _____|*
//                 ^..............*
//                 0
//                 + + +      + + +
// cnt   :         1 2 3      . N N+1
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose(a), cnt=0) |-> (1, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt == N+1);
 //($rose(a), cnt=0) |-> (1, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt >  N  );
endproperty

N == 0も含む可変遅延３（cnt = -1）

//------- Variable Repetion -----------------
//    (N >= 0)    |<===== N ====>|
//                |__            |
// a     : _______|1 2 3    . . N __ 
// b     :      _________   _____|*
//                 ^..............*
//                -1
//                 + + +      + + +
// cnt   :         0 1 2      . . N
property prop_variable_repeat_0(a, b, N);
   int cnt;
   ($rose(a), cnt=-1) |-> (1, cnt++)[*1:$] ##0 $rose(b) ##0 (cnt == N);
endproperty

可変遅延の場合はaの立ち上がり後の形状は期待しておらず任意の形でよい。なので立ち上がり後ずっとHighは期待しておらず、直ぐに立ち下がってしまってもよい。

■ 信号bが必ずしも立ち上がらない場合を考慮

これまで信号が信号aが立ち上がったら信号bも立ち上がる事を前提のプロパティを考えてきた。その事が確実に保証されていればそれで良いのだが、必ずしもbが立ち上がらない事もある場合。そのような場合にはこれらのプロパティはvacuous passとなってしまう。

● strong()を使用

そのような場合には以下のように右辺にstrongを追加して、必ずその条件が成立する事を期待し、そうならなかった場合にはfailとなるようにする事ができる。

strongを追加してvacuous passを防ぐ

property prop_variable_repeat_0(a, b, N); // N >= 0
   int cnt;
   ($rose(a), cnt=0) |-> strong( (a, cnt++)[+] ##0 $rose(b) ##0 (cnt > N) );
property

property prop_variable_delay_0(a, b, N); // N >= 0
   int cnt;
   ($rose(a), cnt=0) |-> strong( (1, cnt++)[+] ##0 $rose(b) ##0 (cnt > N) );
property

尚、ここでは[*1:$]のショートカット表現として[+]が使えるのでここではそれを使用した。因みに不定遅延および連続値のショートカット表現には以下の物がある。

不定遅延値のショートカット表現

##[*] // Equal to ##[0:$]
##[+] // Equal to ##[1:$]

不定連続値のショートカット表現

[*]  // Equal to [*0:$]
[+]  // Equal to [*1:$]

strongは以下の様に別プロパティにとして分けても良い

信号bが立ち上がる事を保証するプロパティを追加

property prop_variable_repeat_0(a, b, N); // N >= 0
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt++)[+] ##0 $rose(b) ##0 (cnt > N) ;
endproperty

property prop_rise_b(a, b);
   $rose(a) |-> strong( b[->1] );
endproperty

別プロパティとして以下の様にuntil_withのstrong版のs_until_withを使っても良い。

bが立ち上がるまでaがhighとなる事が”必ず”起きる

property prop_rise_b(a, b);
   $rose(a) |-> a s_until_with b;
endsequence

● 「～まで」の条件に内部ローカル変数の値を使用

上ではbが必ず立ち上がる事を期待してstrongを適用した。しかし、「～まで」の終了条件に信号bを使わず、内部ローカル変数のカウント値を使えば、その場所でカウントが終了し、bを期待する事ができる。この方法ならstrongを使わずとも、vacuous passを防ぐ事ができる。

信号bに依存しないカウント終了条件

property prop_variable_delay(a,,b,N);
   int cnt;
   ($rose(a), cnt= 0) |-> (1, cnt++)[+] ##0 (cnt >  N  ) ##0 $rose(b);
 //($rose(a), cnt= 0) |-> (1, cnt++)[+] ##0 (cnt == N+1) ##0 $rose(b);
 //($rose(a), cnt=-1) |-> (1, cnt++)[+] ##0 (cnt == N  ) ##0 $rose(b);
endproperty

property prop_variable_repeat(N);
   int cnt;
   ($rose(a), cnt= 0) |-> (a, cnt++)[+] ##0 (cnt >  N  ) ##0 $rose(b);
 //($rose(a), cnt= 0) |-> (a, cnt++)[+] ##0 (cnt == N+1) ##0 $rose(b);
 //($rose(a), cnt=-1) |-> (a, cnt++)[+] ##0 (cnt == N  ) ##0 $rose(b);
endproperty

カウント値にN+1を期待するでも> Nを期待するでも、初期値を-1にしてNを期待するでもどれでもO.Kだが、信号bを条件として使えないので、ここでは+=!bでのインクリメントの作戦は使えない。

これらのプロパティでは期待される位置でbが立たなかった場合、その時点で必ずFAILとなる。

● 可変遅延・連続繰り返しのsequence化

これまで見てきた内部変数のカウントを使った可変の遅延・連続繰り返しの部分をsequenceとして定義する事ができる。そうするといろいろなプロパティで利用できる。さらにpackageに置けば汎用的に使えるライブラリとする事ができる。
これまで|->の右辺に可変の遅延・繰り返しを使用してきたが、sequence化するにあたり、左辺に使われる事も考慮してfirst_match()を追加した方が良い。不定の遅延や繰り返しは右辺では暗黙的にfirst_match()が適用されるが、左辺では明示的に入れないと最初のマッチ条件だけでなく延々とその後のマッチ条件を探してしまう。

可変遅延・連続繰り返しのsequence化

package my_sva_pkg;

  sequence seq_delay(D); // D >= 0
    int cnt;
  //(1, cnt= 0) ##0 first_match( (1, cnt++)[+] ##0 (cnt == D+1) );
    (1, cnt= 0) ##0 first_match( (1, cnt++)[+] ##0 (cnt >  D  ) );
  //(1, cnt=-1) ##0 first_match( (1, cnt++)[+] ##0 (cnt == D  ) );
  endsequence

  sequence seq_repeat(R,a); // R >= 1
    int cnt;
    (1, cnt= 0) ##0 first_match( (a, cnt++)[+] ##0 (cnt == R) );
  endsequence

endpackage

信号間の距離LENは遅延サイクル値と等しいが(##LEN)、信号の連続繰り返しのサイクル数の値だと+1する必要がある(s1[*(R+1)])ので注意。１回繰り返しはサイクルステップは進まず、そのサイクルに留まるので。２回繰り返しで１サイクル遅延する。

距離LENとDelay(D)およびRepeat(R)の関係

//                 _________________
// a     : _______|<==== LEN ===> __ 
// b     :      ___._____________|.
//                 0              LEN
// Dealy(D)        |------------->|
//                 1              LEN + 1
// Repeat(R)       |------------->|

汎用可変遅延・繰り返しsequenceの使用例

// D = LEN
property prop_variable_delay(a,,b,LEN);
   $rose(a) |-> seq_delay(LEN)    ##0 $rose(b);
endproperty

// R = LEN + 1
property prop_variable_repeat(LEN);
   $rose(a) |-> seq_repeat(LEN+1,a) ##0 $rose(b);
endproperty

【参考】Solving Complex Users' Assertions

■ 信号bが必ずしも立ち上がらない場合を許容

これまで信号aが立ち上がったら必ず信号bも立ち上がる事を期待としてきた。しかし、以下の様に信号bが必ずしも立ち上がらない事が許容される場合も考えてみる。

bが立ち上がらない事を許容

//                 __________          ___________
// a     : _______|^         |________|^      ____
// b     : __________________________________|*
//                 ^#########          ^......*

この場合信号bは動作を期待する右辺では使えない。

● 左辺で可変遅延・連続繰り返しを使用

動作を期待する右辺では使えないので、発動条件を指定する左辺側で使う。「aがbまで繰り返したら」と言う不定長の条件が左辺に入るのでfirst_match()が必要になる。そして、その時aがHighのサイクル数をカウントし、そのカウント値を右辺で期待する。
以下で「aとb両方立ち上がった場合にその距離が指定した値になっている」と言うプロパティになる。

左辺でbを使う

property prop_variable_repeat_0(a, b, N); // N >= 0
   int cnt;
   (!b ##1 $rose(a), cnt=0) ##0 first_match((a, cnt += !b)[+] ##0 b) |-> (cnt == N  );
 //(!b ##1 $rose(a), cnt=0) ##0 first_match((a, cnt++    )[+] ##0 b) |-> (cnt == N+1);
 //(!b ##1 $rose(a), cnt=0) ##0 first_match((a, cnt++    )[+] ##0 b) |-> (cnt >  N  );
 //(!b ##1 $rose(a), cnt=0) ##0 first_match((a, cnt++    )[+] ##0 b) |-> (cnt == N  );
endproperty

ここでも+=!bでインクリメントしたり、N>0を期待したり、N+1を期待したり、-1で初期化したりといろいろとバリエーションはあり得る。

● first_matchの代わりにintersectの使用

「～まで」を表すのに無限長表現を含んだ<seq_1> [*1:$] ##0 <seq_2>と最初のマッチに限定するfirst_match()を用いたが、このfirst_match()の使用はあまりよろしくないと言う話もあり、代替手段として<seq_1> intersect <seq_2>[->1]の使用が推奨されている。

Assertion to check variable distance of two signals

intersectを使用した場合は以下の様になる。

first_matchを使用せずintersectを利用

property prop_variable_repeat_0(a, b, N); // N >= 0
   int cnt;
   ($rose(a), cnt= 0) ##0 ((a, cnt += !b)[+] intersect b[->1]) |-> (cnt == N  );
 //($rose(a), cnt= 0) ##0 ((a, cnt++    )[+] intersect b[->1]) |-> (cnt == N+1);
 //($rose(a), cnt= 0) ##0 ((a, cnt++    )[+] intersect b[->1]) |-> (cnt >  N  );
 //($rose(a), cnt=-1) ##0 ((a, cnt++    )[+] intersect b[->1]) |-> (cnt == N  );
endproperty

[->1]は１回の不連続繰り返し、intersectは２つのシーケンスの同時開始、同時終了を表す。なのでこれらを使うと「～まで」を表現できる。

最近のSVAの仕様では「～まで」の表現にuntilやuntil_withを使用できるようになった。なので以下のようなプロパティが考えられる。

until, until_withを使用は使用できない

property prop_variable_repeat_until(a, N);
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt++) until !a |-> (cnt == N);
endsequence

property prop_variable_repeat_0_until_with(a, b, N);
   int cnt;
   ($rose(a), cnt=0) |-> (a, cnt++) until_with b |-> (cnt > N);
endproperty

しかし、試してみたがうまく行かなかった。until/until_withの両辺はpropertyとみなされ、評価される毎に内部ローカル変数がコピーされるため、結果カウントがされない様だ。

EDA Playground Link : SVA Dynamic Variable until/until_with usage

Verification Academy Forum : Variable Delay or Repetition with “until/until_with”

■ EDA Playgroundでの例

• SVA Variable Delay and Continuation
• A Dynamic Variable Signal Distance Check

■ 参考記事

• SystemVerilog アサーション入門（後編）
• 平凡なる好奇 [SVA] 2. シーケンス (sequence)
• Verification Guid Variable delay in SVA
• Solving Complex Users' Assertions
• SVA: Package for dynamic and range delays and repeats
• Verification Academy/Forum/SystemVerilog/ Assertion with variable declaration in SVA
• Assertion with variable declaration in SVA
• Assertion to check variable distance of two signals