(57)【特許請求の範囲】
【請求項１】
ゲートレベルのネットリストを用いた設計検証を行う設計検証プログラムにおいて、
コンピュータを、
作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する作成処理手段、
前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける関連づけ処理手段、
として機能させることを特徴とする設計検証プログラム。
【請求項２】
前記作成処理手段は、前記ＲＴＬ記述のモジュール名を変更し、前記ＲＴＬ記述のレジスタに関する記述を全て削除し、削除したレジスタが出力する信号の信号名を、前記ＲＴＬ回路外部からの入力信号の信号名とした前記モニタ記述を作成することを特徴とする請求項１記載の設計検証プログラム。
【請求項３】
前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述またはテストベンチ記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記入力信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする請求項２記載の設計検証プログラム。
【請求項４】
前記作成処理手段は、前記ＲＴＬ記述のモジュール名および入出力信号名の定義文を削除し、前記ＲＴＬ記述のレジスタに関する記述を全て削除し、前記ネットリストの内部信号または出力信号に対応する信号を出力する組み合わせ回路に関する記述を削除した前記モニタ記述を作成することを特徴とする請求項１記載の設計検証プログラム。
【請求項５】
前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述またはテストベンチ記述またはアサーションチェッカモデル記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記モニタの削除された前記レジスタが出力していた信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする請求項４記載の設計検証プログラム。
【請求項６】
ゲートレベルのネットリストを用いた設計検証を行う設計検証方法において、
作成処理手段が、作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成し、
関連づけ処理手段が、前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける、
ことを特徴とする設計検証方法。
【請求項７】
ゲートレベルのネットリストを用いた設計検証を行う設計検証装置において、
作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する作成処理部と、
前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける関連づけ処理部と、
を有することを特徴とする設計検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は設計検証プログラム、設計検証方法および設計検証装置に関し、特に、ゲートレベルのネットリスト記述を用いた設計検証プログラム、設計検証方法および設計検証装置に関する。
【背景技術】
【０００２】
ＬＳＩ（Large Scale Integration）の回路設計では、一般的にハードウェア記述言語（ＨＤＬ：Hardware Description Language）を用いて、論理回路を設計する技術が知られている（例えば、特許文献１、２参照）。
【０００３】
図３６は、設計検証フローを示すフローチャートである。
論理検証においては、まず、作成したＲＴＬ記述（Resister Transfer Level）のシミュレーションによる論理検証を行い回路の論理機能動作を確認する（ステップＳ９１）。
【０００４】
論理検証後、論理合成を行いゲートレベルのネットリスト（Netlist）記述を生成する（ステップＳ９２）。
ネットリスト記述とＲＴＬ記述のＦｏｒｍａｌ検証（論理等価検証）を行い、論理が等価であることを確認する（ステップＳ９３）。
【０００５】
論理等価の確認ができたら、レイアウトを行い、タイミング調整やテスト回路追加等を行った実配線のネットリスト記述および遅延情報ファイル（ＳＤＦ：Standard Delay Format）を生成する（ステップＳ９４）。
【０００６】
実配線のネットリスト記述および遅延情報ファイルを用いて、ゲートレベルのダイナミック・シミュレーションによる論理検証、タイミング検証を行い、回路の論理機能動作の確認およびタイミングスペックの確認を行う（ステップＳ９５）。
【特許文献１】特開２００５−２０２７０１号公報
【特許文献２】特開平９−３１１８８２号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
ＲＴＬ記述の検証の際には、ＰＳＬ（Property Specification Language）やＳＶＡ（SystemVerilog Assertion）等のアサーション言語のアサーションチェッカを用いて内部信号のアサーションチェック（プロパティチェック）を行っている。詳しくは、ある条件が成立していなければならない部分にアサーションチェッカを用いてチェック用のコードを入れ、その条件に違反している場合はエラーを出力することでプログラムをチェックしている。
【０００８】
ゲートレベルのダイナミック・シミュレーションによる論理検証においては、ＲＴＬ記述検証では発見できない非同期回路による誤動作やＳＴＡ（Static Timing Analyzer）でのタイミングケア漏れによる誤動作等を発見するための検証を行うが、現状のネットリスト検証ではＲＴＬ記述の検証で使用したアサーションチェッカをそのまま使うことができない。
【０００９】
これは論理合成後のネットリスト記述が、ＲＴＬ記述と論理が等価であっても異なる回路構成になってしまったり、ＲＴＬ記述とは異なる信号名に変わってしまったりするためである。
【００１０】
図３７は、ＲＴＬ記述により実現されるモジュール回路の一例を示す図である。
モジュール回路９０は、入力側からレジスタ（Ｄ−ＦＦ回路）Ｆ９１と、ＡＮＤ回路ＡＮＤ９１と、レジスタＦ９２と、ＡＮＤ回路ＡＮＤ９２と、ＡＮＤ回路ＡＮＤ９３とを有している。
【００１１】
レジスタＦ９１には信号名「ＤＩＮ」の信号が入力され、信号名「ＣＬＫ」の信号に同期して動作する。
ＡＮＤ回路ＡＮＤ９１の入力には、それぞれ信号名「ＸＭＳＫ」の信号およびレジスタＦ９１が出力する信号が入力される。
【００１２】
レジスタＦ９２には、ＡＮＤ回路ＡＮＤ９１が出力する信号名「ａ」の信号が入力され、信号名「ＣＬＫ」の信号に同期して動作する。
ＡＮＤ回路ＡＮＤ９２の入力には、信号名「ＸＭＳＫ」の信号およびレジスタＦ９２が出力する信号が入力される。
【００１３】
ＡＮＤ回路ＡＮＤ９３の入力には、信号名「ａ」の信号の論理を反転させた信号およびＡＮＤ回路ＡＮＤ９２が出力する信号名「ｂ」の信号が入力される。
ここで、アサーションチェッカ９１は、信号名「ＣＬＫ」の信号に同期して動作し、信号名「ａ」の信号および信号名「ｂ」の信号をチェックする。
【００１４】
図３８は、ネットリスト記述により実現されるネットリスト回路の一例を示す図である。
ネットリスト回路９０ａは、図３７に示すモジュール回路９０を実現するＲＴＬ記述を論理合成して得られたネットリスト記述により実現される回路である。
【００１５】
ネットリスト回路９０ａでは、ＡＮＤ回路ＡＮＤ９２の論理とＡＮＤ回路ＡＮＤ９３の論理とがまとめられてＡＮＤ回路ＡＮＤ９４になっており、信号名「ａ」の信号は、信号名「ｎ０」の信号に変わってしまっている。また、信号名「ｂ」の信号は、論理圧縮されて対応する信号が存在しなくなっている。このため、アサーションチェッカ９１は、対象となる信号が存在せず、チェックすることができない（動作しない）。
【００１６】
ここで、アサーションチェッカ９１をネットリスト回路９０ａ用に作り直すことも考えられるが、論理合成の度に異なる回路構成に変わる可能性があり、アサーションチェッカ９１の構成を一義的に定めることはできず、実現させるのは難しい。
【００１７】
このように、論理合成によって回路構成が変化した場合や、ＲＴＬ記述とは異なる信号名に変わってしまった場合、アサーションチェックを行うことができず、誤動作が発生したとき、どこの内部信号で誤動作が発生しているのかを解析するのに非常に時間がかかるという問題がある。
【００１８】
また誤動作が外部端子まで伝搬しない場合、誤動作を発見することができないという問題がある。
本発明はこのような点に鑑みてなされたものであり、ネットリスト検証でＲＴＬ記述と同等のアサーションチェックを可能とする設計検証プログラム、設計検証方法および設計検証装置を提供することを目的とする。
【課題を解決するための手段】
【００１９】
上記目的を達成するために、以下のような設計検証プログラムが提供される。この設計検証プログラムは、ゲートレベルのネットリスト記述を用いた設計検証を行うプログラムであり、コンピュータを、作成処理手段、関連づけ処理手段、として機能させる。
【００２０】
作成処理手段は、作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する。
関連づけ処理手段は、ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名をモニタ記述の入力信号の信号名に関連づける。
【００２１】
このような設計検証プログラムによれば、作成処理手段によりモニタ記述が作成され、関連づけ処理手段により、ネットリスト記述の入出力信号に対応するモニタ記述の入力信号が関連づけられる。従って、レジスタ・トランスファ・レベルで使用していた組み合わせ回路の内部信号名でアサーションチェックが可能となる。
【発明の効果】
【００２２】
開示の設計検証プログラム、設計検証方法および設計検証装置によれば、ネットリスト検証でＲＴＬ記述と同等のアサーションチェックが可能となるため、誤動作発生箇所を容易に発見することができる。
【発明を実施するための最良の形態】
【００２３】
以下、本発明の実施の形態を、図面を参照して詳細に説明する。
まず、本発明の概要について説明し、その後、実施の形態を説明する。
図１は、本発明の概要を示す図である。
【００２４】
設計検証プログラムは、ゲートレベルのネットリスト記述を用いた設計検証を行うプログラムであり、コンピュータ１を、作成処理手段２、関連づけ処理手段３、として機能させる。
【００２５】
作成処理手段２は、作成されたＲＴＬのＲＴＬ記述４からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する。
ここで、組み合わせ回路は、論理式に基づき、ＡＮＤ回路やＯＲ回路等のゲート素子を組み合わせたもので、入力の値だけで出力が定まり、過去の状態には影響されない回路である。また、レジスタは、組み合わせ回路と記憶回路で構成され、出力は入力と回路の現在の状態によって定まるものを言う。
【００２６】
関連づけ処理手段３は、ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名をモニタ記述の入力信号の信号名に関連づける。
【００２７】
詳しくは、モニタ記述に記述された入力信号の信号名に等しい、ネットリスト記述に記述された入力信号の信号名を互いに関連づける。また、モニタ記述を作成する際に、削除したレジスタが出力していた信号の信号名に等しい、ネットリスト記述に記述されたレジスタが出力する信号の信号名を互いに関連づける。
【００２８】
このような設計検証プログラムによれば、作成処理手段２によりモニタ記述が作成され、関連づけ処理手段３により、ネットリスト記述の入出力信号に対応するモニタ記述の入力信号が関連づけられる。従って、ＲＴＬで使用していた組み合わせ回路の内部信号名でアサーションチェックが可能となり、ＲＴＬと同等のアサーションチェックがネットリスト検証で可能になる。
【００２９】
以下、本発明の実施の形態を説明する。
図２は、設計検証装置のハードウェア構成例を示す図である。
設計検証装置１００は、ＣＰＵ（Central Processing Unit）１０１によって装置全体が制御されている。ＣＰＵ１０１には、バス１０７を介してＲＡＭ（Random Access Memory）１０２、ハードディスクドライブ（ＨＤＤ:Hard Disk Drive）１０３、グラフィック処理装置１０４、入力インタフェース１０５、および通信インタフェース１０６が接続されている。
【００３０】
ＲＡＭ１０２には、ＣＰＵ１０１に実行させるＯＳ（Operating System）のプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、ＲＡＭ１０２には、ＣＰＵ１０１による処理に必要な各種データが格納される。ＨＤＤ１０３には、ＯＳやアプリケーションプログラムが格納される。また、ＨＤＤ１０３内には、プログラムファイルが格納される。
【００３１】
グラフィック処理装置１０４には、モニタ１０４ａが接続されている。グラフィック処理装置１０４は、ＣＰＵ１０１からの命令に従って、画像をモニタ１０４ａの画面に表示させる。入力インタフェース１０５には、キーボード１２とマウス１３とが接続されている。入力インタフェース１０５は、キーボード１２やマウス１３から送られてくる信号を、バス１０７を介してＣＰＵ１０１に送信する。
【００３２】
通信インタフェース１０６は、ネットワーク１０に接続されている。通信インタフェース１０６は、ネットワーク１０を介して、他のコンピュータとの間でデータの送受信を行う。
【００３３】
以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。このようなハードウェア構成のシステムにおいて設計検証を行うために、設計検証装置１００内には、以下のような機能が設けられる。
【００３４】
図３は、設計検証装置の構成を示すブロック図である。
設計検証装置１００は、アサーションチェック部２００と、設計検証部３００と、ＲＴＬ記述格納部４００と、ネットリスト記述格納部５００と、実配線ＳＤＦ格納部６００と、モニタ記述格納部７００と、テストベンチ記述格納部８００と、ライブラリ格納部９００と、ＦＶ（Formal Verification）スクリプト格納部１０００とを有している。
【００３５】
ＬＳＩの回路設計ではユーザが、ハードウェア記述言語（ＨＤＬ）を用いて、ＲＴＬで回路の論理機能の記述を行う。
アサーションチェック部２００は、ある条件が成立していなければならない部分にチェック用のコードを入れ、その条件に違反している場合はエラーを出力することで、プログラムをチェックする。
【００３６】
設計検証部３００は、後述する設計検証処理を行うことによって、作成されたＲＴＬ記述の検証を行う。
ＲＴＬ記述格納部４００には、アサーションチェックが行われたＲＴＬ記述が格納される。
【００３７】
ネットリスト記述格納部５００には、ＲＴＬ記述の論理合成およびレイアウト処理により作成されたネットリスト記述が格納される。
実配線ＳＤＦ格納部６００には、レイアウト処理によって配設された実配線ＳＤＦが格納される。
【００３８】
モニタ記述格納部７００には、アサーションチェックを行うために作成されたモニタ記述が格納される。
テストベンチ記述格納部８００には、論理的に正常に動作するか否かを確認するための入力値と期待値の集合を備えるテストベンチ記述が格納される。
【００３９】
ライブラリ格納部９００には、ＲＴＬ記述とネットリスト記述を関連づけたライブラリが格納される。
ＦＶスクリプト格納部１０００には、ＲＴＬ記述からの変更内容が設定されたＦＶスクリプトが格納される。
【００４０】
図４は、設計検証部の機能を示すブロック図である。
設計検証部３００は、シミュレーション実行部３１０と、論理合成部３２０と、Ｆｏｒｍａｌ検証部３３０と、レイアウト実行部３４０と、モニタ記述作成部３５０と、関連づけ処理部３６０と、タイミング検証部３７０とを有している。
【００４１】
シミュレーション実行部３１０は、作成されたＲＴＬ記述のシミュレーションを行って回路の論理機能動作を確認する。
論理合成部３２０は、ＨＤＬで記述された論理機能を実際のゲート回路に変換してネットリスト記述を出力する。
【００４２】
Ｆｏｒｍａｌ検証部３３０は、出力されたネットリスト記述がＲＴＬ記述と等価であることを検証するＦｏｒｍａｌ検証を行う。
レイアウト実行部３４０は、論理等価の検証ができたネットリスト記述に対してレイアウトを行い、タイミング調整やテスト回路追加等を行った実配線のネットリスト記述および寄生容量、抵抗を含んだ遅延情報ファイル（ＳＤＦ）を作成する。
【００４３】
モニタ記述作成部３５０は、アサーションチェックを行ったＲＴＬ記述からレジスタを全て削除した組み合わせ回路のみのモニタ記述を作成する。
関連づけ処理部３６０は、モニタ記述作成部３５０が作成したモニタ記述の入力信号と、ネットリスト記述の入力信号およびネットリスト記述内部のレジスタが出力する信号とを関連づける。
【００４４】
タイミング検証部３７０は、実配線のネットリスト記述および遅延情報ファイルに加え、モニタ記述を用いてゲートレベルのダイナミック・シミュレーションによる論理検証、ＳＴＡによるタイミング検証を行い、回路の論理機能動作の確認およびタイミングスペックの確認を行う。
【００４５】
次に、本実施の形態の設計検証方法について説明する。
＜第１の実施の形態の設計検証方法＞
図５は、第１の実施の形態の設計検証処理を示す処理フローである。
【００４６】
まず、シミュレーション実行部３１０が、作成され、ＲＴＬ記述格納部４００に格納されているＲＴＬ記述のシミュレーションによる論理検証を行い、回路の論理機能動作を確認する（ステップＳ１）。
【００４７】
論理機能動作が期待通りでなかった場合（ステップＳ１のＮｏ）、処理を終了する。
論理検証動作が期待通りであった場合（ステップＳ１のＹｅｓ）、論理合成部３２０が、論理合成を行いゲートレベルのネットリスト記述を生成する（ステップＳ２）。生成したネットリスト記述はネットリスト記述格納部５００に格納する。
【００４８】
次に、Ｆｏｒｍａｌ検証部３３０が、ネットリスト記述とＲＴＬ記述のＦｏｒｍａｌ検証を行い、論理が等価であることを確認する（ステップＳ３）。
論理が等価でない場合（ステップＳ３のＮｏ）、処理を終了する。
【００４９】
論理が等価である場合（ステップＳ３のＹｅｓ）、レイアウト実行部３４０が、レイアウトを行い、実配線のネットリスト記述および遅延情報ファイルを生成する（ステップＳ４）。生成したネットリスト記述はネットリスト記述格納部５００に格納し、生成した遅延情報ファイルは、実配線ＳＤＦ格納部６００に格納する。
【００５０】
一方、モニタ記述作成部３５０は、ＲＴＬ記述格納部４００からＲＴＬ記述を取り出し、モジュール回路（組み合わせ回路）のモニタ記述を作成するモニタ記述作成処理を行う（ステップＳ５）。この処理については後に詳述する。
【００５１】
そして、作成されたモジュール回路のモニタ記述をモニタ記述格納部７００に格納する。
また、関連づけ処理部３６０は、モニタ記述の信号をネットリスト記述格納部５００に格納されているネットリスト記述の信号またはテストベンチ記述格納部８００に格納されているテストベンチ記述の信号に関連づけてこれらの信号同士を互いに関連づける関連づけ処理を行う（ステップＳ６）。この処理についても後に詳述する。
【００５２】
タイミング検証部３７０は、実配線のネットリスト記述および遅延情報ファイルに加え、モニタ記述を用いてゲートレベルのダイナミック・シミュレーションによる論理検証、タイミング検証を行う（ステップＳ７）。
【００５３】
論理機能動作が期待通りでなかった場合（ステップＳ７の動作Ｎｏ）、処理を終了する。
タイミングスペックが満たされなかった場合（ステップＳ７のタイミングＮｏ）、ステップＳ４に移行し、再度レイアウトを行う。
【００５４】
論理機能動作が期待通りであり、かつ、タイミングスペックを満たした場合（ステップＳ７のＹｅｓ）、タイミング検証部３７０が、実配線のネットリスト記述および遅延情報ファイルを用いて、ＳＴＡによるタイミング検証およびタイミングスペックの確認を行う（ステップＳ８）。
【００５５】
論理的に問題がある場合（ステップＳ８の動作Ｎｏ）、処理を終了する。
タイミングスペックが満たされなかった場合（ステップＳ８のタイミングＮｏ）、ステップＳ４に移行し、再度レイアウトを行う。
【００５６】
論理的に問題がなく、かつ、タイミングスペックを満たした場合（ステップＳ８のＹｅｓ）、処理フローを終了する。
なお、論理機能動作が期待通りでなかった場合（ステップＳ１のＮｏ）、論理が等価でない場合（ステップＳ３のＮｏ）、論理機能動作が期待通りでなかった場合（ステップＳ７の動作Ｎｏ）、および論理的に問題がある場合（ステップＳ８の動作Ｎｏ）は、ユーザによって再度ＲＴＬ記述が作成（再調整）され、第１の設計検証処理が再度繰り返される。
【００５７】
このようにして論理検証およびタイミング検証を行った後に、試作品のチップを作成し、実機評価での動作確認を行う。
実機動作が期待通りでなかった場合、回路の論理に問題がある場合は再度ＲＴＬ記述を作成し、タイミングに問題がある場合は再度レイアウトを行う。
【００５８】
実機評価の確認ができたら、回路の量産に入り、ＬＳＩの回路設計は完了する。
＜第１のモニタ記述作成処理＞
次に、図５に示すステップＳ５のモニタ記述作成処理（第１のモニタ記述作成処理）について詳しく説明する。
【００５９】
図６は、第１のモニタ記述作成処理を示すフローチャートである。
まず、モニタ記述作成部３５０が、ＲＴＬ記述格納部４００に格納されているＲＴＬ記述を取り出し、ＲＴＬ記述のモジュール回路名を別の名前に変更する（ステップＳ１１）。
【００６０】
次に、モニタ記述作成部３５０が、別の名前に変更したＲＴＬ記述からレジスタ記述に関する部位を全て削除する（ステップＳ１２）。
次に、モニタ記述作成部３５０が、削除したモニタ記述に含まれる信号の信号名を、モニタ記述の外部から入力される信号の信号名として追加する（ステップＳ１３）。
【００６１】
以上で、第１のモニタ記述作成処理を終了する。
次に、第１のモニタ記述作成処理の具体例を説明する。
図７は、ＲＴＬ記述格納部に格納されているＲＴＬ記述の一例を示す図であり、図８は、図７に示すＲＴＬ記述により実現されるモジュール回路を示す図である。
【００６２】
図８に示すモジュール回路１１は、図７に示すＲＴＬ記述ｒ１により実現される回路である。
モジュール回路１１のモジュール回路名は、「dut」であり、入力側からレジスタ（Ｄ−ＦＦ）Ｆ０＿ｒｅｇと、ＡＮＤ回路ａｎｄ２と、レジスタＦ１＿ｒｅｇと、ＡＮＤ回路ａｎｄ３と、ＡＮＤ回路ａｎｄ４とを有している。
【００６３】
レジスタＦ０＿ｒｅｇには信号名「ＤＩＮ」の信号が入力され、信号名「ＣＬＫ」の信号に同期して動作する。
ＡＮＤ回路ａｎｄ２には、モジュール回路１１外部から入力される信号名「ＸＭＳＫ」の信号およびレジスタＦ０＿ｒｅｇが出力する信号名「ｆ０」の信号が入力される。
【００６４】
レジスタＦ１＿ｒｅｇの入力には、ＡＮＤ回路ａｎｄ２が出力する信号名「ａ」の信号が入力され、信号名「ＣＬＫ」の信号に同期して動作する。
ＡＮＤ回路ａｎｄ３の入力には、信号名「ＸＭＳＫ」の信号およびレジスタＦ１＿ｒｅｇが出力する信号名「ｆ１」の信号が入力される。
【００６５】
ＡＮＤ回路ａｎｄ４の入力には、信号名「ａ」の信号の論理を反転させた信号およびＡＮＤ回路ＡＮＤ２が出力する信号名「ｂ」の信号が入力される。
アサーションチェック部２００は、信号名「ＣＬＫ」の信号に同期して動作し、信号名「ａ」の信号および信号名「ｂ」の信号をチェックする。
【００６６】
以下、この回路を用いて第１のモニタ記述作成処理の具体例を説明する。
図９は、図７に示すＲＴＬ記述に第１のモニタ記述作成処理を施したモニタ記述を示す図である。
【００６７】
まず、図７に示すＲＴＬ記述ｒ１のモジュール回路名「dut」を、図９に示すモニタ記述の別の名前「check＿dut」に書き替える。
また、ＲＴＬ記述のレジスタに関する記述、すなわち、７行目の「reg f0,f1;」、および１７〜２０行目の「always @(posedge CLK) begin・・・end」を削除する。なお、図９ではコメントアウトしている。
【００６８】
そして、１行目のｍｏｄｕｌｅ文に「f0,f1」を追加し、４行目（ｉｎｐｕｔ定義箇所）に「input f0,f1」を追加する。これにより第１のモニタ記述作成処理によって作成されたモニタ記述ｍ１が得られる。
【００６９】
図１０は、第１のモニタ記述作成処理によって作成されたモジュール回路を示す図である。
図１０中、点線で示したデバイスは、削除されたデバイスを示している。
【００７０】
モジュール回路１１ａは、モニタ記述ｍ１により実現される回路であり、モジュール回路１１のモジュール回路名「dut」が、「check＿dut」に変更されている。
また、レジスタＦ０＿ｒｅｇおよびレジスタＦ１＿ｒｅｇが削除されている。
【００７１】
そして、ＡＮＤ回路ａｎｄ２に入力される信号名「ｆ０」の信号の入力元が、レジスタＦ０＿ｒｅｇからモジュール回路１１ａの外部に変わっている。また、ＡＮＤ回路ａｎｄ３に入力される信号名「ｆ１」の信号の入力元が、レジスタＦ１＿ｒｅｇからモジュール回路１１ａの外部に変わっている。
【００７２】
＜第１の関連づけ処理＞
次に、図５に示すステップＳ６の関連づけ処理（第１の関連づけ処理）について説明する。
【００７３】
図１１は、第１の関連づけ処理を示すフローチャートである。
まず、関連づけ処理部３６０が、モニタ記述作成処理にて生成したモジュール回路のモニタ記述をネットリスト記述またはテストベンチ記述に追加する（ステップＳ２１）。このステップでは、モニタ記述の信号をネットリスト記述またはテストベンチ記述の信号に関連づける処理は行わない。
【００７４】
次に、関連づけ処理部３６０が、図６のステップＳ１３にて追加したモニタ記述の外部から入力される信号の信号名とネットリスト記述のレジスタが出力する信号の信号名とをネットリスト記述またはテストベンチ記述上で関連づける。
【００７５】
具体的には、ライブラリ格納部９００に格納されているライブラリを検索し、ＲＴＬ記述に記述されているレジスタと同等のレジスタがネットリスト記述に存在しているか否かを判断する（ステップＳ２２）。
【００７６】
同等のレジスタが存在している場合（ステップＳ２２のＹｅｓ）、そのレジスタが出力する信号の信号名を、ＲＴＬ記述に記述されているレジスタが出力する信号の信号名に関連づける（ステップＳ２３）。
【００７７】
一方、存在していない場合（ステップＳ２２のＮｏ）、削除されたレジスタの内容をＦＶスクリプト格納部１０００に格納されているＦＶスクリプトから検索し、代わりの信号名または固定値をＲＴＬ記述に記述されているレジスタが出力する信号の信号名に関連づける（ステップＳ２４）。このＦＶスクリプトを用いる処理は、モニタ記述の特殊関連づけ処理として後に詳述する。
【００７８】
次に、関連づけ処理部３６０が、モニタ記述に入力される信号の信号名にネットリスト記述に入力される信号の信号名をネットリスト記述上で関連づける。
具体的には、ＲＴＬ記述に入力される信号の信号名と同等の信号名がネットリスト記述に存在するか否かを判断する（ステップＳ２５）。
【００７９】
存在する場合（ステップＳ２５のＹｅｓ）、同等の信号名を関連づける（ステップＳ２６）。
一方、存在しない場合（ステップＳ２５のＮｏ）、変更された信号名をＦＶスクリプト格納部１０００に格納されているＦＶスクリプトから検索し、その信号名をＲＴＬ記述に入力される信号の信号名に関連づける（ステップＳ２７）。この処理についてもモニタ記述の特殊関連づけ処理として後に詳述する。
【００８０】
次に、関連づけ処理部３６０は、処理結果を格納先に格納する（ステップＳ２８）。具体的には、ステップＳ２１でモニタ記述をネットリスト記述に追加した場合、ステップＳ２２〜ステップＳ２７の処理が施されたネットリスト記述をネットリスト記述格納部５００に格納する。また、モニタ記述をテストベンチ記述に記載した場合、ステップＳ４２〜ステップＳ４７の処理が施されたテストベンチ記述をテストベンチ記述格納部８００に格納する。
【００８１】
以上で第１の関連づけ処理を終了する。
次に、第１の関連づけ処理の具体例を説明する。ステップＳ２８にて説明したように、モニタ記述をネットリスト記述に追加する方法とテストベンチ記述に追加する方法がある。以下順番に説明する。
【００８２】
＜第１の関連づけ処理の第１の具体例＞
本具体例は、図７に示すＲＴＬ記述ｒ１を論理合成したネットリスト記述に、図９に示すモニタ記述ｍ１を追加する例である。
【００８３】
図１２は、図７に示すＲＴＬ記述を論理合成したネットリスト記述を示す図であり、図１３は、第１の関連づけ処理を施したネットリスト記述を示す図である。
まず、第１のモニタ記述作成処理で作成したモニタ記述ｍ１を下記のようにインスタンス化して未接続で図１２に示すネットリスト記述ｎ１に追加する。
check＿dut inst＿check＿dut( .CLK(), .XMSK(),
.DIN(), .f0(), .f1(), .DOUT() );
次に、モニタ記述ｍ１における外部から入力される信号の信号名「ｆ０」、「ｆ１」にネットリスト記述ｎ１のレジスタが出力する信号の信号名を関連づける。
【００８４】
前述したように、ＲＴＬ記述ｒ１に記述されているレジスタと同等のレジスタがネットリスト記述ｎ１に存在するか否かを、ライブラリ格納部９００に格納されているライブラリから検索する。本具体例では、信号名「ｆ０」の信号を出力するレジスタｆ０＿ｒｅｇおよび信号名「ｑ１」の信号を出力するレジスタｆ１＿ｒｅｇがネットリスト記述ｎ１に存在するので、外部から入力される信号の信号名「ｆ０」にネットリスト記述ｎ１のレジスタｆ０＿ｒｅｇが出力する信号の信号名「ｆ０」を関連づけ、外部から入力される信号の信号名「ｆ１」にネットリスト記述ｎ１のレジスタｆ１＿ｒｅｇが出力する信号の信号名「ｑ１」を関連づける（下記下線部参照）。
check＿dut inst＿check＿dut( .CLK(), .XMSK(),
.DIN(), .f0(f0), .f1(q1), .DOUT() );
次に、モニタ記述ｍ１に入力される信号の信号名にネットリスト記述ｎ１に入力される信号の信号名を関連づける。
【００８５】
前述したように、ＲＴＬ記述ｒ１に入力される信号の信号名に同等の信号名をネットリスト記述ｎ１から検索する。本具体例では信号名「ＣＬＫ」の信号、信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号が存在するので、これらの信号名を関連づける（下記下線部参照）。
check＿dut inst＿check＿dut ( .CLK(CLK), .XMSK(XMSK),
.DIN(DIN), .f0(f0), .f1(q1), .DOUT() );
以上の処理を行うことで、第１の関連づけ処理を施したネットリスト記述ｎ２が得られる。このネットリスト記述ｎ２に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【００８６】
図１４は、第１の関連づけ処理によって関連づけられたネットリスト回路を示す図である。
ネットリスト回路２１は、図１３に示すネットリスト記述ｎ２により実現される（タイミング検証用の）回路である。
【００８７】
このネットリスト回路２１には、モジュール回路１１ａが追加され、モジュール回路１１ａの信号名「ｆ０」の信号にネットリスト回路２１のレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号が接続され、モジュール回路１１ａの信号名「ｆ１」の信号にレジスタｆ１＿ｒｅｇの信号名「ｑ１」の信号が接続されている。
【００８８】
また、ネットリスト回路２１に入力される信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号、信号名「ＣＬＫ」の信号がそのままモジュール回路１１ａの同じ信号名の入力信号に接続されている。
【００８９】
アサーションチェック部２００は、モジュール回路１１ａの信号名「ａ」の信号および信号名「ｂ」の信号をチェックすることにより、ネットリスト回路２１のアサーションチェックを行うことができる。
【００９０】
次に、第１の関連づけ処理の第２の具体例について説明する。
＜第１の関連づけ処理の第２の具体例＞
本具体例は、図７に示すＲＴＬ記述ｒ１を論理合成したネットリスト記述外部のテストベンチ記述上に、図９に示すモニタ記述ｍ１を追加する例である。
【００９１】
図１５は、第１の関連づけ処理を施したテストベンチ記述を示す図である。
まず、第１のモニタ記述作成処理で作成したモニタ記述ｍ１を第１の具体例と同様にインスタンス化してテストベンチ記述へ追加する。
check＿dut inst＿check＿dut ( .CLK(), .XMSK(),
.DIN(), .f0(), .f1(), .DOUT() );
次に、モニタ記述ｍ１の外部から入力される信号の信号名「ｆ０」、「ｆ１」にネットリスト記述のレジスタが出力する信号の信号名を関連づける。
【００９２】
前述したように、ＲＴＬ記述ｒ１に記述されているレジスタと同等のレジスタがネットリスト記述ｎ１に存在するか否かを、ライブラリ格納部９００に格納されているライブラリから検索する。本具体例では、信号名「ｆ０」の信号を出力するレジスタｆ０＿ｒｅｇおよび信号名「ｑ１」の信号を出力するレジスタｆ１＿ｒｅｇがネットリスト記述ｎ１に存在するので、外部から入力される信号の信号名「ｆ０」にネットリスト記述ｎ１のレジスタｆ０＿ｒｅｇが出力する信号の信号名「ｆ０」を関連づけ、外部から入力される信号の信号名「ｆ１」にネットリスト記述ｎ１のレジスタｆ１＿ｒｅｇが出力する信号の信号名「ｑ１」を関連づける（下記下線部参照）。なお、信号名の前にインスタンス名を付加する。
check＿dut inst＿check＿dut (.CLK(), .XMSK(),
.DIN(), .f0(inst＿dut.f0), .f1(inst＿dut.q1), .DOUT() );」
次に、モニタ記述ｍ１に入力される信号の信号名にネットリスト記述ｎ１に入力される信号の信号名を関連づける。
【００９３】
前述したように、ＲＴＬ記述ｒ１に入力される信号の信号名に同等の信号名をネットリスト記述ｎ１から検索する。本具体例では信号名「ＣＬＫ」の信号、信号名「ＸＭＳＫ」の信号および信号名「ＤＩＮ」の信号が存在するので、これらの信号名を関連づける（下記下線部参照）。なお、信号名の前にインスタンス名を付加する。
check＿dut inst＿check＿dut(.CLK(inst＿dut.CLK), .XMSK(inst＿dut.XMSK),
.DIN(inst＿dut.DIN), .f0(inst＿dut.f0), .f1(inst＿dut.q1), .DOUT() );
以上の処理を行うことで、第１の関連づけ処理を施したテストベンチ記述ｔ１が得られる。このテストベンチ記述ｔ１に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【００９４】
また、本具体例は、ネットリスト記述およびテストベンチ記述がＶｅｒｉｌｏｇの場合のみ適用することができる。
図１６は、第１の関連づけ処理によって関連づけられたテストベンチ回路を示す図である。
【００９５】
テストベンチ回路３１は、図１５に示すテストベンチ記述ｔ１により実現される回路である。
このテストベンチ回路３１は、ネットリスト回路２１ａとは別個にモジュール回路１１ａが追加され、モジュール回路１１ａの信号名「ｆ０」の信号にネットリスト回路２１ａのレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号が接続され、モジュール回路１１ａの信号名「ｆ１」の信号にレジスタｆ１＿ｒｅｇの信号名「ｑ１」の信号が接続されている。
【００９６】
また、ネットリスト回路２１ａに入力される信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号、信号名「ＣＬＫ」の信号がそのままモジュール回路１１ａの同じ信号名の入力信号に接続されている。
【００９７】
アサーションチェック部２００は、モジュール回路１１ａの信号名「ａ」の信号および信号名「ｂ」の信号をチェックすることにより、ネットリスト回路２１ａのアサーションチェックを行うことができる。
＜モニタ記述の特殊関連づけ処理＞
次に、図１１に示すステップＳ２４、Ｓ２７のモニタ記述の特殊関連づけ処理について説明する。
【００９８】
複数のレジスタに同じ論理が入力される場合や、固定値がレジスタに入力される場合は、論理合成したネットリスト記述ではそのレジスタが削除される場合がある。
またネットリスト記述の信号名がＲＴＬ記述とは異なる信号名に変更される場合もある。
【００９９】
このようなケースでは、単純にネットリスト記述に記述されているレジスタが出力する信号の信号名やモジュール回路に入力する信号の信号名をモニタ記述の信号名に関連づける処理ができない。より詳しくは、ネットリスト記述のレジスタが削除された場合や入力信号名が変更された場合、そのままＲＴＬ記述とネットリスト記述のＦｏｒｍａｌ検証を行うと不一致になる。そのためモニタ記述の特殊関連づけ処理を行うことになる。
【０１００】
具体的には、変更内容に対応するＦＶスクリプトを用意してＲＴＬ記述とネットリスト記述が等価であることを検証する。このＦＶスクリプトにＲＴＬ記述からの変更内容が設定されているため、変更内容を読み取りモニタ記述の関連づけ処理に使用する。なお、論理合成時のログファイル等でも変更内容が出力されている場合、ログファイルを読み込んで処理を行ってもよい。
【０１０１】
以下、第１の関連づけ処理の第１の具体例で述べた例と同様のケース、すなわち、モジュール回路のモニタ記述をネットリスト記述に追加してネットリスト記述と関連づける例を用いてモニタ記述の特殊関連づけ処理を説明する。
【０１０２】
図１７は、ＲＴＬ記述の他の例を示す図であり、図１８は、図１７に示すＲＴＬ記述により実現されるモジュール回路を示す図である。
図１７に示すＲＴＬ記述ｒ２により図１８に示すモジュール回路４１が実現される。
【０１０３】
モジュール回路４１は、レジスタＱ０＿ｒｅｇと、レジスタＱ１＿ｒｅｇ０〜Ｑ１＿ｒｅｇ２と、ＡＮＤ回路ａｎｄ５と、セレクタ４２とを有している。
レジスタＱ０＿ｒｅｇと、レジスタＱ１＿ｒｅｇ０〜Ｑ１＿ｒｅｇ２とは、それぞれ信号名「ＣＬＫ」の信号により動作する。レジスタＱ１＿ｒｅｇ０の入力には論理‘０’（固定値）の信号が入力され、レジスタＱ０＿ｒｅｇおよびレジスタＱ１＿ｒｅｇ２の入力には、それぞれ信号名「Ａ」の信号が入力される。また、レジスタＱ１＿ｒｅｇ１の入力には、信号名「Ａ」の信号の論理を反転させた信号が入力される。
【０１０４】
ＡＮＤ回路ａｎｄ５の入力には、信号名「Ｂ」の信号とレジスタＱ０＿ｒｅｇが出力する信号名「ｑ０」の信号とが入力され、これらの信号の論理に応じて信号名「Ｃ」の信号を出力する。
【０１０５】
セレクタ４２の入力には、レジスタＱ１＿ｒｅｇ０が出力する信号名「ｑ１［０］」の信号とレジスタＱ１＿ｒｅｇ１が出力する信号名「ｑ１［１］」の信号とレジスタＱ１＿ｒｅｇ２が出力する信号名「ｑ１［２］」の信号とが入力され、これらのうちの１つを選択した信号名「Ｄ」の信号を出力する。
【０１０６】
レジスタＱ０＿ｒｅｇおよびレジスタＱ１＿ｒｅｇ２のように、複数のレジスタで同じ信号名「Ａ」の信号が入力される場合や、レジスタＱ１＿ｒｅｇ０のように固定値が入力される場合は、論理合成したネットリスト記述ではそのレジスタが削除される場合がある。
【０１０７】
図１９は、図１７に示すＲＴＬ記述を論理合成したネットリスト記述により実現されるネットリスト回路を示す図である。
図１９に示すネットリスト回路５１では前者の例としてレジスタＱ０＿ｒｅｇに対応するレジスタｑ０＿ｒｅｇが削除されている。また、後者の例としてレジスタＱ１＿ｒｅｇ０に対応するレジスタｑ１＿ｒｅｇ＿０が削除され、セレクタ４２の代わりにＡＮＤ回路ＡＮＤ６が設けられている。このような場合、モニタ記述の特殊関連づけ処理を行ってＦＶスクリプト格納部１０００に格納されているＦＶスクリプトから、削除されたレジスタの内容を検索し、代わりの信号または固定値を関連づける。
【０１０８】
また、ＲＴＬ記述ｒ２の信号名「Ｂ」の信号がネットリスト回路５１では信号名「Ｂ＿０」の信号に変更されている。このような場合、モニタ記述の特殊関連づけ処理を行ってＦＶスクリプト格納部１０００に格納されているＦＶスクリプトから、変更した信号名を検索し、その信号名を関連づける。
【０１０９】
図２０は、図１７に示すＲＴＬ記述に、モニタ記述の特殊関連づけ処理を施したモニタ記述を示す図である。
モニタ記述については、前述したように、ＲＴＬ記述ｒ２のモジュール回路名「dut2」を別の名前「check＿dut2」に変更する。
【０１１０】
また、モニタ記述のレジスタに関する記述、すなわち、
reg q0;
reg [2:0] q1;
always @(posedge CLK) begin
q0 <= A;
end
always @(posedge CLK) begin
if( A )
q1 <= 3'b100;
else
q1 <= 3'b010;
end
を削除する。
【０１１１】
そして、１行目のｍｏｄｕｌｅ文に「q0、q1」を追加し、２行目（ｉｎｐｕｔ定義箇所）に「q0」を追加し、３行目（ｉｎｐｕｔ定義箇所）に「input [2:0] q1;」を追加する。これにより図２０に示すモニタ記述ｍ２が得られる。
【０１１２】
図２１は、図１７に示すＲＴＬ記述に、モニタ記述の特殊関連づけ処理を施すときのＦＶスクリプトを示す図であり、図２２は、図１７に示すＲＴＬ記述に、モニタ記述の特殊関連づけ処理を施したネットリスト記述を示す図である。
【０１１３】
図２１に示すように、変更内容に対応するＦＶスクリプトｆｖ１を用意する。
まず、レジスタｑ０＿ｒｅｇは削除されているため、ＦＶスクリプトｆｖ１の３行目から信号名「ｑ０］」の信号は信号名「ｑ１［２］」の信号と同等であることを読み込んで、レジスタｑ０＿ｒｅｇが出力する信号の信号名「ｑ０」には信号名「ｑ１［２］」を関連づける。すなわち図２２に示すネットリスト記述ｎ３の１３行目を「q0(q1＿2＿),」のように記述する。
【０１１４】
またレジスタｑ１＿ｒｅｇ＿０が削除されているため、ＦＶスクリプトｆｖ１の２行目からレジスタｑ１＿ｒｅｇ＿０が出力する信号の信号名「ｑ１［０］」は論理‘０’の信号の信号名であることを読み込んで、レジスタＱ０＿ｒｅｇが出力する信号の信号名「ｑ１［０］」には論理‘０’の信号の信号名を関連づける。すなわち、ネットリスト記述ｎ３の１４行目を「q1(｛q1＿2＿, q1＿1＿, 1'b0｝));」のように記述する。
【０１１５】
さらに、信号名「Ｂ」の信号が信号名「Ｂ＿０」の信号に変更されているため、ＦＶスクリプトｆｖ１の１行目から信号名「Ｂ」の信号が信号名「Ｂ＿０」の信号に変更されたことを読み込んで、信号名「Ｂ」に信号名「Ｂ＿０」を関連づける。すなわち、ネットリスト記述ｎ３の１３行目を「.B(B＿0),」のように記述する。
【０１１６】
以上の処理を行うことで、モニタ記述ｍ２の信号がネットリスト記述の信号に関連づけられたネットリスト記述ｎ３が得られる。このネットリスト記述ｎ３に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【０１１７】
図２３は、特殊関連づけ処理が施されたネットリスト記述により実現されるネットリスト回路を示す図である。
ネットリスト記述ｎ３により実現されるネットリスト回路５１ａには、モジュール回路４１ａが追加されている。
【０１１８】
ネットリスト回路５１ａでは、モジュール回路４１ａの信号名「ｑ０」の信号に信号名「ｑ１［２］」の信号が接続されている。
また、モジュール回路４１ａの信号名「ｑ１［０］」の信号に論理‘０’の信号が接続されている。
【０１１９】
また、モジュール回路４１ａの信号名「Ｂ」の信号に信号名「Ｂ＿０」の信号が接続されている。
このように、ネットリスト記述のレジスタが削除された場合や入力信号名が変更された場合についてもモニタ記述の信号をネットリスト記述へ関連づけることができる。
【０１２０】
以上述べたように、第１の実施の形態の設計検証装置１００によれば、ネットリスト記述で動作しているレジスタの出力について、ＲＴＬ記述で使用していた組み合わせ回路の内部信号名でアサーションチェックすることができるので、ネットリスト検証でＲＴＬ記述と同等のアサーションチェックが可能になり、誤動作発生箇所を容易かつ確実に発見することができる。また、外部端子まで伝搬せずに発見できなかった誤動作を容易かつ確実に発見することができる。
【０１２１】
＜第２の実施の形態＞
次に、第２の実施の形態の設計検証装置について説明する。
以下、第２の実施の形態の設計検証装置について、前述した第１の実施の形態の設計検証装置との相違点を中心に説明し、同様の事項については、その説明を省略する。
【０１２２】
図２４は、第２の実施の形態の構成を示すブロック図である。
第２の実施の形態の設計検証装置１００ａは、アサーションチェッカがＰＳＬの場合であり、ｖｕｎｉｔを使ってＲＴＬ記述とは別個に記述してあるアサーションチェッカモデル記述を格納するアサーションチェッカモデル記述格納部１１００をさらに有している。
【０１２３】
以下、第２の実施の形態の設計検証装置１００ａによる設計検証方法（第２の設計検証方法）について説明する。
＜第２の設計検証方法＞
第２の設計検証方法は、モニタ記述作成処理および関連づけ処理が第１の設計検証方法とは異なっている。
【０１２４】
図２５は、第２の設計検証方法を示す処理フローである。
モニタ記述作成部３５０は、ＲＴＬ記述に加え、ステップＳ４のレイアウトによって得られたネットリスト記述を用いてモニタ記述作成処理を行う（ステップＳ５ａ）。そして、モニタ記述作成処理が施されたモニタ記述をモニタ記述格納部７００に格納する。
【０１２５】
また、関連づけ処理部３６０は、モニタ記述作成処理が施されたモニタ記述の信号をネットリスト記述格納部５００に格納されているネットリスト記述の信号、テストベンチ記述の信号またはアサーションチェッカモデル記述の信号に関連づけてこれらの信号を関連づける関連づけ処理を行う（ステップＳ６ａ）。
【０１２６】
＜第２のモニタ記述作成処理＞
以下、本実施の形態のステップＳ５ａのモニタ記述作成処理（第２のモニタ記述作成処理）について詳しく説明する。
【０１２７】
図２６は、第２のモニタ記述作成処理を示すフローチャートである。
まず、モニタ記述作成部３５０が、ＲＴＬ記述のモジュール回路名および入出力信号名の定義文を削除する（ステップＳ３１）。
【０１２８】
次に、モニタ記述作成部３５０が、別の名前に変更したＲＴＬ記述からレジスタ記述に関する部位を全て削除する（ステップＳ３２）。
次に、モニタ記述作成部３５０が、ＲＴＬ記述に残った組み合わせ回路で生成される信号で、その信号がネットリスト記述の内部信号または出力信号に存在する場合は、組み合わせ回路内のその部分を削除する（ステップＳ３３）。
【０１２９】
以上で第２のモニタ記述作成処理を終了する。
次に、モニタ記述作成処理の具体例を説明する。
図２７は、図７に示すＲＴＬ記述に、第２のモニタ記述作成処理を施したモニタ記述を示す図である。
【０１３０】
まず、ＲＴＬ記述ｒ１のモジュール回路名、入出力信号名の定義文すなわち、１行目〜３行目の「module dut ( CLK, DIN, XMSK, DOUT )・・・DOUT;」および２１行目の「endmodule」を削除する。なお、図２７ではコメントアウトしている。
【０１３１】
また、ＲＴＬ記述ｒ１からレジスタ記述、すなわち、６行目の「reg f0，f1;」、および１７〜２０行目の「always @(posedge CLK) begin・・・end」を削除する。なお、図２７ではコメントアウトしている。
【０１３２】
そして、ＲＴＬ記述ｒ１の組み合わせ回路で生成される信号で、その信号が図１２に示すネットリスト記述ｎ１の内部信号または出力信号に存在する１５行目の「assign DOUT=b & ~a;」を削除する。
【０１３３】
これにより、図２７に示すモニタ記述ｍ３が得られる。
図２８は、図２７に示すモニタ記述により実現される組み合わせ回路を示す図である。
図２８中、点線で示した部分は、削除されたことを示している。
【０１３４】
組み合わせ回路６１は、第２のモニタ記述作成処理により、モジュール回路１１の枠組みが削除されている。
また、レジスタＦ０＿ｒｅｇ、Ｆ１＿ｒｅｇが削除されている。
【０１３５】
そして、ＡＮＤ回路ａｎｄ４が削除されている。
＜第２の関連づけ処理＞
次に、図２５に示す本実施の形態のステップＳ６ａの関連づけ処理（第２の関連づけ処理）について説明する。
【０１３６】
図２９は、第２の関連づけ処理の処理フローを示す図である。
まず、関連づけ処理部３６０が、第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述を、ネットリスト記述、テストベンチ記述、またはアサーションチェッカモデル記述に直接記述し追加する（ステップＳ４１）。
【０１３７】
次に、関連づけ処理部３６０が、ＲＴＬ記述のレジスタが出力する信号にネットリスト記述格納部５００に格納されているネットリスト記述のレジスタが出力する信号を関連づける。
【０１３８】
具体的には、ライブラリ格納部９００に格納されているライブラリを検索し、ＲＴＬ記述と同等のレジスタがネットリスト記述に存在するか否かを判断する（ステップＳ４２）。
【０１３９】
同等のレジスタが存在しない場合（ステップＳ４２のＮｏ）、モニタ記述の特殊関連づけ処理を行う。すなわち、ＦＶスクリプト格納部１０００に格納されているＦＶスクリプトから、削除されたレジスタの内容を検索し、代わりの信号または固定値をモニタ記述のレジスタに関連づける（ステップＳ４３）。
【０１４０】
一方、存在する場合（ステップＳ４２のＹｅｓ）、モニタ記述にネットリスト記述のレジスタが出力する信号と同じ信号名が存在しているか否かを判断する（ステップＳ４４）。
【０１４１】
存在する場合（ステップＳ４４のＹｅｓ）、ステップＳ４６に移行する。
一方、存在しない場合（ステップＳ４４のＮｏ）、ネットリスト記述のレジスタが出力する信号の信号名をモニタ記述のレジスタに関連づける（ステップＳ４５）。
【０１４２】
次に、関連づけ処理部３６０が、組み合わせ回路に入力される信号にネットリスト記述またはテストベンチ記述に入力される信号を関連づける。
具体的には、ステップＳ４１にて追加した組み合わせ回路の信号にネットリスト記述またはテストベンチ記述と同じ信号名が存在するか否かを判断する（ステップＳ４６）。
【０１４３】
存在しない場合（ステップＳ４６のＮｏ）、モニタ記述の特殊関連づけ処理を行う。すなわち、変更された信号名をＦＶスクリプトから検索し、その信号を関連づける（ステップＳ４７）。
【０１４４】
一方、存在する場合（ステップＳ４６のＹｅｓ）、ステップＳ４８に移行する。
次に、関連づけ処理部３６０が、処理結果を格納先に格納する（ステップＳ４８）。
具体的には、ステップＳ４１でモニタ記述をネットリスト記述に追加した場合、ステップＳ４２〜ステップＳ４７の処理が施されたモニタ記述が追加されたネットリスト記述をネットリスト記述格納部５００に格納する。ステップＳ４１でモニタ記述をテストベンチ記述に追加した場合、ステップＳ４２〜ステップＳ４７の処理が施されたモニタ記述が追加されたテストベンチ記述をテストベンチ記述格納部８００に格納する。ステップＳ４１でモニタ記述をアサーションチェッカモデル記述に追加した場合、ステップＳ４２〜ステップＳ４７の処理が施されたモニタ記述が追加されたアサーションチェッカモデル記述をアサーションチェッカモデル記述格納部１１００に格納する。
【０１４５】
以上で第２の関連づけ処理を終了する。
次に、第２の関連づけ処理の具体例を説明する。ステップＳ４８にて説明したように、モニタ記述をネットリスト記述に追加する方法とテストベンチ記述に追加する方法とアサーションチェッカモデル記述に追加する方法とがある。以下順番に説明する。
【０１４６】
＜第２の関連づけ処理の第１の具体例＞
本具体例は、第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述を第２の関連づけ処理を行うことによりネットリスト記述内部に追加してネットリスト記述に関連づける例である。
【０１４７】
図３０は、図１２に示すネットリスト記述ｎ１に、第２の関連づけ処理を施したネットリスト記述を示す図である。
まず、第２のモニタ記述作成処理で作成した組み合わせ回路のモニタ記述ｍ３を下記のようにネットリスト記述ｎ１へ直接記述し追加する。また、ＲＴＬ記述ｒ１にアサーションチェッカが記述されている場合、ここでアサーションチェッカも追加する。
// psl default clock = ( posedge CLK ) ;
// psl property
// chk = always ｛ a ｝ |=> ｛ b ｝ ;
// psl assert chk ;
wire a, b;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、ＲＴＬ記述ｒ１のレジスタが出力していた信号名「ｆ０」、「ｆ１」の信号に、ネットリスト記述ｎ１のレジスタが出力する信号名の信号を関連づける。
【０１４８】
具体的には、ライブラリ格納部９００に格納されているライブラリを検索し、ＲＴＬ記述ｒ１と同等のレジスタがネットリスト記述ｎ１に存在するか否かを判断する。
本具体例では、レジスタＦ０＿ｒｅｇに対応するレジスタｆ０＿ｒｅｇおよびレジスタＦ１＿ｒｅｇに対応するレジスタｆ１＿ｒｅｇが存在する。
【０１４９】
ここで、レジスタＦ０＿ｒｅｇが出力していた信号の信号名「ｆ０」はネットリスト記述ｎ１に存在するため何もしない。何もしなくても、モニタ記述ｍ３の信号名「ｆ０」の信号は、ネットリスト記述ｎ１のレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号に接続されたことになる。
【０１５０】
一方、レジスタＦ１＿ｒｅｇが出力していた信号の信号名「ｆ１」はネットリスト記述ｎ１に存在しないため、ネットリスト記述のレジスタｆ１＿ｒｅｇが出力する信号の信号名「ｑ１」を関連づける（下記下線部参照）。
// psl default clock = ( posedge CLK ) ;
// psl property
// chk = always ｛ a ｝ |=> ｛ b ｝ ;
// psl assert chk ;
wire a, b;
wire f1;
assign f1 = q1;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、モニタ記述ｍ３の組み合わせ回路に入力される信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号にネットリスト記述ｎ１に入力される信号を関連づける。
【０１５１】
具体的には、ネットリスト記述ｎ１を検索し、これらの信号名の信号と同等の信号名の信号が存在するか否かを判断する。
本具体例では信号名「ＸＭＳＫ」の信号、信号名「ＣＬＫ」の信号は存在するので何もしない。何もしなくても、モニタ記述ｍ３の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号はネットリスト記述ｎ１の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号とそれぞれ関連づけられたことになる。
【０１５２】
以上の処理を行うことで、モニタ記述ｍ３の信号がネットリスト記述ｎ１の信号に関連づけられたネットリスト記述ｎ４が得られる。このネットリスト記述ｎ４に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【０１５３】
図３１は、図３０に示すネットリスト記述により実現されるネットリスト回路を示す図である。
ネットリスト記述ｎ４により実現されるネットリスト回路７１には、組み合わせ回路６１が追加されている。
【０１５４】
組み合わせ回路６１の信号名「ｆ０」の信号にネットリスト回路７１のレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号が接続され、組み合わせ回路６１の信号名「ｆ１」の信号にレジスタｆ１＿ｒｅｇが出力する信号名「ｑ１」の信号が接続されている。
【０１５５】
また、ネットリスト回路７１に入力される信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号、信号名「ＣＬＫ」の信号がそのまま組み合わせ回路６１の同じ信号名の入力信号に接続されている。
【０１５６】
アサーションチェック部２００は、組み合わせ回路６１の信号名「ａ」の信号および信号名「ｂ」の信号をチェックすることにより、ネットリスト回路７１のアサーションチェックを行うことができる。
【０１５７】
＜第２の関連づけ処理の第２の具体例＞
本具体例は、第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述を第２の関連づけ処理を行うことによりテストベンチ記述に追加してネットリスト記述に関連づける例である。
【０１５８】
図３２は、第２の関連づけ処理を施したテストベンチ記述を示す図である。
第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述ｍ３を下記のようにテストベンチ記述へ直接記述し追加する。ＲＴＬ記述ｒ１内部にアサーションチェッカが記述されている場合、ここでアサーションチェッカも追加される。
// psl default clock = ( posedge CLK ) ;
// psl property
// chk = always ｛ a ｝ |=> ｛ b ｝ ;
// psl assert chk ;
wire a, b;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、ＲＴＬ記述ｒ１のレジスタが出力していた信号名「ｆ０」、「ｆ１」の信号に、ネットリスト記述ｎ１のレジスタが出力する信号名の信号を関連づける。
【０１５９】
具体的には、ライブラリ格納部９００に格納されているライブラリを検索し、ＲＴＬ記述ｒ１と同等のレジスタがネットリスト記述ｎ１に存在するか否かを判断する。
本具体例ではレジスタＦ０＿ｒｅｇに対応するレジスタｆ０＿ｒｅｇおよびレジスタＦ１＿ｒｅｇに対応するレジスタｆ１＿ｒｅｇが存在するので、ネットリスト記述ｎ１のレジスタが出力する信号と同じ信号名がモニタ記述ｍ３に存在しているか否かを判断する。
【０１６０】
本具体例では、ネットリスト記述ｎ１のレジスタｆ０＿ｒｅｇが出力する信号の信号名はインスタンス名を含む「inst＿dut.f0」であり、ネットリスト記述ｎ１のレジスタｆ１＿ｒｅｇが出力する信号の信号名はインスタンス名を含む「inst＿dut.f1」であるため、同じ信号名はモニタ記述ｍ３に存在しない。従って、信号名「inst＿dut.f0」に信号名「ｆ０」の信号を関連づけ、信号名「inst＿dut.f1」に信号名「ｆ１」の信号を関連づける（下記下線部参照）。
// psl default clock = ( posedge CLK ) ;
// psl property
// chk = always ｛ a ｝ |=> ｛ b ｝ ;
// psl assert chk ;
wire a, b;
wire f0, f1;
assign f0 = inst＿dut.f0;
assign f1 = inst＿dut.q1;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、モニタ記述ｍ３の組み合わせ回路に入力される信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号にネットリスト記述ｎ１に入力される信号を関連づける。
【０１６１】
具体的には、ネットリスト記述ｎ１を検索し、これらの信号名の信号と同等の信号名の信号が存在するか否かを判断する。
本具体例では信号名「ＸＭＳＫ」の信号、信号名「ＣＬＫ」の信号は存在するので何もしない。何もしなくても、モニタ記述ｍ３の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号はネットリスト記述ｎ１の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号とそれぞれ接続されたことになる。
【０１６２】
以上の処理を行うことで、モニタ記述ｍ３の信号がネットリスト記述ｎ１の信号に関連づけられたテストベンチ記述ｔ２が得られる。このテストベンチ記述ｔ２に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【０１６３】
図３３は、図３２に示すテストベンチ記述により実現されるテストベンチ回路を示す図である。
テストベンチ記述ｔ２により実現されるテストベンチ回路８１には、組み合わせ回路６１が追加されている。また、ネットリスト回路２１ａは、図１２に示すネットリスト記述ｎ１により実現される回路である。すなわち、モニタ記述を第２の関連づけ処理を行うことによりテストベンチ記述に追加する場合はネットリスト記述には手を加えない。
【０１６４】
組み合わせ回路６１の信号名「ｆ０」の信号にネットリスト回路２１ａのレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号が接続され、組み合わせ回路６１の信号名「ｆ１」の信号にレジスタｆ１＿ｒｅｇが出力する信号名「ｑ１」の信号が接続されている。
【０１６５】
また、ネットリスト回路２１ａに入力される信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号、信号名「ＣＬＫ」の信号がそのまま組み合わせ回路６１の同じ信号名の入力信号に接続されている。
【０１６６】
アサーションチェック部２００は、組み合わせ回路６１の信号名「ａ」の信号および信号名「ｂ」の信号をチェックすることにより、ネットリスト回路２１ａのアサーションチェックを行うことができる。
【０１６７】
＜第２の関連づけ処理の第３の具体例＞
本具体例は、第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述を第２の関連づけ処理を行うことによりアサーションチェッカモデル記述内部に追加してネットリスト記述に関連づける例である。
【０１６８】
図３４は、第２の関連づけ処理を施したアサーションチェッカモデル記述を示す図である。
第２のモニタ記述作成処理で生成した組み合わせ回路のモニタ記述ｍ３を下記のようにアサーションチェッカへ直接記述し追加する。この例でのアサーションチェッカはＲＴＬ記述とは別ファイルである。
wire a, b;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、ＲＴＬ記述ｒ１のレジスタが出力していた信号名「ｆ０」、「ｆ１」の信号に、ネットリスト記述ｎ１のレジスタが出力する信号名の信号を関連づける。
【０１６９】
具体的には、ライブラリ格納部９００に格納されているライブラリを検索し、ＲＴＬ記述ｒ１と同等のレジスタがネットリスト記述ｎ１に存在するか否かを判断する。
本具体例では、レジスタＦ０＿ｒｅｇに対応するレジスタｆ０＿ｒｅｇおよびレジスタＦ１＿ｒｅｇに対応するレジスタｆ１＿ｒｅｇが存在する。
【０１７０】
ここで、レジスタＦ０＿ｒｅｇが出力していた信号の信号名「ｆ０」はネットリスト記述ｎ１に存在するため何もしない。何もしなくても、モニタ記述の信号名「ｆ０」の信号は、ネットリスト記述ｎ１のレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号に接続されたことになる。
【０１７１】
一方、レジスタＦ１＿ｒｅｇが出力していた信号の信号名「ｆ１」はネットリスト記述ｎ１に存在しないため、ネットリスト記述ｎ１のレジスタｆ１＿ｒｅｇが出力する信号の信号名「ｑ１」を関連づける（下記下線部参照）。
wire a, b;
wire f1;
assign f1 = q1;
assign a = f0 & XMSK;
assign b = f1 & XMSK;
次に、モニタ記述ｍ３の組み合わせ回路に入力される信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号にネットリスト記述ｎ１に入力される信号を関連づける。
【０１７２】
具体的には、ネットリスト記述ｎ１を検索し、これらの信号名の信号と同等の信号名の信号が存在するか否かを判断する。
本具体例では信号名「ＸＭＳＫ」の信号、信号名「ＣＬＫ」の信号は存在するので何もしない。何もしなくても、モニタ記述ｍ３の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号はネットリスト記述ｎ１の信号名「ＸＭＳＫ」の信号および信号名「ＣＬＫ」の信号とそれぞれ接続されたことになる。
【０１７３】
以上の処理を行うことで、モニタ記述ｍ３の信号がネットリスト記述ｎ１の信号に接続されたアサーションチェッカモデル記述ａ１が得られる。このアサーションチェッカモデル記述ａ１に追加されたモニタ記述部分のアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
【０１７４】
図３５は、図３４に示すアサーションチェッカモデル記述により実現されるネットリスト回路を示す図である。
ネットリスト記述ｎ１により実現されるネットリスト回路２１ａに組み合わせ回路６１を備えるアサーションチェッカモデル回路６１ａが追加されている。このように、本具体例においてもネットリスト記述には手を加えない。
【０１７５】
アサーションチェッカモデル回路６１ａの信号名「ｆ０」の信号にネットリスト回路２１ａのレジスタｆ０＿ｒｅｇが出力する信号名「ｆ０」の信号が接続され、アサーションチェッカモデル回路６１ａの信号名「ｆ１」の信号にレジスタｆ１＿ｒｅｇが出力する信号名「ｑ１」の信号が接続されている。
【０１７６】
また、ネットリスト回路２１ａに入力される信号名「ＸＭＳＫ」の信号、信号名「ＤＩＮ」の信号、信号名「ＣＬＫ」の信号がそのままアサーションチェッカモデル回路６１ａの同じ信号名の入力信号に接続されている。
【０１７７】
このアサーションチェッカモデル回路６１ａのアサーションチェックを行うことでネットリスト検証でのアサーションチェックが可能となる。
アサーションチェック部２００は、アサーションチェッカモデル回路６１ａの信号名「ａ」の信号および信号名「ｂ」の信号をチェックすることにより、ネットリスト回路２１ａのアサーションチェックを行うことができる。
【０１７８】
以上、本発明の設計検証プログラム、設計検証方法および設計検証装置を、図示の実施の形態に基づいて説明したが、本発明はこれに限定されるものではなく、各部の構成は、同様の機能を有する任意の構成のものに置換することができる。また、本発明に、他の任意の構成物や工程が付加されていてもよい。
【０１７９】
また、本発明は、前述した各実施の形態のうちの、任意の２以上の構成（特徴）を組み合わせたものであってもよい。
なお、上記の処理機能は、コンピュータによって実現することができる。その場合、設計検証装置１００が有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、例えば、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリ等が挙げられる。磁気記録装置としては、例えば、ハードディスク装置（ＨＤＤ）、フレキシブルディスク（ＦＤ）、磁気テープ等が挙げられる。光ディスクとしては、例えば、ＤＶＤ（Digital Versatile Disc）、ＤＶＤ−ＲＡＭ（Random Access Memory）、ＣＤ−ＲＯＭ（Compact Disc Read Only Memory）、ＣＤ−Ｒ（Recordable）／ＲＷ（ReWritable）等が挙げられる。光磁気記録媒体としては、例えば、ＭＯ（Magneto-Optical disk）等が挙げられる。
【０１８０】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭ等の可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【０１８１】
設計検証プログラムを実行するコンピュータは、例えば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送される毎に、逐次、受け取ったプログラムに従った処理を実行することもできる。
【０１８２】
以上の実施形態に関し、更に以下の付記を開示する。
（付記１）  ゲートレベルのネットリストを用いた設計検証を行う設計検証プログラムにおいて、
コンピュータを、
作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する作成処理手段、
前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける関連づけ処理手段、
として機能させることを特徴とする設計検証プログラム。
【０１８３】
（付記２）  前記作成処理手段は、前記ＲＴＬ記述のモジュール名を変更し、前記ＲＴＬ記述のレジスタに関する記述を全て削除し、削除したレジスタが出力する信号の信号名を、前記ＲＴＬ回路外部からの入力信号の信号名とした前記モニタ記述を作成することを特徴とする付記１記載の設計検証プログラム。
【０１８４】
（付記３）  前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記入力信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記２記載の設計検証プログラム。
【０１８５】
（付記４）  前記関連づけ処理手段は、前記モニタ記述を、テストベンチ記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記入力信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記２記載の設計検証プログラム。
【０１８６】
（付記５）  前記作成処理手段は、前記ＲＴＬ記述のモジュール名および入出力信号名の定義文を削除し、前記ＲＴＬ記述のレジスタに関する記述を全て削除し、前記ネットリストの内部信号または出力信号に対応する信号を出力する組み合わせ回路に関する記述を削除した前記モニタ記述を作成することを特徴とする付記１記載の設計検証プログラム。
【０１８７】
（付記６）  前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記モニタの削除された前記レジスタが出力していた信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記５記載の設計検証プログラム。
【０１８８】
（付記７）  前記関連づけ処理手段は、前記モニタ記述を、テストベンチ記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記モニタの削除された前記レジスタが出力していた信号のインスタンス名を含む信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記５記載の設計検証プログラム。
【０１８９】
（付記８）  前記関連づけ処理手段は、前記モニタ記述を、アサーションチェッカモデル記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記モニタの削除された前記レジスタが出力していた信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記５記載の設計検証プログラム。
【０１９０】
（付記９）  前記関連づけ処理手段は、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが存在するか否かを判断し、存在しない場合は論理等価検証用スクリプトから、削除された前記レジスタが出力していた信号の信号名に対応する前記ネットリストの信号名を検索し、検索された信号の信号名を、削除された前記レジスタが出力していた信号の信号名に関連づけることを特徴とする付記３または４もしくは６ないし８のいずれかに記載の設計検証プログラム。
【０１９１】
（付記１０）  前記関連づけ処理手段は、前記モニタに入力される信号の信号名に等しい前記ネットリストに入力される信号の信号名が存在するか否かを判断し、存在しない場合は論理等価検証用スクリプトから、前記モニタに入力される信号の信号名に対応する前記ネットリストの信号名を検索し、検索された信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記３または４もしくは６ないし８のいずれかに記載の設計検証プログラム。
【０１９２】
（付記１１）  前記関連づけ処理手段は、ライブラリの検索結果に基づいて前記判断を行うことを特徴とする付記１０記載の設計検証プログラム。
（付記１２）  前記関連づけ処理手段により信号が接続された状態で、前記組み合わせ回路のアサーションチェックを行うことを特徴とする付記１記載の設計検証プログラム。
【０１９３】
（付記１３）  ゲートレベルのネットリストを用いた設計検証を行う設計検証方法において、
作成処理手段が、作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成し、
関連づけ処理手段が、前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける、
ことを特徴とする設計検証方法。
【０１９４】
（付記１４）  ゲートレベルのネットリストを用いた設計検証を行う設計検証装置において、
作成されたＲＴＬのＲＴＬ記述からレジスタに関する記述を削除した組み合わせ回路のモニタのモニタ記述を作成する作成処理部と、
前記ＲＴＬを論理合成して得られるネットリストのネットリスト記述における入出力信号の信号名のうち、対応する信号の信号名を前記モニタ記述の入力信号の信号名に関連づける関連づけ処理部と、
を有することを特徴とする設計検証装置。
【０１９５】
（付記１５）  前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述またはテストベンチ記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記入力信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記２記載の設計検証プログラム。
【０１９６】
（付記１６）  前記関連づけ処理手段は、前記モニタ記述を、前記ネットリスト記述またはテストベンチ記述またはアサーションチェッカモデル記述に追加し、削除された前記レジスタに対応する前記ネットリスト記述に記述された前記レジスタが出力する信号の信号名を、前記モニタの削除された前記レジスタが出力していた信号の信号名に関連づけ、前記モニタに入力される信号の信号名に等しい前記ネットリストの信号の信号名を、前記モニタに入力される信号の信号名に関連づけることを特徴とする付記５記載の設計検証プログラム。
【図面の簡単な説明】
【０１９７】
【図１】本発明の概要を示す図である。
【図２】設計検証装置のハードウェア構成例を示す図である。
【図３】設計検証装置の構成を示すブロック図である。
【図４】設計検証部の機能を示すブロック図である。
【図５】第１の設計検証処理を示す処理フローである。
【図６】第１のモニタ記述作成処理を示すフローチャートである。
【図７】ＲＴＬ記述格納部に格納されているＲＴＬ記述の一例を示す図である。
【図８】図７に示すＲＴＬ記述により実現されるモジュール回路を示す図である。
【図９】第１のモニタ記述作成処理を施したモニタ記述を示す図である。
【図１０】作成されたモジュール回路を示す図である。
【図１１】第１の関連づけ処理を示すフローチャートである。
【図１２】論理合成したネットリスト記述を示す図である。
【図１３】第１の関連づけ処理を施したネットリスト記述を示す図である。
【図１４】関連づけられたネットリスト回路を示す図である。
【図１５】第１の関連づけ処理を施したテストベンチ記述を示す図である。
【図１６】関連づけられたテストベンチ回路を示す図である。
【図１７】ＲＴＬ記述の他の例を示す図である。
【図１８】ＲＴＬ記述により実現されるモジュール回路を示す図である。
【図１９】ネットリスト記述により実現されるネットリスト回路を示す図である。
【図２０】モニタ記述の特殊関連づけ処理を施したモニタ記述を示す図である。
【図２１】モニタ記述の特殊関連づけ処理用のＦＶスクリプトを示す図である。
【図２２】モニタ記述の特殊関連づけ処理を施したネットリスト記述を示す図である。
【図２３】ネットリスト記述により実現されるネットリスト回路を示す図である。
【図２４】第２の実施の形態の構成を示すブロック図である。
【図２５】第２の設計検証方法を示す処理フローである。
【図２６】第２のモニタ記述作成処理を示すフローチャートである。
【図２７】第２のモニタ記述作成処理を施したモニタ記述を示す図である。
【図２８】モニタ記述により実現される組み合わせ回路を示す図である。
【図２９】第２の関連づけ処理の処理フローを示す図である。
【図３０】第２の関連づけ処理を施したネットリスト記述を示す図である。
【図３１】ネットリスト記述により実現されるネットリスト回路を示す図である。
【図３２】第２の関連づけ処理を施したテストベンチ記述を示す図である。
【図３３】テストベンチ記述により実現されるテストベンチ回路を示す図である。
【図３４】第２の関連づけ処理を施したアサーションチェッカモデル記述を示す図である。
【図３５】アサーションチェッカモデル記述により実現されるネットリスト回路を示す図である。
【図３６】設計検証フローを示すフローチャートである。
【図３７】ＲＴＬ記述により実現されるモジュール回路の一例を示す図である。
【図３８】ネットリスト記述により実現されるネットリスト回路の一例を示す図である。
【符号の説明】
【０１９８】
１１、１１ａ、４１、４１ａ  モジュール回路
２１、２１ａ、５１、５１ａ、７１  ネットリスト回路
３１、８１  テストベンチ回路
６１  組み合わせ回路
６１ａ  アサーションチェッカモデル回路
１００、１００ａ  設計検証装置
２００  アサーションチェック部
３００  設計検証部
３１０  シミュレーション実行部
３２０  論理合成部
３３０  Ｆｏｒｍａｌ検証部
３４０  レイアウト実行部
３５０  モニタ記述作成部
３６０  関連づけ処理部
３７０  タイミング検証部
４００  ＲＴＬ記述格納部
５００  ネットリスト記述格納部
６００  実配線ＳＤＦ格納部
７００  モニタ記述格納部
８００  テストベンチ記述格納部
９００  ライブラリ格納部
１０００  ＦＶスクリプト格納部
１１００  アサーションチェッカモデル記述格納部
ａ１  アサーションチェッカモデル記述
ｆｖ１  ＦＶスクリプト
ｍ１、ｍ２、ｍ３  モニタ記述
ｎ１、ｎ２、ｎ３、ｎ４  ネットリスト記述
ｒ１、ｒ２  ＲＴＬ記述
ｔ１、ｔ２  テストベンチ記述
【図１】
0004983642.tif 000002
【図２】
0004983642.tif 000003
【図３】
0004983642.tif 000004
【図４】
0004983642.tif 000005
【図５】
0004983642.tif 000006
【図６】
0004983642.tif 000007
【図７】
0004983642.tif 000008
【図８】
0004983642.tif 000009
【図９】
0004983642.tif 000010
【図１０】
0004983642.tif 000011
【図１１】
0004983642.tif 000012
【図１２】
0004983642.tif 000013
【図１３】
0004983642.tif 000014
【図１４】
0004983642.tif 000015
【図１５】
0004983642.tif 000016
【図１６】
0004983642.tif 000017
【図１７】
0004983642.tif 000018
【図１８】
0004983642.tif 000019
【図１９】
0004983642.tif 000020
【図２０】
0004983642.tif 000021
【図２１】
0004983642.tif 000022
【図２２】
0004983642.tif 000023
【図２３】
0004983642.tif 000024
【図２４】
0004983642.tif 000025
【図２５】
0004983642.tif 000026
【図２６】
0004983642.tif 000027
【図２７】
0004983642.tif 000028
【図２８】
0004983642.tif 000029
【図２９】
0004983642.tif 000030
【図３０】
0004983642.tif 000031
【図３１】
0004983642.tif 000032
【図３２】
0004983642.tif 000033
【図３３】
0004983642.tif 000034
【図３４】
0004983642.tif 000035
【図３５】
0004983642.tif 000036
【図３６】
0004983642.tif 000037
【図３７】
0004983642.tif 000038
【図３８】
0004983642.tif 000039