(57)【要約】    【課題】  イメージ及び前イメージ計算のための改良された方法、及び探索空間をプルーニングするための改良された方法を提供する。    【解決手段】  システムに関するイメージ又は前イメージ計算を実行する方法は、有限状態モデルによってシステムを表現するステップ、二分決定グラフ（BDD）を使用して状態集合を表現するステップ、満足化可能性検査（SAT）に基づく探索アルゴリズムを実行するステップを備え、SATが解空間全体の探索を副問題に分割し、当該解空間に存在する複数の解を列挙することにより各副問題を解決するために、BDDに基づくイメージ計算が使用され、またSAT手順において探索空間をプルーニングする方法は、所定のBDDの集合における暗黙の論理和又は論理積に対してBDD束縛を使用するステップ、変数の部分割り当てが暗黙の論理和又は論理積を満足する場合は探索を続行するステップ、及び変数の部分割り当てが暗黙の論理和又は論理積を満足しない場合はバックトラッキングを実行するステップを備える。【選択図】    図１
2004288204.tif 000002
【特許請求の範囲】
【請求項１】
ブール満足化可能性検査手順において探索空間をプルーニングするためのプルーニング方法であって、
所定の二分決定グラフの集合における論理和又は論理積に対して二分決定グラフ束縛手法を使用するステップ、
変数の部分割り当てが前記論理和又は論理積を満足する場合は探索を続行するステップ、
変数の部分割り当てが前記論理和又は論理積を満足しない場合はバックトラッキングを実行するステップを備えることを特徴とするプルーニング方法。
【請求項２】
前記論理和を処理するために単一の二分決定グラフに対する二分決定グラフ束縛手法が複数回使用され、変数の部分割り当てが所定の集合におけるいずれかの二分決定グラフを満足する場合にのみ探索を続行するステップ、
前記論理積を処理するために複数の二分決定グラフに対する二分決定グラフ束縛手法を用いるステップを備えることを特徴とする請求項１に記載のプルーニング方法。
【請求項３】
単一の二分決定グラフに対する前記二分決定グラフ束縛手順において、
リスト内の割り当て済み変数の値を設定し、二分決定グラフ内に前記値に基づく「１つの」ノードへの経路が二分決定グラフ内に存在する場合は、部分割り当てが二分決定グラフを満足すると判定することを特徴とする請求項２に記載のプルーニング方法。
【請求項４】
複数の二分決定グラフに対する前記二分決定グラフ束縛手順において、
リスト内の割り当て済み変数の値を設定し、前記値に従ってロックステップ方式で複数の二分決定グラフを走査し、前記二分決定グラフのロックステップ走査内に「１つの」ノードに至る経路が存在する場合は、部分割り当てが論理積を満足すると判定することを特徴とする請求項２に記載のプルーニング方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、イメージ及び前イメージ計算に関し、特に、二分決定グラフ（BDD：Binary Decision Diagram）に基づく手法と満足化可能性試験（SAT：Satisfiability Testing）に基づく手法を結合して、その相補的な利点を活用する手法に関する。
【背景技術】
【０００２】
イメージ及び前イメージ計算は、超大規模集積回路（VLSI：Very Large Scale Integrated Circuit）コンピューター支援設計（CAD：Computer Aided Design）の検証、合成、試験など多数のアプリケーションの中核を成す記号状態空間走査において、中心的な役割を果たす。本開示では逐次システム検証のための精密な到達可能性解析を中心に述べるが、この手法は、精密不変検査、精密モデル検査、近似到達可能性解析、近似不変検査、及び近似モデル検査にも適用できる。ここでは、説明を簡素化し理解しやすくするためにイメージ計算についてのみ考察するが、提示する手法は前イメージ計算にも同様に適用できることに留意されたい。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
BDDに基づく方法
記号状態空間走査に基づく検証手法は、ブール関係における入力集合のイメージを計算するためのBDDに基づく有効アルゴリズムを使用する。記号状態空間走査の詳細については、J.R.Burch,E.M.Clarke,D.E.Long,K.L.McMillan,and D.L.Dill; and Symbolic model checking for sequential circuit verification（逐次回路検査のための記号モデル検査）. IEEE Transactions on Computer-Aided Design（コンピューター支援設計に関するIEEE報告書）,13（4）:401-424,April 1994、及び0.Coudert,C.Berthet,and J.C.Madre. Verification of synchronous sequential machines using symbolic execution（シンボリック実行を使用した同期順序機械の検証）. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems（有限状態システムのための自動検証方法に関する国際ワークショップ講演集所収）, Volume 407 of Lecture Notes in Computer Science（コンピューター・サイエンスの講義ノート第４０７巻）, pages 365-373,June 1989を参照のこと。BDDに関する詳細については、R.E.Bryant.Graph-based algorithms for Boolean function manipulation（ブール関数処理のためのグラフ・ベース・アルゴリズム）.IEEE Transactions on Computers（コンピューターに関するIEEE報告書）,C35（8）:677-691,August 1986を参照のこと。
【０００４】
検証問題のための入力集合とは、現在の状態Pである。また、ブール関係とは、遷移関係T、すなわち現在の状態と次の状態との有効な組み合わせである。ハードウェアの場合は、Ｔの定義に一次入力を組み込むと更に便利である。関係の特性関数、入力、及びイメージ集合を使用してBDDを表現すると、イメージ計算をブール演算と変数定量化によって効率的に実行することができる。用途の一例としては、到達可能な状態の集合の計算が挙げられる。この計算は、システムの初期状態を示す集合Ｐから開始し、イメージ計算を不動点に到達するまで反復することによって実行される。
【０００５】
これまで多数の研究者が、分割遷移関係の使用を提唱してきた。これらの手法では、遷移関係全体に関するBDDは演繹的に作成されない。J.R.Burch,E.M.Clarke,and D.E.Long. Representing circuits more efficiently in symbolic model checking（記号モデル検査における効率的な回路表現）, In Proceedings of the 28th Design Automation Conference（第２８回設計自動化会議講演集所収）, pages 403-407, June 1991、及びH.J.Touati, H.Savoj, B.Lin, R.K.Brayton, and A.Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDDs（BDDを使用した有限状態機械の間接的状態列挙）. In Proceedings of the International Conference on Computer-Aided Design（コンピューター支援設計に関する国際会議講演集所収）, pages 130-133,1990.
通常、区画は複数のBDDを使用して表現され、その論理積がイメージ計算時に初期変数定量化とインターリーブされる。これまで、良好な定量化スケジュールを検出するための発見的手法は多数提唱されている。定量化スケジュールとはすなわち、ピーク変数の数が最小になる論理積の順序付けである。詳細については、D.Geist and I.Beer. Efficient model checking by automatic ordering of transition relation partitions（遷移関係区画の自動順序付けによる効率的なモデル検査）, in Proceedings of the Internation Conference on Computer-Aided Verification（コンピューター支援検証に関する国際会議講演集所収）, Volume 818 of Lecture Notes in Computer Science（コンピューター・サイエンス講義ノート第８１８巻）, pages 299-310,1994、及びR.K.Ranjan, A.Aziz, R.K.Brayton, B.F.Plessier, and C.Pixley.Efficient BDD algorithms for ESM synthesis and verification （ＥＳＭ合成及び検証のための有効BDDアルゴリズム）, in International Workshop for Logic Synthesis（論理合成に関する国際ワークショップ）, May 1995. Lake Tahoe,CAを参照のこと。更に、イメージ計算を副問題に効果的に分割するための、遷移関係と状態集合の論理和区画の使用についても関心が払われてきた。詳細については、G.Cabodi, P.Camurati, and S.Quer. Improving the efficiency of BDD-based operators by means of partitioning（分割によるＢＤＤベース演算子の効率向上）, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（集積回路及びシステムのコンピューター支援設計に関するＩＥＥＥ報告書）, 18（5）:545-556, May 1999, 1.-H.Moon, J.Kukula, K.Ravi, and F.Somenzi. To split or to conjoin: The question in image computation（イメージ計算における質問）, in Proceedings of the Design Automation Conference（設計自動化会議講演集所収）, pages 23-28,June 2000、及びA.Narayan, A.J.Isles, J.Jam, H.K.Brayton, and A.Sangiovanni-Vincentelhi. Reachability analysis using partitioned ROBDDs（分割されたROBDDを使用した到達可能性解析）, in Proceedings of the International Conference on Computer-Aided Design（コンピューター支援検証に関する国際会議講演集所収）, pages 388-393,1997を参照のこと。
【０００６】
重要なのは、BDDに基づく手法は、BDDを使用して状態の集合と遷移関係を表現できる場合には良好な結果をもたらすという事実である。この表現は、全体として使用することも、使いやすく区画に分割した形式で使用することもできる。ただし、BDDのサイズは、変数の数、変数の順序、表現される論理式の性質などの様々な要因によって大きく左右される。従来から多数の研究がなされてきたが、純粋にBDD手法に基づく検証手法は、現実的なサイズ及び機能を持つ設計に使用するには信頼性が低すぎる。
【０００７】
BDDベースの方法とSATベースの方法の結合
一方、試験用途で広く使用されている代替手法は、論理積正規形（CNF：Conjunctive Normal Form）を使用して遷移関係を表現し、さらには、ブール満足化可能性検査（SAT：Boolean Satisfiability Checking）を使用して解析を実行する。詳細については、T.Larrabee., Test pattern generation using Boolean Satisfiability（ブール満足化可能性を使用した試験パターンの生成）, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（集積回路及びシステムのコンピューター支援設計に関するＩＥＥＥ報告書）,11（1）:4-15,January 1992を参照のこと。SATソルバー技術は近年大幅に改良されており、J.P.Marquez-SilvaのGrasp package, http://algos.inesc.pt/~jpms/software.htmlをはじめとする多数の高度パッケージが入手可能になっている。
【０００８】
所定の２つの組み合わせ回路C1及びC2の等価性を検査する場合には、対応する出力のXORの評価結果が決して１にならないことを証明する手法が広く普及している（図７）。対応する出力のXOR1は、「マイター回路出力」とも呼ばれる。上記の命題の証明は、マイター用のBDDを作成するか、あるいはそのマイター出力に関しては満足する割り当てがないことを証明するためのSATソルバーを使用することによって得られる。この２つの方法を個別に使用すると証明に失敗する場合には、例えば図７に示すようにBDDとSATを結合することもできる。マイター回路には、回路を２つの部分に分割する切断線が示されている。２つの部分とは、回路入力と切断線の間に位置する回路の部分PIと、切断線と出力の間に位置する回路の部分POである。POに関してはBDDが作成され、PIはCNFで表現される。SATソルバーはその後、PIに関するCNFを使用して、切断線での有効な組み合わせをすべて列挙するための処理を開始する。また同時に、POに関するBDDのon集合に有効な組み合わせが含まれていないことを確認するための検査も実行される。A.Gupta and P.Ashar. Integrating a Boolean Satisfiability checker and BDDs for combinational verification（組み合わせ検証のためのブール満足化可能性チェッカー及びBDD）.In Proceedings of the VLSI Design Conference（VLSI設計会議講演集所収）,January 1998を参照のこと。切断線における有効な組み合わせを列挙することは、PIに対応するブール関係における入力集合のイメージを計算することとまったく同じである。等価検査のためにBDDとSATを結合する方法は、その他にも提唱されている。 J.Burch and V.Singhal.Tight integration of combinational verification methods（組み合わせ検証方法の緊密な統合）. In Proceedings of the International Conference on Computer-Aided Design（コンピューター支援設計に関する国際会議講演集所収）,pages 570-576,1998を参照のこと。
【０００９】
特性検査については、有界モデル検査及び記号到達可能性解析の領域でも、SATソルバーがバグの検出に効果的であることが実証されている。P.A.Abdulla, P.Bjesse, and N.Een.Symbolic reachability analysis based on SAT-solvers（SATソルバーに基づく記号到達可能性解析）. In Tools and Algorithms for the Analysis and Construction of Systems （TACAS）（「システムの解析及び構築のためのツール及びアルゴリズム」所収）,2000、A. Biere, A.Cimatti, B.M.Clarke, and Y.Zhu.Symbolic model checking without BDDs（BDDを使用しない記号モデル検査）. In Tools and Algorithms for the Analysis and Construction of Systems （TACAS）（「システムの解析及び構築のためのツール及びアルゴリズム」所収）, Volume 1579 of Lecture Notes in Computer Science（コンピューター・サイエンス講義ノーと第１５７９巻）,1999、及びP.Williams, A.Biere, E.M.Clarke, and A.Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking（効率的な記号モデル検査のための決定図とSAT手順の組み合わせ）. In Proceedings of the Internation Conference on Computer-Aided Verification（コンピューター支援検証に関する国際会議講演集所収）, Volume 1855 of Lecture Notes in Computer Science（コンピューター・サイエンス講義ノート第１８５５巻）, pages 124-138,2000を参照のこと。これらの研究に共通するテーマは、命題の適切なブール式を作成することにより対象の問題をSAT問題に変換し、状態集合の他の非標準表現を利用することである。これらの研究者は、単一の満足するソリューションが存在する場合にそれを検出する手段として、SATソルバーの既知の機能を使用しているに過ぎない。つまり、すべての満足する問題を検出するためにSATソルバーが使用されるように問題を公式化することは、未だ試みられていないのである。
【００１０】
この点において、本発明の手法は、分解パラダイムを独立して公式化したMoon et al.とは区別されるべきである。I.-H.Moon, J.Kukula, K.Ravi, and F.Somenzi．To split or to conjoin: The question in image computation（分割するか、結合するか：イメージ計算における問題）. In Proceedings of the Design Automation Conference（設計自動化会議講演集所収）, pages 23-28, June 2000を参照のこと。本発明とこの研究との間には、細部において、「なぜSATなのか」のセクションで述べるような顕著な相違点がある。
【００１１】
次のサブセクションでは、標準的なSAT決定手順に必要とされる背景について述べる。
【００１２】
満足化可能性検査（SAT）
ブール満足化可能性（SAT）問題は制約条件満足問題として広く知られており、試験生成、論理検証、タイミング解析といったコンピューター支援設計において多数の用途を有する。ブール式が与えられた場合、その目的は、式の評価結果が真となる変数への0-1値の割り当てを検出するか、あるいはこうした割り当てが存在しないことを実証するかのいずれかである。ブール式は通常、論理積正規形（CNF：Conjunctive Normal Form）で表現される。これは、「和の積（product-of-sums）形」とも呼ばれる。CNFにおける和の項（句）は各々、単一リテラルの和である。リテラルとは、変数又はその否定である。n句とは、ｎ個のリテラルを有する句である。例えば、（vi+vj'+vk）は3句である。式全体の評価結果が1となるためには、各々の句が満足されること、すなわち評価結果が１になることが必要とされる。
【００１３】
この問題の複雑性は、NP完全であることが知られている。実際には、従来のほとんどのSATソルバーは、Davis-Putnamアルゴリズムをベースとしている。M.Davis and H.Putnam. A computing procedure for quantification theory（定量化理論に関する計算手順）. Journal of the ACM,7:201-205,1960を参照のこと。基本アルゴリズムは空の割り当てから開始し、自由変数に0又は1の値を１つずつ割り当てることによって進行する。各割り当ての後、アルゴリズムはその割り当ての他の変数に対する直接含意と推移含意を決定する。これは通常、「束縛」と呼ばれる。含意手順の実行時に矛盾が検出されなかった場合は、アルゴリズムは次の自由変数を選択し、同じ手順を繰り返す。矛盾が検出された場合は新たな部分割り当てを試みる。この部分割り当てでは、最も最近割り当てられた変数のうち、割り当てが１回しか試みられていないものを相補することにより行われる。このステップは、「バックトラッキング」と呼ばれる。アルゴリズムは、すべての句が満足されたか、解が検出されたか、あるいは可能な割り当てが尽きた時点に終了する。アルゴリズムは、解が存在する場合にそれを検出するという点において、完全である。
【００１４】
図８に、基本的なDavis-Putnam探索手順のための疑似コードを示す。関数名と変数名は、明白な意味を持つ。この手順は、Implications（）、Bound()、Backtrack()、Next_free_var（）、及びVal（）の各関数を増強することにより、長年をかけて改良されてきた。GRASPの研究では、コンフリクト解析による非発生順のバックトラッキングを使用すること、そして将来に同じ矛盾を繰り返すのを回避するためにコンフリクト句をデータベースに追加することを提唱した。 J.P.Marques-Silva and K.A.Sakallah. Grasp: A new search algorithm for satisfiability（Grasp：満足化可能性のための新規探索アルゴリズム）. In Proceedings of the International Conference on Computer-Aided Design（コンピューター支援設計に関する国際会議講演集所収）, pages 220-227, November 1996を参照のこと。
【００１５】
本発明の第１の目的は、上記従来技術の欠点を解決し、イメージ及び前イメージ計算のための改良された方法を提供することである。
【００１６】
本発明の第２の目的は、上記従来技術の欠点を解決し、探索空間をプルーニングするための改良された方法を提供することである。
【課題を解決するための手段】
【００１７】
上記目的を達成するため本発明のプルーニング方法は、ブール満足化可能性検査手順において探索空間をプルーニングするためのプルーニング方法であって、所定の二分決定グラフの集合における論理和又は論理積に対して二分決定グラフ束縛手法を使用するステップ、変数の部分割り当てが前記論理和又は論理積を満足する場合は探索を続行するステップ、変数の部分割り当てが前記論理和又は論理積を満足しない場合はバックトラッキングを実行するステップを備えることを特徴とする。
【００１８】
請求項２の本発明のプルーニング方法は、前記論理和を処理するために単一の二分決定グラフに対する二分決定グラフ束縛手法が複数回使用され、変数の部分割り当てが所定の集合におけるいずれかの二分決定グラフを満足する場合にのみ探索を続行するステップ、前記論理積を処理するために複数の二分決定グラフに対する二分決定グラフ束縛手法を用いるステップを備えることを特徴とする。
【００１９】
請求項３の本発明のプルーニング方法は、単一の二分決定グラフに対する前記二分決定グラフ束縛手順において、リスト内の割り当て済み変数の値を設定し、二分決定グラフ内に前記値に基づく「１つの」ノードへの経路が二分決定グラフ内に存在する場合は、部分割り当てが二分決定グラフを満足すると判定することを特徴とする。
【００２０】
請求項４の本発明のプルーニング方法は、複数の二分決定グラフに対する前記二分決定グラフ束縛手順において、リスト内の割り当て済み変数の値を設定し、前記値に従ってロックステップ方式で複数の二分決定グラフを走査し、前記二分決定グラフのロックステップ走査内に「１つの」ノードに至る経路が存在する場合は、部分割り当てが論理積を満足すると判定することを特徴とする。
【００２１】
本発明のイメージ計算手法では、状態集合はBDDを使用して表現され、遷移関係はCNF論理式を使用して表現される。次の状態の有効な組み合わせが、SATのためのバックトラッキング探索アルゴリズムを使用してすべて列挙される。このアルゴリズムは、一次入力、現在の状態変数、及び次の状態変数の全空間をしらみ潰しに探索する。ただし、SATを使用してリーフまでに存在するすべての解を列挙するのではなく、SAT決定手順の中間地点でBDDに基づくイメージ計算が呼び出され、これにより探索ツリーのその地点より下のすべての解が効果的に取得される。本発明の手法は、イメージ計算を多数の副問題に分解する論理和分解を提供するSATとみなすことができる。各副問題は、BDDを使用して処理される。
【００２２】
本発明の目的を実現するため、システムに関するイメージ計算を実行する方法が提供され、前記方法は有限状態モデルによってシステムを表現するステップ、二分決定グラフ（BDD）を使用して状態集合を表現するステップ、満足化可能性検査（SAT）に基づくバックトラック探索アルゴリズムを実行するステップを備え、SATが解空間全体の探索を副問題に分割し、解空間に存在する複数の解を列挙することにより各副問題を解決するために、BDDに基づくイメージ計算が使用される。
【００２３】
この方法は、到達可能性解析、不変検査、又はモデル検査を精密又は近似に実行するために使用されるのが望ましい。
【００２４】
前記有限状態モデルの遷移関係は、論理積正規形（CNF）を使用して表現するのが望ましい。
【００２５】
探索アルゴリズム内のケア集合として、動的に変化するイメージの補集合が使用されるのが望ましい。
【００２６】
SATにおける探索は、変数への部分割り当てが暗黙の論理和又は論理積を満足する場合は探索が続行され、満足されない場合はバックトラッキングするように、BDDの所定の集合における暗黙の論理和又は論理積に対してBDD束縛を行うことによってプルーニングされ、前記BDD束縛は、入力集合を表現するBDDの暗黙の論理和に対して前記BDD束縛を適用するとともに、イメージ集合のためのケア集合を表現するBDDの暗黙の論理積に対して前記BDD束縛を適用することによって更に完遂されるのが望ましい。
【００２７】
SATにおける論理和分解は、変数が出現する句の数などのSATに基づく発見的手法と、変数に関して余因子化された入力集合とケア集合BDDのサイズなどのBDDに基づく発見的手法によって選択された決定変数に対して、値を割り当てることにより完遂されるのが望ましい。
【００２８】
SATにおける論理和分解の程度は、適応可能であるのが望ましい。
【００２９】
BDDに基づくイメージ計算手順は、以下のステップによって複数の解を決定するのが更に望ましい。すなわち、CNF表現内の満足されない句の各々に関するBDDから成るBDDの集合を作成するステップ。入力集合BDDを前記BDDの集合に追加するステップ。変数の部分割り当てをBDD上に投影するステップ。定量化の対象として最小コストの変数を選択するステップであって、前記選択は、（１）前記BDDの集合の部分集合に含まれるBDDのサイズであって、選択された変数が前記部分集合の各BDD内に出現するサイズ、（２）前記部分集合に含まれるBDDの積のサイズの推定値、（３）前記部分集合に含まれるBDDの変数サポート集合のサイズ、及び（４）定量化が可能な変数の数、に応じたコスト関数によって決定される。部分集合におけるすべてのBDDの論理積と、選択された変数、並びにBDDの集合内の残存BDDに出現しないその他すべての定量化すべき変数の定量化とを同時に実行するステップであって、残存BDDは、前記BDDの集合から除去された前記部分集合である。
【００３０】
BDDの部分集合を、直前のステップで実行された論理積と定量化の結果に置換するステップ。最小コスト変数を選択するステップを反復するステップ。論理積と定量化を同時に実行し、定量化すべき変数が尽きるまで置換を実行するステップ。及び、集合内の残存BDDと、次の状態変数の部分割り当てを表現するBDDとの論理積を実行するステップ。
【００３１】
BDDに基づく副問題は、割り当てられない変数の数、割り当て済み変数を投影した後の束縛BDDのサイズに応じたコスト関数に基づいて開始されるのが更に望ましい。
【００３２】
BDDに基づく副問題の開始後も資源の限界を事由としてそれを中止でき、中止された場合は、SATを使用して問題が更に分解されるのが更に望ましい。
【００３３】
本発明の他の態様は、イメージ計算ではなく前イメージ計算に対して上記方法を使用することである。
【００３４】
本発明の更に他の態様は、SAT手順において探索空間をプルーニングする方法であって、前記方法は、所定のBDDの集合における暗黙の論理和又は論理積に対してBDD束縛を使用するステップ、変数の部分割り当てが暗黙の論理和又は論理積を満足する場合は探索を続行するステップ、及び変数の部分割り当てが暗黙の論理和又は論理積を満足しない場合はバックトラッキングを実行するステップを備える。
【００３５】
単一のBDDに対するBDD束縛は、前記論理和の処理のために複数回使用され、変数の部分割り当てが所定の集合内のBDDを満足する場合にのみ探索が続行され、複数のBDDに対するBDD束縛を使用して前記論理積が処理されるのが望ましい。
【００３６】
単一のBDDに対する前記BDD束縛手順は、リスト内の割り当て済み変数の値を設定し、BDD内に前記値に基づく「１つの」ノードへの経路がBDD内に存在する場合は、部分割り当てがBDDを満足すると判定することにより実行されるのが更に望ましい。
【００３７】
複数のBDDに対する前記BDD束縛手順は、リスト内の割り当て済み変数の値を設定し、前記値に従ってロックステップ方式で複数のBDDを走査し、前記BDDのロックステップ走査内に「１つの」ノードに至る経路が存在する場合は、部分割り当てが論理積を満足すると判定することにより実行されるのが更に望ましい。
【発明の効果】
【００３８】
本発明によれば、SATソルバーとBDDの双方の利点を結合し、かつ両者間の動的な対話を可能にするイメージ計算のための統合手法が提供される。更に、高細粒度のCNF式を使用することにより、BDD副問題の初期定量化の利点も実現される。これは、純粋なBDDベースの手法に適用することも可能である。
【実施例】
【００３９】
以下、本発明の実施の形態について図面を参照して詳細に説明する。
【００４０】
イメージ計算
次に、単一統合フレームワーク内でBDDに基づく手法とSATに基づく手法を結合してイメージ計算を実行するための本発明の手法の好適な実施例について説明する。本発明の手法の大部分は、特にイメージ計算での使用を目的とする。本発明の手法の特徴は、GRASPなどの最新鋭のSATアルゴリズムに見られる特徴と共通する部分が多く、事実これらの手法に追加されるものとみなすことができる。GRASPの詳細については、P.Marquez-Silva．Grasp package（GRASPパッケージ）（http://algos.inesc.pt/"jpms/software.html）を参照のこと。
【００４１】
表現フレームワーク
本発明で使用される表現フレームワークは、BDDを使用して入力集合とイメージ集合を表現し、CNF式を使用してブール関係を表現するステップを備える。このような表現方法を選択したのは、BDDに基づく方法は遷移関係に関するBDDをその全体であれ一部分であれ効果的に処理することができず、失敗に終わることが多いからである。更に、複雑なシステムの場合は入力集合とイメージ集合に関するBDDも大きくなるが、本発明の手法では単一のBDDを使用してこれらの集合を表現する必要はない。本発明の手法では、論理和的に分解されたBDDの集合に対しても十分な効果を発揮する。
【００４２】
この構成を、図１に示す。本発明の実施例では、単純な「発生順」論理和分割が使用される。そのため、蓄積中の集合に関するBDDのサイズがしきい値を超えると、その集合に対するその後の追加情報を格納するためのBDDが新規に作成される。ただし、本発明の精神と範囲から乖離することなく、これらの集合を管理するために代替の表現を使用できることは、当該技術に精通した当業者には明らかであろう。
【００４３】
CNF-BDDを使用したイメージ計算
下記方程式（1）に、標準的なイメージ計算式を示す。ここで、x、y、wはそれぞれ、現在の状態、次の状態、及び一次入力の変数の集合を表す。また、P（x）は入力集合、T（x、w、y）は遷移関係を表す。
【数１】
2004288204.tif 000003
【００４４】
好適な実施例を記述するために使用されるフレームワークでは、P（x）とImage（y）は（複数の）BDDとして表現され、Tは、x、w、y、及び回路の内部信号を表すその他の追加変数zを有するCNF式として表現される。イメージ集合は、CNF式Tのすべての解を列挙し、y変数の組み合わせだけを記録し、更にx変数の値をP（x）を満足するものだけに限定することによって計算される。x変数をP（x）を満足するものだけに限定することにより、上記の式で論理積が効果的に実行されるようになることに注意する必要がある。この限定は、BDD束縛によって実行される。基本的には、SAT探索手順の実行中には、BDD（s）P（x）のon集合に属さないx変数への部分割り当ては、直ちにプルーニングされる。 A.Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification（組み合わせ検証のためのブール満足化可能性チェッカーとBDDの統合）. In Proceedings of the VLSI Design Conference（VLSI設計会議講演集所収）, January 1998を参照のこと。また、CNF式の（単一ではなく）すべての解を列挙し、これらの解のうちy変数だけから成る組み合わせを考慮することにより、他の変数（x、w、z）に対する定量化が効果的に実行されることに注意する必要がある。
【００４５】
Unreached（y）は、イメージ集合のためのケア集合として使用される。イメージ計算が反復して実行される到達可能性解析などの用途では、この集合は到達された状態の現在の集合の否定として計算できる。ここでも、BDDを使用してUnreached（y）を表現しているために、このイメージ・ケア集合に対してBDD束縛を実行することによりSAT探索空間の追加のプルーニングを得ることが可能になる。要約すると、イメージ計算には以下の方程式が使用される。
【数２】
2004288204.tif 000004
【００４６】
BDD束縛
BDD束縛を実行するための簡単な手法としては、探索ツリーのリーフまでに存在する完全なSAT解をすべて列挙し、その後、各解が所定のBDDを満足するかどうか検査する方法がある。しかし、SAT解は夥しい数に上る可能性があるので、これは明らかに非効率的である。
【００４７】
本発明の構成では、x/y変数は入力／イメージ集合BDDとCNF式の間で共用される。そのため、SAT内のこれらの変数の１つに対して値が設定もしくは暗黙に定義されている場合は常に、部分割り当てと所定のBDDとの交点が非ヌルかどうかの判定が行われる。これが非ヌルの場合は、SAT手順の以降のステップが実行される。非ヌルでない場合は、このサブツリーの下に論理積と矛盾しない解が検出されないため、バックトラッキングが実行される。
【００４８】
本発明の発明者のうち数名が、初期束縛手法と呼ばれる類似の手法を使用したところ、探索ツリーの大きな部分空間をプルーニングにより除去したことによって、バックトラックの回数が大幅に減少したことが確認された。詳細については、A.Gupta and P.Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification（組み合わせ検証のためのブール満足化可能性チェッカーとBDDの統合）. In Proceedings of the VLSI Design Conference（VLSI設計会議講演集所収）, January 1998を参照のこと。ハウンディング集合が小さいほど、プルーニングは大きくなり、SATソルバーが高速化される可能性が高まることに注意する必要がある。
【００４９】
イメージ集合に対する束縛：良好なフィードバック効果
入力集合P（x）及びイメージ・ケア集合Unreached（y）に対する束縛に加えて、「Current（y）」と呼ばれる現在計算中のイメージ集合のBDDに対しても束縛を行うと、本発明のイメージ計算手順の根本的なスピードアップを実現することができる。単一イメージ計算中にUnreached（y）は変化しないが、Current（y）は、イメージ集合に関する新たな解が列挙するたびに動的に更新されることに注意する必要がある。そのため、y変数への部分割り当てがCurrent（y）に含まれている場合は、完全な割り当てに対する拡張部分はすでに列挙されていると考えられる。この場合はSATソルバーがそれ以上探索を行うことは無意味なので、バックトラックを開始できる。つまり、イメージ集合が大きくなるほど、SATソルバーが探索空間の残りの部分を処理する速度が高まり、良好なフィードバック効果が生まれるのである。
【００５０】
実装の細目：x 変数の束縛
P（x）に対するBDD束縛に関しては、図８のBound（）関数は、x変数に対する部分割り当てが、P（x）に関するBDDのon集合を満足しているかどうか検査するように修正されている。ここでも、部分割り当てが各BDDとの間にヌル交点を有している場合、SATソルバーは矛盾が存在しているかのごとくにバックトラックを開始する。
【００５１】
図２に、単一BDDのためのBound（）手順の疑似コードを示す。この手順では、初期引数はP（x）に関するBDDであり、再帰的引数は探索ツリーの下流でその投影バージョンを維持する。project_variable-in-bdd（）手順は、標準的なBDDパッケージに含まれているbdd_substitute（）演算かbdd_cofactor（）演算を使用することによって容易に実装できる。詳細については、F. Somenzi et al.CUDD: University of Colorado Decision Diagram Package（CUDD：コロラド大学決定ダイアグラム・パッケージ）.http://vlsi.colorado.edu/~fabio/CUDD/を参照のこと。ただし、これらの標準的なBDD演算は、ユニーク・テーブルとキャッシュのルックアップにおいてかなりのオーバーヘッドを要する。一方、本発明では、単純な関連表を使用してx変数の割り当てが記録される。変数の投影（投影解除）は、一定時間の演算によって、関連内に値を設定（設定解除）するだけで完遂できる。ただし、zero_bddに対する検査では、引数BDDの走査が必要とされる。これは、変数の関連付けにより決定される分岐を取ることで実行される。 one_bddへの経路が検出されると走査が終了され、そのBDDはzero_bddと等しくないことが証明される。これに要する時間は、ワースト・ケースではBDDのサイズに比例する時間となる。さらなる機能強化の手段として、各BDDノードについて、経路の有無を示す値がそのノードのone_bddに関連付けられる。そのためのビットの修正は、このノードの下流にある変数の値が修正された場合にのみ必要となる。その結果、空検査の複雑性の平均は、BDDサイズより良好になる可能性が高い（p.18）。
【００５２】
実装の細目：y変数の束縛
SAT探索時に、y変数に対する部分割り当てと（Unreached（y）∧!Current（y））との交点が非ヌルの場合は、探索を続行する必要がある。非ヌルでない場合は、バックトラックを開始できる。
【００５３】
前述したように、到達された状態集合R=UiRIに対しては、論理和分割の使用が可能である。そのため、Unreached集合と!Current集合のいずれも、BDDの積、すなわち、Unreached（y）=∩i!Ri（y）、及び!Current（y）=∩i!Currenti（y）として表現できる。最初に、複数BDDの明示の積を実行するのではなく、y変数に対する部分割り当てが各BDDに別個に投影される。続いて、この複数のBDDは修正済みのbdd_equal zero（）手順を使用してロックステップ方式で走査され、その積にone_bddに至る経路が存在するかどうかが決定される。この疑似コードを図３に示す。所定の手順においては、個々のBDDへの変数値の投影は実行済みであると想定される。実際の実装では、変数の投影と空状態の検出は、相補済みBDDノードの処理とともに、単一の経路において実行される。ワースト・ケースの複雑性は、完全積の実際の計算に伴う複雑性であるが、実際の処理では、この手順はone_bddへの経路が検出され次第終了する。
【００５４】
SATリーフのBDD
これまで、イメージ計算のための手法について、可能な限りBDD束縛を実行して探索空間をプルーニングしながら、SAT解決手法を使用してCNF式のすべての解を列挙することを中心に説明してきた。この方法にはまだ、純粋にSATに基づく手法（すなわち、解が１度に１つの割合で列挙され、再使用されない手法）が抱えるいくつかの欠点が残る。この欠点は、包含及びプルーニングを目的として部分解（キューブ）を検査することによってある程度は解消できる。しかし、実際には更に改良することが可能である。
【００５５】
この点については、純粋なSATベースの手法と純粋なBDDベースの手法を比較すると理解しやすくなる。本質的には、いずれの手法も同じブール変数の探索空間を対象として処理を行う。SATソルバーは明示的な決定ツリーを使用し、BDD演算はその基礎にあるDAG（Directed Acyclic Graphs：閉路なし有向グラフ）を対象とする。BDDベースの手法は、すべての解を同時に捕捉するのに適している。ただし、変数の順序づけの制約により、中間／最終結果においてサイズのブローアップ（爆発的な増大）が生じる恐れがある。一方、SAT決定ツリーには変数の順序付けの制約がないため、規模の大きな問題を扱いやすい。ただし、これは標準的なものではないので、多数の副問題の計算を繰り返し実行することになりがちである。
【００５６】
両手法がそれぞれ有する利点を組み合わせるため、本発明の手法はSAT決定ツリーを使用して最上位の探索空間を構成する。このツリーでは、任意の経路に沿って、SATソルバーを使用してツリーの探索を更に進めるのではなく、BDDベースの手法を起動し、その経路の下のサブツリーに存在するすべての解を計算する。図４に、「SATリーフのBDD（BDDs at SAT Leaves）」と呼ばれるこの統合方式を示す。ある意味では、SAT決定ツリーは「ルートの大きな問題をリーフの小さな副問題に論理和的に分割すること」ということができる。リーフの各々は、純粋にBDDに基づく手法によって処理できる。
【００５７】
リーフ副問題：BDDに基づくイメージ計算
SAT決定ツリーの各リーフで解決すべきBDD副問題の式を以下に示す。
【数３】
2004288204.tif 000005
【００５８】
これは、SAT決定ツリーのある経路の末端をルートとするサブツリーから、イメージ集合の解Newを計算する式である。ここで、変数vの集合については、割り当て済みの集合は「v'」として表され、割り当てられていない集合は「v"」として表される。Path（x’）/Path（y'）は、この経路に存在するx/y変数の部分割り当てを表現するBDDである。Unsat（x",w",z",y"）は、この経路の割り当て済み変数によって投影され、原始CNF式に出現する割り当てられない変数に関して表現された、この経路の末端に存在するすべての満足されない句の積である。最後に、P（X）|Path（x'）は、この経路の部分割り当てxに対する集合P（x）の制約を表す。
【００５９】
この方程式の存在定量化に続く部分は、式としては標準的な純粋にBDDベースの手法と同一であることに注意する必要がある。異なっているのは、ブール関係Unsatの細粒度とその論理積分解だけである。標準的な手法では、ブール関係T（x,w,y）は、現在の状態変数、一次入力変数、及び次の状態変数についてのみ表現された遷移関係である。また、その論理積分解は、通常、次の状態変数の分割に基づいて実行される。
【００６０】
本発明の手法では、ブール関係は、逐次回路の次の状態論理を実装する内部ゲート上の信号を表す現在の状態変数、一次入力変数、次の状態変数、及び中間変数の集合に関するCNF式として表現される。更に、論理積分解は、回路からゲートへの構造分解を辿る。このように、この手法は細粒度が高く、標準的な手法よりも多数のブール変数を処理しなければならないが、初期定量化の可能性が増大するという利点がある。初期定量化は、上記で指摘したように、イメージ計算時の爆発的な拡大の問題を克服する手段として有効である（これについては、次のセクションで詳述する）。
【００６１】
高細粒度のCNF区画を使用することのもう１つの利点は、前イメージ計算を実行することにペナルティがないことである。これまで多数の研究者が、逆方向の記号走査は順方向の走査ほど効率的ではないと指摘してきた。その１つの理由は、状態空間のほぼ例外なく不規則な到達不能部分を処理する必要があるためである。更に、ほとんどの方法は、現在の状態（x）変数を共用するとともに、次の状態（y）変数を分割することにより得られる区画を使用する。この方式はx変数の初期定量化を伴うイメージ計算を実行するには好都合だが、y変数を定量化する必要がある前イメージ計算の場合はうまく機能しない。これとは対照的に、高細粒度のCNF式を使用する本発明は、x変数とy変数に関して対称である。そのため、本発明の手法は、イメージ計算だけでなく、前イメージ計算にも同様に適用できる。
【００６２】
リーフ副問題：定量化スケジュール
実際の処理では、良好な定量化スケジュールを選択することが重要である。良好な定量化スケジュールとは、イメージ計算時に中間ブローアップを回避できるような、区画の論理積に対する順序付けである。良好なスケジュールは、典型的には、個々の区画の変数サポート集合を解析することにより、線形化スケジュールのアクティブな変数の数を最小限にとどめようとする。詳細については、D.Geist and I.Beer．Efficient model checking by automatic ordering of transition relation partitions（遷移関係区画の自動順序付けによる効率的なモデル検査）. In Proceedings of the Internation Conference on Computer-Aided Verification（コンピューター支援検証に関する国際会議講演集所収）, Volume 818 of Lecture Notes in Computer Science（コンピューター・サイエンス講義ノート第８１８巻）, pages 299-310,1994、I.-H.Moon, J.Kukula, K.Ravi, and F.Somenzi. To split or to conjoin: The question in image computation（分割するか、結合するか：イメージ計算における問題）. In Proceedings of the Design Automation Conference（設計自動化会議講演集所収）, pages 23-28,June 2000、及びR.K.Ranjan, A.Aziz, R.K.Brayton, B.F.Plessier, and C.Pixley. Efficient BDD algorithms for ESM synthesis and verification（ＥＳＭ合成及び検証のための有効ＢＤＤアルゴリズム）, in International Workshop for Logic Synthesis（論理合成に関する国際ワークショップ）, May 1995. Lake Tahoe,CAを参照のこと。
【００６３】
次に、単一のBDDを使用して入力集合P（x）が表現される場合の、本発明のリーフ計算手順の詳細を示す。P（x）が複数のBDDの論理和として表現される場合、このリーフ計算は、論理和においては各BDDについて個別に繰り返され、その結果得られた解の論理和が副問題の解として取られる。
【００６４】
図５に、各リーフ・イメージ計算について、定量化スケジュールの疑似コードを示す。この手順は、投影されたP（x）（及び、潜在的にはUnreached（y））と、投影された満足されない句に関するBDDから成るBDDのコレクションBから始まる。次に、定量化の対象となる変数vが発見手法により選択される。最小コスト変数は、変数が出現する各BDDのサイズの積としてコストが推定される貪欲方式で選択される。vが選択されると、vが出現するすべての連言肢が集合Cに収集される。続いて、C内のvの論理積と定量化が実行され、この結果がB内の集合Cと置換される。（y変数は定量化できないので、決して選択されることはない）。この基本ループは、定量化が可能な変数が尽きるまで反復される。残りのBDD（y変数だけを有する）が互いに結合され、さらにその結果が経路（y）（割り当て済みy変数）と結合されて、その経路に対応する新たなイメージ解の集合が得られる。
【００６５】
この公式は線形化スケジュールの生変数解析には依存せず、BDDの実際のサイズを考慮して選択を行うことに注意する必要がある。そのためこの公式は、論理積の線系列形式よりも、論理積ツリーの形式の方が計算のバランスを良好に保つことができる。関連の実験では、この発見的手法は、変数サポートに基づく他の実験に比較してはるかに良好な成績を残した。
【００６６】
完全イメージ計算手順
イメージ集合のすべての解を列挙するための完全な手順の実施例を、図６に示す。この実施例は、すでに公開されているGRASP SATソルバーの改良型である。P.Marquez-Silva. Grasp package（GRASPパッケージ）. http://algos.inesc.pt/~jpms/software.htmlを参照のこと。GRASPは説明のための例として使用されていることに注意する必要がある。本発明の範囲は、GRASPに限定されるものと解釈してはならない。
【００６７】
次に、原始の骨組みについて説明する。初期前処理の完了後の手順は、SAT決定ツリーを必要に応じた深度まで探索する外部ループ#1（第10行）から成る。内部ループ#2（第24行）は主に、決定変数が選択されたか、変数に対して何らかの値を暗黙に定義するためのバックトラッキングが実行された後に、制約条件を伝播して競合の有無を検査するために使用される。ループ#3（第26行）は矛盾の有無を検査するために実際に演繹法を実行し、診断を使用してその矛盾の解決を試み、矛盾がなくなるまでこれを繰り返す。GRASPでは、複数の解を列挙するために使用されたものを含み、すべてのバックトラッキング演算の原因を記録するための句が追加される。
【００６８】
イメージ集合のすべての解を検出するために本発明の手順に備えられる完全性引数の大部分は、GRASPの原始手順の完全性をベースとしている。J.P.Marques-Silva. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits（組み合わせ切り替え回路における満足化可能性問題のための探索アルゴリズム）.PhD thesis, EECS Department, University of Michigan(ミシガン大学EECS学部博士論文), May 1995を参照のこと。原始手順になされた改良は、SATリーフのBDDの手法（第11〜18行）、及びBDD束縛の手法（第7〜8行、第42〜57行）を導入したことである。原始手順は更に、決定変数の値が試行された最初の値であるか、その２番目の値が暗黙に定義される場合にのみコンフリクト解析を実行するように修正された（第27行）。
【００６９】
リーフにおいてすべてのBDD解を検出し、BDD束縛が失敗した場合に探索空間をプルーニングすることの正当性は、前のセクションで説明した引数に起因する。いずれの場合も、次の解を探索するために、発生順のバックトラッキング（第14〜17行、第54〜56行）が実行される。BDD束縛が成功した場合は（第42行）、解が検出されたかどうか、すなわち、すべての句が満足されたかどうかが決定される。すべての句が満足された場合は、SAT解が検出されたのであり、この解は通常の方法で処理される。続いて、次の解を検出するための発生順のバックトラッキングが実行される（第45〜48行）。
【００７０】
修正（第27行）を行ったのは、発生順バックトラッキングの句を記録するための句を追加するのを避けるためである。修正済みGRASPアルゴリズムの形式をとる本実施例では、発生順のバックトラッキングは解が検出されたか、BDD束縛が失敗した後に実行される。ただし、発生順バックトラッキングの句が記録されない場合は、診断時のGRASPのコンフリクト解析は不完全となり、このコンフリクト解析に基づいて非発生順バックトラッキングを実行すると誤った結果となる恐れがある。そのため、変数の２番目の値が何らかの句（原始句かコンフリクト句のいずれか）によって暗黙に定義される場合は、診断を実行できる。定義されない場合は、診断を実行しないことによって非発生順バックトラッキングが無効化され、代わりに単純な発生順バックトラッキングが実行される（第34〜39行）。非発生順バックトラッキングの代わりに発生順バックトラッキングを実行しても、影響されるのは手順の効率だけであり、その完全性は維持されることに注意する必要がある。
【００７１】
なぜSATなのか
先に指摘したように、最近、純粋なBDDを使用したイメージ計算問題の論理和分解の使用に関心が高まってきており、使用実績は顕著な向上を遂げている。G.Cabodi, P.Camurati, and S.Quer. Improving the efficiency of BDD-based operators by means of partitioning（分割によるBDDベース・演算子の効率向上）. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（集積回路及びシステムのコンピューター支援設計に関するIEEE報告書）, 18（5）:545-556, May 1999、及びI.-H.Moon, J.Kukula, K.Ravi, and F.Somenzi. To split or to conjoin: The question in image computation（イメージ計算における質問）. In Proceedings of the Design Automation Conference（設計自動化会議講演集所収）, pages 23-28, June 2000を参照のこと。本発明に従ってSAT決定ツリーを使用して探索ツリーを分割し、そのリーフでBDDに基づくイメージ計算を使用して結合を行うことによっても、同様の分解結果を得ることができる。ただし、SATの利点は単に論理和分解にとどまらず、これが本発明の手法と従来手法との違いとなっている。
【００７２】
特に、本発明では、変数決定（分割）の含意を容易に実行できる。理論的には、含意の導出はSATを使用しない状況でも同様に可能である。例えば、BDDなどを使用して回路構造上に直接導出することができる。しかし、この方法はこれまでイメージ計算で実際に使用されたことはなかった。標準的な最新鋭のSATパッケージを使用することにより、この方向での長年の成果と、効率的なバックトラッキングとコンフリクト解析の関連手法での長年の成果を活用し、基礎を成す探索空間のプルーニングの効果を高めることが可能となる。P.Marquez-Silva.Grasp package（GRASPパッケージ）.http://algos.inesc.pt/~jpms/software.htmlを参照のこと。BDD束縛の使用はこれに追加されるプルーニング手法であり、これにより初期バックトラッキングが可能となり、BDDに基づくリーフ計算を起動することさえも不要となる。
【００７３】
本発明の手法と従来手法のもう１つの相違点は、基礎を成す探索空間の細粒度である。焦点は設計のゲート・レベルの構造から直接導出される遷移関係に関するCNF式に当てられるので、遷移関係についてきわめて細粒度の高い区画を得ることができる。この区画は、イメージ及び前イメージ計算に関して対称でもある。これにより、全体をはるかに細かい区画に分割することが可能になり、さらには決定（分割）変数を内部信号とすることもできる。これらの変数の選択には、BDDに基づく基準とSATに基づく基準のいずれも使用できる。この基準の例としては、余因子BDDサイズの推定値や、変数が出現する句の数などが挙げられる。G.Cabodi, P.Camurati, and S.Quer. Improving the efficiency of BDD-based operators by means of partitioning（分割によるBDDベース・演算子の効率向上）. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems（集積回路及びシステムのコンピューター支援設計に関するIEEE報告書）, 18（5）:545-556, May 1999を参照のこと。（単一の解ではなく）複数の解を目標とするSATに基づく基準も探索される。また、細粒度が高いため、各区画について、初期定量化の利点をより広範に活用することができる。この利点は、BDDに基づく定量化スケジュール・アルゴリズムに反映されている。このアルゴリズムは、定量化する変数の選択に異なる基準（BDDの実際のサイズ）を使用し、線系列ではなく論理積のツリーとして構成される。
【００７４】
最後に、本発明の手法の目標には、SATとBDDをシームレスに結合して、イメージ計算問題を解決するための時間とスペース間のトレードオフをスムーズかつ適応可能にすることが含まれる。 本発明のアルゴリズムでは、SATからBDDへの移行はBDD副問題がトリガーされたときに発生する。理想的には、BDDがブローアップしないことが確実なときに常にこの移行を実行するのが望ましい。ただし、これを演繹的に予測するための簡単な方法は見あたらない。CNF式とBDDは完全な互換性があるので、SATとBDDの間の境界は曖昧である。理論的には、回路の様々な部分に関してCNFとBDDを自由に混合し、より適切な表現に対して所要の解析を実行することが可能である。本発明の手法は、この実現に向けた一ステップである。
【００７５】
実験
ここでは、到達可能性解析の実験結果を示す。この結果は、本発明の手法における個々の着想と取り組みの方向性が有効であることを実証している。
【００７６】
CUDDのBDDパッケージとGRASPのSAT ソルバーに基づくイメージ計算手法の実施例を実装した。CUDDの詳細については、F.Somenzi et al. CUDD:University of Colorado Decision Diagram Package(CUDD：コロラド大学決定ダイアグラム・パッケージ).http://vlsi.colorado.edu/~fabio/CUDD/、及びP.Marquez-Silva. Grasp package（GRASPパッケージ）. http://algos.inesc.pt/~jpms/software.htmlを参照のこと。このセクションでは、到達可能性解析は困難であると知られるいくつかのISCASベンチマーク回路に対して実施した実験の結果を述べる。実験はすべて、296 MHzのプロセッサーと768 MBのメモリーを搭載するUItraSPARCワークステーション上で行った。
【００７７】
ここでは、精密到達可能性解析の実験だけを取り上げる。本発明の手法では、近似到達可能性解析、不変検査、及びモデル検査での使用をはじめとして、多種多様な方向での適応と機能増強が容易であることは明らかである。
【００７８】
表1に、CNF-BDDプロトタイプと呼ばれる本実施例とVISとの比較を示す。VISの詳細については、R.K.Brayton et al.VIS: A system for verification and synthesis（ＶＩＳ：検証及び合成のためのシステム）. In R.Alur and T.Henzinger, editors（編集）, Proceedings of the Internation Conference on Computer-Aided Verification（コンピューター支援検証に関する国際会議講演集所収）, Volume 1102 of Lecture Notes in Computer Science（コンピューター・サイエンスの講義ノーと第１１０２巻）, pages 428-432, June 1996を参照のこと。表１は、純粋な幅優先探索を使用して、実用的な処理が困難であることが知られているいくつかのベンチマーク回路に対して実行した精密到達可能性解析の結果を示す。回路名とラッチ数はそれぞれ、カラム１、カラム２に示す。
【表１】
2004288204.tif 000006
【００７９】
本発明の手法では、カラム３に示す遷移関係のCNF表現に出現する変数の数を回路の複雑性の測定基準とした。カラム４は、完了したステップ数を示す。ここで、「（p）」は部分走査を示す。カラム5は、到達した状態の数を示す。カラム6は、VISによって消費されたCPU時間（単位：秒）を示す。各実験では、10時間のタイムアウトを使用した。ただし、タイムアウトになる前にVISがメモリー不足となるケースが何度か発生した。この場合は、同カラムで「-」として示している。カラム7〜11は、CNF-BDDプロトタイプの数を示す。カラム7は、消費されたCPU時間（単位：秒）を示す。カラム8と9は、CUDDパッケージが報告した消費メモリー量とピークBDDノード数を示す。本発明の修正済みSATソルバーの有効性を具体的に示すため、BDD副問題（リーフ）の数と、BDD束縛（束縛）によるバックトラック数をカラム10と11にそれぞれ示す。どの実験でも、SATソルバーによる非発生順のバックトラッキングは観察されていない。そのため、全ステップにおけるイメージ計算時のバックトラックの総数は、カラム10と11の和となる。
【００８０】
この表から、本発明のCNF-BDDプロトタイプは、4回路のうち３回路においてVISより良好な成績を収めたことが分かる。s1512については、本発明のプロトタイプの成績が不振だったのはステップ数が1024と多く、SATソルバーを再起動する各ステップのオーバーヘッドが大きいためと思われる。s1269の場合、プロトタイプはVISの約2倍の高性能を示した。いずれの回路についても、CNF-BDDの数は、最近I.-H. Moon, J.Kukula, K.Ravi, and F.Somenzi． To split or to conjoin: The question in image computation（分割するか、結合するか：イメージ計算における問題）. In Proceedings of the Design Automation Conference（設計自動化会議講演集所収）, pages 23-28,June 2000で報告されたs1269の891秒、s1512の2016秒よりも劣っている。本発明の手法の真の利点は、s1423やs5378のような難解な回路に見いだすことができる。これらの回路では、VISと本発明のプロトタイプのいずれも走査を完了することができない。s1423の場合、VISはステップ11まで完了できた。本発明のプロトタイプは、VISの３倍以上の速度で同数のステップを完了した。事実、本プロトタイプは、所定の時間内に到達可能性計算をVISより２ステップ多く完了できる。同様に、s5378の場合、本発明のプロトタイプはステップ6までをVISよりも短時間で完了し、所定の時間内に更に2ステップを完了できる。メモリー量とピークのカラムを見ると明らかなように、本発明の手法はこれらの実験を実行してもまだメモリーの限界に達しないと予想されるが、VISは所定の時間内にメモリーの限界に達する。また、本発明の手法ではBDD束縛がSAT探索空間内のプルーニングに絶大な効果を発揮するので、バックトラック数の制御にも十分な余裕がある。更に、どの実験についても、BDD束縛情報の計算に要するオーバーヘッドはごくわずかであった。
【表２】
2004288204.tif 000007
【００８１】
本発明の手法と標準的な純粋にBDDベースの手法を対比するため、s1423について詳細な実験を実施した。このとき、必要とされるメモリー消費量の統計データを抽出できるようにVISインターフェースを変更することができなかった。そのため、これらの実験は「NanoTrav」と呼ばれるスタンドアロン型の走査プログラムを使用して実施した。このプログラムは、CUDDパッケージに同梱して配布されている。F. Somenzi et al. CUDD:University of Colorado Decision Diagram Package（CUDD：コロラド大学決定ダイアグラム・パッケージ）. http://vlsi.colorado.edu/~fabio/CUDD/を参照のこと。NanoTravには区画化された遷移関係の初期定量化又はクラスター化を行うための高度な発見的手法が含まれていないため、その成績は概してVISに劣る。この制約によりメモリー所要量にある程度の影響が現れた。表2は、主に全体的な傾向を示すことを目的として示す。この表では、カラム1と2はステップ数と到達した状態を示す。カラム3は、NanoTravが消費したCPU時間（単位：秒）を示す。カラム4と5はそれぞれ、各イメージ計算の終了時点のピーク・ノード数と活性ノード数を示す。カラム6、7、8は、CNF-BDD手法の同じ項目の結果を示す。カラム9と10はそれぞれ、SATリーフにおけるBDDの数（リーフ）と、BDD束縛によるバックトラック数（束縛）を示す。
【００８２】
この表から明らかなように、メモリー所要量はステップ数の増大に伴って増え続ける。ただし、増大のペースは、CNF-BDDプロトタイプよりもNanoTravの方が速い。11番目のステップでは、NanoTravのピークBDDノードはCNF-BDDの4倍に上る。言うまでもなく、CNF-BDDはほぼ同じ時間内に２つの到達可能性ステップを余分に完了できる。更に、CNF-BDDプロトタイプは１４番目のステップの実行中にもメモリーの限界に達しなかったが、10時間後にタイムアウトにより強制終了された。
【００８３】
本発明の手法では、SATリーフにおけるBDDのトリガー条件を動的に変更することにより、SATソルバーとBDD間のトレードオフを行うことができる。ただし、イメージ計算においては、メモリーと時間のトレードオフが提供されるだけであり、状態集合を表現するためにモノリシックBDDを使用する場合のメモリー所要量が低減されるわけではない。これまでのセクションで説明したように、本発明の手法は論理和区画（複数BDD）形式の状態集合を処理するのに非常に適している。しかし、プロトタイプをこの方向に拡張することが可能なことは明らかである。
【００８４】
以上好ましい実施の形態及び実施例をあげて本発明を説明したが、本発明は必ずしも上記実施の形態及び実施例に限定されるものではなく、その技術的思想の範囲内において様々に変形して実施することができる。
【００８５】
例えば、本発明の範囲には、本発明の手法を近似走査、不変検査、CTLモデル検査などの他の用途に拡張することが含まれる。また、基本イメージ計算戦略にいくつかの機能増強を行うことも可能である。
【図面の簡単な説明】
【００８６】
【図１】本発明によるCNF-BDD表現の構成を示す図である。
【図２】本発明による単一のBDDに対する単一束縛のための疑似コードを示す図である。
【図３】本発明による複数のBDDと投影との論理積に対する複数束縛のための疑似コードを示す図である。
【図４】本発明によるSATにおけるBDDを示す図である。
【図５】本発明によるリーフ・イメージ計算の一実施例のための疑似コードを示す図である。
【図６】本発明による完全なSAT-BDDイメージ計算手順の実施例のための疑似コードを示す図である。
【図７】従来の組み合わせ検証のためのマイター回路を示す図である。
【図８】従来のSATのためのバックトラッキング探索手順を示す図である。
【図１】
2004288204.tif 000008
【図２】
2004288204.tif 000009
【図３】
2004288204.tif 000010
【図４】
2004288204.tif 000011
【図５】
2004288204.tif 000012
【図６】
2004288204.tif 000013
【図７】
2004288204.tif 000014
【図８】
2004288204.tif 000015