(57)【要約】【課題】  回路中にフィードバックループがある場合にも、効率よく論理等価性検証を行う。【解決手段】  回路動作を表現可能な回路記述を用いて、２つの回路の回路データ１０１、１０２を読み込む回路データ読み込み処理１０３と、階層の境界にバウンダリマークを挿入するバウンダリマーク挿入処理１０４と、バウンダリマークの情報を用いて組み合わせ回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを検証点として両論理回路の検証点の対応付けを行うループ切断機能付き検証点対応付け処理１０５と、検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、２つの論理回路の論理一致を出力させる論理等価性検証処理１０６とを行う。【選択図】  図１
2005038357.tif 000002
【特許請求の範囲】
【請求項１】
検証回路と参照回路の二つの各論理回路で各検証点を対応付け、その各検証点毎に論理が等価であるか否かを検証することにより、該各論理回路が論理的に等価であるか否かを判定する論理等価性検証装置であって、
該各論理回路の二つの各回路情報に対して階層の境界部分にバウンダリマークを挿入するバウンダリマーク挿入手段と、
該バウンダリマークを用いて該各論理回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを該検証点として該各論理回路で対応付けを行うループ切断機能付き検証点対応付け手段とを備えた論理等価性検証装置。
【請求項２】
前記各論理回路の動作を表現した回路記述から前記二つの各回路情報を読み込む回路データ読み込み手段を更に有し、前記バウンダリマーク挿入手段は、読み込まれた該二つの各回路情報に対して階層の境界部分にバウンダリマークを挿入する請求項１に記載の論理等価性検証装置。
【請求項３】
前記各論理回路で互いに対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、該各論理回路の論理一致信号を出力する論理等価性検証手段を更に有した請求項１または２に記載の論理等価性検証装置。
【請求項４】
前記バウンダリマーク挿入手段は、階層構造を有するデータに対しては、階層を展開しながら下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークを挿入する請求項１に記載の論理等価性検証装置。
【請求項５】
前記バウンダリマーク挿入手段は、階層名が保持されて階層展開されたフラットデータに対しては、保持されている階層名の違いから階層の境界を判断しながら、下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークを挿入する請求項１または４に記載の論理等価性検証装置。
【請求項６】
前記バウンダリマーク挿入手段は、階層データに対しては、階層の全ての境界にバウンダリマークを挿入する請求項１に記載の論理等価性検証装置。
【請求項７】
前記バウンダリマーク挿入手段は、階層名が保持されて階層展開されたフラットデータに対しては、ネット名と論理素子の端子名との階層名の違いから階層の境界を判断しながら、階層の全ての境界にバウンダリマークを挿入する請求項１または６に記載の論理等価性検証装置。
【請求項８】
前記ループ切断機能付き検証点対応付け手段は、階層の境界を示すバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断した切断点を新たな検証点として設定して、全ての検証点の対応付けを行う請求項１に記載の論理等価性検証装置。
【請求項９】
前記ループ切断機能付き検証点対応付け手段は、バウンダリマークのうち、ドライバー素子の出力端子に隣接するバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断した切断点を新たな検証点として設定して、全ての検証点の対応付けを行う請求項１に記載の論理等価性検証装置。
【請求項１０】
前記ループ切断機能付き検証点対応付け手段は、前記検証点毎に外部入力端子および検証点に繋がる組み合せ回路からなるロジックコーンを生成する請求項１に記載の論理等価性検証装置。
【請求項１１】
前記ループ切断機能付き検証点対応付け手段は、検証点毎のロジックコーンに対して共通の部分回路を括り出してサブロジックコーンを生成し、該サブロジックコーンの出力をサブ検証点として前記二つの各論理回路で対応付けを行う請求項１または３に記載の論理等価性検証装置。
【請求項１２】
前記ループ切断機能付き検証点対応付け手段は、前記二つの各論理回路で前記サブ検証点の対応付けがとれない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行う請求項１１に記載の論理等価性検証装置。
【請求項１３】
前記論理等価性検証手段は、前記二つの各論理回路において前記サブ検証点毎にサブロジックコーンをサブ回路対として論理比較を行い、論理比較によってサブ回路対で論理が一致しない場合には、階層を展開して、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行い、
該二つの各論理回路でサブ検証点の対応付けがとれ、かつ、論理比較によってサブ回路対で論理が一致したときに、そのサブ検証点を検証点として設定して、該二つの各論理回路において検証点毎にロジックコーンを回路対として論理比較を行う請求項１１または１２に記載の論理等価性検証装置。
【請求項１４】
検証回路と参照回路の二つの各論理回路が論理的に等価であるか否かを判定する論理等価性検証方法であって、
該各論理回路の動作を表現することができる回路記述を用いて、該各論理回路の二つの回路情報を読み込む回路データ読み込みステップと、
該各論理回路に対して、階層の境界部分にバウンダリマークを挿入するバウンダリマーク挿入ステップと、
各論理回路に対して、該バウンダリマークの情報を用いて組み合わせ回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを検証点として一方の論理回路と他方の論理回路との検証点の対応付けを行うループ切断機能付き検証点対応付けステップと、
該一方の論理回路と他方の論理回路とで対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、該二つの各論理回路の論理一致を出力させる論理等価性検証ステップとを有する論理等価性検証方法。
【請求項１５】
前記バウンダリマーク挿入ステップは、階層構造を有するデータに対しては、階層を展開しながら下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークの挿入を行い、階層名が保持されて階層展開されたフラットデータに対しては、保持されている階層名の違いから階層の境界部分を判断しながら、下位階層内にドライバー素子を有する階層の境界にバウンダリマークの挿入を行う請求項１４に記載の論理等価性検証方法。
【請求項１６】
前記バウンダリマーク挿入ステップは、階層データに対しては、階層の全ての境界部分にバウンダリマークの挿入を行い、階層名が保持されて階層展開されたフラットデータに対しては、ネット名と論理素子の端子名との階層名の違いから階層の境界部分を判断しながら、階層の全ての境界部分にバウンダリマークの挿入を行う請求項１４に記載の論理等価性検証方法。
【請求項１７】
前記ループ切断機能付き検証点対応付けステップは、階層の境界部分を示すバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定して、全ての検証点の対応付けを行う請求項１４に記載の論理等価性検証方法。
【請求項１８】
前記ループ切断機能付き検証点対応付けステップは、バウンダリマークのうち、ドライバー素子の出力端子に隣接するバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定して、全ての検証点の対応付けを行う請求項１４に記載の論理等価性検証方法。
【請求項１９】
前記ループ切断機能付き検証点対応付けステップは、検証点毎に外部入力端子および検証点に繋がる組み合せ回路からなるロジックコーンを生成する請求項１４に記載の論理等価性検証方法。
【請求項２０】
前記ループ切断機能付き検証点対応付けステップは、検証点毎のロジックコーンに対して共通の部分回路を括り出してサブロジックコーンを生成し、該サブロジックコーンの出力をサブ検証点として二つの各論理回路で対応付けを行う請求項１４に記載の論理等価性検証方法。
【請求項２１】
前記ループ切断機能付き検証点対応付けステップは、二つの各論理回路で前記サブ検証点の対応付けがとれない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行う請求項２０に記載の論理等価性検証方法。
【請求項２２】
前記論理等価性検証ステップは、前記二つの各論理回路において前記サブ検証点毎にサブロジックコーンをサブ回路対として論理比較を行い、論理比較によってサブ回路対で論理が一致しない場合には、階層を展開して、より上位のサブロジックコーンの出力をサブ検証点として二つの各論理回路で対応付けを行い、二つの各論理回路でサブ検証点の対応付けがとれ、かつ、論理比較によってサブ回路対で論理が一致したときに、そのサブ検証点を検証点として設定して、二つの各論理回路において検証点毎にロジックコーンを回路対として論理比較を行う請求項２０または２１に記載の論理等価性検証方法。
【請求項２３】
請求項１４〜２２のいずれかに記載の論理等価性検証方法の各処理手順をコンピュータに実行させるための制御プログラム。
【請求項２４】
請求項２３に記載の制御プログラムが記録されたコンピュータ読み出し可能な可読記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＬＳＩ（大規模集積回路）などの設計において、検証すべき回路（以下、検証回路という）と、ある基準回路（以下、参照回路という）とで検証点を対応付け、その検証点毎に論理が等価であるか否かを検証する論理回路等価検証装置、論理回路等価検証方法、この処理手順を実行するための制御プログラムおよびこれを記録した可読記録媒体に関する。
【背景技術】
【０００２】
近年、プロセスの微細加工技術の進歩に伴って、大規模な回路設計が可能になっている。このような大規模回路を設計するため、ハードウェア記述言語で表現された機能論理から論理回路を自動生成させる論理生成技術や、テスト回路を自動生成させるテスト合成技術や、消費電力を最適化するパワー合成技術などが実用化されて進展している。
【０００３】
また、配線の微細化に伴って、配線遅延が増大するため、セルの種類や配線の構造を変更させるゲートサイジング技術やクロックツリー合成技術などのように、配線遅延を考慮して回路を修正し、タイミングを最適化させる技術が実用化されて進展している。
【０００４】
このような回路の自動生成技術および自動修正技術では、セルのドライブ能力の変更や、論理の組み替えなどが行われるが、論理は変更させずに回路構成のみが変更される。このため、その関連技術として、回路構成の変更前と後とで論理が一致しているか否かを判定する論理等価性検証技術が不可欠となっている。
【０００５】
シミュレーションによる検証手法では、回路の大規模化に伴って十分な検証精度を有するテストパターンを生成することが困難になっている。また、十分な検証精度を有するテストパターンが得られても、膨大な長さのテストパターンとなり、シミュレーションに多くの時間を必要とする。
【０００６】
また、例えば順序回路を検証する場合、順序回路は内部状態を有するため、入力信号とレジスタの値で決定される回路の状態としては、各信号の値が”０”および”１”のみで表されるものとして、２のｘ乗（ｘは入力信号数＋レジスタ数）の状態が考えられる。この全状態をシミュレーションで検証することは非常に困難である。
【０００７】
このため、二つの論理回路を検証する際には、一般に、機能を数学的に表現して、基準（リファレンス；参照対象）となる論理回路（参照回路）の論理と、検証対象の論理回路（検証回路）の論理とを直接比較することによって、数学的に論理の等価性を検証する論理比較手法が用いられている。なお、回路構造の差を認識して検証する手法として、回路をノードとアークとで構成されたトポロジーと考え、論理を属性として与えて処理する方法も知られているが、本発明では、数学的に論理の等価性を検証する論理比較手法を採用しているため、ここではその詳細な説明は省略する。
【０００８】
論理比較手法では、組み合わせ回路の検証が対象とされており、組み合わせ回路に対して検証点の論理が作成され、それを比較することによって論理の等価性が検証される。このときの論理表現方法としては、２分決定グラフ（ＢＤＤ：Binary Decision Diagrams）を用いた技術が知られている。ＢＤＤは、入力変数の順序付けを行うことによって、等価な論理のＢＤＤ表現が一意的に決定されるという特徴を有している（非特許文献１参照）。組み合わせ回路に対して検証点の論理をＢＤＤとして表現することによって、容易に論理等価性を判定することができる。
【０００９】
また、順序回路は内部状態を有しており、論理の組み合わせの数が膨大なものとなって取り扱いが容易ではないため、論理比較手法では、順序回路が検証点で切断されて組み合せ回路（ロジックコーン）とレジスタ素子とに分割される。そして、検証点毎に参照回路と検証回路とで検証点の対応付けが行われて、組み合せ回路として論理等価性が検証される。
【００１０】
図１４は、従来の順序回路である参照回路および検証回路について、検証点の対応付けを説明するための模式図である。
【００１１】
図１４に示すように、まず、外部入力端子３０ａおよび外部出力端子３０ｂを有する順序回路で構成された参照回路および検証回路のそれぞれに対して、組み合せ回路で構成されるロジックコーン１０およびレジスタ素子２０に分割される。
【００１２】
次に、レジスタ素子２０の入力ピン２０ａおよび外部出力ピン３０ｂが検証点として設定され、図１４に点線で示すように検証点が参照回路と検証回路間において１対１に対応付けられている。その後、参照回路と検証回路とで、対応付けされた全ての検証点について、ロジックコーン１０およびレジスタ素子２０の論理等価性が検証される。
【００１３】
検証の対象となる参照回路および検証回路の検証点を１対１に対応付ける手法としては、例えば特許文献１に開示されているように、レジスタや外部入出力端子の名称による対応付け処理が一般的に行われている。また、例えば特許文献２には、名称によらず、効率よく対応付けを行う手法も提案されている。
【非特許文献１】S.Minatoet.al., “Shared Binary Decision Diagram with Attributed Edges for EfficientBoolean Function Manipulation”, Proc. of 27th DAC, pp.52-57, 1990.
【特許文献１】特開平８−２２４８５号公報
【特許文献２】特開平１０−３４０２７８号公報
【発明の開示】
【発明が解決しようとする課題】
【００１４】
上記従来の順序回路には、状態を保持するレジスタとして、フリップフロップ素子、ラッチ素子やメモリ素子などのレジスタ素子で構成されたものが含まれている。上述した論理比較手法では、順序回路がこのレジスタ素子の部分で切断され、組み合せ回路で構成されたロジックコーンおよびレジスタ素子が論理回路と検証回路とで対応付けられて論理等価性が検証される。
【００１５】
ところが、上記従来の組み合わせ回路中にフィードバックループが存在すると、レジスタ機能を有するラッチが構成されることがある。このような場合には、ループ上のネットを切断して組み合わせ回路に分割し、この切断点を新たな検証点とすることによって論理等価性検証を行うことが可能である。しかし、上記従来技術では、レジスタ素子間に存在する組み合せ回路で構成されたフィードバックループによるレジスタ（ラッチ）については対象外であり、レジスタ素子部分で切断されるため、このような組み合わせ回路中にフィードバックループが存在する回路については、適用することができないという問題がある。
【００１６】
また、参照回路と検証回路とで、論理が等価であっても回路構造に差がある場合には、ループ上のネットを切断する個所を参照回路と検証回路とで１対１に対応させることは容易でない。特に、多重ループが構成されている場合や、階層構造を有する回路データと、階層が展開されたフラットな回路データとを比較する場合のように、回路構造が大きく異なる場合などには、検証点を対応付けることができず、検証不能となって論理不一致として処理されるという問題がある。
【００１７】
本発明は、上記従来の問題を解決するもので、組み合わせ回路中にフィードバックループを有する回路の場合にも、効率よく論理等価性検証を行うことができる論理等価性検証装置、論理等価性検証方法、この処理手順を実行するための制御プログラムおよびこれを記録した可読記録媒体を提供することを目的とする。
【課題を解決するための手段】
【００１８】
本発明の論理等価性検証装置は、検証回路と参照回路の二つの各論理回路で各検証点を対応付け、その各検証点毎に論理が等価であるか否かを検証することにより、該各論理回路が論理的に等価であるか否かを判定する論理等価性検証装置であって、該各論理回路の二つの各回路情報に対して階層の境界部分にバウンダリマークを挿入するバウンダリマーク挿入手段と、該バウンダリマークを用いて該各論理回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを該検証点として該各論理回路で対応付けを行うループ切断機能付き検証点対応付け手段とを備えたものであり、そのことにより上記目的が達成される。
【００１９】
また、好ましくは、本発明の論理等価性検証装置において、各論理回路の動作を表現した回路記述から前記二つの各回路情報を読み込む回路データ読み込み手段を更に有し、前記バウンダリマーク挿入手段は、読み込まれた該二つの各回路情報に対して階層の境界部分にバウンダリマークを挿入する。
【００２０】
さらに、好ましくは、本発明の論理等価性検証装置において、各論理回路で互いに対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、該各論理回路の論理一致信号を出力する論理等価性検証手段を更に有している。
【００２１】
さらに、好ましくは、本発明の論理等価性検証装置におけるバウンダリマーク挿入手段は、階層構造を有するデータに対しては、階層を展開しながら下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークを挿入する。
【００２２】
さらに、好ましくは、本発明の論理等価性検証装置におけるバウンダリマーク挿入手段は、階層名が保持されて階層展開されたフラットデータに対しては、保持されている階層名の違いから階層の境界を判断しながら、下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークを挿入する。
【００２３】
さらに、好ましくは、本発明の論理等価性検証装置におけるバウンダリマーク挿入手段は、階層データに対しては、階層の全ての境界にバウンダリマークを挿入する。
【００２４】
さらに、好ましくは、本発明の論理等価性検証装置におけるバウンダリマーク挿入手段は、階層名が保持されて階層展開されたフラットデータに対しては、ネット名と論理素子の端子名との階層名の違いから階層の境界を判断しながら、階層の全ての境界にバウンダリマークを挿入する。
【００２５】
さらに、好ましくは、本発明の論理等価性検証装置におけるループ切断機能付き検証点対応付け手段は、階層の境界を示すバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断した切断点を新たな検証点として設定して、全ての検証点の対応付けを行う。
【００２６】
さらに、好ましくは、本発明の論理等価性検証装置におけるループ切断機能付き検証点対応付け手段は、バウンダリマークのうち、ドライバー素子の出力端子に隣接するバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断した切断点を新たな検証点として設定して、全ての検証点の対応付けを行う。
【００２７】
さらに、好ましくは、本発明の論理等価性検証装置におけるループ切断機能付き検証点対応付け手段は、前記検証点毎に外部入力端子および検証点に繋がる組み合せ回路からなるロジックコーンを生成する。
【００２８】
さらに、好ましくは、本発明の論理等価性検証装置におけるループ切断機能付き検証点対応付け手段は、検証点毎のロジックコーンに対して共通の部分回路を括り出してサブロジックコーンを生成し、該サブロジックコーンの出力をサブ検証点として前記二つの各論理回路で対応付けを行う。
【００２９】
さらに、好ましくは、本発明の論理等価性検証装置におけるループ切断機能付き検証点対応付け手段は、前記二つの各論理回路で前記サブ検証点の対応付けがとれない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行う。
【００３０】
さらに、好ましくは、本発明の論理等価性検証装置における論理等価性検証手段は、前記二つの各論理回路において前記サブ検証点毎にサブロジックコーンをサブ回路対として論理比較を行い、論理比較によってサブ回路対で論理が一致しない場合には、階層を展開して、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行い、該二つの各論理回路でサブ検証点の対応付けがとれ、かつ、論理比較によってサブ回路対で論理が一致したときに、そのサブ検証点を検証点として設定して、該二つの各論理回路において検証点毎にロジックコーンを回路対として論理比較を行う。
【００３１】
本発明の論理等価性検証方法は、検証回路と参照回路の二つの各論理回路が論理的に等価であるか否かを判定する論理等価性検証方法であって、該各論理回路の動作を表現することができる回路記述を用いて、該各論理回路の二つの回路情報を読み込む回路データ読み込みステップと、該各論理回路に対して、階層の境界部分にバウンダリマークを挿入するバウンダリマーク挿入ステップと、各論理回路に対して、該バウンダリマークの情報を用いて組み合わせ回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを検証点として一方の論理回路と他方の論理回路との検証点の対応付けを行うループ切断機能付き検証点対応付けステップと、該一方の論理回路と他方の論理回路とで対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、該二つの各論理回路の論理一致を出力させる論理等価性検証ステップとを有するものであり、そのことにより上記目的が達成される。
【００３２】
また、好ましくは、本発明の論理等価性検証方法におけるバウンダリマーク挿入ステップは、階層構造を有するデータに対しては、階層を展開しながら下位階層内にドライバー素子を有する階層の境界部分にバウンダリマークの挿入を行い、階層名が保持されて階層展開されたフラットデータに対しては、保持されている階層名の違いから階層の境界部分を判断しながら、下位階層内にドライバー素子を有する階層の境界にバウンダリマークの挿入を行う。
【００３３】
さらに、好ましくは、本発明の論理等価性検証方法におけるバウンダリマーク挿入ステップは、階層データに対しては、階層の全ての境界部分にバウンダリマークの挿入を行い、階層名が保持されて階層展開されたフラットデータに対しては、ネット名と論理素子の端子名との階層名の違いから階層の境界部分を判断しながら、階層の全ての境界部分にバウンダリマークの挿入を行う。
【００３４】
さらに、好ましくは、本発明の論理等価性検証方法におけるループ切断機能付き検証点対応付けステップは、階層の境界部分を示すバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定して、全ての検証点の対応付けを行う。
【００３５】
さらに、好ましくは、本発明の論理等価性検証方法におけるループ切断機能付き検証点対応付けステップは、バウンダリマークのうち、ドライバー素子の出力端子に隣接するバウンダリマークおよび検証点を起点とし、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定して、全ての検証点の対応付けを行う。
【００３６】
さらに、好ましくは、本発明の論理等価性検証方法におけるループ切断機能付き検証点対応付けステップは、検証点毎に外部入力端子および検証点に繋がる組み合せ回路からなるロジックコーンを生成する。
【００３７】
さらに、好ましくは、本発明の論理等価性検証方法におけるループ切断機能付き検証点対応付けステップは、検証点毎のロジックコーンに対して共通の部分回路を括り出してサブロジックコーンを生成し、該サブロジックコーンの出力をサブ検証点として二つの各論理回路で対応付けを行う。
【００３８】
さらに、好ましくは、本発明の論理等価性検証方法におけるループ切断機能付き検証点対応付けステップは、二つの各論理回路で前記サブ検証点の対応付けがとれない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として該二つの各論理回路で対応付けを行う。
【００３９】
さらに、好ましくは、本発明の論理等価性検証方法における論理等価性検証ステップは、前記二つの各論理回路において前記サブ検証点毎にサブロジックコーンをサブ回路対として論理比較を行い、論理比較によってサブ回路対で論理が一致しない場合には、階層を展開して、より上位のサブロジックコーンの出力をサブ検証点として二つの各論理回路で対応付けを行い、二つの各論理回路でサブ検証点の対応付けがとれ、かつ、論理比較によってサブ回路対で論理が一致したときに、そのサブ検証点を検証点として設定して、二つの各論理回路において検証点毎にロジックコーンを回路対として論理比較を行う。
【００４０】
本発明の制御プログラムは、請求項１４〜２２のいずれかに記載の論理等価性検証方法の各処理手順をコンピュータに実行させるためのものであり、そのことにより上記目的が達成される。
【００４１】
本発明の可読記録媒体は、請求項２３に記載の制御プログラムが記録されたコンピュータ読み出し可能なものであり、そのことにより上記目的が達成される。
【００４２】
以上の「入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定し」において、ネットとは一または複数のネットである。例えばフィードバックループを構成するネットを一つ検出するとそれを切断しているが、基本的には、例えばフィードバックループを構成する一または複数のネット全てを認識し、その中から適切なネットを選択し、切断する。例えば最下層のバウンダリマークからトレースすることにより、最初に見つけたネットを切断する手法で、不適切な切断点を選択することがないようにしている。したがって、「入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出し、検出されたネットを切断しその切断点を新たな検証点として設定し」は、「入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネット全てを検出し、検出されたネットの一本を切断し、その切断した切断点を新たな検証点として設定し」を含んでいる。
【００４３】
上記構成により、以下に、本発明の作用について説明する。
【００４４】
論理比較手法によって基準（リファレンス；参照対象）となる論理回路（参照回路）と、検証対象の論理回路（検証回路）とが論理的に等価であるか否かを検証する際には、基本的なアルゴリズムとして、
１）参照回路と検証回路とで検証点の対応付け
ａ）参照回路をロジックコーンおよびレジスタに分割する
ｂ）検証回路をロジックコーンおよびレジスタに分割する
ｃ）参照回路と検証回路とでロジックコーン（検証点）を対応付ける
２）参照回路と検証回路とでロジックコーンおよびレジスタ部分の論理等価性を検証する、
といった処理手順で検証が行われる。
【００４５】
本発明では、上記１）の各処理を３段階で行い、参照回路および検証回路に対して、回路データ読み込み処理、バウンダリマーク挿入処理、およびループ切断機能付き検証点の対応付け処理を行う。
【００４６】
まず、回路データ読み込み処理は、それぞれの論理回路の動作を表現することができる回路記述を用いて、二つの各回路情報を読み込むことによって行われる。
【００４７】
次に、バウンダリマーク挿入処理は、それぞれの各論理回路に対して、階層の境界部分にバウンダリマークを挿入することにより行われる。
【００４８】
バウンダリマークは、例えば、階層構造を有するデータに対しては、階層を展開しながら下位階層内にドライバー素子を有する階層の境界部分に挿入し、また、階層名が保持されて階層展開されたフラットデータに対しては、保持されている階層名の違いから階層の境界部分を判断しながら、下位階層内にドライバー素子を有する階層の境界部分に挿入する。
【００４９】
バウンダリマークは、ブロックの出力端子（検証点となる部分）に挿入することができるが、単純にブロックの出力端子に挿入すると、バウンダリマーク列が生成されてしまうため、ドライバー素子を有する階層の境界部分に挿入する。これによって、挿入されるバウンダリマークの数が減り、階層の境界情報を利用することができるため、参照回路と検証回路とで検証点やループ切断点の対応付けが容易となる。
【００５０】
または、バウンダリマークは、階層データに対しては、階層の全ての境界に挿入し、階層名が保持されて階層展開されたフラットデータに対しては、ネット名と論理素子の端子名との階層名の違いから階層の境界部分を判断しながら、階層の全ての境界部分に挿入する。
【００５１】
この場合、階層（ブロック）の境界部分に全てバウンダリマークが挿入されるため、検証点やループ検出の始点としては、ドライバー素子の出力端子に隣接するバウンダリマークのみを用いるように、バウンダリマークから候補を絞り込むようにする。これによって、挿入されるバウンダリマークの数は増えるが、処理量は特に増加されない。
【００５２】
階層構造を有する回路データはブロックで構成されており、それぞれのブロックは、ブロック（最下層はセル）とネットとで構成されている。また、ブロックの情報としては、ブロック情報（ブロック名、ブロックの入出力端子名と端子の方向性、セルの場合はセルの出力端子および内部状態毎の論理式など）、ブロックの接続情報（端子の接続）およびブロックの階層情報（親、兄弟、子）が含まれており、ネットの情報としては、ネット情報（ネットの接続）が含まれている。トップブロックの属性をみれば、ブロックの階層情報により、階層の有無を判断することができる。また、一般に、階層展開されたフラットデータにおいても階層名は保持されており、ユニークな番号がふられるようなことは少ないため、階層の境界を特定することができる。
【００５３】
このように階層構造を利用してバウンダリマークを挿入することによって、バウンダリマークを用いて階層の境界部分を特定することができ、このバウンダリマークの情報を用いてループ検出やロジックコーンの生成をも行うことができる。
【００５４】
階層構造を有するデータにおいて、階層展開を行う理由は、下位階層のないリーフセルで構成されたゲートレベルで回路を表現することができるからである。論理等価性検証手法には、階層のブロック単位で下位階層から検証する方法（階層検証方法）と、階層展開して（下位階層のない）リーフセルで構成されたフラットな回路で検証する方法（フラット検証方法）の２種類がある。階層検証方法では、参照回路と検証回路とで階層構造が一致している必要があり、検証途中の中間階層で差が生じた場合に処理が複雑になるという問題がある。例えば論理合成前後の検証のように、このような問題が生じない回路の検証時には、最下位の階層から検証する階層検証手法を用いて、階層を展開せずに同じ階層構造のまま処理することが適している。
【００５５】
一方、バッファ挿入などによるタイミング調整は、階層展開された後のフラットなネットリストに対して行われ、調整前の階層構造を有するデータと調整後の階層展開されたフラットなデータとが検証されることが多い。このような場合には、階層構造を有するデータを階層展開させてフラットなデータとして検証することが適している。また、階層展開して処理する手法の方が、より一般的な手法であり、論理合成の前後の検証にも適用することができる。但し、階層展開を行う場合には、データ量が増えるために使用メモリ量が増大する。
【００５６】
次に、ループ切断機能付き検証点対応付け処理では、それぞれの論理回路に対して、バウンダリマークの情報を用いて組み合わせ回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを検証点として一方の論理回路と他方の論理回路との検証点の対応付けが行われる。
【００５７】
検証点としては、レジスタ素子の入力端子と外部出力端子とが用いられる。検証点としてフリップフロップなどのようなレジスタ素子の入力端子が用いられるのは、順序回路をレジスタ部分で切断して、回路全体を、組み合せ回路（ロジックコーン）の集合とレジスタの集合とに分けるためである。組み合せ回路であれば、ＢＤＤ（binary disition diagram）で表現することができるため、論理比較を容易に行うことが可能である。
【００５８】
また、ブラックボックス素子は、論理が不明な素子として取り扱われ、この入力端子も検証点となる。例えば、メモリ素子はレジスタの塊であり、論理は記載されていない。このメモリ素子をレジスタとして処理しようとすると、例えば２５６Ｍｂｙｔｅのレジスタに分割させる必要がある。タイミング改善のための回路修正前後で検証を行う場合などには、メモリ素子が変更されることはないため、参照回路と検証回路とで同じメモリ素子を用いるという前提でブラックボックス素子として取り扱うことができる。
【００５９】
ここで、論理回路には、順序回路と組み合せ回路とがあり、大規模集積回路には、順序回路が含まれている。また、順序回路には状態を保持するレジスタが設けられており、レジスタにはフリップフロップ素子、ラッチ素子やメモリ素子などのようなレジスタ素子によって構成されたものと、フィードバック構造を有する組み合せ回路でレジスタ（ラッチ）が構成されたものとがある。
【００６０】
論理比較手法では、組み合せ回路の検証が行われる。順序回路を検証する場合には、状態の組み合せ数が膨大になるため、順序回路を組み合せ回路の集合とレジスタ素子の集合とに分割して検証が行われる。
【００６１】
従来技術では、論理回路がレジスタ素子部分で切断され、組み合せ回路で構成されたロジックコーンの集合とレジスタ素子の集合とに対して検証が行われる。この場合、フィードバック構造を有する組み合せ回路で構成されたレジスタ（ラッチ）については、レジスタ素子ではないため、対応することができない。
【００６２】
そこで、本発明では、ループ切断機能付き検証点対応付け処理において、階層の境界を示すバウンダリマーク（ドライバー素子を有する階層の境界部分に挿入されたもの、またはドライバー素子の出力端子に隣接するもの）および検証点を起点として、同一ネット上にバウンダリマークが複数挿入されている場合には下位階層から順にスキャンして、入力方向に検索手順に従って回路をトレースしてフィードバックループを構成するネットを検出する。検出されたネットを切断しその切断点を新たな検証点として設定し、全ての検証点の対応付けを行う。
【００６３】
このように、参照回路と検証回路とでバウンダリマークを用いることによって始点を一致させ、トレース方法を一致させることによって、ほぼ同一個所でループを切断させることができる。なお、ループ部分の論理構造が大幅に異なる場合には対応できないが、タイミング調整のための回路修正の場合には通常対応することができる。
【００６４】
また、ループ検証機能付き検証点対応付け処理では、検証点毎に外部入力端子および検証点に繋がる組み合せ回路からなるロジックコーンを生成し、検証点毎のロジックコーンに対して共通の部分回路を括り出してサブロジックコーンを生成し、サブロジックコーンの出力をサブ検証点として二つの論理回路で対応付けを行う。参照回路と検証回路とでサブ検証点の対応付けがとれない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として二つの論理回路で対応付けを行う。対応付けができれば、そのサブロジックコーンの出力をサブ検証点とする。
【００６５】
次に、論理等価性検証処理では、参照回路と検証回路とで対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較が行われ、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、二つの各論理回路の論理一致信号が出力される。
【００６６】
例えば、参照回路のロジックコーンに対応するＢＤＤを作成し、同様に、検証回路のロジックコーンに対応するＢＤＤを作成して、ＢＤＤ同士の比較を行うことによって、論理等価性を検証することができる。
【００６７】
ここで、等価であっても、論理の組み替えが行われた回路の検証を行う場合には、対応付けが行われたサブロジックコーンが全て等価になるという保証はない。例えば、サブロジックコーンの最終段のインバータの位置が、隣接するサブロジックコーンの初段に移動された回路との比較を行う場合に、そのサブロジックコーンと隣接するサブロジックコーンとの切れ目でネット名が対応付けられる場合などのように、サブロジックコーンが一致しない場合もある。
【００６８】
そこで、本発明では、論理等価性検証処理において、参照回路と検証回路とで検証点毎にロジックコーンを回路対として論理比較を行う前に、サブ検証点毎にサブロジックコーンをサブ回路対として論理比較を行う。論理比較によってサブ回路対で論理が一致しない場合には、階層を展開し、より上位のサブロジックコーンの出力をサブ検証点として二つの各論理回路で対応付けを行って、この上位のサブロジックコーンを検証対象とする。この上位のサブロジックコーンでもサブ回路対の論理が一致しない場合には、さらに上位のサブロジックコーンを検証対象とし、最終的にはサブロジックコーンなしで構成されたロジックコーンそのものを検証対象として、等価性検証を行う。
【発明の効果】
【００６９】
以上により、本発明によれば、階層の境界にバウンダリマークを挿入し、この情報に基づいて参照回路と検証回路とで１対１に対応する検証点を決定することによって、組み合わせ回路中にフィードバックループが存在する回路であっても、論理等価性検証を正確に行うことができる。
【００７０】
また、同一ネット上のバウンダリマークのトレース順と回路のトレース順とを規定することによって、階層をまたいで複雑なループが構成された回路に対しても、検証点を効率よく決定することができる。
【００７１】
さらに、回路の切断はループ部分のみであるため、一つの検証点当たりのロジックコーンの回路規模は保持され、さらに、共通部分をサブロジックコーンとして括り出すことにより、論理等価性検証処理の複雑化を抑えて、高速に検証処理を行うことができる。
【００７２】
さらに、検証点の対応付け処理のみを論理等価性検証の前処理として適用することによって、組み合わせ回路中にフィードバックループが存在してもループが切断されて検証点の対応付けができるため、従来技術を利用して回路の論理等価性を検証することができる。
【発明を実施するための最良の形態】
【００７３】
以下、本発明の論理回路等価性検証装置の実施形態について図面を参照しながら説明する。なお、ここでは、論理素子（プリミティブ）は、一般的なセルベースの設計を想定し、単に論理セルと表現している。
【００７４】
図１は本発明の論理回路等価性検証装置の一実施形態における要部構成を示すブロック図である。
【００７５】
図１において、この論理回路等価性検証装置１００は、コンピュータシステムで構成されており、可読記録媒体としての記憶部内の制御プログラムまたは可読記録媒体からインストールなど読み込まれた記憶部内の制御プログラムに基づいて、制御部としてのＣＰＵ（中央演算処理装置）が、後述する回路データ読み込み処理と、バウンダリマーク挿入処理と、ループ切断機能付き検証点対応付け処理と、論理等価性検証処理とを実行することにより、参照回路と検証回路の二つの各論理回路が論理的に等価であるか否かを判定する。
【００７６】
制御部（図示せず）は、参照回路の回路データ１０１と検証回路の回路データ１０２とを読み込む回路データ読み込み処理部１０３（回路データ読み込み処理手段）と、階層情報に基づいて階層の境界にバウンダリマークを挿入するバウンダリマーク挿入処理部１０４（バウンダリマーク挿入処理手段）と、組み合わせ回路のループを切断して参照回路と検証回路とで検証点の対応付けを行うループ切断機能付き検証点対応付け処理部１０５（ループ切断機能付き検証点対応付け処理手段）と、対応付けされた検証点毎に論理等価性検証を行って検証結果１０７を出力する論理等価性検証処理部１０６（論理等価性検証処理手段）とを有している。
【００７７】
以下に、それぞれの処理部について詳細に説明する。
【００７８】
まず、回路データ読み込み処理部１０３について説明する。
【００７９】
回路データ読み込み処理部１０３では、それぞれの論理回路の動作を表現することができる回路記述によって記述された参照回路の回路データ１０１と検証回路の回路データ１０２とが読み込まれる。
【００８０】
この回路データ読み込み処理部１０３については、従来技術と同様であるため、ここでは詳細な説明は省略する。
【００８１】
次に、バウンダリマーク挿入処理部１０４について説明する。
【００８２】
バウンダリマーク挿入処理部１０４では、回路データ読み込み処理部１０３で読み込まれたそれぞれの回路の回路データ１０１、１０２に対して、階層の境界にバウンダリマークが挿入される。
【００８３】
図２は、図１のバウンダリ挿入処理部１０４による処理手順を示すフローチャートである。この処理は、参照回路と検証回路とに対してそれぞれ行われる。
【００８４】
まず、ステップＳ１０１において、回路データ読み込み処理部１０３で読み込まれた回路データが階層構造を有するか否かが判断される。階層構造を有するデータ（階層データ）である場合（ＹＥＳ）と、階層構造を持たないデータ、例えば階層展開されたフラットなデータのように階層構造を持たないデータである場合（ＮＯ）とで、処理が分けられる。
【００８５】
読み込まれた回路データが階層データである場合（ＹＥＳ）には、ステップＳ１０２で子ブロックが順にスキャンされ、ステップＳ１０３で下位階層内にドライバーセルを有する階層の境界にバウンダリマークが挿入される。同一ネットに対して複数のバウンダリマークが挿入される場合には、識別可能なようにネット毎にグループ化される。
【００８６】
次に、ステップＳ１０４では、未処理の子ブロックがあるか否かが判断され、未処理の子ブロックがある場合（全ての子ブロックを処理したか。；ＮＯ）にはステップＳ１０２の処理に戻り、未処理の子ブロックがない場合（全ての子ブロックを処理したか。；ＹＥＳ）にはステップＳ１０５の処理に移行し、ステップＳ１０５で直下の全ての子ブロックの階層が展開される。
【００８７】
さらに、ステップＳ１０６では、子ブロックの階層展開後に新たな子ブロックがあるか否かが判断され、新たな子ブロックがある場合（新たな子ブロックがないか。；ＮＯ）にはステップＳ１０２の処理に戻り、新たな子ブロックがない場合（新たな子ブロックがないか。；ＹＥＳ）には処理が終了する。
【００８８】
一方、読み込まれた回路データが階層を持たないデータの場合（ＮＯ）には、ステップＳ１０７でネットが順にスキャンされて、ステップＳ１０８でネットの名称とそのネットに接続されている端子の名称とを順に取得する。
【００８９】
次に、ステップＳ１０９では、ネット名と端子名とで階層名が比較され、階層が異なる場合（ＹＥＳ）にはステップＳ１１０の処理において下位階層内にドライバーセルを有する階層の境界にバウンダリマークが挿入される。同一ネットに対して複数のバウンダリマークが挿入される場合には、識別可能なようにネット毎にグループ化される。
【００９０】
さらに、ステップＳ１１１では、未処理の端子があるか否かが判断され、未処理の端子がある場合（全ての端子を処理したか。；ＮＯ）にはステップＳ１０７の処理に戻り、未処理の端子がない場合（全ての端子を処理したか。；ＹＥＳ）にはステップＳ１１２の処理に移行して未処理のネットがあるか否かが判断され、未処理のネットがある場合（全てのネットを処理したか。；ＮＯ）にはスップＳ１０７の処理に戻り、未処理のネットがない場合（全てのネットを処理したか。；ＹＥＳ）には処理を終了する。
【００９１】
図３は、図２のバウンダリマークの挿入処理の一例を説明するための図である。
【００９２】
図３（ａ）に示すように、ドライバーセルｂ１〜ｂ３を有する階層（ブロック）ｈ１と、ドライバーセルｂ１およびｂ２を有する階層（ブロック）ｈ２とがある場合に、図３（ｂ）に示すように、下位階層内にドライバーセルを有する階層の境界に、ドライバーセルｂ２およびｂ３の出力端子に隣接してバウンダリマークｍ１およびｍ２が設けられる。バウンダリマークｍ１の挿入位置の候補としては、図３（ａ）に示すｍ１’の位置も挙げられるが、ドライバーセルｂ２の出力端子に隣接して図３（ｂ）に示すｍ１の位置にバウンダリマークが挿入される。
【００９３】
なお、ここでは、ドライバーセルを有する階層の境界にバウンダリマークが挿入されているが、階層の全ての境界にバウンダリマークを挿入して、後のループ切断機能付き検証点処理部１０５による処理時に、処理対象のバウンダリマークを絞り込むようにしてもよい。
【００９４】
次に、ループ切断機能付き検証点対応付け処理部１０５について説明する。
【００９５】
ループ切断機能付き検証点対応付け処理部１０５では、それぞれの論理回路に対して、バウンダリマーク挿入処理部１０４で挿入されたバウンダリマークの情報を用いて、組み合わせ回路のフィードバックループが切断されると共に、その切断点と、外部出力端子と、レジスタセルおよびブラックボックスセルの入力端子とを検証点として参照回路と検証回路との検証点の対応付けが行われる。
【００９６】
図４は、図１のループ切断機能付き検証点対応付け処理部１０５による処理手順を示すフローチャートである。
【００９７】
図４に示すように、まず、ステップＳ２０１において、外部出力端子と、レジスタセルおよびブラックボックスセルの入力端子とが検証点として設定される。この処理は、参照回路および検証回路のそれぞれに対して行われる。
【００９８】
次に、ステップＳ２０２において、バウンダリマーク処理部１０４で挿入されたバウンダリマークと検証点とを起点として、入力方向に、入力端子、バウンダリマークまたは検証点に到達するまで回路がトレースされる。
【００９９】
なお、バウンダリマークはネット毎にグループ化されており、同一ネット上に複数のバウンダリマークが挿入されている場合には、最下層のバウンダリマークから順に回路がトレースされる。また、バウンダリマーク挿入処理部１０５において、全ての階層の境界にバウンダリマークが挿入されている場合には、挿入されたバウンダリマークのうち、ドライバー素子の出力端子に隣接するバウンダリマークと検証点とが起点とされる。ループが検出された場合にはループ上のネットが切断され、切断点が新たな検証点として設定される。この処理は、参照回路および検証回路のそれぞれに対して行われる。
【０１００】
例えば、
入力  Ａ−−−−ＢＵＦ−−−−−−ＩＮＶ−−−−−−Ｙ  出力
（論理属性  ｆ＝ｉ）  （論理属性  ｆ＝ｎｏｔ（ｉ））
のような論理属性を有するセルで構成された回路では、ＹからＡに向かって回路がトレースされる。そのトレース結果を論理式で単純に表すと、
Ｙ＝ＩＮＶ（ＢＵＦ（Ａ））
となり、論理を簡単化すると、
Ｙ＝〜Ａ
となる。
【０１０１】
次に、ステップＳ２０３で検証点の対応付けが行われる。この処理は、参照回路と検証回路とで対応をとりながら行われる。
【０１０２】
さらに、ステップＳ２０４で検証点毎に外部入力端子および検証点に繋がる組み合わせ回路が抽出されて、ロジックコーンが生成される。この処理は、参照回路および検証回路のそれぞれに対して行われる。
【０１０３】
さらに、ステップＳ２０５で各ロジックコーンの共通部分が括り出されて、サブロジックコーンが生成され、サブロジックコーンの出力がサブ検証点として設定される。この処理は、参照回路および検証回路のそれぞれに対して行われる。
【０１０４】
さらに、ステップＳ２０６でサブ検証点の対応付けが行われる。サブ検証点の対応付けがとれない場合には、階層が展開され、より上位のサブロジックコーンの出力がサブ検証点として設定されて、対応付けが行われる。この処理は、参照回路と検証回路とで対応をとりながら行われる。
【０１０５】
図５は、図４の検証点設定処理Ｓ２０１の詳細を示すフローチャートである。
【０１０６】
外部出力端子と、レジスタセルおよびブラックボックスセルの入力端子とに対して検証点を設定する検証点設定処理ステップＳ２０１について詳細に説明する。
【０１０７】
図５に示すように、まず、ステップＳ２１１では外部端子が順にスキャンされる。
【０１０８】
ステップＳ２１２では、外部出力端子と外部双方向端子とが検証点として設定される。外部双方向端子は入力と出力とに分けられて、出力が検証点として設定される。
【０１０９】
さらに、ステップＳ２１３では、未処理の外部端子があるか否かが判断され、未処理の外部端子がある場合（全ての外部端子を処理したか。；ＮＯ）にはステップＳ２１１の処理に戻り、未処理の外部端子がない場合（全ての外部端子を処理したか。；ＹＥＳ）にはステップＳ２１４の処理に移行する。
【０１１０】
ステップＳ２１４ではセルが順にスキャンされる。
【０１１１】
ステップＳ２１５では、レジスタセルおよびブラックボックスセルの入力端子と双方向端子とが検証点として設定される。セルの入力端子は検証点として、セルの出力端子は外部入力端子として扱われ、双方向端子は入力と出力とに分けられて、入力が検証点として設定され、出力が外部入力端子として扱われる。
【０１１２】
ステップＳ２１６では未処理のセルがあるか否かが判断され、未処理のセルがある場合（全てのセルを処理したか。；ＮＯ）にはステップＳ２１４の処理に戻り、未処理のセルがない場合（全てのセルを処理したか。；ＹＥＳ）には、この検証点設定処理が終了する。
【０１１３】
図６は、図４に示すループ切断処理２０２の詳細を示すフローチャートである。
【０１１４】
ループ切断処理２０２では、バウンダリマーク処理部１０４で挿入されたバウンダリマークと検証点とを起点として、入力方向に、入力端子、バウンダリマークまたは検証点に到達するまで回路をトレースする。以下、詳細に説明する。
【０１１５】
まず、ステップＳ２２１において、バウンダリマークおよび検証点を起点としてネットを順にスキャンする。なお、グループ化された同一ネット上のバウンダリマークは、階層名により順序付けて下位階層のバウンダリマークから順にスキャンされる。
【０１１６】
次に、ステップＳ２２２では、起点のネットに接続された出力端子から入力側に、検索手順に従って回路がトレースされる。検索手順は、例えば、探索深さを優先して行われ、かつ、ネット名やセル名などの名称によって対応付けが可能であれば名称のソート順に行われる。
【０１１７】
ステップＳ２２３では、トレース済みのフラグを参照することによってトレース済みのネットであるか否かが判断され、既にトレース済みであれば（ＹＥＳ）、ステップＳ２２４でネットが切断されて切断点を新たな検証点として設定する。
【０１１８】
また、ステップＳ２２３で未トレースのネットであれば（ＮＯ）、トレース済みのフラグを設定する。
【０１１９】
さらに、ステップＳ２２６では、深さ優先の探索枝として未トレースのネットがあるか否かが判断され、入力側に未探索の枝（ネット）がある場合（全てトレースしたか；ＮＯ）にはステップＳ２２２の処理に戻って、未探索の枝（ネット）をトレース処理する。また、未探索の枝（ネット）が入力側にない場合には出力側に戻り、未探索の枝（ネット）があれば（全てトレースしたか；ＮＯ）、ステップＳ２２２に戻って、未探索の枝（ネット）をトレース処理する。
【０１２０】
ステップＳ２２６で未トレースのネットがなくなれば（全てトレースしたか；ＹＥＳ）、ステップＳ２２７で未処理のバウンダリマークおよび検証点のネットがあるか否かが判断され、未処理のバウンダリマークおよび検証点のネットがある場合（全てのマークを処理したか；ＮＯ）にはステップＳ２２１の処理に戻り、未処理のバウンダリマークおよび検証点のネットがない場合（全てのマークを処理したか；ＹＥＳ）には処理を終了する。
【０１２１】
次に、論理等価性検証処理部１０６について説明する。
【０１２２】
論理等価性検証処理部１０６では、参照回路と検証回路とで対応付けられた検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較が行われ、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、二つの論理回路の論理一致結果が信号出力される。
【０１２３】
この論理等価性検証処理部１０６において、参照回路と検証回路とで検証点毎にロジックコーンを回路対として論理比較を行う前に、サブ検証点毎にサブロジックコーンをサブ回路対として論理比較が行われる。論理比較によってサブ回路対で論理が一致しない場合には、階層が展開され、より上位のサブロジックコーンの出力をサブ検証点として二つの論理回路で対応付けが行われ、この上位のサブロジックコーンが検証対象とされる。この上位のサブロジックコーンで対応付けがとれない場合や、サブ回路対の論理が一致しない場合には、さらに上位のサブロジックコーンが検証対象とされ、最終的にはサブロジックコーンなしで構成されたロジックコーンそのものを検証対象として、等価性検証が行われる。二つの論理回路でサブ検証点の対応付けがとれ、かつ、論理比較によってサブ回路対で論理が一致したときに、そのサブ検証点が検証点として設定されて、二つの論理回路において検証点毎にロジックコーンを回路対として論理比較される。
【０１２４】
論理等価性の検証は、例えば、参照回路のロジックコーン（またはサブロジックコーン）に対応するＢＤＤを作成し、同様に、検証回路のロジックコーン（またはサブロジックコーン）に対応するＢＤＤを作成して、ＢＤＤ同士の比較を行うことによって行われる。この場合、レジスタ部分は一致するものとして、一致しない場合には検証点の対応付け時点で不一致とみなすことができる。また、ブラックボックス素子についても、参照回路と検証回路とで同じ素子であるか否かを検証し、一致しない場合には不一致とみなすことができる。ブラックボックス素子が一致している場合には、論理が不明であるため、この素子の前（入力端子部分）の論理が一致する（ブラックボックス素子を超える論理最適化がない）とみなして処理を行うことができる。また、参照回路と検証回路とでレジスタ部分やブラックボックス素子が一致しない場合には、例えば次段のロジックコーンにレジスタ部分の差を伝播させて、ロジックコーンのネットワーク全体で論理等価性を検証することもできる。
【０１２５】
なお、この論理等価性検証処理部１０６による論理比較については、従来技術と同様であるため、ここではその詳細な説明は省略する。
【０１２６】
次に、本実施形態の論理等価性検証方法について、回路例を用いて具体的に説明する。
【０１２７】
図７は、論理等価性が検証される回路の一例を示す回路図であって、図７Ａは検証の基準となる参照回路、図７Ｂは比較対象となる検証回路である。
【０１２８】
図７Ａに示す参照回路は階層構造を有するが、図７Ｂに示す検証回路が階層展開されたフラットな回路であるため、視覚的に対比させるために、トップから階層を透かして見た回路図を示している。
【０１２９】
図７Ａ中の点線で示す枠は中間階層を表しており、トップブロックＢＫ０の子ブロックとして、ＢＫ１、ＢＫ２およびＢＫ３が設けられている。ブロックＢＫ１は、三つのＮＡＮＤ論理ゲートセル２０４、２０５および２０７と、ドライバーセルとしてのバッファ２０６とによって組み合せ回路が構成され、ＮＡＮＤ論理ゲートセル２０５および２０７によってフィードバックループが構成されている。
【０１３０】
また、ブロックＢＫ２は、階層Ｈ１〜３の三つのＮＡＮＤ論理ゲートセル２０８、２０９および２１１と、ドライバーセルとしてのバッファ２１０および２１２とによって組み合せ回路が構成され、ＮＡＮＤ論理ゲートセル２０９および２１１によってフィードバックループが構成されている。
【０１３１】
さらに、ブロックＢＫ３は、ＮＯＲ論理ゲートセル２１３と、レジスタセルとしてのフリップフロップ２１４と、ドライバーセルとしてのバッファ２１２との直列接続によって組み合せ回路が構成されている。
【０１３２】
この図７Ａの参照回路には、外部端子として、外部入力端子Ｉ１〜Ｉ３およびＣＫと、外部出力端子Ｏ１、Ｏ２とが設けられている。外部入力端子ＣＫはクロック入力端子である。
【０１３３】
外部入力端子Ｉ１はブロックＢＫ１のＮＡＮＤ論理ゲートセル２０４の入力端子に接続され、外部入力端子Ｉ２はブロックＢＫ１のＮＡＮＤ論理ゲートセル２０４の入力端子と、ブロックＢＫ２のＮＯＲ論理ゲートセル２１３の入力端子とに接続され、外部入力端子Ｉ３はブロックＢＫ３のＮＯＲ論理ゲートセル２１３の入力端子に接続されている。
【０１３４】
また、外部入力端子であるクロック入力端子ＣＫはバッファ２０３を介してブロックＢＫ１のＮＡＮＤ論理ゲートセル２０７の入力端子と、ブロックＢＫ２のＮＡＮＤ論理ゲートセル２１１の入力端子と、ブロックＢＫ３のフリップフロップ２１４のクロック入力端子ＣＫと接続されている。
【０１３５】
また、外部出力端子Ｏ１はバッファ２０１を介してブロックＢＫ２のバッファ２１０の出力端子に接続され、外部出力端子Ｏ２はバッファ２０２を介してブロックＢＫ２のバッファ２１２の出力端子に接続されている。
【０１３６】
また、ブロックＢＫ２のバッファ２１０の出力端子とブロックＢＫ１のＮＡＮＤ論理ゲートセル２０４の入力端子とはネットＮ１によって接続されており、ブロックＢＫ１のバッファ２０６の出力端子とブロックＢＫ２のＮＡＮＤ論理ゲートセル２０８の入力端子とはネットＮ２によって接続されている。ブロックＢＫ３のバッファ２１５の出力端子と、ブロックＢＫ２のＮＡＮＤ論理ゲートセル２０８の入力端子とはネットＮ３によって接続されており、バッファ２０３の出力端子と、ブロックＢＫ２のＮＡＮＤ論理ゲートセル２１１の入力端子、ブロックＢＫ３のフリップフロップ２１４のクロック入力端子ＣＫト、ブロックＢＫ１のＮＡＮＤ論理ゲートセル２０７の入力端子とはネットＮ４によって接続されている。
【０１３７】
さらに、ブロックＢＫ１内において、ＮＡＮＤ論理ゲートセル２０４の出力端子とＮＡＮＤ論理ゲートセル２０５の入力端子とはネットＢＫ１／Ｎ１によって接続されており、ＮＡＮＤ論理ゲートセル２０５の出力端子と、ＮＡＮＤ論理ゲートセル２０７の入力端子およびバッファ２０６の入力端子とはネットＢＫ１／Ｎ２によって接続されており、ＮＡＮＤ論理ゲートセル２０７の出力端子とＮＡＮＤ論理ゲートセル２０５の入力端子とはネットＢＫ１／Ｎ３によって接続されている。
【０１３８】
ブロックＢＫ２内において、ＮＡＮＤ論理ゲートセル２０８の出力端子と、ＮＡＮＤ論理ゲートセル２０９の入力端子とはネットＢＫ２／Ｎ１によって接続されており、ＮＡＮＤ論理ゲートセル２０９の出力端子と、ＮＡＮＤ論理ゲートセル２１１の入力端子およびバッファ２１０の入力端子とはネットＢＫ２／Ｎ２によって接続されており、ＮＡＮＤ論理ゲートセル２１１の出力端子とＮＡＮＤ論理ゲートセル２０９の入力端子およびバッファ２１２ｂの入力端子とはネットＢＫ２／Ｎ３によって接続されている。
【０１３９】
ブロックＢＫ３において、ＮＯＲ論理ゲートセル２１３の出力端子と、フリップフロップ２１４のデータ入力端子ＤとはネットＢＫ３／Ｎ１によって接続されており、フリップフロップの出力端子Ｑとバッファ２１５の入力端子とはネットＢＫ３／Ｎ２によって接続されている。
【０１４０】
一方、図７Ｂの検証回路は、図７Ａの参照回路に対して、階層展開が行われ、ドライブ能力調整用バッファとしてバッファ２１６〜２１８が挿入された回路である。図７Ｂでは、挿入されたバッファ２１６〜２１８にハッチングを施して示している。
【０１４１】
図７Ｂにおいて、この検証回路は、階層名が保持されて階層展開されており、ネット名やセルの端子名から階層が異なることが分かる。例えば、ブロックＢＫ２のバッファ２１０とブロックＢＫ１のＮＡＮＤ論理ゲートセル２０４を接続するネット名はＮ１であり、バッファ２１０の端子名はＨ１／Ｈ２／Ｈ３／Ｙである。ここで、端子名Ｈ１〜Ｈ３は、階層毎に対応付けられている名称であり、Ｙはバッファの出力端子名（ネット名ではなくセルの端子名である）である。
【０１４２】
ブロック間を接続するネットＮ１の名称は、ブロックＢＫ２のバッファ２１０の出力端子からドライブ能力調整用バッファ２１６の入力端子まではＮ１、ドライブ能力調整用バッファ２１６の出力端子からブロックＢＫ２のＮＡＮＤ論理ゲートセル２０４の入力端子まではＮ１＿１とされている。また、ブロック間を接続するネットＮ４の名称は、バッファ２０３の出力端子からドライブ能力調整用バッファ２１８の入力端子まではＮ４、ドライブ能力調整用バッファ２１８の出力端子からドライバ能力調整用バッファ２１７の入力端子およびブロックＢＫ２のＮＡＮＤ論理ゲートセル２１１の入力端子まではＮ４＿１、ドライブ能力調整用バッファ２１７の出力端子からブロックＢＫ１のＮＡＮＤ論理ゲートセル２０７の入力端子、ブロックＢＫ３のフリップフロップ２１４のクロック入力端子ＣＫまではＮ４＿２としている。
【０１４３】
この図７の例では、参照回路（図７Ａ）と検証回路（図７Ｂ）とは論理的に等価であり、回路構造の差は、挿入されたドライバ能力調整用のバッファ部分のみである。
【０１４４】
これらの二つの回路が論理的に等価であるか否かの検証は、図１に示すように、回路データ読み込み処理部１０３、バウンダリマーク挿入処理部１０４、ループ切断機能付き検証点対応付け処理部１０５および論理等価性検証処理１０６によって行われる。
【０１４５】
ここで、回路データ読み込み処理部１０３および論理等価性検証処理部１０６については、従来手法と同様であるので、ここではその説明を省略し、本発明の特徴部分であるバウンダリマーク挿入処理部１０４およびループ切断機能付き検証点対応付け処理部１０５について、回路例を挙げて詳細に説明する。
【０１４６】
まず、バウンダリマーク挿入処理部１０４による処理について説明する。
【０１４７】
図８Ａは、図７Ａの参照回路に対して階層展開が行われ、階層の境界にバウンダリマークが挿入された後の回路例を示す図である。
【０１４８】
ここでは、ブロックＢＫ１、ＢＫ２およびＢＫ３の各ブロックの階層が展開され、下位階層内にドライバーセルを有する階層の境界（ネットＮ１、Ｎ２、Ｎ３およびＮ５上）にバウンダリマーク３０１〜３０４が挿入されている。この図８Ａでは、挿入されたバウンダリマークバッファ２１６〜２１８を菱形としてハッチングにより示している。
【０１４９】
例えばブロックＢＫ２において、バウンダリマークの挿入位置の候補としては、図７Ａに示すように、ブロックＨ３とＨ２との境界、ブロックＨ２とＨ１との境界、ブロックＨ１とその上位階層との境界の３箇所が考えられるが、ここでは下位階層内にドライバーセルを有するブロック（階層）Ｈ３とＨ２との階層の境界にバウンダリマーク３０３を挿入している。
【０１５０】
図８Ｂは、図７Ｂの検証回路に対して、階層の境界にバウンダリマークが挿入された後の回路例を示す図である。
【０１５１】
ここでも、図８Ａと同様に、下位階層内にドライバーセルを有する階層の境界（ネットＮ１、Ｎ２、Ｎ３およびＮ５上）にバウンダリマーク３０１〜３０４を挿入している。この図８Ｂでは、挿入されたバウンダリマークバッファ２１６〜２１８を菱形としてハッチングを施している。
【０１５２】
次に、ループ切断機能付き検証点対応付け処理１０５の処理について説明する。なお、ここでは、参照回路（図８Ａ）と検証回路（図８Ｂ）とで、同じ処理が行われるため、参照回路を代表として説明するが、検証回路についても同様の処理が行われるものとする。
【０１５３】
図９は、図８Ａの参照回路に対して、検証点設定処理によって、レジスタセルの入力端子が検証点に設定され、出力端子が外部入力端子とされた後の回路例を示す図である。
【０１５４】
図９において、レジスタセルとしてのフリップフロップ２１４の入力端子ＤおよびＣＫが外部出力端子３０５および３０６に変換され、フリップフロップ２１４の出力端子Ｑは外部入力端子３０７に変換され、これらが新たな検証点３０５〜３０７として設定されている。図９では、変換された外部入出力端子３０５〜３０７を三角形としてハッチングを施して示している。
【０１５５】
このように、フリップフロップ２１４の入出力端子を外部入出力端子に変換する理由は、順序回路をレジスタ部分で切断することによって、回路を組み合せ回路（ロジックコーン）の集合とレジスタセルの集合とに分けることができるからである。
【０１５６】
図１０は、図９の参照回路に対して、ループ切断処理によって、フィードバックループを構成するネットが切断され、切断点に外部入出力端子が挿入されて、これらが検証点として設定された後の回路例を示す図である。
【０１５７】
図１０において、ブロックＢＫ１のネットＢＫ１／Ｎ２が切断され、外部入力端子３０９および外部出力端子３０８が挿入されている。また、ブロックＢＫ２のネットＢＫ２／Ｎ２が切断され、それぞれ、外部入力端子３１１および外部出力端子３１０が挿入されている。図１０では、挿入された外部入出力端子３０８〜３１１を三角形としてハッチングを施して示している。
【０１５８】
このループ切断処理は、図６に示すフローチャートに従って処理される。ここでは、図９に示す回路のバウンダリマーク３０３を起点とした場合の例について説明する。
【０１５９】
バウンダリマーク３０３から入力方向に回路をトレースしてループが切断されるので、まず、バウンダリマーク３０３からバッファ２１０、ネットＢＫ２／Ｎ２、ＮＡＮＤ論理ゲートセル２０９、ネットＢＫ２／Ｎ１、ＮＡＮＤ論理ゲートセル２０８、ネットＮ２、バウンダリマーク３０１の順に回路がトレースされ、ネットＢＫ２／Ｎ２、ネットＢＫ２／Ｎ１およびネットＮ２に対してトレース済みのフラグが設定される。
【０１６０】
次に、ＮＡＮＤ論理ゲートセル２０８に戻り、ネットＮ３およびバウンダリマーク３０２の順に回路がトレースされ、ネットＮ３に対してトレース済みのフラグが設定される。
【０１６１】
さらに、ＮＡＮＤ論理ゲートセル２０９に戻り、ネットＢＫ２／Ｎ３、ＮＡＮＤ論理ゲートセル２１１およびネットＢＫ２／Ｎ２の順に回路がトレースされる。ここで、ネットＢＫ２／Ｎ２はトレース済みであるため、このネットが切断されて、図１０に示すように外部入力端子３１０および外部出力端子３１１が挿入され、新たな検証点として設定される。
【０１６２】
このように、階層の境界のバウンダリマークを起点として、同一ネット上のバウンダリマークは下位階層から順にスキャンし、探索手順として、例えば探索深さ優先で回路をトレースすることによって、参照回路と検証回路とで回路構造が同じであれば、ループネットの切断点を一致させることができる。また、参照回路と検証回路とで名称を対応付けられる場合には、探索手順として、名称でソートされた順に回路をトレースすることによって、参照回路と検証回路とで回路構造が異なる場合でも、ループ切断点をほぼ一致させることができる。これにより、簡単に参照回路と検証回路とで検証点の対応付けを行うことが可能になり、ループネットの切断点が異なるために検証点の対応付けが行えず、検証点の対応付けの段階で論理不一致とみなされることが少なくなる。
【０１６３】
図１１は、図１０の参照回路から、検証点毎に、検証点および外部入力端子に繋がる組み合せ回路で構成されるロジックコーンが生成された例を示す図である。
【０１６４】
例えば、図１１（ａ）では、検証点である外部出力端子Ｏ１と、切断されたネットＢＫ２／Ｎ２（外部入力端子３１１）とに繋がるロジックコーンが生成されている。
【０１６５】
図１１（ｂ）では、検証点である外部出力端子Ｏ２と、切断されたネットＢＫ２／Ｎ２（外部入力端子３１１）およびクロック入力端子ＣＫとに繋がるロジックコーンが生成されている。
【０１６６】
図１１（ｃ）では、切断されたネットＢＫ１／Ｎ２（外部出力端子３０８）と、切断されたネットＢＫ２／Ｎ２（外部入力端子３１１）、外部入力端子Ｉ１、Ｉ２、ネットＢＫ１／Ｎ２（外部入力端子３０９）およびクロック入力端子ＣＫとに繋がるロジックコーンが生成されている。
【０１６７】
図１１（ｄ）では、検証点であるネットＢＫ２／Ｎ２（外部出力端子３１０）と、ネットＢＫ１／Ｎ２（外部出力端子３０９）、ネットＢＫ３／Ｎ２（外部入力端子３０７）、ネットＢＫ２／Ｎ２（外部出力端子３１１）およびクロック入力端子ＣＫとに繋がるロジックコーンが生成されている。
【０１６８】
図１１（ｅ）では、検証点であるネットＢＫ３／Ｎ１（外部出力端子３０５）と、外部入力端子Ｉ２およびＩ３とに繋がるロジックコーンが生成されている。
【０１６９】
図１１（ｆ）では、外部入力端子ＣＫと、ネットＮ４（外部出力端子検証点である外部出力端子３０６）とに繋がるロジックコーンが生成されている。
【０１７０】
図１２は、図１１に示すロジックコーンに対して、共通の部分回路がサブロジックコーンとして括り出された例を示す図である。各ロジックコーン中、四角で囲まれた部分がサブロジックコーンを示している。
【０１７１】
図１２（ａ）および図１２（ｃ）に示すロジックコーンでは、サブロジックコーンＳ３が共通の部分回路となっている。
【０１７２】
図１２（ｂ）および（ｄ）に示すロジックコーンでは、サブロジックコーンＳ２が共通の部分回路となっている。
【０１７３】
図１２（ｂ）、（ｃ）、（ｄ）および（ｆ）に示すロジックコーンでは、サブロジックコーンＳ１が共通の部分回路となっている。
【０１７４】
図１３は、図１２で括り出されたサブロジックコーンが取り出され、ロジックコーンがサブロジックコーンと組み合わせ回路とによって再構成された例を示す図である。
【０１７５】
例えば図１３（ａ）では、検証点である外部出力端子Ｏ１に対するロジックコーンが、論理ゲートセル２０１とサブロジックコーンＳ３とによって構成されている。
【０１７６】
図１３（ｂ）では、検証点である外部出力端子Ｏ２に対するロジックコーンが、論理ゲートセル２０２および２１２とサブロジックコーンＳ２とによって構成されている。
【０１７７】
図１３（ｃ）では、検証点であるネットＢＫ１／Ｎ２（外部出力端子３０８）に対するロジックコーンが、論理ゲートセル２０５、２０４および２０７と、入力端子Ｉ１、Ｉ２およびネットＢＫ１／Ｎ２（検証点３０９）と、サブロジックコーンＳ３およびＳ１とによって構成されている。
【０１７８】
図１３（ｄ）では、検証点であるネットＢＫ２／Ｎ２（外部出力端子３１０）に対するロジックコーンが、論理ゲートセル２０９、２０８、２０６および２１５と、ネットＢＫ１／Ｎ２（入力端子３０９）およびネットＢＫ３／Ｎ２（入力端子３０７）と、サブロジックコーンＳ２とによって構成されている。
【０１７９】
図１３（ｅ）では、検証点であるネットＢＫ３／Ｎ１（外部出力端子３０５）に対するロジックコーンが、論理ゲートセル２１３と、入力端子Ｉ２およびＩ３とによって構成されている。
【０１８０】
図１３（ｆ）では、サブロジックコーンＳ１が、出力ネットＮ４と、論理ゲートセル２０３と、入力端子ＣＫとによって構成されている。
【０１８１】
図１３（ｇ）では、サブロジックコーンＳ２が、出力ネットＢＫ２／Ｎ３と、論理ゲートセル２１１と、出力ネットＢＫ２／Ｎ２（入力端子３１１）と、サブロジックコーンＳ１とによって構成されている。
【０１８２】
図１２（ｈ）では、サブロジックコーンＳ３が、出力ネットＮ１と、論理ゲートセル２１０と、出力ネットＢＫ２／Ｎ２（入力端子３１１）とによって構成されている。
【０１８３】
括り出されたサブロジックコーンＳ１〜Ｓ３の出力ネットは、サブ検証点として設定される。
【０１８４】
検証回路に対しても、参照回路と同様に、一連の処理が行われ、検証点の対応付けが行われる。全ての検証点の対応付けが取れなければ、論理不一致が出力される。また、サブロジックコーンのサブ検証点についても、対応付けが行われ、対応付けられたものだけがサブロジックコーンとして扱われる。対応付けが取れなかったものについては、サブロジックコーンが階層展開され、上位のサブロジックコーンでサブ検証点の対応付けが行われる。
【０１８５】
参照回路と検証回路とで、対応付けられたサブ検証点のサブロジックコーンに対して検証が行われ、論理が一致しなかったものについては、サブロジックコーンが階層展開されて、上位のサブロジックコーンでサブ検証点の対応付けが行われる。サブロジックコーンの論理が一致すれば、サブロジックコーンとして扱われ、参照回路と検証回路とで、対応付けられた検証点のロジックコーンに対して検証が行われる。全ての検証点の組み合わせ回路対で論理が一致すれば、論理等価性検証処理部１０６から、論理一致結果が出力される。
【０１８６】
ロジックコーンを構成する共通の部分回路はサブロジックコーンとして括り出されているので、サブロジックコーンの対応付けが可能であれば、一度検証されたサブロジックコーンを再度検証する必要がなく、効率良く検証を行うことができる。
【０１８７】
以上により、本実施形態によれば、論理等価性検証装置１００は、制御プログラムに基づいて、回路動作を表現可能な回路記述を用いて、二つの回路の回路データ１０１、１０２を読み込む回路データ読み込み処理と、階層の境界にバウンダリマークを挿入するバウンダリマーク挿入処理と、バウンダリマークの情報を用いて組み合わせ回路のフィードバックループを切断すると共に、その切断点と外部出力端子とレジスタ素子およびブラックボックス素子の入力端子とを検証点として両論理回路の検証点の対応付けを行うループ切断機能付き検証点対応付け処理と、検証点毎に組み合せ回路で構成されるロジックコーンを回路対として論理比較を行い、全ての検証点の対応付けがとれ、かつ、論理比較によって全ての回路対で論理が一致したときに、二つの論理回路の論理一致を出力させる論理等価性検証処理とを実行する。これによって、フィードバックループがある場合や回路構造が大きく異なる場合にも、効率よく論理等価性検証を行うことができる。
【産業上の利用可能性】
【０１８８】
ＬＳＩ（大規模集積回路）などの設計において、検証すべき回路（以下、検証回路という）と、ある基準回路（以下、参照回路という）とで検証点を対応付け、その検証点毎に論理が等価であるか否かを検証する論理回路等価検証装置および論理回路等価検証方法の分野において、回路中にフィードバックループがある場合にも、効率よく論理等価性検証を行うことができる。
【図面の簡単な説明】
【０１８９】
【図１】本発明の論理等価性検証装置の実施形態における要部構成を示すブロック図である。
【図２】図１のバウンダリマーク挿入処理部による各処理手順を示すフローチャートである。
【図３】（ａ）および（ｂ）はそれぞれ、バウンダリマークの挿入例について説明するための図である。
【図４】図１のループ切断機能付き検証点対応付け処理部による各処理手順を示すフローチャートである。
【図５】図４の検証点設定処理の各処理手順を示すフローチャートである。
【図６】図４のループ切断処理の各処理手順を示すフローチャートである。
【図７Ａ】本発明により論理等価性検証を行うための検証の基準となる参照回路の回路図である。
【図７Ｂ】本発明により論理等価性検証を行うための比較対象となる検証回路の回路図である。
【図８Ａ】本発明により論理等価性検証を行うための参照回路に対してバウンダリマーク挿入後の回路例を示す回路図である。
【図８Ｂ】本発明により論理等価性検証を行うための検証回路に対してバウンダリマーク挿入後の回路例を示す回路図である。
【図９】本発明により論理等価性検証を行うための参照回路に対して、フリップフロップの入出力端子を外部入出力端子に変換した例を示す回路図である。
【図１０】本発明により論理等価性検証を行うための参照回路に対して、ループを切断して切断点を外部入出力端子に変換した例を示す回路図である。
【図１１】（ａ）〜（ｆ）はそれぞれ、検証点毎のロジックコーンの本発明の構成例を示す図である。
【図１２】（ａ）〜（ｆ）はそれぞれ、ロジックコーン内の共通の部分回路の本発明の構成例を示す図である。
【図１３】（ａ）〜（ｈ）はそれぞれ、ロジックコーン内の共通の部分回路をサブロジックコーンとして括りだした本発明の構成例を示す図である。
【図１４】順序回路である参照回路と検証回路とで対応する検証点の関係を説明するための模式図である。
【符号の説明】
【０１９０】
１０１  回路データ（参照回路）
１０２  回路データ（検証回路）
１０３  回路データ読み込み処理部
１０４  バウンダリマーク挿入処理部
１０５  ループ切断機能付き検証点対応付け処理部
１０６  論理等価性検証処理部
１０７  検証結果（データ）
２０１〜２１５  論理ゲートセル
２１６〜２１８  論理ゲートセル（ドライブ能力調整用バッファ）
３０１〜３０４  バウンダリマーク
３０５〜３０７  フリップフロップの入出力端子から変換した外部入出力端子
３０８〜３１１  ループ切断点から変換された外部入出力端子
Ｓ１、Ｓ２、Ｓ３  サブロジックコーン
【図１】
2005038357.tif 000003
【図２】
2005038357.tif 000004
【図３】
2005038357.tif 000005
【図４】
2005038357.tif 000006
【図５】
2005038357.tif 000007
【図６】
2005038357.tif 000008
【図７Ａ】
2005038357.tif 000009
【図７Ｂ】
2005038357.tif 000010
【図８Ａ】
2005038357.tif 000011
【図８Ｂ】
2005038357.tif 000012
【図９】
2005038357.tif 000013
【図１０】
2005038357.tif 000014
【図１１】
2005038357.tif 000015
【図１２】
2005038357.tif 000016
【図１３】
2005038357.tif 000017
【図１４】
2005038357.tif 000018