(57)【特許請求の範囲】
【請求項１】
検証問題の困難度を評価する方法であって、
コンピュータが、デザイン及び特性群を含む入力であって、前記特性群中の特性が前記デザインに関して検証される入力を、受信するステップと、
前記コンピュータが前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行するステップであって、前記デザインについて自動テストパターン生成プロセスを実行するプロセスを有するステップと、
前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立することにより、各特性についての特性検証メトリック値を確立するステップであって、前記特性検証メトリック値が前記デザインの各特性を検証する困難度を表すステップと、
を反復するステップと、
前記コンピュータが前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定するステップであって、前記デザイン検証メトリック値が前記デザインの前記特性群を検証する困難度を表すステップと、
を有することを特徴とする方法。
【請求項２】
前記デザインが、或る回路の回路設計を含み、
前記デザイン検証メトリック値が、回路検証メトリック値を有することを特徴とする請求項１記載の方法。
【請求項３】
デザイン検証メトリック値を判定する前記ステップが、
前記特性群中の各特性について重みを割り当てるステップと、
前記特性検証メトリック値の重み付け平均と、特性に割り当てられた重みに従って重み付けされた特性の特性検証メトリック値を計算するステップと、
重み付け平均から、デザイン検証メトリック値を生成するステップと、
を有することを特徴とする請求項１記載の方法。
【請求項４】
前記デザインにおける各特性について複数の検証プロセスを実行する前記ステップが、前記デザインについて限定モデル検査プロセスを実行するプロセスを有し、
特性検証メトリック値を確立する前記ステップが、
前記限定モデル検査プロセスの成長率を判定するステップと、
前記成長率がレート閾値より少ない場合に、前記デザインについて抽象化プロセスを実行するステップと、
を有することを特徴とする請求項１記載の方法。
【請求項５】
前記デザインにおける各特性について複数の検証プロセスを実行する前記ステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立する前記ステップが、前記残存する第３要素数が残存する要素閾値より多い場合に、高い困難度を確立することを特徴とする請求項１記載の方法。
【請求項６】
前記デザインにおける各特性について複数の検証プロセスを実行する前記ステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立する前記ステップが、
前記抽象性は抽象化された第１要素数とオリジナルの第２要素数との比率を有する前記デザインの抽象性を算出するステップと、
前記抽象性が抽象性閾値より大きい場合に、低い困難度を確立するステップと、
を有することを特徴とする請求項１記載の方法。
【請求項７】
検証問題の困難度を評価するためにコンピュータに、
デザイン及び特性群を含む入力であって、前記特性群中の特性が前記デザインに関して検証される入力を受信させるステップと、
前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行させるステップであって、前記デザインについて自動テストパターン生成プロセスを実行させるプロセスを有するステップと、
前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立させることにより、各特性についての特性検証メトリック値を確立させるステップであって、前記特性検証メトリック値が前記デザインの各特性を検証する困難度を表すステップと、
を反復させるステップと、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定させるステップであって、前記デザイン検証メトリック値が前記デザインの前記特性群を検証する困難度を表すステップと、
を実行させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項８】
検証問題の困難度を評価するシステムであって、
デザイン及び特性群を含む入力であって、前記特性群中の特性が前記デザインに関して検証される入力を受信する手段と、
前記特性群中の特性の各々について、前記デザインにおける各特性について複数の検証プロセスを実行し、前記検証プロセスに従って、各特性について特性検証メトリック値を確立することを反復する手段であって、前記複数の検証プロセスが前記デザインについて自動テストパターン生成プロセスを実行するプロセスを有し、前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立することにより、各特性についての特性検証メトリック値を確立し、前記特性検証メトリック値が前記デザインの各特性を検証する困難度を表す手段と、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定する手段であって、前記デザイン検証メトリック値が前記デザインの前記特性群を検証する困難度を表す手段と、
を有することを特徴とするシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は一般に集積回路設計の技術分野に関連し、特に形式検証問題(formal  verification  problem)の困難度を評価することに関連する。
【背景技術】
【０００２】
回路技術の進歩は集積回路に極めて多くのトランジスタの配置をもたらし、より複雑な回路設計を必要とする。しかしながら既存の回路設計評価法は、より複雑な回路設計に直面した場合に一般に非効率的である。従って回路設計を評価する既存の技法は状況によっては満足のゆくものでないかもしれない。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明の課題は、形式検証（フォーマルベリフィケーション）問題の困難度を評価する従来技術に付随する欠点及び問題点を軽減又は解消することである。
【課題を解決するための手段】
【０００４】
一形態によれば、検証問題の困難度の評価は、デザイン及び特性を含む入力を受信することを含み、その特性はそのデザインで検証されるものである。検証プロセスはそのデザインの各特性について実行される。特性検証メトリック値が検証プロセスに従って特性の各々について確立される。特性検証メトリック値はそのデザインの特性を検証する困難度を表す。デザイン検証メトリック値が特性検証メトリック値から決定され、デザイン検証メトリック値はそのデザインを検証する困難度を表す。
【発明を実施するための最良の形態】
【０００５】
本発明の実施例は１以上の技術的恩恵をもたらす。一形態による技術的恩恵は、回路を検証するための困難度(difficulty  level)が見積もられることである。回路の特性を検証するための困難度は、特性群中の各特性について判定される。回路を検証するための困難度は、特性の困難度から検証される。回路についての困難度を用いて、その回路を検証するのに要するリソース量を評価し、検証方法論を考案し、検証エンジンパラメータを調整し、検証用に回路設計を修正し、或いは適切な他の如何なることを実行してもよい。
【０００６】
本発明の実施形態は上記の技術的恩恵の全部又は一部を含んでもよいし、全く含まなくてもよい。他の１以上の技術的恩恵は、本願に含まれる図面、明細書及び特許請求の範囲から当業者に明らかになるであろう。
【０００７】
本発明並びにその特徴及び利点の理解の完全を更に期するため、添付図面に関連する以下の説明が参照される。
【実施例１】
【０００８】
本発明の実施例及びその利点は図１乃至図４を参照することで最良に理解され、図中同様な及び対応する部分については同様な番号が使用される。
【０００９】
図１は形式検証問題の困難度を評価するシステム１０の一例を示すブロック図である。本実施例によれば、システム１０は回路を検証する困難度を確立する。回路の特性を検証するための困難度は、一群の特性中の各特性について決定される。回路を検証する困難度は、その特性の困難度から確立される。
【００１０】
一般に、回路の仕様はその回路に意図される動作を記述し、回路の設計はその意図される動作を実行するように設計される算術的及び論理的処理を記述する。仕様及び設計は数学的モデルで表現されてもよい。数学的モデルは、その設計がその仕様に従って記述される意図される動作を実行するか否かを確認するために形式検証プロセスに従って比較されてもよい。しかしながら比較の実効は一般に困難である。更に場合によっては検証プロセスは決して完了しないかもしれない。
【００１１】
システム１０は形式検証問題の困難度を評価する。一実施例によれば、困難度は検証問題を実行するのに要するリソース量を反映してもよい。リソースは、例えば、計算時間、メモリ、又は計算時間及びメモリの双方を含んでもよい。一般に、より高い困難度はより多くのリソースを示し、より低い困難度はより少ないリソースを示す。困難度を評価することで、検証方法論が工夫されてもよいし、或いは完全な検証プロセスを実行する前に形式検証問題が修正されてもよい。
【００１２】
図示の例によれば、システム１０はクライアントシステム２０、データベース２２、サーバシステム２４を図１に示されるような結合関係で含む。一実施例によれば、クライアント２０は、形式検証問題の困難度を推定するためにユーザがサーバ２４と通信することを可能にする。
【００１３】
データベース２２はサーバシステム２４で使用されるデータを格納する。図示の例によれば、データベース２２は検証におけるモデル３０を格納する。モデル３０はシステム１０で分析されるモデルを表現する。モデル３０は検証及び特性３６における設計（デザイン）３４を含む。デザイン３４は回路設計のような検証される適切な如何なる設計内容を表現してもよい。回路設計は、20,000ラッチに及ぶ及び30,000ゲートに及ぶような適切内如何なるサイズのレジスタトランスファレベル(RTL:  register-transfer  level)回路を含んでよい。例えば回路を設計するプロセスに使用される超高速集積回路(VHSIC)ハードウエア記述言語(VHDL)又はベリログ(VERILOG)で、デザイン３４は表現されてもよい。
【００１４】
しかしながらデザイン３４は適切な如何なる設計を表現してもよい。一例として、デザイン３４は仕様レベルの又はシステムレベルの回路設計を表現してもよい。別の例として、デザイン３４は回路設計ではなくソフトウエア設計を表現してもよい。
【００１５】
特性３６は検証されるデザイン３４の特徴を表現する。一実施例によれば、概して特徴は指定された条件下での回路の動作を記述する。特性３６の具体例は、ビジュアルインタラクティングウィズシンセシス(VIS:  Visual  Interacting  with  Synthesis)ベンチマーク群のような、工業的又は学術的なベンチマークデザインに関連する特性を含んでよい。特性はシステムの時間的振る舞いを捕らえるように使用されてもよいし、或いは特性は時間によらないシステムの特徴を表現してもよい。
【００１６】
サーバシステム２４はアプリケーションを管理し、そのアプリケーションは形式検証問題の困難度を評価するのに使用されてもよい。図示の例によれば、サーバシステム２４は検証エンジン４０、困難性推定器４４及びデザイン修正器４８を含む。
【００１７】
検証エンジン４０は検証プロセスを実行するためのソフトウエアエンコードエンジンを表す。検証プロセスは、或るデザインの特性を検証するプロセスに関連し、フォーマルな及びインフォーマルな検証プロセスを含んでよい。検証プロセスの具体例は、例えば、自動テストパターン生成(ATPG)プロセス、充足性限定モデル検査(SAT:  satisfiability-based  bounded  model  checking)プロセス、二分決定図(BDD)に基づくシンボリックモデル検査プロセス、シミュレーションプロセス、他の適切な検証プロセス又はそれらの如何なる組み合わせを含んでもよい。
【００１８】
困難度推定器４４は検証問題の困難度を推定する。一実施例によれば、困難度推定器４４は検証メトリックを計算し、検証メトリックは検証問題の困難度を推定するのに使用される。困難度推定器４４は、困難度を推定する適切な如何なる技法に従って動作してもよい。方法例が図２を参照しながら説明される。
【００１９】
一実施例によれば、検証エンジン４０及び困難度推定器４４は、検証エンジン４０のための検証パラメータ又は検証方法論を確立するよう協同する。検証パラメータは、検証エンジンのパラメータに関連し、期間満了（タイムアウト）、労力、深さ(depth)、他のパラメータ又はそれらの適切な如何なる組み合わせを含んでもよい。
【００２０】
一実施例によれば、検証エンジン４０は、検証問題についてサンプルラン(sample  run)を行い、その結果を困難度推定器４４に通知する。困難度推定器４４はそのサンプルランから検証メトリックを算出する。検証メトリックは、困難度を減らすために検証パラメータがどのように変えられるかを示す。一例として、問題に対する困難度が高かったならば、検証エンジン４０のタイムアウト値が増やされてもよい。別の例として、検証パラメータは特定の一群の又は特定の一連の検証エンジン４０を選択するように変えられてもよく、その検証エンジンは、より多くのリソースを使用する検証エンジン４０を下回るより少ないリソースを利用する。
【００２１】
デザイン修正器４８は困難度推定器４４からの結果に応答してデザイン３４を修正するために使用される。デザイン３４はデザイン３４の困難度を減らすように修正されてよい。一実施例によれば、デザイン修正器４８はシステム１０からの結果に応じてユーザがデザイン３４を修正することを可能にする。別の実施例によれば、デザイン修正器４８はシステム１０からの結果に応答してデザイン３４を自動的に修正してもよい。修正は最終的なデザインに必ずしも必要とされない。一例として、修正は回路設計を検証するためにのみ行われ、実際の回路製品に対しては除去されてもよい。
【００２２】
一実施例によれば、検証メトリックは以下の手法で計算されてもよい。モデル３０は回路Ｒのデザイン３４と、検証される回路Ｒのｎ個の特性{P1,…,Pn}の群３６とを含む。回路Ｒの特性Piの特性検証メトリック値V(R,Pi)は、回路Rの特性Piを検証する困難度を表す。一例として、より高いメトリック値はより高い困難度を示し、より低いメトリック値はより低い困難度を示す。
【００２３】
本実施例によれば、或る特性について、合格の検証メトリック値及び不合格の検証メトリック値が計算される。一例として、合格の検証メトリック値Vpass(R,Pi)は特性Piが最終的には合格することを仮定し、不合格の検証メトリック値Vfail(R,Ri)は特性Piが最終的には不合格になることを仮定する。
【００２４】
デザイン３４のデザイン検証メトリック値は、デザイン３４についての一群の特性を検証する困難度を示す。一例として、回路Rの回路検証メトリック値V(R)は、回路Rについての一群の特性を検証する困難度を示すために計算される。回路検証メトリック値V(R)は、特性検証メトリック値V(R,Pi)の重み付け平均から計算されてもよい。
【００２５】
一実施例によれば、回路検証メトリック値V(R)は合格の検証メトリック値Vpass(R,Pi)から計算されてよい。なぜなら場合によっては不合格の検証メトリック値が推定困難だからである。一実施例によれば、回路検証メトリック値V(R)は次式（１）に従って計算されてもよい：
【００２６】
【数１】
0004806306.tif 000002
ここで、wiは特性Piの重み（ウエイト）を表す。合格の検証メトリック値は、不合格の検証メトリック値の過剰近似として使用されるかもしれない。
【００２７】
特性は適切な如何なる手法で重み付けされてもよい。一実施例によれば、より有力な特性又はより重要な特性には、より有力でない又はより重要でない特性のものより大きなウエイトが与えられる。一例として、より大きな円錐状影響圏(cone  of  influence)を有する特性には、より大きなウエイトが与えられる。
【００２８】
検証メトリック値は適切な如何なる手法で表現されてもよい。一例として、その値は或る数値で、或る範囲で又は或る分類で表現されてもよい。一実施例によれば、検証メトリック値はｍ個の異なるレベル群{L1,…,Lm}の分類で表現されてもよい。困難度の数ｍは所望の計算時間及び精度に依存して選択されてもよい。一群の困難度の具体例が図２を参照しながら詳細に説明される。
【００２９】
図２は一群の困難度を例示するテーブル６０である。図示の例によれば、この群（集合又はセット）は６つの異なるレベルL1,…L6を含む。それらのレベルは、些細な(trivial)、簡易な(easy)、並の(moderate)、困難な(hard)、非常に困難な(very  hard)、及び不確定の(undecided)レベルである。近似的な時間は、その困難度の問題について検証を実行するのに要すると思われる近似的な時間を表す。不確定の困難度は、困難度を決定できなかったことを示す。
【００３０】
本発明の範囲から逸脱せずに、修正、追加又は省略が一群の困難度の例になされてもよい。一例として、その群はより多数の、より少数の又は別の困難度を含んでもよい。別の例として、近似的な時間は異なってもよい。別の例として、困難度の程度は近似的時間以外のパラメータで表現されてもよい。
【００３１】
図１を再び参照するに、回路検証メトリック値は信頼度(confidence  value)を含んでもよい。信頼度は適切な如何なる手法で判断されてもよい。一例として、或る回路についてより大きなカバレッジを用意する一群の特性から計算された回路検証メトリック値には、より小さなカバレッジを用意する群から計算された回路検証メトリック値よりも大きな信頼度が与えられてもよい。
【００３２】
システム１０の１以上の要素は具体的な必要性に応じて統合されてもよいし或いは分離されてもよい。例えば、クライアントシステム２０及びサーバシステム２４の機能は、例えば単独のパーソナルコンピュータのような単独のコンピュータシステムを用いて用意されてもよい。何らかの要素が分離される場合には、その要素は、１以上のローカルエリアネットワーク（LAN）、メトロポリタンエリアネットワーク（MAN）、広域ネットワーク（WAN）、インターネットのようなグローバルコンピュータネットワークその他の有線若しくは無線リンクを用いて結合されてよい。
【００３３】
「コンピュータ」は、入力を受け入れ、所定の規則に従ってその入力を処理し、出力を生成する適切な如何なる装置にも関連し、例えば、パーソナルコンピュータ、ワークステーション、ネットワークコンピュータ、無線電話機、パーソナルディジタルアシスタント、これら若しくは他の装置内の１以上のマイクロプロセッサ、又は他の適切な如何なる処理装置にも関する。
【００３４】
システム１０の１以上の要素には、適切な入力装置、出力装置、大容量記憶媒体、プロセッサ、メモリ又はその他の要素が、システム１０の動作に従って情報を受信し、処理し、格納し又は通信するために含まれてもよい。一例として、システム１０の１以上の要素は、論理装置、インターフェース、メモリ、他の要素又はそれらの適切な如何なる組み合わせを含んでもよい。「論理装置又はロジック(logic)」はハードウエア、ソフトウエア、その他の論理装置又はそれらの適切な如何なる組み合わせに関連してもよい。或る論理装置は、装置の動作を管理し、例えばプロセッサを構成してもよい。「プロセッサ」は命令を実行し且つ動作を実行するためにデータを処理する適切な如何なる装置にも関連してよい。
【００３５】
「インターフェース」は、装置の入力を受信し、装置から出力を送信し、入力、出力若しくは双方の適切な処理を実行し、又はそれらの適切な如何なる組み合わせをも行う装置の論理装置に関連し、１以上のポート、対話ソフトウエア又は双方で構成されてもよい。「メモリ」は情報を記憶し及び検索を支援する論理装置に関連し、ランダムアクセスメモリ(RAM)、リードオンリメモリ（ROM）、磁気ドライブ、ディスクドライブ、コンパクトディスク（CD）ドライブ、ディジタルビデオディスクドライブ（DVD）、取り外し可能なメディアストレージ、その他の適切な如何なるデータストレージ媒体又はそれらの適切な如何なる組み合わせで構成されてもよい。
【００３６】
本発明の範囲から逸脱せずに、修正、追加又は省略がシステム１０になされてもよい。一例として、システム１０は回路設計を評価するように説明されるが、システム１０はソフトウエアを評価するために使用されてもよい。更に、システム１０の動作はより多数の、より少数の又は他のモジュールで実行されてもよい。更に、システム１０の動作は、ソフトウエア、ハードウエア、他の論理装置又はそれらの適切な如何なる組み合わせから成る適切な如何なる論理装置を用いて実行されてもよい。本願で使用される「各々」は、或る集合中のメンバ各々、又は或る集合の部分集合中のメンバ各々に関連する。
【００３７】
図３は或る回路の特性を検証する困難度を評価する方法例のフローチャートである。一実施例によれば、設計はラッチのような回路素子を有する回路を表現する。設計の構造的及び機能的な特徴は、或る特性について特性検証メトリック値を評価するために分析される。構造的特徴はデザイン３４の構造を記述し、機能的特徴はデザイン３４の動作を記述する。本方法は図１のシステムのような適切な如何なるシステムで実行されてもよい。
【００３８】
ステップ１００から本方法は始まり、入力が受信される。入力はモデル３０を含み、モデルはデザイン３４及び特性群３６中の特性で構成される。特性はマイター(miter)としてデザイン３４に挿入されてもよい。ステップ１０４では論理的な円錐状影響圏がデザイン３４から生成される。論理的な円錐状影響圏は、デザイン３４をゲートに合成し、その後にゲートから論理的な円錐状影響圏を抽出することにより生成されてもよい。
【００３９】
ステップ１０８では自動テストパターン生成(ATPG)プロセスが実行される。自動テストパターン生成プロセスは様々な信号での一連の値を正当化しようとする。プロセス中に、完全なデザイン３４の分析が必要とされないように、直接的なローカルな競合が発見される。従って自動テストパターン生成プロセスの結果及びランタイムは、困難度を示す。
【００４０】
一実施例によれば、小さなランタイムは低い困難度に対応し、大きなランタイムは高い困難度に対応する。図示の例では、ランタイム閾値より小さなランタイムは、その問題が些細なものであることを示す。ランタイム閾値は、些細な問題を確認するために選択される適切な如何なる値でもよい。一例として、ランタイム閾値は、１，２，３又は４秒のような５秒未満でもよい。
【００４１】
ステップ１１２にて、自動テストパターン生成プロセスのランタイムがランタイム閾値より小さかったならば、本方法はステップ１１６に進む。ステップ１１６では問題は些細なものとして分類される。そして本方法はステップ１５２に進む。
【００４２】
ステップ１１２にて、ランタイムがランタイム閾値より小さかったならば、本方法はステップ１２０に進み、限定モデル検査（BMC:  Bounded  Model  Checking）プロセスが実行される。本プロセスは、１０乃至６０秒（例えば約２０秒）のような適切な如何なる時間にわたって実行されてもよい。限定モデル検査プロセスは、特定の長さのカウンタ例を考察し、そのようなカウンタ例が存在する場合及びその場合にのみ充足可能である命題数式を検査する。一般に、或る境界内の時間フレーム数は所定数だけ前進的に増やされ、時間制限を超えるまで、より多くの時間フレーム数の間にわたって問題が解かれる。各ステップは、２乃至２０時間フレーム（例えば１０時間フレーム）のような適切な如何なる時間フレーム数だけ増やされてもよい。
【００４３】
一実施例によれば、時間フレーム数の増加率（レート）が困難度を示す。一実施例では、よい低いレートが高い困難度を示し、より高いレートが低い困難度を示す。図示の例によれば、或るレート閾値より少ないレートが高い困難度を示す。レート閾値は、例えば毎秒１０乃至６０時間フレーム（例えば、毎秒２０，３０又は５０時間フレーム）のような適切な如何なる値でもよい。
【００４４】
ステップ１２４にてレートがレート閾値より小さかった場合に、本方法はステップ１２８に進み、抽象化(abstraction)プロセスがデザイン３４について実行される。抽象化プロセスは、回路を適切に簡易化し、回路のサイズを減らす。一例として、冗長ラッチのような冗長回路要素が除去されてもよい。
【００４５】
抽象化プロセスは適切な如何なる手法で実行されてもよい。一実施例によれば、限定モデル検査プロセスを用いてプロセスが実行されてもよい。限定モデル検査プロセスは、２０乃至３０フレーム（例えば、２５フレーム）のような適切な如何なる限定を有してもよく、１０乃至６０秒（例えば、２０秒）のような適切な如何なる期間にわたって実行されてもよい。
【００４６】
一実施例によれば、オリジナル回路（当初回路）はオリジナル回路要素を含む。回路要素はオリジナル回路から抽象化され、残る回路要素を有する抽象化された回路を生み出す。例えば、充足不可能なコーン(cone)を構成するラッチが維持され、その残りは１次入力として抽象化される。回路の抽象性(abstractability)は、オリジナル回路から抽象化された要素数及びオリジナル回路要素数の関数として表現されてもよい。一例として、抽象性は、抽象化された回路要素とオリジナル回路要素との比率で規定されてもよい。
【００４７】
回路の抽象性及び残る回路要素数は困難度を示すかもしれない。例えばより高い抽象性はより低い困難度を示し、より多くの残存回路要素数は高い困難度を示してもよい。従って抽象性及び残存回路要素数は、問題を大まかな分類に分類するのに使用されてもよい。大まかな分類の具体例は図４を参照しながら詳細に説明される。
【００４８】
図４は抽象化された回路の最終的サイズ及び回路の抽象性に従う大まかな分類を例示するテーブル７０である。一実施例によれば、抽象性は、抽象化された回路要素の数とオリジナル回路要素数との比率として表現され、４つのカテゴリに分けられる。抽象化された回路のサイズ（最終サイズ）は、抽象化された回路のフリップフロップ（FF）の数として表現され、５つのカテゴリに分けられる。
【００４９】
本発明の範囲から逸脱せずに、修正、追加又は省略が大まかな分類例になされてもよい。一例として、大まかな分類はより多数の、より少数の、異なる最終サイズ又は抽象性のカテゴリを有してもよい。別の例として、大まかな分類はより多数の、より少数の又は異なる分類を有してもよい。
【００５０】
図３を再び参照するに、ステップ１２４でレートがレート閾値より小さくなかったならば、本方法はステップ１３０に進む。ステップ１３２ではBDDベースのシンボリックモデル検査プロセスが実行される。BDDベースのシンボリックモデル検査プロセスは、２進決定グラフのようにエンコードされる状態マシンを検証するプロセスに関連する。シンボリックモデル検査プロセスは適切な如何なる時間にわたって実行されてもよい。例えばそのプロセスは、抽象化された回路については約２０秒及び抽象化されてない回路については４０秒のように、１０乃至６０秒の間に実行されてもよい。
【００５１】
ステップ１３６ではシンボリックモデル検査プロセスによるデータが分析される。データは、抽象化プロセスが実行される場合にそれが過剰にアグレッシブ(aggressive)であるか否かを確認するために使用される。二分決定ダイアグラムのステップが短期間の内に深く進行するならば、その抽象性は過剰にアグレッシブであるとして指定される。例えば１５乃至２５秒（例えば、約２０秒）の内に、１４０より多く（例えば１５０より多く）深く進行する二分決定ダイアグラムステップを伴う抽象化は、過剰にアグレッシブであるとして指定されてよい。ステップ１４０にて抽象化が過剰にアグレッシブであると指定された場合には、本方法はステップ１４４に進み、その問題は不確定として分類される。そして本方法はステップ１５２に進む。
【００５２】
ステップ１４０で抽象化が過剰にアグレッシブであると指定されなかったならば、本方法はステップ１４８に進む。本方法はステップ１４８で二分決定ダイアグラムデータに従って分類される。シンボリックモデル検査プロセスがそのランタイム中に完了したならば、その困難度は些細な又は簡易なものとして指定されてよい。そうでなければ、二分決定ダイアグラムデータの他の特徴が、困難度を指定してもよいし、或いはステップ１３９で生成された分類を改良するために使用されてもよい。
【００５３】
一実施例によれば、二分決定ダイアグラム遷移関係のサイズが困難度を示す。より小さな遷移関係はより低い困難度を示す。一例として、15,000ノード未満の遷移関係のサイズは、低い困難度であってよい。二分決定ダイアグラムの成長率（レート）が困難度を示してもよい。より低いレートがより低い困難度を示してよい。一実施例によれば、BDDデータに従って問題を分類するのに以下のガイドラインが使用されてもよい。その分類はステップ１３０で生成された分類を改良し、最終的な分類を生成するために使用されてもよい：
１．２０秒でサイズが90,000ノードより大きかったならば、困難度は並の乃至非常に困難なものである。
【００５４】
２．２０秒でサイズが30,000ノードより小さかったならば、困難度は些細な乃至簡易なものである。
【００５５】
３．４０秒でサイズが160,00ノードより大きかったならば、困難度は困難な乃至非常に困難なものである。
【００５６】
４．４０秒でサイズが100,000ノードより小さかったならば、困難度は並の乃至簡易なものである。
【００５７】
ステップ１５２では結果が報告される。結果の報告後に本方法は終了する。
【００５８】
本発明の範囲から逸脱せずに、修正、追加又は省略が本方法になされてもよい。本方法はより多数の、より少数の又は他のステップを含んでもよい。更に、本発明の範囲から逸脱せずに適切な如何なる順序でステップが実行されてもよい。
【００５９】
上記の方法は合格する特性に適用する。同様な方法が不合格の特性に使用されてもよい。本方法は適切な如何なるガイドラインを含んでもよい。一例として、回路要素数が困難度を示してもよい。より多くの回路要素数が高い困難度を示してもよい。別の例として、二分決定ダイアグラム実行の深さが困難度を示してもよい。より深い２分決定ダイアグラムの進行は低い困難度を示してもよい。別の例として、限定検査フレームの成長率が困難度を示してもよい。より大きなレートがより低い困難度を示してよい。別の例として、二分決定ダイアグラム遷移関係が困難度を示してよい。より小さな遷移関係はより低い困難度を示してよい。
【００６０】
本発明の実施例は１以上の技術的恩恵をもたらす。一実施例による技術的恩恵は、回路を検証するための困難度が見積もられることである。回路の特性を検証するための困難度は、特性群中の各特性について判定される。回路を検証するための困難度は、特性の困難度から検証される。回路についての困難度を用いて、その回路を検証するのに要するリソース量を評価し、検証方法論を考案し、検証エンジンパラメータを調整し、検証用に回路設計を修正し、或いは適切な他の如何なることを実行してもよい。
【００６１】
本開示は或る実施例及び一般的に関連する方法の観点から説明されたが、実施例及び方法の代替例及び（ステップの）置換例は当業者に明白であろう。従って上記の実施例の説明は本開示内容を限定しない。添付の特許請求の範囲に規定されるように、本開示の精神及び範囲から逸脱せずに、他の変更、置換及び代替も可能である。
【００６２】
（付記１）
検証問題の困難度を評価する方法であって、
デザイン及び特性群を含む入力を受信するステップであって、前記特性群中の特性は前記デザインに関して検証されるところのステップと、
前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行するステップと、
前記検証プロセスに従って、各特性について特性検証メトリック値を確立するステップであって、前記特性検証メトリック値は前記デザインの各特性を検証する困難度を表現するところのステップと、
を反復するステップと、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定するステップであって、前記デザイン検証メトリック値は前記デザインの前記特性群を検証する困難度を表すところのステップと、
を有することを特徴とする方法。
【００６３】
（付記２）
前記デザインが、或る回路の回路設計を含み、
前記デザイン検証メトリック値が、回路検証メトリック値を有する
ことを特徴とする付記１記載の方法。
【００６４】
（付記３）
デザイン検証メトリック値を判定する前記ステップが、
前記特性群中の各特性について重みを割り当てるステップと、
前記特性検証メトリック値の重み付け平均と、特性に割り当てられた重みに従って重み付けされた特性の特性検証メトリック値を計算するステップと、
重み付け平均から、デザイン検証メトリック値を生成するステップと、
を有することを特徴とする付記１記載の方法。
【００６５】
（付記４）
特性検証メトリック値を確立するステップが、
特性について合格の特性検証メトリック値を確立するステップより成り、該合格の特性検証メトリック値は、前記特性が合格するのを仮定して前記特性を検証する困難度を表す
ことを特徴とする付記１記載の方法。
【００６６】
（付記５）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて自動テストパターン生成プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立する
ことを特徴とする付記１記載の方法。
【００６７】
（付記６）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて限定モデル検査プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、
前記限定モデル検査プロセスの成長率を判定するステップと、
前記成長率がレート閾値より少ない場合に、前記デザインについて抽象化プロセスを実行するステップと、
を有することを特徴とする付記１記載の方法。
【００６８】
（付記７）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、前記残存する第３要素数が残存する要素閾値より多い場合に、高い困難度を確立する
ことを特徴とする付記１記載の方法。
【００６９】
（付記８）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、
前記抽象性は抽象化された第１要素数とオリジナルの第２要素数との比率を有する前記デザインの抽象性を算出するステップと、
前記抽象性が抽象性閾値より大きい場合に、低い困難度を確立するステップと、
を有することを特徴とする付記１記載の方法。
【００７０】
（付記９）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの成長率を算出するステップと、
前記成長率が成長率閾値より大きかった場合に、高い困難度を選択するステップと、
を有することを特徴とする付記１記載の方法。
【００７１】
（付記１０）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの遷移関係のサイズを算出するステップと、
前記遷移関係のサイズが遷移関係サイズ閾値より小さかった場合に、低い困難度を選択するステップと、
を有することを特徴とする付記１記載の方法。
【００７２】
（付記１１）
媒体に組み込まれる、検証問題の困難度を評価する論理装置であって、
デザイン及び特性群を含む入力を受信するステップであって、前記特性群中の特性は前記デザインに関して検証されるところのステップと、
前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行するステップと、
前記検証プロセスに従って、各特性について特性検証メトリック値を確立するステップであって、前記特性検証メトリック値は前記デザインの各特性を検証する困難度を表現するところのステップと、
を反復するステップと、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定するステップであって、前記デザイン検証メトリック値は前記デザインの前記特性群を検証する困難度を表すところのステップと、
をコンピュータに実行させることを特徴とする論理装置。
【００７３】
（付記１２）
前記デザインが、或る回路の回路設計を含み、
前記デザイン検証メトリック値が、回路検証メトリック値を有する
ことを特徴とする付記１１記載の論理装置。
【００７４】
（付記１３）
デザイン検証メトリック値を判定する前記ステップが、
前記特性群中の各特性について重みを割り当てるステップと、
前記特性検証メトリック値の重み付け平均と、特性に割り当てられた重みに従って重み付けされた特性の特性検証メトリック値を計算するステップと、
重み付け平均から、デザイン検証メトリック値を生成するステップと、
を有することを特徴とする付記１１記載の論理装置。
【００７５】
（付記１４）
特性検証メトリック値を確立するステップが、
特性について合格の特性検証メトリック値を確立するステップより成り、該合格の特性検証メトリック値は、前記特性が合格するのを仮定して前記特性を検証する困難度を表す
ことを特徴とする付記１１記載の論理装置。
【００７６】
（付記１５）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて自動テストパターン生成プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立する
ことを特徴とする付記１１記載の論理装置。
【００７７】
（付記１６）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて限定モデル検査プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、
前記限定モデル検査プロセスの成長率を判定するステップと、
前記成長率がレート閾値より少ない場合に、前記デザインについて抽象化プロセスを実行するステップと、
を有することを特徴とする付記１１記載の論理装置。
【００７８】
（付記１７）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、前記残存する第３要素数が残存する要素閾値より多い場合に、高い困難度を確立する
ことを特徴とする付記１１記載の論理装置。
【００７９】
（付記１８）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、
前記抽象性は抽象化された第１要素数とオリジナルの第２要素数との比率を有する前記デザインの抽象性を算出するステップと、
前記抽象性が抽象性閾値より大きい場合に、低い困難度を確立するステップと、
を有することを特徴とする付記１１記載の論理装置。
【００８０】
（付記１９）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの成長率を算出するステップと、
前記成長率が成長率閾値より大きかった場合に、高い困難度を選択するステップと、
を有することを特徴とする付記１１記載の論理装置。
【００８１】
（付記２０）
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの遷移関係のサイズを算出するステップと、
前記遷移関係のサイズが遷移関係サイズ閾値より小さかった場合に、低い困難度を選択するステップと、
を有することを特徴とする付記１１記載の論理装置。
【００８２】
（付記２１）
検証問題の困難度を評価するシステムであって、
デザイン及び特性群を含む入力を受信する手段であって、前記特性群中の特性は前記デザインに関して検証されるところの手段と、
前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行し、
前記検証プロセスに従って、各特性について特性検証メトリック値を確立することを反復する手段であって、前記特性検証メトリック値は前記デザインの各特性を検証する困難度を表現するところの手段と、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定する手段であって、前記デザイン検証メトリック値は前記デザインの前記特性群を検証する困難度を表すところの手段と、
を有することを特徴とするシステム。
【００８３】
（付記２２）
検証問題の困難度を評価する方法であって、
デザイン及び特性群を含む入力を受信するステップであって、前記デザインは回路についての回路設計を含み、前記特性群中の特性は前記デザインに関して検証されるところのステップと、
前記特性群中の特性の各々について、
前記デザインにおける各特性について複数の検証プロセスを実行するステップと、
前記検証プロセスに従って、各特性について特性検証メトリック値を確立するステップであって、前記特性検証メトリック値は前記デザインの各特性を検証する困難度を表現するところのステップと、
を反復するステップであって、前記特性検証メトリック値を確立するステップは、
特性について合格の特性検証メトリック値を確立するステップであって、該合格の特性検証メトリック値は、前記特性が合格するのを仮定して前記特性を検証する困難度を表すところのステップより成るところのステップと、
前記特性群の前記特性検証メトリック値からデザイン検証メトリック値を判定するステップであって、前記デザイン検証メトリック値は回路検証メトリック値を含み、前記デザイン検証メトリック値は前記デザインの前記特性群を検証する困難度を表すところのステップであって、前記デザイン検証メトリック値を確立するステップは、
前記特性群中の各特性について重みを割り当てるステップと、
前記特性検証メトリック値の重み付け平均と、特性に割り当てられた重みに従って重み付けされた特性の特性検証メトリック値を計算するステップと、
重み付け平均から、デザイン検証メトリック値を生成するステップと、
を有するところのステップとを有し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて自動テストパターン生成プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、前記自動テストパターン生成プロセスのランタイムがランタイム閾値より少ない場合に、低い困難度を確立し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて限定モデル検査プロセスを実行するプロセスを有し、
特性検証メトリック値を確立するステップが、
前記限定モデル検査プロセスの成長率を判定するステップと、
前記成長率がレート閾値より少ない場合に、前記デザインについて抽象化プロセスを実行するステップとを有し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、前記残存する第３要素数が残存する要素閾値より多い場合に、高い困難度を確立し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、
前記デザインに抽象化プロセスを実行し、抽象化された第１要素数を、オリジナルの第２要素数を有するデザインから抽象化し、残存する第３要素数を生成するステップを有し、
特性検証メトリック値を確立するステップが、
前記抽象性は抽象化された第１要素数とオリジナルの第２要素数との比率を有する前記デザインの抽象性を算出するステップと、
前記抽象性が抽象性閾値より大きい場合に、低い困難度を確立するステップとを有し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの成長率を算出するステップと、
前記成長率が成長率閾値より大きかった場合に、高い困難度を選択するステップとを有し、
前記デザインにおける各特性について複数の検証プロセスを実行するステップが、前記デザインについて１以上の２分決定ダイアグラムに基づいてシンボリックモデル検査プロセスを実行するステップを有し、
特性検証メトリック値を確立するステップが、
前記２分決定ダイアグラムの遷移関係のサイズを算出するステップと、
前記遷移関係のサイズが遷移関係サイズ閾値より小さかった場合に、低い困難度を選択するステップとを有する
ことを特徴とする方法。
【図面の簡単な説明】
【００８４】
【図１】形式検証問題の困難度を評価するシステムの一例を示すブロック図である。
【図２】一群の困難度を例示するテーブルである。
【図３】或る回路の特性を検証する困難度を評価する方法例のフローチャートである。
【図４】抽象化された回路の最終的サイズ及び抽象性に従う大まかな分類を例示するテーブルである。
【符号の説明】
【００８５】
１０  システム
２０  クライアントシステム
２２  データベース
２４  サーバシステム
３４  デザイン
３６  特性
３９  モデル
４０  検証エンジン
４４  困難度推定器
４８  デザイン修正器
【図１】
0004806306.tif 000003
【図２】
0004806306.tif 000004
【図３】
0004806306.tif 000005
【図４】
0004806306.tif 000006