SVAの入門的な何か

SVA(SystemVerilog Assertion)に関する資料とかサイトがあんまりないので、とりあえずまとめてみます。メモも含まれるので、間違っていたらtwitterとかで指摘してください。

未検証のものも含まれるから注意。

SVAの構造

Sequence記述

検証を行う時に、検証対象となる条件を指定するところ。特定のサイクル、または複数にまたがるサイクルの条件を指定する。sequence ~ endsequence内に記載。下記に記載する通り、シーケンス演算子がpropertyの中で使えるため、簡単なものであればsequenceを記述せずpropertyだけで済む。

  • 定義できるところ
    • モジュール内
    • インターフェース内(System Verilog)
    • 外部宣言領域??? ← よくわからない
sequence SEQ(a, b);		//propertyから与えられる引数順に記載
	(
		a ^ b			//xor(a, b)
	);
endsequence

あと、シーケンス内ではシーケンス演算子が使える。

シーケンス演算子

演算子説明使い方
s1 ##n s2sequence1が成立してからnサイクル後にsequence2を評価reqを送ってからackはnサイクル以内に必ず来る。とか、n~mサイクル以内に来る
s1 ##[n:m] s2sequence1が成立してからn~mサイクル後にsequence2を評価
s [*n]sequenceが一旦成立するとnサイクル連続して繰り返されるirqはnサイクル連続してEnableの必要がある、とか、n~mサイクル以内連続する
s [*n:m]sequenceが一旦成立するとn~mサイクル連続して繰り返される
b[->n:m]
b[=n:m]
s1 and s2sequence1, 2共に成立することを検証する
s1 or s2sequence1, 2のどちらかが成立することを検証する
s1 intersect s2よくわからない
b throuthout sseaquenceを評価中にboolが常に真で在り続けることを評価
s1 within s2sequence2を評価中にのみsequence1の評価を行い、結果としてsequence1の評価を返す
first_match(s)Riviera-PRO 2013.02.81.4877ではまだサポートしてないみたい。
s.ended
s.matched

Property記述

評価をする条件をプロパティ演算子を使って指定する。propertiesの結果がfalseになった場合はassertion違反となる。

コンカレント・即値

コンカレントアサーションか即値アサーションかを記述し、シーケンスを指定することで、ある条件の状態時に真偽を評価する。

  • コンカレントアサーション
    • ある信号のエッジで評価をする。普通はこっちをよく使う。@(posedge iCLOCK) 等。多分@(negedge iCLOCK)もいけるんだよね?
  • 即値アサーション
    • ある信号のレベル変化で即座に評価。即値アサーションは、アサーション自体の記述ミスが起きやすいので条件の評価を十分にすること。

プロパティ演算子

プロパティ演算子によって、評価をする条件を指定する。

プロパティ演算子条件使われ方
p1 and p2property1, 2が共に成立するとき評価—-
p1 or p2property1, 2どちらかが成立するとき評価—-
not ppropertyが成立しないときに評価—-
if(b) p1 else p2boolがTrueならproperty1を評価、Falseならproperty2を評価—-
disable iff(b)boolがTrueの時は他のプロパティの評価を無視して常にTrueになる(つまりbがtrueならばエラー無し)例えばResetがTrueの時はpropertyの条件にかかわらずTrueにするなどで使える。
s |-> psequenceならば(同サイクルのproperty)が成立するときに評価—-
s |=> psequenceならば(次サイクルのproperty)が成立するときに評価—-

Assertion記述

ディレクティブ

プロパティの利用方法を指定する。

ディレクティブ条件判定利用方法
assertプロペティを偽と判断するとエラーと判断するproperty通りに動作しているかのチェックに使用(propertyを満たさない場合はエラー)
assumeプロペティを偽と判断するとエラーと判断する期待される入力を与えておき、シミュレーション時にその値と一致しない場合はエラー
cover

assertion用演算子

演算子用途使い方
$sample()
$past()1Cycleまたは複数サイクル前に評価した値を取得$past(data, 1); //1サイクル前のdataを取得
$onehot()式がonehotである時1を返す
$onehot0()式がonehotまたは0である時、1を返す
($onehot(式) || 式 == 0) と等価
$isunknown()式がのいずれかのビットがXまたはZである時1を返す
$countones()式がのベクタにおいて、1の数をカウントして返す。X, Zは含まれない

よく使われるアサーション

Reqを送ってn_cycle以上m_cycle以内には必ずAckが来ることを検証するアサーション

property PRO_BUS_REQ_ACK;
	@(posedge iCLOCK) disable iff (!inRESET) (oDATAIO_REQ |-> ##[1:50] iDATAIO_ACK);	//inRESETがLowでなおかつ、oDATAIO_REQを送って1~50 iCLK Cycle以内にiDATAIO_ACKが来ない場合に評価
endproperty
 
assert property(PRO_BUS_REQ_ACK);								//PRO_BUS_REQ_ACKのpropertyを満足する場合はエラー

一度EmptyではなくなったFIFOが再びEmptyにならないことを検証するアサーション

property PRO_FIFO_NEVER_EMPTY;
	@(posedge iCLOCK) disable iff (!inRESET) (!oFIFO_EMPTY |=> !oFIFO_EMPTY);	//inRESETがLowでなおかつ、!oFIFO_EMPTYの時は次のサイクルでも!oFIFO_EMPTY となると評価
endproperty
 
assert property(PRO_FIFO_NEVER_EMPTY);								//PRO_BUS_REQ_ACKのpropertyを満足する場合はエラー

常にn~mの間でしか値を持たないカウンタをかどうかを検証するアサーション

 
property PRO_COUNTER_CHECK;
	@(posedge iCLOCK) (b_counter >= 0 && b_counter <= 9);		//0~9の間でしか値を持たない
endproperty
 
assert property(PRO_COUNTER_CHECK);