(57)【要約】【課題】検証対象レジスタに対する検証精度を向上させる。【解決手段】検証対象回路１００の構成から検証対象となる検証対象レジスタを特定し（ステップＳ１０１）、特定された検証対象レジスタについて、カバレッジ基準となる検証を要するパターンを抽出する（ステップＳ１０２）。このステップＳ１０２では、ＤＩＲＷマトリックスとは、検証対象回路１００に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移をあらわしたＤＲＩＷマトリックスを用意し、このＤＩＲＷマトリックスを利用して、マトリックスカバレッジ基準１１０と、実装カバレッジ基準１２０との２種類のカバレッジ基準を決定する。【選択図】図１
2010003281.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得手段、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得手段によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出手段、
前記ＤＦＧ抽出手段によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出手段、
前記パス抽出手段によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定手段、
前記特定手段によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別手段、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段、
として機能させることを特徴とする検証支援プログラム。
【請求項２】
前記コンピュータを、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別された状態遷移を実現するための条件を抽出する条件抽出手段として機能させ、
前記決定手段は、前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移と、当該状態遷移について前記条件抽出手段によって抽出された条件とを前記カバレッジ基準に決定することを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
コンピュータを、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＤＩＲＷマトリックスに含まれるすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段、
として機能させることを特徴とする検証支援プログラム。
【請求項４】
前記コンピュータを、
前記検証対象回路に対する検証内容をあらわす検証シナリオと、前記検証対象回路の実装情報と、前記検証対象回路の仕様書に含まれるレジスタの属性をあらわすレジスタリストとを取得する取得手段、
前記取得手段によって取得された検証シナリオと実装情報とレジスタリストとから、前記ＣＤＦＧを生成するＣＤＦＧ生成手段、として機能させ、
前記ＤＦＧ抽出手段は、前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ生成手段によって生成されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出することを特徴とする請求項１または２に記載の検証支援プログラム。
【請求項５】
前記ＣＤＦＧ生成手段は、前記取得手段によって取得された検証シナリオと実装情報とレジスタリストとから、前記検証シナリオを複数回連続して実行させる場合の前記ＣＦＧ内のデータの流れが記述されたＣＤＦＧを生成することを特徴とする請求項４に記載の検証支援プログラム。
【請求項６】
前記ＣＤＦＧ生成手段は、前記取得手段が、前記検証対象回路に対する検証内容をあらわす複数の検証シナリオを取得した場合、当該複数の検証シナリオを連続して実行させる場合の前記ＣＦＧ内のデータの流れが記述されたＣＤＦＧを生成することを特徴とする請求項４に記載の検証支援プログラム。
【請求項７】
前記コンピュータを、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別された状態遷移について当該状態遷移に応じたパスの妥当性に関する情報を用いたシミュレーションが実行された場合、前記決定手段によって決定されたカバレッジ基準を分母とし、前記実行されたシミュレーションの数を分子とした算出結果を検証カバレッジとして出力する算出手段として機能させることを特徴とする請求項１〜６のいずれか一つに記載の検証支援プログラム。
【請求項８】
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段と、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得手段と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得手段によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出手段と、
前記ＤＦＧ抽出手段によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出手段と、
前記パス抽出手段によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定手段と、
前記特定手段によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別手段と、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段と、
を備えることを特徴とする検証支援装置。
【請求項９】
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスが記録されたメモリにアクセス可能なコンピュータによる検証支援方法であって、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得工程と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得手段によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出工程と、
前記ＤＦＧ抽出工程によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出工程と、
前記パス抽出工程によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定工程と、
前記特定工程によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別工程と、
前記判別工程によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定工程と、
を含むことを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
ハードウェア設計された検証支援回路に含まれるレジスタに対する検証処理を支援する分野に関する。
【背景技術】
【０００２】
従来、所望の機能を実現するためハードウェア（回路）を設計した場合には、実際のハードウェア製造に移行する前段階の処理として設計内容に漏れがないかの論理検証をおこなう作業が必須となる。具体的には、ハードウェアの設計内容に沿った検証シナリオを生成し、この検証シナリオを入力した場合の出力結果を用いて論理検証がおこなわれていた。
【０００３】
また、上述のようにして生成した検証シナリオによる検証処理を客観的に評価するために、検証カバレッジが求められる。検証カバレッジは、検証対象に対するシミュレーションのパターンが十分であるか否かの指標をあらわす情報である。具体的には、たとえば、検証を要するすべてのシミュレーションのパターンを母集団とした場合に、実行したシミュレーションのパターン数の割合によって求めた網羅率が検証カバレッジとして提供される。この場合、検証カバレッジ（網羅率）が高ければ検証精度も高いと判断される。
【０００４】
ここで問題になるのが、母集団となる“検証を要するシミュレーションの全パターン”の抽出の手法である。この母集団に相当するシミュレーションの全パターンをカバレッジ基準という。そして、このカバレッジ基準として、実質的に検証に役に立たないパターンを抽出してしまうと、たとえシミュレーションの網羅率が高くても実際の検証効率の向上にはつながらない場合がある。
【０００５】
そこで、現在は特定の基準に沿って、網羅的にパターンを抽出するパスカバレッジやコードカバレッジという手法が利用されている。パスカバレッジは、検証対象回路に含まれるレジスタにおいて状態遷移を生じるすべてのパスを検証するためのパターンとする。したがって、パスカバレッジでは、これらのパターンの集合がカバレッジ基準となる。また、コードカバレッジは、ラインカバレッジとも呼ばれ、検証対象回路に相当するソースコードの記述されたレジスタの入出力に関するパスを検証するためのパターンとする。コードカバレッジの場合も、これらのパターンの集合がカバレッジ基準となる。
【０００６】
【特許文献１】特開２００６−１９０２０９号公報
【特許文献２】特開２００６−２０１９８０号公報
【非特許文献１】Ｈａｒｒｙ．Ｄ．Ｆｏｓｔｅｒ，他２名「Ａｓｓｅｒｔｉｏｎ−Ｂａｓｅｄ  Ｄｅｓｉｇｎ」（２ｎｄ  Ｅｄｉｔｉｏｎ），「Ｐｒｏｇｒａｍｍｉｎｇ  Ｃｏｄｅ  ｍｅｔｒｉｃｓ」，ｐｐ．１２９−１３０
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、上述したような従来のカバレッジ基準には、非効率な点が多く、検証効率を向上させるための判断基準に役立てるには困難な面があった。具体的には、パスカバレッジの場合、抽出されるパターンは、検証対象回路に含まれるレジスタへ入力される可能性のあるすべてのパラメータ値を網羅したものとなる。したがって、レジスタの数や種類によっては、無限大に近い数のパターンが生じてしまう。結果として、検証カバレッジを算出する際の分母の値が大きく、処理時間が膨大になってしまうという問題があった。
【０００８】
また、コードカバレッジの場合、複数の条件分岐をもつ回路を検証対象回路とした際に、検証を要するパスが抜けてしまうことがあった。結果として不十分なパターンが提供されてしまうため、検証カバレッジとして信頼性の低いものとなり、検証精度が低下してしまうという問題があった。
【０００９】
上述した従来技術による問題点を解消するため、検証対象レジスタに対する検証精度を向上させる検証支援プログラム、検証支援装置および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【００１０】
ここで開示する技術は、検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する処理と、前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）を取得する処理と、前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出する処理と、抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出する処理と、抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する処理と、特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する処理と、前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定する処理と、を含んでいる。
【００１１】
また、ここで開示する技術は、検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する処理と、前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＤＩＲＷマトリックスに含まれるすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定する処理と、を含んでいる。
【発明の効果】
【００１２】
これらの開示した技術によれば、検証対象レジスタに対する検証精度を向上させることができるという効果を奏する。
【発明を実施するための最良の形態】
【００１３】
以下に添付図面を参照して、この検証支援プログラム、検証支援装置および検証支援方法の好適な実施の形態を詳細に説明する。この検証支援プログラム、検証支援装置および検証支援方法では、検証対象回路に含まれるレジスタにおいて生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを利用して効率的な検証を実現するためのカバレッジ基準を決定し、検証精度の高い検証カバレッジを提供することによって検証を支援する。
【００１４】
（検証支援処理の概要）
まず、本実施の形態にかかる検証支援処理の概要について説明する。図１は、本実施の形態にかかる検証支援処理の概要を示す説明図である。図１のように、ハードウェアの検証をおこなう場合には、検証対象となる回路（ここでは、検証対象回路１００）の構成か
ら検証対象となるレジスタ（以下、「検証対象レジスタ」という）を特定する（ステップＳ１０１）。
【００１５】
ここで、検証対象回路１００に含まれるレジスタの種類について説明する。レジスタの種類は、下記の３つに大別される。本実施の形態では、これら３つに分類されたどのレジスタであっても検証対象レジスタに特定することが可能である。
【００１６】
１．検証対象回路の外部からアクセス可能なＩ／Ｏレジスタ
例）検証対象回路１００のｒ１，ｒ２
２．仕様書の記載されている内部レジスタ
例）検証対象回路１００のＬ，ｔ
３．実装依存で有無が決まる仕様書に記載されていない実装依存レジスタ
例）検証対象回路１００の？
【００１７】
ステップＳ１０１において、検証対象レジスタが特定されると、特定された検証対象レジスタについて、カバレッジ基準となる検証を要するパターンの母集団を決定する（ステップＳ１０２）。カバレッジ基準とは、検証カバレッジ（検証の網羅率）を求める際の網羅性を評価する基準とである。したがって、本実施の形態の場合、カバレッジ基準とは、検証対象回路１００における検証を要するシミュレーションの全パターンである。また、本実施の形態の場合、ステップＳ１０２の処理によってマトリックスカバレッジ基準１１０と、実装カバレッジ基準１２０との２種類のカバレッジ基準が決定される。
【００１８】
（ＤＩＲＷマトリックス）
本実施の形態では、上述したように、あらたにＤＩＲＷマトリックスを用意し、この、このＤＲＩＷマトリックスを利用することによって、図１にて説明したようなカバレッジ基準（１１０，１２０）を生成する。ＤＩＲＷマトリックスとは、検証対象回路１００に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたデータ群である。ここでは、まず、ＤＲＩＷマトリックスについて説明する。図２−１は、ＤＩＲＷマトリックスの状態遷移図（内部レジスタ検証）である。また、図２−２は、ＤＩＲＷマトリックスを示す真理値表（内部レジスタ検証）である。
【００１９】
本実施の形態で利用するＤＩＲＷマトリックスとは、検証対象回路１００に含まれるレジスタの状態遷移に応じたパスの状況をあらわした情報である。図２−１の状態遷移図は、検証対象となるレジスタにおいて実際に起こる可能性のある下記の４つの状態の遷移例をあらわしている。
【００２０】
・Ｄｅｃｌａｒｅ（定義）
・Ｉｎｉｔｉａｌｉｚｅ（初期化）
・Ｒｅａｄ（読み出し）
・Ｗｒｉｔｅ（書き込み）
【００２１】
なお、図２−１の状態遷移図において、実線によって矢印が示されている遷移（たとえば、Ｗｒｉｔｅ→Ｒｅａｄなど）は、正しいパスを意味している。また、破線によって矢印が示されている遷移（たとえば、Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅなど）は、設計意図の確認を要するパスを意味している。また、矢印が示されていない遷移（たとえば、Ｄｅｃｌａｒｅ→Ｒｅａｄなど）は、バグとなるパスを意味している。なお、ここで説明するＤＩＲＷマトリックスの場合、Ｄｅｃｌａｒｅへの遷移は起こらないため、Ｄｅｃｌａｒｅへの遷移をあらわす矢印は存在しない。
【００２２】
そして、図２−１の状態遷移を図表化したものが図２−２の真理値表である。図２−２では、遷移前（ｂｅｆｏｒｅ）から遷移後（ａｆｔｅｒ）のパスに対して、それぞれ妥当性に関する情報を３種類に分けて設定している。具体的には、正しいパスをあらわす「○」、設計意図の確認を要するパスをあらわす「△」、バグとなるパスをあらわす「×」となっている。
【００２３】
（カバレッジ基準）
つぎに、上述したＤＩＲＷマトリックスを利用して生成されるマトリックスカバレッジ基準１１０と、実装カバレッジ基準１２０との２種類のカバレッジ基準について説明する。
【００２４】
・マトリックスカバレッジ基準
まず、マトリックスカバレッジ基準について説明する。図３は、マトリックスカバレッジ基準を示す説明図である。マトリックスカバレッジ基準の場合、図３に示した真理値表の斜線部分が対象となる。すなわち、マトリックスカバレッジ基準では、ＤＩＲＷマトリックスに設定されたすべての状態遷移を実現するシミュレーションのパターンがカバレッジ基準を構成する母集団となる。
【００２５】
したがって、図３の真理値表では１２通りの状態遷移があるため、検証カバレッジを求める際の分母も１２となる。そして、これら１２通りのシミュレーションのパターンのうち実行されたパターン数が分子となって求められた網羅率が検証カバレッジとして提供される。
【００２６】
・実装カバレッジ基準
つぎに、実装カバレッジ基準について説明する。図４は、実装カバレッジ基準を示す説明図である。図４の真理値表には、検証対象回路１００におけるレジスタの実装例が記されている。そして、実装カバレッジ基準の場合、図４に示した真理値表の実装有をあらわす斜線部分が対象となる。すなわち、ＤＩＲＷマトリックスに設定された状態遷移の中の、さらに、実装されているレジスタによって生じる状態遷移を実現するシミュレーションのパターンがカバレッジ基準の母集団となる。
【００２７】
したがって、図４の真理値表では４通りの状態遷移があるため、検証カバレッジを求める際の分母も４となる。そして、これら４通りのシミュレーションのパターンのうち実行されたパターン数が分子となって求められた網羅率が検証カバレッジとして提供される。
【００２８】
このように、本実施の形態では、ＤＩＲＷマトリックスを利用してマトリックスカバレッジ基準１１０と、実装カバレッジ基準１２０の２種類のカバレッジ基準が決定される。これら決定されたカバレッジ基準は、特定のレジスタに着目して遷移状態が抽出されたため、従来のパスカバレッジのように検証を要するパターン数が膨大になるような事態を防ぐことができる。また、従来のコードカバレッジのように必要なパスが抜けてしまうような事態を防ぐことができる。
【００２９】
また、検証対象回路１００に含まれる他のレジスタについてのカバレッジ基準を求めたい場合には、他のレジスタをあらたに検証対象レジスタに特定して、同様の処理をおこなえばよい。このように、検証を要するレジスタに対してのみカバレッジ基準を決定するため、不必要なパターンのシミュレーションを排除することができる。
【００３０】
以下の説明では、検証支援装置によって、上述したような、ＤＩＲＷマトリックスを利用したカバレッジ基準の決定を実現するための具体的な構成および処理内容について説明
する。
【００３１】
（検証支援装置のハードウェア構成）
図５は、検証支援装置のハードウェア構成を示すブロック図である。図５において、検証支援装置５００は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）５０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）５０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）５０３と、磁気ディスクドライブ５０４と、磁気ディスク５０５と、光ディスクドライブ５０６と、光ディスク５０７と、通信Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）５０８と、入力デバイス５０９と、出力デバイス５１０と、を備えている。また、各構成部はバス５５０によってそれぞれ接続されている。
【００３２】
ここで、ＣＰＵ５０１は、検証支援装置５００の全体の制御を司る。ＲＯＭ５０２は、ブートプログラムや、検証支援プログラムなどの各種プログラムを記憶している。ＲＡＭ５０３は、ＣＰＵ５０１のワークエリアとして使用される。磁気ディスクドライブ５０４は、ＣＰＵ５０１の制御にしたがって磁気ディスク５０５に対するデータのリード／ライトを制御する。磁気ディスク５０５は、磁気ディスクドライブ５０４の制御で書き込まれたデータを記憶する。なお、ＲＯＭ５０２には、検証支援プログラムによって生成された検証シナリオによる検証シミュレーションを実行する検証プログラムが記録されていてもよい。このような場合は、検証支援装置５００によって検証シナリオに留まらず、実際の検証結果まで提供することができる。
【００３３】
光ディスクドライブ５０６は、ＣＰＵ５０１の制御にしたがって光ディスク５０７に対するデータのリード／ライトを制御する。光ディスク５０７は、光ディスクドライブ５０６の制御で書き込まれたデータを記憶したり、光ディスク５０７に記憶されたデータをコンピュータに読み取らせたりする。
【００３４】
通信インターフェース（以下、「Ｉ／Ｆ」と略する）５０８は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク５１１に接続され、このネットワーク５１１を介して他の装置に接続される。そして、通信Ｉ／Ｆ５０８は、ネットワーク５１１と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。通信Ｉ／Ｆ５０８には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００３５】
入力デバイス５０９は、検証支援装置５００に対しての外部からの入力を受け付ける。入力デバイス５０９としては、具体的には、キーボード、マウスなどが挙げられる。
【００３６】
キーボードの場合、たとえば、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウスの場合、たとえば、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。また、ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００３７】
出力デバイス５１０は、検証支援装置５００によって生成された検証シナリオや、検証シナリオによる検証結果などを出力する。出力デバイス５１０としては、具体的には、ディスプレイ、プリンタなどが挙げられる。
【００３８】
ディスプレイの場合、たとえば、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイとしてさらに、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。また、プリンタの場合、たとえば、画像データや文書データを印刷する。さらに、レーザプリ
ンタやインクジェットプリンタを採用することができる。
【００３９】
（検証支援装置の機能的構成）
つぎに、検証支援装置５００の機能的構成について説明する。図６−１は、検証支援装置の機能的構成を示すブロック図である。検証支援装置５００は、記録部６０１と、取得部６０２と、ＣＤＦＧ生成部６０３と、ＤＦＧ抽出部６０４と、パス抽出部６０５と、特定部６０６と、判別部６０７と、決定部６０８と、算出部６０９と、を含む構成である。この制御部となる機能（取得部６０２〜算出部６０９）は、具体的には、たとえば、図５に示したＲＯＭ５０２、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶された検証支援プログラムをＣＰＵ５０１に実行させることにより、または、通信Ｉ／Ｆ５０８により、その機能を実現する。
【００４０】
記録部６０１は、検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する機能部である。ＤＩＲＷマトリックスにおけるパスの妥当性に関する情報は、検証対象回路１００の設計意図が反映されている。この記録部６０１は、たとえば、磁気ディスク５０５や光ディスク５０７などによって実現される。
【００４１】
取得部６０２は、検証支援装置５００によって効率的なカバレッジ基準を抽出するために必要な入力データを取得する機能部である。具体的に取得部６０２では、検証対象回路１００に対する検証内容をあらわす検証シナリオと、検証対象回路１００の実装情報と、検証対象回路１００の仕様書に含まれるレジスタの属性をあらわすレジスタリストとを取得する。なお、取得されたデータは、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４２】
なお、取得部６０２によって取得するデータのうち、レジスタリストの取得は任意となる。レジスタリストを取得しなかった場合には、同じく取得部６０２によって取得された検証対象回路１００の実装情報から検証対象回路１００に含まれるレジスタを抽出してレジスタリストを生成するリスト生成部（不図示）を用意してもよい。ここでも、生成されたレジスタリストは、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４３】
ＣＤＦＧ生成部６０３は、取得部６０２によって取得された実装情報とレジスタリストとから、検証対象回路１００の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）を生成する機能部である。なお、生成されたＣＤＦＧは、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４４】
ＤＦＧ抽出部６０４は、ＣＤＦＧ生成部６０３によって生成されたＣＤＦＧから、検証対象回路１００に含まれたレジスタのうち検証対象レジスタとして指定されたレジスタが記述されたＤＦＧを抽出する機能部である。なお、抽出されたＤＦＧの情報は、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４５】
パス抽出部６０５は、ＤＦＧ抽出部６０４によって抽出されたＤＦＧの中から内部レジスタに関するデータの流れをあらわすパスを抽出する機能部である。なお、抽出されたパスの情報は、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４６】
特定部６０６は、パス抽出部６０５によって抽出されたパスに含まれる検証対象レジスタの状態遷移をＤＦＧに基づいて特定する機能部である。パスに含まれる検証対象レジスタの状態遷移とは、ＤＩＲＷマトリックスについて説明で述べたように、Ｄｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の前状態と後状態との変化である。具体的には、ＤｅｃｌａｒｅからＲｅａｄへの遷移、ＩｎｉｔｉａｌｉｚｅからＷｒｉｔｅへの遷移などがあり、ＤＦＧの記述から判断することができる。なお、特定結果は、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４７】
判別部６０７は、特定部６０６によって特定された状態遷移がＤＩＲＷマトリックスに設定されているかを判別する機能部である。なお、判別結果は、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶される。
【００４８】
決定部６０８では、２種類の手法によってカバレッジ基準を決定することができる。まず、実装カバレッジ基準を抽出する場合、決定部６０８は、判別部６０７によってＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を検証対象レジスタの検証カバレッジを算出する際の母集団として抽出する。一方、マトリックスカバレッジ基準を抽出する場合、決定部６０８は、ＤＩＲＷマトリックスに含まれるすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団として抽出する。
【００４９】
実装カバレッジ基準、マトリックスカバレッジ基準いずれの場合も、上述のように決定部６０８によって決定され状態遷移群による母集団が、検証対象レジスタにおけるカバレッジ基準となる。この決定部６０８によって決定されたカバレッジ基準は、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶されてもよいし、外部装置によって検証シミュレーションを実行させるために通信Ｉ／Ｆ５０８などを用いて外部へ出力されてもよい。
【００５０】
算出部６０９は、判別部６０７によってＤＩＲＷマトリックスに設定されていると判別された状態遷移について、当該状態遷移に応じたパスの妥当性に関する情報を用いたシミュレーションが実行された場合、決定部６０８によって決定されたカバレッジ基準を分母とし、実行されたシミュレーションの数を分子とした算出結果を検証カバレッジとして出力する。この算出結果は、すなわち、決定部６０８によって決定されたカバレッジ基準の網羅率をあらわしている。なお、算出部６０９によって出力された検証カバレッジは、出力デバイス５１０においてディスプレイへの表示やプリンタへの印刷出力をおこなってもよいし、ＲＡＭ５０３、磁気ディスク５０５、光ディスク５０７などの記憶領域に記憶されてもよい。さらに、通信Ｉ／Ｆ５０８による外部装置へ送信してもよい。
【００５１】
また、図６−２は、カバレッジ基準の決定手順を示すフローチャートである。図６−１にて説明した機能部を備えた検証支援装置５００によって最も特徴的な点は、ＣＤＦＧを取得してＤＩＲＷマトリックスから実装カバレッジ基準を決定するための処理の手順である。したがって、以下に、カバレッジ基準の決定手順について説明する。さらに、図６−２を用いて説明する。
【００５２】
図６−２のフローチャートにおいて、まず、検証対象回路１００のＣＤＦＧを取得する（ステップＳ６２１）。そして、取得したＣＤＦＧから検証対象レジスタを含むＤＦＧを抽出する（ステップＳ６２２）。このステップＳ６２２によって抽出したＤＦＧを参照して検証対象レジスタに関するパスを抽出する（ステップＳ６２３）。
【００５３】
さらに、ステップＳ６２３によって抽出したパスの状態遷移を特定し（ステップＳ６２４）、特定した状態遷移がＤＩＲＷマトリックスに設定されているか否かを判断する（ス
テップＳ６２５）。ＤＩＲＷマトリックスに設定されていなければ（ステップＳ６２５：Ｎｏ）、そのまま一連の処理を終了する。一方、ＤＩＲＷマトリックスに設定されている場合（ステップＳ６２５：Ｙｅｓ）、設定されているすべての状態遷移をカバレッジ基準として決定し（ステップＳ６２６）、一連の処理を終了する。
【００５４】
このように検証支援装置５００に含まれるレジスタを検証対象レジスタとしてカバレッジ基準を決定する場合、どのようなレジスタが検証対象レジスタに設定されたとしても、実装カバレッジ基準、マトリックスカバレッジ基準のいずれか、もしくは双方のカバレッジ基準を決定することができる。また、このカバレッジ基準を用いて効率的な検証カバレッジを算出することもできる。
【００５５】
また、図６−１の機能構成の説明にて述べたように、検証支援装置５００によってカバレッジ基準を決定する際は、マトリックスカバレッジ基準を決定するか、実装カバレッジ基準を決定するかによって、要求される機能部の構成が大きく異なる。マトリックスカバレッジ基準を決定する場合は、図６−１に示した機能部のうち、ＤＩＲＷマトリックスが記録された記録部６０１以外は、決定部６０８が用意されていればよい。
【００５６】
したがって、検証支援装置５００の利用者や上位システムが求める検証精度や、検証支援装置５００の利用環境に応じて上記の２種類のカバレッジ基準のうちのいずれか一方を決定するような利用方法であってもよい。マトリックスカバレッジ基準を利用する場合は、ＤＩＲＷマトリックスを取得すれば、一意的に決定されるため、カバレッジ基準決定処理は高速に実現できる。そして、マトリックスカバレッジ基準として決定されたパターンは、ＤＩＲＷマトリックスに設定されているすべての状態遷移に対応するシミュレーションのパターンである。したがって、後述する実装カバレッジ基準と比べると、多数のパターンをシミュレートしなければ、網羅率が上がらない。
【００５７】
一方、実装カバレッジ基準を利用する場合は、処理手順が多いため、マトリックスカバレッジ基準と比べて、カバレッジ基準決定処理に時間を要する。そして、実装カバレッジ基準として決定されたパターンは、検証対象回路１００に実装されているレジスタによって実際に生じる可能性のある状態遷移に絞られたパターンである。したがって、マトリックスカバレッジ基準と比べて、カバレッジ基準となるシミュレーションのパターン数も少なくなり、シミュレートしたパターン数が少なくても、高い網羅率となる。なお、マトリックスカバレッジ基準の場合であっても、従来のカバレッジ基準と比較して、格段にシミュレーションのパターン数が少なくて済む。
【００５８】
つぎに、上述したカバレッジ基準の決定と、決定されたカバレッジ基準を用いた検証カバレッジの算出について、具体的な入出力例を用いて説明する。
【００５９】
（検証カバレッジの算出手順）
まず、検証カバレッジを算出するまでの全体の処理手順について説明する。図７は、検証カバレッジの算出手順を示すフローチャートである。ここで、実際の手順説明の前に検証カバレッジの算出に用いる入力データについて説明する。本実施の形態は、下記のｉ）〜ｉｖ）の情報の入力を受け付けてカバレッジ基準を決定する。
【００６０】
ｉ）    検証シナリオ
ｉｉ）  検証対象となるレジスタのリスト
ｉｉｉ）ハードウェアの実装情報
ｉｖ）  ＤＩＲＷマトリックス
これらｉ）〜ｉｉｉ）の情報については個々に説明する。また、ｉｖ）ＤＩＲＷマトリックスは、図２−１および図２−２にて説明した情報である。このｉｖ）ＤＩＲＷマトリ
ックスの利用が、本実施の形態の特徴的な処理となる。
【００６１】
図７のフローチャートでは、まず、上記の情報のうちｉ）〜ｉｉｉ）が入力されることによって、検証シナリオの中の実行範囲を特定し（ステップＳ７０１）、実装記述を解析する（ステップＳ７０２）。その後、ｉｖ）のＤＩＲＷマトリックスが入力されることによってパスを抽出する（ステップＳ７０３）。その後、抽出されたパスからカバレッジ基準を決定する（ステップＳ７０４）。そして、決定されたカバレッジ基準を用いて検証カバレッジが算出され（ステップＳ７０５）、一連の処理を終了する。以下、各ステップの処理内容について入力される情報とともに詳細に説明する。
【００６２】
（実行範囲を特定：ステップＳ７０１）
ステップＳ７０１では、システム全体のＲＴＬ（Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ
Ｌｅｖｅｌ：レジスタ転送レベル）記述と、システム全体の検証シナリオと、システム全体のレジスタリストとの情報が入力される（上記ｉ）〜ｉｉｉ）に相当）。ここで、図８は、検証対象回路の仕様書を示す説明図である。ステップＳ７０１において入力される検証対象回路１００の検証シナリオは、仕様書８００の記載内容に応じて設定される。
【００６３】
そして、図９は、検証シナリオの記載例を示す説明図である。図９の検証シナリオ９００は、図８にて説明した仕様書８００を反映した検証処理によって構成されている。また、図１０は、仕様書に含まれるレジスタリスト例を示す説明図である。検証シナリオ９００に登場するレジスタは、それぞれレジスタリスト１０００に記載されたような構成になっている。さらに、図１１は、ＲＴＬ記述の記載例（その１）を示す説明図である。このＲＴＬ記述１１００がハードウェアの実装情報となる。また、ＲＴＬ記述１１００の中の記述１１０１は、レジスタリスト１０００（図１０参照）に記載されたレジスタに相当する。
【００６４】
なお、上述したように、レジスタリスト１０００は、ＲＴＬ記述１１００から生成可能である。したがって、レジスタリスト１０００が入力されなかった場合には、ＲＴＬ記述１１０から生成されるが、生成されたレジスタリストには、図１０のレジスタリスト１０００の制約条件部分の情報が含まれていない。制約条件が含まれていない場合、レジスタの設定制約無しとなり、検証範囲が拡大してしまう。したがって、レジスタリスト１０００を用意することによって、制約条件分検証範囲を限定することができる。
【００６５】
以上説明した情報が入力されると、ステップＳ７０１ではＲＴＬ記述１１００の全体から検証シナリオ９００によって検証を実行する範囲を抽出する。したがって、ステップＳ７０１の処理後、特定した範囲に関するＲＴＬ記述と、検証シナリオと、レジスタリストとが出力される。
【００６６】
なお、ステップＳ７０１における実行範囲の特定の際には、入力された情報に対して利用者が範囲抽出をおこなってもよいが、公知の技術を用いてもよい。たとえば、上記特許文献１に記載の技術を利用することによって容易に実行範囲を特定することができる。また、ステップＳ７０１の処理は、システム全体の中から利用者にとって検証を要する範囲を特定して検証支援をおこなうための選別処理となる。したがって、ステップＳ７０１によって検証支援処理全体の処理効率を向上させることができる。なお、ステップＳ７０１の処理を省略してシステム全体を検証対象としてもよい。
【００６７】
（実装記述の解析：ステップＳ７０２）
ステップＳ７０２では、ステップＳ７０１によって実行範囲が特定されたＲＴＬ記述（図１１参照）と、レジスタリスト（図１０参照）とが入力される。そして、入力されたＲＴＬ記述から制御の流れをあらわすＣＦＧとデータの流れをあらわすＤＦＧとを生成する。
【００６８】
図１２は、ＣＦＧの構成例を示す回路図である。図１２のＣＦＧ１２００は、ＲＴＬ記述による制御の流れを視覚的にあらわしている。図１１のＲＴＬ記述１１００の場合は、記述１１０２〜１１０８によってデータの制御がおこなわれている。したがって、ＣＦＧ１２００の処理の流れは記述１１０２〜１１０８相当となる。
【００６９】
また、ＣＦＧ１２００には、５つのＤＦＧが含まれている。図１３−１〜図１３−５は、ＤＦＧ１〜５の構成を示す回路図である。図１３−１〜図１３−５にあらわされたレジスタは、下記のようなパラメータが付与されそれぞれ演算がおこなわれる。なお、ＤＦＧ１２００は、図１１の記述１１０２に相当する。また、ＤＦＧ１は図１１の記述１１０３に、ＤＦＧ２は記述１１０４に、ＤＦＧ３は記述１１０５に、ＤＦＧ４は記述１１０６に、ＤＦＧ５は記述１１０７，１１０８に、それぞれ相当する。
【００７０】
・ｒ１＝ａ，ｒ２＝ｂ，ｒ３＝ｃ，ｒ４＝ｐ１，ｒ５＝ｐ２，ｒ６＝ｄ
・ｔ，Ｌ：内部レジスタ
・＋：加算
・Ｓ：面積を求める演算
【００７１】
上述のように、ＣＦＧと、ＤＦＧとが生成されると、これらの生成結果を用いて、さらに、ＣＤＦＧが生成される。図１４は、ＣＤＦＧの構成例を示す回路図である。図１４のように、ＣＤＦＧ１４００は、ＣＦＧ（図１２参照）と、ＤＦＧ（図１３−１〜図１３−５参照）とを合成した構成となる。このＣＤＦＧの生成に関する技術として、たとえば、ＲＴＬ記述から回路生成をおこなう高位合成技術を用いてもよい（松永祐介、「高位合成技術の基礎」、電子情報通信学会ソサエティ大会、２００３年９月）。
【００７２】
さらに、図１５は、ＣＤＦＧのデータ構造を示す説明図である。ステップＳ７０２では、最終的に、入力されたＲＴＬ記述に対応するＣＤＦＧのデータ１５００を出力する。ＣＤＦＧのデータ１５００は、図１５のようなデータ構造になっており、ＣＦＧごとに、ＣＦＧ内のＤＦＧが含まれた構造となっている。
【００７３】
（パスの抽出：ステップＳ７０３）
ステップＳ７０３では、ステップＳ７０２の実装記述の解析によって生成されたＣＤＦＧと、ＤＩＲＷマトリックスとが入力されＤＩＲＷに対応するパスが出力される。ステップＳ７０３では、図２−１および図２−２にて説明したＤＩＲＷマトリックスを参照して特定の内部レジスタに関するパスを抽出する。図１６は、内部レジスタｔに関するパス抽出手順を示す説明図である。図１６を用いて内部レジスタｔに関するパス抽出手順について説明する。
【００７４】
ステップＳ７０２によって生成したＣＤＦＧにおいて、内部レジスタｔが利用される箇所は、ＤＦＧ１、ＤＦＧ２、ＤＦＧ４、ＤＦＧ５の４箇所である。したがって、この４箇所のＤＦＧの内部レジスタｔのパスにおいてどのような遷移が起こっているかが抽出される。具体的には、内部レジスタｔの場合、下記のような抽出がおこなわれる。
【００７５】
・ＤＦＧ１の０のｔをＩｎｉｔｉａｌｉｚｅするパス（ステップＳ１６０１）
・ＤＦＧ２のｔへＳをＷｒｉｔｅするパス（ステップＳ１６０２）
・ＤＦＧ４のｔからｒ６へＲｅａｄするパス（ステップＳ１６０３）
・ＤＦＧ５のＬからｔへＷｒｉｔｅするパスとｔからｒ６へＲｅａｄするパス（ステップＳ１６０４）
【００７６】
なお、上述したＤＦＧ１，ＤＦＧ２，ＤＦＧ４，ＤＦＧ５に含まれている内部レジスタｔは、それぞれＲＴＬ記述１１００によって条件が設定されている。たとえば、ＤＦＧ１は、記述１１０２によって条件なし、ＤＦＧ２では、記述１１０３によってｒ４の値を０に設定するなどである。そして、ステップＳ７０３では、上述のように抽出されたパスに対して、さらに、ＤＩＲＷマトリックに応じたパスの場合分け（×、△、○）に応じてそれぞれパス抽出をおこなう。
【００７７】
まず、バグを生じる（×）パス抽出について説明する。図１７は、バグを生じるパス抽出を示す説明図である。図１７の真理値表１７００に示すように、バグを生じるパスは、Ｄｅｃｌａｒｅ→Ｒｅａｄ（×１）が存在する。しかしながら、検証対象回路１００には、内部レジスタｔについてＤｅｃｌａｒｅ→Ｒｅａｄの状態遷移が生じるパスは存在しない。したがって、バグを生じる（×）パスは抽出されない。
【００７８】
つぎに、設計意図の確認を要する（△）パス抽出について説明する。図１８は、確認を要するパス抽出を示す説明図である。図１８の真理値表１８００に示すように、確認を要するパスは、Ｄｅｃｌａｒｅ→Ｗｒｉｔｅ（△１）と、Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅ（△２）と、Ｗｒｉｔｅ→Ｗｒｉｔｅ（△３）と、が存在する。この３つのパスのうち、ＤＦＧ２と、ＤＦＧ５とにＷｒｉｔｅ→Ｗｒｉｔｅ（△３）のパスが存在しており、確認を要する（△）パスとして抽出される。本実施の形態では、このように、抽出されたパスは、内部レジスタｔが実装されているパスを意味する。したがって、ＤＩＲＷマトリックスに設定されている状態遷移のうち、抽出されたパスをあらわす状態遷移には、専用のフラグを立てるなどして他の状態遷移と区別が付くようにする。
【００７９】
最後に、正常な（○）パス抽出について説明する。図１９は、正常なパス抽出を示す説明図である。図１９の真理値表１９００に示すように、正常なパスは、上述した４つのパス（×１および△１〜３）以外の８つのパスは正常なパスとなる。これら８つのパスのうち、ＤＦＧ１には、Ｄｅｃｌａｒｅ→Ｉｎｉｔｉａｌｉｚｅ（○１）と、Ｉｎｉｔｉａｌｉｚｅ→Ｒｅａｄ（○３）と、Ｉｎｉｔｉａｌｉｚｅ→Ｗｒｉｔｅ（○４）とが存在している。
【００８０】
また、ＤＦＧ２には、Ｉｎｉｔｉａｌｉｚｅ→Ｗｒｉｔｅ（○４）と、Ｗｒｉｔｅ→Ｒｅａｄ（○７）が存在している。また、ＤＦＧ４には、Ｉｎｉｔｉａｌｉｚｅ→Ｒｅａｄ（○３）と、Ｗｒｉｔｅ→Ｒｅａｄ（○８）とが存在している。そして、ＤＦＧ５には、Ｉｎｉｔｉａｌｉｚｅ→Ｗｒｉｔｅ（○４）と、Ｒｅａｄ→Ｗｒｉｔｅ（○８）とが存在している。そして、これらのパスは正常な（○）パスとして抽出される。また、ここでも、上述した△のパスと同様に、ＤＩＲＷマトリックスに設定されている状態遷移のうち、抽出されたパスをあらわす状態遷移には、他の状態遷移と区別するためのフラグを立てる。
【００８１】
このように、ステップＳ７０３では、ＤＩＲＷマトリックスを利用して検証対象となるレジスタ（上述の例では内部レジスタｔ）のパスをすべて検出することができる。なお、ステップＳ７０３によって、全レジスタに対する処理が終了したか否かを判断しているように、ステップＳ７０３のパス抽出は、検証対象となるレジスタすべてに対して順次おこなわれる。したがって、検証対象回路１００の場合は、内部レジスタｔの他にもレジスタ（たとえば、内部レジスタＬや、実装依存レジスタ？など）が存在するため、これら他のレジスタに対しても、上述のようなパス抽出を実行する。
【００８２】
さらに、このステップＳ７０３では、シミュレーションの実行時に実際に対応する状態遷移が起こったことを確認するためのアサーションを生成することもできる。このアサーションとは、具体的には、該当するパスによって実際に状態遷移が生じる際の条件である。この条件は、ＣＤＦＧを構成するデータの中の対応レジスタの記述を参照することによって生成することができる。
【００８３】
たとえば、ＣＤＦＧを構成するデータがＰＳＬ言語を使用した記述であった場合には、下記のようなアサーションが生成される。
・Ｄ（Ｄｅｃｌａｒｅ）→Ｉ（Ｉｎｉｔｉａｌｉｚｅ）
ａｓｓｅｒｔ  ａｌｗａｙｓ（〜ＲＥＳＥＴ｜＝＞ｔ＝０）＠（ＰｐｏｓｅｇｅＣＬＫ）・Ｉ（Ｉｎｉｔｉａｌｉｚｅ）→Ｒ（Ｒｅａｄ）
ａｓｓｅｒｔ  ａｌｗａｙｓ（ｒ４＝＝０｜＝＞ｒ５＝＝１）ａｂｏｒｔ（〜ＲＥＳＥＴ）＠（ＰｐｏｓｅｇｅＣＬＫ）
【００８４】
これら生成されたアサーションは、後述するステップＳ７０４において実装カバレッジ基準を決定する際に併せて出力される。ここで、図２０は、マーク付きＤＩＲＷマトリックスの出力例を示す図表である。ステップＳ７０３のパス抽出処理によって、抽出されたパスに相当する状態遷移にはフラグが立てられている。したがって、ステップＳ７０３の処理後、ＤＩＲＷマトリックスは、図表２０００のように、実装の有無をあらわすマーク（ｙｅｓ）が付与されたデータ群として出力される。このとき、上述したようなアサーションを生成した場合には、アサーションも付与されたデータとなる。
【００８５】
（カバレッジ基準の決定：ステップＳ７０４）
ステップＳ７０４では、検証支援装置５００の利用者や上位システムからの指示に応じて、マトリックスカバレッジ基準と、実装カバレッジ基準との２種類のカバレッジ基準を決定する。マトリックスカバレッジ基準を決定する場合には、最初に取得したＤＩＲＷマトリックスに設定されているすべての状態遷移が対象となる。したがって、マトリックスカバレッジ基準として、図３に示したような、斜線部分の１２通りの状態遷移によって構成される。
【００８６】
一方、実装カバレッジ基準を決定する場合には、ステップＳ７０３の処理によるパス抽出結果を利用する。ここで、図２１および図２２は、実装カバレッジ基準の生成例を示す図表である。ステップＳ７０４では、図２１の図表２１００の斜線部分のように、実装有り（ｙｅｓ）と設定されている状態遷移からなる母集団がカバレッジ基準として決定される。このように決定されたカバレッジ基準が実装カバレッジ基準となる。したがって、実装カバレッジ基準としては、図４に示したような斜線部分の４通りの状態遷移によって構成される。
【００８７】
また、ステップＳ７０３においてアサーションを生成した場合には、アサーションを考慮して、より高精度な実装カバレッジ基準を決定してもよい。アサーションは、１つの状態遷移において複数のパターンが生成されることがある。したがって、アサーションを考慮する場合は、図２２の図表２２００の斜線部分のように、同じ状態遷移であっても、アサーションごとに決定する。したがって、アサーションを考慮した実装カバレッジ基準として、６通りの状態遷移＋アサーションの集合体が決定される。なお、検証シミュレーションの実行や検証カバレッジの算出を外部の装置によっておこなう場合は、決定されたカバレッジ基準の出力までを一連の処理として検証支援装置５００の処理を終了してもよい。
【００８８】
（検証カバレッジ算出：ステップＳ７０５）
最後に、ステップＳ７０４にて決定されたカバレッジ基準を用いて検証カバレッジを算出する。たとえば、マトリックスカバレッジ基準の場合は、図３に示した全１２通りの状態遷移をシミュレーションのパターンとして検証をおこなう。そして１２通りのパターンを母集団とした場合の検証の網羅率［検証実行パターン数／１２パターン］の算出結果が検証カバレッジとして出力される。実装カバレッジ基準の場合も同様に、図４に示した全４通りの状態遷移をシミュレーションのパターンとして検証をおこなう。網羅率の式は、
通常は［検証実行パターン数／４パターン］、アサーションを考慮する場合は［検証実行パターン数／６パターン］となる。この場合も算出結果が検証カバレッジとして出力される。
【００８９】
以上説明したように、本実施の形態によれば、カバレッジ基準を決定する際に、第１段階として、ＤＩＲＷマトリックスを利用することにより、シミュレーションのパターン数の種類が、検証対象回路１００によって生じる可能性のある状態遷移に限られる。この処理によって、パスが抜けることもなく、なおかつ無限大に近い数あったパターンの種類を大幅に絞ることができ、検証カバレッジを算出する際の分母の値を小さくできる。このようなカバレッジ基準を利用することによって、検証カバレッジの算出の処理時間が大幅に短縮される。
【００９０】
また、第２段階として、ＤＩＲＷマトリックスに設定されている状態遷移の中から、さらに、実装されているレジスタによって生じる状態遷移に限定してカバレッジ基準を決定する。したがって、検証が必要なパスによっておこる状態遷移のみを効率的に抽出することができる。
【００９１】
＜他の実施の形態：連続検証シナリオ＞
つぎに、他の実施の形態として、複数の検証シナリオを連続して実行させる連続検証シナリオを用いる場合について説明する。上述した実施の形態の検証対象回路の場合、図９に示したような検証シナリオ９００を１回実行させることによって、十分に検証対象となるパスを抽出することができた。
【００９２】
しなしながら、検証対象回路のＲＴＬ記述の内容によっては、十分に検証対象となるパスを抽出できないこともある。そこで、本実施の形態では、検証シナリオを連続して実行させることによって１回の検証シナリオでは抽出できなかったパスを抽出する。ここで、連続して実行させる検証シナリオは、同一の検証シナリオでもよいし、異なる検証シナリオでもよい。
【００９３】
ここでは、同一の検証シナリオを連続して２回実行させる場合を例に挙げて説明する。図２３は、連続検証シナリオの記載例を示す説明図である。また、図２４は、ＲＴＬ記述の記載例（その２）を示す説明図である。図２３の検証シナリオ２３００は、図２４に示したＲＴＬ記述２４００の処理を２回繰り返して実行させる処理をあらわしている。２回目シナリオには、１回目シナリオの出力と、２回目シナリオの入力との関係が示されている。
【００９４】
ここで、図２５は、連続検証シナリオを用いた場合のＣＤＦＧの構成例を示す回路図である。図２４に示したＲＴＬ記述２４００では、図２５のようなＣＤＦＧ２５００が生成される。なお、ＣＤＦＧ２５００全体は、図２４の記述２４０１に相当する。そして、ＣＤＦＧ２５００を構成する各ＤＦＧにおいて、ＤＦＧ１は図２４の記述２４０２に、ＤＦＧ２は記述２４０３に、ＤＦＧ３は記述２４０４に、ＤＦＧ４は記述２４０５にそれぞれ相当する。
【００９５】
そして、１回目シナリオでは、ｒ１〜ｒ５にそれぞれパラメータが設定され、ｒ６の値が読み出される。そして、２回目シナリオでは、１回目シナリオの処理によって求められたｒ６の値がｒ１に設定され、ｒ２，ｒ３の値は、そのまま、再度ｒ２，ｒ３に設定される。これらｒ１〜ｒ３の設定によって再度ＣＤＦＧ２５００の処理を実行することによって２回目シナリオが実行されることになる。
【００９６】
そして、本実施の形態の場合も、連続検証シナリオの中から検証対象となるレジスタに関するパスの抽出をおこなう。ここでも、内部レジスタｔを検証対象レジスタとして図２６は、連続検証シナリオを用いた場合の内部レジスタｔに関するパス抽出手順を示す説明図である。図２６のように、ＣＤＦＧ２５００において、内部レジスタｔが利用される箇所はＤＦＧ１，ＤＦＧ３，ＤＦＧ４の３箇所である。したがって、この３箇所のＤＦＧの内部レジスタｔのパスにおいてどのような遷移が起こっているかが抽出される。具体的には、内部レジスタｔの場合、下記のような抽出がおこなわれる。
【００９７】
・ＤＦＧ１の０のｔをＩｎｉｔｉａｌｉｚｅするパス（ステップＳ２６０１）
・ＤＦＧ３のｔからｒ６へＲｅａｄするパス（ステップＳ２６０２）
・ＤＦＧ４のＬからｔへＷｒｉｔｅするパス（ステップＳ２６０３）
【００９８】
なお、上述したＤＦＧ１，ＤＦＧ３，ＤＦＧ４に含まれている内部レジスタｔは、それぞれＲＴＬ記述１１００によって条件が設定されている。たとえば、ＤＦＧ１は、記述２４０２によって条件なし、ＤＦＧ３では、記述２４０４によってｒ５の値を０に設定するなどである。
【００９９】
そして、本実施の形態の場合は、さらに、ｒ６の値を用いて再度ＣＤＦＧ２５００を実行するため、２回目のＣＤＦＧ２５００からも内部レジスタｔに関するパスを抽出する。図２７は、連続検証シナリオに応じた連続パスの生成例を示す説明図である。図２３の検証シナリオ２３００では、図２７のように、１回目シナリオが実行された後、１回目シナリオの実行結果ｒ６を用いて２回目シナリオを実行することによって連続パスが生成される。そして、２回目シナリオの中からも、１回目シナリオと同様に、ＤＦＧ１，ＤＦＧ３，ＤＦＧ４から内部レジスタｔに関するパスを抽出する。
【０１００】
つぎに、上述のように抽出されたパスに対して、さらに、ＤＩＲＷマトリックスに応じたパスの場合分け（×，△，○）に応じてそれぞれパス抽出をおこなう。まず、バグを生じる（×）パス抽出について説明する。図２８は、連続検証シナリオを用いた場合のバグを生じるパス抽出を示す説明図である。図２８の真理値表２８００に示すように、バグを生じるパスは、Ｄｅｃｌａｒｅ→Ｒｅａｄ（×１）が存在する。そして、検証対象回路には、内部レジスタｔについてＤｅｃｌａｒｅ→Ｒｅａｄの状態遷移が生じるパスとして、１回目シナリオ実行時のｒ３と、ＤＦＧ３とが存在する。したがって、実装が確認されたパスとして抽出されたパスの状態遷移には、専用のフラグを立てるなどして他の状態遷移と区別が付くようにする。なお、１回目シナリオによってパスが抽出された状態遷移については、２回目シナリオから抽出する必要がないため、２回目シナリオのＤＦＧ３からは特に抽出処理をおこなわない。
【０１０１】
つぎに、設計意図の確認を要する（△）パス抽出について説明する。図２９は、連続検証シナリオを用いた場合の確認を要するパス抽出を示す説明図である。図２９の真理値表２９００に示すように、確認を要するパスは、Ｄｅｃｌａｒｅ→Ｗｒｉｔｅ（△１）と、Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅ（△２）と、Ｗｒｉｔｅ→Ｗｒｉｔｅ（△３）と、が存在する。
【０１０２】
これら３つのパスのうち、Ｄｅｃｌａｒｅ→Ｗｒｉｔｅ（△１）のパスは、１回目シナリオのｒ３と、ＤＦＧ４とから抽出することができる。また、Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅ（△２）のパスは、２回目シナリオのＤＦＧ１から抽出することができる。そして、Ｗｒｉｔｅ→Ｗｒｉｔｅ（△３）のパスは、２回目シナリオのＤＦＧ４から抽出することができる。ここでも、抽出されたパスをあらわす状態遷移には、専用のフラグを立てるなどして他の状態遷移と区別が付くようにする。設計意図の確認を要する（△）パスのうち、Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅ（△２）と、Ｗｒｉｔｅ→Ｗｒｉｔｅ（△３）との両パスについては、１回目シナリオを実行するだけでは、あらわれないパスであり、本実施の形態のように２回目シナリオを実行することによってはじめて抽出可能となる。
【０１０３】
最後に、正常な（○）パス抽出について説明する。図３０は、連続検証シナリオを用いた場合の正常なパス抽出を示す説明図である。図３０は、正常なパス抽出を示す説明図である。図３０の真理値表３０００に示すように、正常なパスは、上述した４つのパス（×１および△１〜３）以外の８つのパスは正常なパスとなる。本実施の形態では、１回目シナリオと２回目シナリオとを実行させることによって、上述した正常な（○）８つのパスのうち、Ｉｎｉｔｉａｌｉｚｅ→Ｉｎｉｔｉａｌｉｚｅ以外のすべてのパス（○１〜○７）を抽出することができる。
【０１０４】
そして、○１〜○７のうち、特に○４および○５のパスについては、２回目シナリオが実行されることによってはじめて抽出可能となるパスである。すなわち、図３０のように、Ｒｒａｄ→Ｉｎｉｔｉａｌｉｚｅ（○４）は、２回目シナリオのＤＦＧ１から抽出され、Ｒｅａｄ→Ｒｅａｄ（○５）は、２回目シナリオのＤＦＧ４から抽出される。他の正常なパス（○１〜○３，○６，○７）については、１回目シナリオから抽出可能であるため個々の説明は省略する。そして、抽出された○１〜○７のパスについても、ＤＩＲＷマトリックスに設定されている状態遷移のうち、抽出されたパスをあらわす状態遷移には、他の状態遷移と区別するためのフラグを立てる。
【０１０５】
このように、内部レジスタｔに関する実装パスを抽出した後は、実装カバレッジ基準を生成するための処理に移行する。図３１は、連続検証シナリオを用いた場合のマーク付きＤＩＲＷマトリックスの出力例を示す図表である。パス抽出処理によって、抽出されたパスに相当する状態遷移にはフラグが立てられている。したがって、ステップＳ７０３の処理後、ＤＩＲＷマトリックスは、図表３１００のように、実装の有無をあらわすマーク（ｙｅｓ）が付与されたデータ群として出力される。また、抽出したパスの状態遷移が起こったことを確認するためのアサーションを生成した場合には、このアサーションも付与されたデータとなる。
【０１０６】
そして、図３２、図３３は、連続検証シナリオを用いた場合の実装カバレッジ基準の生成例を示す図表である。図３２では、図表３１００の斜線部分のように、実装有り（ｙｅｓ）と設定されている状態遷移からなる母集団がカバレッジ基準として決定される。このように決定されたカバレッジ基準が実装カバレッジ基準となる。したがって、実装カバレッジ基準としては、１１通りが実装カバレッジ基準の分母となる。
【０１０７】
また、図３３では、図表３１００のうち、斜線部分のように、アサーションを考慮した遷移状態が、実装カバレッジ基準となる。したがって、実装カバレッジ基準としては、１３通りが実装カバレッジ基準の分母となり、より高精度な実装カバレッジ基準となる。そして、図３２もしくは図３３の基準によって生成した実装カバレッジ基準を用いて検証カバレッジを算出する。検証カバレッジの算出は、図７のステップＳ７０５の処理と同様であるため説明を省略する。
【０１０８】
（パラメータ算出）
なお、上述したパス抽出処理結果を利用して検証シナリオを実行する際の、パラメータを算出することもできる。すなわち、ＣＤＦＧ２５００と、抽出されたＤＩＲＷに対応する実装パスを参照することによって、検証シナリオにパラメータとして代入される可能性のある値を算出すればよい。
【０１０９】
図２８〜図３０のように、×，△，○の各パスが抽出されたが、これら各パスには下記のような値が入力される可能性がある。
【０１１０】
・×のパス
Ｄｅｃｌａｒｅ→Ｒｅａｄ：ｒ４＝１，ｒ５＝０（１回目）
・△のパス
Ｄｅｃｌａｒｅ→Ｗｒｉｔｅ：ｒ４＝１，ｒ５＝１（１回目）
Ｗｒｉｔｅ→Ｉｎｉｔｉａｌｉｚｅ：ｒ５＝１（１回目）、ｒ４＝０（２回目）
Ｗｒｉｔｅ→Ｗｒｉｔｅ：ｒ４＝１（１回目）、ｒ４＝１，ｒ５＝１（２回目）
・○のパス
Ｄｅｃｌａｒｅ→Ｉｎｉｔｉａｌｉｚｅ：ｒ４＝０（１回目）
Ｉｎｉｔｉａｌｉｚｅ→Ｒｅａｄ：ｒ４＝０，ｒ５＝０（１回目）、ｒ４＝０，ｒ５＝０（２回目）
Ｉｎｉｔｉａｌｉｚｅ→Ｗｒｉｔｅ：ｒ４＝０，ｒ５＝１（１回目）、ｒ４＝０，ｒ５＝１（２回目）
Ｒｅａｄ→Ｉｎｉｔｉａｌｉｚｅ：ｒ５＝１（１回目）、ｒ４＝０（２回目）
Ｒｅａｄ→Ｒｅａｄ：ｒ５＝０（１回目）、ｒ４＝１，ｒ５＝０（２回目）
Ｒｅａｄ→Ｗｒｉｔｅ：ｒ５＝０（１回目）、ｒ４＝１，ｒ５＝１（２回目）
Ｗｒｉｔｅ→Ｒｅａｄ：ｒ５＝０（１回目）、ｒ４＝１，ｒ５＝０（２回目）
なお、設定されていないパラメータは任意の値をとればよい。
【０１１１】
パラメータの算出は、上述の値が代入される場合について、それぞれ入力される可能性がある値を算出する。当然のことながら、検証対象パス数に応じてパラメータの算出は複雑になるが、ソルバーやＭａｔｈｅｍａｔｉｃａなどの既存の演算アプリケーションを利用することによって容易に実現することができる。
【０１１２】
図３４は、パラメータ付き検証シナリオの出力例を示す図表である。上述したような処理によって算出された値を検証シナリオにパラメータを設定して、図３４のようにパラメータ値付き検証シナリオ３４００として出力することができる。このように、パラメータ付きの検証シナリオを生成することによって、効率的に検証シナリオを実行することができる。
【０１１３】
このように、１回の検証シナリオの実行では、パスの抽出が不十分な場合には、連続して複数の検証シナリオを実行させることによって、抽出できなかったパスを抽出することができる。検証対象回路の構成によって、検証シナリオを１回実行すれば十分にパスを抽出できる場合もあれば、３回実行させないと十分にパスを抽出できない場合もある。また、利用する検証シナリオによっても抽出結果が異なることがある。したがって、あらかじめ、各種シミュレーションツールを用いて、どのような検証シナリオを利用するのが効率的であるかを検証してもよいし、利用者が、利用する検証シナリオの種類や回数を適宜組み合わせてもよい。
【０１１４】
以上説明したように、本実施の形態にかかる検証支援処理では、効率的に決定されたカバレッジ基準を用いて求めた検証カバレッジを利用させるため、結果として信頼性の高い検証情報となる。したがって、このような検証カバレッジを利用することによって、検証対象レジスタに対する検証精度を向上させることができる。
【０１１５】
なお、本実施の形態で説明した検証支援方法は、あらかじめ用意されたプログラムをパーソナル・コンピュータやワークステーションなどのコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤなどのコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また、このプログラムは、インターネットなどのネットワークを介して配布することが可能な媒体であってもよい。
【０１１６】
また、本実施の形態で説明した検証支援装置５００は、スタンダードセルやストラクチャードＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）などの特定用途向けＩＣ（以下、単に「ＡＳＩＣ」と称す）やＦＰＧＡなどのＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）によっても実現することができる。具体的には、たとえば、上述した検証支援装置５００の機能（取得部６０２〜算出部６０９）をＨＤＬ記述によって機能定義し、そのＨＤＬ記述を論理合成してＡＳＩＣやＰＬＤに与えることにより、検証支援装置５００を製造することができる。
【０１１７】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０１１８】
（付記１）コンピュータを、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得手段、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得手段によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出手段、
前記ＤＦＧ抽出手段によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出手段、
前記パス抽出手段によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定手段、
前記特定手段によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別手段、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段、
として機能させることを特徴とする検証支援プログラム。
【０１１９】
（付記２）前記コンピュータを、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別された状態遷移を実現するための条件を抽出する条件抽出手段として機能させ、
前記決定手段は、前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移と、当該状態遷移について前記条件抽出手段によって抽出された条件とを前記カバレッジ基準として決定することを特徴とする付記１に記載の検証支援プログラム。
【０１２０】
（付記３）前記コンピュータを、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＤＩＲＷマトリックスに含まれるすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団として抽出する決定手段、
として機能させることを特徴とする検証支援プログラム。
【０１２１】
（付記４）前記コンピュータを、
前記検証対象回路に対する検証内容をあらわす検証シナリオと、前記検証対象回路の実装情報と、前記検証対象回路の仕様書に含まれるレジスタの属性をあらわすレジスタリストとを取得する取得手段、
前記取得手段によって取得された検証シナリオと実装情報とレジスタリストとから、前記ＣＤＦＧを生成するＣＤＦＧ生成手段、として機能させ、
前記ＤＦＧ抽出手段は、前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ生成手段によって生成されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出することを特徴とする付記１または２に記載の検証支援プログラム。
【０１２２】
（付記５）前記ＣＤＦＧ生成手段は、前記取得手段によって取得された検証シナリオと実装情報とレジスタリストとから、前記検証シナリオを複数回連続して実行させる場合の前記ＣＦＧ内のデータの流れが記述されたＣＤＦＧを生成することを特徴とする付記４に記載の検証支援プログラム。
【０１２３】
（付記６）前記ＣＤＦＧ生成手段は、前記取得手段が、前記検証対象回路に対する検証内容をあらわす複数の検証シナリオを取得した場合、当該複数の検証シナリオを連続して実行させる場合の前記ＣＦＧ内のデータの流れが記述されたＣＤＦＧを生成することを特徴とする付記４に記載の検証支援プログラム。
【０１２４】
（付記７）前記コンピュータを、
前記判別手段によって前記パスに含まれる前記検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されていると判別された場合、前記取得手段によって取得された検証シナリオと、前記ＣＤＦＧ生成手段によって生成されたＣＤＦＧとを用いて、前記パスに接続されている前記検証対象レジスタにパラメータとして代入される可能性のある値を算出する算出手段、
前記算出手段によって算出された値を前記検証シナリオに設定したパラメータ値付き検証シナリオを生成するシナリオ生成手段、
として機能させることを特徴とする付記５または６に記載の検証支援プログラム。
【０１２５】
（付記８）前記コンピュータを、
前記取得部によって前記レジスタリストが取得されなかった場合、前記取得手段によって取得された検証対象回路の実装情報から当該検証対象回路に含まれるレジスタを抽出してレジスタリストを生成するリスト生成手段として機能させ、
前記ＣＤＦＧ生成手段は、前記取得手段によって取得された実装情報と、前記リスト生成手段によって生成されたレジスタリストとから、前記ＣＤＦＧを生成することを特徴とする付記４〜７のいずれか一つに記載の検証支援プログラム。
【０１２６】
（付記９）前記ＣＤＦＧ生成手段は、前記取得手段が、前記検証対象回路の中の検証対象となる範囲が限定された検証シナリオ、実装情報およびレジスタリストを取得した場合、
前記範囲限定手段から出力された前記検証対象となる範囲に限定された特定された検証シナリオ、実装情報およびレジスタリストとから、前記検証対象回路のＣＤＦＧを生成することを特徴とする付記４〜８のいずれか一つに記載の検証支援プログラム。
【０１２７】
（付記１０）前記コンピュータを、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別された状態遷移について当該状態遷移に応じたパスの妥当性に関する情報を用いたシミュレーションが実行された場合、前記決定手段によって決定されたカバレッジ基準を分母とし、前記実行されたシミュレーションの数を分子とした算出結果を検証カバレッジとして出力する算出手段として機能させることを特徴とする付記１〜９のいずれか一つに記載の検証支援プログラム。
【０１２８】
（付記１１）検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段と、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得手段と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得手段によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出手段と、
前記ＤＦＧ抽出手段によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出手段と、
前記パス抽出手段によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定手段と、
前記特定手段によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別手段と、
前記判別手段によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段と、
を備えることを特徴とする検証支援装置。
【０１２９】
（付記１２）検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスを記録する記録手段と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記記録手段に記録されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定手段と、
を備えることを特徴とする検証支援装置。
【０１３０】
（付記１３）検証支援装置が、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスをメモリに記録する記録工程と、
前記検証対象回路の実装時における制御の流れが記述されたＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に当該ＣＦＧ内のデータの流れが記述されたＤＦＧ（Ｄａｔａ  
Ｆｌｏｗ  Ｇｒａｐｈ）が書き込まれたＣＤＦＧ（Ｃｏｎｔｒｏｌ  Ｄａｔａ  Ｆｌｏｗ
Ｇｒａｐｈ）を取得するＣＤＦＧ取得工程と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＣＤＦＧ取得工程によって取得されたＣＤＦＧから、前記検証対象レジスタが記述されたＤＦＧを抽出するＤＦＧ抽出工程と、
前記ＤＦＧ抽出工程によって抽出されたＤＦＧの中から前記検証対象レジスタに関するデータの流れをあらわすパスを抽出するパス抽出工程と、
前記パス抽出工程によって抽出されたパスに含まれる検証対象レジスタの状態遷移を、前記ＤＦＧに基づいて特定する特定工程と、
前記特定工程によって特定されたパスに含まれる検証対象レジスタの状態遷移が前記ＤＩＲＷマトリックスに設定されているかを判別する判別工程と、
前記判別工程によって前記ＤＩＲＷマトリックスに設定されていると判別されたすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定工程と、
を実行することを特徴とする検証支援方法。
【０１３１】
（付記１４）検証支援装置が、
検証対象回路に含まれるレジスタにおいてＤｅｃｌａｒｅと、Ｉｎｉｔｉａｌｉｚｅと、Ｒｅａｄと、Ｗｒｉｔｅとの４つの状態の中から生じる可能性のある状態遷移と当該状態遷移に応じたパスの妥当性に関する情報とが設定されたＤＩＲＷマトリックスをメモリに記録する記録工程と、
前記検証対象回路の中の任意のレジスタが検証対象レジスタに指定された場合、前記ＤＩＲＷマトリックスに含まれるすべての状態遷移を、前記検証対象レジスタの検証カバレッジを算出する際の母集団となるカバレッジ基準に決定する決定工程と、
を実行することを特徴とする検証支援方法。
【図面の簡単な説明】
【０１３２】
【図１】本実施の形態にかかる検証支援処理の概要を示す説明図である。
【図２−１】ＤＩＲＷマトリックスの状態遷移図である。
【図２−２】ＤＩＲＷマトリックスを示す真理値表である。
【図３】マトリックスカバレッジ基準を示す説明図である。
【図４】実装カバレッジ基準を示す説明図である。
【図５】検証支援装置のハードウェア構成を示すブロック図である。
【図６−１】検証支援装置の機能的構成を示すブロック図である。
【図６−２】カバレッジ基準の決定手順を示すフローチャートである。
【図７】検証カバレッジの算出手順を示すフローチャートである。
【図８】検証対象回路の仕様書を示す説明図である。
【図９】検証シナリオの記載例を示す説明図である。
【図１０】仕様書に含まれるレジスタリスト例を示す説明図である。
【図１１】ＲＴＬ記述の記載例（その１）を示す説明図である。
【図１２】ＣＦＧの構成例を示す回路図である。
【図１３−１】ＤＦＧ１の構成を示す回路図である。
【図１３−２】ＤＦＧ２の構成を示す回路図である。
【図１３−３】ＤＦＧ３の構成を示す回路図である。
【図１３−４】ＤＦＧ４の構成を示す回路図である。
【図１３−５】ＤＦＧ５の構成を示す回路図である。
【図１４】ＣＤＦＧの構成例を示す回路図である。
【図１５】ＣＤＦＧのデータ構造を示す説明図である。
【図１６】内部レジスタｔに関するパス抽出手順を示す説明図である。
【図１７】バグを生じるパス抽出を示す説明図である。
【図１８】確認を要するパス抽出を示す説明図である。
【図１９】正常なパス抽出を示す説明図である。
【図２０】マーク付きＤＩＲＷマトリックスの出力例を示す図表である。
【図２１】実装カバレッジ基準の生成例を示す図表（その１）である。
【図２２】実装カバレッジ基準の生成例を示す図表（その２）である。
【図２３】連続検証シナリオの記載例を示す説明図である。
【図２４】ＲＴＬ記述の記載例（その２）を示す説明図である。
【図２５】連続検証シナリオを用いた場合のＣＤＦＧの構成例を示す回路図である。
【図２６】連続検証シナリオを用いた場合の内部レジスタｔに関するパス抽出手順を示す説明図である。
【図２７】連続検証シナリオに応じた連続パスの生成例を示す説明図である。
【図２８】連続検証シナリオを用いた場合のバグを生じるパス抽出を示す説明図である。
【図２９】連続検証シナリオを用いた場合の確認を要するパス抽出を示す説明図である。
【図３０】連続検証シナリオを用いた場合の正常なパス抽出を示す説明図である。
【図３１】連続検証シナリオを用いた場合のマーク付きＤＩＲＷマトリックスの出力例を示す図表である。
【図３２】連続検証シナリオを用いた場合の実装カバレッジ基準の生成例を示す図表（その１）である。
【図３３】連続検証シナリオを用いた場合の実装カバレッジ基準の生成例を示す図表（その２）である。
【図３４】パラメータ付き検証シナリオの出力例を示す図表である。
【符号の説明】
【０１３３】
５００  検証支援装置
５０１  ＣＰＵ
５０２  ＲＯＭ
５０３  ＲＡＭ
５０４  磁気ディスクドライブ
５０５  磁気ディスク
５０６  光ディスクドライブ
５０７  光ディスク
５０８  通信Ｉ／Ｆ
５０９  入力デバイス
５１０  出力デバイス
６０１  記録部
６０２  取得部
６０３  ＣＤＦＧ生成部
６０４  ＤＦＧ抽出部
６０５  パス抽出部
６０６  特定部
６０７  判別部
６０８  決定部
６０９  算出部
【図１】
2010003281.tif 000003
【図２−１】
2010003281.tif 000004
【図２−２】
2010003281.tif 000005
【図３】
2010003281.tif 000006
【図４】
2010003281.tif 000007
【図５】
2010003281.tif 000008
【図６−１】
2010003281.tif 000009
【図６−２】
2010003281.tif 000010
【図７】
2010003281.tif 000011
【図８】
2010003281.tif 000012
【図９】
2010003281.tif 000013
【図１０】
2010003281.tif 000014
【図１１】
2010003281.tif 000015
【図１２】
2010003281.tif 000016
【図１３−１】
2010003281.tif 000017
【図１３−２】
2010003281.tif 000018
【図１３−３】
2010003281.tif 000019
【図１３−４】
2010003281.tif 000020
【図１３−５】
2010003281.tif 000021
【図１４】
2010003281.tif 000022
【図１５】
2010003281.tif 000023
【図１６】
2010003281.tif 000024
【図１７】
2010003281.tif 000025
【図１８】
2010003281.tif 000026
【図１９】
2010003281.tif 000027
【図２０】
2010003281.tif 000028
【図２１】
2010003281.tif 000029
【図２２】
2010003281.tif 000030
【図２３】
2010003281.tif 000031
【図２４】
2010003281.tif 000032
【図２５】
2010003281.tif 000033
【図２６】
2010003281.tif 000034
【図２７】
2010003281.tif 000035
【図２８】
2010003281.tif 000036
【図２９】
2010003281.tif 000037
【図３０】
2010003281.tif 000038
【図３１】
2010003281.tif 000039
【図３２】
2010003281.tif 000040
【図３３】
2010003281.tif 000041
【図３４】
2010003281.tif 000042