(57)【要約】【課題】一実施例では、1つ又は複数のグリッドを用いて1つ又は複数の回路を検証する方法は、回路にアクセスする工程と、回路上で1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを生成する工程とを含む。【解決手段】各検証インスタンスは、1つ又は複数のタスクを備える。方法は、複数のノードを含むグリッドにわたってタスク及びシードを分散させる工程、及び、シードを用いて、タスクによってグリッド内のノードで検証のインスタンスを実行する工程も含む。【選択図】図６
2007012062.tif 000002
【特許請求の範囲】
【請求項１】
1つ又は複数のグリッドを用いて1つ又は複数の回路を検証する方法であって、
回路にアクセスする工程と、
前記回路上で1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを生成する工程であって、各検証インスタンスが1つ又は複数のタスクを備える工程と、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させる工程と、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行する工程とを備えることを特徴とする方法。
【請求項２】
請求項1記載の方法であって、
前記検証インスタンスのそれぞれの実行を監視する工程と、
前記検証インスタンスの第１のものが、1つ又は複数の終結基準に到達した場合、前記第１の検証インスタンスを終結させる工程とを更に備えることを特徴とする方法。
【請求項３】
請求項2記載の方法であって、
前記第１の検証インスタンスを終結させた後、1つ又は複数の到達状態を前記第１の検証インスタンスから前記検証インスタンスの1つ又は複数の第２のものに通信する工程を更に備えることを特徴とする方法。
【請求項４】
請求項3記載の方法であって、
前記第２の検証インスタンスに通信した前記到達状態を用いて前記第２の検証インスタンスの実行を続ける工程を更に備えることを特徴とする方法。
【請求項５】
請求項1記載の方法であって、
前記回路の状態空間を区画化する工程と、
前記区画のそれぞれにおいて、前記シードの1つ又は複数を生成する工程と、
前記区画を前記グリッドにわたって前記タスク及び前記シードとともに分散させる工程と、
各検証インスタンスを前記区画の1つ又は複数に対して実行する工程とを更に備えることを特徴とする方法。
【請求項６】
1つ又は複数のグリッドを用いて1つ又は複数の回路を検証するロジックであって、
実行するよう1つ又は複数の媒体内に実施され、実施されると、
回路にアクセスし、
それぞれが1つ又は複数のタスクを備える1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを前記回路上で生成し、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させ、かつ、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行するよう動作可能であることを特徴とするロジック。
【請求項７】
1つ又は複数のグリッドを用いて1つ又は複数の回路を検証するシステムであって、
回路にアクセスする手段と、
前記回路上で1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを生成する手段であって、各検証インスタンスが1つ又は複数のタスクを備える手段と、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させる手段と、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行する手段とを備えることを特徴とするシステム。
【請求項８】
検証するよう1つ又は複数の回路を処理する方法であって、
大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当てる工程と、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成する工程と、
減縮回路毎に遷移関係（TR）を生成する工程と、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成する工程とを備えることを特徴とする方法。
【請求項９】
検証するよう1つ又は複数の回路を処理するロジックであって、
実行するよう1つ又は複数の媒体内に符号化されており、実行されると、
大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当て、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成し、
減縮回路毎に遷移関係（TR）を生成し、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成するよう動作可能であることを特徴とするロジック。
【請求項１０】
検証するよう1つ又は複数の回路を処理するシステムであって、
大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当てる手段と、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成する手段と、
減縮回路毎に遷移関係（TR）を生成する手段と、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成する手段とを備えることを特徴とするシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、一般に、回路検証に関し、特に、１つ又は複数の回路を1つ又は複数のグリッドを用いて検証することに関する。
【背景技術】
【０００２】
正式な検証、特にエラー検出は、設計の複雑度の増大とともに重要度が急速に高まっている。検証における一般的な制約として、時間及び費用を含む、利用可能なものとして存在する総資源量がある。充足可能性（SAT）ベース境界モデル検査（BMC）手法は、深度があまり高くないエラー状態を検出するうえで好ましい手法であることが多い。しかし、こうした手法は、多くの時間フレームを検査する必要がある場合、費用が非常に高くなることがあり得る。2進判定図（BDD）ベースの手法は、多くの画像工程について大容量のBDDを構築するのに費用が非常に高いものであり得るので、画像BDDの容量が適度に小さい状態に留まる、こうした高深度の場合についてはより好適な選択である。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明は、1つ又は複数の回路の検証に関する欠点及び課題の一方又は両方を軽減又は除去することができる。
【課題を解決するための手段】
【０００４】
一実施例では、1つ又は複数のグリッドを用いて1つ又は複数の回路を検証する方法は、回路にアクセスする工程と、回路上の検証の1有機ジョブ・コントローラ又は複数のインスタンスを実行するための１つ又は複数のシードを生成する工程とを含む。検証の各インスタンスは、1つ又は複数のタスクを備える。上記方法は、タスク及びシードを、複数ノードを含むグリッドにわたって分散させる工程、及び、シードを用いて、タスクによって、グリッド内のノードで検証のインスタンスを実行する工程も含む。
【０００５】
本発明の特定の実施例は、技術上の1つ又は複数の利点を提供することができる。例として、SATベースのBMCアルゴリズム（すなわち、SAT‐BMCアルゴリズム）とBDDアルゴリズムとの混成によって、SAT‐BMCを並行して実行して隣接状態空間を探査することができるシードであり得る種々の候補高深度状態の探索が可能になることがあり得る。深度が高い可能性があるそうしたシード状態から始めて、複数BMCランによって、更に高深度の状態に達し、解析を行うことができることがあり得るものであり、これは、既存の手法がカバーする範囲外であり得る。状態空間は、複数BMCランを、各シードから１つ始めることによって検査することができる。ランタイムを実用的なものに維持するために、ランは並列に行われる。多数のノードからの、これ以外の場合にはアイドル状態の中央処理装置（CPU）サイクルを用いる、グリッドの計算能力を用いて並列ランを実現する。特定の実施例は、グリッドの別々のノード上で別個に構築され、解析される、区分化され減縮され順序付けられた２進判定図（POBDD）表現を体系的に検査することができる。
【０００６】
特定の実施例は、BMCを並列化するうえでの非伝統的なやり方を提供するものであり、それによって、複数BMCランを並列に発火して別々の状態空間領域を同時に探査することが可能になる、実施例は、２つの研究成果、すなわち、スマート・シミュレーション又は効率的なバグ発見の混成手法と、並列フレームワークにおいて検証を行うことへの最近の取り組みが交差する点に位置する。BMC手法が現在、不合格特性のデファクト標準であり、BDDベースの手法は、特性が正常であることを確認するうえで選択するものであるので、特定の実施例は、何れかのケースの発生に応じ、自動的に処理するよう企図されている。特定の実施例は、回路の解析における従来技術をかなり拡張することができる。
【発明を実施するための最良の形態】
【０００７】
本発明の特定の実施例は、前述の技術上の利点の全部又は一部を提供するか、前述の技術上の利点を何ら提供しないものである。特定の実施例は、他の技術上の1つ又は複数の利点を提供することができ、そのうちの１つ又は複数は、添付図面、以下の記載、及び特許請求の範囲から当業者に容易に明らかであり得る。
【０００８】
本発明並びにその特徴及び利点が更に徹底的に分かるようにするために、添付図面に関して解釈される以下の記載を参照する。
【実施例】
【０００９】
図１は、1つ又は複数のグリッドを用いて1つ又は複数の回路を解析する例示的システム１０を示す。システム１０は、検査用の回路１２を含む。限定ではなく例として、回路１２の検査は、回路１２内の1つ又は複数のエラーの検出と、回路１２の1つ又は複数の特性の検証との一方又は両方を含み得る。システム１０は、下記のように、グリッド１６、サーバ２２、及び回路１２の検査用のデータ２８を含む。1つ又は複数のリンクがシステム１０の構成部分をお互いに結合する。限定ではなく例として、リンクは、1つ若しくは複数の回路基板内の１つ若しくは複数の配線、1つ若しくは複数の内部/外部バス、1つ若しくは複数のローカル・エリア・ネットワーク（LAN）、1つ若しくは複数のメトロポリタン・エリア・ネットワーク（MAN）、1つ若しくは複数のワイド・エリア・ネットワーク（WAN）、1つ若しくは複数のインターネット部分、又は、該当する場合、前述の2つ以上のリンクの組み合わせを含み得る。特定の実施例では、ネットワーク１４によって、サーバ２２とグリッド１６との間の通信が促進される。
【００１０】
回路１２は、例えば、ハードウェアに相当する特定の1つ又は複数の仕様によって、ハードウェアが適切に動作するか否かを判定するよう検査するハードウェア、又はこのハードウェアの論理表現や他の表現を含む。限定ではなく例として、回路１２は、特定の機能を備えるよう配置され、お互いに結合された、ゲート、カウンタ、反転器、バッファや他の回路構成部分を含み得る。別の例として、回路１２は、そうした構成部分の論理表現や他の表現を含み得る。回路１２は、何百万もの回路構成部分を含み得る。特定の機能を備えるために、回路１２は、1つ又は複数の特性を備えている必要があり得る。回路１２は、そうした何百万の特性を備えている必要があり得る。特定の実施例では、1つ又は複数の論理表現が回路１２の特性を表し得る。回路１２の「特性」への言及は、回路１２の、論理的に表すことが可能な状態、特徴、ふるまい若しくは動作、又は回路１２の別の特性を包含し得る。回路１２の「状態」への言及は、該当する場合、特性を包含し得る。
【００１１】
回路１２を検査する従来の試行では、単一プロセッサのみを用いている。近年、解析のために並列でかつ分散させた手法を用いた種々の試みが行われている。こうした手法は全て、解析を行うためにノード２０の専用ネットワークが存在することを前提としている。パソコンの計算能力が増大し続けるとともに、計算グリッドの概念が受け入れられるようになってきている。ここでは、グリッド１６は、個々の利用に特化したノード２０のネットワークであるが、他のタスクに一部の時間、利用可能なものとして存在することがあり得る。これは、いくつかのノード２０からの、この場合以外にはアイドル状態のCPUサイクルを用いることによって並列性が可能であるという特有の環境である。グリッド１６は、2つ以上のサブグリッド１８を含み得る。サブグリッド１８は、グリッド１６のより小さな表現である。各サブグリッド１８は、1つ又は複数のノード２０を含む。ノード２０は、回路１２を解析するうえで割当てられたジョブを行う、ハードウェア、ソフトウェア、組み込み論理構成部分、及び/又は、前述の2つ以上の構成部分の組み合わせを含む。限定ではなく例として、ノード２０は、1つ若しくは複数のデスクトップ型コンピュータ、又は、1つ若しくは複数のラップトップであり得る。ノード２０はヘテロジニアスであり得るものであり、同じものでなくてよい。限定ではなく例として、サーバ２２は、単一ジョブをノード２０間で分散させ、ノードでは、ジョブが複数タスクに分けられる。限定ではなく別の例として、サーバ２２は単一ジョブをサブグリッド１８又はグリッド１６に分散させ得る。ジョブは、例として、サーバ２２によって割り当てられる基準に基づいた高深度BMCの区画を含み得る。解析中、グリッド１６のノード２０全てが、サーバ２２からの命令によってタスクの処理を停止し得る。実施例では、各ノード２０は、ジョブ内の複数タスクのうちの単一タスクを実行し得る。完了タスクは組み合わせられ、更に解析するようサーバ２２に供給される。ノード２０はお互いに無関係に動作し、よって、検証をグリッド１６にスケーリングすることが適切である。特定の実施例では、各ノード２０は、並列コンピュータ環境において同時に、すなわち、並列に実行する。
【００１２】
サーバ２２は、解析するよう回路１２にアクセスするための、ハードウェア、ソフトウェア、組み込み論理構成部分、又は前述の2つ以上の構成部分の組み合わせを含む。コンピュータ・システム３０のユーザは、インタフェースを用いて、又はネットワーク１４を介してサーバ２２と通信し得る。限定ではなく例として、解析回路１２は、下記のように、回路１２内の状態の識別を含む。サーバ２２は、区画化モジュール２４及びグリッド管理モジュール２６を含む。区画化モジュール２４は、下記のように、回路１２の状態空間を区画化するための、ハードウェア。ソフトウェア、若しくは、埋め込み論理構成部分、又は、前述の2つ以上の構成部分の組み合わせを含む。回路１２の状態空間は、回路１２の全状態を全て、又は実質的に含む。回路１２の状態空間の区画は、回路１２の状態空間の1つ又は複数の部分を含む。グリッド管理モジュール２６は、下記のように、グリッド１６上の計算資源を管理するための、ソフトウェア、埋め込み論理構成部分、又は構成部分の組み合わせを含む。データ２８は、特定の実施例において、サーバ２２が回路１２を検査するのに用いる、回路１２のタイプを規定するデータや他のデータを含む。特定の実施例では、1つ又は複数のノード２０は、サーバ２２及びデータ２８へのアクセスを設ける。限定ではなく例として、コンピュータ・システム３０のユーザは1つ又は複数のノード２０をアクセスして、サーバ２２への入力を備え、サーバ２２からの出力、及びデータ２８を受信し得る。なお更なる例として、コンピュータ・システム３０のユーザは、ネットワーク１４を介してサーバ２２及びノード２０に通信し得る。限定ではなく例として、コンピュータ・システム３０は、回路１２を解析するための、ハードウェア、ソフトウェア、組み込み論理構成部分、及び/又は前述の2つ以上の構成部分の組み合わせを含む。限定ではなく例として、コンピュータ・システム３０は、1つ若しくは複数のデスクトップ型コンピュータ、又は1つ又は複数のラップトップであり得る。
【００１３】
グリッド計算環境における課題は、専用並列計算環境におけるものとは極めて異なるものである。ノード２０の可用性は保証されていないため、そうしたフレームワークを用いるアルゴリズムは何れも、特定の計算から結果を何ら受信しないか特定の計算から部分的な結果のみを受信することに持ちこたえることができなければならない。第２に、計算ネットワークは単一のタスクに常時特化している訳でないので、グリッド１６上でスケジューリングされるタスクはわずかなネットワーク・トラフィックを用いなければならない。可能な限り、別々のノード２０上の計算は、依存性が少ない状態で、お互いに無関係である必要がある。そうした状況下では、伝統的なアルゴリズムは、グリッド・ベースのネットワークにスケーリングするために注意深い手直しを行う必要がある。不合格特性を識別するために、BMC手法は現在、デファクト標準である。SAT‐BMCは、探査の深度に境界をつけ、この境界を順次増加させることによって、容量のより大きな設計の状態空間を探査することができる。充足可能性検査の技術分野における顕著な改善によって、SAT‐BMCは今では、多くの産業用設計の特性検証中に回路１２を検査するよう慣例的に施される。SATベースのBMC手法は、深度があまり高くないエラー状態を検出するうえで好ましい手法である。しかし、こうした手法は、検査するのに多くの時間フレームが必要である場合に費用が非常に高くなることがあり得る。特性が正常であることを確認するために、別の手法、通常は、BDDベースの手法が、一般的に選択される。BDDベースの手法は、多くの画像工程についての大容量BDDの構築の費用が非常に高くなるので、画像BDDの容量が比較的小さい状態に留まる高深度の場合に、より好適な選択となる。特性が異常であるか否かは事前に分からないので、それぞれの手法が、全ての特性に対して特定の順序で実行される。実用的で効率的なグリッド・ベースの手法は、両方のケースを自動的に処理することができる。
【００１４】
単一ノード２０上で実行する手法は、実行環境の計算能力の制約が理由で明白な制限を有している。分散手法に関する提案が、BDDベース・モデル検査及び並列SATソルバに向けて行われている。しかし、こうした手法は、基本的に、幅優先中心の観点から状態空間を解析するので、不十分な状態に留まっている。BDDベースの手法は、大容量BDDの形式での別々のノード２０間の通信も必要とし、このことによって、こうした手法は、大容量並列計算環境を用いることから排除される。
【００１５】
特定の実施例は、以上で明確にした類の課題に対処するための直感的かつ魅力的な手法を提供する。SAT‐BMCアルゴリズム及びBDDアルゴリズムの混成によって、SAT‐BMCを並列に実行して隣接状態空間を探査することができるシードであり得る種々の候補高深度状態を探索することが可能になる。深度が高い可能性があるそうしたシード状態から始めれば、複数BMCランは、更なる高深度状態に到達し、解析を行うことができることがあり得るものであり、これは、既存の手法がカバーする範囲外であり得る。
【００１６】
特定の実施例はBDDベースの手法を用いることを含む一方、そうしたシード状態を生成するために、グラフの容量は、なお制御下にある。到達可能性のいくつかの初期工程の場合、BDDを用いて高速に進めることが可能である。しかし、グラフの容量が増大するにつれ、BDDベースの状態空間解析は費用が非常に高いものになる。このことは、BDDベース手法がBMCランをシーディングする機能を大きく制限し得る。上記混成手法において解決に値する別の課題は、シードが多くあると仮定すれば、より重要であり、優先すべきであるシードがどれであるかが明らかでないということである。特定の実施例は、グリッドの別々のノード上で無関係に構築され、検査される複数のPOBDD表現を体系的に検査することができる。このことは、合格特性にも恩恵を与えることが明らかである。上記課題に対する実用的な解決策は、回路１２を分析するうえで従来技術をかなり拡張し得る。
【００１７】
状態空間解析を用いたBDDの容量を制御するために、状態空間区画化を用いる。区画化によって、状態空間を高深度で記号によって探査する手段が提供されるということが実証的に分かっている。実際に、各部分空間を方向と考えれば、区画化による到達可能性は、そうしたそれぞれの方向に沿った局所化幅優先探索（L‐BFS）である。そうしたL‐BFS検索によって供給される高深度状態は、初期シ―ド状態を後続BMCランに供給して、人気のあるSAT‐BMC手法を用いる前に探査することができない領域の探査を支援するのに用いることが可能である。
【００１８】
特定の実施例は、適切などの回路１２にも適用することができる。多くの回路１２の場合、BDDベースの解析は、区画化なしでも費用が非常に高くなることがあり得る。よって、高深度シード状態を生成するための時間は、法外に長いものであり得る。BDDランタイムはグラフの容量に直接比例するので、各区画のグラフ容量は、過小近似を用いて更に制限される。よって、特定の実施例は、区画化BDDに加えて、過小近似ベースの手法を提供する。
【００１９】
到達可能性の計算中にグラフ容量を制御下におくために、多くの区画を作成しなければならない。しかし、そうした場合には、BMCに最良のシード状態を備える区画が事前に分かることは難しい。よって、区画化とBMCとの組み合わせは、BMCの複数インスタンスの生成と、ノード２０のグリッド１６上でのそうしたケースのそれぞれの実行とによって更に拡張される。この考え方は、多くの計算環境において大容量計算グリッド１６が利用可能なものとして存在するようになってきていることを考えると、なお魅力的にみえる。この手法は、回路１２の適切な解析に用いることができる。更に、この手法は、BMCの並列化に対する非伝統的なやり方を提案している。この研究は、２つの研究成果、すなわち、スマート・シミュレーション又は効率的なバグ発見の混成手法と、並列フレームワークにおいて検証を行うことについての最近の成果が交差する点に位置する。
【００２０】
SATベース手法又は自動検査パターン生成（ATPG）ベース手法を用いれば、BDDを用いて検査することができなかった回路１２を処理することが可能となっている。しかし、前述のような従来の手法は、複数のエンジンを用いた混成手法という性質を有している。よって、こうした手法は、SATエンジン若しくはATPGエンジン、又はBMCの形成などの個々の手法における改良を容易に用いることが可能である。従来の研究では、目標状態からのプレ画像計算を行って、シミュレーション用の拡大目標を備える。シミュレーションの検証及び拡張（SIVA）のツールは、BDD及びSATによって拡張した、シミュレーション環境における最良優先探索を、現行状態と目標状態との間のハミング距離を案内コスト関数として行う。従来の他の手法は、関心信号群にわたる状態カバレッジを最大にするために、インタリーブ・シミュレーション・ランと、BDDベースの記号シミュレーションと、ATPGベースのBMCとを用いている。
【００２１】
上記バグハント手法と対照的に、別の類の手法は、主に、特性（場合によっては境界深度特性）を確認する目的で公式エンジンの組み合わせを用いる。例えば、一部の手法は、BDDベースの到達可能性解析を用い、BDD機能解析によって、関連する通常形式（CNF）クローズを計算して、SATベースのBMCの探索空間を刈り込み、特性検査を、SAT及びBDDによって分解された部分に構造的に区画化し、記号軌道評価と、SAT/BDDベースの記号モデル検査との組み合わせを用いる。
【００２２】
特定の実施例は、２つの主要な局面において前述の従来の手法とは異なる。まず、シミュレーションは、上記手法の多くの、探索の根幹を構成する。本願開示の手法ではこのことはあてはまらない。ハードで高深度のバグの場合、シミュレーション・ベース手法は、探索空間の関心領域にアクセスすることができないことがあり得る。第２に、本願開示の混成手法は、状態空間の直交領域を包含する複数のサブ課題であって、更に並列に探査されるサブ課題を生成することができるという特定の狙いによって新規のやり方で策定されている。
【００２３】
BDD及びSAT‐BMCを組み合わせた従来の混成手法は、モノリシックの、順序付けられた2進判定図（OBDD）を選択されたデータ構造として用いており、このことは、通常、状態空間の幅優先処理につながった。しかし、OBDDを用いる場合、探索の方向、及び、通常生成されるグラフの容量を制御することは難しい。これは、状態空間内の高深度の状態に（それが任意であっても、少数のみであっても）効率的に到達することが難しいことが多い。対照的に、解析を区画の部分集合に制限することによって、部分的であっても深度が高いカバレッジを実現するうえでの制御されたやり方が提供される。区画化によって、個々のグラフを制御下の区画内になお維持する一方で、高深度で状態空間を記号によって探査する手段が提供される。生成されるグラフの容量は、情報の喪失を犠牲にしても、過小近似を用いることによって更に削減することが可能である。別々の多くの初期状態を供給して後続BMCランをシーディングするのに、そうした複数L‐BFS探索による高深度状態を用いることが可能である。こうしたものは、伝統的なSAT‐BMC手法を用いて探査できなかった領域を探査し得る。特定のL‐BFS探索が、設計におけるエラーに相当する方向に至る場合、相当するシードから始まるBMCは、元の初期状態から始まる伝統的なBMCよりもずっと効率的であることが分かり得る。より効果的な方法論を提供する特定の実施例は、複数エンジンを用いた混成手法の特性を有している。
【００２４】
通常の混成手法は、並列探査にもともと向いている訳でない。本願開示の手法によって、複数BMCランを並列に発火して別々の状態空間領域を同時に探査することを可能にする非伝統的な並列BMC手法がもたらされる。
【００２５】
並列検証を行う他のいくつかの手法が提案されている。一部のものは、明示的なモデル検査器を並列化する。他の手法では、並列化BDDを、到達可能性解析に用いる。並列到達可能性を用いた解析は、先行して考察されている。特定の実施例は、バグハントよりも完全性を意図した他の分散モデル検査手法とは異なる。大半の手法は概ね、幅優先探索を並列化するに過ぎない。高深度状態に到達するうえでの制約は、大きなハンディーの下にある状態に留まっている。更に、こうした手法は、大容量BDDの形式における、別々のプロセッサ間でのメッセージ転送を必要とする。このことは、大容量グリッド１６を効果的に用いることができる方法を大いに制限することがあり得る。従来の別の手法は、異種ワークステーション・ネットワークにわたってSATベースBMCを分散させるものである。この手法は、分散一対（binate）被覆問題（BCP）を行って大容量SAT問題を解決するアルゴリズムを含む。同様に、従来の別の手法では、並列マルチスレッドSATソルバが論じられている。
【００２６】
BMC手法が現在、不合格特性のデファクト標準であり、BDDベース手法は、通常、特性が正常であることを確認するための選択であるので、特定の実施例は、発生に応じて、何れかのケースを自動的に処理するよう企図されている。
【００２７】
SATに基づいたBMCは、探査することができる、状態の深度に対する制約を有するが、それは、BMCが、エラーがあると思われるパスの長さに数が等しい複数時間フレームを明示的に展開することに基づいているからである。BDDは、到達可能性の連続画像計算を算出するものであり、かつ、遷移関係（TR）の容量が管理可能であり、連続画像の容量が小さいと仮定した場合、高深度まで進むことが可能である。残念ながら、そうした画像は、非常に低深度で容量が大きくなることが多く、BDDは更に進むことができない。BDDが容量における動的な爆発を表さなくても、計算された画像群は、実行不可能なほど長い時間が算出に必要になるほど容量が大きくなるまで、容量が絶え間なく増加する。よって、低深度の場合、SATは、状態群を記憶しないが、単にパスを計算するものであるので、更に進むことができることがあり得る。
【００２８】
エラーは、回路１２内の比較的高深度にあり得る。限定ではなく例として、イーサネット（登録商標）・スイッチのハードウェア実施形態は、比較的多数の時間フレームにわたって初期化を行い得る。イーサネット（登録商標）・スイッチのハードウェア実施形態を実施する回路１２の1つ又は複数の特性は、初期設定段階よりも高深度に必然的に位置するものである。BMCは、初期設定段階よりも深度が高いエラーを検出することが非効果的である可能性が高いものである。BDDを用いた回路１２の到達可能性解析はBMCの代替策であり得る。カウンタに似た種々の回路１２は、そうした回路１２が、コンパクトなBDD表現を有しているが、実質的に管理不能な数のSATクローズにつながるという意味で「BDDフレンドリ」である。VIS‐Verilog  Benchmarkスイートによる「B12」回路１２は、そうした回路１２の例である。よって、種々のシナリオでは、BMCは不適切であり、BDDを用いたエラー検出が必要である。BDDは、到達可能性の連続画像計算を算出し、かつ、遷移関係の容量が管理可能であり、連続画像の容量が小さいという仮定で、高深度まで進むことが可能である。残念ながら、そうした画像の容量は、非常に低深度で大きくなることが多く、BDDは更に進むことができない。BDDの容量が劇的な増加を表さない場合も、算出画像の容量は、実行不可能なほど長い時間を算出が要するようになるほど容量が大きくなるまで絶え間なく増加する。よって、BDDは、画像BDDの容量が比較的小さい状態に留まる高深度の場合に、より好適な選択である。
【００２９】
２つの主要な考え方が、高深度探査に対して存在している。最初のものは、扱いやすい状態にBDD容量が確実に留まっているようにすることによって、完全性を犠牲にして、BDDを用いて高深度に進むことである。これは、区画化及び過小近似を用いることによって達成される。BDDの容量は制限され、多くのBMCインスタンスが生成され、これらは並列に実行することが可能である。各区画は、BDDベースの到達可能性から得る状態によってシーディングされる。第２の考え方は、不完全なBDD解析が、生成されるシードの深度を保証することができないということによって動機付けされる。よって、高深度エラーに到達するために、状態空間が、各シードから１つの複数BMCランを始めることによって検査される。ランタイムを実用的なものに維持するために、ランは並列に行われる。このことは、多数のノード２０からの、この場合以外はアイドル状態のCPUサイクルを用いる、グリッド１６の計算能力を用いることによって達成される。特定の実施例では、状態空間区画化に基づいたBMCの並列化は、別々のパラメータ又は別々のシード状態を用いて無関係にBMCの複数インスタンスを実行することによって達成される。こうしたシード状態は、別々の区画内の到達可能状態から選択される高深度状態である。特定の実施例では、ノード２０はお互いに無関係に機能するので、グリッドに似たシステム１０に検証をスケーリングするのに適している。これは、高深度状態探査を行うことができないという、伝統的なＳＡＴ‐ＢＭＣの主要な欠点を解決するものである。これは、ＢＭＣ並列化の非伝統的なやり方である。ＢＤＤベースの探査がＴＲを低費用で構築することができる回路の場合、特定の実施例は、高深度状態探査を行うことができないという、伝統的なＳＡＴ‐ＢＭＣの主要な欠点を解決するようにみえる。
【００３０】
区画化の考え方は上記で、ＰＯＢＤＤと呼ばれる機能表現手法を論ずるのに用いられている。n個の入力Xn=｛x1,…,xn｝にわたって規定されたブール関数f:Bn→  Bを前提とすれば、fのPOBDD表現χfは、k個の関数対、χf=｛(x1,f1),…,(wk,fk)｝であり、ここで、
wi:Bn→  B及びfi:Bn→  BもXnにわたって定義され、wi及びfiは、1≦i≦kの場合、変数順序付けπを遵守するROBDDであり、w1∨w2∨…∨wk=1であり、i≠jの場合、wi∧wj=0であり、1≦i≦kの場合、fi=wi∧fであるという条件を満たす。集合｛w1,…,wk｝はWによって表す。各wiはウインドウ関数と呼び、fが定義されるブール空間の区画を表す。各区画は、減縮された順序付けられたBDD（ROBDD）として別個に表し、異なる変数順序を有し得る。大半のROBDDベースのアルゴリズムは、POBDDに容易に適合させることができる。
【００３１】
POBDDは正準であり、種々のブール演算をPOBDDに対して、ROBDDに対してと同様に効率的に行うことが可能である。更に、POBDDは、特定の類の関数の場合、ROBDDと比べて指数関数的にコンパクトであり得る。この表現の実用性は、組み合わせ回路の出力のROBDDを構築することによっても表される。
【００３２】
特定の実施例は、そうしたウインドウ・ベース状態区画化を含む。この理由は、この表現が正準であり、各区画内で否定を局所で行うことが可能になるからである。状態群を分割する他の手法は、否定を行うために大局同期化処理を行う必要があり、これは費用が高いことがあり得る。
【００３３】
SAT‐BMCは、下記のフレームワークなどの適切なフレームワークに基づくものであり得る。有限遷移システムM上で時間論理特性pを検証するものとする。Mは単一初期状態Iを有し得るものであり、特性pは不変であり得る。BMC問題を、k個の時間フレームの展開反復論理アレイ（ILA）であるMに対して提起する。モジュール
【００３４】
【数１】
2007012062.tif 000003
は、特定の時間フレームにおいて特性pの違反を検査するモニタである。よって、回路は、初期状態Iから始めて、最大kの長さのMの全実行の空間内のpに対する反例が存在するという条件を符号化する。この回路は、通常、CNF公式に変換され、zchaffＳＡＴソルバなどの通常のＳＡＴソルバによって決定される。ＳＡＴソルバによって戻される合格割り当ては反例をpに変換する一方、合格可能でない公式は、最大k個の特性深度までMの、エラーのない特性を保証する。後者の場合、このプロセスを通常、特性pの違反が検出されるか、kに対するユーザ定義境界、又は特定のリソース制約を超えるまで、（後にBMC問題のステップ・サイズとして表す）n個の時間フレーム、kを増加させることによって反復する。
【００３５】
特定の実施例は、SATの初期シード状態を判定するための以下の手法を含む。まず、少数のBDDベース区画が完全に探査され、この実施形態は、一定数の画像計算後に、例えば、5個の画像毎に新たなシードを作成する。これを行うために、到達可能状態のスナップショットが得られ、こうした状態の部分集合を用いてＳＡＴソルバをシーディングする。状態の全てではなく、少数の状態を選ぶことが重要である。さもなければ、ＳＡＴソルバは、非常に多数のクローズを得ると詰まることがあり得る。実施例では、過小近似が、単に、群からいくつかのランダム状態を選ぶことによって行われる。この近似の品質は、例えば、案内された検索を用いることによって、特に、設計者からの入力によって更に向上させることが可能である。SATソルバ・インスタンスは、得られたシードから、BMCに似たアルゴリズムを実行する。通常、SAT‐BMCは、20という低深度まで実行するが、それは、zcahffSATソルバを用いて数分で計算することが可能であるからである。SATインスタンスは、和からSATの単一のインスタンスを実行するのではなく、別個に実行する。これは、状態空間の別々の部分からのシード状態が、非常に異なるものであり得るものであり、SATのクローズを生成するうえで一緒に合成される場合、SATソルバの効果性が激しく低下することがあり得るからである。
【００３６】
特定の実施例は、構成がかなり明確な、適切な手順を提供する。例えば、エラーが検出される場合、実際に設計上の真のエラーであり、初期状態から、エラーを備えた状態までのトレースが生成される。特定の深度までの境界完全性は、初期状態群を、BMCに転送されるシード群毎に加えることによって達成することが可能である。あるいは、同じ結果が、初期状態からBMCを別個に実行することによって生じ得るものであり、その場合、この設計は、この深度までエラーがないということが保証される。
【００３７】
要約すれば、回路１２を解析する特定の実施例は以下の２つの段階を有する。
【００３８】
高深度シードを生成する工程。完全な探索を、状態空間について、TRを区画化することによって行い、グラフも関連した算出も扱いやすい状態に留まるように計算状態群についても行う。BDD算出がもう管理可能でない場合、連続した過小近似が行われる。画像計算の各工程で、実際の状態群の部分集合を用いる。そうした過小近似は、深度がより高い状態に常につながる訳でない連続した探索をもたらし得る。しかし、確率論的に言えば、計算画像群内の状態数が、先行工程における和を超える場合（これはよくあることである。）、TRの区画から得られるより小さな画像関数を連続して施すことによって、高深度探索のパス内のほとんどの状態は実際に高深度のものになる。
【００３９】
並列シードSAT。SATの初期シード状態を判定するために、2つの手法を用いる。まず、少数のBDDベース区画を完全に探査し、CNFクローズを等間隔で書き出す。あるいは、多数の区画が過小近似によって非常に速く探査され、結果として生じる高深度状態を用いてSATをシーディングする。少なくともBMC実行部分集合は、状態探索に沿った種々の点から複数BMCランを始めさせることによって高深度状態から始まる。全てのBMCランを並列に行うことができるので、これはBMCを並列化する非伝統的な手法につながる。
【００４０】
特定の実施例では、1つ又は複数のグリッド１６を用いてBMCが高深度のものであるようにする基本アルゴリズムは、以下の工程を含み得る、すなわち、
1.  Partition_reach:  到達可能性における状態区画化を用いて、状態空間を探査する、発散する別々のパスを得る。
【００４１】
2.  Approx_Partition_reach:  超過小近似によって到達可能性解析を行う。各画像計算中に、新たに探索された到達可能状態の部分集合を選び、これを到達可能性群に加えてBDD爆発問題を避ける。
【００４２】
3.  Generate_seed:  等間隔で、シード生成閾値を超えると、シードを記憶し、これをSATソルバの新たなインスタンスに転送する。
【００４３】
4.  Start_Seeded_SAT:  こうしたシードのそれぞれから、SATベースBMCのインスタンスを最大、十分に低い深度まで実行する。
【００４４】
5.  Run_in_Parallel:  サブグリッド１８それぞれ、又はグリッド１６のノード２０それぞれに対して１つのSATインスタンスを実行する。
【００４５】
6.  Termination_condition:  エラーが検出されるかタイムアウトに達するまでBDD探査及び全SAT探査が並列に続行することを可能にする。
【００４６】
深度が高い可能性があるそうした状態から始めれば、複数BMCランは、更なる高深度状態に到達し、エラーを見つけることができることがあり得るものであり。これは既存の手法が到達しないことであり得る。高深度探査の場合、方法論は、管理可能容量BDDを用いることを含み、これは、区画化及び過小近似を用いることによって達成される。BDDの容量は制御され、多くのBMCインスタンスは並列に実行され、それぞれは、BDDベースの到達可能性から得られる状態によってシーディングされる。
【００４７】
手順の適切性は、構成上、かなり明白である。例えば、エラーが検出された場合、これは、設計における真のエラーであり、初期状態から、エラーを備えた状態までのトレースが生成される。境界完全性、すなわち、特定の深度までの完全性は、BMCに転送される全シード群に初期状態群を加えることによって達成することが可能である。あるいは、同じ結果が、BMCを初期状態とは別個に実行することによって生じ得る、その場合、この設計は、この深度までエラーがないことが保証される。
【００４８】
図２は、1つ又は複数のグリッドにわたって分散させた複数シードSAT‐BMCランを用いた１つ又は複数の回路の解析例を概念的に示す。三角形はSATを用いた探索を表し、楕円形は、BDDを用いた連続画像計算を表す。初期BDD段の深度はdbであり、SAT段の深度はdsである。前述の組み合わせはmax(db.ds）の深度までの少なくとも一状態が保証され、深度dsまでエラーがないことが保証される。完全性の点では、これは、BMCより悪いものでなく、同時に、深度がより高いシードも一部有する。経験的に、深度がより高いこうしたシードはエラーを見つけるうえで非常に効果的である。初期状態から、BMCは効果的に、深度dsまでしか進むことが可能でない。その代わり、本願提案の手法では、BDDは深度dbまで進み、多くのSATインスタンスがそれまでシーディングされ、これは、異なる深度ds1,ds2,..,dsnに対して効果的であり得る。よって、これによって、これ以外の場合には捕らえることが難しいエラーに到達することが可能である。
【００４９】
図３は、例示的なグリッド管理モジュール２６を示す。特定の実施例では、グリッド管理モジュール２６はCyberGRIPである。CyberGRIPは、OJC（有機ジョブ・コントローラ）３２と、グリッド・リソース・マネージャ（GRM）３４と、サイト・リソース・マネージャ（SRM）３６との３つの構成部分を含む。OJC３２は、CyberGRIPが投入ジョブを実行する方法を制御する。GRM３４は、最適計算資源を定め、ノード２０間の通信を管理する。各ノード２０は関連SRM３６を有している。ウィンドウズ（登録商標）のパソコンのSRM３６は、ウィンドウズ（登録商標）用グリッド・ミディエータ（GMW）・マネージャと呼ばれている。各サーバ２２は、そのSRM３６と通信し、ジョブを実行するためのミドルウェアを有している。
【００５０】
CyberGRIPは、サーバ２２のウェブ・ポータル３８を介して、ソラリス・マシンやリナックス・マシンのみならず、オフィス使用ウィンドウズ（登録商標）・マシンも備える仮想化計算資源にジョブを投入することができる環境を実現することが可能である。コンピュータ・システム３０のユーザは、ノード２０の性能や他の特性が分かっていなくてもこれを行うことが可能である。ソラリス・マシン又はリナックス・マシンがサーバ２２の場合、汎用バッチ・システム、例えば、コンドルをグリッド管理モジュール２６として用いることが可能である。ウィンドウズ・マシンがサーバ２２の場合、ＧＭＷマネージャに対応するＧＭＷクライアントをマシンにインストールしなければならない。CyberGRIPによって、ユーザがサーバ２２のウェブ・ポータル３８を介して使用仮想化ノード２０にジョブを投入することが可能になる。ユーザは、個々のノード２０の性能や他の特性が分かっていなくてもこれを行うことが可能である。エラーが検出されると、グリッド１６上のノード２０は全て、問題の処理を停止する。
【００５１】
図４はOJC３２を示す。コンピュータ・システム３０のユーザは、OJC３２と通信して、OJCスクリプト４０によってジョブを実行する。OJPインタプリタ４２はジョブ間依存性を解釈する。OJCインタプリタ４２は、ツリー構造の作成及び変更をジョブ制御部４４に送る。ジョブ制御部４４はジョブを選択し、この選択をＯＪＣインタプリタ４２に送り、ＯＪＣインタプリタ４２はジョブ実行要求をＧＲＭ３４に送る。ジョブが完了し次第、ＧＲＭ３４はＯＪＣインタプリタ４２に通知する。
【００５２】
図５は、例示的なＤＪＣをＯＪＣ３２によって示す。ＤＪＣ機能は、実行対象ジョブ数を初期ジョブ入力時に静的に決めることが可能でなく、かつ、実行対象ジョブ数が動的に変動する場合に効果を現す。従来、ＤＪＣを自動的に行うことが難しいので、操作者は、実行が必要なものがどれであるかを考慮に入れることなく、投入されたジョブ全てを実行する手法と、先行して実行されたジョブの実行結果に基づいて各ジョブを実行するか否かを個々に決める手法との２つのうちの一方を利用した。前述の手法は何れも、非効率であることが分かった。こうした決定を自動化することによって、ＯＪＣ３２はジョブ実行の効率をかなり向上させる。
【００５３】
図６は、1つ又は複数のグリッド１６を用いて1つ又は複数の回路を解析する例示的な方法を示す。方法は工程１００から始まり、工程１００では、サーバ２２は、自動的に、又は、コンピュータ・システム３０のユーザからの入力に応答して、検査する回路１２をアクセスする。工程１０２では、サーバ２２は回路１２の状態空間を複数の区画に区画化する。工程１０４では、サーバ２２は、区画上でSAT‐BMCのインスタンスを実行するよう、各区画内にシードを生成する。特定の実施例では、前述のように、シードは、SAT‐BMCのインスタンスを実行するための1つ又は複数の初期状態である。工程１０６では、サーバ２２は回路１２の状態空間の区画をグリッド１６にわたって分散させる。特定の実施例では、前述のように、サーバ２２は各区画をグリッド１６のサブグリッド１８に分散させる。各サブグリッド１８は、それに分散させた区画上のSAT‐BMCのインスタンスを実行する。特定の実施例では、1つ又は複数の第１のサブグリッド１８で実行されるSAT‐BMCの1つ又は複数の第１のインスタンスは、1つ又は複数の第２のサブグリッド１８で実行されるSAT‐BMCの1つ又は複数の第２のインスタンスとは異なる。限定でなく例として、SAT‐BMCの第１のインスタンスは第１の1つ又は複数のパラメータ群によって実行することができ、SAT‐BMCの第２のインスタンスは第１の1つ又は複数のパラメータ群とは別の第２の1つ又は複数のパラメータ群によって実行することができる。
【００５４】
工程１０８では、サブグリッド１８が、回路１２の状態空間の区画上でSAT‐BMCのインスタンスを実行している間、サーバ２２はSAT‐BMCの各インスタンスを監視する。工程１１０で、サブグリッド１８で実行されるSAT‐BMCのインスタンスが1つ又は複数の終結基準に到達する場合、サーバ２２は、サブグリッド１８でのSAT‐BMCのそのインスタンスを終結する。限定でなく例として、終結基準は、著しいメモリ爆発、新たな状態に到達することがない状態での所定の経過時間量、別の終結基準、又は、2つ以上のそうした基準の組み合わせを含み得る。工程１１２では、サーバ２２は、1つ又は複数の到達状態をSAT‐BMCの終結インスタンスに関連した区画から、1つ又は複数のサブグリッド１８の1つ又は複数の実行中SAT‐BMCインスタンスに関連した1つ又は複数の他の区画に通信し、この時点で方法は終了する。特定の実施例では、サーバ２２は、SAT‐BMCが1つ又は複数のエラーを1つ又は複数の、回路１２の状態空間区画内で検出することと、SAT‐BMCのインスタンス全てが1つ又は複数の終結基準を満たすこととのうちの先行する一方の時点まで、グリッド１６を用いて回路１２上でSAT‐BMCを続行する。サーバ２２がグリッド１６を用いた回路１２上のSAT‐BMCを中止すると、サーバ２２は、1つ又は複数のユーザによる解析のために、回路１２の検査の1つ又は複数の結果を通信する。図６に示す方法の特定の工程は、特定の順序で行われるように図示し、説明しているが、図６に示す方法の適切な工程は、適切な順序で行い得る。
【００５５】
図７は、解析するための、1つ又は複数の、容量が比較的大きな回路１２の処理の例を示す。大容量回路１２に高深度BMCを用いることは、望ましい目標である。TRは、高深度の到達可能状態を見つける上で重要である。しかし、大容量回路１２のTRは構築することが可能でない。特定の実施例では、スライス回路１２が、適切な手法であり得る。これは、容量削減に部分割り当てを用いることを含む。結果として生じる方法は、状態空間の一部をみるものであり、これは完全なBMCを実行するほどではないが、シミュレーションのみを実行した場合よりも多くのものをみるものである。処理７０は、スライスなしで大容量回路１２を処理することを示す。処理７０では、TRは構築されないが、BDD爆発が生じる。よって、TRは何ら作成されず、到達可能性はなく、高深度BMCは何ら実行することが可能でない。処理７２は、スライス後の、多くの区画を有する、大容量回路１２の処理を示す。処理７２では、出力は数多くのTRスライス７４を含み、かつ、BMCのインスタンスを実行するよう、各TRスライス７４がサブグリッド１８又はノード２０に与えられる。図８は、解析するための、1つ又は複数の、容量が比較的大きな回路の処理の例を更に示す。TRスライス７４が存在している状態で、TRスライス７４が、有効な遷移を捕らえるか否かということが問題として残っている。各TRスライス７４は少数の有効遷移部分集合を捕捉し得る。しかし、遷移は、初期状態８０から捕捉されないことがあり得る。図９は、1つ又は複数のシミュレーションを用いて高深度BMCを容易にする例を示す。特定の実施例では、初期状態８０を、他の有効初期状態９０を加えることによって拡張することができる。初期状態９０はシミュレーションを用いて加えられる。各TRスライス７４を、初期状態９０の群とアラインさせて、各TRスライス７４が、有効遷移を初期状態９０から捕捉することを可能にする。
【００５６】
図１０は、解析するための、1つ又は複数の、容量が比較的大きな回路１２を処理する方法の例を示す。方法は工程１５０から始まり、工程１５０では、回路１２をシミュレートして到達可能状態群を生成する。初期状態からの回路１２のシミュレーションによって、到達可能状態群を見つける。到達可能状態を用いて、設計を更に簡単にする。特定の実施例では、M個のベクトルを、到達可能状態群から生成することができる。工程１５２では、サーバ２２がベクトルを検査して、回路１２の1つ又は複数のラッチ変数に対する割り当て値を生成する。特定の実施例では、N個のラッチ変数の部分集合を、割り当て値を用いて、上記作成されたデータベース・シミュレーション出力内のM個のベクトルを検査することによって生成することができる。更に、P個の部分割り当てを生成することができる。ラッチ変数を、深度優先探索（DFS）を用いて、又は適切な手法によって選択することが可能である。サーバ２２は、工程１５４で、1つ又は複数のラッチ変数に割り当てられた1つ又は複数の値を用いて回路１２を減縮する。特定の実施例では、カリフォルニア大学バークレー校のマルチレベル合成ツールであるSWEEP  in  SISなどの合成手法を用いて生成回路を単純にすることができる。特定の実施例では、静的抽象化によって、回路１２上で処理が行われる前にも回路１２の容量を削減することができる。工程１５６では、回路１２が首尾よく減縮するか否かについての判定が行われる。回路１２が減縮しない場合、処理は、工程１５４から、別の割り当て値及び/又はラッチ変数を用いて続く。回路１２が減縮する場合、1つ又は複数の減縮された回路のそれぞれのTRが工程１５８で生成される。工程１６０では、サーバ２２は、割り当て値の生成に用いない到達可能状態を用いてシードを生成する。特定の実施例では、より少数のシードを最初に用いるが、シード数は、画像計算が効果的でない場合に動的に増加する。工程１６２では、サーバ２２は、工程１６０において生成されたシードを用いて各TRスライスに対して並列にSAT‐BMCのインスタンスを実行する。特定の実施例では、サーバ２２はBDDを経ることなく、単にシミュレーションを用いて回路１２の高深度に到達することができる。図１０に示す方法の特定の工程を、特定の順序で行うものとして図示し、説明したが、図１０に示す方法の適切な工程は、適切な順序で行うことができる。
【００５７】
特定の実施例を用いて本発明を説明しており、当該技術分野における当業者は、本発明を説明するのに用いる特定の実施例に対する1つ又は複数の変更、置換、変形、改変又は修正が分かり得る。本発明は、特許請求の範囲の範囲内の前述の変更、置換、変形、改変及び修正を全て包含するものである。
【００５８】
（付記１）回路にアクセスする工程と、
前記回路上で1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを生成する工程であって、各検証インスタンスが1つ又は複数のタスクを備える工程と、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させる工程と、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行する工程とを備えることを特徴とする、1つ又は複数のグリッドを用いて1つ又は複数の回路を検証する方法。
【００５９】
（付記２）前記検証インスタンスのそれぞれの実行を監視する工程と、
前記検証インスタンスの第１のものが、1つ又は複数の終結基準に到達した場合、前記第１の検証インスタンスを終結させる工程とを更に備えることを特徴とする付記１記載の方法。
【００６０】
（付記３）前記第１の検証インスタンスを終結させた後、1つ又は複数の到達状態を前記第１の検証インスタンスから前記検証インスタンスの1つ又は複数の第２のものに通信する工程を更に備えることを特徴とする付記２記載の方法。
【００６１】
（付記４）前記第２の検証インスタンスに通信した前記到達状態を用いて前記第２の検証インスタンスの実行を続ける工程を更に備えることを特徴とする付記３記載の方法。
【００６２】
（付記５）前記回路の状態空間を区画化する工程と、
前記区画のそれぞれにおいて、前記シードの1つ又は複数を生成する工程と、
前記区画を前記グリッドにわたって前記タスク及び前記シードとともに分散させる工程と、
各検証インスタンスを前記区画の1つ又は複数に対して実行する工程とを更に備えることを特徴とする付記１記載の方法。
【００６３】
（付記６）前記区画を過小近似して、前記区画と関連した2進判定図（BDD）の容量を制御する工程を更に備えることを特徴とする付記５記載の方法。
【００６４】
（付記７）前記検証インスタンスの1つ又は複数がそれぞれ、
前記回路上の充足可能性（SAT）ベース境界モデル検査の1つ又は複数のインスタンスと、
前記回路の状態空間全体未満をそれぞれが包含する、前記回路上の公式な検証（FV）の1つ又は複数のインスタンスとのうちの1つ又は複数を備えることを特徴とする付記１記載の方法。
【００６５】
（付記８）前記検証インスタンスの1つ又は複数の第１のものを実行する工程が、前記検証インスタンスの1つ又は複数の第２のものとは無関係に前記第１の検証インスタンスを実行することを特徴とする付記１記載の方法。
【００６６】
（付記９）前記検証インスタンスの2つ以上をお互いに並列に実行する工程を更に備えることを特徴とする付記１記載の方法。
【００６７】
（付記１０）それぞれが受信する2つ以上のサブグリッドを備える前記グリッドが、前記検証インスタンスの１つを備えることを特徴とする付記１記載の方法。
【００６８】
（付記１１）前記サブグリッドの1つ又は複数の第１のものが、前記検証インスタンスの1つ又は複数の第１のものを第１の1つ又は複数のパラメータ群を用いて実行し、
前記サブグリッドの1つ又は複数の第２のものが、前記検証インスタンスの1つ又は複数の第２のものを第２の1つ又は複数のパラメータ群を用いて実行し、
前記第１のパラメータ群及び前記第２のパラメータ群が、少なくとも部分的にお互いに異なることを特徴とする付記１０記載の方法。
【００６９】
（付記１２）前記ノードの2つ以上が、お互いにヘテロジニアスであることを特徴とする付記１記載の方法。
【００７０】
（付記１３）実行するよう1つ又は複数の媒体内に実施され、実施されると、
回路にアクセスし、
それぞれが1つ又は複数のタスクを備える1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを前記回路上で生成し、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させ、かつ、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行するよう動作可能であることを特徴とする、1つ又は複数のグリッドを用いて1つ又は複数の回路を検証するロジック。
【００７１】
（付記１４）前記検証インスタンスのそれぞれの実行を監視し、
前記検証インスタンスの第１のものが、1つ又は複数の終結基準に到達した場合、前記第１の検証インスタンスを終結させるよう更に動作可能であることを特徴とする付記１３記載のロジック。
【００７２】
（付記１５）前記第１の検証インスタンスを終結させた後、1つ又は複数の到達状態を前記第１の検証インスタンスから前記検証インスタンスの1つ又は複数の第２のものに通信するよう更に動作可能であることを特徴とする付記１４記載のロジック。
【００７３】
（付記１６）前記第２の検証インスタンスに通信した前記到達状態を用いて前記第２の検証インスタンスの実行を続けるよう更に動作可能であることを特徴とする付記１５記載のロジック。
【００７４】
（付記１７）前記回路の状態空間を区画化し、
前記区画のそれぞれにおいて、前記シードの1つ又は複数を生成し、
前記区画を前記グリッドにわたって前記タスク及び前記シードとともに分散させ、
各検証インスタンスを前記区画の1つ又は複数に対して実行するよう更に動作可能であることを特徴とする付記１３記載のロジック。
【００７５】
（付記１８）前記区画を過小近似して、前記区画と関連した2進判定図（BDD）の容量を制御するよう更に動作可能であることを特徴とする付記１７記載のロジック。
【００７６】
（付記１９）前記検証インスタンスの1つ又は複数がそれぞれ、
前記回路上の充足可能性（SAT）ベース境界モデル検査の1つ又は複数のインスタンスと、
前記回路の状態空間全体未満をそれぞれが包含する、前記回路上の公式な検証（FV）の1つ又は複数のインスタンスとのうちの1つ又は複数を備えることを特徴とする付記１３記載のロジック。
【００７７】
（付記２０）前記検証インスタンスの1つ又は複数の第１のものを実行する工程が、前記検証インスタンスの1つ又は複数の第２のものとは無関係に前記第１のインスタンスを実行する工程を備えることを特徴とする付記１３記載のロジック。
【００７８】
（付記２１）前記検証インスタンスの2つ以上をお互いに並列に実行するよう更に動作可能であることを特徴とする付記１３記載のロジック。
【００７９】
（付記２２）それぞれが受信する2つ以上のサブグリッドを備える前記グリッドが、前記検証インスタンスの１つを実行することを特徴とする付記１３記載のロジック。
【００８０】
（付記２３）前記サブグリッドの1つ又は複数の第１のものが、前記検証インスタンスの1つ又は複数の第１のものを第１の1つ又は複数のパラメータ群を用いて実行し、
前記サブグリッドの1つ又は複数の第２のものが、前記検証インスタンスの1つ又は複数の第２のものを第２の1つ又は複数のパラメータ群を用いて実行し、
前記第１のパラメータ群及び前記第２のパラメータ群が、少なくとも部分的にお互いに異なることを特徴とする付記２２記載のロジック。
【００８１】
（付記２４）前記ノードの2つ以上が、お互いにヘテロジニアスであることを特徴とする付記１３記載のロジック。
【００８２】
（付記２５）回路にアクセスする手段と、
前記回路上で1つ又は複数の検証インスタンスを実行するための1つ又は複数のシードを生成する手段であって、各検証インスタンスが1つ又は複数のタスクを備える手段と、
複数のノードを備えたグリッドにわたってタスク及び前記シードを分散させる手段と、
前記シードを用いて、前記タスクによって前記グリッド内の前記ノードで前記検証インスタンスを実行する手段とを備えることを特徴とする、1つ又は複数のグリッドを用いて1つ又は複数の回路を検証するシステム。
【００８３】
（付記２６）大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当てる工程と、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成する工程と、
減縮回路毎に遷移関係（TR）を生成する工程と、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成する工程とを備えることを特徴とする、検証するよう1つ又は複数の回路を処理する方法。
【００８４】
（付記２７）前記減縮回路の全体状態空間、又は、
前記減縮回路の前記全体状態空間の一部分のみによって減縮回路毎の前記TRを生成する工程を更に備えることを特徴とする付記２６記載の方法。
【００８５】
（付記２８）前記大容量回路をシミュレートする工程が、
前記大容量回路を初期状態からシミュレートして、前記大容量回路の1つ又は複数の第１の到達可能状態をそれぞれが備える1つ又は複数のベクトルを生成する工程と、
前記大容量回路に関連した1つ又は複数のラッチ変数を選択する工程と、
前記ベクトルにおける前記到達可能状態の1つ又は複数の第１のものによって前記ラッチ変数に値を割り当てる工程とを備え、
前記減縮回路を生成する工程が、前記ラッチ変数に割り当てられた値によって前記大容量回路を合成する工程を備え、
前記減縮回路上の前記検証インスタンスの前記初期状態を生成する工程が、前記ベクトル内の前記到達可能状態の1つ又は複数の第２のものによって前記初期状態を生成する工程を備えることを特徴とする付記２６記載の方法。
【００８６】
（付記２９）深度優先探索（DFS）に関連した変数順序によって前記ラッチ変数を選択する工程を更に備えることを特徴とする付記２８記載の方法。
【００８７】
（付記３０）前記減縮回路が1つ又は複数の基準を満たすことができない場合、ラッチ変数の選択と、前記ラッチ変数への値の割り当てと、前記基準を満たす1つ又は複数の減縮回路を生成するための前記大容量回路の合成とを繰り返す工程を更に備えることを特徴とする付記２８記載の方法。
【００８８】
（付記３１）前記減縮回路上の前記検証インスタンスの1つ又は複数のそれぞれが、
前記減縮回路上の充足可能性（SAT）ベース境界モデル検査（BMC）の1つ又は複数のインスタンスと、
前記減縮回路の状態空間全体未満をそれぞれが包含する、公式な検証（FV）の1つ又は複数のインスタンスとのうちの1つ又は複数を備えることを特徴とする付記２６記載の方法。
【００８９】
（付記３２）前記TR及び前記初期状態群を、複数のノードを備えたグリッドにわたって分散させる工程と、
前記グリッド内の前記ノードを用いて、前記TRをお互いに並列に処理する工程とを更に備えることを特徴とする付記２６記載の方法。
【００９０】
（付記３３）静的抽象化を用いて、前記1つ又は複数の縮減回路を生成する工程を更に備えることを特徴とする付記２６記載の方法。
【００９１】
（付記３４）前記初期状態群を生成する工程が、
1つ又は複数の2進判定図（BDD）を用いる工程と、
前記減縮回路上で1つ又は複数のシミュレーションを実行する工程との1つ又は複数を備えることを特徴とする付記２６記載の方法。
【００９２】
（付記３５）
実行するよう1つ又は複数の媒体内に符号化されており、実行されると、
大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当て、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成し、
減縮回路毎に遷移関係（TR）を生成し、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成するよう動作可能であることを特徴とする、検証するよう1つ又は複数の回路を処理するロジック。
【００９３】
（付記３６）前記減縮回路の全体状態空間、又は、
前記減縮回路の前記全体状態空間の一部分のみによって減縮回路毎の前記TRを生成するよう更に動作可能であることを特徴とする付記３５記載のロジック。
【００９４】
（付記３７）前記大容量回路をシミュレートして、
前記大容量回路を初期状態からシミュレートして、前記大容量回路の1つ又は複数の第１の到達可能状態をそれぞれが備える1つ又は複数のベクトルを生成し、
前記大容量回路に関連した1つ又は複数のラッチ変数を選択し、
前記ベクトルにおける前記到達可能状態の1つ又は複数の第１のものによって前記ラッチ変数に値を割り当て、
前記減縮回路を生成して、前記ラッチ変数に割り当てられた値によって前記大容量回路を合成し、かつ、
前記減縮回路上の前記検証インスタンスの前記初期状態を生成して、前記ベクトル内の前記到達可能状態の1つ又は複数の第２のものによって前記初期状態を生成するよう更に動作可能であることを特徴とする付記３５記載のロジック。
【００９５】
（付記３８）深度優先探索（DFS）に関連した変数順序によって前記ラッチ変数を選択するよう更に動作可能であることを特徴とする付記３７記載のロジック。
【００９６】
（付記３９）前記減縮回路が1つ又は複数の基準を満たすことができない場合、ラッチ変数の選択と、前記ラッチ変数への値の割り当てと、前記基準を満たす1つ又は複数の減縮回路を生成するための前記大容量回路の合成とを繰り返すよう更に動作可能であることを特徴とする付記３７記載のロジック。
【００９７】
（付記４０）前記減縮回路上の前記検証インスタンスの1つ又は複数それぞれが、
前記減縮回路上の充足可能性（SAT）ベース境界モデル検査（BMC）の1つ又は複数のインスタンスと、
前記減縮回路の状態空間全体未満をそれぞれが包含する、公式な検証（FV）の1つ又は複数のインスタンスとのうちの1つ又は複数を備えることを特徴とする付記３５記載のロジック。
【００９８】
（付記４１）前記TR及び前記初期状態を、複数のノードを備えたグリッドにわたって分散させ、
前記グリッド内の前記ノードを用いて、前記TRをお互いに並列に処理するよう更に動作可能であることを特徴とする付記３５記載のロジック。
【００９９】
（付記４２）静的抽象化を用いて、前記1つ又は複数の減縮回路を生成するよう更に動作可能であることを特徴とする付記３５記載のロジック。
【０１００】
（付記４３）前記初期状態群を生成して、
1つ又は複数の2進判定図（BDD）を用い、
前記減縮回路上で1つ又は複数のシミュレーションを実行するか、
1つ又は複数のBDDを用い、1つ又は複数のシミュレーションを前記減縮回路上で実行するよう更に動作可能であることを特徴とする付記３５記載のロジック。
【０１０１】
（付記４４）
大容量回路をシミュレートして、前記大容量回路に関連した1つ又は複数のラッチ変数に1つ又は複数の値を割り当てる手段と、
前記大容量回路からの1つ又は複数の減縮回路を、前記ラッチ変数に割り当てられた前記値によって生成する手段と、
減縮回路毎に遷移関係（TR）を生成する手段と、
前記TRによって前記減縮回路上の1つ又は複数の検証インスタンスの初期状態群を生成する手段とを備えることを特徴とする、検証するよう1つ又は複数の回路を処理するシステム。
【図面の簡単な説明】
【０１０２】
【図１】1つ又は複数のグリッドを用いて1つ又は複数の回路を解析するシステム例を示す図である。
【図２】1つ又は複数のグリッドにわたって分散させた複数シードSAT‐BMCランを用いた1つ又は複数の回路の解析例を概念的に示す図である。
【図３】図１に示すシステム内のグリッド管理モジュール例を示す図である。
【図４】図３に示すグリッド管理モジュール内の有機ジョブ・コントローラ（ＯＪＣ）の例を示す図である。
【図５】図４に示すＯＪＣによる動的ジョブ制御（ＤＪＣ）の例を示す図である。
【図６】1つ又は複数のグリッドを用いて１つ又は複数の回路を解析する方法例を示す図である。
【図７】解析するための、比較的大容量の1つ又は複数の回路の処理の例を示す図である。
【図８】解析するための、比較的大容量の1つ又は複数の回路の処理の例を更に示す図である。
【図９】BMCの高深度化を促進するために1つ又は複数のシミュレーションを用いる例を示す図である。
【図１０】解析するための、比較的大容量の1つ又は複数の回路を処理する方法の例を示す図である。
【符号の説明】
【０１０３】
１０  システム
１２  回路
１４  ネットワーク
１６  グリッド
１８  サブグリッド
２０  ノード
２２  サーバ
２４  区画化モジュール
２６  グリッド管理モジュール
２８  データ
３０  コンピュータ・システム
３２  OJC
３４  グリッド・リソース・マネージャ
３６  サイト・リソース・マネージャ
３８  ウェブ・ポータル
４０  OJCスクリプト
４２  OJCインタプリタ
４４  ジョブ制御部
７０  処理
７２  処理
７４  TRスライス
８０  初期状態
９０  初期状態
【図１】
2007012062.tif 000004
【図２】
2007012062.tif 000005
【図３】
2007012062.tif 000006
【図４】
2007012062.tif 000007
【図５】
2007012062.tif 000008
【図６】
2007012062.tif 000009
【図７】
2007012062.tif 000010
【図８】
2007012062.tif 000011
【図９】
2007012062.tif 000012
【図１０】
2007012062.tif 000013