忍者ブログ

雑記

【SystemVerilog】【SVA】throughout、intersect

雑記 > codeのメモ > 【SystemVerilog】【SVA】throughout、intersect

SVAのthroughoutとintersect

SVAで throughout の使い方がよくわからなかったのでメモ。ちなみにLanguage Reference Manual(LRM)でintersect、throughoutを調べてgoogle翻訳すると以下の通り。

  • intersect
    • バイナリ演算子intersectは、両方のオペランド・シーケンスが一致すると予想され、オペランド・シーケンスの終了時刻が同じでなければならない場合に使用されます。
  • throughout
    • シーケンスは、正しい動作の為にいくつかの条件の前提の下ではしばしば発生します。例えば、トランザクションの処理中に真でなければならない場合、またはトランザクションの処理中に特定の値の発生が禁止されている場合。

throughout

以下はCASE1,CASE2の間、SIGNALが変化しないことをチェックするproperty

property vp_sample_throughout(SIGNAL,CASE1,CASE2);
  @(posedge clk) disable iff(~rst_n)
  $rose(CASE1) |-> ( $stable(SIGNAL) throughout $rose(CASE2)[->1] );
endproperty

throughoutの部分はCASE2が1回発生するまでの間$stable(SIGNAL)であることをチェックするという内容だが、

$rose(CASE1)|->

がないとシミュレーション開始からチェックされる

intersect

以下はCASE1,CASE2の間、SIGNALが1回立ち上がることをチェックするproperty

property vp_sample_intersect(SIGNAL,CASE1,CASE2);
  @(posedge clk) disable iff(~rst_n)
  $rose(CASE1) |-> ( $rose(SIGNAL)[=1] intersect $rose(CASE2)[->1] );
endproperty

intersectはシーケンスとシーケンスを比較するものだが、$rose(CASE2)[->1]がチェックの終了になる。$rose(CASE2)[->1]部分を$fell(CASE1)[->1]とすると、CASE1の立ち上がりから立下りまでの間にSIGNALが1回立ち上がることというチェックになる

CASE1,CASE2,SIGNALはすべてシーケンスではなく信号を想定

関連記事

コメント

カレンダー

06 2018/07 08
S M T W T F S
2 3 4 5 6
8 9 10 11 12 13 14
16 17 18 19 20 21
22 23 24 25 26 27 28
29 30 31