説明

等価検証のためのデジタル回路の状態素子をマッピングするためのシステム及び方法

【課題】等価検証のためのデジタル回路の状態素子をマッピングするシステム及び方法を提供する。
【解決手段】第1の回路と第2の回路の一次入力と一次出力からそれらの各状態素子までの回路の2点間の任意のパスに沿った状態素子の最小のカウントである第1の逐次的な深さを決定し102、特有の第1の逐次的な深さを有する第1の回路と第2の回路の第1の状態素子を識別及びマッピングし104、第1の回路と第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定し106、特有の第2の逐次的な深さを有する第1の回路と第2の回路の第2の状態素子を識別し108、プロセスがもはや状態素子の新しい特有のマッピングを発生しない場合を除いて、106と108を反復する。

【発明の詳細な説明】
【技術分野】
【0001】
本発明は等価検証に関し、特に等価検証のためのデジタル回路の状態素子をマッピングするためのシステム及び方法に関する。
【背景技術】
【0002】
本発明はDARPAにより授与された政府の契約番号HR0011-08-C-0005に関する。米国政府はこの発明においてある権利を有する。
【0003】
集積回路設計に関連されるプロセスは通常、高いレベルの抽象から中間及び低いレベルの抽象までの幾つかの設計変換を含んでいる。各レベルで、任意の変換が機能的又は論理的に設計を変更しないことを証明するため等価検証が行われる。
【0004】
通常の等価検証方法は、通常、等価として検証された構成間の状態素子のマッピングを必要とする。これらのマッピング方法は幾つかのカテゴリのうちの1つに入る。かなり共通であるネーミング方法は同様に名づけられた各設計中の対応する点をマップする。しかしながら、状態素子の名称はネーミング方法を使用して幾つかの設計ツールにより行われる設計変換期間中に変更されるか失われる可能性がある。さらに、ネーミング方法はリバースエンジニアリング型の応用にはほとんど使用できない。別の方法は状態素子のファンイン論理コーン(例えば二分決定グラフすなわちBDD)の正準表現を使用する関数方法である。しかしながら関数方法は情報が利用可能ではないときコーンの全ての入力がマップされることをしばしば必要とし、それによって円形の問題を生む。
【0005】
別の方法は両者の設計レベルをシミュレートし、その後シミュレーションコンポーネントの選択を類似の値ベクトルを有する状態素子に一致するか狭めるシミュレーション方法である。シミュレーション方法はしかしながら意図的または意図的ではない変換が存在する場合、使用するのが困難である可能性がある。構造的方法と呼ばれる別の方法では、ネットリスト対ネットリスト型の比較が行われ、これは組合せコーン構造を検査する。幾つかの例では、これらの方法の組合せが使用される。しかしながら等価検証のための通常の方法の多く又は全ては幾つかの欠点を有する。したがって等価検証を行うための改良された方法が必要とされる。
【発明の概要】
【0006】
本発明の特徴は等価検証のためのデジタル回路の状態素子をマッピングするためのシステム及び方法に関する。1実施形態では、本発明は第1の回路と第2の回路の間の等価検証のため状態素子をマッピングする方法に関し、この方法は(a)第1の回路と第2の回路の一次入力と一次出力から第1及び第2の回路の各状態素子までの第1の逐次的な深さを決定し、その第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントであり、(b)特有の第1の逐次的な深さを有する第1の回路と第2の回路の第1の状態素子を識別し及びマッピングし、(c)第1の回路と第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定し、(d)特有の第2の逐次的な深さを有する第1の回路と第2の回路の第2の状態素子を識別し、(e)プロセスがもはや状態素子の新しい特有のマッピングを発生しない場合を除いて、(c)と(d)を反復するステップを含んでいる。
【0007】
別の実施形態では、本発明は第1の回路と第2の回路との間の等価検証のため状態素子をマッピングする方法に関し、その方法は(a)第1の回路と第2の回路の一次入力と一次出力から第1及び第2の回路の各状態素子までの第1の逐次的な深さを決定し、第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントであり、(b)各状態素子の第1の逐次的な深さに基づいて第1の回路と第2の回路の各状態素子の第1の特徴ベクトルを発生し、(c)特有の第1のベクトルを有する第1の回路と第2の回路の状態素子を識別し、第1および第2の回路の識別された状態素子の第1の特徴ベクトルがほぼ同一であるならば、第1の回路の識別された状態素子を第2の回路の識別された状態素子へマッピングし、(d)第1の回路と第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定し、(e)各識別された状態素子の第2の逐次的な深さに基づいて第1の回路と第2の回路の各識別された状態素子の第2の特徴ベクトルを発生し、(f)特有の第2のベクトルを有する第1の回路と第2の回路の状態素子を識別し、特有の第2のベクトルを有する第1及び第2の回路の識別された状態素子の第2の特徴ベクトルがほぼ同一であるならば、特有の第2のベクトルを有する第1の回路の識別された状態素子を特有の第2のベクトルを有する第2の回路の識別された状態素子へマッピングし、(g)マッピングプロセスの終了のためのしきい値状態が満足されたか否かを決定するステップを含んでいる。
【図面の簡単な説明】
【0008】
【図1】本発明の1実施形態による第1の回路と第2の回路間の等価検証のために状態素子をマッピングするプロセスのフローチャートである。
【図2】本発明の1実施形態による第1の回路と第2の回路間の等価検証のために状態素子をマッピングする別のプロセスのフローチャートである。
【図3】本発明の1実施形態による一次入力からデジタル回路の各状態素子までの逐次的な深さの決定を示すデジタル回路の概略図である。
【図4】本発明の1実施形態による一次出力からデジタル回路の各状態素子までの逐次的な深さの決定を示す図3のデジタル回路の概略図である。
【図5】本発明の1実施形態による各一次入力と一次出力からデジタル回路の各状態素子までの逐次的な深さからなる特徴ベクトルの決定を示す図3のデジタル回路の概略図である。
【図6】本発明の1実施形態による特有の特徴ベクトルを有する状態素子のグループ化と、特有の特徴ベクトルを有する状態素子の識別とを示している図3のデジタル回路の概略図である。
【図7】本発明の1実施形態による図6の同一の特徴ベクトルを有する状態素子のグループ化と、特有の特徴ベクトルを有する状態素子の識別とを示している表である。
【図8】本発明の1実施形態による設計ツールが変換を行った後の図3のデジタル回路の概略図であり、ここでは状態素子は最適化され、逐次的な深さにおける効果を示している。
【図9】本発明の1実施形態による図8に示されている状態素子の除去により生じるそれぞれの特徴ベクトルの小さな差を示すための図7の表の再生図である。
【図10】本発明の1実施形態による図8に示されている状態素子の除去により生じるそれぞれの特徴ベクトルの小さな差を示す表である。
【図11】本発明の1実施形態による逐次的な深さのマッピングプロセスに関連されるマッピング性能における改良と、通常のマッピングツールとの比較を示すグラフである。
【発明を実施するための形態】
【0009】
図面を参照すると、第1の回路と第2の回路との間の等価検証のために状態素子をマッピングするためのシステム及び方法の実施形態が示されている。これらの方法は一次入力と出力から各回路の各状態素子までの逐次的な深さの決定を含むことができ、逐次的な深さは回路の2つの点間の可能なパスに沿って遭遇された状態素子の最小のカウントである。この方法はまた一次入力と出力から特有の逐次的な深さを有する第1の回路及び第2の回路の状態素子を識別及びマッピングするステップを含んでいる。幾つかの実施形態では、この方法は第1の回路の特有に識別された状態素子を第2の回路の対応する特有に識別された状態素子へマップする。方法はその後、第1の回路と第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定し、特有の第2の逐次的な深さを有する第1の回路と第2の回路の第2の状態素子を識別してマッピングするステップも含むことができる。幾つかの実施形態では、前述の動作は方法がもはや状態素子の新しい特有のマッピングを発生しなくなるまで反復される。
【0010】
幾つかの実施形態では、逐次的な深さの方法は等価検証のための改良された性能を与え、最適の性能の他の等価検証と共に使用されることができる。1実施形態では、逐次的な深さの方法は通常の等価検証ツールの開始点として使用されることができる。このような場合、逐次的な深さの方法は通常の等価検証ツールの性能を非常に改良できる。幾つかの実施形態では、ここで説明する逐次的な深さの方法は機能ツール、シミュレーションツール、ネーミングツール又は他の適切な検証ツールのような通常の等価検証ツールの1つと共に使用される。
【0011】
図1は本発明の1実施形態による第1の回路と第2の回路との間の等価検証のために状態素子をマッピングするプロセスのフローチャートである。ブロック102では、プロセスは最初に第1の回路と第2の回路の一次入力と一次出力から第1及び第2の回路の各状態素子までの第1の逐次的な深さを決定し、それにおいて第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントである。幾つかの実施形態では、第1の逐次的な深さは一次入力又は出力のうちの1つと任意のパスに沿った特定の状態素子との間で遭遇される最少数の状態素子のカウントである。多数の実施形態では、プロセスは第1の回路の各状態素子から第1の回路の各一次入力及び一次出力までの第1の逐次的な深さを決定し、第2の回路の各状態素子から第2の回路の一次入力及び一次出力までの第1の逐次的な深さを決定する。
【0012】
ブロック104で、プロセスは特有の第1の逐次的な深さを有する第1の回路と第2の回路の第1の状態素子を識別する。幾つかの実施形態では、プロセスは同一ではないまたは特有の第1の状態素子を識別するためにほぼ同一の第1の逐次的な深さを有する第1の状態素子をグループ化する。特有の逐次的な深さのカウントまたはシグネチャは第1と第2の回路間の状態素子をマップする機会を与える。1実施形態では、第1の状態素子の識別においてプロセスはほぼ同じ第1の逐次的な深さを有する第1の回路の状態素子をグループ化し、1つのグループカウントを有する第1の回路の第1の状態素子を選択し、ほぼ同じ第1の逐次的な深さを有する第2の回路の状態素子をグループ化し、1つのグループカウントを有する第2の回路の第1の状態素子を選択する。1つのグループカウントは特有の逐次的な深さを有する状態素子に対応できる。
【0013】
ブロック106で、プロセスは第1の回路及び第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定する。幾つかの実施形態では、残りの状態素子は先に識別されておらず特有の逐次的な深さをマップされていない状態素子である。幾つかの実施形態では、第2の逐次的な深さは識別された第1の状態素子のうちの1つと特定の状態素子の間の状態素子のカウントである。1実施形態では、第2の逐次的な深さの決定においてプロセスは第1の回路の各識別された第1の状態素子から第1の回路の各状態素子までの第2の逐次的な深さを決定し、第2の回路の各識別された第1の状態素子から第2の回路の各状態素子までの第2の逐次的な深さを決定する。
【0014】
ブロック108で、プロセスは特有の第2の逐次的な深さを有する第1の回路と第2の回路の第2の状態素子を識別し、これらを他の回路の対応するコンポーネントへマップする。幾つかの実施形態では、プロセスは同一ではないか特有の第2の状態素子を識別するためほぼ同一の第1の逐次的な深さを有する第2の状態素子をグループ化する。1実施形態では、第2の状態素子の識別においてプロセスはほぼ同じ第2の逐次的な深さを有する第1の回路の状態素子をグループ化し、1のグループカウントを有する第1の回路の第2の状態素子を選択し、ほぼ同じ第2の逐次的な深さを有する第2の回路の状態素子をグループ化し、1のグループカウントを有する第2の回路の第2の状態素子を選択する。選択されたグループは第1と第2の回路間の状態素子をマップする機会を与える。
【0015】
ブロック110で、プロセスはそのプロセスが状態素子の新しいマッピングを発生しているか否かを決定する。ノーであるならばプロセスは終了する。イエスであるならば、プロセスはブロック106へ戻り、ブロック110の条件が満たされるまでブロック106と108の動作を繰返し反復する。1実施形態では、プロセスはブロック106と108の連続的な反復が状態素子の新しい特有のマッピングを発生しなくなるまでブロック106と108の動作を反復する。
【0016】
1実施形態では、プロセスは異なる順序で動作のシーケンスを実行できる。別の実施形態ではプロセスは動作の1以上を省略できる。他の実施形態では、動作の1以上は同時に行われる。幾つかの実施形態では、付加的な動作が行われることができる。
【0017】
図2は本発明の1実施形態による第1の回路と第2の回路との間の等価検証のために状態素子をマッピングする別のプロセス200のフローチャートである。ブロック202で、プロセスは最初に第1の回路及び第2の回路の一次入力および一次出力から第1及び第2の回路の各状態素子までの第1の逐次的な深さを決定し、ここで第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントである。幾つかの実施形態では、第1の逐次的な深さは一次入力または一次出力のうちの1つと任意のパスに沿った特定の状態素子との間で遭遇された最少数の状態素子のカウントである。1実施形態では、第1の逐次的な深さの決定において、プロセスは第1の回路の各一次入力及び一次出力のそれぞれから第1の回路の各状態素子までの第1の逐次的な深さを決定し、第2の回路の一次入力及び一次出力から第2の回路の各状態素子までの第1の逐次的な深さを決定する。
【0018】
ブロック204で、プロセスは各状態素子に対する第1の逐次的な深さに基づいて第1の回路と第2の回路の各状態素子の第1の特徴ベクトルを発生する。幾つかの実施形態では特徴ベクトルは各一次入力と各一次出力からそれぞれの状態素子までの逐次的な深さの測定からなる。
【0019】
ブロック206で、プロセスは特有の第1のベクトルを有する第1の回路と第2の回路の第1の状態素子を識別し、第1及び第2の回路の識別された状態素子の第1の特徴ベクトルがほぼ同じであるならば、第1の回路の識別された状態素子を第2の回路の識別された状態素子へマップする。幾つかの実施形態では、プロセスは同一ではないか特有の第1のベクトルを識別するためほぼ同一の逐次的な深さのベクトルを有する第1のベクトルをグループ化する。1実施形態では、第1の状態素子の識別においてプロセスはほぼ同じ第1のベクトルを有する第1の回路の状態素子をグループ化し、1つのグループカウントを有する第1の回路の第1の状態素子を選択し、ほぼ同じ第1のベクトルを有する第2の回路の状態素子をグループ化し、1つのグループカウントを有する第2の回路の第1の状態素子を選択する。1つのグループカウントは特有の逐次的な深さを有する状態素子に対応できる。
【0020】
1実施形態では、特徴ベクトルが1デジット異なるとき別の特徴ベクトルとほぼ同一である。別の実施形態では、特徴ベクトルが予め定められた割合異なるとき別の特徴ベクトルにほぼ同一である。別の実施形態では、1つの特徴ベクトルは特徴ベクトルが予め選択された距離アルゴリズムにより許容可能に思われる予め選択されたしきい値だけ異なるとき別の特徴ベクトルにほぼ同一である。些細な差にかかわらず状態素子をマッピングするための距離メトリックまたは距離アルゴリズムを以下さらに詳細に説明する。
【0021】
ブロック208で、プロセスは第1の回路及び第2の回路の識別された第1の状態素子から残りの状態素子までの第2の逐次的な深さを決定する。幾つかの実施形態では、残りの状態素子は特有の第1の逐次的な深さと同じであると先に識別されていない状態素子である。1実施形態では、第2の逐次的な深さの決定において、プロセスは第1の回路の識別された各状態素子から第1の回路の各状態素子までの第2の逐次的な深さを決定し、第2の回路の各識別された各状態素子から第2の回路の各状態素子までの第2の逐次的な深さを決定する。
【0022】
ブロック210で、プロセスは各状態素子の第2の逐次的な深さに基づいて第1の回路及び第2の回路の各識別された状態素子の第2の特徴ベクトルを生成する。幾つかの実施形態では、各第2の特徴ベクトルは識別された状態素子からそれぞれの状態素子までの逐次的な深さの測定からなる。
【0023】
ブロック212で、プロセスは特有の第2のベクトルを有する第1の回路と第2の回路の第2の状態素子を識別し、特有の第2のベクトルを有する第1及び第2の回路の識別された状態素子の第2の特徴ベクトルがほぼ同一であるならば、特有の第2のベクトルを有する第1の回路の識別された状態素子を特有の第2のベクトルを有する第2の回路の識別された状態素子へマップする。幾つかの実施形態では、プロセスは同一ではないか特有の第2のベクトルを識別するためにほぼ同一の逐次的な深さを有する第2のベクトルをグループ化する。1実施形態では、第2の状態素子の識別において、プロセスはほぼ同じ第2のベクトルを有する第1の回路の状態素子をグループ化し、1つのグループカウントを有する第1の回路の第2の状態素子を選択し、ほぼ同じ第2のベクトルを有する第2の回路の状態素子をグループ化し、1つのグループカウントを有する第2の回路の第2の状態素子を選択する。
【0024】
ブロック216で、プロセスはそのプロセスが状態素子の新しいマッピングを発生しているか否かを決定する。ノーであるならばプロセスは終了する。イエスであるならば、プロセスはブロック208へ戻り、ブロック216の条件が満たされるまでブロック208から214の動作を繰返し反復する。幾つかの実施形態では、ブロック208から214の動作の連続的な反復が状態素子の任意の新しい特有のマッピングを発生しなくなるときブロック216の条件は満たされる。
【0025】
1実施形態では、プロセスは異なる順序で動作のシーケンスを実行できる。別の実施形態ではプロセスは1以上の動作を省略できる。他の実施形態では、1以上の動作は同時に行われる。幾つかの実施形態では、付加的な動作が行われることができる。
【0026】
幾つかの実施形態では、フロップ間の差別化を行うことができる逐次的な深さ以外の特徴も使用されることができる。1つのこのような実施形態では、他の特徴の1以上が付加的な差別化要因として特徴ベクトルに付加される。
【0027】
図3は本発明の1実施形態による一次入力Aからデジタル回路の各状態素子までの逐次的な深さの決定を示すデジタル回路300の概略図である。特定の実施形態では、この一次入力からの逐次的な深さの決定は図1および2のプロセスのブロック102と202と関連して使用されることができる。
【0028】
回路300は一次入力A、一次入力B、一次出力F、一次出力G、状態素子i0、i1、i2、i3、i4、i5、i6、i7、i8、i9を含んでいる。一次入力Aへの各状態素子の逐次的な深さ(例えば2つの点間の任意のパスに沿って遭遇される状態素子の最小のカウント)が決定され、図3の各状態素子ボックス上に表示される。例えばi0から一次入力Aまでの最小の距離パスは1つの状態素子、即ちi0を横切るので、状態素子i0から一次入力Aまでの逐次的な深さは“1”である。状態素子i1から一次入力Aまでの逐次的な深さは到達ができないので“-”であり、または違った方法で述べられ、無限の距離にある。状態素子i9から一次入力Aまでの逐次的な深さは、一次入力Aへの最短パスが3つの状態素子即ちi9、i7およびi4またはi5を横切るので“3”である。他の状態素子からの逐次的な深さは類似の方法で決定される。
【0029】
図3の回路は逐次的な深さプロセスによって使用されることができる1回路の1例である。他の実施形態では、逐次的な深さのプロセスは他の回路により使用されることができる。他の実施形態では、例えば逐次的な深さのプロセスは図3の回路よりも付加的なまたは少数の一次入力と出力及び状態素子を有する回路によって使用されることができる。
【0030】
図4は本発明の1実施形態による一次出力Gからデジタル回路の各状態素子までの逐次的な深さの決定を示す図3のデジタル回路300の概略図である。一次出力Gまでの各状態素子の逐次的な深さが決定され、各状態素子ボックス上に併記されている。例えば状態素子i9から一次入力Aまでの逐次的な深さは、i9から一次出力Gへの最小の距離パスが1つの状態素子、即ちi9を横切るので“1”である。状態素子i8から一次出力Gまでの逐次的な深さはi8から到達ができないので“-”である。状態素子i1から一次出力Gまでの逐次的な深さは、最短パスがi1、i2またはi3と、i6およびi9を横切るので“4”である。他の状態素子からの逐次的な深さは類似の方法で決定される。
【0031】
図5は本発明の1実施形態による各一次入力と一次出力からデジタル回路300の各状態素子までの逐次的な深さからなる特徴ベクトルの決定を示す図3のデジタル回路300の概略図である。各状態素子における特徴ベクトルはA、B、F、Gのベクトル順序における一次入力及び出力までの逐次的な深さを示している。例えば各特徴ベクトルの第1の数字の逐次的な深さは一次入力Aまでの逐次的な深さを図3に示されているものと同一の計算された数で示している。同様に、各特徴ベクトルの最後の数字の逐次的な深さは一次出力Gまでの逐次的な深さを図4に示されているものと同一の計算された数で示している。幾つかの実施形態では特徴ベクトルが決定されると、プロセスはこれらを特有の特徴ベクトルを有する状態素子を識別してマップするために使用することができる。
【0032】
図6は本発明の1実施形態による同一の特徴ベクトル(i2、i3、i4、i5)を有する状態素子のグループ化と、特有の特徴ベクトル(i0、i1、i6、i7、i8、i9)を有する状態素子の識別とを示している図3のデジタル回路300の概略図である。
【0033】
図7は本発明の1実施形態による図6の同一の特徴ベクトルを有する状態素子のグループ化と、特有の特徴ベクトルを有する状態素子の識別とを示している表である。この表では、共通の特徴ベクトルは共にグループ化され、グループ識別番号を割当てられている。表及び図6から認められるように、i2、i3およびi4、i5の特徴ベクトルは特有ではなく、残りの特徴ベクトルは特有である。通常、(例えば特有の逐次的な深さを有する)サイズ1のグループは回路間でマップされることができる。
【0034】
ここで説明されている幾つかのプロセスによれば、特有であるとして識別される特徴ベクトルはその後の逐次的な深さの決定で使用されることができる。多くの実施形態では、反復的なプロセスはプロセスの連続的な反復が状態素子の新しい特有のマッピングを発生しなくなるまで特有のベクトルを有する新しい状態素子を識別するために先にマップされた状態素子からの逐次的な深さを決定し続ける。幾つかの実施形態では、図3乃至6のデジタル回路と図7の表は図1および2に示されている1以上のプロセスで使用される。
【0035】
図8は本発明の1実施形態による設計ツールが変換を行った後の図3のデジタル回路に基づいたデジタル回路400の概略図であり、ここでは状態素子(ij)は最適化されており逐次的な深さにおける効果を示している。一次出力Fからの逐次的な深さは状態素子(ij)が最適化された後に各状態素子で示されている。
【0036】
図9は本発明の1実施形態による図8に示されている状態素子の除去により生じるそれぞれの特徴ベクトルの小さな差を示すための図7の表の再生図である。
【0037】
図10は本発明の1実施形態による図8に示されている状態素子の除去により生じるそれぞれの特徴ベクトルの小さな差を示している表である。図9および10の表から認められるように、図10の一次出力Fに関する逐次的な深さ(特徴ベクトルの第3の数字)が図9の対応する状態素子のグループ化と比較して1を効率的に差し引いていることを除いて、特徴ベクトルはほぼ同じである。回路構成間の意図的または非意図的な合成差のために、設計を横切る対応する状態素子又はフロップは特徴ベクトルにおいてこのような小さな差を有する可能性がある。幾つかの実施形態では、ここで説明するプロセスはこれらの小さな差にもかかわらず状態素子をマップするための距離メトリックまたは距離アルゴリズムを使用できる。例えば1実施形態では、プロセスはユークリッド距離アルゴリズム、マンハッタン距離アルゴリズム、ハミング距離アルゴリズムまたは間に「些細な距離」を有するベクトルをグループ化するための別の適切な距離アルゴリズムを使用できる。
【0038】
図11は本発明の1実施形態による逐次的な深さのマッピングプロセスに関連されるマッピング性能における改良と、通常のマッピングツールとの比較を示すグラフである。各列では、グラフは逐次的な深さと通常のプロセスの両者がマップしたフロップ(例えば状態素子)の割合と、逐次的な深さのプロセスのみがマップされたフロップの割合と、通常のプロセスのみがマップされたフロップの割合と、逐次的な深さのマッチングプロセスも通常のマッピングツールもマップしないフロップの割合とを示している。3つの異なる回路設計の結果は各3つの列で示されている1つの回路設計により示されている。第1の回路設計はメモリアレイを形成しない約1000のフロップを含んでいる。第2の設計は半分に満たないフロップがメモリアレイで使用されている約10,000のフロップを含んでいる。第3の設計は大部分のフロップがメモリアレイで使用されている約27,000フロップを含んでいる。1つの通常のプロセスに加えて逐次的な深さのプロセスを使用することにより、24パーセントまでのより多くのフロップがマップされることができ、それによって包括的な等価検証のためのさらに良好なツールを与えることができる。
【0039】
通常、メモリアレイの状態素子はアドレスビットのマッピングが知られていないときには名前を付けることが困難である可能性がある。幾つかのケースでは、機能ツールの使用が多数のメモリアレイを含む回路に非常によく適している。幾つかの実施形態では、逐次的な深さのマッピングプロセスはしかしながらメモリアレイコンポーネントでのネーミングプロセスを非常に補助することができる。幾つかのケースでは、逐次的な深さのマッピングプロセスは構造的及び機能的の両方法を含んだプロセスで使用されることができる。
【0040】
前述の説明は本発明の多くの特定の実施形態を含んでいるが、これらは本発明の技術的範囲の限定として解釈されるべきではなく、その特別な実施形態の例として解釈されるべきである。したがって本発明の技術的範囲は示された実施形態ではなく請求項およびそれらの等価物によって決定されるべきである。

【特許請求の範囲】
【請求項1】
第1の回路と第2の回路との間の等価検証のために状態素子をマッピングする方法において、前記方法は、
(a)前記第1の回路と前記第2の回路の一次入力と一次出力から前記第1及び前記第2の回路の各状態素子までの第1の逐次的な深さを決定し、それにおいて前記第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントであり、
(b)特有の第1の逐次的な深さを有する前記第1の回路と前記第2の回路の第1の状態素子を識別してマッピングし、
(c)前記第1の回路と前記第2の回路の前記識別された第1の状態素子から前記残りの状態素子までの第2の逐次的な深さを決定し、
(d)特有の第2の逐次的な深さを有する前記第1の回路と前記第2の回路の第2の状態素子を識別してマッピングし、
(e)前記プロセスがもはや状態素子の新しい特有のマッピングを発生しない場合を除いて、前記(c)と(d)のステップを反復するステップを含んでいる方法。
【請求項2】
前記第1の回路と前記第2の回路の一次入力と一次出力から前記状態素子までの前記第1の逐次的な深さの決定は、
前記第1の回路の各前記一次入力と一次出力から前記第1の回路の各前記状態素子までの前記第1の逐次的な深さを決定し、
前記一次入力と一次出力から前記第2の回路の各前記状態素子までの前記第1の逐次的な深さを決定するステップを含んでいる請求項1記載の方法。
【請求項3】
前記特有の第1の逐次的な深さを有する前記第1の回路と前記第2の回路の前記第1の状態素子の識別してマッピングするステップは、
同一の第1の逐次的な深さを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記第1の状態素子を選択し、
同一の第1の逐次的な深さを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記第1の状態素子を選択し、
前記第1の回路と第2の回路の前記選択された第1の状態素子がほぼ同じ第1の逐次的な深さを有するならば、前記第1の回路の前記選択された第1の状態素子を前記第2の回路の前記選択された第1の状態素子へマッピングするステップを含んでいる請求項1記載の方法。
【請求項4】
前記第1の回路と前記第2の回路の前記識別された第1の状態素子から前記残りの状態素子までの前記第2の逐次的な深さの決定は、
前記第1の回路の前記識別された各第1の状態素子から前記第1の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定し、
前記第2の回路の前記識別された各第1の状態素子から前記第2の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定するステップを含んでいる請求項1記載の方法。
【請求項5】
前記特有の第2の逐次的な深さを有する前記第1の回路と前記第2の回路の第2の状態素子の識別及びマッピングは、
同一の第2の逐次的な深さを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記第2の状態素子を選択し、
同一の第2の逐次的な深さを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記第2の状態素子を選択し、
前記第1の回路と第2の回路の前記選択された第2の状態素子がほぼ同じ第2の逐次的な深さを有するならば、前記第1の回路の前記選択された第2の状態素子を前記第2の回路の前記選択された第2の状態素子へマッピングするステップを含んでいる請求項1記載の方法。
【請求項6】
前記プロセスがもはや状態素子の新しい特有のマッピングを発生しない場合を除いた(c)と(d)の前記反復は、(c)と(d)の連続的な反復が状態素子の新しい特有のマッピングを発生しないことを含んでいる請求項1記載の方法。
【請求項7】
前記第1の回路と前記第2の回路の一次入力と一次出力から前記状態素子までの前記第1の逐次的な深さの決定は、
前記第1の回路の各前記一次入力と一次出力から前記第1の回路の各前記状態素子までの前記第1の逐次的な深さを決定し、
前記一次入力と一次出力から前記第2の回路の各前記状態素子までの前記第1の逐次的な深さを決定するステップを含んでおり、
前記特有の第1の逐次的な深さを有する前記第1の回路と前記第2の回路の前記第1の状態素子の識別及びマッピングは、
同一の第1の逐次的な深さを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記第1の状態素子を選択し、
同一の第1の逐次的な深さを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記第1の状態素子を選択し、
前記第1の回路と第2の回路の前記選択された第1の状態素子がほぼ同じ第1の逐次的な深さを有するならば、前記第1の回路の前記選択された第1の状態素子を前記第2の回路の前記選択された第1の状態素子へマッピングするステップを含んでいる請求項1記載の方法。
【請求項8】
前記第1の回路と前記第2の回路の前記識別された第1の状態素子から前記残りの状態素子までの前記第2の逐次的な深さの決定は、
前記第1の回路の前記識別された各第1の状態素子から前記第1の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定し、
前記第2の回路の前記識別された各第1の状態素子から前記第2の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定するステップを含んでおり、
前記特有の第2の逐次的な深さを有する前記第1の回路と前記第2の回路の第2の状態素子の識別及びマッピングは、
同一の第2の逐次的な深さを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記第2の状態素子を選択し、
同一の第2の逐次的な深さを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記第2の状態素子を選択し、
前記第1の回路と第2の回路の前記選択された第2の状態素子がほぼ同じ第2の逐次的な深さを有するならば、前記第1の回路の前記選択された第2の状態素子を前記第2の回路の前記選択された第2の状態素子へマッピングするステップを含んでおり、
前記プロセスがもはや状態素子の新しい特有のマッピングを発生しない場合を除いて、(c)と(d)の前記反復は、(c)と(d)の連続的な反復が状態素子の新しい特有のマッピングを発生しない請求項7記載の方法。
【請求項9】
第1の回路と第2の回路との間の等価検証のため状態素子をマッピングする方法において、前記方法は、
(a)前記第1の回路と前記第2の回路の一次入力と一次出力から前記第1及び第2の回路の各状態素子までの第1の逐次的な深さを決定し、前記第1の逐次的な深さは回路の2つの点間の任意のパスに沿った状態素子の最小のカウントであり、
(b)前記各状態素子の前記第1の逐次的な深さに基づいて前記第1の回路と前記第2の回路の各状態素子の第1の特徴ベクトルを発生し、
(c)特有の第1のベクトルを有する前記第1の回路と前記第2の回路の状態素子を識別し、前記第1および第2の回路の前記識別された状態素子の前記第1の特徴ベクトルがほぼ同一であるならば、前記第1の回路の前記識別された状態素子を前記第2の回路の前期識別された状態素子へマッピングし、
(d)前記第1の回路と前記第2の回路の前記識別された第1の状態素子から前記残りの状態素子までの第2の逐次的な深さを決定し、
(e)前記識別された各状態素子の前記第2の逐次的な深さに基づいて前記第1の回路と前記第2の回路の識別された各状態素子の第2の特徴ベクトルを発生し、
(f)特有の第2のベクトルを有する前記第1の回路と前記第2の回路の状態素子を識別し、特有の第2のベクトルを有する前記第1及び第2の回路の前記識別された状態素子の前記第2の特徴ベクトルがほぼ同一であるならば、特有の第2のベクトルを有する前記第1の回路の前記識別された状態素子を特有の第2のベクトルを有する前記第2の回路の前記識別された状態素子へマッピングし、
(g)前記マッピングプロセスの終了のためのしきい値条件が満足されたか否かを決定するステップを含んでいる方法。
【請求項10】
前記マッピングプロセスの終了のためのしきい値条件が満足されたか否かの決定は、
前記マッピングプロセスの終了のための前記しきい値条件が満足されるまで(d)-(f)を反復するステップを含んでいる請求項9記載の方法。
【請求項11】
前記マッピングプロセスの終了のための前記しきい値条件が満足されるまで前記(d)-(f)を反復するステップは、
(d)-(f)の連続的な反復が状態素子の新しい特有のマッピングを発生しない請求項10記載の方法。
【請求項12】
前記第1の回路と前記第2の回路の一次入力と一次出力の前記第1の逐次的な深さの決定は、
前記第1の回路の各前記一次入力と一次出力から前記第1の回路の各前記状態素子までの前記第1の逐次的な深さを決定し、
前記第2の回路の前記一次入力と一次出力から前記第2の回路の各前記状態素子までの前記第1の逐次的な深さを決定するステップを含んでいる請求項9記載の方法。
【請求項13】
前記特有の第1のベクトルを有する前記第1の回路と前記第2の回路の前記状態素子の識別及び識別された状態素子のマッピングは、
ほぼ同一の第1のベクトルを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記第1の状態素子を選択し、
同一の第1のベクトルを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記第1の状態素子を選択し、
前記第1の回路と第2の回路の前記選択された状態素子の前記第1のベクトルがほぼ同じであるならば、前記第1の回路の前記選択された状態素子を前記第2の回路の前記選択された状態素子へマッピングするステップを含んでいる請求項9記載の方法。
【請求項14】
前記第1および第2の回路の前記選択された状態素子の前記第1の特徴ベクトルがほぼ同じであるならば、前記第1の回路の前記選択された状態素子を前記第2の回路の前記選択された状態素子へマッピングするステップは、前記第1の回路の第2のベクトルと前記第2の回路の第2のベクトルとの僅かな差を解くための距離アルゴリズムを使用することを含んでいる請求項13記載の方法。
【請求項15】
前記距離アルゴリズムはユークリッド距離アルゴリズム、マンハッタン距離アルゴリズム、ハミング距離アルゴリズムからなるグループから選択されたアルゴリズムを含んでいる請求項14記載の方法。
【請求項16】
前記残りの状態素子への前記第1の回路と前記第2の回路の前記識別された第1の状態素子の前記第2の逐次的な深さの決定は、
前記第1の回路の前記識別された各状態素子から前記第1の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定し、
前記第2の回路の前記識別された各状態素子から前記第2の回路の前記残りの各状態素子までの前記第2の逐次的な深さを決定するステップを含んでいる請求項9記載の方法。
【請求項17】
前記特有の第2のベクトルを有する前記第1の回路と前記第2の回路の状態素子の前記識別および識別された状態素子のマッピングは、
ほぼ同一の第2のベクトルを有する前記第1の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第1の回路の前記状態素子を選択し、
ほぼ同一の第2のベクトルを有する前記第2の回路の状態素子をグループ化し、
1つのグループカウントを有する前記第2の回路の前記状態素子を選択し、
特有の第2のベクトルを有する前記第1及び第2の回路の前記選択された状態素子の前記第2の特徴ベクトルがほぼ同じであるならば、特有の第2のベクトルを有する前記第1の回路の前記選択された状態素子を特有の第2のベクトルを有する前記第2の回路の前記選択された状態素子へマッピングするステップを含んでいる請求項9記載の方法。
【請求項18】
特有の第2のベクトルを有する前記第1及び第2の回路の前記選択された状態素子の前記第2の特徴ベクトルがほぼ同じであるならば、特有の第2のベクトルを有する前記第1の回路の前記選択された状態素子を特有の第2のベクトルを有する前記第2の回路の前記選択された状態素子へマッピングするステップは、前記第1の回路の第2のベクトルと前期第2の回路の第2のベクトルとの僅かな差を解くための距離アルゴリズムを使用することを含んでいる請求項17記載の方法。
【請求項19】
前記距離アルゴリズムはユークリッド距離アルゴリズム、マンハッタン距離アルゴリズム、ハミング距離アルゴリズムからなるグループから選択されたアルゴリズムを含んでいる請求項18記載の方法。

【図1】
image rotate

【図2】
image rotate

【図3】
image rotate

【図4】
image rotate

【図5】
image rotate

【図6】
image rotate

【図7】
image rotate

【図8】
image rotate

【図9】
image rotate

【図10】
image rotate

【図11】
image rotate


【公開番号】特開2012−164301(P2012−164301A)
【公開日】平成24年8月30日(2012.8.30)
【国際特許分類】
【外国語出願】
【出願番号】特願2011−257506(P2011−257506)
【出願日】平成23年11月25日(2011.11.25)
【出願人】(503455363)レイセオン カンパニー (244)
【Fターム(参考)】