(57)【特許請求の範囲】
【請求項１】
電子回路設計の合成検証のための自動仮定を生成する、コンピュータによって実行される方法であって、プロセッサを用いて、
電子回路設計の挙動の第１の集合及び第２の集合を特定する段階と、
前記第１及び第２の集合の挙動に基づいて、前記挙動の第１の集合と第２の集合を分離する最小不完全決定論的有限オートマトン（ＩＤＦＡ）を反復的に計算する段階と、
前記最小ＩＤＦＡからの一般化によって決定論的有限オートマトン（ＤＦＡ）を判断する段階と、ここで、前記ＤＦＡは前記ＩＤＦＡから情報を収集するための学習処理を実行することにより判断され、
前記ＤＦＡアクションを判断する段階の結果を有形コンピュータ可読媒体上に記憶する段階と、
を含むことを特徴とする方法。
【請求項２】
前記挙動の第１の集合Ｓ1は、
0005269511.tif 000110
を満足し、前記挙動の第２の集合Ｓ12は、
0005269511.tif 000111
を満足し、ここでＬ1は、第１の言語であり、Ｌ2は、第２の言語であることを特徴とする請求項１に記載の方法。
【請求項３】
前記最小ＩＤＦＡがＬ1及びＬ2を分離するか否かを判断する段階、
を更に含むことを特徴とする請求項２に記載の方法。
【請求項４】
前記最小ＩＤＦＡがＬ1及びＬ2を分離するか否かを判断するアクションは、
前記最小ＩＤＦＡがＬ1及びＬ2を分離しないと判断される反証例を取得する段階と、
前記反証例がＬ1に属するか否かを判断する段階と、
を含む、
ことを特徴とする請求項３に記載の方法。
【請求項５】
前記反証例がＬ1に属すると判断される場合に該反証例を前記第１の集合に追加し、又は該反証例がＬ1に属さないと判断される場合に該反証例を前記第２の集合に追加する段階を更に含むことを特徴とする請求項４に記載の方法。
【請求項６】
前記反証例は、モデル検査から得られることを特徴とする請求項４に記載の方法。
【請求項７】
前記挙動の第１の集合又は前記第２の集合は、最初は空であることを特徴とする請求項１に記載の方法。
【請求項８】
前記最小ＩＤＦＡに対する問い合わせを更に含むか又はそれを実行する段階を含むことを特徴とする請求項１に記載の方法。
【請求項９】
前記最小ＩＤＦＡを反復的に計算するアクションは、
前記第１の集合及び前記第２の集合にわたってツリー状ＩＤＦＡの折り畳みを構成する段階と、
前記ツリー状ＩＤＦＡの一致パーティションを判断する段階と、
前記第１及び第２の集合を厳密に分離するオートマトンを判断する段階と、
を含む、
ことを特徴とする請求項１に記載の方法。
【請求項１０】
前記一致パーティションは、前記ツリー状ＩＤＦＡの状態数である濃度ｋのものであり、前記第１の集合及び前記第２の集合を分離する各ＩＤＦＡは、該第１の集合及び該第２の集合にわたって該ツリー状ＩＤＦＡに対して準同形であり、又は
前記折り畳みを構成するアクションは、前記第１の集合及び前記第２の集合にわたる前記ツリー状ＩＤＦＡの複数の状態から該第１の集合及び該第２の集合を分離する前記最小ＩＤＦＡの別の複数の状態へのマップを推定することによって実行される、
ことを特徴とする請求項９に記載の方法。
【請求項１１】
前記一致パーティションを判断するアクションは、
ｋ個の状態のパーティションを列挙するのに必要なビットの第１の数ｍを定義する段階と、
0005269511.tif 000112
状態が割り当てられるパーティションの第２の数を表すブール変数のベクトル
を定義する段階と、
前記パーティションが一致していることを保証する１つ又はそれよりも多くのブール制約の集合を構成する段階と、
を含む、
ことを特徴とする請求項９に記載の方法。
【請求項１２】
ｍが、ｌｏｇ2ｋに等しく、前記１つ又はそれよりも多くのブール制約の集合は、各状態ｓに対して
0005269511.tif 000113
を含み、
前記１つ又はそれよりも多くのブール制約の集合は、前記パーティションによる遷移関係を観察する段階を含み、又は
前記１つ又はそれよりも多くのブール制約の集合は、拒否状態及び拒否を異なるパーティションに配置する段階を含む、
ことを特徴とする請求項１１に記載の方法。
【請求項１３】
前記第１の集合及び前記第２の集合は、共に有限であることを特徴とする請求項１に記載の方法。
【請求項１４】
前記第１の集合又は前記第２の集合におけるサンプルが、前記電子回路設計における回路構成要素の挙動を構成することを特徴とする請求項１に記載の方法。
【請求項１５】
前記最小ＩＤＦＡから一般化することによってＤＦＡを判断するアクションは、
前記最小ＩＤＦＡの部分遷移関数に一致する全体遷移関数を表す最も単純な決定木を判断する段階、
を含む、
ことを特徴とする請求項１に記載の方法。
【請求項１６】
前記全体遷移関数は、アルファベット記号を該アルファベット記号がどの状態に遷移するかに従って分類し、該全体遷移関数は、分類のサンプルを該サンプルに一致する前記最も単純な決定木を判断するために提供し、該最も単純な決定木を判断するアクションは、ＩＤ３法を用いて実行され、該最も単純な決定木を判断するアクションは、決定木学習法を用いて実行され、該最も単純な決定木は、前記ＤＦＡのアルファベットを定めるブール変数上で分岐し、又は
前記最も単純な決定木の葉は、前記ＤＦＡの次の状態を示す、
ことを特徴とする請求項１５に記載の方法。
【請求項１７】
少なくとも１つのプロセッサによって実行されたときに、当該少なくとも１つのプロセッサに、請求項１から請求項１６のいずれかに記載の方法を実行させる実行可能コードを有する、コンピュータ使用可能記憶媒体に記録されたコンピュータプログラム。
【請求項１８】
請求項１から請求項１６のいずれかに記載の方法を実行するための手段を含む、電子機器の合成検証のための自動仮定を生成するためのシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、合成検証のための自動仮定を生成する方法、システム、及びコンピュータプログラム製品に関する。
【背景技術】
【０００２】
ハードウエアシステム及びソフトウエアシステムの関連において、システムをデバッグし、又はシステムが何らかの特性を示すことを明らかにするためにソフトウエア試験が広範囲に展開されている。それにも関わらず、ソフトウエア試験は、それ自体では、システムがある一定の種類の欠陥を持たないことを立証することができないことが多い。更に、それは、同じくそれ自体では、システムがある一定の特性を示すことを明らかにすることもできない。それに反して、形式的検証は、数学的方法を用いることにより、ソフトウエア及びハードウエアシステムの正しさを十分に立証又は反証し、従って、問題のシステムがある一定の欠陥を持たず、又はある一定の特性を示すことを立証することができる。
【０００３】
より具体的には、抽象的な数学的モデルを用いることにより、形式的検証は、問題のシステムがある一定の要件を満たすこと、又はシステムがある一定の特性又は挙動を示すことができることの立証を試みるものである。すなわち、そのようなシステムの形式的検証は、これらのシステムの抽象的数学的モデルに対して形式的な証明を与えることにより行われる。システムをモデル化するのに使用されることが多い数学的オブジェクトの一部の典型的な例は、有限状態機械及び様々なオートマトンである。
【０００４】
形式的検証過程には、一般的に２つの手法がある。一方の手法は、一般的にモデル検査と呼ばれている。モデル検査は、多くの場合に、有限数学的モデルの系統的に網羅的な調査で構成され、モデルにおける全ての状態及び遷移を調査することにより問題のシステムを検証する。モデル検査はまた、多くの場合に、システム内の各個々の状態を考慮する必要性を回避して演算時間を短縮するために、一部の抽象化技術を呼び出す。
【０００５】
他方の手法は、ある一定の定理証明過程を伴う、システムに関する数学的推論の公式バージョンで構成された論理的推論である。検証される項目は、多くの場合に、線形時相論理又は計算ツリー論理のような何らかの形式の時相論理を用いて表される。この後者の論理的推論手法の欠点は、論理的推論手法が、通常は部分的に自動化され、その効率及び実行可能性が、問題のシステムに関するユーザの知識に依存する場合があるという点である。
【０００６】
論理的推論手法の様々な限界及び欠点のために、モデル検査は、ハードウエアシステム及びソフトウエアシステムの正しさを形式的に検証する広く受け入れられた技術となっている。この技術の広い適用性に対する大きな障害の１つは、現実の世界のシステムの複雑性増大から生じる状態爆発問題である。合成検証は、状態爆発の問題を緩和する手法である。合成検証は、ソフトウエアシステム及びハードウエアシステムに関する検証タスクをシステムの個々の構成要素に関するより単純な検証問題に分解する。例えば、２つの構成要素Ｍ1とＭ2から成るシステムＭと、Ｍに対して検証する必要がある特性Ｐとを考察する。合成検証に対する仮定−保証様式は、以下のように説明する推論規則：Ａが全ての環境においてＭ1に対して維持され、かつＭ2がＡを満足するあらゆる環境においてＰを満足するように仮定Ａを特定することにより、ＰをＭに対して検証することができる、を用いる。この推論規則の適用を成功させる鍵は、コンパクトな仮定Ａの自動特定である。
【０００７】
【非特許文献１】Ｒ．Ｌ．Ｒｉｖｅｓｔ及びＲ．Ｅ．Ｓｃｈａｐｉｒｅ著「ホーミングシーケンスを用いた有限オートマトンの推論」、ＳＴＯＣ’８９：計算の理論に関する２１回年次ＡＣＭシンポジューム講演論文集、４１１ページから４２０ページ
【発明の開示】
【発明が解決しようとする課題】
【０００８】
従来、一部の従来技術の手法は、分離オートマトンを計算するための多項式−時間近似法を提案している。これらの方法は、正規言語の能動学習のためのＡｎｇｌｕｉｎのＬ*法の修正に基づくものである。一部の従来技術の手法は、このＬ*に基づく手法の符号による実施を呈示している。それにも関わらず、この手法の主な欠点は、近似限界がないという点である。すなわち、最悪な場合のシナリオでは、Ｌ*法は、自明な解Ｍ1を分離言語として戻し、従って、単にＭ1を最小にするだけでは取得することはできないと考えられる状態空間低減に関して利益を提供しないことになる。従って、合成検証における状態−爆発問題の影響を緩和する必要性が存在する。
【課題を解決するための手段】
【０００９】
２つの言語を分離する最小決定論的有限オートマトンを計算する方法、システム、及びコンピュータプログラム製品を開示する。本発明の一部の実施形態では、本方法は、サンプリング手法及びブール充足可能性解法を用いる。しかし、本発明の一部の実施形態では、本方法は、仮定−保証推論を用いた形式的検証の中間アサーションの生成に適用することができる。
【００１０】
本発明の態様、目的、及び利点の更なる詳細は、以下の詳細説明、図面、及び特許請求の範囲で説明する。上述の概要及び以下の詳細説明は、共に例示的かつ説明的なものであり、本発明の範囲に関して限定的であることを意図していない。
【００１１】
添付図面は、本発明の理解を深めるために含まれており、「発明を実施するための最良の形態」と共に本発明の原理を説明する役目をするものである。
【発明を実施するための最良の形態】
【００１２】
本発明のいくつかの実施形態は、合成検証のための自動仮定を生成する方法、システム、及びコンピュータプログラム製品を提供する。図１Ａを参照すると、処理は、１５２で、電子回路設計の第１の集合及び第２の集合の挙動を特定することにより始まる。特定したデータは、システム設計（電子ハードウエア、ソフトウエア、又はハードウエア及びソフトウエアの両方の組合せであるかを問わず）を「有限オートマトン」として特徴付けるために使用されることになり、有限オートマトン（有限状態機械とも呼ばれる）は、有限数の状態、それらの状態間の遷移、及びアクションで構成された挙動のモデルである。
【００１３】
次に、処理は、１５４で、第１及び第２の集合の挙動のサンプリングに基づいて、最小「不完全決定論的有限オートマトン」（ＩＤＦＡ）を反復的に計算する。決定論的有限状態機械は、状態及び入力記号の各対に対して、次の状態への１つ、かつ１つのみの遷移がある有限状態機械である。一部の場合には、有限状態オートマトンは、ある一定の挙動をモデル化するのに使用される何らかの情報を含まないので、不完全である場合がある。
【００１４】
ＩＤＦＡに基づいて、処理は、１５６で、最小ＩＤＦＡから一般化することにより決定論的有限オートマトン（ＤＦＡ）を判断する。これは、本質的に、ＤＦＡを判断するためにＩＤＦＡから十分な情報を収集するために学習処理を実行することにより達成される。それを判断した後、１５８で、ＤＦＡを有形コンピュータ可読媒体上に記憶することができる。
【００１５】
本発明の様々な実施形態は、合成検証のための自動仮定を生成する方法及びシステムを伴うので、本発明の一部の実施形態の基盤を提供するために、合成検証のための数学的モデルに対して最初に以下で説明する。
【００１６】
Ｉ．合成検証のための数学的モデル
この節で開示するのは、本発明の一部の実施形態でソフトウエア及びハードウエアシステムの正しさを形式的に立証するのに使用される数学的モデルである。
合成検証は、ソフトウエア及びハードウエアシステムの検証タスクをシステムの個々の構成要素のより単純な検証問題に分解する。２つの構成要素Ｍ1及びＭ2を含むシステムＭ、及びＭに対して検証する必要がある特性Ｐを最初に考察する。合成検証の仮定−保証様式では、以下の推論規則を用いる。
0005269511.tif 000002
（１）
【００１７】
上述の推論規則は、Ａが全ての環境においてＭ1を維持し、かつＡを満足するあらゆる環境においてＭ2がＰを満足させるような仮定Ａを特定することにより、ＰをＭに対して検証することができると説明している。言語−定理フレームにおいては、正規言語のような処理は、モデル化されて、有限オートマトンにより指定される。処理合成は、言語の交差であり、処理は、特性ＰをＬ（：Ｐ）とのその交差が空である時に満足する。従って、上述の推論規則は、以下のように書くことができる。
0005269511.tif 000003
（２）
【００１８】
次に、本方法及びシステムは、Ｌ（Ｍ2）及びＬ（：Ｐ）の交差をＭ2’と指定する。次に、仮定−保証引数を構成する問題は、Ｌ（Ａ）がＬ（Ｍ1）における全ての文字列を受諾するが、Ｌ（Ｍ2’）においては全ての文字列を拒否するという意味において、Ｌ（Ｍ1）及びＬ（Ｍ2’）を分離するオートマトンを見つけることに帰する。
【００１９】
明らかに、目的の１つは、仮定−保証規則の前例を検査する際に状態爆発の問題を最小にするために、できるだけ少数の状態を有するオートマトンＡを見つけることである。
【００２０】
決定論的オートマトンに対しては、最小状態分離オートマトンを見つけるという問題は、ＮＰ完全である。これは、ＮＰ完全であることが示される不完全決定論的有限オートマトン（ＩＤＦＡ）の最小状態での実行を見つける問題に還元可能である。この複雑性を回避するために、正規言語の能動学習のＬ*法の修正に基づく多項式時間近似法が提案されている。この手法の主な欠点は、近似限界がないという点である。すなわち、最悪な場合には、本方法は、自明な解Ｌ（Ｍ1）を分離言語として戻し、従って、単にＭ1を最小にするだけでは取得することはできないと考えられる状態空間低減に関して利益が得られないことになる。実際には、本発明の一部の実施形態において考慮したハードウエア検証問題に関する一部の実験においては、この手法では、ベンチマーク問題のいずれに対しても状態簡約が得られなかった。
【００２１】
開示する数学的モデルは、最小分離オートマトン問題を厳密に解くものである。検証問題全体は、Ｍ1及びＭ2’が記号で表された時にＰＳＰＡＣＥ完全であるので、多項式時間内で中間アサーションを見つけるという下位問題を解くことを必要とする理由がない。更に、仮定−保証推論の目標は、複雑性が｜Ｍ1｜ｘ｜Ｍ2’｜ではなく、｜Ｍ1｜＋｜Ｍ2’｜に比例する検証手順である。これが達成された場合、全体的な複雑性は、Ａが小さいことを条件として、｜Ａ｜において幾何学関数的であるということは重要ではないであろう。
【００２２】
この根本的な理由を念頭において、本発明の一部の実施形態では、ハードウエア検証の仮定−保証推論に適する最小分離オートマトン問題の厳密な手法を示す。本発明の一部の実施形態では、ＩＤＦＡ最小化の問題に向けて、ＩＤＦＡのサンプリングベースの方法を使用する。本方法では、Ｌ（Ｍ1）及びＬ（Ｍ2’）内にサンプル文字列を反復的に生成し、各段階でサンプルセットに一致した最小オートマトンを計算する。１組のラベル付き文字列に一致した最小オートマトンを見つけることは、それ自体、ＮＰ完全な問題である。本発明の一部の実施形態では、次に、ブール充足可能性（ＳＡＴ）解法を用いてそれを解く。サンプリング手法が使用されるのは、ＩＤＦＡ最小化問題を解く標準的な技術では、ハードウエア検証の場合に非実際的であると考えられる明示的な状態表現が必要であるからである。
【００２３】
ハードウエア用途に関しては、アルファベットは、Ｍ1及びＭ2を結ぶブール信号の数において幾何級数的であることも考慮に入れるべきである。この難しさも、Ｌ*ベースの手法において観察され、問い合わせ回数は、アルファベットのサイズに比例する。本発明の一部の実施形態では、部分的なアルファベットにわたってオートマトンを学習し、決定木学習法を用いてアルファベット全体まで一般化することによりこの問題を処理する。
【００２４】
合成ハードウエアベンチマークの集合を用いて、本発明の一部の実施形態では、この手法は、近似的Ｌ*手法により簡約が得られない場合に、厳密な最小中間アサーションを生成するのに有効であることを示している。一部の場合には、それによって最先端の方法を用いた直接的なモデル検査と比較して、全体的な検証において実質的な簡約が得られる。
【００２５】
Ａ．決定論的有限オートマトン（ＤＦＡ）
定義１：決定論的有限オートマトン（ＤＦＡ）Ｍは、５つ組（Ｓ、Σ、ｓ0、δ、Ｆ）であり、ここで、（１）Ｓは、状態の有限集合、（２）Σは、有限アルファベット、（３）δ：ＳｘΣ→Ｓは、遷移関数、（４）
0005269511.tif 000004
は、初期状態、（５）
0005269511.tif 000005
は、受諾状態の集合又は最終状態の集合である。尚、Ｆは、空の集合とすることができる。
定義２：不完全決定論的有限オートマトン（ＩＤＦＡ）Ｍは、６つ組（Ｓ、Σ、δ、ｓ0、Ｆ、Ｒ）であり、ここで、（１）Ｓは、状態の有限集合、（２）Σは、有限アルファベット、（３）
0005269511.tif 000006
は、部分遷移関数、（４）
0005269511.tif 000007
は、初期状態、（５）
0005269511.tif 000008
は、受諾状態の集合、（６）
0005269511.tif 000009
は、拒否状態の集合である。
【００２６】
直観的には、ＩＤＦＡは、一部の状態が完全アルファベットに対して外方の遷移を有することができないために不完全であり、一部の状態は、受諾状態でも拒否状態でもない。記号ａで状態ｓからの遷移がない場合、δ（ｓ、ａ）＝⊥である。ＤＦＡ及びＩＤＦＡの両方に対して、遷移関数δは、文字列に適用するために通常の方法で拡張することができる。すなわち、
0005269511.tif 000010
及び
0005269511.tif 000011
である場合、
0005269511.tif 000012
の時に
0005269511.tif 000013
であり、それ以外は、
0005269511.tif 000014
である。
【００２７】
文字列ｓは、
0005269511.tif 000015
の場合、ＤＦＡにより受け入れられ、そうでなければ、ｓは、Ｍにより拒否される。文字列ｓは、
0005269511.tif 000016
の場合、ＩＤＦＡにより受け入れられる。文字列ｓは、
0005269511.tif 000017
の場合、ＩＤＦＡのＭにより拒否される。
２つの言語
0005269511.tif 000018
を考慮すると、ＤＦＡ又はＩＤＦＡは、Ｌ1における全ての文字列を受け入れ、Ｌ2における全ての文字列を拒否した時にＬ1及びＬ2を分離する。Ｌ1及びＬ2の最小分離オートマトン（ＭＳＡ）は、Ｌ1及びＬ2を分離する最小数の状態に関するオートマトンである。
【００２８】
Ｂ．Ｌ*手法
比較のために、学習分離オートマトンのＬ*ベースの近似法に対して最初に説明する。Ｌ*手法では、学習者は、先生に質問を行うことにより未知の正規言語Ｌに対して最小ＤＦＡＡを推定する。メンバーシップ質問においては、学習者は、文字列πを示して、先生は、
0005269511.tif 000019
の場合はイエス、それ以外はノーと答える。同等性質問においては、学習者は、オートマトンＡを提案し、先生は、Ｌ（Ａ）＝Ｌの場合はイエスと答え、そうでなければ反証例を示す。反証例は、正（すなわち、Ｌ＼Ｌ（Ａ））である場合があり、又は負（すなわち、Ｌ（Ａ）＼Ｌ内の文字列）の場合がある。Ａのサイズにおいて多項式であるいくつかの質問においてＡを見出すことを保証する学習者の方法は、当業者には公知である。
【００２９】
Ｃｏｂｌｅｉｇｈ法では、２つの言語Ｌ1及びＬ2の分離オートマトンを学習するためにこの手順を若干修正する。これは、先生により行われる応答においてのみＬ*法と異なっている。同等性質問の場合、ＡがＬ1及びＬ2の分離オートマトンである場合にイエスと答える。そうでなければ、Ｌ1＼Ｌ（Ａ））内の文字列として正の反証例、又はＬ2∩Ｌ（Ａ）内の文字列として負の反証例を示す。文字列πに関するメンバーシップ質問に対して、先生は、
0005269511.tif 000020
の場合にイエスと答え、
0005269511.tif 000021
の場合にノーと答える。πがＬ1内でもＬ2内でもない場合、その選択は、任意である。先生は、最小分離オートマトンを知らないので、正しい答えを示すことはできず、従って、単純にノーと答える。従って、実際には、先生は、学習者にＬ1を学習するように求めるが、Ｌ1及びＬ2を分離するあらゆる推測を受け入れる意志がある。学習者のためのＡｎｇｌｕｉｎの方法を用いると、学習した分離オートマトンＡは、Ｌ1の最小オートマトンと同様に、状態を有していないことが分る。しかし、これは、最小分離オートマトンよりも任意に大きなものとすることができる。
【００３０】
Ａｎｇｌｕｉｎの元の方法における場合のように、質問の数は、Ａというサイズにおいては多項式であり、特に、同等性質問の数は、高々Ａにおける状態の数である。仮定−保証アプリケーションにおいては、Ｌ1＝Ｌ（Ｍ1）及びＬ2＝Ｌ（Ｍ2’）である。ハードウエア検証に対しては、Ｍ1及びＭ2’は、記号によって表された非決定論的有限オートマトン（ＮＦＡ）である（隠し入力及び：Ｐのオートマトンの構成から生じる非決定論）。メンバーシップ質問に答えることは、従って、ＮＰ完全であり、これは、本質的に、限定モデル検査の問題であり、一方、同等性質問に答えることは、ＰＳＰＡＣＥ完全であり、これは、記号モデル検査の問題である。従って、実際には、本方法の実行時間は、単に幾何級数的である。
【００３１】
Ｃ．最小分離オートマトン問題の厳密解法
２つの言語Ｌ1及びＬ2に対して厳密なＭＳＡを見つけるために、一部の実施形態では、ＩＤＦＡを最小にするＰｅｎａ及びＯｌｉｖｅｉｒａの一般的な手法に従うことになる。これは、同等性質問のみを用いる学習手法である。それは、２つの有限集合のストリームを分離する最小ＤＦＡを計算することができるサブルーチンに依存するものである。Ｐｅｎａ及びＯｌｉｖｅｉｒａの手法は、有限状態機械に限定されるが、その技術は、Ｌ1及びＬ2自体が正規言語でなくても、正則分離子を有するあらゆる言語Ｌ1及びＬ2に適用することができる。
【００３２】
この手順の全体的な流れは、処理１に示している。サンプルストリームの２つの集合
0005269511.tif 000022
及び
0005269511.tif 000023
を維持する。主ループは、Ｓ1及びＳ2を分離する最小ＤＦＡを計算することにより始まる（以下で説明する手順を用いて）。次に、学習者は、Ａに対して同等性質問を行う。ＡがＬ1及びＬ2を分離する場合、この手順は終了する。そうでなければ、先生からの反証例ストリームπを取得する。
0005269511.tif 000024
であり、従って、
0005269511.tif 000025
がＳ1に追加される場合、πをＳ2に追加する。この手順は、同等性質問が成功するまで繰り返される。以下の手法では、負の反証例を最初に試験し、次に、正の反証例を試験する。それにも関わらず、この順番は、任意であり、実際には、この順番は、１つの言語に向けて結果をバイアスさせる回避するために質問毎に無作為に選択することができる。
【００３３】
この手順において、先生は、モデルチェッカを使用して実施することができる。すなわち、検査
0005269511.tif 000026
及び
0005269511.tif 000027
は、モデル検査の問題である。このアプリケーションにおいては、Ｌ1及びＬ2は、記号で表されたＮＦＡの言語であり、記号モデル検査方法を用いて検査が行われる。尚、Ｌ（Ａ）内の閉じ込めを試験するには、Ａを補完することが必要であるが、これは、Ａが決定論的であることから簡単である。
【００３４】
定理１：有限Σに対して
0005269511.tif 000028
とする。Ｌ1及びＬ2が正則分離子を有する場合、処理１は、終了し、Ｌ1及びＬ2の最小分離オートマトンを出力する。
証明：ｋ個の状態で、Ａ’をＬ1及びＬ2の最小状態分離オートマトンとする。
0005269511.tif 000029
及び
0005269511.tif 000030
であるので、Ａ’は、Ｓ1及びＳ2の分離オートマトンということになる。従って、Ａは、ｋ個の状態のみを有する（Ｓ1及びＳ2の分離オートマトンであることから）。従って、この手順が終了した場合、Ａは、Ｌ1及びＬ2の最小分離オートマトンである。更に、有限のｋ個の状態で、有限Σを凌いで有限に多くのＤＦＡがある。毎回の反復時に、１つのこのようなオートマトンが、Ｓ1及びＳ2の分離子として除外される。従って、処理は終了すべきである。
【００３５】
この時点で、有限言語Ｓ1及びＳ2の最小分離オートマトンを計算することのみが残る。この問題は、広範囲に研究されており、ＮＰ完全であることは公知である。
定義３：ＩＤＦＡのＭ＝（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）は、関係
0005269511.tif 000031
がｓ0にルートを有する方向付けられたツリーである時にツリー状である。
あらゆる２つの互いに素の有限集合の文字列Ｓ1及びＳ2を考慮すると、Ｓ1を受け入れてＳ2を拒否するツリー状ＩＤＦＡが構成されることになり、ＴＲＥＥＳＥＰ（Ｓ1、Ｓ2）と呼ばれる。
定義４：
0005269511.tif 000032
を互いに素の有限言語とする。Ｓ1及びＳ2のツリー状分離子ＴＲＥＥＳＥＰ（Ｓ1、Ｓ2）は、ツリー状ＤＦＡ（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）であり、Ｓは、
0005269511.tif 000033
の接頭辞の集合であり、ｓ0は、空文字列であり、Ｆ＝Ｓ1及びＲ＝Ｓ2であり、
0005269511.tif 000034
である場合に
0005269511.tif 000035
それ以外は⊥である。
【００３６】
Ｏｌｉｖｅｉｒａ及びＳｉｌｖａの方法は、Ｓ1及びＳ2を分離する全てのＩＤＦＡＡが、ＴＲＥＥＳＥＰ（Ｓ1、Ｓ2）の準同形であることを示し、この方法は、次の節で定める。従って、ｋ個の状態の分離オートマトンＡを見つけるために、本発明の一部の実施形態では、ＴｒｅｅＳｅｐ（Ｓ1、Ｓ2）からＡの状態までのマップを推測しさえすればよく、相応にＡを形成する。この処理は、折り畳みと呼ばれる。
定義５：Ｍ＝（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）及びＭ’＝（Ｓ’、Σ’、ｓ0’、δ’、Ｆ’、Ｒ’）をアルファベットΣ上の２つのＩＤＦＡとする。マップφ：Ｓ→Ｓ’は、以下の時に、Ｍ’上へのＭの折り畳みである。
ａ．
0005269511.tif 000036
ｂ．全ての
0005269511.tif 000037
に対して、
0005269511.tif 000038
0005269511.tif 000039
であれば、
0005269511.tif 000040
ｃ．全ての
0005269511.tif 000041
かつ
ｄ．全ての
0005269511.tif 000042
【００３７】
以下の定理は、Ｓ1及びＳ2の全ての分離ＩＤＦＡが、ツリー状オートマトンＴＲＥＥＳＥＰ（Ｓ1、Ｓ2）の折り畳みとして取得することができるというものである。そのマップは、ツリー上で帰納的に容易に得られる。
定理２（ＯＬＩＶＥＩＲＡ及びＳＩＬＶＡ）：受諾集合Ｓ1及び拒否集合Ｓ2で、Ｔ＝（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）をツリー状ＩＤＦＡとする。Σ上のＩＤＦＡＡは、ＴからＡまでの折り畳みΣが存在する場合、かつＴからＡまでの折り畳みΣが存在する場合にのみ、Ｓ1及びＳ2の分離オートマトンである。
【００３８】
次に示すのは、状態を分割することによりツリーＴの折り畳みを形成する方法である。Гが集合Ｓのパーティションである場合、Ｓの要素ｓを含むГの要素を以下に［ｓ］Гで示す。
定義６：Ｍ＝（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）をΣ上のＩＤＦＡとする。Ｍの一致パーティションは、
ａ．全ての
0005269511.tif 000043
に対して、
0005269511.tif 000044
であり、
かつ
0005269511.tif 000045
かつ［ｓ］Γ  ＝［ｔ］Γであれば、
0005269511.tif 000046
かつ
ｂ．全ての状態
0005269511.tif 000047
及び
0005269511.tif 000048
に対して、
0005269511.tif 000049
であるようなＳのパーティションГである。
定義７：Ｍ＝（Ｓ、Σ、ｓ0、δ、Ｆ、Ｒ）をＩＤＦＡとし、ГをＳの一致パーティションとする。Ｍ／Гの商は、
ａ．
0005269511.tif 000050
ｂ．
0005269511.tif 000051
ｃ．
0005269511.tif 000052
かつ
ｄ．
0005269511.tif 000053
であるようなＩＤＦＡ（Г’、Σ’、ｓ0’、δ’、Ａ’、Ｒ’）である。
【００３９】
上記においては、
0005269511.tif 000054
は、⊥，Ｔ，及びＳの要素を収容する格子内の最小上界を表している。一致性は、最小上界が決してＴではないことを保証する。
定理３：受諾集合Ｓ1及び拒否集合Ｓ2で、Ｔがツリー状ＩＤＦＡとする。Ｔが濃度ｋの一致パーティションГを有する時にＳ1及びＳ2を厳密に分離するｋ個の状態のＩＤＦＡが存在する。更に、Ｔ／Гは、Ｓ1及びＳ2を分離する。
証明：Гは、Ｓ（Ｔ）の一致パーティションであると仮定する。ｓを［ｓ］Гにマップする関数φは、Ｔ／Г上へのＴの折り畳みであるということになる。従って、定理２により、Ｔ／Гは、をＳ1及びＳ2分離し、ｋ個の状態を有する。逆に、Ａは、Ｓ1及びＳ2を分離するｋ個の状態のＩＤＦＡであると仮定する。定理２により、ＴからＡへの折り畳みφが存在する。折り畳みの定義により、φにより導出されたパーティションは、一致パーティションであり、かつ（高々）ｋ個の状態を有する。
【００４０】
この理論に従って２つの互いに素の有限集合Ｓ1及びＳ2の最小分離オートマトンを見つけるために、対応するツリー状オートマトンＴのみを最初に構成する必要があり、次に、Ｓ（Ｔ）の最小一致パーティションГを取得することができる。最小オートマトンＡは、次に、Ｔ／Гである。
一部の実施形態では、ＳＡＴ解法を使用すると、ｋ個の状態の一致パーティションの存在の問題の以下の符号化を用いて最小パーティションを見つけることができる。ｎ＝［ｌｏｇ2ｋ］とする。これは、パーティションを列挙するために必要とされるビット数である。各状態
0005269511.tif 000055
に対しては、ブール変数
0005269511.tif 000056
のベクトルを導入する。これは、ｓが割り当てられるパーティションの番号及び商の対応する状態を表している。次に、パーティションが一致していることを保証するブール制約の集合を構成する。最初に、各ｓに対しては、
0005269511.tif 000057
（
0005269511.tif 000058
のビット数の上に表される）が存在すべきである。次に、記号ａに対して外向き遷移を有する状態ｓ及びｔの全ての対に対しては、制約
0005269511.tif 000059
が存在する。すなわち、パーティションは、遷移関係を尊重すべきである。最後に、状態
0005269511.tif 000060
及び
0005269511.tif 000061
の全ての対に対して、次に、制約
0005269511.tif 000062
を取得することができる。すなわち、拒否及び受諾状態は、同じパーティション内に置くことはできない。この集合の制約は、ＳａｔＥｎｃ（Ｔ）と呼ばれる。真理値割り当てψは、パーティションГ＝｛Г0、．．．、Гk-1｝がＴの一致パーティションである時に厳密にＳａｔＥｎｃ（Ｔ）を満足し、ここで、
0005269511.tif 000063
である。従って、満足する割り当てから、一致パーティションを抽出することができる。
【００４１】
有限集合Ｓ1及びＳ2の最小分離オートマトンは、処理２により見つけることができる。尚、商オートマトンＴ／Гは、ＩＤＦＡである。Ｔ／Гは、例えば、全ての不在遷移を拒否状態に行かせて、Ｓ1及びＳ2を分離するＤＦＡが得られるようにすることにより、あらゆる選択方法において部分遷移関数を完成することによりＤＦＡに変換することができる。本発明の一部の実施形態では、それによって２つの言語Ｌ1及びＬ2のＭＳＡを計算する手順が完成する。
【００４２】
処理２：ＳＡＴ符号化ＳＡＭＰＬＥＭＳＡ（Ｓ1、Ｓ2）を使用した有限言語に対するＭＳＡの計算
１．Ｔ＝ＴＲＥＥＳＥＰ（Ｓ1、  Ｓ2）とする；
２．ｋ＝１とする；
３．（１）の間に以下を行う
４．ＳＡＴＥＮＣ（Ｔ）が満足されれば、
５．ψをＳａｔＥｎｃ（Ｔ）の満足できる割り当てとする；
６．
0005269511.tif 000064
とする；
７．Ａ＝Ｔ／Γとする；
８．δ（Ａ）を何らかの方法で全体関数に拡張する；
９．ＤＦＡのＡに戻る
１０．ｋ＝ｋ＋１にする；
仮定−保証推論の中間アサーションを見つけるために、処理１を用いてＬ（Ｍ1）及びＬ（Ｍ2’）のＭＳＡのみを計算すべきである。
処理１：全体的な手順
ａ．ＡｓＧｒ（Ｌ1、Ｌ2）
１．Ｓ1＝｛｝；Ｓ2＝｛｝；
２．（１）である間に以下を行う
３．ＡをＳ1及びＳ2に対するＭＳＡとする；
４．
0005269511.tif 000065
であれば、次に
５．Ｌ（Ａ）∩Ｌ2＝φであれば、次に
６．真を戻す（Ａは、Ｌ1及びＬ2を分離する、特性が保持される）
７．それ以外であれば、
８．
0005269511.tif 000066
及び
0005269511.tif 000067
とする；（負の反証例）
９．
0005269511.tif 000068
であれば、次に
１０．偽を戻す；（Ｌ1及びＬ2は互いに素ではない、特性は、保持されない）
１１．それ以外であれば、
１２．
0005269511.tif 000069
１３．それ以外であれば、
１４．
0005269511.tif 000070
及び
0005269511.tif 000071
とする；（正の反証例）
１５．
0005269511.tif 000072
であれば、次に
１６．偽を戻す；（Ｌ1及びＬ2は互いに素ではない、特性は、保持されない）
１７．それ以外であれば、
１８．
0005269511.tif 000073
【００４３】
本発明の一部の実施形態の手法は、この時点で、この手順の全体的な複雑性を考慮する。Ｍ1及びＭ2’は、それぞれ、テキストサイズ｜Ｍ1｜及び｜Ｍ2’｜を有するブール回路として記号で表すと仮定することができる。次に、これらの機械の状態数は、それぞれ、Ｏ（２|M1|）及びＯ（２|M2'|）である。｜Ａ｜をＭＳＡのテキストサイズとする。尚、これは、状態数、Σのサイズの両方に比例する。主ループの毎回の反復では、ＳＡＴ問題ＳＡＴＥＥＮＣ（Ｔ）を解き、かつ２つのモデル検査問題を解く。ＳＡＴ問題は、最悪の場合、所定のサイズの全ての可能なＤＦＡを列挙することにより解くことができ、従って、Ｏ（２|A|）である。モデル検査問題は、Ｏ（｜Ａ｜×２|M1|）及びＯ（｜Ａ｜×２|M2'|）である。反復回数は、毎回の反復により１つのオートマトンが除去されるので、高々２|A|、すなわち、可能なオートマトン数である。従って、全体的な実行時間は、Ｏ（２|A|（２|A|＋｜Ａ｜ｘ（２|M1|＋２|M2'|）））である。これは、単純に｜Ａ｜、｜Ｍ1｜、及び｜Ｍ2’｜において幾何級数的であるが、明らかなことに、Ｍ1及びＭ2の積を計算するコストを負わずに済む。Ａのサイズを固定すると、この方法は、Ｏ（２|M1|＋２｜Ｍ２’｜）の実行時間を生じることを示すことができる。
【００４４】
残念ながら、｜Ａ｜は、最悪の場合にＬ（Ａ）＝Ｌ（Ｍ1）であるので、｜Ｍ1｜においては、最悪の場合は幾何級数的である。これは、全体的な複雑性が入力サイズにおいて２倍に幾何級数的であることを意味する。２倍に幾何級数的である方法をＰＳＰＡＣＥ完全な問題に適用することは、非論理的であると思われるであろう。しかし、実際には、小さな中間アサーションがある場合、この手法は、単純に幾何級数的である方法よりも効率的である可能性があることを観察することができる。しかし、アルファベットが大きい場合、遷移関数をコンパクトに符号化する何らかの方法を見つける必要性が存在すると考えられる。
【００４５】
Ｄ．決定木学習を用いた一般化
上述のように、ハードウエア検証においては、アルファベット＿のサイズは、Ｍ１とＭ２の間を通るブール信号の数において幾何級数的である。これは、実際には、Ｌ（Ｍ1）及びＬ（Ｍ2’）から取得したサンプルが含むアルファベット記号は取るに足らない部分に過ぎない可能性があることを意味する。従って、ＩＤＦＡＡも、Σの小さな部分に対する遷移を含むことになる。従って、適切な方法で完全なアルファベットにわたってこのＩＤＦＡからＤＦＡに一般化する何らかの方法を見つける必要性が存在すると考えられる。これは、とても良定義問題とは言えない。ある意味では、ＩＤＦＡの部分遷移関数と一致した「最も単純な」全体関数を推論してＯｃｃａｍの剃刀の適用を実行することができる。これを行う方法は数多くあるであろう。例えば、記号ａの所定の状態からの遷移がＩＤＦＡで定められていない場合、何らかの距離尺度に従って最も近い定義済み記号の次の状態にマップすることができる。
【００４６】
ここで取り上げる手法は、決定木学習法を用いて決定木としての部分遷移関数の最も単純な一般化を見つけようとするものである。アルファベット記号を考慮すると、決定木は、このアルファベットを定めるブール変数の値で分岐し、その葉でオートマトンの次の状態が得られる。一部の実施形態では、ＩＤＦＡの部分遷移関数と一致した全体遷移関数を表す最も単純な決定木を見つけることが望ましい場合がある。別の言い方をすれば、あらゆる状態の遷移関数は、アルファベット記号をどの状態にそれらが遷移するかに従って分類する分類子と見なすことができる。部分遷移関数は、この分類のサンプルを達成すると考えることができ、一部の実施形態では、これらのサンプルと一致した最も単純な決定木を見つけることが望ましい場合がある。直観的に、中間アサーションは、Ｍ1とＭ2の間で交換される信号の小さな集合だけに依存すると予測することができ、従って、一部の実施形態では、この手順を少数の信号に依存する遷移関数に向けてバイアスすることが望ましい場合がある。これを達成するために、ＩＤ３法は、一部の実施形態の例から決定木を学習するために使用することができる。
【００４７】
これは、処理２の行８において、これまで見てきたアルファベットのサンプルに基づいて完全な分離言語がどうあるべきかに関する推測を表す記号的に表したＤＦＡにＩＤＦＡを一般化することを可能にする。この推測が正しくない場合、先生は、この推測を拒否し、従って次の推測を洗練する反証例を生成することになる。
【００４８】
ＩＩ．本発明の例示的な実施形態
電子回路の合成検証のための自動仮定を生成するための本発明の一部の実施形態で実施されるような方法及びシステムの全体的な流れのブロック図を示す図１Ｂを参照する。１０２で、本方法は、本発明の一部の実施形態において、最初にサンプルの２つの集合Ｓ1及びＳ2を特定する。しかも、本発明の一部の実施形態では、検証すべき特性を更に特定する。本方法及びシステムは、次に、１０４で、最小分離不完全決定論的有限オートマトン（ＩＤＦＡ）を反復的に計算する。１１２で、本方法及びシステムは、以前に計算したＩＤＦＡを一般化し、完全なＤＦＡを出力して１０８に進む。一実施形態では、本方法及びシステムは、続いて１０８で、不完全決定論的有限オートマトンＡがＬ1及びＬ2を分離するか否かを判断する。
【００４９】
１０８で、不完全決定論的有限オートマトンＡがＬ1及びＬ2を分離すると判断された場合、この反復的手順は、終了して１１４に進む。そうでなければ、本方法及びシステムは、不完全決定論的有限オートマトンＡが厳密にＬ1及びＬ2を分離すると判断されるまで、アクション１０４から１０８を繰り返す。Ａが厳密にＬ1及びＬ2を分離するか否かを判断するアクションの後、本方法及びシステムは、次に、１１４で、一般化するアクションの結果を有形コンピュータ可読媒体に記憶する。
【００５０】
最小分離不完全決定論的有限オートマトン（ＩＤＦＡ）を反復的に計算するアクションに関する更なる詳細を例示する図２を参照する。２０２で、本方法及びシステムは、ツリー状不完全決定論的有限オートマトン（ＩＤＦＡ）Ｔを構成する。次に、本方法及びシステムは、２０４で、ＩＤＦＡの折り畳みを構成する。次に、２０６で、本方法及びシステムは、不完全決定論的有限オートマトンＴの状態数を表す濃度ｋの一致パーティションГを判断する。一方、本方法及びシステムは、商Ｔ／Гを判断する。先に示した数学的モデルに従って、商Ｔ／Гは、サンプルの２つの集合Ｓ1及びＳ2を厳密に分離する。
【００５１】
１０８で、ＡがＬ1及びＬ2を分離するか否かを判断するアクションの更なる詳細を例示する図３を参照する。不完全決定論的有限オートマトンＡが、Ｌ1及びＬ2を分離すると判断された場合、この反復的手順は終了し、本方法及びシステムは、３１０のアクション１１０に進む。不完全決定論的有限オートマトンＡが、Ｌ1及びＬ2を分離しないと判断された場合、本方法及びシステムは、３０２で、反証例πを取得する。一実施形態では、本方法及びシステムは、例えば、先生から反証例πを取得する。反証例πを取得した後、本方法及びシステムは、次に、３０４で、反証例πがＬ1に属するか否かを判断する。３０８で、反証例πがＬ1に属すると判断された場合、本方法及びシステムは、反証例πを第１の集合の例Ｓ1に追加する。３０６で、反証例πがＬ1に属さないと判断された場合、本方法及びシステムは、反証例πを第２の集合の例Ｓ2に追加する。
【００５２】
２０６の一致パーティションГを判断するアクションの更なる詳細を例示する図４を参照する。４０２で、本方法及びシステムは、最初に、パーティションを列挙するために必要とされるビット数ｍを定める。一実施形態では、Гは、Ｓ1及びＳ2上のツリー状ＩＤＦＡの状態数を表す濃度ｋに関する。別の実施形態では、ｍ＝ｌｏｇ2ｋである。４０４で、本方法及びシステムは、状態ｓが割り当てられるパーティションの番号を表すブール変数のベクトルを定める。４０６で、本方法及びシステムは、パーティションが一致していることを保証するブール制約の集合を構成する。
【００５３】
パーティションが一致していることを保証するブーリアン制約の更なる詳細を例示する図５を参照する。第１に、５０２は、各状態ｓに対して、ｖsのビットにわたって表される時に、ｖs＜ｋが存在すべきであることを示している。更に、５０４は、記号ａ上に外向き遷移を有する状態（ｓ、ｔ）の全ての対に対して、制約
0005269511.tif 000074
が存在することを示している。すなわち、パーティションは、遷移関係を尊重すべきである。更に、５０６は、状態
0005269511.tif 000075
の全ての対に対して、制約
0005269511.tif 000076
が存在することを示している。換言すると、制約５０６は、拒否状態及び受諾状態を同じパーティション内に置くことはできないことを要求する。
【００５４】
次に、これらの制約５０２、５０４、及び５０６を使用して、ベクトルブール変数
0005269511.tif 000077
を解く。パーティションГ＝｛Г0、．．．、Гk-1｝が、Ｔの一致パーティションである時に、厳密にこれらの制約を満足する真理割り当てψは、Ｔの一致パーティションであり、ここで、
0005269511.tif 000078
である。従って、満足する割り当てから、一致パーティションを抽出することができる。
【００５５】
以前に計算したＩＤＦＡから完全なＤＦＡを一般化するアクションの更なる詳細を例示する図６を参照する。決定論的有限オートマトン（ＤＦＡ）に対する計算した不完全決定論的有限オートマトン（ＩＤＦＡ）を一般化するアクション１１２の終了後、本方法及びシステムは、本発明の一部の実施形態では、部分遷移関数δを完成することによりＤＦＡに以前に計算したＩＤＦＡを一般化するために６０２に進む。代替的に、６０４で、本方法及びシステムは、本発明の一部の実施形態では、以前に計算したＩＤＦＡの部分遷移関数と一致した全体遷移関数を表す最も単純な決定木を判断するために６０４に進む。
【００５６】
このようにして、あらゆる状態の遷移関数は、本発明の一部の実施形態では、アルファベット記号を分類する分類子と見なすことができ、その状態に従ってアルファベット記号が遷移する（６０６）。部分遷移関数は、本発明の一部の実施形態では、この特定の種類の分類の「サンプル」を提供し、提供されたこれらのサンプルに一致する最も単純な決定木を見つけることを助けるものと見なすことができる（６０８）。更に、アルファベット記号を考慮すると、決定木は、アルファベットを洗練するブール変数の値で分岐し（６１０）、その葉では、オートマトンの次の状態が得られる（６１２）。中間アサーションはソフトウエア及びハードウエアのシステムの２つの構成要素Ｍ1及びＭ2の間で交換された信号の小さな集合だけに依存することが直観的に予想されるので、この手順は、少数の信号に依存する遷移関数に向けてバイアスする場合がある。本発明の一部の実施形態では、この目的を達成するために供給された例から決定木を学習するＩＤ３法を用いることができる（６１４）。
【００５７】
処理１において先に示すような全体的手順のブロック図を例示する図７を参照する。７０２で、本方法及びシステムは、最初に、サンプルの２つの集合Ｓ1及びＳ2を特定する。７０４で、本方法及びシステムは、サンプルの２つの集合Ｓ1及びＳ2の最小分離オートマトンＡを更に特定する。本方法及びシステムは、次に、７０６で
0005269511.tif 000079
か否かを判断する。７０８で
0005269511.tif 000080
と判断された場合、本方法及びシステムは、更に、
0005269511.tif 000081
か否かを判断する。７１８で
0005269511.tif 000082
と判断された場合、本方法及びシステムは、真を戻す。すなわち、最小分離オートマトンＡは、Ｌ1及びＬ2を分離し、特性ｐが保持される。
0005269511.tif 000083
と判断された場合、本方法及びシステムは、７１０で反証例πを特定し、ここで、
0005269511.tif 000084
である。本方法及びシステムは、７１２で反証例
0005269511.tif 000085
か否かを判断する。反証例
0005269511.tif 000086
である場合、本方法及びシステムは、７１４で偽を戻す。すなわち、Ｌ1及びＬ2は互いに素ではなく、ｐは、保持されない。
0005269511.tif 000087
と判断された場合、本方法及びシステムは、７１６で反証例πをＳ1に追加する。
【００５８】
７０６で
0005269511.tif 000088
が偽であると判断された場合、本方法及びシステムは、７２０で
0005269511.tif 000089
及び
0005269511.tif 000090
の両方を満足する反証例πを特定する。本方法及びシステムは、７２２で
0005269511.tif 000091
か否かを判断する。
0005269511.tif 000092
と判断された場合、本方法及びシステムは、次に、７２６で偽を戻す。すなわち、Ｌ1及びＬ2は互いに素ではなく、ｐは、保持されない。それに反して、
0005269511.tif 000093
と判断された場合、本方法及びシステムは、７２４でπをＳ2に追加する。アクション７１４、７１６、７１８、７２４、及び７２６の後に、本方法及びシステムは、７２８で同等性質問が成功するか否かを判断し、同等性質問が成功した場合、７３０でこの反復的手順を終了する。代替的に、７３２で、本方法及びシステムは、７０２に戻り、そこで、７２８で同等性質問が失敗すると判断される。
【００５９】
本発明の別の実施形態を例示する図８を参照する。８０２で、本方法及びシステムは、反復的に生成されるサンプルの集合で始まる。８０４で、本方法及びシステムは、完全なＤＦＡのＡを生成する学習法を呼び出す（８０６）。８０８で、本方法及びシステムは、
0005269511.tif 000094
か否かを判断する。別の実施形態では、
0005269511.tif 000095
の判断は、モデル検査呼び出しを構成する。
0005269511.tif 000096
の判断が失敗したと判断された８１０で、本方法及びシステムは、更に、
0005269511.tif 000097
か否かを判断する。別の実施形態では、
0005269511.tif 000098
の判断は、限定モデル検査呼び出しを構成する。
0005269511.tif 000099
の判断により偽が戻された場合、８１２でバグが報告される。代替的に、
0005269511.tif 000100
の判断により真が戻された場合、本方法及びシステムは、次に、８２０で最初に特定されたサンプルの集合に戻って、正のサンプルをそれに追加する。
【００６０】
0005269511.tif 000101
の判断が保持されていると判断された８１４で、本方法及びシステムは、
0005269511.tif 000102
か否かを判断する。別の実施形態では、
0005269511.tif 000103
の判断は、モデル検査呼び出しを構成する。８１４で、
0005269511.tif 000104
の判断により真が戻された場合、８２０で特性ｐが保持される。８１４で、
0005269511.tif 000105
の判断により偽が戻された場合、本方法及びシステムは、更に、８１６でサンプル
0005269511.tif 000106
か否かを判断する。別の実施形態では、
0005269511.tif 000107
か否かの判断は、限定モデル検査呼び出しを構成する。８１６で
0005269511.tif 000108
と判断された場合、本方法及びシステムは、バグを報告し、又は特性ｐは、保持されない（８１８）。８１６で
0005269511.tif 000109
が失敗すると判断された場合、本方法及びシステムは、８２０で最初に特定された集合のサンプルに戻って、負のサンプルをそれに追加する。
【００６１】
２ビットシフトレジスタを含む例示的なハードウエア回路を例示する図９を参照する。データは、ｘ１＿１、ｘ２−１からｘ１＿８、ｘ２＿８に移動中である。ｘＪ１及びｘＪ２は、自由入力を表している。ｘ１＿７の値は、ｘＪ１が１である場合にのみ更新される。同様に、ｘ２＿７の値は、ｘＪ２が１である場合にのみ更新される。初めは、全てのレジスタは、０に設定される。証明すべき特性は、ｘ１＿８及びｘ２＿８が、ｘ１＿１及びｘ２＿１が過去に１であった場合にのみ１であると説明する。仮定保証の適用のために、設計は、本発明の一実施形態に従ってＭ1及びＭ2に分解することができる。
【００６２】
図９に示す回路に関して本発明の一実施形態で本方法により生成された仮定オートマトンを例示する図１０を参照する。本発明の一実施形態におる方法の適用により、手元の特性を検証することができる最も小さい仮定オートマトンである３状態オートマトンが学習される。
本発明の一部の実施形態は、Ｃａｄｅｎｃｅ製ＳＭＶ（記号モデル検証器）又は他の「記号モデル検証器」上で実施することができる。本発明の一実施形態では、ユーザは、２つの成分へのソフトウエア及びハードウエアのシステムの分解を指定する。Ｃａｄｅｎｃｅ製ＳＭＶをＢＤＤベースのモデル検査システムとして使用して仮定を検証し、更に、増分ＢＭＣエンジンとして反証例を検査することができる。ＳＡＴ解法も上述の実施例において使用される。ＩＤ３法も、決定木を生成するように開発することができる。Ｃｏｂｌｅｉｇｈにより提案されているＬ*ベースの方法も、Ｒ．Ｌ．Ｒｉｖｅｓｔ及びＲ．Ｅ．Ｓｃｈａｐｉｒｅ著「ホーミングシーケンスを用いた有限オートマトンの推論」、ＳＴＯＣ’８９：計算の理論に関する２１回年次ＡＣＭシンポジューム講演論文集、４１１ページから４２０ページに提案されている最適化バージョンを用いて実施することができる。
【００６３】
本発明の一部の実施形態は、本発明の精神又はその本質的な特徴から逸脱することなく他の特定の形態に具現化することができることが当業者によって認められるであろう。従って、ここで開示した実施形態は、全ての点において例示的であり、制限的ではないと考えられる。本発明の一部の実施形態の範囲は、以上の説明ではなく、特許請求の範囲により示されており、その均等物の意味及び範囲に該当する全ての変更は、そこに包含されるものとする。
【００６４】
システムアーキテクチャ概要
図９は、本発明の実施形態を実行するのに適する例示的なコンピュータシステム１４００のブロック図である。コンピュータシステム１４００は、プロセッサ１４０４、システメモリ１４０６（例えば、ＲＡＭ）、静的記憶装置１４０８（例えば、ＲＯＭ）、ディスクドライブ１４１０（例えば、磁気又は光）、通信インタフェース１４１２（例えば、モデム又はイーサネットカード）、ディスプレイ１４１４（例えば、ＣＲＴ又はＬＣＤ）、入力デバイス１４１６（例えば、キーボード）、及びカーソル制御装置１４１８（例えば、マウス又はトラックボール）のようなサブシステム及びデバイスを相互接続する情報を伝達するためのバス１４０２又は他の通信機構を含む。
【００６５】
本発明の実施形態によれば、コンピュータシステム１４００は、システメモリ１４０６内に含まれた１つ又はそれよりも多くの命令のうちの１つ又はそれよりも多くシーケンスを実行するプロセッサ１４０４により特定の演算を行う。このような命令は、静的記憶装置１４０８又はディスクドライブ１４１０のような別のコンピュータ可読／使用可能媒体からシステメモリ１４０６に読み取ることができる。代替的な実施形態では、本発明の一部の実施形態を実行するためにソフトウエア命令の代わりに、又はソフトウエア命令と組み合わせて配線回路を使用することができる。
【００６６】
本明細書で使用される用語「コンピュータ可読媒体」又は「コンピュータ使用可能媒体」は、実行に向けて命令をプロセッサ１４０４に供給することに関わるあらゆる媒体を指す。このような媒体は、多くの形を取ることができ、不揮発性媒体及び揮発性媒体を含むがこれらに限定されない。不揮発性媒体としては、例えば、ディスクドライブ１４１０のような光ディスク又は磁気ディスクがある。揮発性媒体としては、システメモリ１４０６のような動的メモリがある。
【００６７】
一般的な形のコンピュータ可読媒体としては、例えば、フロッピーディスク、フレキシブルディスク、ハードディスク、磁気テープ、あらゆる他の磁気媒体、ＣＤ−ＲＯＭ、あらゆる他の光媒体、パンチカード、紙テープ、孔のパターンを有するあらゆる他の物理的媒体、ＲＡＭ、ＰＲＯＭ、ＥＰＲＯＭ、ＦＬＡＳＨ−ＥＰＲＯＭ、あらゆる他のメモリチップ又はカートリッジ、又はコンピュータ可読のあらゆる他の媒体がある。
【００６８】
本発明の実施形態では、本発明を実施する命令のシーケンスの実行は、単一のコンピュータシステム１４００により行われる。本発明の他の実施形態によれば、通信リンク１４２０（例えば、ＬＡＮ、ＰＴＳＮ、又は無線ネットワーク）により結合された２つ又はそれよりも多くのコンピュータシステム１４００は、互いと協働して本発明を実施するために必要な命令のシーケンスを実行することができる。
コンピュータシステム１４００は、通信リンク１４２０及び通信インタフェース１４１２を通じてプログラム、すなわち、アプリケーションコードを含むメッセージ、データ、及び命令を送受信することができる。受信プログラムコードは、受信時にプロセッサ１４０４により実行され、及び／又はその後の実行に向けてディスクドライブ１４１０又は不揮発性記憶装置に記憶することができる。
【００６９】
以上の明細書において、本発明を特定的な実施形態を参照して説明した。しかし、本発明のより広い精神及び範囲から逸脱することなく、様々な修正及び変更を行うことができることが明らかであろう。例えば、上述の処理フローは、処理アクションの特定の順序に関連して説明したものである。しかし、説明した処理アクションの多くのものの順序は、本発明の範囲又は作業に影響を与えることなく変更することができる。従って、本明細書及び図面は、制限的な意味ではなく例示的であると考えるものとする。
【図面の簡単な説明】
【００７０】
【図１Ａ】電子回路の合成検証のための自動仮定を生成する本発明の一部の実施形態に具現化された方法及びシステムの全体的な流れのブロック図である。
【図１Ｂ】電子回路の合成検証のための自動仮定を生成する本発明の一部の実施形態に具現化された方法及びシステムの全体的な流れの更なる詳細のブロック図である。
【図２】最小分離不完全決定論的有限オートマトン（ＩＤＦＡ）を反復的に計算するアクションに関するより詳細を示す図である。
【図３】Ａが２つの言語を分離するか否かを判断するアクションの更なる詳細を示す図である。
【図４】一致パーティションΓを判断するアクションの更なる詳細を示す図である。
【図５】パーティションが一致していることを保証するブール制約の更なる詳細を示す図である。
【図６】以前に計算したＩＤＦＡから完全なＤＦＡを一般化するアクションの更なる詳細を示す図である。
【図７】処理１において先に示すような全体的な手順のブロック図である。
【図８】本発明の別の実施形態による仮定の自動化された生成の方法を示す図である。
【図９】２ビットシフトレジスタを含む例示的なハードウエア回路を示す図である。
【図１０】図９に示す回路に対して本発明の一実施形態で本方法により生成された仮定オートマトンを示す図である。
【図１１】同時処理モデルでのタイミング閉鎖の方法を実行することができるコンピュータ化されたシステムを示す図である。
【符号の説明】
【００７１】
１５２  処理
ＤＦＡ  決定論的有限オートマトン
ＩＤＦＡ  不完全決定論的有限オートマトン
【図１Ａ】
0005269511.tif 000114
【図１Ｂ】
0005269511.tif 000115
【図２】
0005269511.tif 000116
【図３】
0005269511.tif 000117
【図４】
0005269511.tif 000118
【図５】
0005269511.tif 000119
【図６】
0005269511.tif 000120
【図７】
0005269511.tif 000121
【図８】
0005269511.tif 000122
【図９】
0005269511.tif 000123
【図１０】
0005269511.tif 000124
【図１１】
0005269511.tif 000125