(57)【特許請求の範囲】
【請求項１】
検証対象のハードウェアの論理を検証するための論理検証用入力時系列を生成する論理検証用入力時系列の生成装置であって、
ハードウェアの動作における状態を表す有限状態機械の記述を入力する手段と、
前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求め、初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求め、前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の手段と、
前記入力時系列の集合から入力時系列の短い順に入力時系列を選択し、選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求め、求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す手段と、
前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する手段とを備える
ことを特徴とする論理検証用入力時系列の生成装置。
【請求項２】
検証対象のハードウェアの論理を検証するための論理検証用入力時系列をコンピュータによって生成する論理検証用入力時系列の生成方法であって、
前記コンピュータが、
ハードウェアの動作における状態を表す有限状態機械の記述を入力する過程と、
前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求める前処理の過程と、
初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求める前処理の過程と、
前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の過程とを有するとともに、
前記入力時系列の集合から入力時系列の短い順に入力時系列を選択する過程と、
選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求める過程と、
該過程で求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す過程と、
前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する過程とを有する
ことを特徴とする論理検証用入力時系列の生成方法。
【請求項３】
前記深さ優先探索において探索が不可能になった状態に到達したとき、過去に網羅していない状態遷移の中で、その状態から最短の入力時系列で遷移可能である状態遷移を探索し、その新たに探索した状態遷移の到達先の状態から、さらに深さ優先探索を継続する
ことを特徴とする請求項２に記載の論理検証用入力時系列の生成方法。
【請求項４】
前記入力した有限状態機械の記述は、複数のユニットの状態を表す有限状態機械の記述であり、その有限状態機械の中で、ユニットの対称性によりユニットの順序性を無視した場合に同一の状態となるものの一つを代表状態として定める前処理の過程を有し、
前記入力時系列の集合から入力時系列の短い順に入力時系列を選択する過程では、初期状態から代表状態に到達する入力時系列の中から、入力時系列を選択し、
前記深さ優先探索により新たな入力時系列を生成する過程では、探索した状態遷移の到達先が代表状態であれば、深さ優先探索を継続し、探索した状態遷移の到達先が代表状態以外であれば、遷移前の状態から到達先の状態が含まれる代表状態に遷移する状態遷移が存在するか否かを調べ、存在すれば遷移前の状態に戻り改めて深さ優先探索を継続し、遷移前の状態から到達先の状態が含まれる代表状態に遷移する状態遷移が存在しなければ、上記の探索で求めた状態遷移を選択し、深さ優先探索を終了する
ことを特徴とする請求項２に記載の論理検証用入力時系列の生成方法。
【請求項５】
検証対象のハードウェアの論理を検証するための論理検証用入力時系列を生成する論理検証用入力時系列の生成装置のコンピュータに実行させるためのプログラムを記憶するコンピュータ読み取り可能な記憶媒体であって、
前記コンピュータを、
ハードウェアの動作における状態を表す有限状態機械の記述を入力する手段と、
前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求め、初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求め、前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の手段と、
前記入力時系列の集合から入力時系列の短い順に入力時系列を選択し、選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求め、求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す手段と、
前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する手段として機能させるための、
論理検証用入力時系列の生成プログラムを記憶する記憶媒体。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、装置の状態を有限状態機械の記述として表すことのできる装置を検証するための論理検証用入力時系列を自動生成する装置およびその生成方法およびそのプログラムを記憶した記憶媒体論理検証用装置の論理検証用入力時系列を自動生成する装置およびその生成方法およびそのプログラムを記憶した記憶媒体に関するものである。特に、マルチプロセッサシステムにおけるキャッシュコヒーレンシープロトコルの検証、もしくはマルチプセッサシステムにおける各々のプロセッサを連結するバスが正しく制御されているかを検証する論理検証用入力時系列の生成装置および生成方法に関するものである。
【０００２】
プロセッサ等のハードウェアを設計する際の論理検証の方法として、一般的に、論理検証用シミュレータにテスト命令列を入力して論理シミュレーションを行なう方法がある。一方、ハードウェアが大規模化、複雑化し、さらに設計期間も短縮されていることから、短時間で信頼性の高い論理検証を行なう必要がある。
【０００３】
本発明を適用するマルチプロセッサシステムにおけるキャッシュコヒーレンシープロトコルとバス制御の論理検証について説明する。
一般的に、プロセッサと主記憶の間に高速な記憶装置であるキャッシュがある。プロセッサが頻繁にアクセスする命令やデータを頻繁にアクセスする命令やデータをキャッシュに記憶させることにより、主記憶のアクセスを低減し、計算機の処理速度を上げることができる。
【０００４】
マルチプロセッサシステムでは、同一のデータのコピーが複数のキャッシュに存在することがある。そのため、データの内容が変更された際、主記憶だけでなく他のキャッシュにも変更を通知し、システム内のデータの統一性を保つことが非常に重要である。データの統一性を保つためには、システム全体で制御の取決めを行なう必要がある。この取決めをキャッシュコヒーレンシープロトコルという。
【０００５】
キャッシュコヒーレンシープロトコルを検証するためには、以下の特徴をもつマルチプロセッサシステムの状態の状態遷移の時間的経過を表す入力時系列を生成する必要がある。
【０００６】
その入力時系列はキャッシュの状態を全て網羅する。特に、ｌｏａｄ命令とｓｔｏｒｅ命令は、バスを通じて他のプロセッサにキャッシュの内容を通知する（図２参照）ので、複数のプロセッサがｌｏａｄ命令またはｓｔｏｒｅ命令を実行すると、バス上に多数の競合が発生する。そのため、キャッシュコヒーレンシープロトコルを検証する入力時系列を生成し、バス制御を検証する入力時系列を生成する必要がある。そして、その入力時系列は、バス上に多数の複雑な競合を長時間発生するものである必要がある。また、各々のプロセッサが入力時系列を実行する際に、実行結果を容易に検証できるものである必要がある。
【０００７】
図１を説明する前に、図２によりマルチプロセッサシステムの動作状態を説明する。
図２において、
３０、３１、３２、３３はそれぞれｃｐｕ０、ｃｐｕ１、ｃｐｕ２、ｃｐｕ３である。ｃｐｕ０、ｃｐｕ１、ｃｐｕ２、ｃｐｕ３はそれぞれキャッシュメモリ４０、４１、４２、４３をもつ。図２のキャッシュは＄１と＄２の階層構造に構成されていることを表す。
【０００８】
３４はメモリ（ｍｅｍｏｒｙ）であって、各プロセッサの共有メモリである。
３５はバスである。
４０はｃｐｕ０のキャッシュである。
【０００９】
４１はｃｐｕ１のキャッシュである。
４２はｃｐｕ２のキャッシュである。
４３はｃｐｕ３のキャッシュである。
【００１０】
図２（ａ）はｃｐｕ０のロード命令の前の状態と後の状態を表す。前の状態はｃｐｕ０がｃｐｕ２にデータのロードを要求したことを表す。後の状態はｃｐｕ２がｃｐｕ０にデータをロードしたことを表す。
【００１１】
図２（ｂ）はｃｐｕ０のストア命令の前の状態と後の状態を表す。前の状態はｃｐｕ０がｃｐｕ２にデータのストアを要求したことを表す。後の状態はｃｐｕ２がｃｐｕ０にデータをストアしたことを表す。
【００１２】
図２（ａ）、図２（ｂ）に示されるように、マルチプロセッサシステムは、キャッシュの状態に応じて様々な状態を持つ。
図２（ｃ）はキャッシュの状態の定義である。
【００１３】
キャッシュのＶａｌｉｄ、Ｅｘｃｌｕｓｉｖｅ、Ｄｉｒｔｙの状態の組み合わせに応じてキャッシュの状態が定義される。
Ｖａｌｉｄはデータが有効（１）もしくは有効でない（０）ことを表す。
【００１４】
Ｅｘｃｌｕｓｉｖｅはデータのコピーが他のキャッシュに存在していない（１）、あるいは存在する（０）ことを表す。
Ｄｉｒｔｙはデータのコピーが主記憶の内容と異なる（１）もしくは一致する（０）ことを表す。
【００１５】
Ｖａｌｉｄ、Ｅｘｃｌｕｓｉｖｅ、Ｄｉｒｔｙの状態の組合せに応じて、Ｍｏｄｉｆｉｅｄ（Ｍ）、Ｏｗｎｅｄ（Ｏ）、Ｅｘｃｌｕｓｉｖｅ（Ｅ）、Ｓｈａｒｅｄ（Ｓ）、Ｉｎｖａｌｉｄ（Ｉ）が定義される。
Ｍｏｄｉｆｉｅｄ（Ｍ）はＶａｌｉｄが１で有効、Ｅｘｃｌｕｓｉｖｅが１でデータのコピーが他のキャッシュに存在してなく、Ｄｉｒｔｙが１で主記憶の内容と一致する状態を表す。
【００１６】
Ｏｗｎｅｄ（Ｏ）はＶａｌｉｄが１で有効、Ｅｘｃｌｕｓｉｖｅが０でデータのコピーが他のキャッシュに存在していて、Ｄｉｒｔｙが１で主記憶の内容と一致する状態を表す。
【００１７】
Ｅｘｃｌｕｓｉｖｅ（Ｅ）はＶａｌｉｄが１で有効、Ｅｘｃｌｕｓｉｖｅが１でデータのコピーが他のキャッシュに存在してなく、Ｄｉｒｔｙが０で主記憶の内容と一致していない状態を表す。
【００１８】
Ｓｈａｒｅｄ（Ｓ）はＶａｌｉｄが１で有効、Ｅｘｃｌｕｓｉｖｅが０でデータのコピーが他のキャッシュに存在していて、Ｄｉｒｔｙが０で主記憶の内容と一致していない状態を表す。
【００１９】
Ｉｎｖａｌｉｄ（Ｉ）はＶａｌｉｄが０で無効である状態を表す。
【００２０】
【従来の技術】
従来のマルチプロセッサシステムの入力時系列の生成方法について説明する。
キャッシュコヒーレンシーとバス制御の論理検証は、テスト命令列を生成し、シミュレータにテスト命令列を入力し、シミュレーションにより論理検証を行なう。
【００２１】
従来のテスト命令列の生成方法は、ランダム命令列とバイアス命令列の２つの生成方法があり、その双方の命令列を使用してシミュレーションをしていた。
ランダム命令列は計算機の乱数により、命令、使用するレジスタ、レジスタの値を決定する。
【００２２】
バイアス命令列は、設計誤りを生じやすい動作を人手により生成するものである。
検証作業者は、キャッシュコヒーレンシープロトコルとバス制御において、設計誤りを起こしやすい項目を抽出する。これらの項目に対して、誤動作を生じやすい動作を調べて、その動作を実現するバイアス命令列を次の手順で生成する。
【００２３】
（ａ）  キャッシュコヒーレンシープロトコルについて
１．キャッシュ状態の定義を調べる（図２（ｃ）参照）。
２．キャッシュの状態を変化させる命令を調べる（図２（ａ）、（ｂ）等参照）。
【００２４】
（ｂ）バス制御について
１．バスの仕様を調べる。
２．バス上に多数の複雑な競合を発生させる入力時系列を生成する。例えば、あるプロセッサが命令を実行した後に他のプロセッサまたは主記憶にデータアクセスする命令を見つける。そして、全てのプロセッサが上記の特徴を持つ命令を実行する。その際に、全てのプロセッサの実行結果が、バスが命令を受理する順番に依存しないような工夫をする。
【００２５】
３．入力時系列をシミュレターに実行できる命令列に変換する。
論理シミュレーションの実行は、バイアス命令列を様々な状況の下で実行することにより検証項目ができるだけ網羅される様にする。
【００２６】
具体的には次の手順で論理シミュレーションを行なう。
１．人が記述して指示ファイルを作成する。このファイルで乱数を発生させる初期値、
テスト命令列中でテストを行なう機能（キャッシュコヒーレンシープロトコル、バス制御）の割合を示す指示値、バイアス命令列とランダム命令列を組み合わせる割合を決定する指示値を設定する。
【００２７】
２．指示ファイルをスクリプトファイル（機械が読み込むファイル）に変換する。
３．スクリプトファイルで設定した値に従って論理シミュレーション用テスト命令列を生成する。
【００２８】
４．上記の論理シミュレーション用テスト命令列をシミュレータで実行して動作（レジスタの値、データの値等）を確認する。
検証項目に対するバイアス命令列を様々な状況の下で実行するために、指示ファイルの初期値や指示値を様々な値に設定する。様々な状況を網羅する論理検証を行なうように上記の作業をする。
【００２９】
また、本出願人は、パイプライン処理するプロセッサのハードウェア設計をするための論理検証用入力列を自動生成する技術を開発した（特開平７−６０４８７１号公報参照）。これは、パイプラインの有限状態機械の記述に基づいて、パイプラインの多数の状態を実現する入力時系列を生成するものである。
【００３０】
【発明が解決しようとする課題】
上記のように従来のマルチプロセッサのキャッシュコヒーレンシープロトコルとバス制御の検証は、計算機によりランダム命令列を作成し、人手作業によりバイアス命令列を作成して行なってきたが、次のような問題がある。
（１）ランダム命令列は、無意味な命令が多発するとともに、発生した命令も比較的単純な動作のものしか実現できない。そのため、キャッシュコヒーレンシープロトコルに対して、キャッシュの初期状態に近い状態しか網羅できない。また、
バス制御に対して、バス上での単純な競合が短時間しか発生できない。
（２）バイアス命令列は、人手作業のため、時間がかかり生成コストが非常に高い。また、キャッシュコヒーレンシープロトコルに対して、キャッシュの初期状態から到達しにくい状態遷移を網羅する動作を調べることは非常に困難である。
【００３１】
また、バス制御に対して、多数のプロセッサが同時に命令を実行する時にバス制御の順序に依存しないような命令列を生成することは非常に困難である。また、命令列を誤って生成する可能性もある。
【００３２】
本発明は、キャッシュの全ての状態遷移を網羅する入力時系列とバス上に多数の複雑な競合を発生する入力時系列を自動的に短時間で生成することのできる論理検証用入力時系列を自動生成する装置およびその生成方法およびそのプログラムを記憶した記憶媒体を提供することを目的とする。
【００３３】
【課題を解決するための手段】
第１の本発明は、検証対象のハードウェアの論理を検証するための論理検証用入力時系列を生成する論理検証用入力時系列の生成装置であって、ハードウェアの動作における状態を表す有限状態機械の記述を入力する手段と、前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求め、初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求め、前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の手段と、前記入力時系列の集合から入力時系列の短い順に入力時系列を選択し、選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求め、求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す手段と、前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する手段とを備えるようにした。
【００３４】
第２の本発明は、検証対象のハードウェアの論理を検証するための論理検証用入力時系列をコンピュータによって生成する論理検証用入力時系列の生成方法であって、前記コンピュータが、ハードウェアの動作における状態を表す有限状態機械の記述を入力する過程と、前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求める前処理の過程と、初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求める前処理の過程と、
前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の過程とを有するとともに、
前記入力時系列の集合から入力時系列の短い順に入力時系列を選択する過程と、
選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求める過程と、
該過程で求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す過程と、前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する過程とを有するようにした。
【００３５】
また、第３の本発明は、検証対象のハードウェアの論理を検証するための論理検証用入力時系列を生成する論理検証用入力時系列の生成装置のコンピュータに実行させるためのプログラムを記憶するコンピュータ読み取り可能な記憶媒体であって、前記コンピュータを、ハードウェアの動作における状態を表す有限状態機械の記述を入力する手段と、前記入力した有限状態機械の記述に基づいて、初期状態から到達可能な状態集合を求め、初期状態から到達可能な各々の状態に対して、状態遷移の経過を表す最短の入力時系列の集合を求め、前記入力時系列の集合に係る個々の状態遷移を過去に網羅した状態遷移として登録する前処理の手段と、前記入力時系列の集合から入力時系列の短い順に入力時系列を選択し、選択した入力時系列の到達先の状態から遷移可能である状態遷移の中で、過去に網羅していない状態遷移の集合を求め、求めた各々の状態遷移の到達先を出発点として、入力時系列の予め定めた長さの範囲内で、過去に網羅していない状態遷移を深さ優先探索し、新たに探索した状態遷移を過去に網羅した状態遷移として追加登録するとともに、新たに探索した状態遷移を初めに選択した入力時系列に付け加えて、新たな入力時系列を生成する処理を繰り返す手段と、前記深さ優先探索により新たに生成した入力時系列を、全ての状態遷移を網羅する入力時系列の集合の中に登録する手段として機能させるための、論理検証用入力時系列の生成プログラムを記憶する構成を持つようにした。
【００３６】
図１は本発明の基本構成を示す。
図１において、
Ａは論理検証用入力時系列の自動生成装置である。
【００３７】
１は入力装置であって、有限状態機械の記述を入力するものである。
２は到達可能状態生成手段であって、初期状態から到達可能な状態を求めるものである。
【００３８】
３は入力時系列生成手段であって、初期状態から到達可能な状態までの状態遷移の入力時系列を求めるものである。
４は深さ優先探索手段であって、到達した状態からさらに経路の深い方向へ状態を探索するものである。
【００３９】
５は入力時系列登録手段であって、求めた入力時系列を登録するものである。６は出力装置であって、入力時系列を出力するものである。
図１の動作を説明する。
【００４０】
有限状態機械の記述を有限状態機械の記述の入力手段１により入力する。
到達可能状態生成手段２は初期状態から到達可能な状態を求め、登録する。
入力時系列生成手段３は初期状態から到達可能状態に至るまでの状態遷移の入力時系列を生成し、過去の入力時系列として登録する。
【００４１】
深さ優先探索手段４は初期状態から到達できる状態からさらに先の状態まで状態遷移の経路をたどって深さ優先探索をする。
入力時系列登録手段５は深さ優先探索で新たに求めた入力時系列を登録する。
【００４２】
深さ優先探索により、到達可能な状態までの入力時系列が全て求まったら、求めた入力時系列を出力装置により出力する。
例えば、有限状態の記述は、マルチプロセッサのキャッシュの状態をハードウェア記述言語を用いて表現する。そして、キャッシュの有限状態機械を表す有限状態機械形式ファイルを生成する。
【００４３】
また、入力時系列の生成は、例えば、前述のパイプラインの論理検証用の入力時系列を自動生成するのに使用したのと同様の論理検証システム（特開平７−６０４８７１号公報）に、上記の有限機械形式ファイルと有限機械の探索手続きを入力することにより行なう。
【００４４】
この手続きに従って、キャッシュの全ての状態を網羅する入力時系列を自動生成することができる。
上記の深さ優先探索は、次のような変形が可能である。
【００４５】
▲１▼  探索可能な状態遷移が既に全て網羅していたら、その時点で深さ優先探索を終了する。
▲２▼  探索可能な状態が既に網羅されていても、予め指定した入力時系列の長さの範囲で網羅していない状態遷移を探索する。
【００４６】
▲３▼  各マルチプロセッサの状態の組合せの対称性を考慮し、状態の組合せの代表状態を定めて代表状態により探索する。
本発明の入力時系列によりバス制御の探索を行なう時は、次のように行なう。
【００４７】
マルチプロセッサにおけるキャッシュの全ての状態を網羅する入力時系列を利用して、バス制御を検証する入力時系列を生成する。そして、各プロセッサに対して互いに異なるキャッシュのラインを定める。さらに、各々のプロセッサは、設定されたキャッシュのラインに対して命令を発行し（ｃｐｕ０はｌｉｎｅ０に対する命令、ｃｐｕ１はｌｉｎｅ１に対する命令等）、各々のマルチプロセッサ毎の入力時系列を生成する。この入力時系列をバス制御を検証する入力時系列（テスト命令列）に変換する。
【００４８】
この時、以下の変形が可能である。
▲１▼  各々のプロセッサに対して、上記の入力時系列をある集合に従って並べ換える。
【００４９】
▲２▼  各々のプロセッサに対して、上記の入力時系列をｋ個のグループに分類して並べ換える。
▲３▼  各々のプロセッサに対して、上記の入力時系列を入力時系列の長さの短い順に並べ換える。
【００５０】
▲４▼  各々のプロセッサに対して、上記の入力時系列をランダムに並べ換える。
▲５▼  各々のプロセッサに対して、上記の入力時系列集合の長さの等しい入力時系列を同じグループにして、これをｋ個のグループに分類して並べ換える。
【００５１】
本発明によれば、検証対象のハードウェアの動作を表す有限状態機械の記述に基づいて、有限状態機械の全ての状態遷移を網羅する入力時系列を自動的に生成することが可能である。そのため、マルチプロセッサにおけるキャッシュコヒーレンシープロトコルを検証する入力時系列を容易に生成することができる。さらに、この入力時系列を基にマルチプロセッサシステムのバス制御を検証する入力時系列（テスト命令列）を容易に生成することができる。
【００５２】
【発明の実施の形態】
図３、図４、図５、図６、図７を参照して本発明を具体的に説明する。
図３は本発明を適用する状態図の例（その１）である。
【００５３】
図３（ａ）は状態図の例（その１）であり、有限状態機械の記述はこの状態図を記述するものである。
丸で囲った番号（▲１▼、▲２▼、▲３▼、▲４▼、▲５▼、▲６▼、▲７▼）はシステムの状態であり、例えば、マルチプロセッサシステムにおいて各プロセッサがとる状態（前述のＩｎｖａｌｉｄ、Ｍｏｄｉｆｉｅｄ等）の組合わせとして定められる状態を表す。
【００５４】
▲１▼は初期状態を表す（例えば、各プロセッサが全てＩｎｖａｌｉｄ）。
状態間の矢印は状態の遷移する方向を表す。矢印に付けた番号は状態遷移の番号を表す。例えば状態▲１▼から状態▲６▼への状態遷移は１１である。
【００５５】
図３（ｂ）は図３（ｃ）において初期状態から到達できる経路（状態遷移）を黒丸で表したものである。
初期状態から到達できる状態は、状態▲２▼、▲３▼、▲４▼、▲５▼、▲６▼である。例えば、状態▲３▼へは状態遷移１１→６→１０（最短経路）で到達できる。これを入力時系列（１１、６、４）と表す。
【００５６】
本発明は、初期状態から到達できる状態からの状態遷移をさらに求める（これを深さ優先探索と称する）。例えば、状態▲３▼から状態▲４▼への状態遷移２を求める。探索する深さは予めきめておく。
【００５７】
図３（ｃ）は、このようにして求めた状態遷移の経路を表にしたものである。
図３（ｃ）において、状態遷移は初期状態から到達できる状態遷移を表す。
入力時系列は初期状態から到達できる状態までに経過する状態遷移を登録したものである（状態遷移の経路が複数とれる場合は最短経路を採用する）。
【００５８】
入力時系列の短い順番は、図３（ｃ）の入力時系列の短い方からの順番を表す。初期状態から状態▲２▼、▲４▼、▲６▼への経路はそれぞれ最短である。その次に短い経路（４番目の長さ）は状態▲５▼への遷移である。その次に短い経路（５番目の長さ）は状態▲３▼への遷移である。
【００５９】
新たに生成する入力時系列は初期状態から到達可能な状態から深さ優先探索して求めたものである。例えば、状態▲２▼から状態▲１▼への状態遷移１２を求め、新たに登録した状態遷移として登録する（入力時系列（９、１２））。同様に状態遷移▲３▼、▲４▼、▲５▼、▲６▼からの状態遷移を求め登録する。
【００６０】
図４は本発明を適用する状態図の例（その２）である。
図４（ａ）は状態図の例（その２）である。
図４（ｂ）は図４（ａ）において初期状態から到達できる経路（状態遷移）を黒丸で表したものである。
【００６１】
図４（ｃ）は、このようにして求めた状態遷移を表にしたものである。
図５は状態図の例（その３）である。
図５（ａ）は状態図の例であり、図４（ａ）の場合と状態▲５▼と状態▲８▼の間の遷移の方向が異なるのみである。
【００６２】
図５（ｂ）は初期状態から到達可能な状態の集合を示す。
図６は本発明の代表状態の説明図である。
図６（ａ）はマルチプロセッサシステムの初期状態を表す。
【００６３】
図６（ａ）において、
３０、３１、３２、３３はそれぞれｃｐｕ０、ｃｐｕ１、ｃｐｕ２、ｃｐｕ３である。
【００６４】
３５はバスである。
３４はメモリであって，共有メモリである。
初期状態において、各ｃｐｕがＩｎｖａｌｉｄであることを表す。
【００６５】
図６（ｂ）において、ｃｐｕ０の状態は（Ｃ，Ｅ，Ｍ）、ｃｐｕ１の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ２の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ３の状態は（Ｉ，Ｉ，Ｉ）である状態を表す。（Ｉ、Ｉ、Ｉ）のうち、左側のＩは１次キャッシュがＩｎｖａｌｉｄ、中央のＩは２次キャッシュがＩｎｖａｌｉｄ、右側のＩはｃｐｕ全体がＩｎｖａｌｉｄであることを表す。
【００６６】
図６（ｃ）において、ｃｐｕ０の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ１の状態は（Ｃ，Ｅ，Ｍ）、ｃｐｕ２の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ３の状態は（Ｉ，Ｉ，Ｉ）である状態を表す。Ｃはキャッシュと主記憶（メモリ）の状態が同じであることを示す。
【００６７】
図６（ｄ）において、ｃｐｕ０の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ１の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ２の状態は（Ｃ，Ｅ，Ｍ）、ｃｐｕ３の状態は（Ｉ，Ｉ，Ｉ）である状態を表す。
【００６８】
図６（ｅ）において、ｃｐｕ０の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ１の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ２の状態は（Ｉ，Ｉ，Ｉ）、ｃｐｕ３の状態は（Ｃ，Ｅ，Ｍ）である状態を表す。
【００６９】
各ｃｐｕが同一である場合には、図６（ｂ）、図６（ｃ）、図６（ｄ）、図６（ｅ）は状態の組合せが同じであり、対称性から同一の状態と見なすことができる。従って、図６（ｂ）を各状態の代表状態とし、図６（ｂ）への状態遷移のみを入力時系列として登録し、図６（ｃ）、図６（ｄ）、図６（ｅ）への状態遷移は入力時系列として省略することができる。
【００７０】
図７は代表状態による入力時系列の生成方法の説明図である。
図７において、
グループ１は“ＡＢＢＢ”、“ＢＡＢＢ”、“ＢＢＡＢ”、“ＢＢＢＡ”の状態のグループである。▲１▼はグループ１の代表状態である。
【００７１】
グループ２は“ＡＡＢＢ”、“ＡＢＡＢ”、“ＢＢＡＡ”、“ＡＢＢＡ”の状態のグループである。▲２▼はグループ２の代表状態である。
グループ３は“ＣＤＤＤ”、“ＤＣＤＤ”、“ＤＤＣＤ”、“ＤＤＤＣ”の状態のグループである。▲３▼はグループ３の代表状態である。
【００７２】
図７の状態グループにおいて、入力時系列を求める時、代表状態▲１▼から状態遷移１で代表状態▲２▼に遷移した時は状態遷移１を登録し、代表状態▲２▼から探索を継続する。
【００７３】
あるいは、代表状態▲１▼から状態遷移２でグループ２の状態▲２▼’に到達した時は、状態遷移２を登録しないでグループ１の代表状態▲１▼に戻り、代表状態▲１▼からさらに探索を続ける。
【００７４】
また、例えば、グループ１の代表状態▲１▼から  状態遷移３でグループ３の状態▲３▼’に到達したとする。この時、代表状態▲１▼から代表状態▲３▼に遷移する状態遷移が存在しなければ処理を終了する。
【００７５】
図８はバス制御するための入力時系列を生成する時のキャッシュラインの設定方法を示すものである。
ｃｐｕ０のキャッシュラインはｌｉｎｅ０、ｃｐｕ１のキャッシュラインはｌｉｎｅ１、ｃｐｕ２のキャッシュラインはｌｉｎｅ２、ｃｐｕ３のキャッシュラインはｌｉｎｅ３を設定したことを表している。
【００７６】
入力時系列の命令列のキャッシュのラインを指定するアドレスを図８のようにｃｐｕ毎に異なるようにする。そして、各プロセッサに対するテスト命令列は設定したキャッシュラインをアドレスとして入力時系列をもとに生成する。
【００７７】
図９は本発明のシステム構成の実施の形態を示す図である。
図９において、
５０はコンピュータである。
【００７８】
５１はｃｐｕである。
５２はメモリである。
５３はメモリにロードされた入力時系列生成プログラムである。
【００７９】
５４はメモリにロードされたテスト命令列生成プログラムである。
５５はメモリにロードされた有限状態機械の記述である。
５６はメモリにロードされたキャッシュラインの記述である。
【００８０】
５８は入出力インタフェースである。
６１は入力装置であって、有限状態機械を入力するキーボード、あるいは生成された有限状態機械の記述のファイルを保持している磁気ディスク装置等の記憶装置である。
【００８１】
６２は有限状態機械の記述を表す。
６５はドライブ装置であって、記憶媒体７０に記憶されている内容をメモリ５２にロードするものである。
【００８２】
７０は記憶媒体であって、入力時系列生成プログラム、テスト命令列生成プログラムを記憶しているものである。
７１は入力時系列生成プログラムであって、有限状態機械の記述に基づいて、入力時系列を生成するプログラムである。
【００８３】
７２はテスト命令列生成プログラムであって、入力時系列をもとにバス制御を検証するための命令列を生成するものである。
図９の構成において、入力時系列を生成する時は、記憶媒体７０の入力時系列生成プログラム７１をコンピュータ５０のメモリ５２にロードする。また、有限状態機械の記述をメモリ５２にロードする。そして、入力時系列生成プログラム５３と有限状態機械の記述５３により入力時系列を生成する。生成された入力時系列は出力装置７５に出力され、磁気ディスク等に保持される。
【００８４】
また、入力時系列をもとにバス制御のテスト命令列を生成するプログラムを記憶媒体７０からメモリ５２にロードする。そして、キャッシュのラインを指定するデータを入力装置６１を使用して入力し、生成された入力時系列をもとにテスト命令列を生成し、出力装置７５に出力して保持する。そして、そのテスト命令列をバス制御検証シミュレータ（図示せず）に入力することによりバス制御を検証する。
【００８５】
図１０は本発明の実施の形態１であって、フローチャートで表したものである。
図示のステップの番号に従って実施の形態１の動作を説明する。
【００８６】
Ｓ１  有限状態機械の記述を入力する。また、入力時系列の長さの範囲を指定する。
Ｓ２  手続きの全体の部分の処理である。
【００８７】
Ｓ３  手続きの前処理の部分である。有限状態機械の記述に基づいて到達可能な状態を生成する。そして、到達可能な状態に到る状態遷移の入力時系列を生成する。その入力時系列を過去に網羅した状態遷移として登録する。
【００８８】
Ｓ４は手続きの本体部であり、深さ優先探索に関する処理である。
Ｓ１１  入力時系列を選択できたか判定する。選択できればＳ１２の処理を行ない、選択できなければＳ１８の処理を行なう。
【００８９】
Ｓ１２  到達先の状態から過去に網羅していない状態遷移を抽出する。
Ｓ１３  状態遷移を選択できるか判定する。選択できればＳ１４の処理を行ない、選択できなければＳ１１以降の処理を繰り返す。
【００９０】
Ｓ１４  深さ優先探索により指定した長さの範囲内で過去に網羅していない状態遷移の探索をする。
Ｓ１５  深さ優先探索中に指定した長さの範囲を超えるか判定する。超えればＳ１６の処理をする。超えなければＳ１７の処理をする。
【００９１】
Ｓ１６  深さ優先探索中に指定した長さの範囲を超えれば、その時点で深さ優先探索を中止する。
Ｓ１７  新たに探索し状態遷移列に対して、過去に網羅した状態遷移列として登録する。元の入力時系列に追加し、新たな入力時系列を生成する。新たな入力時系列を出力する入力時系列の集合に登録する。
【００９２】
Ｓ１８  初期状態から遷移可能な全ての状態遷移を網羅する入力時系列集合を出力する。
次に実施の形態１の記述の例を示すが、そこで使用する関数について図５を参照して説明する。
【００９３】
（１）  ｒｅａｃｈａｂｌｅ＿ｓｔａｔｅ：初期状態をＰとすると、ｒｅａｃｈａｂｌｅ＿ｓｔａｔｅ（Ｐ）として状態集合（１、２、３、４、５、６、７）を返す。
【００９４】
（２）  ｒａｎｄａｍ＿ｓｔａｔｅ：到達可能な状態をＰとすると、ｒａｎｄａｍ＿ｓｔａｔｅ（Ｐ）として状態３を返す。
（３）  ｆｉｎｄ＿ｓｅｑｕｅｎｃｅ：到達した状態を（４）とすると、ｆｉｎｄ＿ｓｅｑｕｅｎｃｅ（４）として状態遷移列（２、６、５）を返す。
【００９５】
（４）  ｓｅｌｅｃｔ＿ｆｉｎｄ＿ｓｅｑｕｅｎｃｅ：到達可能な入力時系列の集合Ｓ＝｛（１）、（２）、（１、３）、・・・・、（１、７、８、３、６、５）｝とすると、ｓｅｌｅｃｔ＿ｆｉｎｄ＿ｓｅｑｕｅｎｃｅ（Ｓ）としては入力時系列（１）を返す（集合Ｓのどれか１つの要素）。
【００９６】
（５）  ｆｉｎｄ＿ｓｔａｔｅ：入力時系列ｑ＝（１、３、６、５）とすると、ｆｉｎｄ＿ｓｔａｔｅ（ｑ）として状態４を返す。
（６）  ｆｉｎｄ＿ｔｒａｎｓｉｔｉｏｎ：状態３に対して、ｆｉｎｄ＿ｔｒａｎｓｉｔｉｏｎ（３）とすると、状態遷移の集合Ｗ＝（６、９）を返す。
【００９７】
（７）  ｒａｎｄａｍ＿ｔｒａｎｓｉｔｉｏｎ：上記のＷに対して、ｒａｎｄａｍ＿ｔｒａｎｓｉｔｉｏｎ（Ｗ）とすると、状態遷移９（ランダムに選択された１つ）を返す。
【００９８】
（８）  ａｄｄ＿ｔｒａｎｓｉｔｉｏｎ：入力時系列ｑ＝（２、９、１１）に対して、付加したい状態遷移をｔ＝８とすると、ａｄｄ＿ｔｒａｎｓｉｔｉｏｎ（ｑ、ｔ）は（２、９、１１、８）を返す。
【００９９】
（９）  ｆｉｎｄ＿ｎｅａｒｅｓｔ＿ｔｒａｎｓｉｔｉｏｎ：この関数に対しては、図４を参照して説明する。状態ｐ＝５と状態遷移の集合Ｗ＝（１、２、６、７、９、１０）（図４（ｂ）の黒丸の状態遷移）に対して、ｆｉｎｄ＿ｎｅａｒｅｓｔ＿ｔｒａｎｓｉｔｉｏｎ（ｐ、Ｗ）として入力時系列（５、４）を返す（状態５からの状態遷移の経路のうち、求められていない最も近い状態遷移を含むもの）。
（１１）  ｓｅｌｅｃｔ＿ｌａｓｔ＿ｅｌｅｍｅｎｔ：入力時系列ｑ＝（２、９、１１）に対して、ｓｅｌｅｃｔ＿ｌａｓｔ＿ｅｌｅｍｅｎｔ（ｑ）として状態（１１）を返す。
（１２）  ｇｒｏｕｐ＿ｏｆ＿ｒｅｐｒｅｓｅｎｔ＿ｓｔａｔｅ：この関数に対しては図６を参照する。ｇｒｏｕｐ＿ｏｆ＿ｒｅｐｒｅｓｅｎｔ＿ｓｔａｔｅは代表状態の集合を表す。
【０１００】
本発明の実施の形態１のプログラムの記述の例を次に示す。
生成する入力時系列の長さの下限をｌｅｎｇｔｈlow 、上限をｌｅｎｇｔｈhighとする。
【０１０１】
0003718049.tif 000002
0003718049.tif 000003
0003718049.tif 000004
【０１０２】
0003718049.tif 000005
図１１は本発明の実施の形態２であって、フローチャートで表したものである。
【０１０３】
本発明の実施の形態２は、深さ優先探索において、すでに求められている状態遷移が見つかった時は探索を終了するようにしたものである。
例えば、図４で初期状態▲１▼から状態▲７▼へ到達する状態遷移列は（２、９）が求まっている。また、初期状態▲１▼から状態前へ到達する状態遷移列は（２、６）が求まっている。この状態において、状態▲２▼から深さ優先探索する時、状態遷移３が求まる。そして、さらに深さ優先探索すると、状態遷移９が求まる。状態遷移９は求まっているが状態▲７▼から状態▲６▼へ状態遷移１１は過去に求められていない。そこで、状態遷移の系列１−３−９−１１を登録する。このとき、状態遷移の系列１−３−９−１１が指定した深さの範囲内ですでに過去において求まっている時は、探索を終了する。
【０１０４】
図１１のフローチャートは、Ｓ１５で深さ優先探索により指定した長さの範囲を超えなければ、Ｓ１７で探索不可能状態（その先の状態遷移がすでに求められている）に対して最短の入力時系列により過去に網羅していない状態遷移を探索できるか判定し、できればＳ１４以降の深さ優先探索を継続する（その状態からの深さ優先探索で、指定した深さで範囲内で新しい経路が探索できる時、深さ優先探索を継続する）。最短の入力時系列により過去に網羅していない状態遷移を探索できなければ、Ｓ１８で新たな状態遷移列に対して過去に網羅した状態遷移に登録する。さらに、元の入力時系列に追加し、新たな入力時系列を生成する。また、新たな入力時系列を出力する集合に追加する（Ｓ１９）。
【０１０５】
図１１のフローチャートは、上記の点で図１０の本発明の実施の形態２のフローチャートと異なるのみである。
本発明の実施の形態２のプログラムの記述の例を次に示す。
【０１０６】
生成する入力時系列の長さの下限をｌｅｎｇｔｈlow 、上限をｌｅｎｇｔｈhighとする。
0003718049.tif 000006
0003718049.tif 000007
0003718049.tif 000008
0003718049.tif 000009
図１２は本発明の実施の形態３のフローチャートである。
【０１０７】
本発明の実施の形態３は代表状態により入力時系列を求めるものである。代表状態により入力時系列を求める方法は図６と図７で説明した通りである。
図１２のフローチャートにおいて、Ｓ１、Ｓ２、Ｓ１１、Ｓ１２、Ｓ１３までの処理は図１０のフローチャートと同様である。Ｓ１３以降が代表状態を求めて深さ優先探索をする処理である。
【０１０８】
Ｓ１  有限状態機械の記述を入力する。また、入力時系列の長さの範囲を指定する。
Ｓ２  手続きの全体の部分である。
【０１０９】
Ｓ３  手続きの前処理の部分である。有限状態機械の記述に基づいて到達可能な状態を生成する。そして、到達可能な状態に到る入力時系列を生成する。その入力時系列を過去に網羅した状態遷移として登録する。代表状態を抽出する。
【０１１０】
Ｓ４は手続きの本体部であり、深さ優先探索の処理である。代表状態を抽出する。
Ｓ１１  入力時系列を選択できたと判定する。選択できればＳ１２の処理を行ない、選択できなければＳ２２の処理を行なう。
【０１１１】
Ｓ１２  到達先の状態から過去に網羅していない状態遷移を抽出する。
Ｓ１３  過去に網羅していない状態遷移を選択できるか判定する。選択できればＳ１４の処理を行ない、選択できなければＳ１１以降の処理を行なう。
【０１１２】
Ｓ１４  深さ優先探索中に指定した長さの範囲を超えるか判定する。超えればＳ１５の処理をする。超えなければＳ１６の処理をする。
Ｓ１５  この時点で深さ優先探索を中止する。
【０１１３】
Ｓ１６  到達先の状態が代表状態か判定する。代表状態であればＳ１７の処理を行ない、代表状態でなければＳ１８の処理を行なう。
Ｓ１７  到達先の状態に進む。
【０１１４】
Ｓ１８  遷移前の状態から到達先の状態が含まれるグループの代表状態への遷移が存在するか判定する。代表状態への遷移が存在すればＳ１９の処理を行なう。代表状態への遷移が存在しなければＳ２０の処理を行なう。
【０１１５】
Ｓ１９  遷移前の状態に戻る。
Ｓ２０  新たな状態遷移列に対して過去に網羅した状態遷移に登録する。さらに、元の入力時系列に追加し、新たな入力時系列を生成する。また、新たな入力時系列を出力となる集合に追加する。
【０１１６】
Ｓ２１  元の入力時系列の到達先の状態に戻る。
Ｓ２２  初期状態から遷移可能な全ての状態遷移を網羅する入力する時系列集合を出力する。
【０１１７】
本発明の実施の形態３のプログラムの記述の例を次に示す。
生成する入力時系列の長さの下限をｌｅｎｇｔｈlow 、上限をｌｅｎｇｔｈhighとする。
【０１１８】
0003718049.tif 000010
0003718049.tif 000011
0003718049.tif 000012
0003718049.tif 000013
図１３は本発明の実施の形態４であって、フローチャートで表したものである。
【０１１９】
本発明の実施の形態４は、入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、マルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力するものである。
【０１２０】
Ｓ１で入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、Ｓ２ないしＳ１７でその入力時系列の集合を生成し、Ｓ１８でマルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力する。それ以外は、図１０のフローチャートと同様である。
【０１２１】
図１４は本発明の実施の形態５であって、フローチャートで表したものである。
本発明の実施の形態５は、入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、マルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力するものである。
【０１２２】
Ｓ１で入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、Ｓ２ないしＳ１８でその入力時系列の集合を生成する。Ｓ１９でマルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力する。それ以外は、図１１のフローチャートと同様である。
【０１２３】
図１５は本発明の実施の形態６であって、フローチャートで表したものである。
本発明の実施の形態６は、入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、マルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力するものである。
【０１２４】
Ｓ１で入力時系列を生成するための入力として、マルチプロセッサにおける全てのキャッシュの動作を表す有限状態機械の記述を入力する。そして、Ｓ２ないしＳ２１でその入力時系列を生成する。Ｓ２２でマルチプロセッサのキャッシュコヒーレンシーを完全に検証することのできる入力時系列の集合を出力する。それ以外は、図１２のフローチャートと同様である。
【０１２５】
図１６は本発明の実施の形態７のフローチャートであって、上記の実施の形態１ないし実施の形態６で求めた入力時系列をもとにして、さらにマルチプロセッサのバス制御のためのテスト命令列を生成するものである。
【０１２６】
その手順は次の通りである。
（ａ）  キャッシュの状態集合を全て網羅するｎ個の入力時系列の集合｛σ1 ，σ2 ，・・・，σn ｝を生成する。この入力時系列は前述の実施の形態の方法により生成する。
【０１２７】
（ｂ）  各マルチプロセッサのキャッシュのラインを設定する（各マルチプロセッサにおいて異なるようにする）。
（ｃ）  生成した入力時系列集合に対して、プロセッサ番号（１，２，３，４）を付加した次の入力時系列を集合を生成する。
【０１２８】
｛σ11，σ12，・・・，σ1n｝（プロセッサ０に対して）
｛σ21，σ22，・・・，σ2n｝（プロセッサ１に対して）
｛σ31，σ32，・・・，σ3n｝（プロセッサ２に対して）
｛σ41，σ42，・・・，σ4n｝（プロセッサ３に対して）
（ｄ）  （ｃ）で求めた入力時系列をある基準（後述する）に従って
並べ換える。
｛σ1a1(1)  ，σ1a1(2)  ，・・・，σ1a1(n)  ｝（プロセッサ０に対して）
｛σ2a2(1)  ，σ2a2(2)  ，・・・，σ2a2(n)  ｝（プロセッサ１に対して）
｛σ3a3(1)  ，σ3a3(2)  ，・・・，σ3a3(n)  ｝（プロセッサ２に対して）
｛σ4a4(1)  ，σ4a4(2)  ，・・・，σ4a4(n)  ｝（プロセッサ３に対して）
｛σ4a4(1)  ，σ4a4(2)  ，・・・，σ4a4(n)  ｝（プロセッサ３に対して）
（プロセッサがｍ個あるとき、ｍ番目のプロセッサに対しては｛σmam(1)  ，σmam(2)  ，・・・，σmam(n)  ｝）
（ｅ）  （ｄ）で求めた入力時系列をもとにして、それぞれのプロセッサで実行するテスト命令列を生成する。
【０１２９】
そして、その命令列をバス制御を検証するためのテストシミュレーターに入力し、バス制御の検証をする。
（ｆ）  シミュレータ（図示せず）において、プロセッサ番号ｉ（１≦ｉ≦ｍ）は入力時系列｛σiai(1)  ，σiai(2)  ，・・・，σiai(n)  ｝を実行する）。但し、入力時系列を実行する度に各々のプロセッサで同期を取る。
【０１３０】
プロセッサが４つの時、
プロセッサ０は｛σ1a1(1)  ，σ1a1(2)  ，・・・，σ1a1(n)  ｝を実行する。
【０１３１】
プロセッサ１は｛σ2a2(1)  ，σ2a2(2)  ，・・・，σ2a2(n)  ｝を実行する。
プロセッサ２は｛σ3a3(1)  ，σ3a3(2)  ，・・・，σ3a3(n)  ｝を実行する。
【０１３２】
プロセッサ３は｛σ4a4(1)  ，σ4a4(2)  ，・・・，σ4a4(n)  ｝を実行する。
バス制御のテストシミュレータにおいて、それぞれの入力時系列（テスト命令列）を実行する時、次のようにして同期をとる。
【０１３３】
ｉ．各々のプロセッサは、同期を取って一斉に｛σ1a1(1)  ，σ2a2(1)  ，σ3a3(1)  ，σ4a4(1)  ｝を実行する。
ii. 各々のプロセッサは、入力時系列の実行が終了したら一旦停止する。
【０１３４】
iii ．各々のプロセッサは、同期を取って一斉に｛σ1a1(2)  ，σ2a2(1)  ，σ3a3(2)  ，σ4a4(2)  ｝を実行する。
iv. この操作をｎ回繰り返す。
【０１３５】
図１６の本発明の実施の形態７のフローチャートを説明する。
Ｓ１  マルチプロセッサの有限状態機械の記述に基づいて入力時系列を生成する（上記の（ａ））。
【０１３６】
Ｓ２  各マルチプロセッサのキャッシュラインを特定する（マルチプロセッサ毎に異なるキャッシュラインを生成する上記の（ｂ））。
Ｓ３  各々のプロセッサに対する入力時系列集合を生成する（上記の（ｃ））。
【０１３７】
Ｓ４  各々のプロセッサに対する入力時系列集合に基づいて新たな入力時系列を生成する（上記の（ｄ））。
Ｓ５  各々のプロセッサに対するテスト命令列を生成する（上記の（ｅ））。
【０１３８】
Ｓ６  テストシミュレータにおいて各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は入力時系列（テスト命令列とされている）｛σiai(1)  ，σiai(2)  ，・・・，σiai(n)  ｝を実行する。但し、入力時系列を実行する度に各々のプロセッサで同期を取る（上記の（ｆ））。
【０１３９】
図１７は本発明の実施の形態８であって、フローチャートで表したものである。
本発明の実施の形態８は、実施の形態７において入力時系列の入れ換えを次のようにしたものである。
【０１４０】
（ａ）、（ｂ）、（ｃ）は上記と同様である。
（ｄ）  上記（ｃ）で求めたプロセッサ番号（１，２，３，４）を付加した次のｎ個の入力時系列
｛σ11，σ12，・・・，σ1n｝（プロセッサ０に対して）
｛σ21，σ22，・・・，σ2n｝（プロセッサ１に対して）
｛σ31，σ32，・・・，σ3n｝（プロセッサ２に対して）
｛σ41，σ42，・・・，σ4n｝（プロセッサ３に対して）
をｋ個のグルーブに分類して、ｋ個のグループを並べ換える。
0003718049.tif 000014
（ｅ）  （ｄ）で求めた入力時系列をもとにして、各プロセッサで実行するテスト命令列を生成する。
【０１４１】
（ｆ）  各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は、１番目のグループ
｛σiai1(1)   ，σiai1(2)   ，・・・，σiai1(n) ｝の全ての入力時系列（テスト命令列）を任意の順番で実行する。２、３、・・・、ｋ番目のグループも同様に行なう。
【０１４２】
プロセッサが４個の時、
プロセッサ０は１番目のグループ｛σ1a11(1)   ，σ1a11(2)   ，・・・，σ1a11(n)   ・・・ ｝の全ての時系列を任意の順番で実行する。
【０１４３】
プロセッサ１は１番目のグループ｛σ2a21(1)   ，σ2a21(2)   ，・・・，σ2a21(n) ｝の全てを任意の順番で実行する。
プロセッサ２は１番目のグループ｛σ3a31(1)   ，σ3a31(2)   ，・・・，σ3a31(n) ｝の全てを任意の順番で実行する。
プロセッサ３は１番目のグループ｛σ4a41(1)   ，σ4a41(2)   ，・・・，σ4a41(n) ｝の全てを任意の順番で実行する。
【０１４４】
但し、各々のプロセッサは、入力時系列を実行する度に同期を取る。
（ｇ）  ２、３、・・・、ｋ番目のグループに対しても、同様のことを行なう。
【０１４５】
図１７の本発明の実施の形態８のフローチャートを説明する。
Ｓ１  マルチプロセッサの有限状態機械の記述に基づいて入力時系列を生成する（上記の（ａ））。
【０１４６】
Ｓ２  各マルチプロセッサのキャッシュラインを特定する（マルチプロセッサごとに異なるキャッシュラインを生成する上記の（ｂ））。
Ｓ３  各々のプロセッサに対する入力時系列集合を生成する（上記の（ｃ））。
【０１４７】
Ｓ４  各々のプロセッサに対する入力時系列集合に基づいて新たな入力時系列集合を生成する（上記の（ｄ））。
Ｓ５  各々のプロセッサに対するテスト命令列を生成する（上記の（ｅ））。
【０１４８】
Ｓ６  テストシミュレータにおいて各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は１番目のグルーブσiai1(1),σIai1(2),・・・・の全ての入力時系列を任意の順番で実行する。２，３・・・，ｋ番目のグループも同様に行う。その時、各プロセッサで同期を取る（上記の（ｆ））。
【０１４９】
図１８は本発明の実施の形態９であって、フローチャートで表したものである。
本発明の実施の形態９は各々入力時系列を長さの短い順に並べ換えるものである。
（ａ）、（ｂ）、（ｃ）は上記と同様である。
【０１５０】
（ｄ）  上記（ｃ）で求めたプロセッサ番号（１，２，３，４）を付加した次のｎ個の入力時系列
｛σ11，σ12，・・・，σ1n｝（プロセッサ０に対して）
｛σ21，σ22，・・・，σ2n｝（プロセッサ１に対して）
｛σ31，σ32，・・・，σ3n｝（プロセッサ２に対して）
｛σ41，σ42，・・・，σ4n｝（プロセッサ３に対して）
を入力時系列の長さの短い順に入力時系列を並べ換える。
【０１５１】
｛σ1a1(1)  ，σ1a1(2)  ，・・・，σ1a1(n)  ｝，
｛σ1a2(1)  ，σ1a2(2)  ，・・・，σ1a2(n)  ｝，
｛σ1a3(1)  ，σ1a3(2)  ，・・・，σ1a3(n)  ｝，
｛σ1a4(1)  ，σ1a4(2)  ，・・・，σ1a4(n)  ｝，
（ｅ）（ｄ）で求めた入力時系列をもとにして、各プロセッサで実行するテスト命令列を生成する。
【０１５２】
（ｆ）各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は、入力時系列（テスト命令列）σiai1(1)   ，σiai1(2)   ，・・・を順番に実行する。但し、入力時系列を実行する度に各々のプロセッサの同期を取る。
【０１５３】
プロセッサが４個の時、
プロセッサ０は｛σ1a1(1)，σ1a1(2)，・・・，σ1a1(n)｝を順番に実行する。
【０１５４】
プロセッサ１は｛σ2a2(1)，σ2a2(2)，・・・，σ2a2(n)｝を順番に実行する。
プロセッサ２は｛σ3a3(1)，σ3a3(2)，・・・，σ3a(n) ｝を実行する。
【０１５５】
プロセッサ３は｛σ4a4(1)，σ4a4(2)，・・・，σ4a(n) ｝を実行する。
但し、各々のプロセッサは、入力時系列を実行する度に同期を取る。
ｉ．各々のプロセッサは、同期を取って一斉に｛σ1a1(1)  ，σ2a2(1)  ，σ3a3(1)  ，σ4a4(1)  ｝を実行する。
【０１５６】
ii. 各々のプロセッサは、入力時系列の実行が終了したら一旦停止する。
iii ．各々のプロセッサは、同期を取って一斉に｛σ1a1(2)  ，σ2a2(1)  ，σ3a3(2)  ，σ4a4(2)  ｝を実行する。
【０１５７】
iv. この操作をｎ回繰り返す。
図１８の本発明の実施の形態９のフローチャートを説明する。
Ｓ１  マルチプロセッサの有限状態機械の記述に基づいて入力時系列を生成する（上記の（ａ））。
【０１５８】
Ｓ２  各マルチプロセッサのキャッシュラインを特定する（マルチプロセッサごとに異なるキャッシュラインを生成する上記の（ｂ））。
Ｓ３  各々のプロセッサに対する入力時系列集合を生成する（上記の（ｃ））。
【０１５９】
Ｓ４  各々のプロセッサに対する入力時系列集合に対して，入力時系列の長さの短い順に入力時系列を並べ換えて，新たな入力時系列を生成する（上記の（ｄ））。
【０１６０】
Ｓ５  各々のプロセッサに対するテスト命令列を生成する（上記の（ｅ））。Ｓ６  テストシミュレータにおいて各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は入力時系列σiai(1), σiai(2), ・・・を実行する。但し、実行する度に、各プロセッサで同期を取る（上記の（ｆ））。
【０１６１】
図１９は本発明の実施の形態１０であって、フローチャートで表したものである。
本発明の実施の形態１０は各々の入力時系列集合の入力時系列をランダムに並べ換えるものである。
【０１６２】
（ａ）、（ｂ）、（ｃ）は上記と同様である。
（ｄ）  上記（ｃ）で求めたプロセッサ番号（１，２，３，４）を付加した次のｎ個の入力時系列
｛σ11，σ12，・・・，σ1n｝（プロセッサ０に対して）
｛σ21，σ22，・・・，σ2n｝（プロセッサ１に対して）
｛σ31，σ32，・・・，σ3n｝（プロセッサ２に対して）
｛σ41，σ42，・・・，σ4n｝（プロセッサ３に対して）
をランダムに並べ換える。
【０１６３】
｛σ1a1(1)  ，σ1a1(2)  ，・・・，σ1a1(n)  ｝，
｛σ1a2(1)  ，σ1a2(2)  ，・・・，σ1a2(n)  ｝，
｛σ1a3(1)  ，σ1a3(2)  ，・・・，σ1a3(n)  ｝，
｛σ1a4(1)  ，σ1a4(2)  ，・・・，σ1a4(n)  ｝，
（ｅ）（ｄ）で求めた入力時系列をもとにして、各プロセッサで実行するテスト命令列を生成する。
【０１６４】
（ｆ）各々のプロセッサは入力時系列を順番に実行する。
プロセッサ０は｛σ1a1(1)，σ1a1(2)，・・・，σ1a1(n)｝を順番に実行する。
【０１６５】
プロセッサ１は｛σ2a2(1)，σ2a2(2)，・・・，σ2a2(n)｝を順番に実行する。
プロセッサ２は｛σ3a3(1)，σ3a3(2)，・・・，σ3a(n) ｝を実行する。
【０１６６】
プロセッサ３は｛σ4a4(1)，σ4a4(2)，・・・，σ4a(n) ｝を実行する。
但し、各々のプロセッサは、入力時系列を実行する度に同期を取る。
ｉ．各々のプロセッサは、同期を取って一斉に｛σ1a1(1)  ，σ2a2(1)  ，σ3a3(1)  ，σ4a4(1)  ｝を実行する。
【０１６７】
ii. 各々のプロセッサは、入力時系列の実行が終了したら一旦停止する。
iii ．各々のプロセッサは、同期を取って一斉に｛σ1a1(2)  ，σ2a2(1)  ，σ3a3(2)  ，σ4a4(2)  ｝を実行する。
【０１６８】
iv. この操作をｎ回繰り返す。
図１９の実施の形態１０のフローチャートを説明する。
Ｓ１  マルチプロセッサの有限状態機械の記述に基づいて入力時系列を生成する（上記の（ａ））。
【０１６９】
Ｓ２  各マルチプロセッサのキャッシュラインを特定する（マルチプロセッサごとに異なるキャッシュラインを生成する上記の（ｂ））。
Ｓ３  各々のプロセッサに対する入力時系列集合を生成する（上記の（ｃ））。
【０１７０】
Ｓ４  各々のプロセッサに対する入力時系列集合に対して，入力時系列をランダムに並べ換え，新たな入力時系列を生成する（上記の（ｄ））。
Ｓ５  各々のプロセッサに対するテスト命令列を生成する（上記の（ｅ））。Ｓ６  テストシミュレータにおいて各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は、入力時系列σiai(1), σiai(2), ・・・を順番に実行する。但し、入力時系列を実行する度に各プロセッサで同期を取る（上記の（ｆ））。
【０１７１】
図２０は本発明の実施の形態１１であって、フローチャートで表したものである。
本発明の実施の形態は，ｋ個のグルーブに分類して、ｋ個のグループを並べ換える。そして，入力時系列を長さの等しい入力時系列を１つのグループにしてｋ個のグループに分類する。そして、グループ内の入力時系列を任意の順番で並べ換え、グループは長さの順番に並べ換えたものである。
（ｄ）  上記（ｃ）で求めたプロセッサ番号（１，２，３，４）を付加した次のｎ個の入力時系列
｛σ11，σ12，・・・，σ1n｝（プロセッサ０に対して）
｛σ21，σ22，・・・，σ2n｝（プロセッサ１に対して）
｛σ31，σ32，・・・，σ3n｝（プロセッサ２に対して）
｛σ41，σ42，・・・，σ4n｝（プロセッサ３に対して）
をｋ個のグルーブに分類して、ｋ個のグループを並べ換える。さらに，入力時系列を長さの等しい入力時系列を１つのグループににしてｋ個のグループに分類する。そして、グループ内の入力時系列を任意の順番で並べ換え、グループは長さの順番に並べ換える。
0003718049.tif 000015
（ｅ）（ｄ）で求めた入力時系列をもとにして、各プロセッサで実行するテスト命令列を生成する。
【０１７２】
（ｆ）各々のプロセッサ番号ｉ（１≦ｉ≦ｍ）は、１番目のグループ｛σiai(1)  ，σiai(2)  ，・・・，σiai(n)  ｝の全ての入力時系列を任意の順番で実行する。
【０１７３】
プロセッサが４個の時、
プロセッサ０は１番目のグループ｛σ1a11(1)   ，σ1a11(2)   ，・・・，σ1a11(n) ｝の全てを任意の順番で実行する。
プロセッサ１は１番目のグループ｛σ2a21(1)   ，σ2a21(2)   ，・・・，σ2a21(n) ｝の全てを任意の順番で実行する。
プロセッサ２は１番目のグループ｛σ3a31(1)   ，σ3a31(2)   ，・・・，σ3a31(n) ｝の全てを任意の順番で実行する。
プロセッサ３は１番目のグループ｛σ4a41(1)   ，σ4a41(2)   ，・・・，σ4a41(n) ｝の全てを任意の順番で実行する。
【０１７４】
但し、各々のプロセッサは、入力時系列を実行する度に同期を取る。
（ｇ）  ２、３、・・・、ｋ番目のグループに対しても、同様のことを行なう。
【０１７５】
図２０の本発明の実施の形態８のフローチャートを説明する。
Ｓ１  マルチプロセッサの有限状態機械の記述に基づいて入力時系列を生成する（上記の（ａ））。
【０１７６】
Ｓ２  各マルチプロセッサのキャッシュラインを特定する（マルチプロセッサごとに異なるキャッシュラインを生成する上記の（ｂ））。
Ｓ３  各々のプロセッサに対する入力時系列集合を生成する（上記の（ｃ））。
【０１７７】
Ｓ４  各々のプロセッサに対するｎ個の入力時系列集合に基づいて，入力時系列をｋ個のグルーブに分類して、ｋ個のグループを並べ換える。さらに，入力時系列を長さの等しい入力時系列を１つのグループににしてｋ個のグループに分類する。そして、グループ内の入力時系列を任意の順番で並べ換え、グループは長さの順番に並べ換えて，新たな入力時系列を生成する（上記の（ｄ））。
【０１７８】
Ｓ５  各々のプロセッサに対するテスト命令列を生成する（上記の（ｅ））。Ｓ６  テストシミュレータにおいて各々のプロセッサ番号ｉ番目（１≦ｉ≦ｍ）は１番目のグルーブσiai1(1),σIai1(2),・・・・の全ての入力時系列を任意の順番で実行する。２，３・・・，ｋ番目のグループも同様に行う。その時、各プロセッサで同期を取る（上記の（ｆ））。
【０１７９】
【発明の効果】
本発明によれば、ハードウェア記述言語を用いて検証しようとする機能の動作を記述することにより、全ての状態を網羅する入力時系列を容易に生成することができる。また、求めた入力時系列に基づいて、自動的に論理シミュレーション用テスト命令列を生成できる。そのため、論理検証用テスト命令列のコストが削減できる。また，設計の誤りを早期に発見することができ，信頼性の高い論理検証を行うことができる。
【０１８０】
また、本発明をマルチプロセッサシステムに適用した場合、マルチプロセッサが全て同じ場合、その対称性を利用して冗長性を最小限に抑えて能率的に入力時系列を生成できる。
【０１８１】
さらに、本発明をバス制御の検証に適用すれば、バス上に多数の複雑な競合を長時間発生させることのできるテスト命令列を容易に生成することができる。そのため、バス制御の論理検証の信頼性を大幅に向上させることができる。
【０１８２】
また、論理シミュレーションにおいて、各々のプロセッサが入力時系列を実行する際に、他のプロセッサの実行結果に影響を及ぼさないので、実行結果が一意になり、正確なテスト結果を得ることができる。
【図面の簡単な説明】
【図１】  本発明の基本構成を示す図である。
【図２】本発明の有限状態機械を示す図である。
【図３】本発明を適用する状態図の例（その１）を示す図である。
【図４】本発明を適用する状態図の例（その２）を示す図である。
【図５】本発明を適用する状態図の例（その３）を示す図である。
【図６】本発明の代表状態の説明図である。
【図７】本発明の代表状態による入力時系列の生成方法の説明図である。
【図８】本発明のバス制御を検証する入力時系列の生成方法の説明図である。
【図９】本発明のシステム構成の実施の形態を示す図である。
【図１０】本発明の実施の形態１を示す図である。
【図１１】本発明の実施の形態２を示す図である。
【図１２】本発明の実施の形態３を示す図である。
【図１３】本発明の実施の形態４を示す図である。
【図１４】本発明の実施の形態５を示す図である。
【図１５】本発明の実施の形態６を示す図である。
【図１６】本発明の実施の形態７を示す図である。
【図１７】本発明の実施の形態８を示す図である。
【図１８】本発明の実施の形態９を示す図である。
【図１９】本発明の実施の形態１０を示す図である。
【図２０】本発明の実施の形態１１示す図である。
【符号の説明】
１：入力装置
２：到達可能状態生成手段
３：入力時系列生成手段
４：深さ優先探索手段
５：入力時系列登録手段
６：出力装置
【図１】
0003718049.tif 000016
【図２】
0003718049.tif 000017
【図３】
0003718049.tif 000018
【図４】
0003718049.tif 000019
【図５】
0003718049.tif 000020
【図６】
0003718049.tif 000021
【図７】
0003718049.tif 000022
【図８】
0003718049.tif 000023
【図９】
0003718049.tif 000024
【図１０】
0003718049.tif 000025
【図１１】
0003718049.tif 000026
【図１２】
0003718049.tif 000027
【図１３】
0003718049.tif 000028
【図１４】
0003718049.tif 000029
【図１５】
0003718049.tif 000030
【図１６】
0003718049.tif 000031
【図１７】
0003718049.tif 000032
【図１８】
0003718049.tif 000033
【図１９】
0003718049.tif 000034
【図２０】
0003718049.tif 000035