(57)【要約】【課題】検証対象モジュールに入力を与え、検証対象モジュールの出力を期待値と比較するシミュレーション環境を生成するＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムを提供する。【解決手段】回路記述を読み込む回路記述読込手段と、回路記述について最上位階層からモジュール間の信号接続関係を解析する解析手段と、検証対象モジュールへ入力を与えているモジュールのプロパティ記述から検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成するプロパティ生成手段と、プロパティ記述からテストベクタを発生し、ドライブ用テストベンチ記述を生成するドライブ用テストベンチ生成手段と、検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成するチェック用テストベンチ生成手段とを有する。【選択図】図１６
2006323856.tif 000002
【特許請求の範囲】
【請求項１】
論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能検証において、
前記回路記述を読み込む回路記述読込手段と、
前記回路記述について最上位階層からモジュール間の信号接続関係を解析する解析手段と、
検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、前記検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成するプロパティ生成手段と、
前記プロパティ記述からテストベクタを発生し、ドライブ用テストベンチ記述を生成するドライブ用テストベンチ生成手段と、
前記検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成するチェック用テストベンチ生成手段
とを有することを特徴とするＬＳＩ設計検証装置。
【請求項２】
前記ドライブ用テストベンチ記述および前記チェック用テストベンチ記述から、それらを並列実行する上位階層のトップ用テストベンチ記述を生成するトップ用テストベンチ生成手段と、
前記検証対象モジュールのモデル記述とのインタフェースとなるシミュレーション用の上位モデル記述を生成する上位モデル生成手段
とを更に有することを特徴とする請求項１記載のＬＳＩ設計検証装置。
【請求項３】
前記ドライブ用テストベンチ記述、前記チェック用テストベンチ記述、前記トップ用テストベンチ記述、及び前記上位モデル記述とからなるシミュレーション環境において、
論理シミュレーションを行う論理シミュレーション手段と、
コードカバレッジ計測を実行するコードカバレッジ計測手段と、
コードカバレッジ計測手段によりレポートされた非活性化コードについて、仕様上活性され得るかどうかを、検証対象モジュールへ入力を与えているモジュールのプロパティ記述から自動的に判定する自動判定手段
とを更に有することを特徴とする請求項１又は２記載のＬＳＩ設計検証装置。
【請求項４】
前記自動判定手段において、前記非活性化コードが、仕様上活性化され得ないと判定された場合、レポートされた非活性コードを削除する非活性コード削除手段と、その削除したファイルの行番号をレポートするレポート手段とを更に有することを特徴とする請求項３記載のＬＳＩ設計検証装置。
【請求項５】
前記自動判定手段において、前記非活性化コードが、仕様上活性化されうると判定した場合、レポートされた非活性コードを活性化させるランダム値生成制約テストベンチ記述を生成するランダム値生成制約テストベンチ生成手段を更に有することを特徴とする請求項３又は４記載のＬＳＩ設計検証装置。
【請求項６】
回路記述読込手段、解析手段、プロパティ生成手段、ドライブ用テストベンチ生成手段及びチェック用テストベンチ生成手段を備えるＬＳＩ設計検証装置を用いる、論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能検証方法において、
前記回路記述読込手段が前記回路記述を読み込むステップと、
前記解析手段が前記回路記述について最上位階層からモジュール間の信号接続関係を解析するステップと、
前記プロパティ生成手段が検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成するステップと、
前記ドライブ用テストベンチ生成手段が前記プロパティ記述からテストベクタを発生し、ドライブ用テストベンチ記述を生成するステップと、
前記チェック用テストベンチ生成手段が前記検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成するステップ
とを有することを特徴とするＬＳＩ設計検証方法。
【請求項７】
トップ用テストベンチ生成手段が前記ドライブ用テストベンチ記述及び前記チェック用テストベンチ記述から、それらを並列実行する上位階層のトップ用テストベンチ記述を生成するステップと、
上位モデル生成手段が前記検証対象モジュールのモデル記述とのインタフェースとなるシミュレーション用の上位モデル記述を生成するステップ
とを更に有することを特徴とする請求項６記載のＬＳＩ設計検証方法。
【請求項８】
前記ドライブ用テストベンチ記述、前記チェック用テストベンチ記述、前記トップ用テストベンチ記述、及び前記上位モデル記述とからなるシミュレーション環境において、
論理シミュレーション手段及びコードカバレッジ計測手段がそれぞれ論理シミュレーション及びコードカバレッジ計測を実行後、自動判定手段がコードカバレッジ計測によってレポートされた非活性化コードについて、仕様上活性され得るかどうかを、検証対象モジュールへ入力を与えているモジュールのプロパティ記述から自動的に判定するステップを有することを特徴とする請求項６又は７記載のＬＳＩ設計検証方法。
【請求項９】
前記自動的に判定するステップにおいて、前記非活性化コードが仕様上活性化され得ないと判定した場合、レポート手段が、レポートされた非活性コードを削除する処理およびその削除したファイルの行番号をレポートするステップを有することを特徴とする請求項８記載のＬＳＩ設計検証方法。
【請求項１０】
前記自動的に判定するステップにおいて、前記非活性化コードが仕様上活性化されうると判定した場合、ランダム値生成制約テストベンチ生成手段が、レポートされた非活性コードを活性化させるランダム値生成制約テストベンチ記述を生成する処理を行うステップを有することを特徴とする請求項８又は９記載のＬＳＩ設計検証方法。
【請求項１１】
論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能を検証するＬＳＩ設計検証装置を制御するためのプログラムであって、
前記回路記述を読み込む命令と、
前記回路記述について最上位階層から信モジュール間の号接続関係を解析する命令と、
検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成する命令と、
前記プロパティ記述からテストベクタを発生し、ドライブ用テストベンチ記述を生成する命令と、
前記検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成する命令
とを前記ＬＳＩ設計検証装置に実行させることを特徴とするＬＳＩ設計検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、フォーマル・ベリフィケーションの一つである回路記述とプロパティの比較を行うＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムに関するものである。
【背景技術】
【０００２】
半導体集積回路の設計プロセスでは、始めに、設計する集積回路に対して要求する回路動作及び機能を抽象度の高いＲＴＬ（レジスタ・トランスファ・レベル）により定義（ＲＴＬ記述）し、次に、論理合成処理によりＲＴＬ記述から半導体製造技術を考慮した抽象度の低いゲートレベルにより定義（ゲートレベル記述）し、最後に、ゲートレベル記述の上方からマスクパターンを作成し、実際の半導体集積回路の製造を行うという段階を経て行われている。
【０００３】
しかし、近年における回路の大規模化及び複雑化により、モデルとテストベクタを使用したこれまでの検証手法では、膨大な検証時間が必要となるほか、全てのケースを人間が考え出して検証することは限界に達している。そのため、近年では、フォーマル・ベリフィケーション（形式的論理検証）技術の一つであり、仕様と回路が一致しているかどうかを検証するプロパティチェックにより、回路記述とプロパティ（動作使用をある書式で表現したもの）とを比較する検証方法が導入され始めている。
【０００４】
ここでいうフォーマル・ベリフィケーションには、プロパティ・チェックと、論理等価性検証の二つの意味がある。「プロパティ・チェック」とは、設計した論理回路が設計仕様（プロパティ）を満たしているかどうかを検証することを意味する。そして、「論理等価性検証」とは、二つの回路が論理的に等価であるかどうかを検証することを意味する。ただし、論理等価性検証では、二つの回路が等しいかどうかを検証するだけで、設計者が意図したとおりの論理機能が実現できたかどうかはわからない。これを確かめるために、たとえば、シミュレーションやプロパティ・チェックが必要である。
【０００５】
通常、プロパティ・チェックでは、テストベクタによるシミュレーション検証手法に比べ、網羅的なチェックが行える。しかし、適応出来る回路規模に制約があるため、プロパティをモジュール毎に分割した上で、各モジュール毎にプロパティを検証する必要があり、モジュール間のプロパティ同士を検証することはできない。そのため、モジュール毎のプロパティは完全に独立してしまっており、プロパティ間の相関関係の正当性は検証されない。従って、各モジュール間のインタフェース仕様の最適化に関しては、マルチサイクルパス等において、たとえ仕様的にタイミング余裕があったとしても、シミュレーション波形等から手動で判断するしかない。そのため、各モジュール間のインタフェース仕様の最適化は非常に難しく、迂闊に調整を行うとタイミングがずれてしまい不具合を混入しかねないため、あまり行われていないという問題がある。
【０００６】
更に、近年ではランダムなテストベクタを自動生成するシミュレーション環境効率化ツールによって、複雑な条件下で発生する、いわゆるコーナーケースバグを抽出する手法が適用されている。しかし、このシミュレーション環境は検証者が検証対象モジュールのプロパティからマニュアルで構築するため、多くの時間を要し、かつ正確性に乏しい。また、ランダムに生成されるテストベクタは、仕様上入力されないテストベクタを多く含むため、シミュレーション時間が長期化してしまい、検証に多大な時間を要してしまう。
【０００７】
更に、シミュレーション時に、HDLソースコードの実行有無を計測して得られるコード活性化率について、非活性コード部分が実現している機能が、仕様上活性化し得るか否かの判断方法が確立されていないため、その非活性コード情報をもとにした冗長記述削除による面積削減が有効になされていない。
【発明の開示】
【発明が解決しようとする課題】
【０００８】
本発明は、外部モジュールのプロパティ情報（回路の動作仕様を専用の書式で表現したもの）から、検証対象モジュールに入力を与えるシミュレーション環境を自動生成し、また、検証対象モジュールのプロパティ情報から、検証対象モジュールの出力を期待値と比較するシミュレーション環境を自動生成し、これらを統合したシミュレーション環境を生成することにより、シミュレーション時間を短縮化したＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムを提供する。
【課題を解決するための手段】
【０００９】
本発明の第１の特徴は、論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能検証において、回路記述を読み込む回路記述読込手段と、回路記述について最上位階層から信号接続関係を解析する解析手段と、検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成するプロパティ生成手段と、プロパティ記述からテストベクタを発生し、入力するドライブ用テストベンチ記述を生成するドライブ用テストベンチ生成手段と、検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成するチェック用テストベンチ生成手段とを有するＬＳＩ設計検証装置としたことである。
【００１０】
本発明の第１の特徴に係るＬＳＩ設計検証装置では、仕様の正確性確認済みのモジュールのプロパティ記述から信頼性のあるテストベンチ記述を自動生成するドライブ用テストベンチ生成手段及びチェック用テストベンチ生成手段を有するため、テストベンチ記述作成に関わる時間を短縮することができ、シミュレーション時間を短縮することができる。
【００１１】
本発明の第２の特徴は、論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能検証方法において、（イ）回路記述を読み込むステップと、（ロ）回路記述について最上位階層から信号接続関係を解析するステップと、（ハ）検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成するステップと、（ニ）テストベクタを発生し、入力するドライブ用テストベンチ記述を生成するステップと、（ホ）検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成するステップとを有するＬＳＩ設計検証方法としたことである。
【００１２】
本発明の第２の特徴に係るＬＳＩ設計検証装置では、仕様の正確性確認済みのモジュールのプロパティ記述から信頼性のあるテストベンチ記述を自動生成するため、テストベンチ記述作成に関わる時間を短縮することができ、シミュレーション時間を短縮することができる。
【００１３】
本発明の第３の特徴は、論理演算機能を有する回路の構成要素を抽象化の度合いに応じて上位から下位まで複数の層に階層化してなる回路記述の論理シミュレーションを用いたＬＳＩの機能を検証するＬＳＩ設計検証装置を制御するためのプログラムであって、（イ）回路記述を読み込む命令と、（ロ）回路記述について最上位階層から信号接続関係を解析する命令と、（ハ）検証対象モジュールへ入力を与えているモジュールのプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成する命令と、（ニ）テストベクタを発生し、入力するドライブ用テストベンチ記述を生成する命令と、（ホ）検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力を比較するチェック用テストベンチ記述を生成する命令とをＬＳＩ設計検証装置に実行させるＬＳＩ設計検証プログラムとしたことである。
【００１４】
本発明の第３の特徴に係るＬＳＩ設計検証装置では、仕様の正確性確認済みのモジュールのプロパティ記述から信頼性のあるテストベンチ記述を自動生成する命令を有するため、テストベンチ記述作成に関わる時間を短縮することができ、シミュレーション時間を短縮することができる。
【発明の効果】
【００１５】
本発明によれば、外部モジュールのプロパティ情報から、検証対象モジュールに入力を与えるシミュレーション環境を自動生成し、また、検証対象モジュールのプロパティ情報から、検証対象モジュールの出力を期待値と比較するシミュレーション環境を自動生成し、これらを統合したシミュレーション環境を生成することにより、シミュレーション時間を短縮化したＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムを提供できる。
【発明を実施するための最良の形態】
【００１６】
次に図面を参照して、本発明の実施形態について説明する。以下の図面の記載において、同一又は類似の部分には同一又は類似の符号を付している。
【００１７】
（第１の実施の形態）
（ＬＳＩ設計検証装置の構成） 
図１に示す本発明の第１の実施の形態に係るＬＳＩ設計検証装置１は、中央演算処理装置（ＣＰＵ）２と、ＣＰＵ２に入出力制御装置３３を介して接続された入力装置３１及び出力装置３２と、ＣＰＵ２に接続された共通データベース４及び一時記憶装置３５とから少なくとも構成されている。ＣＰＵ２には、図示を省略したデータベース管理手段が備えられている。そして、共通データベース４との入出力が必要な場合は、このデータベース管理手段を介して、必要なファイルの格納場所を探し、ファイルの読み出し・書き込み処理がなされる。本実施の形態において、「共通データベース」とは、下位階層モジュール間の接続関係、モジュール間における信号の接続関係、信号毎のプロパティ情報などを格納する記憶装置である。
【００１８】
ＣＰＵ２には、共通データベース格納手段９、回路記述読込手段１０、解析手段１１、プロパティ読込手段１２、モジュール間プロパティ抽出手段１３、信号動作部分抽出手段１４、比較手段１５、不一致検出手段１６、レポート生成手段１７、冗長部削除手段１８、レジスタ挿入手段１９、波形表示手段２０が少なくとも含まれている。
【００１９】
共通データベース格納手段９は、階層間の信号接続関係のデータを共通データベース４に格納する。回路記述読込手段１０は、ＬＳＩ設計検証装置１に実験回路等の回路記述を読み込む。解析手段１１は、読み込んだ回路記述を上位階層から、モジュール間の接続関係及び信号の入出力関係を解析する。プロパティ読込手段１２は、共通データベース４から各検証対象モジュールのプロパティをＬＳＩ設計検証装置１に読み込む。モジュール間プロパティ抽出手段１３は、読み込んだ各検証対象モジュールのプロパティ中において、モジュール間の信号が含まれている箇所（以下、「モジュール間信号プロパティ」とする）のみを抽出する。信号動作部分抽出手段１４は、抽出されたモジュール間信号プロパティから各信号の出力側のモジュールにある出力動作が定義されたプロパティ（以下、「出力動作プロパティ」とする）と、入力側モジュールに存在する期待動作が定義されたプロパティ（以下、「期待動作プロパティ」とする）の信号動作部分を抽出する。比較手段１５は、出力動作プロパティと期待動作プロパティの信号動作部分を用いて、各信号の出力側と入力側のプロパティ同士を比較する。不一致検出手段１６は、プロパティ同士を比較した結果、比較対象モジュル間において共通の信号が仕様され、その信号がプロパティの条件として記述されている場合、条件同士が一致するか否かを判断し、不一致した条件を検出する。レポート生成手段１７は、不一致検出手段１６において不一致した条件を検出した場合、エラーとしてレポートを生成する。冗長部削除手段１８は、インタフェース仕様に余裕があり、階層設計手法を用いない場合、信号の冗長部分を削除する。レジスタ挿入手段１９は、インタフェース仕様に余裕があり、階層設計手法を用いる場合、信号の階層境界にレジスタを挿入する。波形表示手段２０は、レポート生成手段１７で生成されたレポートに基づき、不一致内容について関連する信号の時間変化を波形表示する。
【００２０】
入力装置３１は、キーボード、マウス、ＯＣＲ等の認識装置、イメージスキャナ等の図形入力装置、音声認識装置等の特殊入力装置などにより、出力装置３２は、液晶ディスプレイ、ＣＲＴディスプレイ等の表示装置、インクジェットプリンタ、レーザープリンタなどの印刷装置等によりそれぞれ構成される。入出力制御装置（入出力インタフェース）３３は、これらの入力装置３１、出力装置３２、あるいは図示を省略したＣＤ−ＲＯＭ、ＭＯ、ＺＩＰなどの記憶装置の読み取り装置等をＣＰＵ２につなぐインタフェースである。データの流れから見ると、入出力制御装置３３は、入力装置３１、出力装置３２、外部記憶装置の読み取り装置と主記憶装置３５とのインタフェースとなる。主記憶装置３５には、ＲＯＭ及びＲＡＭが組み込まれている。ＲＯＭは、ＣＰＵ２において実行されるプログラムを格納しているプログラム記憶装置等として機能する。ＲＡＭは、ＣＰＵ２におけるプログラム実行処理中に利用されるデータ等を一時的に格納したり、作業領域として利用される一時的なデータメモリ等として機能する。共通データベース４は、回路記述情報をモジュール単位で格納するための記憶装置であり、モジュール名データベース５を有する。
【００２１】
（第１の実施形態の全体のフロー）
図２は、本発明の第１の実施の形態に係るＬＳＩ設計検証方法を示したフロー図である。
【００２２】
（イ）まず、ステップＳ１１において、ＲＴＬ等の回路記述４１を読み込む。そして、ステップＳ１２において、回路記述４１を最上位（トップ）階層から解析し、第２階層（下位階層）モジュール間の接続関係を解析する。そして、（ａ）モジュール間に存在する信号は何か、（ｂ）その信号がどのモジュールから出力され、どのモジュールへの入力となっているのか、そして（ｃ）その信号がモジュール内部においてどのような信号名で接続されているのかを定義したデータを図４に示すような共通データベース４に記憶する。例えば、図３に示す回路記述４１をステップＳ１１において読込む。更に、ステップＳ１２において、最上位（ＴＯＰ）階層４５を解析することにより、乗算器（ＭＵＬＴ）４６と算術論理演算ユニット（ＡＬＵ）４７、ＭＵＬＴ４６とコントローラ（ＣＯＮ）４８、ＡＬＵ４７とＣＯＮ４８との接続関係を解析する。そして、解析された接続関係は、図４に示すような共通データベース４に記憶する。
【００２３】
（ロ）次に、ステップＳ１３において、各モジュールの比較したいプロパティ（各検証対象モジュールのプロパティ）をそれぞれ読み込み、共通データベース４から「モジュール間信号プロパティ」を検出し、抽出する。本発明の第１の実施形態では、プロパティＡ４２ａとプロパティＢ４３ａが読み込まれる。そして、共通データベース４からプロパティＡ４２ａ及びプロパティＢ４３ａのモジュール間プロパティ（プロパティＡ’４２ｂ及びプロパティＢ’４３ｂ）がそれぞれ検出され、抽出される。
【００２４】
（ハ）次に、ステップＳ１４において、ステップＳ１３で抽出されたモジュール間信号プロパティから、「出力動作プロパティ」と「期待動作プロパティ」の信号動作部分を抽出する。
【００２５】
（ニ）次に、ステップＳ１５において、ステップＳ１４で抽出された出力動作プロパティ（出力側）及び期待動作プロパティ（入力側）の信号動作部分を用いて、各信号の出力側と入力側のプロパティ同士を比較する。
【００２６】
（ホ）次に、ステップＳ１６において、比較対照となるモジュール間に、共通の信号が使用されていて、その信号がプロパティに条件として記述されている場合は、条件同士が一致するか否かを判断する。ステップＳ１６の判断の結果、条件同士が一致しない場合は、ステップＳ１７において不一致した条件を検出し、エラーとしてレポートを生成する。即ち、ステップＳ１６においてプロパティ同士を比較した結果、ステップＳ１７においてどちらか一方のプロパティが不足していれば、プロパティが存在する階層から不足分のプロパティを抜き出し、プロパティが存在しない階層の情報に変換する。このとき、関係する信号の時間変化を波形として画面に表示する。
【００２７】
（ヘ）ステップＳ１６の判断の結果、プロパティの条件が一致している場合は、ステップＳ１８において、インタフェース仕様に余裕があるか否かを判断する。インタフェース仕様に余裕がない場合は、そのまま処理を終了する。インタフェース仕様に余裕がある場合は、ステップＳ１９において、階層設計手法を用いるか否かを判断する。階層設計手法を用いる場合は、ステップＳ２０において、信号の階層境界にレジスタを挿入し、処理を終了する。階層設計手法を用いない場合は、ステップＳ２１において、信号の冗長部分を削除し、処理を終了する。
【００２８】
（実験回路の仕様）
次に、本発明の第１の実施の形態で使用する実験回路の仕様について、図３を参照しながら説明する。図３には、本発明の第１の実施の形態で使用する実験回路の回路図を示す。
【００２９】
本発明の第１の実施の形態で使用する実験回路は、トップと呼ばれる最上位階層と、乗算器（ＭＵＬＴ）４６、算術論理演算ユニット（ＡＬＵ）４７、及びコントローラ（ＣＯＮ）４８からなる第２階層（下位階層）からなる。図２に示すフローのステップＳ１１において、この回路が読み込まれると、ステップＳ１２において最上位階層から、モジュール間の接続関係を解析した結果、以下の（ａ）〜（ｄ）ような信号の入出力関係が解析される。
【００３０】
（ａ）図３に示すように、最上位階層には、４ビットデータからなる信号Ａ及び信号Ｂと、２ビットコマンドからなる外部入力信号（OP）と、クロック信号（CLK）と、リセット信号Ｂ（RESETB）とが入力される。そして、外部入力信号（OP）の内容に従って、信号Ａと信号Ｂの演算を行い、８ビットデータからなる結果信号（RESULT）として出力する。外部入力信号（OP）は、ＡＮＤ演算、加算、減算、乗算を選択することができる。
【００３１】
（ｂ）下位階層（第２階層）である乗算器（ＭＵＬＴ）４６には、信号Ａ、信号Ｂ、開始信号（STB）、クロック信号（CLK）、リセット信号Ｂ（RESETB）が入力される。ＭＵＬＴ４６では、開始信号がアサートしたら、信号Ａと信号Ｂとの乗算を行い、結果信号（RESULT）として出力する。そして、演算が終了すると、終了信号（Done）をアサートする。演算消費サイクルは信号Ｂのデータの内容により、１１〜１５サイクルで変化する。
【００３２】
（ｃ）下位階層（第２階層）であるＡＬＵ４７には、信号Ａ、信号Ｂ、外部入力信号（OP）、クロック信号（CLK）、リセット信号Ｂ（RESETB)が入力される。
【００３３】
ＡＬＵ４７では、外部入力信号（OP）の内容に従って、信号Ａと信号Ｂとの演算を行い、結果信号（RESULT）として出力する。外部入力信号（OP）は、ＡＮＤ演算、加算、減算を選択することができる。
【００３４】
（ｄ）下位階層（第２階層）であるコントローラ（ＣＯＮ）４８には、外部入力信号（OP）、乗算器（ＭＵＬＴ）４６の終了信号（Done）、８ビットからなるＭＵＬＴ４６の演算結果（R_M）、８ビットからなるＡＬＵ４７の演算結果（R_A）、クロック信号（CLK）、リセット信号Ｂ（RESETB)が入力される。ＣＯＮ４８では、外部入力信号（OP）の内容によって、ＡＬＵ４７、ＭＵＬＴ４６からの信号を演算結果（RESULT）として振り分けて出力する。また、ＣＯＮ４８は、ＭＵＬＴ４６を動作させる開始信号STBを制御する。更に、ＭＵＬＴ４６からの終了信号（Done）を待って、演算結果を出力する。そして、ＭＵＬＴ４６からの終了信号（Done）が１２サイクル後に８返ってこない場合は、エラーとする。
【００３５】
（共通ＤＢの作成方法）
次に、図４に共通データベース４を示す。共通データベース４には、最上位階層のモジュール名（第１項）、最上位階層のモジュールに含まれるモジュール名（第２項）、各モジュール毎の組み合わせ（第３項）、各モジュール間の接続情報（第４項）、抽出された信号に関連するプロパティ情報（第５項）、及び信号の組み合わせ毎に変換されたプロパティ情報（第６項）がモジュール毎に蓄積される。
【００３６】
例えば、図３に示すような最上位階層を解析した結果は、図４に示すように、まず、共通データベース４の第１項には、最上位階層のモジュール名「最上位（ＴＯＰ）」が記憶される。そして、「最上位（ＴＯＰ）４５」に含まれるモジュール名が第２項に記憶される。ここでは、「乗算器（ＭＵＬＴ）４６、コントローラ（ＣＯＮ）４８、算術論理演算ユニット（ＡＬＵ）４７」が第２項に記憶される。
【００３７】
次に、第３項では、第２項に記憶されている各モジュール毎の組み合わせ情報が記憶される。例えば、乗算器（ＭＵＬＴ）４６は、コントローラ（ＣＯＮ）４８及び算術論理演算ユニット（ＡＬＵ）４７との組み合わせが考えられるため、第２項のＭＵＬＴ４６に対応する第３項に、ＣＯＮ４８とＡＬＵ４７が記憶される。同様に、ＣＯＮ４８は、ＭＵＬＴ４６及びＡＬＵ４７との組み合わせが考えられるため、第２項のＣＯＮ４８に対応する第３項には、ＭＵＬＴ４６とＡＬＵ４７が記憶される。更に、ＡＬＵ４７は、ＭＵＬＴ４６及びＣＯＮ４８との組み合わせが考えられるため、第２項のＡＬＵ４７に対応する第３項には、ＭＵＬＴ４６とＣＯＮ４８が記憶される。
【００３８】
次に、第４項には、第２項で抽出した各モジュール間の接続情報を記憶する。例えば、第２項の乗算器（ＭＵＬＴ）４６は、第３項を見ると、ＭＵＬＴ４６とコントローラ（ＣＯＮ）、ＭＵＬＴ４６と算術論理演算ユニット（ＡＬＵ）４７の組み合わせが考えられ、これら２つの組み合わせのそれぞれの接続関係が第４項に記憶されることになる。従って、図４に示す実施例では、ＭＵＬＴ４６とＣＯＮ４８の接続関係として、「MULT: STB(STB), Done(Done), R_M(R_M) / CON: STB(STB), Done(Done), R_M(R_M) 」というＭＵＬＴ４６とＣＯＮ４８の接続関係が第４項に記憶される。そして、ＭＵＬＴ４６とＡＬＵ４７とは接続関係がないため、ＭＵＬＴ４６とＡＬＵ４７の接続関係を記憶する第４項には何も記載されない。
【００３９】
次に、第５項には、抽出された信号に関連するプロパティ情報が記憶される。即ち、モジュール乗算器（ＭＵＬＴ）４６とコントローラ（ＣＯＮ）４８との接続関係として第４項で抽出された信号（STB, Done, R_M）に関連するプロパティ情報を、ＭＵＬＴ４６及びＣＯＮ４８のそれぞれのプロパティから抽出し、第５項に記憶する。例えば、第４項で抽出された信号「STB, Done, R-M」を含むプロパティとして、ＭＵＬＴ４６側では、図５（ａ）に示すようなプロパティ情報が抽出され、ＣＯＮ４８側では、図５（ｂ）に示すようなプロパティ情報が抽出され、第５項に記憶される。
【００４０】
次に、第６項には、信号の組み合わせ毎に変換されたプロパティ情報がモジュール毎に蓄積される。即ち、第５項のプロパティから、２つのモジュール間に関連しない信号のプロパティをのぞき、関連する信号動作のプロパティのみを抽出したものを第６項に格納する。
【００４１】
（モジュール間信号プロパティの一例）
次にモジュールの１つである乗算器（ＭＵＬＴ）４６の単体検証用プロパティの一例を図５（ａ）に示す。ここでは、開始信号（STB）がアサートしてから、信号Ｂの値によって、１１〜１５サイクルで演算が完了することを検証する。そして、図５（ａ）のＣはサイクルを表し、「Ｃ１」の場合、１サイクル後を意味する。
【００４２】
図５（ｂ）には、コントローラ（ＣＯＮ）４８の単体検証用プロパティの一例を示す。ここでは、（イ）ＣＯＮ４８は、リセット解除後、外部入力信号（OP）が乗算（2'11）の時は３サイクル後に開始信号（STB）が１にアサートし、（ロ）ＣＯＮ４８は、リセット解除後、外部入力信号（OP）が乗算（2'b11）の時は乗算器（ＭＵＬＴ）４６の実行開始後、１２サイクル以内に終了信号（Done）が返ってきた場合は、正常終了（current_sate == 3'b100）となる、という２つの動作を検証する。
【００４３】
（実施例１−１：プロパティ間に不一致がある場合）
次に、図６〜図１３を用いて、本発明の第１の実施の形態に係るＬＳＩ設計検証方法において上述したＬＳＩ設計検証方法に即して、プロパティ間に不一致がある場合の実施例について説明する。
【００４４】
［処理手順１］
ステップＳ１１〜Ｓ１２に対応し、図６及び図７のステップＳ１０１〜Ｓ１３６までの処理において、最上位階層（トップ）から、下位階層（第２階層）モジュール間の信号の接続関係を示す信号リスト４０を作成する。本実施例１−１においては、乗算器（ＭＵＬＴ）４６、コントローラ（ＣＯＮ）４８、算術論理演算ユニット（ＡＬＵ）４７という３つの下位階層モジュール間の信号の接続関係を示す信号リスト４０が作成され、共通データベース４に格納される。図８（ａ）にＭＵＬＴ４６の入力接続関係を表す信号リスト４０ａ、図８（ｂ）にＣＯＮ４８の入力接続関係を表す信号リスト４０ｂの一例を示す。尚、本実施例１−１では、ＭＵＬＴ４６とＣＯＮ４８との関係についてのみ比較していくこととする。
【００４５】
（イ）まず、図６のステップＳ１０１において、最上位階層の回路記述であるＲＴＬファイル（ＲＴＬ回路記述）４１を読み込む。次に、ステップＳ１０２において、読み込んだＲＴＬファイル（ＲＴＬ回路記述）４１を一行読み込み、図２のステップＳ１２に対応して、モジュール間の信号の相関解析を開始する。
【００４６】
（ロ）次に、ステップＳ１０３において、モジュール宣言がなされているか否かを判断する。モジュール宣言がなされていない場合は、ステップＳ１０２の処理へ戻り、ＲＴＬファイル（ＲＴＬ回路記述）４１の次の一行を読み込む。ステップＳ１０３の判断において、モジュール宣言がなされている場合は、次のステップＳ１０４の処理へ進む。
【００４７】
（ハ）次に、ステップＳ１０４において、共通データベース４の第１項に、モジュール宣言がなされているモジュール名を格納する。そして、ステップＳ１０５において、モジュール名毎のデータベース（即ち、最上位階層毎のデータベース）を共通データベース４の中にモジュール名データベース５として作成する。
【００４８】
（ニ）次に、ステップＳ１０７において、モジュール名データベース５のデータを一行ずつ読み込み、ステップＳ１０８でモジュールブロックにある全てのデータを読み込んだか否かが判断される。モジュールブロックのデータの読み込みが終了していない場合は、ステップＳ１０６の処理へ戻り、データをモジュール名データベース５に書き込む。モジュールブロックのデータの読み込みが終了している場合は、ステップＳ１０９の処理へ進み、モジュール名データベース５を終了する。
【００４９】
（ホ）次に、ステップＳ１１０において、ＲＴＬファイル（ＲＴＬ回路記述）４１の最終行であるか否かが判断される。最終行ではない場合は、ステップＳ１０２の処理へ戻り、ステップＳ１０２からステップＳ１１０までの処理を繰り返す。最終行である場合は、ステップＳ１１１の処理へ進む。
【００５０】
（ヘ）ステップＳ１１１において、共通データベース４の最初のポイントへ移動する。次に、ステップＳ１１２において、共通データベース４を読み込み、ステップＳ１１３において、共通データベース４から第１項のモジュール名を読み出す。そして、ステップＳ１１４において、対応するモジュール名データベース５を読み出す。
【００５１】
（ト）ステップＳ１１５において、読み出したモジュール名データベース５のデータを一行読み込む。次に、ステップＳ１１６において、共通データベース４内にモジュール宣言されているものがあるか否かを判断する。モジュール宣言されているものがない場合は、ステップＳ１１５の処理へ戻り、読み出したモジュール名データベース５の次のデータを一行読み込む。モジュール宣言されているものがある場合は、ステップＳ１１７の処理へ進む。
【００５２】
（チ）ステップＳ１１７では、対応するモジュール名データベース５の第２項に検出したモジュール名の追加を行う。ステップＳ１１８において、モジュール名データの最終行であるか否かを判断する。 最終行でない場合は、ステップＳ１１２の処理へ戻り、ステップＳ１１２からステップＳ１１７までの処理を繰り返す。最終行である場合は、ステップＳ１１９において、モジュール名データをクローズする。
【００５３】
（リ）次に、ステップＳ１２０において、共通データベース４の最終モジュール名か否かを判断する。最終モジュール名ではない場合は、ステップＳ１１２からステップＳ１１９までの処理を繰り返す。最終モジュール名である場合は、ステップＳ１２１において、共通データベース４の最初のポイントへ移動する。
【００５４】
（ヌ）次に、ステップＳ１２２において、共通データベース４を読み込む。そして、ステップＳ１２３において、共通データベース４からモジュール名を読み出し、ステップＳ１２４において、対応するモジュール名データベース５を読み出す。
【００５５】
（ル）ステップＳ１２５において、第２項のデータがあるか否かを判断する。
【００５６】
第２項のデータがない場合は、ステップＳ１３６において、全処理を終了する。
【００５７】
第２項のデータがある場合は、ステップＳ１２６において、階層モジュール名として定義する。そして、ステップＳ１２７において、共通データベース４の最初のポイントへ移動する。
【００５８】
（ヲ）ステップＳ１２８において、共通データベース４を読み込み、ステップＳ１２９において対応するモジュール名データベース５を読み込む。そして、ステップＳ１３０において、下層モジュールを含むか否かが判断される。下層モジュールを含む場合は、ステップＳ１２６の処理へ戻り、階層モジュール名として定義し、ステップＳ１２６からＳ１２９までの処理を繰り返す。ステップＳ１３０において、下層モジュールを含まない場合は、ステップＳ１３１の処理へ進み、最上位モジュールとして定義する。
【００５９】
（ワ）ステップＳ１３２において、最上位モジュールの第２項のデータを読み出す。そして、ステップＳ１３３において、第２項のデータから２つずつのモジュールの組み合わせを作成し、第３項のデータとして共通データベース４に書き込む。
【００６０】
（カ）次に、ステップＳ１３４において、最上位モジュールのモジュール名データベース５から第３項のデータのモジュール間接続情報（端子、配線）を抽出し、第４項として書き出す。そして、ステップＳ１３５において、第３項のデータの最後であるか否かを判断する。第３項のデータの最後ではない場合は、ステップＳ１３４の処理を繰り返す。第３項のデータの最後である場合は、モジュール間の共通端子情報の抽出し処理を終了する。
【００６１】
[処理手順２]
次に、ステップＳ１２に対応して、共通データベース４に格納されている信号リスト４０から、下位階層（第２階層）モジュールである乗算器（ＭＵＬＴ）４６とコントローラ（ＣＯＮ）４８との間のインタフェース信号が含まれているプロパティ箇所のみを検出し、抽出する。例えば、ここでは、ＭＵＬＴ４６とＣＯＮ４８との間のインタフェース信号として、図８（ａ）に示すＭＵＬＴ４６の信号リスト４０ａから「CON.STB==MULT.STB」を、図８（ｂ）に示すＣＯＮ４８の信号リスト４０ｂから「MULT.Done==CON.Done」を抽出する。
【００６２】
図９を参照して、プロパティの検出・抽出フローについて説明する。
【００６３】
（イ）まず、ステップＳ２０１において、共通データベース４を読み込み、ステップＳ２０２において、共通データベース４から、第４項のデータ（モジュール間接続情報）を読み出す。第４項のデータとして、たとえば、図８（ａ）及び図８（ｂ）に示す信号接続関係を示すデータが読み込まれる。そして、ステップＳ２０２の処理後、ステップＳ２１０とステップＳ２２０の処理の両方へ同時に進む。
【００６４】
（ロ）まず、ステップＳ２１０において、ターゲット・プロパティ・フラグを初期化し「０」に設定する。また、ステップＳ２２０において、リファレンス・プロパティ・フラグを初期化し「０」に設定する。次に、読み込んだ共通データベース４の第４項のデータについて、ステップＳ２１１において共通端子に関するプロパティ（ターゲット）を、ステップＳ２２１において共通端子に関するプロパティ（リファレンス）をそれぞれ検索する。
【００６５】
（ハ）そして、ステップＳ２１２及びステップＳ２２２において、それぞれ共通端子に関するプロパティか否かを判断し、共通端子に関するプロパティではない場合は、ステップＳ２１１及びステップＳ２２１の処理へ戻り次の検索を開始する。共通端子に関するプロパティである場合は、ステップＳ２１３の処理へ進みターゲット・プロパティ・フラグを「１」に、ステップＳ２２３の処理へ進みリファレンス・プロパティ・フラグを「１」にそれぞれ設定する。
【００６６】
（ニ）次に、ステップＳ２１４及びステップＳ２２４において、それぞれ、図５（ａ）、（ｂ）に示すような共通端子に関するプロパティに対応するモジュールのプロパティ・ファイルを読み込む。そして、読み込んだプロパティ・ファイルから、ステップＳ２１５及びステップＳ２２５において、プロパティを一行読み込む。
【００６７】
（ホ）ステップＳ２１６及びステップＳ２２６において、第４項のデータの信号が含まれているか否かが判断される。第４項のデータが含まれている場合は、ステップＳ２１７、ステップＳ２２７の処理へそれぞれ進み、信号名を最上位階層での名称に変換し、プロパティを第５項へ書き出す。例えば、ターゲット側では、図８（ａ）の乗算器（ＭＵＬＴ）４６の入力接続関係を示す信号リスト４０ａから抽出された「CON.STB==MULT.STB」は、図５（ａ）に示すような「MULT:{if(C0(STB==1’b0)    C1(forever(STB==1’b1)){ (B == 4'b0000) == C1(C11(Done));(B == 4'b0001) == C1(C12(Done));・・・・・}」に変換され、第５項に格納される。更に、リファレンス側では、コントローラ（ＣＯＮ）４８の信号に関しても同様に「MULT.Done==CON.Done」は、図５（ｂ）に示すような「CON: {if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){(OP == 2’b11) == C2(STB == 1'b0)    C3(forever(STB == 1'b1));・・・・・} 」に変換され、第５項に格納される。ステップＳ２１６及びステップＳ２２６において、第４項のデータの信号が含まれていない場合は、ステップＳ２１８及びステップＳ２２８の処理へそれぞれ進む。
【００６８】
（ヘ）次に、ステップＳ２１８及びステップＳ２２８において、プロパティ・ファイルの最終行であるか否かが判断される。プロパティ・ファイルの最終行ではない場合、ステップＳ２１５及びステップＳ２２５の処理へ戻り、ステップＳ２１５〜Ｓ２１８、ステップＳ２２５〜Ｓ２２８までの処理をそれぞれ繰り返す。プロパティ・ファイルの最終行である場合は、ステップＳ２３０の処理へ進む。
【００６９】
（ト）ステップＳ２３０において、ターゲット・プロパティ・フラグが「１」であり、且つ、リファレンス・プロパティ・フラグが「１」であるか否かが判断される。ターゲット・プロパティ・フラグが「１」であり、且つ、リファレンス・プロパティ・フラグが「１」である場合は、ステップＳ２３４の処理へ進む。
【００７０】
ターゲット・プロパティ・フラグが「１」であり、且つ、リファレンス・プロパティ・フラグが「１」ではない場合は、ステップＳ２３１の処理へ進み、プロパティ不足メッセージを出力し、ステップＳ２３２の処理へ進む。そして、ステップＳ２３２では、プロパティ・フラグの片方が「１」になっているか否かが判断され、「１」になっていない場合は、ステップＳ２３４の処理へ進む。「１」になっている場合は、ステップＳ２３３の処理へ進み、不足プロパティを出力し、ステップＳ２３４の処理へ進む。
【００７１】
（チ）最後に、ステップＳ２３４において、第４項のデータの最後であるか否かが判断される。第４項のデータの最後ではない場合は、ステップＳ２０２の処理へ戻り、ステップＳ２０２からＳ２３４までの処理を繰り返す。第４項のデータの最後である場合は、プロパティの抽出処理を終了する。
【００７２】
[処理手順３]  
次に、ステップＳ１３に対応し、図１０のステップＳ３０１〜ステップＳ３３０までの処理において、ステップＳ１２で抽出されたモジュール間信号プロパティから、各信号の出力側のモジュールにある出力動作が定義されたプロパティと、入力側モジュールに存在する期待動作が定義されたプロパティの信号動作部分を抽出する。
【００７３】
（イ）まず、ステップＳ３０１において、共通データベース４を読み込み、ステップＳ３０２において、共通データベース４から第５項のデータを読み出す。
【００７４】
そして、ステップＳ３０２の処理後、ステップＳ３１０とステップＳ３２０の処理の両方へ同時に進む。
【００７５】
（ロ）先ず、ステップＳ３１０においてターゲット・モジュールのプロパティ、ステップＳ３２０においてリファレンス・モジュールのプロパティをそれぞれ読み込む。例えば、ターゲット・モジュールのプロパティとしては、図５（ａ）に示す乗算器（ＭＵＬＴ）４６のプロパティが、リファレンス・モジュールのプロパティとしては図５（ｂ）に示すコントローラ（ＣＯＮ）４８のプロパティがそれぞれ読み込まれる。
【００７６】
（ハ）次に、ステップＳ３１１及びステップＳ３２１において、共通端子以外のデータを抜き出す。そして、ステップＳ３１２及びステップＳ３２２において、次のプロパティを読み込む。
【００７７】
（ニ）ステップＳ３１３及びＳ３２３において、共通端子以外の置き換えが可能であるか否かが判断される。共通端子以外の置き換えが可能ではない場合、ステップＳ３１２及びＳ３２２の処理へ戻り、次のプロパティを読み込む。共通端子以外の置き換えが可能である場合は、ステップＳ３１４においてターゲット・プロパティを置き換え、ステップＳ３２４において、リファレンス・プロパティを置き換える。
【００７８】
（ａ）ここで、たとえば、終了信号（Done）に注目した場合、出力側が乗算器（ＭＵＬＴ）４６で、入力側がコントローラ（ＣＯＮ）４８となっている。また、開始信号（STB）に注目した場合、出力側がＣＯＮ４８で、入力側がＭＵＬＴ４６である。即ち、終了信号（Done）に注目すると、ＭＵＬＴ４６側が終了信号（Done）を生成しているため、ＭＵＬＴ４６のプロパティの左辺は終了信号（Done）が生成される場合の条件となる。この場合左辺は開始信号（STB）と信号Ｂによって構成されているが、信号ＢはＣＯＮ４８に入力しておらず、ＣＯＮ４８とＭＵＬＴ４６の間の相関を考えた場合、関係なくなり、ターゲット側のプロパティ（ＭＵＬＴ４６のプロパティ）は、「C0(STB==1'b0)))C1(forever(RESETB==1'b1))==C1(within15(Done))」となる。
【００７９】
（ｂ）一方、コントローラ（ＣＯＮ）４８側のプロパティは、図５（ｂ）又は図１１（ａ）に示すように、「if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){(OP == 2’b11)    C3(within12(Done)) == C3(within12(C1(current_state == 3'b100)));}」であるが、図１１（ｂ）の「(OP == 2’b11) == C2(STB == 1'b0)    C3(forever(STB == 1'b1));」のように証明されているため、「(OP == 2’b11) 」に「C2(STB == 1'b0)    C3(forever(STB == 1'b1))」を代入することにより、図１１（ｃ）に示すように、「if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){C2(STB == 1'b0)    C3(forever(STB == 1'b1))))C3(within12(Done)) == C3(within12(C1(current_state == 3'b100)));}」と変換することが可能となる。
【００８０】
（ホ）ステップＳ３１５及びステップＳ３２５において、共通データベース４の第６項にターゲット及びリファレンスプロパティを置き換えたデータを書き込む。そして、ステップＳ３３０において、全てのプロパティの置き換えが終了したか否かが判断される。全てのプロパティの置き換えが終了していない場合は、ステップＳ３０２の処理へ戻り、ステップＳ３０２からステップＳ３３０までの処理を繰り返す。全てのプロパティの置き換えが終了している場合は、プロパティ動作抽出処理（処理手順３）を終了する。
【００８１】
[処理手順４]
次に、ステップＳ１５に対応し、図１２のステップＳ４０１からステップＳ４１４までの処理において、乗算器（ＭＵＬＴ）４６側とコントローラ（ＣＯＮ）４８側のプロパティの比較を行う。
【００８２】
（イ）まず、ステップＳ４０１において、共通データベース４を読み込む。そして、ステップＳ４０２において、共通データベース４の第６項のプロパティ（図１１（ｃ）等）を読み出す。  次に、ステップＳ４０３において、それぞれのプロパティをソートし、ステップＳ４０４において、等価な式を削除する。
【００８３】
たとえば、図１１（ｃ）に示す、コントローラ（ＣＯＮ）４８側のプロパティは、「if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){C2(STB == 1'b0)    C3(forever(STB == 1'b1)))) C3(within12(Done)) == C3(within12(C1(current_state == 3'b100)));}」から等価な式を削除すると、「C0(STB == 1'b0)  C1(forever(STB == 1'b1)))) C1(within12(Done))」となる。即ち、開始信号（STB）が「０」から「１」に変化し１２サイクル以内に終了信号（Done）がアサートした場合を意味する。また、乗算器（ＭＵＬＴ）４６側のプロパティは、「C0(STB==1’b0)))C1(forever(STB==1’b1) == C1 (within15 (Done))」のままであり、開始信号（STB）が「０」から「１」に変化後、１５サイクル以内に終了信号（Done）がアサートすることを意味する。
【００８４】
（ロ）次に、ステップＳ４０５において、削除されなかった式が存在するか否かが判断される。削除されなかった式が存在しない場合は、比較処理を終了する。削除されなかった式が存在する場合は、ステップＳ４０６において、式を比較する。たとえば、本発明の第１の実施の形態の実施例１−１では、乗算器（ＭＵＬＴ）４６側のプロパティ「C0(STB==1’b0)))C1(forever(STB==1’b1) == C1 (within15 (Done))」と、コントローラ（ＣＯＮ）４８側のプロパティ「C0(STB == 1'b0)    C1(forever(STB == 1'b1)))) C1(within12(Done))」とが、ステップＳ４０６において、比較される。
【００８５】
（ハ）図２のステップＳ１３に対応し、ステップＳ４０７において、動作の辻褄が合っているか否かが判断される。辻褄があっていない場合は、ステップＳ４０８において、不一致情報を出力し、比較処理を終了する。即ち、本実施例１−１の場合、コントローラ（ＣＯＮ）４８側のプロパティで条件として使われている、終了信号（Done）のアサートまでのサイクル数は、実際に終了信号（Done）を生成している乗算器（ＭＵＬＴ）４６から見た場合、ＭＵＬＴ４６のサイクル数を満たさない場合があることがわかる。即ち、ＭＵＬＴ４６側は、開始信号（STB）が０から１に変化した後、１５サイクル以内に終了信号（Done）をアサートするが、コントローラ（ＣＯＮ）４８側は、開始信号（STB）が０から１に変化した後、１２サイクル以内に終了信号（Done）がアサートした場合を想定しているため、ＭＵＬＴ４６側が１３サイクルから１５サイクルで終了信号（Done）をアサートした場合、ＣＯＮ４８側では受け入れ体制が整っていないことになる。
【００８６】
尚、もし、ＣＯＮ４８側が１６サイクル以内に終了信号（Done）がアサートした場合を想定している場合は、ＣＯＮ４８はＭＵＬＴ４６に対して余裕を持っていることとなる。このような場合については、次の実施例（実施例１−２）において詳しく説明する。尚、動作の辻褄があっている場合は、ステップＳ４０９において、階層設計か否かが判断されるが、ステップＳ４０９〜ステップＳ４１４までの処理については、実施例１−２において説明することとする。
【００８７】
[処理手順５]
ステップＳ１７に対応して、図１２のステップＳ４０７において、乗算器（ＭＵＬＴ）４６とコントローラ（ＣＯＮ）４８とのプロパティ間に不一致があることが解析できたため、ステップＳ４０８において、不一致の内容をレポート（出力）し、開始信号（STB）と終了信号（Done）との関係を図１３に示すように波形表示する。
【００８８】
たとえば、図１１（ｂ）に示す記述は、「外部入力信号（OP）が「１１」の場合、２サイクル後に開始信号（STB）は「０」、３サイクル後に開始信号（STB）は「１」になる。」ことを示している。これを波形表示した場合、図１３の出力側の開始信号（STB）は、C0からC2までは「０」であり、C3で「１」になっていることが図１３に示すように波形表示される。
【００８９】
（実施例１−２：  冗長の削除）
次に、図１４と、前述してきた図２、図６乃至図１０、及び図１２を用いて、本発明の第１の実施の形態に係るＬＳＩ設計検証方法における実施例１−２として、図１２のステップＳ４１０の処理に係るプロパティ間に冗長な部分がある場合についての実施例を説明する。
【００９０】
図１４（ａ）、（ｂ）に、本発明の第１の実施の形態に係る実施例１−２で用いる乗算器（ＭＵＬＴ）４６及びコントローラ（ＣＯＮ）４８の単体検証用プロパティの一例を示す。また、トップ階層４５の仕様として、「外部入力Ｂは３以下である」という制約が追加されるため、更に「BB=4'b0011」を追加する。
【００９１】
[処理手順１]
実施例１−１と同様に、図２のステップＳ１１〜Ｓ１２に対応し、図６及び図７のステップＳ１０１〜Ｓ１３６までの処理において、最上位階層から下位階層（第２階層）モジュール間の信号の接続関係を示す信号リスト４０を作成する。
【００９２】
本実施例１−２では、乗算器（ＭＵＬＴ）４６、コントローラ（ＣＯＮ）４８、算術論理演算ユニット（ＡＬＵ）４７という３つの下位階層モジュール間信号の接続関係を示す信号リスト４０が作成され、共通データベース４に格納される。
【００９３】
尚、本実施例１−２では、ＭＵＬＴ４６とＣＯＮ４８との関係についてのみ比較検討していくこととする。図８（ａ）にＭＵＬＴ４６の入力接続関係、図８（ｂ）にＣＯＮ４８の入力接続関係を示す。
【００９４】
[処理手順２]
次に、ステップＳ１３において、共通データベース４に格納されている信号リスト４０から、下位階層（第２階層）モジュールである乗算器（ＭＵＬＴ）４６とコントローラ（ＣＯＮ）４８との間のインタフェース信号が含まれているプロパティ箇所のみを検出し、抽出する。ここでは、「CON.STB==MULT.STB」と「MULT.Done==CON.Done」とが抽出される。抽出されたこれらの信号に注目し、ＭＵＬＴ４６、ＣＯＮ４８のそれぞれの単体検証用プロパティ（図１４（ａ）、図１４（ｂ））から、終了信号Doneが関係するプロパティを抽出する。尚、本実施例１−２では、ＭＵＬＴ４６側、ＣＯＮ４８側共に全てのプロパティが対象となる。
【００９５】
[処理手順３]
ステップＳ１３において、ステップＳ１２で抽出されたモジュール間信号プロパティから、各信号の出力側のモジュールにある出力動作が定義されたプロパティと、入力側モジュールに存在する期待動作が定義されたプロパティの信号動作部分を抽出する。即ち、本発明の実施例１−２では、終了信号（Done）に関しては、出力側が乗算器（ＭＵＬＴ）４６で、入力側がコントローラ（ＣＯＮ）４８であり、開始信号（STB）に関しては、出力側がＣＯＮ４８で、入力側がＭＵＬＴ４６である。
【００９６】
更に、ステップＳ１３において、ＭＵＬＴ４６及びＣＯＮ４８の両方に関連する信号が含まれているプロパティを抽出し、共通データベース４に格納する。即ち、図１４（ａ）及び図１４（ｂ）に示すような、ＭＵＬＴ４６及びＣＯＮ４８の単体検証用プロパティ２０ｃ、２０ｄを抽出する。
【００９７】
次に、実施例１−１の処理手順３に対応して、図１０のステップＳ３１３〜Ｓ３１４、ステップＳ３２３〜Ｓ３２４において、まず、終了信号（Done）に関しては、乗算器（ＭＵＬＴ）４６側が生成しているため、図１４（ａ）に示すＭＵＬＴ４６の単体検証用プロパティにおける左辺は、終了信号（Done）が生成される場合の条件となる。このＭＵＬＴ４６側の左辺は、開始信号（STB）と信号Ｂにより構成されているが、信号Ｂはコントローラ（ＣＯＮ）４８に入力されておらず、ＣＯＮ４８とＭＵＬＴ４６との間の相関を考えた場合、ＭＵＬＴ４６側のプロパティは、「C0(STB==1'b0)))C1(forever(STB==1'b1)==C1(within13(Done)))」となる。
【００９８】
一方、終了信号（Done）に関して、ＣＯＮ４８は入力側である。ＣＯＮ４８側の単体検証用プロパティは、図１４（ｂ）に示すように「if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){(OP == 2'b11)    C3(within15(Done)) == C3(within15(C1(current_state == 3'b100)));}」であるが、図１４（ｂ）の「(OP == 2'b11) == C2(STB == 1'b0)    C3(forever(STB == 1'b1));」により、「(OP == 2'b11)」が既に証明されているため、「(OP == 2'b11)」に「C2(STB == 1'b0)    C3(forever(STB == 1'b1))」を代入することによって、「if{C0(RESETB == 1'b0)    C1(forever(RESETB == 1'b1)){C2(STB == 1'b0)    C3(forever(STB == 1'b1))    C3(within15(Done)) == C3(within15(C1(current_state == 3'b100)));}」と書き換えることができる。
【００９９】
[処理手順４]
次に、ステップＳ１５に対応し、図１２のステップＳ４０１からステップＳ４１４までの処理において、乗算器（ＭＵＬＴ）４６側とコントローラ（ＣＯＮ）４８側のプロパティの比較を行う。尚、ステップＳ４０１からＳ４０７までの処理は、実施例１−２と同じであるため違う点についてのみ簡単に説明する。
【０１００】
（イ）まず、ステップＳ４０１において、共通データベース４を読込み、ステップＳ４０２において、共通データベース４の第６項のプロパティ（図１４（ｃ）、（ｄ）等）を読み出す。次に、ステップＳ４０３において、それぞれのプロパティをソートし、ステップＳ４０４において、等価な式を削除する。
【０１０１】
（ロ）次に、ステップＳ４０５において、削除されなかった式が存在するか否かが判断される。削除されなかった式が存在しない場合は、比較処理を終了する。削除されなかった式が存在する場合は、ステップＳ４０６において、式を比較する。たとえば、本発明の第１の実施の形態の実施例１−２では、ＭＵＬＴ４６側のプロパティ「C0(STB==1'b0)))C1(forever(STB==1'b1)==C1(within13(Done)))」と、ＣＯＮ４８側のプロパティ「C0(STB == 1'b0)    C1(forever(STB == 1'b1))    C1(within15(Done))」とが、ステップＳ４０６において比較される。
【０１０２】
（ハ）図２のステップＳ１６に対応し、ステップＳ４０７において、動作の辻褄が合っているか否かが判断される。辻褄があっていない場合は、ステップＳ４０８において、不一致情報を出力し、比較処理を終了する。辻褄が合っている場合は、ステップＳ４０９の処理へ進み、階層設計であるか否かが判断される（ステップＳ１９に対応）。ステップＳ４０９において、階層設計でない場合は、ステップＳ４１０において、冗長な部分の情報を出力し（ステップＳ２１に対応）、処理を終了する。
【０１０３】
即ち、本実施例１−２の場合、コントローラ（ＣＯＮ）４８側のプロパティで条件として使われている終了信号（Done）のアサートまでのサイクル数は、実際に終了信号（Done）を生成している乗算器（ＭＵＬＴ）４６から見た場合、ＭＵＬＴ４６のサイクル数を満たすことがわかる。即ち、ＭＵＬＴ４６側は、開始信号（STB）が０から１に変化した後、１３サイクル以内に終了信号（Done）をアサートするが、ＣＯＮ４８側は、開始信号（STB）が０から１に変化した後、１５サイクル以内に終了信号（Done）がアサートした場合を想定しているため、余裕をもっていることがわかる。このとき、ＭＵＬＴ４６から見た２サイクルの冗長部分について、ユーザは、どのような処理を施すかを画面上に表示されるため、ユーザの判断によって、自動的に冗長部分の削減処理を行うことができる。
【０１０４】
[処理手順５]
（レジスタ挿入）
本実施例１−２では、コントローラ（ＣＯＮ）４８側に２サイクル冗長があることが判明されるため、ステップＳ２０に対応し、冗長な部分にレジスタを挿入する。ステップＳ４０９においてＣＯＮ４８側を階層設計する場合は、ステップＳ４１１の処理へ進み、ＲＴＬファイル（ＲＴＬ回路記述）４１を読み込む。ここで、ＣＯＮ４８を階層設計する場合、論理合成以降の処理で遅延計算を容易にするため、階層境界の入出力にフリップ・フロップ回路（F/F）を挿入する必要がある。
【０１０５】
そこで、ステップＳ４１２において、対象となる信号のレジスタ間から、コントローラ（ＣＯＮ）４８部分の記述を分離する。次に、ステップＳ４１３において、中間変数毎に分離することにより、レジスタ挿入可能箇所を特定する。そして、ステップＳ４１４において、レジスタ挿入に可能な個数の組み合わせで、中間変数毎に分離したＣＯＮ４８にレジスタを追加し、ファイルに出力し、比較処理を終了する。
【０１０６】
尚、ＣＯＮ４８の入力である終了信号（Done）は処理手順４より、Done回路に仕様サイクルのタイミング的に２サイクルの冗長があることが判明しているので、入力直後にフリップ・フロップ回路を挿入しても、論理的に不具合は発生しない。従って、ユーザの判断により、ＣＯＮ４８内の終了信号（Done）の直後にフリップ・フロップ回路を挿入することも可能である。
【０１０７】
（第１の実施の形態の効果）
本発明の第１の実施の形態によれば、階層間における接続関係をリストにすることで、下位階層（第２階層）で独立に作成されたプロパティ（群）から、階層間のインターフェースに関わるもののみを抽出することを可能とし、階層的プロパティチェック手法を可能とする。また、プロパティを外部入力の制約を考慮して、注目している階層間のインターフェース信号のみに変換することで、階層間の信号の受け渡し動作を明確にすることができる。更に、本発明の第１の実施の形態によれば、注目する信号に関わる複数のプロパティを統合し、最適化することで階層間の信号の受け渡し動作を明確にすることができる。
【０１０８】
更に、本発明の第１の実施の形態によれば、階層間のプロパティを比較し、インターフェース部分の不一致を検出出来るので、下位階層毎に独立に作成されていたプロパティを用いて、上位階層のインターフェースの検証を行うことができ、大規模回路の検証に対応することができる。更に、本発明の第１の実施の形態によれば、欠落しているプロパティを検出出来るので、プロパティチェック手法の質の向上へとつながる。更に、本発明の第１の実施の形態によれば、プロパティが欠落している際に、接続先モジュールのプロパティを利用し、追加作成の際の基礎として使用することにより、プロパティチェック手法の効率化が行える。
【０１０９】
更に、本発明の第１の実施の形態によれば、階層間におけるインターフェースの不一致を波形化することで、不一致箇所の特定を容易に行える。更に、本発明の第１の実施の形態によれば、階層間のプロパティを比較し、インターフェース部分の不一致を検出出来るので、下位階層毎に独立に作成されていたプロパティを用いて、上位階層のインターフェースの検証を行うことができ、大規模回路の検証に対応することができる。更に、本発明の第１の実施の形態によれば、階層設計を行う場合、論理合成以降の処理で遅延計算を容易するための、階層境界へのレジスタ挿入を不具合を混入することなく、確実に行うことができる。更に、本発明の第１の実施の形態によれば、仕様的な冗長部分を不具合を混入することなく、確実に削減することでき、品質の高い回路記述を作成することが出来る。
【０１１０】
本発明によれば、現在、完全に独立してしまっているモジュール毎のプロパティ同士を検証することにより、各モジュール間のインタフェース仕様の最適化を行うことのできるＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムを提供することができる。
【０１１１】
（第２の実施の形態）
（概念図）
図１５に本発明の第２の実施の形態に係るＬＳＩ設計検証方法の概念図を示す。図１５に示す統合シミュレーション環境８０は、論理シミュレーションにおける最上位のトップ用テストベンチ記述（検証専用言語）６８と、論理シミュレーションにおけるドライブ用テストベンチ記述（検証専用言語）６１と、論理シミュレーションにおける期待値チェック用テストベンチ記述（検証専用言語）６７と、検証対象モジュールの上位のテスト用モデル記述（ＨＤＬ）６４とから構成される。検証対象がモジュールＴである場合において、まず、検証対象モジュールＴを最上位モジュールのモデル記述（M(TOP)）から解析し、検証対象モジュールＴへ入力を与えるモジュールＩのモデル記述（M(I)）６０の入力接続関係（C(I)）及び検証対象モジュールＴの入力接続関係（C(T)）を得る。そして、ドライブ用テストベンチ記述６１は、検証対象モジュールＴへ入力を与えるモジュールＩのプロパティ記述（プロパティ言語）６２に基づき生成される。チェック用テストベンチ記述６７は、検証対象モジュールＴのプロパティ記述（プロパティ言語）６６に基づき生成される。上位のトップ用テストベンチ記述６８は、ドライブ用テストベンチ記述６１とチェック用テストベンチ記述６７とから構成される。また、上位テスト用モデル記述６４は、検証対象モジュールＴのモデル記述６３から生成される。更に、モデル記述６３は、レポート６５により非活性化コードをレポートする。
【０１１２】
（ＬＳＩ設計検証装置の構成） 
図１６に示す本発明の第２の実施の形態に係るＬＳＩ設計検証装置１は、本発明の第１の実施の形態で説明したように、中央演算処理装置（ＣＰＵ）２と、ＣＰＵ２に入出力制御装置３３を介して接続された入力装置３１及び出力装置３２と、ＣＰＵ２に接続された共通データベース４及び主記憶装置３５とから少なくとも構成されている。ＣＰＵ２には、図示を省略したデータベース管理手段が備えられていることは第１の実施の形態と同様である。
【０１１３】
ＣＰＵ２には、回路記述読込手段１０、解析手段１１、プロパティ生成手段２１、ドライブ用テストベンチ生成手段２２、チェック用テストベンチ生成手段２３、トップ用テストベンチ生成手段２４、上位モデル生成手段２５、論理シミュレーション手段２６、コードカバレッジ計測手段２７、自動判定手段２８が少なくとも含まれている。
【０１１４】
回路記述読込手段１０は、ＬＳＩ設計検証装置１に実験回路等の回路記述を読み込む。解析手段１１は、読み込んだ回路記述を上位階層から、モジュール間の接続関係及び信号の入出力関係を解析する。プロパティ生成手段２１は、検証対象モジュールへ入力を与えているプロパティ記述から、検証対象モジュールに接続した信号のみで構成されたプロパティ記述を生成する。ドライブ用テストベンチ生成手段２２は、プロパティ記述からテストベクタを発生し、入力するドライブ用テストベンチ記述を生成する。チェック用テストベンチ生成手段２３は、検証対象モジュールのプロパティ記述から、シミュレーション上の出力と仕様上の出力とを比較するチェック用テストベンチ記述を生成する。トップ用テストベンチ生成手段２４は、ドライブ用テストベンチ記述及びチェック用テストベンチ記述からそれらを並列実行する上位階層のトップ用テストベンチ記述を生成する。
【０１１５】
上位モデル生成手段２５は、検証対象モジュールのモデル記述とのインタフェースとなるシミュレーション用の上位モデル記述を生成する。論理シミュレーション手段２６は、ドライブ用テストベンチ記述、チェック用テストベンチ記述、トップ用テストベンチ記述、及び上位モデル記述とからなるシミュレーション環境において論理シミュレーションを行う。コードカバレッジ計測手段２７は、コードカバレッジ計測を実行する。自動判定手段２８は、コードカバレッジ計測によりレポートされた非活性化コードについて、仕様上活性され得るかどうかを検証対象モジュールへ入力を与えているモジュールのプロパティ記述から自動的に判定する。
【０１１６】
（第２の実施形態の全体フロー）
図１７は、本発明の第２の実施の形態に係るＬＳＩ設計検証方法を示したフロー図である。
【０１１７】
（イ）まず、ステップＳ３１において、回路記述を最上位モジュールのモデル記述M(TOP)５９から解析し、モジュール階層構造、モジュール間に存在する信号は何か、またその信号がどのモジュールから出力され、どのモジュールへの入力となっているのかを解析する。検証対象モジュールTの入力信号を出力している或るモジュールをモジュールIとするとき、モジュールIの入力接続関係（C(I)）６９（ａ）及びモジュールTの入力接続関係（C(T)）６９（ｂ）を得る。
【０１１８】
（ロ）次に、ステップＳ３２において、モジュールIのプロパティ記述P(I)６２より、出力が検証対象モジュールTへの入力となっている信号名を含むプロパティ記述（P(I--T)）７４を抽出する。
【０１１９】
（ハ） 次に、ステップＳ３３において、ステップＳ３２で抽出されたプロパティ記述（P(I--T)）７４からドライブ用テストベンチ記述T(drive)６１を生成する。
【０１２０】
（ニ）ステップＳ３４において、検証対象モジュールＴのプロパティ記述P(T)６６がある場合、これをもとに統合シミュレーション環境８０上の出力値と仕様上の出力期待値とを比較するチェック用テストベンチ記述T(check)６７を生成する。検証対象モジュールＴのプロパティ記述P(T)６６がない場合、使用者がマニュアルでチェック用テストベンチ記述T(check)６７を記述する。
【０１２１】
（ホ）ステップＳ３５において、ドライブ用テストベンチ記述T(drive)６１及びチェック用テストベンチ記述T(check)６７をコンカレントに実行する上位のテストベンチ記述T(TOP)６８を生成し、これと検証対象モジュールＴのモデル記述M(T)６３とのインタフェースとなるシミュレーション用の上位のモデル記述M(TEST)６４を生成し、上位のテストベンチ記述T(TOP)６８、ドライブ用テストベンチ記述T(drive)６１、チェック用テストベンチ記述T(check)６７およびシミュレーション用の上位のモデル記述M(TEST)６４からなる統合シミュレーション環境８０を得る。
【０１２２】
（ヘ）ステップＳ３６において、ステップＳ３５で得た統合シミュレーション環境８０において、生成されるランダム値集合の基になるランダムシード値（SEED）を設定して、モジュールＴのモデル記述M(T)６３を対象とした論理シミュレーションを実行する。同時にモジュールＴのモデル記述M(T)６３のコードカバレッジ計測を実行する。
【０１２３】
（ト）ステップＳ３７において、チェック用テストベンチ記述T(check)６７により統合シミュレーション環境８０上の出力値と使用上の出力期待値とが一致するか否かが判断される。チェック用テストベンチ記述T(check)６７により統合シミュレーション環境８０上の出力値と仕様上の出力期待値との不一致がレポートされた場合、ステップＳ３８において、エラーレポート６５ａより使用者がＨＤＬ記述を修正する。チェック用テストベンチ記述T(check)６７により統合シミュレーション環境８０上の出力値と仕様上の出力期待値との一致がレポートされた場合、ステップＳ３９の処理へ進む。
【０１２４】
（チ）ステップＳ３９において、ステップＳ３６のコードカバレッジレポート６５ｂのレポートから非活性化コードの有無を判断する。ステップＳ３９の判断において、非活性化コードがない場合、そのまま処理を終了する。ステップＳ３９の判断において非活性化コードがある場合、ステップＳ４０の判断へ進む。
【０１２５】
（リ）ステップＳ４０において、ステップＳ３２で得たモジュールＩのプロパティ記述P(I)６２から仕様的に活性化される可能性の有無について判断する。仕様上活性化され得ないと判定した場合、ステップＳ４１において、その非活性化コードを削除し、削除された非活性コードの行番号を削除レポート７０としてレポートした後、ステップＳ３６により再度シミュレーションを実行する。
【０１２６】
（ヌ）ステップＳ４０で活性化され得ると判定した場合、ステップＳ４２において、仕様上活性化されない可能性の有無について判断する。ステップＳ４２において、活性化されない可能性がない場合、ステップＳ４３の処理へ進む。
【０１２７】
ステップＳ４３において、そのコードを活性化させるランダム値生成制約用テストベンチ記述T(drive-cst)７１を生成し、ステップＳ３１へ戻る。ステップＳ４２において、活性化されない可能性がある場合、ステップＳ４４の処理へ進む。
【０１２８】
ステップＳ４４において、前回の非活性化コードが活性されないかどうか判断する。活性化される場合、ステップＳ４５の処理へ進む。
【０１２９】
（ル）ステップＳ４５において、ステップＳ４４の判断で活性化され得るか、され得ないか判定不能な場合、ステップＳ３６における前シミュレーションの非活性化コードの中で活性化されたコードがないか確認する。新たに活性化されたコードがない場合は、処理を終了する。新たに活性化されたコードがある場合は、テストパタン数（NUM）を増加させるランダム値制約用テストベンチ記述（T(drive-cst)）７１を生成し、かつ、ランダムシード値（SEED）を変更し、新たなランダムシード値７２を生成し、新たなNUM値（テストパタン数）７３を生成し
、ステップＳ３６により再度シミュレーションを実行する。ステップＳ４４において、前回の非活性化コードが活性されない場合、処理を終了する。
【０１３０】
（実験回路の仕様）
次に、本発明の第２の実施の形態で使用する実験回路の仕様について、図１８、図１９を参照しながら説明する。図１８には、本発明の第２の実施の形態で使用する実験回路の回路図を示す。図１９には、本発明の第２の実施の形態で使用する実験回路ＡＬＵ内のモジュール構成を示す。
【０１３１】
本発明の第２の実施の形態で使用する実験回路は、最上位階層（ＴＯＰ）７５と、第２階層（下位階層）であるコントローラ（ＣＯＮ）７６及び算術論理演算ユニット（ＡＬＵ）７７とからなる。上述した検証対象モジュールＴをＡＬＵ７７、モジュールＴへの入力となる既存モジュールＩをＣＯＮ７６とした場合について、本発明の第２の実施の形態に係るＬＳＩ設計検証方法を用いて、モデル記述M(ALU)の論理機能を確認するシミュレーション環境を自動生成する方法について以下に説明する。
【０１３２】
最上位階層のモデル記述M(TOP)５９から、モジュール間の接続関係を解析した結果、以下の（ａ）〜（ｃ）のような信号の入出力関係が解析される。
【０１３３】
（ａ）図１８に示すように、最上位階層モデル記述M(TOP)５９には、１９ビットデータからなる入力信号（IN）と、クロック信号（CLK）とが入力され、８ビットデータからなる出力信号（OUT）を出力する。ここで入力信号（IN）は、８ビットからなるデータＡ及びデータＢと、３ビットからなる外部入力信号OP（オペレータ情報）から構成される。外部入力信号（OP）は、ＡＮＤ、ＯＲ、ＥＸ−Ｏ、加算、減算の論理演算あるいは「０」を算出することができる。そして、入力信号（IN）が入力されると、外部入力信号（OP）により、データＡとデータＢの演算を行い、演算結果を出力信号（OUT）に出力する。
【０１３４】
（ｂ）次に、下位階層（第２階層）であるパラレル入力シリアル出力コンバータ（ＣＯＮ）７６には、１９ビットデータからなる入力信号Ｃ（CIN）と、クロック信号（CLK）とが入力され、６ビットデータからなる出力信号Ｃ（COUT）、２ビットコマンドからなるセレクタＣ（CSEL)、リセット信号Ｃ（CRESET）を出力する。ＣＯＮ７６は、エンプティ状態及びフル状態からなる２つの内部状態を有し、(1)エンプティ状態の場合は入力信号Ｃ（CIN）をレジスタＡ（８ビット）、レジスタＢ（８ビット）、外部入力信号OP（オペレータ情報）（３ビット）に振り分けフル状態にし、(2)フル状態の場合は、次のシーケンスで信号を出力する：
CRESET=1 -- CRESET=0 -- CRESET=1,CSEL=00,COUT=A -- CSEL=01,COUT=B -- CSEL=10,COUT=OPそして、このシーケンスで信号を出力した後、エンプティ状態に戻る。
【０１３５】
（ｃ）次に、下位階層（第２階層）であるシーケンシャル入力（ＡＬＵ）７７には、８ビットデータからなる入力信号Ａ（AIN）と、２ビットコマンドセレクタＡ（ASEL）と、リセット信号Ａ（ARESET）と、クロック信号（CLK）とが入力され、出力信号Ａ（AOUT）が出力される。そして、まず、(1)入力信号Ａ（AIN）をコマンドセレクタＡ（ASEL）の値によって各レジスタＡ（８ビット）、レジスタＢ（８ビット）、及び外部入力信号OP（オペレータ情報）（３ビット）へ格納する。即ち：
「ASEL=2’b00」のとき入力信号Ａ（AIN）をレジスタＡに格納し、
「ASEL=2’b01」のとき入力信号Ａ（AIN）をレジスタＢに格納し、
「ASEL=2’b10」のとき入力信号Ａ（AIN）[2:0]を外部入力信号OP（オペレータ情報）に格納する；
(2)外部入力信号OP（オペレータ情報）に値が格納されると、データＡとデータＢに演算ＯＰを施し、次のサイクルで結果を出力信号Ａ（AOUT）に出力する。外部入力信号OP（セレクタＡ（ASEL）信号）によってＡＮＤ（000）、ＯＲ(001)、ＥＸ−Ｏ（010）、加算（011）、減算（100）、０出力（それ以外）を変える；(3)リセット信号Ａ（ARESET）がアサートされたら全レジスタ値を０にする。
【０１３６】
（実施例２−１）
次に、図１７〜図３９を用いて、本発明の第２の実施の形態に係るＬＳＩ設計検証方法について上述したＬＳＩ設計検証方法に即した実施例について説明する。
【０１３７】
［処理手順１］  
まず、図１７のステップＳ３１に対応して、まず、図２０のステップＳ５０１において、最上位モジュールのモデル記述M(TOP)５９から回路記述を読み込み、ステップＳ５０２において、回路モジュールの階層構造および下位階層（第２階層）間の信号接続関係を解析する。そして、ステップＳ５０３において、実施回路のモジュール構造を取得した後、ステップＳ５０４において、モジュールIの入力接続関係C(I)６９ａおよびモジュールTの入力接続関係C(T)６９ｂを抽出する。即ち、以下の説明においては、モジュールIの入力接続関係C(I)６９ａをCONの入力接続関係C(CON）として、モジュールTの入力接続関係C(T)６９ｂをALUの入力接続関係C(ALU)として抽出する。
【０１３８】
図２１に本発明の第２の実施の形態における実施回路のモジュール構造を示す。図２１に示すモジュール構造では、「モジュール名（ＨＤＬ記述におけるインスタンス名）」というように、括弧の左側にはモジュール名、括弧内にはＨＤＬ記述におけるインスタンス名を表す。図２１に示すように、最上位回路トップ７５には、コントローラ（ＣＯＮ）７６及び算術論理演算ユニット（ＡＬＵ）７７が含まれる。そして、ＡＬＵ７７は、レジスタ選択コントローラ（SELECTOR）、データA保持用レジスタ（AREG）、データB保持用レジスタ（BREG）、オペレータOP保持用レジスタ（OPREG）、演算回路（alu8）、演算結果OUT保持用Ｒレジスタ(RREG)を有する。
【０１３９】
次に、図２２（ａ）にコントローラ（ＣＯＮ）７６の入力接続関係C(CON)、図２２（ｂ）にＡＬＵ７７の入力接続関係C(ALU)をそれぞれ示す。図２２（ａ）に示すＣＯＮ７６の入力接続関係C(CON)では、外部入力信号PI.CLKはＣＯＮ７６の信号CON.CLK、外部入力信号PI.INはＣＯＮ７６の入力信号CON.CINであることを示す。また、図２２（ｂ）に示すＡＬＵ７７の入力接続関係C(ALU)では、外部入力信号PI.CLKはＡＬＵ７７の信号ALU.CLK、ＣＯＮ７６の出力信号CON.COUTはＡＬＵ７７の入力信号ALU.AIN、ＣＯＮ７６の信号CON.CSELはＡＬＵ７７の信号ALU.ASEL、ＣＯＮ７６のリセット信号CON.CRESETはＡＬＵ７７のリセット信号ALU.ARESETであることを示す。
【０１４０】
［処理手順２］
次に、ステップＳ３２に対応して、図２３のステップＳ５０６において、モジュールＴのプロパティ記述P(T)６６およびモジュールIのプロパティ記述P(I)６２を取得する。そして、モジュールＴのプロパティ記述P(T)６６をモジュールＡＬＵ７７の単体検証用プロパティ記述P(ALU)として、モジュールIのプロパティ記述P(I)６２をモジュールＣＯＮ７６の単体検証用プロパティ記述P(CON)として以下に示す。
【０１４１】
本発明の第２の実施の形態に係る実施例２−１において、モジュールTのプロパティ記述P(T)をモジュールＡＬＵ７７の単体検証用プロパティ記述P(ALU)として、モジュールIのプロパティ記述P(I)６２をモジュールＣＯＮ７６の単体検証用プロパティ記述P(CON)として以下に示す。
【０１４２】
ＡＬＵ７７の単体検証用プロパティ記述P(ALU)は、前述した本発明の第２の実施の形態の実施回路仕様におけるＡＬＵ７７の動作(1)、(2)、(3)を検証するためのプロパティ記述P(ALU-1)、P(ALU-2)、P(ALU-3)より構成され、モジュールＣＯＮ７６の単体検証用プロパティ記述P(CON)は、ＣＯＮ７６の動作(1)、(2)を検証するためのプロパティ記述P(CON-1)、P(CON-2)より構成される。図２４（ａ）にＡＬＵ７７の単体検証用のプロパティ記述P(ALU)、図２４（ｂ）にＣＯＮ７６の単体検証用プロパティ記述P(CON)を示す。ここで、プロパティ記述では、実回路の階層構造に即した記述をする必要があるため、例えばＡＬＵ７７のレジスタＡは、TOP.ALU.AREG.outのように記述する必要があるが、簡略化のため単にＡと表記する。また、図２４（ａ）〜（ｃ）において、「Cn」の「ｎ」は「ｎサイクル後」を表す。例えば、「C0(ASEL==2'b00)==C1(A==AIN)」という記述における「C0」は「０サイクル後」、「C1」は「１サイクル後」を表す。
【０１４３】
次に、モジュールIのプロパティ記述P(I)６２について、モジュールTに関係した信号のみで構成されたプロパティ記述P(I--T)７４を抽出する。プロパティ記述P(I--T)７４は次の処理Ａにより得られるため、ステップＳ５０７において、処理Ａを実行する。
【０１４４】
[処理A]
（イ）まず、ステップＳ５０８において、プロパティ記述P（I）６２について、モジュールIの出力信号名を検索する（即ち、図２４（ｂ）に示すプロパティ記述P(CON)について、ＣＯＮ７６の出力信号名を検索する。）。
【０１４５】
（ロ）次に、ステップＳ５０９において、検索された信号名について、ステップＳ５０１〜Ｓ５０４までの処理手順１で得たモジュールTの入力接続関係C(T)６９（ｂ）の左辺に信号名があるか否かを判断する。ない場合はステップＳ５１１において、その項を消去し、左辺に信号名がある場合はステップＳ５１０においてそのままにする（即ち、検索された信号名について、図２２（ｂ）に示す算術論理演算ユニット（ＡＬＵ）７７の入力接続関係C(ALU)の左辺に信号名がない場合はその項を消去し、左辺に信号名がある場合はそのままにする。）。
【０１４６】
（ハ）最後に、記述の途中の場合は（イ）の処理に戻って途中の行から検索し、記述の終端の場合は、ステップＳ５１２において、プロパティ記述P(I)について、プロパティ記述P(I--T)を抽出し、終了する。
【０１４７】
以上の処理Ａを図２４（ｂ）に示すプロパティ記述P(CON-1)およびプロパティ記述P(CON-2)に適用すると、プロパティ記述P(CON-1)は全て消去され、プロパティ記述P(CON-2)より図２４（ｃ）に示すプロパティ記述P(CON--ALU)を得る。
【０１４８】
［処理手順３］
次に、ステップＳ３３に対応して、図２５のステップＳ５１４〜ステップＳ５２６の処理において、処理手順２で得られたプロパティ記述P(I--T)７４（図２４（ｃ）P(CON--ALU)）より、ドライブ用テストベンチT(drive)６１を生成する。テストベンチ記述はタスク部とクラス宣言部からなる。よって、ドライブ用テストベンチ記述T(drive)６１は、ドライブ用タスク部テストベンチ記述T(drive_TASK)６１ａとドライブ用クラス宣言部テストベンチ記述T(drive_DECLARE)６１ｂとにより構成される。タスク部では、実質的な処理シーケンスが記述される。
【０１４９】
ドライブ用タスク部テストベンチ記述T(drive_TASK)６１ａは、処理Aで得られたプロパティ記述P(I--T)７４に次の処理Ｂを施して得られる。図２５を用いて、処理Ｂのフローを説明する。
【０１５０】
[処理B]    
まず、図２５のステップＳ５１４において、プロパティ記述P(I--T)を取得し、ステップＳ５１５において、処理Ｂを実行する。
【０１５１】
（イ）ステップＳ５１６において、モジュールTの入力接続関係C(T)６９ｂの左辺の信号名を右辺の信号名に変換する。即ち、図２２（ｂ）に示すモジュールALUの入力接続関係C(ALU)の左辺の信号名を右辺の信号名に変換する。
【０１５２】
（ロ） 次に、ステップＳ５１７において、値が固定されてないモジュールTへの入力信号（IN）をランダム生成値が割り当てられる記述“rand.IN”に変換する。尚、この際にビット幅を調整する。即ち、ＡＬＵ７７への入力Ａ（AIN）ををrand.INNに変換し、ビット幅を調整する。
【０１５３】
（ハ） 次に、ステップＳ５１８において、時相に関する記述を抽出し、ステップＳ５１９において、抽出した時相に関する記述が絶対時間であるか否かを判断する。絶対時間である場合は、ステップＳ５２０において、絶対時間から相対時間へ変換する。ステップＳ５１９の判断において、抽出した時相に関する記述が既に絶対時間である場合は、ステップＳ５２１の処理へ進む。
【０１５４】
（ニ） ステップＳ５２１において、条件文以外において、DUT(被検証回路)の信号のサンプル値と期待値の比較を表現する“==”をドライブを表現する“=”へ変換し、“““”を“,”へ変換する。例えば、処理Aで取得したプロパティ記述P(CON--ALU)において、「C2((CRESET==1’b1))) (CSEL==2’b00))) (COUT==A));」という記述は、（ハ）の処理で「C2((ARESET==1’b1))) (ASEL==2’b00))) (AIN==rand.A));」となっているものを「C2((ARESET=1’b1),(ASEL=2’b00),(AIN=rand.A));」というように変換する。
【０１５５】
（ホ）次に、ステップＳ５２２において、一連のテストパターンのシーケンスを繰り返し入力するためのforループ記述を追加する。このとき繰り返す回数をNUMとする。また、ステップＳ５２３において、チェック部の比較が終了するまで次のテストベクタの入力を待つ必要があり、nサイクル待つ“@n”を記述する(nは処理手順4で決定する)。即ち、ステップＳ５２１で得た「C2((ARESET=1’b1),(ASEL=2’b00),(AIN=rand.A));」中の「C2」は、ここで「@1」に変換する。そして、記述の終わりに「@n」を加える。
【０１５６】
（ヘ） ステップＳ５２４において、シミュレーション終了記述‘exit(0)’、変数宣言、タスクブロック化する記述“task  タスクが属するクラス名名:::タスク名名(){{処理シーケンス本体体}”を追加する。
【０１５７】
（ト）以上のステップＳ５１４〜Ｓ５２４までの処理Bを本発明の第２の実施の形態に係る実施例２−１に適用すると、ステップＳ５２５において、図２６（ａ）に示すドライブ用タスク部テストベンチ記述T(drive_TASK)６１ａを得られる。
【０１５８】
（チ）次に、ステップＳ５２６において、ドライブ用クラス宣言部テストベンチ記述T(drive_DECLARE)６１ｂを生成する。クラス宣言部では、変数宣言およびタスク宣言が記述される。ランダム生成値を割り当てる変数はタスク内でなく、クラス宣言内で宣言する。変数宣言の変数名は処理B（ロ）より、タスク宣言の宣言名はステップＳ５２４により得られる。以上の処理を本発明の第２の実施の形態に係る実施例に適用し、図２６（ｂ）に示すドライブ用クラス宣言部テストベンチ記述T(drive_DECLARE)６１ｂを得る。
【０１５９】
［処理手順４］
次にステップＳ３４において、チェック用テストベンチ記述T(check)６７を生成する。チェック用テストベンチ記述T(check)６７は、ドライブ用テストベンチ記述T(drive)６１同様、チェック用タスク部テストベンチ記述T(check_TASK)６７ａとチェック用クラス宣言部テストベンチ記述T(check_DECLARE)６７ｂとにより構成される。
【０１６０】
ステップＳ３４においてチェック用テストベンチ記述T(check)６７を生成する前に、まず、チェック用タスク部テストベンチ記述T(check_TASK)６７ａを生成する。
【０１６１】
チェック用タスク部テストベンチ記述T(check_TASK)６７ａは、（イ） モジュールTの各プロパティ記述P(T-n)を変換して得るプロパティチェック用テストベンチ記述T(T-n)と、（ロ）上述した（イ）で得た全タスクを並列に実行するための、コンカレント処理用テストベンチ用記述T(T-all)の２つとから構成される。
【０１６２】
そこで、チェック用タスク部テストベンチ記述T(check_TASK)６７ａを生成するために、プロパティチェック用テストベンチ記述T(T-n)を生成する。
【０１６３】
テストベンチ記述におけるDUT(被検証回路)信号の出力値と期待値の比較チェックは、条件文以外において“==”で実現され、これにより左辺と右辺を比較し、一致しない場合は、エラーをレポートして、シミュレーションを終了する。
【０１６４】
プロパティチェック用テストベンチ記述T(T-n)は、各プロパティ記述P(T-n)に図２８のステップＳ５３０〜Ｓ５４１の処理からなる処理Ｃを施して得る。
【０１６５】
[処理C]
上述した処理Ｃを本発明の実施の形態に係るプロパティ記述P(T-n)に対応してプロパティ記述P(ALU-2)に適用し、テストベンチ記述T(ALU-2)を得る場合について以下に示す。
【０１６６】
（イ）図２８のステップＳ５３０において、プロパティ記述P(T-n)に処理Ｃを実行する。まず、ステップＳ５３１において、.nを用いた時相に関する変換する。テストベンチ記述では、過去のDUT(被検証回路)の信号値をサンプル可能であるが、未来の値はサンプル不能である。よって、最も未来の時相へ基準(現在の時刻)をシフトする必要がある。まず、図２４（ａ）に示すP(ALU-2)で、C3が基準となるため、ステップＳ５３１の処理を行うと図２７（ａ）に示すような混在記述PT(ALU-2）#1を得る。ここで、「signal.n」でｎサイクル前のsignal（信号）の値を表す。
【０１６７】
（ロ）次に、ステップＳ５３２において、＠を用いた時相に関する変換を行う。テストベンチ記述における「signal.n」は、nサイクル前からの値を保持する必要があるため、nが大きいほどメモリ消費量が大きい。そこでnサイクル時間を進める記述「＠n」を用いて変換する。このとき、図２７（ａ）中の「AOUT==A.1   B.1」では、左辺と右辺の時間が異なるので、変数AOUTexpを宣言し、これを用いて記述を分割する。しかし、「OUT=￣IN.1」のような場合、
pre_IN=￣IN
@1 OUT=pre_IN
としてもメモリ消費量は変わらないので、このような場合は変換しないこととする。
【０１６８】
図２７（ａ）に示す混在記述PT(ALU-2)#1にステップＳ５３２の処理を行い、図２７（ｂ）に示す混在記述PT(ALU-2）#2を得る。即ち、図２７（ａ）に示す混在記述PT(ALU-2)#1では、「OP.1==3'b000==AOUT==A.11B.1;」にステップＳ５３２の処理を施すと、図２７（ｂ）に示す混在記載PT(ALU-2)#2に示すように、まず、期待値の生成及びその変数への格納を行うべく「@1 OP==3'b000==AOUTexp==AAB;」と変換する。次に、実測値と期待値とを比較すべく「@1 AOUT==AOUTexp」と変換する。以上のステップＳ５３１及びＳ５３２の処理をオペレータ情報OPの全ての場合について適用し、次のステップＳ５３３及びＳ５３４ではオペレータ情報OPの全ての場合について変換する。
【０１６９】
（ハ）ステップＳ５３３において、条件文の変換を行う。まず、プロパティ記述における「==(imply記述)」の左辺は条件を表すためテストベンチ記述のif文に変換する。さらに、外部入力信号OP（オペレータ情報）の全ての場合について、時相およびレジスタが同一であるため、これらは同時に成立せず、if/else_if文あるいは、case文で結合できる。図２７（ｂ）に示す混在記述PT(ALU-2)#2にステップＳ５３３の処理を施すと図２９（ａ）に示すタスク部テストベンチ記述T(ALU-2）を得ることができる。
【０１７０】
（ニ）次に、ステップＳ５３４において、whileループ及びタスクブロック化する記述の追加を行う。まず、ループ文を付加し、シミュレーションの終了はドライブ用テストベンチ記述T(drive)６１で制御されているため、ここでは無限ループにするための「while(1)」を用い、ドライブ側で実行される強制終了でループ処理を終了することにする。更に、変数宣言、タスクブロック化する記述を追加すると、ステップＳ５３５において、プロパティチェック用テストベンチ記述T(T-n)を取得する。
【０１７１】
図２９（ａ）に示すチェック用タスク部テストベンチ記述T(ALU-2)にステップＳ５３４の処理を施すと図２９（ｂ）に示すチェック用タスク部テストベンチ記述T(ALU-2)を得ることができる。同様に、図２４（ａ）に示すプロパティ記述P(ALU-1)に以上の処理（ステップＳ５３１〜Ｓ５３４）を適用すると、ステップＳ５３５において、図２９（ｃ）に示すチェック用タスク部テストベンチ記述T(ALU-1)を得ることができる。同様に、図２４（ａ）に示すプロパティ記述P(ALU-3)に以上の処理（ステップＳ５３１〜Ｓ５３４）を適用すると、ステップＳ５３５において、図３０（ａ）に示すチェック用タスク部テストベンチ記述T(ALU-3)を得ることができる。
【０１７２】
（ホ）ここで、ステップＳ５３６において、Ｓ５３０〜Ｓ５３４で求めたドライブ用テストベンチ記述T(drive)６１（図２６（ａ）及び（ｂ））における@nのnを求める。nは各チェック用テストベンチ記述T(check)の比較“==”が行われる時刻が、ドライブ用テストベンチ記述T(drive)における時刻において最も遅いものについて、その時刻とドライブ用テストベンチ記述T(drive)におけるn=0の場合の最後の時刻との差である。
【０１７３】
たとえば、実施例２−１において、ドライブ用テストベンチ記述T(drive)６１における時間(時刻)を図３０（ｂ）に示すタスク部テストベンチ記述Ｔ（drive_TASK）６１ａの右側の列に示すように(T=n)と記述する。このとき、図２９（ｃ）に示すチェック用タスク部テストベンチ記述T(ALU-1)では、ASEL==2’b00ならT=4、ASEL==2’b01ならT=5、ASEL==2’b10ならT=6、T(ALU-2)ではT=7、T(ALU-3)ではT=3となり、T=7が最も遅いため、n=7-5=2となる。
【０１７４】
（ヘ）次に、ステップＳ５３７〜Ｓ５３９の処理において、コンカレント処理用テストベンチ記述T(T-all)を生成する。コンカレント処理用テストベンチ記述T(T-all)には、ステップＳ５３７〜Ｓ５３９の処理が施され３つの事項が記述される。まず、ステップＳ５３７において、タスクT(T-n)が属するクラスをインスタンス化を記述する。次に、ステップＳ５３８において、並列実行するタスク名を列挙した「fork/join」文を記述する。そして、ステップＳ５３９において、タスクブロック化(タスク名：check_all)する記述を追加する。以上のステップ
Ｓ５３７〜Ｓ５３９は、各プロパティチェック用テストベンチ記述T(T-n)を生成する際のステップＳ５３４から得られる。
【０１７５】
（ト）以上のステップＳ５３７〜Ｓ５３９の処理を実施例２−１に適用すると、ステップＳ５４０において、図３０（ｃ）に示すテストベンチ記述T(ALU-all)が生成される。従って、上述したステップＳ５３０〜Ｓ５４０の処理を実行することにより、ステップＳ５４１において、T(ALU-1)、T(ALU-2)、T(ALU-3)、T(ALU-all)から構成されたチェック用タスク部テストベンチ記述T(check_TASK)６１ａを生成することができる。
【０１７６】
（チ）次に、チェック用クラス宣言部テストベンチ記述T(check_DECLARE)６１ｂを生成する。チェック用のクラス宣言部では、タスク部においてランダム変数を使用しないため、タスク宣言のみを記述する。これらは各プロパティチェック用テストベンチ記述T(T-n)を生成する際のステップＳ５３４およびコンカレント処理用のタスク名check_allから得られる。
【０１７７】
上述したように、ステップＳ５３０〜Ｓ５４０までの処理を実施例２−１に適用すると、ステップＳ５４１において、図３０（ｄ）に示すチェック用クラス宣言部テストベンチ記述T(check_DECLARE)６１ｂを生成することができる。
【０１７８】
［処理手順５］
次に、図３１のステップＳ５４２〜Ｓ５４６までの処理において、ドライブ用テストベンチ記述T(drive)６１、チェック用テストベンチ記述T(check)６７をコンカレントに実行し、これらの上位に位置するTOP用テストベンチ記述T(TOP)６８を生成する。
【０１７９】
（イ）まず、図３１のステップＳ５４２において、TOP用メイン部テストベンチ記述T(check_DECLARE)６７ｂを取得する。次に、ステップＳ５４３において、T(drive)及びT(check)が属するクラスのインスタンス化を記述する。次に、ステップＳ５４４において、「fork/join」記述で並行に実行するタスク名を列挙する。次に、ステップＳ５４５において、メインブロック化する記述「mainnメインブロック名名{{処理本体体}」を追加する。そして、ステップＳ５４２〜Ｓ５４５までの処理により、ステップＳ５４６において、上位テストベンチ記述T(TOP)を生成する。これらは実施例２−１に依存せず、図３２（ａ）に示すTOP用メイン部テストベンチ記述T(check_DECLARE)６７ｂを用いる。また、実施例２−１においてもこれを用いる。以上で得られた上位テストベンチ記述T(TOP)６８と検証対象モジュールM(T)６３とのインタフェースとなるシミュレーション用の上位モデル記述M(TEST)６４を生成する。
【０１８０】
（ロ）次に、ステップＳ５４７〜Ｓ５５１までの処理において、シミュレーション用のシミュレーション用上位モデル記述M(TEST)６４を生成する。まず、ステップＳ５４７において、検証対象モジュールTのモデル記述M(T)６３を取得する。次に、ステップＳ５４８において、宣言部として、モジュール宣言、および検証対象モジュールにおいてinputおよびoutput宣言されている信号をwire宣言し、さらにクロック生成用に上位クロックTEST_CLKをreg宣言を記述する。
【０１８１】
（ハ）次に、ステップＳ５４９において、インスタンス部として、検証対象モジュールのモデル記述M(T)６３のインスタンスを記述する。更に、ステップＳ５５０において、クロック生成部として、上位クロック生成、上位クロック生成の検証対象モジュールのクロックへの割り当て、上位クロックの初期値を記述する。そして、ステップＳ５５１において、シミュレーション用上位モデル記述M(TEST)を生成する。実施例において、検証対象モジュールALUのモデル記述M(ALU)から得られたシミュレーション用上位モデル記述M(TEST)６４を図３２（ｂ）に示す。
【０１８２】
（ニ）最後に、ステップＳ５５２において、上位テストベンチ記述T(TOP)６８、ドライブ用テストベンチ記述T(drive）６１、チェック用テストベンチ記述T(check)６７及びシミュレーション用上位モデル記述M(TEST)６４からなる統合シミュレーション環境８０を得る。
【０１８３】
［処理手順６］
次に、図３３に示すステップｓ５５４において、ランダムシード値SEEDを用いて、図３１のステップｓ５５２で得られた統合シミュレーション環境８０において、検証対象モジュールのモデル記述M(T)６３を対象とした論理シミュレーションおよびカバレッジ計測を実行する。これは、テストベンチ用ツール、シミュレーションツール、コードカバレッジツールを同時に使用するものである。この際、ステップＳ５５５において、NUM値およびランダムシード値SEEDはレポートされるようにしておく。尚、ランダムシード値SEEDは、生成されるランダム値の集合の基になる値で、この値を変えることによって生成されるランダム値の集合を変えることができる。そして、実施例２−１において、ランダムシード値SEEDをデフォルト設定値のままで、ステップＳ５５５で得られた統合シミュレーション環境８０において、モデル記述M(ALU)を対象とした論理シミュレーションおよびカバレッジ計測を実行する。
【０１８４】
［処理手順７］
次に、図３３のステップＳ５５６において、モデル記述の修正が行われる。ステップＳ５５７において、エラーの有無が確認され、エラーレポート６５がレポートされる場合は、図１７のステップＳ３１に対応する図２０のステップＳ５０１〜Ｓ５０４までの処理に戻り、エラーがレポートされなくなるまで、使用者がモデル記述を修正する。
【０１８５】
ステップＳ５５７において、検索対象モジュールＡＬＵのモデル記述M(ALU)に関するシミュレーションで、エラーがレポートされなくなるまでM(ALU)の修正が済むと、処理手順８に対応したステップＳ５５８の処理へ進む。
【０１８６】
［処理手順８］  図３３のステップＳ５５８において、コードカバレッジのレポートから非活性化コードが無いかどうか判断し、図３５のステップＳ５６０〜Ｓ５７８までの処理に対応する処理手順９の処理へ進む。
【０１８７】
そこで、たとえば、本発明の第２の実施形態に係る実施例２−１において、以下の2つ（非活性化コード１と非活性化コード２）が非活性化コードとしてレポートされたと仮定する。
【０１８８】
(1)  非活性化コード1として、検証対象モジュールALU下のモジュールSELECTORのcaseブロックにおいて、sel==default値で、非活性化がレポートされたとする。図３４（ａ）に非活性化コードレポートR(UA1)を示す。
【０１８９】
(2)  非活性化コード2として、検証対象モジュールALU下のモジュールalu8のcaseブロックにおいて、op==default値について、非活性化がレポートされたとする。図３４（ｂ）に非活性化コードレポートR(UA2)を示す。
【０１９０】
［処理手順９］
図３３のステップＳ５５８に対応する処理手順８において、非活性化コードがある場合、処理手順２で得たプロパティ記述P(I--T)７４から仕様的に活性化されることがないかどうか、処理手順９として図３５のステップＳ５６０〜Ｓ５７８において判定する。そこで、検証対象モジュールのモデル記述M(T)６３で検出された非活性化コードについて、図Ｓ５６０〜Ｓ５７８までの処理Ｄにより仕様上活性化され得るかどうかを判定する。
【０１９１】
[処理D]  
（イ）まず、ステップＳ５６０において、処理Ｄの実行を開始する。まず、ステップＳ５６１において、検証対象モジュールのモデル記述M(T)６３で検出された非活性化コードの信号をS(T)とし、その値をVALとする。次に、ステップＳ５６２において、VALがcase文の「default」あるいはif文の「else」であるかを判断し、ステップＳ５６３において「default」あるいは「else」に相当する値を
求める。次に、ステップＳ５６４において、信号S(T)をモデル記述M(T)６３内でトレースし、ステップＳ５６５において、信号S(T)のモデル記述M(I)６０における信号名S(I)を求め、これをSIGとする。そして、ステップＳ５６６において、検索対象をSIGが記述されたプロパティ記述P(I)６２とする。
【０１９２】
（ロ）次に、ステップＳ５６７において、 条件文以外で左辺に記述された信号名SIGを検索する。ステップＳ５６８において、検索された記述について、右辺において固定値を与えているか否かを判断し、右辺において固定値を与えている場合は、ステップＳ５６９において、その固定値を記憶しステップＳ５７０の処理へ進む。ステップＳ５６８の判断において、右辺でREG変数（レジスタ変数）を与えている場合は、ステップＳ５７１の処理へ進む。
【０１９３】
（ハ）次に、ステップＳ５７０において、プロパティ記述の途中であるか否かを判断する。プロパティ記述の途中の場合はステップＳ５６７の処理へ戻り、続きの行から検索を行う。ステップＳ５７０において、プロパティ記述の終端の場合はステップＳ５７６の処理へ進む。
【０１９４】
（ニ）ステップＳ５７１において、検索対象のSIGをモデル記述M(I)内でトレースする。次に、ステップＳ５７２において、信号のとり得る値が特定できてトレースできるか否かを判断し、できる場合はステップＳ５７３においてその制約を記憶する。ステップＳ５７４において、その信号が主入力信号であるか否かを判断する。その信号が主入力信号である場合は、処理９を終了し、主入力でない場合は、ステップＳ５７５において、新たにSIG、検索対象を他のP(I)６２としてステップＳ５７０の処理へ戻る。尚、ステップＳ５７４において、信号のとり得る値が特定できない場合、「判定不能」として処理を終了する。
【０１９５】
（ホ）値VALがステップＳ５６９で得た固定値やステップＳ５７３で得た値の制約範囲に含まれているか否かをステップＳ５７６において判断する。含まれている場合、ステップＳ５７８において、「活性化され得る」と判定し処理を終了する。含まれていない場合ステップＳ５７７において、「活性化され得ない」と判定し処理を終了する。
【０１９６】
以上のステップＳ５６０〜Ｓ５７８までの処理を実施例２−１の非活性化コード1および非活性化コード2に適用した場合を以下に示す。
【０１９７】
まずはじめに、ステップＳ５６０において非活性化コード1の判定に処理Ｄの実行を開始する。そして、上述したステップＳ５６１〜Ｓ５６３の処理により、記述R(UA-1)からS(T)=sel、VAL=2’b11となる。ステップＳ５６４において、セレクタ信号（sel）をM(ALU)内でトレースし、sel(モジュール:SELECTOR（セレクタ）)--ASEL(モジュール:ALU)とする。更に、ステップＳ５６５において、図２０のステップＳ５０４で求めたC(ALU)よりS(I)=CSELとなり、SIG=CSELとする。
【０１９８】
そして、ステップＳ５６６において、検索対象をプロパティ記述P(CON-2)とする。
【０１９９】
次に、ステップＳ５６７〜Ｓ５７０において、「2’b00」、「2’b01」、「2’b10」の固定値を記憶しステップＳ５７６の処理へ進む。ステップＳ５７６において、値VALの「2’b11」は「2’b00」、「2’b01」、「2’b10」の制約外であるため「仕様上活性化され得ない」と判定し処理を終了する。
【０２００】
次に、ステップＳ５６０において非活性化コード２の判定に処理Ｄの実行を開始した場合について検討する。上述したステップＳ５６１〜Ｓ５６３の処理において、記述R(UA-2)からS(T)=op、VAL=3'b101、3'b110、3'b111となる。ステップＳ５６４において、sel信号をM(ALU)内でトレースし、op(モジュール:alu8)--OPOUT (モジュール:ALU)--opout=ain[2:0](モジュール:OPREG)--AIN(モジュール:ALU)となる。更に、ステップＳ５６５において、図２０のステップＳ５０４で求めたC(ALU)より、S(I)=COUTとなり、SIG=COUTとする。そして、ステップＳ５６６において、検索対象をプロパティ記述P(CON-2)とする。
【０２０１】
次に、ステップＳ５６７〜Ｓ５６８、ステップＳ５７１〜Ｓ５７５の処理を実行し、COUT=OP(REG変数)より、プロパティ記述P(CON-1)を検索する。そして、ステップＳ５７１において、信号をOP=CIN[18:16](モジュール:CON)をトレースする。ステップＳ５７２において、入力信号Ｃ（CIN）は主入力で、かつとり得る値が3ビット(3’b000から3’b111)であることが特定する。最後にステップＳ５７６において、値VALの「3'b101」、「3'b110」、「3'b111」は「3’b000」から「3’b111」に含まれるのでステップＳ５７８において「仕様上活性され得る」として判定し、処理を終了する。
【０２０２】
［処理手順１０］
ステップＳ５７７において、「仕様上活性化され得ない」と判定された場合、ステップＳ５８１において、その非活性化コードを削除し、ステップＳ５８２において削除された非活性コードの行番号をレポート後、図２０のステップＳ５０１の処理へ戻る。例えば、実施例２−１の非活性化コード1について、モデル記述M(ALU-1)のdefault文は、仕様上活性化され得ないことが確認されたので、モデル記述M(ALU-1)からdefault文をコメントアウト“//”で無効化し、そのファイルにおける削除行番号をステップＳ５８２においてレポートし、図２０のステップＳ５０１の処理へ戻る。図３７に修正版モデル記述M(ALU-1)を示す。
【０２０３】
［処理手順１１］
ステップＳ５７８において、「活性化され得る」と判断された場合、ステップＳ５８５において、そのコードを活性化させるランダム値生成制約用テストベンチ記述T(drive-cst)を生成し、図３３のステップＳ５５４の処理に戻り、これをドライブ用テストベンチ記述T(drive)６１にインクルードして、再度シミュレーションを実行する。
【０２０４】
例えば、実施例２−１において、非活性化コード2について、モデル記述M(ALU-2)のdefault文は、仕様上活性化され得ることが確認され、トレース結果より「3’b0000=OPP=3’b111」であるので、モデル記述M(ALU-2)のdefault文を活性化させるテストベクタを生成させるための制約用テストベンチ記述を生成する。また、テストベンチ記述T(drive)６１において、「AIN={5’b00000,rand.OP}」より、ランダム生成されるOP値に対して、「OPP=3'b101」かつ「OPP=3'b111」というランダム生成制約を加えて、図３８に示すランダム制約用テストベンチ記述T(cst1)７１ａを得る。更に、 実施例２−１において、生成制約用テストベンチ記述T(cst1)７１ａをドライブ用テストベンチ記述T(drive)６１にインクルードして、再度シミュレーションを実行する。
【０２０５】
［処理手順１２］
ステップＳ５７６において、活性化され得るか、され得ないか判定不能な場合、ステップＳ５８８において前回の非活性化コードで活性化されたコードがないか判断する。 活性化されたコードがない場合は処理を終了する。活性化されたコードがある場合は、ステップＳ５８９において、前回のシミュレーション時のNUM値を「prenum」とするとき、これより大きい値が生成されるようランダム生成制約７１を生成する。更に、ステップＳ５９０において、ランダムシード値SEEDを変更するオプションを付加し、異なるランダム値の集合を生成するよう指定してシミュレーションを実行し、終了する。これら2つの値を変えることによって、異なるランダム値の集合を生成することができ、非活性化コードを活性化させる可能性を上げることができる。
【０２０６】
例えば、実施例２−１において、「prenum=5」であったとすると、図３９に示すランダム制約用テストベンチ記述T(cst2)７１ｂを得る。実施例２−１において、生成制約用テストベンチ記述T(cst2)７１ｂをドライブ用テストベンチ記述T(drive)６１にインクルードし、かつランダムSEED値を変更するオプションを付加し、ステップＳ３６により再度シミュレーションを実行する。
【０２０７】
［処理手順１３］
図３３のステップＳ５５８において、コードカバレッジ計測がレポートする非活性化コードが無くなった場合、あるいは、ステップＳ５５８において、前シミュレーション時にレポートされた非活性化コードについて、活性化が全くなかった場合、本手法の処理を終了する。たとえば実施例２−１において、非活性化コード１は削除され、非活性化コード２について2回目のシミュレーションで解消され、本処理を終了する。
【０２０８】
（第２の実施の形態の効果）
本発明の第２の実施の形態によれば、検証対象モジュールへ入力を与え、かつ仕様誤りおよび仕様抜けが無いことが確認済みのモジュールのプロパティ記述から信頼性のあるドライブ用テストベンチ記述作成を自動生成することによって、テストベンチ記述に関わる時間を短縮することを可能とし、かつ仕様内の有効なテストベクタのみ生成させることによってシミュレーション時間を短縮することを可能とする。
【０２０９】
更に、本発明の第２の実施の形態によれば、検証対象モジュールのプロパティ記述から、チェック用テストベンチ記述を自動生成することによって、テストベンチ記述作成に関わる時間を短縮することを可能とする。更に、本発明の第２の実施の形態によれば、ドライブ用テストベンチ記述およびチェック用テストベンチ記述を並行実行する上位階層のトップ用テストベンチ記述作成を自動生成することによって、テストベンチ記述作成に関わる時間を短縮することを可能とする。
【０２１０】
更に、本発明の第２の実施の形態によれば、非活性化コードについて、テストパタンの不足で活性化されないのか、仕様上活性され得ないかを自動で判定することで、前者の場合、その非活性化コードを誤って削除してしまうことを防止し、後者の際に無駄なシミュレーション時間を省くことを可能とする。更に、本発明の第２の実施の形態によれば、仕様上活性され得ないと判断した非活性化コードを削除することによって、面積削減することを可能とする。更に、本発明の第２の実施の形態によれば、仕様上活性され得ると判断した非活性化コードを活性化させるランダム値生成制約テストベンチ記述を自動生成し、これを読み込んでシミュレーションすることによって、非活性コードを活性化させ検証確度を上げることを可能とする。
【０２１１】
本発明によれば、外部モジュールのプロパティ情報（回路の動作仕様を専用の書式で表現したもの）から、検証対象モジュールに入力を与えるシミュレーション環境を自動生成し、また、検証対象モジュールのプロパティ情報から、検証対象モジュールの出力を期待値と比較するシミュレーション環境を自動生成し、これらを統合したシミュレーション環境を生成することにより、シミュレーション時間を短縮化したＬＳＩ設計検証装置、ＬＳＩ設計検証方法、及びＬＳＩ設計検証プログラムを提供することができる。
【０２１２】
（その他の実施の形態）
上記のように、本発明は第１乃至第３の実施の形態によって記載したが、この開示の一部をなす論述及び図面は、この発明を限定するものであると理解すべきではない。この開示から、当業者には様々な代替実施の形態、実施例、及び製造工程技術が明らかとなろう。
【０２１３】
本発明はここでは記載していない様々な実施の形態等を含むことは勿論である。従って、本発明の技術的な範囲は上記説明から妥当な特許請求の範囲に係る発明特定事項によってのみ定められるものである。
【図面の簡単な説明】
【０２１４】
【図１】本発明におけるＬＳＩ設計検証装置の構成図である。
【図２】本発明に係るＬＳＩ設計検証方法のフロー図である。
【図３】本発明の第１の実施形態に係る実験回路を示した回路図である。
【図４】本発明に係る共通データベース４を示した図である。
【図５】図５（ａ）は、本発明に係るMULT側のプロパティ情報の一例、図５（ｂ）は、ＣＯＮ側のプロパティ情報の一例を示す。
【図６】本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−１の処理手順１のフロー図（その１）である。
【図７】本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−１の処理手順１のフロー図（その２）である。
【図８】図８（ａ）は、本発明の第１の実施形態に係るMULTの信号リストを示したものであり、図８（ｂ）は、ＣＯＮの信号リストを示したものである。
【図９】本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−１の処理手順２のプロパティ検出・抽出に関するフロー図である。
【図１０】本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−１の処理手順３のフロー図である。
【図１１】図１１（ａ）は、ＣＯＮ側のプロパティを示したものであり、図１１（ｂ）はＣＯＮ側のプロパティを変換した一例を示したものである。
【図１２】本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−１の処理手順４及び５のフロー図である。
【図１３】本発明の第１の実施形態に係るＬＳＩ設計検証方法における波形表示の一例を示す。
【図１４】図１４（ａ）に本発明の第１の実施形態に係るＬＳＩ設計検証方法の実施例１−２で用いるMULTの単体検証用プロパティの一例、図１４（ｂ）にＣＯＮの単体検証用プロパティの一例を示す。
【図１５】本発明の第２の実施形態に係るＬＳＩ設計検証方法の概念図を示す。
【図１６】本発明におけるＬＳＩ設計検証装置の構成図である。
【図１７】本発明に係るＬＳＩ設計検証方法のフロー図である。
【図１８】本発明の第２の実施形態に係るＬＳＩ設計検証方法で用いる実験回路図を示す。
【図１９】本発明の第２の実施形態に係る実験回路ＡＬＵのモジュール構成を示す。
【図２０】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順１のフロー図である。
【図２１】本発明の第２の実施形態における実験回路のモジュール構造を示す
【図２２】図２２（ａ）に本発明の第２の実施形態に係るＣＯＮの入力接続関係、図２２（ｂ）にＡＬＵの入力接続関係を示す。
【図２３】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順２のフロー図である。
【図２４】図２４（ａ）に本発明の第２の実施形態に係るＡＬＵの単体検証用プロパティ、図２４（ｂ）にＣＯＮの単体検証用プロパティ、図２４（ｃ）にプロパティ記述P(CON--ALU)を示す。
【図２５】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順３のフロー図である。
【図２６】図２６（ａ）に本発明の第２の実施形態に係るドライブ用タスク部テストベンチ記述、図２６（ｂ）にクラス宣言部テストベンチ記述を示す。
【図２７】図２７（ａ）に本発明の第２の実施形態に係る混在記述例（その１）、図２７（ｂ）に混在記述例（その２）を示す。
【図２８】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順４のフロー図である。
【図２９】図２９（ａ）に本発明の第２の実施形態に係る回路ALU-2のタスク部テストベンチ記述（その１）、図２９（ｂ）にALU-2のタスク部テストベンチ記述（その２）、図２９（ｃ）にALU-1のタスク部テストベンチ記述を示す。
【図３０】図３０（ａ）に本発明の第２の実施形態に係る回路ALU-3のタスク部テストベンチ記述、図３０（ｂ）にタスク部テストベンチ記述T(drive_TASK)、図３０（ｃ）にタスク部テストベンチ記述T(ALU-all)、図３０（ｄ）にクラス宣言部テストベンチ記述T(check_DECLARE)を示す。
【図３１】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順５のフロー図である。
【図３２】図３２（ａ）にトップ用メイン部テストベンチ記述、図３２（ｂ）にシミュレーション用モデル記述を示す。
【図３３】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順６乃至８のフロー図である。
【図３４】図３４（ａ）は非活性化コードレポートR(UA1)、図３４（ｂ）は非活性化コードレポートR(UA2)を示す。
【図３５】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順９のフロー図である。
【図３６】本発明の第２の実施形態に係るＬＳＩ設計検証方法の実施例２−１の処理手順１０乃至１３のフロー図である。
【図３７】本発明の第２の実施形態に係る修正版モデル記述M(ALU-1)を示す。
【図３８】本発明の第２の実施形態に係るランダム制約用テストベンチ記述T(cst1)を示す。
【図３９】本発明の第２の実施形態に係るランダム制約用テストベンチ記述T(cst2)を示す。
【符号の説明】
【０２１５】
１  ＬＳＩ設計検証装置
２  中央演算処理装置（ＣＰＵ）
４  共通データベース
５  モジュール名データベース
９  共通データベース格納手段
１０  回路記述読込手段
１１  解析手段
１２  プロパティ読込手段
１３  モジュール間プロパティ抽出手段
１４  信号動作部分抽出手段
１５  比較手段
１６  不一致検出手段
１７  レポート生成手段
１８  冗長部削除手段
１９  レジスタ挿入手段
２０  波形表示手段
２１  プロパティ生成手段
２２  テストベンチ生成手段
２２ａ  ドライブ用テストベンチ生成手段
２２ｂ  チェック用テストベンチ生成手段
２２ｃ  トップ用テストベンチ生成手段
２２ｄ  ランダム値生成制約用テストベンチ生成手段
２３  上位モデル生成手段
２４  論理シミュレーション手段
２５  コードカバレッジ計測手段
２６  自動判定手段
２７  非活性コード削除手段
２８  レポート手段
３１  入力装置
３２  出力装置
３３  入出力制御装置
３５  主記憶装置
４０、４０ａ、４０ｂ   信号リスト
４１  ＲＴＬ回路記述（ＲＴＬファイル）
４２ａ  プロパティＡ
４２ｂ  プロパティＡ’
４３ａ  プロパティＢ
４３ｂ  プロパティＢ’
４５  トップ階層
４６  乗算器（ＭＵＬＴ）
４７  算術論理演算ユニット（ＡＬＵ）
４８  コントローラ（ＣＯＮ）
６０  モデルＩ
６１  ドライブ用テストベンチ
６２  プロパティＩ
６３  モデルＴ
６４  モデルＴＥＳＴ
６５  レポート
６６  プロパティＴ
６７  チェック用テストベンチ
６８  テストベンチ
６９  入力接続関係
７０  削除レポート
７１  ランダム値生成制約
７２  新SEED値
７３  新NUM値
７４  プロパティ記述P(I--T)    ７５  最上位モジュール（TOP）
７６  コントローラ（ＣＯＮ）
７７  算術論理演算ユニット（ＡＬＵ）
８０  統合シミュレーション環境
８１  セレクタ
８２  Ａレジスタ
８３  Ｂレジスタ
８４  ＯＰレジスタ
８５  ＡＬＵ
８６  Ｒレジスタ
【図１】
2006323856.tif 000003
【図２】
2006323856.tif 000004
【図３】
2006323856.tif 000005
【図４】
2006323856.tif 000006
【図５】
2006323856.tif 000007
【図６】
2006323856.tif 000008
【図７】
2006323856.tif 000009
【図８】
2006323856.tif 000010
【図９】
2006323856.tif 000011
【図１０】
2006323856.tif 000012
【図１１】
2006323856.tif 000013
【図１２】
2006323856.tif 000014
【図１３】
2006323856.tif 000015
【図１４】
2006323856.tif 000016
【図１５】
2006323856.tif 000017
【図１６】
2006323856.tif 000018
【図１７】
2006323856.tif 000019
【図１８】
2006323856.tif 000020
【図１９】
2006323856.tif 000021
【図２０】
2006323856.tif 000022
【図２１】
2006323856.tif 000023
【図２２】
2006323856.tif 000024
【図２３】
2006323856.tif 000025
【図２４】
2006323856.tif 000026
【図２５】
2006323856.tif 000027
【図２６】
2006323856.tif 000028
【図２７】
2006323856.tif 000029
【図２８】
2006323856.tif 000030
【図２９】
2006323856.tif 000031
【図３０】
2006323856.tif 000032
【図３１】
2006323856.tif 000033
【図３２】
2006323856.tif 000034
【図３３】
2006323856.tif 000035
【図３４】
2006323856.tif 000036
【図３５】
2006323856.tif 000037
【図３６】
2006323856.tif 000038
【図３７】
2006323856.tif 000039
【図３８】
2006323856.tif 000040
【図３９】
2006323856.tif 000041