フォーマル・べリファイア(formal verifier)は,設計結果の回路を数学的に解析することで,その結果を検証するツール。シミュレータのように設計結果の回路を疑似的に動作させて検証するのではなく,設計結果そのものを解析する。この意味では,スタティック・タイミング・アナライザもフォーマル・ベリファイアの仲間といえる。

 ただし,現在EDAの世界で,フォーマル・ベリファイアといえば,論理機能を検証するために,設計結果そのものを数学的に解析するツールを指している。フォーマル・ベリファイアの一番のメリットは,その定義にあるように,シミュレーション・パターンが必要ない点である。作成する手間が省けるうえ,検証に漏れがない。しかし,後述するようにどんな場合でも有効というわけではない。

2つの種類がある

 現在,フォーマル・ベリファイアと呼ばれている市販ツールは2種類ある。仕様検証(property checking)注1)するためのツールと等価性検証(equivalency checking)するためのツールである。

 前者は,設計した論理回路が設計仕様(property)を満たしているかどうかを検証する1)。ここでpropertyとは,例えば「ノードAとノードBは同時には論理値“1”にならない」とか,「ready信号が“1”になるまでデータ信号が入力されない」「ある回路がデッド・ロックになることはない」といったものだ。

 一方,後者のequivalency checkingのツールは,2つの論理が等しいかどうか検証する。

 例えばRTL(register transfer level)を手修正した場合の変更前後を比較したり,論理合成ツールに入力する前のRTL記述と出力結果のゲートレベル論理回路(ネットリスト)を比較する。また,タイミングやチップ面積を微調整するために,論理機能が変わらないように人手設計変更した回路と,合成ツールが生成したままの回路を比較するような場合に使う。従来の設計フローでは,些細な回路変更に対し,繰り返しシミュレーションしていた部分を高速に検証できる利点がある。

 ただし,equivalency checkingで分かることは,2つの回路が等しいかどうかだけで,設計者の意図したとおりの論理機能が実現できたかどうかはわからない。これを確かめるには,たとえば,シミュレーションやproperty checkingが必要である。

市販ツールも実設計適用レベルへ

 フォーマル・ベリファイアの研究は1970年代から大学などの研究機関で始まり,1980年代後半からコンピュータ・メーカーなどが自社で開発,製品設計に適用してきた。1990年代の半ばになって,equivalency checking向けの市販ツールが登場,1990年代の後半になって,property checking向けのツールも発表されている。また,property checking技術を利用し,あらかじめ決められた検証項目(例えば,one-hotエンコーダで複数の制御信号が“1”になっていないかをチェックするなど)を検証するツールも登場している。equivalency checkingでは,100万ゲートを超えるゲート・レベルの回路を1時間以内に検証可能となっており,実用レベルに達してきた。一方,property checkingは,シミュレータに比べて扱える規模が小さく,また有効利用にはproperty記述(HDLのような標準記述は存在しない)方法などのノウハウが必要であり課題は多い。検証対象となる設計レベルは,equivalency checkingがRTL,ゲート・レベル,トランジスタ・レベルの各レベルなのに対し,property checkingは主にRTLである。


グラフ理論の技術を利用

 フォ−マル・ベリファイアにはさまざまな実現手段がある2)。その中で,順序付き二分決定グラフ(OBDD:ordered binary decision diagram)を利用する方法が広く使われている。

 OBDDはブール式をグラフ(注:グラフ理論のグラフ,折れ線グラフとか棒グラフではない)で表現する。同一の論理機能は,変形していけば,同一形状のグラフ(これを既約順序付き二分決定グラフ(ROBDD:reduced ordered binary decision diagram)という)に落ち着くという性質を利用する。

 例えば,のようにハードウエア記述言語で記述した設計仕様と,設計結果の回路が論理的に等しいかを比較する。それぞれをブール式に変換し,その後OBDDで表現する。OBDDの形状を比較して同一かどうか判定する。

 OBDDを利用したフォーマル・ベリファイアの場合,論理が不一致と判定すると,それを確認するためのシミュレーション・パターンを生成する。すなわち,このパターンを双方の回路に入力すると,異なる出力パターンが出てくる。いくつかの製品では,異なる部分(回路図やHDL記述)を明示することができる。

注1)property checkingはmodel checkingとも呼ばれる。


(99. 9. 6更新)

参考文献

1)平石,藤田ほか「特集:論理設計の形式的検証」,『情報処理』,vol.35,no.8,pp.708-749,1994年8月.

2)若林,向山,藤田,田中,山際,菅波「CADの取り組み/検証技術の高速化」,『日経BP最新ASIC設計術'94』,pp.126-130,1993年7月.

このEDA用語辞典は,日経エレクトロニクス,1996年10月14日号,no.673に掲載した「EDAツール辞典(NEC著)」を改訂・増補したものです。