(57)【要約】【課題】本発明の課題は、論理回路の状態遷移グラフ中で矛盾する箇所を検出するのみでなく、一旦検出された矛盾箇所を記憶領域に保持しておき、動作として存在してはならない状態についても検証項目として明示的に記述する論理検証支援システムを提供すことを目的とする。【解決手段】上記課題は、論理回路を検証するための検証項目を作成する論理検証支援システムであって、前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手段を有することを特徴とする論理検証支援システムにより達成される。【選択図】  図２
2008204371.tif 000002
【特許請求の範囲】
【請求項１】
論理回路を検証するための検証項目を作成する論理検証支援システムであって、
前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手段を有することを特徴とする論理検証支援システム。
【請求項２】
前記矛盾抽出手段は、前記矛盾箇所となった前記状態情報と前記状態遷移情報とを矛盾情報を用いて矛盾項目を作成して検証技術者へ通知することを特徴とする請求項１記載の論理検証支援システム。
【請求項３】
前記矛盾抽出手段によって抽出された前記矛盾箇所を含めて前記状態情報と前記状態遷移情報とを用いて検証項目を作成する検証項目作成手段を有することを特徴とする請求項１記載の論理検証支援システム。
【請求項４】
前記論理回路の動作を規定する仕様記述データに従って、状態遷移グラフ作成に係る前記状態情報と前記遷移条件情報とを作成すると共に、該仕様記述データの修正によって使用しなくなった状態情報と遷移条件情報とに使用しないマークを付加して削除することなく保存する状態遷移グラフ作成手段を有することを特徴とする請求項３項記載の論理検証支援システム。
【請求項５】
前記検証項目作成手段は、前記使用しないマークが付加されている前記状態遷移情報で示される処理を実行しないと判断した場合、該状態遷移情報に処理を実行しないフラグを付加することを特徴とする請求項４記載の論理検証支援システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理回路の状態遷移グラフ中で矛盾する箇所を検出するのみでなく、一旦検出された矛盾箇所を記憶領域に保持しておき、動作として存在してはならない状態についても検証項目として明示的に記述する論理検証支援システムに関する。
【背景技術】
【０００２】
従来の論理回路の論理検証方法では、図１に示すように、論理回路を検証する検証技術者２が自然言語で記載された仕様書１の内容を読んで理解して、論理回路への入力に対する動作の期待値を自然言語で記述した表形式で検証項目３を作成していた。図１中、Ａ及びＢは論理回路への入力データの種別を示し、（α）及び（β）は論理回路の処理内容を示している。
【０００３】
例えば、検証技術者２は、仕様書１で「Ａが入力されたら、（α）処理、Ｂが入力されたら、（β）処理」などの記述を理解し、「Ａを回路の入力として論理シミュレーション」した場合、「（α）の処理が実施されたことを確認」し、「Ｂを回路の入力として論理シミュレーション」した場合、「（β）の処理が実施されたことを確認」する等を記述した検証項目の一覧を作成していた。
【特許文献１】特開平８−１１０９０７号公報
【特許文献２】特開平８−２９２８８４号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
上述したような従来の論理回路の論理検証方法では、検証技術者２が経験に基づいて「どのような検証をすべきか」を判断して検証項目を手作業で書き出していた。このような場合、自然言語等で記載された文書による仕様書１が与えられると、検証技術者２は、例えば、ＡやＢがあらゆる想定可能な順序で入力された場合を考慮した全組合せについて十分検討したか否かの判断が検証技術者２の経験に依存しており、検討が十分であったか否かの確認は容易ではなかった。その過程で、検証技術者２は経験に基づいて矛盾箇所を発見した場合、修正するための所定の手続きを行い、修正された仕様書１を再度チェックしていた。
【０００５】
その結果、このような経験に基づく矛盾の抽出及び検証項目の抽出では、検証すべき項目を抽出しきれないまま検証作業を完了させてしまい、論理回路の提供先で検証項目抜けなどに起因する論理障害が発生すると言った問題を招くこともあった。
【０００６】
よって、本発明の目的は、論理回路の状態遷移グラフ中で矛盾する箇所を検出するのみでなく、一旦検出された矛盾箇所を記憶領域に保持しておき、動作として存在してはならない状態についても検証項目として明示的に記述する論理検証支援システムを提供することである。
【課題を解決するための手段】
【０００７】
上記課題を解決するため、本発明は、論理回路を検証するための検証項目を作成する論理検証支援システムであって、前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手段を有するように構成される。
【０００８】
上記手段を機能としてコンピュータに実行させるためのプログラム、そのプログラムを記憶したコンピュータ読み取り可能な記憶媒体、及び、上記手段を機能としてコンピュータが処理する方法とすることもできる。
【発明の効果】
【０００９】
本願発明は、論理回路の状態遷移グラフ中で矛盾する箇所を検出するのみでなく、一旦検出された矛盾箇所を記憶領域に保持しておき、動作として存在してはならない状態についても検証項目として明示的に記述することが可能となる。
【発明を実施するための最良の形態】
【００１０】
以下、本発明の実施の形態を図面に基づいて説明する。
【００１１】
図２は、本発明の一実施例に係る論理検証システムの機能構成を示す図である。図２において、論理検証システム１００は、仕様記述作成部１０と、検出項目抽出部３０と、テストデータ作成部８０と、論理シミュレータ９０とを有する。
【００１２】
論理検証システム１００は、１つのコンピュータ装置で実現されてもよいし、２又は３のコンピュータ装置で実現されてもよい。検出項目抽出部３０の全体は、１つのコンピュータ装置で運用されることが望ましい。複数のコンピュータ装置で実現する場合には、各処理部１０、３０、８０及び９０で作成されたデータを外部記憶媒体に格納し、各処理部で必要に応じて読み込むようにすればよい。又は、複数のコンピュータ装置をネットワークなどで互いに接続可能な構成とすればよい。
【００１３】
仕様書記述作成部１０は、検証技術者２が論理回路仕様書又は規格書などに基づいて、所定の記述形式で論理回路への入力データ及び論理回路の機能（状態遷移など）を入力した内容から仕様記述データ１０ａを作成する。
【００１４】
検証項目抽出部３０は、仕様書記述作成部１０によって作成された仕様記述データ１０ａを用いて検証項目を抽出して検証項目情報３７ａを作成する処理部であり、仕様記述解析部３１と、状態遷移グラフ作成部３２と、矛盾抽出部３４と、検証項目作成部３７とを有する。
【００１５】
仕様記述解析部３１は、仕様記述データ１０ａを読み込んで解析し、仕様記述データ１０ａに基づいて状態リスト３０ａと入力データ３０ｂとを生成して記憶領域に格納する。
【００１６】
状態遷移グラフ作成部３２は、状態リスト３０ａと入力データ３０ｂとを用いて、状態を示す状態構造体３２ａと状態遷移を示すリンク構造体２３ｂとを作成して、これら状態構造体３２ａとリンク構造体２３ｂとに基づいて論理回路の機能を表す状態遷移グラフデータを作成する。また、状態遷移グラフ作成部３２は、検証技術者２によって仕様記述データ１０ａが修正されることによって、使用されなくなった状態遷移部分について「使用しない」マーク（×）を付加して状態遷移グラフデータを更新する。
【００１７】
矛盾抽出部３４は、仕様記述データ１０ａに基づく論理回路の状態遷移に矛盾がないかを解析する処理部であり、矛盾があった場合に矛盾情報構造体３４ａを作成する矛盾情報作成部３５を有する。矛盾抽出部３４は、状態遷移グラフ作成部３２によって作成された状態遷移グラフデータ３２ａから論理的な矛盾がないかを解析し、矛盾を検出すると、仕様矛盾項目情報３４ａによって状態遷移の矛盾を示す仕様矛盾項目ファイル３４ｆを作成して記憶領域に出力し、そして、検証技術者２に矛盾が存在することを通知する。
【００１８】
検証技術者２は、仕様矛盾項目ファイル３４ｆを解析して、仕様記述作成部１０を実行させて、仕様記述データ１０ａを修正して更新する。
【００１９】
検証項目作成部３７は、検証すべき項目を示す検証項目構造体３７ａを作成して、検証項目構造体３７ａに基づいて処理の実行可否を明示的に記載した検証項目を検証項目ファイル３７ｆに出力する処理部であって、矛盾部検証項目作成部３８と、エッジ部検証項目作成部３９とを有する。
【００２０】
検証項目作成部３７は、矛盾情報構造体３４ａを用いて、「使用しない」マーク（×）が付加された状態遷移部分に対して、処理の実行可否を明示的に表現した検証項目の作成の要否を判断し、作成要の場合に「使用しない」マーク（×）が付加された状態遷移部分を「処理を実行しない」と明示的に記載した検証項目として書き出すために「処理を実行しない」フラグ（黒丸）を矛盾情報構造体３４ａに設定する。処理の実行可否を明示的に表現した検証項目の作成が不要の場合、検証項目作成部３７ａは、「使用しない」マーク（×）に基づいて検証項目は作成しない。
【００２１】
また、検証項目作成部３７は、「使用しない」マーク（×）が付されていない状態構造体３２ａに対して、状態構造体３２ａの内容に基づいて検証項目構造体３７ａを作成する。この場合、検証項目作成部３７は、「処理を実行しない」フラグ（黒丸）を付加することはない。又は、「処理を実行する」フラグを付加してもよい。
【００２２】
検証項目作成部３７は、更に、矛盾部検証項目作成部３８と、エッジ部検証項目作成部３９とによって、夫々で検証項目構造体３７ａを作成し、その検証項目構造体３７ａに基づいて検証項目を検証項目ファイル３７ｆへ出力させる。
【００２３】
矛盾部検証項目作成部３８は、矛盾情報構造体３７ａを用いて、矛盾する箇所の検証項目構造体３７ａを作成して、その検証項目構造体３７ａに基づいて検証項目を検証項目ファイル３７ｆへ出力する。
【００２４】
エッジ部検証項目作成部３９は、状態構造体３２ａを用いて、矛盾情報構造体３７ａ以外について検証項目構造体３７ａを作成して、その検証項目構造体３７ａに基づいて検証項目を検証項目ファイル３７ｆへ出力する。
【００２５】
テストデータ作成部８０は、検証項目抽出部３０によって作成された検証項目情報３７ａを用いて、検証技術者２によるテストベンチ及びテストパターンの作成を支援する処理部であり、回路をシミュレーションするための種々のテストデータ８０ａとして記憶領域に出力する。
【００２６】
論理シミュレータ９０は、テストデータ作成部８０によって作成されたテストデータ８０ａを読み込んで、設計された回路を検証するためのシミュレーションを実行する処理部である。
【００２７】
論理検証支援システム１００を実現する１乃至３のコンピュータ装置は、図３に示すようなハードウェア構成を有する。図３は、本発明の一実施例に係る論理検証支援システムを実現するコンピュータ装置のハードウェア構成を示す図である。
【００２８】
図３において、論理検証支援システム１００は、コンピュータによって制御される装置であって、ＣＰＵ（Central Processing Unit）１１と、メモリユニット１２と、表示ユニット１３と、出力ユニット１４と、入力ユニット１５と、通信ユニット１６と、記憶装置１７と、ドライバ１８とで構成され、システムバスＢに接続される。
【００２９】
ＣＰＵ１１は、メモリユニット１２に格納されたプログラムに従って論理検証支援システム１００を制御する。メモリユニット１２は、ＲＡＭ（Random Access Memory）及びＲＯＭ（Read-Only Memory）等にて構成され、ＣＰＵ１１にて実行されるプログラム、ＣＰＵ１１での処理に必要なデータ、ＣＰＵ１１での処理にて得られたデータ等を格納する。また、メモリユニット１２の一部の領域が、ＣＰＵ１１での処理に利用されるワークエリアとして割り付けられている。
【００３０】
表示ユニット１３は、ＣＰＵ１１の制御のもとに必要な各種情報を表示する。出力ユニット１４は、プリンタ等を有し、利用者からの指示に応じて各種情報を出力するために用いられる。入力ユニット１５は、マウス、キーボード等を有し、論理検証支援システム１００が処理を行なうための必要な各種情報を利用者が入力するために用いられる。
【００３１】
通信ユニット１６は、論理検証支援システム１００が例えばインターネット、ＬＡＮ（Local Area Network）等のネットワークを介する通信の制御をするための装置である。
【００３２】
記憶装置１７は、例えば、ハードディスクユニットにて構成され、各種処理を実行するプログラム等のデータを格納する。
【００３３】
論理検証支援システム１００よって行われる回路設計方法での処理を実現するプログラムは、例えば、ＣＤ−ＲＯＭ（Compact Disk Read-Only Memory）等の記憶媒体１９によって論理検証支援システム１００に提供される。即ち、プログラムが保存された記憶媒体１９がドライバ１８にセットされると、ドライバ１８が記憶媒体１９からプログラムを読み出し、その読み出されたプログラムがシステムバスＢを介して記憶装置１７にインストールされる。そして、プログラムが起動されると、記憶装置１７にインストールされたプログラムに従ってＣＰＵ１１がその処理を開始する。
【００３４】
尚、プログラムを格納する媒体としてＣＤ−ＲＯＭに限定するものではなく、コンピュータが読み取り可能な媒体であればよい。本発明に係る処理を実現するプログラムは、通信ユニット１６によってネットワークを介してダウンロードし、記憶装置１７にインストールするようにしても良い。また、論理検証支援システム１００が外部との接続を行うＵＳＢ（Universal Serial Bus）等のインタフェースを有する場合には、ＵＳＢ接続によって外部記憶媒体からプログラムを読み込んでもよい。
【００３５】
次に、仕様記述作成部１０が、検証技術者２が入力されたデータから作成する仕様記述データ１０ａの例について図４で説明する。図４は、仕様記述データの例を示す図である。
【００３６】
図４において、仕様記述データ１０ａは、入力データ定義部１０ａ−２と、処理内容定義部１０ａ−４とを有する。
【００３７】
データ定義部１０ａ−２には、入力データの有効範囲が示される。この場合、１バイトのデータ入力が成されることを示す「0x00」から「0xff」までを有効データの範囲として定義している。
【００３８】
また、特別な処理を実行する、或いは処理状態の遷移を行わせる入力（マーク）種別を定義し、特別な処理実行する状態の定義、開示条件、終了条件とその状態で入力できる値の制約で定義する。例えば、マークＡは入力データ「0xfe」で定義され、マークＢは入力データ「0xff」で定義されている。また、状態遷移定義では、「状態Ａ」へと遷移するための開示条件がマークＡであり、「状態Ａ」から遷移するための終了条件がマークＢであり、入力値制約はないことが定義されている。
【００３９】
処理内容定義部１０ａ−４には、入力データ定義部１０ａ―２で定義される各データの入力時に実行すべき処理、入力データ定義部１０ａ―２で定義される状態遷移定義で実行すべき処理が定義される。この場合、「通常処理」の欄では、初期状態から「入力データ定義部」で定義されたマーク又はマークにより遷移した状態のいずれにも合致しない場合の処理が存在することを示している。各処理の「：」の右には任意の値を複数個記載可能である。この場合、状態Ａで処理（α）を実行し、マークＢの入力によって処理（β）を実行することが定義されている。
【００４０】
この時点では、このようにして作成された仕様書記述データ１０ａには、矛盾が含まれていてもよい。従って、検証技術者２は、思いつく項目を書き出すことができる。本実施例では、一般に、規格や仕様を理解する際、間違った解釈をすることが多い箇所に論理障害が多くなるため、論理検証支援システム１００ではあえて矛盾した止揚を受付けて、以下に説明されるように、矛盾を指摘すると共に、論理検証の際に注意すべき点であるとして仕様書内のその矛盾した箇所の情報は全て保存される。
【００４１】
仕様書記述データ１０ａは仕様書記述解析部３１によって解析され、状態リスト３１ａと入力データリスト３１ｂとに分けられて記憶領域に格納される。状態リスト３１ａには、状態遷移定義で定義される、例えば、初期状態としての「通常状態」、「状態Ａ」などの状態名と、状態遷移するための条件（以下、状態遷移条件という）と、処理内容定義部で定義される内容とが含まれる。入力データリスト３１ｂには、有効データと、マーク名と、マークとして認識される値とが含まれる。
【００４２】
そして、状態遷移グラフ作成部３２によって状態構造体３２ａ及びリンク構造体３２ｂが作成される。図５は、状態遷移グラフ作成処理を説明するためのフローチャート図である。図５において、状態遷移グラフ作成部３２は、状態リスト３１ａを参照して、状態毎にその状態を示す構造体を状態構造体３２ａとして記憶領域に作成する（ステップＳ１３１）。この場合、仕様修正などによって、既に状態構造体３２ａが作成されている場合、その存在している状態構造体３２ａを採用して別の記憶領域に格納する。
【００４３】
状態遷移グラフ作成部３２は、入力データリスト３１ｂを参照して、状態への遷移条件毎に状態遷移を示す構造体をリンク構造体３２ｂとして作成する（ステップＳ１３２）。遷移条件と、実行すべき処理を示す処理名とをリンク構造体３２ｂに設定し、その遷移元と遷移先との状態構造体にポインタで接続する（ステップＳ１３３）。
【００４４】
また、状態遷移グラフ作成部３２は、仕様修正によって存在しなくなった状態構造体及びリンク構造体に「使用しない」マーク（×）を付加して、そのまま記憶領域に保存しておく（ステップＳ１３４）。存在しなくなった状態構造体は、前回から記憶領域に保存されている状態構造体３２ａと、今回採用した状態構造体３２ａとの差分で取得し、差分となった状態構造体３２ａに「使用しない」マーク（×）を付加して今回採用の状態構造体３２ａとして記憶領域に格納すればよい。存在しなくなったリンク構造体についても同様である。「使用しない」マーク（×）の付与は、状態構造体３２ａ及びリンク構造体３２ｂ内の要素として備え、「使用しない」ことを示す情報を設定するようにすればよい。
【００４５】
次に、矛盾抽出部３４によって矛盾情報構造体３４ａ及び使用矛盾項目ファイル３４ｆが作成される。図６は、矛盾抽出処理を説明するためのフローチャート図である。
【００４６】
図６において、矛盾抽出部３４は、記憶領域から状態遷移グラフ作成部３２によって作成された状態構造体３２ａを順に１つ読み出して、入力データリスト３１ａを参照して、状態構造体３２ａに接続元として接続されたリンク構造体３２ｂに対して、そのリンク構造体３２ｂの遷移条件を含む遷移条件を持つリンク構造体３２ｂが既に記憶領域に格納されているか否かを確認する（ステップＳ１４１）。例えば、遷移条件の「マークＡ以外（0xfe以外）」と「マークＢ（0xff）」とは互いに排他とはならない関係となるリンク構造体３２ｂ同士であるか否かを確認すればよい。
【００４７】
ステップＳ１４１では、状態構造体３２ａ及びリンク構造体３２ｂには、仕様修正によって「使用しない」マーク（×）が付与されているものも含めて確認を行なう。
【００４８】
同じ遷移条件が存在しない場合（ステップＳ１４２のＮＯ）、矛盾抽出部３４は、入力データリスト３１ａを参照して、状態構造体３２ａへのポインタと、その状態構造体に接続元として接続されたリンク構造体３２ｂの遷移条件に設定する値と、関連するリンク構造体３２ｂへのポインタとを記憶領域に格納する（ステップＳ１４３）。
【００４９】
一方、同じ遷移条件が存在する場合（ステップＳ１４２のＹＥＳ）、矛盾抽出部３４は、処理中の状態構造体３２ａへのポインタと、既にある値と関連したリンク構造体３２ｂへのポインタと、著利中のリンク構造体３２ｂへのポインタと、矛盾した値の集合とを示す矛盾情報構造体３４ａを作成して、図７に示すような矛盾情報保存部４１に保存する（ステップＳ１４２−２）。また、矛盾抽出部３４は、矛盾情報構造体３４ａへのポインタを図７に示すような矛盾情報保存部４１に保存する（ステップＳ１４２−４）。
【００５０】
図７を参照すると、矛盾情報保存部４１には、ポインタ領域４１ａと、矛盾情報構造体３４ａと、矛盾した遷移条件を示す値集合４１ｓとが保存される。ポインタ領域４１ａには、作成された矛盾情報構造体３４ａへのポインタが順次格納される。矛盾情報構造体３４ａは、矛盾するリンク構造体３２ｂが存在する状態構造体３２ａへのポインタと、同じ値を持つリンク構造体３２ｂの夫々のポインタと、入力データリスト３１ａを参照することによって同一の値となる遷移条件の記述を示す値集合４１ｓ等の要素で構成される。
【００５１】
例えば、遷移条件の記述「マークＡ以外」と遷移条件の記述「マークＢ」とは、入力データリスト３１ｂを参照することによって、同じ値「0xff」となり、値集合４１ｓには、「マークＡ以外」と「マークＢ」とが設定される。
【００５２】
矛盾情報保存部４１で保存される矛盾情報構造体３４ａからポインタによって参照される状態構造体３２ａとリンク構造体３２ｂとには、仕様修正によって「使用しない」マーク（×）が付加されている構造体が存在していてもよい。
【００５３】
図６に戻って、矛盾抽出部３４は、状態構造体３２ａを全て処理したか否かを判断する（ステップＳ１４４）。全て処理していない場合、矛盾抽出部３４は、ステップＳ１４１へ戻って、上記同様の処理を繰り返す。
【００５４】
一方、全て処理している場合、矛盾抽出部３４は、矛盾情報保存部４１に保存されている矛盾情報構造体３４ａ夫々について仕様矛盾項目を作成し、仕様矛盾項目ファイル３４ｆとして出力する（ステップＳ１４５）。そして、矛盾抽出部３４は、仕様矛盾項目ファイル３４ｆを検証技術者２へ通知して（ステップＳ１４６）、矛盾抽出処理を終了する。
【００５５】
状態遷移グラフ作成部３２と矛盾抽出部３４と処理による状態遷移グラフが作成される過程と仕様矛盾項目ファイル３４ｆが作成される過程を図８で説明する。図８は、矛盾項目抽出までの過程を示す図である。
【００５６】
図８において、状態遷移グラフ作成部３２は、状態リスト３１ａを入力して、状態遷移グラフ５０中の状態を作成する（ステップＳ１１）。ここでは、「状態」として通常処理と状態Ａとを示す状態構造体３２ａが作成される。
【００５７】
状態遷移グラフ作成部３２は、入力データリスト３１ｂを参照して、仕様記述中の状態への遷移条件それぞれについて「状態遷移」を示すエッジを設定する（ステップＳ１２）。「状態遷移」を示すエッジは、リンク構造体３２ｂで示される。状態遷移グラフ５１では、マークＡに係る入力（マークＡの入力及びマークＡ以外の入力）によって成される、通常処理状態と状態Ａとの間の状態遷移、通常処理状態内での状態遷移、及び状態Ａ内での状態遷移を追加した様子を示している。状態遷移グラフ５２では、マークＢに係る入力（マークＢの入力）によって成される、通常処理状態内での状態遷移、及び状態Ａ内での状態遷移を追加した様子を示している。
【００５８】
次に、矛盾抽出部３４は、状態遷移グラフ作成部３２によって作成された状態遷移グラフ５２上の各状態からの遷移について、遷移条件間に矛盾が無いかをチェックする（ステップＳ１３）。状態遷移グラフ５３では、状態遷移グラフ作成部３２によって作成された状態遷移グラフ５２内において矛盾のある遷移条件（エッジ）を点線で示している。矛盾のある遷移条件（エッジ）に係わる状態構造体３２ａとリンク構造体３２ｂとが矛盾状態構造体３４ａで特定される。
【００５９】
そして、矛盾抽出部３４は、矛盾点を所定形式のファイルに出力して、検証技術者２に通知し、論理検証支援システム１００内にも保存する（ステップＳ１４）。仕様矛盾項目ファイル３４ｆは、例えば、矛盾点毎に、遷移元、遷移先、遷移条件の項目があり、それらに値が対応づけられている。
【００６０】
状態遷移グラフ５３に示される矛盾５８に対して、遷移元に「通常処理」状態が設定され、「通常処理」状態で２つのエッジ間で矛盾があったため遷移先に「通常処理」状態、「通常処理」状態のように繰り返して設定され、遷移条件にマークＡ以外、マークＢのようにエッジ毎に値が設定される。更に、状態遷移グラフ５３に示される矛盾５９に対して、遷移元に「状態Ａ」が設定され、「状態Ａ」で２つのエッジ間で矛盾があったため遷移先に「状態Ａ」、「状態Ａ」のように繰り返して設定され、遷移条件にマークＡ以外、マークＢのようにエッジ毎に値が設定される。
【００６１】
このような仕様矛盾項目ファイル３４ｆを参照して、検証技術者２は仕様記述データ１０ａを修正すると、仕様記述解析部３１、状態遷移グラフ作成部３２、矛盾抽出部３５による上述した処理が実行され、修正されて使用しないことになった部分には、「使用しない」マーク（×）が付加される。
【００６２】
更に、論理検証支援システム１００では、検証項目作成部３７によって検証項目が記述される検証項目ファイル３７ｆが作成される。図９は、検証項目作成処理を説明するためのフローチャート図である。図９において、検証項目作成部３７は、図６のステップＳ１４３にて状態遷移グラフ作成部３２によって記憶領域に格納されたポインタで関連付けられている状態構造体３２ａとリンク構造体３２ｂとの組み合わせを順次取得する（ステップＳ１５１）。
【００６３】
検証項目作成部３７は、矛盾情報保存部４１に格納されていて、リンク構造体３２ｂに「使用しない」マーク（×）が付与されていて、他の遷移条件の一部でありその処理内容が相違し、かつ、同一の遷移条件を持つリンク構造体３２ｂが存在しないことを確認する（ステップＳ１５２）。ステップＳ１５２の条件が成立する場合、検証項目作成部３７は、処理の実行可否を明示的に記載することを示す「処理を実行しない」フラグの設定が必要であると判断する。一方、ステップＳ１５２の条件が成立しない場合、検証項目作成部３７は、「処理を実行しない」フラグの設定は不要であると判断する。
【００６４】
ステップＳ１５２での確認によって「処理を実行しない」フラグの設定が必要か否かを判断する（ステップＳ１５３）。「処理を実行しない」フラグの設定が必要であると判断すると、そして、検証項目作成部３７は、状態構造体３２ａと、「処理を実行しない」フラグを付与したリンク構造体３２ｂとを格納して（ステップＳ１５３−４）、ステップＳ１５７へと進む。
【００６５】
一方、ステップＳ１５２での確認によって「処理を実行しない」フラグの設定が不要であると判断すると、検証項目作成部３７は、ステップＳ１５２を満たさない場合であって、状態構造体３２ａに「使用しない」マーク（×）が設定されている組み合わせか否かを判断する（ステップＳ１５４）。状態構造体３２ａに「使用しない」マーク（×）が設定されている組み合わせの場合、検証項目作成部３７は、検証項目構造体３７ａを作成することなく、ステップＳ１５７へと進む。
【００６６】
一方、ステップＳ１５４にて、状態構造体３２ａに「使用しない」マーク（×）が設定されていない組み合わせである場合、検証項目作成部３７は、「処理を実行しない」フラグを付与することなく、状態構造体３２ａと、リンク構造体３２ｂとを記憶領域に格納する（ステップＳ１５６）。
【００６７】
検証項目作成部３７は、全ての組み合わせを処理したか否かを判断する（ステップＳ１５７）。全ての組み合わせを処理していない場合、検証項目作成部３７は、ステップＳ１５１へ戻り、上記同様の処理を繰り返す。一方、全ての組み合わせを処理した場合、検証項目作成部３７は、記憶領域内に格納された検証項目構造体３７ａに基づいて検証項目を記述し、検証項目ファイル３７ｆへ出力する（ステップＳ１５８）。
【００６８】
検証項目の記述するために、記憶領域から順に検証項目構造体３７ａを取得して、その検証項目構造体３７ａから状態構造体３２ａを取得して、その状態構造体３２ａに設定されている状態名を取得する。また、その検証項目構造体３７ａからリンク構造体３２ｂを取得して、そのリンク構造体３２ｂに設定されている遷移条件と「処理を実行しない」フラグの有無を取得する。取得した状態名と、遷移条件と、「処理を実行しない」フラグの有無とによって、「処理を実行しない」フラグ有りの場合、「状態名：遷移条件：処理実行が検出されたら論理障害」を意味するように記述し、「処理を実行しない」フラグ無しの場合、「状態名：遷移条件：処理実行が検出されなかったら論理障害」を意味するように記述して検証項目ファイル３７ｆへ出力することによって、検証項目表が検証項目ファイル３７ｆ内に作成される。
【００６９】
検証項目作成部３７によって行われる検証項目表作成処理について図１０、図１１及び図１２で説明する。図１０は、検証項目表作成処理の概要を説明するためのフローチャート図である。図１０において、検証項目作成部３７は、状態遷移グラフ作成部３２によって作成された状態遷移グラフで示される処理毎に値を割り振る（ステップＳ２０１）。例えば、通常処理に対して「００１」、処理（α）に対して「０１０」、処理（β）に対して「１００」の値を割り振る。
【００７０】
そして、検証項目作成部３７は、状態遷移グラフの未選択の「状態」を一つ選択し（ステップＳ２０２）、選択できたか否かを判断する（ステップＳ２０３）。未選択の「状態」がなく選択できなかった場合、検証項目作成処理を終了する。
【００７１】
一方、未選択の「状態」があり選択できた場合、その選択した「状態」を状態構造体３２ａとして持つ、未選択の矛盾情報構造体３４ａを矛盾情報保存部４１から取得し（ステップＳ２０４）、未選択の矛盾情報構造体３４ａを取得できたか否かを判断する（ステップＳ２０５）。未選択の矛盾情報構造体３４ａがなく取得できなかった場合、検証項目作成部３７は、ステップＳ２０７へと進む。
【００７２】
一方、未選択の矛盾情報構造体３４ａが存在して取得できた場合、検証項目作成部３７は、矛盾部検証項目作成部３８によって図１１で説明される矛盾情報構造体３４ａを用いた検証項目作成処理を実行する（ステップＳ２０６）。
【００７３】
そして、検証項目作成部３７は、ステップＳ２０２で選択した「状態」を始点とするエッジで未選択のものから一つ選択し（ステップＳ２０７）、選択できたか否かを判断する（ステップＳ２０８）。エッジは、状態遷移グラフにおいて状態から他の状態又は自身への状態遷移部分を意味し、リンク構造体３２ｂで示される部分である。未選択のエッジがなく選択できなかった場合、検証項目作成部３７は、ステップＳ２０２へと戻り、上記同様の処理を繰り返す。
【００７４】
一方、未選択エッジを選択できた場合、検証項目作成部３７は、エッジ部検証項目作成部３９によって図１２で説明されるステップＳ２０７で選択したエッジに対する検証項目作成処理を実行して（ステップＳ２０９）、検証項目作成部３７は、ステップＳ２０２へと戻り、上記同様の処理を繰り返す。ステップＳ２０９では、矛盾のないエッジに対して検証項目が作成される。
【００７５】
図１１は、図１０のステップＳ２０６における矛盾部検証項目作成部による矛盾情報構造体を用いた検証項目作成処理を説明するためのフローチャート図である。図１１において、矛盾部検証項目作成部３８は、矛盾情報構造体３４ａからポイントされるリンク構造体３２ｂから順に未選択のリンク構造体（Ａ）を選択し、その選択したリンク構造体（Ａ）と同一の状態を遷移元として持つリンク構造体（Ｂ）からその遷移条件がリンク構造体（Ａ）の遷移条件を含む未選択のものを１つ選択して（ステップＳ２２１）、選択できたか否かを判断する（ステップＳ２２２）。リンク構造体（Ａ）の遷移条件とリンク構造体（Ｂ）の遷移条件とが一致する場合も「遷移条件を含む」とする。
【００７６】
未処理のリンク構造体（Ｂ）が存在し選択できた場合、矛盾部検証項目作成部３８は、リンク構造体（Ａ）について、その処理に割り振られた値と、それと矛盾するリンク構造体（Ｂ）の処理に割り振られた値の論理積を計算する（ステップＳ２２３）。
【００７７】
例えば、後述される図１３に示される状態遷移グラフ６１内の点線で示されるエッジ６１ｐが矛盾情報構造体３４ａからポイントされるリンク構造体３２ｂで示される矛盾となる遷移状態の１つである。状態Ａからの状態遷移を示すエッジ６１ｐは、「状態Ａの時、マークＢが入力されたら処理（β）を実行する」ことを示し、処理（β）を実行するため値「１００」が割り振られている。エッジ６１ｐには値「１００」を反転させて値「０１１」を取得する。
【００７８】
一方、同一の状態Ａからの他の状態遷移を示すエッジ６１ｑは、「状態Ａの時、Ａ以外のマーク（マークＢ）が入力されたら処理（α）を実行する」ことを示し、処理（β）を実行するため値「０１０」が割り振られている。
【００７９】
従って、値「０１１」と値「０１０」との論理積は、「０１０」となり非０（ゼロ）の値となる。その場合、検証項目の記述対象として考慮する。
【００８０】
矛盾部検証項目作成部３８は、論理積の値が非０（ゼロ）であるか否かを判断する（ステップＳ２２４）。論理積の値が非０（ゼロ）である場合、矛盾部検証項目作成部３８は、「使用しない」マーク（×）が付加されていないリンク構造体（エッジ）である、又は、「使用しない」マーク（×）及び「処理を実行しない」フラグ（黒丸）が付加されているリンク構造体（エッジ）である場合に、検証項目構造体３７ａを作成して記憶領域に保存し（ステップＳ２２５）、ステップＳ２２１へと進み、上記同様の処理を繰り返す。一方、論理積の値が０（ゼロ）である場合、矛盾部検証項目作成部３８は、ステップＳ２２１へと進み、上記同様の処理を繰り返す。
【００８１】
検証項目構造体３７ａは、ポインタで関連付けられている状態構造体３２ａとリンク構造体３２ｂとの組み合わせを特定する要素で構成される。例えば、検証項目構造体３７ａには、状態構造体３２ａへのポインタと、リンク構造体３２ｂへのポインタなどが設定される。
【００８２】
一方、ステップＳ２２６において、矛盾部検証項目作成部３８は、未処理のリンク構造体（Ｂ）が存在せず選択できなかった場合、記憶領域に保存されている検証項目構造体３７ａに基づいて検証項目を記述して検証項目ファイル３７ｆに出力し（ステップＳ２２６）、矛盾情報構造体を用いた検証項目作成処理を終了する。検証項目の記述後、記憶領域に保存されている検証項目構造体３７ａを削除しておく。
【００８３】
ステップＳ２２６において、検証項目は、例えば下記の記述形式で書き出される。(  )内に検証項目構造体３７ｆから取得した値が書き込まれる。
【００８４】
「処理を実行しない」フラグが付加されていない場合、『（状態名）時、（遷移条件）入力、（処理内容）すること』と記述する。一方、「処理を実行しない」フラグが付加されている場合、『（状態名）時、（遷移条件）入力、（処理内容）しないこと』と記述する。このように記述することによって、元々矛盾すると判断された状態遷移グラフ中のエッジに対して、処理していることを確認するのか、処理してはいけないことを確認するのかを明示的に検査項目として示すことができる。
【００８５】
図１２は、図１０のステップＳ２０９におけるエッジ部検証項目作成部３９による矛盾のないエッジに対する検証項目作成処理を説明するためのフローチャート図である。図１２において、エッジ部検証項目作成部３９は、図１０のステップＳ２０２で選択した「状態」を示す状態構造体３２ａと、ステップＳ２０７で選択した「エッジ」を示すリンク構造体３２ｂとに基づいて、検証項目構造体３７ｆを作成して記憶領域に格納する（ステップＳ２４１）。
【００８６】
エッジ部検証項目作成部３９は、記憶領域に保存されている検証項目構造体３７ａに基づいて検証項目を記述して検証項目ファイル３７ｆに出力し（ステップＳ２４３）、矛盾のないエッジに対する検証項目作成処理を終了する。
【００８７】
ステップＳ２４３において、検証項目は、例えば『（状態名）時、（遷移条件）入力、（処理内容）すること』の記述形式で書き出される。(  )内に検証項目構造体３７ｆから取得した値が書き込まれる。
【００８８】
図１３は、矛盾を含む状態遷移グラフから作成される検証項目の記述例を示す図である。図１３において、状態遷移グラフ６１は、図８の状態遷移グラフ５３に含まれる矛盾５８及び５９が検証技術者２によって修正された状態を示している。従って、状態遷移グラフ６１において、矛盾５８として検出されたエッジ６１ｍと、矛盾５９として検出されたエッジ６１ｐとには「使用しない」マーク（×）が付与されている。また、検証技術者２によって、エッジ６１ａが追加されている。更に、検証項目作成部３７によって「処理を実行しない」フラグ（黒丸）が矛盾５９として検出されたエッジ６１ｐに付与されている。
【００８９】
このような状態遷移グラフ６１に基づく検証項目は、検証項目ファイル３７ｆに書き出され、例えば、エッジ６１ａに対して検証項目『通常処理時、マークＡ以外かつマークＢ以外入力、通常処理を実行すること』が記述され、エッジ６１ｎに対して検証項目『通常処理時、マークＢ入力、処理（β）を実行すること』が記述され、エッジ６１ｃに対して検証項目『マークＡ入力、処理（α）を実行し、状態Ａに遷移すること』が記述され、エッジ６１ｑに対して検証項目『状態Ａ時、マークＡ以外入力、処理（α）を実行すること』が記述され、エッジ６１ｐに対して検証項目『状態Ａ時、マークＢ入力、処理（β）を実行しないこと』が記述され、エッジ６１ｅに対して検証項目『状態Ａ時、マークＡ入力、処理（α）を実行し、通常処理状態に遷移すること』が記述される。
【００９０】
ここで、エッジ６１ｐは検証技術者２よる修正によって使用しないことになっているが、『状態Ａ時、マークＢ入力、処理（β）を実行しないこと』と記述されることによって明示的に示されることにより、より確実な検証を行なうことができる。
【００９１】
上述したように、本実施例では、一般的に、規格や使用を理解する際、間違った解釈をすることが多い箇所に論理障害が多くなるため、論理検証支援システム１００ではあえて矛盾した仕様を受け付けて、矛盾を指摘すると共に、論理検証の際に注意すべき点であるとしてその矛盾した箇所の情報を全て保存する。
【００９２】
指摘を受けた検証技術者２により最終的に矛盾のない仕様書記述データ１０ａを得た場合であっても、それまでに保存しておいた矛盾内容と、状態遷移グラフを生成するために元になる状態構造体３２ａとリンク構造体３２ｂと矛盾情報構造体３４ａとを用いて、検証項目を記述する。
【００９３】
検証技術者は、検証項目ファイル３７ｆに基づいて論理検証用のテストパターンを作成し、テストパターンを含むテストデータ８０ａが出力される。テストデータ８０ａを用いて論理シミュレーションを実行し、その実行結果からそれぞれの検証項目に従って期待された動作と一致したかを確認する。
【００９４】
上述した実施例において、使用記述解析方法（Ｐａｒｓｅｒの実現方法）、状態遷移グラフの生成については、例えば、「Ｃ−データ構造とプログラム−」、Leendert Ammerral、オーム社、１９９０年、及び、"Lex & Yacc"、J.R.Levine、Oreilly Associates Inc.、１９９２年を参照すればよい。
【００９５】
以上の説明に関し、更に以下の項を開示する。
（付記１）
論理回路を検証するための検証項目を作成する論理検証支援システムであって、
前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手段を有することを特徴とする論理検証支援システム。
（付記２）
前記矛盾抽出手段は、前記矛盾箇所となった前記状態情報と前記状態遷移情報とを矛盾情報を用いて矛盾項目を作成して検証技術者へ通知することを特徴とする付記１記載の論理検証支援システム。
（付記３）
前記矛盾抽出手段は、前記矛盾箇所となった前記状態情報と前記状態遷移情報とを矛盾項目情報として矛盾情報保存領域に保存することを特徴とする付記１又は２記載の論理検証支援システム。
（付記４）
前記矛盾抽出手段によって抽出された前記矛盾箇所を含めて前記状態情報と前記状態遷移情報とを用いて検証項目を作成する検証項目作成手段を有することを特徴とする付記１記載の論理検証支援システム。
（付記５）
前記論理回路の動作を規定する仕様記述データに従って、状態遷移グラフ作成に係る前記状態情報と前記遷移条件情報とを作成すると共に、該仕様記述データの修正によって使用しなくなった状態情報と遷移条件情報とに使用しないマークを付加して削除することなく保存する状態遷移グラフ作成手段を有することを特徴とする付記４項記載の論理検証支援システム。
（付記６）
前記検証項目作成手段は、前記使用しないマークが付加されている前記状態遷移情報で示される処理を実行しないと判断した場合、該状態遷移情報に処理を実行しないフラグを付加することを特徴とする付記５記載の論理検証支援システム。
（付記７）
前記検証項目作成手段は、前記使用しないマーク及び前記処理を実行しないフラグが付加されている状態遷移情報に対して、該状態遷移情報で示される処理が実行されないことを明示的に示す検証項目を作成することを特徴とする付記６記載の論理検証支援システム。
（付記８）
前記検証項目作成手段は、
前記矛盾箇所に係る前記状態情報と前記状態遷移情報とを用いて該矛盾箇所に関して検証すべき第一検証項目を作成する第一検証項目作成手段と、
前記矛盾が検出されない前記状態情報と前記状態遷移情報とを用いて検証すべき第二検証項目を作成する第二検証項目作成手段とを有することを特徴とする付記４乃至８のいずれか一項記載の論理検証支援システム。
（付記９）
コンピュータが論理回路を検証するための検証項目を作成する論理検証支援方法であって、該コンピュータに、
前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手順を実行させることを特徴とする論理検証支援方法。
（付記１０）
論理回路を検証するための検証項目を作成する論理検証支援処理をコンピュータに実行させるプログラムであって、該コンピュータに、
前記論理回路の動作における該論理回路の状態を示す状態情報毎に、遷移元状態から遷移先状態の遷移を示す状態遷移情報によって示される遷移条件が他状態遷移情報の遷移条件に含まれる場合に矛盾箇所として抽出する矛盾抽出手順を実行させることを特徴とする論理検証支援方法。
【図面の簡単な説明】
【００９６】
【図１】従来の検証項目作成方法を説明するための図である。
【図２】本発明の一実施例に係る論理検証システムの機能構成を示す図である。
【図３】本発明の一実施例に係る論理検証支援システムを実現するコンピュータ装置のハードウェア構成を示す図である。
【図４】仕様記述データの例を示す図である。
【図５】状態遷移グラフ作成処理を説明するためのフローチャート図である。
【図６】矛盾抽出処理を説明するためのフローチャート図である。
【図７】矛盾情報保存部の例を示す図である。
【図８】矛盾項目抽出までの過程を示す図である。
【図９】検証項目作成処理を説明するためのフローチャート図である。
【図１０】検証項目表作成処理の概要を説明するためのフローチャート図である。
【図１１】図１０のステップＳ２０６における矛盾部検証項目作成部による矛盾情報構造体を用いた検証項目作成処理を説明するためのフローチャート図である。
【図１２】図１０のステップＳ２０９におけるエッジ部検証項目作成部３９による矛盾のないエッジに対する検証項目作成処理を説明するためのフローチャート図である。
【図１３】矛盾を含む状態遷移グラフから作成される検証項目の記述例を示す図である。
【符号の説明】
【００９７】
２            検証技術者
１０          仕様記述作成部
１０ａ        仕様記述データ
１１          ＣＰＵ
１２          メモリユニット
１３          表示ユニット
１４          出力ユニット
１５          入力ユニット
１６          通信ユニット
１７          記憶装置
１８          ドライバ
１９          記憶媒体
２０          ＬＳＩ
３０          検証項目抽出部
３１          仕様記述解析部
３１ａ        状態リスト
３１ｂ        入力データリスト
３２          状態遷移グラフ作成部
３２ａ        状態構造体
３２ｂ        リンク構造体
３４          矛盾抽出部
３４ｆ        仕様矛盾項目ファイル
３５          矛盾情報作成部
３７          検証項目作成部
３７ａ        検証項目構造体
３７ｆ        検証項目ファイル
３８          矛盾部検証項目作成部
３９          エッジ部検証項目作成部
８０          テストデータ作成部
８０ａ        テストデータ
９０          論理シミュレータ
【図１】
2008204371.tif 000003
【図２】
2008204371.tif 000004
【図３】
2008204371.tif 000005
【図４】
2008204371.tif 000006
【図５】
2008204371.tif 000007
【図６】
2008204371.tif 000008
【図７】
2008204371.tif 000009
【図８】
2008204371.tif 000010
【図９】
2008204371.tif 000011
【図１０】
2008204371.tif 000012
【図１１】
2008204371.tif 000013
【図１２】
2008204371.tif 000014
【図１３】
2008204371.tif 000015