(57)【要約】【課題】検証が困難な実行結果が同一になる条件式の組み合わせを含む回路であっても、ハードウェア検証の漏れを防ぎ、バグのないハードウェア設計を実現させること。【解決手段】検証支援装置１００では、検証対象情報の設計情報１１０として入力されたハードウェア記述１０１と仕様書１０２とを用いて、検証対象回路の検証に関する出力情報１２０を生成する。そこで、検証支援装置１００では、ハードウェア記述１０１中から、実行結果が同一になる条件式を含んだ条件分岐記述を抽出すると、実行結果が同一になる各条件式と他の条件式とを含む条件分岐記述を生成する。そして、あらたに生成された条件分岐記述ごとに漏れのない検証を実行するためのアサーション情報１２１を生成する。【選択図】図１
2011237890.tif 000002
【特許請求の範囲】
【請求項１】
条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得工程と、
前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出工程と、
前記抽出工程によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成工程と、
前記作成工程によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成工程と、
前記生成工程によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項２】
前記抽出工程では、前記条件式の組み合わせが抽出されなかった場合、前記ハードウェア記述の中から条件分岐処理を表す条件分岐記述を抽出し、
前記生成工程では、前記抽出工程によって抽出された条件分岐記述において、前記条件の成立を確認するアサーションを生成することを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
前記生成工程では、前記条件として、前記作成工程によって作成された各条件分岐記述の中に含まれている各条件式が、指定された優先度であることを検証するアサーションを生成することを特徴とする請求項１または２に記載の検証支援プログラム。
【請求項４】
前記ハードウェア記述を、前記検証対象回路内の制御の流れを表すＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換工程を前記コンピュータに実行させ、
前記抽出工程では、前記変換工程によって変換されたＣＦＧの中から、前記識別子が付与された条件式の組み合わせを抽出することを特徴とする請求項１〜３のいずれか一つに記載の検証支援プログラム。
【請求項５】
前記出力工程によって出力されたアサーション情報を用いて、前記条件式の組み合わせごとに対応付けられた検証シナリオを実行させた場合の出力値が期待値と等しいか否かに応じて前記検証対象回路を検証する検証工程を前記コンピュータに実行させることを特徴とする請求項１〜４のいずれか一つに記載の検証支援プログラム。
【請求項６】
条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得手段と、
前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出手段と、
前記抽出手段によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成手段と、
前記作成手段によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成手段と、
前記生成手段によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力手段と、
を備えることを検証支援装置。
【請求項７】
取得手段と抽出手段と作成手段と生成手段と出力手段とを備えたコンピュータが、
前記取得手段によって、条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得工程と、
前記抽出手段によって、前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出工程と、
前記作成手段によって、前記抽出工程によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成工程と、
前記生成手段によって、前記作成工程によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成工程と、
前記出力手段によって、前記生成工程によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力工程と、
を実行することを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウェア設計された検証対象回路に対する検証処理を支援する検証支援プログラム、検証支援装置および検証支援方法に関する。
【背景技術】
【０００２】
従来、所望の機能を実現するためハードウェア（回路）を設計した場合には、実際のハードウェア製造に移行する前段階の処理として設計内容に漏れがないかの論理検証を行う作業が必須となる。具体的には、ハードウェアの設計内容に沿った検証シナリオを生成し、この検証シナリオを入力した場合の出力結果を用いて論理検証が行われていた。
【０００３】
また、上述のようにして生成した検証シナリオによる検証処理を客観的に評価するために、検証カバレッジが求められる。検証カバレッジは、検証対象に対するシミュレーション検証のパターンが十分であるか否かの指標を表す情報である。具体的には、たとえば、検証を要するすべてのシミュレーション検証のパターンを母集団とした場合に、実行したシミュレーション検証のパターン数の割合によって求めた網羅率が検証カバレッジとして提供される。この場合、検証カバレッジ（網羅率）が高ければ検証精度も高いと判断される。
【０００４】
ここで問題になるのが、母集団となる“検証を要するシミュレーション検証の全パターン”の抽出の手法である。この母集団に相当するシミュレーション検証の全パターンをカバレッジ基準という。そして、このカバレッジ基準として、実質的に検証に役に立たないパターンを抽出してしまうと、たとえシミュレーション検証の網羅率が高くても実際の検証効率の向上にはつながらない場合がある。
【０００５】
そこで、現在は特定の基準に沿って、網羅的にパターンを抽出するパスカバレッジやコードカバレッジという手法が利用されている。パスカバレッジは、検証対象回路に含まれるレジスタにおいて状態遷移を生じるすべてのパスを検証するためのパターンとする。したがって、パスカバレッジでは、これらのパターンの集合がカバレッジ基準となる。また、コードカバレッジは、ラインカバレッジとも呼ばれ、検証対象回路に相当するソースコードの記述されたレジスタの入出力に関するパスを検証するためのパターンとする。コードカバレッジの場合も、これらのパターンの集合がカバレッジ基準となる。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００６−１９０２０９号公報
【特許文献２】特開２００６−２０１９８０号公報
【非特許文献】
【０００７】
【非特許文献１】Ｈａｒｒｙ．Ｄ．Ｆｏｓｔｅｒ，他２名「Ａｓｓｅｒｔｉｏｎ−Ｂａｓｅｄ Ｄｅｓｉｇｎ」（２ｎｄ Ｅｄｉｔｉｏｎ），「Ｐｒｏｇｒａｍｍｉｎｇ Ｃｏｄｅ ｍｅｔｒｉｃｓ」，ｐｐ．１２９−１３０，２００４
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、上述のようなカバレッジ基準を網羅するような検証シナリオを生成して検証を行った場合にも、実際に回路を動作させると、検証漏れによるバグが発生することがあった。これは、上述したカバレッジ基準が１００％となる検証シナリオであっても、回路内部の分岐条件についての検証を見落としてしまっていたことに起因する。
【０００９】
図２８は、３つの条件式からなる条件分岐例を示す説明図である。ここで、分岐条件についての検証の見落としが発生する場合について説明する。図２８は、条件式Ａ，Ｂ，Ｃという３つの条件式を含んだ条件分岐例である。図２８のような複数の条件式を含む条件分岐の場合、通常、条件式Ｃ＞Ｂ＞Ａといったように条件式同士の優先度が設定されている。
【００１０】
図２９は、アサーションを用いた検証例を示す説明図である。図２９のように、条件分岐記述が優先度の設定を満たしているかを検証するため、隣接する階層関係の条件式同士を組み合わせて、優先度を検証するためのアサーションを生成する。アサーションを生成するには、組み合わせる条件式よりも優先度の高い条件式を否定するような入力を設定する。したがって、具体的には、条件式Ｂと条件式Ａとから下記のようなアサーションｉが
生成される。同様に、条件式Ｃと条件式Ｂとから下記のようなアサーションｉｉが生成さ
れる。
【００１１】
・アサーションｉ  ：ｃｏｖｅｒ（！条件式Ｃａｎｄ（条件式Ｂａｎｄ条件式Ａ））
または
（Ｃ，Ｂ，Ａ）＝（０，１，１）…期待値ｂ
・アサーションｉｉ：ｃｏｖｅｒ（条件式Ｃａｎｄ条件式Ｂ）
または
（Ｃ，Ｂ，Ａ）＝（１，１，０）…期待値ｃ
【００１２】
そして、生成されたアサーションを含んだ検証シナリオを作成して、検証シミュレーションを実行する。そして、検証シミュレーションの実行結果が期待値と一致すれば正常であると判断する。一方、検証シミュレーションの実行結果が期待値と一致しなければ、優先度の設定を満たさないバグがあると判断できる。
【００１３】
図３０は、正しい実装例を示す説明図である。一方、図３１〜図３５は、バグモデル１〜５を示す説明図である。図３０のような条件分岐記述が正しい実装として提供され、優先度として条件式Ｃ＞Ｂ＞Ａという設定がなされている場合、図３１〜図３５に例示するような優先度の異なる条件分岐記述のバグモデル１〜５が発生する可能性がある。
【００１４】
図３６は、各バグモデルの検証例を示す図表である。バグモデル１〜５についても、上述したようなアサーションｉ，ｉｉを生成すれば、バグの有無を検証することができる。
図３６の図表３６００では、条件式Ａ，Ｂ，Ｃへの入力ごとに実装内容に応じた出力の違いを表している。図表３６００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。
【００１５】
アサーションｉを実行することによって図表３６００内の斜線でマーキングを施したブ
ロックの出力を検出することができる。また、アサーションｉｉを実行することによって
図表３６００内の点描でマーキングを施したブロックの出力を検出することができる。したがって、図表３６００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。
【００１６】
一方、矢印３６０１が示す各入力の場合、実装時のバグを見落としてしまう可能性がある。しかしながら、矢印３６０１が示す各入力であっても、全種類の出力（ａ，ｂ，ｃ，ｚ）を網羅していることになる。したがって、上述のパスカバレッジの観点からみると、網羅率は１００％となってしまう。ところが、実際には、上述のように矢印３６０１が示す出力のいずれのバグモデルであっても正しい実装と同じ出力となるため、実装時のバグを見落としてしまう可能性があるといった問題があった。
【００１７】
図３７は、実行結果が同一になる記述例を示す説明図である。さらに、条件分岐記述の実行結果を示す文（たとえば、図２８の文ａ，ｂ，ｃ，ｚ）の記述内容が異なっていても、実行結果が同一になる場合には、さらに、バグを見落としてしまう可能性がある。図３７の記述例１では文ａの記述内容を表しており、記述例２では文ｃの記述内容を表している。
【００１８】
記述例１，２を比較すると、文ａ（ｘ＝α；）と文ｃ（ｔｍｐ＝α；  ｘ＝ｔｍｐ；）とは完全一致ではないが、最終的な出力はｘ＝αとなる。したがって、文ａと文ｃとの実行結果は同一の値となる。上述のような命令自体の記述が異なっても、実行結果が同一になる条件分岐記述では、たとえ、出力からバグが検知された場合であっても、バグの原因を特定できない。また、αが出力された場合に、文ａか文ｃのいずれか一方の検証漏れを判断することができないという問題があった。
【００１９】
１つの側面では、本発明は、３つ以上の条件式を含み、かつ、実行結果が同一になる条件式の組み合わせを含む回路であっても、ハードウェア検証の漏れを抑制することを目的とする。
【課題を解決するための手段】
【００２０】
上述した課題を解決し、目的を達成するため、本開示技術は、条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する処理と、前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する処理と、抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する処理と、作成された条件分岐記述ごとに、任意の条件の成立を確認するアサーションを生成する処理と、生成された各アサーションを前記検証対象回路のアサーション情報として出力する処理と、を含むことを要件とする。
【発明の効果】
【００２１】
３つ以上の条件式を含み、かつ、実行結果が同一になる条件式の組み合わせを含む回路であっても、ハードウェア検証の漏れを抑制することが可能となるという効果を奏する。
【図面の簡単な説明】
【００２２】
【図１】本実施の形態にかかる検証支援処理の一例を示す説明図である。
【図２】実行結果が同一になるため検出不可能であったバグモデルの一例を示す説明図である。
【図３】図２に示したバグモデルの検証結果を示す図表である。
【図４】文ｃと文ａとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。
【図５】文ｂと文ｃとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。
【図６】文ｂと文ａとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。
【図７】検証支援装置のハードウェア構成を示すブロック図である。
【図８】検証支援装置の機能的構成を示すブロック図である。
【図９】検証支援処理の手順を示すフローチャートである。
【図１０】実行結果が同一になる記述の抽出処理を示す説明図である。
【図１１】組み合わせ回路からＣＦＧへの変換例を示す説明図である。
【図１２】実行結果が同一になる記述の分割例を示す説明図である。
【図１３】ＣＦＧの分割例を示す説明図である。
【図１４】分割された条件式｛Ｃ，Ｂ｝の検証例を示す説明図である。
【図１５】条件式｛Ｃ，Ｂ｝のＣＦＧを適用したアサーション生成例を示す説明図である。
【図１６】分割された条件式｛Ａ，Ｂ｝の検証例を示す説明図である。
【図１７】条件式｛Ａ，Ｂ｝のＣＦＧを適用したアサーション生成例を示す説明図である
【図１８】生成したアサーションによるバグの検出例を示す説明図である。
【図１９】文ｃと文ａとの実行結果が同一になる場合のアサーション生成例を示す説明図である。
【図２０】図１９にて生成したアサーションによる検証結果を示す図表である。
【図２１】文ｂと文ｃとの実行結果が同一になる場合のアサーション生成例を示す説明図である。
【図２２】図２１にて生成したアサーションによる検証結果を示す図表である。
【図２３】文ｂと文ａとの実行結果が同一になる場合のアサーション生成例を示す説明図である。
【図２４】図２３にて生成したアサーションによる検証結果を示す図表である。
【図２５】検証支援装置の実装例を示す説明図である。
【図２６】ｃｏｖｅｒ文を用いたシミュレーション検証の実装例を示す説明図である。
【図２７】シミュレーション結果の出力例を示す図表である。
【図２８】３つの条件式からなる条件分岐例を示す説明図である。
【図２９】アサーションを用いた検証例を示す説明図である。
【図３０】正しい実装例を示す説明図である。
【図３１】バグモデル１を示す説明図である。
【図３２】バグモデル２を示す説明図である。
【図３３】バグモデル３を示す説明図である。
【図３４】バグモデル４を示す説明図である。
【図３５】バグモデル５を示す説明図である。
【図３６】各バグモデルの検証例を示す図表である。
【図３７】実行結果が同一になる記述例を示す説明図である。
【発明を実施するための形態】
【００２３】
以下に添付図面を参照して、この発明にかかる検証支援プログラム、検証支援装置および検証支援方法の好適な実施の形態を詳細に説明する。
【００２４】
図１は、本実施の形態にかかる検証支援処理の一例を示す説明図である。図１のように、本実施の形態では、検証支援装置１００は、検証対象情報の設計情報１１０として入力されたハードウェア記述１０１と仕様書１０２とを用いて、検証対象回路の検証に関する出力情報１２０を生成する。なお、図１に示したように、出力情報１２０としてアサーション情報１２１と検証結果１２２とを出力している。実際には、検証結果１２２は、検証支援装置１００内に、アサーション情報１２１を用いたシミュレーション検証を実行する機能部を備えている場合にのみ出力可能となる。
【００２５】
本実施の形態にかかる検証支援処理では、ハードウェア記述１０１中から、実行結果が同一になる条件式を含んだ条件分岐記述を抽出すると、実行結果が同一になる各条件式と他の条件式とを含む条件分岐記述を生成する。そして、あらたに生成された条件分岐記述ごとに漏れのない検証を実行するためのアサーション情報を生成する。そこで、まず、条件分岐記述が表す処理内容と、検証漏れが発生する条件について説明する。
【００２６】
図２は、実行結果が同一になるため検出不可能であったバグモデルの一例を示す説明図である。図２のように、実行結果が同一になる命令（文ａ、文ｃ）を含む条件分岐記述２００において、条件分岐記述２１０のような条件式の優先度に誤り２１１のあるバグモデル（上述したバグモデル４に相当）が提供されたとする。この時点で、検証者は、誤りがあるか否かはわかっていないため、アサーションを利用して、条件分岐記述２１０がバグモデルであるか否かを検証したい。そこで、条件分岐記述２１０の条件式の階層関係の隣接状態から、アサーションｉ，ｉｉを生成する。
【００２７】
図３は、図２に示したバグモデルの検証結果を示す図表である。アサーションｉは、図
３の図表が示す項番２についての検証を行い、アサーションｉｉは、図３の図表が示す項
番３についての検証を行うことができる。アサーションｉでは、いずれの実装も条件式Ｃ
＞Ｂの優先度を満たすためバグは検知されない。もう一方の、アサーションｉｉでは、バ
グモデル４の誤り実装は条件式Ａと条件式Ｃとの優先度が入れ替わっている。本来であれば、正しい実装との実行結果の違いからバグを検知できる。ところが、正しい実装と同一の出力となるため、バグとして検知できない。同様の問題は、他の例でも発生する。
【００２８】
図４は、文ｃと文ａとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。図４の図表４００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表４
００内の斜線でマーキングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行することによって図表４００内の点描でマーキングを施したブロック
の出力を検出することができる。
【００２９】
図表４００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。ところが、文ｃと文ａとの実行結果が同一になるため、誤った実装としてバグモデル３，４が提供されてしまうと、矢印４０１が示すようにバグを検知することができない。
【００３０】
図５は、文ｂと文ｃとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。図５の図表５００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表５
００内の斜線でマーキングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行することによって図表５００内の点描でマーキングを施したブロック
の出力を検出することができる。
【００３１】
図表５００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。ところが、文ｂと文ｃとの実行結果が同一になるため、誤った実装としてバグモデル２が提供されてしまうと、矢印５０１が示すようにバグを検知することができない。
【００３２】
図６は、文ｂと文ａとの実行結果が同一になる記述を含むバグモデルの検証結果を示す図表である。図６の図表６００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表６
００内の斜線でマーキングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行することによって図表６００内の点描でマーキングを施したブロック
の出力を検出することができる。
【００３３】
図表６００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。ところが、文ｂと文Ａａとの実行結果が同一になるため、誤った実装としてバグモデル１が提供されてしまうと、矢印６０１が示すようにバグを検知することができない。
【００３４】
以上説明したように、条件分岐記述内に実行結果が同一になる条件式が含まれている場合、アサーションを生成しても、他の条件式の実行結果が、正しい実装との実行結果が同一になると、たとえバグを含んでいてもバグを含んだ出力との差異が表れない。したがって、検証漏れが発生し、バグの発生を見落としてしまう可能性がある。
【００３５】
そこで、本実施の形態では、実行結果が同一になる条件式を分離して、それぞれあらたな条件分岐記述を作成する。あらたに作成された条件分岐記述には実行結果が同一になる条件式が含まれないため、出力から条件式を辿ることができる。したがって、以下に、本実施の形態にかかる検証支援処理を行う検証支援装置１００の具体的な構成例と処理手順について説明する。
【００３６】
（検証支援装置のハードウェア構成）
つぎに、検証支援装置１００のハードウェア構成について説明する。図７は、検証支援装置のハードウェア構成を示すブロック図である。図７において、検証支援装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）７０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ Ｍｅｍｏｒｙ）７０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）７０３と、磁気ディスクドライブ７０４と、磁気ディスク７０５と、光ディスクドライブ７０６と、光ディスク７０７と、通信Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）７０８と、入力デバイス７０９と、出力デバイス７１０と、を備えている。また、各構成部はバス７２０によってそれぞれ接続されている。
【００３７】
ここで、ＣＰＵ７０１は、検証支援装置１００の全体の制御を司る。ＲＯＭ７０２は、ブートプログラムや、検証支援プログラムなどの各種プログラムを記憶している。ＲＡＭ７０３は、ＣＰＵ７０１のワークエリアとして使用される。磁気ディスクドライブ７０４は、ＣＰＵ７０１の制御にしたがって磁気ディスク７０５に対するデータのリード／ライトを制御する。
【００３８】
磁気ディスク７０５は、磁気ディスクドライブ７０４の制御で書き込まれたデータを記憶する。なお、ＲＯＭ７０２には、検証支援プログラムによって生成されたアサーション情報や、アサーション情報と検証シナリオを用いたシミュレーション検証を実行する検証プログラムが記録されていてもよい。このような場合は、検証支援装置１００によって生成したアサーション情報に留まらず、実際の検証結果まで検証者に提供することができる。
【００３９】
光ディスクドライブ７０６は、ＣＰＵ７０１の制御にしたがって光ディスク７０７に対するデータのリード／ライトを制御する。光ディスク７０７は、光ディスクドライブ７０６の制御で書き込まれたデータを記憶したり、光ディスク７０７に記憶されたデータをコンピュータに読み取らせたりする。
【００４０】
通信インターフェース（以下、「Ｉ／Ｆ」と略する）７０８は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク７１１に接続され、このネットワーク７１１を介して他の装置に接続される。そして、通信Ｉ／Ｆ７０８は、ネットワーク７１１と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。通信Ｉ／Ｆ７０８には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００４１】
入力デバイス７０９は、検証支援装置１００に対しての外部からの入力を受け付ける。入力デバイス７０９としては、具体的には、キーボード、マウスなどが挙げられる。
【００４２】
キーボードの場合、たとえば、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウスの場合、たとえば、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。また、ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４３】
出力デバイス７１０は、検証支援装置１００によって生成された検証シナリオや、検証シナリオによる検証結果などを出力する。出力デバイス７１０としては、具体的には、ディスプレイ、プリンタなどが挙げられる。
【００４４】
ディスプレイの場合、たとえば、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイとしてさらに、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。また、プリンタの場合、たとえば、画像データや文書データを印刷する。さらに、レーザプリンタやインクジェットプリンタを採用することができる。
【００４５】
（検証支援装置の機能的構成）
図８は、検証支援装置の機能的構成を示すブロック図である。検証支援装置１００は、取得部８０１と、抽出部８０２と、作成部８０３と、生成部８０４と、出力部８０５と、変換部８０６と、検証部８０７と、を含む構成である。この制御部となる機能（取得部８０１〜検証部８０７）は、具体的には、たとえば、図７に示したＲＯＭ７０２、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶装置に記憶されたプログラムをＣＰＵ７０１に実行させることにより、または、通信Ｉ／Ｆ７０８により、その機能を実現する。
【００４６】
取得部８０１は、検証対象回路のハードウェア記述１０１を取得する。特に、本実施の形態の場合、条件分岐記述内の実行結果が同一になる条件式同士に所定の識別子が付与されたハードウェア記述１０１を取得する。なお、上述のような識別子が付与されたハードウェア記述１０１は、通常のハードウェア記述に対して、事前に設計者や検証者によって識別子が埋め込まれたものを取得してもよいし、外部のツールを利用して識別子が付与されたものを取得してもよい。また、ハードウェア記述１０１は、識別子に限らず、実行結果が同一になる条件式の組み合わせが特定できるようなマーキングが施されていればよい。取得されたハードウェア記述１０１は、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶される。
【００４７】
抽出部８０２は、ハードウェア記述１０１の中から所定の条件式の組み合わせを抽出する機能を有する。具体的には、抽出部８０２は、取得部８０１によって取得されたハードウェア記述１０１の中から所定の識別子が付与された条件式の組み合わせを抽出する。なお、上述したように、ハードウェア記述１０１の中の実行結果が同一になる条件式の組み合わせに所定の識別子を付与する以外の他の手法によってマーキングが施されている場合には、該当する手法に応じて実行結果が同一になる条件式の組み合わせを抽出する。抽出された条件式の組み合わせは、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶される。
【００４８】
作成部８０３は、指定された条件式を利用した条件分岐記述を作成する機能を有する。具体的には、作成部８０３は、抽出部８０２によって抽出された各条件式について、排他性があると設定された条件式以外の他の条件式と階層関係をなす条件分岐記述を作成する。なお、作成部８０３では、ハードウェア記述１０１の記述順序にしたがって各条件式の階層関係を判断することができる。
【００４９】
したがって、たとえば、図１のような条件式Ａ，Ｂ，Ｃを含んだ条件分岐記述において、実行結果が同一になる条件式の組み合わせとして条件式Ａ，Ｃが抽出された場合、作成部８０３は、条件式Ａ，Ｃとその他の条件式Ａとの階層関係を特定して、あらたに、条件式Ａについて条件式Ａ，Ｂを含んだ条件分岐記述を作成する。同様に、作成部８０３は条件式Ｃについても条件式Ｃ，Ｂを含んだ条件分岐記述を作成する。なお、作成された条件分岐記述は、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶される。
【００５０】
生成部８０４は、作成部８０３によって作成された各条件分岐記述において、あらかじめ指定された所定の条件の成立を検証するアサーションを生成する機能を有する。具体的には、たとえば、生成部８０４は、指定された所定の条件として、作成部８０３によって作成された各条件分岐記述の中に含まれている各条件式が、指定された優先度であることを検証するアサーションを生成する。
【００５１】
その他に、生成部８０４は、抽出部８０２によって抽出された条件式が同時に成立したことを検証するｃｏｖｅｒ文をアサーションとして生成する。生成されたアサーションは、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶される。
【００５２】
また、上述した抽出部８０２では、実行結果が同一になる条件式の組み合わせが抽出されなかった場合には、ハードウェア記述１０１の中から条件分岐処理を表す条件分岐記述を抽出する。すなわち、抽出部８０２は、検証対象として実行結果が同一になる条件式を含まない、通常の条件分岐記述を抽出する。実行結果が同一になる条件式の組み合わせが含まれていない場合には、単純に条件分岐記述の実行結果を検証すればよい。したがって、生成部８０４では、抽出部８０２によって抽出された条件分岐記述において、所定の条件の成立を確認するアサーションを生成する。
【００５３】
出力部８０５は、生成部８０４によって生成された各アサーションを検証対象回路のアサーション情報１２１として出力する機能を有する。出力形式としては、たとえば、ディスプレイへの表示、プリンタへの印刷出力、さらに、通信Ｉ／Ｆ７０８による外部装置への送信がある。また、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶することとしてもよい。
【００５４】
変換部８０６は、ハードウェア記述１０１を、検証対象回路内の制御の流れを表すＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する機能を有する。ハードウェア
記述１０１がＣＦＧに変換された場合、抽出部８０２は、変換部８０６から出力されたＣＦＧの中から識別子が付与された条件式の組み合わせを抽出する。ＣＦＧへの変換には各種専用のツールを利用することができる（公知であるため詳しい説明は省略する）。なお、変換後のＣＦＧは、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶される。
【００５５】
検証部８０７は、出力部８０５によって出力されたアサーション情報１２１を用いた検証処理を実行する機能を有する。具体的には、検証部８０７は、生成部８０４によって生成された条件式の組み合わせごとに対応付けられた検証シナリオの出力値が期待値と等しいか否かに応じて検証対象回路を検証する。検証部８０７によって、実行された検証シナリオの実行結果と、出力値と期待値の比較とは、検証結果１２２として出力される。検証結果１２２の出力形式としては、たとえば、ディスプレイへの表示、プリンタへの印刷出力や通信Ｉ／Ｆ７０８による外部装置への送信がある。また、検証結果１２２は、ＲＡＭ７０３、磁気ディスク７０５、光ディスク７０７などの記憶領域に記憶することとしてもよい。
【００５６】
なお、変換部８０６や検証部８０７に相当する機能部は、必須の構成ではなく、検証支援装置１００の外部に用意してもよい。変換部８０６の機能を外部装置にて実現する構成の場合、検証支援装置１００は、外部装置によって変換されたＣＦＧが入力される構成となる。また、検証部８０７も同様に外部装置によって実行する構成であってもよい。検証部８０７を外部に用意した場合、検証支援装置１００の出力情報１２０としてはアサーション情報１２１が出力される。
【００５７】
（検証支援処理の手順）
図９は、検証支援処理の手順を示すフローチャートである。図９のフローチャートは、検証支援装置１００が、検証対象回路のハードウェア記述１０１を取得して、ハードウェア記述１０１の記述内容に応じて、条件分岐記述の検証を行うためのアサーション情報１２１を出力するまでの手順を示している。図９の各処理を実行することによって、条件分岐記述の構成に応じた適切なアサーション情報１２１が生成されるため、漏れのない検証を実現することができる。
【００５８】
図９において、検証支援装置１００は、まず、取得部８０１によってハードウェア記述１０１を取得したか否かを判断する（ステップＳ９０１）。ステップＳ９０１では、ハードウェア記述１０１を取得するまで待機状態となる（ステップＳ９０１：Ｎｏのループ）。その後、検証支援装置１００は、ハードウェア記述１０１を取得すると（ステップＳ９０１：Ｙｅｓ）、抽出部８０２によって、ハードウェア記述１０１の中から識別子が付与された条件式の組み合わせを抽出する（ステップＳ９０２）。
【００５９】
その後、検証支援装置１００は、ステップＳ９０２によって識別子が付与された条件式の組み合わせが抽出できたか否かを判断する（ステップＳ９０３）。ステップＳ９０３において、識別子が付与された条件式の組み合わせが抽出されると（ステップＳ９０３：Ｙｅｓ）、検証支援装置１００は、作成部８０３によって、抽出された各条件式について、識別子が付与されていない条件式との条件分岐記述を作成する（ステップＳ９０４）。
【００６０】
一方、ステップＳ９０３において、識別子が付与された条件式の組み合わせが抽出されなかった場合（ステップＳ９０３：Ｎｏ）、実行結果が同一となる条件式は含まれていないため、検証支援装置１００は、ステップＳ９０１によって取得したハードウェア記述１０１に含まれる条件分岐記述について通常の検証を行えばよい。したがって、検証支援装置１００は、そのままステップＳ９０５の処理に移行する。
【００６１】
その後、検証支援装置１００は、生成部８０４によって、ステップＳ９０４にて作成された条件分岐記述もしくはステップＳ９０２によって抽出された条件分岐記述において、所定の条件を成立させるアサーションを生成する（ステップＳ９０５）。最後に、検証支援装置１００は、ステップＳ９０５によって生成されたアサーションをアサーション情報１２１として出力部８０５から出力して（ステップＳ９０６）、一連の処理を終了する。
【００６２】
以下には、上述したような機能を備えた検証支援装置１００による検証支援処理の詳細な処理内容について説明する。
【００６３】
（実行結果が同一になる記述の抽出処理）
図１０は、実行結果が同一になる記述の抽出処理を示す説明図である。まず、上述したように検証支援装置１００では、あらかじめ付与された識別子を利用してハードウェア記述１０１の中から条件式の組み合わせを抽出している。ここでは、識別子を付与するための前処理として、仕様書１０２から実行結果が同一になる条件式を抽出するまでの処理を説明する。
【００６４】
まず、仕様書１０２の中からパスと実行結果の関係を抽出する（ステップＳ１００１）。したがって条件分岐記述であれば、パスとして各条件が抽出される。また、各条件と共に、実行結果が紐付いた状態で抽出される。図１０の例では、パスと実行結果の関係を表す、分岐名Ａ，Ｂ，Ｃ、それぞれの実行結果が抽出される。ステップＳ１００１では、たとえば、リスト構造を利用して条件分岐ごとに条件、実行結果（仕様書１０２から抽出する場合には、期待値）を特定して、データ構造として抽出される。
【００６５】
その後、抽出されたパスと実行結果の関係の中から、実行結果が同一になる文を抽出する（ステップＳ１００２）。したがって、ステップＳ１００２によって、分岐名Ｃと分岐名Ａの実行結果は同一（＝α）、分岐名Ｂの実行結果は単一であるという抽出結果が出力される。その後、上述した抽出結果を参照して、ハードウェア記述１０１に対して識別子を付与するなどのマーキングを施せばよい。
【００６６】
（ＣＦＧへの変換処理）
図１１は、組み合わせ回路からＣＦＧへの変換例を示す説明図である。つぎに、図１１を用いてＲＴＬ記述からＣＦＧへの変換について説明する。検証支援装置１００では、ハードウェア記述１０１の組み合わせ回路１１００をＣＦＧ１１１０に変換することによって（ステップＳ１１０１）、後述する分割処理を容易に実現することができる。ＣＦＧ１１１０では、分岐名ごとに、条件式のｔｒｕｅ／ｆａｌｓｅに応じた飛び先が紐付けられている。
【００６７】
（条件分岐記述の分割処理）
図１２は、実行結果が同一になる記述の分割例を示す説明図である。条件分岐記述は、実行結果が同一になる記述が複数個含まれないように分割処理を施す。具体的には、組み合わせ回路１１００内に、実行結果が同一になる記述として条件式Ｃ，Ａがそれぞれ存在する場合、２つの条件式を分離して、残りの条件式との条件分岐記述を作成する。
【００６８】
したがって、組み合わせ回路１１００からは、条件式Ｃと他の条件式（条件式Ａを除く）の組み合わせから構成される条件分岐記述１２０１が生成される。同じく、組み合わせ回路１１００からは、条件式Ａと他の条件式（条件式Ｃを除く）の組み合わせから構成される条件分岐記述１２０２が生成される。
【００６９】
図１３は、ＣＦＧの分割例を示す説明図である。図１２の処理をＣＦＧによって表すと図１３のようになる。すなわち、検証支援装置１００は、実行結果が同一になる文が示された情報１３００によって、ＣＦＧ１１１０を分割して（ステップＳ１３０１）、ＣＦＧ１３１０と、ＣＦＧ１３２０が生成される。ＣＦＧ１３１０は、条件式｛Ａ，Ｂ｝を含んだ条件分岐記述のｔｒｕｅ／ｆａｌｓｅに応じた飛び先を表している。また、ＣＦＧ１３２０は、条件式｛Ｃ，Ｂ｝を含んだ条件分岐記述のｔｒｕｅ／ｆａｌｓｅに応じた飛び先を表している。
【００７０】
（分割された各条件分岐記述の検証処理）
図１４は、分割された条件式｛Ｃ，Ｂ｝の検証例を示す説明図である。検証支援装置１００は、分割された各条件分岐記述について、それぞれ検証処理を行う。そこで、検証支援装置１００は、まず、条件式｛Ｃ，Ｂ｝を含んだ条件分岐記述１２０１について検証処理を行う。
【００７１】
条件分岐記述１２０１の場合、条件式Ｂ，Ｃが成立した場合、それぞれの実行結果ｂ，ｃは異なる値を示す。したがって、条件式Ｃ＞Ｂという優先度を検証するためのアサーションｉすなわち（Ｃ，Ｂ）＝（１，１）を生成することによって、確実にバグを検知する
ことができる。
【００７２】
図１５は、条件式｛Ｃ，Ｂ｝のＣＦＧを適用したアサーション生成例を示す説明図である。ＣＦＧの分割処理によってＣＦＧ１３２０が生成された場合には、上位の分岐から順番にアサーション１５００を生成する（ステップＳ１５０１）。したがって、まず、分岐名Ｃに示された飛び先に基づいて、分岐名Ｃと分岐名Ｂとを成立させるアサーションｉと
して（Ｃ，Ｂ，Ａ）＝（１，１，０）を生成する。つぎに、飛び先の分岐名Ｂに示された飛び先に基づいて、アサーションを生成する。分岐名Ｂの飛び先は終了になるため、分岐名Ｂに関しては実際のアサーションは生成されない。
【００７３】
図１６は、分割された条件式｛Ａ，Ｂ｝の検証例を示す説明図である。検証支援装置１００は、つぎに、条件式｛Ａ，Ｂ｝を含んだ条件分岐記述１２０２について検証処理を行う。条件分岐記述１２０２の場合、条件式Ｂ，Ａが成立した場合、それぞれの実行結果ｂ，ａは異なる値を示す。したがって、条件式Ｂ＞Ａという優先度を検証するためのアサーションｉｉすなわち（Ａ，Ｂ）＝（１，１）を生成することによって、確実にバグを検知
することができる。
【００７４】
図１７は、条件式｛Ａ，Ｂ｝のＣＦＧを適用したアサーション生成例を示す説明図である。ＣＦＧの分割処理によってＣＦＧ１３１０が生成された場合には、上位の分岐から順番にアサーション１７００を生成する（ステップＳ１７０１）。したがって、まず、分岐名Ａに示された飛び先に基づいて、分岐名Ａと分岐名Ｂとを成立させるアサーションｉｉ
として（Ｃ，Ｂ，Ａ）＝（０，１，１）を生成する。つぎに、飛び先の分岐名Ｂに示された飛び先に基づいて、アサーションを生成する。ここでも、分岐名Ｂの飛び先は終了になるため、分岐名Ｂに関しては実際のアサーションは生成されない。なお、以上の説明では、分割後の条件分岐記述１２０１，１２０２の順にアサーションの生成について説明したが、処理順序は問わず、可能であれば並列に処理してもよい。
【００７５】
図１８は、生成したアサーションによるバグの検出例を示す説明図である。図１８の図表１８００は、図１５にて説明したアサーションｉと図１７にて説明したアサーションｉｉとを実行した場合の入力と出力との関係を表している。バグモデル４に相当する、条件
式の優先度に誤り２１１のある条件分岐記述２１０が提供された場合、検証支援装置１００は、従来の検証と同様にアサーションｉ，ｉｉを実行する。
【００７６】
アサーションｉの場合、実装も条件式Ｃ＞Ｂの優先度を満たすため、バグは検知されな
い。一方、アサーションｉｉの場合、正しい実装とバグモデル４の出力が異なるため、条
件式Ａ，Ｂ間の優先度の誤りを検知することができる。
【００７７】
（生成したアサーションのバグモデルへの適用結果）
つぎに、上述の処理によって生成したアサーションのバグモデルへの適用結果について、具体例を挙げて説明する。
【００７８】
＜文ｃと文ａとの実行結果が同一になる場合＞
図１９は、文ｃと文ａとの実行結果が同一になる場合のアサーション生成例を示す説明図である。条件分岐記述１９００は、文ｃと文ａとの実行結果が同一（＝α）になる。したがって、検証支援装置１００では、条件分岐記述１９００の条件式Ｃと条件式Ａとを分離した条件式Ｃ，Ｂに基づいて、アサーション１９０１が生成される。同様に、検証支援装置１００では、条件分岐記述１９００の条件式Ｃと条件式Ａとを分離した条件式Ｂ，Ａに基づいて、アサーション１９０２が生成される。
【００７９】
図２０は、図１９にて生成したアサーションによる検証結果を示す図表である。図表２０００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表２０００内の斜線でマーキ
ングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行す
ることによって図表２０００内の点描でマーキングを施したブロックの出力を検出することができる。
【００８０】
図表２０００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。したがって、図表２０００では、アサーション１９０１，１９０２によってバグモデル１〜５すべてが検知できることを表している。
【００８１】
＜文ｂと文ｃとの実行結果が同一になる場合＞
図２１は、文ｂと文ｃとの実行結果が同一になる場合のアサーション生成例を示す説明図である。条件分岐記述２１００は、文ｂと文ｃとの実行結果が同一（＝α）になる。したがって、検証支援装置１００では、条件分岐記述２１００の条件式Ｃと条件式Ｂとを分離した条件式Ｃ，Ａに基づいて、アサーション２１０１が生成される。同様に、検証支援装置１００では、条件分岐記述２１００の条件式Ｃと条件式Ｂとを分離した条件式Ｂ，Ａに基づいて、アサーション２１０２が生成される。
【００８２】
図２２は、図２１にて生成したアサーションによる検証結果を示す図表である。図表２２００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表２２００内の斜線でマーキ
ングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行す
ることによって図表２２００内の点描でマーキングを施したブロックの出力を検出することができる。
【００８３】
図表２２００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。したがって、図表２２００では、アサーション２１０１，２１０２によってバグモデル１〜５すべてが検知できることを表している。
【００８４】
＜文ｂと文ａとの実行結果が同一になる場合＞
図２３は、文ｂと文ａとの実行結果が同一になる場合のアサーション生成例を示す説明図である。条件分岐記述２３００は、文ｂと文ａとの実行結果が同一（＝α）になる。したがって、検証支援装置１００では、条件分岐記述２３００の条件式Ｂと条件式Ａとを分離した条件式Ｃ，Ｂに基づいて、アサーション２３０１が生成される。同様に、検証支援装置１００では、条件分岐記述２３００の条件式Ｂと条件式Ａとを分離した条件式Ｃ，Ａに基づいて、アサーション２３０２が生成される。
【００８５】
図２４は、図２３にて生成したアサーションによる検証結果を示す図表である。図表２４００の出力を表すブロックのうち、太字で表示されている文字は正しくない出力を表している。そして、アサーションｉを実行することによって図表２４００内の斜線でマーキ
ングを施したブロックの出力を検出することができる。また、アサーションｉｉを実行す
ることによって図表２４００内の点描でマーキングを施したブロックの出力を検出することができる。
【００８６】
図表２４００の出力のうち、斜線もしくは点描でマーキングを施したブロックと太字とが重複するブロックはバグの検出例を表している。したがって、図表２４００では、アサーション２３０１，２３０２によってバグモデル１〜５すべてが検知できることを表している。
【００８７】
以上説明したように、検証支援装置１００では、３つ以上の条件式を含む条件分岐記述の中で実行結果が同一になってしまう場合であっても、実行結果が同一になる条件式同士を分割すればよい。すなわち、条件分岐記述の中から実行結果が同一になる条件式を抽出して、抽出された条件式と、残りの条件式を含んだ条件分岐記述を生成することによって、分割された条件分岐記述が生成される。そして、各条件分岐記述についてそれぞれアサーションを生成すれば、分割前の条件分岐記述に含まれる各条件の実行結果を漏れなく個別に検証することができる。
【００８８】
＜検証支援装置の実装例＞
図２５は、検証支援装置の実装例を示す説明図である。図２５のように、検証支援装置１００は、仕様書１０２から実行結果が同一になる文を抽出する（ステップＳ２５０１）。その後、検証支援装置１００は、ステップＳ２５０１の抽出結果を参照して、実行結果が同一になる文があるか否かを判断する（ステップＳ２５０２）。一方、検証支援装置１００は、並列にＲＴＬ記述によって表された組み合わせ回路１１００をＣＦＧに変換して（ステップＳ２５０３）、ＣＦＧ１１１０として出力する。
【００８９】
さらに、検証支援装置１００は、ステップＳ２５０２の判断結果に応じてＣＦＧ１１１０を用いた処理に移行する。ステップＳ２５０２において、実行結果が同一になる文があると判断された場合（ステップＳ２５０２：Ｙｅｓ）、検証支援装置１００は、ＣＦＧを分割する（ステップＳ２５０４）。ステップＳ２５０４の分割処理において、検証支援装置１００は、条件式Ａ，Ｂ，Ｃを含む条件分岐記述から、条件式｛Ａ，Ｂ｝を含む条件式のＣＦＧ１３１０と、条件式｛Ｃ，Ｂ｝を含む条件式のＣＢＦ１３２０とを作成する。その後、検証支援装置１００は、分割されたＣＦＧ１３１０，１３２０ごとにアサーションを生成し（ステップＳ２５０５）、優先度検証のアサーション２５０６を生成する。
【００９０】
一方、ステップＳ２５０２において、実行結果が同一になる文がないと判断された場合（ステップＳ２５０２：Ｎｏ）、検証支援装置１００は、ＣＦＧ１１１０のアサーションを生成し（ステップＳ２５０５）、優先度検証のアサーション２５０７を生成する。
【００９１】
なお、検証支援装置１００は、ステップＳ２５０５では、アサーション生成処理（ステップ２５１０〜Ｓ２５４０）を行っている。アサーション生成処理において、検証支援装置１００は、まず、条件式の組み合わせをすべて抽出して（ステップＳ２５１０）、条件式間の組み合わせ情報２５１１を生成する。
【００９２】
その後、検証支援装置１００は、条件式間の組み合わせ情報２５１１に対して優先度関係の有無を判別し（ステップＳ２５２０）、優先度有りと判別された条件式の組み合わせ（ＡとＣ，ＣとＢ、ＢとＡの条件式）２５２１を抽出する。続いて、検証支援装置１００は、抽出した条件式の組み合わせ２５２１の中から、同時成立の可能性がある条件式の組み合わせを抽出する（ステップＳ２５３０）。ステップＳ２５３０によってＡとＣ，！ＡとＣとＢの条件式２５３１が抽出される。
【００９３】
そして、検証支援装置１００は、抽出された条件式２５３１について、ｃｏｖｅｒ文を生成することによって（ステップＳ２５４０）、優先度検証のアサーション２５０６もしくはアサーション２５０７が生成される。
【００９４】
以上説明したように、本実装例では、条件分岐処理によって条件分岐記述が所定の条件（３つ以上の条件式を含み、かつ、排他性があると設定されている）を満たす構成か否かを判断する。したがって、検証対象回路の構成に応じてそれぞれ、検証漏れのないアサーション情報１２１を生成することができる。
【００９５】
＜ｃｏｖｅｒ文を用いたシミュレーション検証＞
図２６は、ｃｏｖｅｒ文を用いたシミュレーション検証の実装例を示す説明図である。検証支援装置１００では、検証対象回路において条件分岐記述を検証するアサーション情報１２１が生成されると、検証対象回路のハードウェア記述１０１と、検証シナリオ１１１、期待値１１２、アサーションを表すｃｏｖｅｒ文記述１１３を用いて、シミュレーション検証を行う（ステップＳ２６０１）。
【００９６】
そして、検証支援装置１００は、ステップＳ２６０１によるシミュレーション検証後に、シミュレーション出力が期待値１１２と等しいか否かの判断を行う（ステップＳ２６０２）。ステップＳ２６０２によって、シミュレーション出力が期待値１１２と等しいと判断された場合（ステップＳ２６０２：Ｙｅｓ）、検証支援装置１００は、そのままステップＳ２６０３の処理に移行する。一方、検証支援装置１００は、シミュレーション出力が期待値１１２と等しくないと判断された場合（ステップＳ２６０２：Ｎｏ）、ハードウェア記述１０１に期待値１１２通りに動作しない原因となるバグがあると判断する（ステップＳ２６０５）。
【００９７】
検証支援装置１００は、シミュレーション出力が期待値１１２と等しいと判断した場合（ステップＳ２６０２：Ｙｅｓ）には、さらに、ｃｏｖｅｒ文記述１１３の処理が成立するか否かを判断する（ステップＳ２６０３）。そして、検証支援装置１００は、ｃｏｖｅｒ文記述１１３の処理が成立する場合（ステップＳ２６０３：Ｙｅｓ）、検証シナリオ１１１を実行した場合に、同時成立箇所も含めて期待値１１２通りの動作が実行されたと判断する（ステップＳ２６０４）。
【００９８】
一方、ステップＳ２６０３において、ｃｏｖｅｒ文記述１１３の処理が成立しない場合（ステップＳ２６０３：Ｎｏ）、検証支援装置１００は、検証シナリオ１１１を実行した場合に、期待値１１２通りの動作が実行されたが、同時成立箇所は未検証であると判断する（ステップＳ２６０６）。同時成立箇所は未検証であるとは、すなわち、検証シナリオ１１１の不足を意味する。したがって、検証者は、未検証箇所を検証するための検証シナリオ１１１を用意することによって、検証精度を向上させることができる。
【００９９】
図２７は、シミュレーション結果の出力例を示す図表である。図２６にて説明したシミュレーション検証の結果に応じた出力例に応じて、それぞれ図表２７００のように判定される。検証者は、この判定結果を参照して、検証シナリオの漏れを特定し、不足している検証シナリオを補完することによって、真の網羅率１００％となる検証カバレッジを実現することができる。
【０１００】
以上説明したように、検証支援プログラム、検証支援装置および検証支援方法によれば、実行結果が同一になる条件式同士をそれぞれ独立させた条件分岐記述を作成して、アサーション情報１２１を生成する。したがって、検証支援装置１００は、発生する可能性のあるバグモデルを残すことなく検出可能となり、高精度な検証を実現することができる。
【０１０１】
また、上記技術では、ハードウェア記述１０１の中から実行結果が同一になる条件式の組み合わせが抽出できなかった場合には、実行結果が同一になるような条件式は含まれていないと判断することができる。したがって、検証支援装置１００は、不必要な抽出処理が排除されるため処理効率を向上させることができる。
【０１０２】
また、上記技術では、指定された条件として、検証支援装置１００においてあらたに作成された各条件分岐記述の中に含まれている各条件式が、指定された優先度であることを検証するアサーションを生成する機能を備えることもできる。したがって、検証支援装置１００は、優先度の設定を満たし、検証漏れのないシミュレーション検証を実行するためのアサーション情報１２１を生成することができる。
【０１０３】
また、上記技術では、さらに、検証対象回路のハードウェア記述１０１を、回路内の制御の流れを表すＣＦＧ（Ｃｏｎｔｒｏｌ Ｆｌｏｗ Ｇｒａｐｈ）に変換して、ＣＦＧを対象に条件分岐記述を抽出することもできる。したがって、検証支援装置１００は、ＣＦＧを利用することによってハードウェア記述１０１を対象とする場合に増して、処理負荷が少なく高速に条件分岐記述を抽出することができる。
【０１０４】
また、上記技術では、抽出された条件式が同時に成立したことを検証するｃｏｖｅｒ文をアサーションとして生成することもできる。したがって、検証支援装置１００は、設定された条件の成立を確認するためのアサーション情報１２１を自動的に生成することができる。
【０１０５】
また、上記技術では、出力されたアサーション情報１２１を用いて、検証シナリオ１１１を実行させた際の出力値が期待値１１２と等しいか否かを判断する機能を備えることもできる。したがって、検証支援装置１００は、検証対象回路の動作を自動的に検証することもできる。
【０１０６】
なお、本実施の形態で説明した検証支援方法は、あらかじめ用意されたプログラムをパーソナル・コンピュータやワークステーションなどのコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤなどのコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムは、インターネットなどのネットワークを介して配布してもよい。
【０１０７】
また、本実施の形態で説明した検証支援装置１００は、スタンダードセルやストラクチャードＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）などの特定用途向けＩＣ（以下、単に「ＡＳＩＣ」と称す。）やＦＰＧＡなどのＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）によっても実現することができる。具体的には、たとえば、上述した検証支援装置１００の機能（取得部８０１〜検証部８０７）をＨＤＬ記述によって機能定義し、そのＨＤＬ記述を論理合成してＡＳＩＣやＰＬＤに与えることにより、検証支援装置１００を製造することができる。
【０１０８】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０１０９】
（付記１）条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得工程と、
前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出工程と、
前記抽出工程によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成工程と、
前記作成工程によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成工程と、
前記生成工程によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１１０】
（付記２）前記抽出工程では、前記条件式の組み合わせが抽出されなかった場合、前記ハードウェア記述の中から条件分岐処理を表す条件分岐記述を抽出し、
前記生成工程では、前記抽出工程によって抽出された条件分岐記述において、前記条件の成立を確認するアサーションを生成することを特徴とする付記１に記載の検証支援プログラム。
【０１１１】
（付記３）前記生成工程では、前記条件として、前記作成工程によって作成された各条件分岐記述の中に含まれている各条件式が、指定された優先度であることを検証するアサーションを生成することを特徴とする付記１または２に記載の検証支援プログラム。
【０１１２】
（付記４）前記ハードウェア記述を、前記検証対象回路内の制御の流れを表すＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換工程を前記コンピュータに実行させ、
前記抽出工程では、前記変換工程によって変換されたＣＦＧの中から、前記識別子が付与された条件式の組み合わせを抽出することを特徴とする付記１〜３のいずれか一つに記載の検証支援プログラム。
【０１１３】
（付記５）前記生成工程は、前記抽出工程によって抽出された各条件式を同時に成立させるｃｏｖｅｒ文を前記アサーションとして生成することを特徴とする付記１〜４のいずれか一つに記載の検証支援プログラム。
【０１１４】
（付記６）前記出力工程によって出力されたアサーション情報を用いて、前記条件式の組み合わせごとに対応付けられた検証シナリオを実行させた場合の出力値が期待値と等しいか否かに応じて前記検証対象回路を検証する検証工程を前記コンピュータに実行させることを特徴とする付記１〜５のいずれか一つに記載の検証支援プログラム。
【０１１５】
（付記７）条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得手段と、
前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出手段と、
前記抽出手段によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成手段と、
前記作成手段によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成手段と、
前記生成手段によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力手段と、
を備えることを検証支援装置。
【０１１６】
（付記８）取得手段と抽出手段と作成手段と生成手段と出力手段とを備えたコンピュータが、
前記取得手段によって、条件分岐記述内の実行結果が同一になる条件式同士に識別子が付与された検証対象回路のハードウェア記述を取得する取得工程と、
前記抽出手段によって、前記ハードウェア記述の中から前記識別子が付与された条件式の組み合わせを抽出する抽出工程と、
前記作成手段によって、前記抽出工程によって抽出された条件式の組み合わせの各条件式について、前記組み合わせ以外の条件式と階層関係をなす条件分岐記述を、前記ハードウェア記述の記述順序にしたがって作成する作成工程と、
前記生成手段によって、前記作成工程によって作成された条件分岐記述ごとに、条件の成立を確認するアサーションを生成する生成工程と、
前記出力手段によって、前記生成工程によって生成された各アサーションを前記検証対象回路のアサーション情報として出力する出力工程と、
を実行することを特徴とする検証支援方法。
【符号の説明】
【０１１７】
１００  検証支援装置
１０１  ハードウェア記述
１０２  仕様書
１１１  検証シナリオ
１１２  期待値
１１３  ｃｏｖｅｒ文記述
１２１  アサーション情報
１２２  検証結果
８０１  取得部
８０２  抽出部
８０３  作成部
８０４  生成部
８０５  出力部
８０６  変換部
８０７  検証部
【図１】
2011237890.tif 000003
【図２】
2011237890.tif 000004
【図３】
2011237890.tif 000005
【図４】
2011237890.tif 000006
【図５】
2011237890.tif 000007
【図６】
2011237890.tif 000008
【図７】
2011237890.tif 000009
【図８】
2011237890.tif 000010
【図９】
2011237890.tif 000011
【図１０】
2011237890.tif 000012
【図１１】
2011237890.tif 000013
【図１２】
2011237890.tif 000014
【図１３】
2011237890.tif 000015
【図１４】
2011237890.tif 000016
【図１５】
2011237890.tif 000017
【図１６】
2011237890.tif 000018
【図１７】
2011237890.tif 000019
【図１８】
2011237890.tif 000020
【図１９】
2011237890.tif 000021
【図２０】
2011237890.tif 000022
【図２１】
2011237890.tif 000023
【図２２】
2011237890.tif 000024
【図２３】
2011237890.tif 000025
【図２４】
2011237890.tif 000026
【図２５】
2011237890.tif 000027
【図２６】
2011237890.tif 000028
【図２７】
2011237890.tif 000029
【図２８】
2011237890.tif 000030
【図２９】
2011237890.tif 000031
【図３０】
2011237890.tif 000032
【図３１】
2011237890.tif 000033
【図３２】
2011237890.tif 000034
【図３３】
2011237890.tif 000035
【図３４】
2011237890.tif 000036
【図３５】
2011237890.tif 000037
【図３６】
2011237890.tif 000038
【図３７】
2011237890.tif 000039