要約
SystemVerilog標準言語は、一貫性を保ちながらVerilog HDLを拡張してモデリング機能と検証言語機能を盛り込んでいこうという設計業界全体の取り組みにより誕生しました。従来のVerilog HDLを拡張し、検証言語機能を持たせることにより、SystemVerilogの重要な目的は達成されました。つまりSystemVerilogは、強化された設計機能、検証機能、およびアサーション機能を併せ持つ統一言語となりました。これにより、設計者の生産性が向上し、設計エンジニアと検証エンジニアは高性能な検証を実行して、さらに複雑な設計が実現できるようになりました。
SystemVerilogの第一の特長は、SystemVerilogアサーション（SVA）です。SVAはシミュレーションとフォーマル検証のセマンティクスを統合し、検証手法に合わせて回路を制御します。ここではSVAについて概説し、SystemVerilog言語が提供するデザイン構文/テストベンチ構文とアサーションの統合という他に類を見ない長所について、アサーション専用言語を使用するその他の方式と比較しながら詳しく説明します。
はじめに
SystemVerilogは2002年5月に標準化委員会であるAccelleraの認定により標準規格となりました。その時点のバージョンはSystemVerilog 3.0であり、主に大規模デザインを簡潔に記述できるよう、Verilog HDLのデザインモデリング機能を強化することに重点を置いていました。SystemVerilog 3.0の認定に併せて、SystemVerilogを最も必要性の高い検証にも対応させるため、複数の企業から定評のある技術が提供されました。
SystemVerilog 3.1の標準化に際しては、提供されたこれらの技術を取り込んでシンタックスとセマンティクスをSystemVerilog（およびVerilog HDL）の残りの部分と統合することに重点が置かれました。この統合により、共通の環境で設計エンジニアと検証エンジニアの両方が協力して作業を行い、実際のチップを可能な限り短期間で市場に投入できるようになります。SystemVerilog委員会では、2003年5月にAccelleraにより認定されたSystemVerilog 3.1を提供することでこの目的を果たしました。
SystemVerilogアサーションの利点
SystemVerilogのように、アサーションを設計/検証言語に直接的に組み込むことには大きな利点があります。そのためSystemVerilogでは、シミュレーションとフォーマル検証の両方で使用できるよう、アサーションと設計/検証言語が効果的に統合されています。SVAの主な利点をまとめると次のとおりです。
| ■ |
使い慣れた言語とシンタックスをベースにしているので採用しやすい |
| ■ |
回路制御論理コンテキストに応じたアサーション記述個所の自動認識により記述量が少なくて済む |
| ■ |
特別なインターフェイスを用いることなく、アサーションとテストベンチ間のシンプルな接続および相互動作を実現 |
| ■ |
メッセージおよびエラーの重大度のカスタマイズと制御が可能 |
| ■ |
Verilog HDLとC関数の混在シミュレーションに対応 |
| ■ |
明確に定義されたセマンティクスによりシミュレーションの結果とフォーマル検証の結果のミスマッチを回避 |
| ■ |
アサーションとのコ・シミュレーションによるオーバーヘッドの排除とシミュレーション最適化アルゴリズムの活用による検証性能の向上 |
これらの利点について、以下の各項で説明します。
SystemVerilogアサーションの概要
SystemVerilogアサーションは、ユーザーが既に慣れ親しんでいる考え方に基づいて、デザインの複雑な動作を明確かつ簡潔に記述する方法を設計エンジニアと検証エンジニアに提供するために開発されました。SVAとSystemVerilogのシンタックスが統合されたことで、デザインコードやその他の検証コードにアサーションを直接埋め込めるようになり、ツールが周囲のコードのコンテキストから多くの情報を推定できるようになりました。これにより、アサーション専用言語を使用した場合のように情報を重複させる必要がないので、動作を定義するためにユーザーが記述するコードの量が多くのケースで実質的に削減され、使用モデルがシンプルになります。
SVAのセマンティクスは、シミュレーション（イベントベース）とフォーマル検証（サイクルベース）間でアサーションの評価が等しいことが保証されるように定義されています。等価性を保証することにより、SVAで定義された動作はすべてのツールによって同様に解釈されます。また、アサーションとデザイン/検証コードの統合により相互動作が能率的になり、アサーションの能力が増大します。特に、SystemVerilogでは、アサーションからテストベンチに情報を伝達することができ、アプリケーション・プログラミング・インターフェイス（API）を必要とせずにアサーションのステータスに対してテストベンチの動作を呼応させることができます。
SystemVerilogには、immediateとconcurrentという2種類のアサーションがあります。どちらのタイプのアサーションも設計エンジニアの意図を表し、可能な限り迅速かつ直接的に問題の原因を特定することを目的としています。immediateアサーションは、alwaysブロックまたはinitialブロック内のどこででも使用できる手続き文で、テストされる条件式と、式の評価結果に従って実行される一連の文を含みます。immediateアサーションのシンタックスは次のとおりです。
immediate_assert_statement ::=
assert ( expression ) [[ pass_stmt ] else fail_stmt ]＊1
＊1この例のように、シンタックスの例では、太字はキーワードや必須の記号、［ ］はオプション項目、｛ ｝は0回以上指定できる項目を示します。
式は、if文の場合と全く同様に、文が実行されると直ちに評価されます。pass_stmtは式の条件がtrueの場合に実行され、それ以外の場合はfail_stmtが実行されます。pass文とfail文が存在する場合は、これらの文は条件式が評価された直後に実行されます。
アサーションは式が true になるということを暗黙的に示すので、アサーション違反にはそれに応じた重大度が設定されます。SystemVerilog には4つのシステム・タスク（$fatal、$error、$warning、$info）があり、fail 文のブロックにそれらを含めることで、違反の重大度を示したり、ユーザーが定義したデバッグ・メッセージを必要に応じて出力したりできます。これは VHDL の assert 文とほぼ同じ機能です。
concurrentアサーション
シミュレーションとフォーマル検証におけるSVAの本当のメリットは、VHDLのアサーションでは行えない、時間軸に応じた動作を指定できる点にあります。concurrentアサーションでは、このようなシーケンシャル動作を簡潔に指定し、その動作を不連続な刻み（通常は"posedge clk"などのクロック刻み）において評価することができます。concurrentアサーションの概念と構成要素は、それぞれが下方のレイヤ上に構築された一連のレイヤであると考えることができます。
|
|
|
図1 SystemVerilogアサーションのレイヤ
|
|
アサーションの基本機能は、所定の回路またはコンポーネントでtrueであると期待される一連の動作を定義することです。ブーリアン表現は最も基本的なレイヤで、特定の時点における信号の値を定義します。シーケンシャル表現はブーリアン表現のレイヤの上に形成され、一定期間における信号値間の時相関係を定義します。プロパティ宣言レイヤはシーケンシャル表現のレイヤの上に形成され、検証対象となるハードウェア動作を定義します。アサーション指示レイヤは、これらのハードウェア動作を明示的にデザインに関連付け、検証ツールがこれらの動作をどのように使用するかを指定します。
サンプリング
シミュレーション・ツールとサイクルベースでデザインを認識するフォーマル検証ツールの一貫性を確実に保つために、SystemVerilogのconcurrentアサーションでは、サンプリングされた信号値を使用して式を評価します。サンプリングされた信号値は、クロック発生前の最終シミュレーション・タイムステップの終わり（たとえば、PLI＊2によって定義されるリード・オンリーの同期時間）における信号の値として定義されます。このように、イベントの順序付けや評価といったシミュレータの内部メカニズムに関係なく、予測可能な結果を評価から得ることができます。
＊2 PLI = プログラミング・ランゲージ・インターフェイス。
|
|
|
図2 SystemVerilogアサーションにおける値のサンプリング
|
値はタイムステップの先頭で他の動作が発生する前にサンプリングされます。
|
クロックエッジを基準としたサンプリング信号の明示的な概念は、SystemVerilogアサーションの動作の重要な要素であり、アサーションが単にSystemVerilog言語の一部であるという理由により可能になったと言うこともできます。Verilog HDLのスケジューリング・メカニズムの拡張により、値のサンプリングがサポートされ、アサーションが言語の他の部分とシームレスに機能するための「フック」が備わりました。このようなスケジューリングの拡張により、シミュレータやその他のツールで、アサーションの実行および回路やテストベンチのモデリングに既存の最適化アルゴリズムを適用できるようになりました。
上述の「フック」がVerilog HDLの一部とはならない他のアサーション専用言語ではこの明示的なサンプリング・メカニズムを定義できません。制限付きのコーディングスタイルに従えば、Verilog HDLでもこの動作に近づけることはできます。ただし、マルチクロック・システムなどにおいては依然レース・コンディションが生じる可能性があるため、この目的を達成するためにVerilog HDLのスケジューリングを機能強化しないことには、すべてのケースでフォーマル検証ツールとシミュレーション・ツールの一貫性を保証することは不可能です。
レース・コンディションはVerilog HDLのイベントベース・スケジューリングのセマンティクスによって生じるもので、これにより同一のシミュレーション時間に複数のイベントが発生する場合があります。合成ツールとフォーマル検証ツールは回路をサイクルベースで認識するので、レース・コンディションは常にSystemVerilogアサーションが使用するのと同じサンプリングのセマンティクスに従って解決されます。つまり、アサーションにより、実質的には合成前のRTL検証で合成後の回路動作を推定できるので、合成前後のミスマッチが解消されます。
concurrent アサーションと immediate アサーションには2つの重要な相違点があります。第1に、concurrent アサーションは、 always ブロックまたは initial ブロック内の文としてデザインで手続き的にインスタンス化されるほかに、手続き的ブロックの外部でモジュールレベルの文（継続的代入文と同様）として宣言型のインスタンス化を行うこともできます。第2に、concurrent アサーションでは、immediate アサーションのように組み合わせ条件のみではなく、チェック対象の時相動作を指定できます。concurrent アサーションのシンタックスは次のとおりです。
concurrent_assert_statement ::=
assert property ( sequential_expr_or_property )
[[ pass_stmt ] else fail_stmt ]
シーケンシャル表現は信号のサンプリング値を使用して評価され、pass/fail文によりアサーションとテストベンチの通信が可能になります。アサーションは言語の構成要素なので、これらの文ではSystemVerilogのすべての機能を利用してイベントのトリガ設定、カバレッジ情報の記録、検証コードのフローに対するその他の操作（Cコードの呼び出しなど）が行えます。アサーション専用言語は実質的に「リード・オンリー」なので、回路動作の監視のみが可能で、回路やテストベンチの信号値を操作することはできません。
シーケンシャル表現
SystemVerilogでは、アサーションで信号のサンプリングの適切なセマンティクスが定義されているので、式の間の時相関係を明確にしてシーケンシャル表現またはブーリアン表現のシーケンスを指定することができます。シーケンスのマッチを判断するため、ブーリアン表現は、シーケンスに関連付けられたクロックによって定義される連続したサンプリング・ポイントで評価されます。すべての式がtrueであれば、シーケンスはマッチしています。最も基本的なシーケンシャル表現は、「aに続き次クロックでbが起きる」といったものです。これはSystemVerilogで次のように表現されます。
a ##1 b
この例で、"##1"は、シーケンスに含まれる連続したブーリアン表現の間の1クロック遅延を示しています。
サイクル遅延演算子"##"と遅延演算子"#"の類似性に注目してください。遅延演算子"#"は、遅延するタイムユニット数を指定します。このように既存のVerilog HDL構文の自然な拡張構文により、Verilog HDLのユーザーにとって周知である遅延の概念から構文の意味を容易に類推が可能です。この拡張構文は、明示的なクロックサイクル遅延を指定するためにSystemVerilog のどこにでも使用できます。これは、アサーションとシーケンスの定義をSystemVerilogの一部として含めることによって、言語のさまざまなエリアで同じ構文を共通概念で使用できることの一例です。
SystemVerilogでは1つのブーリアン表現または他のシーケンスをシーケンスの要素にできるという点を理解しておくことが重要です。シーケンスの観点では、ブーリアン表現は、長さ1の縮退シーケンスです。したがって次の式は、
s1 ##1 s2
シーケンスs1終了後のクロックでシーケンスs2が開始するという意味です。
|
|
|
シーケンスs2はs1の完了の次のサイクルで開始します。
|
|
|
|
シーケンスs2はs1の完了と同じサイクルで開始します。
|
シーケンシャル表現は式の間の時相関係を指定するのに便利なだけでなく、言語の要素としてシーケンシャル表現を捉えることができるので、再利用と参照が可能である点が重要です。このようにSystemVerilogには、他のシーケンシャル表現の構築のため、または以下で説明するようにアサートされるプロパティの一部として、言語のどこででも宣言と再利用が可能なシーケンスの概念が導入されています。
SystemVerilogでは次のシンタックスを使用してシーケンスを宣言します。
sequence_declaration ::=
sequence name [ ( formal_item {, formal_item } ) ] ;
{ assertion_variable_declaration }
sequence_spec ;
endsequence
ジェネリックなフォーマル引数のリストにより、シーケンスがインスタンス化される時に渡される実際の引数に対して適用される汎用の時相関係としてシーケンスを指定することができます。例えば次のシーケンスは、
sequence seq1 (a,b);
a ##2 b;
endsequence
2つの式のシーケンスを表現しています。このシーケンスが次のようにインスタンス化されると、
seq1(e,f)
シーケンス定義のジェネリックなフォーマル引数aおよびbがそれぞれ実際の引数eおよびfに置換されるので、eとfの時相関係は次のようになります。
e ##2 f
下記の表は、シーケンスに対して実行できる操作の一部をまとめたものです。
|
|
|
この方式では、シーケンスの開始時に関係なく、
関連付けられたシーケンスがマッチとなったサイクルで true のブーリアンを返します。
|
|
|
|
シーケンス "s1 or s2" には複数のマッチがあります。
つまり、s1がマッチしてs2がマッチするサンプルのそれぞれです。
s1がマッチした場合は、s2がマッチしているかどうかに関係なく、
"or" シーケンスもマッチします （その逆も同じです）。
|
|
|
|
s1は第4サイクルでマッチしていますが、
"and" シーケンスは、第6、第7、第8サイクルのs2がマッチするサイクルまでマッチしません。
|
|
|
|
s2は第6、第7、第8サイクルでマッチします。
インターセクト・シーケンスはs2とs1の両方がマッチする第7サイクルでのみマッチします。
|
|
|
|
シーケンスs1には、第6、第7、第8サイクルに複数マッチがあります。first_match演算子は、
第6サイクルでマッチするシーケンスのみくり返します。
|
シーケンスのローカル変数
シーケンスは信号間の時相的な順序関係を指定します。ただし、一部の複雑な動作を記述するには、シーケンスの特定ポイントにおいて値を明示的にセーブし、後のシーケンスで参照できる必要があります。「データがパイプラインに入った時、そのデータは3?5クロック後の間に出現し、その値は1インクリメントされたものとなる」というシーケンスを考えてみてください。
sequence s5;
int d;
@ (posedge clk) (d = data, valid) ##[3:5] (dout == (d+1));
endsequence
valid信号はデータがパイプラインに入るタイミングをマークし、3?5クロック後に、パイプラインの出力であるdoutは入力データを1インクリメントした値に等しくなります。
シーケンス固有のデータをシーケンスで直接的に取り出すことにより、ユーザが専用のステートマシンやその他の補助的な記述を用意してデータを取り出す必要はなくなり、その補助的な記述をシーケンスのそれぞれの評価に関連付ける必要がなくなります。また、補助的な記述が実際には回路の一部ではないということを他のツールに知らせなくてはならないという問題もなくなるので、ツールの使用フローがシンプルになります。
プロパティ
多くの場合、シーケンスは単体で明示的な動作を十分に表現できますが、プロパティ宣言レイヤにより、さらに一般的な動作を指定することができます。特に、プロパティにより、シーケンスの意味の反転（シーケンスが発生しない場合など）、シーケンス評価の無効化、または他の何らかの事象によってシーケンスが発生するという定義が行えます。プロパティ構文では、次のシンタックスを使用してこれらの機能を実現できます。
property_declaration ::=
property name [ ( formal_item {, formal_item } ) ] ;
{ assertion_variable_declaration }
property_spec ;
endproperty
property_spec ::=
[clocking_event]
[ disable iff( expression )] [ not ] property_expr
property_expr ::= sequence_expr | implication_expr
プロパティ定義は、property-endpropertyというキーワードのペアで指定され、シーケンス定義と全く同様にフォーマル引数と引数渡しをサポートします。次の例を考えてみてください。
property p1;
@ (posedge clk) disable iff (test) not abort_seq;
endproperty
not演算子はabort_seqシーケンスの意味を反転するので、abort_seqが発生するとシーケンシャル表現は実行されません。"disable iff"節は、test信号が1の場合にのみ、シーケンスの評価を無効にします。SystemVerilogのどこにでも使用されるキーワードdisableとiffの再利用に注目してください。このプロパティは、「test信号がローの間はabort_seqシーケンスが発生しないことをチェックする」と解釈することができます。
もう一つの有用な動作概念はインプリケーション（含蓄）の概念です。有効なinit_seqシーケンスの発生後にのみabort_seq シーケンスをチェックする場合を考えてみます。このプロパティは次のように記述されます。
@(posedge clk) init_seq |=> abort_seq;
上記で、|=>は非オーバーラップ・インプリケーション演算子です。このプロパティ式は、先行シーケンスinit_seqの正常終了のそれぞれが、次のクロックでの後続シーケンスabort_seqの発生を示しているということを表しています＊3。先行すべきシーケンスが発生しないクロックサイクルでは、後続するシーケンスは評価されず、プロパティは空のtrueであると認識されます。
＊3 オーバーラップ・インプリケーション演算子"|->"は、先行シーケンスがマッチするのと同じクロックで後続シーケンスが開始することを示します。
マルチクロックのサポート
ここまでの全ての例では、1つのクロックでシーケンスのすべての信号をサンプリングしていました。ユーザーが慎重にすべてのレース・コンディションを回避するシングルクロック・システムでは、Verilog HDLのセマンティクスでアサーション言語をシミュレーションに接続し、正しい答えを得ることができました＊4。しかし、他の設計グループのモジュールやベンダのIPブロックなどが含まれてシステムが大規模になるに伴い、これらの厳密なガイドラインにあわせた設計を行うことができる可能性は非常に小さくなってきています。既に説明したように、アサーションをSystemVerilogに統合する利点は、このような過度に厳密なデザイン規約を排除するようにセマンティクスが定義される点にあります。レース・コンディションの問題は、前述のサンプリング・メカニズムの規定によって解決済みです。
クロックの異なるシーケンスを連接する時は、マルチクロック連接演算子"##"を使用します。
＊4 このようなシングルクロック・アサーション言語の一例はAccelleraのOpen Verification Libraryです。
@(clk1) s1 ## @(clk2) s2;
|
|
|
シーケンスs1がclk1で検出されたあとで次のclk2でs2が開始します。
|
最初のシーケンスはclk1の各サイクルで評価され、このシーケンスがマッチすると、##演算子は次のclk2へ移動してシーケンスs2の評価を開始します。2つのクロックが同じ場合、これは下記と等価です。
@(clk) s1 ##1 s2;
シングルクロック・シーケンスと同様、マルチクロック・システムでも、いつ開始したかに関係なく、サブシーケンスの終わりを追跡すると便利です。シーケンスのmatched方式では、シングルクロックの場合のended方式と同様に、この機能を使用できます。ただし、endedと異なり、matchedでは、もう一方のクロックの最初の発生まで、シーケンス評価の結果が保存されます。
|
|
|
clk2でのシーケンスs2の完了は
clk1の次の発生までラッチされます。シーケンスs3はs2のマッチ後の
次のclk1イベントで開始します。
|
マルチクロック・シーケンスの連接とmatched方式を含めることにより、複数のクロックドメインにまたがる動作を指定するシーケンスとプロパティを記述することができます。サンプリングのセマンティクスおよびラッチされたmatchedの動作により、2つのクロックエッジが一致している場合、すなわちクロックが重なる動作時にもレースは発生しなくなります。この機能がなければ、このような状況でレース・コンディションが発生する可能性が非常に高くなります。
手続き的アサーション
実際、ほとんどの順序アサーションは何らかの形式のハードウェア動作意図の表現（「これが発生するとあれが発生する」）なので、アサーションを記述する人は、アサーションをトリガするための先行式（条件）を指定する必要があります。前述のように、アサーションと設計言語の統合の利点は、設計エンジニアが容易にアサーションをデザインに埋め込めることです。ただし、宣言型のアサーションを効果的に使用するには、その性質から、設計者が追加作業を行わなくてはならないこともあります。
有限ステートマシン設計を考えてみます。このタイプのデザインのアサーションは、「この状態の時、それが発生する」という形式になることが多く、たとえば、「ACK状態の時、fooがハイであれば、reqは5クロックサイクル間ローのままである」となります。このアサーションは、次のように宣言型でコーディングを行うことができます。
P4: assert property(
@ (posedge clk) (st == ACK) && (foo == 1) |-> !req[*5]);
次に、これに伴うステートマシンのRTLコードがどのようになるか見てみましょう。
always @ (posedge clk)
case (st)
ACK:
if (foo == 1)
begin // when in this state, req should be low for 5 clocks
...
end
...
endcase
デザインとアサーションでは、クロックとトリガ状態という2つの情報が重複しています。これらの情報を重複させるのではなく、アサーションのシンタックスが設計言語の一部であるという事実により、これらの情報を手続き的にRTLコードに埋め込み、使用法からこれらの情報を推定させることができます＊5（下記参照）。
always @ (posedge clk)
case (st)
ACK:
if (foo == 1)
begin
P5: assert property (!req[*5]);
...
end
この手続き的concurrentアサーション（P5）は、上記の宣言型concurrentアサーション（P4）と意味上は等価になるように定義されていますが、使い方と管理がさらに容易です。手続き的に埋め込まれたアサーションは、宣言型のアサーションと同様に、サンプリングされた信号値を使用して、定義されたトリガ条件を評価します。先行式の定義ルールには、case文とif-else文の両方が含まれており、手続き的アサーションに対して複雑なトリガを推定させることもできます。
結果として手続き的アサーションの利点は、管理が容易になるという点です。つまり、有限ステートマシンのコードが変更された場合に、アサーションのトリガ条件は自動的に更新されます。これに相当する宣言型のアサーションの場合は、正しいトリガ条件を更新するために手作業でコードを変更する必要があり、人為ミスによりアサーションがデザインを正確に反映しなくなる可能性があります。
アサーションとテストベンチの相互作用
前述のように、アサーションと設計/検証言語の統合の利点は、アサーションからテストベンチへ情報を伝達できる点です。アサーション専用言語には、このような通信メカニズムはありません。SystemVerilogでは、アサーションのpass文とfail文で任意の手続き文を実行できるので、発生したシーケンスやカバレッジに対するカウンタの更新、または検証の効果に影響する可能性のあるその他のもの（信号値の設定、クラスオブジェクト方式の呼び出し、Cコードの呼び出しなど）をテストベンチに通知することができます。
「アボートサイクル発生後2クロックサイクル間は新しいバスサイクルを開始しない」というプロパティを含むバスプロトコルを考えてみてください。このプロパティは次のようにコーディングできます。
property wait_after_abort;
@ (posedge clk) abort_cycle |=> !cycle_start[*2];
endproperty
P6: assert property (wait_after_abort);
abort_cycleシーケンスが検出されると、このプロパティにより、cycle_start信号が2クロックサイクル間0であることが指示されます。プロパティP6はこの動作を明文化しており、シミュレーションで動作をチェックするためのモニタとして、またはフォーマル検証ツールでその動作が発生しないことを証明するために使用することができます。
＊5 埋め込まれたアサーションのわかりやすさに注目してください。このアサーションは、前の例でコメントとして示されていたのと同じ情報を明確に示しています。
ただし、このプロパティが最上位レベルのインターフェイスの動作を定義している場合、テストベンチは、この動作に従わなくてはならないバス・トランザクションを生成していることになります。テストベンチを作成する検証エンジニアは、生成されるスティミュラスがその動作に違反しないようにするための制約条件として、アサーション情報を再利用することができます。
この種のテストベンチは次のようになります。
program manual_stimulus_generator;
repeat(1000) begin
generate_transaction(addr,data);
while(wait_cnt > 0)
@ (posedge clk) wait_cnt--;
end
endprogram
wait_cntカウンタは、テストベンチによって生成されるバス・トランザクション間の遅延を指定するために使用されます。coverディレクティブの使用により、abort_cycleシーケンスを使用してこのカウンタをセットすることができます。
cover property( abort_cycle ) wait_cnt = 2;
coverディレクティブの使用によりabort_cycleシーケンスの検出が可能になり、検出されなかった場合のエラーは発生しません。このシーケンスが検出されると、wait_cntカウンタは2にセットされ、テストベンチは2クロックサイクル待機してから次のトランザクションを生成します。SystemVerilogのスケジューリングのセマンティクスにより、pass文の実行とテストベンチ間にレース・コンディションがないことが保証されます。これは、アサーションが他の言語で記述されていた場合には保証されません。
SystemVerilogでは、テストベンチと回路の間に明示的な同期インターフェイスを指定することができます。クロッキング・ドメイン構文は、テストベンチが定義対象のクロックを基準としてテスト対象デバイス（DUT）信号のサンプリングとドライブを行うタイミングを定義します。デフォルトの場合、テストベンチによる信号のサンプリングはアサーションによって使用されるサンプリングと同じなので、テストベンチはアサーションと同じ値にアクセスすることができます。前述のように、これによってテストベンチ/アサーションとDUT間のレース・コンディションが回避されるだけでなく、合成前のRTL検証時に、合成ルールに従ってレース・コンディションが解消された状態で、テストベンチに「合成後」の回路動作を認識させることができます。
設計者のためのSystemVerilogアサーション
アサーションは、何らかの方法で回路設計者に利用されてこそ価値があります。これまで典型的な検証プロセスでは、回路が動作する環境、および回路の機能仕様に関して設計者が理解しているつもりの前提の正当性の確認にかなりの部分が費やされます。私たち設計者は何度｢動くはずだ｣と言っておきながら、実際には仕様を読み間違えていたり（少なくとも仕様に対する解釈が同僚と違っていたり）、記述された機能が意図したものとわずかに異なってしまうようなつまらない間違いをRTLコードで犯していたりしたでしょう。このため、設計者が、デザインの残りの部分や検証方式に容易に適用できる使い慣れた方法で、簡潔に前提を定義できることが非常に重要です。
設計者が既に使用している言語とSystemVerilogアサーションの統合は、設計者によるこのパラダイムの利用を可能にし、おそらくはアサーション専用言語に比べてSystemVerilogが最も優れている点です。SystemVerilogアサーションはデザインコードに直接的に埋め込めるので、アサーションをデザインに追加するために必要な労力はわずかです。設計者は、プロパティを宣言型としてまたは手続き的に直接記述することも、ライブラリの検証済みプロパティをインスタンス化することもできます＊6。いずれにせよ、アサーションはデザインの一部になり、設計者にとって使いやすく、使用される可能性が高くなります。
VHDLユーザーは、言語混在に対応したツールのサポートにより、SystemVerilogでconcurrentアサーションを記述することができ、bind文を使用してアサーションをSystemVerilogと同様にVHDLのコンポーネントまたはインスタンスに接続できます。SVAのブーリアン表現は、言語混在に対応したツールがVHDL信号を含むVerilog HDL式の記述をサポートするのと同様に、VHDL信号をサポートします。
＊6 アサーションは統合されているので、Verilog HDLユーザーが使い慣れた既存のライブラリ・メカニズムによってサポートされているモジュール、プログラム、またはインターフェイスに組み込むことができます。
検証のためのSystemVerilogアサーション
検証エンジニアは、さまざまな手段とツールを使用して徹底的な機能チェックを行う場合があります。この方式を有効にするには、各検証ツールの結果に一貫性がなくてはなりません。そうでなければ、設計よりもツールの問題の解明に多くの労力が割かれてしまいます。SystemVerilogアサーションのユーザーは一貫性のある結果を得ることができます。なぜなら、SystemVerilog では、値のサンプリング、およびアサーションの実行が行えるように、Verilog HDLのスケジューリングのセマンティクスが明示的に拡張されており、シミュレーションとフォーマル検証ツールで同じ答えが得られるようになっているからです。
なお、アサーションのこのセマンティクスが確実に認識されるように、SystemVerilog標準言語では、シミュレーションのタイムスライスにいくつかの新しいコールバック・ポイントを定義することで、この条件をサポートしています。これらの拡張仕様は、定義上Verilog HDLには存在しないため、専用言語とVerilog HDLを同様に確実に認識させ、相互作用させることは、不可能ではないにしても困難になります＊7。
また、スケジューリングのセマンティクスおよびSystemVerilogでのアサーションの統合により、テストベンチとアサーションの連携も可能になります。つまり、テストベンチがアサーションの存在を認識し、アサーションの状態に対して反応できるということです。アサーションが専用言語で記述される場合、テストベンチが参照できるものは何もありません。スケジューリングの拡張仕様により、アサーションの評価後に、タイムスライスの後段のポイントで、検証コードを実行することができます。実際、concurrentアサーションのpass/fail文ブロックはこのような検証コードの一例で、アサーションからテストベンチへ情報を伝達するための便利なメカニズムです。他のアサーション言語にはスケジューリングも通信メカニズムもありません。
また、統一言語により検証環境が非常に柔軟になります。たとえば、SystemVerilogにはPLIを必要とせずにC関数を直接的に呼び出す機能があります。これにより、C関数をアサーションのpass/failブロックに含めて、アサーションがパスまたは違反した時に自動的に呼び出させることができます。
assert property (myprop) call_Cpass(); else call_Cfail();
アサーションの違反またはパスに基づくC（またはVerilog HDL）関数の直接呼び出しによって特定の動作を実行させることは、アサーションの診断情報やカバレッジ情報を生成する上で重要です。SystemVerilogでは、これらの検証情報の生成に必要なカスタマイズが行えます。
統一言語SystemVerilogでは、機能性と柔軟性という利点に加えて、性能も大幅に向上します。言語の統一により、シミュレーション最適化アルゴリズムをアサーション、テストベンチ、およびデザインに適用できるため、長い間HDLシミュレーション・ツールと検証専用ツール間のボトルネックであった通信オーバーヘッドが解消されます。
前述のアサーション・スケジューリング・メカニズムは、このような最適化が引き継がれるようにするために、既存のVerilog HDLスケジューリングの拡張仕様として設計されています。アサーションをはじめとするSystemVerilogの可用性と性能の向上は、主にこれらの概念が1つの言語に統合され、これらの概念全てを1つのシミュレーション・プラットフォームとしてインプリメンテーションの観点からも結び付けられるようになったことによるものです＊8。
＊7 新しいコールバックを利用してアサーション専用言語をSystemVerilogと相互作用させることもできますが、アサーションは言語に組み込み済みなので、このような面倒な作業は必要ありません。
＊8 シノプシスのHDLシミュレータVCSは、Verilog HDLおよびVHDLにネイティブ・コード生成アルゴリズムをSystemVerilogに拡張することにより、テストベンチとアサーションおよびデザインの性能を最大にします。
結論
近年、特に検証効率の向上やバグの迅速な検出にあたりアサーションで成功を収めている技術チームが増加しているという事実が示すとおり、ユーザーとEDAベンダは、検証問題に対処する上でアサーションは非常に重要な技術であるということで意見が一致しています。ただし、ここで解説したように、使いやすさ、予測可能性、移植性といった多数の利点は、アサーションがデザインとテストベンチの両方を記述する言語の一部となって初めて達成可能なものです。これがまさに使い慣れたVerilog HDLをベースに発展してきたSystemVerilog言語なのです。
検証方式に取り入れるアサーション言語を慎重に調査するには、検証方式に関与するすべての設計/検証言語を調査するとともに、これらの言語の相互作用を理解しておく必要があります。実際、相互作用のための手段そのものは非常に微妙ですが、アサーションの適用を成功させるには最も重要な条件かもしれません。SystemVerilogは、設計のための構文とアサーションを含む検証のための構文を備えた統一言語であり、これらの構文の相互作用を明示的に定義します。その結果、SystemVerilogを使用することで、技術チームは以下のことを理解できるようになります。
■ アサーションとテストベンチの通信を確立する方法
■ アサーションの結果として生成されるメッセージ出力のカスタマイズ方法
■ アサーションのパスまたは違反に基づくVerilog関数およびC関数呼び出しの作成方法
■ 回路の制御構造の推論によってアサーションコードを最小限に抑える方法
さらに、SystemVerilogアサーションでは、シミュレーション・ツールとフォーマル検証ツールによるアサーションの評価方法の認識が一貫しているので、これらのツール間のミスマッチをデバッグする必要はなくなります。
ユーザーの観点からは、アサーション機能と設計/検証言語の統合には多くの利点があります。一方、業界の観点からは、異質なアサーション言語の統合により、ユーザーが必要とする機能性を網羅する単一の言語標準が実現することを意味します。SystemVerilog言語に統合されたアサーションにより、EDAベンダは、複数の言語をサポートするためにリソースを割くことなく、能率化されたフローに対応した強力な機能でツールを改善することに集中できます。
結果として、ユーザーはさらに優れたツールを手に入れることができ、単一の標準言語に基づく検証環境を構築できます。この検証環境は、SystemVerilog標準によって規定されるデザインと検証の動作の解釈が一貫しているので、様々なベンダのツールを自由に選ぶことができるからです。また、SystemVerilogベースの環境では、設計/検証フローのあらゆる側面がサポートされているので、設計エンジニアと検証エンジニアによる最高の共同作業とコミュニケーションにより、デザインを正しく機能させることができるようになります。
|
