[SVA] 3. プロパティ (property)

SVAの並列アサーションで使用する プロパティ(property) の構文について、よく使うものを挙げています。

　property <プロパティ名> ( (<引数1>, <引数2>, ...);
    @(posedge clock)  disable iff ( <条件> ) ...;
  endproperty

( (<引数1>, <引数2>, ...) と disable iff ( <条件> ) は省略できます。
また、<引数> は型やbit数を指定する必要はありません。

[ 注釈 ]
本記事中の P, S, B の意味は以下になります。

　P : サブプロパティ もしくは シーケンス, ブーリアン
  S : シーケンス もしくは ブーリアン
  B : ブーリアン (条件式)

除外

disable iff ( <条件> ) を使用して、条件を満たす間のアサーション監視を除外することができます。条件にはリセットがよく使われると思います。

  /* リセット中は監視しない */
  property p1;
    @(posedge clock) disable iff (reset)  ...;
  endproperty

Implication

|->, |=> を使用して、左辺の条件を満たした場合に右辺の振る舞いをチェックすることができます。

S1 |-> P2	S1 成立と同じサイクルで P2 をチェック
S1 |=> P2	S1 成立の次のサイクルで P2 をチェック

  /* a == 1 検出と同じタイミングで b == 1 を検出 */
  property p1;
    @(posedge clock)  a |-> b;
  endproperty

  /* a == 1 検出の次のタイミングで b == 1 を検出 */
  property p2;
    @(posedge clock)  a |=> b;
  endproperty


  SVA_P1 : assert property(p1);
  SVA_P2 : assert property(p2);

|=> は |-> ##1 と表現することもできます。
2サイクル後や 3サイクル後を表現したい場合は、|-> ##n とした方が分かりやすいと思います。

分岐 (if-else)

if-else を使用して、監視するプロパティを分岐させることができます。

if (B) P1	B が成立している場合のみ P1 を監視
if (B) P1 else P2	B が成立している場合は P1 を監視 B が成立していない場合は P2 を監視

  /* リセット中は監視しない */
  property p1;
    @(posedge clock) if (!reset)  ...;
  endproperty

その他

他にも下記のような構文があるようです。しかし、上に挙げたプロパティの構文と、シーケンス、システムファンクション を使用すればほとんどのアサーション記述は可能ではないかと思います。

not P

P1 or P2

P1 and P2

case

S #-# P

S #=# P

nexttime P

s_nexttime P

always P

s_always P

eventually P

s_eventually P

P1 until P2

P1 s_until P2

P1 until_with P2

P1 s_until_with P2

P1 implies P2

accept_on P

reject_on P

sync_accept_on P

sync_reject_on P