"検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付ける入力手段と、前記入力手段によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成する原因結果グラフ生成手段と、前記原因結果グラフ生成手段によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索する探索手段と、前記探索手段によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成する連結手段と、前記連結手段によって生成された原因結果グラフと、前記連結手段によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出する整合性検出手段と、前記整合性検出手段によって検出された検出結果を出力する出力手段と、を備えることを特徴とする検証支援装置。前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに前記他の原因結果グラフの結果ノードを追加する追加手段と、前記追加手段によって追加された結果ノードを含む前記連結済み原因結果グラフを構成するノードのうち、同一時間距離のノード間において排他関係があるか否かを判定することで前記記述データの矛盾性を検出する矛盾性検出手段と、を備え、前記出力手段は、前記矛盾性検出手段によって検出された検出結果を出力することを特徴とする請求項1に記載の検証支援装置。前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに含まれる論理和ノードに基づいて、前記連結済み原因結果グラフからサブグラフを抽出するサブグラフ抽出手段を備え、前記出力手段は、前記サブグラフ抽出手段によって抽出されたサブグラフを検証シナリオとして出力することを特徴とする請求項1に記載の検証支援装置。入力手段、原因結果グラフ生成手段、探索手段、連結手段、整合性検出手段および出力手段を備えるコンピュータが、前記入力手段により、検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付ける入力工程と、前記原因結果グラフ生成手段により、前記入力工程によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成する原因結果グラフ生成工程と、前記探索手段により、前記原因結果グラフ生成工程によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索する探索工程と、前記連結手段により、前記探索工程によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成する連結工程と、前記整合性検出手段により、前記連結工程によって生成された原因結果グラフと、前記連結工程によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出する整合性検出工程と、前記出力手段により、前記整合性検出工程によって検出された検出結果を出力する出力工程と、を実行することを特徴とする検証支援方法。検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付ける入力工程と、前記入力工程によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成する原因結果グラフ生成工程と、前記原因結果グラフ生成工程によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索する探索工程と、前記探索工程によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成する連結工程と、前記連結工程によって生成された原因結果グラフと、前記連結工程によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出する整合性検出工程と、前記整合性検出工程によって検出された検出結果を出力する出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。請求項5に記載の検証支援プログラムを記録した前記コンピュータに読み取り可能な記録媒体。しかしながら、論理回路におけるレジスタなどの状態保存モジュールの論理検証では仕様書より読み取った各レジスタ書き換え条件をモニタし誤りがあれば報告する検証プロパティを大量に作成する必要があった。しかもこれらの検証プロパティ間には優先順位が存在し、その優先順位を考慮した検証プロパティを誤りなく作成することは非常に困難な作業であった。この発明は、上述した従来技術による問題点を解消するため、検証期間の短縮化と設計者の作業労力の軽減化を図ることができる検証支援装置、検証支援方法、検証支援プログラム、および記録媒体を提供することを目的とする。本発明の一側面として、検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付け、入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成し、生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索し、探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成し、生成された原因結果グラフと、連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出し、検出された検出結果を出力する検証支援装置、検証支援方法、検証支援プログラム、および記録媒体が提案される。本発明にかかる検証支援装置、検証支援方法、検証支援プログラム、および記録媒体によれば、検証期間の短縮化と設計者の作業労力の軽減化を図ることができるという効果を奏する。以下に添付図面を参照して、この発明にかかる検証支援装置、検証支援方法、検証支援プログラム、および記録媒体の好適な実施の形態を詳細に説明する。なお、実施の形態における説明内容は、後述する各実施の形態1~9に共通する内容である。実施の形態<検証システムのシステム構成>まず、この発明の実施の形態にかかる検証システムについて説明する。検証システムは、検証対象回路の論理検証をおこなうシステムである。図1は、この発明の実施の形態にかかる検証システムのシステム構成図である。図1において、検証システム100は、検証支援装置101と検証装置102とから構成されている。検証支援装置101は、原因結果記述データ111を入力し、検証プロパティ112、検証シナリオ113、仕様書データ114、レビュー情報115を生成、出力するコンピュータ装置である。原因結果記述データ111については図3で後述する。ここで、検証プロパティ112とは、検証対象回路を構成する論理回路におけるレジスタの動作条件を示す原因と、その動作条件を満たした場合の動作内容状態変化を示す結果と、からなる記述データである。たとえば、レジスタが0から1に書き換わると2サイクル後に○○になる。といった検証プロパティ121や、○○になったということは2サイクル前にレジスタが0から1に書き換わっていなければならない。といった検証プロパティ122などがある。検証プロパティ112は、たとえば、PSLなどの検証プロパティ言語など、コンピュータが解釈可能な言語により記述される。また、検証シナリオ113とは、検証対象回路のある機能の検証する場合に、当該機能の流れシナリオを示す記述データである。たとえば、CPUの演算器の機能を検証する場合、AB=Cになるという動作がおこなわれるかどうかを検証するために演算器へ入力されるパターンデータである。検証装置102は、検証対象回路の回路情報116たとえば、HDL記述やネットリストと、検証支援装置101からの検証プロパティ112や検証シナリオ113を取り込んで、検証プロパティ112や検証シナリオ113どおりに検証対象回路が動作するかどうかを検証するコンピュータ装置である。<コンピュータ装置のハードウェア構成>つぎに、図1に示したコンピュータ装置検証支援装置101、検証装置102のハードウェア構成について説明する。図2は、図1に示したコンピュータ装置のハードウェア構成を示すブロック図である。図2において、コンピュータ装置は、CPU201と、ROM202と、RAM203と、HDDハードディスクドライブ204と、HDハードディスク205と、FDDフレキシブルディスクドライブ206と、着脱可能な記録媒体の一例としてのFDフレキシブルディスク207と、ディスプレイ208と、I/Fインターフェース209と、キーボード210と、マウス211と、スキャナ212と、プリンタ213と、を備えている。また、各構成部はバス200によってそれぞれ接続されている。ここで、CPU201は、コンピュータ装置の全体の制御を司る。ROM202は、ブートプログラムなどのプログラムを記憶している。RAM203は、CPU201のワークエリアとして使用される。HDD204は、CPU201の制御にしたがってHD205に対するデータのリード/ライトを制御する。HD205は、HDD204の制御で書き込まれたデータを記憶する。FDD206は、CPU201の制御にしたがってFD207に対するデータのリード/ライトを制御する。FD207は、FDD206の制御で書き込まれたデータを記憶したり、FD207に記憶されたデータを検証支援装置101に読み取らせたりする。また、着脱可能な記録媒体として、FD207のほか、CD-ROMCD-R、CD-RW、MO、DVDDigitalVersatileDisk、メモリーカードなどであってもよい。ディスプレイ208は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ208は、たとえば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。I/F209は、通信回線を通じてインターネットなどのネットワークに接続され、このネットワークを介して他の装置に接続される。そして、I/F209は、ネットワークと内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F209には、たとえばモデムやLANアダプタなどを採用することができる。キーボード210は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス211は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ212は、画像を光学的に読み取り、コンピュータ装置内に画像データを取り込む。なお、スキャナ212は、OCR機能を持たせてもよい。また、プリンタ213は、画像データや文書データを印刷する。プリンタ213には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。<原因結果記述データ111>つぎに、図1に示した原因結果記述データ111について説明する。図3は、原因結果記述データ111を示す説明図である。図3において、原因結果記述データ111は、結果定義情報と原因定義情報と、から構成される電子データである。ここで、結果定義情報とは、レジスタの状態変化の原因およびその結果のうち、レジスタが状態変化した結果を定義する情報である。結果定義情報は、レジスタ情報とフィールド情報と値情報とを有する。レジスタ情報とは、レジスタの物理位置を特定する情報であり、レジスタのアドレスとレジスタ名とから構成される。また、フィールド情報とは、フィールドの位置を示すレンジと、フィールド名から構成される。また、値情報とは、フィールドのとり得る値を特定する情報であり、書換値と当該フィールドがその書換値であるときの意味を表す値情報とその値が初期値かどうかをあらわす情報から構成される。また、原因定義情報とは、レジスタの状態変化の原因およびその結果のうち、レジスタが状態変化する原因を定義する情報である。原因定義情報は、優先度と書換条件とテンプレート情報とを有する。優先度とは、当該書換条件の優先順位をあらわしている。すなわち、図3の例では、フィールド名:IntReady0iを、その指定値0に書き換えるための条件の優先度が1であることを示している。書換え条件とは、当該フィールドを値情報の書換値にするための条件記述を表す。たとえば、C_RESET=1となったら次のサイクルでといったテキストデータが記述される。このテキストデータは、レビューとして表示されることとなる。テンプレート情報とは、前述の書換条件をフォーマルに定義する部であり、後述の図4に示すテンプレートDBのテンプレートとパラメータ値を用いて定義される情報である。具体的には、テンプレートの型を特定するテンプレートタイプと、テンプレートタイプのパラメータの定義とを記述する。図3では、テンプレートタイプとして1-1が記述され、その1-1のパラメータAをC_RESETと定義し、パラメータNを1と定義している。<テンプレートDB>つぎに、テンプレートDBについて説明する。図4は、テンプレートDBの記憶内容を示す説明図である。図4において、テンプレートDB400は、テンプレートタイプごとにテンプレート内容とテンプレート記述とを記憶している。テンプレート内容とは、テンプレート記述の意味をあらわす情報たとえば、テキストデータである。また、テンプレート記述は検証プロパティ言語で記述されている。テンプレート記述は、原因-結果に関する記述データを、パラメータを用いて抽象化した情報である。実施の形態1つぎに、この発明の実施の形態1について説明する。実施の形態1は、レジスタ書換え条件が発生したらレジスタ値が指定値へ変化することをチェックする検証プロパティ112を自動生成する形態である。<検証支援装置の機能的構成>まず、実施の形態1にかかる検証支援装置の機能的構成について説明する。図5は、実施の形態1にかかる検証支援装置の機能的構成を示すブロック図である。図5において、検証支援装置500は、テンプレートDB400と、入力部501と、テンプレート抽出部502と、検証プロパティ生成部503とを備えている。入力部501は、図3に示した原因結果記述データ111の入力を受け付ける。テンプレート抽出部502は、入力された原因結果記述データ111のテンプレートタイプを手がかりとして、テンプレートDB400からテンプレートタイプが一致するテンプレート記述を抽出する。検証プロパティ生成部503は、テンプレート抽出部502によって抽出されたテンプレート記述に、原因結果記述データ111の記述内容を与えることにより、検証プロパティ112を自動生成する。生成された検証プロパティ112の集合は、検証プロパティ群510としてメモリたとえば、図2に示したRAM203、HD205などに保持される。なお、上述した入力部501、テンプレート抽出部502、および検証プロパティ生成部503は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置500の検証支援処理手順>図6は、実施の形態1にかかる検証支援処理手順を示すフローチャートである。図6において、まず、入力部501により、原因結果記述データ111の入力を待ち受けるステップS601:No。そして、原因結果記述データ111が入力された場合ステップS601:Yes、未処理のレジスタがあるか否かを判断するステップS602。未処理のレジスタがあった場合ステップS602:Yes、テンプレート抽出部502により、その原因結果記述データ111に該当するテンプレート記述を抽出するステップS603。そして、検証プロパティ生成部503により、抽出されたテンプレート記述に原因結果記述データ111を与えることにより、検証プロパティ112を生成しステップS604、ステップS602に戻る。なお、ステップS602において、未処理のレジスタがないと判断された場合ステップS602:No、一連の処理を終了する。生成された検証プロパティ112は、検証装置102に与えられ、検証対象回路の論理検証が実行される。<具体例>図7は、実施の形態1にかかる検証プロパティ112の自動生成例を示す説明図である。ここでは、図3に示した原因結果記述データ111を例にあげて説明する。図3に示した原因結果記述データ111が与えられた場合、原因結果記述データ111のテンプレートタイプを手がかりとして、図4に示したテンプレートDB400からテンプレート記述を抽出する。そして、抽出されたテンプレート記述に、レジスタ書き換え条件として、原因結果記述データ111内のパラメータAを与え、レジスタ値の指定値変化として、パラメータNと、フィールド名:IntRdy0iと、値:01’b0を与えることにより、IntRdy0iはC_RESET=1となったら次のサイクルで0へ書き換わりを意味する検証プロパティ112を生成する。このように、実施の形態1によれば、設計者は、原因結果記述データ111を与えるだけで、レジスタ書換え条件が発生したらレジスタ値が指定値へ変化することをチェックする検証プロパティ112を簡単かつ自動的に生成することができる。したがって、設計者による検証作業の効率化、検証期間の短縮化を図ることができる。実施の形態2つぎに、この発明の実施の形態2について説明する。実施の形態2は、実施の形態1において、競合条件を追加表現する形態である。競合とは、複数の検証プロパティ112間で、矛盾しあう結果が同時に起こることである。このような場合、原因結果記述データ111の優先度の値をチェックして、検証プロパティ112に追加することで、優先順位の低い検証プロパティ112を用いた検証を途中でキャンセルすることができる。なお、実施の形態1と同一構成には同一符号を付し、その説明を省略する。<検証支援装置の機能的構成>まず、実施の形態2にかかる検証支援装置の機能的構成について説明する。図8は、実施の形態2にかかる検証支援装置の機能的構成を示すブロック図である。図8において、検証支援装置800は、入力部501、テンプレート抽出部502、および検証プロパティ生成部503のほか、検証プロパティ抽出部801と、書換条件生成部802と、を有する。検証プロパティ抽出部801は、検証プロパティ群510から競合しあう検証プロパティ112を抽出する。書換条件生成部802は、抽出された競合しあう検証プロパティ112におけるレジスタの書き換えが発生する条件を示す記述データ書換条件を生成する。検証プロパティ生成部503は、競合しあう検証プロパティ生成元となる原因結果記述データ111の優先度に基づいて、優先度の高い書換条件を検証プロパティ112のキャンセル条件に追加する。具体的には、たとえば、検証プロパティ言語の一つであるPSLのabort文を用いて、優先度の低い方の検証プロパティ112のabort文に、優先度が高い方の検証プロパティ112の書換条件を追加する。なお、上述した検証プロパティ抽出部801、および書換条件生成部802は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置800の検証支援処理手順>図9は、実施の形態2にかかる検証支援処理手順を示すフローチャートである。図9において、まず、検証プロパティ抽出部801により、任意の検証プロパティ112を抽出しステップS901、この検証プロパティ112と競合する検証プロパティ112が抽出されたか否かを判断するステップS902。競合する検証プロパティ112が抽出されなかった場合ステップS902:No、ステップS905に移行する。一方、競合する検証プロパティ112が抽出された場合ステップS902:Yes、書換条件生成部802により競合しあう検証プロパティ112ごとに書換条件を生成するステップS903。そして、検証プロパティ生成部503により、競合しあう検証プロパティ112の優先度に基づいて、優先度チェック済み検証プロパティ112を生成するステップS904。そして、優先度未チェックの検証プロパティ112があるか否かを判断しステップS905、優先度未チェックの検証プロパティ112がある場合ステップS905:Yes、ステップS902に戻る。一方、優先度未チェックの検証プロパティ112がない場合ステップS905:No、一連の処理を終了する。<具体例>図10は、実施の形態2にかかる検証プロパティ112の自動生成例を示す説明図である。図10中、検証プロパティP1は、C_RESET=1となったら次のサイクルで0へ書き換わりであり、検証プロパティP2は、Init0iビットが解除されたら1へ書き換わりとする。ここでは、便宜上、自然言語であらわしているが、実際は検証プロパティ言語で記述されている。また、検証プロパティP1は優先度:1とし、検証プロパティP2は優先度:3とする。検証プロパティP1と検証プロパティP2は、レジスタの書き換え結果が互いに矛盾するプロパティである。検証プロパティ抽出部801により、競合しあう検証プロパティP1,P2が抽出されると、書換条件生成部802により、検証プロパティP1の書換条件CN1と、検証プロパティP2の書換条件CN2とを生成する。検証プロパティP1において、C_RESET=1が発生するということは、それ以前がC_RESET=0であるということが条件となる。したがって、書換条件CN1が生成される。同様に、検証プロパティP2では、Init0iビットの解除前が1であり解除後が0ということである。書換条件CN1:endpointCN1={~C_RESET;C_RESET};書換条件CN2:endpointCN2={Init0i;~Init0i};そして、検証プロパティ生成部503では、優先度の高い方の検証プロパティP1には、その書換条件CN1を追加することにより、優先度チェック済み検証プロパティQ1を生成する。一方、優先度の低い方の検証プロパティP2には、その書換条件CN2を検証プロパティP2に追加するとともに、検証プロパティ言語のabortなどで記述された書換条件CN1からなるキャンセル文を追加することで、優先度チェック済みプロパティQ2を生成する。これにより、優先度チェック済み検証プロパティQ2では、書換条件CN1が発生した場合、チェックをキャンセルすることとなる。したがって、優先度チェック済み検証プロパティQ1,Q2は競合することはない。したがって、検証プロパティ間で競合が発生しても、優先度の低い方の検証プロパティのチェックがキャンセルされ、優先度が高い検証プロパティのチェックが継続するということとなる。このように、実施の形態2によれば、設計者は、原因結果記述データ111に優先度を与えるだけで、優先度が高い条件が発生したら低い条件のチェックをキャンセルするという検証プロパティを、検証プロパティ言語のキャンセル文たとえばPSLのabort文により簡単かつ自動的に生成することができる。したがって、設計者による検証作業の効率化、検証期間の短縮化を図ることができる。実施の形態3つぎに、この発明の実施の形態3について説明する。実施の形態3は、実施の形態1において、逆命題の検証プロパティ112を生成する形態である。ここで、逆命題とは、レジスタ値が変化0→1または1→0したならば必ず変化する前もしくは変化と同じタイミングに書換え条件が発生していることをチェックすることである。<検証支援装置の機能的構成>まず、実施の形態3にかかる検証支援装置の機能的構成について説明する。図11は、実施の形態3にかかる検証支援装置の機能的構成を示すブロック図である。図11において、検証支援装置1100は、入力部501、テンプレート抽出部502、および検証プロパティ生成部503のほか、逆命題書換条件生成部1101と、を有する。逆命題書換条件生成部1101は、入力部501によって入力された原因結果記述データ111から書換条件を抽出し、逆命題の書換条件を生成する。具体的には、ある書換結果が発生するための一または複数の書換条件を抽出する。たとえば、IntRdy0iは次のサイクルで0へ書き換わりという書換結果があるとすると、当該結果が発生するための書換条件たとえば、C_RESET=1となったらなどを抽出する。そして、個々の書換条件によるキャンセル文をたとえばPSLのabort文を用いて表現することで、逆命題の書換条件を生成する。この場合、検証プロパティ生成部503では、逆命題の書換条件が与えられると、検証プロパティ言語の記述の否定文たとえばPSLのnever文を用いて、逆命題の書換結果を表現する。この逆命題の書換条件と逆命題の書換結果とを組み合わせることで、逆命題の検証プロパティ書換結果は発生することがない。ただし書換条件が発生する場合を除くを生成することができる。なお、上述した逆命題書換条件生成部1101は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置1100の検証支援処理手順>図12は、実施の形態3にかかる検証支援処理手順を示すフローチャートである。図12において、まず、入力部501により、原因結果記述データ111の入力を待ち受けるステップS1201:No。そして、原因結果記述データ111が入力された場合ステップS1201:Yes、未処理のレジスタがあるか否かを判断するステップS1202。未処理のレジスタがあった場合ステップS1202:Yes、テンプレート抽出部502により、その原因結果記述データ111に該当するテンプレート記述を抽出するステップS1203。つぎに、逆命題書換条件生成部1101により、入力された原因結果記述データ111から書換条件を抽出して、逆命題の書換条件を生成するステップS1204。そして、検証プロパティ生成部503により、逆命題の検証プロパティ112を生成しステップS1205、ステップS1202に戻る。なお、ステップS1202において、未処理のレジスタがないと判断された場合ステップS1202:No、一連の処理を終了する。生成された逆命題の検証プロパティは、検証装置102に与えられ、検証対象回路の論理検証が実行される。<具体例>図13は、実施の形態3にかかる逆命題の検証プロパティ112の自動生成例を示す説明図である。ここでは、レジスタのIntRdy0iが1から0へ書き換わったという結果を例にして説明する。0への書換条件がCN1~CN9とすると、レジスタのIntRdy0iが1から0へ書き換わったということは、書換条件CN1~CN9のうち少なくともいずれか一つが発生しているばずである。換言すれば、書換条件CN1~CN9なしでは、レジスタのIntRdy0iが1から0へ書き換わらないことと同じである。したがって、書換条件CN1~CN9によるキャンセル文をたとえばPSLのabort文を用いて表現し、また、レジスタのIntRdy0iが1から0へ書き換わったという記述の否定文をたとえばPSLのnever文を用いて表現する。この2つの表現を組み合わせることで、逆命題の検証プロパティ112を生成することができる。このように、実施の形態3によれば、設計者は、逆命題の検証プロパティを自動的に生成することができるため、検証プロパティ112の品質向上および検証精度の向上を図ることができる。したがって、設計者による検証作業の効率化、検証期間の短縮化を図ることができる。実施の形態4つぎに、実施の形態4について説明する。実施の形態4は、仕様書データ114を自動生成する形態である。仕様書データ114を自動生成することができれば、設計者の仕様書作成の負担を軽減することができる。また、設計者が作成した仕様書と比較して矛盾箇所を見つけることができる。<検証支援装置の機能的構成>まず、実施の形態4にかかる検証支援装置の機能的構成について説明する。図14は、実施の形態4にかかる検証支援装置の機能的構成を示すブロック図である。図14において、検証支援装置1400は、入力部1401と、データ抽出部1402と、仕様書データ生成部1403と、から構成されている。図14において、入力部1401は、図3に示した原因結果記述データ111の入力を受け付ける。データ抽出部1402は、原因結果記述データ111から、仕様書データ114の生成に必要なデータを抽出する。仕様書データ生成部1403は、データ抽出部1402によって抽出されたデータを用いて、仕様書データ114を生成する。なお、上述した入力部1401、データ抽出部1402、および仕様書データ生成部1403は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。図15は、生成された仕様書データ114の一例を示す説明図である。レジスタマップ1501は、レジスタ内のアドレスとレジスタ名とを関連付けたマップである。アドレスおよびレジスタ名は、原因結果記述データ111のレジスタ情報から抽出される。フィールドマップ1502は、ビット番号とフィールド名と初期値とからなるマップである。ビット番号は、原因結果記述データ111のフィールド情報内のレンジから抽出される。フィールド名は、原因結果記述データ111のフィールド情報内のフィールド名から抽出される。初期値は、原因結果記述データ111のフィールド情報内の初期値欄に印がある書換値から抽出される。また、レジスタ詳細説明表ビット詳細説明および変化条件1503は、値とその意味とを関連付けたデータである。値は原因結果記述データ111のフィールド情報内の書換値から抽出される。意味は値情報から抽出される。<検証支援装置1400の検証支援処理手順>図16は、実施の形態4にかかる検証支援処理手順を示すフローチャートである。図16において、まず、入力部1401により、原因結果記述データ111の入力を待ち受けるステップS1601:No。そして、原因結果記述データ111が入力された場合ステップS1601:Yes、データ抽出部1402により、原因結果記述データ111のレジスタ情報からアドレスおよびレジスタ名を抽出するステップS1602。そして、仕様書データ生成部1403により、レジスタマップ1501を生成するステップS1603。つぎに、生成されたレジスタマップ1501の中で未処理のレジスタがあるか否かを判断するステップS1604。未処理のレジスタがある場合ステップS1604:Yes、データ抽出部1402により、原因結果記述データ111からビット番号、フィールド名および初期値を抽出するステップS1605。そして、仕様書データ生成部1403により、フィールドマップ1502を生成するステップS1606。そして、ステップS1604に戻る。また、ステップS1604において、未処理のレジスタがない場合ステップS1604:No、データ抽出部1402により、値および意味を抽出するステップS1607。そして、仕様書データ生成部1403により、レジスタ詳細説明表1503を生成するステップS1608。これにより、一連の処理を終了する。この実施の形態4によれば、仕様書データ114レジスタマップ1501、フィールドマップ1502、レジスタ詳細説明表1503を自動生成することができるため、設計者の仕様書作成の負担を軽減することができる。また、設計者が作成した仕様書と比較して矛盾箇所を見つけることができる。これにより、設計者による検証作業の効率化、検証期間の短縮化を図ることができる。実施の形態5つぎに、実施の形態5について説明する。実施の形態5は、原因結果グラフを用いて原因結果記述データ111において不足な部分がないかどうかをチェックする形態である。原因結果グラフは、ノードとエッジにより、図3に示した原因結果記述データ111を図形化したデータである。ノードは原因と結果途中結果含むをあらわしている。各ノードの左側には、原因や結果途中結果含むをあらわす記述を付す。また、エッジはノードを連結することで、連結先のノードの原因と結果の因果関係をあらわしている。図17は、原因結果グラフを示す説明図である。図17に示した原因結果グラフ1700において、ノード1701~1703は、それぞれ状態Aである、Cをする、Dをするといった原因をあらわすノードである。以降、原因をあらわすノードを原因ノードと称す。リーフノードは原因ノードとなる。ノード1704は、原因ノード1701,1702の論理積ANDをあらわすノードである。ルートノードでもなくリーフノードでもないノードは途中結果ノードとなる。論理和ORノードも途中結果ノードとなりうる。ノード1705は、状態Bになるといった結果をあらわすノードである。以降、結果をあらわすノードを結果ノードと称す。ルートノードは結果ノードとなる。ノード1706は、ノード1701~1705からなる原因結果グラフ1700に連結されていないノードである。ノード1706は、状態Aになるといった結果をあらわす結果ノードであるが、その結果を発生させる原因レジスタ書換条件が存在しない。実施の形態5では、原因結果記述データ111から、このようなノード1706を検出することで、原因結果記述データ111に不足が生じているか否かをチェックする。このように、原因結果記述データ111の不足分をチェックするため、原因結果グラフに時間概念を導入する。時間の概念をあらわすため、原因結果グラフのエッジに時間的重みを加える。この重みは、原因結果グラフのエッジにサイクル数を付すことで表現する。また、結果ノードまたは途中結果ノードについて、結果が発生する時間にn~mサイクルといった範囲が生じる場合には、時間的なOR論理和結合ノード以下、tORと称することもある。を利用する。図18は、時間の概念を導入した原因結果グラフの一例を示す説明図である。この原因結果グラフ1800は、状態AのときにCをすると2~3サイクル後に状態Bになるということをあらわしている。また、原因結果記述データ111から原因結果グラフが生成された場合、原因結果グラフ間の整合性チェックのため、一つの原因結果グラフの原因ノードとこの原因ノードと一致する他の原因結果グラフの結果ノードとを連結する。図19は、2つの原因結果グラフの連結例を示す説明図である。図19において、原因結果グラフ1901は、図18に示した原因結果グラフ1800の原因ノードをまとめたグラフである。原因結果グラフ1901は、ノードNa,Nb,Nc,N1~N3からなるグラフである。ノードNa,Ncは原因ノード、ノードNbは結果ノードである。また、原因結果グラフ1902は、ノードNa,Ne,Nfからなるグラフである。ノードNeは原因ノードであり、ノードNa,Nfは結果ノードである。図19において、原因結果グラフ1901の原因ノードNaと原因結果グラフ1902の結果ノードNaとは同一であるため、原因ノードNaと結果ノードNaとを連結することで、あらたな原因結果グラフ1903を生成する。<検証支援装置の機能的構成>つぎに、実施の形態5にかかる検証支援装置の機能的構成について説明する。図20は、実施の形態5にかかる検証支援装置の機能的構成を示すブロック図である。図20において、検証支援装置2000は、入力部2001と、原因結果グラフ生成部2002と、ノード探索部2003と、連結部2004と、整合性検出部2005と、出力部2006とから構成されている。入力部2001は、図3に示した原因結果記述データ111の入力を受け付ける。原因結果グラフ生成部2002は、原因結果記述データ111に基づいて原因結果グラフを生成する。たとえば、状態変化前のレジスタの状態を原因ノードとし、状態変化後のレジスタの状態を結果ノードとし、エッジで連結する。また、テンプレート情報のパラメータNからサイクル数を読み出して、エッジの時間的な重みとする。ノード探索部2003は、一の原因結果グラフの原因ノードに一致する他の原因結果グラフの結果ノードを探索する。具体的には、図19に示したように、原因結果グラフ1901の原因ノードNaに一致する原因結果グラフ1902の結果ノードNaを探索する。また、連結部2004は、ノード探索部2003による探索結果に基づいて、原因結果グラフどうしを連結する。具体的には、図19に示したように、原因結果グラフ1901の原因ノードNaに一致する結果ノードが他の原因結果グラフ1902にある場合、原因結果グラフ1901の原因ノードNaと原因結果グラフ1902の結果ノードNaとを連結し、あらたな原因結果グラフ1903を生成する。整合性検出部2005は、連結部2004による連結終了後の原因結果グラフの中から、結果ノードのみからなる原因結果グラフを検出する。換言すれば、連結処理を繰り返した結果、原因結果グラフにおいてリーフノードが外部入力での処理のみで構成されているかどうかをチェックする。出力部2006は、整合性検出部2005によって検出された検出結果をレビュー情報115として出力する。なお、上述した入力部2001、原因結果グラフ生成部2002、ノード探索部2003、連結部2004、整合性検出部2005、および出力部2006は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置2000の検証支援処理手順>つぎに、実施の形態5にかかる検証支援装置2000の検証支援処理手順について説明する。図21は、実施の形態5にかかる検証支援装置2000の検証支援処理手順を示すフローチャートである。図21において、まず、入力部2001により、原因結果記述データ111の入力を待ち受けるステップS2100:No。そして、原因結果記述データ111が入力された場合ステップS2100:Yes、原因結果グラフ生成部2002により、原因結果グラフを生成するステップS2102。そして、ノード探索部2003により、生成された原因結果グラフの集合の中から、任意の原因結果グラフを抽出するステップS2103。抽出した原因結果グラフのすべての原因ノードを処理していない場合ステップS2104:No、その原因結果グラフの原因ノードに一致する結果ノードを他の原因結果グラフから探索されたか否かを判断するステップS2105。探索された場合ステップS2105:Yes、連結部2004により、原因結果グラフどうしを連結しステップS2106、ステップS2104に戻る。一方、探索されなかった場合ステップS2105:No、連結をおこなわずにステップS2104に戻る。すべての原因ノードが処理された場合ステップS2104:Yes、すべての原因結果グラフを処理したか否かを判断するステップS2107。処理していない場合ステップS2107:No、ステップS2103に戻る。一方、処理した場合ステップS2107:Yes、整合性検出部2005により整合性チェックをおこないステップS2108、その結果を出力部2006によりレビュー情報115として出力するステップS2109。これにより、一連の処理を終了する。この実施の形態5によれば、原因結果グラフを用いて原因結果記述データ111において不足な部分がないかどうかという整合性のチェックをおこなうことができる。したがって、設計者は、原因結果記述データ111を検証プロパティ112の生成に先立って確認することができ、不足部分がある場合には、原因結果記述データ111の見直しをおこなうことができる。この見直し後の原因結果記述データ111を上述した実施の形態1~4に適用することにより、高品質の検証プロパティ112や仕様書データ114を自動生成することができ、誤った検証プロパティ112や仕様書データ114の生成を未然に防止することができる。実施の形態6つぎに、実施の形態6について説明する。実施の形態6は、実施の形態5に示した原因結果グラフを用いて原因結果記述データ111に矛盾性があるかどうかをチェックする形態である。このチェックは、原因結果グラフ間において、同一タイミングのノードどうしの排他関係の有無によりおこなわれる。矛盾性の有無は、同一タイミングのノードの内容が排他関係にあるか否かによりチェックする。たとえば、同一タイミングで、一方のノードがレジスタのIntRdy0iが1から0へ書き換わったという結果をあらわし、他方のノードがレジスタのIntRdy0iが1から0へ書き換わったという結果をあらわしている場合、両者は矛盾することとなる。図22は、実施の形態6にかかる原因結果グラフの排他関係を示す説明図である。図22において、原因結果グラフ2200と原因結果グラフ2210は、上述した実施の形態5による連結処理前の状態を示している。そして、原因結果グラフ2200の原因ノード2201と原因結果グラフ2210の原因ノード2211との間に排他関係があるか否かをチェックする。矛盾性の有無を調べる場合、それに先立って、実施の形態5で示したように、原因結果グラフを連結し、エッジに時間距離をあらわす時間的重みを付す。そして、一つのノードから結果ノードまでの経路が複数存在し、かつ、結果ノードまでの時間距離が異なる場合には、当該のノードを展開する。また、混同を避けるため、展開されたノードにレベルを付す。図23は、連結処理された原因結果グラフの展開状態を示す説明図である。ここでは、図19に示した連結処理後の原因結果グラフ1903を展開する。結果ノードNbをノードNaまで辿る場合、2つの経路が特定される。1つは、Nb-N3-N1-Naという経路であり、その経路におけるノードNa~ノードNbまでの時間距離は、その経路中のエッジに付された時間的重みの合計値2となる。もう1つは、Nb-N3-N2-Naという経路であり、その経路におけるノードNa~ノードNbまでの時間距離は、その経路中のエッジに付された時間的重みの合計値3となる。このようにノードNaから結果ノードNbまでの経路が複数存在するため同数の時間距離が存在する。このような場合、ノードNaを経路ごとに展開する。この展開によりノードNaが2つ存在することとなるが、区別するためにラベルを付す。時間距離2の経路Nb-N3-N1-Naについては、ラベルt1と時間距離2を付し、時間距離3の経路Nb-N3-N2-Naについては、ラベルt2と時間距離3を付す。ノードNc,Neについても同様に展開する。なお、同一経路のノードには同一ラベルを付す。たとえば、ノードN1を含む経路Nb-N3-N1-Naのノードに対しては同一ラベルt1を付し、ノードN2を含む経路Nb-N3-N2-Naのノードに対しては同一ラベルt2を付す。このように、原因結果グラフ1903を展開すると、原因結果グラフ2300が得られる。以後、展開したノードが展開した数存在するため、ラベルと時間距離を用いて区別する。たとえば、ノードNaは2つ存在するため、一方のノードNaをノードNat1,2と標記し、他方のノードNaをノードNat2,3と標記する。つぎに、上述した展開処理による展開後の原因結果グラフの原因ノードに、他の結果ノードが関連付けられる場合には、当該他の結果ノードを追加する。展開後の原因結果グラフ1903は、もともと図19に示した原因結果グラフ1901と原因結果グラフ1902とが連結されたグラフであり、連結後の原因結果グラフ1903は、結果ノードNbのみを結果ノードとしていたため、原因結果グラフ1902の結果ノードNfは除外していたが、ここでは、その結果ノードNfを原因結果グラフ1903に追加する。図24は、追加処理後の原因結果グラフを示す説明図である。図24に示した原因結果グラフ2400は、図23に示した原因結果グラフ2300に、図19に示した結果ノードNfを追加したグラフである。また、追加される結果ノードNfに対する同一原因ノードNeが展開により複数ここでは2つ存在する。原因ノードNet1,3に対しては、結果ノードNfに対しても同一ラベルt1を付す。また、時間距離は、図19に示した連結前の原因結果グラフにおける原因ノードNeと結果ノードNf間のエッジの時間的重み分減算する。この場合、原因ノードNet1,3の時間距離は3であり、原因ノードNeと結果ノードNf間のエッジの時間的重みは1であるため、ノードNfの時間距離は2となる。原因ノードNet2,4に対しても、上記と同様にノードNfを追加して、結果ノードNft2,3とする。そして、同一ラベル、同一時間距離のノードの間に排他関係があるかどうかをチェックする。チェックされる排他関係は、ユーザーから指示されるものと、同じフィールドに異なる値書換えがあるといった関係のように自動抽出されるものとがある。図25は、矛盾性が存在する原因結果グラフを示す説明図である。たとえば、同一ラベル同一時間距離をもつノードNft1,2とノードNct1,2に排他関係があるかどうかをチェックする。同様に、ノードNft2,3とノードNct2,3についても排他関係があるかどうかをチェックする。ラベルが異なっていたり、時間距離が異なっている場合、排他関係が存在しても矛盾は生じない。図26は、矛盾性が生じない原因結果グラフを示す説明図である。図26において、ノードNft1,1とノードNct1,2とは、時間距離が異なっている。したがって、ノードNft1,1とノードNct1,2の内容が排他関係にあったとしても、時間がずれているため矛盾性はなく共存することとなる。ノードNft2,2とノードNct2,3についても同様である。<検証支援装置の機能的構成>つぎに、実施の形態6にかかる検証支援装置の機能的構成について説明する。図27は、実施の形態6にかかる検証支援装置の機能的構成を示すブロック図である。なお、実施の形態5に示した構成と同一構成には同一符号を付し、その説明を省略する。検証支援装置2700は、入力部2001、原因結果グラフ生成部2002、ノード探索部2003、連結部2004、整合性検出部2005、出力部2006のほか、連結済み原因結果グラフ群2701と、グラフ抽出部2702と、展開部2703と、追加部2704と、矛盾性検出部2705と、を備えている。連結済み原因結果グラフ群2701は、連結部2004によって連結された連結済み原因結果グラフの集合である。グラフ抽出部2702は、連結済み原因結果グラフ群2701から連結済み原因結果グラフを抽出する。展開部2703は、抽出された連結済み原因結果グラフについて、図23に示した展開処理をおこなう。追加部2704は、図24に示したように、展開処理された原因結果グラフに、連結部2004により除外された結果ノードを追加する。矛盾性検出部2705は、図25および図26に示したように、追加処理済みの原因結果グラフ内の同一ラベル、同一時間距離である二つ以上のノードの間に排他関係があるかどうかをチェックする。なお、出力部2006は、矛盾性検出部2705による検出結果をレビュー情報115として出力する。なお、上述したグラフ抽出部2702、展開部2703、追加部2704、および矛盾性検出部2705は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置2700の検証支援処理手順>つぎに、実施の形態6にかかる検証支援装置2700の検証支援処理手順について説明する。図28は、実施の形態6にかかる検証支援装置2700の検証支援処理手順を示すフローチャートである。まず、グラフ抽出部2702により、連結済み原因結果グラフを抽出するステップS2801。そして、展開部2703による展開処理をおこないステップS2802、追加部2704により追加可能な結果ノードがあれば追加するステップS2803。そして、矛盾性検出部2705により排他関係チェックをおこなうステップS2804。そして、未処理の連結済み原因結果グラフがある場合ステップS2805:Yes、ステップS2801に戻り、ない場合ステップS2805:No、出力部2006により、矛盾性チェック結果をレビュー情報115として出力するステップS2806。これにより、一連の処理を終了する。このように、実施の形態6によれば、原因結果グラフを用いて原因結果記述データ111において矛盾がないかどうかという整合性のチェックをおこなうことができる。したがって、設計者は、原因結果記述データ111を検証プロパティ112の生成に先立って確認することができ、矛盾がある場合には、原因結果記述データ111の見直しをおこなうことができる。この見直し後の原因結果記述データ111を上述した実施の形態1~4に適用することにより、高品質の検証プロパティ112や仕様書データ114を自動生成することができ、誤った検証プロパティ112や仕様書データ114の生成を未然に防止することができる。実施の形態7つぎに、実施の形態7について説明する。実施の形態7は、実施の形態5に示した原因結果グラフを用いて、原因結果グラフからなるべくいくつかの原因結果を連結するシナリオ113を選択する形態である。これにより、効率の良い検証シナリオ113を生成することができる。原因結果グラフは、原因ノードと結果ノードとが直接または他のノードを介して間接的に連結されることで、検証シナリオ113を構成する。図29は、原因結果グラフからの検証シナリオ113の選択例を示す説明図である。図29において、原因結果グラフ2900は、原因ノード2901と結果ノード2902とが連結されたグラフである。原因結果グラフ2900は、原因ノード2901のEをするという原因条件が発生した場合に状態Aになるという結果が生じるという検証シナリオS1をあらわしている。また、原因結果グラフ2910は、原因ノード2903~2905と、途中結果ノード2906と、結果ノード2907とが連結されたグラフである。原因結果グラフ2910は、原因ノード2903の状態Aであると、原因ノード2904のCをするとが発生した場合途中結果ノード2906のANDに相当、結果ノード2907の状態Bになるが少なくとも結果ノード2907はORノードであるため生じるという検証シナリオS2である。このように、原因結果グラフが異なれば、原因結果グラフごとに検証シナリオ113が得られるが、検証シナリオ113数が多いと煩雑である。したがって、原因結果グラフ2900の結果ノード2902と原因結果グラフ2910の原因ノード2903が一致することを利用して、実施の形態5で示した連結部2004により原因結果グラフ2900,2910を連結することで、検証シナリオS1と検証シナリオS2をまとめた検証シナリオS3を得ることができる。検証シナリオS3のみを用いて検証装置102により論理検証をおこなえば、検証シナリオS1,S2を用いた論理検証をおこなう必要はないため、論理検証回数の低減化を図ることができる。<検証支援装置の機能的構成>つぎに、実施の形態7にかかる検証支援装置の機能的構成について説明する。図30は、実施の形態7にかかる検証支援装置の機能的構成を示すブロック図である。なお、実施の形態5および実施の形態6に示した構成と同一構成には同一符号を付し、その説明を省略する。検証支援装置3000は、入力部2001、原因結果グラフ生成部2002、ノード探索部2003、連結部2004、整合性検出部2005、出力部2006、連結済み原因結果グラフ群2701、グラフ抽出部2702、展開部2703のほか、サブグラフ抽出部3001を備えている。サブグラフ抽出部3001は、展開部2703による展開済みの原因結果グラフからサブグラフを抽出する。具体的には、展開済みの原因結果グラフのORノードまたはtORノードを検出し、ORノード,tORノードについては、その手前のノード群を分離する。図31は、サブグラフの抽出例を示す説明図である。図31において、ノードN1はANDノードであるため、その手前のノード群ノードNet1,3,Nat1,2と、ノードNct1,2とは分離しない。ノードN2も同様である。一方、ノードN3はtORノードであるため、その手前の一方のノード群ノードNet1,3,Nat1,2,Nct1,2,N1と他方のノード群ノードNet2,4,Nat2,3,Nct2,3,N2とを分離して、サブグラフSG1とサブグラフSG2を抽出する。抽出されるサブグラフSG1,SG2は、AND結合を含みOR,tOR結合を含まないサブグラフとなる。これにより、サブグラフSG1ノードNet1,3,Nat1,2,Nct1,2,N1,N3,Nbによってあらわされる検証シナリオ113と、サブグラフSG2ノードNet2,4,Nat2,3,Nct2,3,N2,N3,Nbによってあらわされる検証シナリオ113とを得ることができる。なお、上述したサブグラフ抽出部3001は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置3000の検証支援処理手順>つぎに、実施の形態7にかかる検証支援装置3000の検証支援処理手順について説明する。図32は、実施の形態6にかかる検証支援装置3000の検証支援処理手順を示すフローチャートである。まず、グラフ抽出部2702により、連結済み原因結果グラフを抽出するステップS3201。そして、展開部2703による展開処理をおこなうステップS3202。そして、サブグラフ抽出部3001により、展開処理後の原因結果グラフからサブグラフを抽出するステップS3203。そして、未処理の連結済み原因結果グラフがある場合ステップS3204:Yes、ステップS3201に戻り、ない場合ステップS3204:No、出力部2006により、検証シナリオ113を出力するステップS3205。これにより、一連の処理を終了する。このように、実施の形態7によれば、原因結果グラフを用いて効率的な検証シナリオ113を自動生成することができる。したがって、検証期間の短縮化を図ることができる。実施の形態8つぎに、実施の形態8について説明する。実施の形態8は、レジスタ書き換え条件が発生しレジスタ値が指定値へセットされる条件のカバレッジを測定するプロパティを自動生成する形態である。書き換えがおこなわれたか否かをチェックするためには、最低限書き換え条件が1回でも発生していることが必要である。1回でも書き換え条件が発生し、かつ、エラーがなかった場合、書き換えは正常におこなわれたこととなる。すなわち、書き換え条件によるレジスタの書き換えにより検証済みであることを設計者に教えるために、論理検証に用いた検証プロパティ112についてカバレッジ情報を生成する。カバレッジ情報は、元の検証プロパティ112をたとえばPSLのcover文で表現することで生成される。これにより、どの検証プロパティ112が検証で十分チェックされたか否かを判別することができる。図33は、カバレッジ情報の生成例を示す説明図である。検証プロパティ3301は、C_RESET=1となったら次のサイクルで0へ書き換わりをあらわすプロパティである。検証装置102から検証済みの信号を受けたり、また設計者からの検証済みの操作入力を受けると、検証プロパティ3301からカバレッジ情報3302に変換される。カバレッジ情報3302は、検証プロパティ3301に関するcover文である。<検証支援装置の機能的構成>つぎに、実施の形態8にかかる検証支援装置の機能的構成について説明する。図34は、実施の形態8にかかる検証支援装置の機能的構成を示すブロック図である。なお、実施の形態1に示した構成と同一構成には同一符号を付し、その説明を省略する。検証支援装置3400は、検証プロパティ抽出部3401と、カバレッジ情報生成部3403と、から構成されている。検証プロパティ抽出部3401は、検証プロパティ群510から論理検証をおこなう検証プロパティ112を抽出する。なお、上述した検証プロパティ抽出部3401、およびカバレッジ情報生成部3403は、具体的には、たとえば、図2に示したROM202,RAM203,HD205などの記録媒体に記録されているプログラムを、CPU201に実行させることによって、またはI/F209によって、その機能を実現する。<検証支援装置3400の検証支援処理手順>つぎに、実施の形態8にかかる検証支援装置3400の検証支援処理手順について説明する。図35は、実施の形態8にかかる検証支援装置3400の検証支援処理手順を示すフローチャートである。まず、検証プロパティ抽出部3401により、論理検証に用いる検証プロパティ112を抽出するステップS3501。カバレッジ情報生成部3403により、その検証プロパティ112についてカバレッジ情報を生成しステップS3502、ステップS3503に移行する。ステップS3503では、未処理の検証プロパティ112があるか否かを判断し、未処理の検証プロパティ112がある場合ステップS3503:Yes、ステップS3501に戻る。一方、未処理の検証プロパティ112がない場合ステップS3503:No、一連の処理を終了する。このように、実施の形態8によれば、どの検証プロパティ112が論理検証で十分チェックされたか否かを判別することができるカバレッジ情報を生成することで、論理検証の重複実施のような無駄を防止して、検証期間の短縮化を図ることや、論理検証の不十分さを明確に示すことで、検証漏れを回避することを図ることができる。実施の形態9つぎに、実施の形態9について説明する。実施の形態9は、実施の形態1~4において、原因結果グラフにより定義された検証プロパティ112を波形表示し、意図した検証プロパティ112であるかを視覚的に確認する形態である。図36は、検証プロパティの波形表示例を示す説明図である。ここで、検証プロパティ3601は、C_RESETが立ち上がったら次のサイクルでIntRdy0iを0に書き換えるというプロパティである。符号3602は、検証プロパティ3601の波形表示である。波形表示3602では、サイクルC1でC_RESETの立ち上がりを検出し、次のサイクルC2でIntRdy0i=0を検出している。このように、実施の形態9によれば、検証プロパティ112を視覚的にわかりやすい形式で表示することができる。このように、上述した実施の形態によれば、検証項目のタイプを整理しパラメータを表化することで記述量を減少させ、かつ、計算機読み取り可能とすることでさまざまな検証プロパティ112を自動的に作成することができる。また、検証プロパティ作成だけでなく仕様書および矛盾チェックなどの支援もおこなうことで設計TATの低減化を図ることもできる。さらに、検証プロパティ112を自動生成することで、PSLなどの検証プロパティ言語に精通していない設計者にも容易にアサーションベース検証を行うことができる。以上説明したように、検証支援装置、検証支援方法、検証支援プログラム、および記録媒体によれば、検証期間の短縮化と設計者の作業労力の軽減化を図ることができるという効果を奏する。なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナルコンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、CD-ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な伝送媒体であってもよい。付記1検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付ける入力手段と、検証プロパティに関するテンプレート群の中から、前記入力手段によって入力されたテンプレート特定情報により特定されるテンプレートを抽出するテンプレート抽出手段と、前記テンプレート抽出手段によって抽出されたテンプレートと、前記入力手段によって入力された原因に関する記述および結果に関する記述とに基づいて、前記原因から前記結果までの前記レジスタの状態変化をあらわす検証プロパティを生成する検証プロパティ生成手段と、を備えることを特徴とする検証支援装置。付記2前記検証プロパティ生成手段によって生成された検証プロパティ群の中から前記結果に関する記述が競合しあう検証プロパティを抽出する検証プロパティ抽出手段と、前記検証プロパティ抽出手段によって抽出された検証プロパティのうち優先度が高い方の検証プロパティの原因に関する記述を抽出する原因記述抽出手段と、を備え、前記生成手段は、前記優先度が低い方の検証プロパティに、前記原因記述抽出手段によって抽出された原因に関する記述の内容を優先処理する記述を追加することにより、あらたな検証プロパティを生成することを特徴とする付記1に記載の検証支援装置。付記3検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付ける入力手段と、検証プロパティに関するテンプレート群の中から、前記入力手段によって入力されたテンプレート特定情報により特定されるテンプレートを抽出するテンプレート抽出手段と、前記入力手段によって入力されたレジスタの状態変化の原因に関する記述に基づいて、逆命題の原因に関する記述を生成する逆命題原因記述生成手段と、前記テンプレート抽出手段によって抽出されたテンプレートと、前記逆命題原因記述生成手段によって生成された記述とに基づいて、前記原因が発生しなければ前記結果が発生しないことを意味する逆命題の検証プロパティを生成する検証プロパティ生成手段と、を備えることを特徴とする検証支援装置。付記4表示画面を有する表示手段と、前記表示画面を制御して、前記検証プロパティに関する波形情報を表示する表示制御手段と、を備えることを特徴とする付記1~3のいずれか一つに記載の検証支援装置。付記5検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とを含む記述データの入力を受け付ける入力手段と、前記入力手段によって入力された原因に関する記述および結果に関する記述の中から、レジスタのアドレスおよび動作に関するデータを抽出するデータ抽出手段と、前記データ抽出手段によって抽出されたデータに基づいて、前記検証対象回路の仕様書データを生成する仕様書生成手段と、を備えることを特徴とする検証支援装置。付記6検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付ける入力手段と、前記入力手段によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成する原因結果グラフ生成手段と、前記原因結果グラフ生成手段によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索する探索手段と、前記探索手段によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成する連結手段と、前記連結手段によって生成された原因結果グラフと、前記連結手段によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出する整合性検出手段と、前記整合性検出手段によって検出された検出結果を出力する出力手段と、を備えることを特徴とする検証支援装置。付記7前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに前記他の原因結果グラフの結果ノードを追加する追加手段と、前記追加手段によって追加された結果ノードを含む前記連結済み原因結果グラフを構成するノードのうち、同一時間距離のノード間において排他関係があるか否かを判定することで前記原因結果記述データの矛盾性を検出する矛盾性検出手段と、を備え、前記出力手段は、前記矛盾性検出手段によって検出された検出結果を出力することを特徴とする付記6に記載の検証支援装置。付記8前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに含まれる論理和ノードに基づいて、前記連結済み原因結果グラフからサブグラフを抽出するサブグラフ抽出手段を備え、前記出力手段は、前記サブグラフ抽出手段によって抽出されたサブグラフを検証シナリオとして出力することを特徴とする付記6に記載の検証支援装置。付記9検証対象回路に関する検証プロパティ群の中から任意の検証プロパティを抽出する検証プロパティ抽出手段と、前記検証プロパティ抽出手段によって抽出された検証プロパティを用いて前記検証対象回路の論理検証が十分におこなわれたことを示すカバレッジ情報を生成するカバレッジ情報生成手段と、を備えることを特徴とする検証支援装置。付記10検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付ける入力工程と、検証プロパティに関するテンプレート群の中から、前記入力工程によって入力されたテンプレート特定情報により特定されるテンプレートを抽出するテンプレート抽出工程と、前記テンプレート抽出工程によって抽出されたテンプレートと、前記入力工程によって入力された原因に関する記述および結果に関する記述とに基づいて、前記原因から前記結果までの前記レジスタの状態変化をあらわす検証プロパティを生成する検証プロパティ生成工程と、を含んだことを特徴とする検証支援方法。付記11検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付ける入力工程と、検証プロパティに関するテンプレート群の中から、前記入力工程によって入力されたテンプレート特定情報により特定されるテンプレートを抽出するテンプレート抽出工程と、前記入力工程によって入力されたレジスタの状態変化の原因に関する記述に基づいて、逆命題の原因に関する記述を生成する逆命題原因記述生成工程と、前記テンプレート抽出工程によって抽出されたテンプレートと、前記逆命題原因記述生成工程によって生成された記述とに基づいて、前記原因が発生しなければ前記結果が発生しないことを意味する逆命題の検証プロパティを生成する検証プロパティ生成工程と、を含んだことを特徴とする検証支援方法。付記12検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とを含む記述データの入力を受け付ける入力工程と、前記入力工程によって入力された原因に関する記述および結果に関する記述の中から、レジスタのアドレスおよび動作に関するデータを抽出するデータ抽出工程と、前記データ抽出工程によって抽出されたデータに基づいて、前記検証対象回路の仕様書データを生成する仕様書生成工程と、を含んだことを特徴とする検証支援方法。付記13検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付ける入力工程と、前記入力工程によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成する原因結果グラフ生成工程と、前記原因結果グラフ生成工程によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索する探索工程と、前記探索工程によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成する連結工程と、前記連結工程によって生成された原因結果グラフと、前記連結工程によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出する整合性検出工程と、前記整合性検出工程によって検出された検出結果を出力する出力工程と、を含んだことを特徴とする検証支援方法。付記14前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに前記他の原因結果グラフの結果ノードを追加する追加工程と、前記追加工程によって追加された結果ノードを含む前記連結済み原因結果グラフを構成するノードのうち、同一時間距離のノード間において排他関係があるか否かを判定することで前記原因結果記述データの矛盾性を検出する矛盾性検出工程と、を含み、前記出力工程は、前記矛盾性検出工程によって検出された検出結果を出力することを特徴とする付記13に記載の検証支援方法。付記15前記連結工程によって生成された原因結果グラフ以下、連結済み原因結果グラフというに含まれる論理和ノードに基づいて、前記連結済み原因結果グラフからサブグラフを抽出するサブグラフ抽出工程を含み、前記出力工程は、前記サブグラフ抽出工程によって抽出されたサブグラフを検証シナリオとして出力することを特徴とする付記13に記載の検証支援方法。付記16検証対象回路に関する検証プロパティ群の中から任意の検証プロパティを抽出する検証プロパティ抽出工程と、前記検証プロパティ抽出工程によって抽出された検証プロパティを用いて前記検証対象回路の論理検証が十分におこなわれたことを示すカバレッジ情報を生成するカバレッジ情報生成工程と、を含んだことを特徴とする検証支援方法。付記17検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付けさせる入力工程と、検証プロパティに関するテンプレート群の中から、前記入力工程によって入力されたテンプレート特定情報により特定されるテンプレートを抽出させるテンプレート抽出工程と、前記テンプレート抽出工程によって抽出されたテンプレートと、前記入力工程によって入力された原因に関する記述および結果に関する記述とに基づいて、前記原因から前記結果までの前記レジスタの状態変化をあらわす検証プロパティを生成させる検証プロパティ生成工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記18検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とテンプレート特定情報とを含む記述データの入力を受け付けさせる入力工程と、検証プロパティに関するテンプレート群の中から、前記入力工程によって入力されたテンプレート特定情報により特定されるテンプレートを抽出させるテンプレート抽出工程と、前記入力工程によって入力されたレジスタの状態変化の原因に関する記述に基づいて、逆命題の原因に関する記述を生成させる逆命題原因記述生成工程と、前記テンプレート抽出工程によって抽出されたテンプレートと、前記逆命題原因記述生成工程によって生成された記述とに基づいて、前記原因が発生しなければ前記結果が発生しないことを意味する逆命題の検証プロパティを生成させる検証プロパティ生成工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記19検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述とを含む記述データの入力を受け付けさせる入力工程と、前記入力工程によって入力された原因に関する記述および結果に関する記述の中から、レジスタのアドレスおよび動作に関するデータを抽出させるデータ抽出工程と、前記データ抽出工程によって抽出されたデータに基づいて、前記検証対象回路の仕様書データを生成させる仕様書生成工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記20検証対象回路を構成するレジスタの状態変化の原因に関する記述と前記状態変化の結果に関する記述と前記原因から前記結果までの時間距離とを含む記述データの入力を受け付けさせる入力工程と、前記入力工程によって入力された記述データに基づいて、前記原因と前記結果との関係をノードとエッジと前記時間距離によりあらわす原因結果グラフを生成させる原因結果グラフ生成工程と、前記原因結果グラフ生成工程によって生成された原因結果グラフ群の中から、一の原因結果グラフの原因に関するノード以下、原因ノードというと同一内容の結果に関するノード以下、結果ノードというを、前記一の原因結果グラフ以外の他の原因結果グラフから探索させる探索工程と、前記探索工程によって探索された探索結果に基づいて、前記一の原因結果グラフの原因ノードと前記他の原因結果グラフの結果ノードとを連結することにより、あらたな原因結果グラフを生成させる連結工程と、前記連結工程によって生成された原因結果グラフと、前記連結工程によって連結されなかった残余の原因結果グラフとに基づいて、前記記述データの整合性を検出させる整合性検出工程と、前記整合性検出工程によって検出された検出結果を出力させる出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記21前記連結手段によって生成された原因結果グラフ以下、連結済み原因結果グラフというに前記他の原因結果グラフの結果ノードを追加させる追加工程と、前記追加工程によって追加された結果ノードを含む前記連結済み原因結果グラフを構成するノードのうち、同一時間距離のノード間において排他関係があるか否かを判定することで前記原因結果記述データの矛盾性を検出させる矛盾性検出工程と、を前記コンピュータに実行させ、前記出力工程は、前記矛盾性検出工程によって検出された検出結果を出力させることを特徴とする付記20に記載の検証支援プログラム。付記22前記連結工程によって生成された原因結果グラフ以下、連結済み原因結果グラフというに含まれる論理和ノードに基づいて、前記連結済み原因結果グラフからサブグラフを抽出させるサブグラフ抽出工程を、前記コンピュータに実行させ、前記出力工程は、前記サブグラフ抽出工程によって抽出されたサブグラフを検証シナリオとして出力させることを特徴とする付記20に記載の検証支援プログラム。付記23検証対象回路に関する検証プロパティ群の中から任意の検証プロパティを抽出させる検証プロパティ抽出工程と、前記検証プロパティ抽出工程によって抽出された検証プロパティを用いて前記検証対象回路の論理検証が十分におこなわれたことを示すカバレッジ情報を生成させるカバレッジ情報生成工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記24付記17~23のいずれか一つに記載の検証支援プログラムを記録した前記コンピュータに読み取り可能な記録媒体。"