アサーション活用の手引き：その基本から、記述ノウハウ、フォーマル解析への展開まで（4/5 ページ）

ICの高機能化が進むに従い、その機能を検証する作業が非常に大きな課題となってきている。この課題を解決するものとして期待され、現在、着実に普及しつつあるのが、アサーションベース検証（ABV）である。本稿では、まずこのABVの基本について説明する。続いて、アサーションを記述する上での注意点などを紹介する。さらに、アサーションを利用したもう1つの検証手法であるフォーマル解析についても解説を加える。

[矢ヶ部 常義（日本ケイデンス・デザイン・システムズ），EDN]

パフォーマンスの低下を招く記述

　個々のアサーションがどのくらいシミュレーションに負荷を与えるかは、アサーション自体だけでなく、設計、テストスティミュラスに大きく依存する。しかし、パフォーマンスの低下が少ないアサーションを記述するよう意識しておくことは常に重要である。

リスト8　常時、活性化されるアサーション　

　イベントドリブン型のシミュレータでは、イベント（何らかの状態の変化）数が多くなればなるほど、シミュレーションのパフォーマンスが低下する。ゲートレベルのシミュレーションがRTLシミュレーションよりも遅いのは、前者のほうが格段にイベント数が多くなるためだ。同様の理由から、アサーションもイベント数が少なくなるように記述することが重要である。では、逆にどのようなアサーションを記述するとイベント数が多くなるのだろうか。

リスト9　ブーリアンチェックのみで負荷が軽いアサーション　

　リスト8のアサーションは、START信号が論理レベルの1のとき、常に活性化される。もし、このコードの真意がSTART信号の立ち上がりエッジをとらえたいということであるなら、信号のエッジ検出機能を使用して、$rose（START）と記述すべきだ。

リスト10　長い繰り返しが生じるアサーション　

　ただし、リスト9のようにブーリアンを常にチェックするようなアサーションであれば、1サイクルで終了し、かつ最適化が容易なので、シミュレーションへの負荷は比較的少ない。一方、長い繰り返しがあり、それが長期間にわたって終了しない場合、チェックが毎サンプリング行われるため、シミュレーション上のオーバーヘッドとなる（リスト10）。

リスト11　巨大なシフトレジスタが生成されるアサーション　

　また、PSLのprevやSVAの$pastは、過去の値を保持するために、内部的にシフトレジスタを生成する。大きなサイクル数を指定すると、そのサイクル数分のシフトレジスタが生成され、その巨大なシフトレジスタにおいてすべてのサイクルでシフト動作が発生するため、大きなオーバーヘッドとなる（リスト11）。

リスト12　非常に大きなオーバーヘッドとなるアサーション　

　HDLで記述したモニターと、アサーション言語で記述したモニターには大きな違いがある。通常、HDLで記述したモニターでは、1つチェックが始まると、それが終了するまで次のチェックは始まらない。それに対し、アサーション言語で記述したモニターでは、開始条件がそろえば、次々と個別のものとして多重にチェックが開始される。これをアサーションの「オーバーラップ」と呼び、大きなオーバーヘッドの原因ともなる。例えば、リスト12のアサーションでは、stall信号が真のとき、次々と個別のモニターの処理が始まる。

　シミュレーションに対し、記述したアサーションがどのくらいの負荷になるのかを見積もる方法としては、次のようなものがある。それは、アサーションと同等の内容をHDLのモニターとして1つ1つ記述してシミュレーションで動作させた場合に、どれくらいのオーバーヘッドになるかを考慮することである。それにより、アサーションによる負荷を多少は判断することができる。

　どのようなアサーションでも、イベントが発生する限りパフォーマンスを落とす原因となる。そのデメリットを上回るだけの効果が得られるアサーションを記述することが重要である。

フォーマル解析での利用

　ここまでに何度か触れてきたが、フォーマル解析はアサーションを活用した検証手法の1つである。実装が仕様を満足しているか否かを数学的に証明しようというもので、テストベンチは必要としない。ここで言う実装とは、SystemVerilog（Verilog HDLも含む）やVHDLで記述されたRTLのコードのことであり、アサーション（プロパティ）が仕様に当たる。

　例えば、「FIFOがオーバーフローしないこと」という仕様があったとする。フォーマル解析では、この仕様を表したアサーションとFIFOの設計データを入力するだけで、オーバーフローが絶対に起こり得ないことを網羅的に検証する。シミュレーションはテストベンチに依存した検証であるため、テストベンチの品質によってはバグを見逃す可能性がある。それに対し、フォーマル解析は、シミュレーションでは発見が困難なコーナーケースのバグの発見を可能にする。

図3　フォーマル解析での状態空間の探索　

　通常、フォーマル解析では、入力信号の取り得る組み合わせのすべてに対して検証を行う。すなわち、設計の仕様上、絶対に起こり得ない状態まで検証される。そのため、検証の負荷を減らすために、より実機に近い振る舞いで設計の検証が行えるよう、最低限の制約を加える必要がある。この制約のことを「入力制約」と呼ぶ。入力制約を用いることにより、アサーションにおける意図しないフェイル（擬似フェイル）の発生を防ぐことができる。例えば、FIFOを入力制約なしで検証すると、FIFOがフルの状態にあるのにもかかわらず、さらに書き込みを行おうとするために、意図しないオーバーフローのフェイルが発生する。これを防止するために、FIFOがフルの状態では書き込みを行わないという入力制約を追加するのである。

　フォーマル解析では、初期状態から次のサイクルで到達可能な状態空間の探索が自動的に行われる（図3）。その状態においてアサーションのフェイルがないかどうかを解析し、フェイルが発見されなければ次のサイクルで到達可能な状態空間を探索する。このような処理を繰り返す中で、到達可能な状態空間に変化がない時点（不動点）までにアサーションのフェイルがなければ、フォーマル解析の結果としてパスと判定する。なお、フォーマル解析を実行する中で、指定した時間内にすべての状態空間を探索できなかった場合には、全状態探索不能（Explored）という判定になる。

図4　シミュレーション環境へのフィードバック　

　フォーマル解析では、どのようなシーケンスでアサーションがフェイルになったのかを最短のパスで表した波形情報が生成される。この情報を基にデバッグすることもできるが、フォーマル解析のツールによっては、シミュレーション環境を生成できるので、それを用いたデバッグも可能である（図4）。

　多くのフォーマル解析ツールは、自動チェック機能を備えており、RTLのコードから自動的に検証項目を抽出することができる。この機能ではアサーションを準備する必要がないため、リントチェックと同じ感覚で、RTLコードの記述後すぐに実行できる。具体的には、デッドコード、FSM（有限ステートマシン）の状態到達可能性/状態デッドロック、バスのコンテンション（競合）/フローティングなどをチェックする機能が用意されている。筆者のこれまでの経験から言えば、最低限これらの問題が発生しないことを確認した上で、ユーザーが定義したアサーションを用いて検証を行うべきである。なぜなら、このような問題から影響を受けて、ユーザーが定義したアサーションでフェイルが生じるケースが多いからだ。無駄なデバッグ時間を削減するために、自動チェック機能をぜひ活用したい。

表2　フォーマル解析の適用が容易な個所の例　

　ところで、フォーマル解析はどのような個所に適用すべきものなのだろうか。フォーマル解析は、設計のすべてに対して適用すべきではない。費用対効果について考慮し、基本的にはデータパス系よりもコントロール系を中心に適用すべきである（表2）。また、シミュレーションで高い費用対効果を得ることが難しいような、多くの入力状態を持つ論理に対して適用すると効果的だ。最近では、パッドリング（I/O Pad-Ring）接続検証に適用することも多く、従来シミュレーションで行っていたフローを完全にフォーマル解析に置き換えることができるとともに、検証時間も大きく短縮できる。

　技術的な問題から、通常、フォーマル解析をチップレベルでの検証に適用するのは困難である。チップレベルでの検証項目は、エンドツーエンドの検証になることが多い。そこで問題のないことを証明するには、非常に多くの状態空間を探索する必要があり、現実的な時間内では解を出せないためだ。

　フォーマル解析には、アサーションを数学的証明手法で完全に検証できるというメリットがある。しかし、フォーマル解析手法で用いることのできるアサーションには現実的には制限があり、どのようなアサーションでもフォーマル解析を用いて検証できるわけでない。そのため、シミュレーションとフォーマル解析の特徴をよく理解し、互いを補うような形で検証を行うことが重要である。