"ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証プログラムにおいて,前記コンピュータを,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成手段,生成された要求毎に,各要求と各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成手段,生成された要求毎に,各要求に対して実行されたアサーションと,各要求に対して設定された前記期待値情報におけるアサーションとの整合性を判定する整合性判定手段,前記整合性の判定結果を出力する出力手段,として機能させることを特徴とする設計検証プログラム。請求項1において,前記試験パターンは,順序付けされた複数の要求を含む試験パターンを生成し,前記整合性判定手段は,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序とが異なる場合,エラー判定することを特徴とする設計検証プログラム。ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証プログラムにおいて,前記コンピュータを,順序付けされた複数の要求を含む試験パターンを生成する試験パターン生成手段,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序との整合性を判定する整合性判定手段,前記整合性の判定結果を出力する出力手段,として機能させることを特徴とする設計検証プログラム。ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと一致するか検証する設計検証装置において,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成手段と,生成された要求毎に,各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成手段と,生成された要求毎に,各要求に対して実行されたアサーションと,前記期待値情報における各要求に対して実行が期待されるアサーションとの整合性を判定する整合性判定手段と,前記整合性の判定結果を出力する出力手段とを備えることを特徴とする設計検証装置。ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと一致するかコンピュータに検証させる設計検証方法において,前記コンピュータが,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成工程と,生成された要求毎に,各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成工程と,生成された要求毎に,各要求に対して実行されたアサーションと,前記期待値情報における各要求に対して実行が期待されるアサーションとの整合性を判定する整合性判定工程と,前記整合性の判定結果を出力する出力工程とを実行することを特徴とする設計検証方法。アサーションのための試験パターンは,検証回路の規模や機能の増加に比例して膨大となるため,現状,ツールによる任意なパラメータ設定により,自動的に大量に生成され,この自動生成された膨大な試験パターンに対するアサーションが実行される。しかしながら,従来,試験パターンの動作とアサーションの動作は,互いに関連づけが行われておらず,それぞれ独立に動作していた。このため,例えば,試験パターンによる検証回路の入出力動作でアサーションの判定が行われるため,試験パターンが期待する動作と,検証回路の入出力動作が一致しているか,などの整合性に関しての検証が十分に行うことができず,十分な検証精度が確保されていない。具体的には,試験パターンが期待する動作が,検証回路の入出力動作で欠落しても,アサーションの判定結果によりエラーを検出することができない。例えば,10回の試験パターンに対して,何らかのエラー原因により,1回の検証回路の出力動作が欠落し,アサーション判定結果により9回の正常判定が行われた場合,正常のみのアサーション判定結果からは,欠落に対するエラーを検出できない。また,何らかのエラー原因により,10回の試験パターンに対して,余分な検証回路の出力動作を含む11回のアサーション判定が行われ,全て正常判定が行われた場合も,正常のみのアサーション判定結果からは,余分は検証回路の出力に対するエラーを検出できない。また,自動生成された膨大な試験パターンのうち,エラーの発生箇所である一部の動作結果のみでエラーの解析が行われている。このため,エラー発生時の検証回路の状態を適切に把握することができず,エラー原因の特定に多くの解析工数を要し,作業効率の低下を招いている。特に,エラー原因とその影響によるエラー発生までに時間のずれが生じる場合では,解析工数がさらに増大する。そこで,本発明の目的は,アサーションベース検証において,検証精度を向上させ,さらに,解析作業工数を削減することができる設計検証プログラム,設計検証装置,設計検証方法を提供することにある。上記目的を達成するための設計検証プログラム,設計検証装置,設計検証方法は,ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと一致するかコンピュータに検証させる設計検証処理において,コンピュータが,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成工程と,生成された要求毎に,各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成工程と,生成された要求毎に,各要求に対して実行されたアサーションと,期待値情報における各要求に対して実行が期待されるアサーションとの整合性を判定する整合性判定工程と,整合性の判定結果を出力する出力工程とを実行することを要件とする。さらに,上記目的を達成するための設計検証プログラム,設計検証装置,設計検証方法は,ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証処理において,コンピュータが,順序付けされた複数の要求を含む試験パターンを生成する試験パターン生成工程と,試験パターンにおける複数の要求の実行順序と,実際に実行された要求の実行順序との整合性を判定する整合性判定工程と,整合性の判定結果を出力する出力工程とを実行することを要件とする。開示の設計検証プログラム,設計検証装置,設計検証方法によれば,試験パターンの要求単位で,要求と関連付けてアサーションの実行を検証することができるため,アサーションベース検証において,検証精度を向上させ,さらに,解析作業工数を削減することができる。図1は,本実施の形態における設計検証装置の機能構成を示す図であり,図2は,本実施の形態における設計検証処理のフロー図である。図1及び図2を参照して,本実施の形態の設計検証装置100における設計検証処理の概要について説明する。まず,オペレータにより,試験項目に応じた試験パターンの試験制約情報500例えば,禁止動作であって,リード,ライトの発生順序,アドレス,データなどで定義するが試験パターン生成部201に入力される図2のS101。試験パターン生成部201は,試験制約情報500の条件を満たす試験パターンを自動生成する図2のS102。生成された試験パターンは,試験パターン記憶部502に記憶され,さらに,試験パターン/アサーション連携部202及びシーケンス制御部203に通知される。また,オペレータ操作により,アサーションの制約情報501をあらかじめ生成し,試験パターン/アサーション連携部202に入力する。アサーションの制約情報501は,あらかじめ登録されている複数のアサーションそれぞれを識別するために付されたアサーションIDについて,そのアサーションを試験パターンの各要求に対して実行するかどうかの適用の有無有効/無効を有する情報である。アサーション制約情報501は,図4にて例示する。試験パターン/アサーション連携部202は,アサーション制約情報を用いて,生成された試験パターンと,アサーションとの関連付けを行い,生成された試験パターンの各要求に対して有効となるアサーションの定義種類と,試験パターンとアサーションの整合性を判定するための条件要求単位の実行回数などを含むアサーション期待値テーブルを生成する図2のS103。アサーション期待値テーブルは,図4にて例示する。試験パターン/アサーション連携部202は,アサーション期待値テーブルを整合性判定部207に通知する。アサーション期待値テーブルについては後述する。試験パターンを構成する要求は,リード又はライトなどの単アクセス,又は特定の回路機能を実現するための複数の単アクセスのシーケンス複アクセスなどを単位とする。さらに,シーケンス制御部204は,生成された試験パターンの要求発行順序を含むシーケンス動作テーブルを生成し図2のS104,要求の発行順序を監視する。シーケンス制御部204は,シーケンス動作テーブルを整合性判定部207に通知する。シーケンス動作テーブルは,図5にて例示する。論理シミュレータ204は,試験パターン記憶部502に格納される試験パターン及びアサーション記憶部503に格納されるアサーションを用いて,検証回路504に対してアサーションを実行する図2のS105。状態監視部205は,検証回路504の状態を監視する図2のS106。具体的には,状態監視部205は,試験パターンの要求が発生しているかどうか監視し,要求が発生すると,その発生した要求を整合性判定部207に通知する。さらには,状態監視部205は,実行されるアサーション及びその成立条件を監視し,実行されたアサーション及びその実行結果をアサーション判定部206及び整合性判定部207に通知する。アサーション判定部206は,実行されたアサーション毎にその実行結果を判定し図2のS107,アサーションの実行結果に対する判定OK又はNGをアサーション判定記憶部505に格納する。アサーション判定部206は,アサーションの実行結果に対する判定及びアサーションの実行回数を整合性判定部207に通知する。整合性判定部207は,アサーション期待値テーブルから得られる試験パターンに対して期待されるアサーション動作,及びシーケンス動作テーブルから得られる期待される試験パターン動作と,状態監視部205から通知される情報発生した要求,実行されたアサーション及びその実行結果と,アサーション判定部206から通知される判定情報,アサーションの実行回数情報とから得られる実際のアサーション動作及び試験パターン動作との比較に基づいて,アサーション動作の整合性判定,試験パターン動作の整合性判定を行う図2のS108,さらに,整合性判定部207は,アサーション判定におけるNG判定アサーションエラーが発生した場合の該アサーションエラーに対応する試験パターンの要求の検出を行う。整合性判定部207は,整合性判定の結果及び検出結果を整合性判定記憶部506に格納する。すべての試験パターンに対する上記設計検証処理が終了するまで,上記設計検証処理を繰り返す図2のS109。図3は,本実施の形態における設計検証装置のハードウェア構成例を示す図である。図3において,設計検証装置100は,CPU102,ROM104,RAM106,記憶媒体アクセス装置108,入力装置110及び出力装置112を備える。CPU102は,設計検証装置100の全体的な制御を行い,設計検証プログラムを実行する。ROM104は,設計検証プログラムなどの各種コンピュータプログラムを記憶している。RAM106は,CPU102のワークエリアとして使用されるメモリである。記憶媒体アクセス装置108は,磁気ディスクドライブや光ディスクドライブなどであり,CPU102の制御に従って,磁気ディスクや光ディスクなどの記憶媒体109にアクセスして,データの読み出し及び書き込みを行う。入力装置110は,例えばキーボードやマウスなどであり,検証支援プログラムの実行に対する外部からの操作を可能とする。出力装置112は,例えばディスプレイやプリンタ装置であり,ディスプレイは設計検証プログラムの実行結果を表示し,プリンタ装置は,設計検証プログラムの実行結果を印刷出力する。各構成要素は,バス120を介して接続されている。また,ネットワークに接続して通信するための通信インターフェースなど他の機能要素を備えていてもよい。図1に示された設計検証装置100の各機能部試験パターン生成部201,試験パターン/アサーション連携部202,シーケンス制御部203,論理シミュレータ204,状態監視部205,アサーション判定部206,整合性判定部207は,図3に示したROM104,RAM106,記憶媒体109などの記憶領域に記憶された設計検証プログラムとして提供され,CPU102が該設計検証プログラムを実行することにより,各機能部の機能が実現される。また,図1に示された設計検証装置100のデータ類記憶部試験パターン記憶部502,アサーション記憶部503,検証回路記憶部504,アサーション判定記憶部505,整合性判定記憶部506は,図3に示したROM104,RAM106,記憶媒体109などの記憶領域として提供され,CPU102による設計検証プログラムの実行に伴う該記憶領域へのアクセスにより,該記憶領域に対するデータ類の読み出し及び書き込みが行われる。以下に,アサーション期待値テーブルの生成処理S103,シーケンス動作テーブルの生成処理S104,及び整合性判定処理S108について,さらに詳細に説明する。図4は,試験パターン/アサーション連携部202によるアサーション期待値テーブルの生成を説明する図である。オペレータ操作により,アサーションの制約情報501があらかじめ生成し,試験パターン/アサーション連携部202に入力される。アサーションの制約情報は,あらかじめ登録されている複数のアサーションそれぞれを識別するために付されたアサーションIDについて,そのアサーションを試験パターンの各要求に対して実行するかどうかの適用の有無有効/無効,及び,実行する場合有効の場合の実行回数を期待値として有する。例えば,図4のアサーション制約情報501において,アサーションIDA~Dを有効とし,アサーションIDE以降を無効と設定することで,複数のアサーションから,アサーションIDA~Dのアサーションのみが実行される。登録されている複数のアサーションから,今回の検証に必要なアサーションのみを選択することができる。また,図4のアサーション制約情報600において,アサーションIDと要求との対応関係として設定される数値は,各要求の試験パターン動作を行う場合の,各アサーションが実行される回数である。例えば,アサーションIDAと要求1との対応関係として期待値1が設定されているので,要求1の試験パターン動作を行う場合に,アサーションIDAが実行される回数は1回である。同様に,アサーションIDBと要求3との対応関係として期待値2が設定されているので,要求3の試験パターン動作を行う場合に,アサーションIDBが実行される回数は2回である。期待値0が設定される場合は,対応する要求の試験パターン動作を行う場合に,対応するアサーションIDのアサーションは実行されない。例えば,アサーションIDBと要求1との対応関係として期待値0が設定されているので,アサーションIDBは有効設定されていても,要求1の試験パターン動作に対しては,アサーションIDBは実行されない。試験パターン/アサーション連携部202は,試験パターン生成部201により生成された試験パターンを受け付け,アサーション制約情報501から,有効設定されているアサーションIDについて,試験パターン生成部201により生成された試験パターンの要求に対応する各アサーションIDの設定値を抽出し,これを,アサーション期待値テーブル602とする。アサーション期待値テーブル602は,生成された試験パターンに対して,要求単位で,期待されるアサーションの実行回数が関連付けられたテーブルである。図5は,シーケンス制御部203によるシーケンス動作テーブルの生成を説明する図である。シーケンス制御部203は,試験パターン生成部201により生成された試験パターンを受け付ける。試験パターンの要求は,実行される順に順序づけられ,シーケンス制御部203は,実行順に要求を記録したシーケンス動作テーブル604を生成する。例えば,図5において,生成された試験パターンの要求の実行順序が,要求1,要求2,要求1,要求1の順である場合は,シーケンス制御部203は,その実行順序に従って要求が並べられたシーケンス動作テーブル604を生成する。なお,回路によっては,要求の実行順序の入れ替わりが許可されている場合がある。この場合は,試験パターンで設定された順序通りに要求が実行されないときにエラーとしないため,要求の実行順序に代わって,シーケンス制御部203は,試験パターンに含まれる各要求毎に実行回数を期待値として記録したシーケンス動作テーブル604を生成する。例えば,図5において,生成された試験パターンで実行される要求が,実行順に要求1,要求2,要求1,要求1である場合,シーケンス制御部203は,要求1の実行回数3回,要求2の実行回数1回をシーケンス動作テーブルとして記録する。要求の実行順序の入れ替わりが許可されている場合は,シーケンス制御部203に対して,要求の実行回数を期待値とするための切替制約情報をあらかじめ定義する。図6乃至図8は,整合性判定部207による整合性判定処理を説明する図である。図6において,整合性判定部207は,試験パターン/アサーション連携部202よりアサーション期待値テーブル602を受領し,アサーション期待値テーブル602で期待されるアサーションと,実際に実行されるアサーションとの整合性一致/不一致を判定する。例えば,整合性判定部207は,状態監視部205から通知される情報発生した要求,実行されたアサーション及びその実行結果と,アサーション判定部206から通知される判定情報とから得られる実際のアサーション動作及び試験パターンの情報を取得する。そして,整合性判定部207は,実際に実行された要求に対して実際に実行されたアサーションと,アサーション期待値テーブル602で設定されている要求に対するアサーションIDの実行回数設定値とを比較し,一致しているかどうか判定する。例えば,図6に例示されるように,要求1の実行において,アサーションIDAが2回実行された場合,又は,要求2の実行において,アサーションIDDが実行されなかった場合に,整合性判定部207は,アサーション期待値テーブル602の設定値との不一致を検出する。整合性判定部207は,不一致を検出すると,エラーNG出力する。図7において,整合性判定部207は,シーケンス制御部203よりシーケンス動作テーブル604を受領し,シーケンス動作テーブル604で期待される要求の実行順序と,実際に実行される要求の実行順序との整合性を判定する。例えば,整合性判定部207は,要求が発生する毎に,状態監視部205から,実際に発生した要求の情報を取得し,その実際に発生した要求と,シーケンス動作テーブル604に記録されている要求の実行順序とを比較し,整合性を判定する。例えば,図7において,シーケンス動作テーブル604において,要求の実行順序が,最初に要求1が実行され,その次に要求2が実行されるものと期待される場合において,実際に実行された要求は,最初に要求1が実行され,その次に再度要求1が実行されたような場合,整合性判定部207は,シーケンス動作テーブル604に記録された実行順序との不一致を検出する。整合性判定部207は,不一致を検出すると,エラーNG出力する。また,シーケンス動作テーブル604が,実行順序に代わって,要求毎の実行回数を記録している場合,整合性判定部207は,要求毎に,期待される実行回数と,実際の実行回数とを比較し,整合性一致/不一致を判定する。図7に示される例では,要求1について,期待される実行回数が3回であるのに対して,実際の実行回数が2回であったため,整合性判定部207は不一致を検出する。図8において,整合性判定部207は,アサーション判定部206からの判定情報として,アサーションエラーNGの発生通知を受けると,そのアサーションエラーに対応するアサーションが実行時の要求を検出する。具体的には,整合性判定部207は,アサーションエラーが試験パターンのどの要求実行時に発生したかを判定する。整合性判定部207は,アサーション判定部206からアサーションの実行回数情報を取得し,状態監視部205から実行される要求の情報を順次取得し,それらの情報からアサーションエラー発生時に実行されている要求を特定する。図8の例では,整合性判定部207は,アサーションIDAの実行に対するアサーションエラー発生時に実行されていた要求は,最初の要求1の次に実行された2回目の要求1であることを特定する。これにより,アサーションエラー発生時の検証回路の状態を,要求単位で特定することができる。図9及び図10は,整合性判定処理のシーケンス例を示す図である。図9では,試験パターンとして,最初に要求1が実行され,その次に要求2が実行される。また,アサーション期待値テーブル600に設定された期待動作として,1回のアサーションIDAのアサーションが要求1で実行され,それぞれ1回ずつのアサーションIDB,C,Dのアサーションが要求2で実行されることが期待されるものとする。論理シミュレータ204は,要求1により検証回路504に対してアサーションを実行する。状態監視部205は,要求1の実行を整合性判定部207に通知する。アサーション判定部206は,アサーションの実行結果を整合性判定部207に通知するが,このとき,アサーション判定部206は,要求1の有効範囲有効期間中に,2回のアサーションIDAの実行結果を通知する。整合性判定部207は,要求1の有効期間中に実行された2回目のアサーションIDAのアサーションの実行が,期待動作と不一致である旨判定し,エラーNG出力する。さらに,アサーション判定部206は,要求2の有効範囲有効期間中に,それぞれ1回ずつのアサーションIDB,Cの実行結果を通知するが,アサーションIDDの実行結果を通知しなかった場合,整合性判定部207は,要求2の有効期間中にアサーションIDDが実行されなかったと判断し,期待動作と不一致である旨判定し,エラー出力する。図10では,図9と同様に,試験パターンとして,最初に要求1が実行され,その次に要求2が実行される。また,アサーション期待値テーブル600に設定された期待動作として,1回のアサーションIDAのアサーションが要求1で実行され,それぞれ1回ずつのアサーションIDB,C,Dのアサーションが要求2で実行されることが期待されるものとする。論理シミュレータ204は,要求1により検証回路504に対してアサーションを実行する。状態監視部205は,要求1の実行を整合性判定部207に通知する。アサーション判定部206は,アサーションの実行結果を整合性判定部207に通知するが,このとき,アサーション判定部206は,要求1の有効期間中に,1回のアサーションIDAの実行結果に加えて,1回のアサーションIDEの実行結果を通知する。整合性判定部207は,要求1の有効期間中に実行されたアサーションIDEのアサーションの実行が,期待動作と不一致である旨判定し,エラー出力する。さらに,アサーション判定部206は,要求2の有効期間中に,それぞれ1回ずつのアサーションIDB,Cの実行結果を通知し,さらに次の要求の有効期間中に,アサーションIDDの実行結果を通知する。整合性判定部207は,アサーションIDDの実行結果を受領するものの,要求2の有効期間中に受領しないため,要求2の有効期間中にアサーションIDDが実行されなかったと判断し,期待動作と不一致である旨判定し,エラー出力する。以上説明したように,本実施の形態例では,自動生成される試験パターンと,アサーションとの関連付けを行い,生成された試験パターンの各要求について,期待されるアサーション動作を含む期待値テーブルを生成する。そして,要求単位毎に,実際に実行されるアサーションの種類,実行回数及び実行タイミングを判定し,要求単位毎に,期待されるアサーション動作と実際に実行されるアサーション動作との一致/不一致を判定し,不一致の場合に,エラー出力する。さらに,生成された試験パターンの要求発行順序を期待値として,実際の要求発行順序との一致/不一致を判定し,不一致の場合にエラー出力する。これにより,試験パターンの要求単位で,要求と関連付けてアサーションの実行を検証することができるため,検証精度が向上し,アサーションエラーがどの要求に対応するものであるか容易に解析することができるようになる。本実施の形態における設計検証プログラムは,上述した設計検証処理をコンピュータ装置パーソナルコンピュータやワークステーションを含むに実行させるためのプログラムであり,本実施の形態における設計検証方法は,該プログラムをコンピュータ装置設計検証装置で実行させることで実現される。以上説明した実施の形態の主な技術的特徴は、以下の付記の通りである。付記1ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証プログラムにおいて,前記コンピュータを,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成手段,生成された要求毎に,各要求と各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成手段,生成された要求毎に,各要求に対して実行されたアサーションと,各要求に対して設定された前記期待値情報におけるアサーションとの整合性を判定する整合性判定手段,前記整合性の判定結果を出力する出力手段,として機能させることを特徴とする設計検証プログラム。付記2付記1において,前記整合性判定手段は,各要求に対して,前記期待値情報におけるアサーションと異なるアサーションが実行された場合に,エラー判定することを特徴とする設計検証プログラム。付記3付記1において,前記整合性判定手段は,各要求に対して,一定期間内に,前記期待値情報におけるアサーションが実行されない場合に,エラー判定することを特徴とする設計検証プログラム。付記4付記1において,前記期待値情報は,各要求に対して実行が期待されるアサーションの実行回数を含み,前記整合性判定手段は,各要求に対して実行されたアサーションの実行回数と,前記期待値情報におけるアサーションの実行回数とが異なる場合に,エラー判定することを特徴とする設計検証プログラム。付記5付記1において,前記試験パターンは,順序付けされた複数の要求を含む試験パターンを生成し,前記整合性判定手段は,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序とが異なる場合,エラー判定することを特徴とする設計検証プログラム。付記6ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証プログラムにおいて,前記コンピュータを,順序付けされた複数の要求を含む試験パターンを生成する試験パターン生成手段,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序との整合性を判定する整合性判定手段,前記整合性の判定結果を出力する出力手段,として機能させることを特徴とする設計検証プログラム。付記7ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと一致するか検証する設計検証装置において,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成手段と,生成された要求毎に,各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成手段と,生成された要求毎に,各要求に対して実行されたアサーションと,前記期待値情報における各要求に対して実行が期待されるアサーションとの整合性を判定する整合性判定手段と,前記整合性の判定結果を出力する出力手段とを備えることを特徴とする設計検証装置。付記8ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと一致するかコンピュータに検証させる設計検証方法において,前記コンピュータが,少なくとも一つの要求を含む試験パターンを生成する試験パターン生成工程と,生成された要求毎に,各要求に対して実行が期待されるアサーションとを関連付けた期待値情報を生成する期待値情報生成工程と,生成された要求毎に,各要求に対して実行されたアサーションと,前記期待値情報における各要求に対して実行が期待されるアサーションとの整合性を判定する整合性判定工程と,前記整合性の判定結果を出力する出力工程とを実行することを特徴とする設計検証方法。付記9ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証装置において,順序づけされた複数の要求を含む試験パターンを生成する試験パターン生成手段と,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序との整合性を判定する整合性判定手段と,前記整合性の判定結果を出力する出力手段とを備えることを特徴とする設計検証プログラム。付記10ハードウェア記述言語で記述された論理回路の論理シミュレーション実行結果が,前記論理回路の設計仕様として記述されたアサーションと適合するかコンピュータに検証させる設計検証方法において,前記コンピュータが,順序づけされた複数の要求を含む試験パターンを生成する試験パターン生成工程と,前記試験パターンにおける前記複数の要求の実行順序と,実際に実行された要求の実行順序との整合性を判定する整合性判定工程と,前記整合性の判定結果を出力する出力工程とを実行することを特徴とする設計検証方法。"