(57)【特許請求の範囲】
【請求項１】
階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部端子を検証点 として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証装置において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力手段と、
前記中間形式を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子に関する情報である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理手段と、
前記階層展開中間形式から比較対象とする前記検 証点を抽出し検証点情報を出力する検証点抽出手段と、
前記階層展開中間形式及び前記検証点情報を参照し前記階層切り口端子情報を用いて前記前記検証対象論理回路を部分回路に分割して部分回路データを生成する回路分割手段と、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証手段と、
前記比較検証手段による検証結果を判断する検証結果判断部と、
前記検証結果の判断結果不一致の場合前記階層展開中間形式の前記階層切り口端子情報を用いて前記部分回路データから部分回路情報を抽出する部分回路情報抽出手段と、
前記検証結果を出力する検証結果出力手段とを備えることを特徴とする論理回路検証装置。
【請求項２】
前記階層展開処理手段で生成した前記階層展開中間形式に対し定数伝播処理を行うための定数伝播処理手段を備えることを特徴とする請求項１記載の論理回路検証装置。
【請求項３】
階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部端子を検証点 として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証装置において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力手段と、
前記中間形式を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子に関する情報である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理手段と、
前記階層展開中間形式から比較対象とする前記検 証点を抽出し検証点情報を出力する検証点抽出手段と、
前記階層展開中間形式及び前記検証点情報を参照し前記階層切り口端子情報を用いて前記前記検証対象論理回路を部分回路に分割して部分回路データを生成する回路分割手段と、
前記回路分割手段での回路分割後に前記部分回路データに前記階層切り口端子に関してその入力側の部分回路の持つ論理情報を前記階層切り口端子に記憶させる処理を行う部分回路情報抽出手段と、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証手段と、
前記比較検証手段による検証結果を判断する検証結果判断部と、
前記検証結果を出力する検証結果出力手段とを備えることを特徴とする論理回路検証装置。
【請求項４】
前記階層切り口端子情報が、前記階層展開処理のときに前記部分回路データに設定したバッファに保存することを特徴とする請求項１又は３記載の論理回路検証装置。
【請求項５】
階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部端子を検証点 として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証プログラムを格納した記憶媒体において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対象とする検証点 を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路データを再度参照し前記階層展開中間形式の階層切り口端子情報を用いて新たな部分回路情報を抽出する部分回路情報抽出ステップとを有することを特徴とする論理回路検証プログラムを格納した記憶媒体。
【請求項６】
前記階層展開処理ステップで生成した前記階層展開中間形式に対し定数伝播処理を行うための定数伝播処理ステップを有することを特徴とする請求項８記載の論理回路検証プログラムを格納した記憶媒体。
【請求項７】
階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部端子を検証 点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証プログラムを格納した記憶媒体において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対象とする検証点 を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記回路分割ステップの後に前記部分回路データに前記階層切り口端子に関してその入力側の部分回路の持つ論理情報を前記階層切り口端子に記憶させる処理を行う部分回路情報抽出ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップとを有し、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路情報抽出ステップで前記階層切り口端子に記憶させてある前記論理情報を利用して再度比較検証ステップで再検証を行うことを特徴とする論理回路検証プログラムを格納した記憶媒体。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は論理回路検証装置及び論理回路検証方法及び論理回路検証プログラムを格納した記録媒体に関し、特に論理回路の形式検証における論理等価性を検証するための論理回路検証装置及び論理回路検証方法及び論理回路検証プログラムを格納した記録媒体に関する。
【０００２】
【従来の技術】
従来２つの論理回路の等価性を検証するには、これら２つの検証対象の論理回路における論理が等価とみなす個所を、フリップフロップなどのレジスタや、外部切り口端子に注目して回路を部分回路に分割し、信号名などの情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証していた。
【０００３】
部分回路毎の論理等価性の検証には、ＢＤＤ（２分決定グラフ：ＢｉｎａｌｙＤｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍｓ）を用いることが多い。
【０００４】
ＢＤＤは入力変数の順序付けを行えば、等価な論理のＢＤＤ表現を一意に決定できるため、これを利用して論理の等価性を検証する。
【０００５】
近年では、回路をＶＨＤＬ（ＩＥＥＥ１０７６）やＶｅｒｉｌｏｇ−ＨＤＬ（ＩＥＥＥ１３６４）などのハードウェア記述言語を用いて記述し、より大規模な回路を記述するために、回路を特定の機能毎に複数の階層分割して記述し、論理合成ツールにより論理回路を自動生成する方法が一般的に行われている。
【０００６】
この論理合成時に、回路をより最適化するために、対象回路が複数の階層から成る場合にはこれら複数の階層を同時に最適化を行う。また、対象回路の上位階層が定数情報を持つ場合には、この定数情報を上位階層から下位階層へ伝播させることにより、簡単化することが要求されている。
【０００７】
同様に、一部部分の論理を他の階層に移動させることで他の階層内の論理を簡単化することや、階層内の配置配線精度の向上させることも要求されている。
【０００８】
一般的な従来の第１の論理回路検証方法においては、この要求に応じた回路の最適化を行なった場合の等価性検証を行う例について、最適化前の回路１００を示す図３及び最適化後の回路４００を示す図７を参照すると、これら両回路１００，４００の論理検証方法としては、階層毎に検証を行う。
【０００９】
回路１００及び回路４００の各々の下層（ＳＵＢ）階層２０１，２０１Ａにおける検証点としてレジスタであるフリップフロップ２１２の入力端子Ｇをそれぞれ検証点４０１，４０１Ａとし、各々の論理をブール式で示すと、それぞれ式（１），（２）で表される。
【００１０】
回路１００：Ｇ＝Ｄ＊Ｅ  ・・・・・・・・・・・・・・・・・・・（１）
回路４００：Ｇ＝Ｄ  ・・・・・・・・・・・・・・・・・・・・・（２）
従って、一致判定により、このまま式（１）、（２）を比較すると論理的に不一致であると判定してしまう。
【００１１】
このように、従来の第１の論理回路検証方法では、階層を跨いだ定数の伝播などの影響を考慮した検証を行うことができないことが問題であった。
【００１２】
このため、特開平１０−６３７０７号公報記載の従来の第２の論理回路検証方法では、最適化前の回路１００及び最適化後の回路４００を、それぞれ図１４に示す回路７００及び図１５に示す回路８００のように、複数の階層を１つの階層に展開し、もともとの検証点であるフリップフロップの入力端子Ｇに相当する検証点７０１，８０１について、論理検証を行っていた。
【００１３】
検証点７０１，８０１の各々の論理をブール式で示すと、それぞれ次式で表される。
【００１４】
回路７００：ＳＵＢ／Ｇ＝ＳＵＢ／Ｆ  ・・・・・・・・・・・・・・（３）
ＳＵＢ／Ｆ＝Ｃ＊１  ・・・・・・・・・・・・・・・・・・・・・・（４）
Ｃ＝Ａ＊Ｂ  ・・・・・・・・・・・・・・・・・・・・・・・・・・（５）
式（３）〜（５）を要約すると、
ＳＵＢ／Ｇ＝Ａ＊Ｂ  ・・・・・・・・・・・・・・・・・・・・・・（６）
回路８００：ＳＵＢ／Ｇ＝Ｃ  ・・・・・・・・・・・・・・・・・・（７）
Ｃ＝Ａ＊Ｂ  ・・・・・・・・・・・・・・・・・・・・・・・・・・（８）
式７，８を要約すると、
ＳＵＢ／Ｇ＝Ａ＊Ｂ  ・・・・・・・・・・・・・・・・・・・・・・（９）
従来の第２の論理回路検証方法は、式（６），（９）を比較することにより、論理的に一致すると判定していた。
【００１５】
この結果、階層を展開することにより検証すべき部分回路が大きくなるために、部分回路の検証時に用いるＢＤＤで表現する場合に、必要なメモリ量が大きくなるという問題がある。
【００１６】
【発明が解決しようとする課題】
上述した従来の第１の論理回路検証装置及び論理回路検証方法は、対象回路が複数の階層から成る場合には、階層を跨いだ定数の伝播などの影響を考慮した検証を行うことができないという欠点があった。
【００１７】
上記欠点の解消を図った従来の第２の論理回路検証装置及び論理回路検証方法は、階層を展開することにより検証すべき部分回路が大きくなるために、部分回路の検証時に用いるＢＤＤで表現する場合に、必要なメモリ量が大きくなるという欠点があった。
【００１８】
本発明の目的は、階層を跨いだ最適化を行った回路についても検証可能とし、より少ないメモリ量で検証する論理回路検証装置及び論理回路検証方法を提供することにある。
【００１９】
【課題を解決するための手段】
請求項１記載の発明の論理回路検証装置は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証装置において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力手段と、
前記中間形式を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子に関する情報である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理手段と、
前記階層展開中間形式から比較対照とする前記検証点を抽出し検証点情報を出力する検証点抽出手段と、
前記階層展開中間形式及び前記検証点情報を参照し前記階層切り口端子情報を用いて前記前記検証対象論理回路を部分回路に分割して部分回路データを生成する回路分割手段と、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証手段と、
前記比較検証手段による検証結果を判断する検証結果判断部と、
前記検証結果の判断結果不一致の場合前記階層展開中間形式の前記階層切り口端子情報を用いて前記部分回路データから部分回路情報を抽出する部分回路情報抽出手段と、
前記検証結果を出力する検証結果出力手段とを備えて構成されている。
【００２０】
また、請求項２記載の発明は、請求項１記載の論理回路検証装置において、前記階層展開処理手段で生成した前記階層展開中間形式に対し定数伝播処理を行うための定数伝播処理手段を備える構成とするものである。
【００２１】
また、請求項３記載の発明の論理回路検証装置は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証装置において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力手段と、
前記中間形式を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子に関する情報である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理手段と、
前記階層展開中間形式から比較対照とする前記検証点を抽出し検証点情報を出力する検証点抽出手段と、
前記階層展開中間形式及び前記検証点情報を参照し前記階層切り口端子情報を用いて前記前記検証対象論理回路を部分回路に分割して部分回路データを生成する回路分割手段と、
前記回路分割手段での回路分割後に前記部分回路データに前記階層切り口端子に関してその入力側の部分回路の持つ論理情報を前記階層切り口端子に記憶させる処理を行う部分回路情報抽出手段と、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証手段と、
前記比較検証手段による検証結果を判断する検証結果判断部と、
前記検証結果を出力する検証結果出力手段とを備えて構成される。
【００２２】
さらに、請求項４記載の発明は、請求項１又は３記載の論理回路検証装置において、前記階層切り口端子情報が、前記階層展開処理のときに前記部分回路データに設定したバッファに保存することを特徴とするものである。
【００２３】
請求項５記載の発明の論理回路検証方法は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証方法において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対照とする検証点を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路データを再度参照し前記階層展開中間形式の階層切り口端子情報を用いて新たな部分回路情報を抽出する部分回路情報抽出ステップとを有することを特徴とするものである。
【００２４】
また、請求項６記載の発明は、請求項５記載の論理回路検証方法において、前記階層展開処理ステップで生成した前記階層展開中間形式に対し定数伝播処理を行うための定数伝播処理ステップを有することを特徴とするものである。
【００２５】
また、請求項７記載の発明の論理回路検証方法は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証方法において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対照とする検証点を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記回路分割ステップの後に前記部分回路データに前記階層切り口端子に関してその入力側の部分回路の持つ論理情報を前記階層切り口端子に記憶させる処理を行う部分回路情報抽出ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップとを有し、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路情報抽出ステップで前記階層切り口端子に記憶させてある前記論理情報を利用して再度比較検証ステップで再検証を行うことを特徴とするものである。
【００２６】
請求項８記載の発明の論理回路検証プログラムを格納した記憶媒体は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証プログラムを格納した記憶媒体において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対照とする検証点を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路データを再度参照し前記階層展開中間形式の階層切り口端子情報を用いて新たな部分回路情報を抽出する部分回路情報抽出ステップとを有することを特徴とするものである。
【００２７】
また、請求項９記載の発明は、請求項８記載の論理回路検証プログラムを格納した記憶媒体において、前記階層展開処理ステップで生成した前記階層展開中間形式に対し定数伝播処理を行うための定数伝播処理ステップを有することを特徴とするものである。
【００２８】
請求項１０記載の発明の論理回路検証プログラムを格納した記憶媒体は、階層構造を有する検証対象の論理回路における論理が等価とみなす個所を、レジスタ及び又は外部切り口端子を検証点として抽出し、この検証点に注目して回路を部分回路に分割し、信号名を含む情報から論理等価点を決定し、対応する部分回路毎に論理等価性を検証することにより、複数の論理回路相互間の論理等価性を検証する論理回路検証プログラムを格納した記憶媒体において、
検証対象論理回路の回路データとライブラリから回路情報を読み込みこの回路情報を中間形式に変換出力するデータ入力ステップと、
前記中間形式の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理ステップと、
前記階層展開中間形式から比較対照とする検証点を抽出し、検証点情報に出力する検証点抽出ステップと、
前記階層展開中間形式及び前記検証点情報を参照し、前記階層切り口端子情報を用いて回路分割を行い、部分回路データを出力する回路分割ステップと、
前記回路分割ステップの後に前記部分回路データに前記階層切り口端子に関してその入力側の部分回路の持つ論理情報を前記階層切り口端子に記憶させる処理を行う部分回路情報抽出ステップと、
前記検証点情報及び前記部分回路データを参照して対応する部分回路の論理等価性を検証する比較検証ステップと、
前記検証点情報及び前記部分回路データの検証結果を判定する検証結果判断ステップと、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果が一致の場合は、前記検証結果を出力する検証結果出力ステップとを有し、
前記検証結果判断ステップで前記検証点情報及び前記部分回路データの検証結果両者が不一致の場合には、前記部分回路情報抽出ステップで前記階層切り口端子に記憶させてある前記論理情報を利用して再度比較検証ステップで再検証を行うことを特徴とするものである。
【００２９】
【発明の実施の形態】
次に、本発明の実施の形態について図面を参照して詳細に説明する。
【００３０】
本実施の形態の論理回路検証方法は、複数の論理回路相互間の形式検証における論理等価性の検証において、階層展開処理の部分において階層切り口端子情報を保存し、その情報を利用して検証対象の論理回路を部分回路に分割し、この部分回路毎に論理等価性を検証することを特徴とするものである。
【００３１】
次に、本発明の第１の実施の形態をブロックで示す図１を参照すると、この図に示す本実施の形態の論理回路検証装置は、検証対象となる階層構造を持つ論理回路の回路データＦ１とライブラリＦ２から回路情報を読み込みこの回路情報を中間形式Ｆ３に変換出力するデータ入力部１と、中間形式Ｆ３からの回路情報を階層展開しこの階層展開処理において階層間の境界の端子である階層切り口端子情報を保存した階層展開中間形式Ｆ４を出力する階層展開処理部２と、階層展開中間形式Ｆ４から比較対照とする検証点を抽出し検証点情報Ｆ５を出力する検証点抽出部３と、階層切り口端子情報を含む階層展開中間形式Ｆ４及び検証点情報Ｆ５を参照し上記階層切り口端子情報を用いて対象回路を部分回路に分割して部分回路データＦ６を生成する回路分割部４と、検証点情報Ｆ５及び部分回路データＦ６を参照して対応する部分回路の論理等価性を検証する比較検証部５と、検証結果を判断する検証結果判断部６と、検証結果の判断結果不一致の場合階層展開中間形式Ｆ４の階層切り口端子情報を用いて部分回路データＦ６から部分回路情報を抽出する部分回路情報抽出部７と、検証結果Ｆ７を出力する検証結果出力部８とを備える。
【００３２】
ここで、回路データＦ１は、ＶＨＤＬ（ＩＥＥＥ１０７６）やＶｅｒｉｌｏｇ−ＨＤＬ（ＩＥＥＥ１３６４）などのハードウェア記述言語や、ＥＤＩＦなどのネットリストから成る。また、ライブラリＦ２は、回路データＦ１の中で使用されるマクロの論理情報を記述したデータである。
【００３３】
また、中間形式Ｆ３、検証点情報Ｆ５、部分回路データＦ６は一時的に記憶装置に格納され処理の中間段階で利用する。
【００３４】
次に、図１及び処理をフローチャートで示す図２を参照して本実施の形態の動作について説明すると、本実施の形態では、階層切り口端子からその入力側の部分回路情報を探索・抽出して再検証することにより、論理等価性を検証する。この図では処理のフローを実線で、データの流れを点線でそれぞれ示す。
【００３５】
まず、データ入力部１は、回路データＦ１及びライブラリＦ２を読み込み、これら回路データＦ１及びライブラリＦ２を中間形式Ｆ３に変換する（ステップＳ１）。
【００３６】
階層展開処理部２は、中間形式Ｆ３の回路情報を階層展開しこの階層展開処理において階層間の境界端子である階層切り口端子情報を保存した階層展開中間形式Ｆ４を生成する（ステップＳ２）。
【００３７】
次に、検証点抽出部３は、階層展開中間形式Ｆ４から比較対照とする検証点を抽出し、検証点情報Ｆ５に出力する（ステップＳ３）。
【００３８】
次に、回路分割部４は、階層展開中間形式Ｆ４及び検証点情報Ｆ５を参照し、階層切り口端子情報を用いて回路分割を行い、部分回路データＦ６を出力する（ステップＳ４）。
【００３９】
次に、比較検証部５は、検証点情報Ｆ５及び部分回路データＦ６を参照して対応する部分回路の論理等価性を検証する（ステップＳ５）。
【００４０】
検証方法として、ＢＤＤ（２分決定グラフ：Ｂｉｎａｒｙ  ＤｅｃｉｓｉｏｎＤｉａｇｒａｍｓ）を用いた検証手法や、ＡＴＰＧ（自動テストパターン発生器：Ａｕｔｏｍａｔｉｃ  Ｔｅｓｔ  Ｐａｔｔｅｒｎ  Ｇｅｎｅｒａｔｏｒ）を用いてテストパターンを生成し、シミュレーションを行う検証手法などにより検証する。
【００４１】
検証結果判断部６は、検証点情報Ｆ５及び部分回路データＦ６の検証結果を判定し（ステップＳ６）、両者が一致すれば、検証結果を検証結果出力部８に送り、検証結果出力部８は検証結果Ｆ７を出力する（ステップＳ８）。
【００４２】
ステップＳ６で、両者が不一致の場合には、部分回路情報抽出部７は、部分回路データＦ６及び階層展開中間形式Ｆ４を再度参照し階層展開中間形式Ｆ４の階層切り口端子情報を用いて新たな部分回路情報を抽出する新たな部分回路情報を抽出し（ステップＳ７）、比較検証部５に供給し、比較検証部５は、再度ステップＳ５の検証を行う。
【００４３】
検証対象の回路の全ての部分の検証が完了するまで（ステップＳ９）、比較検証部５での検証（ステップＳ４）を反復する。
【００４４】
次に、検証対象回路の回路データＦ１の一例である回路１００を回路図で示す図３を参照すると、この回路１０は上位（ＴＯＰ）階層１０１と、その下位の階層である下位（ＳＵＢ）階層２０１とを有する。
【００４５】
ＴＯＰ階層１０１は、入力端が端子Ａ，Ｂに接続された論理ゲートＣ１１１と、出力端が端子Ｅに接続された定数情報１１２とを有する。
【００４６】
ＳＵＢ階層２０１は、入力端が端子Ｄ，Ｅに接続された論理ゲートＦ２１１と、入力端子Ｇが論理ゲートＦ２１１の出力端に出力端子Ｈが端子Ｉにクロック端子が端子ＣＬＫ１にそれぞれ接続されたフリップフロップ２１２とを有する。
【００４７】
検証点としてＴＯＰ階層１０１の外部の端子Ａ，Ｂ，Ｊと、クロック端子ＣＬＫと、ＳＵＢ階層１０２の外部の端子Ｄ，Ｅ，Ｉと、クロック端子ＣＬＫ１とを有する。このうち、端子Ｄ，Ｅ，Ｉと、クロック端子ＣＬＫ１は、ＴＯＰ階層１０１／ＳＵＢ階層２０１との間の階層切り口端子である。
【００４８】
回路１００の回路データを階層単位に分割して記述した図４を参照すると、図４（Ａ）はＴＯＰ階層１０１を、図４（Ｂ）はＳＵＢ階層２０１をそれぞれ示す。図４（Ａ）に示すＴＯＰ階層１０１は、ＳＵＢ階層２０１に対応するブロック１０２を有する。
【００４９】
図３、図４及び図３の回路データを本実施の形態で階層展開を実施した結果の回路２００を回路図で示す図５を参照してデータ入力部１に読み込んだ回路データＦ１が階層を持つ構造である場合の処理について説明すると、このように、回路２００が複数の、この例では２つの階層を持つ構造である場合には、回路データＦ１は、図４（Ａ），（Ｂ）に示すように、ＴＯＰ／ＳＵＢ２つの階層の各々について別々のデータ単位の構成を有する。
【００５０】
階層展開処理では、２つの階層、ＴＯＰ階層１０１とＳＵＢ階層２０１に対して、ブロック１０２をＳＵＢ階層２０１で置き換えることで実現できる。その際にブロック１０２が持つ各切り口端子情報を保存するために、上下間の階層切り口端子Ｄ，Ｅ，Ｉ，クロック端子ＣＬＫ１の各位置にバッファ７０１〜７０４を挿入してそれぞれ接続する。
【００５１】
このバッファ７０１〜７０４には、それぞれ識別子ＳＵＢ／Ｄ，ＳＵＢ／Ｅ，ＳＵＢ／Ｉ，ＳＵＢ／ＣＬＫ１を付加し、階層切り口端子であったことを識別できるようにしておく。同様に、論理ゲートＦ２１１及びフリップフロップ２１２の各端子にも識別子ＳＵＢ／Ｆ，ＳＵＢ／Ｇ及びＳＵＢ／Ｈを付加する。このようにして図５に示すように１つの階層構造に変換する。
【００５２】
回路２００のうちフリップフロップ２１２等のレジスタの入力端子ＳＵＢ／Ｇ４０１の入力側回路３００を抽出して示した図６（Ａ）を参照すると、この入力側回路３００は、端子Ａ，Ｂ、論理ゲートＣ１１１、信号源１１２、論理ゲートＳＵＢ／Ｆ２１１、バッファ７０１，７０２を有する。
【００５３】
入力側回路３００は、さらに、図６（Ｂ），（Ｃ），（Ｄ）にそれぞれ示す部分回路３０１，３０２，３０３に分割する。
【００５４】
部分回路３０１は、バッファＳＵＢ／Ｄ７０１Ａ，ＳＵＢ／Ｅ７０２Ａ、論理ゲートＳＵＢ／Ｆ２１１、端子ＳＵＢ／Ｇ４０１を有し、部分回路３０２は、端子Ａ，Ｂ、論理ゲートＣ１１１、バッファＳＵＢ／Ｄ７０１Ｂを有し、部分回路３０３は、信号源１１２、バッファＳＵＢ／Ｅ７０２Ｂを有する。
【００５５】
次に、図５、図６を参照して、回路分割部４における回路分割処理ステップＳ３について説明すると、フリップフロップ２１２の入力端子ＳＵＢ／Ｇ４０１を検証点とした場合の部分回路は、その入力側の回路となるが、データ入力部１において、設定されている階層切り口情報を保存するためのバッファ７０１，７０２があるので、そこまでを部分回路３０１として認識する。
【００５６】
同様にして、階層切り口情報を保存するためのバッファ７０１，７０２の入力側の回路の各々を、部分回路３０２，３０３として認識する。
【００５７】
次に、回路１００に対し定数情報を用い階層を跨いだ最適化を行った結果の回路４００を回路図で示す図７を参照すると、この回路４００は、最適化した上位（ＴＯＰ）階層１０１Ａと、その下位の階層である下位（ＳＵＢ）階層２０１Ａとを含む。
【００５８】
ＴＯＰ階層１０１Ａは、入力端が端子Ａ，Ｂに接続された論理ゲートＣ１１１を有する。最適化前の上位階層１０１に存在した信号源１１２は省略されている。
【００５９】
ＳＵＢ階層２０１Ａは、入力端子Ｇが端子Ｄに出力端子Ｈが端子Ｉにクロック端子が端子ＣＬＫ１にそれぞれ接続されたフリップフロップ２１２を有する。最適化前の下位階層２０１に存在した論理ゲートＦ２１１は省略されている。
【００６０】
回路４００を本実施の形態の論理回路検証方法により階層展開を行った結果の回路５００を回路図でを示す図８、及び図８の回路のうちフリップフロップ２１２の入力端子ＳＵＢ／Ｇ４０１Ａの入力側回路６００を抽出して示した図９（Ａ）を参照すると、この入力側回路６００は、端子Ａ，Ｂ、論理ゲートＣ１１１、バッファ７０１を有し、最適化前の同機能の回路に存在した信号源１１２、論理ゲートＳＵＢ／Ｆ２１１、バッファ７０２は省略されている。
【００６１】
同様に、入力側回路６００を分割した部分回路６０１，６０２をそれぞれ示す図９（Ｂ），（Ｃ）を参照すると、部分回路６０１は、バッファＳＵＢ／Ｄ７０１Ａを、部分回路６０２は、端子Ａ，Ｂ、論理ゲートＣ１１１、バッファＳＵＢ／Ｄ７０１Ｂをそれぞれ有する。
【００６２】
次に、図５〜図９を参照して、比較検証部５での比較検証（ステップＳ４）の検証結果の判断（ステップＳ５）で不一致として判定された場合の処理について説明する。
【００６３】
対応する検証点としてフリップフロップ２１２の入力端子ＳＵＢ／Ｇ４０１、入力端子ＳＵＢ／Ｇ４０１，４０１Ａについての検証を行う。
【００６４】
対応する各々の部分回路はぞれぞれ、部分回路３０１、部分回路６０１である。これら２つの部分回路３０１，６０１について等価性を検証すると（ステップＳ４，Ｓ５）両者は不一致であると判定する。不一致であったので、それぞれの部分回路の入力側の情報を検索すると、部分回路３０１には階層切り口端子ＳＵＢ／Ｄ，ＳＵＢ／Ｅ対応バッファ７０１，７０２が接続され、一方、部分回路６０１には階層切り口端子ＳＵＢ／Ｄ対応バッファ７０１が接続されている。
【００６５】
従って、さらに、その入力側に接続されている部分回路３０２，３０３及び部分回路６０２を抽出する（ステップＳ６）。これらの再度抽出した部分回路３０２，３０３及び部分回路６０２を用いて、部分回路３０１，６０１の各々に入力側の部分回路を接続して検証対象の部分回路を拡大し、再度比較検証すると、両者が一致すると判断できる。
【００６６】
ここで、入力側の部分回路を接続することにより検証対象の部分回路を拡大し、再検証する際には、一度の処理で全ての部分回路を接続する必要はなく、一部分のみ接続し検証対象部分回路を拡大し、一致するまで、部分回路の接続、再検証処理を繰り返しても同様である。
【００６７】
このように、本実施の形態では、現在処理中の階層の論理を検証する場合に、他階層にある論理を参照することができる処理を行っているので、複数の階層を跨いだ最適化を行っている場合の論理の等価性の検証においても、正しく検証することが可能となっている。
【００６８】
また、部分回路を階層切り口端子のあった位置で分割する処理を行っているために、少なくとも部分回路を最大限に大きくすることなく検証できるようになり、使用メモリ量を抑えることが可能となる。
【００６９】
次に、本発明の第２の実施の形態を図１と共通の構成要素には共通の参照文字／数字を付して同様にブロックで示す図１０を参照すると、この図に示す本実施の形態の前述の第１の実施の形態との相違点は、部分回路情報抽出部７の代わりに回路分割部４での回路分割後に部分回路データＦ６に階層切り口端子に関してその入力側の部分回路の持つ論理情報を階層切り口端子に記憶させる処理を行う部分回路情報抽出部７Ａを備えることである。
【００７０】
次に、図１０及び処理を図２と共通の構成要素には共通の参照文字／数字を付して同様にフローチャートで示す図１１を参照して本実施の形態の動作について相違点を重点的に説明すると、本実施の形態では、回路分割部４での回路分割（ステップＳ４）の後に、部分回路データＦ６の階層切り口端子についてその入力側の部分回路の持つ論理情報を上記階層切り口端子に記憶させる部分回路情報抽出処理ステップＳ７Ａを行う。
【００７１】
その後の比較検証部５及び比較結果判断部５での部分回路の比較検証ステップＳ４，Ｓ５において不一致となった場合には、階層切り口端子に記憶させてある上記論理情報を利用してステップＳ５，Ｓ６で再検証を行う。
【００７２】
これにより、入力側の部分回路の抽出処理を随時行う必要がなくなる。
【００７３】
また、この場合には、すべての階層切り口端子についてその入力側の部分回路の持つ論理情報の抽出を行うのではなく、特定の条件を設定し、その条件にある場合のみ論理情報の抽出を行ってもよい。
【００７４】
例えば、階層を跨いだ最適化が定数伝播の場合だけである場合には、定数情報のみを抽出条件とし、階層切り口端子の入力側の論理が、定数に簡単化される場合のみを抽出し、階層切り口端子に記憶させる。
【００７５】
このようにすることで、抽出対象の論理情報を低減でき、高速に処理できることとともに使用メモリ量の抑制、及び再検証の必要性の有無の判定が可能となり処理の高速化が可能となる。
【００７６】
次に、本発明の第３の実施の形態を図１と共通の構成要素には共通の参照文字／数字を付して同様にブロックで示す図１２を参照すると、この図に示す本実施の形態の前述の第１の実施の形態との相違点は、階層展開処理部２の後に、生成した階層展開中間形式Ｆ３に対し定数伝播処理を行うための定数伝播処理部１１を備えることである。
【００７７】
図１３を併せて参照して本実施の形態の動作について第１の実施の形態との相違点について説明すると、本実施の形態では、ステップＳ２の階層展開処理の後、生成した階層展開中間形式Ｆ４に対し、定数伝播処理部１１において、上位階層で設定される定数を下位階層に伝播させるよう階層を跨いだ定数伝播処理ステップＳ１１を行い、予め、階層展開で出現可能性が予想される下位階層の論理を簡単化しておく。
【００７８】
これにより、比較検証部５おいて階層を跨いだ最適化により不一致と判定されることを事前に防ぐことができるようになる。
【００７９】
従って、本実施の形態は、階層を跨いだ定数伝播により最適化された場合に効果がある。
【００８０】
【発明の効果】
以上説明したように、本発明の論理回路検証装置及び論理回路検証方法は、中間形式を階層展開しこの階層展開処理において階層切り口端子情報を保存した階層展開中間形式を生成する階層展開処理手段と、検証結果の判断結果不一致の場合階層切り口端子情報を用いて部分回路データから部分回路情報を抽出する部分回路情報抽出手段とを備えることにより、現在処理中の階層の論理を検証する場合に、他階層にある論理を参照することができるので、複数の階層を跨いだ最適化を行っている場合の論理の等価性の検証においても、正しく検証することが可能となるという効果がある。
【００８１】
また、部分回路を階層切り口端子のあった位置で分割することにより、少なくとも部分回路を最大限に拡大することなく検証できるようになり、使用メモリ量の抑制が可能となるという効果がある。
【図面の簡単な説明】
【図１】本発明の論理回路検証装置の第１の実施の形態を示すブロック図である。
【図２】本実施の形態の論理回路検証方法における動作の一例を示すフローチャートである。
【図３】本実施の形態の論理回路検証方法における第１の対象回路例の回路データを示す回路図である。
【図４】図３の回路を階層単位に分割して記述した回路図である。
【図５】図３の回路データを本実施の形態の論理回路検証方法により階層展開を行った結果の回路を示す回路図である。
【図６】図５の回路データの一部を抜粋した回路の回路図及びこの回路データを階層単位に分割して記述した回路図である。
【図７】図３の回路に対し定数情報を用い階層を跨いだ最適化を行った結果の回路を示す回路図である。
【図８】図７の回路を本実施の形態の論理回路検証方法により階層展開を行った結果の回路を示す回路図である。
【図９】図８の回路データの一部を抜粋した回路の回路図及びこの回路データを階層単位に分割して記述した回路図である。
【図１０】本発明の論理回路検証装置の第２の実施の形態を示すブロック図である。
【図１１】本実施の形態の論理回路検証方法における動作の一例を示すフローチャートである。
【図１２】本発明の論理回路検証装置の第３の実施の形態を示すブロック図である。
【図１３】本実施の形態の論理回路検証方法における動作の一例を示すフローチャートである。
【図１４】図３の回路を通常の方法により階層展開を行った結果の回路を示す回路図である。
【図１５】図７の回路を通常の方法により階層展開を行った結果の回路を示す回路図である。
【符号の説明】
１    データ入力部
２    階層展開処理部
３    検証点抽出部
４    回路分割部
５    比較検証部
６    検証結果判断部
７，７Ａ    部分回路情報抽出部
８    検証結果出力部
１１    定数伝播処理部
１０１    ＴＯＰ階層
１０２    ブロック
２０１    ＳＵＢ階層
１１１    論理ゲートＣ
１１２    定数情報
２１１    論理ゲートＦ
２１２    フリップフロップ
１００，２００，３００，４００，５００，６００    回路
３０１，３０２，３０３，６０１，６０２    部分回路
７０１〜７０４    バッファ
【図１】
0003652220.tif 000002
【図２】
0003652220.tif 000003
【図３】
0003652220.tif 000004
【図４】
0003652220.tif 000005
【図５】
0003652220.tif 000006
【図６】
0003652220.tif 000007
【図７】
0003652220.tif 000008
【図８】
0003652220.tif 000009
【図９】
0003652220.tif 000010
【図１０】
0003652220.tif 000011
【図１１】
0003652220.tif 000012
【図１２】
0003652220.tif 000013
【図１３】
0003652220.tif 000014
【図１４】
0003652220.tif 000015
【図１５】
0003652220.tif 000016