(57)【特許請求の範囲】
【請求項１】
検証対象への入力群のベクトルが必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得させる取得工程と、
前記取得工程によって取得された論理式を用いて、前記検証対象への入力群のベクトルと、前記検証対象からの出力または／および前記検証対象の入出力に応じて状態遷移にする有限状態機械の状態変数からなる変数群のベクトルとにより、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出させる優先条件算出工程と、
前記入力制約条件を表現する論理式と、前記優先条件算出工程によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力群のベクトルのパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記変数群のベクトルの値割り当てにおける前記検証対象への入力群のベクトルのパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築させる構築工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項２】
前記構築工程は、
前記入力制約条件を表現する論理式に基づいて、前記基本パターンを発生させる基本パターン発生器の動作を表現する論理式を算出させる基本パターン発生器算出工程と、
前記優先条件を表現する論理式に基づいて、前記優先パターンを発生させる優先パターン発生器の動作を表現する論理式を算出させる優先パターン発生器算出工程と、を含み、
前記基本パターン発生器算出工程によって算出された論理式と前記優先パターン発生器算出工程によって算出された論理式とに基づいて、前記パターン発生器を構築させることを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
請求項１または２に記載の論理検証プログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項４】
検証対象への入力群のベクトルが必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得する取得手段と、
前記取得手段によって取得された論理式を用いて、前記検証対象への入力群のベクトルと、前記検証対象からの出力または／および前記検証対象の入出力に応じて状態遷移にする有限状態機械の状態変数からなる変数群のベクトルとにより、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出する優先条件算出手段と、
前記入力制約条件を表現する論理式と、前記優先条件算出手段によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力群のベクトルのパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記変数群のベクトルの値割り当てにおける前記検証対象への入力群のベクトルのパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築する構築手段と、
を備えることを特徴とする検証支援装置。
【請求項５】
取得手段、優先条件算出手段、および構築手段を備えるコンピュータが、
前記取得手段により、検証対象への入力群のベクトルが必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得する取得工程と、
前記優先条件算出手段により、前記取得工程によって取得された論理式を用いて、前記検証対象への入力群のベクトルと、前記検証対象からの出力または／および前記検証対象の入出力に応じて状態遷移にする有限状態機械の状態変数からなる変数群のベクトルとにより、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出する優先条件算出工程と、
前記構築手段により、前記入力制約条件を表現する論理式と、前記優先条件算出工程によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力群のベクトルのパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記変数群のベクトルの値割り当てにおける前記検証対象への入力群のベクトルのパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築する構築工程と、
を実行することを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、ハードウェアの論理検証を支援する検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法にかかり、特に、モジュール単位で実施する論理シミュレーションの環境構築を支援する検証支援装置、検証支援方法、および検証支援プログラムに関する。
【背景技術】
【０００２】
従来、一般に、ハードウェアモジュールは仕様で規定された範囲の入力パターンを受け取ったときに正しく動作するように作られており、もともと許されない入力パターンを受け取った場合の動作は規定されない。したがって、モジュール単位で論理シミュレーションを行なう場合はモジュールへの入力パターンを仕様で定められた範囲内に保つ必要があり、そうしなければ意味のあるシミュレーション結果が得られない。
【０００３】
入力パターンの作成には、事前に人手で作成しておいたパターンを用いる場合や、シミュレーションしながら動的に自動生成するパターン発生器を用いる場合、あるいはそれらを組み合わせる場合などがある。
【０００４】
通常、パターン発生器はＣ、ＳｙｓｔｅｍＣ、Ｖｅｒｉｌｏｇ、ＶＨＤＬなどの言語を使って人手で作成されている。これに対して近年、フォーマルな入力制約条件に関する記述からパターン発生器を自動生成する技術も知られるようになった（たとえば、下記非特許文献１を参照。）。入力制約条件とは、検証対象となるハードウェアモジュールに送られる入力が必ず満たさなければならない条件のことである。ここで、非特許文献１のようにフォーマルな入力制約に関する記述からパターン発生器を自動生成する例について説明する。
【０００５】
図１４は、検証対象となるハードウェアモジュールの一例を示す説明図である。図１４において、検証対象１４００はｃｌｋをクロック入力とする順序回路であり、１ビット入力ｃｍｄおよびｒｅｑ、１ビット出力ａｃｋ、３２ビット入力ｗｄ、および３２ビット出力ｒｄを持っている。この検証対象の入力に関しては次の入力制約条件がある。
【０００６】
・ｃｍｄ＝０かつｒｅｑ＝１を入力したらＲｅａｄ動作が始まり、ａｃｋ＝１の応答によってＲｅａｄ動作が終了するまでｃｍｄとｒｅｑの値を変更してはならない。
・ｃｍｄ＝１かつｒｅｑ＝１を入力したらＷｒｉｔｅ動作が始まり、ａｃｋ＝１の応答によってＷｒｉｔｅ動作が終了するまでｃｍｄ、ｒｅｑ、およびｗｄの値を変更してはならない。
【０００７】
この例のように、一般に入力制約条件は検証対象１４００におけるその時刻の入出力値だけでなく、過去の入出力値にも依存する。そこで、入力制約が守られているかどうかを判定する仕組みを導入する。
【０００８】
図１５は、入力制約条件を定義するモデルを示す説明図である。図１５では、入力制約条件が守られているかどうかを判定する仕組みを順序機械Ｍ0と入力制約条件に対応する論理式Ｃ0を使ったモデル化がおこなわれている。順序機械Ｍ0は状態変数ｓおよび状態変数ｔを持つ。状態変数ｓおよび状態変数ｔは検証対象１４００（順序回路）の動作状態や入出力値をあらわす変数である。
【０００９】
図１６は、状態変数ｓの値変化を表現した状態遷移グラフを示す説明図である。ｓ＝０は初期状態、ｓ＝１はＲｅａｄ動作中の状態、ｓ＝２はＷｒｉｔｅ動作中の状態に対応する。一方、状態変数ｔは常に１サイクル前のｗｄの値を保持している。入力制約は順序機械Ｍ0の状態変数ｓおよび状態変数ｔと検証対象の入出力値を用いて次の式（１）に示す論理式Ｃ0で表現される。
【００１０】
【数１】
0004759392.tif 000002
【００１１】
入力制約の論理式Ｃ0を出発点として、パターン発生器（Ｇ0）を自動生成することができる。図１７は、入力制約条件の論理式Ｃ0を出発点として自動生成されたパターン発生器（Ｇ0）を示す説明図である。図１７に示したパターン発生器（Ｇ0）は、以下の論理式（２）〜（４）に示した動作をする。
【００１２】
ｃｍｄ←（ｓ＝１）？０：（ｓ＝２）？１：ｒａｎｄｏｍ（１）・・・・・・・・（２）
ｒｅｑ←（（ｓ＝１）＋（ｓ＝２））？１：ｒａｎｄｏｍ（１）・・・・・・・・（３）
ｗｄ←（ｓ＝２）？ｔ：ｒａｎｄｏｍ（３２）・・・・・・・・・・・・・・・・（４）
【００１３】
ここで、論理式「ｘ？ｙ：ｚ」は条件ｘが成立するとき値ｙを持ち成立しないとき値ｚを持つ３項演算であり、下記論理式（５）と等価である。また、「ｒａｎｄｏｍ（ｎ）」はビット幅ｎのランダム値を発生させる関数である。たとえば、式（４）を例に挙げると、検証対象がＷｒｉｔｅ動作中の場合、ｗｄはｔの値を持ち、Ｗｒｉｔｅ動作中でない場合、３２ビットのランダム値を持つ。
【００１４】
【数２】
0004759392.tif 000003
【００１５】
ここで、パターン発生器（Ｇ0）の動作を決める一般的な手順について説明する。検証対象の入力群はｎビットの＜ｙ＞＝（ｙ１，ｙ２，…，ｙｎ）で構成される。また、その他の変数群（検証対象の出力や検証対象に付加した順序機械の状態変数）はｍビットの＜ｘ＞＝（ｘ１，ｘ２，…，ｘｍ）で構成される。＜ｘ＞，＜ｙ＞は、それぞれカッコ内の変数からなるベクトルである。
【００１６】
入力制約として与えられる論理式は、＜ｘ＞と＜ｙ＞の論理関数ｆと等価であるとする。これに対して、目的のパターン発生器（Ｇ0）は下記の形で構成することができる。
【００１７】
【数３】
0004759392.tif 000004
【００１８】
ここで、ｒ1，ｒ2，…，ｒnはここで新たに導入した論理変数であり、ランダムに０または１の値を取るものとする。論理関数群ｇ1，ｇ2，…，ｇnは次の手順［１］〜［５］で求められる。
【００１９】
［１］  ｙ2，…，ｙnには何らかの適切な値を設定する仮定の下で簡単化した制約条件を求める。この制約条件は下記式（６）の通りである。
【００２０】
【数４】
0004759392.tif 000005
【００２１】
［２］  式（６）への定数代入により、ｙ1に値０を出力できる条件およびｙ１に値１を出力できる条件を求める。それらを用いて、ｙ１に０を出力できるが１を出力できないときは値０、１を出力できるが０を出力できないときは値１、それ以外のときはランダム値ｒ1に等しい値を持つように、下記式（７）の論理関数ｇ1を構成する。
【００２２】
【数５】
0004759392.tif 000006
【００２３】
［３］  ｙ1には式（７）の論理関数ｇ1の値を使用し、ｙ3，…，ｙnには何らかの適切な値を設定する仮定の下で簡単化した制約条件を求める。この制約条件は下記式（８）の通りである。
【数６】
0004759392.tif 000007
【００２４】
［４］  ［２］と同様にしてあらたな論理関数ｇ2を求める。この論理関数ｇ2は下記式（９）の通りである。
【００２５】
【数７】
0004759392.tif 000008
【００２６】
［５］  以降も同様にして、論理関数ｇnまで求める。ここで、演算∃ｖ．ｆは「論理関数ｆの値を１にするようなｖの値割り当てが存在するための、残りの変数に関する条件」を正確に求める演算である。変数ｖiが１ビットの論理変数であるとき、∃演算は次のように定義される。
【００２７】
【数８】
0004759392.tif 000009
【００２８】
変数ｖiが値集合Ｖを持つ多値変数であるときは、∃演算は次のように定義される。
【００２９】
【数９】
0004759392.tif 000010
【００３０】
変数群（ｙ1，…，ｙm）に関する∃演算は、次のように定義される。
【００３１】
【数１０】
0004759392.tif 000011
【００３２】
なお、∃演算は二分決定グラフ（ＢＤＤ）等の技術により計算機上で効率的に実行できることが広く知られている。上記式（１）におけるｗｄのように多ビット入力変数を含んだ論理式を出発点とする場合は、それをビット毎に分割した式（１３）のように書き換えてから取り扱えば良い。
【００３３】
【数１１】
0004759392.tif 000012
【００３４】
あるいは別の方法として、ｗｄ＝ｔの関係が成り立つことを示す１ビット変数ｗｄ＿ｔを導入して次の形に書き換えることもできる。
【００３５】
【数１２】
0004759392.tif 000013
【００３６】
以下に、上記式（６）を出発点として上記式（２）〜（４）の右辺に相当する論理関数ｇ1，ｇ2，ｇ3を求める例を以下の［１］〜［６］に示す。
【００３７】
［１］  ｒｅｑとｗｄ＿ｔには何らかの適切な値を設定する前提の下で簡単化した制約条件ｆ’（ｓ，ｃｍｄ）を求める。この制約条件ｆ’（ｓ，ｃｍｄ）は下記式（１５）の通りである。
【００３８】
【数１３】
0004759392.tif 000014
【００３９】
［２］  制約条件ｆ’（ｓ，ｃｍｄ）への定数代入により、ｃｍｄに値０を出力できる条件ｆ’（ｓ，０）およびｃｍｄに値１を出力できる条件ｆ’（ｓ，１）を求める。それらを用いて、ｃｍｄに０を出力できるが１を出力できないときは値０、１を出力できるが０を出力できないときは値１、それ以外のときはランダム値ｒ1に等しい値を持つように、論理関数ｇ1（ｓ，ｒ1）を構成する。これらの条件ｆ’（ｓ，０）、条件ｆ’（ｓ，１）、および論理関数ｇ1（ｓ，ｒ1）は下記式（１６）〜（１８）の通りである。
【００４０】
【数１４】
0004759392.tif 000015
【００４１】
［３］  ｃｍｄには論理関数ｇ1（ｓ，ｒ1）の値を使用するとし、ｗｄ＿ｔには何らかの適切な値に設定する前提の下での制約条件ｆ”（ｓ，ｒ1，ｒｅｑ）を求める。この制約条件ｆ”（ｓ，ｒ1，ｒｅｑ）は下記式（１９）の通りである。
【００４２】
【数１５】
0004759392.tif 000016
【００４３】
［４］  制約条件ｆ”（ｓ，ｒ1，ｒｅｑ）への定数代入により、ｒｅｑに値０を出力できる条件ｆ”（ｓ，ｒ1，０）、およびｒｅｑに値１を出力できる条件ｆ”（ｓ，ｒ1，１）を求める。それらを用いて、ｒｅｑに０を出力できるが１を出力できないときは値０、１を出力できるが０を出力できないときは値１、それ以外のときはランダム値ｒ2に等しい値を持つように、論理関数ｇ2（ｓ，ｒ1，ｒ2）を構成する。これらの条件条件ｆ”（ｓ，ｒ1，０）、条件ｆ”（ｓ，ｒ1，１）、および論理関数ｇ2（ｓ，ｒ1，ｒ2）は、下記式（２０）〜（２２）の通りである。
【００４４】
【数１６】
0004759392.tif 000017
【００４５】
［５］  ｃｍｄには論理関数ｇ1（ｓ，ｒ1）、ｒｅｑには論理関数ｇ2（ｓ，ｒ1，ｒ2）の値を使用するときの制約条件ｆ'''（ｓ，ｒ1，ｒ2，ｗｄ＿ｔ）を求める。この制約条件ｆ'''（ｓ，ｒ1，ｒ2，ｗｄ＿ｔ）は、下記式（２３）の通りである。
【００４６】
【数１７】
0004759392.tif 000018
【００４７】
［６］  制約条件ｆ'''（ｓ，ｒ1，ｒ2，ｗｄ＿ｔ）への定数代入により、ｗｄ＿ｔに値０を出力できる条件ｆ'''（ｓ，ｒ1，ｒ2，０）、およびｗｄ＿ｔに値１を出力できる条件ｆ'''（ｓ，ｒ1，ｒ2，１）を求める。それらを用いて、ｗｄ＿ｔに０を出力できるが１を出力できないときは値０、１を出力できるが０を出力できないときは値１、それ以外のときはランダム値ｒ3に等しい値を持つように、論理関数ｇ3（ｓ，ｒ1，ｒ2，ｒ3）を構成する。これらの条件ｆ'''（ｓ，ｒ1，ｒ2，０）、条件ｆ'''（ｓ，ｒ1，ｒ2，１）、および論理関数ｇ3（ｓ，ｒ1，ｒ2，ｒ3）は、下記式（２４）〜（２６）の通りである。
【００４８】
【数１８】
0004759392.tif 000019
【００４９】
１ビット変数であるｃｍｄおよびｒｅｑには、それぞれｇ1とｇ2の値をそのまま代入すれば良い。このとき、変数ｒ1、ｒ2の値はランダム値生成関数ｒａｎｄｏｍ（１）を使って毎回新しく生成するようにする。
【００５０】
３２ビット変数ｗｄについてはｇ3に基づいて、ｗｄ＿ｔすなわちｇ3の値が０になるケースではｔ以外の３２ビットランダム値を代入し、ｇ3の値が１になるケースではｔの値をそのまま代入し、ｇ3の値がランダム値になるケースでは任意の３２ビットランダム値を代入すれば良い。これにより、パターン発生器（Ｇ0）の動作を表現する論理式Ｇ0（下記式（２７）〜（２９））を得ることができる。
【００５１】
【数１９】
0004759392.tif 000020
【００５２】
【非特許文献１】ジュン・ユアン、ケン・アルビン、アドナン・アジズ、カール・ピクスレイ（J. Yuan, Ken Albin, Adnan Aziz, and Carl Pixley）著,  「コンストレイント  シンセシス  フォー  エンビロンメント  モデリング  イン  ファンクショナル  ベリフィケーション （Constraint Synthesis for Environment Modeling in Functional Verification）」, in Proc. デザイン  オートメーション  カンファレンス出版（Design Automation Conference） 2003, pp. 296.299, 2003.
【発明の開示】
【発明が解決しようとする課題】
【００５３】
論理検証環境の作成者には、次の２つの異なるタイプの要求に対するバランスを考慮して、入力パターンを作成もしくは自動生成することが求められている。
（ｉ）特別な状況を狙い撃ちでテストしたい。
（ii）可能な限り広範囲の状況をテストしたい。
【００５４】
たとえば、割り込みや例外処理が発生する状況など、設計誤りがありそうな状況を優先的にカバーしたいという要求が（ｉ）であり、普通では思い付かないような考え抜けを発見したいという要求が（ii）である。
【００５５】
（ii）の要求を満足するには非常に多くのパターンを作成もしくは自動生成する必要がある。人手では大量なパターンを作成することができないため、通常、人手で作成できるのは（ｉ）の要求に対するパターンに限られる。
【００５６】
パターン発生器を用いれば、大量なパターンを自動生成することができたが、（ii）の要求に応えるためには単にパターンの量が多いだけでなく、その分布が仕様で定められた範囲を網羅していることが重要である。そのようなパターン発生器を作成するには仕様情報を詳細に理解し、それをパターン発生器の構成に反映させる必要がある。
【００５７】
しかしながら、そのようなパターン発生器の作成作業には工数がかかり、間違いも多く、また、仕様変更や仕様の誤解があった場合の手戻り工数も大きい。したがって、『（ii）可能な限り広範囲の状況をテストしたい。』という要求を満たすことができないという問題があった。
【００５８】
一方、上記非特許文献１のような従来技術を用いれば、（ii）の要求を満たしたパターン発生器を仕様記述（入力制約）から誤りなく自動生成することができ、仕様の変更や修正にも簡単に対応することができる。
【００５９】
しかしながら、上記非特許文献１のような従来技術には（ｉ）の要求を考慮する仕組みが含まれておらず、パターンの発生順序はユーザの意図しない乱数によって決められてしまうことになる。したがって、現在のハードウェア設計の検証では、論理シミュレーションですべての入力パターンをテストすることは、必要なパターン数が多すぎるため不可能である。
【００６０】
現在のハードウェア設計の検証では、どのような順序でパターンを発生させるか、あるいはどのような分布でパターンを発生させるかを制御することが重要であるが、上記非特許文献１のような従来技術では、そのような制御をすることができない。したがって、『（ｉ）特別な状況を狙い撃ちでテストしたい。』という要求を満たすことができないという問題があった。
【００６１】
この発明は、上述した従来技術による問題点を解消するため、特別な状況を狙い撃ちでテストしつつ、可能な限り広範囲の状況をテストすることができる検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【００６２】
上述した課題を解決し、目的を達成するため、この発明にかかる検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法は、検証対象への入力が必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得し、取得された論理式を用いて、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出し、前記入力制約条件を表現する論理式と、算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力のパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記検証対象への入力のパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築することを特徴とする。
【００６３】
この発明によれば、優先条件を考慮したパターン発生器の動作を表現する論理式を得ることができる。
【００６４】
また、上記発明において、前記入力制約条件を表現する論理式に基づいて、前記基本パターンを発生させる基本パターン発生器の動作を表現する論理式を算出し、前記優先条件を表現する論理式に基づいて、前記優先パターンを発生させる優先パターン発生器の動作を表現する論理式を算出し、算出された論理式と前記優先パターン発生器算出手段によって算出された論理式とに基づいて、前記パターン発生器を構築することとしてもよい。
【００６５】
この発明によれば、基本パターン発生器と優先パターン発生器との機能を明確に分割することができる。
【００６６】
また、上記発明において、前記優先検証動作が複数存在する場合に、ユーザによって指定された前記優先検証動作の優先順位を取得し、さらに、前記取得手段によって取得された前記優先検証動作の優先順位に従って前記優先パターンが発生するように、前記パターン発生器を構築することとしてもよい。
【００６７】
この発明によれば、優先順位の変更を容易におこなうことができる。
【００６８】
また、上記発明において、前記優先検証動作が複数存在する場合、前記各優先検証動作に応じた各優先条件を表現する論理式の論理積を算出し、前記入力制約条件を表現する論理式と、算出された論理積とに基づいて、前記基本パターンと前記各優先パターンとを選択的に発生させるパターン発生器を構築することとしてもよい。
【００６９】
この発明によれば、複数の優先条件を同時に満足する優先条件を用いることで、優先パターン発生器の数を低減して、構築されるパターン発生器の内部構成を簡略化することができる。
【００７０】
また、上記発明において、前記入力制約条件を表現する論理式は、前記検証対象の入出力と前記検証対象の入出力に応じて状態遷移する有限状態機械の状態変数とを用いた論理式であり、前記優先条件を表現する論理式は、前記検証対象への入力群と、前記検証対象からの出力または／および前記有限状態機械の状態変数からなる変数群とを用いた論理式であることとしてもよい。
【００７１】
この発明によれば、過去の入出力の値を考慮して、優先条件付きのパターン発生器を構築することができる。
【００７２】
また、上記発明において、前記入力群と前記変数群とを用いた論理式に基づいて、前記優先条件が満たされる場合に前記変数群によって特定される前記優先パターンの選択条件を表現する論理式を算出し、算出された前記優先パターンの選択条件を表現する論理式の値に応じて前記基本パターンと前記優先パターンとを選択的に発生させるパターン発生器を構築することとしてもよい。
【００７３】
この発明によれば、基本パターン発生器からの基本パターン、すべての優先パターン発生器からのすべての優先パターンについて、自動的に優先順序をつけることができる。
【００７４】
また、上記発明において、前記入力群と前記変数群とを用いた論理式に基づいて、前記優先条件が満たされる場合に前記変数群によって特定される前記優先パターンの選択条件を表現する論理式を算出し、前記入力制約条件を表現する論理式と、前記優先条件を表現する論理式と、前記優先パターンの選択条件を表現する論理式とに基づいて、前記入力制約条件および前記優先条件を満たす優先条件付制約論理式を算出し、算出された優先条件付制約論理式に基づいて、前記基本パターンと前記優先パターンとを選択的に発生させるパターン発生器を構築することとしてもよい。
【００７５】
この発明によれば、入力制約条件とすべての優先条件とを統合することができる。
【発明の効果】
【００７６】
本発明にかかる検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法によれば、特別な状況を狙い撃ちでテストしつつ、可能な限り広範囲の状況をテストすることができるという効果を奏する。
【発明を実施するための最良の形態】
【００７７】
以下に添付図面を参照して、この発明にかかる検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法の好適な実施の形態を詳細に説明する。なお、説明中、数式で表現されるベクトルの記号は、文章中では＜＞を用いて表記する。たとえば、数式内でベクトルｘが表記されている場合、文章中では＜ｘ＞と表記する。
【００７８】
（実施の形態１）
（検証支援装置のハードウェア構成）
まず、この発明の実施の形態１にかかる検証支援装置のハードウェア構成について説明する。図１は、この発明の実施の形態１にかかる検証支援装置のハードウェア構成を示すブロック図である。
【００７９】
図１において、検証支援装置は、ＣＰＵ１０１と、ＲＯＭ１０２と、ＲＡＭ１０３と、ＨＤＤ（ハードディスクドライブ）１０４と、ＨＤ（ハードディスク）１０５と、ＦＤＤ（フレキシブルディスクドライブ）１０６と、着脱可能な記録媒体の一例としてのＦＤ（フレキシブルディスク）１０７と、ディスプレイ１０８と、Ｉ／Ｆ（インターフェース）１０９と、キーボード１１０と、マウス１１１と、スキャナ１１２と、プリンタ１１３と、を備えている。また、各構成部はバス１００によってそれぞれ接続されている。
【００８０】
ここで、ＣＰＵ１０１は、検証支援装置の全体の制御を司る。ＲＯＭ１０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ１０３は、ＣＰＵ１０１のワークエリアとして使用される。ＨＤＤ１０４は、ＣＰＵ１０１の制御にしたがってＨＤ１０５に対するデータのリード／ライトを制御する。ＨＤ１０５は、ＨＤＤ１０４の制御で書き込まれたデータを記憶する。
【００８１】
ＦＤＤ１０６は、ＣＰＵ１０１の制御にしたがってＦＤ１０７に対するデータのリード／ライトを制御する。ＦＤ１０７は、ＦＤＤ１０６の制御で書き込まれたデータを記憶したり、ＦＤ１０７に記憶されたデータを検証支援装置に読み取らせたりする。
【００８２】
また、着脱可能な記録媒体として、ＦＤ１０７のほか、ＣＤ−ＲＯＭ（ＣＤ−Ｒ、ＣＤ−ＲＷ）、ＭＯ、ＤＶＤ（Ｄｉｇｉｔａｌ  Ｖｅｒｓａｔｉｌｅ  Ｄｉｓｋ）、メモリーカードなどであってもよい。ディスプレイ１０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ１０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００８３】
Ｉ／Ｆ１０９は、通信回線を通じてインターネットなどのネットワーク１１４に接続され、このネットワーク１１４を介して他の装置に接続される。そして、Ｉ／Ｆ１０９は、ネットワーク１１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ１０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００８４】
キーボード１１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス１１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００８５】
スキャナ１１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ１１２は、ＯＣＲ機能を持たせてもよい。また、プリンタ１１３は、画像データや文書データを印刷する。プリンタ１１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００８６】
（検証支援装置の機能的構成）
つぎに、この発明の実施の形態１にかかる検証支援装置の機能的構成について説明する。図２は、この発明の実施の形態１にかかる検証支援装置の機能的構成を示すブロック図である。図２において、検証支援装置２００は、取得部２０１と、優先条件算出部２０２と、構築部２０３と、から構成されている。
【００８７】
まず、取得部２０１は、論理式を取得する。具体的には、たとえば、ユーザが作成した論理式を読み込む。読み込まれる論理式は、たとえば、入力制約条件（Ｃ0）を表現する論理式である。入力制約条件（Ｃ0）とは、検証対象への入力が必ず満たさなければならない条件である。図１４に示した検証対象１４００の場合、入力制約条件（Ｃ0）としては、以下の条件が例として挙げられる。
【００８８】
［入力制約条件（Ｃ0）］：
・ｃｍｄ＝０かつｒｅｑ＝１を入力したらＲｅａｄ動作が始まり、ａｃｋ＝１の応答によってＲｅａｄ動作が終了するまでｃｍｄとｒｅｑの値を変更してはならない。
・ｃｍｄ＝１かつｒｅｑ＝１を入力したらＷｒｉｔｅ動作が始まり、ａｃｋ＝１の応答によってＷｒｉｔｅ動作が終了するまでｃｍｄ、ｒｅｑ、およびｗｄの値を変更してはならない。
【００８９】
上述した入力制約条件（Ｃ0）を表現する論理式は、検証対象の入出力の論理積や論理和の組み合わせで表現される。図１４に示した検証対象１４００の場合、入力はｃｍｄ，ｒｅｑ，ｗｄ、出力はａｃｋ，ｒｄであるため、これらの論理積や論理和の組み合わせで表現される。
【００９０】
また、入力制約条件（Ｃ0）を表現する論理式は現在の入出力だけではなく、過去の入出力値にも依存することがある。この場合、入力制約条件は適当な有限状態機械と組み合わせて表現することができる。有限状態機械は検証対象の入出力を監視しながら状態遷移する。したがって、入力制約条件（Ｃ0）を表現する論理式は、検証対象の入出力と有限状態機械の状態変数で構成される。当該論理式の詳細は、後述する実施例１，２で説明する。
【００９１】
なお、以降の説明において、論理式の表現対象（たとえば、各種条件、動作、各種パターン発生器）については（）付き符号で説明するが、対応する論理式については、数式に対応させるため、（）を除いた符号で説明する。たとえば、上述の場合、入力制約条件は、「入力制約条件（Ｃ0）」と表記されるため、その論理式はＣ0と表記する。
【００９２】
また、取得部２０１は、優先検証動作（Ｐk）を表現する論理式Ｐkも取得する。なお、ｋはｋ＝１〜ｎの整数である。優先検証動作（Ｐk）とは、検証対象の検証動作の中から優先的に選ばれた検証動作である。図１４に示した検証対象１４００の場合、優先検証動作（Ｐk）としては、以下の条件が例として挙げられる。この優先検証動作（Ｐk）は、単一（ｋ＝１）であってもよく、また、複数（ｋ＝２〜ｎ）であってもよい。なお、優先検証動作（Ｐk）を表現する論理式Ｐkは、ユーザによって記述される。
【００９３】
［優先検証動作（Ｐ1）］：Ｒｅａｄ動作またはＷｒｉｔｅ動作が間隔を置かず２回連続して起こる場合をテストしたい。
【００９４】
また、取得部２０１は、優先検証動作（Ｐk）が複数存在する場合、ユーザによって指定された優先検証動作（Ｐk）の優先順位を取得する。この優先順位の利用法は後述する。また、特願２００４−２３５８５２の方法を用いれば、対象モジュールのインターフェース仕様記述から前記の有限状態機械および入力制約条件を自動生成することが可能である。したがって本実施の形態においては有限状態機械や入力制約の代わりにインターフェース仕様記述を出発点としても良い。
【００９５】
また、優先条件算出部２０２は、取得部２０１によって取得された論理式Ｃ0，Ｐkを用いて、優先条件（Ｃk）を表現する論理式Ｃkを算出する。優先条件（Ｃk）とは、優先検証動作（Ｐk）において入力制約条件（Ｃ0）を満たす入力を検証対象に送りたいという条件である。
【００９６】
優先条件算出部２０２は、具体的には、入力制約条件（Ｃ0）を表現する論理式Ｃ0と優先検証動作（Ｐk）を表現する論理式Ｐkとの論理積をとることにより、優先条件（Ｃk）を表現する論理式Ｃkを算出する。優先検証動作（Ｐk）を表現する論理式Ｐkが複数存在する場合、優先条件（Ｃk）を表現する論理式Ｃkは、優先検証動作（Ｐk）を表現する論理式Ｐkごとに算出される。
【００９７】
優先条件（Ｃk）を表現する論理式Ｃkも、入力制約条件（Ｃ0）を表現する論理式Ｃ0と同様、検証対象の入出力の論理積や論理和の組み合わせで表現される。図１４に示した検証対象１４００の場合、入力はｃｍｄ，ｒｅｑ，ｗｄ、出力はａｃｋ，ｒｄであるため、これらの論理積や論理和の組み合わせで表現される。
【００９８】
また、優先条件（Ｃk）を表現する論理式Ｃkは現在の入出力だけではなく、過去の入出力値にも依存することがある。この場合、優先条件（Ｃk）は上述した有限状態機械と組み合わせて表現することができる。したがって、優先条件（Ｃk）を表現する論理式Ｃkも、検証対象の入出力と有限状態機械の状態変数で構成される。
【００９９】
特に、優先条件（Ｃk）を表現する論理式Ｃkは、検証対象への入力群＜ｙ＞と、検証対象からの出力または／および有限状態機械の状態変数からなる変数群＜ｘ＞とを用いた論理式Ｃkであらわすことができる。
【０１００】
図３は、入力制約条件（Ｃ0）と優先条件（Ｃk）とを定義するモデルを示す説明図である。図３において、順序機械Ｍ0は、検証対象１４００の入出力を監視しながら状態遷移する有限状態機械である。
【０１０１】
また、図２において、優先検証動作（Ｐk）が複数（たとえば、ｋ＝２）存在する場合、優先条件算出部２０２は、優先検証動作（Ｐ1）に応じた優先条件（Ｃ1）を表現する論理式Ｃ1と、優先検証動作（Ｐ2）に応じた優先条件（Ｃ2）を表現する論理式Ｃ2との論理積Ｃ1・Ｃ2を算出することもできる。この論理積Ｃ1・Ｃ2により表現される優先条件（Ｃ1・Ｃ2）は、２つの論理式Ｃ1，Ｃ2により表現される優先条件（Ｃ1），（Ｃ2）を同時に満足する優先条件となる。
【０１０２】
また、構築部２０３は、各種論理式に基づいて、パターン発生器（Ｇ）を構築する。具体的には、構築部２０３は、入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先条件算出部２０２によって算出された優先条件（Ｃk）を表現する論理式Ｃkとに基づいて、入力制約条件（Ｃ0）を満たす検証対象への入力のパターン（以下、「基本パターン」という）と、優先条件（Ｃk）を満たす検証対象への入力のパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器（Ｇ）を構築する。
【０１０３】
ここで、構築部２０３内の機能的構成について説明する。構築部２０３は各種算出部を有する。これら算出部は、入力されてくる論理式に基づいてあらたな論理式を算出する。具体的には、論理式が入力されると、上述した非特許文献１による算出法（式（１）〜（２９））により、あらたな論理式を算出する。特に断らない限り、算出部はこの算出法により論理式を算出する。
【０１０４】
基本パターン発生器算出部２１１は、入力制約条件（Ｃ0）を表現する論理式Ｃ0に基づいて、基本パターンを発生させる基本パターン発生器（Ｇ0）の動作を表現する論理式（Ｇ0）を算出する。基本パターンとは、入力制約条件（Ｃ0）を満たす検証対象への入力のパターンである。基本パターン発生器算出部２１１は、非特許文献１と同一の機能を果たす。
【０１０５】
優先パターン発生器算出部２１２は、優先条件（Ｃk）を表現する論理式Ｃkに基づいて、優先パターンを発生させる優先パターン発生器（Ｇk）の動作を表現する論理式Ｇkを算出する。優先パターンとは、優先条件（Ｃk）を満たす検証対象への入力のパターンという。優先条件（Ｃk）を表現する論理式（Ｃk）が複数存在する場合、優先パターン発生器（Ｇk）の動作を表現する論理式Ｇkは、優先条件（Ｃk）を表現する論理式Ｃkごとに算出される。
【０１０６】
優先パターン選択条件算出部２１３は、検証対象への入力群＜ｙ＞と変数群＜ｘ＞とを用いた論理式（Ｃk）に基づいて、優先条件（Ｃk）が満たされる場合に変数群＜ｘ＞によって特定される優先パターンの選択条件を表現する論理式Ｓkを算出する。
【０１０７】
優先条件（Ｃk）を表現する論理式Ｃkの値が１になるような論理変数＜ｘ＞および論理変数＜ｙ＞の値割り当ての場合、優先条件（Ｃk）が満たされたこととなる。パターン発生器が制御できるのは論理変数＜ｙ＞の値だけであり、特定の論理変数＜ｘ＞の値に対しては論理変数＜ｙ＞の値をどのように選んでも論理式Ｃkを１にすることが不可能な場合がある。
【０１０８】
その反対のケース、すなわち論理変数＜ｙ＞の値を適切に選ぶことで論理式Ｃkの値を１できる可能性のある論理変数＜ｘ＞の条件を、優先パターン選択条件（Ｓk）と呼ぶ。優先条件（Ｃk）を表現する論理式Ｃkに対する優先パターン選択条件（Ｓk）は、∃演算を使って論理式の形で算出することができる。この優先パターン選択条件（Ｓk）は、下記式（３０）の通りである。
【０１０９】
【数２０】
0004759392.tif 000021
【０１１０】
また、構築部２０３は、接続部２１４を有する。接続部２１４は、入力されてくる論理式によって表現されるパターン発生器や条件に応じて、これらの出力をセレクタ回路に接続する。これにより、入力されてくる論理式によって表現されるパターン発生器を組み合わせて、上述した基本パターンと優先パターンとを選択的に発生させるパターン発生器（Ｇ）を構築する。
【０１１１】
図４は、構築部２０３によって構築されたパターン発生器（Ｇ）を示す説明図である。また、図５は、構築されたパターン発生器（Ｇ）の内部構成を示す説明図である。図５では、一つの基本パターン発生器（Ｇ0）と、ｋ個の優先パターン発生器（Ｇk）と、ｋ個の優先パターン選択条件（Ｓk）と、これらを接続するｋ個のセレクタ回路Ｔkと、から構成されている。
【０１１２】
図５においては、基本パターン発生器（Ｇ0）の出力およびｋ個の優先パターン発生器（Ｇk）の出力は、それぞれ対応するセレクタ回路Ｔkの信号入力に接続され、優先パターン選択条件（Ｓk）の出力は、各セレクタ回路ＴkのＯＮ／ＯＦＦの制御入力と接続される。また、全セレクタ回路Ｔkのうちｎ番目のセレクタ回路Ｔnは、検証対象の入力端子に接続される。
【０１１３】
図５では、ｎ番目の優先パターン発生器（Ｇn）が、検証対象の入力端子に接続されるセレクタ回路Ｔnに直接接続されているため、ｎ番目の優先パターン発生器（Ｇn）からの優先パターンが、最も最優先される入力パターンとなる。すなわち、ｋの値が大きいほどその優先パターン発生器（Ｇk）からの優先パターンが優先出力される。そして、基本パターン発生器（Ｇ0）からの基本パターンが最も優先度が低くなっている。
【０１１４】
また、優先検証動作（Ｐk）が複数存在する場合、優先条件（Ｃk）を表現する論理式も同数存在し、それに対応して優先パターン選択条件（Ｓk）も同数存在する。したがって、取得部２０１により、ユーザによって指定された優先検証動作（Ｐk）の優先順位が取得された場合、その優先順位に従って優先パターンが発生するようにパターン発生器（Ｇ）を構築することができる。具体的には、優先順位に従って、複数の優先パターン発生器（Ｇk）とセレクタ回路Ｔkとの接続を変更すればよい。
【０１１５】
たとえば、図５において、優先パターン発生器（Ｇn-1）からの優先パターンが優先パターン発生器（Ｇn）よりも優先順位が高い場合、図５に示した優先パターン選択条件（Ｓn）と優先パターン選択条件（Ｓn-1）とを入れ替えるとともに、図５に示した優先パターン選択条件（Ｇn）と優先パターン選択条件（Ｇn-1）とを入れ替える。これにより、ユーザの指定に従った順序で検証対象にパターンを送ることができる。
【０１１６】
なお、上述した取得部２０１、優先条件算出部２０２、および構築部２０３は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７等に記録されたプログラムを、ＣＰＵ１０１が実行することによって、または、Ｉ／Ｆ１０９によって、その機能を実現する。
【０１１７】
（検証支援装置２００の検証支援処理手順）
つぎに、この発明の実施の形態１にかかる検証支援装置２００の検証支援処理手順について説明する。図６は、この発明の実施の形態１にかかる検証支援装置２００の検証支援処理手順を示すフローチャートである。
【０１１８】
図６において、まず、取得部２０１により入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先検証動作（Ｐk）を表現する論理式Ｐkとを取得する（ステップＳ６０１）。つぎに、優先条件算出部２０２により、論理式Ｐkを用いて、優先条件（Ｃk）を表現する論理式Ｃkを算出する（ステップＳ６０２）。
【０１１９】
つぎに、基本パターン発生器算出部２１１により、論理式Ｃ0を用いて基本パターン発生器（Ｇ0）の動作を表現する論理式（Ｇ0）を算出するとともに、優先パターン発生器算出部２１２により、論理式Ｃkを用いて優先パターン発生器（Ｇk）の動作を表現する論理式（Ｇk）を算出する（ステップＳ６０３）。
【０１２０】
そして、優先パターン選択条件算出部２１３により、論理式Ｃkを用いて優先パターン選択条件（Ｓk）を表現する論理式Ｓkを算出する（ステップＳ６０４）。このあと、論理式Ｇ0，Ｇk，Ｓkを用いて、接続部２１４により、基本パターン発生器（Ｇ0）、優先パターン発生器（Ｇk）および優先パターン選択条件（Ｓk）をセレクタ回路に接続することで、優先条件付きのパターン発生器（Ｇ）を構築する（ステップＳ６０５）。
【０１２１】
このように、上述した従来技術では、ユーザがパターンの発生順序を制御することができなかったが、実施の形態１では論理式の形で優先条件（Ｃk）を表現することで、優先条件（Ｃk）に当てはまるパターンをできるだけ先行してテストし、それ以外のパターンを後の段階でテストするという順序付けが可能になる。
【０１２２】
この順序付け機能を利用すれば、早い段階で基本機能をテストしたり問題の起こりやすい状況を集中的にテストすることができるようになる。その結果として、論理検証作業の効率向上に大きな効果がある。
【０１２３】
また、パターン発生器生成を入力制約条件（Ｃ0）および各優先条件（Ｃk）に対して分割処理することで、計算機のメモリ使用量などのコストを低く抑えることができる。さらに、構築されたパターン発生器（Ｇ）においては、各機能が明確に分離されており、セレクタ回路の構成を自動または手動で変更することで優先順位を変えて再利用することが容易である。
【０１２４】
以下、上述した実施の形態１の実施例について説明する。実施例１は、単一の優先検証動作、すなわち、単一の優先条件（ｋ＝１）により、優先条件付きのパターン発生器（Ｇ）を構築する例である。一方、実施例２は、複数の優先検証動作、すなわち、複数の優先条件（ｋ＝２〜ｎ）により、優先条件付きのパターン発生器（Ｇ）を構築する例である。
【実施例１】
【０１２５】
まず、上述した実施の形態１にかかる検証支援装置２００の実施例１について説明する。実施例１では、検証対象の入力群をｎビットの論理変数＜ｙ＞＝（ｙ1，ｙ2，…，ｙn）とし、その他の変数群（検証対象の出力や検証対象に付加した順序機械の状態変数）をｍビットの論理変数＜ｘ＞＝（ｘ1，ｘ2，…，ｘm）とすると、優先条件（Ｃk）は論理変数＜ｘ＞および論理変数＜ｙ＞からなる論理式Ｃkで与えられる。
【０１２６】
この論理式Ｃkの値が１になるような論理変数＜ｘ＞および論理変数＜ｙ＞の値割り当ての場合、優先条件が満たされることとなる。パターン発生器（Ｇ）が制御できるのは論理変数＜ｙ＞の値だけであり、特定の論理変数＜ｘ＞の値に対しては論理変数＜ｙ＞の値をどのように選んでも論理式Ｃkを１にすることが不可能な場合がある。
【０１２７】
その反対のケース、すなわち＜ｙ＞の値を適切に選ぶことで論理式Ｃkの値を１にできる可能性のある＜ｘ＞の条件が、上述した優先パターン選択条件（Ｓk）である。優先条件を表現する論理式Ｃkに対する優先パターン選択条件（Ｓk）は、上記式（３０）に示した∃演算を使って生成することができる。
【０１２８】
また、入力制約条件（Ｃ0）などの論理式Ｃ0からパターン発生器（Ｇ0）を自動生成する方法は、上述した非特許文献１の従来技術をそのまま利用すればよい。具体例として、図１４に示した検証対象１４００に対して次の優先条件を加えた場合のパターン発生器生成手順を示す。
【０１２９】
［優先条件（Ｃ1）］：Ｒｅａｄ動作またはＷｒｉｔｅ動作が間隔を置かず２回連続して起こる場合をテストしたい。
【０１３０】
この優先条件（Ｃ1）を論理式Ｃ1で表現する場合、その補助として図７のモデルを使用する。図７は、実施例１における入力制約条件（Ｃ0）と優先条件（Ｃ1）とを定義するモデルを示す説明図である。図７において、順序機械Ｍは、上述した順序機械Ｍ0に新たな状態変数ｕを加えた順序機械である。つぎに、この状態変数ｕの状態遷移グラフを示す。
【０１３１】
図８は、状態変数ｕの状態遷移グラフを示す説明図である。図８において、ｕ＝０は初期状態であり、ｕ＝１は１回目のＲｅａｄ動作が終了した直後の状態、ｕ＝２は１回目のＷｒｉｔｅ動作が終了した直後の状態に対応する。
【０１３２】
このモデルを用いると、Ｒｅａｄ動作またはＷｒｉｔｅ動作が間隔を置かず２回連続する状況を次の論理式Ｐ1で表現することができる。
【０１３３】
【数２１】
0004759392.tif 000022
【０１３４】
実際の優先条件（Ｃ1）は、上記論理式Ｐ1と暗黙の条件である入力制約条件（Ｃ0）を同時に満たした条件である。この優先条件（Ｃ1）は、下記式（３２）の通りである。
【０１３５】
【数２２】
0004759392.tif 000023
【０１３６】
優先条件（Ｃ1）に対する優先パターン選択条件（Ｓ1）は次のように求められる。
【０１３７】
【数２３】
0004759392.tif 000024
【０１３８】
また、上記非特許文献１などの従来技術を使って、入力制約条件（Ｃ0）から基本パターン発生器（Ｇ0）を、優先条件（Ｃ1）から優先パターン発生器（Ｇ1）を生成する。その結果として得られる基本パターン発生器（Ｇ0）の動作は、上述した式（２）〜（４）によって表現される。
【０１３９】
一方、優先パターン発生器（Ｇ1）の動作は次の論理式で表現される。
【０１４０】
【数２４】
0004759392.tif 000025
【０１４１】
そして、上述した優先パターン選択条件（Ｓ1）と優先パターン発生器（Ｇ1）と基本パターン発生器（Ｇ0）とを組み合わせ、さらにセレクタ回路を付加することにより、優先条件付きのパターン発生器（Ｇ）を生成する。
【０１４２】
図９は、構築部２０３によって構築されたパターン発生器（Ｇ）を示す説明図である。また、図１０は、構築されたパターン発生器（Ｇ）の内部構成を示す説明図である。図１０において、セレクタ回路Ｔ1は、優先パターン選択条件（Ｓ1）が１のときは優先パターン発生器（Ｇ1）の出力を選択し、優先パターン選択条件（Ｓ1）が０のときは基本パターン発生器（Ｇ0）の出力が選択する。
【０１４３】
この実施例１の優先条件付きのパターン発生器（Ｇ）によれば、論理式の形で優先条件（Ｃ1）を表現することで、優先条件（Ｃ1）に当てはまるパターンをできるだけ先行してテストし、それ以外のパターンを後の段階でテストするという順序付けが可能になる。
【０１４４】
この順序付け機能を利用すれば、早い段階で基本機能をテストしたり、問題の起こりやすい状況を集中的にテストすることができるようになる。その結果として、論理検証作業の効率化を図ることができる。また、パターン発生器の生成を入力制約および優先条件に対して分割処理することで、計算機のメモリ使用量などのコストの低減化を図ることができる。
【実施例２】
【０１４５】
つぎに、上述した実施の形態１にかかる検証支援装置２００の実施例２について説明する。実施例２は、複数の優先条件を用いてパターン発生器の生成処理をおこなう例である。この実施例２では、上述した実施例１を用いて説明する。この実施例２において、実施例１に対してさらに次の優先条件を加えることとする。
【０１４６】
［優先条件（Ｃ2）］：ｗｄの値が１ずつ増加するように制約したい。
【０１４７】
この優先条件（Ｃ2）に関しては新しい状態変数を追加する必要はなく、次の論理式Ｐ2で表現することができる。
【０１４８】
Ｐ2＝（ｗｄ＝ｔ＋１）・・・・・・・・・・・・・・・・・・・・・・・・・（３７）
【０１４９】
なお、この式（３７）の記号「＋」は、加算記号であり、ｗｄの値が１ずつ増加することをあらわしている。実際の優先条件（Ｃ2）は、論理式Ｐ2と暗黙の条件である入力制約条件（Ｃ0）を同時に満たすものである。この優先条件（Ｃ2）は、下記式（３８）の通りである。
【０１５０】
【数２５】
0004759392.tif 000026
【０１５１】
優先条件（Ｃ2）に対する優先パターン選択条件（Ｓ2）は次のように求められる。
【０１５２】
Ｓ2＝∃（ｃｍｄ，ｒｅｑ，ｗｄ）．Ｃ2＝（ｓ＝０）＋（ｓ＝１）・・・・・（３９）
【０１５３】
優先条件（Ｃ2）から生成できる優先パターン発生器（Ｇ2）の動作は次の通りである。
【０１５４】
ｃｍｄ←（ｓ＝１）？０：ｒａｎｄｏｍ（１）・・・・・・・・・・・・・・・（４０）
ｒｅｑ←（ｓ＝１）？１：ｒａｎｄｏｍ（１）・・・・・・・・・・・・・・・（４１）
ｗｄ←（（ｓ＝０）＋（ｓ＝１））？ｔ＋１：ｒａｎｄｏｍ（３２）・・・・・（４２）
【０１５５】
そして、優先パターン発生器（Ｇ2）および優先パターン選択条件（Ｓ2）と、実施例１で示した優先パターン選択条件（Ｓ1）と優先パターン発生器（Ｇ1）と基本パターン発生器（Ｇ0）とを組み合わせることにより、２つの優先条件（Ｃ1），（Ｃ2）に対応したパターン発生器（Ｇ’）を構成することができる。
【０１５６】
図１１は、優先条件（Ｃ1），（Ｃ2）に対応したパターン発生器（Ｇ’）の内部構成を示す説明図である。図１１においては、優先条件（Ｃ2），（Ｃ1）の順で優先してパターンが採用される。また、セレクタ回路Ｔ1，Ｔ2の接続を変更することにより優先順位を逆にすることも容易である。
【０１５７】
また、優先条件（Ｃ1），（Ｃ2）の論理積によって、２つの優先条件（Ｃ1），（Ｃ2）が同時に満足されるという意味のあらたな優先条件（Ｃ3）を作り、３つの優先条件（Ｃ1）〜（Ｃ3）に対する優先条件付きのパターン発生器を生成してもよい。この優先条件（Ｃ3）は、下記式（４３）の通りである。
【０１５８】
【数２６】
0004759392.tif 000027
【０１５９】
優先条件（Ｃ3）に対する優先パターン選択条件（Ｓ3）は次のように求められる。
【０１６０】
【数２７】
0004759392.tif 000028
【０１６１】
優先条件（Ｃ3）から生成できる優先パターン発生器（Ｇ3）の動作は次の通りである。
【０１６２】
【数２８】
0004759392.tif 000029
【０１６３】
このとき、優先条件（Ｃ3）が最も優先されるように構成すれば、まず２つの優先条件（Ｃ1），（Ｃ2）を同時に満足するパターンを探し、次に個別に満足できるパターンを探すパターン発生器を実現することができる。
【０１６４】
この実施例２によれば、実施例１と同様の効果を得ることができる。また、実施例２によれば、パターン発生器（Ｇ’）に示した各部分の機能が明確に分離されており、セレクタ部分の構成を自動または手動で変更することで優先順位を変えて容易に再利用することができる。
【０１６５】
（実施の形態２）
つぎに、この発明の実施の形態２にかかる検証支援装置２００について説明する。実施の形態１では、入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先条件（Ｃk）を表現する論理式Ｃkと、優先パターン選択条件（Ｓk）を表現する論理式Ｓkとを用いて、優先条件付きのパターン発生器（Ｇ）を構築する例について説明したが、実施の形態２では、入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先条件（Ｃk）を表現する論理式Ｃkと、優先パターン選択条件（Ｓk）を表現する論理式Ｓkと用いて、あらかじめ入力制約条件（Ｃ0）および優先条件（Ｃk）を統合した論理式Ｃを用いた例である。
【０１６６】
実施の形態２においては、図１に示したハードウェア構成を用いるため、その説明を省略する。また、実施の形態１で説明した内容と同一内容については同一符号を付し、その説明を省略する。
【０１６７】
（検証支援装置２００の機能的構成）
図１２は、この発明の実施の形態２にかかる検証支援装置２００の機能的構成を示すブロック図である。図１２において、優先条件付制約論理式算出部１２００は、入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先条件（Ｃk）を表現する論理式Ｃkと、優先パターン選択条件（Ｓk）を表現する論理式Ｓkとに基づいて、入力制約条件（Ｃ0）および優先条件（Ｃk）を満たす優先条件付制約論理式Ｃを算出する。具体的には、下記式により算出する。
【０１６８】
【数２９】
0004759392.tif 000030
【０１６９】
なお、上述した優先条件付制約論理式算出部１２００は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７等に記録されたプログラムを、ＣＰＵ１０１が実行することによって、または、Ｉ／Ｆ１０９によって、その機能を実現する。
【０１７０】
（検証支援装置２００の検証支援処理手順）
つぎに、この発明の実施の形態２にかかる検証支援装置２００の検証支援処理手順について説明する。図１３は、この発明の実施の形態２にかかる検証支援装置２００の検証支援処理手順を示すフローチャートである。
【０１７１】
図１３において、まず、取得部２０１により入力制約条件（Ｃ0）を表現する論理式Ｃ0と、優先検証動作（Ｐk）を表現する論理式Ｐkとを取得する（ステップＳ１３０１）。つぎに、優先条件算出部２０２により、論理式Ｐkを用いて、優先条件（Ｃk）を表現する論理式Ｃkを算出する（ステップＳ１３０２）。
【０１７２】
つぎに、基本パターン発生器算出部２１１により、論理式Ｃ0を用いて基本パターン発生器（Ｇ0）の動作を表現する論理式Ｇ0を算出するとともに、優先パターン発生器算出部２１２により、論理式Ｃkを用いて優先パターン発生器（Ｇk）の動作を表現する論理式Ｇkを算出する（ステップＳ１３０３）。
【０１７３】
そして、優先パターン選択条件算出部２１３により、論理式Ｃkを用いて優先パターン選択条件（Ｓk）を表現する論理式Ｓkを算出する（ステップＳ１３０４）。このあと、優先条件付制約論理式算出部１２００により、論理式Ｇ0，Ｇk，Ｓkを用いて、論理式Ｇ0，Ｇkを統合した単一の優先条件付制約論理式Ｃを算出する（ステップＳ１３０５）。この優先条件付制約論理式Ｃが、優先条件付きのパターン発生器（Ｇ）の動作を表現する論理式となる。
【０１７４】
このように、実施の形態２によれば、入力制約条件（Ｃ0）およびすべての優先条件（Ｃk）を統合し、単一の論理式を得ることができる。このように、入力制約条件（Ｃ0）およびすべての優先条件（Ｃk）を一つの論理式に統合してからパターン発生器生成処理をおこなうことで、生成されるパターン発生器（Ｇ）の規模を小さくする最適化処理をおこないやすいという効果が得られる。
【実施例３】
【０１７５】
つぎに、上述した実施の形態２にかかる検証支援装置２００の実施例３について説明する。実施例１では基本パターン発生器（Ｇ0）と優先パターン発生器（Ｇ1）とをそれぞれ生成したが、実施例３では、入力制約条件（Ｃ0）と優先条件（Ｃ1）とを統合した優先条件付制約論理式Ｃを生成してから、優先条件付制約論理式Ｃをもとに、上述した非特許文献１の従来技術を用いてパターン発生器（Ｇ）を生成する。
【０１７６】
優先条件付制約論理式Ｃは、実施例１で求めた優先パターン選択条件（Ｓ1）を用いて次のように求めることができる。
【０１７７】
【数３０】
0004759392.tif 000031
【０１７８】
この優先条件付制約論理式Ｃから生成できるパターン発生器（Ｇ）の動作は次の通りである。
【０１７９】
【数３１】
0004759392.tif 000032
【０１８０】
実施例２のように優先条件が２つ、３つの場合にも、同様に優先条件付制約論理式Ｃ’，Ｃ”を求めることができる。これらの優先条件付制約論理式Ｃ’，Ｃ”は、下記式（５３）、（５４）の通りである。
【０１８１】
【数３２】
0004759392.tif 000033
【０１８２】
優先条件付制約論理式Ｃ’から生成できるパターン発生器（Ｇ’）の動作は次の通りである。
【０１８３】
【数３３】
0004759392.tif 000034
【０１８４】
優先条件付制約論理式Ｃ”から生成できるパターン発生器（Ｇ”）の動作は次の通りである。
【０１８５】
【数３４】
0004759392.tif 000035
【０１８６】
この実施例３によれば、入力制約条件（Ｃ0）およびすべての優先条件（Ｃk）を一つの論理式に統合してからパターン発生器（Ｇ）〜（Ｇ”）の生成処理をおこなうことで、生成されるパターン発生器（Ｇ）〜（Ｇ”）の規模を小さくする最適化処理をおこないやすいという効果を得ることができる。
【０１８７】
以上説明したように、この発明の実施の形態１，２にかかる検証支援装置によれば、特別な状況を狙い撃ちでテストしつつ、可能な限り広範囲の状況をテストすることができる。したがって、検証作業の短縮化および高精度化を図ることができる。
【０１８８】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な伝送媒体であってもよい。
【０１８９】
（付記１）検証対象への入力が必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得させる取得工程と、
前記取得工程によって取得された論理式を用いて、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出させる優先条件算出工程と、
前記入力制約条件を表現する論理式と、前記優先条件算出工程によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力のパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記検証対象への入力のパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築させる構築工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１９０】
（付記２）前記構築工程は、
前記入力制約条件を表現する論理式に基づいて、前記基本パターンを発生させる基本パターン発生器の動作を表現する論理式を算出させる基本パターン発生器算出工程と、
前記優先条件を表現する論理式に基づいて、前記優先パターンを発生させる優先パターン発生器の動作を表現する論理式を算出する優先パターン発生器算出工程と、を含み、
前記基本パターン発生器算出工程によって算出された論理式と前記優先パターン発生器算出工程によって算出された論理式とに基づいて、前記パターン発生器を構築させることを特徴とする付記１に記載の検証支援プログラム。
【０１９１】
（付記３）前記取得工程は、
前記優先検証動作が複数存在する場合に、ユーザによって指定された前記優先検証動作の優先順位を取得させ、
前記構築工程は、
さらに、前記取得工程によって取得された前記優先検証動作の優先順位に従って前記優先パターンが発生するように、前記パターン発生器を構築させることを特徴とする付記１または２に記載の検証支援プログラム。
【０１９２】
（付記４）前記優先条件算出工程は、
前記優先検証動作が複数存在する場合、前記各優先検証動作に応じた各優先条件を表現する論理式の論理積を算出させ、
前記構築工程は、
前記入力制約条件を表現する論理式と、前記優先条件算出工程によって算出された論理積とに基づいて、前記基本パターンと前記各優先パターンとを選択的に発生させるパターン発生器を構築させることを特徴とする付記１〜３のいずれか一つに記載の検証支援プログラム。
【０１９３】
（付記５）前記入力制約条件を表現する論理式は、
前記検証対象の入出力と前記検証対象の入出力に応じて状態遷移する有限状態機械の状態変数とを用いた論理式であり、
前記優先条件を表現する論理式は、
前記検証対象への入力群と、前記検証対象からの出力または／および前記有限状態機械の状態変数からなる変数群とを用いた論理式であることを特徴とする付記４に記載の検証支援プログラム。
【０１９４】
（付記６）前記構築工程は、
前記入力群と前記変数群とを用いた論理式に基づいて、前記優先条件が満たされる場合に前記変数群によって特定される前記優先パターンの選択条件を表現する論理式を算出する優先パターン選択条件算出工程を含み、
前記優先パターン選択条件算出工程によって算出された前記優先パターンの選択条件を表現する論理式の値に応じて前記基本パターンと前記優先パターンとを選択的に発生させるパターン発生器を構築させることを特徴とする付記５に記載の検証支援プログラム。
【０１９５】
（付記７）前記構築工程は、
前記入力群と前記変数群とを用いた論理式に基づいて、前記優先条件が満たされる場合に前記変数群によって特定される前記優先パターンの選択条件を表現する論理式を算出させる優先パターン選択条件算出工程と、
前記入力制約条件を表現する論理式と、前記優先条件を表現する論理式と、前記優先パターンの選択条件を表現する論理式とに基づいて、前記入力制約条件および前記優先条件を満たす優先条件付制約論理式を算出させる優先条件付制約論理式算出工程を含み、
前記優先条件付制約論理式算出工程によって算出された優先条件付制約論理式に基づいて、前記基本パターンと前記優先パターンとを選択的に発生させるパターン発生器を構築させることを特徴とする付記５に記載の検証支援プログラム。
【０１９６】
（付記８）付記１〜７のいずれか一つに記載の論理検証プログラムを記録したコンピュータ読み取り可能な記録媒体。
【０１９７】
（付記９）検証対象への入力が必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得する取得手段と、
前記取得手段によって取得された論理式を用いて、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出する優先条件算出手段と、
前記入力制約条件を表現する論理式と、前記優先条件算出手段によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力のパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記検証対象への入力のパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築する構築手段と、
を備えることを特徴とする検証支援装置。
【０１９８】
（付記１０）検証対象への入力が必ず満たさなければならない入力制約条件を表現する論理式と、前記検証対象の検証動作の中から優先的に選ばれた検証動作（以下、「優先検証動作」という）を表現する論理式とを取得する取得工程と、
前記取得工程によって取得された論理式を用いて、前記優先検証動作において前記入力制約条件を満たす入力を前記検証対象に送りたいという優先条件を表現する論理式を算出する優先条件算出工程と、
前記入力制約条件を表現する論理式と、前記優先条件算出工程によって算出された前記優先条件を表現する論理式とに基づいて、前記入力制約条件を満たす前記検証対象への入力のパターン（以下、「基本パターン」という）と、前記優先条件を満たす前記検証対象への入力のパターン（以下、「優先パターン」という）とを選択的に発生させるパターン発生器を構築する構築工程と、
を含んだことを特徴とする検証支援方法。
【産業上の利用可能性】
【０１９９】
以上のように、本発明にかかる検証支援プログラム、該プログラムを記録した記録媒体、検証支援装置、および検証支援方法は、ハードウェアモジュールの検証に有用である。
【図面の簡単な説明】
【０２００】
【図１】この発明の実施の形態１にかかる検証支援装置のハードウェア構成を示すブロック図である。
【図２】この発明の実施の形態１にかかる検証支援装置の機能的構成を示すブロック図である。
【図３】入力制約条件（Ｃ0）と優先条件（Ｃk）とを定義するモデルを示す説明図である。
【図４】構築部によって構築されたパターン発生器（Ｇ）を示す説明図である。
【図５】構築されたパターン発生器（Ｇ）の内部構成を示す説明図である。
【図６】この発明の実施の形態１にかかる検証支援装置の検証支援処理手順を示すフローチャートである。
【図７】実施例１における入力制約条件（Ｃ0）と優先条件（Ｃ1）とを定義するモデルを示す説明図である。
【図８】状態変数ｕの状態遷移グラフを示す説明図である。
【図９】構築部によって構築されたパターン発生器（Ｇ）を示す説明図である。
【図１０】構築されたパターン発生器（Ｇ）の内部構成を示す説明図である。
【図１１】優先条件（Ｃ1），（Ｃ2）に対応したパターン発生器（Ｇ’）の内部構成を示す説明図である。
【図１２】この発明の実施の形態２にかかる検証支援装置の機能的構成を示すブロック図である。
【図１３】この発明の実施の形態２にかかる検証支援装置の検証支援処理手順を示すフローチャートである。
【図１４】検証対象となるハードウェアモジュールの一例を示す説明図である。
【図１５】入力制約条件を定義するモデルを示す説明図である。
【図１６】状態変数ｓの値変化を表現した状態遷移グラフを示す説明図である。
【図１７】入力制約条件の論理式Ｃ0を出発点として自動生成されたパターン発生器（Ｇ0）を示す説明図である。
【符号の説明】
【０２０１】
２００  検証支援装置
２０１  取得部
２０２  優先条件算出部
２０３  構築部
２１１  基本パターン発生器算出部
２１２  優先パターン発生器算出部
２１３  優先パターン選択条件算出部
２１４  接続部
１２００  優先条件付制約論理式算出部
１４００  検証対象
【図１】
0004759392.tif 000036
【図２】
0004759392.tif 000037
【図３】
0004759392.tif 000038
【図４】
0004759392.tif 000039
【図５】
0004759392.tif 000040
【図６】
0004759392.tif 000041
【図７】
0004759392.tif 000042
【図８】
0004759392.tif 000043
【図９】
0004759392.tif 000044
【図１０】
0004759392.tif 000045
【図１１】
0004759392.tif 000046
【図１２】
0004759392.tif 000047
【図１３】
0004759392.tif 000048
【図１４】
0004759392.tif 000049
【図１５】
0004759392.tif 000050
【図１６】
0004759392.tif 000051
【図１７】
0004759392.tif 000052