(57)【要約】      （修正有）【課題】  回路設計に使用される不変性検査に関する欠点及び問題点を軽減又は解消すること。 【解決手段】  １以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行する。初期状態及びエラー状態に対する状態空間を第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを実行し、状態空間を１以上の第１ステップによる第１方向で検索するために、ＦＳＭの１以上の第３ステップを実行する。【選択図】  図１
2006012134.tif 000002
【特許請求の範囲】
【請求項１】
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行するステップ；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行するステップ；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行するステップ；
を有することを特徴とする不変性を検査する方法。
【請求項２】
請求項１記載の方法であって、１以上のＢＤＤが、１以上のハードウエア要素、１以上のソフトウエア要素又は１以上の組み込まれた論理要素に対応することを特徴とする方法。
【請求項３】
請求項１記載の方法であって、前記第１方向のＦＳＭの状態空間の検索と前記第２方向のＦＳＭの状態空間の検索とを、最終的な結果に達するまで交互に継続することを特徴とする方法。
【請求項４】
請求項３記載の方法であって、前記第１方向でＦＳＭのステップを実行することに関する１以上のコストが、ＦＳＭのステップを実行する場合の最大コストより成る閾値を超える場合に：
前記第１方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第２方向でのＦＳＭのステップの実行だけを継続するステップ；並びに
前記第２方向でＦＳＭのステップを実行することに関する１以上のコストが、前記閾値を超える場合に：
前記第２方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第１方向でのＦＳＭのステップの実行だけを継続するステップ；
を有することを特徴とする方法。
【請求項５】
請求項１記載の方法であって、ＦＳＭの１以上の第１ステップを実行するステップに先立って：
前記第１方向で第１イメージを、前記第１方向とは逆の前記第２方向で第２イメージを計算するステップ；及び
前記第１イメージの算出に関連する１以上のコストが前記第２イメージの算出に関連する１以上のコストより少ない場合に、ＦＳＭの状態空間を前記第２方向で検索する前に、ＦＳＭの状態空間を前記第１方向で検索するステップ；
を有することを特徴とする方法。
【請求項６】
１以上の媒体の中で実行時にエンコードされる論理プログラムを実行させる論理装置であって：
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行するステップ；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行するステップ；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行するステップ；
を実行させる不変性を検査する論理装置。
【請求項７】
請求項６記載の論理装置であって、１以上のＢＤＤが、１以上のハードウエア要素、１以上のソフトウエア要素又は１以上の組み込まれた論理要素に対応することを特徴とする論理装置。
【請求項８】
請求項６記載の論理装置であって、前記第１方向のＦＳＭの状態空間の検索と前記第２方向のＦＳＭの状態空間の検索とを、最終的な結果に達するまで交互に継続することを特徴とする論理装置。
【請求項９】
請求項８記載の論理装置であって、前記第１方向でＦＳＭのステップを実行することに関する１以上のコストが、ＦＳＭのステップを実行する場合の最大コストより成る閾値を超える場合に：
前記第１方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第２方向でのＦＳＭのステップの実行だけを継続するステップ；並びに
前記第２方向でＦＳＭのステップを実行することに関する１以上のコストが、前記閾値を超える場合に：
前記第２方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第１方向でのＦＳＭのステップの実行だけを継続するステップ；
を実行させることを特徴とする論理装置。
【請求項１０】
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行する手段；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスする手段；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較する手段；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止する手段；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行する手段；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスする手段；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較する手段；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止する手段；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行する手段；
を有することを特徴とする不変性を検査するシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、一般に回路設計に関連し、特に不変性検査（ｉｎｖａｒｉａｎｔ  ｃｈｅｃｋｉｎｇ）に関連する。
【背景技術】
【０００２】
本願はＵ．Ｓ．Ｃ§１１９（ｅ）に基づく２００４年５月２１日付けの米国仮出願第６０／６７３，３５９号に関連する。
【０００３】
順序付き二分決定グラフ（ＯＢＤＤ）に基づく不変性検査は回路設計における（成立すべき条件を示す）アサーションを検査する好ましい方法である。ＯＢＤＤによる不変性検査は、例えば境界モデル検査（ＢＭＣ）とは異なり、条件の充足性及び非充足性の双方の検証機能を与える。このことは、例えば抽象詳細化（ａｂｓｔｒａｃｔｉｏｎ  ｒｅｆｉｎｅｍｅｎｔ）の場合に重要であるかもしれない。その場合には一連の誤り否定及び以後の詳細化の後に、ある属性が最終的に正しいことを証明する。ＯＢＤＤによる不変性検査は、２方向にわたることを許容し、各方向は：初期状態より前方又は可能性のある誤り状態から後方である。１つの方向は相当に一層効率的な演算機能を提供するかもしれない。例えば、１つの方向は少数のステップで固定点に到達するかもしれない。別の例としては、１つの方向では演算の複雑さが非常に少ないかもしれない。しかしながら、ユーザはどの方向がより多くの効率的な演算をもたらすかもしれないことを事前には知らない。
【発明の開示】
【発明が解決しようとする課題】
【０００４】
本発明の課題は、回路設計に使用される不変性検査に関する欠点及び問題点を軽減又は解消することである。
【課題を解決するための手段】
【０００５】
一実施例によれば、不変性を検査する方法は、初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行するステップを含む。本方法は、ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスするステップ、前記第１特性を１以上の第１の所定の基準と比較するステップ、前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を停止するステップ、ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを実行するステップ、ＦＳＭの１以上の第２ステップに対応する第２特性にアクセスするステップ、前記第２特性を１以上の第２の所定の基準と比較するステップ、前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を停止するステップ、ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを実行するステップを有する。
【発明を実施するための最良の形態】
【０００６】
以下、本発明の実施例による不変性を検査する方法、論理装置及びシステムが説明される。この場合において、論理装置又は論理要素なる語は、ソフトウエアで構成される論理プログラムや、ハードウエアで構成される論理回路を含む概念である。
【０００７】
本発明の特定の実施例は、１以上の技術的利益をもたらす。例えば、特定の実施例は、前方及び後方検索を互いにインターリーブするＯＢＤＤによる動的な手法をもたらす。この手法は、より短い方向を選択することを促し、それと同時に冗長的な計算に起因するオーバーヘッドを限定することを促す。特定の実施例は、異なる変数順序を有する２つのＯＢＤＤを使用し、いくらかの追加的なオーバーヘッドと引き替えに改善された完了（プログラムの完了）をもたらす。これらの手法は、１方向の検査におけるかなりの効率の利得をもたらす。特定の実施例は単独の経路で前方及び後方（順方向及び逆方向）検索を同時に実行するが、従来の手法は典型的には探索空間を近似する又は枝刈りする（探索すべき枝数を減らす）ために１つの掃引を行い、その後に実際の検証を行うために別方向で別の掃引を行う、或いはこのプロセスを反復さえしていた。特定の実施例は、標準的な順方向検索アルゴリズムを置換する。
【０００８】
特定の実施例は上述の技術的利益の全部又は一部をもたらすかもしれないし、全くもたらさないかもしれない。特定の実施例は１以上の他の技術的利益をもたらし、１以上のそれらは図面、明細書及び特許請求の範囲から当業者に明白になるであろう。
【０００９】
本発明並びにその特徴及び利益をより完全に理解するため、添付図面に関連する以下の説明が参照される。
【実施例１】
【００１０】
図１は不変性検査に関する例示的なシステム１０を示す。参照する図はディジタル回路（適切ならば、複数のディジタル要素を含む）のようなハードウエア要素の絵を含む。システム１０は、コンピュータシステム１２、ツール１４及びデータ１６を含む。コンピュータシステム１２はユーザが入力を与えること及び検証ツール１４から出力を受信することができるようにする。以下に説明されるように、ツール１４は設計内容の１以上の特性（の条件の充足性）を検証すること、設計内容の１以上の特性の（条件の非充足性）を検証すること、或いは双方を行うことを試みるかもしれない。ツール１４は、充足性の検証、非充足性の検証又は双方を試みるためにデータ１６を使用してもよい。ツール１４は、設計内容の１以上の特性の条件充足性を検証すること、設計内容の１以上の特性の条件の非充足性を検証すること又は双方を行うことを試行するハードウエア、ソフトウエア又は双方を含んでもよい。コンピュータシステム１２、ツール１４及びデータ１６は互いに離れているように図示及び記述されているが、本発明は、コンピュータシステム１２、ツール１４及びデータ１６の２以上が適切ないかなる度合いでもそれで互いに結合されることをも想定している。非限定的な例として、特定の実施例では、ツール１４はコンピュータシステム１２のソフトウエア要素であり、データ１６はコンピュータシステム１２に格納されてもよい。
【００１１】
順次的なシステム（シーケンシャルシステム）の複雑さが増大すると、到達可能性の分析を実行できるようにするには効率的な技法が必要になる。到達可能な状態の集合は極めて大きくなり得るので、その集合の明示的な表現（例えばリスト形式による表現）は、どの環境下でも不適切である。ＯＢＤＤは状態集合の特性関数を表現できる。そのような象徴的な表現形式は、到達可能な状態を算出するために実行される操作に良く機能し：到達可能な状態が（子を巡回した後に孫を巡回する）幅優先検索又は横型検索に従って算出されるならば、特性関数による表現は、１つの演算の中で総ての対応する良好な状態の算出を可能にする。このため、「象徴的な幅優先検索」なる語がしばしば使用される。演算の複雑さは、生じる状態集合のＯＢＤＤのサイズに依存する。
【００１２】
不変性検査は状態空間検索に基づく率直なフォーマル検証アプリケーションである。常に全体的に保持する特性が検査される、例えば  ｏｖｅｒｆｌｏｗ＝０。状態空間検索の間に、その特性に違反する状態に到達すると、その検索は終了し、「失敗」（ｆａｉｌｅｄ）を返す。特性違反状態を発見せずに検索が固定点に達すると、その検索は「合格」（ｐａｓｓｅｄ）を返す。
【００１３】
到達可能な状態の算出は、順次的なシステムの最適化及び検証にとって中核的なタスクである。ＯＢＤＤによる検索技法の本質的な部分は、その遷移関係である：
【００１４】
【数１】
2006012134.tif 000003
これは、総てのラッチの遷移関係の結合である。δｉはｉ番目のラッチの伝達関数であり、ｘ，ｙ及びｅは現在の状態、次の状態及び入力変数を表す。このモノリシックの遷移関係は、単一のＯＢＤＤとして表現され、通常は大きすぎて到達可能な状態を算出することを許容しない。ときに、モノリシックな遷移関係は複数のＯＢＤＤで表現する場合でさえ大きすぎることがある。従って、更に洗練された到達可能状態算出法は分割された遷移関係（即ち、ＯＢＤＤのクラスタ）を利用し、その各々が一群のラッチの遷移関係を表現する。一群のラッチＰ１，．．．，Ｐｊにわたって分割された遷移関係は、次のように記述される：
【００１５】
【数２】
2006012134.tif 000004
到達可能な状態の計算は、一群の既に到達した状態Ｒの反復的なイメージ（ｉｍａｇｅ）計算Ｉｍｇ（ＴＲ，Ｒ）より成る：
【００１６】
【数３】
2006012134.tif 000005
分割された遷移関係を利用することで、イメージ計算はＰｉにわたって反復することができ、∃演算は積の演算（初期の数量化）中に適用できる：
【００１７】
【数４】
2006012134.tif 000006
ここで、νｉは後続のＴＲｋ，（ｉ＜ｋ≦ｊ）に現れない（ｘ∪ｅ）中の変数である。
【００１８】
ＡｎｄＥｘｉｓｔ又はＡｎｄＡｂｓｔｒａｃｔ演算は、２つの関数（ここでは分割）にＡＮＤ演算を実行し、存在する定量化（∃ｘｉｆ＝（ｆｘｉ＝１∨ｆｘｉ＝０））を所与の変数群に同時に適用し、その変数は残りの分割のサポートにはない。通常のＡＮＤ演算とは異なり、ＡｎｄＥｘｉｓｔ演算は、結果のＯＢＤＤのサイズに関する急増する上限を有するだけであるが、多くの実用的アプリケーションに関し、イメージ計算中にＯＢＤＤサイズが破裂することを防ぐ。
【００１９】
複数の分割を共に結合するスケジュールを見出す標準的な方法はＩＷＬＳ９５による方法であり、ＡｎｄＥｘｉｓｔ演算に含まれる変数の数を最小化する強引な方法（ｇｒｅｅｄｙ  ｓｃｈｅｍｅ）を使用する。ＩＷＬＳ９５方法はＶＩＳパッケージでの標準的な分割法である。
【００２０】
順方向検索及び逆方向検索は不変性検査問題に等しく適用可能である。検索方向は不変性検査問題の複雑性に重要な影響をしばしば与えることを実験は示している。問題は、どの方法が他方より好ましいかを前もって見出すことが不可能なことにある。本発明の特定の実施例は、実行中に方向を選択することによって順方向検索及び逆方向検索を互いに組み合わせる発見的方法を使用する。
【００２１】
図２Ａ及び２Ｂは順方向及び逆方向検索を組み合わせる例を示す。順方向サーチ１８は、初期状態Ｉから始まる幅優先サーチ（ＢＦＳ：ｂｒｅａｔｈ−ｆｉｒｓｔ  ｓｅａｒｃｈ）に従ってタマネギの皮のような「オニオンリング」を付加することによって、探索される到達可能な状態空間が広がる。逆方向サーチ２０は、特性違反状態Ｐから始まるプレイメージ（ｐｒｅｉｍａｇｅ）計算を反復することで、到達可能な誤り状態により設定された状態に伸びる。図２Ａでは、駄目な特性の場合には、順方向サーチ１８は最終的には逆方向サーチ２０と交わる。オニオンリング数はエラーの深さを決定する。２つの特殊な場合が生じるかもしれない：（１）到達可能な状態空間が、考察中の特性に違反する総ての状態を含む総ての可能な状態（即ち、ｎ個の状態ビットが与えられる場合に２ｎ個の状態）を網羅する場合；（２）駄目な状態集合が、２ｎ個の可能な総ての状態（初期状態及び到達可能な状態の総てを含む）を網羅する場合である。図２Ｂでは、合格する特性の場合に、順方向サーチ１８及び逆方向サーチ２０の各々が互いに交わらずに固定点にそれぞれ到達している。しかしながら、固定点に到達した順方向サーチ１８又は逆方向サーチ２０が終了すると、その特性は正しいことが証明される。
【００２２】
組み合わせられた検索手法は少なくとも次の利点を有する。そのような手法は演算負担のより軽い方向を選択することを促す。そのような手法は、少数の演算ステップで固定点に到達する見込みのある方向を選択することを促す。駄目な特性の場合には検索は最終的には交わるので、何らの計算も冗長的ではない；それらは解（ソリューション）に総て寄与している。しかしながら、上述のことは事前には知られていない。結合された検索は次の事項に適切に取り組む必要がある。合格する特性の場合に、一方の方向は他方よりも先に固定点に到達するので、集束しない方向の計算は冗長的である；それらはソリューションに寄与していない。２方向についての演算のコストは非常に不均衡なので、１方向を試みることさえ非常に高価になることが判明するかもしれない。２つの状態集合をＯＢＤＤとして表現することは、全体的な複雑さの問題を増やしてしまう。
【００２３】
特定の実施例では、インターリーブする発見的方法は、組み合わせた検索の上記の利点を最大化し、それと同時に上記の事項に対処しようとする。インターリーブする発見的方法は、イメージ又はプレイメージを計算することに関連するコストを評価することによって検索方向を動的に決定する。コストメトリックは、プレイメージ計算の分割された遷移関係に関する反復計算中に、最大のＯＢＤＤサイズになる。最初のステップでは、インターリーブする発見的方法は、初期のコストを決定するために各方向のイメージを計算する。後続のステップでは、計算は、その最新の計算実行におけるコストのより低い方向に進行し、即ち、そのコストが他方向の最新のイメージのコストを超えるまで、一方の方向に計算が進行する。
【００２４】
この点に関して行う判定は何らの手動的なパラメータ設定を必要とせず、完全に動的且つ自己整合的なプロセスを与える。通常は、順方向検索に関するコスト及び逆方向検索に関するコストは互いにかなり相違する。その結果、インターリーブする発見的方法は、より良好な方向を選択するように向かう。この不均衡性を更に活用するため、イメージ計算の最大コストを限定する閾値が使用されてもよい。動作中にこの閾値を超えると、イメージ計算は中止され、インターリーブする発見的方法は、双方向の検索をディセーブルし、中止されていない方向の単方向検索に戻す。この閾値は、ある方向における法外にコスト高の計算を回避することを促す。この閾値は、ある方向で利用可能なメモリの割り当てを不均衡に超えた場合しか、イメージ計算が中止されないように、（非常に大きな値に）控えめに設定されてもよい。
【００２５】
閾値はメモリオーバーフローを引き起こす検索方向を回避するために使用されてもよい。もしも設定が比較的積極的（控えめでない）ならば、そのような閾値はアプリケーションを調整するパラメータとして使用されてもよい。異なる検索方向についてのコストが非常にアンバランスな回路については、より低い閾値は、より高価な方向でのイメージを計算するのに費やす時間をかなり減らすことができる。ある対称的な振る舞いを示す回路については、より低い閾値が効率を改善する。
【００２６】
特定の実施例では、以下のアルゴリズム例がインターリブスルアルゴリズムのメインループになっている：
【００２７】
【数５】
2006012134.tif 000007
図３は駄目な特性の場合にインターリーブするエラートレースの計算例を示す。駄目な特性の場合のエラートレースの計算（又は逆の例）は、単なる順方向又は逆方向検索の場合よりも複雑にインターリーブする。駄目な特性の場合には、順方向検査１８で算出された状態及び逆方向検索２０で算出された状態は領域２２で重なる。この交わりから、任意的な要（ピボット）となる状態が選択される。この状態は、初期状態から到達可能であり、その特性に反する状態はこの状態から到達可能である。エラートレースは、初期状態Ｉからピボット状態ｐを及びそこから状態Ｐを導出する。エラートレースの計算は、双方の検索に関し、オニオンリング（即ち、各反復の最前線の状態）が保存される。（Ｉからｐへの）エラートレースの第１部分は、ｐから始まってＩへ戻るプレイメージ計算を利用し、その結果をオニオンリングに再構築して算出される。反復の各々について、特定のオニオンリングからの任意的な状態が選択される。（ｐからＰへの）エラートレースの第２部分は、ｐから始まりＰへ至るイメージ計算を利用して同様な手法で算出される。そして、双方の部分は、完全なエラートレースを行うために結合される。その計算のオニオンリングを保存することは、オーバーヘッドをその計算に付加する。インターリーブに関するこのオーバーヘッドは、単方向のアプローチに関するものよりも小さいかもしれない。その理由は、インターリーブはより安価な方向を選択する点にあるかもしれない。従って、オニオンリングを格納することは、より能率的であるかもしれない。
【００２８】
２つの遷移関係及び２つの完全に異なる状態集合（到達可能な状態及び駄目な状態）が存在することは、表現を複雑にし、ＯＢＤＤの中でかなり大きなサイズのオーバーヘッドを招くかもしれない。イメージ計算中のＡｎｄＥｘｉｓｔ演算は、変数再配列プロセス及びその結果の変数順序を支配する傾向がある。ＯＢＤＤの変数順序と異なる条件で２つのサーチ及び２つのＡｎｄＥｘｉｓｔ操作を行わせることは、１つの方向で大きなＯＢＤＤを生成することに起因して、或いは２つのＡｎｄＥｘｉｓｔ操作の結果による前後の再配列化に起因してパフォーマンスに不利に影響するかもしれない。特定の実施例では、これらの問題に対する解決手段は、変数順序が互いに異なる２つのＯＢＤＤを利用することである：１つのＯＢＤＤは順方向検索用であり、もう１つのＯＢＤＤは逆方向検索用である。
【００２９】
２つのＯＢＤＤを利用する利点は、各ＯＢＤＤで１つの検索しか実行されず、１つの主要な状態集合しか表現されることを要しないことである。その結果、変数再配列は１つのＡｎｄＥｘｉｓｔ操作だけを標的とするので、変数再配列は良好な結果を生成する。この利点は、多くの場合に、２つのＯＢＤＤを利用するＯＢＤＤ法に関連する欠点に勝る傾向がある。互いに異なる変数順序を有する２つのＯＢＤＤは、どのノードも互いに共用できない。最悪の場合、これは２のべき乗で破裂することを招く。しかしながら、最良の場合には、互いに異なる２つの関数の表現が指数関数的により小さくできる。２つのＯＢＤＤを導入して維持することはオーバーヘッドを生み出す。小型の場合には、そのようなオーバーヘッドは重大になるかもしれない。利用可能なメモリは２つのＯＢＤＤに割り当てられるであろう。このことは問題になるかもしれない。なぜなら、どの程度多くのメモリを各ＯＢＤＤが必要とするか及びどの程度多くの様々なキャッシュやスタックが加わるかもしれないかは不明だからである。
【００３０】
到達可能な状態集合及び駄目な状態集合の間で算出された交わりで駄目な特性を検出することは、ＯＢＤＤ間の連絡を必要とする。図２Ａは上述したような駄目な特性の例を示す。互いに異なる変数順序を有する２つのＯＢＤＤの間の交差は、最悪の場合、指数関数的になる。特定の実施例は、交差の存在を検査し、一方のＯＢＤＤから他方へのトンネル通信を行うために例えば以下のアルゴリズムを使用する。
【００３１】
【数６】
2006012134.tif 000008
上記のアルゴリズムは、ｆを表すＯＢＤＤ−Ｆ及びｇを表すＯＢＤＤ−Ｇが互いに１に対する割り当て評価を共用するか否かを検査する。そのような場合、アルゴリズムは「真」を変える。そのような割当が存在しなければ、アルゴリズムは「偽」を返す。アルゴリズムは、総て充足する割り当てを記号的にテストしながら、ＢＦＳ順にｗ．ｌ．ｏ．ｆ  Ｆを検索する。ｇは異なる変数順序でＧで表現されるので、ｇは単に並列的に検索できない。その代わりに、ｇはｆの再帰（反復）における現在の分岐変数によって分解される。現在の再帰点（Ｆ’，Ｇ’）にて、Ｆ’のトップノードがインデックスｘｉを有するならば、以後の再帰的なペアは（Ｆ’｜ｘｉ＝０，Ｇ’｜ｘｉ＝０）及び（Ｆ’｜ｘｉ＝１，Ｇ’｜ｘｉ＝１）になる。アルゴリズムは、ペア（真，真）に到達できたときは常に「真」を返して終了する。このアルゴリズムの実行時間は最悪の場合指数関数的に増えるかもしれない。これは、例えば、ｇがＯＢＤＤ−Ｆの変数順序で指数関数的に大きなＯＢＤＤサイズを有し、ｆが高密である（即ち、各変数がＦ中の総ての経路について検査される）場合に起こるかもしれない。
【００３２】
ｆが高密でないときは常に計算は非常に簡潔になる。上記のアルゴリズムは、ＯＢＤＤのＩＴＥ演算の実行時間に匹敵する平均的な実行時間を有するかもしれない。上記のアルゴリズムの算出されるテーブルは、ＩＴＥ演算に類似するキャッシュとして実現されもよく、それは算出されるテーブルの最大メモリ消費量を制限する。特定の実施例では、上記のアプリケーションには、ＯＢＤＤが交わるか否かを知ることで十分である。交わり自身の計算は必要とされない。アルゴリズムの副産物として、交わりの１つの充足する割当が容易に算出できる。特定の実施例では、２つのＯＢＤＤ法が、１つのＯＢＤＤインターリブ法と同じ発見的方法及びメトリックを使用する。
【００３３】
特定の実施例では、不変性（成立すべき条件を示すアサーション）の検査は、初期状態から誤りのある状態への状態遷移の経路を発見すること、或いはそのような経路が存在しないことを立証することを含む。インターリブによる不変性検査は次の２つの地点から始まる：（１）システムの初期状態及び（２）特性で指定される可能な誤り状態（又は悪い状態）。第１ステップでは、双方の開始点に対する反復計算がなされる、即ち、システムの初期状態から１回の反復後に到達可能な状態と、１遷移の範疇で到達可能なエラー状態による状態とが算出される。第１ステップは、各方向の計算に対するコストを得るための測定として機能する。このコストは、反復されるイメージ演算中の二分決定グラフ（ＢＤＤ：ｂｉｎａｒｙ  ｄｅｃｉｓｉｏｎ  ｄｉａｇｒａｍ）ノードの最大数により表現される。イメージを算出するのに要する労力を表現する他のコストメトリックは十分かもしれない。
【００３４】
特定の実施例では、計算の以後のステップで、順方向及び逆方向の計算が入れ替えられ、例えば、一方の方向における反復計算は、そのコストが他方の方向における最新の反復計算のコストを超えるまで実行される。更に、一方向での計算は、その計算がコスト的に大きすぎる場合に、例えば所定のサイズの制約を超える場合に中止されてもよい。その場合に、他方向の計算は中断され、計算は一方向で進行する。計算は、以下の１以上が生じた場合に終了する：
１．総ての状態が初期状態（駄目な特性）から到達可能である。
【００３５】
２．総ての状態が悪い状態（失敗）である。
【００３６】
３．到達可能な及び悪い状態（失敗）が交わる。
【００３７】
４．順方向検索が悪い状態に到達せずに集束する（合格の特性）。
【００３８】
５．逆方向検索が到達可能な状態（合格）に到達せずに集束する。
【００３９】
特定の実施例では、駄目な特性のエラートレース（証明）の作成に関し、初期状態からエラー状態への経路は、順方向計算、逆方向計算又は双方を用いて作成されてもよい。
【００４０】
上述したように、特定の実施例では、不変性を検査する２つの方法がある：
１．初期状態から可能なエラー状態へ向かう検索（順方向）。
【００４１】
２．エラー状態から初期状態へ向かう検索（逆方向）。
【００４２】
一方の方向は以下の理由の１以上によって他方より好ましいかもしれない：
１．一方の方向は他方よりも少ないステップで集束する。
【００４３】
２．一方の方向は他方よりも少ないステップで総ての状態に到達する。
【００４４】
３．一方の方向の計算コスト他方よりも非常に少ない。
【００４５】
上記のどれが生じるかどうか及び演算はコスト的にどの程度であるかを事前に判定する方法はない。特定の実施例では、この点にインターリブ不変性検査の利点がある。インターリーブ不変性検査は進行する方向を動的に決定するので、より効率的な方向を選択する一層多くの見込みがある。動的なコスト測定を行うことによって、何らの固定的な閾値を要しない。従って、本方法は基礎にするＢＤＤのサイズによらず尺度変更できる。更に、特性が良好でなければ、順方向及び逆方向双方の計算がエラートレースを計算するために共に使用される。従って、何らの計算も浪費されない。
【００４６】
図４は不変性検査の方法例を示す。本方法はステップ１００から始まり、初期状態及びエラー状態に対する初期の方向でＦＳＭの状態空間を検索するために、ツール１４は１以上のＢＤＤに対応するＦＳＭの１以上の初期ステップを実行する。ステップ１０２では、ツール１４はＦＳＭの１以上の初期ステップに対応するプロファイル（特性）にアクセスする。ステップ１０４では、ツール１４はその特性を１以上の所定の基準と比較する。ステップ１０６では、ツール１４は、特性及び１以上の所定の基準の比較結果に従って、初期の方向における状態空間の検索を止める。ステップ１０８では、ＦＳＭの１以上の先行するステップからの部分的な結果に従って、初期状態及びエラー状態に関する先行する方向とは逆の次の方向で状態空間を検索するために、ツール１４はＦＳＭの１以上の次のステップを実行する。ステップ１１０では、ツール１４はＦＳＭの１以上の次のステップに対応する特性にアクセスする。ステップ１１２では、ツール１４はその特性と１以上の所定の基準とを比較する。ステップ１１４では、特性と１以上の所定の基準との間の比較結果に従って、次の方向での状態空間の検索を止める。ステップ１１６では、ＦＳＭの状態空間の検索を終える条件に合致するならば、本方法は終了する。ステップ１１６にて、ＦＳＭの状態空間の検索を終える条件に合致しなかったならば、本方法はステップ１０８に戻る。図４に示される方法では特定のステップが特定の順序で生じるように図示及び記述されたが、本発明は、適切ないかなる順序でもそれで生じる図４のどの方法ステップをも想定している。
【００４７】
本発明に関する１以上の修正は当業者に明白であり、特許請求の範囲における本発明はそのような総ての修正を包含する。特許請求の範囲に反映されていない明細書中の記述は本発明を限定するものではない。
【００４８】
以下、本発明により教示される手段を例示的に列挙する。
【００４９】
（付記１）
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行するステップ；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行するステップ；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行するステップ；
を有することを特徴とする不変性を検査する方法。
【００５０】
（付記２）
付記１記載の方法であって、１以上のＢＤＤが、１以上のハードウエア要素、１以上のソフトウエア要素又は１以上の組み込まれた論理要素に対応することを特徴とする方法。
【００５１】
（付記３）
付記１記載の方法であって、前記第１方向のＦＳＭの状態空間の検索と前記第２方向のＦＳＭの状態空間の検索とを、最終的な結果に達するまで交互に継続することを特徴とする方法。
【００５２】
（付記４）
付記３記載の方法であって、前記第１方向でＦＳＭのステップを実行することに関する１以上のコストが、ＦＳＭのステップを実行する場合の最大コストより成る閾値を超える場合に：
前記第１方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第２方向でのＦＳＭのステップの実行だけを継続するステップ；並びに
前記第２方向でＦＳＭのステップを実行することに関する１以上のコストが、前記閾値を超える場合に：
前記第２方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第１方向でのＦＳＭのステップの実行だけを継続するステップ；
を有することを特徴とする方法。
【００５３】
（付記５）
付記１記載の方法であって、ＦＳＭの１以上の第１ステップを実行するステップに先立って：
前記第１方向で第１イメージを、前記第１方向とは逆の前記第２方向で第２イメージを計算するステップ；及び
前記第１イメージの算出に関連する１以上のコストが前記第２イメージの算出に関連する１以上のコストより少ない場合に、ＦＳＭの状態空間を前記第２方向で検索する前に、ＦＳＭの状態空間を前記第１方向で検索するステップ；
を有することを特徴とする方法。
【００５４】
（付記６）
付記１記載の方法であって：
前記第２特性が、第２方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを示し；
前記１以上の第２の所定の基準が、第１方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを示し；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を停止するステップが、第２方向におけるＦＳＭの最新のステップの実行に関する１以上のコストが、第１方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを超える場合に、第２方向における状態空間の検索を停止するステップより成る；
ことを特徴とする方法。
【００５５】
（付記７）
付記１記載の方法であって、ＦＳＭのステップがイメージ又はプレイメージ計算より成ることを特徴とする方法。
【００５６】
（付記８）
付記１記載の方法であって、第１方向又は第２方向での状態空間の検索が駄目な特性に遭遇した場合に、駄目な特性に対するエラートレースを計算するステップを更に有することを特徴とする方法。
【００５７】
（付記９）
１以上の媒体の中で実行時にエンコードされる論理プログラムを実行させる論理装置であって：
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行するステップ；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行するステップ；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスするステップ；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較するステップ；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止するステップ；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行するステップ；
を実行させる不変性を検査する論理装置。
【００５８】
（付記１０）
付記９記載の論理装置であって、１以上のＢＤＤが、１以上のハードウエア要素、１以上のソフトウエア要素又は１以上の組み込まれた論理要素に対応することを特徴とする論理装置。
【００５９】
（付記１１）
付記９記載の論理装置であって、前記第１方向のＦＳＭの状態空間の検索と前記第２方向のＦＳＭの状態空間の検索とを、最終的な結果に達するまで交互に継続することを特徴とする論理装置。
【００６０】
（付記１２）
付記１１記載の論理装置であって、前記第１方向でＦＳＭのステップを実行することに関する１以上のコストが、ＦＳＭのステップを実行する場合の最大コストより成る閾値を超える場合に：
前記第１方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第２方向でのＦＳＭのステップの実行だけを継続するステップ；並びに
前記第２方向でＦＳＭのステップを実行することに関する１以上のコストが、前記閾値を超える場合に：
前記第２方向でのＦＳＭのステップの実行を中止するステップ；及び
前記第１方向でのＦＳＭのステップの実行だけを継続するステップ；
を実行させることを特徴とする論理装置。
【００６１】
（付記１３）
付記９記載の論理装置であって、ＦＳＭの１以上の第１ステップを実行するステップに先立って：
前記第１方向で第１イメージを、前記第１方向とは逆の前記第２方向で第２イメージを計算するステップ；及び
前記第１イメージの算出に関連する１以上のコストが前記第２イメージの算出に関連する１以上のコストより少ない場合に、ＦＳＭの状態空間を前記第２方向で検索する前に、ＦＳＭの状態空間を前記第１方向で検索するステップ；
を実行させることを特徴とする論理装置。
【００６２】
（付記１４）
付記９記載の論理装置であって：
前記第２特性が、第２方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを示し；
前記１以上の第２の所定の基準が、第１方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを示し；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を停止するステップが、第２方向におけるＦＳＭの最新のステップの実行に関する１以上のコストが、第１方向におけるＦＳＭの最新のステップの実行に関する１以上のコストを超える場合に、第２方向における状態空間の検索を停止するステップより成る；
ことを特徴とする論理装置。
【００６３】
（付記１５）
付記９記載の論理装置であって、ＦＳＭのステップがイメージ又はプレイメージ計算より成ることを特徴とする論理装置。
【００６４】
（付記１６）
付記９記載の論理装置であって、第１方向又は第２方向での状態空間の検索が駄目な特性に遭遇した場合に、駄目な特性に対するエラートレースを計算するステップを更に有することを特徴とする論理装置。
【００６５】
（付記１７）
初期状態及びエラー状態に関する有限状態マシン（ＦＳＭ）の状態空間を第１方向で検索するために、１以上の二分決定グラフ（ＢＤＤ）に対応するＦＳＭの１以上の第１ステップを実行する手段；
ＦＳＭの１以上の第１ステップに対応する第１特性に、ユーザ入力なしに自動的にアクセスする手段；
前記第１特性を１以上の第１の所定の基準と、ユーザ入力なしに自動的に比較する手段；
前記第１特性及び前記１以上の第１の所定の基準の比較結果に従って、前記第１方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止する手段；
ＦＳＭの１以上の第１ステップによる第１の結果の一部に従って、前記初期状態及び前記エラー状態に対する状態空間を前記第１方向とは逆の第２方向で検索するために、ＦＳＭの１以上の第２ステップを、ユーザ入力なしに自動的に実行する手段；
ＦＳＭの１以上の第２ステップに対応する第２特性に、ユーザ入力なしに自動的にアクセスする手段；
前記第２特性を１以上の第２の所定の基準と、ユーザ入力なしに自動的に比較する手段；
前記第２特性及び前記１以上の第２の所定の基準の比較結果に従って、前記第２方向の前記状態空間の検索を、ユーザ入力なしに自動的に停止する手段；
ＦＳＭの１以上の第２ステップによる第２の結果の一部に従って、前記状態空間を前記１以上の第１ステップによる前記第１方向で検索するために、ＦＳＭの１以上の第３ステップを、ユーザ入力なしに自動的に実行する手段；
を有することを特徴とする不変性を検査するシステム。
【図面の簡単な説明】
【００６６】
【図１】不変性検査のシステム例を示す図である。
【図２Ａ】順方向及び逆方向検索の組み合わせ例を示す図である。
【図２Ｂ】順方向及び逆方向検索の組み合わせ例を示す図である。
【図３】誤り属性の場合にインターリーブする誤りトレースの演算例を示す図である。
【図４】不変性検査の方法例を示す図である。
【符号の説明】
【００６７】
１２  コンピュータシステム
１４  ツール
１６  データ
１８  順方向サーチ
２０  逆方向サーチ
２２  交差部
【図１】
2006012134.tif 000009
【図２Ａ】
2006012134.tif 000010
【図２Ｂ】
2006012134.tif 000011
【図３】
2006012134.tif 000012
【図４】
2006012134.tif 000013