(57)【特許請求の範囲】
【請求項１】
論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証用のコンピュータ支援設計装置を使用する方法であって、該装置が、主メモリに記憶されたコンピュータプログラムを実行するプロセッサと、メモリに記憶された第１及び第２の別個のディジタル回路の論理ネットワークよりなり、別個のディジタル回路の論理ネットワーク各々はディジタル回路の物理的論理設計を反映しており、別個のディジタル回路の論理ネットワーク各々は論理ゲートと相互接続された外部出力のセットよりなり、上記論理ゲートはワイヤによって相互接続され、上記論理ネットワークは上記装置における上記論理ゲートのうちの少なくとも一つと関係する論理的相互従属関係のセットを有し、一方の論理ネットワーク用の上記各外部出力は対応する外部出力を他方の論理ネットワークに有し、上記方法は、上記プロセッサによって実行される、
排他的論理和手段を用いて各論理ネットワークからの上記対応する外部出力を排他的論理和する段階と、
少なくとも一つのワイヤ上の位置を構成する上記別個の論理ネットワークの各々の点の間の論理的相互従属関係を判定する段階と、
仮のカット選択領域を上記別個の論理ネットワークの一方において選択し、反射的な仮のカット選択領域を上記別個の論理ネットワークの他方において選択する段階とを備え、上記各領域は論理ゲートのグループからなり、上記外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成し、上記仮のカット選択領域は少なくとも一つの論理ゲートと上記カットの上又は前方への少なくとも一つの関係する論理的相互従属関係とを更に備え、上記反射的な仮のカット選択領域は上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し少なくとも一つの関係する論理的相互従属関係を更に備え、上記方法は、上記プロセッサによって実行される、
上記カットを構成するあらゆる論理ゲートに対し一方の論理ネットワークの論理的相互従属関係を上記カットの上又は前方に有し、或いは、少なくとも一方の論理ネットワークの論理的相互従属関係を有する完全なカットのような他方の論理ネットワークの各々の上記カットの完全性をチェックする段階と、
上記カットが不完全な場合、上記別個の論理ネットワークの各々に対し上記カットを完全にするため要求される論理ゲートを定める論理ゲート判定段階と、
上記排他的論理和手段によってアサートされた等価性を示す出力信号を判定するため、上記別個の論理ネットワークに対し、上記外部出力のセットに最も近い上記仮のカット選択領域及び上記反射的な仮のカット選択領域にブール代数値を印加する影響を判定し、上記各論理ネットワークは等価であるかどうかを検証する検証段階を更に備える方法。
【請求項２】
上記反射的な仮のカット選択領域は一方の論理ネットワークに対し選択され、上記仮のカット選択領域は他方の論理ネットワークに対し選択されるよう上記選択する段階を繰り返す段階を更に有する請求項１記載の方法。
【請求項３】
上記選択する段階は、
一方の論理ネットワークの論理ゲートへの入力として上記ワイヤによって相互接続された少なくとも一つの上記論理ゲートを選択し、上記カットの上又は前方で、或いは、他方の論理ネットワークで、上記選択された論理ゲートに対し少なくとも一つの上記関係する論理的相互従属関係を選択する段階と、
上記選択された論理ゲートと、上記仮のカット選択領域内の上記相互従属関係との表現を格納する段階と、
上記論理ゲートへのあらゆる入力ワイヤが選択されるまで上記選択する段階及び格納する段階を繰り返す段階と、
を更に有する請求項１記載の方法。
【請求項４】
上記別個の論理ネットワークの各々に対する上記仮のカット選択領域の上記カットにはサイズがあり、
上記カットを構成するあらゆる論理ゲートがいずれか一方の論理ネットワークの上記カットの上又は前方で論理的相互従属関係を有するかどうかを表わす上記カットの完全性をチェックする段階と、
上記各カットが完全であるとき各カットの、ゲートの個数によるサイズを比較し、サイズが最も小さいカットを選択する段階と、
上記選択されたカットと、もう一方の論理ネットワークの上記反射的な仮のカット選択領域に対するカットとを用いて上記検証段階を行なう段階と、
を更に有する請求項１記載の方法。
【請求項５】
上記論理ゲート判定段階は、
少なくとも一つの上記外部出力から到達されるが、上記反射的な仮のカット選択領域に格納された上記関係する論理的相互従属関係の一つからは到達できない他方の論理ネットワークの論理ゲートをマークし、上記マークされた論理ゲートを候補点のセットとして格納する段階と、
上記別個の論理ネットワークの各々に対し、一方の論理ネットワーク、又は、他方の論理ネットワークの上記カットの上又は前方に関連する論理的相互従属関係を有する上記論理的相互従属関係のセット内の論理ゲートをマークし、上記マークされた論理ゲートの表現を更なる候補点のセットに格納する段階と、
上記候補点のセットと、上記更なる候補点のセットの両方に格納された論理ゲートをマークし、上記論理ゲートの表現を上記外部出力のセットに最も近い上記反射的な仮のカット選択領域に格納する段階と、
を更に有する請求項１記載の方法。
【請求項６】
上記論理的相互従属関係の判定段階は、
少なくとも一つの上記論理ネットワークの表現をコンピュータ支援設計装置の記憶装置に格納する格納段階と、
上記論理ゲートの中の目標論理ゲートに通じる論理ゲートのファンインに含まれる論理ゲートからなる上記論理ネットワークのカットセットを選択する段階と、
上記目標論理ゲートから通じる上記カットセット内の上記論理ゲートの決定図を構築する構築段階と、
上記目標論理ゲートの所定のブール代数値に対し上記決定図から正当化ベクトルを抽出し、上記論理ネットワーク内の潜在的学習対象領域の論理ゲートをマークするマーク段階と、
上記決定図と、上記潜在的学習対象領域の論理ゲート用の複数の別の決定図との間でブール代数演算を行ない、上記論理的相互従属関係を判定し、上記論理的相互従属関係を上記コンピュータ支援設計装置の記憶装置に格納する判定段階と、
を更に有する請求項１記載の方法。
【請求項７】
上記論理ネットワーク内の目標論理ゲートのセットの中の複数のゲートに対し、上記選択段階、構築段階、マーク段階及び判定段階を繰り返す段階を更に有する請求項６記載の方法。
【請求項８】
上記格納段階は、物理的なディジタル回路設計用の論理設計論理ネットワークの表現を格納する段階を更に有する請求項６記載の方法。
【請求項９】
各未正当化論理ゲートが唯一ではない正当化ベクトルを有する上記論理ネットワーク内の未正当化論理ゲートのセットを選択する段階と、
上記未正当化論理ゲートのセットから目標論理ゲートを選択する段階と、
を更に有する請求項６記載の方法。
【請求項１０】
上記カットセットの選択段階は、上記論理ネットワーク内で上記目標論理ゲートから所定の構造的な距離になるまで各論理ゲートの上記ファンインを後向きにトレースする段階を有する請求項６記載の方法。
【請求項１１】
上記構築段階は、複数の非端頂点と、複数の端頂点と、各非端頂点を別の非端頂点又は端頂点に相互接続する有向パスとからなる二分決定図の構築段階を更に有する請求項６記載の方法。
【請求項１２】
上記二分決定図の構築段階は、
上記カットセット内の上記論理ゲートに変数順列を作成する段階と、
あるサイズに対し上記目標論理ゲートに対応する根頂点から始まる上記論理ネットワークの構造的な深さと、上記二分決定図内の多数の頂点とを定め、上記目標論理ゲートから始まり上記サイズを有する上記カットセット用二分決定図を生成する段階と、
を更に有する請求項１１記載の方法。
【請求項１３】
上記マーク段階は、
上記目標論理ゲートに対応する根頂点から始まる上記決定図を辿ることにより、抽出が非端頂点で停止したとき不完全になるような正当化ベクトルのセットを抽出する段階と、
端頂点に達するまで上記決定図を辿ることにより、上記不完全な各正当化ベクトルを完全化する段階と、
ブール代数値の前向きの伝搬及び後向きの伝搬によって到達し得る全ての論理ゲートを評価するため上記論理ゲートの真理値表と上記論理ネットワークを使用して上記各正当化ベクトルをシミュレーションする段階と、
含意結果ベクトルの共通部分を定め、上記共通部分の表現を上記潜在的学習対象領域に格納する段階と、
を更に有する請求項６記載の方法。
【請求項１４】
上記判定段階は、
上記潜在的学習対象領域から上記論理ゲートの中の一つを選択する段階と、
上記選択された論理ゲートに対し、上記別の決定図の中の一つを構築する段階と、
結果を得るため上記決定図と上記別の決定図の間でブール代数演算を行なう実行段階と、
上記結果から論理的相互従属関係を定め、上記結果の表現を記憶装置に格納する段階と、
を更に有する請求項６記載の方法。
【請求項１５】
上記実行段階は、上記決定図と、上記選択された論理ゲートに対する上記別の決定図との間でブール代数のＡＮＤを行なう段階からなる請求項１４記載の方法。
【請求項１６】
論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証用のコンピュータ支援設計装置であって、該装置は、主メモリに記憶されたプログラムを実行するプロセッサと、メモリに記憶された第１及び第２の別個のディジタル回路の論理ネットワークよりなり、別個のディジタル回路の論理ネットワーク各々はディジタル回路の物理的論理設計を反映しており、別個のディジタル回路の論理ネットワーク各々は論理ゲートと相互接続された外部出力のセットよりなり、上記論理ゲートはワイヤによって相互接続され、上記論理ネットワークは上記装置における上記論理ゲートのうちの少なくとも一つの論理ゲートと関係する論理的相互従属関係のセットを含み、一方の論理ネットワーク用の上記各外部出力は対応する外部出力を他方の論理ネットワークに有し、上記装置は、
各論理ネットワークからの上記対応する外部出力を排他的論理和する手段と、
少なくとも一つのワイヤ上の位置を構成する上記別個の論理ネットワークの各々の点の間の論理的相互従属関係を判定する手段と、
仮のカット選択領域を上記別個の論理ネットワークの一方において選択し、反射的な仮のカット選択領域を上記別個の論理ネットワークの他方において選択する手段とを具備し、上記各領域は論理ゲートのグループからなり、上記外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成し、上記仮のカット選択領域は少なくとも一つの論理ゲートと上記カットの上又は前方への少なくとも一つの関係する論理的相互従属関係とを更に備え、上記反射的な仮のカット選択領域は上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し少なくとも一つの関係する論理的相互従属関係を更に備え、上記装置は、
上記カットを構成するあらゆる論理ゲートに対し一方の論理ネットワークの論理的相互従属関係を上記カットの上又は前方に有し、或いは、少なくとも一方の論理ネットワークの論理的相互従属関係を有する完全なカットのような他方の論理ネットワークの各々の上記カットの完全性をチェックする手段と、
上記カットが不完全な場合、上記別個の論理ネットワークの各々に対し上記カットを完全にするため要求される論理ゲートを定める論理ゲート判定手段と、
上記排他的論理和手段によってアサートされた等価性を示す出力信号を判定するため、上記別個の論理ネットワークに対し、上記外部出力のセットに最も近い上記仮のカット選択領域及び上記反射的な仮のカット選択領域にブール代数値を印加する影響を判定する手段を有する、上記各論理ネットワークは等価であるかどうかを検証する手段を更に具備する装置。
【請求項１７】
決定図の単純化を用いた論理設計検証用のコンピュータ支援設計装置を使用する方法であって、該装置が、主メモリに記憶されたプログラムを実行するプロセッサと、メモリに記憶された第１及び第２の別個のディジタル回路の論理ネットワークよりなり、別個のディジタル回路の論理ネットワーク各々はディジタル回路の物理的論理設計を反映しており、別個のディジタル回路の論理ネットワーク各々は、夫々が論理ゲートと相互接続された外部出力のセット及び外部入力のセットよりなり、上記論理ゲートはワイヤによって相互接続され、上記論理ネットワークは上記装置における上記論理ゲートのうちの少なくとも一つと関係する論理的相互従属関係のセットを有し、上記装置は更に、仮のカット選択領域を上記別個の論理ネットワークの一方において備え、反射的な仮のカット選択領域を上記別個の論理ネットワークの他方において備え、上記各領域は論理ゲートのグループからなり、上記外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成し、上記仮のカット選択領域は少なくとも一つの論理ゲートと上記カットの上又は前方への少なくとも一つの関係する論理的相互従属関係とを更に備え、上記反射的な仮のカット選択領域は上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し少なくとも一つの関係する論理的相互従属関係を更に備え、一方の論理ネットワーク用の上記各外部出力は対応する外部出力を他方の論理ネットワーク各々に有し、上記方法は、
排他的論理和手段を用いて上記別個の論理ネットワークの各々から上記対応する外部出力を排他的論理和する段階と、
少なくとも一つのワイヤ上の位置を構成する上記別個の論理ネットワークの各々の点の間の論理的相互従属関係の判定段階と、
上記仮のカット選択領域を表わす決定図と、上記反射的な仮のカット選択領域を表わす決定図との間でブール代数の排他的論理和を行なうことにより複合決定図を構築する構築段階と、
各学習条件に対し上記カットと上記外部出力の間にある論理ゲートを表わす決定図を構築し、上記学習条件を用いて上記複合決定図を単純化する段階からなる、上記別個の論理ネットワークの各々の学習条件を判定する段階と、
上記単純化された複合決定図の決定図の対を、上記カットに基づいてシャノンの展開式を、上記単純化された複合決定図の支持セット内の変数を上記決定図の対のうちの第１の決定図の第１の値に設定し、上記変数を上記決定図の対のうちの第２の決定図の第２の値に設定することによって適用することにより判定し、上記決定図の対を結合して、上記複合決定図を置き換える単純化複合決定図を構築する段階と、
上記カットを構成するあらゆる論理ゲートに対し上記別個の論理ネットワークの一方の論理的相互従属関係を上記カットの上又は前方に有し、或いは、上記別個の論理ネットワークの少なくとも一方の論理的相互従属関係を有する完全なカットのような上記別個の論理ネットワークの各々の上記カットの完全性をチェックする段階と、
上記カットが不完全な場合、上記別個の論理ネットワークの各々に対し上記カットを完全にするため要求される論理ゲートを定める論理ゲート判定段階と、
上記別個の論理ネットワークの各々に対し上記外部入力に構築された決定図を用いて上記複合決定図を合成し、上記排他的論理和手段によってアサートされた等価性を示す出力信号を判定するため上記決定図の間でブール代数排他的論理和を行ない、上記各論理ネットワークは等価であるかどうかを検証する段階と、
を有する方法。
【請求項１８】
上記論理的相互従属関係の判定段階は、
少なくとも一つの上記論理ネットワークの表現をコンピュータ支援設計装置の記憶装置に格納する格納段階と、
上記論理ゲートの中の目標論理ゲートに通じる論理ゲートのファンインに含まれる論理ゲートからなる上記論理ネットワークのカットセットを選択する段階と、
上記目標論理ゲートから通じる上記カットセット内の上記論理ゲートの決定図を構築する構築段階と、
上記目標論理ゲートの所定のブール代数値に対し上記決定図から正当化ベクトルを抽出する段階を有し、上記論理ネットワーク内の潜在的学習対象領域の論理ゲートをマークするマーク段階と、
上記決定図と、上記潜在的学習対象領域の論理ゲート用の複数の別の決定図との間でブール代数演算を行ない、上記論理的相互従属関係を判定し、上記論理的相互従属関係を上記コンピュータ支援設計装置の記憶装置に格納する判定段階と、
を更に有する請求項１７記載の方法。
【請求項１９】
上記論理ネットワーク内の目標論理ゲートのセットの中の複数のゲートに対し、上記選択段階、構築段階、マーク段階及び判定段階を繰り返す段階を更に有する請求項１８記載の方法。
【請求項２０】
上記格納段階は、物理的なディジタル回路設計用の論理設計論理ネットワークの表現を格納する段階を更に有する請求項１８記載の方法。
【請求項２１】
各未正当化論理ゲートが唯一ではない正当化ベクトルを有する上記論理ネットワーク内の未正当化論理ゲートのセットを選択する段階と、
上記未正当化論理ゲートのセットから目標論理ゲートを選択する段階と、
を更に有する請求項１８記載の方法。
【請求項２２】
上記カットセットの選択段階は、上記論理ネットワーク内で上記目標論理ゲートから所定の構造的な距離になるまで各論理ゲートの上記ファンインを後向きにトレースする段階を有する請求項１８記載の方法。
【請求項２３】
上記構築段階は、複数の非端頂点と、複数の端頂点と、各非端頂点を別の非端頂点又は端頂点に相互接続する有向パスとからなる二分決定図の構築段階を更に有する請求項１８記載の方法。
【請求項２４】
上記二分決定図の構築段階は、
上記カットセット内の上記論理ゲートに変数順列を作成する段階と、
あるサイズに対し上記目標論理ゲートに対応する根頂点から始まる上記論理ネットワークの構造的な深さと、上記二分決定図内の多数の頂点とを定め、上記目標論理ゲートから始まり上記サイズを有する上記カットセット用二分決定図を生成する段階と、
を更に有する請求項２３記載の方法。
【請求項２５】
上記マーク段階は、
上記目標論理ゲートに対応する根頂点から始まる上記決定図を辿ることにより、抽出が非端頂点で停止したとき不完全になるような正当化ベクトルのセットを抽出する段階と、
端頂点に達するまで上記決定図を辿ることにより、上記不完全な各正当化ベクトルを完全化する段階と、
ブール代数値の前向きの伝搬及び後向きの伝搬によって到達し得る全ての論理ゲートを評価するため上記論理ゲートの真理値表と上記論理ネットワークを使用して上記各正当化ベクトルをシミュレーションする段階と、
含意結果ベクトルの共通部分を定め、上記共通部分の表現を上記潜在的学習対象領域に格納する段階と、
を更に有する請求項１８記載の方法。
【請求項２６】
上記判定段階は、
上記潜在的学習対象領域から上記論理ゲートの中の一つを選択する段階と、
上記選択された論理ゲートに対し、上記別の決定図の中の一つを構築する段階と、
結果を得るため上記決定図と上記別の決定図の間でブール代数演算を行なう実行段階と、
上記結果から論理的相互従属関係を定め、上記結果の表現を記憶装置に格納する段階と、
を更に有する請求項１８記載の方法。
【請求項２７】
上記実行段階は、上記決定図と、上記選択された論理ゲートに対する上記別の決定図との間でブール代数のＡＮＤを行なう段階からなる請求項２６記載の方法。
【請求項２８】
上記別個の論理ネットワークの一方の論理ゲートへの入力として上記ワイヤによって相互接続された少なくとも一つの上記論理ゲートを選択し、上記カットの上又は前方で、或いは、上記別個の論理ネットワークのもう一方で、上記選択された論理ゲートに対し少なくとも一つの上記関係する論理的相互従属関係を選択する段階と、
上記選択された論理ゲートと、上記仮のカット選択領域内の上記相互従属関係の表現を格納する段階と、
上記論理ゲートへのあらゆる入力ワイヤが選択されるまで上記選択する段階及び格納する段階を繰り返す段階と、
を更に有する請求項１７記載の方法。
【請求項２９】
上記別個の論理ネットワークの各々に対する上記仮のカット選択領域の上記カットにはサイズがあり、
上記カットを構成するあらゆる論理ゲートが上記別個の論理ネットワークの一方又は上記別個の論理ネットワークの他方内の上記カットの上又は前方で論理的相互従属関係を有する上記カットの完全性をチェックする段階と、
上記各カットが完全であるとき各カットの、ゲートの個数によるサイズを比較し、サイズが最も小さいカットを選択する段階と、
上記選択されたカットと、上記別個の論理ネットワークの他方の中の上記反射的な仮のカット選択領域に対するカットとを用いて上記検証段階を行なう段階と、
を更に有する請求項２８記載の方法。
【請求項３０】
上記論理ゲート判定段階は、
少なくとも一つの上記外部出力から到達されるが、上記反射的な仮のカット選択領域に格納された上記関係する論理的相互従属関係の一つからは到達できない上記別個の論理ネットワークの他方の論理ゲートをマークし、上記マークされた論理ゲートを候補点のセットとして格納する段階と、
上記別個の論理ネットワークの各々に対し、上記別個の論理ネットワークの一方、又は、上記別個の論理ネットワークの他方内の上記カットの上又は前方に関連する論理的相互従属関係を有する上記論理的相互従属関係のセット内の論理ゲートをマークし、上記マークされた論理ゲートの表現を更なる候補点のセットに格納する段階と、
上記候補点のセットと、上記更なる候補点のセットの両方に格納された論理ゲートをマークし、上記論理ゲートの表現を上記外部出力のセットに最も近い上記反射的な仮のカット選択領域に格納する段階と、
を更に有する請求項１７記載の方法。
【請求項３１】
上記構築段階は、
上記別個の論理ネットワークの各々の上記論理ゲートに対する上記カットセットを表わす変数順列を定める段階と、
上記変数順列を用いて上記別個の論理ネットワークの各々の決定図を構築する段階と、
を更に有する請求項１７記載の方法。
【請求項３２】
上記複合決定図はサイズを有し、上記別個の各論理ネットワークの各論理ゲートは上記各論理ゲートのファンインに含まれる論理ゲートの入力コーンを有し、各学習条件はサイズを有し、上記学習条件を判定する段階は、
上記複合決定図のサイズの表現を格納するサイズ表現格納段階と、
上記別個の論理ネットワークの一方に対し、上記カットの前方にある入力コーンから論理ゲートを選択する論理ゲート選択段階と、
上記選択された論理ゲートの論理的相互従属関係のリストを辿り、上記カットの前方にある論理的相互従属関係を選択するトレース段階と、
上記選択された論理的相互従属関係から学習条件を構成する決定図の構築段階と、
上記学習条件のサイズが所定の値より小さいとき、上記学習条件を用いて上記複合決定図を単純化する単純化段階と、
を更に有する請求項１７記載の方法。
【請求項３３】
上記論理的相互従属関係のリストが完全に辿られるまで、上記トレース段階と、上記決定図の構築段階と、上記単純化段階とを繰り返す段階と、
上記別個の論理ネットワークの一方に対し上記カットの前方にあるあらゆる論理ゲートが選択されるまで、上記論理ゲート選択段階と、上記トレース段階と、上記決定図の構築段階と、上記単純化段階とを繰り返す段階と、
上記複合決定図のサイズが所定のパーセンテージ減少するまで、上記サイズ表現格納段階、上記論理ゲート選択段階、上記決定図の構築段階、及び、上記単純化段階を繰り返す段階と、
を更に有する請求項３２記載の方法。
【請求項３４】
上記単純化段階は、
あるサイズを有する単純化複合決定図を作成するため上記学習条件と上記複合決定図の間でブール代数和を行なう段階と、
上記単純化複合決定図の上記サイズが上記複合決定図のサイズより小さいとき、上記複合決定図を上記単純化複合決定図で置き換える段階と、
を更に有する請求項３２記載の方法。
【請求項３５】
上記決定図の対を判定する段階は、
上記単純化複合決定図内のすべての固有変数からなる支持セットの検出段階と、
上記支持セットの変数の選択段階と、
ブール代数の値０と等しい上記変数を使用して直接的かつ論理的相互従属関係を定め、ブール代数の値０に制限された上記決定図のために上記決定図を簡約化する第１の簡約化段階と、
ブール代数の値１と等しい上記変数を使用して直接的かつ論理的相互従属関係を定め、ブール代数の値１に制限された上記決定図のために上記決定図を簡約化する第２の簡約化段階と、
上記簡約化複合決定図のサイズが上記複合決定図のサイズより小さいとき、シャノンの展開式を適用し上記複合決定図を上記簡約化複合決定図で置換することにより、簡約化複合決定図を構成する構成段階と、
を更に有する請求項１７記載の方法。
【請求項３６】
上記支持セットのあらゆる変数が選択されるまで、上記選択段階と、上記ブール代数の値０と等しい変数を使用する簡約化段階と、上記ブール代数の値１と等しい変数を使用する簡約化段階と、上記構成段階とを繰り返す段階を更に有する請求項３５記載の方法。
【請求項３７】
上記複合決定図のサイズが所定のパーセンテージ減少するまで、上記選択段階と、上記ブール代数の値０と等しい変数を使用する簡約化段階と、上記ブール代数の値１と等しい変数を使用する簡約化段階と、上記構成段階とを繰り返す段階を更に有する請求項３５記載の方法。
【請求項３８】
決定図の単純化を用いた論理設計検証用のコンピュータ支援設計装置であって、該装置が、主メモリに記憶されたプログラムを実行するプロセッサと、メモリに記憶された第１及び第２の別個のディジタル回路の論理ネットワークよりなり、別個のディジタル回路の論理ネットワーク各々はディジタル回路の物理的論理設計を反映しており、別個のディジタル回路の論理ネットワーク各々は、夫々が論理ゲートと相互接続された外部出力のセット及び外部入力のセットよりなり、上記論理ゲートはワイヤによって相互接続され、上記論理ネットワークは上記装置における上記論理ゲートのうちの少なくとも一つと関係する論理的相互従属関係のセットを有し、上記装置は更に、仮のカット選択領域を上記別個の論理ネットワークの一方において備え、反射的な仮のカット選択領域を上記別個の論理ネットワークの他方において備え、上記各領域は論理ゲートのグループからなり、上記外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成し、上記仮のカット選択領域は少なくとも一つの論理ゲートと上記カットの上又は前方への少なくとも一つの関係する論理的相互従属関係とを更に備え、上記反射的な仮のカット選択領域は上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し少なくとも一つの関係する論理的相互従属関係を更に備え、一方の論理ネットワーク用の上記各外部出力は対応する外部出力を他方の論理ネットワーク各々に有し、上記装置は、
上記別個の論理ネットワークの各々から上記対応する外部出力を排他的論理和する排他的論理和手段と、
少なくとも一つのワイヤ上の位置を構成する上記別個の論理ネットワークの各々の点の間の論理的相互従属関係を判定する手段と、
上記仮のカット選択領域を表わす決定図と、上記反射的な仮のカット選択領域を表わす決定図との間でブール代数の排他的論理和を行なうことにより複合決定図を構築する手段と、
各学習条件に対し上記カットと上記外部出力の間にある論理ゲートを表わす決定図を構築する手段、及び、上記学習条件を用いて上記複合決定図を単純化する手段を含み、上記別個の論理ネットワークの各々の学習条件を判定する手段と、
上記単純化された複合決定図の支持セット内の変数を上記決定図の対のうちの第１の決定図の第１の値に設定し、上記変数を上記決定図の対のうちの第２の決定図の第２の値に設定することによって、上記カットに基づいてシャノンの展開式を適用することにより上記単純化された複合決定図の決定図の対を判定する手段、及び、上記決定図の対を結合して、上記複合決定図を置き換える単純化複合決定図を構築する手段と、
上記カットを構成するあらゆる論理ゲートに対し一方の論理ネットワークの論理的相互従属関係を上記カットの上又は前方に有し、或いは、少なくとも一方の論理ネットワークの論理的相互従属関係を有する完全なカットのような他方の論理ネットワークの各々の上記カットの完全性をチェックする手段と、
上記カットが不完全な場合、上記別個の論理ネットワークの各々に対し上記カットを完全にするため要求される論理ゲートを定める論理ゲート判定手段と、
上記別個の論理ネットワークの各々に対し上記外部入力に構築された決定図を用いて上記複合決定図を合成し、上記排他的論理和手段によってアサートされた等価性を示す出力信号を判定するため上記決定図の間でブール代数排他的論理和を行なう手段よりなる上記各論理ネットワークの等価性を検証する手段と、
を具備する装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は一般的にコンピュータ支援設計（ＣＡＤ）装置及び方法に係り、特に、コンピュータ装置のディジタル回路設計及び検証のためのＣＡＤ方法及び装置に関する。
【０００２】
【従来の技術】
大規模にプログラム化されたディジタルコンピュータを使用するディジタル回路のコンピュータ支援設計は、十分に発達した技術である。ディジタル回路用ＣＡＤは、提案されたディジタル回路、又は、従来のディジタル回路の論理信号の値の割当、及び、論理ゲート間の論理的相互従属関係に関して、より多量の情報を得るため幾つかの方式を使用している。論理設計解析は、ディジタル回路の構造的論理ネットワークに基づいて論理的相互接続及び相互従属関係を決めるためＣＡＤに使用されている。上記処理の重要な部分は、所定の値の割当の状況の結果として、直接或いは間接の両方で表わすことができる全ての信号値を識別することである。上記部分には、所定の値の割当の状況の結果として、回路内の２個以上の論理ゲートの間で種々の単純又は複雑、かつ、物理的又は論理的関係を認識することが含まれている。
【０００３】
上記解析処理は一般的に学習と呼ばれ、論理的な相互接続及び相互従属関係は、"含意(implication) "と呼ばれる。例えば、ディジタル回路のための自動テストパターン発生器（ＡＴＰＧ）と、論理的ハードウェアの最適化と、論理的ハードウェアのタイミング解析と、ディジタル回路のエンジニアリング変更には、論理設計解析が必要である。ＣＡＤにおいて直面する問題は、時間とメモリ空間の両方に関し計算用資源が要求されることである。上記のような問題に直面する理由は、ＣＡＤの問題は、総じて、一般的にＮＰ完全又は至難問題と呼ばれ、場合によっては指数的な個数の考え得るあらゆる回路への入力値を探索するためのコンピュータを必要とするからである。そのため、最悪の場合、完全な解を見つけるため指数関数的な量の時間及び／又はメモリ空間が必要である。従って、上記問題を解決するため、優れた効率的な発見的方法（ヒューリスティック）又は簡便な方法を設計する必要がある。
【０００４】
例として、ディジタル回路設計の検証を考えてみよう。マリック(S. Malik)等の"論理解析環境における二分決定図を使用する論理検証(Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment)" 、ICCAD、6-9 ページ（1988年発行）と、藤田(M. Fujita) 等の"二分決定図に基づくブール代数比較法の評価及び改良(Evaluation and Improvements of Boolean Comparison Methods Based on Binary Decision Diagrams)"、ICCAD 、2-5 ページ（1988年発行）に記載されているように、上記検証は、一般的に、二分決定図(binary decision diagrams)方式のデータ表現を使用して行なわれる。このような二分決定図ベースの検証処理は、比較される論理設計に既知の論理的相互接続が殆ど又は全くない場合、最も利点がある。論理設計に多数の類似性がある場合、ベルマン(C.L. Berman)とトレビリアン(Trevyllian)の"ＶＬＳＩ回路の論理設計の関数的比較(Functional Comparison of Logic Designs for VLSI Circuits)"、ICCAD、456-459ページ（1989年発行）と、ブランド(D. Brand)の"大規模統合設計の検証(Verification of Large Synthesized Designs)"、ICCAD 、534-537 ページ（1993年発行）と、サーニー(E. Cerny)とマウラス(C. Mauras)の"クロス可制御性とクロス可観測性の関係を用いる恒真論理式チェック(Tautology Checking Using Cross-Controllability and Cross-Observability Relations)"、ICCAD、34-38 ページ（1990年発行）と、クンツ(W. Kunz)の"ハンニバル：再帰的学習に基づく論理検証用の有効なツール(HANNIBAL:An Efficient Tool for Logic Verification Based on Recursive Learning)"、ICCAD 、（1993年発行）に記載されているように、この設計は、屡々、論理ゲート間で一定の値が付与された関係を見つける方式を用いて検証される。
【０００５】
含意関係ベースの検証装置は基本的に二つのフェーズで動作する。フェーズＩの間、検証される二つの回路を構成する論理ゲートの間に生じる含意は学習される。上記含意関係には、二つの回路間の論理的等価及び論理的に逆の信号、又は、ゲート出力の検出が含まれている。回路は種々の学習レベル数を用いて解析される。
【０００６】
フェーズＩＩの間、学習された含意は、内部論理ゲートのセット（集合）と外部出力の間にある回路の一部を検査することにより等価性を証明するため使用される。
【０００７】
【発明が解決しようとする課題】
上記従来の解決法の場合、必要とされる計算時間が解析される学習レベルの数に従って指数関数的に増加するという難点がある。現在の技術によれば、上記方式は解析される学習レベルの数と共に指数関数的に著しく不経済になるので、上記方式を５以上のレベルに適用することは実際的ではない。
【０００８】
従って、一方の論理ゲートでアサートされた一定のブール代数値によって、別の論理的又は物理的に相互接続された論理ゲートに別の一定のブール代数信号を発生させる（又は示させる）論理的相互接続を見つけることは、大規模な回路設計の場合、計算上非効率的になる可能性がある。上記方式には、一定の値が付けられていない別のタイプの有効な"含意関係"を検出し得る一般性はない。含意関係とは、全ての外部入力の値に対して、ある信号値がある値をとるときに、他のある信号値が必ずある値をとる、という関係である。
【０００９】
更に、十分な数の含意関係がない、含意関係の性質が十分ではない、或いは、検査された回路の一部は完全ではないフェーズＩＩの間に、上記回路の一部しか検査されなかった場合、上記方式では設計検証に失敗する。「不完全な」部分は、カットセットと二つの回路の外部出力の間にある回路の一部との解析による二つの回路の検証を直ちに妨げる。最悪の場合、関数的な学習方式は、幾つかの論理的な関係を識別するため指数関数的な時間を必要とすることに注意すべきである。これは、根本的な問題がＮＰ完全性であることに起因する。
【００１０】
ＣＡＤ業界における別の重要な問題は、ディジタル回路の製造欠陥のテストベクトルを得るためのＡＴＰＧの問題である。特定の欠陥のタイプは、冗長性欠陥と呼ばれている。通常のＡＴＰＧ機器でこのような欠陥を検出することは困難な場合が多い。回路内の論理ゲート間の論理的相互関係のより効率的な解析が学習技術を用いて必要とされる場合がある。従って、シュルツ(Schultz)等の"ソクラテス：著しく効率的な自動テストパターン発生システム(SOCRATES:Highly Efficient Automatic Test Pattern Generation System)"、ＩＴＣ(1987)に記載されているように学習ベースのＡＴＰＧ機器は、欠陥が冗長であり、検出困難な場合、一層好ましい動作を行なう。学習によって関係及び制約を発見することにより、目標とされたテストベクトルの探索空間は縮小される。しかし、上記ツールは、一定の評価がされた学習だけを使用することによって制限され、現状技術では、上記学習の中には発見の際に不必要に過剰な計算資源を使うものがある。
【００１１】
従って、上記従来の問題点を解決するためには、ディジタル回路論理ネットワーク内の点の間の論理的相互従属関係を定める論理設計解析を実行し、ディジタル回路が等価であるかどうかを検証し、ハードウェア設計の表現の構成のための計算用資源を削減し、かつ、ディジタル回路におけるゴール向き学習を実行し、即ち、より多くのゲートのレベル数を省くことにより、処理速度を向上させ、所要時間を削減し、処理に要するメモリ空間を削減するコンピュータ支援設計装置及び方法が必要である。
【００１２】
更に、ディジタル回路が論理ゲートの大規模かつ複雑な論理ネットワークである場合、上記問題を解決するコンピュータ支援設計装置及び方法が必要である。
【００１３】
更に、一定の評価がされた"含意関係"と、関数的な評価がされた"含意関係"の両方を検出するコンピュータ支援設計装置及び方法が必要である。
【００１４】
更に、検証されたディジタル回路の対の一方の一部が不適切（不完全）であるか、或いは、完全であるかを判定するコンピュータ支援設計装置及び方法が必要である。
【００１５】
【課題を解決するための手段】
上記問題を解決する本発明は、ディジタル回路の論理ネットワークを構成する論理ゲートの間で論理的相互従属関係（"含意関係"）を決めるための論理設計解析を行い、回路が等価であるかどうかを検証し、ハードウェア設計の表現を構成するための計算用資源の必要量を削減し、ゴール向き学習を実行する関数的学習を採用する。
【００１６】
本発明の一実施例は、ディジタル回路の論理ネットワーク中の点の間で論理的相互従属関係を定める論理設計解析を行なうコンピュータ支援設計装置及び方法である。上記論理ネットワークは、外部出力のセット及び外部入力のセットからなり、両方のセットは論理ゲートと相互接続されている。論理ゲートはワイヤによって相互接続されている。上記各点は、上記論理ゲートの一つにアサートされ、又は、上記論理ゲートの一つからアサートされた信号を伝搬するワイヤ上にある。上記論理ネットワークの表現は、コンピュータ支援設計装置の記憶装置に格納される。論理ゲートの中の目標論理ゲートに繋がる論理ゲートのファンインに含まれる論理ゲートからなる論理ネットワーク内のカットセットが選択される。目標論理ゲートから得られるカットセット内の論理ゲートに対し決定図が構築される。論理ネットワーク中の潜在的学習対象領域内の論理ゲートはマークされる。正当化(justification)ベクトルは、目標論理ゲートの所定のブール代数値の決定図から得られる。上記論理的相互従属関係は判定され、論理的相互従属関係の表現はコンピュータ支援設計装置の記憶装置に格納される。ブール代数演算は、決定図と、潜在的学習対象領域内の論理ゲートの複数の他の決定図の間で実行される。
【００１７】
本発明の他の一実施例は、論理的相互依存関係のある論理ゲートのグループを使用する論理設計検証のためのコンピュータ支援設計装置及び方法である。上記装置は、各々が論理ゲートと相互接続された外部出力のセットよりなる第１及び第２の別個のディジタル回路の論理ネットワークにより構成される。論理ゲートはワイヤによって相互接続されている。論理ネットワークは、装置内の少なくとも一つの論理ゲートと関係のある論理的相互従属関係のセットを有する。別個の各論理ネットワークに対する上記外部出力の各々は、別個の論理ネットワークのもう一方に対応する外部出力がある。上記別個の各論理ネットワークからの対応する出力は、排他的論理和手段を用いて一緒に排他的論理和が行なわれる。仮のカット選択領域は別個の論理ネットワークの一方で選択され、反射的な仮のカット選択領域は別個の論理ネットワークのもう一方で選択される。上記各領域は論理ゲートのグループからなるので、外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成する。仮のカット選択領域は、少なくとも一つの論理ゲートと、カットの上又は前方に少なくとも一つの関係する相互従属関係とを更に有し、反射的な仮のカット選択領域は、上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し少なくとも一つの関係する論理的相互従属関係を更に有する。各回路の等価性は、排他的論理和手段によって示された等価性を表わす出力信号を判定するため、別個の論理ネットワークの各々の外部出力のセットに最も近い仮のカット選択領域及び反射的な仮のカット領域の論理ゲートの回路へのブール代数値の印加の影響を判定することにより検証される。
【００１８】
本発明の他の一実施例は、決定図の単純化を使用する論理設計検証用のコンピュータ支援装置及び方法である。上記装置は、第１及び第２の別個のディジタル回路の論理ネットワークからなり、各論理ネットワークは、夫々論理ゲートと相互接続された外部出力の組及び外部入力の組とからなる。論理ゲートはワイヤを介して相互接続されている。上記論理ネットワークは、装置内の少なくとも一つの論理ゲートに関係する論理的相互従属関係のセットを有する。上記装置は、別個の論理ネットワークの一方に仮のカット領域を更に有し、別個の論理ネットワークのもう一方に反射的な仮のカット選択領域を更に有する。上記各領域は、論理ゲートのグループからなるので、外部出力のセットに最も近い領域内の論理ゲートに接続するワイヤはカットを形成する。仮のカット選択領域は、少なくとも一つの論理ゲートと、上記カットの上又は前方に少なくとも一つの関係する論理的相互依存関係とを更に有する。上記反射的な仮のカット選択領域は、上記仮のカット選択領域内の少なくとも一つの論理ゲートに対し、少なくとも一つの関係する論理的相互依存関係を更に有する。上記別個の論理ネットワークの上記各外部出力は、他の別個の論理ネットワークの各々に対応する外部出力を有する。別個の論理ネットワークの各々からの上記対応する外部出力は排他的論理和手段を用いて排他的論理和される。複合決定図は、仮のカット選択領域を表わす決定図と、反射的な仮のカット選択領域を表わす決定図の間でブール代数排他的論理和を行なうことにより構築される。学習条件は別個の論理ネットワークの各々に対し定められる。上記各学習条件は、カットと外部出力の間にある論理ゲートを表わす決定図よりなり、複合決定図は学習条件を用いて単純化される。共通因子決定図の対は、カットに基づいてシャノンの展開式を適用することにより単純化された複合決定図に対し定められ、上記対は上記複合決定図の代わりに用いられる簡約化複合決定図を構築するため合成される。各論理ネットワークの等価性は、別個の各論理ネットワークの外部入力上に構築された決定図を用いて別個の複合決定図を作成することにより検証され、ブール代数排他的論理和は、排他的論理和手段によってアサートされた等価性を表わす出力信号を定めるため、決定図の間で行なわれる。
【００１９】
本発明の更なる一実施例は、ハードウェア設計の表現を構成するための計算資源必要量の削減用のコンピュータ支援設計装置及び方法である。上記装置は、論理ゲートと夫々相互接続された外部出力のセット及び外部入力のセットよりなるディジタル回路の論理ネットワークからなる。論理ゲートはワイヤによって相互接続されている。上記論理ネットワークは少なくとも一つの論理ゲートと関係する論理的相互従属関係のセットを有する。上記表現は、ハードウェア設計の一部又は全部を表わす決定図よりなる。上記ディジタル回路の論理ネットワークの論理ゲートのファンインに含まれる論理ゲートからなる副回路の論理ネットワークは、上記ディジタル回路の論理ネットワークから選択される。少なくとも一つの上記論理ゲートからなるカットセットが選択され、これにより、上記外部出力のセットに最も近い上記論理ゲートの中に接続する上記ワイヤがカットを形成し、上記カットセット内の各論理ゲートが上記カットの上、又は、前方にある論理的相互従属関係を有するかどうかが判定される。決定図は上記カットセットを用いて構築される。上記決定図は単純化され、これにより、単純化された決定図が上記決定図より小さいとき、単純化された決定図は上記決定図の代わりに用いられる。上記決定図は、上記外部入力のセットを上記ハードウェア設計の表現として用いて合成される。
【００２０】
本発明の更なる一実施例は、ゴール向き学習の実行用のコンピュータ支援設計装置及び方法である。上記装置は、論理ゲートと夫々相互接続された外部出力のセット及び外部入力のセットよりなるディジタル回路の論理ネットワークからなる。上記論理ゲートはワイヤによって相互接続されている。上記論理ネットワークは装置内の少なくとも一つの論理ゲートと関係する論理的相互従属関係のセットを有し、上記外部出力のセットに最も近い上記論理ゲートの中に接続する上記ワイヤがカットを形成するよう少なくとも一つの上記論理ゲートよりなるカットセットを有する。ゴール向き学習は、所定のゴールを満足するよう装置を制御する。上記カットと上記外部出力の間にある論理ゲートのリストが定められ、これにより、各論理ゲートは上記カットから最大限所定の構造的な距離しか離れてない。上記リストから論理ゲートが選択され、上記所定の構造的な距離に等しい学習レベルとの論理的相互従属関係が定められる。上記リスト内の各論理ゲートは、あらゆる論理ゲートが選択されるまで選択される。上記方法は、上記所定の構造的な距離が更なる所定の構造的な距離よりも小さく、かつ、上記所定のゴールが満足されていない間繰り返される。
【００２１】
本発明の更なる他の実施例は、本発明を実施するため最良の態様であると考えられる本発明の好ましい実施例を例として示し記載している以下の詳細な説明によって当業者に容易に分かるようになる。本発明の精神と範囲を逸脱することなく、本発明の他の異なる実施例を構成することが可能であり、かかる実施例の詳細中、種々の明らかな面で変形可能なものがある。従って、以下の添付図面及び実施例の説明は、本質的にその例に限定されることのない例であると考えることが必要である。
【００２２】
【発明の実施の形態】
本発明のコンピュータ支援設計装置は図１に示されている。マイクロプロセッサ３は、主メモリ２に記憶されたコンピュータプログラム７を実行し、２次記憶装置１を使用する。コンピュータ７の実行結果は、ディスプレイ４とプリンタ５に出力され、結果ファイル６に格納される。主メモリ２は、回路が等価的であるかどうかを検証し、ハードウェア設計の表現を構成する計算資源の必要量を減少させ、ゴールを目指した学習を行なうため、論理的相互従属関係を決める論理設計解析の動作のシーケンスを実行するコンピュータプログラム７を格納する。２次記憶装置１はデータファイルを格納し、主メモリ２に格納されたコンピュータプログラム７を実行するマイクロプロセッサ３にデータファイルを提供するため使用される。
【００２３】
Ｉ．  論理設計解析
図１の装置で使用されるような論理的相互従属関係を定める論理設計解析を実行するコンピュータ支援設計装置及び方法のブロック図を図２に示す。コンピュータプログラム７は、他の部品を統合する主制御部１６を含む７個の主な部品からなる（ブロック１０，１１，１２，１３，１４，１５及び１６）。２次記憶装置１は９個のファイル（ブロック９，１７，１８，１９，２０，２１，２２，２３及び２４）を格納する。初期化及び候補セット選択部１０は、論理設計論理ネットワークファイル１から候補論理ゲートセット１７を作成する。未正当化ゲート選択部１１は、論理ネットワークを後向きにトレースすることにより、未正当化ゲートセット１８を発生する。カットセット選択部１２は、各未正当化論理ゲートのファンインにある論理ゲートを選択することによりカットセット２０を生成する。二分決定図構築部１３は、論理ネットワークに具現化された論理を表わすためカットセット２０に基づいて二分決定図２１を生成する。潜在的学習対象領域マーカー部１４は、正当化ベクトル／パスセット２２に格納された正当化ベクトルと、固有ブール代数値セット１９に記憶されたような回路内に既に存在する固有ブール代数値を使用して潜在的学習対象領域セット２３を特定するため二分決定図２１を解析する。最終的に、含意学習部１５は、回路の論理ネットワークに基づいて含意を学習するため潜在的学習対象領域セット２３内の各ゲートに対し一連の二分決定図２４を発生し、含意は、ディスプレイ４とプリンタ５に出力され、結果ファイル６に格納される。
【００２４】
ここで、用語について簡単に説明する。論理回路中のある一つのゲート（ゲートｇ）を選択すると、ゲートｇから外部入力の方向に向かって、すなわち、通常の論理演算の流れの向きとは逆に、他の論理ゲートを辿って外部入力まで到達することができる。このとき、辿った論理ゲートの集合は、ゲートｇの「入力コーン」と呼ぶ。この入力コーンに含まれるゲートの部分集合Ｓにおいて、外部入力からゲートｇに至るパスが、必ずこの集合Ｓの要素であるゲートを通過するような集合Ｃを作ることができる。この部分集合Ｃは、「カットセット（カットライン又はカット）」と呼ばれる。
【００２５】
次に、論理回路をシミュレーションする場合、たとえば、信号値として、０，１，Ｘの３値を使用して、全ての信号値をＸとした後に、外部入力に何らかの信号値を設定して出力に向かって演算を行う。逆に、あるゲートの出力にある論理値（０又は１）を設定して、外部入力の方向へ向かって、矛盾が起きないように信号値を求める処理を「正当化処理（justification)」と呼ぶ。これは、ＡＴＰＧで頻繁に使用される手法である。たとえば、前出のカットＣとゲートｇの間に挟まれている部分論理回路を考える。ゲートｇに論理値１又は０を設定して、部分回路に正当化処理を施して、集合Ｃに含まれる各ゲートに対する値が求められたとする。このとき、集合Ｃのゲートに割り当てられた信号値をベクトル（信号値をスカラーとした場合に、スカラーの集合）として表現したものを「正当化ベクトル」と呼ぶ。
【００２６】
本発明は、論理回路中の含意関係にある信号の組を求めることに関する。「含意関係」とは、全ての外部入力の値に対して、ある信号値がｖ（０又は１）をとるとき、他のある信号が必ずｗ（０又は１）となる関係を表わす。たとえば、ＡＮＤ（論理積）ゲートのある入力が０であるならば、出力は必ず０になる。この関係は、一般に、一方向だけで成り立つ関係であり、逆は必ずしも真ではない。このような含意関係を求める処理を「学習(learning)」と呼ぶ。
【００２７】
本来、全ての外部入力の値の組合せをシミュレーションすることにより、内部信号の含意関係を全て求めることが可能である。しかし、外部入力数が大きい回路では、このようなシミュレーションは実用的ではない。そこで、本発明では、ある内部信号ｓに着目して、その信号から、たとえば、数ゲート分だけ入力方向へ遡ったカットを求める。たとえば、信号ｓの値を１にするためのカット上の信号値（ベクトル）の組（すなわち、複数のベクトル）を求め、この信号値の組を与えて、論理回路の動作をシミュレーションする。この複数回のシミュレーションにおいて、常に同じ値をとった信号（たとえば、信号ｔ）は、信号ｓとの間で含意関係が成立する可能性がある。シミュレーションに用いられる信号値の組は、全ての組合せではないので、信号ｔは、含意関係のある「可能性」のある信号である。このような信号ｔの集合は、「潜在的な学習の対象領域」、すなわち、「潜在的学習対象領域(potential learning area)」である。この領域が求められると、真に含意関係のある信号を求めるための「ふるい」の処理が続く。
【００２８】
本願発明では、カットセット上の複数の「正当化ベクトル」をシミュレーションする。ここでは、一般的な「シミュレーション」、すなわち、常に出力側に向かう演算（前向き伝搬）だけではなく、入力側へ向かう演算（後向き伝搬）を組み合わせた含意操作（含意処理）が行われる。
【００２９】
そのため、まず、カットセット上に信号が割り当てられる。本願発明のシミュレーション、すなわち、含意操作では、カットセットから出力側へ向かう部分だけが処理の対象になるのではなく、カットセット上の信号の入力側も処理の対象になる。含意操作を行う場合、たとえば、カットセット上のある信号の値が１で、その信号のドライバがＡＮＤゲートであった場合、ＡＮＤゲートの全ての入力信号値は１でなければならない。その入力信号値が他のゲートのファンアウトしている場合、そのファンアウト先のゲートに対してもシミュレーションを行うことになる。
【００３０】
「含意結果ベクトル」とは、１回の含意操作を行った結果、回路中の信号上に現れる信号値をベクトル化したものを指す。たとえば、３つの正当化ベクトル１、２及び３に対して、（ｓ，ｔ，ｕ）＝（１，１，１），（１，１，１），（１，１，０）というベクトルが含意結果ベクトルとして求められる。
【００３１】
含意結果ベクトルが得られると、共通部分を定める。「共通部分を定め」とは、目標ゲートであるｓと同じ値を出力しているゲートｔを抽出することを意味する。各ベクトルの含意操作の後、目標ゲートと同じ値が割り当てられたゲートを選択する処理をベクトルの個数分だけ繰り返す。このとき、同じ値でなかったゲートを潜在的学習対象領域から除くことにより、繰返し後に残ったゲートが、潜在的学習対象領域を形成する。この段階で得られた領域は、まだ、潜在的な学習の対象領域であり、後続の判定段階において、正確なブール代数処理を行って、最終的な含意関係を導き出す。
【００３２】
尚、添付図面及び詳細な説明中、論理ネットワークを「トポロジー」と表現し、潜在的学習対象領域を「仮想学習領域」と表現し、正当化ベクトルを「正当ベクトル」と表現する場合がある。
【００３３】
本発明の好ましい実施例に従って論理設計を解析する処理は図３の（Ａ）に示されている。データ構造として記憶された論理設計論理ネットワーク３０は、図４に示したディジタル回路例のように、論理ゲートとその相互接続とにより構成されたディジタル回路の物理的論理設計を反映している。
【００３４】
論理ネットワークのデータ構造は図５に示されている。ゲート番号(GATE＿NUMBER)のフィールドは、論理ネットワーク内の論理ゲートに対する固有の番号を格納する。ゲート値(GATE＿VAL)のフィールドは上記論理ゲートに生じるブール代数値を格納する。ゲート名(GATE＿NAME)及びゲートタイプ(GATE＿TYPE)は、夫々論理ゲートの名前及びタイプを記憶する文字列を格納する。入力数(NO＿IN)及び出力数(NO＿OUT)のフィールドは、夫々、論理ゲートのファンイン(FAN＿IN)及びファンアウト(FAN＿OUT)に含まれる論理ゲートの数を格納する。レベル数(LEVEL＿NO)のフィールドは、レベルが０である外部入力に対し、論理ネットワーク内の論理ゲートが存在するレベルを識別する。ファンアウト及びファンインのフィールドは、夫々、現在の論理ゲートからファンアウトする論理ゲート、及び、現在の論理ゲートにファンインする論理ゲートを識別する番号の配列を格納する。
【００３５】
上記データ構造の使用法を示すため、例として図４の論理ゲート４７を考えてみよう。このゲートのゲート番号フィールドは３に一致する。ゲート値フィールドにはゲートの論理関数に依存する値が割り当てられる。論理ゲート４７は、ＮＯＲゲートであるので、ゲート値フィールドには４が割り当てられる。ゲート名フィールドは"オンリーＮＯＲ"に設定される。ゲートタイプフィールドは"ＮＯＲ"である。入力数及び出力数のフィールドは共に２である。更に、レベル数は２に一致する。配列ファンアウトフィールドは、ゲート４８及び４０のゲート番号を格納する。配列ファンインフィールドは、入力ＮＡＮＤゲートと外部入力信号のゲート番号を格納する。ゲート値フィールドは、ブール代数値０又は１が上記ゲートに割り当てられるまで−１のままである。次いで、ゲート値フィールドは、割り当てられた値をとる。
【００３６】
以下の説明において、未正当化ゲートだけが全ての論理設計解析で使用されるものとして考えられている。以下の説明を読むことにより、拡張された関数的含意として未正当化値以外の論理値を使用し得ることは当業者にとって明白である。特定の出力信号を生成するゲートに入力としてアサートされ得る信号の組合せが二つ以上ある場合、論理ゲートは正当化されない。テストパターンの自動発生中、解析されるべき未正当化ゲートは、論理ネットワーク内の少なくとも一つの論理ゲートにアサートされ、或いは、論理ゲートからアサートされた信号を伝送するワイヤ上にある点であるカット内の値の割当の現在の状況から常に検出される。カットは、完全に回路の内部にあってもよく、或いは、回路の外部入力又は外部出力の何れかと重なっていてもよい。検証中、各論理ゲートは未正当化ゲートである可能性があり、上記各ゲートの解析中、各所定のゲートを正当化させないようブール代数値が各所定のゲートに印加される。
【００３７】
図３の（Ａ）に示された処理は少なくとも二つの目標論理ゲートの選択（ブロック３１）から始まり、かかる目標論理ゲートは未正当化ゲートをなす。目標ゲートは回路内に既に存在するブール代数値の状況に基づいて決まる。例えば、ブール代数の値１がワイヤ４１にアサートされたとき、ＮＡＮＤゲート４０は正当化されていない。その理由は、ブール代数の値０がワイヤ４２と４３の何れか一方又は両方にアサートされた場合の結果として、得られるからである。特に、ブール代数の値０の出力信号を生成するためＮＡＮＤゲート４０に対する入力信号の組合せが二つ以上あるので、ＮＡＮＤゲート４０は正当化されていない。
【００３８】
未正当化ゲートのファンインは、この論理ゲートに印加された未正当化値に基づいて論理的関係を定めるため解析される（ブロック３２）。上記未正当化ゲートのファンインにある論理ゲートは、あらゆる正当値を回路内のあるカットセットに連続的に供給することによりシミュレーションされる。カットセットは、外部入力の方へ後向きにトレースした論理ネットワーク内で論理ネットワークの所定の構造的距離の範囲内にある目標論理ゲートのファンインに現れる全ての論理ゲートのセットにより構成される。カットセットの導出はブロック５５を参照して説明する。カットセット内の各ゲートに対し、ファンインとファンアウトにある論理ゲートに生じる直接論理的相互従属関係を調べるため直接前向き及び直接後向き含意が適用される（ブロック３３）。
【００３９】
例えば、ＮＡＮＤゲート４０がワイヤ４１にアサートされた出力信号として未正当化ブール代数値の１を有する場合、ＮＡＮＤゲート４０へのファンインは解析する必要がある。従って、ブール代数値の１がワイヤ４１にアサートされたとき、この値を検証するため、ワイヤ４２にアサートされ、ブール代数値の０である場合があるＮＯＲゲート４７からの出力、又は、ブール代数値の１である場合があるＮＡＮＤゲート３８の出力を解析する必要がある。ワイヤ４３のブール代数値０は、直接的な後向き含意に起因して、ブール代数値１をワイヤ４１にアサートする。ワイヤ４５上のブール代数値１は、直接前向き含意に起因して、ワイヤ４２にブール代数値０をアサートする。従って、ワイヤ４２上のブール代数値０は、ワイヤ４１上にブール代数値１を発生させるための必要条件である。直接前向き含意によって、ワイヤ４２上のブール代数値０によって、ＮＡＮＤゲート４８はワイヤ４９上にブール代数値１を生じさせる。従って、ワイヤ４９上のブール代数値１は、ワイヤ４１上にブール代数値１を発生させるための必要条件である。
【００４０】
上記ファンインの解析段階及びファンアウトの解析段階の２段階は、論理ゲートの真理値表と、上記ディジタル回路を構成する論理ゲートの連結性とに基づいて直接含意を得るため有用である。論理ゲートを二分決定図として表わすことにより、論理設計解析処理を完全化するため間接含意を得ることが可能になる（ブロック３４）。相互従属関係の判定（学習）は、二分決定図の正当化ベクトルの解析に基づいて回路内の信号割当のある状況下で実現可能であり、次いで、潜在的学習対象領域においてブール代数演算が行なわれる。
【００４１】
論理回路の区分化が不完全であり、かつ、上記区分を使用して論理設計検証が得られないときを判定する本発明の好ましい実施例による処理は、図３の（Ｂ）に示されている。直接及び間接含意によって学習された論理的相互従属関係は、図３の（Ａ）の処理に示されているように入力として使用される。複合回路は、ディジタル回路論理ネットワークの対の対応する出力を合成することにより作成される。カットは各々の回路内で作成され、カットと外部出力の間にある回路の区分だけが調べられる。従って、検証の必要部分は、各回路の上記区分は検証の目的に対し完全であることを保証することである。
【００４２】
本発明の好ましい一実施例に従って論理設計検証を行なう学習条件を使用する処理は、図３の（Ｃ）に示されている。論理的相互従属関係は学習され、複合論理回路内の区分の対の完全性は、上記の如く、図３の（Ｂ）に示した処理においてチェックされる。回路内の学習された論理的関係は、単一の二分決定図として併合され、与えられた回路のあらゆる解析を単純化するため使用される。例えば、上記併合は、各論理関係を表わす二分決定図の間でブール代数の論理積を同時にとることにより行なわれる。
【００４３】
好ましい一実施例によるコンピュータプログラム５０のフローチャートを図７に示す。最大学習レベルは、外部入力の方へ後向きにトレースする目標論理ゲートＧからの所定の構造的距離で定義される。論理ネットワークは、目標論理ゲートＧと最大学習レベルの間に生じる全ての新しい未正当化ゲートを検出するため、目標論理ゲートＧから解析され始め、検出された未正当化ゲートは候補セットＣuとして格納される（ブロック５３）。
【００４４】
新しい目標ゲートＴは候補セットＣuから選択される（ブロック５４）。目標ゲートＴは最初論理ゲートＧと同一であるが、候補セットＣuの各ゲートに変化する。例えば、論理ゲート４０は、図４に示されたディジタル回路の目標論理ゲートをなす。
【００４５】
カットセットλは目標ゲートＴに対し検出される（ブロック５５）。別々の繰り返し中に、別々のカットセットが検出される。好ましい一実施例において、カットセットλは、図４のカット３９のように、外部入力の方へ後向きにトレースすることにより目標ゲートから所定の構造的距離（カット距離）離れている論理ゲートの論理ネットワークを通るカットによって確定される。例えば、繰り返し１において、カット距離は１に一致する場合がある。外部入力がカット距離よりも短い構造的距離にあるとき、外部入力はカットセットの要素になる。目標ゲートのファンインの単純な論理ネットワーク駆動形のトレースによりカットセットが得られる。
【００４６】
カットセットλは目標ゲートＴの二分決定図を構築するため使用され（ブロック５６）、あらゆるタイプの決定図を使用することが可能である。例えば、カープラス(K. Karplus)の"マルチレベル最小化用のイフ−ゼン−エルス図の使用(Using If-Then-Else DAGs For Multi-Level Mininaization)"、ＶＬＳＩに関する１０周年カルテック会議(Decennial Caltech Conference on VLSI)（１９８９年５月）に示されているように、イフ−ゼン−エルス(if-then-else)図を使用してもよく、上記文献の内容を以下に引用する。説明のため、カット３９によって定義されたカットセットを使用する論理ゲート４０の二分決定図を図６の（Ａ）に示す。
【００４７】
各未正当化ゲートに対し、セットＰＬＡＲと呼ばれる潜在的学習対象領域がマークされる（ブロック５７）。上記マークは、最初に、カットセットλを使用する未正当化ゲートに対し構築された二分決定図から正当化ベクトルのセットを集めることにより行なわれる。正当化ベクトルの収集は以下のように行なわれる。
【００４８】
二分決定図の根頂点からのパスは、解析されている未正当化ワイヤの値と等しい値を有する端頂点までトレースされる。かかるパスは正当化ベクトルを構成する。例えば、カット３９によって定義されたカットを使用する論理ゲート４０の二分決定図の正当化ベクトルは図６の（Ａ）に示されている。
【００４９】
ｋ個の上記正当化ベクトルのセットが収集される。各正当化ベクトルはそのベクトルをカットに適用することによってシミュレーションされる。ｋ個の各正当化ベクトルの矛盾のないブール代数値を与える全ゲートの共通部分は、セットＰＬＡＲに集められる。上記ゲートのセットは潜在的学習対象領域を構成する。二分決定図の中の全ての可能な正当化ベクトルがシミュレーションされた場合、セットＰＬＡＲは真の学習点のセットをなす。
【００５０】
潜在的学習対象領域がマークされ、そのマークされた潜在的学習対象領域は真の学習領域ではないとき、潜在的学習対象領域内の各ゲートと目標ゲートＴの間の含意を判定する学習処理を開始し得る（ブロック５８）。上記学習処理には、図６の（Ｂ）に示した論理ゲート４７の二分決定図及び図６の（Ｃ）に示した論理ゲート３８の二分決定図のような潜在的学習対象領域内の各論理ゲートの二分決定図の構築と、図１５に示したようなブール代数演算の実行を含む。
【００５１】
学習処理は、潜在的学習対象領域の全ゲートが調べられるまで繰り返される（ブロック５９）。セットＣu内の未調査の全未正当化ゲートは集められ（ブロック６０）、新目標ゲートＴの選択と、カットセットλの検出と、二分決定図の構築と、潜在的学習対象領域のマークと、含意の学習の段階は、候補セットＣu が空集合になるまで繰り返される（ブロック６１）。含意検出の処理は、所定の最大学習レベルを超えるか、或いは、回路内の全ゲートが正当化されるまで繰り返される（ブロック６２）。最大学習レベルを超えなかった場合、未正当化ゲートがカット内に残っている限り、次の繰り返しの間、学習レベルは増加される（ブロック６３）。好ましい一実施例において、学習レベルは、物理的なレベル１と、物理的な距離（レベル）５に対応する学習レベル５の増分で増加される。
【００５２】
図８を参照するに、目標論理ゲートの中間的なファンイン内の未正当化ゲートを検出するためのルーチンが示されている（ブロック５３）。アブラモビッチ(M. Abramovici) 等の"ディジタル装置の試験と試験可能な設計(Digital Systems Testing and Testable Design)"、コンピュータサイエンスプレス（１９９０年）に記載されているように、縦優先探索は目標論理ゲートＧのファンインを通って後向きにトレースするため使用され、上記文献の内容を以下引用する。
【００５３】
セットＣuは未正当化ゲートだけを含む。未だ候補セットＣuに追加されていないがブール代数値を伝搬する論理ゲートは集められ、リストＬuに格納される（ブロック６７）。ブール代数値の０又は１と一致する出力値ｂを有するゲートＧはリストＬuから選択される（ブロック６８）。ゲートＧへの入力ワイヤは、ゲートＧの特定された値ｂに対し唯一の正当化ベクトルが存在し特定された値ｂがアサートされるかどうかを判定するため調べられる（ブロック６９）。ベクトルが検出された場合、そのベクトルは格納される（ブロック７０）。ベクトルが検出されなかった場合、未正当化ゲートＧはマークされ、リストＣu に追加される（ブロック７１）。ゲートＧがセットＣuに追加されなかった場合、ゲートＧへの入力は選択され（ブロック７６）、その入力がゲートの場合（ブロック７７）、このルーチンは、ゲートＧへの全入力ゲートが選択されるまで（ブロック７９）、上記入力ゲートを使用して縦優先形式で自分自身を再帰的に呼び出す（ブロック７８）。
【００５４】
図９を参照すると、カットセットλの検出用ルーチン（ブロック５５）が示されている。縦優先探索は、目標ゲートＴへの各入力に対し（ブロック８１）、目標ゲートＴのファンインを介して後向きにトレースするため使用される（ブロック８０）。このルーチンは、上記ゲートをカットセットλに格納し（ブロック８２）目標ゲートＴから現在の学習レベルまで物理的な距離をトレースバックするか、又は、外部入力に到達するまで（ブロック８３）、自分自身を再帰的に呼び出す（ブロック８４）。上記縦優先探索は、目標ゲートＴの全入力で再帰的に呼び出される（ブロック８５）。全ての縦優先探索の終了後、カットセットλ内のゲートにより、必要とされるカットセットが得られる。
【００５５】
図１０を参照するに、二分決定図を構築するルーチン（ブロック５６）が示されている。好ましい一実施例において、順序化された二分決定図が使用される。かくして、カットセットλの要素上の変数順序は、例えば、マリック(S. Malik)等の"論理合成環境の二分決定図を使用する論理検証(Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment)"、ICCAD(1988)、6-9 ページに記載されているように、縦優先探索要求ルーチンを用いて呼び出される（ブロック８６）。上記文献の内容は以下に引用されている。可変順序を用いることにより、カットセットλの二分決定図は構築され（ブロック８７）、そのサイズは縮小される（ブロック８８）。上記処理と組み合わされて、二分決定図を構築し、そのサイズを縮小するため適当な二つのアルゴリズムは、ブリアント(R.E. Bryant)の"ブール代数関数表現のグラフベースアルゴリズム(Graph Based Algorithms for Boolean Function Representation)"、ＩＥＥＥコンピュータ学会誌、C-35(1986 年8 月)、ページ677-690 に記載され、その内容を以下引用する。
【００５６】
図１１に示した内部データ構造は、一連の頂点レコードを構成する二分決定図の表現として維持される。ロー（ＬＯＷ）及びハイ（ＨＩＧＨ）フィールドは、子頂点を指示する。例えば、図６の（Ａ）において、０−エッジは頂点４４のＬＯＷフィールドである。０−エッジは、そのロー側の子供である頂点４５を示す。頂点４４及び４５は、図４の別のワイヤに対応する点に注意が必要である。インデックス（ＩＮＤＥＸ）フィールドは、根頂点から始まる頂点の構造的な深さを格納する。例えば、頂点４４のＩＮＤＥＸフィールドは１に等しく、頂点４５のＩＮＤＥＸフィールドは２に等しい。値（ＶＡＬ）フィールドは、０、１又はＸ（ドントケア条件）である。例えば、頂点４４のＨＩＧＨフィールドは、ＶＡＬフィールドが１と等しい端頂点を示す。あらゆる非端頂点のＶＡＬフィールドは、そのフィールドには実際的に値が含まれていないためドントケア条件が存在するので、常にＸである。識別（ＩＤ）フィールドは頂点を個別に特定する整数を格納する。マーク（ＭＡＲＫ）フィールドは、二分決定図をたどる間に調べられた頂点をマークする。
【００５７】
図１２及び１３を参照するに、ブール代数値ｖの潜在的学習対象領域をマークするルーチン（ブロック５７）が示されている。二分決定図は三つの部分で前処理され、これにより、所定のｋ個の正当化ベクトルが各正当化ワイヤに対し抽出される。図６の（Ｃ）において、論理ゲート３８は、ブール代数値の０と一致する出力に対し完全に正当化される。好ましい一実施例において、所定のｋはユーザにより与えられるが、経験的に値ｋ＝１００は十分であることが分かった。
【００５８】
正当化ベクトルは、二分決定図の根頂点から端頂点に進む。図６の（Ａ）、（Ｂ）及び（Ｃ）を参照するに、ＮＡＮＤ論理ゲート４０と、ＮＯＲ論理ゲート４７と、ＮＡＮＤ論理ゲート３８の正当化ベクトルが示されている。図６の（Ａ）には、ブール代数値１だけの正当化ベクトルがある。ブール代数値０は、１組の信号の割当（０，０）しかないので完全に正当化され、これにより、ブール代数の０は論理ゲート４０でアサートされる。図６の（Ｂ）において、論理ゲート４７はブール代数の１と等しい出力に対し完全に正当化されている。
【００５９】
図１４に示した内部データ構造は、二分決定図から得られた正当化ベクトルの表現として維持されている。リーフ二分決定図（ＬＥＡＦ＿ＢＤＤ）フィールドには、各正当化ベクトルの底の二分決定図を格納する。パス長さ（ＰＡＴＨ＿ＬＥＮＧＴＨ）フィールドは正当化ベクトルの節点の数を格納する。部分パス（ＰＡＲＴＩＡＬ＿ＰＡＴＨ）フィールドは、正当化ベクトルに沿って生じる分岐のブール代数値の配列を格納する。ボトムアウト（ＢＯＴＴＯＭ＿ＯＵＴ）フィールドは、正当化ベクトルが完全、又は、不完全の何れであるかを示すフラグを含む。
【００６０】
上記データ構造の使用の例を説明するため、頂点４４の０−分岐と、頂点４５の０−分岐とからなる図６の（Ａ）に示した二分決定図の正当化ベクトルの場合を考えてみよう。この正当化ベクトルは、論理ゲート４７の出力でブール代数の１を正当化する。ＬＥＡＦ＿ＢＤＤフィールドは、ブール代数の０を表わす二分決定図である。パスの長さは２に等しい。ＰＡＲＴＩＡＬ＿ＰＡＴＨフィールドは、頂点４４及び４５の整数識別子を格納する。両方の整数識別子は０−分岐が使用されていることを示すため必要である。ＢＯＴＴＯＭ＿ＯＵＴフィールドは、ブール代数の０の値を有する端頂点でパスが底に達することを示すため真に設定されるフラグである。
【００６１】
パート１において、正当化ベクトルは、根頂点から始まる二分決定図の横優先トレースを用いて抽出される。パート２の間、（非端頂点だけに対し得られた）ベクトルが不完全の場合、正当化ベクトルが完全化されるよう縦優先トレースが行なわれる。パート３において、回路は各正当化ベクトルに対しシミュレーションされ、全ての正当化ベクトルに対し矛盾の無い回路のブール代数値のセットが判定される。以下詳細に説明する。
【００６２】
パート１は最初に根頂点を選択する（ブロック９０）。二分決定図の現在レベル上の頂点が選択され（ブロック９１）と、１レベル下の頂点が選択される（ブロック９２）。選択された頂点がブール代数の０又はブール代数の１の何れかと等しい端頂点である場合（ブロック９３）、選択された頂点は目標ブール値ｖと比較される（ブロック９５）。値が一致し、かつ、所定のｋ個のパスは格納されていない、全ての二分決定図は調べられていない、或いは、二分決定図の全てのパスのセットが得られていない場合（ブロック９６）、正当化ベクトルはセットＰに格納される（ブロック９７）。これ以外の場合、頂点は非端頂点であり（ブロック９３）、かつ、所定のｋ個のパスは格納されていない、全ての二分決定図は調べられていない、或いは、二分決定図の全ての正当化ベクトルのセットが得られていない場合（ブロック９８）、不完全な正当化ベクトルは更なる処理のためセットＱに格納される（ブロック９９）。
【００６３】
１レベル下の頂点を選択し、端頂点であるかどうかを判定する段階は、１レベル下の全頂点が選択されるまで続けられる（ブロック１００）。同様に、二分決定図の現在のレベルにある頂点を選択する段階は、現在のレベルの全頂点が選択されるまで（ブロック１０１）、又は、ｋ個のパスが得られるまで（ブロック１１７）、或いは、他のパスが得られなくなるまで繰り返される。
【００６４】
パート２において、所定のｋ個のパスが得られたとき（ブロック１０３）、正当化ベクトルの抽出処理中に二分決定図全体が列挙された場合、指標が設定される（ブロック１１４）。二分決定図に含まれている全ての可能な正当化ベクトルが得られた場合、二分決定図は列挙される。上記例では、セットＰの全てのパスは完全である。
【００６５】
以下に説明するように、この例のシナリオの場合、セットＰの全てのベクトルのシミュレーションにより、学習条件のセットが得られる。或いは、パスは不完全な正当化ベクトルのセットＱから選択される（ブロック１０４）。二分決定図の縦優先トレースは、目標ブール代数値ｖに等しい正当化ベクトルを検出するため行なわれる（ブロック１０５）。検出されたベクトルはセットＱnewに格納される（ブロック１０６）。縦優先トレースは、セットＱの全てのパスが選択されるまで続けられる（ブロック１０７）。セットＰとセットＱの合併がとられ、セットＰに格納される（ブロック１０８）。
【００６６】
パート３において、各正当化ベクトルのファンインとファンアウトが直接含意を行なうためトレースされる。正当化ベクトルは選択され（ブロック１０９）、前向き及び後向き伝搬によって到達し得る全ての論理ゲートを評価するため、回路は論理ゲートの真理値表と、回路の物理的連結性を用いてシミュレーションされる（ブロック１１０）。検証アルゴリズムにおいて、選択された正当化ベクトルに対し予め格納された全てのブール代数値（含意）は、更に回路に印加される。
【００６７】
シミュレーションの終了時、含意結果ベクトルの共通部分が、この点までにシミュレーションされたあらゆる正当化ベクトルに対する全ての無矛盾の値の現在のベクトルを得るため選ばれる（ブロック１１１）。共通部分は新しい潜在的学習対象領域セットＰＬＡＲとして格納される（ブロック１１２）。パート３はセットＰの全ての正当化ベクトルがシミュレーションされるまで繰り返される（ブロック１１３）。
【００６８】
上記ルーチンの後処理部において、セットＰは二分決定図の全ての正当化ベクトルを含むことを示す指標が設定されたならば（ブロック１１５）、セットＰＬＡＲは真の学習領域を構成し（ブロック１１６）、セットＰＬＡＲの論理ゲートに対し以下に説明する二分決定図を使用するブール代数演算を実行する必要はない。
【００６９】
図１５を参照するに、潜在的学習対象領域の各ゲートと、目標論理ゲートの間の含意を学習するルーチン（ブロック５８）が示されている。この点までに上記方法によれば直接含意による論理的関係が定められる。図１５に示したルーチンは、ディジタル回路の論理ネットワーク内の論理ゲートの間に生じる更なる論理的関係を学習するため間接含意を行なう。
【００７０】
論理ゲートＨは潜在的学習対象領域から選択され（ブロック１２０）、二分決定図はカットセットλを用いて上記ゲートのため構築される（ブロック５５）。間接含意は、目標ゲートＴの二分決定図と、論理ゲートＨの二分決定図にブール代数演算を実行し、上記ブール代数演算の結果に基づいて論理的相互従属関係を判定することにより学習される。
【００７１】
好ましい一実施例において、目標ゲートＴの二分決定図とゲートＨの二分決定図に基づくブール代数のＡＮＤ（ブロック１２１）と、目標ゲートＴの二分決定図の補集合とゲートＨの二分決定図に基づくブール代数のＡＮＤ（ブロック１２６）が行なわれるが、ブール代数のＮＡＮＤと、ＯＲと、ＸＯＲと、それ以外の演算を含む他の単純又は複雑なブール代数演算を行なってもよい。ブール代数のＡＮＤ演算の可能な出力の中の二つは、ゲートＨの二分決定図（又はその補集合）と等しい（ブロック１２２及び１２７）、或いは、目標ゲートＴの二分決定図（又はその補集合）と等しい（ブロック１２４及び１２９）結果である。上記結果は、以下の表１に基づく対偶則を適用することにより間接含意の学習に使用することが可能である。間接含意の各セットは格納され（ブロック１２３、１２５、１２８及び１３０）、上記処理は潜在的学習対象領域の全ゲートが選択されるまで繰り返される（ブロック１３１）。
【００７２】
例えば、ゲートＴとゲートＨの二分決定図はＡＮＤされ、その結果はゲートＨの二分決定図と一致する場合を想定しよう。これは、ゲートＨがブール代数の１と一致するとき、目標ゲートＴもブール代数の１と一致することを意味する。対偶則を用いることにより、目標ゲートがブール代数の０と一致するとき、ゲートＨはブール代数の０と一致することを間接的に含意している。
【００７３】
【表１】
0003857961.tif 000002
上記説明は、例証の目的のため、一定の値が与えられた関係を計算（学習）することに集中している。上記処理は、一定の値が与えられた関係以外の関係がある二つの信号の間の関数的な従属性（関係）を計算するため使用してもよい。例えば、正当化されていないゲートＧと目標ゲートＴが与えられたとき、学習は行なわれないが小さい二分決定図Ｈが生成された場合、上記ゲートの二つの二分決定図のブール代数のＡＮＤを計算し、格納することが可能である。得られた二分決定図Ｈを一定の値が付与された学習処理内の目標二分決定図として用いることが可能であるが、一定の値が付与された学習ではなく、むしろ、"関数的に値を付与された"学習が得られる。二分決定図Ｈのブール代数の０又は１の値は一定のブール代数値を有するディジタル回路内の単一の論理ゲートに必ずしも常に対応するとは限らないので、上記学習は関数的に値を付与される。より複雑なブール代数演算に加えて、ブール代数のＡＮＤ以外の他の演算を関数的に値を付与された関係の学習の更なる処理に容易に使用することができる。
【００７４】
ＩＩ．  論理的相互従属関係のある論理ゲートのグループを使用する論理設計検証
図１の装置で使用されるような論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証用のコンピュータ支援論理設計装置及び方法のブロック図を図１６に示す。コンピュータプログラム７は６個の主要な構成部（ブロック１７９，１８０，１８５，１８６，１８７及び１９７）からなり、他の構成部を統合するための主制御部１７９を含む。２次記憶装置１は、１４個のファイル（ブロック１８１，１８２，１８３，１８４，１８８，１８９，１９０，１９１，１９２，１９４，１９５，１９６，１９８及び１９９）を格納する。含意学習部１８０は、ディジタル回路の対の論理設計論理ネットワークファイル１８１及び１８２を読み込むため使用される。含意学習部１８０は、図２に示したような学習プログラムを構成するが、一つの回路だけではなく、含意ファイル１８３及び１８４の対に二つのディジタル回路の含意を格納する。
【００７５】
複合回路作成部１８５は、排他的論理和（ＸＯＲ）論理ゲートを介して外部出力で接合された二つの論理ネットワークを構成する複合回路ファイル１８８を生成するため使用される。第１回路部１８６のカットセットと第２回路部１８７のカットセットは、共に夫々の回路のカットセットと、もう一方の回路の反射カットセットとを発生する。複数の中間データファイルＩＰ’１９０、ＣＰ１  １９１、ＣＰ２  １９２、Ｔcut １９４、Ｔcomplete  １９５、及びＰＣ  １９６が作成される。その上、含意選択ファイル１８９は中間結果を格納するため使用される。
【００７６】
完全なカットセットが検出されなかった場合、カットセットホール充填部１９７は、完全なカットを生成するため中間データファイルＣＰ２  １９２と、ＩＰ’１９０とを読み込む。カットセットホール充填部１９７は、更に、中間データファイル１９８及び１９９を作成し、回路が検証されたかどうかの判定をディスプレイ２００及びプリンタ２０１に出力し、結果ファイル２０２に格納する。
【００７７】
論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証のプログラム２１０の好ましい一実施例のフローチャートを図１７及び１８に示す。プログラム２１０は二つのフェーズで動作する。フェーズＩは、図７に示したコンピュータプログラムを使用して、論理的相互従属関係（含意）の学習によって検証される各回路の論理設計を解析する（ブロック２１１）。
【００７８】
論理的相互従属関係（含意）は、一方の変数がある特定のブール代数の値であるならば、もう一方の変数は強制的に別の特定のブール代数の値になるような二つのブール代数の変数の間の関係である。例えば、もう一度図４を参照すると、論理ゲート４８に対する論理的相互従属関係が論理ゲート４０に存在するならば、ブール代数の値１がワイヤ４１にアサートされている限り、ブール代数の値１がワイヤ４９にアサートされる。フェーズＩで使用されるデータ構造は図１９及び２０に示されている。
【００７９】
図１９の（Ａ）を参照すると、論理的相互従属関係の仮のリストを格納するリンクしたリストデータ構造が示されている。フェーズＩの進行中、論理的相互従属関係が幾つ得られるかは予め分からない。従って、各論理的相互従属関係が検出される毎に、検出された論理的相互従属関係は動的なリンクドリストデータ構造に追加される。ゲート番号（ＧＡＴＥ＿ＮＵＭＢＥＲ）フィールドは、論理的相互従属関係が得られた論理ゲート番号を格納する。ゲート値（ＧＡＴＥ＿ＶＡＬ）フィールドは、論理的相互従属関係のブール代数値を示す。最後に、次の学習リンクドリスト（ＮＥＸＴ＿ＬＥＡＲＮＩＮＧ＿ＬＩＮＫＥＤ＿ＬＩＳＴ）フィールドは、リンクドリストの次の要素へのポインタを格納する。リングドリストの最後の要素は接地され、ＮＥＸＴ＿ＬＥＡＲＮＩＮＧ＿ＬＩＮＫＥＤ＿ＬＩＳＴフィールドには値ヌルが入る。リンクドリストデータ構造は、論理的相互従属関係が検出された各ブール代数値に対する論理ネットワーク内の各ワイヤに割り当てられる。
【００８０】
図１９の（Ｂ）を参照するに、リンクドリストデータ構造の一例を示す図が示されている。第１の要素７２は、論理的相互従属関係を表わす。論理ゲート１のブール代数の値１と一致する論理的相互従属関係を表わす。第１の要素７２は論理ゲート２のブール代数の値０と一致する論理的相互従属関係を表わす第２のリストの要素７３を示す。要素７３はリンクドリストの最後の要素であり、ヌル値を指し示す。
【００８１】
図２０の（Ａ）を参照するに、フェーズＩ中に論理ゲートのあるレベルの終了時に論理的相互従属関係を格納及び収集するデータ構造が示されている。各学習レベルの全ての論理的相互従属関係が検出された後、等価リスト（ＥＱ＿ＬＩＳＴ）と、反転リスト（ＩＮＶ＿ＬＩＳＴ）と、リスト０（ＬＩＳＴ＿０）と、リスト１（ＬＩＳＴ＿１）の四つのリストが作成される。ＥＱ＿ＬＩＳＴは、リストが割り当てられたゲートと関数的に等価な論理ゲートのリストを収容する。同様に、ＩＮＶ＿ＬＩＳＴは、リストが割り当てられたゲートと関数的に反転した論理ゲートのリストを収容する。ＬＩＳＴ＿０及びＬＩＳＴ＿１は、リストが割り当てられたゲートに夫々ブール代数の値０又は１が印加されたときいつも論理的相互従属関係を有する論理ゲートのリストを収容する。
【００８２】
上記四つのリストのデータ構造は図２０の（Ａ）に示されている。長さ（ＬＥＮＧＴＨ）のフィールドは学習リストの長さ、即ち、論理的相互従属関係のリスト内の論理ゲートの数を格納する。学習（ＬＥＡＲＮＩＮＧ）フィールドは、ゲートの論理的相互従属関係を格納する整数型配列へのメモリアドレスポインタを格納する。上記整数型の値は正又は負の何れかのゲート番号である。正のゲート番号はブール代数の値１が目標ゲートで得られたことを示し、負のゲート番号はブール代数の値０が目標ゲートで得られたことを示す。
【００８３】
図２０の（Ｂ）は、ゲートｋに対する論理的相互従属関係のセットの一例を示す概略図である。ＥＱ＿ＬＩＳＴリストには、ゲートｋと関数的に一致する４個のゲート：５，８，−１０及び１２が記載されている。同様に、ＩＮＶ＿ＬＩＳＴはゲートｋと関数的に逆の４個のゲート：１，−２，７及び１１が記載されている。ＬＩＳＴ＿０は、ブール代数の値０に対する論理的相互従属関係が分かっている３個のゲート：３，１５及び２０が記載されている。最後に、ＬＩＳＴ＿１は、ブール代数の値１に対する論理的相互従属関係が分かっている５個のゲート：４，６，９，１３及び１５が掲載されている。
【００８４】
フェーズＩＩは回路の対を検証する。そのゴールは、外部出力と、各回路のサブセットを構成する論理ゲートのセットの間にある区分の対を使用して等価性を証明することである。
【００８５】
図１７及び１８を再度参照するに、上記二つの回路の各々からの外部出力を合わせ、その外部出力を単独のＸＯＲ論理ゲートに接続することにより複合回路が作成される（ブロック２１２）。従って、組み合わされる出力信号の間のあらゆる不一致は、ＸＯＲ論理ゲートの出力に反射される。
【００８６】
図４４は複合ディジタル回路の論理ネットワークを例証する論理設計の概略図である。複合回路は第１及び第２の別個のディジタル回路の論理ネットワーク４７０及び４７１からなり、各論理ネットワークは、外部出力４７２及び４７３と、外部入力４７４及び４７５のセットを構成する。外部出力は、ワイヤ４７８及び４７９によって相互接続された論理ゲート４７６及び４７７と相互接続される。別個の論理ネットワークの一方の外部出力４９０は、別個の論理ネットワークのもう一方に対応する外部出力を有する。別個の各論理ネットワークからの対応する外部出力は、二つの論理ネットワーク間の等価性を示すワイヤ４８１上の出力信号をアサートする排他的論理和（ＸＯＲ）論理ゲート４８０を使用して排他的論理和される。図４４には排他的論理和論理ゲートが示されているが、ゲートをシミュレーションすることが可能であり、これにより、対応する出力は、ソフトウェアを用いてコンピュータ支援設計装置によって論理的に排他的論理和がなされる。同様に、複合回路は同じ手段によってシミュレーションが行なわれる。
【００８７】
等価性は内部カットと外部出力の対の間にある区分の対を構成する二つの回路の論理ネットワークの一部分だけを調べることにより検証することができる。しかし、かかる回路は一般的に完全であることが必要とされる。カット内の全ての点が同一回路、又は、別の回路のカットの上又は前方に含意点を有するならば、そのカットは完全であると呼ばれる。カットの上又は前方の他のあらゆる論理ゲートに対し含意のないカット上の論理ゲートが存在するならば、一般的に外部出力とカットの間に含まれる回路の一部分だけを調べることにより二つの回路を検証することは不可能である。
【００８８】
従って、各回路に対し仮のカット選択領域ＩＰが検出され、反射的な仮のカット選択領域ＩＰ’は他の回路で検出される（ブロック２１３及び２１７）。上記各仮のカット選択領域ＩＰは、各回路を通る仮のカットと、その回路の外部出力の間に含まれる論理ゲートのセットを構成する。図４４には仮のカット選択領域ＩＰの一例が示され、仮のカット４８２は、論理ゲート４８３、４８４及び４８５からなる仮のカット選択領域ＩＰを確定する。上記仮のカット選択領域は回路の一部分に対応し、ディジタル回路の検証を行なう際に相当性が評価される。各反射的な仮のカット選択領域ＩＰ’は、他の回路内に生じる論理ゲートのセットからなり、仮のカット選択領域ＩＰ内の各含意点はもう一方の回路の対応する含意点に写像される。この写像された点のセットは反射領域ＩＰ’と呼ばれる。反射領域ＩＰ’の一例は図４４に示され、仮のカット４８２は、論理ゲート４８６、４８７、４８８及び４８９からなる反射領域ＩＰ’を確定する。
【００８９】
仮のカット選択領域ＩＰと、反射的な仮のカット選択領域ＩＰ’の両方に対し、二つの回路の一部分を形成する完全なカットを潜在的に構成し得る論理ゲートの点を通るカットが存在する。回路１と回路２の両方は、もう一方の回路に写像する反射的な仮のカット選択領域ＩＰ’を夫々伴う仮のカット選択領域ＩＰを作成するため別個に解析される（回路１の場合のブロック２１４及び回路２の場合のブロック２１８）。かくして、検証を行なうため必要とされる計算資源の量を最小限に抑えるよう最適カット、即ち、より小さいサイズの区分が検出される。夫々の仮のカット選択領域ＩＰと反射的な仮のカット選択領域ＩＰ’とに基づく回路１及び２を通る個々のカットの対は、夫々、回路１及び２の完全なカットλ1 及びλ2 と呼ばれる。何れか一方が完全なカットではない場合（ブロック２１５及び２１９）、そのカットは夫々不完全なカットλ1-incomplete及びλ2-incompleteと呼ばれ、かかる不完全なカットを完全化するため必要とされる論理ゲートが判定される（ブロック２１６及び２２０）。
【００９０】
回路１及び２の各々を通る完全なカットは仮のカット選択領域ＩＰと反射的なカット選択領域ＩＰ’を使用して試行され、上記カットの対は、夫々、カットα及びα’のように名前を付けられる（ブロック２１４及び２１８）。
【００９１】
完全なカットλ1及びλ2が両方の回路１及び２に対し検出されたならば（ブロック２２１）、上記カットのサイズは比較される（ブロック２２２）。カットセットのサイズはゲートの個数に関して定められる。カットセットのホールは、カットの上又は前方でもう一方の回路内に含意のないカットセットのゲートがあることを意味する。カットセットλ1 の方が小さい場合、カットセットλ1が完全なカットと呼ばれる（ブロック２２３）。カットセットλ2の方が小さい場合、カットセットλ2が完全なカットと呼ばれる（ブロック２２４）。カットλ1だけが完全な場合（ブロック２２５）、カットλ1は回路のカットと呼ばれる（ブロック２２３）。一方、カットλ2だけが完全な場合、カットλ2は回路のカットと呼ばれる（ブロック２２４）。
【００９２】
カットセットの完全性のテストの実行後、カットλ1又はλ2を構成する各ゲートのワイヤにブール代数の値を印加することにより、論理ネットワークは検証される（ブロック２２７）。出力信号は論理ネットワーク間の等価性を示すためＸＯＲ論理ゲートからアサートされる。出力信号がブール代数の値０と一致する場合、回路は等価であることが検証される。
【００９３】
図２１を参照すると、外部出力から始めてカットセットαを検出するルーチンのフローチャートが示されている。上記ルーチンは、区分を形成する含意点のセットを選択するため出力ゲートのファンインを介して後向きにトレースする。目標回路の中の何処かにある出力ゲートＧは選択され（ブロック２３０）、ゲートＧが先に選択されている場合（ブロック２３１）、ルーチンは終了する。
【００９４】
ゲートＧのファンインは外部入力の方へ後向きにトレースされるので、ゲートＧの直接の入力にあるゲートＪが選択される（ブロック２３２）。ゲートＪが先に選択されていない場合（ブロック２３３）、ゲートＪの格納された学習含意点のセットは、ゲートＪに対し現在の回路又は他の回路に含意点が存在するかどうかを判定するため調べられる（ブロック２３４）。かかる含意点が同一回路内に存在する場合、解析されている回路のゲートＪと共に仮のカット選択領域に格納され、他の回路内のあらゆる含意点は他の回路の反射的な仮のカット選択領域ＩＰ’に格納される（ブロック２３５）。上記含意点が存在しない場合、この処理はゲートＪを用いて自分自身を再帰的に呼び出す（ブロック２３６）。上記処理はゲートＧへの全ての直接の入力が選択されるまで繰り返される（ブロック２３７）。
【００９５】
図２２を参照すると、仮のカット選択領域ＩＰと反射的な仮のカット選択領域ＩＰ’を格納するデータ構造が示されている。このデータ構造は、仮のカットを構成する論理ゲート番号の整数型配列からなる。上記配列の最大サイズは、前処理コマンドを用いて最大の配列次元を設定するカットサイズマクロによって決められる。
【００９６】
図２３及び２４には、反射的なカットセットαを検出するルーチンが示されている。このルーチンの目的は、第１の回路の区分に関数的に対応する区分を第２の回路に作成することである。
【００９７】
上記ルーチンの第１の部分の間、所定の外部出力からは辿ることができるが、反射的な仮のカット選択領域ＩＰ’のゲートからは辿ることができない第２の回路の全ての論理ゲートがマークされる（ブロック２４０）。
【００９８】
反射的な仮のカット選択領域ＩＰ’には、第１の回路に適合している出力ゲートを有する第２の回路内の所定の出力ゲートの格納された論理的相互従属関係（学習含意点）が含まれることに注意が必要である。上記格納された相互従属関係は、予め経験的、又は、論理的に含意され、図２０の（Ａ）及び（Ｂ）に示したデータ構造を使用して含意ファイル１８３及び１８４に格納される。かくして、たとえ、上記関係は検証される二つの回路の独立性に起因して直接的に含意されなくても、第１の回路の論理ゲートは上記格納された論理的相互従属関係の中の一つを用いて第２の回路に反射される。
【００９９】
反射的なカット選択領域ＩＰ’は完全なカットである場合（ブロック２４１）、第１の回路の論理ゲートはその外部出力から後向きにトレースすることにより解析される。ゲートＧが選択され（ブロック２５７）、後戻りトレース処理は第２の回路の反射的な仮のカット選択領域ＩＰ’の点に写像する第１の回路の全ゲートを識別するため呼び出される（ブロック２５８）。この処理は外部出力の全部が選択されるまで繰り返される（ブロック２５９）。
【０１００】
反射的な仮のカット選択領域ＩＰ’が完全なカットを構成しない場合、反射的な仮のカット選択領域ＩＰ’内の論理ゲートによって到達し得ないゲートは候補点としてセットＣＰ１に格納される（ブロック２４２）。同様に、反射的な仮のカット選択領域ＩＰ’のカットα’の上又は前方の何れかに含意点を有し、第２の回路に対し学習された含意のセット内の全ゲートは、マークされ（ブロック２４３）、候補点としてセットＣＰ２に格納される（ブロック２４５）。
【０１０１】
上記ルーチンの第２の部分の間、第２の回路の各出力ゲートのファンインは、ＣＰ２内の何れのゲートがＣＰ１内の全てのゲートに対しカットセットを形成し得るかを判定するため再帰的に解析される。ゲートＫはある出力ゲートＧに対し選択され（ブロック２４８）、ゲートＫの再帰的な処理が呼び出される（ブロック２４９）。出力ゲートＧの全入力が選択されるまで、処理は繰り返し的に呼び出される（ブロック２５０）。
【０１０２】
出力ゲートＧで開始された再帰的探索は、ＣＰ１とＣＰ２にあるゲートが検出されたとき停止される。かかるゲートは配列Ｔcutに格納される。探索処理の終了時、配列Ｔcutの要素は反射的な仮のカット選択領域ＩＰ’に追加される（ブロック２５１）。
【０１０３】
上記探索処理が外部入力に達したとき、カットは不完全である。上記探索処理が外部入力に達しなかったとき、完全なカットセットが検出される（ブロック２５２）。無関係なゲートは、Ｔcutに追加されたとき、必要とされるカットを与える反射的なカット選択領域ＩＰ’から削除される（ブロック２５３）。上記カットセットは、縦優先探索によって外部出力の最も近くにあるゲートの境界を定めることにより配置される。次いで、処理（ブロック２５５）は、上記と同様に、ファンインの全入力ゲートが解析されるまで（ブロック２５６）、各出力ゲートＧの入力を再帰的に解析する（ブロック２５４）。
【０１０４】
図２５にはカットセットのホールを充填するルーチンのフローチャートが示されている。このルーチンは、回路の区分のギャップを繋ぐためフェーズＩの間に格納された論理的相互従属関係（学習された含意点）のセットを探索することによりカットを作成することを意図している。ギャップを繋ぐため、学習された含意のセットに追加されたとき、場合によっては小さいカットセットを得る助けになる幾つかのゲートを（たとえ、格納された含意がなくても）探す。
【０１０５】
上記ルーチンの第１の部分の間に、ゲートＫはセットαから選択され（ブロック２６０）、ゲートＫが既に調べられていた場合（ブロック２６１）、このルーチンは終了する。或いは、ゲートＫが候補点ＣＰ１のセットから到達できないとき（ブロック２６２）、このルーチンは終了する。ゲートＫが候補セットＣＰ１と候補セットＣＰ２にあるとき（ブロック２６３）、ゲートＫは配列Ｔcutに追加され（ブロック２６４）、ルーチンは終了する。或いは、ゲートＫは外部入力である場合（ブロック２６５）、完全なカットを検出し得ず（ブロック２６６）、このルーチンは終了する。それ以外の場合、ゲートＫの入力ゲートＩは選択され（ブロック２６７）、ゲートＫの全入力ゲートが選択されるまで（ブロック２６９）、上記処理は再帰的に自分自身を呼び出す（ブロック２６８）。
【０１０６】
図２６には、反射的な仮のカット選択領域ＩＰ’に含まれるかどうかを判定するため論理ゲートのファンインを介して後向きにトレースするルーチンが示されている。回路にあるゲートＬに対し（ブロック２８０）、入力ゲートＭが選択される（ブロック２８１）。入力ゲートＭが先に調べられている場合（ブロック２８６）、その入力ゲートは飛ばされ、別のゲートが選択される。或いは、ゲートＭが反射的な仮のカット選択領域ＩＰ’にある場合（ブロック２８２）、ゲートＭはセットＴcompleteに格納される（ブロック２８３）。ゲートＭが反射的な仮のカット選択領域ＩＰ’に含まれない場合、処理はゲートＭを用いて自分自身を再帰的に呼び出す（ブロック２８４）。上記処理は所定のゲートＬに対する全入力ゲートが選択されるまで繰り返される（ブロック２８５）。
【０１０７】
図２７には、カットセットΘが完全かどうか、即ち、セットΘのゲートを除いて外部出力から到達可能な入力が回路内に存在しないかどうかを決定するルーチンが示されている。この処理は、配列Θに格納された所定の部分カットセットが完全なカットセットであるか、或いは、ホールを有するかを判定する。配列Θは回路内のゲートの領域を表わし、図２７のルーチンは所定の領域によって回路内のすべての入力が出力ゲートに到達するのを阻止されるかどうかを判定する。
【０１０８】
ゲートＧは部分カットセットから選択される（ブロック２９０）。そのファンアウトとファンインは、夫々、前向き及び後向き伝搬を用いて回路の論理ネットワークの中をトレースされ（ファンアウトの場合のブロック２９１と、ファンインの場合のブロック２９２）、"＊"でマークされる。かかる選択及びマーキング処理は、ゲートＧへの全入力が選択されるまで（ブロック２９５）、自分自身への再帰呼出しを用いて（ブロック２９４）、ゲートＧのあらゆる入力ゲートＺに対し繰り返される（ブロック２９３）。回路の全ゲートが"＊"でマークされた場合、カットセットは完全である。
【０１０９】
図２８には、論理的相互従属関係のセット内の論理ゲートをマークするルーチンが示されている。ゲートは論理的相互従属関係（学習された含意）のセットから選択され（ブロック３００）、そのゲートの含意点が選択され、マークされる（ブロック３０１）。この処理は全ての含意点が選択されるまで繰り返され（ブロック３０４）、論理的相互従属関係のある全含意点が選択される（ブロック３０５）。
【０１１０】
図２９には、不完全なカットを完全化するため必要とされる論理的ゲートを定めるルーチンが示されている。部分カットセットαのホール（ブロック３１０）及びα’（ブロック３１３）は埋められる。同様に、反射的な仮のカット選択領域ＩＰ’のホール（ブロック３１１）及びＩＰ（ブロック３１４）のホールは埋められる。回路１の場合、完全なカットは、部分カットセットαと、反射的な仮のカット選択領域ＩＰ’とにより構成されることに注意が必要である。同様に、カット２の場合、完全なカットは、部分カットセットα’と、仮のカット選択領域ＩＰとにより構成される。従って、上記二つのカットセットの合併集合が計算され、回路１及び回路２の完全なカットセットとして、夫々、カットセットλ1 及びカットセットλ2 に格納される（カットセットλ1 に対しブロック３１２及びカットセットλ2 に対しブロック３１５）。
【０１１１】
図３０の（Ａ）には、カットセットλ1 及びλ2 を格納するデータ構造が示されている。ゲート番号（ＧＡＴＥ＿ＮＵＭＢＥＲ）フィールドは、回路内の各論理ゲートを識別する固有の数字を格納する。等価フラグ（ＥＱ＿ＦＬＡＧ）と、反転フラグ（ＩＮＶ＿ＦＬＡＧ）と、両方フラグ（ＢＯＴＨ＿ＦＬＡＧ）のフィールドには、夫々、与えられた論理ゲートが、当該回路又はもう一方の回路に等価論理ゲート、反転論理ゲート、或いは、論理的相互従属関係を有するかどうかを示すフラグが含まれている。等価ゲート、反転ゲート、及び論理的相互従属関係は、与えられた論理ゲートの各々の学習リストに格納されることに注意が必要である。０フラグ（０＿ＦＬＡＧ）及び１フラグ（１＿ＦＬＡＧ）フィールドには、夫々、ブール代数の０又はブール代数の１の値が上記ゲートに印加されたならば、与えられたゲートは論理的相互従属関係を有することを示すフラグが格納されている。最後に、完全性フラグ（ＣＯＭＰＬＥＴＥ＿ＦＬＡＧ）は、カットが完全であるかどうかを示す。
【０１１２】
図３０の（Ｂ）は、カットα1及びカットα2を格納するデータ構造が示されている。このデータ構造は同図の（Ａ）に示したようなデータ構造の配列により構成される。上記配列の最大サイズは、前処理コマンドを使用して最大配列次元を定めるカットサイズマクロによって定義される。
【０１１３】
図３１には、部分カット内の論理ゲートをトレースし、マークするルーチンが示されている。部分カットＰＣ内の各ゲートの前向きコーン（ブロック３２０）と後向きコーン（ブロック３２１）は、各論理ゲートの中間的なファンアウトとファンインをたどることによってトレースされ、マークされ、到達した各ゲートはＴＥＭＰ＿Ｄとしてマークされる。上記ルーチンの第２の部分において、外部出力ゲートＰは選択され、部分カットＰＣ内のホールからなるギャップをつなぐかどうかを定めるため解析される（ブロック３２２）。
【０１１４】
図３２には、論理的相互従属関係のセット内の論理ゲートの間のギャップをつなぐ論理ゲートを探すルーチンが示されている。上記論理ゲートは図示しない。当該ゲートＰの入力ゲートＧは選択される（ブロック３３０）。ゲートＧは先に調べられていない場合（ブロック３３１）、かつ、前のルーチンでＴＥＭＰ＿Ｄとしてマークされなかった場合（ブロック３３２）、ゲートＧは、部分カットＰＣのギャップ内の論理的ゲートのセットからなるホールセットに格納される（ブロック３３３）。
【０１１５】
ゲートＧはＴＥＭＰ＿Ｄとしてマークされ、部分カットセットＰＣにあるならば（ブロック３３４）、ゲートＧはギャップにあると考えられるので、更に解析を行なう必要はない。それ以外の場合、この処理はゲートＧを用いて自分自身を再帰的に呼出し（ブロック３３５）、当該ゲートＰに対する全入力が選択されるまで繰り返される（ブロック３３６）。
【０１１６】
図３３には、先にマークされた論理ゲートのトレース、収集及びマーキングルーチンが示されている。このルーチンは、あるゲートＧが先に調べられていない場合（ブロック４１１）、そのゲートＧに基づいて動作する（ブロック４１０）。ゲートＧは先に調べられず、"＊"でマークされている場合（ブロック４１２）、ゲートＧは飛び越される。それ以外の場合、ゲートＧは"＃"でマークされ、配列Ｔ１に格納される（ブロック４１３）。ゲートＧが外部入力の場合（ブロック４１４）、ゲートＧの更なる解析は要求されず、このルーチンは終了する。ゲートＧは外部入力ではない場合、ゲートＧの入力ゲートＨが選択され（ブロック４１５）、上記ルーチンは、ゲートＧの全入力ゲートが選択されるまで（ブロック４１７）、ゲートＨを入力として使用して自分自身を再帰的に呼び出す（ブロック４１６）。
【０１１７】
ＩＩＩ．  二分決定図の単純化を用いる論理設計検証
図１の装置で使用されるような二分決定図の単純化を用いる論理設計検証用のコンピュータ支援設計装置及び方法のブロック図を図３４に示す。上記装置及び方法のゴールは、二分決定図ベースの処理において、二分決定図だけを使用する検証の利点を損なうことなく、ディジタル回路の対を検証するため関数的学習を使用することである。
【０１１８】
検証されている二つの回路を表わす二分決定図が大規模かつ複雑な場合、二つの回路の検証は困難化する。二つの回路が構造的に類似しているとき、関数的学習により二つの回路の対応する外部出力の等価性が非常に頻繁に発見されるので、検証は関数的学習だけを用いて実行し得る。
【０１１９】
目標ワイヤの入力コーン（中間的なファンイン）に含まれているブール代数表現の二分決定図表示が二分決定図ベースの検証に大き過ぎるとき、関数的学習は二分決定図のサイズを縮小するため使用される。関数的学習は、疑似入力変数のセットを選択し、二つの回路の対応する出力関数を表わす二つの二分決定図のＸＯＲ（複合）二分決定図を構築するため論理的相互従属関係を用いることによって検証を高速化するため使用される。論理的相互従属関係（含意）は、ＸＯＲ二分決定図のグラフサイズを更に縮小するためカットの変数の"ドントケア"の組合せ、即ち、二つの所定の回路に存在しないカット変数のブール代数の組合せの検出に更に利用される。
【０１２０】
コンピュータプログラム７は、他の部品を統括する主制御部３５５を含む６個の主要部（ブロック３４２，３４５，３４７，３４９，３５１，３５３及び３５５）からなる。２次記憶装置１は、８個のファイル（ブロック３４０，３４１，３４３，３４４，３４６，３４８，３５０及び３５４）を格納する。含意学習部３４２はディジタル回路の対の論理設計論理ネットワークファイル３４０及び３４１を読み込み、そのファイルの中の間接含意を学習するため使用される。含意学習部３４２は図７に示したコンピュータプログラムよりなるが、しかし、一つの回路だけではなく、含意ファイル３４３及び３４４の対として二つのディジタル回路の間接含意を格納する。
【０１２１】
区分完全性チェック部３４５は、カットセットを作成し、検証される各回路のカットセットが完全な区分であるかどうかをチェックするため使用される。区分完全性チェック部３４５は、二分決定図３４８を構築するため二分決定図構築部３４７により使用される完全なカットセット３４６の対を発生する。区分完全性チェック部３４５は、ブロック３６３に示したように、図１７及び１８に示した論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証プログラム２１０からのルーチンにより構成される。学習条件計算部３４９は、二分決定図のサイズを縮小、単純化する単純化部３５３によって使用される学習条件３５０のセットを作成する。学習条件の使用の他に、格納された論理的相互従属関係（間接含意）は、二分決定図のサイズを更に縮小するため共通因子計算部３５１により使用される。
【０１２２】
従って、目標ワイヤ自体を含む目標ワイヤのコーン内の全てのワイヤに対する二分決定図３５４が構築される。ある中間カットで得られた疑似変数に対して構築された目標コーンの二分決定図はＧdと呼ばれる。次に、学習条件３５０は、目標ワイヤの入力中と、カットの前方で種々の二分決定図を適切に併合することにより得られる。上記学習条件は、単純化部３５３において、Ｇd のサイズを縮小し単純化するため、次々にＧdと論理和される。上記条件は、本質的に、カットの前方の関数の可制御性の"ドントケア"セットからなる。
【０１２３】
Ｇd のサイズの単純化の終了時、結果はディスプレイ３５６及びプリンタ３５７でユーザに表示され、結果ファイル３５８に格納される。
【０１２４】
二分決定図単純化プログラムを用いた論理設計検証の好ましい一実施例を図３５及び３６に示す。このプログラムは三つのフェーズで動作する。フェーズＩは、図７に示したコンピュータプログラムを用いて、検証すべき各回路の論理設計を学習された論理的相互従属関係（含意）によって解析する（ブロック３６１）。
【０１２５】
次に、複合回路は、二つの回路の各々からの外部出力を合わせ、各対をＸＯＲ論理ゲートに供給することにより作成される（ブロック３６２）。かくして、適合する出力信号の間の不一致は、ＸＯＲゲートの出力に反射される。二つの対応する外部出力が関数的に異なる場合、二つの回路の外部入力に供給されたとき、ＸＯＲ論理ゲートの出力にブール代数の値１を生成し、これにより、検証される二つの回路の間の等価性の欠如を示す少なくとも一つのブール代数値の組合せがある。  フェーズＩＩにおいて、ブロック３６３に示したように、図１７及び１８に示した論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証プログラムからの区分完全性チェックルーチンを用いて、回路区分が完全であるかどうかの判定が行なわれる（ブロック３６３）。
【０１２６】
プログラムの残りの部分はフェーズＩＩＩを構成する。全体的なゴールは、検証される両方の回路の併合された区分の差の関数を表わす複合二分決定図（ＸＯＲ二分決定図）を繰り返し単純化することである。
【０１２７】
従って、各回路の区分を構成するカットセットは学習条件と共に使用するのに適することが必要である。適当なカットセットは、カットセットが有するホールの数が非常に少ないという特質を満足する。示唆されるホールの個数の割合は、カットセットにある含意点の個数の３分の１以下である。所定の回路の対を検証するため利用可能な計算資源に依存してこれ以外の割合を同様に試すことができる。ホールは、カットの上又は前方にある別の点に対し含意点のない回路内の点であることに注意が必要である。カットセットが適当ではない場合（ブロック３６４）、回路は代わりに外部出力に関し構築された順序付けされた二分決定図を用いて検証される（ブロック３６５）。
【０１２８】
二つの回路の各々に対し適当なカットセットが存在する場合、変数順序π及びπ’は各カットセットに対し計算され（ブロック３６６）、二分決定図の対、Ｆ（λ）及びＧ（λ’）は構築される（ブロック３６７）。ここに与えられたような二分決定図の構成又は操作に必要な変数順序は、例えば、マリック(S. Malik)等の"論理合成環境の二分決定図を使用する論理検証(Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment)"、ICCAD(1988) 、6−9ページに記載されているような標準的な方法で計算される。上記文献の内容は参考として引用されている。その上、ヒューリスティックに許容可能な二分決定図順序を自動的に決定し得る動的な順序付けベースの二分決定図パッケージは、例えば、デビッドロング(David Long)によって開発され、ペンシルベニア州ピッツバーグにあるカーネギーメロン大学から入手可能なパブリックドメインパッケージのように、容易に入手することができる。
【０１２９】
上記二つの二分決定図から、複合二分決定図Ｈは、二分決定図Ｆ（λ）と二分決定図Ｇ（λ’）のブール代数ＸＯＲを実行することにより計算される（ブロック３６８）。このＸＯＲ二分決定図は、二つの関数Ｆ（λ）とＧ（λ）の差分の関数を表わす。
【０１３０】
学習条件の簡単化処理の一部は、外部出力と各回路のカットの間にある学習条件ＡＮＤ＿ＬＮＧ（ｉ）と呼ばれる二分決定図のセットを構築することである（ブロック３６９）。従って、複合二分決定図Ｈは、二つの回路の各々で内部カット点のカットセット変数に関し構築された二つの回路の対応する外部出力の二つの二分決定図の間のブール代数ＸＯＲ演算によって作成される。上記複合二分決定図Ｈは、二分決定図Ｈnew（ｉ）を作成するため学習条件ＡＮＤ＿ＬＮＧ（ｉ）のセットに格納された各二分決定図と論理積をとられる。各演算の後、Ｈnew（ｉ）のサイズはＨのサイズより小さくなり、Ｈnew（ｉ）は元の複合二分決定図Ｈを置換するので、複合二分決定図が単純化される。
【０１３１】
学習条件の論理積の終了後、得られた二分決定図Ｈは、共通因子化と、学習条件を使用する制限とによって更なるサイズの縮小がなされる。共通因子化段階中、二分決定図Ｈはカット変数に基づくシャノンの展開式を用いて共通因子化される（ブロック３７０）。各共通因子化段階の後、カット変数の間接含意は、共通因子のサイズを縮小するため利用される。
【０１３２】
最後に、二つの共通因子は二分決定図Ｈnewを構築するため結合される。Ｈnewのサイズが二分決定図Ｈのサイズより小さい場合、Ｈは、新しいＸＯＲ二分決定図としてのＨnew によって置換される。共通因子化は、Ｈのサイズが縮小化され続ける限り繰り返される。終了時、統合二分決定図Ｈが二分決定図Ｈ  ０である場合（ブロック３７１）、回路は検証され（ブロック３７２）、この処理は終了する。二分決定図Ｈが二分決定図  １に縮小した場合、二つの関数は互いの補数である。或いは、上記引用文献のブリアント(R.E. Bryant)による"ブール代数関数表現のグラフベースアルゴリズム(Graph Based Algorithms for Boolean Function Representation)"、ＩＥＥＥコンピュータ学会誌、C-35(1986年8月)、ページ677-690 に記載されているように、二分決定図Ｈのサイズが小さい場合（ブロック３７３）、回路の外部入力上に作られた二分決定図を用いて複合二分決定図Ｈを完全に合成することにより検証は進行する（ブロック３７４）。
【０１３３】
上記合成がコンピュータメモリ空間の不足に起因して中断しない場合（ブロック３７５）、夫々の二分決定図、Ｆ（λ）及びＧ（λ’）のブール代数ＸＯＲは外部入力に対し計算される。上記結果が０と一致するとき（ブロック３７６）、回路は検証され（ブロック３７９）、この処理は終了する。上記結果が０と一致しない場合、回路は関数的に別であることが判明し（ブロック３７７）、識別ベクトル（二つの回路に供給されたとき、二つの回路の外部出力に別の値を生成する外部入力におけるブール代数値の合成）は二分決定図Ｈの単純な縦優先トレースによって得られ（ブロック３７８）、プロセスは終了する。
【０１３４】
学習条件の論理積とＸＯＲ二分決定図の共通因子化によるサイズの完全な縮小後に、最終的なＨのサイズが、回路の外部入力に関し完全な合成を完了するためには未だ大き過ぎる場合、順次合成と呼ばれる方法がＸＯＲ二分決定図Ｈの単純化のため使用される（ブロック３８０）。以下順次合成処理を説明する：最初に、別の実現可能なカットセットが存在する場合（ブロック３８１）、検証される二つの回路内で新しいカットセットが選択される（ブロック３８２）。元のカットセットで開始し外部入力の方へＬレベルの横優先トレースを用いることにより新しいカットセットを選択することが可能である。好ましい一実施例の場合、Ｌは３でも構わない。
【０１３５】
或いは、新しいカットは、ブロック３６３に示したように、図１７及び１８に示した論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証プログラム２１０からのルーチンを用いて現在のカットと外部入力の間の別の完全なカットとして選択してもよい。完全なカットを探している間に、不完全なカットしか得られなかった場合、カット内のホールの個数が利用可能な計算資源に基づいてある数にヒューリスティックに制限されているならば、かかるカットを許容してもよい。
【０１３６】
次に、二分決定図Ｈは、ＣＵＴnewと呼ぶ新しいカットセットの変数に対し合成される。これにより、ＣＵＴnewに対し構築された新しいＸＯＲ二分決定図Ｈnewが得られる。ＣＵＴnewの前に二つの回路の一部から得られた学習条件は、二分決定図Ｈnewのサイズを縮小するため二分決定図Ｈnew と論理積をなされる。この処理は、二分決定図Ｈnewのサイズを縮小するため使用された上記学習条件処理と同一である。次いで、ＣＵＴnewの変数と次の制限を使用するシャノンの展開式に基づく共通因子化は、二分定図Ｈnew のサイズを更に縮小するため実行される。この段階の終了後、ＣＵＴnewが元のカットセットを置換し、二分決定図Ｈnewが二分決定図Ｈが置換する順次の合成処理を繰り返すことが可能である。この処理は二分決定図Ｈのサイズが外部入力の実現可能性の点で完全な合成がなすため十分に小さくなるまで続けられる。
【０１３７】
順次の合成動作のあらゆる段階において、コンピュータの記憶資源を使用し尽くすことにより動作が失敗するならば、ＡＴＰＧツールが呼び出される（ブロック３８３）。ＡＴＰＧツールのゴールはＸＯＲゲートの出力にある零スタック(stack-at-0)の障害は冗長であることを証明することである。上記障害が冗長であることが証明された場合、検証は終了し、回路は検証される（ブロック３８５）。障害の冗長性が証明されなかった場合、回路は検証されず、障害を示すテストベクトルが検出される（ブロック３８６）。テストベクトルは、二つの回路の外部入力に供給されると、その二つの回路の外部出力に異なるブール代数値を発生させる。
【０１３８】
図３７には、学習条件ＡＮＤ＿ＬＮＧ（ｉ）のセットの計算ルーチンが示されている。二分決定図Ｈのサイズは格納される（ブロック３９６）。カットλの前方にある出力ＸＯＲゲートの入力コーン（中間的ファンイン）のゲートは選択される（ブロック３９０）。格納された（フェーズＩからの）間接含意のリストは辿られ、学習条件はカットλの前方にある含意から形成される（ブロック３９１）。学習条件のサイズがあるユーザ定義値ｋよりも小さい場合（ブロック３９２）、学習条件Ｃj は二分決定図Ｈを単純化するため使用される（ブロック３９３）。トレース処理は、全含意が検出されるまで繰り返され（ブロック３９４）、全処理はカットλの前方にある全ゲートが検出されるまで繰り返される（ブロック３９５）。その上、現在の二分判定図Ｈのサイズが、格納された二分決定図Ｈのあるパーセント、例えば、２％よりも小さい場合（ブロック３９７）、処理は繰り返される。
【０１３９】
図３８には、カットセットλの変数に基づいて共通因子を計算し、二分決定図のサイズを縮小するため論理的相互従属関係を使用する方法が示されている。共通因子は変数又は関数の何れの引き数として見なし得る。このルーチンは、シャノンの展開式を二分決定図Ｈに適用し、既知の含意に基づいて制限を行なうことにより二分決定図のサイズを縮小することを試みる。
【０１４０】
上記フェーズの間、二分決定図Ｈは、支持（サポート）セット、即ち、二分決定図に含まれた全ての固有変数のセット内の各変数で順次に共通因子化される。例えば、ｖはＨの支持セット内の変数である場合を考えてみよう。ｖに関してＨを共通因子化した後、Ｈの二つの共通因子、Ｈv=0 とＨv=1 が得られる。Ｈv=0は変数ｖがブール代数の０に制限された場合の二分決定図Ｈであり、Ｈv=1は変数ｖがブール代数の１に制限された場合の二分決定図Ｈである。最初に、二分決定図Ｈの支持セットは判定され、サイズはＳＩＺＥ＿ＯＲＩＧＩＮＡＬとして格納される（ブロック４００）。
【０１４１】
次に、支持セットの中の多数のｖが選択され（ブロック４０１）、二分決定図Ｈは変数ｖの値に基づいて共通因子化される（ブロック４０２）。ｖ＝０に対し全ての直接及び間接含意のリストが得られる。上記含意の中にＨの支持セット内の他のあらゆる変数に関係するものがある場合、適当な制限がＨv=0で行なわれる（ブロック４０３）。ｖ＝１に対し全ての直接及び間接含意のリストが得られ、同様の制限処理がＨv=1に対し続けられる（ブロック４０４）。
【０１４２】
例えば、含意ｖ＝０ならばａ＝１（ここで、ａはＨの支持セット内の他の変数である）が存在するならば、変数ａはＨv=0でブール代数の１に制限される。かくして、最終的なＨv=0が得られ、最終的なＨv=1が得られる。Ｈnewは以下のシャノンの展開式：
【０１４３】
【数１】
0003857961.tif 000003
を用いて構成される（ブロック４０５）。ＨnewのサイズがＨのサイズよりも小さい場合（ブロック４０６）、ＨはＨnewで置き換えられ（ブロック４０７）、全処理は新しいＨの支持セットの他の変数に対し繰り返される（ブロック４０８）。
【０１４４】
共通因子化と制限が支持セットの全ての変数に対し行なわれた後、Ｈの最終的なサイズが、少なくともあるパーセンテージ、例えば、２％減少した元のＨのサイズよりも小さいならば、全体の処理は繰り返される（ブロック４０９）。しかし、先行の何れかの繰り返し中に二分決定図のサイズが縮小された全ての変数は、１度しか使用されない。上記判定は本質的にヒューリスティックである。
【０１４５】
図３９には、学習条件を適当に論理積することにより複合二分決定図を単純化するルーチンが示されている。ブール代数の論理積演算は、Ｈと学習条件二分決定図Ｃj の間で計算される（ブロック４３４）。計算結果が複合二分決定図の現在のサイズよりも小さい場合（ブロック４３５）、ブール代数論積演算の結果（Ｈ∧Ｃj）は複合二分決定図Ｈの代わりに用いられる（ブロック４３６）。
【０１４６】
ＩＶ．  ハードウェア設計の表現構成のための計算資源必要量の削減
上記方法により、論理的相互従属関係は、決定図を構築するための計算資源の点で必要とされる時間及び空間を削減するため使用される。第１に、論理的相互従属関係（含意）は所定のディジタル回路内で決められる。かかる論理的相互従属関係は、回路内で生じ得る可能な信号割当状況を制限する。例えば、ある信号が：ａ→ｂを含意する場合、信号ａが大きい値をとるときはいつも、信号ｂは大きい値をとる。従って、信号ａは大きい値をとり、信号ｂは小さい値をとる状況は除かれる。
【０１４７】
論理的相互従属関係で表わされたような上記関係を考慮することにより、同様の信号ａ及び信号ｂを有する決定図を単純化することができる。従って、決定図の構成のための計算資源の点で必要とされる時間及びメモリを削減することが可能である。論理ゲートＧを選択することにより、"新しい"副回路Ｇ＿ｃｏｎｅ＿ｃｉｒｃｕｉｔは、全論理ゲートと、ゲートＧの入力コーンにある外部入力（中間的ファンイン）とから形成される。
【０１４８】
図４０及び４１には、本発明の他の実施例によるハードウェア設計の表現構成のための計算資源必要量を削減する処理のフローチャートが示されている。上記処理の目的は、所定の外部出力又はディジタル回路内の内部ゲートに対し二分決定図を構築し、それにより必要とされる時間と計算メモリ資源の必要量を削減することである。回路内の論理ゲートＧは選択され（ブロック４２０）、中間的なファンイン（入力コーン）は副回路Ｇ＿ｃｏｎｅ＿ｃｉｒｃｕｉｔとしてマークされる（ブロック４２１）。
【０１４９】
副回路Ｇ＿ｃｏｎｅ＿ｃｉｒｃｕｉｔの完全なカットλは、ブロック３６３に示したように、図１７及び１８に示した論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証プログラム２１０からのルーチンを用いて判定される（ブロック４２２）。可能な最良のカットを検出する同様の処理は、完全ではない場合もあるが、フェーズＩＩにおいて行なわれるよう続けられる。論理ゲートＧの二分決定図Ｇdはカットλに関し構築される（ブロック４２３）。コンピュータのメモリ資源の不足のため二分決定図を構築し得ない場合、動作は中止される。
【０１５０】
次に、回路の論理ゲートと共に既に格納された学習条件は二分決定図Ｇd を単純化するため使用される（ブロック４２４）。図３５及び３６に示した二分決定図の単純化プログラム３６０を用いる論理設計検証のため使用された同一ルーチンは、この方法でも使用される（ブロック４２４）。新たに単純化された二分決定図は、Ｇnewという名前が付けられる。二分決定図Ｇnewのサイズが二分決定図Ｇdのサイズより小さい場合（ブロック４２５）、二分決定図Ｇnewは二分決定図Ｇdの代わりに用いられる（ブロック４２６）。元の二分決定図Ｇdに割り当てられたコンピュータメモリ資源は解放される（デアロケーション）。
【０１５１】
分割された二分決定図のサイズが大きい、或いは、対応するカットセットが外部入力の近くにない場合、二分決定図Ｇd は再帰的に単純化される。それ以外の場合、二分決定図Ｇdは回路への外部入力に関し合成される（ブロック４２７）。合成演算が成功したとき（ブロック４２８）、目標二分決定図が構成され（ブロック４２９）、このルーチンは終了する。コンピュータメモリが不足した場合、合成は成功しない。コンピュータメモリが不足したとき、元のカットλと外部入力の間にある新しい完全なカットλ’を判定する必要がある（ブロック４３０）。完全なカットが検出されなかった場合、図１７及び１８に示した論理的相互従属関係のある論理ゲートのグループを用いた論理設計検証プログラム２１０の同一ルーチンを用いて、最大の数の論理的相互従属関係を組み込む不完全なカットが使用される（ブロック４３０）。
【０１５２】
再び、二分決定図Ｇdは新しいカットλを使用して合成される（ブロック４３１）。合成が成功しなかった場合（ブロック４３２）、目標二分決定図は構築されず（ブロック４３３）、このルーチンは終了する。或いは、合成動作が成功して終了し、完全なカットλ’が外部入力にない場合（ブロック４３４）、上記ルーチンは繰り返される。完全なカットλ’が外部入力にある場合、目標二分決定図が構成され（ブロック４３５）、上記ルーチンは終了する。
【０１５３】
本発明の方法によれば、論理的相互従属関係はメモリ必要量と計算時間の両方を削減するため使用し得る利点がある。完全なカットを選択するルーチンと同一ルーチンを採用することにより、二分決定図のサイズを縮小するためカットλ内の変数間の関係を全部利用する。更に、二分決定図のサイズは縮小されるので、コンピュータメモリの必要量は削減される。最後に、合成される二分決定図のサイズが小さいほど、二分決定図の合成をより高速に行なうことができる。従って、時間的な必要量が削減される。
【０１５４】
Ｖ．  ゴール向き学習
本発明によれば、ゴール向き学習(goal directed learning)として周知のより効率的に計算資源を特定のゴールに向ける方法が得られる更なる利点がある。例えば、論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証又は二分決定図の単純化（フェーズＩＩ及びＩＩＩ）を行なう場合、カットλが判定されたとき、カット点と外部出力の間により多くの論理的相互従属関係（含意）が得られるようゴール向き学習の方法を用いて資源を割り当てることができる。これにより得られた論理的相互従属関係の数は増加するので、外部出力により近い新しいカットλを得ることができ、これにより、回路のより小さい部分が得られる。その上、論理的相互従属関係の増加は、本明細書のパートＩＶに記載した方法に利用された差の二分決定図Ｇd を更に単純化するため付加的な学習条件を使用し得ることを更に意味する。
【０１５５】
ゴール向き学習は、計算資源を集中させるため回路の近似的な領域に定義するように初期カットλを扱う。初期カットλは、使用された最大学習レベルが外部出力からの構造的距離ｋである学習方法を用いて回路で得られた場合、ゴール向き学習は、ｋより大きい学習レベル、例えば、ｋ＋ｉを用いて、初期カットの近傍で論理的相互従属関係の判定に集中する。ここで、上記ｉの値の一例は２である。学習処理は初期カットλの周辺の回路の上記領域に採用され、上記仮想領域はゴール向き学習領域と呼ばれる。
【０１５６】
以下、ゴール向き学習の実行方法を説明する。元のカットλと、外部出力の間にあるカットλk+iが、元のカットからｋ＋ｉの距離を用いて定められる。カットλから始めて、学習処理は、学習レベルｋ＋ｉの関数的学習を利用して、カットλとカットλk+iの間にある全ての論理ゲートで学習する。これにより定められた論理的相互従属関係は、回路内の更なる論理的相互従属関係を定めるため、或いは、より良いカットλを検出するため使用される。
【０１５７】
図４２には、本発明の他の実施例によるゴール向き学習を実行する処理のフローチャートが示されている。カットλと、カットλから最大でｋ＋Ｌ１の構造的距離にある外部出力との間にある全論理ゲートからなるリストＬ（λ，ｋ＋Ｌ１）が検出される（ブロック４５０）。かかるリストはゴール向き学習領域をなす。ゲートＧはリストＬ（λ，ｋ＋Ｌ１）から選択され（ブロック４５１）、論理的相互従属関係は、学習レベルがｋ＋ｉと一致する関数的学習（フェーズ１）を用いて判定される（ブロック４５２）。上記選択及び判定段階は、リストＬ（λ，ｋ＋Ｌ１）内の全ゲートが選択されるまで、繰り返される（スデップ４５３）。学習レベルの数ｉはある固定的な一定値Ｌ２を超えず、所定の数の付加的な論理的相互従属関係又は他の関係する理由のような何らかの理由から判定段階の結果を満足できない場合（ブロック４５４）、学習レベルパラメータｉは、例えば、２のようなある固定の増分で増加され（ブロック４５５）、処理は繰り返される。
【０１５８】
ゴール向き学習を行なう第２の方法を以下に説明する。元のカットλのｋ＋ｉレベル前に構造的なカットが得られる。この新しいカットはＣＵＴ１と呼ばれる。次に、元のカットλのｋ＋ｉレベル後に構造的なカットが得られる。この新しいカットはＣＵＴ２と呼ばれる。論理設計解析は、学習レベルｋ＋ｉを用いてＣＵＴ１とＣＵＴ２の間で行なわれる。このレベルは最大でｋ＋ｉまで増加させることが可能である。この方法は、計算的にコストの高い解析が行なわれる場合に、回路の領域が認定されるときいつも過剰な論理的相互従属関係を得るため使用され、この過剰な論理的相互従属関係の恩恵を受ける。
【０１５９】
図４２には、本発明の他の実施例によるゴール向き学習を実行する他の処理のフローチャートが示されている。カットλと外部出力、又は、カットλと外部入力の間にあり、どちらの場合でもカットλから最大でｋ±Ｌ１の構造的距離にある全ての論理ゲートからなるリストＬ（λ，ｋ±Ｌ１）が検出される（ブロック４６０）。このリストはゴール向き学習領域をなす。ゲートＧはリストＬ（λ，ｋ±Ｌ１）から選択され（ブロック４６１）、論理的相互従属関係は、学習レベルがｋ＋ｉと一致する関数的学習（フェーズ１）を用いて判定される（ブロック４６２）。上記選択及び判定段階は、リストＬ（λ，ｋ±Ｌ１）内の全ゲートが選択されるまで、繰り返される（スデップ４６３）。学習レベルの数ｉはある固定的な一定値Ｌ２を超えず、所定の数の付加的な論理的相互従属関係又は他の関係する理由のような何らかの理由から判定段階の結果を満足できない場合（ブロック４６４）、学習レベルパラメータｉは、例えば、２のようなある固定の増分で増加され（ブロック４６５）、処理は繰り返される。
【０１６０】
本発明の説明及び記載を特に好ましい実施例に関し行なったが、本発明の精神と目的の範囲を逸脱することなく形態及び詳細の上記及び他の変形を行ない得ることは当業者により理解される。
【０１６１】
【発明の効果】
上記説明のように、本発明によれば、ディジタル回路の論理ネットワークに基づく論理設計解析の際に生じる所謂ＮＰ完全問題の解法のために必要とされる計算時間とメモリ空間が削減される。従って、論理設計解析を必要とするディジタル回路のエンジニアリング変更の際の時間的、メモリ空間的な制約が低減され、エンジニアリング変更の導入が容易になるという利点が得られる。
【０１６２】
更に、本発明によれば、ＣＡＤ業界において重要なディジタル回路の製造欠陥のテストベクトルを得るためのＡＴＰＧの問題が解決される。即ち、従来のＡＴＰＧ機器で検出が困難であった冗長性欠陥と呼ばれる特定の欠陥のタイプを検出し得るようになる。
【図面の簡単な説明】
【図１】本発明を実施するコンピュータ装置のブロック図である。
【図２】図１の装置で使用されるような論理的相互従属関係の判定用の論理設計解析を実行するコンピュータ支援設計装置のブロック図である。
【図３】（Ａ）は間接的な含意のためのディジタル回路の解析処理の一例を示し、（Ｂ）は論理回路設計の一区分が論理設計検証を行なうため完全であるときを判定する処理の一例を示し、（Ｃ）は論理設計検証を行なうため学習条件を使用する処理の一例を示している本発明の一実施例による処理のフローチャートである。
【図４】ディジタル論理回路の一例を示す論理設計の概要図である。
【図５】ディジタル論理回路の論理ゲートの内部データ構造の一例を示す図である。
【図６】（Ａ）乃至（Ｃ）は、図４に示した論理ゲートの二分決定図と正当化ベクトルとを示す図である。
【図７】論理回路の含意を学習することにより論理設計を解析する処理の一例のフローチャートである。
【図８】特定の論理回路のファンインにある未正当化ゲートの検出ルーチンの一例のフローチャートである。
【図９】特定の論理回路のカットセットの検出ルーチンの一例のフローチャートである。
【図１０】カットセットを用いる特定の論理回路の二分決定図構築ルーチンの一例のフローチャートである。
【図１１】二分決定図の頂点レコードの内部データ構造の一例を示す図である。
【図１２】特定の論理ゲートの潜在的学習対象領域の作成ルーチンの一例を示すフローチャートである。
【図１３】特定の論理ゲートの潜在的学習対象領域の作成ルーチンの一例を示すフローチャートである。
【図１４】二分決定図から得られた正当化ベクトルの内部データ構造の一例を示す図である。
【図１５】潜在的学習対象領域の各ゲートと、特定の論理ゲートの間の含意学習ルーチンの一例を示すフローチャートである。
【図１６】図１の装置で使用されるような論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証用のコンピュータ支援設計装置及び方法のブロック図である。
【図１７】本発明の他の実施例による論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証処理の一例のフローチャートである。
【図１８】本発明の他の実施例による論理的相互従属関係のある論理ゲートのグループを用いる論理設計検証処理の一例のフローチャートである。
【図１９】（Ａ）は論理的相互従属関係の仮のリストを格納するリンクドリストのデータ構造を示し、（Ｂ）はリンクしたリストデータ構造の一例を示す図である。
【図２０】（Ａ）は論理ゲートの１レベルの終了時、論理的相互従属関係を収集するリストデータ構造を示し、（Ｂ）は論理的相互従属関係のリストのセットの一例を示す図である。
【図２１】外部出力から始まるカットセットαの検出ルーチンの一例のフローチャートである。
【図２２】仮のカット選択領域と反射的な仮のカット選択領域を格納するデータ構造を示す図である。
【図２３】反射的なカットセットαの検出ルーチンの一例のフローチャートである。
【図２４】反射的なカットセットαの検出ルーチンの一例のフローチャートである。
【図２５】カットセット内のホールの充填ルーチンの一例のフローチャートである。
【図２６】ゲートが反射的な仮のカット選択領域に含まれるかどうかを定めるため、ゲートのファンインを介する後向きトレースルーチンの一例のフローチャートである。
【図２７】カットセットの完全性判定ルーチンの一例のフローチャートである。
【図２８】論理的相互従属関係のセット内の論理ゲートのマークルーチンの一例のフローチャートである。
【図２９】不完全なカットを完全化するため必要な論理ゲートの判定ルーチンの一例のフローチャートである。
【図３０】（Ａ）はカットセットを格納するデータ構造を示し、（Ｂ）はカットを格納するデータ構造を示す図である。
【図３１】部分カットの論理ゲートをトレースし、マークするルーチンの一例のフローチャートである。
【図３２】論理的相互従属関係のセット内の論理ゲートと、それ以外の論理ゲートの間のギャップをつなぐ論理ゲートを探索するルーチンの一例のフローチャートである。
【図３３】先にマークされた論理ゲートをトレースし、マークするルーチンの一例のフローチャートである。
【図３４】図１の装置で使用されるような二分決定図の単純化を用いる論理設計検証用のコンピュータ支援装置のブロック図である。
【図３５】本発明の他の実施例による二分決定図の単純化を用いる論理設計検証処理を示すフローチャートである。
【図３６】本発明の他の実施例による二分決定図の単純化を用いる論理設計検証処理を示すフローチャートである。
【図３７】学習条件のセットを計算するルーチンの一例の示すフローチャートである。
【図３８】カットセットの変数に基づいて共通因子を計算し、二分決定図のサイズを縮小するため既知の論理的相互従属関係を使用するルーチンの一例を示すフローチャートである。
【図３９】学習条件を適当に論理和することにより複合二分決定図を単純化するルーチンの一例を示すフローチャートである。
【図４０】本発明の他の実施例によるハードウェア設計の構成のための計算資源必要量を削減する処理を示すフローチャートである。
【図４１】本発明の他の実施例によるハードウェア設計の構成のための計算資源必要量を削減する処理を示すフローチャートである。
【図４２】本発明の他の実施例によるゴール向き学習を実行する処理を示すフローチャートである。
【図４３】本発明の他の実施例によるゴール向き学習を実行する他の処理を示すフローチャートである。
【図４４】複合ディジタル回路の論理ネットワークを示す論理設計の概略図である。
【符号の説明】
１    ２次記憶装置
２    主メモリ
３    マイクロプロセッサ
４    ディスプレイ
５    プリンタ
６    結果ファイル
７    コンピュータプログラム
１０    候補ゲートセット選択部
１１    未正当化ゲート選択部
１２    カットセット選択部
１３    二分決定図（ＢＤＤ）構築部
１４    潜在的学習対象領域マーカー部
１５    含意学習部
１６    主制御部
１７    候補論理ゲートセット
１８    未正当化ゲートセット
１９    固有ブール代数値セット
２０    カットセット
２１，２４    二分決定図
２２    正当化ベクトル／パスセット
２３    潜在的学習対象領域セット
【図１】
0003857961.tif 000004
【図２】
0003857961.tif 000005
【図３】
0003857961.tif 000006
【図４】
0003857961.tif 000007
【図５】
0003857961.tif 000008
【図６】
0003857961.tif 000009
【図７】
0003857961.tif 000010
【図８】
0003857961.tif 000011
【図９】
0003857961.tif 000012
【図１０】
0003857961.tif 000013
【図１１】
0003857961.tif 000014
【図１２】
0003857961.tif 000015
【図１３】
0003857961.tif 000016
【図１４】
0003857961.tif 000017
【図１５】
0003857961.tif 000018
【図１６】
0003857961.tif 000019
【図１７】
0003857961.tif 000020
【図１８】
0003857961.tif 000021
【図１９】
0003857961.tif 000022
【図２０】
0003857961.tif 000023
【図２１】
0003857961.tif 000024
【図２２】
0003857961.tif 000025
【図２３】
0003857961.tif 000026
【図２４】
0003857961.tif 000027
【図２５】
0003857961.tif 000028
【図２６】
0003857961.tif 000029
【図２７】
0003857961.tif 000030
【図２８】
0003857961.tif 000031
【図２９】
0003857961.tif 000032
【図３０】
0003857961.tif 000033
【図３１】
0003857961.tif 000034
【図３２】
0003857961.tif 000035
【図３３】
0003857961.tif 000036
【図３４】
0003857961.tif 000037
【図３５】
0003857961.tif 000038
【図３６】
0003857961.tif 000039
【図３７】
0003857961.tif 000040
【図３８】
0003857961.tif 000041
【図３９】
0003857961.tif 000042
【図４０】
0003857961.tif 000043
【図４１】
0003857961.tif 000044
【図４２】
0003857961.tif 000045
【図４３】
0003857961.tif 000046
【図４４】
0003857961.tif 000047