(57)【要約】【課題】時系列信号値データから人手を介すことなく自動的に動作命題を作成するシステム、及び論理回路の検証前に動作命題を検証することが可能な動作命題を検証するシステムを提供する。【解決手段】時系列信号値データ１を与えられ複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段２、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報３と信号値遷移情報とに基づいてあるクロックサイクルにおける信号値と当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段４、共通データベースに基づいて同時刻に活性状態にならない複数の信号の組み合わせである同時非活性信号を抽出する同時非活性信号抽出手段５Ａ、抽出された同時非活性信号に基づいて動作命題を生成して出力する動作命題出力手段６を備える。【選択図】図１
2008097504.tif 000002
【特許請求の範囲】
【請求項１】
時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、
回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、
前記共通データベースに基づいて、同時刻に活性状態にならない複数の信号の組み合わせである同時非活性信号を抽出する同時非活性信号抽出手段と、
抽出された前記同時非活性信号に基づいて、動作命題を生成して出力する動作命題出力手段と、
を備えることを特徴とする動作命題の生成システム。
【請求項２】
時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、
回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、
前記共通データベースに基づいて、クロックサイクル単位で変化する前記信号値の遷移の規則性を抽出する信号遷移規則性抽出手段と、
抽出された前記信号値の遷移の規則性に基づいて、動作命題を生成して出力する動作命題出力手段と、
を備えることを特徴とする動作命題の生成システム。
【請求項３】
時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、
回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、
動作命題を与えられ、前記動作命題に含まれる所定の条件を満たす状態を示す信号値遷移情報を抽出する遷移情報抽出手段と、
前記共通データベースに基づく信号値遷移情報と、前記信号値抽出手段により抽出された前記信号値遷移情報とを比較し、整合性の有無を判定する動作命題解析手段と、
前記動作命題解析手段により整合性がないと判断された場合、前記動作命題の修正を指示する動作命題修正手段と、
を備えることを特徴とする動作命題の検証システム。
【請求項４】
時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、
回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、
検証対象の論理回路を読み込み、信号値遷移情報を抽出する論理回路状態遷移抽出手段と、
前記共通データベースに含まれる信号値遷移情報と、前記論理回路状態遷移抽出手段により抽出された前記信号値遷移情報とを比較する遷移情報比較手段と、
前記遷移情報比較手段により、前記共通データベースに含まれる信号値遷移情報が正しいと判定された場合、前記論理回路に含まれる不整合に関する情報を出力する遷移情報不整合情報出力手段と、
前記遷移情報比較手段により、前記論理回路状態遷移抽出手段により抽出された前記信号値遷移情報が正しいと判定された場合、前記時系列信号値データに追加すべき追加時系列信号値データを出力する時系列信号値データ出力手段と、
を備えることを特徴とする動作命題の検証システム。
【請求項５】
時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、
回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、
前記共通データベースから信号値遷移情報を抽出し、各クロックサイクル毎の信号値に無効な状態が存在するか否かに基づいて前記共通データベースの妥当性を検査する妥当性検査手段と、
前記妥当性検査手段による検査結果に基づき、前記時系列信号値データを修正すべき場合、警報を出力する警報出力手段と、
を備えることを特徴とする動作命題の検証システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、動作命題を生成するシステム及び検証するシステムに関する。
【背景技術】
【０００２】
半導体集積回路の設計プロセスでは、始めに、設計する集積回路に対して要求する回路動作及び機能を抽象度の高いＲＴＬ（レジスタ・トランスファ・レベル）でＲＴＬ記述を行う。次に、論理合成処理により、ＲＴＬ記述から半導体製造装置を考慮した抽象度の低いゲートレベルでゲートレベル記述へ変換する。最後に、ゲートレベル記述からマスクパターンを作成し、半導体集積回路の製造を行うという段階を経ていく。
【０００３】
しかし、近年における回路の大規模化及び複雑化により、回路とテストベクタを使用したこれまでの検証手法では、膨大な検証時間が必要となる。また、全てのケースを設計・検証者が考えて検証することは限界に達している。
【０００４】
仮に、全てのケースを検査することができるテストベクタを作成できたとしても、膨大な検査結果を目視により、抜けなく検査されていることを確認することは極めて困難である。
【０００５】
そこで近年では、フォーマル・ベリフィケーション（形式的論理検証）技術の一つとして、動作命題（プロパティ）と検証対象の論理回路（Device Under Test、以下ＤＵＴという）が一致しているかどうかを検証する動作命題検証システムが用いられている。即ち、回路記述と、動作仕様を所定の書式で表した動作命題とを比較する検証手段と、テストベクタと論理回路とをシミュレーションで検証した結果の中に動作命題が実行されているか否かを確認するアサーション検証手段とを備えるシステムが導入され始めている。
【０００６】
ここで、使用される動作命題は、従来、自然言語や波形・図形で記述された仕様書から、設計・検証者が人手で作成する必要があった。近年では、この人手で作成する工程の効率化として、検証対象の論理回路から回路中の状態遷移記述に不要な記述が存在するかなどの検証項目を自動的に抽出する手法が開発されてきている。
【０００７】
しかし、従来の検証手法には以下のような問題があった。
【０００８】
通常、動作命題検証手段は、テストベクタによるシミュレーション検証手段に比べて、網羅的にチェックを行うことができる。設計・検証者が、常に正しい動作命題を入力できるのであれば、完全な検証漏れ防止を実現する強力な手段となる。
【０００９】
しかしながら、従来の自然言語で書かれた仕様書から動作命題を人手で作成する際には、人手が介在することにより以下のような問題が生じていた。
１）設計・検証者の誤認が原因で発生する仕様書と動作命題との不整合により検出漏れが生じる。
２）論理回路の作成が終了するまでは、動作命題の検証を行うことができない。
３）論理回路と動作命題の双方に不整合が含まれている場合、原因の究明が困難である。
【００１０】
よって従来は、論理回路の検証前に動作命題の内容、及び動作命題を表現した動作命題記述の確認作業を行うことができなかった。
【００１１】
更に、検証対象の論理回路が存在しないと動作命題の検証を行うことができないため、作成・生成した動作命題記述自身の検証と、本来の目的である論理回路の回路検証とを分離して行うことができず、双方の作業が混在した状態になっていた。この結果、仮に不一致が検出できたとしても、原因の解明に長時間を要していた。
【００１２】
以下に、従来の検証手法を開示した文献名を記載する。
【特許文献１】特開平２００５−２２２３７１号公報
【発明の開示】
【発明が解決しようとする課題】
【００１３】
本発明は、時系列信号値データから人手を介すことなく自動的に動作命題を作成するシステム、及び論理回路の検証前に動作命題を検証することが可能な動作命題を検証するシステムを提供することを目的とする。
【課題を解決するための手段】
【００１４】
本発明の一態様による動作命題の生成システムは、時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、前記共通データベースに基づいて、同時刻に活性状態にならない複数の信号の組み合わせである同時非活性信号を抽出する同時非活性信号抽出手段と、抽出された前記同時非活性信号に基づいて、動作命題を生成して出力する動作命題出力手段とを備えることを特徴とする。
【００１５】
本発明の一態様による動作命題の生成システムは、時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、前記共通データベースに基づいて、クロックサイクル単位で変化する前記信号値の遷移の規則性を抽出する信号遷移規則性抽出手段と、抽出された前記信号値の遷移の規則性に基づいて、動作命題を生成して出力する動作命題出力手段とを備えることを特徴とする。
【００１６】
本発明の一態様による動作命題の検証システムは、時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、動作命題を与えられ、前記動作命題に含まれる所定の条件を満たす状態を示す信号値遷移情報を抽出する遷移情報抽出手段と、前記共通データベースに基づく信号値遷移情報と、前記信号値抽出手段により抽出された前記信号値遷移情報とを比較し、整合性の有無を判定する動作命題解析手段と、前記動作命題解析手段により整合性がないと判断された場合、前記動作命題の修正を指示する動作命題修正手段とを備えることを特徴とする。
【００１７】
本発明の一態様による動作命題の検証システムは、時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、検証対象の論理回路を読み込み、信号値遷移情報を抽出する論理回路状態遷移抽出手段と、前記共通データベースに含まれる信号値遷移情報と、前記論理回路状態遷移抽出手段により抽出された前記信号値遷移情報とを比較する遷移情報比較手段と、前記遷移情報比較手段により、前記共通データベースに含まれる信号値遷移情報が正しいと判定された場合、前記論理回路に含まれる不整合に関する情報を出力する遷移情報不整合情報出力手段と、前記遷移情報比較手段により、前記論理回路状態遷移抽出手段により抽出された前記信号値遷移情報が正しいと判定された場合、前記時系列信号値データに追加すべき追加時系列信号値データを出力する時系列信号値データ出力手段とを備える。
【００１８】
本発明の一態様による動作命題の検証システムは、時系列信号値データを与えられ、複数の信号のクロックサイクル毎の信号値に関する信号値遷移情報を抽出する信号値抽出手段と、回路の初期状態における複数の信号のそれぞれの信号値に関する初期状態情報と前記信号値遷移情報とに基づいて、あるクロックサイクルにおける信号値と、当該クロックサイクルの前後のクロックサイクルにおける信号値とに関する共通データベースを生成する共通データベース生成手段と、前記共通データベースから信号値遷移情報を抽出し、各クロックサイクル毎の信号値に無効な状態が存在するか否かに基づいて前記共通データベースの妥当性を検査する妥当性検査手段と、前記妥当性検査手段による検査結果に基づき、前記時系列信号値データを修正すべき場合、警報を出力する警報出力手段とを備える。
【発明の効果】
【００１９】
本発明の動作命題の生成システムによれば、時系列信号値データから人手を介すことなく自動的に動作命題を作成し、動作命題の検証システムによれば、論理回路の検証前に動作命題を検証することが可能である。
【発明を実施するための最良の形態】
【００２０】
以下、本発明の実施の形態について図面を参照して説明する。
【００２１】
（１）実施の形態１
本発明の実施の形態１による時系列信号値データより動作命題を自動生成するシステムについて、その構成を図１に示し説明する。
【００２２】
本実施の形態１は、信号値抽出手段２と、共通データベース生成手段４と、同時非活性信号抽出手段５Ａと、動作命題出力手段６とを備える。
【００２３】
信号値抽出手段２に、時系列信号値データ１と信号の初期状態情報３とが入力される。時系列信号値データ１は、仕様書に記述された時刻に対する信号値の変化を示すデータであって、クロックサイクル毎に変化する信号値を示すものである。信号の初期状態情報３は、仕様書に記述された各信号の初期状態情報、例えばバスのアイドル状態時の信号値や不活性状態時の信号値に関する情報である。
【００２４】
そして信号値抽出手段２は、時系列信号値データ１から、クロックサイクルを単位とする各信号の値を抽出する処理を行って、時系列の信号値遷移情報を出力する。
【００２５】
共通データベース生成手段４は、信号値抽出手段２から出力された時系列の信号値遷移情報と、信号の初期状態情報３とを用いて、後述する共通データベースを生成する。
【００２６】
同時非活性信号抽出手段５Ａは、生成された共通データベースから自動的に検証項目として、ここでは同時に活性化されない複数の信号の組み合わせを抽出する処理を行う。
【００２７】
動作命題出力手段６は、抽出された検証項目について、特定言語を用いて記述された動作命題７を出力する。
【００２８】
以下に、上記処理の具体的内容について詳述する。先ず、信号値抽出手段２が行う時系列の信号値遷移情報を出力する処理について述べる。
【００２９】
設計・検証者が、図２に示されたような波形を有するクロック信号ＣＬＫと、プロトコルを定義する６個の信号ｓｉｇＡ、ｓｉｇＣ〜ｓｉｇＧを時系列信号値データとして、システムバスのリード１動作において入力したとする。ここで、各信号ｓｉｇＡ、ｓｉｇＣ〜ｓｉｇＧの信号値は、クロック信号ＣＬＫの立ち上がり時点で判断される。
【００３０】
図２に示された例では、６個の信号ｓｉｇＡ、ｓｉｇＣ〜ｓｉｇＧの全ての信号値が、ロウレベルで活性化される仕様となっている。また、信号ｓｉｇＡの初期状態は、信号値がロウレベルまたはハイレベルの両方を取りうるため、ドントケア（Don’t Care）を示す「Ｘ」にて表記されている。本システムバスは、動作確定までに３クロックサイクルの変化が必要である。
【００３１】
設計・検証者が、このような時系列信号値データを本実施の形態１のシステムに入力すると、信号値抽出手段２によって時間軸、具体的にはクロックサイクル数Ｃ１、Ｃ２、Ｃ３、…に対する各信号値を示すマトリックス状のデータが生成される。
【００３２】
設計・検証者は、このリード１動作に限らず、他の動作、例えばリード２、リード３に対しても、図２に示されたような同様の時系列信号値データを本実施の形態１のシステムに入力する。
【００３３】
尚、信号値抽出手段２、このリード１動作において存在する信号名に限らず、他の動作において存在する信号名を補完して、各動作においてクロックサイクル毎に変化する各信号値のマトリックス状のデータを生成する。その際に、ある動作において存在せず補完された信号は、不活性状態の信号値を持つものとする。
【００３４】
例えば、図３に示されたシステムバスのリード１動作時には、信号ｓｉｇＢは存在しない。しかし、図４に示されたシステムバスのリード２動作時には、信号ｓｉｇＢが存在する。そこで、図３に示されたシステムバスのリード１動作時におけるクロックサイクル毎の各信号値を示すマトリックス状のデータは、図５に示されたように加工される。即ち、リード２動作時に含まれる信号ｓｉｇＢが自動的に挿入される。そして、この信号ｓｉｇＢの信号値は、図１に示された信号の初期状態情報３から抽出され、不活性時における値「１」が全クロックサイクルに追記される。
【００３５】
そして図６に示されるように、３つのリード１、２、３の動作がシステムバスに存在する場合、各動作毎の時系列信号値データに基づいて、クロックサイクル毎の各信号ｓｉｇＡ〜ｓｉｇＧの信号値を示すマトリックス状のデータが生成される。
【００３６】
次に、図７に示されるように、信号値抽出手段２によって生成されたある動作（ここではリード１動作）におけるクロックサイクルＣ１、Ｃ２、Ｃ３毎の各信号値を示すマトリックス状のデータと、図１に示された信号の初期状態情報３における非活性状態における信号とが用いられて、共通データベース生成手段４により共通データベースが生成される。
【００３７】
ここで、共通データベースとは図７に示されたように、信号名（ここでは、ｓｉｇＡ〜ｓｉｇＧ）と、それぞれの初期値データ（ここでは、非活性時の信号値「０」）とを示すデータ（｛ｓｉｇＡ，０｝｛ｓｉｇＢ，０｝｛ｓｉｇＣ，０｝、…、｛ｓｉｇＧ，０｝）と、以下に述べるラベル構造体を示すデータの２種類のデータを含むデータベースである。
【００３８】
図８に、共通データベースに含まれる２種類のデータである初期値データとラベル構造体とを示す。これらのデータは、クロックサイクルＣ１、Ｃ２、Ｃ３毎の信号ｓｉｇＡ〜ｓｉｇＧの信号値の変化を示す時系列信号値データから生成される。
【００３９】
ラベル構造体は、ある時刻、例えばクロックサイクルＣ２における全ての信号ｓｉｇＡ〜ｓｉｇＧの信号値の組み合わせ「０１１０００１」から算出される状態、例えば１０進数に変換して一意に定まる状態ラベルと、その状態に遷移した元の状態、即ち１クロックサイクル前のクロックサイクルＣ１における信号ｓｉｇＡ〜ｓｉｇＧの信号値の組み合わせ「Ｘ１１１１１１」から算出される状態ラベルと、その状態から遷移する先の状態である１クロックサイクル後のクロックサイクルＣ３における信号ｓｉｇＡ〜ｓｉｇＧの信号値の組み合わせ「０１１１１１１」から算出される状態ラベルとを保持する。
【００４０】
図８に示された状態ラベルの一例では、例えば現時点における状態ラベルが「ＬＡＢＥＬ_ＮＡＭＥ」であるとすると、その１クロックサイクル前の状態ラベルは「ＩＮ_ＬＡＢＥＬ」、１クロックサイクル後の状態ラベルは「ＯＵＴ_ＬＡＢＥＬ」となる。
【００４１】
尚、現時点における状態ラベルの前の状態のラベル、及び後の状態のラベルは、ここではそれぞれ１つずつ存在しているが、これに限らずそれぞれ複数存在する場合がある。
【００４２】
また、現時点の状態ラベルの前の状態ラベル、または後の状態のラベルが存在しない場合は、それぞれＮＵＬＬ値が格納される。
【００４３】
ラベルの具体的数値について、図８に示された例では、それぞれのクロックサイクルにおける信号ｓｉｇＡ〜ｓｉｇＧの信号値の組み合わせである２進数の数値から１０進数の数値に変換したものを用いている。しかしこれに限らず、それぞれの状態を一意的に表す数値を用いるのであれば、他の計算手法を用いてもよい。
【００４４】
ここで、具体的なラベルの生成手順として、図８に示された各クロックサイクル毎の各信号値を示すマトリックス状のデータを用いてラベルを生成する手順について説明する。
１）各クロックサイクルＣ１、Ｃ２、Ｃ３における各信号値を示すマトリックスデータから、図８に示されたように、全信号名ｓｉｇＡ〜ｓｉｇＧと、信号の初期状態情報３とを抽出し、共通データベース「ＳＩＧ_ＩＮＦＯ  ｛ｓｉｇＡ、０｝〜｛ｓｉｇＧ、０｝」に格納する。
２）図８において「（ａ）」として示されたように、動作モード毎、クロックサイクル毎の列情報を抽出する。
例えば、クロックサイクルＣ１において、各信号ｓｉｇＡ〜ｓｉｇＧの信号値を列情報として抽出すると、「Ｘ１１１１１１」という情報が取得される。
３）図８において「（ｂ）」として示されたように、信号値が不確定（Don’t Care）であることを示す「Ｘ」については、可能性のある２つのデータ、即ち「０」又は「１」に分けて再加工する。
４）これにより、図８において「（ｃ）」として示されたように、リード１動作時のクロックサイクルＣ１における列データ「Ｘ１１１１１１１」を、「０１１１１１１１」と「１１１１１１１１」とに分けて再加工する。
５）上記クロックサイクルＣ１、Ｃ２、Ｃ３、…毎の列データを２進数と見なし、１０進数に変換して、データベース上のラベル構造体を生成する。
例えば、リード１動作時のクロックサイクルＣ１における列データ「０１１１１１１１」は、「ＬＡＢＥＬ_ＮＡＭＥ＝６３」に、「１１１１１１１１」は「ＬＡＢＥＬ_ＮＡＭＥ＝１２７」に変換する。
６）図８において「（ｄ）」として示されたように、共通データベースのラベル構造体は、ラベル自身の名前と信号遷移のＩＮ／ＯＵＴの遷移ラベルを格納するデータを持つものとする。
例えば、あるクロックサイクルＣ２におけるラベル構造体が「ＬＡＢＥＬ_ＮＡＭＥ＝４９」であるとすると、その１つ前のクロックサイクルＣ１におけるラベル構造体は「ＩＮ_ＬＡＢＥＬ＝６３又は１２７」、その１つ後のクロックサイクルＣ３におけるラベル構造体は「ＯＵＴ_ＬＡＢＥＬ＝６３」となる。
７）以上のような手順１）〜５）で、各動作モード毎、クロックサイクル毎のラベル構造体用のデータを繰り返し構築し、遷移したラベル名を追記していく。
【００４５】
既に存在するラベルの場合、共通データベース内の既存のラベル構造体にデータを追記する。新規ラベルの際には、ラベル構造体を新規作成する、という工程を繰り返す。
【００４６】
尚、新規のラベル構造体を生成した場合には、あるクロックサイクルＣ１における１つ前の信号値が存在しないため、その場合のラベル構造体は「ＩＮ_ＬＡＢＥＬ」には「ＮＵＬＬ」が格納される。
【００４７】
共通データベース生成手段４により共通データベースが生成された後、動作命題の生成が行われる。動作命題は、検証項目に関するデータを自動的に抽出し、抽出したデータに基づいて生成される。
【００４８】
ここでは、検証項目の自動抽出の一例として、あるクロックサイクル中に同時に複数の信号が活性状態（本実施の形態１では、信号値がロウ「０」の状態）にならない、という場合を例にとり説明する。この処理は、図１に示された同時非活性信号抽出手段５Ａにより行われる。
【００４９】
同時非活性信号抽出手段５Ａは、先ず共通データベースから全ラベル名を抽出する。システムバスのリード１動作では、ＬＡＢＥＬ_ＮＡＭＥ＝５２からLＡＢＥＬ_ＮＡＭＥ＝１２７までのラベル名が抽出される。
【００５０】
共通データベースに含まれる初期データ「ＳＩＧ_ＩＮＦＯ  ｛ｓｉｇＡ、０｝〜｛ｓｉｇＧ、０｝」における信号名ｓｉｇＡ〜ｓｉｇＧを、図９に示されたように、行と列とにそれぞれ並べてマトリクス状の２次元配列を作成する。図中、ハッチングが施された右上半分の領域は、左下半分の領域と重複しており、検査不要な箇所である。
【００５１】
ここで、２次元配列における信号名は、初期データ「ＳＩＧ_ＩＮＦＯ  ｛ｓｉｇＡ、０｝〜｛ｓｉｇＧ、０｝」における信号名ｓｉｇＡ〜ｓｉｇＧの順番に行、列にそれぞれ並べる。
【００５２】
２つの信号が同時に活性状態にならないことを調べる検査とは、言い換えれば、同時に活性状態、即ちロウ「ここでは、「０」」になっている状態が共通データベース中のラベルとして存在しているか否かを調べることである。
【００５３】
そこで、先ず図９に示されたような信号ｓｉｇＡ〜ｓｉｇＧを縦軸、横軸にそれぞれ配置したマトリクス状の２次元配列を用意する。
【００５４】
図９に示された２次元配列においては、７個の信号ｓｉｇＡ〜ｓｉｇＧに対し、２１（＝７＊６／２）組みの信号について検査を行う必要がある。初期値を「０」とする２１個の検査フラグを用意する。
【００５５】
そして、それぞれ２つずつの信号の組み合わせにおいて、同時に活性状態、即ち同時にロウ「０」の信号値をとる組み合わせに対しては、検査済であることを示す値「１」に検査フラグを変更する。図９において、検査済の信号の組み合わせ、例えば信号ｓｉｇＣとｓｉｇＡ、ｓｉｇＤとｓｉｇＢ等の組み合わせの検査フラグには、検査終了を意味するチェックを記入する。
【００５６】
逆に、同時に活性状態になることが発見されなかった信号の組み合わせ、例えば図９に示された信号ｓｉｇＢとｓｉｇＡ、ｓｉｇＧとｓｉｇＢの組み合わせの検査フラグには、検査終了のチェックが記入されず残ることになる。
【００５７】
２１個の全ての信号の組み合わせに対する検査が終了した後に、検査フラグが初期状態であることを示す「０」のままである信号の組み合わせ、ここでは信号ｓｉｇＢとｓｉＧＡ、ｓｉｇＧとｓｉｇＢの組み合わせを抽出することで、２つの信号が同時に活性状態、即ち信号値が同時にロウ「０」になり得ないという検証項目を自動的に抽出することができる。
【００５８】
このような同時非活性信号抽出手段５Ａによって抽出された検証項目は、動作命題出力手段６によって、図示されていないシミュレータ検証システムや動作命題検証システムへの入力となる動作命題の書式、即ち動作命題記述として出力される。
【００５９】
図１０に、動作命題記述の一例として、信号ｓｉｇＢと信号ｓｉｇＧとは、同時に活性状態（１’ｂ０即ち「０」）になることはないことを示す書式「ｆｏｒｅｖｅｒ（！（ｓｉｇＢ＝＝１’ｂ０＆＆ｓｉｇＧ＝＝１’ｂ０））」、信号ｓｉｇＡと信号ｓｉｇＢとは、同時に活性状態になることはないことを示す書式「ｆｏｒｅｖｅｒ（！（ｓｉｇＡ＝＝１’ｂ０＆＆ｓｉｇＢ＝＝１’ｂ０））」を示す。
【００６０】
以上のように、本実施の形態１のシステムによれば、論理回路（ＤＵＴ）の検証を行なう前に、時系列信号値データから人手を介すことなく自動的に動作命題を作成することで、ＬＳＩ検証時間の短縮を実現することができる。ここで、本実施の形態１では、時系列信号値データから複数の信号が同時に活性化することがありえないという検証項目に基づく動作命題を生成することができる。
【００６１】
尚、本実施の形態１では２つの信号の組み合わせにおける同時非活性化信号の抽出処理を行っている。しかしこれに限らず、３つ以上の信号の組み合わせに対する同時非活性化信号の抽出も、本実施の形態１と同様の手順で行うことができる。
【００６２】
（２）実施の形態２
本発明の実施の形態２による動作命題の生成システムについて説明する。本実施の形態２では、信号遷移に存在する規則性を見い出して動作命題の自動生成を行うものであり、図１１に本実施の形態２によるシステムの構成を示す。
【００６３】
上記実施の形態１と比較し、共通データベース生成手段４によって生成された共通データベースから自動的に検証項目を抽出する手段が相違する。即ち、上記実施の形態１における同時非活性信号抽出手段５Ａの替わりに、本実施の形態２では信号遷移規則抽出手段５Ｂを備えている。尚、共通データベースを生成するプロセスまでに用いられる時系列信号値データ１、信号の初期状態情報３、信号状態抽出手段２、共通データベース生成手段４は上記実施の形態１と同様であり、説明を省略する。
【００６４】
上記実施の形態１と同様に、共通データベース生成手段４によって共通データベースが生成される。この共通データベースにより、上記実施の形態１において説明したように、３つの連続したクロックサイクルＣ（ｊ−１）、Ｃｊ、Ｃ（ｊ＋１）における各信号ｓｉｇＡ〜ｓｉｇＧの信号値の遷移が明らかとなる。
【００６５】
この共通データベースのなかから、３つの連続したクロックサイクル間で、非活性状態から活性状態、さらに非活性状態に遷移する信号の抽出を行う。ここでは、信号ｓｉｇＡ〜ｓｉｇＧの全ての信号の活性状態は、信号値がロウ「０」のときである。そこで、信号値が「１」→「０」→「１」というように遷移するものの抽出を行う。
【００６６】
具体的な手順としては、共通データベースから、各信号名ｓｉｇＡ〜ｓｉｇＧとそれぞれの信号毎の３つのクロックサイクルに渡る信号値の遷移とを抽出し、図１２に示されたように配置する。その際に、ある信号の信号値の変化が「１」→「０」→「１」でないことが判明した時点で、その信号の信号値の抽出を終了する。
【００６７】
即ち、各信号の信号値が、開始時点で既に「０」である場合は、次に遷移する信号値を抽出する必要が無い。図１２（ａ）に示された例では、信号ｓｉｇＡは開始時点で「０」であるため、以降のクロックサイクルにおける信号値を考慮する必要が無くハッチングで検証枠がマスクされている。
【００６８】
信号ｓｉｇＢ〜ｓｉｇＧは開始時点で全て「１」であるが、次のクロックサイクルで信号ｓｉｇＤ及びｓｉｇＥのみが「０」となり、他の信号は「１」となるので以降のクロックサイクルにおける信号値を考慮する必要はない。
【００６９】
そして、信号ｓｉｇＤのみが次のクロックサイクルで「１」となるので、この信号ｓｉｇＤのみを抽出することになる。図１２（ｂ）に示された例においても、信号ｓｉｇＤのみが検出される。
【００７０】
このようにして、クロックサイクル毎にさらなる信号値の考慮が必要であるか否かを判断して不要な検査を省略しながら、所定の信号値の推移を行う信号名を自動的に抽出する。
【００７１】
このような手順で、信号遷移規則抽出手段５Ｂにより抽出された検証項目は、動作命題出力手段６によって、シミュレータ検証システムや動作命題検証システムの入力となる動作命題の書式（プロパティ記述）として出力される。
【００７２】
図１３に、信号ｓｉｇＤが活性状態になれば、次のサイクルで必ず信号ｓｉｇＤの信号値が「１」になることを示す書式の一例として、（ｓｉｇＤ＝＝１’ｂ０→ｎｅｘｔ＿Ｃ（ｓｉｇＤ＝＝１’ｂ１））を示す。
【００７３】
このように、本実施の形態２によれば、時系列信号値データから信号遷移の規則性に関する検証項目に基づく動作命題を自動的に抽出することができる。
【００７４】
そして、検証対象である論理回路（ＤＵＴ）の検証を行なう前に、仕様書と動作命題との整合性を取り、作成した動作命題の検証と本来の目的である論理回路の検証とを分離して進めることで、論理回路の検証に要する全体の時間の短縮を実現することができる。
【００７５】
本実施の形態２では、３クロックサイクルにおける信号値の遷移についての検証項目に基づいて動作命題を生成するが、検証するクロックサイクルは任意に設定することができる。そして、上記例と同様な手順により自動的に規則性のある信号遷移を抽出することが可能である。
【００７６】
（３）実施の形態３
本実施の形態３による動作命題の検証システムは、動作命題が既に存在しており、この動作命題の検証を行うものである。
【００７７】
動作命題は、仕様が自然言語でのみ記述されている等の理由で、仕様書の波形情報から動作命題を自動生成することができない場合がある。このような人手が介在する動作命題中に存在する仕様書との不整合性に対しても、本実施の形態３によれば共通データベースを活用することで動作命題を検証することができる。
【００７８】
図１４に、本実施の形態３による動作命題の検証システムの構成を示す。本システムは、上記実施の形態１〜２と同様に、時系列信号値データ１及び信号の初期状態情報３とが入力される信号値抽出手段２と、共通データベース生成手段４の他に、さらに共通データベースと、動作命題１５が入力される遷移情報抽出手段１６、動作命題解析手段１７、動作命題修正要求手段１９とを備える。
【００７９】
信号値抽出手段２と共通データベース生成手段４の動作については上記実施の形態１〜２において述べた通りであり、説明を省略する。
【００８０】
遷移情報抽出手段１６は、共通データベース生成手段４によって生成された共通データベースから抽出された信号値の遷移情報と、既存の動作命題１５とを与えられ、動作命題において記述された所定の条件式を満たす状態を信号値の遷移情報から抽出する処理を行う。
【００８１】
動作命題解析手段１７は、動作命題１５を、各信号の信号値がクロックサイクル毎に変化している信号値の遷移情報に変換し、動作命題１５における記述が論理的に正しいか否かを、共通データベースから抽出された遷移情報と比較解析する。
【００８２】
動作命題解析手段１７の解析により、動作命題１５から変換された信号値の遷移情報と、共通データベースから変換された信号値の遷移情報との間に整合性があると判断された場合、動作命題１５には修正すべき誤りがないため処理を終了する。
【００８３】
一方、動作命題１５からの信号の遷移情報と、共通データベースからの信号の遷移情報との間で整合性がとれていないと判断された場合には、動作命題修正要求手段１９が、動作命題１５の修正を促すメッセージを設計・検証者に対して出力する。動作命題１５が、設計・検証者によって修正される。このメッセージの出力後、遷移情報抽出手段１６の処理へ戻る。
【００８４】
以上説明した本実施の形態３によれば、動作命題１５から変換された状態遷移情報と、仕様書の波形情報から抽出された状態遷移情報との整合性を判断することで、既存の動作命題の検証を行うことが可能となる。
【００８５】
（４）実施の形態４
本発明の実施の形態４によるシステムについて、その構成を示した図１５を用いて説明する。本実施の形態４は、検証対象の論理回路（ＤＵＴ）が既に存在する場合に、論理回路と時系列信号値データとの整合性について比較検証を行うものである。
【００８６】
本システムは上記実施の形態１〜３と同様に、時系列信号値データ１及び信号の初期状態情報３とが入力される信号状態抽出手段２と、共通データベース生成手段４を備え、さらに共通データベースと検証対象の論理回路（ＤＵＴ）２５とが入力される論理回路遷移情報抽出手段２６と、遷移情報比較手段２７と、追加時系列信号値データ２９を出力する時系列信号値データ出力手段２８と、遷移情報不整合情報出力手段３０とを備えている。共通データベースを生成するまでの処理は上記実施の形態１〜３と同様であり、説明を省略する。
【００８７】
以下に、共通データベースを生成した後の処理について述べる。検証対象の論理回路（ＤＵＴ）２５と共通データベースとが論理回路遷移情報抽出手段２６に入力される。図１６に一例として示されたような検査対象となる論理回路（ＤＵＴ）の回路構造から、例えばリード３動作における各信号ｓｉｇＡ〜ｓｉｇＧのクロックサイクルＣ１、Ｃ２、Ｃ３における信号値の遷移を示す信号値の遷移情報が抽出される。この信号値の遷移情報から、図１６に示されたように信号遷移のラベル名が抽出される。ここでは、クロックサイクルＣ１、Ｃ２、Ｃ３において、信号ｓｉｇＡ〜ｓｉｇＧの信号値を２進数にみたてて並べた後、１０進数に変換した値が６３→５１→５７と遷移していくことがわかる。このような遷移ラベル名を抽出する。
【００８８】
この論理回路遷移情報抽出手段２６で抽出された信号遷移のラベル名と、共通データベース生成手段４により抽出された信号遷移のラベル名とが、遷移情報比較手段２７により比較判定される。
【００８９】
比較された結果、両者に整合性があると判定されたときは処理を終了する。整合性がないと判定されたときは、以下のような４つの場合が考えられる。
【００９０】
１）検証対象の論理回路（ＤＵＴ）に存在する信号遷移が、時系列信号値データから抽出した共通データベースの信号遷移に存在しない場合
この場合は、以下の２つの場合が存在する。
【００９１】
１−１）時系列信号値データが正しい場合
この場合は、時系列信号値データが正しい場合に相当する。この場合は、論理回路（ＤＵＴ）に不要な回路が存在することになる。この場合は論理回路２９が正しくないことになり、遷移情報不整合情報出力手段３０が、論理回路の修正に必要な不整合の情報を設計・検証者に対して出力し、回路の修正を促す。
【００９２】
１−２）論理回路が正しい場合
設計途中で仕様変更が発生し、論理回路（ＤＵＴ）には追加仕様を反映したが、仕様書には追加仕様を反映しておらず、時系列信号値データが正しくない場合が相当する。このような場合には論理回路が正しいことになり、時系列データ出力手段３１において、仕様書を更新するための追加の時系列信号値データ３２を生成する
２）検証対象の論理回路（ＤＵＴ）には存在しない信号遷移が、時系列信号値データから抽出した共通データベースの信号遷移に存在する場合
この場合は、以下のような２つの場合が存在する。
【００９３】
２−１）時系列信号値データが正しい場合
論理回路に存在すべき必要な回路が存在しない場合が相当し、論理回路は正しくないことになる。そこで、設計・検証者にその旨のメッセージを出力し、遷移情報不整合情報出力手段３０において論理回路の修正に必要な不整合情報を出力して論理回路の修正を促す。
【００９４】
２−２）論理回路が正しい場合
設計途中で仕様変更が発生し、論理回路（ＤＵＴ）には仕様変更を反映したが、仕様書には反映しておらず、時系列信号値データが正しくない場合が相当する。このような場合は論理回路が正しいことになり、設計・検証者にメッセージを出力し、論理回路から抽出した信号遷移情報に基づいて、時系列データ出力手段３１において正しい時系列信号値データを生成するために必要な追加の時系列信号値データ３２を生成する。
【００９５】
上記４つの場合（１−１、１−２、２−１、２−２）は、それぞれ同時に発生することはなく相反する関係にある。そこで、遷移情報比較手段２７において不整合である旨の比較結果が出力されると、その出力を与えられた遷移情報不整合情報出力手段２９は４つの可能性を表示する。この表示に基づいて、設計・検証者はいずれの場合が該当するか判断し、上述したような修正を行う。
【００９６】
遷移情報比較手段２７から比較結果を与えられた時系列信号値データ出力手段２８は、その比較結果に基づいて、追加すべき時系列信号を示す追加時系列信号値データ２９を生成して出力する。
【００９７】
このように本実施の形態４によれば、検証対象の論理回路（ＤＵＴ）２５が存在する場合、この論理回路２５を用いて仕様書と論理回路と間の整合性を比較し、不整合が存在する場合は修正に必要な情報を出力することで、検証効率を向上させることができる。
【００９８】
（５）実施の形態５
本発明の実施の形態５による動作命題の検証システムについて説明する。上記実施の形態１、２、３では、時系列信号値データから生成された共通データベースに基づいて、動作命題の自動抽出を行う。
【００９９】
しかし、仕様書に書かれている時系列信号値データ自体に、記述漏れが存在することがある。そこで、共通データベースから検証項目を抽出する前に、与えられた時系列信号値データの妥当性を検査する必要がある。
【０１００】
図１７に示されたように、本実施の形態５によるシステムは、時系列信号値データ１と信号の初期状態情報３とが入力される信号値抽出手段２、共通データベース生成手段４、共通データベース４７を出力する妥当性検査手段４５、警報出力手段４６を備えている。
【０１０１】
信号値抽出手段２、共通データベース生成手段４により共通データベースを生成するまでの処理は上記実施の形態１〜４と同様であり、説明を省略する。
【０１０２】
妥当性検査手段４５は、仕様書の時系列信号値データを修正するように時系列信号値データに基づいて作成された共通データベースの妥当性を検査する手段である。検査した結果、妥当性があると判断された場合は、妥当性の確かめられた共通データベース４７が出力される。妥当性がないと判断された場合は、警告出力手段４６が設計・検証者に対して時系列信号値データの修正を促すため警告を出力する。
【０１０３】
本実施の形態５では、上記実施の形態１におけるシステムバスのリード１、２、３動作の時系列信号値データに基づいて作成された共通データベースを用いて、時系列信号値データにおいて不足している信号値の遷移情報の検出を行う。
【０１０４】
上記実施の形態１において、図８を用いて説明したように、共通データベースには、信号値の遷移情報、即ち各信号毎に、現時点における信号値、クロックサイクルが１つ前における信号値、クロックサイクルが１つ後における信号値に関するラベル構造体が含まれている。
【０１０５】
このようなラベル構造体における各ラベル「ＬＡＢＥＬ_ＮＡＭＥ」、「ＩＮ_ＬＡＢＥＬ」、「ＯＵＴ_ＬＡＢＥＬ」を検査する。図１９に示された例では、「ＬＡＢＥＬ_ＮＡＭＥ＝６２、５６、４８、５０」の４つは、ラベル構造体の「ＯＵＴ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態、即ち１つ後のクロックサイクルにおいて信号値が無効な状態である。また、「ＬＡＢＥＬ_ＮＡＭＥ＝１２７」は、「ＩＮ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態、即ち１つ前のクロックサイクルにおける信号値が無効な状態である。回路動作が、ある動作を行った後、必ずアイドリング状態に戻ることを前提とすると、いずれのクロックサイクルにおいてもその前後において有効な信号値をとることになる。従って、あるクロックサイクルの１つ前、あるいは１つ後において無効な信号値が存在するということは、全ての状態遷移を記述しきれていないことを意味する。
【０１０６】
特に、「ＩＮ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態であるということは、当該クロックサイクルの１つ前の信号値が無効な状態であることを意味するので、当該クロックサイクルはリード動作の初期状態である可能性が高い。
【０１０７】
信号の初期状態情報として、信号の初期における信号値が、例えば図１８に一例として示されたように、「ＩＮＩＴ＿ＳＩＧ：ｓｉｇＡ＝０，ｓｉｇＢ＝１，ｓｉｇＣ＝１，ｓｉｇＤ＝１，ｓｉｇＥ＝１，ｓｉｇＦ＝１，ｓｉｇＧ＝１；」というように記載されている場合、その信号値に従ってラベル構造体中の「ＩＮ_ＬＡＢＥＬ」に追記が行われる。
【０１０８】
一方、「ＯＵＴ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態である場合は、２つの可能性が存在する。
【０１０９】
第１の可能性は、所望の動作が全て仕様書に記載されており、あるサイクルクロックから１つ後のサイクルクロックへの遷移が初期状態である場合が相当する。このように全ての所望の動作が記載されていると判断した場合には、「ＯＵＴ_ＬＡＢＥＬ」に初期状態が記載されるように、時系列信号値データにおける最終クロックサイクルに初期状態を付記する。
【０１１０】
第２の可能性は、仕様書において所望の動作の記載漏れが存在している場合が相当する。この場合は、「ＯＵＴ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態である場合には、その旨を警告するメッセージを出力する。
【０１１１】
設計・検証者は、「ＯＵＴ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態であることを示すメッセージを受けた場合、所望の動作が仕様書に含まれる時系列信号値データに全て記載しているか否かについて確認する。
【０１１２】
図１９に示されたような共通データベースのラベル遷移図が、図示されていないモニタ画面上に表示されている場合は、画面上の遷移図で接続がとぎれている最終箇所から初期のクロックサイクルへの接続を行う。この処理を通じて、共通データベースの更新を行う。
【０１１３】
図１９に示されたラベル構造体において、あるクロックサイクルから１つ次のクロックサイクルにおける信号値、即ち「ＯＵＴ_ＬＡＢＥＬ」が「ＮＵＬＬ」状態であるものとして、「６２」、「５６」、「４８」、「５０」が存在する。このように、あるクロックサイクルで信号値が停止して以降のクロックサイクルでの信号値が存在せず、接続先がない最終クロックサイクルが存在する。また、「１２７」のように、その１つ前のクロックサイクルにおける信号値が存在しないクロックサイクルが存在する。
【０１１４】
このような場合、図２０に示されたように、接続がとぎれた最終クロックサイクル「６２」、「５６」、「４８」、「５０」から次のクロックサイクルの信号値として、初期状態の「１２７」に接続することで、修正を行っている。
【０１１５】
このような修正により、仕様書と時系列信号値データとの間で整合性が保証され、この時系列信号値データを用いて動作命題を作成した場合に、動作命題と仕様書との整合性も確保される。
【０１１６】
上述したように本実施の形態５によれば、検証対象である論理回路（ＤＵＴ）を用いて検証を行なう前に、仕様書と時系列信号値データとの整合性を確保し、さらに動作命題と仕様書との整合性を確保することが可能である。
【０１１７】
上述した実施の形態は一例であって、本発明を限定するものではなく、本発明の技術的範囲内において様々に変形することが可能である。
【図面の簡単な説明】
【０１１８】
【図１】本発明の実施の形態１によるシステムの構成を示すブロック図。
【図２】同実施の形態１において仕様書に記述された時系列信号値データの一例を示す波形図。
【図３】同実施の形態１において時系列信号値データから抽出したクロックサイクル毎の各信号の信号値を示すマトリクスデータを示した説明図。
【図４】同実施の形態１において仕様書に記述された追加時系列信号値データの一例を示す波形図。
【図５】同実施の形態１においてリード１、リード２動作時におけるクロックサイクル毎の各信号の信号値を示すマトリクスデータを示した説明図。
【図６】同実施の形態１において仕様書に書かれた３つの時系列信号値データから変換して得られたリード１、リード２動作時におけるクロックサイクル毎の各信号の信号値を示すマトリクスデータを示した説明図。
【図７】同実施の形態１において共通データベースに含まれる信号情報データの一例を示す説明図。
【図８】同実施の形態１において共通データベースに含まれるラベル構造体の一例を示す説明図。
【図９】同実施の形態１において同時非活性信号の検査フラグを示す説明図。
【図１０】同実施の形態１において同時非活性信号の検査結果に基づいて得られた動作命題の一例を示す説明図。
【図１１】本発明の実施の形態２によるシステムの構成を示すブロック図。
【図１２】同実施の形態２において連続する３クロックサイクルに渡って信号が遷移する規則を抽出するプロセスを示す説明図。
【図１３】同実施の形態２において抽出された動作命題の一例を示す説明図。
【図１４】本発明の実施の形態３によるシステムの構成を示すブロック図。
【図１５】本発明の実施の形態４によるシステムの構成を示すブロック図。
【図１６】同実施の形態４において検証対象の論理回路記述から信号遷移情報を抽出する例を示す説明図。
【図１７】本発明の実施の形態５によるシステムの構成を示すブロック図。
【図１８】本発明の実施の形態５において信号の初期状態情報の一例を示す説明図。
【図１９】同実施の形態５におけるラベル構造体の遷移の一例を示す説明図。
【図２０】図１９におけるラベル構造体の遷移状態を修正した場合の遷移を示す説明図。
【符号の説明】
【０１１９】
１  時系列信号値データ
２  信号値抽出手段
３  信号の初期状態情報
４  共通データベース生成手段
５Ａ  同時非活性信号抽出手段
５Ｂ  信号遷移規則抽出手段
６  動作命題出力手段
７  動作命題
１５  動作命題
１６  遷移情報抽出手段
１７  動作命題解析手段
１９  動作命題修正要求手段
２５  検証対象の論理回路
２６  論理回路状態遷移抽出手段
２７  遷移情報比較手段
２８  時系列信号値データ出力手段
２９  追加時系列信号値データ
３０  遷移情報不整合情報出力手段
４５  妥当性検査手段
４６  警報出力手段
４７  共通データベース
【図１】
2008097504.tif 000003
【図２】
2008097504.tif 000004
【図３】
2008097504.tif 000005
【図４】
2008097504.tif 000006
【図５】
2008097504.tif 000007
【図６】
2008097504.tif 000008
【図７】
2008097504.tif 000009
【図８】
2008097504.tif 000010
【図９】
2008097504.tif 000011
【図１０】
2008097504.tif 000012
【図１１】
2008097504.tif 000013
【図１２】
2008097504.tif 000014
【図１３】
2008097504.tif 000015
【図１４】
2008097504.tif 000016
【図１５】
2008097504.tif 000017
【図１６】
2008097504.tif 000018
【図１７】
2008097504.tif 000019
【図１８】
2008097504.tif 000020
【図１９】
2008097504.tif 000021
【図２０】
2008097504.tif 000022