(57)【要約】【課題】従来よりも検証を高速化し得る回路検証装置、回路検証システム及び回路検証機能付ＬＳＩを提供する。【解決手段】本発明の回路検証システム１では、本質的に並列性が高い回路シミュレーションとスキップキューブの計算とを、ハードウェア化したスキップキューブ計算回路４によって実行するようにしたことにより、これら回路シミュレーション及びスキップキューブの計算をほぼ並列に実行できるようになり、高速にスキップキューブを計算できる。【選択図】図１
2009294738.tif 000002
【特許請求の範囲】
【請求項１】
複数の入力パターンを取得する取得手段と、
各前記入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき論理ゲートの演算結果を検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、
前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて各前記入力パターン毎に算出するスキップキューブ計算用ハードウェアモジュールと
を備えることを特徴とする回路検証装置。
【請求項２】
前記入力パターンを生成する入力パターン生成装置と無線又は有線で通信可能に接続され、
前記取得手段は、前記複数の入力パターンを一括して前記入力パターン生成装置から受信し、
前記スキップキューブ計算用ハードウェアモジュールで算出した複数の前記スキップキューブを一括して前記入力バターン生成装置へ送信する
ことを特徴とする請求項１記載の回路検証装置。
【請求項３】
前記シミュレーション用ハードウェアモジュール及び前記スキップキューブ計算用ハードウェアモジュールは、供給されるプログラムデータに基づいて内部の回路構造を変更し得るフイールド・プログラマブル・ゲートアレイからなり、前記回路シミュレーションに用いる検証対象回路に変更するプログラムデータに基づいて、前記回路シミュレーション及び前記スキップキューブを算出するスキップキューブ計算回路に変換する
ことを特徴とする請求項１又は２記載の回路検証装置。
【請求項４】
複数の入力パターンを生成する入力パターン生成装置と、回路検証装置とから構成されており、
前記回路検証装置は、
前記複数の入力パターンを取得する取得手段と、
各前記入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき論理ゲートの演算結果を検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、
前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて各前記入力パターン毎に算出するスキップキューブ計算用ハードウェアモジュールとを備える
ことを特徴とする回路検証システム。
【請求項５】
前記入力パターン生成装置と前記回路検証装置とが無線又は有線で通信可能に接続され、
前記入力パターン生成装置は、前記入力パターンを生成して、前記複数の入力パターンを一括して前記回路検証装置へ送信し、前記回路検証装置において各前記入力パターン毎に算出した複数の前記スキップキューブを前記回路検証装置から一括して受信し、
前記回路検証装置は、前記複数の入力パターンを前記入力パターン生成装置から一括して受信し、前記スキップキューブ計算用ハードウェアモジュールで算出した複数の前記スキップキューブを前記入力パターン生成装置へ一括して送信する
ことを特徴とする請求項４記載の回路検証システム。
【請求項６】
前記回路検証装置は、
前記シミュレーション用ハードウェアモジュール及び前記スキップキューブ計算用ハードウェアモジュールは、供給されるプログラムデータに基づいて内部の回路構造を変更し得るフイールド・プログラマブル・ゲートアレイからなり、前記回路シミュレーションに用いる検証対象回路に変更するプログラムデータに基づいて、前記回路シミュレーション及び前記スキップキューブを算出するスキップキューブ計算回路に変換する
ことを特徴とする請求項４又は５記載の回路検証システム。
【請求項７】
外部から取得した入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき、回路が仕様通りに動作しているかを検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、
前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて算出するスキップキューブ計算用ハードウェアモジュールと
を備えることを特徴とする回路検証機能付ＬＳＩ。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路検証装置、回路検証システム及び回路検証機能付ＬＳＩに関し、例えば効率的な解空間探索に基づいたコンパイルドシミュレーションを行う準形式的検証技術に適用して好適なものである。
【背景技術】
【０００２】
近年、回路の検証の重要性やコストの増加に伴い、大規模設計の効率的な形式的検証が非常に重要となっている。そして、効率的な解空間探索に基づいたコンパイルドシミュレーションを行う準形式的検証技術が提案されており、充足可能性判定（Satisfiability：ＳＡＴ)に基づいた検証手法と同等の効率を実現できることが示されている（例えば、非特許文献１参照）。
【０００３】
この準形式的検証手法では、最新のＳＡＴソルバで用いられている矛盾学習や非年代順バックトラックといった手法を適用して効率的な解空間探索を行うようになされている。これにより、準形式的検証手法では、シミュレーションに基づく手法の問題点の一つである、可能な入力パターンの総数が入力数に対して指数関数的に増加するという問題を解決している。また、この準形式的検証手法では、たとえ網羅的な検証が実現不可能な場合においてもカバレッジ、つまり検証が完了した空間の割合が簡単に求められるという利点も存在する。
【０００４】
かかる準形式的検証手法について以下簡単に説明する。以下の表１の「手続き１」は準形式的検証手法の基本的な手続きを示す。
【０００５】
【表１】
2009294738.tif 000003
【０００６】
この手続き１では、Ｖがこれまで検証した入力パターンの集合を保持しているとすると、先ずＶから最小項を取り出すことで、未だ検証を行っていない新しい入力パターンを生成する。子の入力パターンに対して、関数シミュレート回路を呼び出すことで回路のシミュレーションを行う。関数シミュレート回路の本体は、対象回路構造に基づいて自動的に生成される。関数中の各文は回路中にあるゲートの計算に対応している。例えば、仮に対象回路が２つの入力端子を有する１つのＡＮＤゲートからなる場合には、関数の本体は以下のようになる。
【０００７】
【数１】
2009294738.tif 000004
【０００８】
生成されたシミュレータはグラフ探索等の計算が必要でないため、効率的なシミュレーションが可能である。コンパイルドシミュレーションに加えて、関数シミュレート回路は対象回路の出力におけるスキップキューブ（後述する）の計算を行う。ここでスキップキューブとは、結果である出力値が同じになり、シミュレーションを行う必要がない入力パターンの集合をいい、出力値を決定している入力パターンの一部である。
【０００９】
具体的にはこのスキップキューブはキューブ表現によって表される。キューブ表現とは、変数を「０」、「１」及び「−」の３つの値を用いて示す表現をいう。ここで「−」は値が「０」及び「１」のどちらでも良いということを表す。例えばキューブ[０，１]と[０，０]との和の集合では、スキップキューブは[０，−]となる。
【００１０】
スキップキューブは論理ゲート毎に入力と出力の依存関係を元に計算される。より詳細に説明すると、例えば、５つの入力端子を有するＡＮＤゲートに対して入力パターン[０，１，１，１，１]でシミュレーションを行ったとする。このときの出力値は０となるが、これは１番目の入力値が０であることに由来し、この１番目の入力値が０である限りは他の入力値が変化しようとも同じ結果になる。よって、この場合スキップキューブは[０，−，−，−，−]となり、これに該当する例えば[０，１，１，１，０]や[０，１，０，０，０]等の他の入力パターンに対してはシミュレーションを回避できる。このようなシミュレーションを繰り返すことで、満たすべき性質(プロパティ)を満たすと証明された入力パターンがスキップキューブ集合に追加されてゆき、全ての入力パターンがスキップキューブ集合に含まれることにより回路がプロパティに対して正しいと証明され得る。
【００１１】
ここで、ある入力パターンＶに対する配線におけるスキップキューブＡv（ｗ）は以下の４つのように定義される。なお、ここでｗは配線からの出力を示す。先ず第１の定義としては、仮に配線が支配値μを持ち、２つの入力端子を有する論理ゲート（例えば、μ=０ならばＡＮＤゲート（論理積ゲート）)であり、入力される信号値をそれぞれａとｂとしたとき、スキップキューブＡv（ｗ）は下記の数２のように計算する。ここで支配値μとは、論理ゲートの出力が一意に決まる入力値のことであり、ＡＮＤゲートの場合は０、ＯＲゲートの場合には１となる。
【００１２】
【数２】
2009294738.tif 000005
【００１３】
なお、ｍａｘ（Ａv（ａ），Ａv（ｂ））は、Ａv（ａ）及びＡv（ｂ）の２集合のうち濃度の高い、いずれかのＡv（ａ）又はＡv（ｂ）の集合を表す。
【００１４】
また、第２の定義としては、仮に配線が入力の信号値ａを持つインバータならば、Ａv（ｗ）＝Ａv（ａ）とする。さらに、第３の定義としては、仮に配線が初期入力ｘiであれば、Ａv（ｗ）＝（Ｂ１，…，ＢＮ）とする。ここでｊ＝ｉならばＢｊ＝「ｗv」、それ以外の場合にはＢｊ＝「−」とする。第４の定義としては、配線が支配値μを持たないゲート(例えば排他的論理和ゲート)の出力であり、入力の信号値がａとｂのとき、Ａv（ｗ）＝Ａv（ａ）∩Ａv（ｂ）とする。
【００１５】
２つ以上の入力端子を有する論理ゲートの場合でも、同様にスキップキューブは計算できる。上記表１の手続き１の中では、関数シミュレート回路中において各入力パターンに対して出力ｆにおけるスキップキューブＡv（ｆ）を計算する。あるスキップキューブに含まれるいずれの入力パターンも、同じ出力を生成することが証明されているので、それらの入力パターンはシミュレーションする必要がない。従って、スキップキューブを用いた場合の入力パターンの総数は、スキップキューブを用いない場合の入力パターンの総数に比べて格段的に少なくなる。
【００１６】
検証をすでに行った入力パターンの集合Ｖ、つまり明示的にシミュレーションを行った入力パターンとスキップキューブとに含まれる入力パターンは二分決定グラフ（ＢＤＤ：Binary Decision Diagram）によって表現される（例えば、非特許文献２参照）。毎回のシミュレーションにおいて、ＢＤＤに含まれない最小項をランダムに選択することで入力パターンを決定する。このようにＢＤＤを用いることで、大きさに比例した時間でＢＤＤに含まれない最小項を計算できる。
【非特許文献１】A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. Lecture Notes in Computer Science, 1579:193-207, 1999.
【非特許文献２】R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677-691, 1986.
【発明の開示】
【発明が解決しようとする課題】
【００１７】
しかしながら、上記表１の手続き１に示した準形式的検証手法を実行可能なソフトウェアをコンピュータに実装し、実行時のプロファイルを解析したところ、下記の表２に示すようなプロファイル結果が得られた。
【００１８】
【表２】
2009294738.tif 000006
【００１９】
このように、準形式的検証手法を全てソフトウェアによって実行した場合には、回路シミュレーション処理とスキップキューブ計算処理の実行に時間がかかり、検証を高速化し難いという問題があった。
【００２０】
そこで本発明は上記した問題点に鑑み、従来よりも検証を高速化し得る回路検証装置、回路検証システム及び回路検証機能付ＬＳＩを提供することを目的とする。
【課題を解決するための手段】
【００２１】
請求項１に係る発明は、複数の入力パターンを取得する取得手段と、各前記入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき論理ゲートの演算結果を検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて各前記入力パターン毎に算出するスキップキューブ計算用ハードウェアモジュールとを備えることを特徴とする。
【００２２】
また、請求項２に係る発明は、前記入力パターンを生成する入力パターン生成装置と無線又は有線で通信可能に接続され、前記取得手段は、前記複数の入力パターンを一括して前記入力パターン生成装置から受信し、前記スキップキューブ計算用ハードウェアモジュールで算出した複数の前記スキップキューブを一括して前記入力バターン生成装置へ送信することを特徴とする。
【００２３】
また、請求項３に係る発明は、前記シミュレーション用ハードウェアモジュール及び前記スキップキューブ計算用ハードウェアモジュールは、供給されるプログラムデータに基づいて内部の回路構造を変更し得るフイールド・プログラマブル・ゲートアレイからなり、前記回路シミュレーションに用いる検証対象回路に変更するプログラムデータに基づいて、前記回路シミュレーション及び前記スキップキューブを算出するスキップキューブ計算回路に変換することを特徴とする。
【００２４】
また、請求項４に係る発明は、複数の入力パターンを生成する入力パターン生成装置と、回路検証装置とから構成されており、前記回路検証装置は、前記複数の入力パターンを取得する取得手段と、各前記入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき論理ゲートの演算結果を検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて各前記入力パターン毎に算出するスキップキューブ計算用ハードウェアモジュールとを備えることを特徴とする。
【００２５】
また、請求項５に係る発明は、前記入力パターン生成装置と前記回路検証装置とが無線又は有線で通信可能に接続され、前記入力パターン生成装置は、前記入力パターンを生成して、前記複数の入力パターンを一括して前記回路検証装置へ送信し、前記回路検証装置において各前記入力パターン毎に算出した複数の前記スキップキューブを前記回路検証装置から一括して受信し、前記回路検証装置は、前記複数の入力パターンを前記入力パターン生成装置から一括して受信し、前記スキップキューブ計算用ハードウェアモジュールで算出した複数の前記スキップキューブを前記入力パターン生成装置へ一括して送信することを特徴とする。
【００２６】
また、請求項６に係る発明は、前記回路検証装置は、前記シミュレーション用ハードウェアモジュール及び前記スキップキューブ計算用ハードウェアモジュールは、供給されるプログラムデータに基づいて内部の回路構造を変更し得るフイールド・プログラマブル・ゲートアレイからなり、前記回路シミュレーションに用いる検証対象回路に変更するプログラムデータに基づいて、前記回路シミュレーション及び前記スキップキューブを算出するスキップキューブ計算回路に変換することを特徴とする。
【００２７】
また、請求項７に係る発明は、外部から取得した入力パターンに基づいて入力側から出力側へ向けて信号値を求めてゆき、回路が仕様通りに動作しているかを検証するための回路シミュレーションを実行するシミュレーション用ハードウェアモジュールと、前記出力側から前記入力側へ向けて伝搬フラグを算出してゆき、前記回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、前記伝搬フラグに基づいて算出するスキップキューブ計算用ハードウェアモジュールとを備えることを特徴とする。
【発明の効果】
【００２８】
本発明の請求項１、４及び７によれば、本質的に並列性が高い回路シミュレーションとスキップキューブの計算とを、ハードウェア化したシミュレーション用ハードウェアモジュール及びスキップキューブ計算用ハードウェアモジュールによって実行するようにしたことにより、これら回路シミュレーション及びスキップキューブの計算をほぼ並列に実行できるようになり、高速にスキップキューブを計算でき、かくして従来よりも検証を高速化し得る。
【発明を実施するための最良の形態】
【００２９】
以下本発明の好適な実施形態について説明する。
【００３０】
（１）本発明における回路検証システムの概略
図１において、１は全体として回路検証システムを示し、入力パターン生成処理プログラムが実装され、ステップＳＰ１の入力パターン生成処理を実行するコンピュータ２と、ステップＳＰ２の回路シミュレーション処理及びステップＳＰ３のスキップキューブ計算処理を順次実行するハードウェアが実装された回路検証装置３とから構成されている。
【００３１】
この回路検証システム１では、従来において、プログラムによりコンピュータ２で実行されていた回路シミュレーション処理とスキップキューブ計算処理とをハードウェア（回路検証装置３）で実行し、ハードウェアとソフトウェアとの協調実行によって準形式的検証の高速化を図るようになされている。
【００３２】
ここで、準形式的検証手法とは、回路の設計が正しいことを数学的に証明する検証手法であって、シミュレーションと同時に回路を解析することで、シミュレーションの必要が無い冗長な入力パターンを動的に割り出してスキップキューブを生成し、当該スキップキューブに基づき冗長な入力パターンを次回以降のシミュレーションの実行から除外することで、シミュレーション回数を大幅に減らすことができる検証手法をいう。
【００３３】
また、この回路検証システム１は、例えばＵＤＰ／ＩＰ（Ｕｓｅｒ Ｄａｔａｇｒａｍ Ｐｒｏｔｏｃｏｌ／Ｉｎｔｅｒｎｅｔ Ｐｒｏｔｏｃｏｌ）等の通信手段によってコンピュータ２と回路検証装置３とが接続されており、これらコンピュータ２及び回路検証装置３間で各種データの授受を実行し得るようになされている。
【００３４】
実際上、コンピュータ２は、ステップＳＰ１において、入力パターン生成処理を実行して、回路検証装置３において回路シミュレーション及びスキップキューブ計算を実行するための入力パターンを、予め決められた所定数だけ生成し、これら複数の入力パターン全てを一度に通信手段を介して回路検証装置３に投機的に送信する。
【００３５】
ここで、回路検証装置３には、検証対象回路を基に形成したスキップキューブ計算回路４が設けられており、当該スキップキューブ計算回路４において回路シミュレーション処理及びスキップキューブ計算処理を実行し得るようになされている。
【００３６】
具体的に、この回路検証装置３には、回路シミュレーションとスキップキューブの計算とを実行し得るスキップキューブ計算回路４が形成されている。先ず始めに回路検証装置３は、ステップＳＰ２において、１パターンの入力パターンをスキップキューブ計算回路４の初期入力側から入力し、初期出力側から所定の出力を得る回路シミュレーション処理を実行し、次のステップＳＰ３へ移行する。
【００３７】
次いで、ステップＳＰ３において、回路検証装置３は、初期出力側から得た出力を基に所定の伝搬フラグ信号を生成し、この伝搬フラグ信号をスキップキューブ計算回路４の初期出力側から初期入力側に向って入力してスキップキューブを算出するスキップキューブ計算処理を実行し得る。そして、回路検証装置３は、コンピュータから受け取った全ての入力パターンに対して回路シミュレーション処理及びスキップキューブ計算処理を順次実行してゆき、各入力パターン毎にスキップキューブを算出する。
【００３８】
次いで、回路検証装置３は、各入力パターン毎に算出した全てのスキップキューブを通信手段を介して一度にコンピュータ２に送信する。コンピュータ２は、受け取った複数のスキップキューブのうち、同じ値のスキップキューブを破棄し、異なる値からなる複数のスキップキューブを記憶部に記憶する。次いで、コンピュータ２は、所定の方法で次の入力パターンを生成し、これら新しく生成した複数の入力パターンと、記憶したスキップキューブとを比較して、当該スキップキューブに含まれる入力パターンを破棄する。また、コンピュータ２は、残ったスキップキューブに含まれない入力パターンを記憶してゆき、これら複数の入力ターン全てを一度に回路検証装置３へ送出する。
【００３９】
このようにして、検証システム１は、複数の入力パターン毎にスキップキューブを生成してゆき、当該スキップキューブに含まれる他の入力パターンについて破棄することでこれら入力パターンを回路検証に用いずに済み、検証に用いる入力パターンの数を格段的に少なくでき、全体の回路検証時間を短縮化させることができる。
【００４０】
因みに、上述した実施の形態においては、検証対象回路の検証を行う製品とは別に、スキップキューブを算出する回路検証装置３を別途検証用として製造し用いるようにした場合について述べたが、本発明はこれに限らず、製品自体に予めスキップキューブ計算回路４を内蔵させておくようにしてもよい。この場合、ＬＳＩ（Large Scale Integrated circuit）にスキップキューブ計算回路４を設けて回路検証機能付ＬＳＩを製造し、これを製品に実装する。この場合には、回路検証機能付ＬＳＩにおいて、回路が仕様通りに動作しているかを検証するための回路シミュレーションを実行し得る。そして、回路検証機能付ＬＳＩに基づいて製品毎にスキップキューブを算出し、当該スキップキューブを基に製品の回路設計が正しいか否かを個別に検証することができる。
【００４１】
（２）回路シミュレート処理及びスキップキューブ計算処理
まず、本発明において、スキップキューブの計算処理をハードウェアで実行する際のスキップキューブＡv（ｗ）の定義について以下説明する。この場合、所定の入力パターンＶに対する配線におけるスキップキューブＡv（ｗ）は以下の４つのように定義される。
なお、ｗは配線の出力を示す。先ず第１の定義としては、仮に配線が支配値μを持つ２つの入力端子を有する論理ゲート（例えば、μ＝０ならばＡＮＤゲート（論理積ゲート））であり、入力される信号値をそれぞれａとｂとしたとき、スキップキューブＡv（ｗ）は下記の数３のように計算する。
【００４２】
【数３】
2009294738.tif 000007
【００４３】
因みに、上述の従来技術で記載した数２との相違点は、２つの入力端子の両入力が支配値μを持っているとき、２つの入力におけるスキップキューブＡv（ａ）及びＡv（ｂ）のいずれか一方を選択するかを任意とする点である。なお、上述の従来技術で記載した数２では、ｍａｘ（Ａv（ａ），Ａv（ｂ））を用いて潜在的に濃度の高い方をスキップキューブとして選択していたが、ｍａｘ（Ａv（ａ），Ａv（ｂ））をハードウェアで実装することが困難であるため、本発明の手法では、例えば最初の入力Ａv（ａ）を常にスキップキューブとしている。
【００４４】
また、第２〜第４の定義については上述の従来技術で記載した第２〜第４の定義と同じである。すなわち、第２の定義としては、仮に配線が入力として信号値ａを持つインバータならば、Ａv（ｗ）＝Ａv（ａ）とする。さらに、第３の定義としては、仮に配線が初期入力ｘiであれば、Ａv（ｗ）＝（Ｂ１，…，ＢＮ）とする。ここでｊ＝ｉならばＢｊ＝「ｗv」、それ以外の場合にはＢｊ＝「−」とする。第４の定義としては、配線が支配値μを持たないゲート(例えば排他的論理和ゲート)の出力であり、入力される信号値がａとｂのとき、Ａv（ｗ）＝Ａv（ａ）∩Ａv（ｂ）とする。そして、本発明においては、上述した第１〜第４の定義に基づいてスキップキューブＡv（ｗ）が計算される。
【００４５】
次に、本発明における回路シミュレーション処理及びスキップキューブ計算処理を実行し得るスキップキューブ計算回路がどうのようにして形成されるかについて図２、図３及び図４を参照しながら具体的に説明する。
【００４６】
図２は、製品に実装され、回路設計が正しいか否かが検証される検証対象回路10のブロック図である。この検証対象回路10は一例であり、入力側から複数の信号値１又は０からなる所定の入力パターンが入力されることにより出力側から出力値が出力され、この入力パターンと出力値とを検証することにより検証対象回路10が最適に動作しているか否かを検証し得る。
【００４７】
スキップキューブ計算回路は、この検証対象回路10を基に形成されることから、先ず始めに一例として示した検証対象回路10について以下説明する。実際上、この検証対象回路10は、２つの入力端子を有するＡＮＤゲート11を備え、当該ＡＮＤゲート11の出力端子に分配部15を介して、他のＡＮＤゲート12の一方の入力端子と、インバータ13の入力端子とが接続されている。また、検証対象回路10は、２つの入力端子を有する他のＡＮＤゲート14の一方の入力端子に、当該インバータ13の出力端子が接続され、当該ＡＮＤゲート14の出力端子がＡＮＤゲート12の他方の入力端子に接続されている。
【００４８】
この場合、検証対象回路10では、回路シミュレーションとして、入力パターン[１，１，０]を入力した場合、ＡＮＤゲート11の２つの入力端子に信号値１であるシミュレーション信号ｘ（１），ｙ（１）が入力され、他のＡＮＤゲート14の他方の入力端子に信号値０であるシミュレーション信号ｚ（０）が入力される。
【００４９】
これにより検証対象回路10は、信号値１を示すシミュレーション信号ａ（１）と、信号値０を示すシミュレーション信号ｃ（０）とが最終端のＡＮＤゲート12の入力端子に入力され、当該ＡＮＤゲート12の出力端子から信号値０を示すシミュレーション信号ｆ（０）が出力される
そして、このような検証対象回路10は、各論理回路が図３（Ａ）〜（Ｃ）に示す論理ブロックに置き換えられることにより、回路シミュレーションとスキップキューブの計算とを実行し得るスキップキューブ計算回路が形成され得る。
【００５０】
具体的に、この実施の形態の場合、図２におけるＡＮＤゲート11，12，14は、図３（Ａ）に示すようなアンドブロック20に置き換えられ、図４に示すように、ＡＮＤゲート11がアンドブロック20a，ＡＮＤゲート12アンドブロック20b，ＡＮＤゲート14がアンドブロック20cとなる。また、図２におけるインバータ13は、図３（Ｂ）に示すようなインバータブロック30に置き換えられ、図２における分配部15は、図３（Ｃ）に示すような分配ブロック40に置き換えられ、スキップキューブ計算回路４が形成され得る。
【００５１】
そして、検証対象装置３には、このようにして検証対象回路10に基づいて形成された図４に示すようなスキップキューブ計算回路４が実装され得る。
【００５２】
因みに、この実施の形態の場合には、説明を簡単にするために、検証対象回路10は２つの入力端子を有するＡＮＤゲート11，12，14とインバータ13のみによって構成されると仮定するが、より一般的な回路についても同様の方法でスキップキューブを計算することは可能であり、またＦＰＧＡ（フイールド・プログラマブル・ゲートアレイ）のような素子については別途後述する。
【００５３】
ここで、図３（Ａ）に示すように、アンドブロック20は、２つの入力端子と、１つの出力端子とを有する第１のＡＮＤゲート21が設けられており、回路シミュレーション時、この第１のＡＮＤゲート21に入力された２つの信号値ａ，ｂに基づいて１つの出力ｗを出力し得る。
【００５４】
これに加えて、このアンドブロック20は、回路シミュレーション後に実行されるスキップキューブ算出時、回路シミュレーション時とは逆の初期出力側から初期入力側へ向って信号値を求めてゆき伝搬フラグａp，ｂpを算出し得るようになされている。ここで伝搬フラグａp，ｂpはスキップキューブを計算する際に必要なものであり、定義については後述する。
【００５５】
アンドブロック20は、伝搬フラグａp，ｂpを求めるための回路構成として、第１のＡＮＤゲート21の一方の入力端子が、インバータ22を介してＯＲゲート23の一方の入力端子に接続されているとともに、第２のＡＮＤゲート24の一方の入力端子にも接続されている。
【００５６】
また、アンドブロック20は、第１のＡＮＤゲート21の他方の入力端子がＯＲゲート23の他方の入力端子に接続され、このＯＲゲート23の出力端子が第３のＡＮＤゲート25の一方の入力端子に接続されている。第２のＡＮＤゲート24及び第３のＡＮＤゲート25は、それぞれ２つの入力端子と、１つの出力端子とを有し、スキップキューブ算出時、当該第２のＡＮＤゲート24及び第３のＡＮＤゲート25の他方の各入力端子に信号値ｗpが入力され得る。
【００５７】
これによりアンドブロック20は、第２のＡＮＤゲート24及び第３のＡＮＤゲート25に入力された信号値ｗpと、回路シミュレーショ-ン時に得た信号値とに基づいて第２のＡＮＤゲート24の出力端子から伝搬フラグｂpを出力し、第３のＡＮＤゲート25の出力端子から伝搬フラグａpを出力し得る。
【００５８】
図３（Ｂ）に示すように、インバータブロック30は、１つのインバータ31が設けられており、回路シミュレーション時、一方の入力端子から入力された信号値ａを逆の信号値（例えば信号値１のとき信号値０）とし、これを出力ｗとして一方の出力端子から出力する。
【００５９】
一方、インバータブロック30は、スキップキューブ算出時、インバータ31が設けられた経路とは異なる経路の入力端子から信号値ｗpが初期出力から初期入力に向けて入力されると、そのまま伝搬フラグａpとして他方の出力端子から出力し得る。
【００６０】
図３（Ｃ）に示すように、分配ブロック40は、回路シミュレーション時、入力端子から入力された信号値ａを分配部41を介して２つの出力端子に送出して出力ｗ１，ｗ２として出力し得る。
【００６１】
一方、分配ブロック40には、ＯＲゲート42が設けられており、伝搬フラグ算出時、初期出力側に設けた入力端子から入力された信号値ｗp1，ｗp2を当該ＯＲゲート42を介して１つの信号値ａpとして出力し得るようになされている。
【００６２】
因みに、図３（Ｃ）に示した分配ブロック40は、分配数が２つ以上増加したときの分配部41及びＯＲゲート42が示されている。すなわち、分配数が増加した場合には、分配部41での分配数が増加し、ＯＲゲート42に入力する初期出力側に設けた入力端子の数が増加することになる。
【００６３】
かくして、図４に示すようにスキップキューブ計算回路４は、回路シミュレーション時に、例えば入力パターンとして[１，１，０]が入力された場合、シミュレーション信号ｘ（１）、ｙ（１）及びｚ（０）が入力端子から入力される。これによりスキップキューブ計算回路４は、シミュレーション信号ｘ（１），ｙ（１）に基づいてアンドブロック20aからシミュレーション信号ａ（１）が出力され、このシミュレーション信号ａ（１）が分配ブロックを介してシミュレーション信号ａ´´（１）としてインバータブロック30の入力端子に出力されるとともに、シミュレーション信号ａ´（１）として最終端のアンドブロック20bに出力する。
【００６４】
インバータブロック30は、シミュレーション信号ａ´´（１）を逆の信号値０に変換してシミュレーション信号ｂ（０）として、アンドブロック20cに出力する。アンドブロック20cは、入力されたシミュレーション信号ｂ（０），ｚ（０）に基づいてシミュレーション信号ｃ（０）を生成し、これを最終端のアンドブロック20bに出力する。最終端のアンドブロック20bは、シミュレーション信号ａ´（１）、ｃ（０）に基づいてシミュレーション信号ｆ（０）を出力する。
【００６５】
このようにしてスキップキューブ計算回路４は、検証対象回路10と同じ回路シミュレーション処理を実行し得、検証対象回路10のシミュレーション解析を行ったときと同じ入力パターンに対する出力値を算出し得るようになされている。
【００６６】
次に、スキップキューブ計算回路４は、スキップキューブ算出処理に移行する。ここで、最終端のアンドブロック20bに設けられた伝搬フラグ算出用の入力端子には、信号値１の伝搬フラグ信号ｆp（１）が入力される。
【００６７】
ここで伝搬フラグについて定義すると、入力パターンＶに対する配線における出力ｗの伝搬フラグｗpv∈[０，１]は、配線におけるスキップキューブＡv（ｗ）が初期出力まで伝搬する場合には信号値１、それ以外の場合には信号値０とする。すなわち、回路シミュレーション時にアンドブロック20bの出力端子から出力される信号値「１」は不変なものであり、信号値が「１」又は「０」であるか不明ではないことから、この場合、伝搬フラグの信号値を「１」とするように定義する。
【００６８】
一方、回路シミュレーション時にアンドブロック20bの２つの入力端子は、その出力端子が信号値「０」であることから、入力端子の信号値が少なくとも何れかが信号値「０」であればよく、この場合、伝搬フラグは任意に選択した一方の信号値を「１」として他方を「０」とする。ここで伝搬フラグの信号値を「０」とした場合には、回路シミュレーション時の信号値が「０」又は「１」のいずれも選択可能なことを表している。このようにして、スキップキューブ４は、回路シミュレーション時における初期入力側へ向って伝搬フラグを順次計算し得るようになされている。
【００６９】
アンドブロック20b、伝搬フラグ信号ｆp（１）が入力されると、伝搬フラグ信号ｆp（１）と、シミュレーション信号ａ´（１）、ｃ（０）とに基づいて伝搬フラグ信号ａp´（１）を出力し、これを一方の出力端子から分配ブロック40に出力する。また、これと同時にアンドブロック20bは、伝搬フラグ信号ｆp（１）と、シミュレーション信号ａ´（１）とに基づいて伝搬フラグ信号ｃp（１）を出力し、これを他方の出力端子から他のアンドブロック20cに出力する。
【００７０】
他のアンドブロック20cは、伝搬フラグ信号ｃp（１）が入力されると、伝搬フラグ信号ｃp（１）と、シミュレーション信号ｂ（０）、ｚ（０）とに基づいて伝搬フラグ信号ｂp（１）を出力し、これを一方の出力端子からインバータブロック30に出力する。これと同時にアンドブロック20cは、伝搬フラグ信号ｃp（１）と、シミュレーション信号ｂ（０）とに基づいて伝搬フラグ信号ｚp（０）を出力し、これを他方の出力端子から最終的な信号値０として得る。
【００７１】
一方、インバータブロック30は、伝搬フラグ信号ｂp（１）を変換せずに、そのまま伝搬フラグ信号ａp´´（１）として分配ブロック40に出力する。分配ブロック40は、伝搬フラグ信号ａp´´（１）と、伝搬フラグ信号ａp´（１）とに基づいて伝搬フラグ信号ａｘp（１）をアンドブロック20aに出力する。
【００７２】
アンドブロック20aは、伝搬フラグ信号ａｘp（１）と、シミュレーション信号ｘ（１），ｙ（１）とに基づいて伝搬フラグ信号ｘp（１）を出力し、これを一方の出力端子から最終的な信号値１として得る。これと同時にアンドブロック20aは、伝搬フラグ信号ａｘp（１）と、シミュレーション信号ｘ（１）とに基づいて伝搬フラグ信号ｙp（１）を出力し、これを一方の出力端子から最終的な信号値１として得る。かくして、最終的な伝搬フラグは[１，１，０]となり、入力パターン[１，１，０]に対応した伝搬フラグが算出される。
【００７３】
このようにして全ての伝搬フラグを算出した後、初期出力ｆにおけるスキップキューブは以下の数４の定理で算出する。
【００７４】
【数４】
2009294738.tif 000008
【００７５】
ここで、Ｖｉはｉ番目の初期入力の信号値を示し、Ｐｉをｉ番目の初期入力の伝搬フラグとする。かくして、この実施の形態の場合、入力パターン[１，１，０]に対応したスキップキューブは[１，１，―]となる。
【００７６】
以上のスキップキューブ算出処理についてまとめると、アンドブロック20、インバータブロック30及び分配ブロック40は、各論理ブロック間の配線が配線対となり、当該配線対のうち一方が信号線であって、他方が伝搬フラグ線である。
【００７７】
また、各配線の伝搬フラグは初期出力から初期入力に向って計算する。そして、２つの入力端子を有する論理ブロックについて伝搬フラグの計算方法を示すと、下記の表３のようになる。
【００７８】
【表３】
2009294738.tif 000009
【００７９】
（３）投機的送信処理
次に、投機的送信処理によるコンピュータ２及び回路検証装置３間における通信の最適化について説明する。本発明において、回路シミュレーション処理及びスキップキューブ計算処理をハードウェア化したことでその部分での処理が高速化しても、コンピュータ２及び回路検証装置３間の通信遅延による通信時間が加算されることで、処理時間が全体として遅くなってしまう可能性もある。
【００８０】
そこで、このような場合を考慮して本発明では、コンピュータ２及び回路検証装置３間において１度に送るデータ量を大きくして通信回数を減らすことにより、コンピュータ２及び回路検証装置３間における通信の最適化を図るようになされている。
【００８１】
具体的に本発明による回路検証システム１は、１パターンの入力パターンに対してその都度、コンピュータ２及び回路検証装置３間で通信を行うのではなく、予め決められた複数パターンの入力パターン群をコンピュータ２で生成する。コンピュータ２は、これら複数の入力パターンの集合を１回の通信によって回路検証装置３へ投機的に一括して送信し、ハードウェアたる回路検証装置３においてこれら複数の入力パターン毎にスキップキューブの計算処理を個別に実行した後、当該入力パターンと同じ数のスキップキューブの集合をコンピュータ２へ投機的に一括して送信する。
【００８２】
これにより回路検証システム１では、１パターンの入力パターンを生成する毎にその都度、回路検証装置３との通信することを回避でき、１回の通信あたりのオーバヘッドが非常に大きい場合でも、通信回数を減らすことにより、従来に比してこの通信オーバヘッドによる問題を解決することができる。
【００８３】
ところで、この回路検証システム１では、この投機的送信手法の問題点として、多くの入力パターンが他の入力パターンによるスキップキューブに含まれることから、スキップキューブの計算処理を実行することが無駄になってしまう可能性がある。しかしながら、この点について実験した結果、投機的送信手法が有効であることが分かった。
【００８４】
ここで実験としては、１６×１６ビットの乗算器の下位８ビットの等価性検証を例題とし、通信手段としてＵＤＰ／ＩＰを用いてコンピュータ２と回路検証装置３とを接続し、入力パターンの数と通信回数との関係について調べた。毎回の通信あたりＮＳ個の入力パターンを送信する時に必要となる通信回数ＮＣを図５に示す。図５に示すように、この実験結果から、投機的な入力パターンの送信によって通信回数が削減できることが分かった。また、生成された入力パターンの総数ＮＶ＝ＮＣ×ＮＳについて調べたところ、図６に示すような結果が得られた。これにより、ＮＳ＝１０００程度まで投機的な入力パターンの送信が有効であることが確認できた。また、１つの入力パターンあたりの計算に２５マイクロ秒、１回の通信に１ナノ秒必要とした場合の、実行時間の見積もりについても調べたところ、図７に示すような結果が得られた。これらの結果より、ＮＳ＝１０００付近が最適であると分かった。この実験結果から、入力パターンの投機的な一括送信によって通信オーバヘッドを格段的に削減することが可能であることが確認できた。
【００８５】
（４）スキップキューブ計算回路内蔵型ＦＰＧＡ
図８（Ａ）に示すように、回路検証装置３には、プログラムにより回路構成を自在に変更し得るＦＰＧＡ50が設けられている。このＦＰＧＡ50は、複数の回路セル51と配線ブロック52をチツプ上に規則的に配列した構成でなり、回路セル51及び配線ブロック52の内部には回路の電気的な接続又は非接続をプログラムし得るデバイスが多数配置されており、これによりこれらのデバイスをプログラムすることによって回路構造を自由に変更することができるようになっている。
【００８６】
実際上、このＦＰＧＡ50の回路セル51には、ルックアップテーブル（Look Up Table：ＬＵＴ）55と、スキップキューブ計算用回路部56とが設けられており、スキップキューブ計算用回路部56においてアンドブロック20、インバータブロック30及び分配ブロック40と同じ演算処理を実行し得るようになされている。
【００８７】
ここで、ＦＰＧＡ50には、ＡＮＤゲート11，12，14をアンドブロック20に置き換えるためのプログラムと、インバータ13をインバータブロック30に置き換えるためのプログラムと、分配部15を分配ブロック40に置き換えるためのプログラムとからなるスキップキューブ回路変換プログラムが予め記憶されている。
【００８８】
そして、図８（Ｂ）に示すように、回路検証装置３には、ユーザが所望する検証対象回路10を備えるスキップキューブ計算回路４の回路構造に変更する場合、ＦＰＧＡ50の回路構造を当該検証対象回路10に変更するプログラムが入力される。
【００８９】
これにより回路検証装置３は、予め記憶しているスキップキューブ回路変更プログラムと自動合成し、例えばＡＮＤゲート11，12，14をアンドブロック20に置き換え、インバータ13をインバータブロック30に置き換え、分配部15を分配ブロック40に置き換えてＦＰＧＡをスキップキューブ計算回路４の回路構造に変更させるＦＰＧＡ構成データＤ１を生成し、これをＦＰＧＡ50に送出する。
【００９０】
そして、ＦＰＧＡ50は、ＦＰＧＡ構成データＤ１を受け取ると、当該ＦＰＧＡ構成データＤ１に基づいて各回路セル51をアンドブロック20、インバータブロック30又は分配ブロック40に自動的に変更して配線ブロック52でこれら回路セル51を電気的に接続又は非接続してスキップキューブ計算回路４を自動的に形成し得るように構成されている。
【００９１】
この点について、図８（Ｂ）に示すように、従来のＦＰＧＡにおいては、回路シミュレーションを実行し得る検証対象回路形成用のプログラム61と、スキップキューブを計算するスキップキューブ計算回路形成用のプログラム62とをその都度それぞれ個別に作成し、これら２つのプログラムを自動合成してＦＰＧＡ構成データＤ２を生成する必要があった。
【００９２】
これに対して、本発明のＦＰＧＡ50は、回路シミュレーションを実行し得る検証対象回路に変更するプログラムを入力するだけで、自動的にスキップキューブを計算し得るスキップキューブ計算回路４に変更でき、スキップキューブ計算回路４の回路構造に変更するためのプログラム作成が不要となる分、回路形成時の手間を省くことができる。
【００９３】
因みに、この実施の形態の場合において、例えば４入力ゲートの伝搬フラグ(表４中ｐ−ｆｌａｇと記載)の計算方法を示すと、その計算結果は下記の表４のようになる。
【００９４】
【表４】
2009294738.tif 000010
【００９５】
この場合、スキップキューブ計算用回路部は、８ビットのメモリを内蔵しており、各２ビットが各入力の支配値「０」、「１」、「−」を保持する。因みに、この実施の形態の場合では、４入力ＬＵＴを用いたが、本発明はこれに限らず、例えば５入力ＬＵＴや、この他種々の基本論理ブロックに対しても同様に適用できる。そして、この場合、ＦＰＧＡ内の各配線は、配線対に置き換えられ、一方が信号線であり、他方が伝搬フラグ線となる。
【００９６】
また、このアーキテクチャに対するコンパイルについては、ＦＰＧＡのものとほぼ同じものを使用できる。この場合、回路シミュレーションを実行するための論理回路は４入力ＬＵＴのネットリストにマッピングされる。各ＬＵＴに対して、各入力の支配値が解析され、スキップキューブ計算用回路部中にプログラムされ得る。因みに、この場合、４入力ＬＵＴに対してスキップキューブ計算用回路部は比較的小さくなり、論理回路部分の面積が２倍弱となるものの、配線数が倍になるため、ＦＰＧＡ全体としては面積効率が半分程度となる。
【００９７】
因みに、スキップキューブ計算用回路部は、例えばＡＮＤゲートやインバータ、ＯＲゲート等の各種回路素子が電気的に接続されて形成されたアンドブロック、インバータブロック及び分配ブロックが、それぞれ個別に設けられ、これら物理的な論理回路を自動的に選択するようにしてもよい。
【００９８】
（５）動作及び効果
以上の構成において、入力パターン生成装置としてのコンピュータ２では、入力パターン生成プログラムを不揮発性メモリ上で実行し、入力パターン生成処理を行うことにより複数の入力パターンを生成する。
【００９９】
回路検証装置３では、生成された複数の入力パターンをコンピュータ２から図示しない取得手段を介して受信すると、各入力パターンに基づいて初期入力側から初期出力側へ向けて信号値を求めてゆき、ＡＮＤゲート11，12，14やインバータ13等の各論理ゲート間の接続関係を検証するための回路シミュレーションを、シミュレーション用ハードウェアモジュールとしてのスキップキューブ計算回路で実行する。
【０１００】
また、回路検証装置３では、回路シミュレーションを実行し終えると、次にスキップキューブ計算処理を実行し、前記出力側から前記入力側へ向けて伝搬フラグを算出してゆく。これにより、回路検証装置３では、回路シミュレーションの結果である出力値が同じになり、当該回路シミュレーションを行う必要がない入力パターンの集合であるスキップキューブを、スキップキューブ計算用ハードウェアモジュールとしてのスキップキューブ計算回路４で実行する。
【０１０１】
かくして、回路検証装置３では、各入力パターン毎にスキップキューブを算出して、算出した複数のスキップキューブのうち、同じ数値のスキップキューブを破棄し、異なる数値からなる全てのスキップキューブをコンピュータ２に送信する。
【０１０２】
このように本発明の回路検証システム１では、本質的に並列性が高い回路シミュレーションとスキップキューブの計算とを、ハードウェア化したスキップキューブ計算回路４によって実行するようにしたことにより、これら回路シミュレーション及びスキップキューブの計算をほぼ並列に実行できるようになり、高速にスキップキューブを計算できる。
【０１０３】
そして、回路検証システム１では、コンピュータ２と回路検証装置３とを無線で通信可能に接続し、コンピュータ２が複数の入力パターンを一括して回路検証装置３へ送信し、回路検証装置３から各入力パターン毎に算出した複数のスキップキューブを一括して受信する。また、回路検証装置３では、複数の入力パターンをコンピュータ２から一括して受信し、スキップキューブ計算用ハードウェアモジュールで算出した複数のスキップキューブをコンピュータ２へ一括して送信する。
【０１０４】
かくして、検証システム１では、１パターンの入力パターンを生成する毎にその都度、コンピュータ２と回路検証装置３との間で通信することを回避でき、１回の通信あたりのオーバヘッドが非常に大きい場合でも、通信回数を減らすことにより、全体として検証の高速化を図ることができる。
【０１０５】
さらに、回路検証装置３では、供給されるプログラムデータたるＦＰＧＡ構成データに基づいて内部の回路構造を変更し得るＦＰＧＡによってスキップキューブ計算回路４を形成するようにしたことにより、検証回路設計に余分な設計コストが発生することを回避でき、また全体的な検証時間を短縮化させることができる。
【実施例】
【０１０６】
次に、実施例である本発明の回路検証システムと、回路シミュレーション処理及びスキップキューブ計算処理をソフトウェアで実行する比較例たるコンピュータとについて処理時間を比較する実験を行った。なお、実施例である本発明の回路検証システムは、入力パターンの生成をコンピュータで実行し、回路シミュレーション処理とスキップキューブ計算処理を回路検証装置で実行するようにした。
【０１０７】
また、実施例及び比較例のコンピュータは、ＣＰＵがＣｏｒｅ２Ｄｕｏ ２．０ＧＨｚ、メモリが１ＧＢの主記憶部を持つコンピュータを用い、当該コンピュータ上のＬｉｎｕｘで実行した。また、実施例においてハードウェア部分となる検証対象装置はＰｏｗｅｒＰＣプロセッサを内蔵したＸｉｌｉｎｘ Ｖｉｒｔｅｘ―ＩＩ Ｐｒｏ ＦＰＧＡを用いた。そして、コンピュータと検証対象装置間の通信はイーサネット(登録商標)上のＵＤＰ／ＩＰを用い、ＦＰＧＡ内蔵プロセッサがこれを制御するようにした。
【０１０８】
例題として１６×１６ビットの乗算器を用いて、出力の下位ｎビットの等価性検証を行った。また、比較例については、従来において説明した準形式的検証手法をソフトウェアのみで実装し、同じ等価性検証試験を行った。ソフトウェアのみの比較例と、ハードウェア・ソフトウェア(ＨＷ／ＳＷ)協調実行による実施例との各高速化の結果は、表５のようになった。
【０１０９】
【表５】
2009294738.tif 000011
【０１１０】
この実験結果から、実施例の回路検証システムは比較例に対して約７倍の高速化を実現できたことを確認した。
【０１１１】
なお、本発明は、本実施形態に限定されるものではなく、本発明の要旨の範囲内で種々の変形実施が可能であり、例えば、コンピュータ２と回路検証装置３とを有線で通信可能に接続するようにしてもよい。
【０１１２】
また、上述した実施の形態においては、ＡＮＤゲート11，12，14はアンドブロック20に置き換えられ、インバータ13はインバータブロック30に置き換えられ、分配部15は分配ブロック40に置き換えられるようにした場合について述べたが、本発明はこれに限らず、オア回路があるとき、当該オア回路をオアブロックに置き換えるようにしてもよい。
【０１１３】
この場合、図９に示すように、オアブロック60は、２つの入力端子と、１つの出力端子とを有する第１のＯＲゲート61が設けられており、回路シミュレーション時、この第１のＯＲゲート61に入力された２つの信号値ａ，ｂに基づいて１つの出力ｗを出力し得る。
【０１１４】
これに加えて、このオアブロック60は、回路シミュレーション後に実行されるスキップキューブ算出時、回路シミュレーション時とは逆の初期出力側から初期入力側へ向って信号値を求めてゆき伝搬フラグａp，ｂpを算出し得るようになされている。
【０１１５】
オアブロック60は、伝搬フラグａp，ｂpを求めるための回路構成として、第１のＯＲゲート61の一方の入力端子が、第２のＯＲゲート62の一方の入力端子に接続されているとともに、インバータ63を介して第１のＡＮＤゲート64の一方の入力端子にも接続されている。
【０１１６】
また、オアブロック60は、第１のＯＲゲート61の他方の入力端子がインバータ65を介して第２のＯＲゲート62の他方の入力端子に接続され、この第２のＯＲゲート62の出力端子が第２のＡＮＤゲート66の一方の入力端子に接続されている。第１のＡＮＤゲート64及び第２のＡＮＤゲート66は、それぞれ２つの入力端子と、１つの出力端子とを有し、スキップキューブ算出時、当該第１のＡＮＤゲート64及び第２のＡＮＤゲート66の他方の各入力端子に信号値ｗpが入力され得る。
【０１１７】
これによりオアブロック60は、第２のＡＮＤゲート66に入力された信号値ｗpと、回路シミュレーショ-ン時に得た信号値ａ，ｂとに基づいて第２のＡＮＤゲート66の出力端子から伝搬フラグａpを出力し得る。また、オアブロック60は、第１のＡＮＤゲート64に入力された信号値ｗpと、回路シミュレーショ-ン時に得た信号値ａとに基づいて第１のＡＮＤゲート64の出力端子から伝搬フラグｂpを出力し得る。
【０１１８】
かくして、ＯＲゲートを含む検証対象回路では、ＯＲゲートをオアブロックに置き換えることにより、回路シミュレーションとスキップキューブの計算とを実行し得るスキップキューブ計算回路を形成できる。
【図面の簡単な説明】
【０１１９】
【図１】回路検証システムの全体構成を示す概略図である。
【図２】検証対象回路の回路構成を示すブロック図である。
【図３】アンドブロック、インバータブロック及び分配ブロックの回路構成を示すブロック図である。
【図４】シミュレーション計算回路の回路構成を示すブロック図である。
【図５】投機的入力パターン生成による通信削減を示すグラフである。
【図６】入力パターンの総数を示すグラフである。
【図７】実行時間見積もりを示すグラフである。
【図８】ＦＰＧＡの詳細説明に供する概略図である。
【図９】オアブロックの回路構成を示すブロック図である。
【符号の説明】
【０１２０】
１  回路検証システム
２  コンピュータ（入力パターン生成装置）
３  回路検証装置
４  シミュレーション計算回路
【図２】
2009294738.tif 000012
【図３】
2009294738.tif 000013
【図４】
2009294738.tif 000014
【図５】
2009294738.tif 000015
【図６】
2009294738.tif 000016
【図７】
2009294738.tif 000017
【図９】
2009294738.tif 000018
【図１】
2009294738.tif 000019
【図８】
2009294738.tif 000020