検証支援プログラム、検証支援装置、および検証支援方法
【課題】シミュレーション時間の短縮化を効率的におこなうこと。
【解決手段】（Ａ）で示したように、テストシナリオｔ１，ｔ２では、Ｓ０→Ｓ１→Ｓ３を通る遷移｛ａ，ｂ｝が重複している。したがって、本実施の形態では、テストシナリオｔ１を、“ｒｅｃｏｒｄ（Ｓ３）”を埋め込んだテストシナリオＴ１に変換する。そして、テストシナリオｔ２を、“ｒｅｓｔｏｒｅ（Ｓ３）”を埋め込んだテストシナリオＴ２に変換する。これにより、テストシナリオｔ２の短縮化を図る。なお、“ｒｅｃｏｒｄ（Ｓ３）”は状態Ｓ３の記録指示を示しており、“ｒｅｓｔｏｒｅ（Ｓ３）”は状態Ｓ３の復元指示を示している。
【解決手段】（Ａ）で示したように、テストシナリオｔ１，ｔ２では、Ｓ０→Ｓ１→Ｓ３を通る遷移｛ａ，ｂ｝が重複している。したがって、本実施の形態では、テストシナリオｔ１を、“ｒｅｃｏｒｄ（Ｓ３）”を埋め込んだテストシナリオＴ１に変換する。そして、テストシナリオｔ２を、“ｒｅｓｔｏｒｅ（Ｓ３）”を埋め込んだテストシナリオＴ２に変換する。これにより、テストシナリオｔ２の短縮化を図る。なお、“ｒｅｃｏｒｄ（Ｓ３）”は状態Ｓ３の記録指示を示しており、“ｒｅｓｔｏｒｅ（Ｓ３）”は状態Ｓ３の復元指示を示している。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路の検証を支援する検証支援プログラム、検証支援装置、および検証支援方法に関する。
【背景技術】
【０００２】
従来から回路シミュレーションのシミュレーション時間を短縮化する技術や、状態遷移表に基づいてテストシナリオを生成する技術が開示されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開平９−２９３０９３号公報
【特許文献２】特開２００１−３３１５４４号公報
【特許文献３】特開２００６−１１２８５２号公報
【特許文献４】特開平５−６２７２号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、上述した従来技術では、対象回路の有限状態機械モデルにおいて、どの状態を保存したり復元したりすればよいかが特定できないため、設計者が人手により該当箇所を指定しなければならず、設計者の負担が増大するという問題があった。また、そのような指定は設計者の能力にも依存するため、設計者ごとにばらつきが生じてしまい、シミュレーション時間が適切に短縮できていない場合もあるという問題があった。
【０００５】
また、通常は、同じ対象回路であってもテストシナリオと有限状態機械モデルは設計者によりそれぞれ作成されるため、シミュレーションをおこなう前に時間がかかったり、設計者の負担が増大するという問題があった。
【０００６】
また、作成されたテストシナリオと有限状態機械モデルとに矛盾が生じた場合、シミュレーションをやり直さなければならず、結果的にシミュレーション時間が増大してしまうという問題があった。さらに、有限状態機械モデルに実質的に同一の遷移パスが異なる遷移パスとして存在していると別々にシミュレーションをしなければならず、結果的にシミュレーション時間が増大してしまうという問題があった。
【０００７】
本発明は、上述した従来技術による問題点を解消するため、シミュレーション時間の短縮化を効率的におこなうことができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上述した課題を解決し、目的を達成するため、本検証支援プログラム、検証支援装置、および検証支援方法は、対象回路に関するテストシナリオ群の中から一のテストシナリオを選択し、選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、前記対象回路に関する有限状態機械モデルの中から検出し、検出された遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、前記有限状態機械モデルの中から特定し、特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定し、決定された登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記一の選択要素の次の要素として埋め込むことを要件とする。
【発明の効果】
【０００９】
本検証支援プログラム、検証支援装置、および検証支援方法によれば、シミュレーション時間の短縮化を効率的におこなうことができるという効果を奏する。
【図面の簡単な説明】
【００１０】
【図１】テストシナリオの短縮化の一例を示す説明図である。
【図２】図１に示した短縮化後のテストシナリオでのシミュレーション時間の比較例を示す説明図である。
【図３】検証支援装置のハードウェア構成を示すブロック図である。
【図４】検証支援装置の機能的構成の一例を示すブロック図である。
【図５】テストシナリオ短縮化処理部の機能的構成を示すブロック図である。
【図６】有限状態機械モデルにおけるテストシナリオ群の埋込前後の関係を示す説明図である。
【図７】テストシナリオ短縮化処理部によるテストシナリオ短縮化処理手順を示すフローチャートである。
【図８】ＦＳＭ検証処理部の機能的構成を示すブロック図である。
【図９】ＦＳＭ検証処理部によるＦＳＭ検証処理手順を示すフローチャートである。
【図１０】登録／復元処理部の機能的構成を示すブロック図である。
【図１１】データベースの記憶内容の一例を示す説明図である。
【図１２】登録／復元処理部による登録／復元処理手順を示すフローチャート（その１）である。
【図１３】登録／復元処理部による登録／復元処理手順を示すフローチャート（その２）である。
【図１４】有限状態機械モデルの修正例を示す説明図である。
【図１５】検証支援装置の機能的構成の一例を示すブロック図である。
【図１６】ＦＳＭ生成処理部の機能的構成を示すブロック図である。
【図１７】ＦＳＭ生成処理部によるＦＳＭ生成処理手順を示すフローチャートである。
【図１８】ＦＳＭ修正処理部および登録／復元処理部の機能的構成を示すブロック図である。
【図１９】ＦＳＭ修正処理部によるＦＳＭ修正処理手順を示すフローチャートである。
【図２０】登録／復元処理部による登録／復元処理手順を示すフローチャート（その３）である。
【発明を実施するための形態】
【００１１】
以下に添付図面を参照して、この発明にかかる検証支援プログラム、検証支援装置、および検証支援方法の好適な実施の形態を詳細に説明する。
【００１２】
・実施の形態１
（テストシナリオの短縮化）
まず、本実施の形態１におけるテストシナリオの短縮化について、図１〜図３を用いて説明する。
【００１３】
図１は、テストシナリオの短縮化の一例を示す説明図である。図１において、（Ａ）は、対象回路に関する有限状態機械モデル（ＦＳＭ）１００と短縮化前のテストシナリオｔ１，ｔ２を示している。また、（Ｂ）は、有限状態機械モデル１００と短縮化後のテストシナリオＴ１，Ｔ２を示している。有限状態機械モデル１００において、Ｓ＃（＃は番号）は状態を示しており、矢印は遷移を示している。
【００１４】
また、遷移を示す矢印の始端側の状態を「遷移元状態」と称し、矢印（遷移）の終端側の状態を「遷移先状態」と称す。なお、Ｓ０は初期状態を示す。本実施の形態で用いられる有限状態機械モデル１００は、あくまで一例であり、その内容は対象回路ごとに決められる。
【００１５】
また、回路のシミュレーションを例に挙げると、遷移は、対象回路を構成する組み合わせ回路に与えられる入力パターンであり、状態は、対象回路を構成する組み合わせ回路の出力先となるレジスタに保持される値である。したがって、遷移先状態とは、遷移としてある入力パターンが組み合わせ回路に与えられると、組み合わせ回路から出力されレジスタに保持された出力値である。なお、遷移元状態は、遷移される前のレジスタの値である。なお、シミュレーションを実行していない段階なので、状態を示すレジスタの値は、実際の０／１といった値ではなく変数であらわされる。
【００１６】
テストシナリオｔ１は、有限状態機械モデル１００において、Ｓ０→Ｓ１→Ｓ３→Ｓ６を通る遷移パスであり、ｔ１＝｛ａ，ｂ，ｃ｝である。また、テストシナリオｔ２は、ＦＳＭにおいて、Ｓ０→Ｓ１→Ｓ３→Ｓ８を通る遷移パスであり、ｔ２＝｛ａ，ｂ，ｄ｝である。ここで、要素ａは（Ｓ０→Ｓ１）を示す遷移である。要素ｂは（Ｓ１→Ｓ３）を示す遷移である。要素ｃは（Ｓ３→Ｓ６）を示す遷移である。要素ｄは（Ｓ３→Ｓ８）を示す遷移である。
【００１７】
（Ａ）で示したように、テストシナリオｔ１，ｔ２では、Ｓ０→Ｓ１→Ｓ３を通る遷移｛ａ，ｂ｝が重複している（Ｒｅｄｕｎｄａｎｃｙ）。したがって、本実施の形態では、テストシナリオｔ１を、“ｒｅｃｏｒｄ（Ｓ３）”を埋め込んだテストシナリオＴ１に変換する。また、テストシナリオｔ２を、“ｒｅｓｔｏｒｅ（Ｓ３）”を埋め込んだテストシナリオＴ２に変換する。これにより、状態Ｓ０から状態Ｓ３までのシミュレーションはテストシナリオＴ１のみで実行されるだけとなり、テストシナリオＴ２など他のテストシナリオでは、状態Ｓ０から状態Ｓ３までのシミュレーションを実行する必要なない。そのかわりに、状態Ｓ３を復元する。これにより、テストシナリオｔ２の短縮化を図る。なお、“ｒｅｃｏｒｄ（Ｓ３）”は状態Ｓ３の記録指示を示しており、“ｒｅｓｔｏｒｅ（Ｓ３）”は状態Ｓ３の復元指示を示している。
【００１８】
図２は、図１に示した短縮化後のテストシナリオでのシミュレーション時間の比較例を示す説明図である。図２において、ＳｉｍＴｉｍｅ（）は、（）内で示されるテストシナリオや遷移パスでシミュレーションをしたときのシミュレーション時間である。たとえば、ＳｉｍＴｉｍｅ（ｔ１）は、テストシナリオｔ１で対象回路をシミュレーションしたときのシミュレーション時間である。
【００１９】
（Ａ）は、図１（Ａ）で示した短縮化前でのシミュレーション時間を示している。テストシナリオｔ１のシミュレーション時間ＳｉｍＴｉｍｅ（ｔ１）とテストシナリオｔ２のシミュレーション時間ＳｉｍＴｉｍｅ（ｔ２）を合計したシミュレーション時間では、状態Ｓ０から状態Ｓ３までの遷移パスのシミュレーション時間ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）が重複しているため、２倍の時間がかかっている。
【００２０】
（Ｂ）は、図１（Ｂ）で示した短縮化後のシミュレーション時間を示している。（Ｂ）では、テストシナリオがｔ２からＴ２に短縮化されたため、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）が重複しておらず、１回分短縮化されている。そのかわりに、（Ｂ）では、テストシナリオＴ１での状態Ｓ３の記録時間ＲｅｃＴｉｍｅ（Ｓ３）と、テストシナリオＴ２での状態Ｓ３の復元時間ＲｅｓＴｉｍｅ（Ｓ３）とが追加される。したがって、この場合、以下の式（１）が成立する場合に、シミュレーション時間が短縮化される。
【００２１】
ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）＞ＲｅｃＴｉｍｅ（Ｓ３）＋ＲｅｓＴｉｍｅ（Ｓ３）
・・・・・・（１）
【００２２】
（検証支援装置のハードウェア構成）
図３は、検証支援装置のハードウェア構成を示すブロック図である。図３において、検証支援装置は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）３０１と、ＲＯＭ（Ｒｅａｄ Ｏｎｌｙ Ｍｅｍｏｒｙ）３０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）３０３と、磁気ディスクドライブ３０４と、磁気ディスク３０５と、光ディスクドライブ３０６と、光ディスク３０７と、ディスプレイ３０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）３０９と、キーボード３１０と、マウス３１１と、スキャナ３１２と、プリンタ３１３と、を備えている。また、各構成部はバス３００によってそれぞれ接続されている。
【００２３】
ここで、ＣＰＵ３０１は、検証支援装置の全体の制御を司る。ＲＯＭ３０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ３０３は、ＣＰＵ３０１のワークエリアとして使用される。磁気ディスクドライブ３０４は、ＣＰＵ３０１の制御にしたがって磁気ディスク３０５に対するデータのリード／ライトを制御する。磁気ディスク３０５は、磁気ディスクドライブ３０４の制御で書き込まれたデータを記憶する。
【００２４】
光ディスクドライブ３０６は、ＣＰＵ３０１の制御にしたがって光ディスク３０７に対するデータのリード／ライトを制御する。光ディスク３０７は、光ディスクドライブ３０６の制御で書き込まれたデータを記憶したり、光ディスク３０７に記憶されたデータをコンピュータに読み取らせたりする。
【００２５】
ディスプレイ３０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ３０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００２６】
インターフェース（以下、「Ｉ／Ｆ」と略する。）３０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク３１４に接続され、このネットワーク３１４を介して他の装置に接続される。そして、Ｉ／Ｆ３０９は、ネットワーク３１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ３０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００２７】
キーボード３１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス３１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００２８】
スキャナ３１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ３１２は、ＯＣＲ（Ｏｐｔｉｃａｌ Ｃｈａｒａｃｔｅｒ Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ３１３は、画像データや文書データを印刷する。プリンタ３１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００２９】
＜検証支援装置の機能的構成＞
図４は、検証支援装置の機能的構成の一例を示すブロック図である。検証支援装置４００は、テストシナリオ短縮化処理部４０１と、シミュレーション実行部４０２と、ＦＳＭ検証処理部４０３と、登録／復元処理部４０４とを備える。テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶されたプログラムをＣＰＵ３０１に実行させることにより、その機能を実現する。
【００３０】
より具体的には、テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４により、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置から読み出されたデータは、ＲＡＭ３０３や磁気ディスク３０５、ＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。また、テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４により、ＣＰＵ３０１が実行した中間的なまたは最終的な実行結果は、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置やＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。
【００３１】
テストシナリオ短縮化処理部４０１は、テストシナリオ群ｔｓを構成するテストシナリオ間で重複する遷移パスを消去して短縮化テストシナリオ群Ｔｓとして出力する。テストシナリオ短縮化処理部４０１の詳細については、図５〜図７を用いて後述する。
【００３２】
シミュレーション実行部４０２は、対象回路のシミュレーションを実行する。具体的には、たとえば、対象回路のハードウェア記述情報（ＤＵＴ）４３０を読み込み、対象回路に短縮化テストシナリオ群Ｔｓを構成するテストシナリオを順次与えることで、テストシナリオごとに対象回路のシミュレーションを実行する。
【００３３】
ＦＳＭ検証処理部４０３は、シミュレーション実行部４０２によるシミュレーションの実行中に有限状態機械モデル１００を検証する。ＦＳＭ検証処理部４０３の詳細については、図８および図９を用いて後述する。
【００３４】
登録／復元処理部４０４は、シミュレーション実行部４０２によるシミュレーションの実行中に、登録／復元対象となった状態をデータベース４２０に登録したり、データベース４２０から読み出して復元する。登録／復元処理部４０４の詳細については、図１０〜図１３を用いて後述する。
【００３５】
＜テストシナリオ短縮化処理部４０１の詳細説明＞
（テストシナリオ短縮化処理部４０１の機能的構成）
図５は、テストシナリオ短縮化処理部４０１の機能的構成を示すブロック図である。テストシナリオ短縮化処理部４０１は、選択部５０１と、検出部５０２と、遷移数特定部５０３と、決定部５０４と、埋込部５０５と、登録／復元対象判断部５０６と、を備えている。
【００３６】
選択部５０１は、対象回路に関するテストシナリオ群の中から一のテストシナリオを選択する。具体的には、たとえば、テストシナリオ群ｔｓを構成するｎ個のテストシナリオｔ１，ｔ２，…，ｔｉ，…，ｔｎから順次選択する。なお、テストシナリオ群ｔｓは、図３に示したＲＯＭ３０２，磁気ディスク３０５などの記憶装置に記憶されている。
【００３７】
また、選択部５０１は、選択テストシナリオを構成する一連の要素（ｓｔｉｍｕｌｕｓ）の中から順次要素（ｓｔｉｍｕｌｉ）を選択する。テストシナリオは、時系列的に対象回路に与える要素の集合である。たとえば、図１に示したテストシナリオｔ１＝｛ａ，ｂ，ｃ｝では、ａ〜ｃは要素（たとえば、入力パターン）である。したがって、テストシナリオｔ１では、“ａ”は（Ｓ０→Ｓ１）を示し、“ｂ”は（Ｓ１→Ｓ３）を示し、“ｃ”は（Ｓ３→Ｓ６）を示す。選択部５０１では、ａ→ｂ→ｃの順に要素を選択する。
【００３８】
検出部５０２は、選択部５０１によって選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、対象回路に関する有限状態機械モデル１００の中から検出する。上述したテストシナリオｔ１を例に挙げると、要素ａを選択要素とした場合、要素ａは状態遷移（Ｓ０→Ｓ１）であるため、要素ａが対象回路に与えられると、対象回路の状態が状態Ｓ０から状態Ｓ１に遷移する。したがって、検出部５０２は、要素ａによる遷移先状態Ｓ１を検出する。すなわち、選択要素が状態遷移（Ｓｊ→Ｓｋ）の場合、検出部５０２は、状態Ｓｋを遷移先状態として検出することになる。なお、状態Ｓｊは遷移元状態である。
【００３９】
遷移数特定部５０３は、検出部５０２によって検出された遷移先状態への入力遷移数と遷移先状態からの出力遷移数を、有限状態機械モデル１００の中から特定する。ここで、入力遷移数とは、検出遷移先状態を遷移先状態として指定する状態遷移の個数である。また、出力遷移数とは、検出遷移先状態を遷移元状態とした場合の検出遷移先状態からの状態遷移の個数である。
【００４０】
たとえば、図１の有限状態機械モデル１００において検出遷移先状態を状態Ｓ３とする。状態Ｓ３は、状態Ｓ１からの遷移先状態であり、それ以外の状態から状態遷移されない。したがって、状態Ｓ３の入力遷移数は、１である。また、状態Ｓ３は、状態Ｓ６，Ｓ７，Ｓ８という３つの状態に遷移する。したがって、状態Ｓ３の出力遷移数は、３である。
【００４１】
決定部５０４は、遷移数特定部５０３によって特定された出力遷移数が入力遷移数よりも多い場合、遷移先状態を登録／復元対象に決定する。ここで、登録／復元対象とは、データベース４２０に登録され、かつ、データベース４２０から読み出されて復元される状態（レジスタに保持される値）である。上述した例では、状態Ｓ３が検出遷移先状態であるが、状態Ｓ３の出力遷移数（３個）は、状態Ｓ３の入力遷移数（１個）よりも多いため、状態Ｓ３は、図１の（Ｂ）に示したように登録／復元対象となる。
【００４２】
埋込部５０５は、決定部５０４によって決定された登録／復元対象をデータベース４２０に登録させる登録指示情報を、一のテストシナリオ内の一の選択要素の次の要素として埋め込む。ここで、登録指示情報とは、登録／復元対象となる状態を、データベース４２０にその状態を登録させる情報である。本実施の形態では、登録／復元対象を状態Ｓｉとすると、“ｒｅｃｏｒｄ（Ｓｉ）”を登録指示情報とする。埋込部５０５は、対象となっているテストシナリオ内において、登録指示情報を、その登録／復元対象に状態遷移させる要素の次の要素に埋め込む。
【００４３】
図６は、有限状態機械モデルにおけるテストシナリオ群の埋込前後の関係を示す説明図である。図６において、（Ａ）は、埋込前のテストシナリオ群ｔｓを示しており、（Ｂ）は、埋込後の短縮化テストシナリオ群Ｔｓを示している。（Ｃ）は、埋込前のテストシナリオ群ｔｓでのシミュレーションの実行内容を示しており、（Ｄ）は、埋込後の短縮化テストシナリオ群Ｔｓでのシミュレーションの実行内容を示している。
【００４４】
（Ｃ）において、テストシナリオｔ１の状態Ｓ３では、出力遷移数が３、入力遷移数が１となる。したがって、埋込部５０５により、テストシナリオｔ１の要素ｂの次の要素として、要素ｃの前に、“ｒｅｃｏｒｄ（Ｓ３）”を要素として埋め込む。これにより、テストシナリオｔ１が、（Ｄ）に示したようにテストシナリオＴ１に変換される。
【００４５】
また、図５において、埋込部５０５は、登録／復元対象をデータベース４２０から復元させる復元指示情報を、他のテストシナリオを構成する一連の要素の先頭要素から他の選択要素までの要素群に代えて、他のテストシナリオに埋め込む。ここで、復元指示情報とは、登録／復元対象となる状態を、データベース４２０からその状態を復元させる情報である。
【００４６】
本実施の形態では、登録／復元対象を状態Ｓｉとすると、“ｒｅｓｔｏｒｅ（Ｓｉ）”を復元指示情報とする。埋込部５０５は、対象となっているテストシナリオ内において、その登録／復元対象までの要素列を削除して、その要素列の代わりに復元指示情報を埋め込む。
【００４７】
（Ａ）において、テストシナリオｔ１，ｔ２では要素列｛ａ，ｂ｝が重複しているため、要素ｂの遷移先状態Ｓ３が、テストシナリオＴ１において、登録指示情報により指定されている。したがって、埋込部５０５により、テストシナリオｔ２の初期の要素ａから要素ｂまでの要素列｛ａ，ｂ｝を消去して、要素列｛ａ，ｂ｝の位置に“ｒｅｓｔｏｒｅ（Ｓ３）”を要素として埋め込む。これにより、テストシナリオｔ２がテストシナリオＴ２に変換される。
【００４８】
また、図５において、登録／復元対象判断部５０６は、検出部５０２によって、一のテストシナリオ以外の他のテストシナリオを構成する一連の要素の中から選ばれた他の選択要素による遷移先状態が、有限状態機械モデルの中から検出された場合、一のテストシナリオにおいて埋込部５０５によって埋め込まれた登録指示情報が指定する登録／復元対象と一致するか否かを判断する。
【００４９】
具体的には、たとえば、図６において、テストシナリオｔ１がテストシナリオＴ１に変換された後、未変換のテストシナリオｔ２が選択された場合、テストシナリオｔ２の先頭要素ａから順次遷移先状態を探索する。そして、探索された状態が、登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”が指定する登録／復元対象（状態Ｓ３）と一致するか否かを判断する。
【００５０】
テストシナリオｔ２では、要素ｂの遷移先状態Ｓ３で登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”が指定する登録／復元対象（状態Ｓ３）と一致する。したがって、図６の（Ｂ）に示したように、テストシナリオｔ２の要素列｛ａ，ｂ｝を消去して、要素列｛ａ，ｂ｝の位置に“ｒｅｓｔｏｒｅ（Ｓ３）”を要素として埋め込む。
【００５１】
したがって、図６の（Ｃ）に示したように、従来だと、テストシナリオｔ１で対象回路のシミュレーションを実行したときに、ａ→ｂ→ｃの順で状態遷移し、その後、テストシナリオｔ２で対象回路のシミュレーションを実行したときに、ａ→ｂ→ｄの順で状態遷移した。
【００５２】
これに対し、本実施の形態では、図６の（Ｄ）に示したように、テストシナリオＴ１で対象回路のシミュレーションを実行したときに、ａ→ｂの順で状態遷移したあと、登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”により、要素ｂの遷移先状態Ｓ３（でのレジスタの値）をデータベース４２０に記録する。そして、ｃにより状態遷移させる。
【００５３】
つぎに、テストシナリオＴ２で対象回路のシミュレーションを実行したときに、テストシナリオｔ２のように、ａ→ｂの順で状態遷移させずに、復元指示情報“ｒｅｓｔｏｒｅ（Ｓ３）”によりデータベース４２０から状態Ｓ３（のレジスタの値）を復元する。その後、要素ｄにより状態遷移させる。これにより、シミュレーション時間が大幅に短縮されることになる。
【００５４】
（テストシナリオ短縮化処理部４０１によるテストシナリオ短縮化処理）
図７は、テストシナリオ短縮化処理部４０１によるテストシナリオ短縮化処理手順を示すフローチャートである。まず、テストシナリオ短縮化処理部４０１は、対象回路に関する有限状態機械モデル１００と対象回路に関するテストシナリオ群ｔｓを取得する（ステップＳ７０１）。具体的には、テストシナリオ短縮化処理部４０１は、有限状態機械モデル１００と対象回路に関するテストシナリオ群ｔｓを検証支援装置４００に読み込ませる。
【００５５】
つぎに、テストシナリオ短縮化処理部４０１は、未選択のテストシナリオがあるか否かを判断する（ステップＳ７０２）。未選択のテストシナリオがない場合（ステップＳ７０２：Ｎｏ）、テストシナリオ短縮化処理を終了する。一方、未選択のテストシナリオがある場合（ステップＳ７０２：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、未選択のテストシナリオを選択する（ステップＳ７０３）。そして、テストシナリオ短縮化処理部４０１は、選択テストシナリオの中で、未選択の要素があるか否かを判断する（ステップＳ７０４）。
【００５６】
未選択の要素がない場合（ステップＳ７０４：Ｎｏ）、テストシナリオ短縮化処理部４０１は、次のテストシナリオを選択させるため、ステップＳ７０２に戻る。一方、未選択の要素がある場合（ステップＳ７０４：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、未選択の要素のうち先頭の要素を選択する（ステップＳ７０５）。
【００５７】
つぎに、テストシナリオ短縮化処理部４０１は、選択要素による遷移先状態の入力遷移数と出力遷移数とを検出する（ステップＳ７０６）。そして、テストシナリオ短縮化処理部４０１は、出力遷移数＞入力遷移数であるか否かを判断する（ステップＳ７０７）。出力遷移数＞入力遷移数でない場合（ステップＳ７０７：Ｎｏ）、登録／復元の対象外であるため、ステップＳ７０４に戻る。一方、出力遷移数＞入力遷移数である場合（ステップＳ７０７：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、遷移先状態が登録／復元対象に設定済みであるか否かを判断する（ステップＳ７０８）。
【００５８】
たとえば、テストシナリオ短縮化処理部４０１は、選択済みのテストシナリオ内の登録指示情報により、遷移先状態が指定されているか否かにより判断する。指定されていなければ、設定済みでないことになり、指定されていれば、設定済みとなる。たとえば、選択済みのテストシナリオ内にすでに、“ｒｅｃｏｒｄ（Ｓ３）”が埋め込まれている場合に、遷移先状態Ｓ３は、登録／復元対象に設定済みとなる。
【００５９】
そして、設定済みでない場合（ステップＳ７０８：Ｎｏ）、テストシナリオ短縮化処理部４０１は、遷移先状態を登録／復元対象として指定してデータベース４２０に登録させる登録指示情報を生成する（ステップＳ７０９）。そして、テストシナリオ短縮化処理部４０１は、生成された登録指示情報を選択要素の次の要素との間に追加して（ステップＳ７１０）、ステップＳ７０４に戻る。
【００６０】
一方、ステップＳ７０８において、登録／復元対象に設定済みである場合（ステップＳ７０８：Ｙｅｓ）、すでに、遷移先状態を指定する登録指示情報が存在する。したがって、テストシナリオ短縮化処理部４０１は、遷移先状態をデータベース４２０から復元させる復元指示情報を生成する（ステップＳ７１１）。そして、テストシナリオ短縮化処理部４０１は、遷移先状態までの遷移列を消去して、その位置に生成された復元指示情報を追加する（ステップＳ７１２）。このあと、ステップＳ７０４に戻る。
【００６１】
このようなテストシナリオ短縮化処理により、テストシナリオ群ｔｓ（ｔ１，ｔ２，…）が短縮化テストシナリオ群Ｔｓ（Ｔ１，Ｔ２，…）に短縮化されることとなる。
【００６２】
＜ＦＳＭ検証処理部４０３の詳細説明＞
（ＦＳＭ検証処理部４０３の機能的構成）
つぎに、図４に示したＦＳＭ検証処理部４０３について具体的に説明する。ＦＳＭ検証処理部４０３は、対象回路に関する有限状態機械モデル１００での状態遷移と実際にシミュレーションを実行したときの状態遷移との同一性を検証する。具体的には、ＦＳＭ検証処理部４０３は、対象回路のハードウェア記述情報４３０に短縮化テストシナリオ群Ｔｓ内のテストシナリオを順次与えることでシミュレーションを実行したときの状態遷移が、対象回路に関する有限状態機械モデル１００の状態遷移と一致するか否かを検証する。
【００６３】
図８は、ＦＳＭ検証処理部４０３の機能的構成を示すブロック図である。ＦＳＭ検証処理部４０３は、遷移先状態判断部８０１と、判断結果出力部８０２とを備えている。
【００６４】
遷移先状態判断部８０１は、対象回路のシミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態と、対象回路に関する有限状態機械モデル１００における対象要素による遷移先状態とが、一致するか否かを判断する。
【００６５】
具体的には、たとえば、テストシナリオＴ１を与えてシミュレーションを実行している場合、有限状態機械モデル１００では、現状態である状態Ｓ０の遷移先状態はＳ１であるのに対し、シミュレーションでの現状態である状態Ｓ０の次状態が状態Ｓ１であれば、一致すると判断する。一方、次状態が状態Ｓ１以外、たとえば、状態Ｓ２であれば、不一致と判断する。
【００６６】
判断結果出力部８０２は、遷移先状態判断部８０１によって判断された判断結果を出力する。判断結果とは、遷移先状態判断部８０１によってすべて一致した場合には、合格としてレポートを出力する。一方、遷移先状態判断部８０１によって不一致が発生した場合、シミュレーションの中止指示情報をシミュレーション実行部４０２に出力する。シミュレーション実行部４０２は、中止指示情報を受け付けると、シミュレーションを中止する。
【００６７】
この場合は、短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との間に不整合が生じているため、設計者は、短縮化テストシナリオ群Ｔｓ（またはテストシナリオ群ｔｓ）と有限状態機械モデル１００の修正を、コンピュータを操作して手作業によりおこなう。そして、修正後に再度、ＦＳＭ検証処理部４０３により検証処理をおこなう。
【００６８】
（ＦＳＭ検証処理部４０３によるＦＳＭ検証処理）
図９は、ＦＳＭ検証処理部４０３によるＦＳＭ検証処理手順を示すフローチャートである。まず、ＦＳＭ検証処理部４０３は、シミュレーションの開始を待ち受け（ステップＳ９０１：Ｎｏ）、シミュレーションが開始された場合（ステップＳ９０１：Ｙｅｓ）、シミュレーションの終了を待ち受ける（ステップＳ９０２）。シミュレーションは、問題なく最後まで実行されて終了する場合と、ＦＳＭ検証処理部４０３からシミュレーション実行部４０２に中止指示情報が出力された結果、シミュレーションが終了する場合がある。
【００６９】
シミュレーションが終了していない場合（ステップＳ９０２：Ｎｏ）、ＦＳＭ検証処理部４０３は、シミュレーションでの選択テストシナリオおよびその選択要素をシミュレーション実行部４０２からの情報により検出する（ステップＳ９０３）。そして、ＦＳＭ検証処理部４０３は、シミュレーション実行部４０２からの情報により状態遷移が発生したか否かを判断する（ステップＳ９０４）。状態遷移が発生していない場合（ステップＳ９０４：Ｎｏ）、ステップＳ９０２に戻る。
【００７０】
一方、状態遷移が発生した場合（ステップＳ９０４：Ｙｅｓ）、ＦＳＭ検証処理部４０３は、次状態と有限状態機械モデル１００での遷移先状態が一致するか否かを判断する（ステップＳ９０５）。一致する場合（ステップＳ９０５：Ｙｅｓ）、ステップＳ９０２に戻る。一方、不一致である場合（ステップＳ９０５：Ｎｏ）、中止指示情報をシミュレーション実行部４０２に出力して（ステップＳ９０６）、ステップＳ９０２に戻る。
【００７１】
また、ステップＳ９０２においてシミュレーションの終了が検出された場合（ステップＳ９０２：Ｙｅｓ）、ＦＳＭ検証処理部４０３は、検証結果（合格または不合格）のレポートを出力する（ステップＳ９０７）。中止指示情報が一度も出力されていない場合は合格を示すレポートを出力する。一方、中止指示情報が出力された場合は、不合格を示すレポートを出力する。
【００７２】
このようなＦＳＭ検証処理により、それぞれ独立して作成された短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との不整合を自動で検出することができる。また、不整合がない場合（不一致がない場合）は、短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との間で整合性がとれていることを保証することができる。
【００７３】
＜登録／復元処理部４０４の詳細説明＞
（登録／復元処理部４０４の機能的構成）
つぎに、図４に示した登録／復元処理部４０４について具体的に説明する。登録／復元処理部４０４は、シミュレーションの実行中に、登録／復元対象となる遷移先状態を特定して、遷移先状態（となるレジスタの値）をデータベース４２０に登録したり、登録された遷移先状態（となるレジスタの値）をデータベース４２０から読み出して復元する。
【００７４】
図１０は、登録／復元処理部４０４の機能的構成を示すブロック図である。登録／復元処理部４０４は、シナリオ抽出部１００１と、判別部１００２と、登録部１００４と、判定部１００３と、復元部１００５と、を備えている。
【００７５】
シナリオ抽出部１００１は、特定の遷移先状態をデータベース４２０に登録させる登録指示情報が埋め込まれたテストシナリオと、特定の遷移先状態をデータベース４２０から復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出する。
【００７６】
具体的には、たとえば、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを順次抽出する。
【００７７】
判別部１００２は、シナリオ抽出部１００１によって抽出された対象テストシナリオを構成する一連の要素の中から対象回路に対象要素を順次与えて模擬する対象回路のシミュレーションの実行中に、対象要素の種類を判別する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓを構成するテストシナリオには、登録指示情報が埋め込まれているテストシナリオＴ１や復元指示情報が埋め込まれているテストシナリオＴ２が存在する。
【００７８】
判別部１００２は、対象テストシナリオの中から対象回路に与えられた対象要素の種別が、（Ｓｊ→Ｓｋ）といった遷移をあらわす要素であるか、登録指示情報ｒｅｃｏｒｄ（Ｓｋ）であるか、復元指示情報ｒｅｓｔｏｒｅ（Ｓｋ）であるかを判別する。
【００７９】
登録部１００４は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態をデータベース４２０に登録する。具体的には、たとえば、登録指示情報が“ｒｅｃｏｒｄ（Ｓｋ）”である場合、状態Ｓｋ、すなわち、対象回路内の組み合わせ回路の出力先となるレジスタの値を、状態Ｓｋの識別子と関連付けてデータベース４２０に登録する。
【００８０】
図１１は、データベース４２０の記憶内容の一例を示す説明図である。データベース４２０は、状態名項目とコンテキスト情報項目とを有し、状態ごとにコンテキスト情報が登録される。ここで、コンテキスト情報とは、対象回路内のレジスタを識別する識別子（たとえば、レジスタ名）とレジスタの値である。図１１では、状態Ｓ３のレジスタｒ１〜ｒｍの値が登録されている。
【００８１】
図１０に戻って、判定部１００３は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態までのシミュレーション時間とデータベース４２０からの所定の復元時間とに基づいて、登録部１００４により登録すべきか否かを判定する。
【００８２】
ここで、特定の遷移先状態までのシミュレーション時間については、シミュレーション実行部４０２により計測されるものとする。たとえば、状態Ｓ０〜Ｓｋまでのシミュレーション時間を、ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）とする。また、データベース４２０への登録時間をＲｅｃとし、データベース４２０からの復元時間をＲｅｓとする。登録時間Ｒｅｃと復元時間Ｒｅｓはあらかじめ設定される。
【００８３】
ここで、特定の遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）を求める。遷移数差分Ｎ（Ｓｋ）は、下記式で表現される。
【００８４】
Ｎ（Ｓｋ）＝Ｎｏｕｔ（Ｓｋ）−Ｎｉｎ（Ｓｋ）・・・・・・・・・・・・・・・（２）
ただし、Ｎｏｕｔ（Ｓｋ）は遷移先状態Ｓｋの出力遷移数、Ｎｉｎ（Ｓｋ）は遷移先状態Ｓｋの入力遷移数である。
【００８５】
そして、下記式（３）を満たすことにより、遷移先状態Ｓｋをデータベース４２０に登録すべきであるか否かを判断する。
【００８６】
Ｎ（Ｓｋ）×ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）＞Ｒｅｃ＋Ｎ（Ｓｋ）×Ｒｅｓ・・・（３）
ただし、Ｎ（Ｓｋ）＞０
【００８７】
シミュレーションは通常複数回実行されるため、１回目のシミュレーションでシミュレーション時間が最短となる状態Ｓｋを特定し、２回目以降は、最短となる状態ＳｋのＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）を適用する。たとえば、テストシナリオｔ１〜ｔ３が同一の状態Ｓ１０を通過する場合、テストシナリオｔ１〜ｔ３ごとに、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）を計測する。
【００８８】
そして、２回目以降のシミュレーションでは、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）が最短となるテストシナリオ（たとえば、テストシナリオｔ２）のＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）を採用する。この場合、上記式（３）は、下記式（４）となる。
【００８９】
Ｎ（Ｓｋ）×Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］＞Ｒｅｃ＋Ｎ（Ｓｋ）×Ｒｅｓ
・・・（４）
ただし、Ｎ（Ｓｋ）＞０
【００９０】
なお、Ｎ（Ｓｋ）が大きければ大きいほど、右辺の第２項Ｎ（Ｓｋ）×Ｒｅｓが大きくなるので、右辺第１項の記録時間Ｒｅｃは無視できる。したがって、Ｎ（Ｓｋ）があらかじめ設定したしきい値以上となった場合、上記（４）式は下記（５）式になる。
【００９１】
Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］＞Ｒｅｓ・・・（５）
【００９２】
したがって、判定部１００３は、式（５）が成立したときは、そのときの遷移先状態をデータベース４２０に登録すべきと判定し、成立しなかったときは登録すべきでないと判定する。
【００９３】
復元部１００５は、判別部１００２により対象要素が復元指示情報であると判別された場合、特定の遷移先状態をデータベース４２０から復元する。ここで、復元とは、特定の遷移先状態（のレジスタの値）をデータベース４２０から読み出して、対象回路内のレジスタに書き込む処理である。本実施の形態は、シミュレーションであるため、モデル化された対象回路のレジスタに、データベース４２０から読み出したレジスタの値を設定することとなる。
【００９４】
具体的には、たとえば、図６の（Ｄ）においてテストシナリオＴ２を与えてシミュレーションした場合に、状態Ｓ３までのシミュレーションを実行しなくても状態Ｓ３が復元される。このように、特定の遷移先状態を復元することで、特定の遷移先状態までシミュレーションする必要がなく、シミュレーション時間の短縮化を図ることができる。
【００９５】
たとえば、特定の遷移先状態Ｓｋまでの最短シミュレーション時間Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］が復元時間Ｒｅｓよりも大きい場合に、その差が、たとえば、１［ｍｓｅｃ］あったとする。そして、遷移数差分Ｎ（Ｓｋ）がＮ（Ｓｋ）＝１０００であったとすると、短縮後では、特定の遷移先状態Ｓｋを通るテストシナリオ群について、１０００×１［ｍｓｅｃ］＝１［ｓｅｃ］もシミュレーション時間を短縮することができる。
【００９６】
（登録／復元処理部４０４による登録／復元処理）
図１２は、登録／復元処理部４０４による登録／復元処理手順を示すフローチャート（その１）である。まず、登録／復元処理部４０４は、シミュレーションの開始を待ち受け（ステップＳ１２０１：Ｎｏ）、シミュレーションが開始された場合（ステップＳ１２０１：Ｙｅｓ）、シミュレーションの終了を待ち受ける（ステップＳ１２０２）。シミュレーションは、問題なく最後まで実行されて終了する場合と、ＦＳＭ検証処理部４０３からシミュレーション実行部４０２に中止指示情報が出力された結果、シミュレーションが終了する場合がある。シミュレーションが終了した場合（ステップＳ１２０２：Ｙｅｓ）、登録／復元処理は終了する。
【００９７】
一方、シミュレーションが終了していない場合（ステップＳ１２０２：Ｎｏ）、登録／復元処理部４０４は、短縮化テストシナリオ群Ｔｓの中から未選択のテストシナリオがあるか否かを判断する（ステップＳ１２０３）。未選択のテストシナリオがない場合（ステップＳ１２０３：Ｎｏ）、登録／復元処理は終了する。
【００９８】
一方、未選択のテストシナリオがある場合（ステップＳ１２０３：Ｙｅｓ）、登録／復元処理部４０４は、未選択のテストシナリオを選択する（ステップＳ１２０４）。そして、登録／復元処理部４０４は、選択テストシナリオ内に未選択の要素があるか否かを判断する（ステップＳ１２０５）。未選択の要素がない場合（ステップＳ１２０５：Ｎｏ）、選択テストシナリオ内の要素はすべてシミュレーションされたため、ステップＳ１２０３に戻る。
【００９９】
一方、未選択の要素がある場合（ステップＳ１２０５：Ｙｅｓ）、登録／復元処理部４０４は、未選択の要素を先頭から抽出する（ステップＳ１２０６）。そして、登録／復元処理部４０４は、抽出要素が復元指示情報であるか否かを判断する（ステップＳ１２０７）。復元指示情報である場合（ステップＳ１２０７：Ｙｅｓ）、登録／復元処理部４０４は、復元指示情報で指定されている状態のコンテキスト情報をデータベース４２０から読み出して復元する（ステップＳ１２０８）。そして、ステップＳ１２０５に戻る。
【０１００】
一方、ステップＳ１２０７において、復元指示情報でない場合（ステップＳ１２０７：Ｎｏ）、図１３のステップＳ１３０１に移行する。
【０１０１】
図１３は、登録／復元処理部４０４による登録／復元処理手順を示すフローチャート（その２）である。まず、登録／復元処理部４０４は、ステップＳ１２０６において抽出された抽出要素を対象回路のハードウェア記述情報４３０に与える（ステップＳ１３０１）。これにより、シミュレーション実行部４０２では、対象回路のシミュレーションが実行される。そして、状態遷移の発生を待ち受ける（ステップＳ１３０２）。
【０１０２】
状態遷移が発生しなかった場合（ステップＳ１３０２：Ｎｏ）、末尾の状態に到達したこととなり、シミュレーション実行部４０２からその旨の通知を受けることになる。この場合は、ステップＳ１２０５に戻る。この場合、ステップＳ１２０５に戻っても未選択要素がないため、ステップＳ１２０３に戻ることになる。なお、現状態から次状態への状態遷移については、状態遷移が発生したものとする。
【０１０３】
一方、ステップＳ１３０２において、状態遷移が発生した場合（ステップＳ１３０２：Ｙｅｓ）、登録／復元処理部４０４は、発生した状態遷移による遷移先状態Ｓｋが登録／復元対象であるか否かを判断する（ステップＳ１３０３）。具体的には、遷移先状態Ｓｋが、すでに他のテストシナリオにおいて登録指示情報で指定されているか否かを判断する。
【０１０４】
遷移先状態が登録／復元対象でない場合（ステップＳ１３０３：Ｎｏ）、ステップＳ１２０５に戻る。一方、遷移先状態が登録／復元対象である場合（ステップＳ１３０３：Ｙｅｓ）、登録／復元処理部４０４は、初期状態Ｓ０から遷移先状態Ｓｋまでのシミュレーション時間をシミュレーション実行部４０２から取得する（ステップＳ１３０４）。そして、登録／復元処理部４０４は、遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）に復元時間Ｒｅｓを乗じた値（Ｎ（Ｓｋ）×Ｒｅｓ）が所定のしきい値Ｔに記録時間Ｒｅｃを乗じた値（Ｔ×Ｒｅｃ）以上であるか否かを判断する（ステップＳ１３０５）。
【０１０５】
Ｎ（Ｓｋ）×Ｒｅｓ≧Ｔ×Ｒｅｃである場合（ステップＳ１３０５：Ｙｅｓ）、登録／復元処理部４０４は、式（５）を満たすか否かを判断する（ステップＳ１３０６）。式（５）を満たさない場合（ステップＳ１３０６：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（５）を満たす場合（ステップＳ１３０６：Ｙｅｓ）、登録／復元処理部４０４は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ１３０７）、ステップＳ１２０５に戻る。
【０１０６】
一方、ステップＳ１３０５において、Ｎ（Ｓｋ）≧Ｔでない場合（ステップＳ１３０５：Ｎｏ）、登録／復元処理部４０４は、式（４）を満たすか否かを判断する（ステップＳ１３０８）。式（４）を満たさない場合（ステップＳ１３０８：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（４）を満たす場合（ステップＳ１３０８：Ｙｅｓ）、登録／復元処理部４０４は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ１３０９）、ステップＳ１２０５に戻る。
【０１０７】
このような登録／復元処理によれば、どの状態を復元すればよいかが自動設定されているため、設計者が試行錯誤して登録／復元対象を探す必要はない。したがって、対象回路のシミュレーションを効率的に短縮化することができる。
【０１０８】
・実施の形態２
つぎに、実施の形態２について説明する。上述した実施の形態１では、設計者が対象回路について、テストシナリオ群ｔｓと有限状態機械モデル１００の両方を作成した例について説明したが、テストシナリオ群ｔｓと有限状態機械モデル１００との不整合をあらかじめ回避するため、実施の形態２では、テストシナリオ群ｔｓから有限状態機械モデル１００を自動生成する。
【０１０９】
また、自動生成した場合に、同一状態が別々の状態として生成されることがあるため、実施の形態２では、本来同一の状態であるが別々に生成された状態どうしを統合して、有限状態機械モデル１００を自動修正する。これにより、修正後の有限状態機械モデル（以下、「修正済ＦＳＭ」）１４００は、修正前に比べて冗長さが低減される。
【０１１０】
また、統合により、統合された状態は、登録／復元対象になる可能性がある。したがって、データベース４２０からコンテキスト情報を復元することが可能となるため、シミュレーション時間の短縮化も図ることができる。以下、実施の形態２について説明するが、実施の形態１と同一箇所には同一符号を付し、その説明を省略する。
【０１１１】
＜ＦＳＭ修正＞
図１４は、有限状態機械モデル１００の修正例を示す説明図である。図１４において、（Ａ）は修正前の有限状態機械モデル１００を示しており、（Ｂ）は修正済ＦＳＭ１４００を示している。
【０１１２】
なお、（Ａ）の状態での短縮化テストシナリオ群Ｔｓは以下のとおりである。
Ｔ１＝｛ａ，ｂ，ｃ，ｒｅｃｏｒｄ（Ｓ８），ｅ｝
Ｔ２＝｛ｆ，ｇ，ｈ，ｊ｝
Ｔ３＝｛ｒｅｓｔｏｒｅ（Ｓ８），ｄ｝
【０１１３】
また、修正済ＦＳＭ１４００により、短縮化テストシナリオ群Ｔｓを修正すると、以下のとおりである。
Ｔ１＝｛ａ，ｂ，ｃ，ｒｅｃｏｒｄ（Ｓ８），ｅ｝
Ｔ２＝｛ｆ，ｇ，ｐ，ｑ｝
Ｔ３＝｛ｒｅｓｔｏｒｅ（Ｓ８），ｄ｝
【０１１４】
すなわち、状態Ｓ９が状態Ｓ８に統合されたため、テストシナリオＴ２の要素ｈ（Ｓ４→Ｓ９）は、要素ｐ（Ｓ４→Ｓ８）に修正される。同様に、テストシナリオＴ２の要素ｊ（Ｓ９→Ｓ１２）は、要素ｑ（Ｓ８→Ｓ１２）に修正される。このように、テストシナリオを修正することで、再度テストシナリオの短縮化をおこなうことができる。たとえば、テストシナリオＴ２は、データベース４２０に登録された状態Ｓ８を復元することで短縮化することが可能となる。
【０１１５】
＜検証支援装置の機能的構成＞
図１５は、検証支援装置の機能的構成の一例を示すブロック図である。検証支援装置１５００は、ＦＳＭ生成処理部１５０１と、テストシナリオ短縮化処理部４０１と、シミュレーション実行部４０２と、ＦＳＭ修正処理部１５０２と、登録／復元処理部１５０３とを備える。テストシナリオ短縮化処理部４０１およびシミュレーション実行部４０２は、実施の形態１と同一内容であるため説明を省略する。
【０１１６】
また、ＦＳＭ生成処理部１５０１〜登録／復元処理部１５０３は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶されたプログラムをＣＰＵ３０１に実行させることにより、その機能を実現する。
【０１１７】
より具体的には、ＦＳＭ生成処理部１５０１〜登録／復元処理部１５０３により、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置から読み出されたデータは、ＲＡＭ３０３や磁気ディスク３０５、ＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。また、ＦＳＭ生成処理部１５０１〜ＦＳＭ修正処理部１５０２により、ＣＰＵ３０１が実行した中間的なまたは最終的な実行結果は、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置やＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。
【０１１８】
ＦＳＭ生成処理部１５０１は、対象回路に関するテストシナリオ群ｔｓから対象回路に関する有限状態機械モデル１００を自動生成する。ＦＳＭ生成処理部１５０１の詳細については、図１６および図１７を用いて後述する。
【０１１９】
ＦＳＭ修正処理部１５０２は、シミュレーション実行部４０２によるシミュレーションの実行中に、ＦＳＭ生成処理部１５０１によって生成された有限状態機械モデル１００を、図１４に示したように修正する。登録対象となった状態をデータベース４２０に登録する機能も有する。ＦＳＭ修正処理部１５０２の詳細については、図１８および図１９を用いて後述する。
【０１２０】
登録／復元処理部１５０３は、シミュレーションの実行中に、登録／復元対象となる遷移先状態を特定して、遷移先状態（となるレジスタの値）をデータベース４２０に登録したり、登録された遷移先状態（となるレジスタの値）をデータベース４２０から読み出して復元する。
【０１２１】
＜ＦＳＭ生成処理部１５０１の詳細説明＞
（ＦＳＭ生成処理部１５０１の機能的構成）
図１６は、ＦＳＭ生成処理部１５０１の機能的構成を示すブロック図である。ＦＳＭ生成処理部１５０１は、更新部１６０５と、シナリオ抽出部１６０１と、遷移先状態特定部１６０２と、中間ＦＳＭ判断部１６０３と、設定部１６０４と、ＦＳＭ出力部１６０６とを備えている。
【０１２２】
更新部１６０５は、対象回路に関する有限状態機械モデル１００に対象状態列が追加されることにより、有限状態機械モデル１００を更新する。更新対象となる有限状態機械モデル１００を、中間ＦＳＭ１６００と称す。まだ１回も更新されていない中間ＦＳＭ１６００は、対象回路の初期状態Ｓ０のみである。
【０１２３】
そして、中間ＦＳＭ１６００に対象状態列が追加されることで、中間ＦＳＭ１６００が更新される。対象状態列とは、更新前の中間ＦＳＭ１６００には含まれていない状態列である。なお、対象状態列は、設定部１６０４により設定される。
【０１２４】
シナリオ抽出部１６０１は、対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する。具体的には、たとえば、テストシナリオ群ｔｓから順次テストシナリオを抽出する。
【０１２５】
遷移先状態特定部１６０２は、抽出部によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する。具体的には、たとえば、抽出テストシナリオの各要素による遷移先状態（レジスタの値。ただし、シミュレーションはまだ実行していないため、実際の０／１といった値ではなく変数でよい。）を検出することとなる。
【０１２６】
たとえば、選択テストシナリオｔ１がｔ１＝｛ａ，ｂ，ｃ，ｅ｝（ただし、ａ＝（Ｓ０→Ｓ１）、ｂ＝（Ｓ１→Ｓ３）、ｃ＝（Ｓ３→Ｓ８）、ｅ＝（Ｓ８→Ｓ１０））とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を特定する。
【０１２７】
中間ＦＳＭ判断部１６０３は、遷移先状態特定部１６０２によって特定された遷移先状態列が、有限状態機械モデル１００に含まれているか否かを判断する。具体的には、最新の中間ＦＳＭ１６００に、遷移先状態特定部１６０２によって特定された遷移先状態列が含まれているか否かを判断する。たとえば、上述の例において、最新の中間ＦＳＭ１６００が｛Ｓ０→Ｓ１｝とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝のうち、｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に含まれていないと判断する。
【０１２８】
これに対し、最新の中間ＦＳＭ１６００が｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０→Ｓ１５｝であるとすると、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０→Ｓ１５｝に、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が含まれていると判断される。
【０１２９】
設定部１６０４は、遷移先状態特定部１６０２によって特定された遷移先状態列のうち、中間ＦＳＭ判断部１６０３によって含まれていないと判断された遷移先状態列を対象状態列に設定して、有限状態機械モデル１００に追加させる。具体的には、上述した例では、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝のうち、｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に含まれていないと判断される。したがって、状態遷移列｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を対象状態列に設定する。
【０１３０】
これにより、更新部１６０５では、対象状態列｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に追加することで、中間ＦＳＭ１６００が更新され、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝となる。
【０１３１】
ＦＳＭ出力部１６０６は、シナリオ抽出部１６０１により未抽出のテストシナリオがない場合、更新部１６０５によって更新された最新の有限状態機械モデル１００を出力する。具体的には、テストシナリオがすべて抽出されると、もう中間ＦＳＭ１６００は更新する余地がない。したがって、最新の中間ＦＳＭ１６００を、完成された有限状態機械モデル１００として出力することとなる。出力された有限状態機械モデル１００は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶される。
【０１３２】
（ＦＳＭ生成処理部１５０１によるＦＳＭ生成処理）
図１７は、ＦＳＭ生成処理部１５０１によるＦＳＭ生成処理手順を示すフローチャートである。まず、ＦＳＭ生成処理部１５０１は、中間ＦＳＭ１６００として初期状態Ｓ０を設定する（ステップＳ１７０１）。つぎに、ＦＳＭ生成処理部１５０１は、シナリオ抽出部１６０１により、テストシナリオ群ｔｓの中から未抽出のテストシナリオがあるか否かを判断する（ステップＳ１７０２）。未抽出のテストシナリオがある場合（ステップＳ１７０２：Ｙｅｓ）、ＦＳＭ生成処理部１５０１は、未抽出のテストシナリオを１つ抽出する（ステップＳ１７０３）。
【０１３３】
そして、ＦＳＭ生成処理部１５０１は、遷移先状態特定部１６０２により、抽出テストシナリオから遷移先状態列を特定する（ステップＳ１７０４）。このあと、ＦＳＭ生成処理部１５０１は、中間ＦＳＭ判断部１６０３により、特定された遷移先状態列のうち、最新の中間ＦＳＭ１６００にない状態列が存在するか否かを判断する（ステップＳ１７０５）。最新の中間ＦＳＭ１６００にない状態列がない場合（ステップＳ１７０５：Ｎｏ）、ステップＳ１７０２に戻る。
【０１３４】
一方、最新の中間ＦＳＭ１６００にない状態列がある場合（ステップＳ１７０５：Ｙｅｓ）、ＦＳＭ生成処理部１５０１は、設定部１６０４により、特定された遷移先状態列のうち、最新の中間ＦＳＭ１６００にない状態列を、対象状態列に設定する（ステップＳ１７０６）。このあと、ＦＳＭ生成処理部１５０１は、更新部１６０５により、対象状態列を最新の中間ＦＳＭ１６００に追加する（ステップＳ１７０７）。これにより、中間ＦＳＭ１６００が更新される。
【０１３５】
そのあと、ステップＳ１７０２に戻る。ステップＳ１７０２において、未抽出のテストシナリオがない場合（ステップＳ１７０２：Ｎｏ）、ＦＳＭ生成処理部１５０１は、ＦＳＭ出力部１６０６により、最新の中間ＦＳＭ１６００を、完成された有限状態機械モデル１００として出力する（ステップＳ１７０８）。
【０１３６】
このように、ＦＳＭ生成処理部１５０１では、テストシナリオ群ｔｓを解析して中間ＦＳＭ１６００に追加することにより、中間ＦＳＭ１６００がいわゆる雪だるま式に大きくなり、テストシナリオ群ｔｓによる状態遷移を網羅する有限状態機械モデル１００を生成することができる。
【０１３７】
＜ＦＳＭ修正処理部１５０２の詳細説明＞
（ＦＳＭ修正処理部１５０２の機能的構成）
図１８は、ＦＳＭ修正処理部１５０２および登録／復元処理部１５０３の機能的構成を示すブロック図である。ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１と、遷移先状態判断部１８０２と、判断結果出力部１８０３と、仮決定部１８０４と、登録済判断部１８０５と、修正部１８０６と、修正済ＦＳＭ出力部１８０７と、登録部１８１４と、を備えている。
【０１３８】
シナリオ抽出部１８０１は、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを抽出する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを順次抽出する。対象テストシナリオが抽出されると、シミュレーション実行部４０２に与えられてシミュレーションが開始する。
【０１３９】
遷移先状態判断部１８０２は、対象回路のシミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態と、ＦＳＭ生成処理部１５０１によって生成された有限状態機械モデル１００における対象要素による遷移先状態とが、一致するか否かを判断する。
【０１４０】
具体的には、たとえば、テストシナリオＴ１を与えてシミュレーションを実行している場合、現状態Ｓ０について有限状態機械モデル１００では、状態Ｓ０の遷移先状態はＳ１であるのに対し、シミュレーションでの現状態Ｓ０の次状態が状態Ｓ１であれば、一致すると判断する。一方、次状態が状態Ｓ１以外、たとえば、状態Ｓ２であれば、不一致と判断する。
【０１４１】
判断結果出力部１８０３は、遷移先状態判断部１８０２によって判断された判断結果を出力する。遷移先状態判断部１８０２によって不一致が発生した場合、シミュレーションの中止指示情報をシミュレーション実行部４０２に出力する。シミュレーション実行部４０２は、中止指示情報を受け付けると、シミュレーションを中止する。一方、遷移先状態判断部１８０２によって一致した場合、仮決定部１８０４を実行する。
【０１４２】
仮決定部１８０４は、遷移先状態判断部１８０２によって一致すると判断された場合、シミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態をデータベース４２０への登録対象に仮決定する。具体的には、たとえば、遷移先状態判断部１８０２によって一致したときの状態Ｓｋを登録対象に仮決定する。
【０１４３】
登録済判断部１８０５は、仮決定部１８０４によって仮決定された登録対象が、データベース４２０に登録済みか否かを判断する。具体的には、データベース４２０を参照して、登録対象と同一のコンテキスト情報がデータベース４２０に登録済であるか否かを判断する。
【０１４４】
登録部１８１４は、登録済判断部１８０５により登録済でないと判断された場合、登録部１８１４により登録対象をデータベース４２０に登録することになる。一方、登録済判断部１８０５により登録済であると判断された場合、コンテキスト情報が同一で状態名が異なる状態がデータベース４２０に登録済であるため、修正部１８０６により有限状態機械モデル１００の修正を実行する。
【０１４５】
修正部１８０６は、登録済判断部１８０５によって登録済みであると判断された場合、登録対象への遷移元状態を、登録対象と一致する登録済みの遷移先状態への遷移元状態に修正し、登録対象からの遷移先状態を、登録済みの遷移先状態からの遷移先状態に修正する。
【０１４６】
具体的には、たとえば、図１４を例に挙げると、状態Ｓ９が登録対象であり、状態Ｓ８が状態Ｓ９に一致する登録済の状態とする。この場合、状態Ｓ９への遷移元状態である状態Ｓ４の遷移先を状態Ｓ８に設定する。すなわち、遷移ｈの遷移先を状態Ｓ８に変更して、遷移ｐとする。
【０１４７】
同様に、状態Ｓ９からの遷移先状態Ｓ１１，Ｓ１２のうち、状態Ｓ１１は、状態Ｓ８からの遷移先状態でもある。すなわち、状態Ｓ９からの遷移ｉは状態Ｓ８からの遷移ｅに一致するため、遷移ｉを削除する。また、状態Ｓ１２に遷移する遷移ｊの遷移元を状態Ｓ９から状態Ｓ８に変更し、遷移ｑとする。修正部１８０６では、登録済判断部１８０５から修正指示を受け付ける都度、修正処理を実行する。
【０１４８】
修正済ＦＳＭ出力部１８０７は、修正された修正済ＦＳＭ１４００を出力する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓ内のテストシナリオについてすべてシミュレーションが終了した場合、最終的に修正済ＦＳＭ１４００を出力する。修正済ＦＳＭ１４００は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶される。
【０１４９】
（ＦＳＭ修正処理部１５０２によるＦＳＭ修正処理）
図１９は、ＦＳＭ修正処理部１５０２によるＦＳＭ修正処理手順を示すフローチャートである。まず、ＦＳＭ修正処理部１５０２は、シミュレーションの開始を待ち受ける（ステップＳ１９０１：Ｎｏ）。シミュレーションが開始された場合（ステップＳ１９０１：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１により、未抽出のテストシナリオがあるか否かを判断する（ステップＳ１９０２）。
【０１５０】
短縮化テストシナリオ群Ｔｓの中で未抽出のテストシナリオがある場合（ステップＳ１９０２：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、未抽出のテストシナリオを抽出する（ステップＳ１９０３）。これにより、抽出テストシナリオがシミュレーション実行部４０２に与えられるため、状態遷移が発生することになる。
【０１５１】
そして、シミュレーション実行部４０２での状態遷移の発生が検出された場合（ステップＳ１９０４：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、発生した状態遷移による遷移先状態と有限状態機械モデル１００での遷移先状態とが一致するか否か判断する（ステップＳ１９０５）。
【０１５２】
不一致である場合（ステップＳ１９０５：Ｎｏ）、抽出テストシナリオと有限状態機械モデル１００との間に齟齬があるため、ＦＳＭ修正処理部１５０２は、判断結果出力部１８０３により、シミュレーション実行部４０２に対し中止指示情報を出力する（ステップＳ１９０６）。これにより、シミュレーション実行部４０２では、シミュレーションを中止することとなる。
【０１５３】
一方、ステップＳ１９０５において、一致すると判断された場合（ステップＳ１９０５：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、仮決定部１８０４により、シミュレーション実行部４０２による状態遷移の発生で得られた遷移先状態をデータベース４２０への登録対象に仮決定する（ステップＳ１９０７）。そして、ＦＳＭ修正処理部１５０２は、仮決定された登録対象と同一コンテキスト情報の状態がデータベース４２０に登録済であるか否かを、登録済判断部１８０５により判断する（ステップＳ１９０８）。
【０１５４】
登録済である場合（ステップＳ１９０８：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、修正部１８０６により有限状態機械モデル１００を修正して（ステップＳ１９０９）、ステップＳ１９０４に戻る。一方、登録済でない場合（ステップＳ１９０８：Ｎｏ）、ＦＳＭ修正処理部１５０２は、登録対象をデータベース４２０に登録して（ステップＳ１９１０）、ステップＳ１９０４に戻る。
【０１５５】
また、ステップＳ１９０４において、状態遷移が発生しなくなった場合（ステップＳ１９０４：Ｎｏ）、抽出テストシナリオによるシミュレーションが終了したこととなり、ステップＳ１９０２に戻る。ステップＳ１９０２において、ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１により、未抽出のテストシナリオがない場合（ステップＳ１９０２：Ｎｏ）、ＦＳＭ修正処理を終了する。
【０１５６】
＜登録／復元処理部１５０３の詳細説明＞
（登録／復元処理部１５０３の機能的構成）
つぎに、図１８を用いて、登録／復元処理部１５０３の機能的構成について説明する。登録／復元処理部１５０３は、判別部１００２と、登録部１８１４と、判定部１００３と、復元部１００５と、を備えている。判別部１００２、判定部１００３および復元部１００５については、実施の形態１と同一構成であるため、説明を省略する。
【０１５７】
判別部１００２は、シナリオ抽出部１８０１によって抽出された対象テストシナリオを構成する一連の要素の中から対象回路に対象要素を順次与えて模擬する対象回路のシミュレーションの実行中に、対象要素の種類を判別する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓを構成するテストシナリオには、登録指示情報が埋め込まれているテストシナリオＴ１や復元指示情報が埋め込まれているテストシナリオＴ２が存在する。
【０１５８】
判別部１００２は、対象テストシナリオの中から対象回路に与えられた対象要素の種別が、（Ｓｊ→Ｓｋ）といった遷移をあらわす要素であるか、登録指示情報ｒｅｃｏｒｄ（Ｓｋ）であるか、復元指示情報ｒｅｓｔｏｒｅ（Ｓｋ）であるかを判別する。
【０１５９】
登録部１８１４は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態をデータベース４２０に登録する。具体的には、たとえば、登録指示情報が“ｒｅｃｏｒｄ（Ｓｋ）”である場合、状態Ｓｋ、すなわち、対象回路内の組み合わせ回路の出力先となるレジスタの値を、状態Ｓｋの識別子と関連付けてデータベース４２０に登録する。ただし、実施の形態２では、ＦＳＭ修正処理部１５０２により登録済となる場合があるため、登録済の場合は、登録しない。
【０１６０】
（登録／復元処理部１５０３による登録／復元処理）
つぎに、登録／復元処理部１５０３による登録／復元処理について説明する。登録／復元処理については、実施の形態１において図１２および図１３を用いて説明したが、図１２の登録／復元処理手順を示すフローチャート（その１）については、実施の形態２においても同一処理であるため、説明を省略する。
【０１６１】
図２０は、登録／復元処理部１５０３による登録／復元処理手順を示すフローチャート（その３）である。まず、登録／復元処理部１５０３は、ステップＳ１２０６において抽出された抽出要素を対象回路のハードウェア記述情報４３０に与える（ステップＳ２００１）。これにより、シミュレーション実行部４０２では、対象回路のシミュレーションが実行される。そして、状態遷移の発生を待ち受ける（ステップＳ２００２）。
【０１６２】
状態遷移が発生しなかった場合（ステップＳ２００２：Ｎｏ）、末尾の状態に到達したこととなり、シミュレーション実行部４０２からその旨の通知を受けることになる。この場合は、ステップＳ１２０５に戻る。この場合、ステップＳ１２０５に戻っても未選択要素がないため、ステップＳ１２０３に戻ることになる。なお、現状態から次状態への状態遷移については、状態遷移が発生したものとする。
【０１６３】
一方、ステップＳ２００２において、状態遷移が発生した場合（ステップＳ２００２：Ｙｅｓ）、登録／復元処理部１５０３は、発生した状態遷移による遷移先状態Ｓｋが登録／復元対象であるか否かを判断する（ステップＳ２００３）。具体的には、遷移先状態Ｓｋが、すでに他のテストシナリオにおいて登録指示情報で指定されているか否かを判断する。
【０１６４】
発生した状態遷移による遷移先状態Ｓｋが登録／復元対象でない場合（ステップＳ２００３：Ｎｏ）、ステップＳ１２０５に戻る。一方、遷移先状態が登録／復元対象である場合（ステップＳ２００３：Ｙｅｓ）、登録／復元処理部１５０３は、発生した状態遷移による遷移先状態Ｓｋがすでにデータベース４２０に登録済であるか否かをコンテキスト情報により判断する（ステップＳ２００４）。具体的には、発生した状態遷移による遷移先状態Ｓｋに一致するコンテキスト情報がある場合は、登録済、ない場合は未登録と判断される。
【０１６５】
登録済である場合（ステップＳ２００４：Ｙｅｓ）、ステップＳ１２０５に戻る。未登録の場合（ステップＳ２００４：Ｎｏ）、登録／復元処理部１５０３は、初期状態Ｓ０から遷移先状態Ｓｋまでのシミュレーション時間をシミュレーション実行部４０２から取得する（ステップＳ２００５）。そして、登録／復元処理部１５０３は、遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）に復元時間Ｒｅｓを乗じた値（Ｎ（Ｓｋ）×Ｒｅｓ）が所定のしきい値Ｔに記録時間Ｒｅｃを乗じた値（Ｔ×Ｒｅｃ）以上であるか否かを判断する（ステップＳ２００６）。
【０１６６】
Ｎ（Ｓｋ）×Ｒｅｓ≧Ｔ×Ｒｅｃである場合（ステップＳ２００６：Ｙｅｓ）、登録／復元処理部１５０３は、式（５）を満たすか否かを判断する（ステップＳ２００７）。式（５）を満たさない場合（ステップＳ２００７：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（５）を満たす場合（ステップＳ２００７：Ｙｅｓ）、登録／復元処理部１５０３は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ２００８）、ステップＳ１２０５に戻る。
【０１６７】
一方、ステップＳ２００６において、Ｎ（Ｓｋ）≧Ｔでない場合（ステップＳ２００６：Ｎｏ）、登録／復元処理部１５０３は、式（４）を満たすか否かを判断する（ステップＳ２００９）。式（４）を満たさない場合（ステップＳ２００９：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（４）を満たす場合（ステップＳ２００９：Ｙｅｓ）、登録／復元処理部１５０３は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ２０１０）、ステップＳ１２０５に戻る。
【０１６８】
このような登録／復元処理によれば、ＦＳＭ修正処理部１５０２において登録されなかった状態についても復元すればよいかが自動設定されているため、設計者が試行錯誤して登録／復元対象を探す必要はない。したがって、対象回路のシミュレーションを効率的に短縮化することができる。
【０１６９】
以上説明したように、本実施の形態によれば、一のテストシナリオに登録指示情報を埋め込むことで、シミュレーション実行時に、登録／復元対象となる遷移先状態（対象回路を構成するレジスタの値）をデータベースに登録することができる。したがって、他のテストシナリオでシミュレーションを実行する場合、登録／復元対象に状態遷移したときは、データベースを参照することで、容易に復元することができる。
【０１７０】
また、データベースに登録された登録／復元対象を復元させる復元指示情報を他のテストシナリオに埋め込んでおくことで、シミュレーション時には、一のテストシナリオと重複するシナリオを実行することなく、データベースを参照するだけで登録／復元対象を復元することができる。このように、短縮化テストシナリオ群を自動生成することができるため、設計者は登録／復元対象を探したりする負担が軽減され、検証期間の短縮化を図ることができる。
【０１７１】
また、シミュレーションと並列に有限状態機械モデルを検証することができ、検証期間の短縮化を図ることができる。また、有限状態機械モデルと短縮化テストシナリオ群は、それぞれ独自に作成されるため、シミュレーションとＦＳＭ検証を並列実行すればその分、不整合を早期発見することができる。
【０１７２】
また、単に、データベースに状態を登録させるだけではなく、シミュレーション時間の短縮が見込めない場合、すなわち、登録および復元の処理時間よりも、重複したテストシナリオでシミュレーションを実行したほうが時間短縮になる場合には、登録／復元対象を登録しない。このように、時間短縮が可能か否かを詳細に判断することができるため、シミュレーションの効率化を図ることができる。
【０１７３】
また、有限状態機械モデルとテストシナリオ群は、それぞれ独自に作成されるが、テストシナリオ群を用いて有限状態機械モデルを自動生成することで、人手により作成する場合よりも整合性を保証することができ、検証精度の向上を図ることができる。
【０１７４】
また、有限状態機械モデルを自動生成した場合、冗長な表現になる場合があるため、シミュレーションの実行に並列して、有限状態機械モデルを修正することで、有限状態機械モデルの最適化を図ることができる。また、修正後の有限状態機械モデルにより短縮化テストシナリオ群の修正を設計者が施すことで、その後、テストシナリオ短縮化処理により、短縮化テストシナリオ群をさらに短縮化することができる。このように、シミュレーション回数を重ねるごとに、テストシナリオが短縮化されるため、シミュレーション時間もより効率的に短縮化することができる。
【０１７５】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムは、インターネット等のネットワークを介して配布してもよい。
【０１７６】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０１７７】
（付記１）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１７８】
（付記２）前記第２の埋込工程は、
前記第１の埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする付記１に記載の検証支援プログラム。
【０１７９】
（付記３）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１８０】
（付記４）前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態までのシミュレーション時間と前記データベースからの所定の復元時間とに基づいて、前記登録工程により登録すべきか否かを判定する判定工程を前記コンピュータに実行させ、
前記登録工程は、
前記判定工程によって登録すべきであると判定された場合、前記特定の遷移先状態を前記データベースに登録することを特徴とする付記３に記載の検証支援プログラム。
【０１８１】
（付記５）前記対象回路のシミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態と、前記対象回路に関する有限状態機械モデルにおける前記対象要素による遷移先状態とが、一致するか否かを判断する遷移先状態判断工程と、
前記遷移先状態判断工程によって判断された判断結果を出力する判断結果出力工程と、
を前記コンピュータに実行させることを特徴とする付記３または４に記載の検証支援プログラム。
【０１８２】
（付記６）前記判断結果出力工程は、
前記遷移先状態判断工程によって不一致と判断された場合、前記シミュレーションの中止指示情報を前記実行手段に出力することを特徴とする付記５に記載の検証支援プログラム。
【０１８３】
（付記７）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新工程と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出工程と、
前記抽出工程によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定工程と、
前記遷移先状態列特定工程によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断工程と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断工程によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定工程と、
前記抽出工程による未抽出のテストシナリオがない場合、前記更新工程によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１８４】
（付記８）前記テストシナリオ群の中から一のテストシナリオを選択する選択工程と、
前記選択工程によって選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、前記ＦＳＭ出力工程によって出力された有限状態機械モデルの中から検出する検出工程と、
前記検出工程によって検出された遷移先状態へ遷移する入力遷移数と前記遷移先状態から遷移する出力遷移数を前記有限状態機械モデルから特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記決定工程によって決定された登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記一の選択要素の次の要素として埋め込む埋込工程と、
をコンピュータに実行させることを特徴とする付記７に記載の検証支援プログラム。
【０１８５】
（付記９）前記検出工程によって、前記一のテストシナリオ以外の他のテストシナリオを構成する一連の要素の中から選ばれた他の選択要素による遷移先状態が、前記有限状態機械モデルの中から検出された場合、前記一のテストシナリオにおいて前記埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象と一致するか否かを判断する登録／復元対象判断工程を前記コンピュータに実行させ、
前記埋込工程は、
前記登録／復元対象判断工程によって一致すると判断された場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記他の選択要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする付記８に記載の検証支援プログラム。
【０１８６】
（付記１０）前記埋込工程によって、特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記埋込工程によって、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、前記対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、当該シミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態と、前記ＦＳＭ出力工程によって出力された有限状態機械モデルにおける前記対象要素による遷移先状態とが、一致するか否かを判断する遷移先状態判断工程と、
前記遷移先状態判断工程によって判断された判断結果を出力する判断結果出力工程と、
を前記コンピュータに実行させることを特徴とする付記９に記載の検証支援プログラム。
【０１８７】
（付記１１）前記判断結果出力工程は、
前記遷移先状態判断工程によって不一致と判断された場合、前記シミュレーションの中止指示情報を、前記シミュレーションを実行する実行手段に出力することを特徴とする付記１０に記載の検証支援プログラム。
【０１８８】
（付記１２）前記遷移先状態判断工程によって一致すると判断された場合、前記シミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態を前記データベースへの登録対象に仮決定する仮決定工程と、
前記仮決定工程によって仮決定された登録対象が、前記データベースに登録済みか否かを判断する登録済判断工程と、
前記登録済判断工程によって登録済みでないと判断された場合、前記登録対象を前記データベースに登録する登録工程と、
前記登録済判断工程によって登録済みであると判断された場合、前記登録対象への遷移元状態を、前記登録対象と一致する登録済みの遷移先状態への遷移元状態に修正し、前記登録対象からの遷移先状態を、前記登録済みの遷移先状態からの遷移先状態に修正する修正工程と、
前記修正工程によって修正された修正後の有限状態機械モデルを出力する修正済ＦＳＭ出力工程と、
を前記コンピュータに実行させることを特徴とする付記１０に記載の検証支援プログラム。
【０１８９】
（付記１３）前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
を前記コンピュータに実行させることを特徴とする付記１０〜１２のいずれか一つに記載の検証支援プログラム。
【０１９０】
（付記１４）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定手段と、
前記遷移数特定手段によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定手段と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定手段によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込手段と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込手段と、
を備えることを特徴とする検証支援装置。
【０１９１】
（付記１５）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出手段と、
前記シナリオ抽出手段によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別手段と、
前記判別手段により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録手段と、
前記判別手段により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元手段と、
を備えることを特徴とする検証支援装置。
【０１９２】
（付記１６）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新手段と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出手段と、
前記抽出手段によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定手段と、
前記遷移先状態列特定手段によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断手段と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断手段によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定手段と、
前記抽出手段による未抽出のテストシナリオがない場合、前記更新手段によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力手段と、
を備えることを特徴とする検証支援装置。
【０１９３】
（付記１７）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
コンピュータが実行することを特徴とする検証支援方法。
【０１９４】
（付記１８）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【０１９５】
（付記１９）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新工程と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出工程と、
前記抽出工程によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定工程と、
前記遷移先状態列特定工程によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断工程と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断工程によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定工程と、
前記抽出工程による未抽出のテストシナリオがない場合、前記更新工程によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【符号の説明】
【０１９６】
１００ 有限状態機械モデル
４００ 検証支援装置
４０１ テストシナリオ短縮化処理部
４０２ シミュレーション実行部
４０３ ＦＳＭ検証処理部
４０４ 登録／復元処理部
４２０ データベース
１５００ 検証支援装置
１５０１ ＦＳＭ生成処理部
１５０２ ＦＳＭ修正処理部
１５０３ 登録／復元処理部
ｔｓ テストシナリオ群
Ｔｓ 短縮化テストシナリオ群
【技術分野】
【０００１】
本発明は、回路の検証を支援する検証支援プログラム、検証支援装置、および検証支援方法に関する。
【背景技術】
【０００２】
従来から回路シミュレーションのシミュレーション時間を短縮化する技術や、状態遷移表に基づいてテストシナリオを生成する技術が開示されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開平９−２９３０９３号公報
【特許文献２】特開２００１−３３１５４４号公報
【特許文献３】特開２００６−１１２８５２号公報
【特許文献４】特開平５−６２７２号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、上述した従来技術では、対象回路の有限状態機械モデルにおいて、どの状態を保存したり復元したりすればよいかが特定できないため、設計者が人手により該当箇所を指定しなければならず、設計者の負担が増大するという問題があった。また、そのような指定は設計者の能力にも依存するため、設計者ごとにばらつきが生じてしまい、シミュレーション時間が適切に短縮できていない場合もあるという問題があった。
【０００５】
また、通常は、同じ対象回路であってもテストシナリオと有限状態機械モデルは設計者によりそれぞれ作成されるため、シミュレーションをおこなう前に時間がかかったり、設計者の負担が増大するという問題があった。
【０００６】
また、作成されたテストシナリオと有限状態機械モデルとに矛盾が生じた場合、シミュレーションをやり直さなければならず、結果的にシミュレーション時間が増大してしまうという問題があった。さらに、有限状態機械モデルに実質的に同一の遷移パスが異なる遷移パスとして存在していると別々にシミュレーションをしなければならず、結果的にシミュレーション時間が増大してしまうという問題があった。
【０００７】
本発明は、上述した従来技術による問題点を解消するため、シミュレーション時間の短縮化を効率的におこなうことができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上述した課題を解決し、目的を達成するため、本検証支援プログラム、検証支援装置、および検証支援方法は、対象回路に関するテストシナリオ群の中から一のテストシナリオを選択し、選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、前記対象回路に関する有限状態機械モデルの中から検出し、検出された遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、前記有限状態機械モデルの中から特定し、特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定し、決定された登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記一の選択要素の次の要素として埋め込むことを要件とする。
【発明の効果】
【０００９】
本検証支援プログラム、検証支援装置、および検証支援方法によれば、シミュレーション時間の短縮化を効率的におこなうことができるという効果を奏する。
【図面の簡単な説明】
【００１０】
【図１】テストシナリオの短縮化の一例を示す説明図である。
【図２】図１に示した短縮化後のテストシナリオでのシミュレーション時間の比較例を示す説明図である。
【図３】検証支援装置のハードウェア構成を示すブロック図である。
【図４】検証支援装置の機能的構成の一例を示すブロック図である。
【図５】テストシナリオ短縮化処理部の機能的構成を示すブロック図である。
【図６】有限状態機械モデルにおけるテストシナリオ群の埋込前後の関係を示す説明図である。
【図７】テストシナリオ短縮化処理部によるテストシナリオ短縮化処理手順を示すフローチャートである。
【図８】ＦＳＭ検証処理部の機能的構成を示すブロック図である。
【図９】ＦＳＭ検証処理部によるＦＳＭ検証処理手順を示すフローチャートである。
【図１０】登録／復元処理部の機能的構成を示すブロック図である。
【図１１】データベースの記憶内容の一例を示す説明図である。
【図１２】登録／復元処理部による登録／復元処理手順を示すフローチャート（その１）である。
【図１３】登録／復元処理部による登録／復元処理手順を示すフローチャート（その２）である。
【図１４】有限状態機械モデルの修正例を示す説明図である。
【図１５】検証支援装置の機能的構成の一例を示すブロック図である。
【図１６】ＦＳＭ生成処理部の機能的構成を示すブロック図である。
【図１７】ＦＳＭ生成処理部によるＦＳＭ生成処理手順を示すフローチャートである。
【図１８】ＦＳＭ修正処理部および登録／復元処理部の機能的構成を示すブロック図である。
【図１９】ＦＳＭ修正処理部によるＦＳＭ修正処理手順を示すフローチャートである。
【図２０】登録／復元処理部による登録／復元処理手順を示すフローチャート（その３）である。
【発明を実施するための形態】
【００１１】
以下に添付図面を参照して、この発明にかかる検証支援プログラム、検証支援装置、および検証支援方法の好適な実施の形態を詳細に説明する。
【００１２】
・実施の形態１
（テストシナリオの短縮化）
まず、本実施の形態１におけるテストシナリオの短縮化について、図１〜図３を用いて説明する。
【００１３】
図１は、テストシナリオの短縮化の一例を示す説明図である。図１において、（Ａ）は、対象回路に関する有限状態機械モデル（ＦＳＭ）１００と短縮化前のテストシナリオｔ１，ｔ２を示している。また、（Ｂ）は、有限状態機械モデル１００と短縮化後のテストシナリオＴ１，Ｔ２を示している。有限状態機械モデル１００において、Ｓ＃（＃は番号）は状態を示しており、矢印は遷移を示している。
【００１４】
また、遷移を示す矢印の始端側の状態を「遷移元状態」と称し、矢印（遷移）の終端側の状態を「遷移先状態」と称す。なお、Ｓ０は初期状態を示す。本実施の形態で用いられる有限状態機械モデル１００は、あくまで一例であり、その内容は対象回路ごとに決められる。
【００１５】
また、回路のシミュレーションを例に挙げると、遷移は、対象回路を構成する組み合わせ回路に与えられる入力パターンであり、状態は、対象回路を構成する組み合わせ回路の出力先となるレジスタに保持される値である。したがって、遷移先状態とは、遷移としてある入力パターンが組み合わせ回路に与えられると、組み合わせ回路から出力されレジスタに保持された出力値である。なお、遷移元状態は、遷移される前のレジスタの値である。なお、シミュレーションを実行していない段階なので、状態を示すレジスタの値は、実際の０／１といった値ではなく変数であらわされる。
【００１６】
テストシナリオｔ１は、有限状態機械モデル１００において、Ｓ０→Ｓ１→Ｓ３→Ｓ６を通る遷移パスであり、ｔ１＝｛ａ，ｂ，ｃ｝である。また、テストシナリオｔ２は、ＦＳＭにおいて、Ｓ０→Ｓ１→Ｓ３→Ｓ８を通る遷移パスであり、ｔ２＝｛ａ，ｂ，ｄ｝である。ここで、要素ａは（Ｓ０→Ｓ１）を示す遷移である。要素ｂは（Ｓ１→Ｓ３）を示す遷移である。要素ｃは（Ｓ３→Ｓ６）を示す遷移である。要素ｄは（Ｓ３→Ｓ８）を示す遷移である。
【００１７】
（Ａ）で示したように、テストシナリオｔ１，ｔ２では、Ｓ０→Ｓ１→Ｓ３を通る遷移｛ａ，ｂ｝が重複している（Ｒｅｄｕｎｄａｎｃｙ）。したがって、本実施の形態では、テストシナリオｔ１を、“ｒｅｃｏｒｄ（Ｓ３）”を埋め込んだテストシナリオＴ１に変換する。また、テストシナリオｔ２を、“ｒｅｓｔｏｒｅ（Ｓ３）”を埋め込んだテストシナリオＴ２に変換する。これにより、状態Ｓ０から状態Ｓ３までのシミュレーションはテストシナリオＴ１のみで実行されるだけとなり、テストシナリオＴ２など他のテストシナリオでは、状態Ｓ０から状態Ｓ３までのシミュレーションを実行する必要なない。そのかわりに、状態Ｓ３を復元する。これにより、テストシナリオｔ２の短縮化を図る。なお、“ｒｅｃｏｒｄ（Ｓ３）”は状態Ｓ３の記録指示を示しており、“ｒｅｓｔｏｒｅ（Ｓ３）”は状態Ｓ３の復元指示を示している。
【００１８】
図２は、図１に示した短縮化後のテストシナリオでのシミュレーション時間の比較例を示す説明図である。図２において、ＳｉｍＴｉｍｅ（）は、（）内で示されるテストシナリオや遷移パスでシミュレーションをしたときのシミュレーション時間である。たとえば、ＳｉｍＴｉｍｅ（ｔ１）は、テストシナリオｔ１で対象回路をシミュレーションしたときのシミュレーション時間である。
【００１９】
（Ａ）は、図１（Ａ）で示した短縮化前でのシミュレーション時間を示している。テストシナリオｔ１のシミュレーション時間ＳｉｍＴｉｍｅ（ｔ１）とテストシナリオｔ２のシミュレーション時間ＳｉｍＴｉｍｅ（ｔ２）を合計したシミュレーション時間では、状態Ｓ０から状態Ｓ３までの遷移パスのシミュレーション時間ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）が重複しているため、２倍の時間がかかっている。
【００２０】
（Ｂ）は、図１（Ｂ）で示した短縮化後のシミュレーション時間を示している。（Ｂ）では、テストシナリオがｔ２からＴ２に短縮化されたため、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）が重複しておらず、１回分短縮化されている。そのかわりに、（Ｂ）では、テストシナリオＴ１での状態Ｓ３の記録時間ＲｅｃＴｉｍｅ（Ｓ３）と、テストシナリオＴ２での状態Ｓ３の復元時間ＲｅｓＴｉｍｅ（Ｓ３）とが追加される。したがって、この場合、以下の式（１）が成立する場合に、シミュレーション時間が短縮化される。
【００２１】
ＳｉｍＴｉｍｅ（Ｓ０→Ｓ３）＞ＲｅｃＴｉｍｅ（Ｓ３）＋ＲｅｓＴｉｍｅ（Ｓ３）
・・・・・・（１）
【００２２】
（検証支援装置のハードウェア構成）
図３は、検証支援装置のハードウェア構成を示すブロック図である。図３において、検証支援装置は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）３０１と、ＲＯＭ（Ｒｅａｄ Ｏｎｌｙ Ｍｅｍｏｒｙ）３０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）３０３と、磁気ディスクドライブ３０４と、磁気ディスク３０５と、光ディスクドライブ３０６と、光ディスク３０７と、ディスプレイ３０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）３０９と、キーボード３１０と、マウス３１１と、スキャナ３１２と、プリンタ３１３と、を備えている。また、各構成部はバス３００によってそれぞれ接続されている。
【００２３】
ここで、ＣＰＵ３０１は、検証支援装置の全体の制御を司る。ＲＯＭ３０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ３０３は、ＣＰＵ３０１のワークエリアとして使用される。磁気ディスクドライブ３０４は、ＣＰＵ３０１の制御にしたがって磁気ディスク３０５に対するデータのリード／ライトを制御する。磁気ディスク３０５は、磁気ディスクドライブ３０４の制御で書き込まれたデータを記憶する。
【００２４】
光ディスクドライブ３０６は、ＣＰＵ３０１の制御にしたがって光ディスク３０７に対するデータのリード／ライトを制御する。光ディスク３０７は、光ディスクドライブ３０６の制御で書き込まれたデータを記憶したり、光ディスク３０７に記憶されたデータをコンピュータに読み取らせたりする。
【００２５】
ディスプレイ３０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ３０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００２６】
インターフェース（以下、「Ｉ／Ｆ」と略する。）３０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク３１４に接続され、このネットワーク３１４を介して他の装置に接続される。そして、Ｉ／Ｆ３０９は、ネットワーク３１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ３０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００２７】
キーボード３１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス３１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００２８】
スキャナ３１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ３１２は、ＯＣＲ（Ｏｐｔｉｃａｌ Ｃｈａｒａｃｔｅｒ Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ３１３は、画像データや文書データを印刷する。プリンタ３１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００２９】
＜検証支援装置の機能的構成＞
図４は、検証支援装置の機能的構成の一例を示すブロック図である。検証支援装置４００は、テストシナリオ短縮化処理部４０１と、シミュレーション実行部４０２と、ＦＳＭ検証処理部４０３と、登録／復元処理部４０４とを備える。テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶されたプログラムをＣＰＵ３０１に実行させることにより、その機能を実現する。
【００３０】
より具体的には、テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４により、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置から読み出されたデータは、ＲＡＭ３０３や磁気ディスク３０５、ＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。また、テストシナリオ短縮化処理部４０１〜登録／復元処理部４０４により、ＣＰＵ３０１が実行した中間的なまたは最終的な実行結果は、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置やＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。
【００３１】
テストシナリオ短縮化処理部４０１は、テストシナリオ群ｔｓを構成するテストシナリオ間で重複する遷移パスを消去して短縮化テストシナリオ群Ｔｓとして出力する。テストシナリオ短縮化処理部４０１の詳細については、図５〜図７を用いて後述する。
【００３２】
シミュレーション実行部４０２は、対象回路のシミュレーションを実行する。具体的には、たとえば、対象回路のハードウェア記述情報（ＤＵＴ）４３０を読み込み、対象回路に短縮化テストシナリオ群Ｔｓを構成するテストシナリオを順次与えることで、テストシナリオごとに対象回路のシミュレーションを実行する。
【００３３】
ＦＳＭ検証処理部４０３は、シミュレーション実行部４０２によるシミュレーションの実行中に有限状態機械モデル１００を検証する。ＦＳＭ検証処理部４０３の詳細については、図８および図９を用いて後述する。
【００３４】
登録／復元処理部４０４は、シミュレーション実行部４０２によるシミュレーションの実行中に、登録／復元対象となった状態をデータベース４２０に登録したり、データベース４２０から読み出して復元する。登録／復元処理部４０４の詳細については、図１０〜図１３を用いて後述する。
【００３５】
＜テストシナリオ短縮化処理部４０１の詳細説明＞
（テストシナリオ短縮化処理部４０１の機能的構成）
図５は、テストシナリオ短縮化処理部４０１の機能的構成を示すブロック図である。テストシナリオ短縮化処理部４０１は、選択部５０１と、検出部５０２と、遷移数特定部５０３と、決定部５０４と、埋込部５０５と、登録／復元対象判断部５０６と、を備えている。
【００３６】
選択部５０１は、対象回路に関するテストシナリオ群の中から一のテストシナリオを選択する。具体的には、たとえば、テストシナリオ群ｔｓを構成するｎ個のテストシナリオｔ１，ｔ２，…，ｔｉ，…，ｔｎから順次選択する。なお、テストシナリオ群ｔｓは、図３に示したＲＯＭ３０２，磁気ディスク３０５などの記憶装置に記憶されている。
【００３７】
また、選択部５０１は、選択テストシナリオを構成する一連の要素（ｓｔｉｍｕｌｕｓ）の中から順次要素（ｓｔｉｍｕｌｉ）を選択する。テストシナリオは、時系列的に対象回路に与える要素の集合である。たとえば、図１に示したテストシナリオｔ１＝｛ａ，ｂ，ｃ｝では、ａ〜ｃは要素（たとえば、入力パターン）である。したがって、テストシナリオｔ１では、“ａ”は（Ｓ０→Ｓ１）を示し、“ｂ”は（Ｓ１→Ｓ３）を示し、“ｃ”は（Ｓ３→Ｓ６）を示す。選択部５０１では、ａ→ｂ→ｃの順に要素を選択する。
【００３８】
検出部５０２は、選択部５０１によって選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、対象回路に関する有限状態機械モデル１００の中から検出する。上述したテストシナリオｔ１を例に挙げると、要素ａを選択要素とした場合、要素ａは状態遷移（Ｓ０→Ｓ１）であるため、要素ａが対象回路に与えられると、対象回路の状態が状態Ｓ０から状態Ｓ１に遷移する。したがって、検出部５０２は、要素ａによる遷移先状態Ｓ１を検出する。すなわち、選択要素が状態遷移（Ｓｊ→Ｓｋ）の場合、検出部５０２は、状態Ｓｋを遷移先状態として検出することになる。なお、状態Ｓｊは遷移元状態である。
【００３９】
遷移数特定部５０３は、検出部５０２によって検出された遷移先状態への入力遷移数と遷移先状態からの出力遷移数を、有限状態機械モデル１００の中から特定する。ここで、入力遷移数とは、検出遷移先状態を遷移先状態として指定する状態遷移の個数である。また、出力遷移数とは、検出遷移先状態を遷移元状態とした場合の検出遷移先状態からの状態遷移の個数である。
【００４０】
たとえば、図１の有限状態機械モデル１００において検出遷移先状態を状態Ｓ３とする。状態Ｓ３は、状態Ｓ１からの遷移先状態であり、それ以外の状態から状態遷移されない。したがって、状態Ｓ３の入力遷移数は、１である。また、状態Ｓ３は、状態Ｓ６，Ｓ７，Ｓ８という３つの状態に遷移する。したがって、状態Ｓ３の出力遷移数は、３である。
【００４１】
決定部５０４は、遷移数特定部５０３によって特定された出力遷移数が入力遷移数よりも多い場合、遷移先状態を登録／復元対象に決定する。ここで、登録／復元対象とは、データベース４２０に登録され、かつ、データベース４２０から読み出されて復元される状態（レジスタに保持される値）である。上述した例では、状態Ｓ３が検出遷移先状態であるが、状態Ｓ３の出力遷移数（３個）は、状態Ｓ３の入力遷移数（１個）よりも多いため、状態Ｓ３は、図１の（Ｂ）に示したように登録／復元対象となる。
【００４２】
埋込部５０５は、決定部５０４によって決定された登録／復元対象をデータベース４２０に登録させる登録指示情報を、一のテストシナリオ内の一の選択要素の次の要素として埋め込む。ここで、登録指示情報とは、登録／復元対象となる状態を、データベース４２０にその状態を登録させる情報である。本実施の形態では、登録／復元対象を状態Ｓｉとすると、“ｒｅｃｏｒｄ（Ｓｉ）”を登録指示情報とする。埋込部５０５は、対象となっているテストシナリオ内において、登録指示情報を、その登録／復元対象に状態遷移させる要素の次の要素に埋め込む。
【００４３】
図６は、有限状態機械モデルにおけるテストシナリオ群の埋込前後の関係を示す説明図である。図６において、（Ａ）は、埋込前のテストシナリオ群ｔｓを示しており、（Ｂ）は、埋込後の短縮化テストシナリオ群Ｔｓを示している。（Ｃ）は、埋込前のテストシナリオ群ｔｓでのシミュレーションの実行内容を示しており、（Ｄ）は、埋込後の短縮化テストシナリオ群Ｔｓでのシミュレーションの実行内容を示している。
【００４４】
（Ｃ）において、テストシナリオｔ１の状態Ｓ３では、出力遷移数が３、入力遷移数が１となる。したがって、埋込部５０５により、テストシナリオｔ１の要素ｂの次の要素として、要素ｃの前に、“ｒｅｃｏｒｄ（Ｓ３）”を要素として埋め込む。これにより、テストシナリオｔ１が、（Ｄ）に示したようにテストシナリオＴ１に変換される。
【００４５】
また、図５において、埋込部５０５は、登録／復元対象をデータベース４２０から復元させる復元指示情報を、他のテストシナリオを構成する一連の要素の先頭要素から他の選択要素までの要素群に代えて、他のテストシナリオに埋め込む。ここで、復元指示情報とは、登録／復元対象となる状態を、データベース４２０からその状態を復元させる情報である。
【００４６】
本実施の形態では、登録／復元対象を状態Ｓｉとすると、“ｒｅｓｔｏｒｅ（Ｓｉ）”を復元指示情報とする。埋込部５０５は、対象となっているテストシナリオ内において、その登録／復元対象までの要素列を削除して、その要素列の代わりに復元指示情報を埋め込む。
【００４７】
（Ａ）において、テストシナリオｔ１，ｔ２では要素列｛ａ，ｂ｝が重複しているため、要素ｂの遷移先状態Ｓ３が、テストシナリオＴ１において、登録指示情報により指定されている。したがって、埋込部５０５により、テストシナリオｔ２の初期の要素ａから要素ｂまでの要素列｛ａ，ｂ｝を消去して、要素列｛ａ，ｂ｝の位置に“ｒｅｓｔｏｒｅ（Ｓ３）”を要素として埋め込む。これにより、テストシナリオｔ２がテストシナリオＴ２に変換される。
【００４８】
また、図５において、登録／復元対象判断部５０６は、検出部５０２によって、一のテストシナリオ以外の他のテストシナリオを構成する一連の要素の中から選ばれた他の選択要素による遷移先状態が、有限状態機械モデルの中から検出された場合、一のテストシナリオにおいて埋込部５０５によって埋め込まれた登録指示情報が指定する登録／復元対象と一致するか否かを判断する。
【００４９】
具体的には、たとえば、図６において、テストシナリオｔ１がテストシナリオＴ１に変換された後、未変換のテストシナリオｔ２が選択された場合、テストシナリオｔ２の先頭要素ａから順次遷移先状態を探索する。そして、探索された状態が、登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”が指定する登録／復元対象（状態Ｓ３）と一致するか否かを判断する。
【００５０】
テストシナリオｔ２では、要素ｂの遷移先状態Ｓ３で登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”が指定する登録／復元対象（状態Ｓ３）と一致する。したがって、図６の（Ｂ）に示したように、テストシナリオｔ２の要素列｛ａ，ｂ｝を消去して、要素列｛ａ，ｂ｝の位置に“ｒｅｓｔｏｒｅ（Ｓ３）”を要素として埋め込む。
【００５１】
したがって、図６の（Ｃ）に示したように、従来だと、テストシナリオｔ１で対象回路のシミュレーションを実行したときに、ａ→ｂ→ｃの順で状態遷移し、その後、テストシナリオｔ２で対象回路のシミュレーションを実行したときに、ａ→ｂ→ｄの順で状態遷移した。
【００５２】
これに対し、本実施の形態では、図６の（Ｄ）に示したように、テストシナリオＴ１で対象回路のシミュレーションを実行したときに、ａ→ｂの順で状態遷移したあと、登録指示情報“ｒｅｃｏｒｄ（Ｓ３）”により、要素ｂの遷移先状態Ｓ３（でのレジスタの値）をデータベース４２０に記録する。そして、ｃにより状態遷移させる。
【００５３】
つぎに、テストシナリオＴ２で対象回路のシミュレーションを実行したときに、テストシナリオｔ２のように、ａ→ｂの順で状態遷移させずに、復元指示情報“ｒｅｓｔｏｒｅ（Ｓ３）”によりデータベース４２０から状態Ｓ３（のレジスタの値）を復元する。その後、要素ｄにより状態遷移させる。これにより、シミュレーション時間が大幅に短縮されることになる。
【００５４】
（テストシナリオ短縮化処理部４０１によるテストシナリオ短縮化処理）
図７は、テストシナリオ短縮化処理部４０１によるテストシナリオ短縮化処理手順を示すフローチャートである。まず、テストシナリオ短縮化処理部４０１は、対象回路に関する有限状態機械モデル１００と対象回路に関するテストシナリオ群ｔｓを取得する（ステップＳ７０１）。具体的には、テストシナリオ短縮化処理部４０１は、有限状態機械モデル１００と対象回路に関するテストシナリオ群ｔｓを検証支援装置４００に読み込ませる。
【００５５】
つぎに、テストシナリオ短縮化処理部４０１は、未選択のテストシナリオがあるか否かを判断する（ステップＳ７０２）。未選択のテストシナリオがない場合（ステップＳ７０２：Ｎｏ）、テストシナリオ短縮化処理を終了する。一方、未選択のテストシナリオがある場合（ステップＳ７０２：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、未選択のテストシナリオを選択する（ステップＳ７０３）。そして、テストシナリオ短縮化処理部４０１は、選択テストシナリオの中で、未選択の要素があるか否かを判断する（ステップＳ７０４）。
【００５６】
未選択の要素がない場合（ステップＳ７０４：Ｎｏ）、テストシナリオ短縮化処理部４０１は、次のテストシナリオを選択させるため、ステップＳ７０２に戻る。一方、未選択の要素がある場合（ステップＳ７０４：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、未選択の要素のうち先頭の要素を選択する（ステップＳ７０５）。
【００５７】
つぎに、テストシナリオ短縮化処理部４０１は、選択要素による遷移先状態の入力遷移数と出力遷移数とを検出する（ステップＳ７０６）。そして、テストシナリオ短縮化処理部４０１は、出力遷移数＞入力遷移数であるか否かを判断する（ステップＳ７０７）。出力遷移数＞入力遷移数でない場合（ステップＳ７０７：Ｎｏ）、登録／復元の対象外であるため、ステップＳ７０４に戻る。一方、出力遷移数＞入力遷移数である場合（ステップＳ７０７：Ｙｅｓ）、テストシナリオ短縮化処理部４０１は、遷移先状態が登録／復元対象に設定済みであるか否かを判断する（ステップＳ７０８）。
【００５８】
たとえば、テストシナリオ短縮化処理部４０１は、選択済みのテストシナリオ内の登録指示情報により、遷移先状態が指定されているか否かにより判断する。指定されていなければ、設定済みでないことになり、指定されていれば、設定済みとなる。たとえば、選択済みのテストシナリオ内にすでに、“ｒｅｃｏｒｄ（Ｓ３）”が埋め込まれている場合に、遷移先状態Ｓ３は、登録／復元対象に設定済みとなる。
【００５９】
そして、設定済みでない場合（ステップＳ７０８：Ｎｏ）、テストシナリオ短縮化処理部４０１は、遷移先状態を登録／復元対象として指定してデータベース４２０に登録させる登録指示情報を生成する（ステップＳ７０９）。そして、テストシナリオ短縮化処理部４０１は、生成された登録指示情報を選択要素の次の要素との間に追加して（ステップＳ７１０）、ステップＳ７０４に戻る。
【００６０】
一方、ステップＳ７０８において、登録／復元対象に設定済みである場合（ステップＳ７０８：Ｙｅｓ）、すでに、遷移先状態を指定する登録指示情報が存在する。したがって、テストシナリオ短縮化処理部４０１は、遷移先状態をデータベース４２０から復元させる復元指示情報を生成する（ステップＳ７１１）。そして、テストシナリオ短縮化処理部４０１は、遷移先状態までの遷移列を消去して、その位置に生成された復元指示情報を追加する（ステップＳ７１２）。このあと、ステップＳ７０４に戻る。
【００６１】
このようなテストシナリオ短縮化処理により、テストシナリオ群ｔｓ（ｔ１，ｔ２，…）が短縮化テストシナリオ群Ｔｓ（Ｔ１，Ｔ２，…）に短縮化されることとなる。
【００６２】
＜ＦＳＭ検証処理部４０３の詳細説明＞
（ＦＳＭ検証処理部４０３の機能的構成）
つぎに、図４に示したＦＳＭ検証処理部４０３について具体的に説明する。ＦＳＭ検証処理部４０３は、対象回路に関する有限状態機械モデル１００での状態遷移と実際にシミュレーションを実行したときの状態遷移との同一性を検証する。具体的には、ＦＳＭ検証処理部４０３は、対象回路のハードウェア記述情報４３０に短縮化テストシナリオ群Ｔｓ内のテストシナリオを順次与えることでシミュレーションを実行したときの状態遷移が、対象回路に関する有限状態機械モデル１００の状態遷移と一致するか否かを検証する。
【００６３】
図８は、ＦＳＭ検証処理部４０３の機能的構成を示すブロック図である。ＦＳＭ検証処理部４０３は、遷移先状態判断部８０１と、判断結果出力部８０２とを備えている。
【００６４】
遷移先状態判断部８０１は、対象回路のシミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態と、対象回路に関する有限状態機械モデル１００における対象要素による遷移先状態とが、一致するか否かを判断する。
【００６５】
具体的には、たとえば、テストシナリオＴ１を与えてシミュレーションを実行している場合、有限状態機械モデル１００では、現状態である状態Ｓ０の遷移先状態はＳ１であるのに対し、シミュレーションでの現状態である状態Ｓ０の次状態が状態Ｓ１であれば、一致すると判断する。一方、次状態が状態Ｓ１以外、たとえば、状態Ｓ２であれば、不一致と判断する。
【００６６】
判断結果出力部８０２は、遷移先状態判断部８０１によって判断された判断結果を出力する。判断結果とは、遷移先状態判断部８０１によってすべて一致した場合には、合格としてレポートを出力する。一方、遷移先状態判断部８０１によって不一致が発生した場合、シミュレーションの中止指示情報をシミュレーション実行部４０２に出力する。シミュレーション実行部４０２は、中止指示情報を受け付けると、シミュレーションを中止する。
【００６７】
この場合は、短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との間に不整合が生じているため、設計者は、短縮化テストシナリオ群Ｔｓ（またはテストシナリオ群ｔｓ）と有限状態機械モデル１００の修正を、コンピュータを操作して手作業によりおこなう。そして、修正後に再度、ＦＳＭ検証処理部４０３により検証処理をおこなう。
【００６８】
（ＦＳＭ検証処理部４０３によるＦＳＭ検証処理）
図９は、ＦＳＭ検証処理部４０３によるＦＳＭ検証処理手順を示すフローチャートである。まず、ＦＳＭ検証処理部４０３は、シミュレーションの開始を待ち受け（ステップＳ９０１：Ｎｏ）、シミュレーションが開始された場合（ステップＳ９０１：Ｙｅｓ）、シミュレーションの終了を待ち受ける（ステップＳ９０２）。シミュレーションは、問題なく最後まで実行されて終了する場合と、ＦＳＭ検証処理部４０３からシミュレーション実行部４０２に中止指示情報が出力された結果、シミュレーションが終了する場合がある。
【００６９】
シミュレーションが終了していない場合（ステップＳ９０２：Ｎｏ）、ＦＳＭ検証処理部４０３は、シミュレーションでの選択テストシナリオおよびその選択要素をシミュレーション実行部４０２からの情報により検出する（ステップＳ９０３）。そして、ＦＳＭ検証処理部４０３は、シミュレーション実行部４０２からの情報により状態遷移が発生したか否かを判断する（ステップＳ９０４）。状態遷移が発生していない場合（ステップＳ９０４：Ｎｏ）、ステップＳ９０２に戻る。
【００７０】
一方、状態遷移が発生した場合（ステップＳ９０４：Ｙｅｓ）、ＦＳＭ検証処理部４０３は、次状態と有限状態機械モデル１００での遷移先状態が一致するか否かを判断する（ステップＳ９０５）。一致する場合（ステップＳ９０５：Ｙｅｓ）、ステップＳ９０２に戻る。一方、不一致である場合（ステップＳ９０５：Ｎｏ）、中止指示情報をシミュレーション実行部４０２に出力して（ステップＳ９０６）、ステップＳ９０２に戻る。
【００７１】
また、ステップＳ９０２においてシミュレーションの終了が検出された場合（ステップＳ９０２：Ｙｅｓ）、ＦＳＭ検証処理部４０３は、検証結果（合格または不合格）のレポートを出力する（ステップＳ９０７）。中止指示情報が一度も出力されていない場合は合格を示すレポートを出力する。一方、中止指示情報が出力された場合は、不合格を示すレポートを出力する。
【００７２】
このようなＦＳＭ検証処理により、それぞれ独立して作成された短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との不整合を自動で検出することができる。また、不整合がない場合（不一致がない場合）は、短縮化テストシナリオ群Ｔｓと有限状態機械モデル１００との間で整合性がとれていることを保証することができる。
【００７３】
＜登録／復元処理部４０４の詳細説明＞
（登録／復元処理部４０４の機能的構成）
つぎに、図４に示した登録／復元処理部４０４について具体的に説明する。登録／復元処理部４０４は、シミュレーションの実行中に、登録／復元対象となる遷移先状態を特定して、遷移先状態（となるレジスタの値）をデータベース４２０に登録したり、登録された遷移先状態（となるレジスタの値）をデータベース４２０から読み出して復元する。
【００７４】
図１０は、登録／復元処理部４０４の機能的構成を示すブロック図である。登録／復元処理部４０４は、シナリオ抽出部１００１と、判別部１００２と、登録部１００４と、判定部１００３と、復元部１００５と、を備えている。
【００７５】
シナリオ抽出部１００１は、特定の遷移先状態をデータベース４２０に登録させる登録指示情報が埋め込まれたテストシナリオと、特定の遷移先状態をデータベース４２０から復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出する。
【００７６】
具体的には、たとえば、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを順次抽出する。
【００７７】
判別部１００２は、シナリオ抽出部１００１によって抽出された対象テストシナリオを構成する一連の要素の中から対象回路に対象要素を順次与えて模擬する対象回路のシミュレーションの実行中に、対象要素の種類を判別する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓを構成するテストシナリオには、登録指示情報が埋め込まれているテストシナリオＴ１や復元指示情報が埋め込まれているテストシナリオＴ２が存在する。
【００７８】
判別部１００２は、対象テストシナリオの中から対象回路に与えられた対象要素の種別が、（Ｓｊ→Ｓｋ）といった遷移をあらわす要素であるか、登録指示情報ｒｅｃｏｒｄ（Ｓｋ）であるか、復元指示情報ｒｅｓｔｏｒｅ（Ｓｋ）であるかを判別する。
【００７９】
登録部１００４は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態をデータベース４２０に登録する。具体的には、たとえば、登録指示情報が“ｒｅｃｏｒｄ（Ｓｋ）”である場合、状態Ｓｋ、すなわち、対象回路内の組み合わせ回路の出力先となるレジスタの値を、状態Ｓｋの識別子と関連付けてデータベース４２０に登録する。
【００８０】
図１１は、データベース４２０の記憶内容の一例を示す説明図である。データベース４２０は、状態名項目とコンテキスト情報項目とを有し、状態ごとにコンテキスト情報が登録される。ここで、コンテキスト情報とは、対象回路内のレジスタを識別する識別子（たとえば、レジスタ名）とレジスタの値である。図１１では、状態Ｓ３のレジスタｒ１〜ｒｍの値が登録されている。
【００８１】
図１０に戻って、判定部１００３は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態までのシミュレーション時間とデータベース４２０からの所定の復元時間とに基づいて、登録部１００４により登録すべきか否かを判定する。
【００８２】
ここで、特定の遷移先状態までのシミュレーション時間については、シミュレーション実行部４０２により計測されるものとする。たとえば、状態Ｓ０〜Ｓｋまでのシミュレーション時間を、ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）とする。また、データベース４２０への登録時間をＲｅｃとし、データベース４２０からの復元時間をＲｅｓとする。登録時間Ｒｅｃと復元時間Ｒｅｓはあらかじめ設定される。
【００８３】
ここで、特定の遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）を求める。遷移数差分Ｎ（Ｓｋ）は、下記式で表現される。
【００８４】
Ｎ（Ｓｋ）＝Ｎｏｕｔ（Ｓｋ）−Ｎｉｎ（Ｓｋ）・・・・・・・・・・・・・・・（２）
ただし、Ｎｏｕｔ（Ｓｋ）は遷移先状態Ｓｋの出力遷移数、Ｎｉｎ（Ｓｋ）は遷移先状態Ｓｋの入力遷移数である。
【００８５】
そして、下記式（３）を満たすことにより、遷移先状態Ｓｋをデータベース４２０に登録すべきであるか否かを判断する。
【００８６】
Ｎ（Ｓｋ）×ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）＞Ｒｅｃ＋Ｎ（Ｓｋ）×Ｒｅｓ・・・（３）
ただし、Ｎ（Ｓｋ）＞０
【００８７】
シミュレーションは通常複数回実行されるため、１回目のシミュレーションでシミュレーション時間が最短となる状態Ｓｋを特定し、２回目以降は、最短となる状態ＳｋのＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）を適用する。たとえば、テストシナリオｔ１〜ｔ３が同一の状態Ｓ１０を通過する場合、テストシナリオｔ１〜ｔ３ごとに、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）を計測する。
【００８８】
そして、２回目以降のシミュレーションでは、ＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）が最短となるテストシナリオ（たとえば、テストシナリオｔ２）のＳｉｍＴｉｍｅ（Ｓ０→Ｓ１０）を採用する。この場合、上記式（３）は、下記式（４）となる。
【００８９】
Ｎ（Ｓｋ）×Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］＞Ｒｅｃ＋Ｎ（Ｓｋ）×Ｒｅｓ
・・・（４）
ただし、Ｎ（Ｓｋ）＞０
【００９０】
なお、Ｎ（Ｓｋ）が大きければ大きいほど、右辺の第２項Ｎ（Ｓｋ）×Ｒｅｓが大きくなるので、右辺第１項の記録時間Ｒｅｃは無視できる。したがって、Ｎ（Ｓｋ）があらかじめ設定したしきい値以上となった場合、上記（４）式は下記（５）式になる。
【００９１】
Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］＞Ｒｅｓ・・・（５）
【００９２】
したがって、判定部１００３は、式（５）が成立したときは、そのときの遷移先状態をデータベース４２０に登録すべきと判定し、成立しなかったときは登録すべきでないと判定する。
【００９３】
復元部１００５は、判別部１００２により対象要素が復元指示情報であると判別された場合、特定の遷移先状態をデータベース４２０から復元する。ここで、復元とは、特定の遷移先状態（のレジスタの値）をデータベース４２０から読み出して、対象回路内のレジスタに書き込む処理である。本実施の形態は、シミュレーションであるため、モデル化された対象回路のレジスタに、データベース４２０から読み出したレジスタの値を設定することとなる。
【００９４】
具体的には、たとえば、図６の（Ｄ）においてテストシナリオＴ２を与えてシミュレーションした場合に、状態Ｓ３までのシミュレーションを実行しなくても状態Ｓ３が復元される。このように、特定の遷移先状態を復元することで、特定の遷移先状態までシミュレーションする必要がなく、シミュレーション時間の短縮化を図ることができる。
【００９５】
たとえば、特定の遷移先状態Ｓｋまでの最短シミュレーション時間Ｍｉｎ［ＳｉｍＴｉｍｅ（Ｓ０→Ｓｋ）］が復元時間Ｒｅｓよりも大きい場合に、その差が、たとえば、１［ｍｓｅｃ］あったとする。そして、遷移数差分Ｎ（Ｓｋ）がＮ（Ｓｋ）＝１０００であったとすると、短縮後では、特定の遷移先状態Ｓｋを通るテストシナリオ群について、１０００×１［ｍｓｅｃ］＝１［ｓｅｃ］もシミュレーション時間を短縮することができる。
【００９６】
（登録／復元処理部４０４による登録／復元処理）
図１２は、登録／復元処理部４０４による登録／復元処理手順を示すフローチャート（その１）である。まず、登録／復元処理部４０４は、シミュレーションの開始を待ち受け（ステップＳ１２０１：Ｎｏ）、シミュレーションが開始された場合（ステップＳ１２０１：Ｙｅｓ）、シミュレーションの終了を待ち受ける（ステップＳ１２０２）。シミュレーションは、問題なく最後まで実行されて終了する場合と、ＦＳＭ検証処理部４０３からシミュレーション実行部４０２に中止指示情報が出力された結果、シミュレーションが終了する場合がある。シミュレーションが終了した場合（ステップＳ１２０２：Ｙｅｓ）、登録／復元処理は終了する。
【００９７】
一方、シミュレーションが終了していない場合（ステップＳ１２０２：Ｎｏ）、登録／復元処理部４０４は、短縮化テストシナリオ群Ｔｓの中から未選択のテストシナリオがあるか否かを判断する（ステップＳ１２０３）。未選択のテストシナリオがない場合（ステップＳ１２０３：Ｎｏ）、登録／復元処理は終了する。
【００９８】
一方、未選択のテストシナリオがある場合（ステップＳ１２０３：Ｙｅｓ）、登録／復元処理部４０４は、未選択のテストシナリオを選択する（ステップＳ１２０４）。そして、登録／復元処理部４０４は、選択テストシナリオ内に未選択の要素があるか否かを判断する（ステップＳ１２０５）。未選択の要素がない場合（ステップＳ１２０５：Ｎｏ）、選択テストシナリオ内の要素はすべてシミュレーションされたため、ステップＳ１２０３に戻る。
【００９９】
一方、未選択の要素がある場合（ステップＳ１２０５：Ｙｅｓ）、登録／復元処理部４０４は、未選択の要素を先頭から抽出する（ステップＳ１２０６）。そして、登録／復元処理部４０４は、抽出要素が復元指示情報であるか否かを判断する（ステップＳ１２０７）。復元指示情報である場合（ステップＳ１２０７：Ｙｅｓ）、登録／復元処理部４０４は、復元指示情報で指定されている状態のコンテキスト情報をデータベース４２０から読み出して復元する（ステップＳ１２０８）。そして、ステップＳ１２０５に戻る。
【０１００】
一方、ステップＳ１２０７において、復元指示情報でない場合（ステップＳ１２０７：Ｎｏ）、図１３のステップＳ１３０１に移行する。
【０１０１】
図１３は、登録／復元処理部４０４による登録／復元処理手順を示すフローチャート（その２）である。まず、登録／復元処理部４０４は、ステップＳ１２０６において抽出された抽出要素を対象回路のハードウェア記述情報４３０に与える（ステップＳ１３０１）。これにより、シミュレーション実行部４０２では、対象回路のシミュレーションが実行される。そして、状態遷移の発生を待ち受ける（ステップＳ１３０２）。
【０１０２】
状態遷移が発生しなかった場合（ステップＳ１３０２：Ｎｏ）、末尾の状態に到達したこととなり、シミュレーション実行部４０２からその旨の通知を受けることになる。この場合は、ステップＳ１２０５に戻る。この場合、ステップＳ１２０５に戻っても未選択要素がないため、ステップＳ１２０３に戻ることになる。なお、現状態から次状態への状態遷移については、状態遷移が発生したものとする。
【０１０３】
一方、ステップＳ１３０２において、状態遷移が発生した場合（ステップＳ１３０２：Ｙｅｓ）、登録／復元処理部４０４は、発生した状態遷移による遷移先状態Ｓｋが登録／復元対象であるか否かを判断する（ステップＳ１３０３）。具体的には、遷移先状態Ｓｋが、すでに他のテストシナリオにおいて登録指示情報で指定されているか否かを判断する。
【０１０４】
遷移先状態が登録／復元対象でない場合（ステップＳ１３０３：Ｎｏ）、ステップＳ１２０５に戻る。一方、遷移先状態が登録／復元対象である場合（ステップＳ１３０３：Ｙｅｓ）、登録／復元処理部４０４は、初期状態Ｓ０から遷移先状態Ｓｋまでのシミュレーション時間をシミュレーション実行部４０２から取得する（ステップＳ１３０４）。そして、登録／復元処理部４０４は、遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）に復元時間Ｒｅｓを乗じた値（Ｎ（Ｓｋ）×Ｒｅｓ）が所定のしきい値Ｔに記録時間Ｒｅｃを乗じた値（Ｔ×Ｒｅｃ）以上であるか否かを判断する（ステップＳ１３０５）。
【０１０５】
Ｎ（Ｓｋ）×Ｒｅｓ≧Ｔ×Ｒｅｃである場合（ステップＳ１３０５：Ｙｅｓ）、登録／復元処理部４０４は、式（５）を満たすか否かを判断する（ステップＳ１３０６）。式（５）を満たさない場合（ステップＳ１３０６：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（５）を満たす場合（ステップＳ１３０６：Ｙｅｓ）、登録／復元処理部４０４は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ１３０７）、ステップＳ１２０５に戻る。
【０１０６】
一方、ステップＳ１３０５において、Ｎ（Ｓｋ）≧Ｔでない場合（ステップＳ１３０５：Ｎｏ）、登録／復元処理部４０４は、式（４）を満たすか否かを判断する（ステップＳ１３０８）。式（４）を満たさない場合（ステップＳ１３０８：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（４）を満たす場合（ステップＳ１３０８：Ｙｅｓ）、登録／復元処理部４０４は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ１３０９）、ステップＳ１２０５に戻る。
【０１０７】
このような登録／復元処理によれば、どの状態を復元すればよいかが自動設定されているため、設計者が試行錯誤して登録／復元対象を探す必要はない。したがって、対象回路のシミュレーションを効率的に短縮化することができる。
【０１０８】
・実施の形態２
つぎに、実施の形態２について説明する。上述した実施の形態１では、設計者が対象回路について、テストシナリオ群ｔｓと有限状態機械モデル１００の両方を作成した例について説明したが、テストシナリオ群ｔｓと有限状態機械モデル１００との不整合をあらかじめ回避するため、実施の形態２では、テストシナリオ群ｔｓから有限状態機械モデル１００を自動生成する。
【０１０９】
また、自動生成した場合に、同一状態が別々の状態として生成されることがあるため、実施の形態２では、本来同一の状態であるが別々に生成された状態どうしを統合して、有限状態機械モデル１００を自動修正する。これにより、修正後の有限状態機械モデル（以下、「修正済ＦＳＭ」）１４００は、修正前に比べて冗長さが低減される。
【０１１０】
また、統合により、統合された状態は、登録／復元対象になる可能性がある。したがって、データベース４２０からコンテキスト情報を復元することが可能となるため、シミュレーション時間の短縮化も図ることができる。以下、実施の形態２について説明するが、実施の形態１と同一箇所には同一符号を付し、その説明を省略する。
【０１１１】
＜ＦＳＭ修正＞
図１４は、有限状態機械モデル１００の修正例を示す説明図である。図１４において、（Ａ）は修正前の有限状態機械モデル１００を示しており、（Ｂ）は修正済ＦＳＭ１４００を示している。
【０１１２】
なお、（Ａ）の状態での短縮化テストシナリオ群Ｔｓは以下のとおりである。
Ｔ１＝｛ａ，ｂ，ｃ，ｒｅｃｏｒｄ（Ｓ８），ｅ｝
Ｔ２＝｛ｆ，ｇ，ｈ，ｊ｝
Ｔ３＝｛ｒｅｓｔｏｒｅ（Ｓ８），ｄ｝
【０１１３】
また、修正済ＦＳＭ１４００により、短縮化テストシナリオ群Ｔｓを修正すると、以下のとおりである。
Ｔ１＝｛ａ，ｂ，ｃ，ｒｅｃｏｒｄ（Ｓ８），ｅ｝
Ｔ２＝｛ｆ，ｇ，ｐ，ｑ｝
Ｔ３＝｛ｒｅｓｔｏｒｅ（Ｓ８），ｄ｝
【０１１４】
すなわち、状態Ｓ９が状態Ｓ８に統合されたため、テストシナリオＴ２の要素ｈ（Ｓ４→Ｓ９）は、要素ｐ（Ｓ４→Ｓ８）に修正される。同様に、テストシナリオＴ２の要素ｊ（Ｓ９→Ｓ１２）は、要素ｑ（Ｓ８→Ｓ１２）に修正される。このように、テストシナリオを修正することで、再度テストシナリオの短縮化をおこなうことができる。たとえば、テストシナリオＴ２は、データベース４２０に登録された状態Ｓ８を復元することで短縮化することが可能となる。
【０１１５】
＜検証支援装置の機能的構成＞
図１５は、検証支援装置の機能的構成の一例を示すブロック図である。検証支援装置１５００は、ＦＳＭ生成処理部１５０１と、テストシナリオ短縮化処理部４０１と、シミュレーション実行部４０２と、ＦＳＭ修正処理部１５０２と、登録／復元処理部１５０３とを備える。テストシナリオ短縮化処理部４０１およびシミュレーション実行部４０２は、実施の形態１と同一内容であるため説明を省略する。
【０１１６】
また、ＦＳＭ生成処理部１５０１〜登録／復元処理部１５０３は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶されたプログラムをＣＰＵ３０１に実行させることにより、その機能を実現する。
【０１１７】
より具体的には、ＦＳＭ生成処理部１５０１〜登録／復元処理部１５０３により、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置から読み出されたデータは、ＲＡＭ３０３や磁気ディスク３０５、ＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。また、ＦＳＭ生成処理部１５０１〜ＦＳＭ修正処理部１５０２により、ＣＰＵ３０１が実行した中間的なまたは最終的な実行結果は、ＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置やＣＰＵ３０１内のキャッシュやレジスタに書き込まれる。
【０１１８】
ＦＳＭ生成処理部１５０１は、対象回路に関するテストシナリオ群ｔｓから対象回路に関する有限状態機械モデル１００を自動生成する。ＦＳＭ生成処理部１５０１の詳細については、図１６および図１７を用いて後述する。
【０１１９】
ＦＳＭ修正処理部１５０２は、シミュレーション実行部４０２によるシミュレーションの実行中に、ＦＳＭ生成処理部１５０１によって生成された有限状態機械モデル１００を、図１４に示したように修正する。登録対象となった状態をデータベース４２０に登録する機能も有する。ＦＳＭ修正処理部１５０２の詳細については、図１８および図１９を用いて後述する。
【０１２０】
登録／復元処理部１５０３は、シミュレーションの実行中に、登録／復元対象となる遷移先状態を特定して、遷移先状態（となるレジスタの値）をデータベース４２０に登録したり、登録された遷移先状態（となるレジスタの値）をデータベース４２０から読み出して復元する。
【０１２１】
＜ＦＳＭ生成処理部１５０１の詳細説明＞
（ＦＳＭ生成処理部１５０１の機能的構成）
図１６は、ＦＳＭ生成処理部１５０１の機能的構成を示すブロック図である。ＦＳＭ生成処理部１５０１は、更新部１６０５と、シナリオ抽出部１６０１と、遷移先状態特定部１６０２と、中間ＦＳＭ判断部１６０３と、設定部１６０４と、ＦＳＭ出力部１６０６とを備えている。
【０１２２】
更新部１６０５は、対象回路に関する有限状態機械モデル１００に対象状態列が追加されることにより、有限状態機械モデル１００を更新する。更新対象となる有限状態機械モデル１００を、中間ＦＳＭ１６００と称す。まだ１回も更新されていない中間ＦＳＭ１６００は、対象回路の初期状態Ｓ０のみである。
【０１２３】
そして、中間ＦＳＭ１６００に対象状態列が追加されることで、中間ＦＳＭ１６００が更新される。対象状態列とは、更新前の中間ＦＳＭ１６００には含まれていない状態列である。なお、対象状態列は、設定部１６０４により設定される。
【０１２４】
シナリオ抽出部１６０１は、対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する。具体的には、たとえば、テストシナリオ群ｔｓから順次テストシナリオを抽出する。
【０１２５】
遷移先状態特定部１６０２は、抽出部によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する。具体的には、たとえば、抽出テストシナリオの各要素による遷移先状態（レジスタの値。ただし、シミュレーションはまだ実行していないため、実際の０／１といった値ではなく変数でよい。）を検出することとなる。
【０１２６】
たとえば、選択テストシナリオｔ１がｔ１＝｛ａ，ｂ，ｃ，ｅ｝（ただし、ａ＝（Ｓ０→Ｓ１）、ｂ＝（Ｓ１→Ｓ３）、ｃ＝（Ｓ３→Ｓ８）、ｅ＝（Ｓ８→Ｓ１０））とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を特定する。
【０１２７】
中間ＦＳＭ判断部１６０３は、遷移先状態特定部１６０２によって特定された遷移先状態列が、有限状態機械モデル１００に含まれているか否かを判断する。具体的には、最新の中間ＦＳＭ１６００に、遷移先状態特定部１６０２によって特定された遷移先状態列が含まれているか否かを判断する。たとえば、上述の例において、最新の中間ＦＳＭ１６００が｛Ｓ０→Ｓ１｝とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝のうち、｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に含まれていないと判断する。
【０１２８】
これに対し、最新の中間ＦＳＭ１６００が｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０→Ｓ１５｝であるとすると、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０→Ｓ１５｝に、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が含まれていると判断される。
【０１２９】
設定部１６０４は、遷移先状態特定部１６０２によって特定された遷移先状態列のうち、中間ＦＳＭ判断部１６０３によって含まれていないと判断された遷移先状態列を対象状態列に設定して、有限状態機械モデル１００に追加させる。具体的には、上述した例では、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝とすると、状態遷移列｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝のうち、｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝が最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に含まれていないと判断される。したがって、状態遷移列｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を対象状態列に設定する。
【０１３０】
これにより、更新部１６０５では、対象状態列｛Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝を最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１｝に追加することで、中間ＦＳＭ１６００が更新され、最新の中間ＦＳＭ１６００｛Ｓ０→Ｓ１→Ｓ３→Ｓ８→Ｓ１０｝となる。
【０１３１】
ＦＳＭ出力部１６０６は、シナリオ抽出部１６０１により未抽出のテストシナリオがない場合、更新部１６０５によって更新された最新の有限状態機械モデル１００を出力する。具体的には、テストシナリオがすべて抽出されると、もう中間ＦＳＭ１６００は更新する余地がない。したがって、最新の中間ＦＳＭ１６００を、完成された有限状態機械モデル１００として出力することとなる。出力された有限状態機械モデル１００は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶される。
【０１３２】
（ＦＳＭ生成処理部１５０１によるＦＳＭ生成処理）
図１７は、ＦＳＭ生成処理部１５０１によるＦＳＭ生成処理手順を示すフローチャートである。まず、ＦＳＭ生成処理部１５０１は、中間ＦＳＭ１６００として初期状態Ｓ０を設定する（ステップＳ１７０１）。つぎに、ＦＳＭ生成処理部１５０１は、シナリオ抽出部１６０１により、テストシナリオ群ｔｓの中から未抽出のテストシナリオがあるか否かを判断する（ステップＳ１７０２）。未抽出のテストシナリオがある場合（ステップＳ１７０２：Ｙｅｓ）、ＦＳＭ生成処理部１５０１は、未抽出のテストシナリオを１つ抽出する（ステップＳ１７０３）。
【０１３３】
そして、ＦＳＭ生成処理部１５０１は、遷移先状態特定部１６０２により、抽出テストシナリオから遷移先状態列を特定する（ステップＳ１７０４）。このあと、ＦＳＭ生成処理部１５０１は、中間ＦＳＭ判断部１６０３により、特定された遷移先状態列のうち、最新の中間ＦＳＭ１６００にない状態列が存在するか否かを判断する（ステップＳ１７０５）。最新の中間ＦＳＭ１６００にない状態列がない場合（ステップＳ１７０５：Ｎｏ）、ステップＳ１７０２に戻る。
【０１３４】
一方、最新の中間ＦＳＭ１６００にない状態列がある場合（ステップＳ１７０５：Ｙｅｓ）、ＦＳＭ生成処理部１５０１は、設定部１６０４により、特定された遷移先状態列のうち、最新の中間ＦＳＭ１６００にない状態列を、対象状態列に設定する（ステップＳ１７０６）。このあと、ＦＳＭ生成処理部１５０１は、更新部１６０５により、対象状態列を最新の中間ＦＳＭ１６００に追加する（ステップＳ１７０７）。これにより、中間ＦＳＭ１６００が更新される。
【０１３５】
そのあと、ステップＳ１７０２に戻る。ステップＳ１７０２において、未抽出のテストシナリオがない場合（ステップＳ１７０２：Ｎｏ）、ＦＳＭ生成処理部１５０１は、ＦＳＭ出力部１６０６により、最新の中間ＦＳＭ１６００を、完成された有限状態機械モデル１００として出力する（ステップＳ１７０８）。
【０１３６】
このように、ＦＳＭ生成処理部１５０１では、テストシナリオ群ｔｓを解析して中間ＦＳＭ１６００に追加することにより、中間ＦＳＭ１６００がいわゆる雪だるま式に大きくなり、テストシナリオ群ｔｓによる状態遷移を網羅する有限状態機械モデル１００を生成することができる。
【０１３７】
＜ＦＳＭ修正処理部１５０２の詳細説明＞
（ＦＳＭ修正処理部１５０２の機能的構成）
図１８は、ＦＳＭ修正処理部１５０２および登録／復元処理部１５０３の機能的構成を示すブロック図である。ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１と、遷移先状態判断部１８０２と、判断結果出力部１８０３と、仮決定部１８０４と、登録済判断部１８０５と、修正部１８０６と、修正済ＦＳＭ出力部１８０７と、登録部１８１４と、を備えている。
【０１３８】
シナリオ抽出部１８０１は、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを抽出する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓの中から対象回路のシミュレーションに用いる対象テストシナリオを順次抽出する。対象テストシナリオが抽出されると、シミュレーション実行部４０２に与えられてシミュレーションが開始する。
【０１３９】
遷移先状態判断部１８０２は、対象回路のシミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態と、ＦＳＭ生成処理部１５０１によって生成された有限状態機械モデル１００における対象要素による遷移先状態とが、一致するか否かを判断する。
【０１４０】
具体的には、たとえば、テストシナリオＴ１を与えてシミュレーションを実行している場合、現状態Ｓ０について有限状態機械モデル１００では、状態Ｓ０の遷移先状態はＳ１であるのに対し、シミュレーションでの現状態Ｓ０の次状態が状態Ｓ１であれば、一致すると判断する。一方、次状態が状態Ｓ１以外、たとえば、状態Ｓ２であれば、不一致と判断する。
【０１４１】
判断結果出力部１８０３は、遷移先状態判断部１８０２によって判断された判断結果を出力する。遷移先状態判断部１８０２によって不一致が発生した場合、シミュレーションの中止指示情報をシミュレーション実行部４０２に出力する。シミュレーション実行部４０２は、中止指示情報を受け付けると、シミュレーションを中止する。一方、遷移先状態判断部１８０２によって一致した場合、仮決定部１８０４を実行する。
【０１４２】
仮決定部１８０４は、遷移先状態判断部１８０２によって一致すると判断された場合、シミュレーションの実行により対象要素において状態遷移が発生したことによる遷移先状態をデータベース４２０への登録対象に仮決定する。具体的には、たとえば、遷移先状態判断部１８０２によって一致したときの状態Ｓｋを登録対象に仮決定する。
【０１４３】
登録済判断部１８０５は、仮決定部１８０４によって仮決定された登録対象が、データベース４２０に登録済みか否かを判断する。具体的には、データベース４２０を参照して、登録対象と同一のコンテキスト情報がデータベース４２０に登録済であるか否かを判断する。
【０１４４】
登録部１８１４は、登録済判断部１８０５により登録済でないと判断された場合、登録部１８１４により登録対象をデータベース４２０に登録することになる。一方、登録済判断部１８０５により登録済であると判断された場合、コンテキスト情報が同一で状態名が異なる状態がデータベース４２０に登録済であるため、修正部１８０６により有限状態機械モデル１００の修正を実行する。
【０１４５】
修正部１８０６は、登録済判断部１８０５によって登録済みであると判断された場合、登録対象への遷移元状態を、登録対象と一致する登録済みの遷移先状態への遷移元状態に修正し、登録対象からの遷移先状態を、登録済みの遷移先状態からの遷移先状態に修正する。
【０１４６】
具体的には、たとえば、図１４を例に挙げると、状態Ｓ９が登録対象であり、状態Ｓ８が状態Ｓ９に一致する登録済の状態とする。この場合、状態Ｓ９への遷移元状態である状態Ｓ４の遷移先を状態Ｓ８に設定する。すなわち、遷移ｈの遷移先を状態Ｓ８に変更して、遷移ｐとする。
【０１４７】
同様に、状態Ｓ９からの遷移先状態Ｓ１１，Ｓ１２のうち、状態Ｓ１１は、状態Ｓ８からの遷移先状態でもある。すなわち、状態Ｓ９からの遷移ｉは状態Ｓ８からの遷移ｅに一致するため、遷移ｉを削除する。また、状態Ｓ１２に遷移する遷移ｊの遷移元を状態Ｓ９から状態Ｓ８に変更し、遷移ｑとする。修正部１８０６では、登録済判断部１８０５から修正指示を受け付ける都度、修正処理を実行する。
【０１４８】
修正済ＦＳＭ出力部１８０７は、修正された修正済ＦＳＭ１４００を出力する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓ内のテストシナリオについてすべてシミュレーションが終了した場合、最終的に修正済ＦＳＭ１４００を出力する。修正済ＦＳＭ１４００は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶装置に記憶される。
【０１４９】
（ＦＳＭ修正処理部１５０２によるＦＳＭ修正処理）
図１９は、ＦＳＭ修正処理部１５０２によるＦＳＭ修正処理手順を示すフローチャートである。まず、ＦＳＭ修正処理部１５０２は、シミュレーションの開始を待ち受ける（ステップＳ１９０１：Ｎｏ）。シミュレーションが開始された場合（ステップＳ１９０１：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１により、未抽出のテストシナリオがあるか否かを判断する（ステップＳ１９０２）。
【０１５０】
短縮化テストシナリオ群Ｔｓの中で未抽出のテストシナリオがある場合（ステップＳ１９０２：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、未抽出のテストシナリオを抽出する（ステップＳ１９０３）。これにより、抽出テストシナリオがシミュレーション実行部４０２に与えられるため、状態遷移が発生することになる。
【０１５１】
そして、シミュレーション実行部４０２での状態遷移の発生が検出された場合（ステップＳ１９０４：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、発生した状態遷移による遷移先状態と有限状態機械モデル１００での遷移先状態とが一致するか否か判断する（ステップＳ１９０５）。
【０１５２】
不一致である場合（ステップＳ１９０５：Ｎｏ）、抽出テストシナリオと有限状態機械モデル１００との間に齟齬があるため、ＦＳＭ修正処理部１５０２は、判断結果出力部１８０３により、シミュレーション実行部４０２に対し中止指示情報を出力する（ステップＳ１９０６）。これにより、シミュレーション実行部４０２では、シミュレーションを中止することとなる。
【０１５３】
一方、ステップＳ１９０５において、一致すると判断された場合（ステップＳ１９０５：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、仮決定部１８０４により、シミュレーション実行部４０２による状態遷移の発生で得られた遷移先状態をデータベース４２０への登録対象に仮決定する（ステップＳ１９０７）。そして、ＦＳＭ修正処理部１５０２は、仮決定された登録対象と同一コンテキスト情報の状態がデータベース４２０に登録済であるか否かを、登録済判断部１８０５により判断する（ステップＳ１９０８）。
【０１５４】
登録済である場合（ステップＳ１９０８：Ｙｅｓ）、ＦＳＭ修正処理部１５０２は、修正部１８０６により有限状態機械モデル１００を修正して（ステップＳ１９０９）、ステップＳ１９０４に戻る。一方、登録済でない場合（ステップＳ１９０８：Ｎｏ）、ＦＳＭ修正処理部１５０２は、登録対象をデータベース４２０に登録して（ステップＳ１９１０）、ステップＳ１９０４に戻る。
【０１５５】
また、ステップＳ１９０４において、状態遷移が発生しなくなった場合（ステップＳ１９０４：Ｎｏ）、抽出テストシナリオによるシミュレーションが終了したこととなり、ステップＳ１９０２に戻る。ステップＳ１９０２において、ＦＳＭ修正処理部１５０２は、シナリオ抽出部１８０１により、未抽出のテストシナリオがない場合（ステップＳ１９０２：Ｎｏ）、ＦＳＭ修正処理を終了する。
【０１５６】
＜登録／復元処理部１５０３の詳細説明＞
（登録／復元処理部１５０３の機能的構成）
つぎに、図１８を用いて、登録／復元処理部１５０３の機能的構成について説明する。登録／復元処理部１５０３は、判別部１００２と、登録部１８１４と、判定部１００３と、復元部１００５と、を備えている。判別部１００２、判定部１００３および復元部１００５については、実施の形態１と同一構成であるため、説明を省略する。
【０１５７】
判別部１００２は、シナリオ抽出部１８０１によって抽出された対象テストシナリオを構成する一連の要素の中から対象回路に対象要素を順次与えて模擬する対象回路のシミュレーションの実行中に、対象要素の種類を判別する。具体的には、たとえば、短縮化テストシナリオ群Ｔｓを構成するテストシナリオには、登録指示情報が埋め込まれているテストシナリオＴ１や復元指示情報が埋め込まれているテストシナリオＴ２が存在する。
【０１５８】
判別部１００２は、対象テストシナリオの中から対象回路に与えられた対象要素の種別が、（Ｓｊ→Ｓｋ）といった遷移をあらわす要素であるか、登録指示情報ｒｅｃｏｒｄ（Ｓｋ）であるか、復元指示情報ｒｅｓｔｏｒｅ（Ｓｋ）であるかを判別する。
【０１５９】
登録部１８１４は、判別部１００２により対象要素が登録指示情報であると判別された場合、特定の遷移先状態をデータベース４２０に登録する。具体的には、たとえば、登録指示情報が“ｒｅｃｏｒｄ（Ｓｋ）”である場合、状態Ｓｋ、すなわち、対象回路内の組み合わせ回路の出力先となるレジスタの値を、状態Ｓｋの識別子と関連付けてデータベース４２０に登録する。ただし、実施の形態２では、ＦＳＭ修正処理部１５０２により登録済となる場合があるため、登録済の場合は、登録しない。
【０１６０】
（登録／復元処理部１５０３による登録／復元処理）
つぎに、登録／復元処理部１５０３による登録／復元処理について説明する。登録／復元処理については、実施の形態１において図１２および図１３を用いて説明したが、図１２の登録／復元処理手順を示すフローチャート（その１）については、実施の形態２においても同一処理であるため、説明を省略する。
【０１６１】
図２０は、登録／復元処理部１５０３による登録／復元処理手順を示すフローチャート（その３）である。まず、登録／復元処理部１５０３は、ステップＳ１２０６において抽出された抽出要素を対象回路のハードウェア記述情報４３０に与える（ステップＳ２００１）。これにより、シミュレーション実行部４０２では、対象回路のシミュレーションが実行される。そして、状態遷移の発生を待ち受ける（ステップＳ２００２）。
【０１６２】
状態遷移が発生しなかった場合（ステップＳ２００２：Ｎｏ）、末尾の状態に到達したこととなり、シミュレーション実行部４０２からその旨の通知を受けることになる。この場合は、ステップＳ１２０５に戻る。この場合、ステップＳ１２０５に戻っても未選択要素がないため、ステップＳ１２０３に戻ることになる。なお、現状態から次状態への状態遷移については、状態遷移が発生したものとする。
【０１６３】
一方、ステップＳ２００２において、状態遷移が発生した場合（ステップＳ２００２：Ｙｅｓ）、登録／復元処理部１５０３は、発生した状態遷移による遷移先状態Ｓｋが登録／復元対象であるか否かを判断する（ステップＳ２００３）。具体的には、遷移先状態Ｓｋが、すでに他のテストシナリオにおいて登録指示情報で指定されているか否かを判断する。
【０１６４】
発生した状態遷移による遷移先状態Ｓｋが登録／復元対象でない場合（ステップＳ２００３：Ｎｏ）、ステップＳ１２０５に戻る。一方、遷移先状態が登録／復元対象である場合（ステップＳ２００３：Ｙｅｓ）、登録／復元処理部１５０３は、発生した状態遷移による遷移先状態Ｓｋがすでにデータベース４２０に登録済であるか否かをコンテキスト情報により判断する（ステップＳ２００４）。具体的には、発生した状態遷移による遷移先状態Ｓｋに一致するコンテキスト情報がある場合は、登録済、ない場合は未登録と判断される。
【０１６５】
登録済である場合（ステップＳ２００４：Ｙｅｓ）、ステップＳ１２０５に戻る。未登録の場合（ステップＳ２００４：Ｎｏ）、登録／復元処理部１５０３は、初期状態Ｓ０から遷移先状態Ｓｋまでのシミュレーション時間をシミュレーション実行部４０２から取得する（ステップＳ２００５）。そして、登録／復元処理部１５０３は、遷移先状態Ｓｋでの遷移数差分Ｎ（Ｓｋ）に復元時間Ｒｅｓを乗じた値（Ｎ（Ｓｋ）×Ｒｅｓ）が所定のしきい値Ｔに記録時間Ｒｅｃを乗じた値（Ｔ×Ｒｅｃ）以上であるか否かを判断する（ステップＳ２００６）。
【０１６６】
Ｎ（Ｓｋ）×Ｒｅｓ≧Ｔ×Ｒｅｃである場合（ステップＳ２００６：Ｙｅｓ）、登録／復元処理部１５０３は、式（５）を満たすか否かを判断する（ステップＳ２００７）。式（５）を満たさない場合（ステップＳ２００７：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（５）を満たす場合（ステップＳ２００７：Ｙｅｓ）、登録／復元処理部１５０３は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ２００８）、ステップＳ１２０５に戻る。
【０１６７】
一方、ステップＳ２００６において、Ｎ（Ｓｋ）≧Ｔでない場合（ステップＳ２００６：Ｎｏ）、登録／復元処理部１５０３は、式（４）を満たすか否かを判断する（ステップＳ２００９）。式（４）を満たさない場合（ステップＳ２００９：Ｎｏ）、ステップＳ１２０５に戻る。一方、式（４）を満たす場合（ステップＳ２００９：Ｙｅｓ）、登録／復元処理部１５０３は、遷移先状態Ｓｋをコンテキスト情報としてデータベース４２０に登録し（ステップＳ２０１０）、ステップＳ１２０５に戻る。
【０１６８】
このような登録／復元処理によれば、ＦＳＭ修正処理部１５０２において登録されなかった状態についても復元すればよいかが自動設定されているため、設計者が試行錯誤して登録／復元対象を探す必要はない。したがって、対象回路のシミュレーションを効率的に短縮化することができる。
【０１６９】
以上説明したように、本実施の形態によれば、一のテストシナリオに登録指示情報を埋め込むことで、シミュレーション実行時に、登録／復元対象となる遷移先状態（対象回路を構成するレジスタの値）をデータベースに登録することができる。したがって、他のテストシナリオでシミュレーションを実行する場合、登録／復元対象に状態遷移したときは、データベースを参照することで、容易に復元することができる。
【０１７０】
また、データベースに登録された登録／復元対象を復元させる復元指示情報を他のテストシナリオに埋め込んでおくことで、シミュレーション時には、一のテストシナリオと重複するシナリオを実行することなく、データベースを参照するだけで登録／復元対象を復元することができる。このように、短縮化テストシナリオ群を自動生成することができるため、設計者は登録／復元対象を探したりする負担が軽減され、検証期間の短縮化を図ることができる。
【０１７１】
また、シミュレーションと並列に有限状態機械モデルを検証することができ、検証期間の短縮化を図ることができる。また、有限状態機械モデルと短縮化テストシナリオ群は、それぞれ独自に作成されるため、シミュレーションとＦＳＭ検証を並列実行すればその分、不整合を早期発見することができる。
【０１７２】
また、単に、データベースに状態を登録させるだけではなく、シミュレーション時間の短縮が見込めない場合、すなわち、登録および復元の処理時間よりも、重複したテストシナリオでシミュレーションを実行したほうが時間短縮になる場合には、登録／復元対象を登録しない。このように、時間短縮が可能か否かを詳細に判断することができるため、シミュレーションの効率化を図ることができる。
【０１７３】
また、有限状態機械モデルとテストシナリオ群は、それぞれ独自に作成されるが、テストシナリオ群を用いて有限状態機械モデルを自動生成することで、人手により作成する場合よりも整合性を保証することができ、検証精度の向上を図ることができる。
【０１７４】
また、有限状態機械モデルを自動生成した場合、冗長な表現になる場合があるため、シミュレーションの実行に並列して、有限状態機械モデルを修正することで、有限状態機械モデルの最適化を図ることができる。また、修正後の有限状態機械モデルにより短縮化テストシナリオ群の修正を設計者が施すことで、その後、テストシナリオ短縮化処理により、短縮化テストシナリオ群をさらに短縮化することができる。このように、シミュレーション回数を重ねるごとに、テストシナリオが短縮化されるため、シミュレーション時間もより効率的に短縮化することができる。
【０１７５】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムは、インターネット等のネットワークを介して配布してもよい。
【０１７６】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０１７７】
（付記１）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１７８】
（付記２）前記第２の埋込工程は、
前記第１の埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする付記１に記載の検証支援プログラム。
【０１７９】
（付記３）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１８０】
（付記４）前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態までのシミュレーション時間と前記データベースからの所定の復元時間とに基づいて、前記登録工程により登録すべきか否かを判定する判定工程を前記コンピュータに実行させ、
前記登録工程は、
前記判定工程によって登録すべきであると判定された場合、前記特定の遷移先状態を前記データベースに登録することを特徴とする付記３に記載の検証支援プログラム。
【０１８１】
（付記５）前記対象回路のシミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態と、前記対象回路に関する有限状態機械モデルにおける前記対象要素による遷移先状態とが、一致するか否かを判断する遷移先状態判断工程と、
前記遷移先状態判断工程によって判断された判断結果を出力する判断結果出力工程と、
を前記コンピュータに実行させることを特徴とする付記３または４に記載の検証支援プログラム。
【０１８２】
（付記６）前記判断結果出力工程は、
前記遷移先状態判断工程によって不一致と判断された場合、前記シミュレーションの中止指示情報を前記実行手段に出力することを特徴とする付記５に記載の検証支援プログラム。
【０１８３】
（付記７）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新工程と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出工程と、
前記抽出工程によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定工程と、
前記遷移先状態列特定工程によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断工程と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断工程によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定工程と、
前記抽出工程による未抽出のテストシナリオがない場合、前記更新工程によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０１８４】
（付記８）前記テストシナリオ群の中から一のテストシナリオを選択する選択工程と、
前記選択工程によって選択された一のテストシナリオを構成する一連の要素の中から選ばれた一の選択要素による遷移先状態を、前記ＦＳＭ出力工程によって出力された有限状態機械モデルの中から検出する検出工程と、
前記検出工程によって検出された遷移先状態へ遷移する入力遷移数と前記遷移先状態から遷移する出力遷移数を前記有限状態機械モデルから特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記決定工程によって決定された登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記一の選択要素の次の要素として埋め込む埋込工程と、
をコンピュータに実行させることを特徴とする付記７に記載の検証支援プログラム。
【０１８５】
（付記９）前記検出工程によって、前記一のテストシナリオ以外の他のテストシナリオを構成する一連の要素の中から選ばれた他の選択要素による遷移先状態が、前記有限状態機械モデルの中から検出された場合、前記一のテストシナリオにおいて前記埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象と一致するか否かを判断する登録／復元対象判断工程を前記コンピュータに実行させ、
前記埋込工程は、
前記登録／復元対象判断工程によって一致すると判断された場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記他の選択要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする付記８に記載の検証支援プログラム。
【０１８６】
（付記１０）前記埋込工程によって、特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記埋込工程によって、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、前記対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、当該シミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態と、前記ＦＳＭ出力工程によって出力された有限状態機械モデルにおける前記対象要素による遷移先状態とが、一致するか否かを判断する遷移先状態判断工程と、
前記遷移先状態判断工程によって判断された判断結果を出力する判断結果出力工程と、
を前記コンピュータに実行させることを特徴とする付記９に記載の検証支援プログラム。
【０１８７】
（付記１１）前記判断結果出力工程は、
前記遷移先状態判断工程によって不一致と判断された場合、前記シミュレーションの中止指示情報を、前記シミュレーションを実行する実行手段に出力することを特徴とする付記１０に記載の検証支援プログラム。
【０１８８】
（付記１２）前記遷移先状態判断工程によって一致すると判断された場合、前記シミュレーションの実行により前記対象要素において状態遷移が発生したことによる遷移先状態を前記データベースへの登録対象に仮決定する仮決定工程と、
前記仮決定工程によって仮決定された登録対象が、前記データベースに登録済みか否かを判断する登録済判断工程と、
前記登録済判断工程によって登録済みでないと判断された場合、前記登録対象を前記データベースに登録する登録工程と、
前記登録済判断工程によって登録済みであると判断された場合、前記登録対象への遷移元状態を、前記登録対象と一致する登録済みの遷移先状態への遷移元状態に修正し、前記登録対象からの遷移先状態を、前記登録済みの遷移先状態からの遷移先状態に修正する修正工程と、
前記修正工程によって修正された修正後の有限状態機械モデルを出力する修正済ＦＳＭ出力工程と、
を前記コンピュータに実行させることを特徴とする付記１０に記載の検証支援プログラム。
【０１８９】
（付記１３）前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
を前記コンピュータに実行させることを特徴とする付記１０〜１２のいずれか一つに記載の検証支援プログラム。
【０１９０】
（付記１４）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定手段と、
前記遷移数特定手段によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定手段と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定手段によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込手段と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込手段と、
を備えることを特徴とする検証支援装置。
【０１９１】
（付記１５）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出手段と、
前記シナリオ抽出手段によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別手段と、
前記判別手段により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録手段と、
前記判別手段により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元手段と、
を備えることを特徴とする検証支援装置。
【０１９２】
（付記１６）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新手段と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出手段と、
前記抽出手段によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定手段と、
前記遷移先状態列特定手段によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断手段と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断手段によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定手段と、
前記抽出手段による未抽出のテストシナリオがない場合、前記更新手段によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力手段と、
を備えることを特徴とする検証支援装置。
【０１９３】
（付記１７）遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
コンピュータが実行することを特徴とする検証支援方法。
【０１９４】
（付記１８）特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【０１９５】
（付記１９）対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新工程と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出工程と、
前記抽出工程によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定工程と、
前記遷移先状態列特定工程によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断工程と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断工程によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定工程と、
前記抽出工程による未抽出のテストシナリオがない場合、前記更新工程によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【符号の説明】
【０１９６】
１００ 有限状態機械モデル
４００ 検証支援装置
４０１ テストシナリオ短縮化処理部
４０２ シミュレーション実行部
４０３ ＦＳＭ検証処理部
４０４ 登録／復元処理部
４２０ データベース
１５００ 検証支援装置
１５０１ ＦＳＭ生成処理部
１５０２ ＦＳＭ修正処理部
１５０３ 登録／復元処理部
ｔｓ テストシナリオ群
Ｔｓ 短縮化テストシナリオ群
【特許請求の範囲】
【請求項１】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項２】
前記第２の埋込工程は、
前記第１の埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項４】
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態までのシミュレーション時間と前記データベースからの所定の復元時間とに基づいて、前記登録工程により登録すべきか否かを判定する判定工程を前記コンピュータに実行させ、
前記登録工程は、
前記判定工程によって登録すべきであると判定された場合、前記特定の遷移先状態を前記データベースに登録することを特徴とする請求項３に記載の検証支援プログラム。
【請求項５】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定手段と、
前記遷移数特定手段によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定手段と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定手段によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込手段と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込手段と、
を備えることを特徴とする検証支援装置。
【請求項６】
特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出手段と、
前記シナリオ抽出手段によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別手段と、
前記判別手段により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録手段と、
前記判別手段により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元手段と、
を備えることを特徴とする検証支援装置。
【請求項７】
対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新手段と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出手段と、
前記抽出手段によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定手段と、
前記遷移先状態列特定手段によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断手段と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断手段によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定手段と、
前記抽出手段による未抽出のテストシナリオがない場合、前記更新手段によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力手段と、
を備えることを特徴とする検証支援装置。
【請求項８】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【請求項１】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項２】
前記第２の埋込工程は、
前記第１の埋込工程によって埋め込まれた登録指示情報が指定する前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込むことを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出工程と、
前記シナリオ抽出工程によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別工程と、
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録工程と、
前記判別工程により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項４】
前記判別工程により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態までのシミュレーション時間と前記データベースからの所定の復元時間とに基づいて、前記登録工程により登録すべきか否かを判定する判定工程を前記コンピュータに実行させ、
前記登録工程は、
前記判定工程によって登録すべきであると判定された場合、前記特定の遷移先状態を前記データベースに登録することを特徴とする請求項３に記載の検証支援プログラム。
【請求項５】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定手段と、
前記遷移数特定手段によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定手段と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定手段によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込手段と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込手段と、
を備えることを特徴とする検証支援装置。
【請求項６】
特定の遷移先状態をデータベースに登録させる登録指示情報が埋め込まれたテストシナリオと、前記特定の遷移先状態を前記データベースから復元させる復元指示情報が埋め込まれたテストシナリオと、を含むテストシナリオ群の中から、対象回路のシミュレーションに用いる対象テストシナリオを抽出するシナリオ抽出手段と、
前記シナリオ抽出手段によって抽出された対象テストシナリオを構成する一連の要素の中から前記対象回路に対象要素を順次与えて模擬する前記対象回路のシミュレーションの実行中に、前記対象要素の種類を判別する判別手段と、
前記判別手段により前記対象要素が前記登録指示情報であると判別された場合、前記特定の遷移先状態を前記データベースに登録する登録手段と、
前記判別手段により前記対象要素が前記復元指示情報であると判別された場合、前記特定の遷移先状態を前記データベースから復元する復元手段と、
を備えることを特徴とする検証支援装置。
【請求項７】
対象回路に関する有限状態機械モデルに対象状態列が追加されることにより、前記有限状態機械モデルを更新する更新手段と、
前記対象回路に関するテストシナリオ群の中から任意のテストシナリオを抽出する抽出手段と、
前記抽出手段によって抽出されたテストシナリオの状態遷移により出現する遷移先状態列を特定する遷移先状態列特定手段と、
前記遷移先状態列特定手段によって特定された遷移先状態列が、前記有限状態機械モデルに含まれているか否かを判断する中間ＦＳＭ判断手段と、
前記遷移先状態列のうち、前記中間ＦＳＭ判断手段によって含まれていないと判断された遷移先状態列を前記対象状態列に設定して、前記有限状態機械モデルに追加させる設定手段と、
前記抽出手段による未抽出のテストシナリオがない場合、前記更新手段によって更新された最新の有限状態機械モデルを出力するＦＳＭ出力手段と、
を備えることを特徴とする検証支援装置。
【請求項８】
遷移先状態への入力遷移数と前記遷移先状態からの出力遷移数を、対象回路に関する有限状態機械モデルの中から特定する遷移数特定工程と、
前記遷移数特定工程によって特定された前記出力遷移数が前記入力遷移数よりも多い場合、前記遷移先状態を登録／復元対象に決定する決定工程と、
前記対象回路に関するテストシナリオ群の中の一のテストシナリオを構成する一連の要素の中に前記決定工程によって決定された登録／復元対象に遷移させる第１の要素がある場合、前記登録／復元対象をデータベースに登録させる登録指示情報を、前記一のテストシナリオ内の前記第１の要素の次の要素として埋め込む第１の埋込工程と、
前記テストシナリオ群の中の他のテストシナリオを構成する一連の要素の中に前記登録／復元対象に遷移させる第２の要素がある場合、前記登録／復元対象を前記データベースから復元させる復元指示情報を、前記他のテストシナリオを構成する一連の要素の先頭要素から前記第２の要素までの要素群に代えて、前記他のテストシナリオに埋め込む第２の埋込工程と、
をコンピュータが実行することを特徴とする検証支援方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【図２０】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【図２０】
【公開番号】特開２０１１−２３７８４１（Ｐ２０１１−２３７８４１Ａ）
【公開日】平成２３年１１月２４日（２０１１．１１．２４）
【国際特許分類】
【出願番号】特願２０１０−１０５８９９（Ｐ２０１０−１０５８９９）
【出願日】平成２２年４月３０日（２０１０．４．３０）
【出願人】（０００００５２２３）富士通株式会社 (25,993)
【Ｆターム（参考）】
【公開日】平成２３年１１月２４日（２０１１．１１．２４）
【国際特許分類】
【出願日】平成２２年４月３０日（２０１０．４．３０）
【出願人】（０００００５２２３）富士通株式会社 (25,993)
【Ｆターム（参考）】
[ Back to top ]