verilog : SVA の演算子

目的:

SVAの演算子等について記す。

各演算子:

(SVA の記述については、こちらを参照。
 下記 動作は、全てを確認した訳では無い為、使用時は注意して下さい。 )

主なシーケンス演算子:

  ( s, s1, s2 : シーケンス 、b : ブーリアン 、 x, y 等 : 信号名 )

演算子	説明
s1 ##n s2	s1 が成立してから nサイクル後に s2 が成立する時
s1 ##[n:m] s2	s1 が成立してから n～mサイクル後に s2 が成立する時
s [*n]	s がnサイクル連続して繰り返された時
s [*n:m]	s がn～mサイクル連続して繰り返された時
b[->n]	b がnサイクル連続 又は 非連続 で繰り返された時
	* ブーリアンのみ
s1 intersect s2	s1, s2 の開始と終了が同じである時
b throughout s	s の継続中、 b が 真の時
s1 within s2	s2 の継続中 に s1 が 真になった場合の s2 終了時

主なプロパティ演算子:

演算子	説明
p1 and p2	p1, 2が共に成立するとき評価
p1 or p2	p1, 2どちらかが成立するとき評価
not p	pが成立しないときに評価
if(b) p1 else p2	bが真ならp1を評価、偽ならp2を評価
disable iff(b)	bが真の時は評価しない(Fail しない)
s |-> p	s が成立した サイクルで p を評価
s |=> p	s が成立した 次のサイクルで p を評価 ( s |-> ##1 p と同じ )

主な関数:

$rose( 信号 )	信号の最下位ビットが '1' に変化した時に 真
$fell( 信号 )	信号の最下位ビットが '0' に変化した時に 真
$stable( 信号 )	信号が 1サイクル前から変化しなければ 真
$past( 信号 , n )	信号のnサイクル前の値,  nが省略された場合は n=1
$onehot( 信号 )	信号の'H' のビット数が 1 の時に 真
$onehot0( 信号 )	信号の'H' のビット数が 1 又は 0 の時に 真
$isunknown(信号)	信号に 'x' や 'z' が含まれる場合に 真
$countones(信号)	信号の'H' のビット数