目次
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 s2 | sequence1が成立してからnサイクル後にsequence2を評価 | reqを送ってからackはnサイクル以内に必ず来る。とか、n~mサイクル以内に来る |
s1 ##[n:m] s2 | sequence1が成立してから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 s2 | sequence1, 2共に成立することを検証する | — |
s1 or s2 | sequence1, 2のどちらかが成立することを検証する | — |
s1 intersect s2 | よくわからない | — |
b throuthout s | seaquenceを評価中にboolが常に真で在り続けることを評価 | — |
s1 within s2 | sequence2を評価中にのみ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 p2 | property1, 2が共に成立するとき評価 | —- |
p1 or p2 | property1, 2どちらかが成立するとき評価 | —- |
not p | propertyが成立しないときに評価 | —- |
if(b) p1 else p2 | boolがTrueならproperty1を評価、Falseならproperty2を評価 | —- |
disable iff(b) | boolがTrueの時は他のプロパティの評価を無視して常にTrueになる(つまりbがtrueならばエラー無し) | 例えばResetがTrueの時はpropertyの条件にかかわらずTrueにするなどで使える。 |
s |-> p | sequenceならば(同サイクルのproperty)が成立するときに評価 | —- |
s |=> p | sequenceならば(次サイクルの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);