1. はじめに

　　今日の複雑なハードウェア設計において、ハードウェア検証のクロージャーに対する特効薬的な解決策は無いと言えるでしょう。それは即ち、全てのデザインコンポーネントの部類に対して検証クロージャーを達成する単一のツールやプロセスが存在しないということです。例えば、単純な32ビットのコンパレータを徹底的にシミュレーションするには、最高速のシミュレータを使ったところで、百数十年もの時間を要します。この結果、カバレッジ空間における抜けが発生します。つまり検証課程において活性化されなかった部分です。スタティックなフォーマル検証は、設計者が開発するブロックに対して、徹底的且つ数学的なテクニックを用いることにより、自動的にすべての取り得るコーナーケースを探索することが可能です。例えば32ビットのコンパレータの証明は秒単位で可能です。とは言うものの、スタティックなフォーマル検証は大規模なデザインに対してはステートの爆発を起こすという問題があり、全てのデザインコンポーネントの部類に対して適用できるわけではありません。例えばMPEGデコーダなどはスタティックなフォーマル検証にとって適切な候補ではありません。ハードウェア検証のクロージャーに対しては特効薬的な方法が無く、きつい設計スケジュールに対して検証リソースも限られている今日のASIC開発フローにおいては、検証に用いる「武器」を賢明に選択し、タイムリーに適用しなければ、検証のクロージャーを達成することは不可能と言えます。

2. 検証クロージャー

　　カバレッジは検証の完全性を測定するものです。しかし何かを測定するには、必ず指標が必要になります。残念ながら検証プロセスに対する特効薬はありませんので、デザインの機能的な振る舞いを完全に特性化するための単一の指標は存在しません。従って今日の設計におけるカバレッジ空間は、複数次元的で垂直的な指標の組み合わせでしか表現し得ません。 　　例えばラインカバレッジはHDLモデルから自動的に抽出することが可能な暗黙的な指標の例です。一次元のカバレッジ空間を形成します。ファンクショナルカバレッジは、他の次元を持つカバレッジ空間を形成する、高位の明示的な指標の例です。アサーションにおけるカバレッジは、カバレッジ空間に更に次元を追加する、明示的な指標の例です。この様に、カバレッジ空間に対する他の多くの次元、つまり指標が存在します。私達はそれらを定義することで、デザインの動作を近似するのに役立てることができます。検証クロージャーというゴールを達成するには、検証課程におけるカバレッジ空間の各次元を最大限にするよう、取り組むことが必要です。 　　シミュレーションを用いたフローでは、ファンクショナルカバレッジのクロージャーを達成するプロセスとして、以下のステップが必要になります。

2-1. カバレッジの制御性と観測性

　　機能検証において、カバレッジには検証クロージャーを計画する際に理解しておかなくてはならない二つの側面があります。即ち制御性のカバレッジと観測 性のカバレッジです。 制御性のカバレッジは、入力スティミュラスのクオリティーに対する基準で、それはデザイン中にある様々なストラクチャー（例えばラインカバレッジ）や、期 待されるデザインの振る舞い（例えばファンクショナルカバレッジ）を活性化する能力の基準です。実際に、今日のシミュレーションによる指標の多くは、実際 には、制御性の測定と言えます。
　 フォーマル検証はシミュレーションとは異なり、入力スティミュラスに依存しません。何故ならばフォーマル検証は入力ベクターやスティミュラスを使用せ ずに、数学的な技法を用いてデザインの完全な入力空間を探索する為です。この意味は、仮にフォーマル検証を用いてプロパティーが真であることが証明された 場合、コーナーケースのバグを露呈させるような入力ベクターのシーケンスは一切必要ないということです。即ち、フォーマル検証では、完全で有効な入力空間 を考慮するため、デザイン中のストラクチャーを入力スティミュラスがいかに活性化できるかというクオリティーを測定する指標が必要ないのです。
フォーマル検証におけるリスクは、入力空間を、起こり得る動作のサブセットに限定する制約条件を用いて証明が実施されたかも知れないという点です。 よってフォーマル検証において、制約の正当性を確認することは極めて重要です。 検証に対して考えなくてはならない他の側面は、観測性のカバレッジです。つまり、全ての期待される動作を正当化するチェッカーが、テストベンチ内に充 分存在するか否かです。アサーションベース検証においては、観測性はアサーション密度という指標で測定されます。これはデザイン中のストラクチャーで、ア サーションによってカバーされていない部分を特定するのに役立ちます。

2-2. カバレッジ指標

　　数多くのカバレッジ指標が、検証プロセスの有効性やクオリティーを決定する目的で開発されています。アドホック的な指標には、例えばバグレート、最後にバグが見つかった時からのシミュレーション時間、全体で実施したシミュレーションサイクル数などがあります。これらの指標は興味深い定量的なデータを示していますが、カバレッジ指標として見た場合、つまりいかに良くデザインが検証されたか、あるいはデザインのどの部分がテストされずに残っているかなどについての定量的なデータは、ほとんどありません。重要なことは、仮に検証されていない機能があったとしても、バグレートがゼロまで減少したならば、検証に対する労力は完全なものだと言えるのか、ということです。
コードカバレッジという考え方は、もともとはソフトウェアのプログラムテスト用に開発された一組の指標をベースにしています。これらのプログラミングコードの指標は、実行スティミュラスによるコードの構文上の特性を測定するものです。言葉を変えて言うならば、それは制御性の測定ということです。
コードカバレッジの価値は、カバレッジの抜けを特定するところにあります。しかし、プログラミングコードの指標の欠点は、RTLコードに与えられたテストスティミュラスの制御性を測定するという側面に限定されてしまうことです。誤りのあるステートメントを活性化しても、シミュレーションの観測点において、デザインのバグがそれ自身を露呈するということにはなりません。
プログラミングコードにおける他の欠点は、機能的な正確さをテストするという意味において、何も定量的な実態が示されないということです。機能的な正確さを知るには、そのためのチェッカーおよびカバレッジ解析のテクニックを組み合わせるべきです。今日、この手法はアサーションのチェッカーおよびモニター（例：Accellera - OVL / Mentor Graphics Questa Verification Library - QVL）によって実現されています。
ストラクチャーカバレッジは、デザインの詳細やインプリメンテーション上の想定項目について最も詳しい設計者が、最も重要なストラクチャーに対してカバレッジを指定するものです。FIFOのフルやエンプティーの状態が検証課程において実行されなくてはならない、などがストラクチャーカバレッジの良い例です。またユーザー定義のファンクショナルカバレッジは、設計者が仕様に対して定義した動作の検証の完全性を測定するために使用します。ファンクショナルカバレッジモデルはしばしば複数のソースによって形成され、それにはアーキテクチャ上、マイクロアーキテクチャ上の仕様なども含まれます。通常は個別の要求項目をファンクショナルカバレッジの項目として指定します。しかし検証プロセスにおいて充分な同時並行性を探索するのであれば、これらファンクショナルカバレッジの項目の乗積によって、トータルのファンクショナルカバレッジモデルを作成することになります。

■プロセスの管理

　　既に議論したように、今日のトータルカバレッジ空間には複数のソースが関与します。これら全データを効果的に管理し、マージし、そして解析する方法を注意深く考慮する必要があります。メンター・グラフィックスはUCDB-Unified Coverage Databaseを用いて、複数ソースからなるカバレッジデータを管理し、サードパーティーのツール（つまり、他のカバレッジデータのソース）に対して読み書き可能なAPIによるアクセスを提供しています。

■データの鮮度

　　設計と検証が進むに連れ、カバレッジデータの精度が下がって行きます。つまり設計や検証の環境が変わるに連れ、これまで到達可能だったカバレッジ項目に、例えばバグにより、もう到達できないかも知れません。このような問題に対する一般的な解決策は、カバレッジデータの期限切れ期日を設定しておくことです。実際に数多くの組織において、期限切れ期日の幅を、カバレッジデータのマージおよび解析に適用しています。例えば先月のデータなどと指定すると、この期間を超えたものは消去してしまいます。

■データのマージ

　　必ずしもすべてのカバレッジ項目が、どの検証環境においても（例えばブロックレベル、クラスターレベル、システムレベルの違いなど）簡単に到達できるとは限りません。さらに、複数回インスタンス化されるブロックに対しては、インスタンス化されたブロックの異なるコンフィグレーションにより、必ずしもすべてのカバレッジ項目が到達できるとは限りません。従ってデザインの未検証機能を特定する解析のためにデータをマージしますが、カバレッジデータは別に保守しておくことが必要になります。しかしながら、低いレベルの検証環境（例えばブロックレベル）においてカバレッジを達成したと考えることは楽観的です。そこにはシステムレベルでのバグが潜んでおり、低いレベルでのカバレッジ項目が、システムレベルの検証環境においては到達不可能となる可能性もあるのです。必ずしも常に可能ではないものの、システムレベルの環境においてカバレッジ項目に到達すればするほど、検証に対する確度は高くなります。このように実践的にクロージャーを達成するためには、リスクとそのトレードオフを理解することが重要になります。 。

■カバレッジモデルの忠実度

　　今日、多くの検証チームは、検証の完全性をファンクショナルカバレッジによって測定することに重点を置いています。明らかに、検証されるべき動作をより良く近似するためには、ファンクショナルカバレッジモデルの高度な忠実度が重要になります。プロジェクトチームがコードカバレッジ指標によってカバレッジモデルを補強できるようになるには、検証フローの後工程（ファンクショナルカバレッジのクロージャーが平らな状態になる点）まで待たなくてはならないかも知れません。即ち設計サイクルの後工程で多くのコードカバレッジの抜けが見つかったような場合、これはファンクショナルカバレッジのモデルの忠実度が低く、従って再モデルが必要となります。

■カバレッジの抜けをターゲットにする

　　到達することが困難なファンクショナルカバレッジの項目、あるいはコードカバレッジの項目は、しばしばフォーマル検証を用いることで、より効果的に検証できることがあります。次のセクションではシミュレーションとフォーマル検証を組み合わせて、高いカバレッジおよび高い検証の確度を達成するためのテクニックについて議論します。

3. フォーマルを補完するシミュレーション

　　今日の複雑なデザインに対してプロパティーを与える際に課題となるのが、デザイン中の深いステートに到達しようとすることでしょう。例えばスタティックなフォーマル解析では、デザイン中に組み込まれたFIFOのハイウォーター・マーク（潜在的なコーナーケース）に到達しようとして、多くのサイクルを浪費してしまいがちです。問題を単純化するために、例えばFIFOの幅や深さを減らすなど、マニュアルでデザインの抽象化をすることも可能かも知れません。もしプロパティーがクリティカルと特定され、いまの検証ゴールが与えられたスケジュールおよび限られたリソースの制約下においてこのプロパティーを証明することであれば、このような抽象化をマニュアルで行い、クロージャーを達成する選択肢もあります。 　　代替の策として、ダイナミックフォーマルという手法を用いることも可能です。これはシミュレーションを用いてフォーマル検証を補完しようというプロセスの例です。つまりダイナミックフォーマル検証では最初に経験則を用いて、シミュレーション実行によって興味ある深いステートの近傍まで到達します。続いて興味ある一組のステートが、自動的にスタティックフォーマルのエンジンに渡され、フォーマル探索の初期値として使用されます（図3参照）。このアプローチにより、スタティックフォーマルのツールが、初期リセットステートから探索を始めたのでは到底到達することのできない深いステートからその探索を開始することが可能になります。

4. シミュレーションを補完するフォーマル

　　セクション2においては、シミュレーションを用いたカバレッジのクロージャーを達成するために用いられる、ごく典型的なアプローチについて議論しました。しかし図2にあるように、カバレッジのクロージャーを達成することが困難であることには違いありません。お分かりのように、ダイレクテッドテストを書き、そしてランダムを偏向してカバレッジの抜けをクローズしようとしても、労力に対する明確なリターンが見え難いことも事実です。検証の確度を改善するためにも、何か代替のソリューションを求めるべきでしょう。フォーマル検証は、シミュレーションを用いたカバレッジのクロージャーに対し、以下の3つの点において補完することが可能です。

1. 抜けをカバーするために用いることのできるシナリオ（入力スティミュラス）を特定する。
2. 低い忠実度のカバレッジモデル により不注意に落してしまった入力空間を部分的に探索する。
3. カバレッジの抜けがある領域内にプロパティーを追加することにより検証の確 度を改善する。

5. まとめ

ここではカバレッジ指標やカバレッジデータの管理について触れました。カバレッジ解析、例えばカバレッジの期限や階層データのマージ、カバレッジモデルの忠実度、そしてカバレッジの抜けをターゲットとしたフォーマル検証など、様々な側面について議論しました。

Harry D. Foster
Principal Engineer
Design Verification and Test Division
Mentor Graphics Corporation