はじめに

商用のフォーマル検証ツールが出現してすでに 25 年が経過している。Wilson Research Group が 2024 年に世界的な規模で実施し、Siemens EDAのHarry D. Foster氏が分析した「Functional Verification Study 2024」によると、フォーマル検証（プロパティ検証）を採用しているプロジェクトはASICで51.5%、FPGAで22%である。
フォーマル検証を適用しているプロジェクトでは、複雑な SoC や機能安全が求められるデザインに対して、以下のA、B、Cを目的として活用していることが、DVCon (Design and Verification Conference) に投稿され発表される多くの論文から伺える。

• Assurance（保証）デザインの動作の正当性を証明する
• Bug hunting（バグハント）デザイン内の既知のバグを特定し、未知のバグを探索する
• Coverage closure（カバレッジクロージャー）coverage ステートメント、bin、要素が到達可能か、到達不可能かを判断する

特にシミュレーションによるリグレッションテストが安定し、多くの新規バグが見つからなくなった状況において、フォーマル検証のバグハント手法を活用して新規バグを発見することは効率的かつ付加価値の高い検証アプローチである。この段階で発見されるバグは非常に厄介であり、そのほとんどは異常なイベントとシナリオの組み合わせの下で、機能操作の奥深いところで発生する。

フォーマル検証の経験者は、フォーマル検証結果から次のアクションへと導くことを直感的に知っている。しかし新規ユーザにとってこの習得は困難である。そこで本稿ではフォーマル検証について、プロジェクトの初期状態から最終段階に至るまで、さまざまな指標を用いて推し進め、フォーマル検証の中でも最も高度な使用方法であるシリコンのバグハントに至るまでの手法について解説する。シリコンバグとは通常は ASIC や SoC においてエンジニアリングサンプルを用いたポストシリコン検証において発見されるバグを指すが、FPGA プロジェクトにおけるシリコンバグの特定にも応用できることを付け加えておく。

フォーマル検証の成功要因

プロジェクトにおいてフォーマル検証の活用を成功裏に収めるには、その成功要因を理解することが不可欠である。DVCon に寄せられる多くの論文と、実際の複数プロジェクトにおいて蓄積されている知見から、以下の６つの指標を抽出し、定義した。

また、シリコンのバグハントにフォーマル検証を適用することは、従来のフォーマル検証におけるモデルチェックとはいくつかの点で異なることを以下にリストしておく。

• 過度な抽象化デザイン全体を検証するのではなく、無関係なモジュールを抽象化または除外して、フォーマル検証を可能な限り効率的にすることを目指す
• 過度な制約どのコンフィギュレーション、動作モード、およびインタフェースがバグを引き起こしたかが特定できているため、それに応じてデザインに制約をあたえ、未使用のインタフェースを無効にする
• 焦点を絞ったアサーション実機で観測されたバグシナリオに基づいて、バグシナリオとバグの定式化につながる前提条件を捉えるプロパティを作成する
• 深い初期状態フォーマル検証を時間0の初期値から開始するのではなく、シミュレーションシーケンスを活用して、設計機能動作の途中状態やバグ発生箇所付近で初期化する

これらの項目については、次のセクションで詳しく解説する。

スパイラルリファインメントによるバグハント手法

シリコンバグ探索で成功するためには、前述の成功要因に取り組むことが不可欠である。成功要因を管理し、さらに重要なことであるが、マネージャーに対して可視化できるようにするために、「スパイラルリファインメント」と呼ばれるバグハントのために図 1.に示すレーダーチャートを導入する。このレーダーチャートは６つの要素から構成されている。この目的は、フォーマル検証に関するエキスパートの有無やインタフェース制約の完全性など、主要な障害要因を特定することである。そして６つの要素を段階的に改善・洗練させることで、シリコンバグを捕捉できるようにする。

この洗練されたアプローチは実証済みのものであり、多くの知見が集まっている。スパイラルリファインメントによるバグハントプロセスは、以下の重要なステップで構成されている。

1. プロジェクトを支援できるフォーマル検証のエキスパートを特定する
2. 実機からの情報を活用して、分割統治法または消去法により、バグのあるモジュールを特定する
3. 前提条件、バグシナリオ、および可能であればイベントのシーケンスを捉えるアサーションを作成する
4. シミュレーショントレースから一連の有意な初期状態を抽出して特定する
5. フォーマル検証が適切なデザイン部分に到達できることを確認するために、最小限の制約でフォーマル検証を実行する
6. 実際のバグに焦点を絞る（ゼロインする）ために、制約とアサーションを絞り込む

シリコンバグのバグハントは、連続するリファインメントを伴う反復プロセスである。説明を簡素化するために、リファインメントステップを以下の 3 つのフェーズに分類する。またそれぞれのフェーズを色別に示したレーダーチャートを図 2.に示す。

• フェーズ 1：「初期」半径 = 8 (橙)、すべての情報を収集しフォーマル検証環境を設定する
• フェーズ 2：「改善」半径 = 6 (灰)、成功要因のそれぞれを改善してバグに近いシナリオを定義する
• フェーズ 3：「最終」半径 = 3 (緑)、クリティカルな成功要因を最適化してバグを見つける

次に各フェーズ（初期 / 改善 / 最終）において、主要な６つの障害要因、つまりレーダーチャートの各要素にどのような特徴があるか、どのような作業項目があるかについて解説する。

フェーズ１（初期）

1. デザインの複雑度
   • A) フォーマル検証が完全な SoC 設計を処理することを期待するのは現実的ではない。そこで標準インタフェースを持つ IP ブロックに焦点を当て、効率化を図る
   • B) メモリやストレージ構造をブラックボックス化する
   • C) プロパティに関連しないブロックや機能を削除する
2. エキスパートの確保
   • A) フォーマル検証を導入する前にフォーマル検証のエキスパートを確保することが重要である
   • B) シミュレーションによるリグレッションがテストベンチ環境を必要とするのと同様に、フォーマルによるリグレッションもフォーマルテスト環境を必要とする。この環境は、アサーションやカバレッジなどのプロパティ、標準インタフェースや独自インタフェースの制約、複雑でフォーマルに不向きなモジュールのモデリング等で構成される
   • C) さらに重要なことに、チームにフォーマル検証のエキスパートがいれば、設計者と協力して設計意図をプロパティに捕捉し、RTL 開発の段階でブロックに対するフォーマル検証を早期に実行する支援が可能である
   • D) フォーマル検証リグレッションの実行のセットアップやメンテナンス、障害発生時の問題のトリアージなども行うことができる
3. フォーマルエンジンの制御性
   • A) フォーマルエンジンがデザインに対して効率的に機能するかどうかを早期に判断することは重要である。プロパティ定義が自動化されたフォーマルアプリを用いてデッドコードの有無、FSM デッドロックなどを自動的にチェックすることは、フォーマルエンジンの制御性、観測性を判断する簡便な方法である
   • B) フォーマル検証ツールには、そのままでは処理が困難な設計構造を処理したり、複雑な状況で反例を見つけたり、ライブネスなど特別なフォーマルプロパティに対処するために、10 以上のフォーマルエンジンで構成されるのが一般的である。複数のフォーマルエンジンとそれらを制御するメカニズムをよく理解しておくと、さらに効率的である
4. アサーションの品質
   • A) フォーマル検証の結果品質は、フォーマルプロパティの質に依存する。不正確または誤ったプロパティは誤発火を引き起こし、余計なデバッグ時間を要する。
   • B) フォーマル検証では、複数のプロパティを同時に検証できる。そのため、ユーザは異なるプロパティの中で多数のシナリオを表現したり、ひとつのシナリオを様々な表現方法のプロパティで捉えたりすることが可能である
   • C) 新しいユーザにとって、プロパティ言語 (SVA や PSL など) を正確に記述することは難しく、その学習曲線を緩和するために、設計者が RTL によるモデリングコードを使用して、問題のあるアサーションを単純なものに簡素化することを奨励している
5. 初期ステート近接性
   • A) リセット信号をトグルするだけでほとんどのデザインブロックの初期化には十分であるが、デザインを熟知していればフォーマル検証に対して意味ある初期ステートをセットアップすることができる
6. 制約の完全性
   • A) 制約は、フォーマル検証の設計空間を制限するのに役立ち、これによりフォーマル検証ツールは現実的な反例を作成し証明を導きだすことができる。フォーマル検証の初期段階では、フォーマルテストベンチに制約を設けないことが推奨される。これによりユーザはプロパティの発火を確認し、ツールがそれらのプロパティを正しく探索できていることを確認できる。また反例は、プロパティの理解を深め、プロパティの修正や改良を行う際に役立つ。
   • B) 制約を再確認するには、シミュレーション環境にその制約を適用してみることが有効で、制約の正当性を確認するのに役立つ

フェーズ２（修正）およびフェーズ３（最終）

バグハントは継続的なリファインメントプロセスである。バグの異なるシナリオを探索するために、フェーズ 2 と 3を反復するのが一般的である。

1. デザインの複雑度
   • A) フォーマル解析に無関係なモジュールをブラックボックス化することに加えて、フォーマル検証のカットポイント、カウンター、およびメモリのリモデリングを行う。このアプローチによりフォーマル検証が扱うデザインの複雑度を下げることができ、さらに直接的にカットポイントを制御する自由度を得ることができる
2. エキスパートの確保
   • A) このフェーズは関係なし
3. フォーマルエンジンの制御性
   • A) 異なるフォーマルエンジンは、異なるクラスのプロパティに特化しており、バグを見つけることに焦点を当てている。証明エンジンよりも反例発見エンジンのみを展開する方が効率的であり得策である
   • B) 各フォーマルエンジンにはそれぞれ異なる特性があり、エンジンの稼働状況を監視することで、最も効果的なエンジンとその設定を特定することができる。フォーマル検証ツールはこの情報をフォーマル検証ナレッジデータベースに記録し、後続するフォーマル検証の実行時に活用することが可能である
4. アサーションの品質
   • A) アサーションは継続的に更新する。バグシナリオやフォーマル検証の反例からデザインの振舞いについてさらに深く学び、アサーションを洗練し、絞り込むことが可能である。フォーマル検証は多くのアサーションを同時に処理できるため、一般的に異なるシナリオをカバーするアサーションを追加する
   • B) プロパティは可能な限りシンプルに保つ、そしてプロパティを可能な限り短く記述する
5. 初期ステート近接度
   • A) バグハントでは、特にシリコンバグの場合には、バグ発生まで数千サイクルに及ぶ機能動作を要することがあり、この長いイベントの履歴をフォーマル検証で再現することは不可能である。時間０から開始する従来のフォーマル検証では、初期の設計検証には適しているが、複雑な機能のバグハントには非効率的である。そこで推奨される手法は、１つは機能シミュレーションのアクティビティを活用し、シミュレーショントレース内の興味深いステート状態からフォーマル検証を開始する方法である。もう１つは時間０から到達可能なサイクル距離内にプロパティをゴール設定し、証明またはカバーされたそのゴールを初期ステートとして次のゴールのプロパティに向けて探索するゴールポスティングという手法である。どちらも複数の初期ステートを利用し複数のフォーマル検証を同時に実行できる
6. 制約の完全性
   • A) 一般的に、フォーマル検証環境に過度な制約を与えるのは危険であるとされる。それは過度な制約によってフォーマル検証は反例を見つけられなくなる可能性があるからである。しかしフォーマル検証の実行効率を向上させるために過制約を使用する利点もある
   • B) 制約を活用して、フォーマル検証を分割して実行しては統合するアプローチを行うことができる。たとえばデザインが異なるモードで動作する場合、制約によって個々の動作モードで複数のフォーマル検証を実行する。各フォーマル実行は個々のプロパティに焦点を絞り、そして結果はより理解しやすくなる
   • C) フォーマル環境に過度な制約を課すことができる状況があり、もし特定の状況下でバグを探索する場合、その特定の状況に焦点を当てるために環境に過度な制約を課すことは有益であると同時に、プロパティが真である条件を確認したい場合、その条件に関してプロパティを証明することが可能になる

ここまでリファインメントプロセスを用いて、主要な６つの障害要因、つまりレーダーチャートの各要素についてフェーズごとに対処し、バグハントを成功裏に導く手法について解説した。目的とするバグを特定し、そしてそれを再現するフォーマルテスト環境が完成したことになる。設計者がやるべき事はバグの根本原因を特定し、RTL コードを修正する。そして RTL が正しく修正されたことを検証する必要があるが、フォーマルテストの環境はすでにあり、再実行することで容易に確認することができる。

このリファインメントプロセスを適用したケーススタディを、次のセクションから３つ紹介する。DDR3 コントローラ、メモリコントローラ、そしてパケットスケジューラについて適用した。

ケース１：DDR3 コントローラ

このケースはポストシリコンバグの例である。バグ発生のシナリオは DDR3 コントローラにおいて特定のメモリバンクとローアドレスの組合せ時に、書込みコマンドを連続発行すると、プリチャージのタイミングに関するプロトコル違反が発生するというものである。

図 3.はプロジェクトチームがフォーマル検証の各要因をどのように最適化しバグ特定に至ったかを表したレーダーチャートである。各要素について以下に説明する。

1. デザインの複雑度
   階層の適切なレベルで DUT を選択することで、フォーマル検証対象のデザインの複雑度を軽減したと同時に、DUT にはデザインを制約するのに役立つ標準インタフェースが存在している
2. エキスパートの確保
   プロジェクトチームにはフォーマル検証の専門知識が無く、ツールベンダにツールの支援とフォーマル検証ノウハウに関するトレーニングを受け、パイロットプロジェクトを立ち上げた
3. フォーマルエンジンの制御性
   メモリとデザインの不要な部分をブラックボックス化し、フォーマルエンジンがデザインを適切に制御できることを確認するために、予備的な自動フォーマルを実行して確認した
4. アサーションの品質
   バグシナリオおよびバグに至る一連のイベントを捉えるために、アサーションを作成した。アサーションの連続をサブゴールとして用い、前出のゴールポスティングを利用して、フォーマルにおける前提条件の連鎖を再現した。これにより、フォーマルエンジンをバグシナリオへと方向づけすることができた
5. 初期ステート近接度
   デザインに直列的な特質があるため、そのままではフォーマル検証手法の適用は困難だった。使用されている初期化シーケンスには init_ok 信号があり、デザインの初期化が完了するとアサートされる仕様だった。これをサブゴールとすることで、バグシナリオにつながる初期ステートの近接度が大幅に改善できた
6. 制約の完全性
   AXI インタフェースに接続するためプロトコルライブラリのアサーションを制約として使用した。DUT には 5 つの AXI インタフェースが存在するが、複雑さを軽減し、全てのトランザクションを 1 つのインタフェースに集中させるため、初期状態および改善状態では 4 つを無効化した。最初は過制約だったが、その後、さまざまなインタフェース間の相互作用を調べるために、徐々にすべてのインタフェースを有効化した

ケース 2：メモリコントローラ

メモリコントローラ内の読み書きの再順序付けの問題がポストシリコンバグとして発覚した。メモリコントローラー内の制御ロジックによってトランザクションの読み書きが再順序付けされる際に、該当するアドレスのデータが更新される前に古いデータが読み出されていた。この問題にはインタフェース制御ユニット、バッファユニット、メモリコントローラの３つのサブブロックが関与している。シリコン上での平均故障間隔(MTBF)は 2 時間〜8 時間であり、ダイナミックシミュレーションで障害を再現することは極めて困難である。そこでフォーマル検証によるバグハントプロセスを適用し、バグの特定と改修を試みた。ここではフェーズ１、２、３に分けて、図 4.に示すレーダーチャートの６つの要素の詳細を説明する。

フェーズ１（初期） - 理解とキャプチャ

1. デザインの複雑度
   実機でポストシリコンテスト中にフェイルするシナリオを観察し、バグトリアージによってメモリコントローラが問題の原因として特定できた
2. エキスパートの確保
   チームにフォーマル検証のエキスパートがいたことは幸いであり、彼らはフォーマル検証によるバグハントプロセスを適用するため、早期から関与していた
3. フォーマルエンジンの制御性
   メモリとデザインの不要な部分はブラックボックス化し、フォーマルエンジンがデザインを適切に探索できることを確認するために、予備的なフォーマル検証を実施した
4. アサーションの品質
   フェイルするシナリオを捉えるためにアサーションを作成され、バグにつながるイベントの組み合わせを観測するために、多くのカバープロパティも追加した。並行して機能シミュレーションでもプロパティのカバレッジをトリガーとしてバグを再現しようとしたが、実機で観測されたイベントの組合せを再現することはできなかった
5. 初期ステートの近接度
   実機での MTBF は少なくとも 2 時間だったが、フェイルを再現するための重要なイベントのシーケンスを理解でき、それをフォーマル検証の初期ステートとして利用した
6. 制約の完全性
   すべてのシナリオを探索し、フォーマル検証がバグにつながるイベントの組み合わせを見つけられるように、意図的にすべてのインタフェースを無制約に設定した

フェーズ２（改善） - 抽象化とアサーション

1. デザインの複雑度
   メモリコントローラとそのサブブロックの機能に焦点を当て、無関係なサブブロックを排除した
2. エキスパートの確保
   このフェーズは関係なし
3. フォーマルエンジンの制御性
   フォーマル検証アルゴリズムが様々なコンフィギュレーションレジスタやカウンタを制御できるように、カットポイントを追加した。さらに一部のステートマシンにもカットポイントを追加したが、その必要性は結果的には無かった
4. アサーションの品質
   これはバグハントの最重要項目だった。シミュレーションではバグにつながるバスのイベントは部分的にしかヒットしなかったので、バグの前提条件を理解するために多数のアサーションを作成した。フォーマル検証では前提条件の85%に達し、改善を繰り返しながら、トランザクションの適切なタイミングと外部トリガでバグを見つけることができた。ただイベントのシーケンスは、ポストシリコンで観察したものとは正確には一致せず、バグには複数の原因があったかという疑問が残った
5. 初期ステートの近接度
   プロジェクトチームは実機でシリコンのテストを継続し、可能な限りソフトウェアを修正した結果、シリコンのバグシナリオに近い初期ステートを特定できた
6. 制約の完全性
   フォーマル検証によりシリコンバグが制約のない環境で特定できた後、反例を精緻化するために、インタフェースの制約、セットアップおよびコンフィギュレーション制約をフォーマル実行に追加した。これは過度に制約されないよう慎重に行われた

フェーズ３（終了） - バグの特定、影響および修正

1. デザインの複雑度
   バグの複数シナリオを探索するため、複数のサブブロックをフォーマル検証に追加した。このアプローチによりフォーマル検証の複雑さは増したが、他の成功要因ですでに良い結果が得られていたので、心配の必要はなかった
2. エキスパートの確保
   このフェーズは関係なし
3. フォーマルエンジンの制御性
   アサーションの 72％はフォーマル検証ツールの学習知識としてキャッシュされていた。適切なエンジンが選択され、その後のフォーマル検証の実行時間は以前より大幅に加速された
4. アサーションの品質
   バグには複数の原因があるとの疑問を解消するために、アサーションを改善し、シリコンで観測された正確なバグシナリオにつながるイベントの正確な組み合わせとシーケンスを特定できた。シリコンのバグは観測可能なシナリオの 1 つにすぎないという設計上の欠点を理解する教訓となった
5. 初期ステートの近接度
   いくつかの初期ステートからフォーマル検証を実行した後、バグが発生するコンフィギュレーションとバグが発生しないコンフィギュレーションを特定した。この情報からバグを回避するソフトウェア修正を検討した。さらにフォーマル検証を使用して、ソフトウェアの修正によりシリコンでバグが再発するのを防ぐのに十分であることを確認した
6. 制約の完全性
   このフェーズではすでに関係なし

バグの RTL 修正には、内部 IP と外部 IP が含まれていたため、長いプロセスとなった。幸いなことにすでに修正されたソフトウェアを利用できたため、設計チームは内部および外部 IP チームと密接に協力し、フォーマル検証のバグハントによって特定された複数のシナリオに対する確実な修正を特定するのに十分な時間があった。

ケース３：パケットスケジューラ

スパイラルリファインメント手法は、もともとシリコンのバグハントのために開発されたが、一部のユーザが経験を積むにつれて、IP ブロックの検証にも採用が広がった。これは特にシミュレーション環境がまだ準備できていないか、利用できない場合に有効である。

フォーマル検証を行うことで、チェックイン前にIPの品質を大幅に向上させることが可能である。スパイラルリファインメントプロセスの適用は、以下の 3 つのフェーズで構成される。

• フェーズ 1：初期：抽象化と到達可能性
• フェーズ 2：改善：証明とバグハント
• フェーズ 3：最終：カバレッジクロージャー

このケースでは、事前にプログラムされた調停スキームに基づいて、着信パケットを優先順位付けして転送するパケットスケジューラーの事例を扱う。

図 5 は、スパイラルリファインメント手法の 3 つのフェーズを示している。

フェーズ１（初期） - 抽象化と到達可能性

1. デザインの複雑度
   このデザインは深さと広がりの両面で複雑であり、フォーマル検証で直接扱うには非効率である、効率を向上させるために、以下の３点を削減した
   • A) チャネルの数とサイズ
   • B) パケットの長さ
   • C) 未処理トランザクションに対するバッファ量
   このデザインは非常にコンフィギュアブル（設定変更可能）であるため、それほど難しくはなく、また設計チームはシンプルで正確な設定を行うのを支援してくれた
2. エキスパートの確保
   社内のフォーマル検証のエキスパートが、デザイン抽象化プロセスの初期段階から参加した。彼らのSVA に関する知識とフォーマル検証に向けたコーディングの技術が、このプロジェクトの成否を左右する要因の一つとして認識されていた
3. フォーマルエンジンの制御性
   メモリとデザインの不要な部分をブラックボックス化し、フォーマルエンジンがデザインを十分に制御できることを確認するために、予備的なフォーマル検証を実行した
4. アサーション品質
   フォーマル検証のエキスパートは設計者と密に連携し、デザインの重要部分や故障シナリオの捕捉のためのアサーションを作成した。パケットのデータ整合性およびクレジットベースのスケジューリング方式に関しては、複雑なアサーションを記述し、さらに充分なアサーションカバレッジを確保するため、アサーション密度も測定した
5. 初期ステートの近接度
   既知の良好なシーケンスを初期ステートとして活用した。図 5 に示すように、これはすべてのフェーズにわたり一定に保たれた
6. 制約の完全性
   パケット転送プロトコル、AXI バスインタフェース、コンフィギュレーションおよびメモリインタフェースに対するアサーション IP は早期に開発されており、したがって図 5.のプロセスにおけるすべてのフェーズで一定に保たれた

フェーズ２（改善） - 証明とバグハント

1. デザインの複雑度
   実行するフォーマル検証でどこに焦点をあてるに応じてデザインの抽象化をカスタマイズし、デザインの複雑度をさらに低減した
2. エキスパートの確保
   社内のフォーマル検証のエキスパートに加えてツールベンダによる支援を受け、サーバーファーム環境においてフォーマル検証を複数コアに分割して実行した
3. フォーマルエンジンの制御性
   すべてのエンジンを用いてフォーマル検証を実行し証明および違反を探索し、すべての情報をキャッシュした。そして以下の４つの段階でマルチプロセッシングを多次元的に活用し、徹底的に効率化を努めた
   • A) オペレーションレベル
     コンフィギュレーションの組合せは数百に及ぶが、設計チームは 14 種類の代表的なコンフィギュレーションを特定し、これに対してフォーマル検証を実施した
   • B) デザインレベル
     異なる抽象度／コンフィギュレーションでフォーマル検証を実行した。例えば：
     • ・ バイパスモードや１つのチャンネル／ストリームなどに注力するように設定する
     • ・ FIFO などバッファリングの閾値を下げ早くデータ破損の仕組みをトリガさせる
     • ・ テスト固有のチャネルや機能に負荷を与えるよう制約を設定する
     • ・ 関係しないモジュールやインスタンスをブラックボックス化する
   • C) セッションレベル
     • ・ セッションごとに異なるターゲットと制約の複数の組合せを構成した
     • ・ ツールによりセッションのセットアップや監視は容易に行えた
   • D) エンジンレベル
     ツールはいくつかのエンジンをオーケストレーションし、マルチコアに対して自動的に起動し、すべての結果を１つのデータベースに集約してくれた。これは完全に自動で行われた
4. アサーションの品質
   ツールから得られるフィードバックをもとにエンジンの健全性や、現在アクティブな論理をフォーマル検証実行中にダイナミックに監視し、その結果からアサーションを追加、修正した。アサーションにデータ独立性や非決定性を加え、デザインの制御性とフォーマル検証の効率を上げる工夫をした
5. 初期ステートの近接度
   これについてはフェーズ１と同じ
6. 制約の健全性
   これについてはフェーズ１と同じ

フェーズ３（最終） - カバレッジ

フェーズ２で証明済みのプロパティを確認し、違反箇所をデバッグした後、この最終フェーズでは、それまで結論が得られなかったプロパティとフォーマルカバレッジに注力した。これは、フォーマルカバレッジのクローズ手法の一部である。

1. デザインの複雑度
   デザインの抽象化などはフェーズ２と同じものを活用した
2. エキスパートの確保
   フェーズ２と同じ
3. フォーマルエンジンの制御性
   フォーマルカバレッジに焦点を当てるよう、フォーマルエンジンのオーケストレーションを調整した。ここでもフェーズ 2 と同様に、4 つのレベルのマルチプロセッシングを活用することで、可能な限り効率化した
4. アサーションの品質
   フォーマルカバレッジは、どこに焦点をあてどの精度が求められるか等の要件に応じて、さまざまな方法で測定した。フォーマルカバレッジには、いくつかの異なる測定方法が存在する。
   • A) 機能カバレッジ： assert、coverおよびcover binステートメントを使用する。バグを特定するだけでなく、その前提条件の活性化なども確認する
   • B) 構造的フォーマルカバレッジ
     • ・ プロパティの構造的影響範囲（COI: Cone of Influence）から算出する
     • ・ 広範囲なフォーマル解析を行う前に導出可能な概略的な解析を行う
     • ・ 初期段階でアサーションの抜けを特定し、必要なプロパティを追加するために利用できる
     • ・ ステートメント、ブランチ、FSM などのカバレッジ要素を対象にすることができる
   • C) 証明コアフォーマルカバレッジ
     • ・ フォーマルによって解析された構造から算出され、構造的 COI の部分集合にあたる
     • ・ 検証カバレッジのエンジンレベルの視点を提供する
     • ・ 後期段階のカバレッジクロージャのための検証指標をレポートする
     • ・ ステートメント、ブランチ、FSM などのカバレッジ要素を対象にすることができる
5. 初期ステートの近接度
   フェーズ 1 と同じ
6. 制約の完全性
   フェーズ 1 と同じ

フォーマルカバレッジという指標を用いることで、設計チームは、フォーマル検証がデザインのすべての機能検証全体で実行されたという十分な確信を得ることができた。

まとめ

フォーマル検証がシリコンにおけるバグハントに不可欠であることは実証されている。スパイラルリファインメントの手法およびレーダーチャートの活用は、非常にストレスが多く、かつ双方向的なプロセスに欠かせない指針を提供してくれる。この手法は成功要因を捉え、さまざまなアプローチを展開する上での助けとなる。事例でも示されているように、このプロセスでは障害要因を特定し、それぞれの成功要因を段階的に改善、洗練することで、シリコン上で発生したバグを正確に特定（ゼロイン）することを目的としている。
バグが特定されると、フォーマル検証環境は、潜在的なソフトウェア修正や RTL 修正を検証のためのゴールデンセットアップとして機能してくれる。この手法を用いることでターンアラウンドタイムを短縮し、劇的に効率を上げ、また副次的な問題の発生を防ぐ助けにもなる。
バグハントのみならず、IP の品質を上げるような場合には、フォーマル検証によるカバレッジクロージャに焦点を置いて実行することで、デザイン全体にわたってフォーマル検証を実施したのと等価の確信を得ることができる。
本稿で提示した手法を用いる上で、単に技術的な要素のみでなく、人的要因や組織の考察、外部コンサルティングの検討なども含む必要があることも付け加えておきたい。

参考文献

• [1] Ram Narayan, "The future of formal model checking is NOW!", DVCon 2014.
• [2] M Achutha KiranKumar et al., "Making Formal Property Verification Mainstream: An Intel® Graphics Experience," DVCon India 2017
• [3] Mandar Munishwar, Vigyan Singhal, et al., "Architectural Formal Verification of System-Level Deadlocks," DVCon 2018.
• [4] Richard Ho, et al., "Post-Silicon Debug Using Formal Verification Waypoints," DVCon 2009
• [5] Blaine Hsieh, et al., "Every Cloud - Post-Silicon Bug Spurs Formal Verification Adoption," DVCon 2015
• [6] Jin Hou et al., "Handling Inconclusive Assertions in Formal Verification," DVCon China 2018
• [7] Mark Eslinger, Ping Yeung., "Formal Bug Hunting with "River Fishing" Techniques," DVCon 2019
• [8] Jeremy Levitt et al., "It's Been 24 Hours - Should I Kill My Formal Run?", Workshop, DVCon 2019
• [9] Abhishek Anand et al., "Bounded Proof Sign-off with Formal Coverage," DVCon 2020
• [10] Ping Yeung, Mark Eslinger, and Jin Hou, Siemens EDA White Paper “Formal Verification Experiences”, 2021