■ はじめに
SVAでは##3や[*3]の様にシーケンスの遅延や連続繰り返しが表される。しかし、この遅延および連続値は固定である必要があり、これらを可変にした以下の様なプロパティは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
ところが、この可変の遅延および繰り返しを可能にする方法がある。
先に結論を書くと以下の様に、サイクル毎のカウント値を内部変数に保持して、その値を参照するのである。
sequence seq_delay(N);
int cnt = 0;
(1, cnt=0) ##0 first_match((1, cnt++)[+] ##1 (cnt == N));
endsequence
sequence seq_repeat(N,a);
int cnt = 0;
(1, cnt=0) ##0 first_match((a, cnt++)[+] ##0 (cnt == N));
endsequence
property prop_variable_delay(N);
$rose(a) |-> seq_delay(N) ##0 $rose(b);
endsequence
property prop_variable_repeat(N);
$rose(a) |-> seq_repeat(N,a) ##1 $rose(b);
endproperty
property prop_variable_delay(N);
int cnt = 0;
($rose(a), cnt=0) ##0 first_match((1, cnt += !b)[+] ##0 $rose(b)) |-> (cnt == N);
endsequence
property prop_variable_repeat(N);
int cnt = 0;
($rose(a), cnt=0) ##0 first_match((a, cnt += !b)[+] ##0 $rose(b)) |-> (cnt == N);
endproperty
又はfirst_matchを使わずにintersectを使用すると以下のようになる。
property prop_variable_delay(N);
int cnt = 0;
(!b ##1 $rose(a), cnt=0) ##0 ((1, cnt += !b)[+] intersect b[->1]) |-> (cnt == N) ;
endsequence
property prop_variable_repeat(N);
int cnt = 0;
(!b ##1 $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>の様に表現される。
//------- Variable Delay --------------------
// |<===== N =====>|
// |_ _|
// a : _______|1 2 3 . . N|__
// cnt 0
// + + + + + +
// 1 2 3 . . N N
// ^...............*
property prop_variable_delay(a, N);
int cnt = 0;
($rose(a), cnt=0) |-> first_match( (1, cnt++)[*1:$] ##1 !a ) ##0 (cnt == N);
endproperty
//------- Variable Repetion -----------------
// |<===== N =====>|
// |______ ______|
// a : _______|1 2 3 . . N|__
// cnt 0
// + + + + + +
// 1 2 3 . . N N
// ^...............*
property prop_variable_repeat(a, N);
int cnt = 0;
($rose(a), cnt=0) |-> first_match( (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) __
// a : _______|1 |__
// cnt : 0
// +
// 1 1
// ^..*
しかし、aとは別のbと言う信号があり、2つの信号の間の立ち上がりをチェックしたい様な場合には、aが立ち上がったと同時にbが立ち上がるN=0の場合も考えられる。
■ N=0の場合も含める
N=0も含めたい場合には「～まで」の条件に付けた##1を##0にしてaの繰り返しにbの立ち上がりを含める必要がある。但しその場合、内部変数のカウント条件からbの立ち上がりサイクルを除く必要があるので、cnt++の代わりにcnt =+ !bにする。
//------- Variable Repetion -----------------
// (N >= 0) |<===== N ====>|
// |______ _____|__
// a : _______|1 2 3 . . N __
// b : ______ _____|
// cnt : 0
// + + + + + +
// 1 2 3 . . N N
// ^..............*
property prop_variable_repeat_0(a, b, N);
int cnt = 0;
($rose(a), cnt=0) |-> first_match( (a, cnt += !b)[*1:$] ##0 $rose(b) ) ##0 (cnt == N);
endproperty
// (N == 0) __
// a : _______|__
// b : __|
// cnt 0
// *
■ 信号bが立ち上がらない場合も考慮
これまで信号が信号aが立ち上がったら信号bも立ち上がる事を前提のプロパティを考えてきた。それが保証されていれば良いが、そうではなく、bが立ち上がらない場合にはこれらのプロパティはvacuous passとなってしまう。なので以下のように右辺にstrongを追加してそのような場合にfailとなるようにすると良い。
sequence prop_variable_repeat_0(a, b, N); // N >= 0
int cnt = 0;
(!b ##1 $rose(a), cnt=0) |-> strong( first_match( (a, cnt += !b)[+] ##0 $rose(b) ) ##0 (cnt == N) );
endsequence
尚、ここでは[*1:$]のショートカット表現として[+]が使えるのでここではそれを使用した。
strongは以下の様に別プロパティにとして分けても良い
property prop_variable_repeat_0(a, b, N); // N >= 0
int cnt = 0;
(!b ##1 $rose(a), cnt=0) |-> first_match( (a, cnt += !b)[+] ##0 $rose(b) ) ##0 (cnt == N) ;
endproperty
property prop_rise_b(a, b);
!b ##1 $rose(a) |-> strong( b[->1] );
endproperty
別プロパティとして以下の様にuntil_withのstrong版のs_until_withを使っても良い。
property prop_rise_b(a, b);
!b ##1 $rose(a) |-> a s_until_with b;
endsequence
■ strongを使わず「～まで」の条件に内部ローカル変数の値を使用
上ではbが必ず立ち上がる事を期待してstrongを適用した。しかし、「～まで」の終了条件に信号bを使わず、内部ローカル変数のカウント値を使えば、その場所でカウントが終了し、bを期待する事ができる。この方法ならstrongを使わずとも、vacuous passを防ぐ事ができる。
property prop_variable_delay(a,,b,N);
int cnt = 0;
($rose(a), cnt=0) |-> first_match( (1, cnt++)[+] ##1 (cnt == N) ) ##0 $rose(b);
endproperty
property prop_variable_repeat(N);
int cnt = 0;
($rose(a), cnt=0) |-> first_match( (a, cnt++)[+] ##0 (cnt == N) ) ##1 $rose(b);
endproperty
これによりbが期待される位置で立たなかった場合に必ずFAILとなる。
■ 汎用可変遅延・繰り返しsequenceのライブラリ化
可変の遅延・繰り返しの終了を信号bに非依存にできたので、それらをsequenceとしてpackageに置けば汎用的に使えるライブラリとする事ができる。
package my_sva_pkg;
sequence seq_delay(N);
int cnt = 0;
(1, cnt=0) ##0 first_match( (1, cnt++)[+] ##1 (cnt == N) );
endsequence
sequence seq_repeat(N,a);
int cnt = 0;
(1, cnt=0) ##0 first_match( (a, cnt++)[+] ##0 (cnt == N) );
endsequence
endpackage
property prop_variable_delay(a,,b,N);
$rose(a) |-> seq_delay(N) ##0 $rose(b);
endproperty
property prop_variable_repeat(N);
$rose(a) |-> seq_repeat(N,a) ##1 $rose(b);
endproperty
【参考】Solving Complex Users' Assertions
■ bが立ち上がらない事もある場合
これまでaが立ち上がったらbも必ず立ち上がる事を期待としてきた。しかし、以下の様にbが立ち上がらない事もある場合を考えてみる。
// __________ ___________
// a : _______| |________| ____
// b : __________________________________|
この場合bを右辺では使えないなので左辺の条件で使い、その時、aからの距離をカウントする。
property prop_variable_repeat_0(a, b, N); // N >= 0
int cnt = 0;
(!b ##1 $rose(a), cnt=0) ##0 first_match((a, cnt += !b)[+] ##0 b) |-> (cnt == N);
endproperty
■ 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を使用した場合は以下の様になる。
property prop_variable_repeat_0(a, b, N); // N >= 0
int cnt = 0;
(!b ##1 $rose(a), cnt=0) ##0 ((a, cnt += !b)[+] intersect b[->1]) |-> (cnt == N);
endproperty
最近のSVAの仕様では「～まで」の表現にuntilやuntil_withを使用できるようになった。なので以下のようなプロパティが考えられる。
property prop_variable_repeat_until(a, N);
int cnt = 0;
($rose(a), cnt=N) |-> (a, cnt++) until !a |-> (cnt == N);
endsequence
sequence prop_variable_repeat_0_until_with(a, b, N);
int cnt = 0;
(!b ##1 $rose(a), cnt=1) |-> (a, cnt += !b) until_with b |-> (cnt == N);
endsequence
しかし、試してみたがうまく行かなかった。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での例
■ 参考記事
- 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