(57)【要約】【課題】検証を容易に出来る回路記述言語の等価性検証方法を提供すること。【解決手段】回路記述言語の等価性検証方法は、第１回路記述言語により記述された、半導体集積回路に関する第１設計データ１０を回路合成して、前記第１回記述言語よりも抽象度の低い第２回路記述言語により記述された第２設計データ１４を得るステップと、前記第２回路記述言語により記述された第３設計データ２０と、前記第２設計データ１４とを比較して両者の対応関係を検証し、対応しない部分について形式的検証を行うステップとを具備し、前記第２、第３設計データ１４、２０が全て対応した場合、及び前記対応しない部分について形式的検証を行った結果、両者が等しい場合、前記第１設計データ１０と前記第３設計データ２０とは等価であると判定される。【選択図】      図２
2007233648.tif 000002
【特許請求の範囲】
【請求項１】
第１回路記述言語により記述された、半導体集積回路に関する第１設計データを回路合成して、前記第１回記述言語よりも抽象度の低い第２回路記述言語により記述された第２設計データを得るステップと、
前記第２回路記述言語により記述された第３設計データと、前記第２設計データとを比較して両者の対応関係を検証し、対応しない部分について形式的検証を行うステップと
を具備し、前記検証の結果、前記第２、第３設計データが全て対応した場合、及び前記対応しない部分について形式的検証を行った結果、両者が等しい場合、前記第１設計データと前記第３設計データとは等価であると判定される
ことを特徴とする回路記述言語の等価性検証方法。
【請求項２】
第１回路記述言語により記述された、半導体集積回路に関する第１設計データを回路合成して、前記第１回記述言語よりも抽象度の低い第２回路記述言語により記述された第２設計データを得るステップと、
前記第２設計データを回路合成して、演算器と該演算器に接続されるデータパスとを含む第１回路情報と、該第１回路情報におけるデータの流れを制御する第１制御情報とを得るステップと、
前記第２回路記述言語により記述された第３設計データを回路合成して、演算器と該演算器に接続されるデータパスとを含む第２回路情報と、該第２回路情報におけるデータの流れを制御する第２制御情報とを得るステップと、
前記第１、第２回路情報を比較して対応関係を検証し、対応しない部分について形式的検証を行い、該第１、第２回路情報が等価であるか否かを検証するステップと、
前記第１、第２制御情報につき形式的検証を行い、該第１、第２制御情報が等価であるか否かを検証するステップと
を具備し、前記第１、第２回路情報が等価であり、且つ前記第１、第２制御情報が等価である場合、前記第１設計データと前記第３設計データとは等価であると判定される
ことを特徴とする回路記述言語の等価性検証方法。
【請求項３】
前記第１回路記述言語により記述された第４設計データを回路合成して、前記第２回路記述言語により記述された前記第３設計データを得るステップを更に備える
ことを特徴とする請求項１または２記載の回路記述言語の等価性検証方法。
【請求項４】
前記第１、第２回路記述言語のうち前記第２回路記述言語は、時間の概念を有し、
前記第１乃至第３設計データのうち前記第２、第３設計データは、前記半導体集積回路の動作の基準となるクロック信号と、該第２、第３設計データ内に含まれる演算とのタイミングに関する情報を含む
ことを特徴とする請求項１乃至３いずれか１項記載の回路記述言語の等価性検証方法。
【請求項５】
前記第１設計データは、該第１設計データに含まれる演算のうち、前記第２設計データにおいて出力すべき変数に関する情報と、該変数を出力するタイミングを指定する情報とを含む
ことを特徴とする請求項４記載の回路記述言語の等価性検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、回路記述言語の等価性検証方法に関する。特にＲＴＬ（Register Transfer Level）と、ＲＴＬより上位レベルの記述言語による設計記述との等価性の検証に関するものである。
【背景技術】
【０００２】
従来、ＬＳＩ（Large Scale Integrated circuit）製品の設計には、ＶＨＤＬ等のハードウェア記述言語（ＨＤＬ：Hardware Description Language）が用いられてきた。このような言語で記述されたＬＳＩの設計データを以下ＲＴＬ記述と呼ぶことにする（以下、各種言語によるＬＳＩの設計データをまとめてハードウェア設計記述と呼ぶことがある）。
【０００３】
また近年では、Ｃ言語など汎用のプログラミング言語をハードウェア用に拡張した言語（例えばＳｙｓｔｅｍＣ等）が、ＬＳＩの設計言語として用いられ始めている。この場合に得られる設計データ（これを以後機能記述と呼ぶ）は、ＲＴＬ記述と異なり時間の概念を有さず、ＲＴＬ記述よりも記述量が少なく済むという利点がある。
【０００４】
機能記述は、合成ツールを用いてＲＴＬ記述に変換され、その後論理回路レベルの設計データに変換される。この際、機能記述とＲＴＬ記述とは機能的に等しくなければならず、両者の間の等価性を検証する必要がある。この等価性を検証する方法については、従来いくつかの提案があるが（例えば特許文献１参照）、従来の方法であると非常に膨大な計算量が必要であり、検証に時間がかかるという問題があった。
【特許文献１】特開２００５−３１６５９５号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
この発明は、検証を容易に出来る回路記述言語の等価性検証方法を提供する。
【課題を解決するための手段】
【０００６】
この発明の第１の態様に係る回路記述言語の等価性検証方法は、第１回路記述言語により記述された、半導体集積回路に関する第１設計データを回路合成して、前記第１回記述言語よりも抽象度の低い第２回路記述言語により記述された第２設計データを得るステップと、前記第２回路記述言語により記述された第３設計データと、前記第２設計データとを比較して両者の対応関係を検証し、対応しない部分について形式的検証を行うステップとを具備し、前記検証の結果、前記第２、第３設計データが全て対応した場合、及び前記対応しない部分について形式的検証を行った結果、両者が等しい場合、前記第１設計データと前記第３設計データとは等価であると判定される。
【０００７】
この発明の第２の態様に係る回路記述言語の等価性検証方法は、第１回路記述言語により記述された、半導体集積回路に関する第１設計データを回路合成して、前記第１回記述言語よりも抽象度の低い第２回路記述言語により記述された第２設計データを得るステップと、前記第２設計データを回路合成して、演算器と該演算器に接続されるデータパスとを含む第１回路情報と、該第１回路情報におけるデータの流れを制御する第１制御情報とを得るステップと、前記第２回路記述言語により記述された第３設計データを回路合成して、演算器と該演算器に接続されるデータパスとを含む第２回路情報と、該第２回路情報におけるデータの流れを制御する第２制御情報とを得るステップと、前記第１、第２回路情報を比較して対応関係を検証し、対応しない部分について形式的検証を行い、該第１、第２回路情報が等価であるか否かを検証するステップと、前記第１、第２制御情報につき形式的検証を行い、該第１、第２制御情報が等価であるか否かを検証するステップとを具備し、前記第１、第２回路情報が等価であり、且つ前記第１、第２制御情報が等価である場合、前記第１設計データと前記第３設計データとは等価であると判定される。
【発明の効果】
【０００８】
本発明によれば、検証を容易に出来る回路記述言語の等価性検証方法を提供出来る。
【発明を実施するための最良の形態】
【０００９】
以下、この発明の実施形態を図面を参照して説明する。この説明に際し、全図にわたり、共通する部分には共通する参照符号を付す。
【００１０】
この発明の第１の実施形態に係る回路記述言語の等価性検証方法について説明する。はじめに、本実施形態に係るＬＳＩのおおまかな設計方法について図１を用いて説明する。図１はＬＳＩの設計方法のフローチャートである。
【００１１】
まず設計すべきＬＳＩのシステム仕様が決定される。そして、その仕様を満たすように、システムレベル設計が行われる（ステップＳ１０）。この際に用いられる記述言語が、ハードウェア記述言語よりも抽象度の高い、ハードウェア用に拡張されたＣ言語であり、例えばＳｙｓｔｅｍＣやＳｐｅｃＣなどである。抽象度とは、設計の詳細度のことであり、詳細度とはＬＳＩの構造と演算の順序付けのことである。ステップＳ１０によって、設計すべきＬＳＩの機能記述（ＬＳＩの設計データ）１０が得られる。この時点において得られる機能記述１０は抽象度が高く、時間の概念を持っていない。すなわちＬＳＩの動作の基準となるクロックと演算とのタイミングについては全く規定されていない。
【００１２】
次に機能記述１０を、合成ツールを用いて動作合成する（ステップＳ１１）。その結果、機能記述１０はＲＴＬ記述１１に変換される。ＲＴＬ記述１１には、その抽象度にいくつかの段階があるが、それについては後述する。更にＲＴＬ記述１１は合成ツールにより、機能合成及び論理合成される（ステップＳ１２）。その結果、ＲＴＬ記述１１はゲートレベルの論理回路（ネットリスト）１２に変換される。
【００１３】
その後、ゲートレベル論理回路１２についてレイアウト設計を行い（ステップＳ１３）、マスクレイアウトデータ１３が得られる。以上によりＬＳＩの設計は終了し、マスクレイアウトデータ１３は実際のＬＳＩの製造ラインへ投入される。
【００１４】
上記のＬＳＩの設計方法において、Ｃ言語をベースに設計された機能記述１０が、ＲＴＬ記述１１と等価であるかを検証する必要がある。換言すれば、ステップＳ１１の動作合成が正しく行われているか否かを検証する必要がある。これが等価性検証である。以下、本実施形態に係る等価性検証方法について図２を用いて説明する。図２は本実施形態に係る等価性検証方法のフローチャートである。
【００１５】
まず、上記ステップＳ１１で機能記述１０を動作合成すると、ＲＴＬ記述１１のうち、最初の段階（最も抽象度が高い）であるスケジュール決定済みデータ１４が得られる。スケジュール決定済みデータ１４は、機能記述１０に含まれる各演算がどのクロックに同期して行われるかが完全に決められた回路記述である。これにより、機能記述１０に時間の概念が与えられる。
【００１６】
次にスケジュール決定済みデータ１４に対して機能合成が行われる（ステップＳ１４）。機能合成においては、まずＬＳＩにおいて使用すべきメモリの構成やレジスタ数等が決定される。次に、実現すべき機能としての演算（例えば加算や減算など）に対して、具体的に使用する演算器が割り付けられる。更に、複数の演算器の間の結線方法として、バスを使うかマルチプレクサを使うかが決定される。このようにしてＲＴＬの抽象度が低下していき、最後に演算器、バス、及びマルチプレクサなどから構成されるデータパス部のデータ１５と、それらを制御する信号を生成する制御部のデータ１６が得られる。このデータパス部データ１５及び制御部データ１６が、ＲＴＬ記述１１のうちで最も抽象度の低い、すなわちＬＳＩの構造と演算の実行順序が全て規定され、ＬＳＩが最も具体的に記述された設計データである。
【００１７】
また、ステップＳ１０において用いた仕様を満たすように、ハードウェア記述言語でＬＳＩの設計が行われる（ステップＳ１５）。これにより、スケジュール決定済みデータ２０が得られる。これによって得られるスケジュール決定済みデータ２０は、機能記述１０をベースにして得られるスケジュール決定済みデータ１４と同一の抽象度を有し、時間の概念を持った設計データである。引き続き、ステップＳ１４と同様に機能合成を行うことにより（ステップＳ１６）、スケジュール決定済みデータ２０に関するデータパス部データ２１及び制御部データ２２が得られる。
【００１８】
なおステップＳ１１における動作合成においては、ステップＳ１５の記述から得られるデータパス部データ２１を利用するという制限付きで合成できるか否かをまず試行する。これが不可能な場合には、通常の動作合成を実施する。
【００１９】
次に、両者の等価性検証を行う（ステップＳ１７）。等価性検証方法について図３を用いて説明する。図３は等価性検証方法のフローチャートである。等価性検証は、両者のデータパス部データ１５、２１及び制御部データ１６、２２を用いて行われる。  
まず等価性検証にあたって、まずデータパス部データ１５とデータパス部データ２１とが比較される（ステップＳ１８）。両者の対応が取れれば、両者は等価であるとみなされる。もしステップＳ１１において、ステップＳ１５の記述から得られるデータパス部データ２１を利用できた場合、当然ながらデータパス部データ１５、２１は全く同一となり、両者は全て対応が取れることになる。また比較の際、両者が対応するか否かについては、必要に応じて対応関係ライブラリ１７が用いられる。対応関係ライブラリ１７は、異なるデータパスでありながら実現すべき動作が等しいものの対応関係に関する情報のことである。データパス部データ２１において、全てのデータパスについて両者の対応が取れなかった場合（ステップＳ１９、ＮＯ）、その取れなかった部分について、形式的検証を行う（ステップＳ２０）。形式的検証は、必要に応じて検証方法ライブラリ１８を用いて行われる。形式的検証には、交換法則などを利用した等価性検証方法が多く知られている。これらを登録したものが検証方法ライブラリ１９である。なお、検証方法ライブラリ１９を利用する場合には、データパス部データ１５、２１だけでなく、制御部データ１６、２２も必要に応じて参照する。なぜなら、検証方法ライブラリ１９に登録されているものの中には、制御部データを参照するような指示を含むものもあり得るからである。
【００２０】
形式的検証を行った結果、両者は等しくない部分を有する場合（ステップＳ２１、ＮＯ）、スケジュール決定済みデータ１４と２０、すなわち機能記述１０とＲＴＬ記述２０とは等価ではないと判断される（ステップＳ２２）。
【００２１】
ステップＳ２１において両者が等しい場合（ステップＳ２１、ＹＥＳ）、及びステップＳ１９において全てのデータパスで対応が取れた場合（ステップＳ１９、ＹＥＳ）、次に制御部データ１６について形式的検証が行われる（ステップＳ２３）。この際も、必要に応じて検証方法ライブラリ１９が用いられる。そして、形式的検証の結果、制御部データ１６、２２が等しければ（ステップＳ２４、ＹＥＳ）、機能記述１０とＲＴＬ記述２０とは等価であると判断される（ステップＳ２５）。等しくない場合には（ステップＳ２４、ＮＯ）、等価でないと判断される（ステップＳ２２）。
【００２２】
以上によって等価性の検証が行われる。本実施形態に係る等価性検証方法について、以下具体例を挙げて説明する。図４は、機能記述１０とそれを合成して得られるデータパス部データ１５及び制御部データ１６、並びにハードウェア記述言語を用いて記述されたスケジュール決定済みデータ２０とそれを合成して得られるデータパス部データ２１及び制御部データ２２の模式図である。
【００２３】
機能記述１０及びスケジュール決定済みデータ２０について簡単に説明する。機能記述１０は次のような設計データである。すなわち、２〜４行目において、入力Ｉｎ、出力Ａ、Ｂ、及び変数Ｘ、Ｙを規定する。そして５、６行目において、変数Ｘ、Ｙは入力Ｉｎを取り込む。７、８行目において、出力Ａ、Ｂにはそれぞれ０、Ｘが代入される。そして、９〜１２行目において、出力Ｂが変数Ｙ以上の値である期間、出力ＢからＹを減算し、更に出力Ａに１を加算する計算を繰り返す。すなわち、ＢをＹで割る除算を行う設計データである。
【００２４】
スケジュール決定済みデータ２０は、４行目でクロックＣＬを規定し、更に機能記述１０における３行目と４行目の間、４行目と５行目の間、５行目と６行目の間、６行目と７行目の間、８行目と９行目の間、及び１１行目と１２行目の間にクロックＣＬを待つ命令（Waitfor(CL)文）を更に備えるものである。Waitfor(CL)文は、新たにクロックＣＬが入力されない限りは、次の行の命令を実行させない機能を有する。それ以外は、スケジュール決定済みデータ２０は機能記述１０と同じである。すなわち、スケジュール決定済みデータ２０は、機能記述１０において各行のクロックに対する実行タイミングが規定されたものである。
【００２５】
これらを合成ツールに入力することで、図４に示すデータパス部データ１５、２１、制御部データ１６、２２が得られる。図示するように、データパス部データ１５は、マルチプレクサｍｕｘ１〜ｍｕｘ４、加算器３０、減算器３１、及び比較器３２を備えている。マルチプレクサｍｕｘ１、ｍｕｘ２はそれぞれ、制御信号ｃｄ１、ｃｄ２に応じて入力信号ｉｎ１を選択し、選択した入力信号ｉｎ１をそれぞれ変数ｘ、ｙとする。マルチプレクサｍｕｘ３は、制御信号ｃｄ３に応じて “０”を選択し、制御信号ｃｄ４に応じて加算器３０の加算結果を選択し、これを出力ａとする。マルチプレクサｍｕｘ４は、制御信号ｃｄ５に応じて変数ｘを選択し、制御信号ｃｄ６に応じて減算器３１の出力を選択し、これを出力ｂとする。加算器３０は出力ａに“１”を加算する。減算器３１は出力ｂから変数ｙを減算する。比較器３２は出力ｂと変数ｙとを比較し、比較結果を比較信号ｄｃ１として出力する。そして制御部１６は、比較信号ｄｃ１に応じて制御信号ｃｄ１〜ｃｄ６を制御する。スケジュール決定済みデータ２０から得られるデータパス部データ２１、及び制御部データ２２も同様である。
【００２６】
以上のようにデータパス部データ１５、２１及び制御部データ１６、２２が得られた後、等価性の検証を行う（ステップＳ１７）。まず、データパス部データ間の対応部分を検出する（ステップＳ１８）。すると、図４に示すように機能記述１０とスケジュール決定済みデータ２０とは、クロックに関する記載以外は全て同じである。従って、対応関係ライブラリ１７を参照するまでもなく、両者に関するデータパス部データ１５、２１は同一となり（ステップＳ１９）、データパスについての形式的検証は不要となる。よって、次に制御部データ１６、２２について形式的検証を行う（ステップＳ２３）。前述の通り、機能記述１０とスケジュール決定済みデータ２０とは、クロックに関する記載以外は全て同じであるから、制御部データ１６、２２についても、クロックについてのみ検証を行えば良い。その結果、制御部データ１６、２２が等しければ（ステップＳ２４）、機能記述１０と、ハードウェア記述言語によって記述されたＲＴＬ記述２０とは等価であると判断される（ステップＳ２５）。
【００２７】
別の例を図５に示す。図５は、機能記述１０とそれを合成して得られるデータパス部データ１５及び制御部データ１６、並びにハードウェア記述言語を用いて記述されたスケジュール決定済みデータ２０とそれを合成して得られるデータパス部データ２１及び制御部データ２２の模式図である。
【００２８】
機能記述１０は図４を用いて説明した通りである。ハードウェア記述言語によって記述されたスケジュール決定済みデータ２０は図４とは異なり、図４における１４〜１６行目が(A,B)=Divider(X,Y)文に置き換えられている。
【００２９】
これらを合成ツールに入力することで、図５に示すデータパス部データ１５、２１、制御部データ１６、２２が得られる。図示するように、機能記述１０を合成して得られるデータパス部データ１５及び制御部データ１６は図４と同様である。これに対してハードウェア記述言語によって記述されたＲＴＬ記述２０を合成して得られるデータパス部データ２１は次のような構成を有している。すなわちデータパスはマルチプレクサｍｕｘ１１〜ｍｕｘ１４及び除算器３３を備えている。マルチプレクサｍｕｘ１１、ｍｕｘ１２はそれぞれ、制御信号ｃｄ１１、ｃｄ１２に応じて入力信号ｉｎ１を選択し、選択した入力信号ｉｎ１をそれぞれ変数ｘ、ｙとする。マルチプレクサｍｕｘ１３、ｍｕｘ１４はそれぞれ、制御信号ｃｄ１３、ｃｄ１４に応じて除算器３３における除算結果及びその余りを出力ａ、ｂとする。そして制御部１６は制御信号ｃｄ１１〜ｃｄ１４を制御する。
【００３０】
上記のデータパス部データ１５、２１及び制御部データ１６、２２が得られた後、等価性の検証を行う（ステップＳ１７）。まず、データパス部データ間の対応部分を検出する（ステップＳ１８）。すると、図４の場合と異なり、データパス部データ１５において除算を行うブロック３４が除算器３３に置き換えられている。すなわち両者の構成は異なる。しかし、両者の構成は違っていても機能として同一であることが既知であれば、形式的検証を行う必要はない。そこで、ブロック３４と除算器３３とが等価であるかについて、対応関係ライブラリ１７を参照する。図６は対応関係ライブラリ１７の一例を示す模式図である。図示するように、対応関係ライブラリ１７には、機能記述１０における７〜１２行目の記述がデータパス部データにおける除算器と等しいことが登録されていたと仮定する。すると、図５においてブロック３４と除算器３３が等価であることが分かるので、形式的検証を行う必要はない。以上の結果、データパス部データ１５、２１は等価であることが分かる（ステップＳ１９）。
【００３１】
よって、次に制御部データ１６、２２について形式的検証を行う（ステップＳ２３）。図７は制御部データ１６の模式図である。図示するように制御部１６は、６つの状態ｓｒ１〜ｓｒ６を有する。図７において、各状態間に記載されているスラッシュ（／）前後の信号名は、それらの信号に基づいて状態遷移することを示しており、スラッシュ前が比較信号ｄｃ１、スラッシュ後が制御信号ｃｄ１〜ｃｄ６を示す。なお、“−”は比較信号ｄｃ１について不問であることを示し、“done”は計算終了を示す。
【００３２】
まず初期状態ｓｒ１において、制御信号ｃｄ１が“１”になると、マルチプレクサｍｕｘ１は入力ｉｎ１を選択してこれをｘとし、状態はｓｒ２へと遷移する。状態ｓｒ２において制御信号ｃｄ２が“１”になると、マルチプレクサｍｕｘ２が入力ｉｎ１を選択してこれをｙとし、状態はｓｒ３へと遷移する。状態ｓｒ３においてｃｄ３、ｃｄ５が“１”になると、マルチプレクサｍｕｘ３、ｍｕｘ４はそれぞれ“０”及び変数ｘをそれぞれ出力ａ、ｂとし、状態ｓｒ４へと遷移する。状態ｓｒ４において、ｃｄ４、ｃｄ６が“１”となり、比較信号ｄｃ１が“１”となると、状態ｓｒ６に遷移する。比較信号ｄｃ１が“１”とは、出力ｂが変数ｙ未満であることを示す。状態ｓｒ６では、ｄｃ１が“１”であるかぎり、除算を繰り返す。そして比較信号ｃｄ１が“０”となった場合、すなわち計算が終了した場合（done）、最終状態ｓｒ５に遷移する。状態ｓｒ４においても、比較信号ｄｃ１が“０”となった場合、計算終了となり、状態ｓｒ６に移ることなく状態ｓｒ５へ遷移する。
【００３３】
図８は制御部データ２２の模式図である。図示するように制御部２２は、４つの状態ｓｒ１１〜ｓｒ１４を有する。まず初期状態ｓｒ１１において、制御信号ｃｄ１１が“１”になると、マルチプレクサｍｕｘ１１は入力ｉｎ１を選択してこれをｘとし、状態はｓｒ１２へと遷移する。状態ｓｒ１２において制御信号ｃｄ１２が“１”になると、マルチプレクサｍｕｘ１２が入力ｉｎ１を選択してこれをｙとし、状態はｓｒ１３へと遷移する。状態ｓｒ１３においてｃｄ１３、ｃｄ１４が“１”になると、状態ｓｒ１４へと遷移し、除算器３３が除算を行って、計算は終了する（done）。
【００３４】
上記図７及び図８に示す制御部１６を比較すると、制御部１６における状態ｓｒ１〜ｓｒ３までの状態遷移条件と、制御部２２における状態ｓｒ１１〜ｓｒ１３までの状態遷移条件とは全く同一である。つまり、両者の制御方法とそれによるデータの流れは等しい。従って制御部１６における状態ｓｒ１〜ｓｒ３までの制御と、制御部２２における状態ｓｒ１１〜ｓｒ１３までの制御とは等価であることが分かる。よって、制御部１６における状態ｓｒ４〜ｓｒ６と、制御部２２におけるｓｒ４の制御とが等価であるか否かについて、形式的検証を行う（ステップＳ２３）。形式的検証には、等価性検証方法が登録された検証方法ライブラリ１９を用いて形式的検証は行われる。そして形式的検証の結果、両者が等しい制御を行っていることが導かれると、図５における機能記述１０とＲＴＬ記述２０とが等価であると判断される。
【００３５】
なお、上記等価性の検証方法は、説明した全ての処理を計算機が主体となって行うことが出来る。図９は、上記等価性検証を行う計算機の内部構成を示すブロック図である。図示するように計算機４０は、ＣＰＵ４１、メインメモリ４２、メモリ４３、ディスプレイ４４、及び入力装置（キーボード）４５を備えている。メモリ４３は設計データ４６、制御部比較プログラム４７、パス比較プログラム４８、回路合成プログラム４９、及び各種ライブラリ５０等を保持する。設計データ４６には、上記した機能記述１０やＲＴＬ記述（スケジュール決定済みデータ、データパス部データ、及び制御部データを含む）１２が含まれる。また各種ライブラリ５０とは、上記対応関係ライブラリ１７や検証方法ライブラリ１８、１９のことである。メインメモリ４２は、メモリ４３内の各プログラム、データなどを一時的に保持する。ＣＰＵ４１は、回路合成プログラム４９によって合成ツールを実行し、上記説明した動作合成（ステップＳ１１）、機能合成（ステップＳ１４、Ｓ１６）、論理合成（ステップＳ１２）を行う回路合成手段として機能する。更にＣＰＵ４１は等価性の検証の際、パス比較プログラム４８、各種ライブラリ５０、及び設計データ４６をメインメモリ４２に読み出し、上記ステップＳ１８〜Ｓ２１の処理を行うデータパス比較検証手段として機能する。更にパス比較プログラム４８の代わりに制御部比較プログラム４７を読み出すことにより、上記ステップＳ２３、Ｓ２４を行う制御部比較手段としても機能する。ディスプレイ４４は、上記ＣＰＵ４１による処理結果を表示する。入力装置４５は、ユーザの命令入力を受け取る。
【００３６】
以上のように、この発明の第１の実施形態に係る回路記述言語の等価性検証方法であると、等価性の検証を容易にすることが出来る。本効果について以下詳細に説明する。  
以下、説明の簡略化のために、スケジュール決定済みデータを単に「ＲＴＬ記述」と呼ぶこととし、データパス部データ及び制御部データを一括して「データ・制御情報」と呼ぶことにする。従来、ハードウェア記述言語によりＲＴＬ記述を作成し、それを合成ツールで機能・論理合成を行う場合でも、ＲＴＬ記述とデータ・制御情報との間における等価性検証が必要である。従来の両者の間の等価性検証は合成ツールが自ら行っており、その等価性検証の信頼性は比較的高い。従って、合成ツールによって得られるデータ・制御情報は、ＲＴＬ記述とほぼ等価と考えて良い。
【００３７】
それに対して近年、Ｃ言語をベースに用いた設計手法が用いられ始めている。この場合、Ｃ言語をベースに用いた記述言語で記述された機能記述が、合成ツールによってデータ・制御情報に変換される。従って、機能記述とデータ・制御情報との間の等価性検証が重要となる。この点、従来の方法であるとＲＴＬ記述と機能記述との間でシミュレーションを行い、その結果によって等価性を検証する方法が知られている。しかし、シミュレーションを用いて等価性を判断する場合、１００％の等価性を保証するためには、想定される全ての信号の組み合わせについて行わなければならない。このためには、膨大な計算量が必要となり、現実的ではない。
【００３８】
しかし本実施形態であると、まずシミュレーションを用いることなく、形式的検証を用いて等価性を検証する。形式的検証を用いることにより、シミュレーションを用いた場合に比べて容易に１００％の等価性を保証することが出来る。そのため、本実施形態では次のような方法を用いている。まず機能記述を作成し、合成ツールによりデータ・制御情報を得る（これを第１データ・制御情報と呼ぶ）。同時に、機能記述と同じ機能を実現するＲＴＬ記述を、従来のハードウェア記述言語により作成し、合成ツールによりデータ・制御情報を得る（これを第２データ・制御情報と呼ぶ）。上記したように、第２データ・制御情報はＲＴＬ記述と等価であることがほぼ保証される。従って、この第２データ・制御情報と第１データ・制御情報との等価性を検証することによって、機能記述が所望の機能を満たしているか、つまり機能記述と第１データ・制御情報とが等価であるかを検証する。両者が等価であることが分かると、上記機能記述は当該合成ツールによって正しいデータ・制御情報が得られることが分かる。
【００３９】
第１データ・制御情報と第２データ・制御情報との等価性を検証する際、上記実施形態で説明したように、互いに等価な箇所を部分毎に見つけていく。そして、従来の蓄積データを用いても等価であるか否かが分からない箇所についてのみ形式的検証を適用する。つまり、等価性の検証をボトムアップに行う。これにより、形式的検証を行うべき箇所を最小限にすることが出来、等価性検証のための計算量を削減し、等価性検証を容易に行うことが出来る。
【００４０】
更に本実施形態であると、データ・制御情報をデータパス部と制御部とに分けて考える。すなわち、回路構成と、その回路におけるデータの流れとに分けて、それぞれについて等価性を検証する。回路構成については、上記のようにボトムアップに等価な箇所を検出（演算器の対応を取る）し、必要な箇所についてのみ形式的検証を行う。従って、回路構成について両者が完全に一致した場合には、データの流れについてのみ形式的検証を行えば良い。データの流れに着目するということは、すなわち回路構成に対する制御方法に着目することと同意であり、制御信号がどのようなタイミングで“１”または“０”になるかを検証すれば良い。そして回路構成に対して形式的検証を適用しようとした場合には、例えば１６ビットや３２ビットなどデータ幅が大きいため計算量が多くなるのに対して、制御信号は通常１ビットであるから計算量が非常に少ない。つまり、回路構成に対する形式的検証を少なくし、または完全に省くことによって、等価性検証のための計算量を圧倒的に少なくすることが出来る。  
以上のような方法を用いることで、抽象度が高いために少ない記述量で済むＣ言語ベースの回路記述言語を用いたＬＳＩ設計の信頼性が向上される。勿論、データパス部と制御部とにわけることなくボトムアップに検証を行うことも出来る。
【００４１】
次に、この発明の第２の実施形態に係る回路記述言語の等価性検証方法について説明する。本実施形態は、上記第１の実施形態においてデータの流れ（制御部）に着目して等価性を判断する際、等価性を判断すべきタイミングに関するものである。図１０はクロックとデータＡ、データＢのタイミングチャートである。ＬＳＩにおいてあるデータＡ、Ｂがあったとして、これらのデータＡ、Ｂが常時、意味のある値を持つとは限らない。例えばデータＡは時刻ｔ０から時刻ｔ３までは意味のある値を有するが、その前後の値は特定の値に定まるものではない。またデータＢについても、時刻ｔ１から時刻ｔ２までは意味のある値を有するが、その前後は定まらない。このような場合、データＡ、Ｂが定まらない時間帯までも等価であることが求められる必要はない。そこで、いずれのタイミングで等価性を判断するかを決定する必要がある。
【００４２】
この点、ＲＴＬ記述はクロックの概念を有しており、既に上記タイミングの規定を有している。しかし、機能記述にはクロックの概念が無いため、上記タイミングをクロックで定義することは不可能である。本実施形態はこのような事情の基、機能記述において上記タイミングを規定する方法に関するものである。
【００４３】
図１１は、本実施形態に係る機能記述１０の一例である。図示するように、第１の実施形態で説明した図４、図５の機能記述１０において、１３行目及び１４行目の記述が追加されている。１３行目で出力すべきデータが指定され、１４行目でいずれのタイミングで出力すべきデータを出力するかが指定される。以下、１３行目及び１４行目の記述を読み出し命令と呼ぶことにする。図１１に示す機能記述１０が与えられると、合成ツールは動作合成（ステップＳ１１）及び機能合成（ステップＳ１４）において、読み出し命令を検索する。そして、読み出し命令を発見した場合、読み出し命令中において指定されたデータが、指定されたタイミングにおいて出力されるように、データパス部データ１５及び制御部データ１６を生成する。前述のように機能記述は時間の概念が無いので、機能記述内における行数や、または信号に対する応答として出力タイミングが指定される。すなわち、次のような指定方法が考えられる。例えば図１１の場合には、データ（Ａ、Ｂ）の出力タイミングを、「１２行目の処理が終了した後」と指定する。または「信号Ａの値が変化した時」と指定する。
【００４４】
上記のように、この発明の第２の実施形態に係る等価性検証方法であると、上記第１の実施形態に比べて更に等価性の検証を容易とすることが出来る。本効果について以下説明する。  
前述のように、等価性は全ての時間（タイミング）において満たされなければならないものではなく、特定のタイミングにおいて満たされれば十分であることが通常である。そこで本実施形態では、機能記述において読み出し命令を用いることにより、等価性検証に必要なデータの出力タイミングを指定する。そして、読み出し命令で指定されたタイミングでのみ等価性を検証出来るようにデータパス部データ及び制御部データを生成することで、検証を簡略化出来る。
【００４５】
また、例えば機能記述においてＸ＝Ａ＋Ｂ＋Ｃという式が存在したとして、等価性検証のために（Ａ＋Ｂ）の値が必要だったと仮定する。このような内部変数は、外部には出力されなくても等価性の検証には非常に役立つ場合や、または必須である場合がある。しかし、合成ツールはＸの値を一括して計算してしまい、（Ａ＋Ｂ）の値はデータパス部データ及び制御部データに反映されない可能性がある。この点、本実施形態であると読み出し命令によってデータパス部データ及び制御部データに反映されるべき値を指定する。すなわち上記の場合、（Ａ＋Ｂ）の値をデータパス部データ及び制御部データで観測出来るようになる。従って、等価性検証に必要な値を確実にデータパス部データ及び制御部データに反映させることが出来、等価性の検証を容易にすることが出来る。
【００４６】
なお、前述の通り機能記述は時間の概念を有しない。従って、例えば機能記述における行数を指定すること、またはいずれの命令に応答して得られる信号であるかを指定することによって、タイミングを指定することが出来る。また、読み出し命令は機能記述の外にあっても良い。すなわち、機能記述とは別のファイルに読み出し命令を保持させる。そして回路合成を行う際、ＣＰＵ４１が読み出し命令を保持したファイルをメインメモリ４２に読み出し、このファイル内の読み出し命令と設計データ４６とに基づいて回路合成を行っても良い。
【００４７】
図１２は、第２の実施形態の変形例に係る機能記述１０の模式図である。図１２に示す機能記述１０は、図１１に示す機能記述とは異なる読み出し命令を有する。すなわち、図４に示す機能記述１０において、指定範囲の最初を示す第１読み出し命令（CareStart(A, B)）が８行目と９行目との間に設けられ、指定範囲の最後を示す第２読み出し命令（CareEnd(A, B)）が最終行に設けられている。第１、第２読み出し命令は、これらに挟まれた１０〜１３行目の文で得られる値Ａ、Ｂが変化する度に、その値Ａ、Ｂを観測することを意味する。すなわち、１０〜１３行目で示される除算が行われる度に、その除算結果Ａ、Ｂが観測されるように、データパス部データ及び制御部データが生成されることになる。
【００４８】
以上のように、この発明の第１、第２の実施形態に係る回路記述言語の等価性検証法であると、形式的検証技術を用いて等価性を検証する。そして、ＲＴＬ記述同士を比較する際、等価性について過去に得られた情報を元に、全体の構成の中から等価である箇所を個々に見つけていく。その結果、等価であることが証明されなかった部分についてのみ、形式的検証を行う。これにより、等価性検証に必要な計算量を削減出来る。また、ＲＴＬ記述においてデータパス部データと制御部データの段階で等価性が検証される。従って、データパス部データに関して等価性が証明された場合、制御部データについてのみ形式的検証を行えば良く、計算量を削減出来る。これにより、検証を容易に出来るハードウェア設計記述の等価性検証方法を提供出来る。
【００４９】
なお、上記実施形態ではＣ言語ベースで記述された機能記述と、ハードウェア記述言語で記述されたＲＴＬ記述との間の等価性検証を例に挙げて説明した。しかし、例えば機能記述同士、またはＲＴＬ記述同士の等価性検証を行う場合でも、上記検証方法を適用出来る。図１３は機能記述同士で等価性検証を行う場合のフローチャートである。これは具体的には次のようなケースが考えられる。例えば、Ｃ言語ベースの回路記述言語を用いてある設計データ（第１設計データと呼ぶ）をプログラムしたとする。この場合、合成ツールに投入しても比較的良い回路が得られないが、両者の等価性は保証されているとする。そして、Ｃ言語ベースの回路記述言語を用いて、第１設計データと同一の機能を達成出来るように設計データ（第２設計データと呼ぶ）をプログラムしたとする。勿論、プログラムの記述内容は第１設計データと異なる。そして、第２設計データを合成ツールに投入して得られる回路は、第１設計データよりも優れていたとする。しかし第２設計データとＲＴＬ記述との間の等価性は検証されていない。このような場合、第１設計データと第２設計データとの等価性を検証し、等価である場合には第２設計データを以後用いることが出来る。
【００５０】
すなわち図１３に示すように、Ｃ言語ベースの回路記述言語を用いてそれぞれ機能記述１０、６０を作成する（ステップＳ１０、Ｓ３０）。そして、それぞれについて動作合成及び機能合成を行って（ステップＳ１４、Ｓ３２）、データパス部データ１５、６２及び制御部データ１６、６３を得る。その後、データパス部データ１５と６２との間の等価性、及び制御部データ１６と６３との間の等価性を、上記第１、第２の実施形態で説明した方法により検証する。
【００５１】
図１４はハードウェア記述言語で記述されたＲＴＬ記述同士を検証する場合のフローチャートである。図示するように、ハードウェア記述言語を用いてそれぞれＲＴＬ記述２０、７０を作成する（ステップＳ１５、Ｓ４０）。そして、それぞれについて機能合成を行って（ステップＳ１６、Ｓ４１）、データパス部データ２１、７２及び制御部データ２２、７１を得る。その後、データパス部データ２１と７２との間の等価性、及び制御部データ２２と７１との間の等価性を、上記第１、第２の実施形態で説明した方法により検証する。
【００５２】
また上記実施形態では、システムレベル設計に用いる記述言語としてＣ言語をベースに用いた言語の場合を例に説明したが、ハードウェア記述言語よりも抽象度の高い言語であれば特に限定されるものでは無い。
【００５３】
なお、本願発明は上記実施形態に限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で種々に変形することが可能である。更に、上記実施形態には種々の段階の発明が含まれており、開示される複数の構成要件における適宜な組み合わせにより種々の発明が抽出されうる。例えば、実施形態に示される全構成要件からいくつかの構成要件が削除されても、発明が解決しようとする課題の欄で述べた課題が解決でき、発明の効果の欄で述べられている効果が得られる場合には、この構成要件が削除された構成が発明として抽出されうる。
【図面の簡単な説明】
【００５４】
【図１】この発明の第１の実施形態に係る半導体集積回路の設計方法のフローチャート。
【図２】この発明の第１の実施形態に係る回路記述言語の等価性検証方法のフローチャート。
【図３】この発明の第１の実施形態に係る回路記述言語の等価性検証方法のフローチャート。
【図４】この発明の第１の実施形態に係る回路記述言語の等価性検証方法の模式図であり、機能記述とＲＴＬ記述の一例を示す図。
【図５】この発明の第１の実施形態に係る回路記述言語の等価性検証方法の模式図であり、機能記述とＲＴＬ記述の一例を示す図。
【図６】この発明の第１の実施形態に係る回路記述言語の等価性検証方法で用いられる対応関係ライブラリの模式図。
【図７】この発明の第１の実施形態に係る回路記述言語の等価性検証方法の模式図であり、ＲＴＬ記述における制御部の一例を示す図。
【図８】この発明の第１の実施形態に係る回路記述言語の等価性検証方法の模式図であり、ＲＴＬ記述における制御部の一例を示す図。
【図９】この発明の第１の実施形態に係る回路記述言語の等価性検証方法を実現する計算機の内部構成のブロック図。
【図１０】クロックと、それに同期するデータ信号のタイミングチャート。
【図１１】この発明の第２の実施形態に係る回路記述言語の等価性検証方法における機能記述の模式図。
【図１２】この発明の第２の実施形態の変形例に係る回路記述言語の等価性検証方法における機能記述の模式図。
【図１３】この発明の第１、第２の実施形態の第１変形例に係る回路記述言語の等価性検証方法のフローチャート。
【図１４】この発明の第１、第２の実施形態の第２変形例に係る回路記述言語の等価性検証方法のフローチャート。
【符号の説明】
【００５５】
１０…機能記述、１１…ＲＴＬ記述、１２…ゲートレベル論理回路、１３…マスクレイアウトデータ、１４、２０…スケジュール決定済みデータ、１５、２１…データパス部データ、１６、２２…制御部データ、１７…対応関係ライブラリ、１８、１９…検証方法ライブラリ、３０…加算器、３１…減算器、３２…比較器、３３…除算器、４０…計算機、４１…ＣＰＵ、４２…メインメモリ、４３…メモリ、４４…ディスプレイ、４５…入力装置、４６…設計データ、４７…制御部比較プログラム、４８…パス比較プログラム、４９…回路合成プログラム、５０…各種ライブラリ
【図１】
2007233648.tif 000003
【図２】
2007233648.tif 000004
【図３】
2007233648.tif 000005
【図４】
2007233648.tif 000006
【図５】
2007233648.tif 000007
【図６】
2007233648.tif 000008
【図７】
2007233648.tif 000009
【図８】
2007233648.tif 000010
【図９】
2007233648.tif 000011
【図１０】
2007233648.tif 000012
【図１１】
2007233648.tif 000013
【図１２】
2007233648.tif 000014
【図１３】
2007233648.tif 000015
【図１４】
2007233648.tif 000016