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

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

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

• 定義できるところ
  • モジュール内
  • インターフェース内(System Verilog)
  • 外部宣言領域??? ← よくわからない

sequence SEQ(a, b);		//propertyから与えられる引数順に記載
	(
		a ^ b			//xor(a, b)
	);
endsequence

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

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

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

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

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

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

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を満足する場合はエラー

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を満足する場合はエラー

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