[SVA] 6. サンプル

SVA (SystemVerilog Assertion) 並列アサーションの簡単なサンプル集。必要に応じて negedge にしたり disable iff を入れたりしてください。

  @(negedge clk)  ...;

  @(posedge clk) disable iff (rst)  ...;

[SVA] 5. その他

SVA (SystemVerilog Assertion) の基本的な記述方法について、前回までの内容を見ていただければなんとなく理解していただけるのではないかと思います。高位合成が流行るにつれてSVAを使う機会がどうなっていくのか私には想像できませんが、あと数年は使うことになるのではないでしょうか。

今回の記事は SVA に関連あるけど、知らなくてもおそらく問題ない内容となっています。

[SVA] 4. system function と control task

SVA で使えるシステムファンクションとコントロールタスクの基本的な記述方法についてまとめます。省略している箇所も多々ありますので、詳細については IEEE Std 1800-2017 を参照ください。

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

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

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

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

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

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

[SVA] 2. シーケンス (sequence)

SVAの並列アサーションで使用する シーケンス(sequence) の構文について、簡単にですがまとめます。sequence で使用する構文は property でも使えますので、property のみでアサーションを記述することもできます。

　sequence <シーケンス名> (<引数1>, <引数2>, ...);
    ....;
  endsequence

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

　S : サブシーケンス もしくは ブーリアン
  B : ブーリアン (条件式)

[SVA] 1. SystemVerilog アサーション

SVA (SystemVerilog Assertion) は論理回路の検証手法の一つです。
SVA を使う主な目的としては「目視による確認漏れを減らす」や「バグの早期発見」だと思いますが、その辺りの話は放り投げて、記述方法についてを数回に分けてまとめたいと思います。

私は基本的なことしか書けないので、詳細について知りたい方は IEEE Std 1800-2017 を参照してください。(私はあまり読みたくないです。1300ページ超えてますし...)

今回は SVA の構文について。SVA には 即時アサーション (Immediate assertion) と 並列アサーション (Concurrent assertion) があります。