(57)【要約】【課題】ブラックボックス化した回路は固定値信号が伝播しない。そのため、論理等価性検証時、およびテスト合成前後等で固定値信号の設定が必要な場合に、ブラックボックス化した回路が存在すると、ブラックボックス化した回路の後続の論理等価性検証ができない。【解決手段】出力に影響しない入力端子を判定する第１のステップと、信号が固定値に設定される外部入力との接続の有無を判定する第２のステップと、前記第２のステップにおいて前記外部入力と接続がない場合に、対象セルを、ユーザの指定、もしくは機能ブロックをもたない記述ファイルを読み込ませるブラックボックス化をする第３のステップと、前記第２のステップにおいて前記外部入力と接続がある場合に、前記対象セルを、論理等価性検証における検証ポイントとなり、かつ前記対象セルの後続の論理に影響を与える擬似論理回路に置換する第４のステップとを用いる。【選択図】図５
2007257440.tif 000002
【特許請求の範囲】
【請求項１】
２つの回路間の論理の等価性を検証する論理等価性検証方法であって、
出力に影響しない入力端子を判定する第１のステップと、
信号が固定値に設定される外部入力との接続の有無を判定する第２のステップと、
前記第２のステップにおいて前記外部入力との接続がない場合に、対象セルを、ユーザの指定もしくは機能ブロックをもたない記述ファイルを読み込ませてブラックボックス化する第３のステップと、
前記第２のステップにおいて前記外部入力との接続がある場合に、前記対象セルを、論理等価性検証における検証ポイントとなり、かつ前記対象セルの後続の論理に影響を与える擬似論理回路に置換する第４のステップと
を有することを特徴とする論理等価性検証方法。
【請求項２】
請求項１に記載の論理等価性検証方法であって、
前記第１のステップが、第１の入力端子を有する回路と、前記第１の入力端子にインバータを付加した入力端子を有する回路との論理等価性を検証するステップであることを特徴とする論理等価性検証方法。
【請求項３】
請求項１に記載の論理等価性検証方法であって、
前記擬似論理回路は、論理等価性検証の検証ポイントとなる第１の回路と、
前記擬似論理回路の第１の入力信号、および前記第１の回路の出力信号がそれぞれ入力されて、前記第１の入力信号と前記第１の回路の出力信号との論理積の信号を前記第１の回路へ出力する第２の回路と、
前記擬似論理回路の第２の入力信号が入力されて、前記第２の入力信号の逆論理の信号を出力する第３の回路と、
前記第２の入力信号、および前記逆論理の信号がそれぞれ入力されて、前記論理積の信号に応じて、前記第２の入力信号、又は前記逆論理の信号を出力する第４の回路と
を有することを特徴とする論理等価性検証方法。
【請求項４】
論理等価性検証の検証ポイントとなる第１の回路と、
前記擬似論理回路の第１の入力信号、および第１の回路の出力信号がそれぞれ入力されて、前記第１の入力信号と前記第１の回路の出力信号との論理積の信号を前記第１の回路へ出力する第２の回路と、
前記擬似論理回路の第２の入力信号が入力されて、前記第２の入力信号の逆論理の信号を出力する第３の回路と、
前記第２の入力信号、および前記逆論理の信号がそれぞれ入力されて、前記論理積の信号に応じて、前記第２の入力信号、又は前記逆論理の信号を出力する第４の回路と
を有することを特徴とする擬似論理回路。
【発明の詳細な説明】
【技術分野】
【０００１】
２つの回路間の論理の等価性を検証する論理等価性検証方法、および擬似論理回路に関する。
【背景技術】
【０００２】
集積回路の開発において、設計工程の途中で論理設計に誤りが混入しないことが重要である。そのために、最終的な集積回路が設計されるまでに、論理設計が正しく行えたかどうかの検証を行う。大規模な集積回路設計では、この論理検証の工数が増大しており、設計工数の全体の半分を論理検証工程が占めることがある。近年の数百万ゲートをもつような大規模集積回路（ＬＳＩ）の設計における論理検証では、論理検証ツールに高速性と高信頼性がより一層要求される。
【０００３】
このような論理検証が必要となる場面は、ゲート数や遅延時間等に関する、信号のタイミング調整や製造テストを行うためのテスト用スキャン回路（ＤｅｓｉｇｎＦｏｒ Ｔｅｓｔａｂｉｌｉｔｙ、以下ＤＦＴ回路）の挿入といった、論理仕様は変更せずに論理回路の実現構成を変更した場合である。その他に、論理合成、最適化、レイアウト設計、およびＥＣＯ(Ｅｎｇｉｎｅｅｒｉｎｇ ＣｈａｎｇｅＯｒｄｅｒ)等がある。このような回路構成の変更をインプリ工程とよび、このインプリ工程によって論理が変更されてしまう可能性が高い。そこで、インプリ工程前のスペック（Ｓｐｅｃｉｆｉｃａｔｉｏｎ）と称する論理回路と、インプリ工程後のインプリ（Ｉｍｐｌｅｍｅｎｔａｔｉｏｎ）と称する論理回路の論理が一致しているかどうかの検証を行い、論理設計の品質を高めることが行われている。このような検証を実現する技術を論理等価性検証技術とよび、これはＣＡＤ（ＣｏｍｐｕｔｅｒＡｉｄｅｄ ｄｅｓｉｇｎ）を用いた技術のひとつである（例えば、特許文献１を参照）。
【０００４】
ところで、ＬＳＩの論理設計は、一般にＨＤＬ（Ｈａｒｄｗａｒｅ Ｄｅｓｃｒｉｐｔｉｏｎ Ｌａｎｇｕａｇｅ）を用いて行われる。そして、このＨＤＬを用いて所望の回路構成のＲＴＬ（ＲｅｇｉｓｔｅｒＴｒａｎｓｆｅｒ Ｌｅｖｅｌ）記述を行い、次いで、このＲＴＬ記述を論理合成することで、ゲートレベルのネットリストへと変換する。このＲＴＬ記述とは、ラッチやフリップフロップといったレジスタと、その間に入る特定の機能を実現する組み合わせ回路とで構築された構造を表現したものである。また、ネットリストとは、論理の構造をゲート素子の論理式で表現したものである。論理等価性検証では、このような論理データがインプリ工程前後で比較される。
【０００５】
そして、２つのＬＳＩの論理比較は、ＬＳＩ内を論理コーンとよばれる論理等価性検証の基本単位に分割し、２つのＬＳＩの対応する論理コーンどうしの論理が一致するかどうかの検証を繰り返すことにより実行される。一般的には、回路をレジスタ等で分割することで、組み合わせ論理のみで構成される論理コーンに分割した後に、検証の対象となる２つの論理コーンの論理が等価であるかを、数学的に検証する。この論理コーンの頂点となるのは、フリップフロップ、ラッチ、外部出力、ブラックボックスモジュールの入力端子、およびカットポイント等といった信号の切り出しやすいポイントである。この論理コーンの頂点が検証ポイントとなり、検証ポイントから前段の検証ポイントまでバックトレースされた論理コーンどうしの論理の比較が、例えば、ＢＤＤ（Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）法、ＡＴＰＧ（Ａｕｔｏｍａｔｉｃ  Ｔｅｓｔ  Ｐａｔｔｅｒｎ  Ｇｅｎｅｒａｔｉｏｎ）法、およびＢＤＤ法とＡＴＰＧ法との組み合わせを用いて実行される（例えば、非特許文献１、２、３を参照）。
【０００６】
ただし、このような論理等価性検証では、２つの回路の論理が等価であると判定されたとしても、回路の動作やＬＳＩのタイミングが正しいことを保証しているわけではない。論理等価性検証とは、２つの回路が論理的に等価であるという保証を与える検証である。
【０００７】
ところで、システムＬＳＩにおいて、インターフェース回路を含んだ回路の論理等価性検証を行う場合には、使用するインターフェース回路に対応したセルライブラリを用いる。しかし、インターフェース回路ではダミーの論理が記述されているか、もしくは後続の論理が記述されていないオープン部分が多い。
また、システムＬＳＩの動作レベルの記述であるビヘイビア記述やアナログマクロ等は、デジタルで表現できないため、ＢＤＤ法やＡＴＰＧ法といった形式的論理等価性検証が適用できない。また、ＲＡＭのように論理の検証が不必要なモジュールも存在する。
【０００８】
以上述べたように、インターフェース回路や検査対象外のモジュールに接続される論理は、検証ポイントが設定されないために論理検証ができない。そこで、ユーザの指定、もしくは機能ブロックをもたない記述ファイルを実際のファイルの代わりに読み込ませることで、そのような部分をブラックボックス化する。ブラックボックス化された部分は検証ポイントとなるので、インターフェース回路や検査対象外のモジュールに接続される論理であっても、論理検証が可能となる。
【０００９】
また、出力信号に影響を与えないような回路は検証する必要がないことから、通常検査対象から外れる。
【００１０】
また、ＬＳＩ設計の流れの中では、前述したＤＦＴ回路の挿入後やレイアウト等といった部分的な回路変更を行った場合に、論理等価検証を行う。ここで、レイアウトとは、ネットリストを実際の集積回路の態様で配置したものであり、素子や配線の配置の効率性も考慮されている場合がほとんどである。
【００１１】
そして、例えば、このようなＤＦＴ回路の挿入前後での検証では、挿入したＤＦＴ回路を考慮せずに論理の等価性を検証するために、外部入力信号に固定値を設定したシステムモードとよばれる状態で論理検証するのが一般的である。
【００１２】
図１を用いて、ＤＦＴ回路の挿入を説明する。図１（ａ）には、同期式フリップフロップ（以下、ＦＦとする。）１０ａを示す。また、図１（ｂ）には、図１（ａ）のＦＦに対して、ＤＦＴ回路を挿入したＦＦ１０ｂを示す。
【００１３】
図１（ａ）のＦＦ１０ａは、ＣＬＯＣＫに入力される信号のタイミングに同期して、ＤＡＴＡに入力された信号がＱＵＩＴに出力される。
図１（ｂ）のＦＦ１０ｂには、図１（ａ）のＦＦ１０ａに対して、入力端子としてＳＣＡＮＩＮ、およびＳＣＡＮＭＯＤＥと、出力端子としてＳＣＡＮＯＵＴとが付加されている。また、ＤＡＴＡとＳＣＡＮＩＮとは、セレクタ１１に接続されている。このセレクタ１１に入力されるＳＣＡＮＭＯＤＥからの信号によって、ＤＡＴＡとＳＣＡＮＩＮの選択が行われる。この信号の選択は、ＴＡＰコントローラ１２の設定によって実行される。そして、ＳＣＡＮＩＮと、ＳＣＡＮＭＯＤＥと、ＳＣＡＮＯＵＴと、セレクタ１１と、ＴＡＰコントローラ１２と、およびそれらを接続する線とを、チップ上のＦＦなどに対して挿入することを、ＤＦＴ回路の挿入と称する。
【００１４】
図２を用いて、複数のＦＦに対するＤＦＴ回路の挿入を説明する。図２に、第１のＦＦ２０と、第２のＦＦ２１と、第１のセレクタ２２と、第２のセレクタ２３と、ＴＡＰコントローラ２４と、Ｉ／Ｏセル２５と、外部入力ピン２６とを示す。第１のＦＦ２０は、入力端子となるＤＡＴＡ２０、ＳＣＡＮＩＮ２０、ＳＣＡＮＭＯＤＥ２０、およびＣＬＯＣＫ２０と、出力端子となるＱＵＩＴ２０およびＳＣＡＮＯＵＴ２０とを有している。第２のＦＦ２１は、入力端子となるＤＡＴＡ２１、ＳＣＡＮＩＮ２１、ＳＣＡＮＭＯＤＥ２１、およびＣＬＯＣＫ２１と、出力端子となるＱＵＩＴ２１およびＳＣＡＮＯＵＴ２１とを有している。また、第１のＦＦ２０のＳＣＡＮＯＵＴ２０が、第２のＦＦのＳＣＡＮＩＮ２１に接続されている。また、第１のＦＦ２０のＤＡＴＡ２０とＳＣＡＮＩＮ２０との信号の切り替えを行うために、ＴＡＰコントローラ２４に接続されたＳＣＡＮＭＯＤＥ２０から第１のセレクタ２２に信号が入力される。また、第２のＦＦ２１のＤＡＴＡ２１とＳＣＡＮＩＮ２１との信号の切り替えを行うために、ＴＡＰコントローラ２４に接続されたＳＣＡＮＭＯＤＥ２１から、第２のセレクタ２３に信号が入力される。第１のセレクタ２２、および第２のセレクタ２３における信号の切り替えは、ＴＡＰコントローラ２４の設定と、ＴＡＰコントローラ２４に接続されている外部入力ピン２６に与えるテスト入力信号とを用いて実現する。また、外部入力ピン２６はＩ／Ｏセル２５と接続されて、ＴＡＰコントローラ２４や回路内部の素子と接続されている。
【００１５】
ＤＦＴ回路挿入前後の検証では、回路内の各ＦＦにおいてＤＡＴＡとＳＣＡＮＩＮとのどちらを選択するのかを、ＴＡＰコントローラ２４の設定と外部入力ピン２６とを用いて決定し、所望の検証を実行する。
【００１６】
ところで、論理等価性検証方法であって、回路合成によって追加された論理がある場合に、追加された論理の情報をもとに追加論理を削除して、論理等価性検証を行う方法が開示されている（例えば、特許文献２を参照）。
【特許文献１】特開２００４−２１３６０５号公報
【特許文献２】特開２００１−６７３７９号公報
【非特許文献１】ＦＵＪＩＴＳＵ.５０、６（１９９９）
【非特許文献２】Ｒ．Ｅ．Ｂｒｙａｎｔ、“Ｇｒａｐｈ−ｂａｓｅｄ  Ａｌｇｏｒｉｔｈｍｓ  ｆｏｒ  Ｂｏｏｌｅａｎ  Ｆｕｎｃｔｉｏｎ  Ｍａｎｉｐｕｌａｔｉｏｎ”、ＩＥＥＥ  Ｔｒａｎｓ．ｏｎ  Ｃｏｍｐｕｔｅｒｓ、Ｃ−３５、ｐｐ６７７−６９１
【非特許文献３】Ｐ．Ｒ．Ｓｔｅｐｈａｎ  ｅｔ  ａｌ、“Ｃｏｍｂｉｎａｔｉｏｎａｌ  Ｔｅｓｔ  Ｇｅｎｅｒａｒｉｏｎ  Ｕｓｉｎｇ  Ｓａｔｉｓｆｉａｂｉｌｉｔｙ”、ＩＥＥＥ  Ｔｒａｎｓ．ｏｎ  ＣＡＤ／ＩＣＡＳ、１５、９、ｐｐ１１６７−１１７６（１９９６）
【発明の開示】
【発明が解決しようとする課題】
【００１７】
以上述べたように、ブラックボックス化した回路は固定値信号が伝播しないため、論理等価性検証時に、信号が固定値に設定される場合に、ブラックボックス化した回路が存在すると、ブラックボックス化した回路の後続において論理等価性検証ができないという問題がある。
【課題を解決するための手段】
【００１８】
本発明は、２つの回路間の論理の等価性を検証する論理等価性検証方法であって、出力に影響しない入力端子を判定する第１のステップと、信号が固定値に設定される外部入力との接続の有無を判定する第２のステップと、前記第２のステップにおいて前記外部入力との接続がない場合に、対象セルを、ユーザの指定もしくは機能ブロックをもたない記述ファイルを読み込ませてブラックボックス化する第３のステップと、前記第２のステップにおいて前記外部入力との接続がある場合に、前記対象セルを、論理等価性検証における検証ポイントとなり、かつ前記対象セルの後続の論理に影響を与える擬似論理回路に置換する第４のステップとを有することを特徴とする。
【発明の効果】
【００１９】
信号が固定値に設定される場合であっても、検証ポイントとなり、かつ後続の論理に影響を与える擬似論理回路を用いることで、出力信号に影響を与えないダミーもしくはオープンとなる端子をもつ回路構成に後続する論理の検証が可能となる。また、出力信号に影響を与えないダミーもしくはオープンとなる端子をもつ回路構成を自動で検索することができる。
【発明を実施するための最良の形態】
【００２０】
図３を用いて、複数のフリップフロップ（以下、ＦＦとする）に対して、テスト用スキャン回路（Ｄｅｓｉｇｎ Ｆｏｒ Ｔｅｓｔａｂｉｌｉｔｙ、以下ＤＦＴ回路）の挿入を説明する。図３に、第１のＦＦ３０と、第２のＦＦ３１と、第１のセレクタ３２と、第２のセレクタ３３と、ＴＡＰコントローラ３４と、Ｉ／Ｏセル３５と、外部入力ピン３６とを示す。第１のＦＦ３０は、入力端子となるＤＡＴＡ３０、ＳＣＡＮＩＮ３０、ＳＣＡＮＭＯＤＥ３０、およびＣＬＯＣＫ３０と、出力端子となるＱＵＩＴ３０およびＳＣＡＮＯＵＴ３０とを有している。第２のＦＦ３１は、入力端子となるＤＡＴＡ３１、ＳＣＡＮＩＮ３１、ＳＣＡＮＭＯＤＥ３１、およびＣＬＯＣＫ３１と、出力端子となるＱＵＩＴ３１およびＳＣＡＮＯＵＴ３１とを有している。また、第１のＦＦ３０のＳＣＡＮＯＵＴ３０が、第２のＦＦのＳＣＡＮＩＮ３１に接続されている。また、第１のＦＦ３０のＤＡＴＡ３０とＳＣＡＮＩＮ３０との信号の切り替えを行うために、ＴＡＰコントローラ３４に接続されたＳＣＡＮＭＯＤＥ３０から第１のセレクタ３２に信号が入力される。また、第２のＦＦ３１のＤＡＴＡ３１とＳＣＡＮＩＮ３１との信号の切り替えを行うために、ＴＡＰコントローラ３４に接続されたＳＣＡＮＭＯＤＥ３１から、第２のセレクタ３３に信号が入力される。第１のセレクタ３２、および第２のセレクタ３３における信号の切り替えは、ＴＡＰコントローラ３４の設定と、ＴＡＰコントローラ３４に接続されている外部入力ピン３６に与えるテスト入力信号とを用いて実現する。また、外部入力ピン３６はＩ／Ｏセル３５と接続されて、ＴＡＰコントローラ３４や回路内部の素子と接続されている。
【００２１】
このように、ＳＣＡＮＩＮと、ＳＣＡＮＭＯＤＥと、ＳＣＡＮＯＵＴと、ＴＡＰコントローラと、それらの接続する線とを、チップ上のＦＦなどに対して挿入することを、ＤＦＴ回路の挿入、もしくはテスト合成と称する。ただし、ＤＦＴ回路の挿入は、図３に示す２つのＦＦの場合に限定されない。
【００２２】
ＤＦＴ回路挿入前後の検証では、回路内の各ＦＦにおいてＤＡＴＡとＳＣＡＮＩＮとのどちらを選択するのかを、ＴＡＰコントローラ３４の設定と外部入力ピン３６とを用いて決定し、所望の検証を実行する。
【００２３】
ところで、Ｉ／Ｏセル３５には外部入力ピン３６との接続以外にも入力があってもよく、その接続部分にダミーの論理が記述されている場合には、Ｉ／Ｏセル３５とＩ／Ｏセル３５に接続された回路３７との間の論理は論理等価性検証の対象とならない（例えば、図８を参照）。そこで、Ｉ／Ｏセル３５に接続された回路３７とＩ／Ｏセル３５との間の論理検証を行う場合には、ＣＡＤツール等でＩ／Ｏセル３５をブラックボックス化する方法、もしくはＩ／Ｏセル３５において、中身が記述されていないファイルを読み込ませることによって、Ｉ／Ｏセル３５をブラックボックス化する方法等を用いる。このブラックボックス化により、Ｉ／Ｏセル３５が検証ポイントに設定されて、Ｉ／Ｏセル３５までの回路３７の論理検証が可能となる。
【００２４】
なお、Ｉ／Ｏセル３５以外であっても、外部入力ピン３６と接続されて、外部入力ピン３６との接続以外にも入力端子を有しているセルにおいて、前記入力端子が前記セルの出力に影響しない構成であると、前記入力端子に回路３７が接続されている場合に、前記セルと回路３７との間の論理等価性検証ができない。そこで、前記セルを、Ｉ／Ｏセル３５と同様にブラックボックス化することで、論理検証が可能となる。
しかし、ブラックボックス化された回路は、一般に、その回路の中身が参照できないために固定値信号が伝播しない。すなわち、Ｉ／Ｏセル３５がブラックボックス化されていると、外部入力ピンに与えた固定値信号であるテスト入力信号が、外部入力ピン３６からＴＡＰコントローラ３４へ伝播しない。したがって、例えば、第１のセレクタ３２においてＤＡＴＡ３０とＳＣＡＮＩＮ３０とを選択するため信号を、ＳＣＡＮＭＯＤＥに与えることができない。これは、第２のＦＦにおいても同様である。
【００２５】
つまり、論理等価性検証時において信号が固定値に設定される場合には、ブラックボックス化した回路の後続に固定値信号が伝播せず、ブラックボックス化した回路に後続する論理の検証ができないという問題がある。
図４は、本発明を用いた論理等価性検証方法の実施例である。図４には、所望の論理を実現する回路デザインとセルライブラリとを選択するステップＳ４０、新しいセルライブラリを生成するステップＳ４１と、論理等価性検証のステップＳ４２とを示す。本発明では、ブラックボックス化したセルや擬似論理回路に置換したセルからなるライブラリがなければ、回路デザインと、ＤＦＴ回路挿入前後での固定値信号の設定とを与えて論理等価性検証を実行する前に、新しいセルライブラリを生成する処理を実行する。ここで、擬似論理回路とは、対象となるセルの回路構成に対して、検証ポイントとなり、かつ後続の論理に影響を与える回路を有する回路構成に変更した回路である。
一方で、すでに、ブラックボックス化したセルや擬似論理回路に置換したセルからなるライブラリがあれば、そのライブラリを用いて論理等価性検証を行う。
図５を用いて、図４に示した新しいセルライブラリを生成する処理Ｓ４１を、詳細に説明する。図５には、検証していない評価対象セルを選択する第１のステップＳ５１と、出力信号に影響しない入力端子があるかどうか判定する第２のステップＳ５２と、信号が固定値に設定される外部入力と接続するかどうかを判定する第３のステップＳ５３と、第３のステップの判定がＮＯの場合に、評価対象セルをブラックボックス化する第４のステップＳ５４と、第３のステップの判定がＹＥＳの場合に、評価対象セルを擬似論理回路に置換する第５のステップＳ５５と、全ての評価対象セルを検証したかどうかを判定する第６のステップＳ５６とを示す。
【００２６】
第１のステップＳ５１では、セルライブラリの中から評価対象セルを選択する。第２のステップＳ５２では、出力信号に影響のない端子が存在するかどうかを判定する。この第２のステップＳ５２の一例には、図６に示すようにインバータを挿入する方法があり、この方法は後述する。第３のステップＳ５３では、出力信号に影響を与えない端子に対して擬似論理回路を導入するか、もしくはブラックボックス化するかを決定する。論理等価性検証時において、注目している端子が、信号が固定値に設定される外部入力と接続しない場合には、第４のステップＳ５４のブラックボックス化へ進む。一方で、論理等価性検証時に、注目している端子が、信号が固定値に設定される外部入力と接続する場合には、第５のステップＳ５５である擬似論理回路の置換へ進む。ここで、第４のステップＳ５４であっても、第５のステップＳ５５であっても、注目している端子の接続先に検証ポイントが生成される。つまり、第３のステップＳ５３で対象となっている回路全てを、第５のステップＳ５５へ進ませることも可能である。しかし、機能ブロックをもたない記述ファイルを用いることで検証ポイントを生成できるブラックボックス化を用いると、検証の簡便性や検証時間短縮という効果がある。
【００２７】
ここから、第２のステップＳ５２と、第３のステップＳ５３と、および第５のステップＳ５５とを詳細に説明する。
【００２８】
図６を用いて、評価対象セル６０の１つの入力端子の前にインバータを付加しない場合（ａ）と、（ａ）とは同一の評価対象セル６０の１つの入力端子の前にインバータを付加する場合（ｂ）とを例に、第２のステップＳ５２を説明する。図６に、（ａ）には、評価対象セル６０と、入力端子ＩＮ（ａ）００および入力端子ＩＮ（ａ）０１と、出力端子ＯＵＴ（ａ）とからなる評価対象回路６２ａを示す。また、（ｂ）には、評価対象セル６０と、入力端子ＩＮ（ｂ）００および入力端子ＩＮ（ｂ）０１と、出力端子ＯＵＴ（ｂ）と、入力端子ＩＮ（ｂ）００に付加したインバータ６１とからなる評価対象回路６２ｂを示す。
【００２９】
評価対象回路６２ａと評価対象回路６２ｂとの回路構成の違いは、インバータ６１の有無だけである。したがって、評価対象セル６０に接続された出力端子ＯＵＴ（ｂ）からの出力が、評価対象セル６０に接続された入力端子ＩＮ（ａ）００への入力に依存するかどうかを判定するためには、評価対象回路６２ａと評価対象回路６２ｂとの論理等価性検証を実行すればよい。このとき、各評価対象回路への同一の入力に対して、評価対象回路６２ａと評価対象回路６２ｂとの論理が一致する場合には、入力端子ＩＮ（ａ）００は、出力端子ＯＵＴ（ｂ）に影響しないといえる。一方で、各評価対象回路への同一の入力に対して、評価対象回路６２ａと評価対象回路６２ｂとの論理が一致しない場合には、入力端子ＩＮ（ａ）００は、出力端子ＯＵＴ（ｂ）に影響するといえる。以上に述べた検証を、評価対象セル６０に接続された全ての入力端子に対して実行することにより、評価対象セル６０において、出力信号に影響しない入力端子があるかどうかの検証が可能となる。
【００３０】
図７に、評価対象セルを選択するステップＳ７０と、評価対象セルをインスタンスするステップＳ７１と、評価対象セルの一つの入力端子にインバータを付加してインスタンスするステップＳ７２と、論理等価性検証を実行して論理の不一致があるかどうかを判定するステップＳ７３と、ステップＳ７３の判定がＮＯの場合に、出力信号に影響しない入力端子として記憶するステップＳ７４と、全ての入力端子について検証したかどうかを判定するステップＳ７５と、出力信号に影響しない入力端子があるかどうかを判定するステップＳ７６とを示す。
図７に示す各ステップを用いた処理によって、図５の第２のステップＳ５２を実行する。ここで、図７と図５の第２のステップＳ５２との関係を詳細に述べると、図７のステップＳ７６の判定がＹＥＳの場合は、図５に示す第３のステップＳ５３へと処理が進む。一方で、ステップＳ７６の判定がＮＯの場合は、図５に示す第６のステップＳ５６へと処理が進む。このとき、ステップＳ７６の判定によって、出力信号に影響しない入力端子をもたないと判定されたセルは、そのままライブラリに格納される。
【００３１】
なお、本発明の実施において、Ｓ７５からＳ７２への処理を、Ｓ７５からＳ７１への処理と変更することもできる。また、Ｓ７５からＳ７１へ処理をループさせる場合には、Ｓ７１、およびＳ７２の順番は入れ替えることができる。
【００３２】
また、第２のステップＳ５２においてインバータを用いない方法には、全ての入力端子に対して、入力値の全ての組み合わせを入力する方法がある。ここで、全ての組み合わせとは、全ての入力端子に対する０（Ｌ：Ｌｏｗ）と１（Ｈ：Ｈｉｇｈ）との組み合わせ全てである。
【００３３】
次いで、第３のステップＳ５３は、設計データ等を用いて、信号が固定値に設定される外部入力と接続するかどうかを判定する。
【００３４】
図８と図９とを用いて、第５のステップＳ５５を説明する。
【００３５】
図８に、出力に影響を与えない回路の一例として、回路８０を示す。回路８０は、入力端子Ａ８およびＣ８と、出力端子Ｘ８と、双方向端子ＥＢ８とを接続するトライステート８３と、入力端子ＰＣ８と、それに接続する、ＮＡＮＤ回路８１およびＡＮＤ回路８２から成るダミーの論理回路と、以上の回路を接続する線とを有するライブラリセルである。回路８０において、出力端子Ｘ８からの出力は、入力端子ＰＣ８の入力に依存しない。したがって、入力端子ＰＣ８までの論理検証をする場合には、回路８０をブラックボックス化する必要がある。なお、回路８０では、出力端子Ｘ８からの出力が、入力端子ＰＣ８の入力に依存しない一例を示したに過ぎない。つまり、本発明を実施するにあたり、回路８０のＡＮＤ回路８１、および論理素子８２の構成に限定されない。
【００３６】
ところで、ブラックボックス化された回路８０には、固定値信号が伝播しない。そこで、回路８０が、信号が固定値設定される外部入力と接続する場合には、回路８０のＮＡＮＤ回路８１とＡＮＤ回路８２からなるダミーの論理回路部分を、図９に示す擬似論理回路９０へと置換する。
図９に、擬似論理回路９０と、入力端子Ａ８、Ｃ８およびＰＣ８と、出力端子Ｘ８と、双方向端子ＥＢ８と、トライステート８３とを示す。擬似論理回路９０はラッチ９１と、セレクタ９２と、ＡＮＤ回路９３と、インバータ９４と、以上の端子および回路を接続する線とを有する。
【００３７】
擬似論理回路９０の構成を、さらに詳細に述べる。擬似論理回路９０では、入力端子Ｒ９を含む２つの入力端子を有するラッチ９１の出力端子とＰＣ８とが、ＡＮＤ回路９３に接続されている。また、ＡＮＤ回路９３の出力端子がラッチ９１の入力端子Ｒ９でない入力端子に入力されている。また、ＡＮＤ回路９３の出力端子と、入力端子Ａ８と、Ａ８と接続されたインバータ９４の出力端子とが、セレクタ９２に接続されている。このセレクタ９２では、ＡＮＤ回路９３の出力端子からの信号を参照して、入力端子Ａ８からの信号と、Ａ８に接続されたインバータ９４の出力端子からの信号とを選択する。
【００３８】
擬似論理回路９０では、ラッチ９１が論理コーンの入力、かつ検証ポイントになる。つまり、図９に示す回路を含む論理コーンの論理等価性検証において、ラッチ９１の入力端子に接続する論理の値には影響されない入力値を用いた検証が可能となり、かつ、入力端子ＰＣ８から入る信号が０に固定化されるときに、ラッチ９１は論理等価性検証の対象外とすることができる。また、セレクタ９２において、ＰＣ８とラッチ９１との出力の論理積によって、入力端子Ａ８からの信号と入力端子Ａ８からの信号の反転との切り替えが実行される。
【００３９】
図９の擬似論理回路９０の動作を、さらに詳細に述べる。ここで、ＰＣ８に０が入力されると、入力端子Ａ８に与えられた信号が出力端子Ｘ８に出力される。一方で、ＰＣ８に１が入力されると、ラッチ９１の出力にしたがって入力端子Ａ８に与えられた信号か、その反転信号が出力端子Ｘ８に出力される。したがって、出力信号Ｘ８の値に入力端子ＰＣ８に与えられた信号が影響を与えるので、ＰＣ８に誤った論理が接続されていたときに不一致として検出される。すなわち、入力端子ＰＣ８までの論理の検証が可能となる。
【００４０】
併せて、入力端子Ａ８への信号が固定値に設定されている場合には、入力端子ＰＣ８にも信号が０となるような固定値信号を入力する。このとき、入力端子Ａに与えられた信号が出力端子Ｘ８に出力される。したがって、入力端子Ａ８に与えられている固定値信号の伝播が可能となる。また、このときラッチ９１は検証対象外となる。
【００４１】
図９の擬似論理回路９０と図８の回路８０とを、論理等価性検証の観点から比較すると、図９の擬似論理回路９０では、ラッチによって論理等価性検証の検証ポイントとなるポイントが設定され、入力端子ＰＣ８の信号が擬似論理回路９０の後続の論理に影響を与える回路を有している。また、ラッチ９１が論理コーンの入力になることで信号入力の自由度が向上する。
【００４２】
なお、本発明の第５のステップＳ５５を実行するにあたり、図９の擬似論理回路９０には限定されない。擬似論理回路として、検証ポイントとなり、かつ後続の論理に影響を与える回路であればよい。
【００４３】
以上述べたように、本発明によって、擬似論理回路へ置換されたセルやブラックボックス化されたセルから構成されるライブラリが作成される。そして、このライブラリをもとにして、論理等価性検証が実行される。これより、信号が固定値に設定される場合でも、擬似論理回路への置換によって、論理等価性検証が可能となる。
【産業上の利用可能性】
【００４４】
本発明は、ＬＳＩ設計における論理等価性検証に関して適用可能である。
【００４５】
以下、本発明の諸態様を付記としてまとめて記載する。
【００４６】
（付記１）２つの回路間の論理の等価性を検証する論理等価性検証方法であって、
出力に影響しない入力端子を判定する第１のステップと、
信号が固定値に設定される外部入力との接続の有無を判定する第２のステップと、
前記第２のステップにおいて前記外部入力との接続がない場合に、対象セルを、ユーザの指定もしくは機能ブロックをもたない記述ファイルを読み込ませてブラックボックス化する第３のステップと、
前記第２のステップにおいて前記外部入力との接続がある場合に、前記対象セルを、論理等価性検証における検証ポイントとなり、かつ前記対象セルの後続の論理に影響を与える擬似論理回路に置換する第４のステップと
を有することを特徴とする論理等価性検証方法。
【００４７】
（付記２）付記１に記載の論理等価性検証方法であって、
前記第１のステップが、第１の入力端子を有する回路と、前記第１の入力端子にインバータを付加した入力端子を有する回路との論理等価性を検証するステップであることを特徴とする論理等価性検証方法。
【００４８】
（付記３）付記１に記載の論理等価性検証方法であって、
前記擬似論理回路は、論理等価性検証の検証ポイントとなる第１の回路と、
前記擬似論理回路の第１の入力信号、および前記第１の回路の出力信号がそれぞれ入力されて、前記第１の入力信号と前記第１の回路の出力信号との論理積の信号を前記第１の回路へ出力する第２の回路と、
前記擬似論理回路の第２の入力信号が入力されて、前記第２の入力信号の逆論理の信号を出力する第３の回路と、
前記第２の入力信号、および前記逆論理の信号がそれぞれ入力されて、前記論理積の信号に応じて、前記第２の入力信号、又は前記逆論理の信号を出力する第４の回路と
を有することを特徴とする論理等価性検証方法。
【００４９】
（付記４）論理等価性検証の検証ポイントとなる第１の回路と、
前記擬似論理回路の第１の入力信号、および第１の回路の出力信号がそれぞれ入力されて、前記第１の入力信号と前記第１の回路の出力信号との論理積の信号を前記第１の回路へ出力する第２の回路と、
前記擬似論理回路の第２の入力信号が入力されて、前記第２の入力信号の逆論理の信号を出力する第３の回路と、
前記第２の入力信号、および前記逆論理の信号がそれぞれ入力されて、前記論理積の信号に応じて、前記第２の入力信号、又は前記逆論理の信号を出力する第４の回路と
を有することを特徴とする擬似論理回路。
【図面の簡単な説明】
【００５０】
【図１】フリップフロップ（１０ａ）（以下、ＦＦとする）に対して、テスト用スキャン回路（以下、ＤＦＴ回路とする）が挿入されたＦＦ（１０ｂ）を示す図である。
【図２】複数のＦＦに対して、ＤＦＴ回路が挿入された一例を示す図である。
【図３】複数のＦＦに対して、ＤＦＴ回路が挿入されており、ＴＡＰコントローラ３４と外部入力ピン３６とに接続されたＩ／Ｏセル３５の入力に、別の回路３７が接続されていることを示す図である。
【図４】本発明の一実施例を示す図である。
【図５】本発明の一実施例における、新しいセルライブラリを生成する処理工程を示す図である。
【図６】評価対象回路（６２ａ）と、評価対象回路（６２ａ）の入力端子のひとつにインバータが付加された回路（６２ｂ）を示す図である。
【図７】インバータを用いて、出力信号に影響しない入力端子があるかどうかを判定する修理工程を示す図である。
【図８】出力信号に影響しない入力端子があるセルを示す図である。
【図９】擬似論理回路を示す図である。
【符号の説明】
【００５１】
１０ａ：フリップフロップ（以下、ＦＦとする）
１０ｂ：テスト用スキャン回路（以下、ＤＦＴ回路とする）が挿入されたＦＦ
１１ｂ：ＤＡＴＡとＳＣＡＮＩＮとの選択をするセレクタ
１２：ＴＡＰコントローラ
２０：第１のＦＦ
２１：第２のＦＦ
２２：第１のＦＦのセレクタ
２３：第２のＦＦのセレクタ
２４：ＴＡＰコントローラ
２５：Ｉ／Ｏセル
２６：外部入力ピン
３０：第１のＦＦ
３１：第２のＦＦ
３２：第１のＦＦのセレクタ
３３：第２のＦＦのセレクタ
３４：ＴＡＰコントローラ
３５：Ｉ／Ｏセル
３６：外部入力ピン
３７：Ｉ／Ｏセルに接続された回路
Ｓ４０：デザインとセルライブラリとの選択をするステップ
Ｓ４１：新しいセルライブラリを生成するステップ
Ｓ４２：論理等価性検証を実行するステップ
Ｓ５１：検証していない評価セルを選択するステップ
Ｓ５２：出力信号に影響しない入力端子があるかどうかを判定するステップ
Ｓ５３：信号が固定値に設定される外部入力と接続するかどうかを判定するステップ
Ｓ５４：ブラックボックス化するステップ
Ｓ５５：擬似論理回路に置換するステップ
Ｓ５６：全ての評価対象セルについて検証したかどうかを判定するステップ
６０：評価対象セル
６１：インバータ
６２ａ：評価対象回路
６２ｂ：評価対象セル６０のひとつの入力端子の前にインバータが付加された評価対象回路
Ｓ７０：評価対象セルを選択するステップ
Ｓ７１：評価対象セルをインスタンスするステップ
Ｓ７２：評価対象セルのひとつの入力端子の前に、インバータを付加してインスタンスするステップ
Ｓ７３：論理等価性検証を実行して論理の不一致があるかどうかを判定するステップ
Ｓ７４：出力信号に影響しない入力端子として記憶するステップ
Ｓ７５：全ての入力端子について検証したかどうかを判定するステップ
Ｓ７６出力信号に影響しない入力端子があるかどうか判定するステップ
８０：Ｘ８からの出力信号に影響を与えない入力端子ＰＣ８を有する回路
８１：ＮＡＮＤ回路
８２：ＡＮＤ回路
８３：トライステート
９０：回路８０に対して、擬似論理回路を用いた回路
９１：ラッチ
９２：セレクタ
９３：ＡＮＤ回路
９４：インバータ
【図１】
2007257440.tif 000003
【図２】
2007257440.tif 000004
【図３】
2007257440.tif 000005
【図４】
2007257440.tif 000006
【図５】
2007257440.tif 000007
【図６】
2007257440.tif 000008
【図７】
2007257440.tif 000009
【図８】
2007257440.tif 000010
【図９】
2007257440.tif 000011