フォーマル検証（formal verification）は，設計の仕様と，設計結果の回路をそれぞれ数学的に解析することで，回路の正しさを検証する手法である。論理シミュレータのように回路を疑似的に動作させて検証するのではなく，回路そのものを解析する。従って，シミュレーション・パターンの作成が不要で，かつ高速・網羅的に検証できるというメリットがある。
仕様と設計結果を比較
フォーマル検証には，大きく2種類ある。一つは「プロパティ・チェッキング（property checking）」であり，もう一つは「等価性検証（equivalency checking）」である。なお，プロパティ・チェッキングは「モデル・チェッキング（model checking）」とも呼ばれる。
前者のプロパティ・チェッキングは，回路が設計仕様（プロパティ）を満たしているかどうかを検証する1）。ここでプロパティとは，例えば，「ノードAとノードBは同時には論理値“1”にならない」とか「ready信号が“1”になるまでデータ信号が入力されない」，「ある回路がデッド・ロックになることはない」といったものである。プロパティ・チェッキングは，定義したプロパティについては網羅的に検証を行うが，プロパティの指定がない部分については検証されない点に注意が必要である。
標準的なプロパティは，あらかじめツールに組み込まれているが，設計に依存したプロパティは，設計者が明示的に定義する必要がある。しかし，漏れなくプロパティを定義することは困難であるため，論理シミュレーションを補完する技術として使う。
二つの回路の論理等価性を見る
一方，後者の等価性検証は，二つ（以上）の回路が論理的に等価かどうかをチェックする。等価性検証はさらに2種類あり，（1）レジスタで回路を分割した組み合わせ回路を対象とするものと，（2）順序回路も検証可能な「シーケンシャル等価性検証」と呼ばれるものである。シーケンシャル等価性検証は，最近，実用化が進んできた。
前者の「組み合わせ回路を対象にした等価性検証」では，例えば，RTLを人手で修正した場合に変更前後の回路を比較する。また，論理合成ツールに入力する前のRTL記述と，出力結果のゲート・レベル・ネットリストの比較に使う。さらに，タイミングやチップ面積を微調整するために人手で設計変更した回路と，合成ツールが生成したままの回路を比較するような場合にも利用される。
一方で後者の「シーケンシャル等価性検証」は，リタイミング，クロック・ゲーティング，パイプラインの変更といった，順序回路の変更を含む最適化の前後や，動作合成前後での動作記述とRTLの検証に利用できる。なお，動作合成の前後で，動作記述のように時間概念のない設計仕様とRTLを比較する時には，比較するタイミングを，スループットやレイテンシを使って指定する必要がある。
動作レベルも扱えるように
検証対象となる設計の抽象レベルは，プロパティ・チェッキングは主にRTLである（図1）。これに対して，等価性検証は，主にRTLやゲート・レベル，トランジスタ・レベルが多い。どちらも，最近，動作レベルを扱える市販ツールが登場してきた。なお，プロパティを記述するには，PSL（Property Specification Language）やSVA（SystemVerilog Assertion)といった言語が使われる。また市販ツールでは，不一致が見つかった場合のデバグ作業を支援するために，反例を示すテストベンチを生成したり，不一致の原因となる部分回路を表示するといった機能を備えている。
【図1 LSI設計工程と検証手段】出典はNECエレクトロニクス。 （画像のクリックで拡大）
大規模回路対応が課題
フォーマル検証の最大の課題は，大規模回路への対応である。特に，順序回路を扱う，プロパティ・チェッキングやシーケンシャル等価性検証は，検証できる回路規模が小さい。組み合わせ回路を対象とした等価性検証であっても，大規模な演算回路では，階層的に検証するなどの工夫が必要である。
また，運用面でも注意が要る。プロパティ・チェッキングの有効利用にはプロパティ記述方法などのノウハウが必要であり，プロパティ自身の正しさの確認方法も含めて課題は多い。等価性検証においては，どういう状態が等価であるかを定義した上で，必要に応じて機能・タイミング等の差分を補完する方法を検討する必要がある。さらに，補完部分の正しさを確認する手段の検討が必要となる。
変数を増やせる新手法が登場
次に，フォーマル検証の基盤技術を説明する。フォーマル・ベリフィケーションにはさまざまな実現手段がある2）。その中で，順序付き二分決定グラフ(OBDD：ordered binary decision diagram)を利用する方法が広く使われている。
OBDDはブール式をグラフで表現する。同一の論理機能は，変形を繰り返していけば，同一形状のグラフ（これを既約順序付き二分決定グラフ（ROBDD：reduced ordered binary decision diagram）と言う）に落ち着くという性質を利用する。
例えば，図2のようにハードウエア記述言語で記述した設計仕様と，設計した回路が論理的に等しいかを比較する。それぞれをブール式に変換し，さらにOBDDで表現する。OBDDの形状を比較することで，同一かどうかを判定する。
【図2 フォーマル検証手法の例】OBDD（ordered binary decision diagram）を利用している。出典はNECエレクトロニクス。 （画像のクリックで拡大）
最近，形式検証に関する基盤技術として，SAT手法（satisfiability, 論理関数の充足可能性判定手法)の研究が急速に進んでいる3)。SAT手法では，論理式を積和形（conjunctive normal form：CNF）で表現し，その論理式全体を1とするような変数値の組み合わせが存在するか否かを判定する。
OBDDでは，論理式を満たす変数の組み合わせをすべて考慮しているのに対して，SAT手法では解が一つでも存在するかどうかを探索する。このため，扱える論理変数の数を飛躍的に増やすことができる。
参考文献
1）平石，藤田ほか「特集：論理設計の形式的検証」，『情報処理』，vol.35，no.8，pp.708-749，1994年8月.
2）若林，向山，藤田，田中，山際，菅波「CADの取り組み／検証技術の高速化」，『日経BP最新ASIC設計術1994』，pp.126-130，1993年7月.
3）藤田，「システムLSI検証技術入門 第19回」，『Design Wave Magazine』pp151-156，2007年2月.
