(57)【要約】【課題】二分決定グラフ（BDD）を用いるアルゴリズムを使用する回路設計法において、区分けのスケジューリングに起因して非効率的になってしまう問題点を軽減ること。【解決手段】一形態では、マルチスレッド到達可能性アルゴリズムのための方法は、分析する回路の状態空間を複数のパーティションに区分けするステップと、スレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップとを有する。スレッドはパーティションの到達可能性分析を互いに並列に実行する。本方法は、早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップを有する。【選択図】図１
2007095029.tif 000002
【特許請求の範囲】
【請求項１】
マルチスレッド到達可能性アルゴリズムのための方法であって、
分析する回路の状態空間を複数のパーティションに区分けするステップと、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップと、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップと、
を有することを特徴とする方法。
【請求項２】
２以上のスレッドが、共用メモリを使用する
ことを特徴とする請求項１記載の方法。
【請求項３】
前記早期通信アルゴリズムに従って、第１のパーティションが最低固定点に到達した後に、パーティションの第１のものが、第１のパーティションの１以上の到達した状態をパーティションの１以上の第２のものに通知する
ことを特徴とする請求項１記載の方法。
【請求項４】
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの現在のイメージ計算をリスタートし、第２のパーティションでの到達可能性分析を促進する
ことを特徴とする請求項３記載の方法。
【請求項５】
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり且つアイドルであり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの到達可能性分析を再開し、通知された状態を組み入れることで少なくとも第２のパーティションでの到達可能性に関する処理を更に進める
ことを特徴とする請求項３記載の方法。
【請求項６】
実行用に媒体中にエンコードされた、マルチスレッド到達可能性アルゴリズムのための論理装置であって、
分析する回路の状態空間を複数のパーティションに区分けするステップと、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップと、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップと、
をコンピュータに実行させる論理装置。
【請求項７】
２以上のスレッドが、共用メモリを使用する
ことを特徴とする請求項６記載の論理装置。
【請求項８】
前記早期通信アルゴリズムに従って、第１のパーティションが最低固定点に到達した後に、パーティションの第１のものが、第１のパーティションの１以上の到達した状態をパーティションの１以上の第２のものに通知する
ことを特徴とする請求項６記載の論理装置。
【請求項９】
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの現在のイメージ計算をリスタートし、第２のパーティションでの到達可能性分析を促進する
ことを特徴とする請求項８記載の論理装置。
【請求項１０】
マルチスレッド到達可能性アルゴリズムのためのシステムであって、
分析する回路の状態空間を複数のパーティションに区分けする手段と、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行する手段と、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進する手段と、
を有することを特徴とするシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は一般に回路設計に技術分野に関連し、特にマルチスレッド到達可能性(multithreaded  reachability)に関する。
【背景技術】
【０００２】
区分けされた二分決定グラフ(BDD:  binary  decision  diagram)に基づくアルゴリズムは、BDDに基づく回路検査でのメモリの急増を減らすためにしばしば使用される。そのようなアルゴリズムは処理用の区分けを計画することに関する問題の影響を受けやすいので、そのようなアルゴリズムはしばしば非効率的になる。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明の課題は、回路設計に関する欠点及び問題点を軽減又は解消することである。
【課題を解決するための手段】
【０００４】
一形態では、マルチスレッド到達可能性アルゴリズムのための方法は、分析する回路の状態空間を複数のパーティションに区分けするステップと、スレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップとを有する。スレッドはパーティションの到達可能性分析を互いに並列に実行する。本方法は、早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップを有する。
【発明を実施するための最良の形態】
【０００５】
本発明の特定の実施例は１以上の技術的恩恵をもたらす。一例として、特定の実施例はマルチスレッド到達可能性アルゴリズムを提供し、そのアルゴリズムは処理用の区分けをスケジューリングすることに関する問題を減らす又は回避しつつ、状態空間中の区分けされた経路における潜在的な並列性(latent  parallelism)を増やす。特定の実施例は、従来の到達可能性アルゴリズムよりも及び区分けされた手法よりもかなり高速に動作するマルチスレッド到達可能性アルゴリズムを提供する。そのような形態は並列フレームワークを用いて実行される場合でさえも更なるゲインをもたらす。特定の実施例ではパーティション間の早期通信、パーティション間の部分的な通信又は双方は、１以上のパーティションが過剰に困難になって処理できない場合でさえも（もしかするとメモリ急増の結果かもしれない）、１以上のパーティションにおける状態空間中の経路の継続性を促す。
【０００６】
特定の実施例は回路検査結果を提供し、その回路は、順序付BDD(OBDD:  ordered  BDD)又は区分けされたOBDD(POBDD:  partitioned  OBDD)に基づくアルゴリズムよりも多くの場合に良好であり、唯１つのプロセッサで動作する場合でさえ良好である。特定の実施例は、BDDに基づく従来の手法よりもかなり高速に誤りのある状態を発見することを促進する。特定の実施例は、従来の到達可能性アルゴリズムよりもかなり高速に誤りのある状態を発見することを促進する。特定のアルゴリズムは、POBDDに基づく一層ロバストな、標準的な、シーケンシャルな到達可能エイアルゴリズムをもたらす。特定の実施例は、POBDDに基づく標準的な到達可能性アルゴリズムにおける純粋な並列処理性を上回る並列処理の増進性を促す。
【０００７】
特定の実施例は上記の技術的利点の全部又は一部をもたらしてもよいし、全くもたらさなくてもよい。特定の実施例は１以上の他の技術的利点をもたらし、それらは本明細書、特許請求の範囲及び図面から当業者に明白になるであろう。
【０００８】
本発明及びその特徴や利点に関する完全な理解を更に期するため、添付図面に関する説明が以下になされる。
【０００９】
以下、本発明の実施例によるシステム、方法及び論理装置が説明される。この場合において、論理装置なる語は、ソフトウエアで構成される論理プログラムや、ハードウエアで構成される論理回路を含む概念である。
【実施例１】
【００１０】
図１はマルチスレッド到達可能性に関するシステム例を示す図である。システムは回路１２を含む。システム１０は以下に説明されるように回路１２での到達可能性分析を実行するための到達可能性データ１６及び到達可能性モジュール１４も含む。１以上のリンクはシステム１０の要素を互いに結合する。非限定的な一例として、リンクは適切ならば１以上の回路板の１以上のワイヤ、１以上の内部又は外部バス、１以上のローカルエリアネットワーク(LAN)、１以上のメトロポリタンエリアネットワーク(MAN)、１以上の広域ネットワーク(WAN)、インターネットの１以上の一部分又はそれらの２以上のリンクの組み合わせを含んでよい。
【００１１】
回路１２は、例えばハードウエアに関する１以上の特定の仕様に従ってハードウエアが適切に動作得るか否かを判定するために、検査用のハードウエア又はハードウエアに関する論理的な若しくは他の表現を含む。非限定的な一例として回路１２は、特定の機能をもたらすために配置された及び互いに結合されたゲート、カウンタ、インバータ、バッファ及び他の回路要素のような回路要素を含んでよい。別の例として、回路１２はそのような要素の論理的な又は他の表現を含んでもよい。回路１２は何百万もの回路要素を含むかもしれない。特定の機能を用意するために、回路１２は１以上の特性を備えなければならない。回路１２はそのような特性を何百万も含むことを要する。特定の実施例では、１以上の論理的表現が回路１２の特性を記述する。回路１２の「特性(property)」に関するものは、回路１２の論理的に表現可能な状態、特徴、挙動又は動作或いは回路１２の別の特性を必要に応じて包含してよい。「状態(state)」に関するものは適切ならば回路１２の１以上の特性を包含してもよい。
【００１２】
到達可能性モジュール１４は、１以上のリンクを介して回路１２にアクセスし且つ回路１２で到達可能性分析を実行する、ハードウエア、ソフトウエア、組み込み済み論理要素又はそれらの２以上の要素の組み合わせを含む。特定の実施例では、回路１２で到達可能性分析を実行することは、以下に説明されるように、回路の状態空間を複数のパーティションに分割すること及び複数のスレッドを用いてそのパーティションについて到達可能性分析を実行することを含む。到達可能性モジュール１４は、回路１２で到達可能性分析を実行する複数のスレッド１８を含む。各スレッド１８は到達可能性分析全体の一部分を実行する。スレッドに関するものは、プロセスの１以上の或るインスタンスと並列的にプロセッサで実行可能な別のプロセスのインスタンスを必要に応じて含む。到達可能性データ１６は、到達可能性分析の特定のパラメータを指定するデータ及び他のデータを含み、そのデータは特定の実施例で到達可能性モジュール１４が回路１２に関する到達可能性分析を実行するのに使用するデータである。特定の実施例では、１以上のコンピュータシステムは、到達可能性モジュール１４、到達可能性データ１６及びそれら双方に対する１以上のユーザアクセスを用意する。非限定的な一例として、コンピュータシステムは到達可能性モジュール１４及び到達可能性データ１６を含み、到達可能性モジュール１４、到達可能性データ１６又は双方に入力を提供したりそれらから出力を受信するためにユーザはそのコンピュータシステムにアクセスする。
【００１３】
到達可能性分析は１以上の有限状態マシーン（FSM:  finite  state  machine）の幅優先走査(breadth-first  traversal)を含む。到達可能性分析のアルゴリズムは、一群の初期状態及び遷移関係（TR）を入力とし、遷移関係は現在の各状態から次に到達可能な状態を関係づける。１以上の最低固定点(LFP:  least  fixed  point)計算は一群の到達可能な状態を生成する。LFP計算は、イメージ計算が固定点に到達するまで実行される一連のイメージ計算を含む。TRは接続可能に(conjunctively)一群のクラスタに区分けされ、イメージ計算中の条件付け(qualification)を支援するために、条件付けスケジュールが区分けされたTRに関連付けられる。
【００１４】
区分けされた順序付二分決定グラフ（POBDD）を利用することは、１以上の到達可能性分析に基づいて回路１２の検査を改善する。以下はPOBDDを用いる１以上の到達可能性分析に基づく回路１２の検査を実行するアルゴリズム例である。
【００１５】
【数１】
2007095029.tif 000003
上記のアルゴリズムは本質的には、パーティションの中でLFPに到達するまで、各パーティションｉの中で可能な限り多くのイメージ計算ステップを実行する。そしてこのアルゴリズムは、各パーティションの中で生じる及びそれらから導出する遷移を考察することで、２以上のパーティションを互いに同期させる。通信に関するものは、これらパーティション間のイメージ計算及び２分決定グラフ(BDD)の以後の遷移（１以上の第１パーティションから１以上の第２パーティションへの遷移）を必要に応じて含んでよい。上記のアルゴリズムは厳密な幅優先走査（BFS）経路を使用していない。そのアルゴリズムは、個々のパーティションにローカルなBFSを実行し、或るパーティションから別のものへの遷移に起因する状態を加えるように同期する。かくてこのアルゴリズムは、状態空間の個々のパーティションのどれが幅優先法で独立にトラバースされるかに従って領域ベースのBFSを使用する。ローカルなLFP計算に関するものは、１以上のパーティションにおける１以上のLFP計算を必要に応じて包含してよい。
【００１６】
並列的検査に関する従来の手法は、分散された到達可能性分析を当てしており、その分析は分散されたフレームワーク及び分散されたメモリを有する並列的環境における状態空間の古典的なBFS経路を含む。これに対して本発明の特定の実施例は、共有メモリモデルとスレッド１８間の高速通信とを使用し、並列処理特性を促す。特定の実施例では、（例えば、抽象化のような）変換が回路１２での到達可能性分析の前に回路１２に適用されてもよい。そのような形態はBDDベースの到達可能性分析を改善し、従って別の検査手法に置換するのではなく、補完しようとするものである。
【００１７】
特定の実施例は、より少ない演算負担でより新たな状態に到達する。標準的なPOBDDベースの到達可能性アルゴリズムは、より多くの状態に速やかに到達するように、ローカルなLFP計算の効率に配慮する。しかしながらどのローカルLFP計算が容易であるかは事前には未知である。通常的にはそれらに到達する複数の経路が存在することが多い。ローカルLFPを通じて又は別のパーティションからの通信を通じてこれらは到達可能である。一群の状態は通信により一層容易に到達可能になる。パーティションが早期に終了し、通信を通じて新たな状態を他のパーティションに与える場合に、新たに計算された一群の状態は受信パーティションにおけるローカルLFP計算を簡易にする。従ってシーケンシャルPOBDDベースの到達可能性アルゴリズムのパフォーマンスは、パーティションが処理される順序に依存すべきである。これはスケジューリングの問題である。シーケンシャルな環境で簡易な計算(パーティション)を発見するために貪欲戦略法(greedy  strategy)を使用することは困難である。しかしながらこの手法をマルチスレッド環境で実行することは比較的容易である。様々なパーティションの間で演算リソースを分割するラウンドロビン法は、簡易なパーティションが簡易でないパーティションより先に終了することを保証する。明らかに、複数のスレッドを用いる到達可能性アルゴリズムで並列処理性を増やすことは、より簡易な計算の貪欲な発見を可能にし、到達可能な状態を速やかに蓄積することを支援する。従って特定の実施例はマルチスレッド（並列）アプローチを使用し、並列処理性を改善する。
【００１８】
上記のPOBDDベースのアルゴリズムは並列化可能である。それらの通信と組み合わせられる各パーティションのローカルなLFP計算は、パラレルに処理されてよい。特定の実施例は全てのパーティションがそれらのローカルLFP計算及び通信の終了するのを待機し、通知された状態を適切なパーティションに転送し始める。しかしながら、経験的に、上述のアルゴリズムのこの簡易な並列化は、限定的な並列化をもたらす。これは以下の理由に起因する：
１．BDD計算の大きな変動。或るパーティションが非常に良好な変数順序を有していた場合又は表現する関数が非常に制御しやすかったならば、その対応する状態空間の表現はコンパクトになる。従ってそのパーティション内のイメージ計算は速く；そのようなパーティションは「容易な(easy)パーティション」である。一方、パーティションが良好な変数を発見していなかった場合又は対応する関数が非常に難しかった場合には、大きなBDDの並べ替えで立ち往生し、処理が進まない。そのようなパーティションは「困難な(hard)パーティション」である。多くの場合に、各パーティションに関するローカルLFP計算の実行時間に大きな変動がある。そのような場合に、全ての容易なパーティションは困難なパーティションのイメージ計算終了を待機し、これは並列処理性を減殺してしまう。
【００１９】
２．ローカルLFP計算の深さ。減殺された並列処理性に関する別の理由は、ローカルLFP計算の深さ(depth)が各パーティションでかなり変動するかもしれないことである。この場合、浅い深さのパーティションは早く終了するが、より深い深さのパーティションは終了するまでに長くかかる。これは結果的にアイドルスレッド(idle  thread)をもたらし、並列性を減殺してしまう。
【００２０】
実際には、多数のパーティションが少数の困難なパーティションを待機するかもしれない。この問題に対処するため、特定の実施例は以下の発見的方法を利用し、並列処理性を改善する：
１．早期通信。最低固定点に到達した後に状態を別のパーティションに通知する。
【００２１】
２．部分的通信。アイドルスレッドで部分的な通信を開始する。
【００２２】
或るパーティションがそのローカルLFP計算を終了した後に、特定の実施例は、そのパーティションがその状態を他のパーティションに速やかに通知することを許容する。各パーティションは、それらのローカルLFP計算の間に、通知されたそれらの状態を非同期的に受け入れる。これは簡易なパーティションが以後のローカルLFP計算を（困難なパーティションの終了を待たずに）進行させることを可能にする。従って或る簡易なパーティションから別の簡易なパーティションへの早期通信は、そのようなパーティション全てが固定点に到達するのを可能にする。これはシーケンシャルな区分けされた到達可能性分析では達成困難である。なぜならそのようなスケジューリング情報を得ることは困難だからである。
【００２３】
早期通信の間に新たな状態が通知されると、特定の実施例は、それらの状態を加えた後に目下のイメージ計算をリスタートする。そのような付加は、困難なイメージ計算を場合によってはかなり簡易にすることができる。これは或る通知された状態の結果であり、その状態は、ローカルLFPを用いて受信パーティションで計算する際に困難な状態であったものに対応する状態である。
【００２４】
上記の手法を適用した後に、特定の実施例では、多くのパーティションは他のパーティションが或る状態を通知するのを依然として待機し、それらのローカルLFP計算を継続するようにするかもしれない。これは、全ての簡易なパーティションが、それらのローカルLFPを終了し且つ更に処理を進めるために困難なパーティションからの連絡を要する場合に生じやすい。並列処理性を強化するため、特定の実施例は困難なパーティションの状態空間の部分小空間を利用してアイドルスレッドで通信を開始する。この通信は容易なパーティションに新たな状態を導入する。これは、通知された状態から集まる最低固定点と共に、容易なパーティションが更に処理を進めることを可能にする。直感的にはこれは容易なパーティション間の活動を促そうとする。特定の実施例は、困難なパーティションの状態空間全部ではなく、状態空間の小部分空間の１以上を利用して、通信における演算負担を減らす。この発見的手法は全てのスレッドをビジーに維持しようとし、それにより並列性の改善に寄与する。更にこの発見的手法は、早期通信インスタンスの数を増やす。かくて部分的な通信及び早期通信の結合は、並列処理性を顕著に改善しやすくする。
【００２５】
以下は上記の手法を利用する並列的な到達可能性アルゴリズム例である。
【００２６】
【数２】
2007095029.tif 000004
特定の実施例は、並列的な通信を組み合わせたローカルLFP計算を実行する。パーティション内の全ての計算は専用のスレッドで管理される。各スレッドは他のスレッドから通知される状態を求めてポーリングする。イメージ計算の全マイクロステップ後に、各スレッドは或る関数(ImproveParallelism)を呼び出し、その関数は並列性を改善する２つの発見的方法を実行する。第１の発見的方法は早期通信を行うことである。第１の発見的方法の一部として、その関数は他のスレッドが何らかの状態を現在のスレッドに通知したか否かを検査する。各スレッドで実行されるアップデートサブルーチン及びこの簡易な検査は、早期通信法を実現する。第２の発見的方法は部分通信を行うことである。この発見的方法の一部分として、アクティブなスレッド全体がアイドルスレッドを検査する。アイドルスレッドが発見されたならば、その発見的方法は現在のパーティションからアイドルスレッドに状態空間の小部分を与える。アイドルスレッドは、この状態の部分集合から、アイドルスレッドに関するパーティションへの通信を開始する。
【００２７】
特定の実施例では、マルチスレッド法において、各スレッドがパーティションを管理する。スレッドに関するパーティションに新たな状態が一切通知されなかったならば、そのスレッドはアイドル状態に戻る。スレッドマネジャは、全てのスレッドがアイドルだった場合に全体的な終了フラグ(global  termination  flag)をアサートする。
【００２８】
並列的にいくつものプロセッサを利用すると、シーケンシャルアルゴリズムを上回るゲインをもたらすことがしばしばある。マルチスレッド法はオーバーヘッドを付加するが、利用可能なリソース量を増やしはしない。かくていくつかのマルチスレッド法だけが実行されるのでなく、シーケンシャル法も実行されてよい（おそらくは僅かに悪化する）。しかしながらマルチスレッド法を利用することは、スケジューリングの障害に起因する非効率性を回避できることで、POBDDに加えてOBDD法を用いることを上回る顕著な利得をもたらす。
【００２９】
特定の実施例は、状態の通知を不必要に待機することを回避するので、並列化を少なくとも部分的に改善できる発見的手法を利用する。特定の実施例は、進行中の(active)ローカルLFP計算にて、通知された状態を利用する発見的手法を利用する。これは簡易なパーティションがそれらの間で集めたローカル最低固定点に到達可能にする。従ってこの子定点にエラーがあった場合には、それは速やかに検出される。更にそのエラー状態が困難なパーティションに有った場合には、それは早期通信を用いて速やかに検出される。マルチスレッドの貪欲な性質はエラーのある状態に簡易に到達するパスを発見可能にする。誤り検出はそのような手法を用いてかなり高速になされる。
【００３０】
或る関数に関し、しばしばPOBDDはOBDDよりかなり小さい。従ってスケジューリングの不安定さがマルチスレッド法で改善可能ならば、スレッド法がオーバーヘッドを持つとしても、通過（合格）する場合に、全状態空間走査を他のBDDベースの方法よりも高速に完了する。特定の実施例は、充分な並列性のない深い到達可能性インスタンスを動的に認識し、非常に深い回路に合う通信法を使用し、或いは双方を行い、非常に深い回路に関する並列性を改善する。
【００３１】
非限定的な例として、回路１２の到達可能性分析を考察する。全ての到達可能な状態が計算されることを要し、到達可能性分析は１６個のパーティションを用いて実行され、１６個の各々は別々のスレッドで動作する。図２Ａ−２Ｃは、各スレッドでなされる作業量に関する発見的方法の影響を示すガントチャート例である。各パーティションは水平破線で表現されている。満たされているセグメントは、そのパーティションに関し、計算を実行するための作業時間を表現する。そのようなステージへの到達完了時点での小さなクロスは他のパーティションへの状態通知を示す。ラインの破断は、対応するスレッドがアイドルであること及び別のスレッドから何らかの状態を得るのを待機していることを示す。マルチプロセッサ環境では、これはプロセッサのアイドリングに対応する。しかしながらマルチスレッド環境では、プロセッサは実行する別のスレッドを計画してもよい。総時間は１つのプロセッサで全てのスレッドを実行する作業時間である。これはアイドル時間を含まない。言い換えれば総作業時間ガントチャートにおける全てのセグメントの長さの合計である。
【００３２】
図２Ａは非限定的な例を示し、純粋なマルチスレッドにおける様々なパーティションでの実行計算が可変期間になり、ほとんどのスレッドは他の全てがそれらのローカルパーティションを完了し、通信の準備をするまでアイドル状態にあることを示す。図２Ｂは早期通信の効果を示す例である。各パーティションは、ローカル固定点演算を完了するとすぐに通信する。他のパーティションは、全てのパーティションがそれらのローカルな作業の終了を待つ必要なしに新たな状態を受信する。これは複数のパーティションが同時に探索されることを可能にし、かくて単独のプロセッサでスケジュールされた場合に、総作業（トータルワーク）については、約１２５５から約２１６秒に時間が短縮する。完全な到達可能性を判定するのにより少ない作業時間しか必要としない。しかしながらそのスケジューリングにおいていくつかのスレッドがアイドルである間に依然としてギャップが存在する。図２Ｃはこれらのギャップを埋める部分通信の効果を示す例である。スレッドがアイドルであった場合に、そのスレッドは別のスレッドから何らかの状態を得る。そのような状態はスレッドが或るイメージ計算を（その状態の入手先である）パーティションとは独立に実行することを可能にする。このことは良好な並列的有用性を保証するが、複数のスレッドによって実行される冗長的な作業が生じるので、トータルの時間は単一プロセッサの場合に測定されたように増えるかもしれない。マルチプロセッサの場合には、プロセッサはアイドルにはならずまるまる使用される。共有メモリを利用し、この手法を支援してもよい。
【００３３】
特定の形態は、区分けされたBDDベースの検査方法の有効性をどのようにして増やすかについての問題の解決を促す。その有効性はしばしばスケジューリング問題（即ち、パーティションが走査される相対的な順序）によって妨げられる。特定の実施例はマルチスレッド到達可能性アルゴリズムを使用し、そのアルゴリズムは、複数のパーティション（場合によっては全てでもよい）のラウンドロビン分析を実行することで、スケジューリング問題を賢明に軽減する。更に特定の実施例ではアルゴリズムは区分けされた状態空間走査の並列処理性を増進する。特定の実施例では、容易なパーティションによる早期通信によって可能な限り早期に状態に到達するように集める。良好でない特性に関し、これは誤りのある状態に至る簡易な経路を見出すことになる。合格する場合はスケジューリング問題には重要でないが、そのような特性についても利得がある。特定の実施例は多くの場合に（合格する又は不合格の場合）、標準的な到達可能性アルゴリズムだけでなく区分けされた手法の双方よりもかなり高速である。共有メモリ並列アーキテクチャで評価される場合にはゲインは増進される。
【００３４】
以上本発明を説明するために特定の実施例が使用されてきたが、本発明を説明するために使用された特定の実施例についての変更、置換、変形、代替又は修正の1以上を当業者は理解するであろう。本発明はそのような変更、置換、変形、代替及び修正の全てを特許請求の範囲内に包含する。
【００３５】
以下、本発明により教示される手段が例示的に列挙される。
【００３６】
（付記１）
マルチスレッド到達可能性アルゴリズムのための方法であって、
分析する回路の状態空間を複数のパーティションに区分けするステップと、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップと、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップと、
を有することを特徴とする方法。
【００３７】
（付記２）
２以上のスレッドが、共用メモリを使用する
ことを特徴とする付記１記載の方法。
【００３８】
（付記３）
単一のプロセッサが、２以上のスレッドを実行する
ことを特徴とする付記１記載の方法。
【００３９】
（付記４）
１以上の到達可能性分析の各々が、１以上の有限状態マシーン（FMS）の幅優先走査を含む
ことを特徴とする付記１記載の方法。
【００４０】
（付記５）
１以上の到達可能性分析の各々が、一群の到達可能な状態を生成するための１以上の最低固定点（LFP）計算を含む
ことを特徴とする付記１記載の方法。
【００４１】
（付記６）
LFP計算が、イメージ計算が固定点に到達するまで実行される一連のイメージ計算を含む
ことを特徴とする付記５記載の方法。
【００４２】
（付記７）
前記早期通信アルゴリズムに従って、第１のパーティションが最低固定点に到達した後に、パーティションの第１のものが、第１のパーティションの１以上の到達した状態をパーティションの１以上の第２のものに通知する
ことを特徴とする付記１記載の方法。
【００４３】
（付記８）
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの現在のイメージ計算をリスタートし、第２のパーティションでの到達可能性分析を促進する
ことを特徴とする付記７記載の方法。
【００４４】
（付記９）
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり且つアイドルであり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの到達可能性分析を再開し、通知された状態を組み入れることで少なくとも第２のパーティションでの到達可能性に関する処理を更に進める
ことを特徴とする付記７記載の方法。
【００４５】
（付記１０）
複数のコンピュータシステムが、スレッドを実行する
ことを特徴とする付記１記載の方法。
【００４６】
（付記１１）
実行用に媒体中にエンコードされた、マルチスレッド到達可能性アルゴリズムのための論理装置であって、
分析する回路の状態空間を複数のパーティションに区分けするステップと、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行するステップと、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進するステップと、
をコンピュータに実行させる論理装置。
【００４７】
（付記１２）
２以上のスレッドが、共用メモリを使用する
ことを特徴とする付記１１記載の論理装置。
【００４８】
（付記１３）
単一のプロセッサで実行される
ことを特徴とする付記１１記載の論理装置。
【００４９】
（付記１４）
１以上の到達可能性分析の各々が、１以上の有限状態マシーン（FMS）の幅優先走査を含む
ことを特徴とする付記１１記載の論理装置。
【００５０】
（付記１５）
１以上の到達可能性分析の各々が、一群の到達可能な状態を生成するための１以上の最低固定点（LFP）計算を含む
ことを特徴とする付記１１記載の論理装置。
【００５１】
（付記１６）
LFP計算が、イメージ計算が固定点に到達するまで実行される一連のイメージ計算を含む
ことを特徴とする付記１５記載の論理装置。
【００５２】
（付記１７）
前記早期通信アルゴリズムに従って、第１のパーティションが最低固定点に到達した後に、パーティションの第１のものが、第１のパーティションの１以上の到達した状態をパーティションの１以上の第２のものに通知する
ことを特徴とする付記１１記載の論理装置。
【００５３】
（付記１８）
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの現在のイメージ計算をリスタートし、第２のパーティションでの到達可能性分析を促進する
ことを特徴とする付記１７記載の論理装置。
【００５４】
（付記１９）
第２のパーティションの１つが、第１のパーティションが到達した状態を通知した時に最低固定点に未到達であり且つアイドルであり、
到達した状態の通知に応答して、第２のパーティションが、通知された状態を組み入れ、第２のパーティションでの到達可能性分析を再開し、通知された状態を組み入れることで少なくとも第２のパーティションでの到達可能性に関する処理を更に進める
ことを特徴とする付記１７記載の論理装置。
【００５５】
（付記２０）
複数のコンピュータシステムが、スレッドを実行する
ことを特徴とする付記１１記載の論理装置。
【００５６】
（付記２１）
マルチスレッド到達可能性アルゴリズムのためのシステムであって、
分析する回路の状態空間を複数のパーティションに区分けする手段と、
パーティションの到達可能性分析を互いに並列に実行するスレッドを各パーティションに割り当て、該スレッドに割り当てられたパーティションで到達可能性分析を実行する手段と、
早期通信アルゴリズム及び部分的通信アルゴリズムの１以上を利用して、パーティションの１以上の第１のものからパーティションの１以上の第２のものへ状態を通知し、前記パーティションの第２のものの到達可能性分析を促進する手段と、
を有することを特徴とするシステム。
【図面の簡単な説明】
【００５７】
【図１】マルチスレッド到達可能性に関するシステム例を示す図である。
【図２Ａ】複数のスレッド各々により実行される特定の発見的方法の具体例を示す図である。
【図２Ｂ】複数のスレッド各々により実行される特定の発見的方法の具体例を示す図である。
【図２Ｃ】複数のスレッド各々により実行される特定の発見的方法の具体例を示す図である。
【符号の説明】
【００５８】
１０  システム
１２  回路
１４  到達可能性モジュール
１６  到達可能性データ
１８  スレッド
【図１】
2007095029.tif 000005
【図２Ａ】
2007095029.tif 000006
【図２Ｂ】
2007095029.tif 000007
【図２Ｃ】
2007095029.tif 000008