ただいまコメントを受けつけておりません。
雑記 > codeのメモ > 【SystemVerilog】【SVA】throughout、intersect
SVAで throughout の使い方がよくわからなかったのでメモ。ちなみにLanguage Reference Manual(LRM)でintersect、throughoutを調べてgoogle翻訳すると以下の通り。
以下は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)|->
がないとシミュレーション開始からチェックされる
以下は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はすべてシーケンスではなく信号を想定
ただいまコメントを受けつけておりません。