忍者ブログ

雑記

【SystemVerilog】【SVA】throughout、intersect

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

SVAで 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)|->

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



以下は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はすべてシーケンスではなく信号を想定

関連記事

SVA: The Power of Assertions in SystemVerilog

コメント

カレンダー

11 2017/12 01
S M T W T F S
1
3 4 5 6 7 8 9
10 11 12 13 14 15 16
17 18 19 20 21 22 23
24 25 26 27 28 29 30
31