(57)【要約】【課題】  回路検証に関する不都合、問題点あるいはその両方を軽減または解消する回路検証方法、回路検証論理及び回路検証システムを提供すること。【解決手段】  複数のエンジンを利用した回路検証方法は、複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査するステップと、前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成するステップと、前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップと、から構成される。【選択図】  図４ 
2005158073.tif 000002
【特許請求の範囲】
【請求項１】
複数のエンジンを利用した回路検証方法であって、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査するステップと、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成するステップと、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップと、
から構成されることを特徴とする方法。
【請求項２】
請求項１記載の回路検証方法であって、
前記複数の到達可能性アルゴリズムは、逆方向分割到達可能性アルゴリズム、順方向分割到達可能性アルゴリズム、順方向記号モノリシック到達可能性アルゴリズム及び逆方向記号モノリシック到達可能性アルゴリズムから構成されることを特徴とする方法。
【請求項３】
請求項１記載の回路検証方法であって、さらに、
前記複数のトレースが所定の遷移関係サイズカットオフに到達すると、前記複数のトレースを終了させるステップを、
有することを特徴とする方法。
【請求項４】
請求項１記載の回路検証方法であって、さらに、
前記複数のトレースにおいて到達したすべてのトレースを利用して、前記選択された効果的な到達可能性アルゴリズムに対する前記初期状態の集合を生成するステップを、
有することを特徴とする方法。
【請求項５】
複数のエンジンを利用した回路検証論理であって、該論理はコンピュータ実行可能な媒体において具現化され、実行時に、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査するステップと、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成するステップと、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップとを、
処理可能であることを特徴とする論理。
【請求項６】
請求項５記載の回路検証論理であって、
前記複数の到達可能性アルゴリズムは、逆方向分割到達可能性アルゴリズム、順方向分割到達可能性アルゴリズム、順方向記号モノリシック到達可能性アルゴリズム及び逆方向記号モノリシック到達可能性アルゴリズムから構成されることを特徴とする論理。
【請求項７】
請求項５記載の回路検証論理であって、さらに、
前記複数のトレースが所定の遷移関係サイズカットオフに到達すると、前記複数のトレースを終了させるステップを、
処理可能であることを特徴とする論理。
【請求項８】
請求項５記載の回路検証論理であって、さらに、
前記複数のトレースにおいて到達したすべてのトレースを利用して、前記選択された効果的な到達可能性アルゴリズムに対する前記初期状態の集合を生成するステップを、
処理可能であることを特徴とする論理。
【請求項９】
複数のエンジンを利用した回路検証システムであって、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査する手段と、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択する手段と、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成する手段と、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行する手段と、
から構成されることを特徴とするシステム。
【請求項１０】
複数のエンジンを利用した回路検証方法であって、
回路のサイズを決定するステップと、
前記回路の深さ及び困難さを推定するため、自動テストパターン生成器（ＡＴＰＧ）を利用するステップと、
前記回路のサイズ、深さ及び困難さに従って、ＡＴＰＧベースファルシフィケイションエンジン、レジスタトランスファレベル（ＲＴＬ）エンジン、深さ有界モデルチェッキング（ＢＭＣ）エンジン、充足可能性ＢＭＣ（ＳＡＴ−ＢＭＣ）エンジン、帰納ＢＭＣエンジン、分割順序付二分決定図（ＰＯＢＤＤ）エンジン、順序付二分決定図（ＯＢＤＤ）エンジン及びプリイメージエンジンからなる複数の検証エンジンから１以上を選択するステップと、
少なくとも、前記選択された検証エンジンを利用して、前記回路の１以上のプロパティの検証を試みるステップと、
から構成されることを特徴とする方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本開示は、一般に回路検証に関し、より詳細には複数のエンジンを利用した回路検証に関する。
【背景技術】
【０００２】
不変量性質（ｉｎｖａｒｉａｎｔ  ｐｒｏｐｅｒｔｙ）に関する非有界モデルチェッキングは、典型的には、記号到達可能性（ｓｙｍｂｏｌｉｃ  ｒｅａｃｈａｂｉｌｉｔｙ）を用いて解かれる。しかしながら、ＢＤＤベースの到達可能性手法は、性能の一貫性を欠く傾向があり、このため、与えられた問題に対して特定の方法を特定することを困難にする。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明は、回路検証に関する不都合、問題点あるいはその両方を軽減または解消するものである。
【課題を解決するための手段】
【０００４】
一実施例では、複数のエンジンを利用した回路検証方法は、複数の到達可能性アルゴリズムを利用して、回路上の複数のトレース（ｔｒａｃｅ）を走査するステップと、前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態集合を生成するステップと、前記回路を検証するため前記生成された初期状態集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップと、から構成される。
【０００５】
本発明の実施例は、１以上の技術的効果を提供するかもしれない。一例として、ある実施例は、様々な到達可能性方法を調停するため、少数の短い計算トレースを調べる。ある実施例は、様々な到達可能性方法を調停するため、計算トレースの自動的、ロウバストかつモジュール的検査を提供する。ある実施例は、効果を潜在的に高めるため、多様な到達可能性技術を効果的に統合する。ある実施例は、多くの場合において、以前の到達可能性アルゴリズムより効果的な規模のオーダである。ある実施例は、ＶＩＳ−Ｖｅｒｉｌｏｇベンチマークでのあらゆる不変的チェッキングプロパティ（ｉｎｖａｒｉａｎｔ  ｃｈｅｃｋｉｎｇ  ｐｒｏｐｅｒｔｙ）を完備するものであってもよい。ある実施例は、完全に自動化され、一旦始動されると人手による介入を必要としない。ある実施例は、ＢＤＤベースの到達可能性手法の性能に関する一貫性の欠如を解消するため、自動での自己調整によるトレースベースのアプローチを提供する。ある実施例は、手動による介入なく、分割されていない状態空間表現及び分割された状態空間表現を利用して、順方向と逆方向の両方向での到達可能性分析の効果を合成する。このような実施例は、ＶＩＳ−Ｖｅｒｉｌｏｇベンチマークのすべての回路に関する不変的チェックを効果的かつ自動的に完了させるものであるかもしれない。このような実施例はまた、例えば、ＢＭＣのような充足可能性（ｓａｔｉｓｆｉａｂｉｌｉｔｙ）ベースのアプローチなどの他の検証アプローチを備えるよう完全モジュール的かつ容易に拡張されるものであってもよい。
【発明の効果】
【０００６】
本発明によると、回路検証に関する不都合、問題点あるいはその両方を軽減または解消する回路検証方法、回路検証論理及び回路検証システムが提供される。
【０００７】
本発明のある実施例は、上記技術的効果のすべてあるいは一部を提供するか、あるいはそれらの何れをも提供しないものであるかもしれない。ある実施例は、ここでの図面、説明及び請求項から当業者には自明であるかもしれない他の技術的効果の１以上を提供するものであるかもしれない。
【発明を実施するための最良の形態】
【０００８】
図１は、複数のエンジンを利用した回路検証のための一例となるシステム１０を示す。システム１０は、後述されるような、検証のための回路１２、回路１２を検証するための検証モジュール１４及び検証データ１６を有する。１以上のリンクにより、システム１０の構成要素は互いに接続されている。一例としてかつ限定することなく、リンクには、適切な場合には、１以上の回路基板上の１以上の配線、１以上の内部または外部バス、１以上のローカルエリアネットワーク（ＬＡＮ）、１以上のメトロポリタンエリアネットワーク（ＭＡＮ）、１以上のワイドエリアネットワーク（ＷＡＮ）、１以上のインターネット部分、あるいは上記リンクの２以上の組み合わせがあげられるかもしれない。
【０００９】
回路１２は、例えば、当該ハードウェアに対応する１以上の仕様に従ってハードウェアが適切に動作するか判断するためテストを行うためのハードウェア、論理または他のハードウェア表現を有する。一例としてかつ限定することなく、回路１２は、特定の機能を提供するよう互いに構成及び接続されたゲート、カウンタ、インバータ、バッファ及び他の回路コンポーネントなどの回路コンポーネントを有するものであってもよい。他の例として、回路１２は、論理やこのようなコンポーネントの他の表現を含むものであってもよい。回路１２は、数百万の回路コンポーネントを有するものであってもよい。ある機能を提供するため、回路１２は、１以上のプロパティを含む必要があるかもしれない。回路１２は、数百万のそのようなプロパティを含む必要があるかもしれない。ある実施例では、１以上の論理表現により、回路１２の１つのプロパティが記述されているかもしれない。回路１２の「プロパティ（ｐｒｏｐｅｒｔｙ）」とは、回路１２の論理的に表現可能な状態、特性、振舞いまたは動作、あるいは回路１２の他のプロパティを含むものであるかもしれない。
【００１０】
検証モジュール１４は、後述のような、１以上のリンクを介し回路１２にアクセスし、回路１２を検証するためのハードウェア、ソフトウェア、埋め込み論理コンポーネントあるいは上記２以上のコンポーネントの組み合わせを含む。ある実施例では、検証回路１２は、回路１２が１以上のプロパティを有するか判断するためのテスト論理１２を含む。一例としてかつ限定することなく、論理１２が１以上のプロパティを含むか判断するためのテスト回路１２は、後述のような、回路１２における状態の特定を含むものであってもよい。検証モジュール１４は、トレースモジュール１８を含む。トレースモジュール１８は、後述のような、トレースベースアルゴリズムを実行するためのハードウェア、ソフトウェア、埋め込み論理コンポーネントあるいは２以上の上記コンポーネントの組み合わせを含む。検証データ１６は、回路１２のタイプを特定するデータと、ある実施例では、検証モジュール１４が回路１２を検証するのに利用する他のデータを含む。ある実施例では、１以上のコンピュータシステムは、検証モジュール１４と検証データ１６へのユーザアクセスを提供する。一例としてかつ限定することなく、１以上のコンピュータシステムは、検証モジュール１４と検証データ１６を有し、ユーザは、検証モジュール１４及び検証データ１６への入力を与え、それらからの出力を受け取るため、１以上のコンピュータシステムにアクセスするようにしてもよい。
【００１１】
ハードウェアの形式検証の通常のアプローチは、設計の不変量プロパティをチェックすることである。不変量の非有界モデルチェッキングは、通常は到達可能性分析を行うことにより実行される。このアプローチは、初期状態から到達可能なすべての状態を検出し、不変量がこれら到達可能な状態において充足されるかチェックする。上記アプローチは、大きな状態集合を表す状態の急増という問題を引き起こす。到達可能性分析は、典型的には、既約順序付き二分決定グラフ（Ｒｅｄｕｃｅｄ  ＯＢＤＤ）を用いて行われる。ブール関数のよりコンパクトな表現である分割ＯＢＤＤ（Ｐａｒｔｉｔｉｏｎｅｄ  ＯＢＤＤ）により、到達可能性分析のさらなる向上が導かれる。
【００１２】
ＢＤＤに基づく到達可能性方法は、性能の一貫性の欠如という問題があり、これにより、与えられた問題に対してどの方法が採用されるべきか予想することが困難になる。ある実施例は、到達可能性分析を行う４つの方法、すなわち、状態集合表現に対する分割または非分割ＢＤＤを用いた順方向または逆方向到達可能性、を分析する。しばしば、ある方法では到達可能性を容易に計算できるが、その他の方法では計算が極めて困難であるケースがある。ある実施例は、上記方法の少数の短いトレースを走査することにより、より効果的な方法を決定するための自動的方策を提供する。これらのトレースは、ＢＤＤサイズでの所定のカットオフに到達するまで、初期計算を観察することにより、様々な方法の性能の短い初期サンプリングを提供する。このアプローチは、到達可能性分析と状態空間分割を実行する効果に対して、最善の方向を決定する。各方法は、自らの適用可能領域を有する。ある実施例は、各方法の長所から恩恵を受けるものである。独立に走査した複数のトレースの終わりで、ある実施例は、それらすべての計算が共有されることを可能にし、各手法の性能を大きく向上させるかもしれない。
【００１３】
上記直感的観察はまた、経験的に妥当とされる。当該手法は、他のアプローチに対して検証時間の劇的な効果を有する極めてロウバストな方法をもたらす。ＶＩＳ−Ｖｅｒｉｌｏｇベンチマークのすべての不変量チェッキングプロパティが効率的かつ自動的に終了される。このアプローチはモジュール的なものであり、他のＢＤＤ/ＳＡＴに基づく方法がトレース中心分析の一部として、そして究極的には本発明のフレームワークの一部として容易に組み込むことができる。本方法が有する固有の安定性と、ＢＤＤに基づく方法の周知の厄介なものであるパラメータ感度からの大なり小なりそれの自由度により、このような統合が切に必要とされていたということが信じられている。
【００１４】
ＢＤＤベースファルシフィケーション（ｆａｌｓｉｆｉｃａｔｉｏｎ）では、大きな不変量のチェッキング問題は、しばしば近似、分割、誘導探索及び混合順方向及び逆方向到達可能性を利用して解決される。記号逆方向到達可能性に対する重複投射を用いた近似法が提案されてきた。この方法の効果は、それが大変高速であるということだが、それは正確な解を与えることはできない。ヒントを利用した誘導された探索方法がまた提案されてきた。この方法は、それの効率性がユーザからの適切なヒントを要するため、人手による介入を必要とする。順方向及び逆方向近似及び厳密な探索を混合した複数の方法が誘導探索に提案されてきた。このような方法の少なくとも１つは、回路１２の状態空間の分割を利用し、目標となる状態集合からの各自の推定距離に基づき分割に優先度を付与する。当該方法は、近似順方向到達可能性を用いて、不変量チェッキングに対する厳密逆方向到達可能性を向上させる。しかしながら、この方法は、厳密順方向到達可能性が効果的である場合には効果的ではない。厳密逆方向到達可能性が極めてコストがかかる場合、このようなアプローチは全く非効率なものとなるであろう。
【００１５】
Ｂを集合｛Ｏ，Ｉ｝を表すとする。
【００１６】
（外１）
2005158073.tif 000003
を非決定性有限状態マシーンとする。ただし、
（外２）
2005158073.tif 000004
は状態空間であり、
（外３）
2005158073.tif 000005
は入力空間であり、
（外４）
2005158073.tif 000006
は状態遷移関数であり、
（外５）
2005158073.tif 000007
は初期状態の集合であり、
（外６）
2005158073.tif 000008
は出力関数である。この有限状態マシーン（ＦＳＭ）の状態数、入力数及び出力数はそれぞれ、ｎ，ｍ及びｋである。遷移関係
（外７）
2005158073.tif 000009
は、
（外８）
2005158073.tif 000010
からＢへの関数として定義される。ただし、
（外９）
2005158073.tif 000011
【００１７】
【数１】
2005158073.tif 000012
である。この遷移関係はしばしば、
【００１８】
【数２】
2005158073.tif 000013
により表される。ただし、
（外１０）
2005158073.tif 000014
は第ｉ状態に対する関数である。所与の状態
（外１１）
2005158073.tif 000015
から到達可能な次の状態の集合
（外１２）
2005158073.tif 000016
は、
（外１３）
2005158073.tif 000017
として計算される。このステップは、順方向画像計算（Ｆｏｒｗａｒｄ  Ｉｍａｇｅ  Ｃｏｍｐｕｔａｔｉｏｎ）として知られる。逆方向画像計算（Ｂａｃｋｗａｒｄ  Ｉｍａｇｅ  Ｃｏｍｐｕｔａｔｉｏｎ）は、次の状態が所与の状態集合
（外１４）
2005158073.tif 000018
すなわち、
（外１５）
2005158073.tif 000019
に属するすべての状態
（外１６）
2005158073.tif 000020
の計算として参照される。ＢＤＤに基づく検証では、遷移関係
（外１７）
2005158073.tif 000021
と状態関数
（外１８）
2005158073.tif 000022
がＢＤＤにより表される。画像計算は、しばしば検証における大きなボトルネックとなる。しばしば、遷移関係は画像計算には大きすぎるものとなってしまう。代わりに、遷移関係は、分割された遷移関係、すなわち、論理積が遷移関係に等しいＢＤＤの集合として表される。これらの論理積は、画像計算まで遅延される。早期定量化（ｅａｒｌｙ  ｑｕａｎｔｉｆｉｃａｔｉｏｎ）と呼ばれる中間的ＢＤＤを低減させる手法が、画像計算において適用される。
【００１９】
順方向到達可能性は、一定の点に到達するまで、初期状態に順方向画像計算を繰り返し適用することにより行われる。与えられた不変量プロパティ
（外１９）
2005158073.tif 000023
が、到達可能性分析においてチェックされる。トータルの到達可能状態が
（外２０）
2005158073.tif 000024
である場合、不変量は通過し、そうでない場合には通過しない。逆方向到達可能性は、
集合
（外２１）
2005158073.tif 000025
からの逆方向画像計算を繰り返し適用することにより行われる。トータルの逆方向到達可能な状態の集合が初期状態を含まない場合、不変量は通過し、そうでない場合には通過しない。到達可能性分析において、到達可能状態集合を表すＢＤＤは、とても大きなものとなるため、画像計算を実行することが不可能である。ＰＯＢＤＤに基づく順方向到達可能性は、論理和状態空間分割に対してＰＯＢＤＤを利用することによりこの問題を解決する。類似のアプローチが、上記遷移関係の論理積の分割に加えて、ＰＯＢＤＤに基づく逆方向到達可能性を実行するのに採用することができる。ここでの「分割（ｐａｒｔｉｔｉｏｎｉｎｇ）」という用語は、適切な場合には、このような状態空間の分割を含むものとされる。
【００２０】
到達可能性は、大多数の実践的ケースに対して困難な問題である。「ケース（ｃａｓｅ）」という用語は、適切な場合には、あるタイプの１以上の回路１２を含むものであってもよい。任意の到達可能性アルゴリズムが与えられると、到達可能性アルゴリズムが適さない場合が存在しうる。従って、すべての状態空間探索方法は、多くの場合において失敗してしまう。異なる到達可能性方法に対して効果性を有する領域は、しばしば論理和である。一例としてかつ限定することなく、順方向、逆方向及び分割状態空間探索の以下の特性を考える。
・順方向探索：順方向探索は、初期状態の集合から状態空間を探索する。それは不変量プロパティを利用して、探索された新たな状態がこのプロパティを満たすかチェックする。通常、順方向探索は、到達可能な状態が構造化された表現を有する場合により効果的であるようである。順方向探索は、簡単または複雑なプロパティによる恩恵は受けない。それは、通過するプロパティが存在する場合、トータルの到達可能空間を検出するであろう。
・逆方向探索：逆方向探索は、プロパティを満たさない状態空間の一部から探索を開始するため、当該プロパティにより依存したものとなる。このため、証明に必要とされる状態空間の関連部分が探索される。他方、これら状態の多くは、初期状態から到達可能ではない。しばしば起こりうるケースではあるが、システムが多すぎる到達不可能な状態を有し、それをＢＤＤにより表すことが極めて困難な場合、逆方向到達可能性は効果的でない。
・分割探索：分割順方向及び逆方向到達可能性は、それが回路の適切な分割を検出すると、状態空間のより深い状態とその多くの状態を迅速に探索することが可能である。回路に適切な分割がない場合、分割到達可能性は、分割に伴うオーバヘッドにより対応するモノリシック（ｍｏｎｏｌｉｔｈｉｃ）な到達可能性より悪いものとなるであろう。
【００２１】
ここで、到達可能性方法Ｍを考える。Ｍを用いた不変量チェッキングは、（ａ）プロパティ通過あるいは非通過、（ｂ）到達可能性が浅いか深いか、及び（ｃ）伴う計算が容易か困難か、の３つの軸を用いて分類されてもよい。容易なケースは、問題を提起しない。ある実施例は、残りのケースである困難なケースに対する向上を提供する。到達可能性問題は、それがかなり大きなグラフやかなり多くのステップ数を必要とするとき、典型的には困難となる。しかしながら、上述のように、異なるアプローチが補完的な性質を有するかもしれない。ある問題は、順方向到達可能性ではグラフの爆発や深い到達可能性計算を引き起こすかもしれないが、他方逆方向到達可能性では、この問題は一定の点に達するまで、かなり小さなグラフまたはかなり少ない画像計算しか要さないかもしれない。このような方法Ｍでの極めて困難な到達可能性問題を他の到達可能性問題でははるかに容易なものに変える可能性により、ある方法が継続的にかなりコストがかかるとわかったとき、当該方法に固執することは非効率であるかもしれない。
【００２２】
より詳細には、方法Ｍが与えられたとき、ある到達可能性インスタンスにおいて生成される深さと爆発がモニタされる場合、Ｍの実行が潜在的な困難さを示していると判断されると、他の直交到達可能性方法への切り替えが考慮されるべきである。補完的な方法を利用することにより、ＢＤＤの爆発を有する到達可能性インスタンスは、小さなＢＤＤを要する他のインスタンスにしばしば変換されるかもしれない。同様に、深いケースは、到達可能性の浅いインスタンスに変換されてもよい。これにより、ＢＤＤの爆発が生じたとしても、より少ないＢＤＤの計算により相対的に扱いやすいものに保つことができるかもしれない。深いケース（非通過プロパティ）と通過ケースの何れも伝統的な充足可能性（ＳＡＴ）有界モデルチェッキング（ＢＭＣ）に対する問題であるため、ある実施例は式の非有界モデルチェッキングを向上させるための手段を利用する。従って、ある方法Ｍの基本的到達可能性計算の時間またはスペースの向上は、様々な非有界モデルチェッキング問題の解を改善することができるが、魅力的な選択肢は、使用されている方法を動的かつ適切に変えることが可能であるというものである。ある実施例は、古典的モノリシック順方向到達可能性、逆方向モニリシック到達可能性、分割順方向到達可能性及び分割逆方向到達可能性の４つのアプローチを考慮する。このとき、ある実施例は、トレース中心のヒューリスティックを利用して、後述のように、どの方法が効果的であるかを予測する。
【００２３】
第１の問いは、多数のものの中でどの方法が選択されるべきであるかということであり、複数の方法が利用される場合には、どの時点でそれらが互いに切り替えられるべきかというものである。第２の問いは、停止された方法に対してすでに実行された計算にどう対処するかということである。このような計算が利用されることがなければ、動的な切り替えによるアプローチはしばしばかなりコストがかかるものとなるかもしれない。第１の問いを解決するため、ある実施例は、所定のカットオフ閾値を超えるまで各方法を実行し、その後所定の基準に従って優位な方法を自動的に選択することに基づくシンプルなアプローチを提供する。第２の問いを解決するため、重複した冗長な計算を浪費に関して、ある実施例は、停止された方法により実行された計算から、最終的に選ばれた到達可能性方法の性能を向上させる。
【００２４】
ある実施例では、トレースベースアルゴリズムが効果的な方法を予測する。アルゴリズムに対するトレースとは、当該アルゴリズムを用いた短い初期計算である。トレースベースアルゴリズムは、順方向及び逆方向記号モノリシック（非分割）到達可能性により逆方向及び順方向到達可能性のそれぞれが従う１つのトレースを実行する。ある実施例では、逆方向到達可能性と分割はバグの検出により適している傾向があるため、この順序が用いられる。所定のサイズのカットオフを超えるまで、トレースは実行される。ある実施例では、このカットオフは、記号演算の効率的なパフォーマンスを可能にするのに十分なだけの小ささであり、状態遷移関係の表現サイズの一定の倍数に設定される。経験的には、遷移関係のサイズの４〜６倍の範囲が、妥当な深さであるが、コスト高でないトレースを導く傾向がある。ある実施例では、カットオフは、時間でなくサイズに基づく。ほとんど爆発がない計算の場合には、計算を完了させるのに１つのトレースで十分であるかもしれない。ある実施例では、何れかのトレースが不変量の通過を決定することができる場合、当該方法は即座に終了される。同様に、順方向の状態集合と逆方向トレースが交差する場合、与えられた不変量はパスされないことが示された。
【００２５】
トレース自らが計算を終了しない場合、当該トレースを利用して、残りの計算に最も効果的なアプローチを予測する。まず、記号順方向及び逆方向到達可能性のトレースから、適切な方向が決定される。直感的には、ＢＤＤノードの閾値内で完了された画像数が、到達可能性計算がどれくらい効果的に進行しているかの尺度を与える。従って、ある実施例は、完了された画像数を最も効果的な方法を決定するための尺度として利用する。これら２つの方向で計算された画像数の間の差が、例えば、プラスマイナス１などの小さいものである場合、アルゴリズムは好ましい方法を効果的に識別することができない。このときある実施例は、例えば、順方向到達可能性などのデフォルトの方法を使用するか、あるいはより大きな閾値を有するトレースを再び実行するという選択肢を有する。少数の試行の後に方向を決定することができない場合、順方向がデフォルトとして選ばれうる。
【００２６】
方向の選択後、トレースベースアルゴリズムは、状態集合が単一のＢＤＤとして表されるモノリシックアプローチより分割到達可能性がより効果的であるか予測しようとする。これは、選択された方向で両方のアプローチを用いて実行されるトレースにより到達される状態数を考慮することにより行われてもよい。何れかの方法により探索された到達可能な状態の合計が、他方の方法のものよりかなり良好な場合、優位な方法が検出されることになる。この合計数が何れのアプローチに対しても同程度である場合、優劣を判定するための意味ある尺度は、カバーされる状態数として定義されるカバー率対対応する時間であるかもしれない。このようにして、最も効果的な方法である確率が高い方法を抽出するのにトレースが利用される。
【００２７】
様々なトレースにより実行される繰り返しの重複計算が無駄にされるかもしれない。これを回避するため、効果的な方法を決定した後、トレースベースアルゴリズムは、すべてのトレースにより到達される状態を追加することにより、初期状態と不変量を拡大する。順方向では、到達可能性分析は、両方の順方向トレースを用いて到達された状態の和集合から開始される。同様に、不変量の否定を満たす状態の集合であるエラー集合は、２つの逆方向トレースにより到達される状態集合の和集合により置き換えられる。計算方向が逆方向である場合、エラー集合は開始状態であり、拡大された初期集合は、トレースにより実行される計算の再利用を可能にするターゲットとなる。
【００２８】
図２は、状態空間分割ある場合とない場合の順方向及び逆方向のトレースによる一例となる状態の探索を示す。これら同心円は、順方向と逆方向のモノリシック（非分割）トレースを表している。これら楕円は、分割順方向及び逆方向到達可能性トレースを表している。不変量プロパティを無効にするため、初期状態から誤った状態が到達可能である。ときどき、図２に示されるように、順方向と逆方向のトレースが互いに交差する。この場合、トレースベースアルゴリズムは停止し、失敗した結果を通知する。そうでない場合、トレースベースアルゴリズムは、他の方向の到達可能集合との交差が得られるまで、選択された方法を実行する。このため、不変量拡大は、失敗するケースに対して有用である。
【００２９】
フロンティア拡大（ｆｒｏｎｔｉｅｒ  ａｕｇｍｅｎｔａｔｉｏｎ）は、図３Ａ〜３Ｃに示される通過プロパティに対する当該方法の性能の向上を促すかもしれない。図３Ａは、トレース後の初期集合とエラー集合の拡大を示す。図３Ｂは、到達可能性の収束を示す。図３Ｃは、拡大なしの到達可能性を示す。図３Ａでは、円はＢＦＳトレースを表し、楕円は分割到達可能性のトレースである。図３Ｂ及び３Ｃは、同一の到達可能な状態の集合Ｒを有する。この同一の状態集合に対して、図３Ｂは図３Ｃより速く収束する。通過した不変量に対して、すべての到達可能な状態は、違反が検出されないことを確認するため探索される必要がある。これは、例えば、図３Ｃに示されるような幅優先探索（ＢＦＳ）により行うことができる。初期状態の集合Ｉが異なる方法により到達した状態により拡大される場合、拡大された初期状態の集合Ｉ’は、順方向到達可能性を実行することにより到達される状態より深い状態を有する可能性がある。直感的には、深さ優先探索（ＤＦＳ）方法がかなりの数の新たな状態を追加する場合、到達可能性がこの集合Ｉ’からＢＦＳを用いて収束するのに必要なステップ数は、図３Ｂに示されるように、より少なくなるかもしれないし、あるいは到達可能性自体がより効率的になるかもしれない。
【００３０】
ある実施例では、各エンジンは、パラレルな計算環境において、同時に、すなわち、パラレルに実行されてもよい。エンジンの１つが終了すると、残りの実行が終了されるようにしてもよい。パラレル環境では、フロンティア拡大手法は、ある方法の中間計算の部分的結果が他の方法を容易にすることを可能にするかもしれない。一例としてかつ限定することなく、モノリシックなＯＢＤＤフロンティアを拡大するため、ＰＯＢＤＤフロンティアが追加されてもよい。十分なプロセッサが利用可能である場合、各ＰＯＢＤＤフロンティア（各分割からの）を利用して、モノリシックフロンティアが拡大されてもよい。これら拡大されたフロンティアの各々は、利用可能なプロセッサを用いてパラレルに実行されてもよい。
【００３１】
ある実施例では、順方向及び逆方向の実行のフロンティアがこのように利用され、これにより、フロンティアが計算されるごとに、それは反対方向の最後に計算されたフロンティアと交差する。これにより、エラー位置の決定に関する時間要求が低減されるかもしれない。別のプロセッサは、フリーの状態に維持されてもよいし、あるいは既存の環境においてスケジューリングされてもよい。ＢＭＣの実行がすでにＫ回終了し、かつＢＤＤの実行がＫ’の深さに達している場合（ただし、ＫはＫ’よりかなり大きい）、ＢＤＤの実行は終了され、ＢＭＣに対してプロセッサが解放されてもよい。
【００３２】
１以上のＰＯＢＤＤフロンティアは、１以上の他のＰＯＢＤＤフロンティアが固定されている間、かなり深くまで進行するようにしてもよい。この場合、深い分割のＰＯＢＤＤフロンティアを利用して、パラレルにＢＭＣの実行が開始されてもよい。一例としてかつ限定することなく、分割の各フロンティアから、ＳＡＴ−ＢＭＣの実行が開始されてもよい。このように、多数の独立なＢＭＣの実行が開始されてもよい。フロンティアのすべての状態をとる代わりに、状態の部分集合が初期状態として利用されてもよく、これにより、ＳＡＴ−ＢＭＣへの問題を出さない傾向がある状態のみを初期状態としてとるフレキシビリティをユーザに与えるかもしれない。
【００３３】
ある実施例は、形式的検証において複数のエンジンを利用するための効率的手法を提供する。ＦＶはしばしば困難である。ワーストケースのシナリオでは（Ｐ−スペース完全またはＮＰ−完全）、ＦＶ問題は手に負えないものであるかもしれない。ＦＶ問題を処理する従来技術として、決定性自動テストパターン生成（ＡＴＰＧ）、非決定性ＡＴＰＧ、順方向到達可能性（ＢＤＤまたはＰＯＢＤＤを用いた）、プリイメージ技術（ＢＤＤまたはＰＯＢＤＤを用いた）、ＳＡＴ−ＢＭＣ技術、帰納ベースＢＭＣ技術及び他の技術などが含まれる。上記技術の１以上を用いたエンジンは、典型的には直交するものであり、このため、自らの適用可能領域を有する。しばしば、これらエンジンのそれぞれが利用される必要がある。しかしながら、あるケースにおいてどの技術が適用されるべきかはっきりしない。ある実施例は、このような決定を自動的に行うようにしてもよい。
【００３４】
従来のエンジン手法によると、各自が回路サイズ（大、中、小）と状態集合の深さ（深い、浅い）により規定される６つのケースが存在する。状態空間の深さは、順方向到達可能性深さを含む。第１のケースでは（大きい回路かつ深い状態空間）、ＰＯＢＤＤ−ＢＭＣ技術が典型的には利用されるが、略式的な解しか提供しない。あるいは、ＡＴＰＧに基づくプリイメージまたは陽動された略式的な検証の利用が可能である。抽象化のため、ＲＴＬソルバ（ｓｏｌｖｅｒ）の利用が可能である。しばしば、ＢＤＤはかなり大きな回路の処理ができない。第２のケースでは（大きな回路かつ浅い状態空間）、ＡＴＰＧベースのファルシファイア（ｆａｌｓｉｆｉｅｒ）が利用される。フォールト（ｆａｕｌｔ）が存在しない場合、帰納ベースＢＭＣが利用される。ＡＴＰＧベースファルシファイアと帰納ベースＢＭＣの使用順序は、逆転可能である。
【００３５】
第３のケースでは（小さい回路かつ浅い状態空間）、ＡＴＰＧ及びＰＯＢＤＤ技術を用いた高速のファルシファイアが典型的には利用される。エラーが存在しない場合、ＢＤＤ、ＳＡＴ−ＢＭＣまたはＰＯＢＤＤ技術が利用される。第４のケースは（小さい回路かつ深い状態空間）、２つのサブケースを含む。第１のサブケースは、困難な関数を含む。これらの関数を処理するのにＰＯＢＤＤが典型的には利用される。第２のサブケースは、より困難さの少ない関数を含む。これらの関数を処理するのにＰＯＢＤＤ（及びときにはＯＢＤＤ）が典型的には利用される。第５のケースでは（中規模の回路及び浅い状態空間）、しばしばＢＭＣ技術が好ましい。２つのサブケースが存在する。第１のサブケースは、困難な関数を含む。これらの関数はしばしば、手に負えないと証明されているが、ＳＡＴ−ＢＭＣ技術は一般にこれらの関数に対して機能する。第２のサブケースは、より困難さの少ない関数を含む。これらの関数の処理には、ＢＭＣ技術がしばしば好ましい。第６のケースは（中規模の回路かつ深い状態空間）、２つのサブケースを含む。第１のサブケースは、困難な関数を含む。これら関数はしばしば手に負えないものであり、典型的には、深いＢＭＣ技術が唯一の選択肢である。第２のサブケースは、より困難さの少ない関数を含む。典型的には、ＰＯＢＤＤ技術が、これら関数に関してスケーラブルな唯一の技術である。
【００３６】
従来のＦＶ技術は、典型的には、順方向到達可能性によるものである。さらに、従来の技術は、しばしば非現実的な主張が真であることを証明しようとする。ある実施例は、より効果的な方法を提供する。ある実施例では、到達不可能な状態空間が小さいものであるような場合、ＡＴＰＧ技術を利用して、エラーを検出するようにしてもよい。到達不可能な状態空間が実際に小さいものである場合、プリイメージベースファルシフィケーション技術が利用されてもよい。大きな回路に対しては、ＡＴＰＧベース反証技術は単独で利用されてもよい。ＡＴＰＧベースファルシフィケーション技術がエラーを検出することができない場合、１以上の従来技術が利用されてもよい。ＡＴＰＧに基づく方法は、テスト生成処理中に実質的な誘導を生成する。これらの方法の一部を利用して、フォールトの困難さが予測されてもよい。ある実施例では、検証のため、ある到達不可能な状態空間に固有の誘導をより正確なものにするためのリサーチがこの点において行われてもよい。理論的には、式Ｐ＝１がプロパティである場合、Ｐ＝０はＯＲゲートの出力をゼロに設定することを要する。論理的には、ＯＲゲートが複数の入力を有する場合、あるいはＰのＦａｎ−ｉｎ  Ｃｏｎｅにおいて大部分のケースが実行困難である場合、これは困難であるとわかるかもしれない。これらＡＴＰＧに基づく方法の一部は、シーケンシャルな学習を利用して実行されてもよい。ある実施例は、ＦＶに関する時間要求を低減させるかもしれない。ある実施例では、従来技術に対して１００〜１０００倍のゲインが得られるかもしれない。ある実施例は、スケーラビリティと安定性の両方の問題に対し解を与えるかもしれない。
【００３７】
図４は、複数のエンジンを利用した回路検証のための一例となる方法を示す。本方法は、ステップ１００からスタートし、検証のため、検証モジュール１４は回路１２にアクセスする。ステップ１０２において、検証モジュール１４は、様々な到達可能性技術を利用して回路１２上のトレースを走査する。ステップ１０４において、検証モジュール１４は、回路１２に対する効果的な到達可能性技術を予測するため、各トレースの結果を互いに比較する。ステップ１０６において、検証モジュールは、ステップ１０２において実行されたすべてのトレースにおいて到達した状態を利用して、予測した効果的な到達可能性技術に対し初期状態を拡大する。ステップ１０８において、検証モジュールは、本方法が終了する時点において、予測された効果的な到達可能性技術と拡大された初期状態を利用して回路の検証を実行する。
【００３８】
本開示は特定の実施例及び一般的に関連する方法に関して説明されたが、上記実施例及び方法の変更及び置換は当業者には明らかであろう。このため、上記実施例に関する説明は、本開示を画定または限定するものではない。本開示の趣旨及び範囲から逸脱することなく、他の変更、置き換え及び変形もまた可能である。
【００３９】
（付記１）  複数のエンジンを利用した回路検証方法であって、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査するステップと、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成するステップと、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップと、
から構成されることを特徴とする方法。
【００４０】
（付記２）  付記１記載の回路検証方法であって、
前記複数の到達可能性アルゴリズムは、逆方向分割到達可能性アルゴリズム、順方向分割到達可能性アルゴリズム、順方向記号モノリシック到達可能性アルゴリズム及び逆方向記号モノリシック到達可能性アルゴリズムから構成されることを特徴とする方法。
【００４１】
（付記３）  付記２記載の回路検証方法であって、
前記複数の到達可能性アルゴリズムは、さらに、パラレル順方向到達可能性アルゴリズム及びパラレル逆方向到達可能性アルゴリズムを有することを特徴とする方法。
【００４２】
（付記４）  付記２記載の回路検証方法であって、
前記効果的な到達可能性アルゴリズムを選択するステップは、前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較に従って、前記効果的な到達可能性アルゴリズムの効果的な方向を選択することから構成されることを特徴とする方法。
【００４３】
（付記５）  付記４記載の回路検証方法であって、
前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較が効果的な方向を明確には特定しない場合、前記効果的な到達可能性アルゴリズムを選択するステップは、前記効果的な到達可能性アルゴリズムに対するデフォルト方向を選択することから構成されることを特徴とする方法。
【００４４】
（付記６）  付記５記載の回路検証方法であって、
前記デフォルト方向は、順方向であることを特徴とする方法。
【００４５】
（付記７）  付記４記載の回路検証方法であって、さらに、
前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較が効果的な方向を明確には特定しない場合、前記複数のトレースが該複数のトレースを終了するための従来の所定の遷移関係サイズカットオフより大きな所定の遷移関係サイズカットオフに到達するまで、前記回路上の前記複数のトレースを再走査するステップを、
有することを特徴とする方法。
【００４６】
（付記８）  付記４記載の回路検証方法であって、
前記効果的な到達可能性アルゴリズムを選択するステップは、さらに、前記複数のトレースのそれぞれにおいて前記選択された効果的な方向により到達した状態数に従って、前記効果的な到達可能性アルゴリズムに対する分割あるいはモノリシックアプローチを選択することを有することを特徴とする方法。
【００４７】
（付記９）  付記１記載の回路検証方法であって、さらに、
前記複数のトレースが所定の遷移関係サイズカットオフに到達すると、前記複数のトレースを終了させるステップを、
有することを特徴とする方法。
【００４８】
（付記１０）  付記１記載の回路検証方法であって、さらに、
前記複数のトレースにおいて到達したすべてのトレースを利用して、前記選択された効果的な到達可能性アルゴリズムに対する前記初期状態の集合を生成するステップを、
有することを特徴とする方法。
【００４９】
（付記１１）  複数のエンジンを利用した回路検証論理であって、該論理はコンピュータ実行可能な媒体において具現化され、実行時に、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査するステップと、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択するステップと、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成するステップと、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行するステップとを、
処理可能であることを特徴とする論理。
【００５０】
（付記１２）  付記１１記載の回路検証論理であって、
前記複数の到達可能性アルゴリズムは、逆方向分割到達可能性アルゴリズム、順方向分割到達可能性アルゴリズム、順方向記号モノリシック到達可能性アルゴリズム及び逆方向記号モノリシック到達可能性アルゴリズムから構成されることを特徴とする論理。
【００５１】
（付記１３）  付記１２記載の回路検証論理であって、
前記複数の到達可能性アルゴリズムは、さらに、パラレル順方向到達可能性アルゴリズム及びパラレル逆方向到達可能性アルゴリズムを有することを特徴とする論理。
【００５２】
（付記１４）  付記１２記載の回路検証論理であって、
前記効果的な到達可能性アルゴリズムを選択するステップは、前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較に従って、前記効果的な到達可能性アルゴリズムの効果的な方向を選択することから構成されることを特徴とする論理。
【００５３】
（付記１５）  付記１４記載の回路検証論理であって、
前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較が効果的な方向を明確には特定しない場合、前記効果的な到達可能性アルゴリズムを選択するステップは、前記効果的な到達可能性アルゴリズムに対するデフォルト方向を選択することから構成されることを特徴とする論理。
【００５４】
（付記１６）  付記１５記載の回路検証論理であって、
前記デフォルト方向は、順方向であることを特徴とする論理。
【００５５】
（付記１７）  付記１４記載の回路検証論理であって、さらに、
前記複数のトレースのそれぞれにおいて終了した画像計算数の互いの比較が効果的な方向を明確には特定しない場合、前記複数のトレースが該複数のトレースを終了するための従来の所定の遷移関係サイズカットオフより大きな所定の遷移関係サイズカットオフに到達するまで、前記回路上の前記複数のトレースを再走査するステップを、
処理可能であることを特徴とする論理。
【００５６】
（付記１８）  付記１４記載の回路検証論理であって、
前記効果的な到達可能性アルゴリズムを選択するステップは、さらに、前記複数のトレースのそれぞれにおいて前記選択された効果的な方向により到達した状態数に従って、前記効果的な到達可能性アルゴリズムに対する分割あるいはモノリシックアプローチを選択することを有することを特徴とする論理。
【００５７】
（付記１９）  付記１１記載の回路検証論理であって、さらに、
前記複数のトレースが所定の遷移関係サイズカットオフに到達すると、前記複数のトレースを終了させるステップを、
処理可能であることを特徴とする論理。
【００５８】
（付記２０）  付記１１記載の回路検証論理であって、さらに、
前記複数のトレースにおいて到達したすべてのトレースを利用して、前記選択された効果的な到達可能性アルゴリズムに対する前記初期状態の集合を生成するステップを、
処理可能であることを特徴とする論理。
【００５９】
（付記２１）  複数のエンジンを利用した回路検証システムであって、
複数の到達可能性アルゴリズムを利用して、回路上の複数のトレースを走査する手段と、
前記複数のトレースの間の結果の比較に従って、前記複数の到達可能性アルゴリズムから前記回路に対する効果的な到達可能性アルゴリズムを選択する手段と、
前記複数のトレースにおいて到達した状態を利用して、前記選択された効果的な到達可能性アルゴリズムに対する初期状態の集合を生成する手段と、
前記回路を検証するため、前記生成された初期状態の集合を利用して、前記選択された効果的な到達可能性アルゴリズムを実行する手段と、
から構成されることを特徴とするシステム。
【００６０】
（付記２２）  複数のエンジンを利用した回路検証方法であって、
回路のサイズを決定するステップと、
前記回路の深さ及び困難さを推定するため、自動テストパターン生成器（ＡＴＰＧ）を利用するステップと、
前記回路のサイズ、深さ及び困難さに従って、ＡＴＰＧベースファルシフィケイションエンジン、レジスタトランスファレベル（ＲＴＬ）エンジン、深さ有界モデルチェッキング（ＢＭＣ）エンジン、充足可能性ＢＭＣ（ＳＡＴ−ＢＭＣ）エンジン、帰納ＢＭＣエンジン、分割順序付二分決定図（ＰＯＢＤＤ）エンジン、順序付二分決定図（ＯＢＤＤ）エンジン及びプリイメージエンジンからなる複数の検証エンジンから１以上を選択するステップと、
少なくとも、前記選択された検証エンジンを利用して、前記回路の１以上のプロパティの検証を試みるステップと、
から構成されることを特徴とする方法。
【図面の簡単な説明】
【００６１】
【図１】複数のエンジンを利用した回路検証のための一例となるシステムを示す。
【図２】一例となる状態の探索を示す。
【図３】通過プロパティに関する性能を向上させるフロンティア拡大を示す。
【図４】複数のエンジンを利用した回路検証のための一例となる方法を示す。
【符号の説明】
【００６２】
１０  システム
１２  回路
１４  検証モジュール
１６  検証データ
１８  トレースモジュール
【図１】
2005158073.tif 000026
【図２】
2005158073.tif 000027
【図３】
2005158073.tif 000028
【図４】
2005158073.tif 000029
【外国語明細書】
2005158073.tif 000030
2005158073.tif 000031
2005158073.tif 000032
2005158073.tif 000033
2005158073.tif 000034
2005158073.tif 000035
2005158073.tif 000036
2005158073.tif 000037
2005158073.tif 000038
2005158073.tif 000039
2005158073.tif 000040
2005158073.tif 000041
2005158073.tif 000042
2005158073.tif 000043
2005158073.tif 000044
2005158073.tif 000045
2005158073.tif 000046
2005158073.tif 000047
2005158073.tif 000048
2005158073.tif 000049
2005158073.tif 000050
2005158073.tif 000051
2005158073.tif 000052
2005158073.tif 000053
2005158073.tif 000054