論理検証方法
【課題】本発明の課題は、検証プロパティと波形とを連動させて、一方を部分的に選択すると対応する他方の部分が視覚的に判別可能な様に表示する論理検証方法を提供すことを目的とする。
【解決手段】上記課題は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、前記検証プロパティを表示するプロパティ表示手順とを実行させ、操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順と、前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法により達成される。
【解決手段】上記課題は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、前記検証プロパティを表示するプロパティ表示手順とを実行させ、操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順と、前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法により達成される。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理回路などの論理検証によって発見される検証プロパティ違反を波形上で解析する際に解析を容易化する論理検証方法に関する。
【背景技術】
【０００２】
従来より、論理回路などを設計する際には、設計対象の機能やタイミングなどが仕様を満たしているか否かを検証する論理検証と呼ばれる作業が行われている。論理検証では仕様を満たしているか否かを確認するために検証プロパティを作成し、検証プロパティを満たしているか否かをチェックするためのチェッカを組み込んだ環境で検証を行っている。一般に、検証プロパティ違反が発見された場合は波形を見ることで違反の原因を解析する手法が取られている。しかしながら、波形から違反の原因を特定するためには、経験と知識を要し容易に原因を特定できるものではなかった。
【０００３】
そこで、波形を用いた解析を容易とするために、検証結果に基づいてエラーメッセージ８０を表示すると共に、注釈情報付き波形データに格納されている信号値の期待値に基づいて、期待される信号波形が実際の波形に重ねて表示し、注釈情報付き波形データに格納されているイベントの情報に基づいて、イベントの論理的関係を示す矢印記号を表示することが提案されている（例えば、特許文献１参照。）。
【特許文献１】特開２００４−３２６５５０号公報（第８図）
【特許文献２】特開２００３−２１６６８３号公報
【特許文献３】特開２００１−２０９６６８号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかしながら、上記従来の論理検証方法では、ユーザは検証プロパティの記述と波形との対応に関する知識を要し、検証プロパティを頭の中に記憶しておいて表示装置に表示された波形との対応で解析を行う必要があった。検証プロパティが複雑な場合、また、信号線が多い場合では、検証プロパティと違反波形との対応関係を頭の中で構築することは困難な場合があり、また解析の際に間違いを生じやすい。
【０００５】
よって、本発明の目的は、検証プロパティと波形とを連動させて、一方を部分的に選択すると対応する他方の部分が視覚的に判別可能なように表示する論理検証方法を提供することである。
【課題を解決するための手段】
【０００６】
上記課題を解決するため、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、前記検証プロパティを表示するプロパティ表示手順と、操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させるように構成される。
【０００７】
また、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、前記波形データに基づいて生成された波形を表示する波形表示手順と、操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させるように構成される。
【０００８】
更に、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定するように構成される。
【０００９】
上記課題を解決するための手段として、本発明は、上記手順をコンピュータに実行させるためのプログラム、そのプログラムを記憶したコンピュータ読み取り可能な記憶媒体、及び、該プログラムによって上記手順を実行する論理検証装置とすることもできる。
【発明の効果】
【００１０】
本願発明は、検証プロパティと波形とを連動させて表示し、一方を部分的に選択すると対応する他方の部分が視覚的に容易に判別可能なようにし、検証プロパティと違反波形との対応関係を容易とすることによって、検証プロパティ違反の解析を容易に正確に行なうことができる。
【発明を実施するための最良の形態】
【００１１】
以下、本発明の実施の形態を図面に基づいて説明する。
【００１２】
本発明に係る論理検証方法を実現する論理検証装置は、コンピュータ装置であって、図１に示すようなハードウェア構成を有する。図１は、本発明の一実施例に係る論理検証装置のハードウェア構成を示す図である。
【００１３】
図１において、論理検証装置１００は、コンピュータによって制御される装置であって、ＣＰＵ（Central Processing Unit）１１と、メモリユニット１２と、表示ユニット１３と、入力ユニット１５と、記憶装置１７と、ドライバ１８とで構成され、システムバスＢに接続される。
【００１４】
ＣＰＵ１１は、メモリユニット１２に格納されたプログラムに従って論理検証装置１００を制御する。メモリユニット１２は、ＲＡＭ（Random Access Memory）及びＲＯＭ（Read-Only Memory）等にて構成され、ＣＰＵ１１にて実行されるプログラム、ＣＰＵ１１での処理に必要なデータ、ＣＰＵ１１での処理にて得られたデータ等を格納する。また、メモリユニット１２の一部の領域が、ＣＰＵ１１での処理に利用されるワークエリアとして割り付けられている。
【００１５】
表示ユニット１３は、ＣＰＵ１１の制御のもとに必要な各種情報を表示する。入力ユニット１５は、マウス、キーボード等を有し、利用者が論理検証装置１００が処理を行なうための必要な各種情報を入力するために用いられる。
【００１６】
記憶装置１７は、例えば、ハードディスクユニットにて構成され、各種処理を実行するプログラム等のデータを格納する。
【００１７】
論理検証装置１００によって行われる論理検証方法での処理を実現するプログラムは、例えば、ＣＤ−ＲＯＭ（Compact Disk Read-Only Memory）等の記憶媒体１９によって論理検証装置１００に提供される。即ち、プログラムが保存された記憶媒体１９がドライバ１８にセットされると、ドライバ１８が記憶媒体１９からプログラムを読み出し、その読み出されたプログラムがシステムバスＢを介して記憶装置１７にインストールされる。そして、プログラムが起動されると、記憶装置１７にインストールされたプログラムに従ってＣＰＵ１１がその処理を開始する。
【００１８】
尚、プログラムを格納する媒体としてＣＤ−ＲＯＭに限定するものではなく、コンピュータが読み取り可能な媒体であればよい。論理検証装置１００が外部とのネットワーク通信を行う通信ユニットを有する場合には、本発明に係る処理を実現するプログラムを通信ユニットによってネットワークを介してダウンロードし、記憶装置１７にインストールするようにしても良い。また、論理検証装置１００が外部記憶装置との接続を行うＵＳＢ（Universal Serial Bus）等のインタフェースを有する場合には、ＵＳＢ接続によって外部記憶媒体からプログラムを読み込んでもよい。
【００１９】
論理検証装置１００のＣＰＵ１１によって実行される論理検証処理について図２で説明する。図２は、論理検証処理の概要を説明するための図である。図２において、論理検証装置１００は、ＣＰＵ１１が検証プロパティ１０２に基づくシミュレーションを行うことによって論理検証を行う論理検証処理部１０１を備えている。
【００２０】
論理検証処理部１０１は、プロパティ入力部１０８と、プロパティ表示部１１０と、状態機械生成部１１２と、論理検証実行部１１５と、波形表示部１１８と、表示操作入力部１１９とを有する。論理検証処理部１０１において生成される情報は、メモリユニット１２又は記憶装置１７の記憶領域に格納される。
【００２１】
プロパティ入力部１０８は、検証プロパティ１０２を論理検証処理部１０１に入力して、検証プロパティ１０２から構文木１０９を生成して記憶領域に格納する。検証プロパティ１０２は、外部記憶装置又は論理検証装置１００内の記憶装置に格納されプロパティ入力部１０８によって論理検証処理部１０１に読み込まれる。
【００２２】
状態機械生成部１１２は、検証プロパティ１０２を検証するために、構文木１０９を用いて検証プロパティ１０２に従った状態遷移を示す状態機械１１３を生成する。また、状態機械生成部１１２は、構文木１０９の各要素と状態機械１１３の各要素との対応関係を示す構文木−状態機械対応情報１１４を生成して記憶領域に格納する。
【００２３】
論理検証実行部１１５は、検証対象となるモジュールソースを示す検証対象データ１０３と設定ファイルなどの検証環境データ１０４とを読み込み、検証対象データ１０３と検証環境データ１０４と状態機械１１３とを用いてモジュールソースに対して論理検証を行う。そして、論理検証実行部１１５は、論理検証結果に基づいて波形データ１１６を生成する。論理検証実行部１１５による論理検証によって違反が検出された場合、波形データ１１６には違反のデータが含まれる。
【００２４】
検証対象データ１０３とは、例えば、回路の動作をクロックに基づくレジスタ間の信号転送で記述したＲＴＬ（Register Transfer Level）などである。検証環境データ１０４とは、例えば、テストベンチなどである。
【００２５】
また、論理検証実行部１１５は、状態機械１１３の各要素と波形データ１１６の各要素との対応関係を示す状態機械−波形対応情報１１７を生成する。波形表示部１１８は、生成された波形データ１１６に基づく波形表示１０６を表示ユニット１３に表示する。
【００２６】
ユーザが波形表示１０６上で波形の一部又は全部を選択すると、ユーザによる入力ユニット１５を用いた表示操作１０７が表示操作入力部１１９に伝えられる。表示操作入力部１１９は、ユーザによる表示操作１０７に応じて、構文木−状態機械対応情報１１４と状態機械−波形対応情報１１７とを用いて、構文木１０９のうち波形表示１０６上での選択に対応する部分に関する情報としてプロパティ表示付加情報１２０を生成する。
【００２７】
プロパティ表示部１１０は、プロパティ−構文木対応情報１１１とプロパティ表示付加情報１２０とに基づいて、プロパティ表示１０５上で表示操作１０７に対応する部分を他の部分と区別できるように表示する。例えば、プロパティ表示部１１０は、表示操作１０７に対応する部分を他の部分とは異なる色、異なる文字の形状（太さ、文字スタイルなど）等によって強調して、プロパティ表示１０５を表示ユニットに表示する。
【００２８】
ユーザがプロパティ表示１０５上で検証プロパティの記述の一部又は全部を選択すると、表示操作入力部１１９に表示操作１０７が伝えられる。表示操作入力部１１９は、ユーザによる表示操作１０７に応じて、構文木−状態機械対応情報１１４と状態機械−波形対応情報１１７とを用いて、波形データ１１６のうちプロパティ表示１０５上での選択に対応する部分に関する情報として波形表示付加情報１２１を生成する。
【００２９】
波形表示部１１８は、波形表示付加情報１２１に基づいて、波形表示１０６上で表示操作１０７に対応する部分を他の部分と区別できるように表示する。例えば、波形表示部１１８は、表示操作１０７に対応する部分を他の部分とは異なる色、異なる線の形状（太さ、線の種類など）等によって強調して、波形表示１０６を表示ユニットに表示する。
【００３０】
図３は、表示操作に応じてプロパティ表示と波形表示とが連動する表示例を示す図である。図３において、ユーザがプロパティ表示２０１又は波形表示２０２の一方を部分的に選択すると、選択部分と連動部分とが強調して表示される。
【００３１】
例えば、ユーザがプロパティ表示２０１の検証プロパティの記述の一部分となる記述「ｂ」をマウスなどで選択すると、プロパティ表示部１１０は、プロパティ表示２０１上の表示操作１０７に応じて記述「ｂ」を強調的に表示し、表示操作入力部１１９は、プロパティ−構文木対応情報１１１を用いてプロパティ表示２０１の記述「ｂ」に対応する構文木１０９の要素「ｂ」を取得して、更に、構文木−状態機械対応情報１１４を用いて構文木１０９の要素「ｂ」に対応する状態機械１１３における要素「ｂ」が成り立つ時の状態データを取得し、状態機械−波形対応情報１１７を用いてこの状態に対応する波形データのうちのプロパティ表示２０１の記述「ｂ」の部分に関する波形表示付加情報１２１を生成する。
【００３２】
従って、波形表示２０２では、波形表示付加情報１２１に基づいて波形表示部１１８によって連動箇所に強調表示２０４が成される。
【００３３】
一方、ユーザが波形表示２０２の検証プロパティの記述の一部分をマウスなどで選択すると、波形表示部１１８は、波形表示２０２上の表示操作１０７に応じて波形部分を強調的に表示し、表示操作入力部１１９は、状態機械−波形対応情報１１７を用いて波形表示２０２上のユーザによって選択された波形部分に対応する状態を取得し、更に、構文木−状態機械対応情報１１４を用いて取得した状態に対応する構文木１０９の要素「ｂ」を取得し、選択された波形部分に対応する情報として構文木１０９の要素「ｂ」を示す情報を含むプロパティ表示付加情報１２０を生成する。
【００３４】
従って、プロパティ表示２０１では、プロパティ表示付加情報１２０に基づいてプロパティ表示部１１０によって連動箇所に強調表示２０３が成される。
【００３５】
プロパティ−構文木対応情報１１１と、構文木−状態機械対応情報１１４と、状態機械−波形対応情報１１７とによる対応関係について図４で説明する。図４は、プロパティ内の記述と波形表示とを連動させるための対応関係の例を示す図である。図４において、検証プロパティ３０１の記述を例にして対応関係を説明する。
【００３６】
検証プロパティ３０１は、｛〜ａ；ａ｝によって「ａがゼロの時１サイクル経過後にaを１にする」ことを前提条件として記述し、「ａがゼロから１」が成立したら、｛ｂ；ｃ｝によって「ｂが１になった１サイクル後にｃが１になる」ことを事後条件として記述している。
【００３７】
構文木３０２は、クロックに応じて変化する検証プロパティ３０１の要素「〜ａ」、「ａ」、「ｂ」及び「ｃ」を末端の要素３０２−１、３０２−２、３０２−３及び３０２−４として生成される。要素３０２−１及び３０２−２は、前提条件として分木する要素である。要素３０２−３及び３０２−４は、事後条件として分木する要素である。
【００３８】
状態機能３０３は、初期状態Ｓ０、構文木３０２の要素３０２−１、３０２−２、３０３−３及び３０４−４が成立する順に状態Ｓ１、Ｓ２、Ｓ３及びＳ４、構文木３０２に含まれないエラー状態Ｓ９を含むように生成される。
【００３９】
波形データ３０４は、基準となるクロックｃｌｋの波形と、論理検証実行部１１５によって生成される信号ａ、ｂ及びｃがとる値と、検証プロパティ３０１を示すＰ１の状態とによって生成される。
【００４０】
プロパティ−構文木対応情報１１１は、検証プロパティ３０１の要素「〜ａ」、「ａ」、「ｂ」及び「ｃ」と構文木３０２の要素３０２−１、３０２−２、３０２−３及び３０２−４とを互いに対応付けした情報である。
【００４１】
構文木−状態機械対応情報１１４は、構文木３０２の要素３０２−１、３０２−２、３０２−３及び３０２−４と状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３及びＳ４とを互いに対応付けした情報である。この場合、構文木−状態機械対応情報１１４では、初期状態Ｓ０及びエラー状態Ｓ９の構文木３０２への対応付けはない。
【００４２】
状態機械−波形対応情報１１７は、生成された波形データ３０４のクロックｃｌｋのサイクルに従った信号ａ、ｂ及びｃの波形と状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３及びＳ９とを互いに対応付けした情報である。状態機械−波形対応情報１１７による対応付けは、生成された波形データ３０４のクロックｃｌｋのサイクルに従った信号ａ、ｂ及びｃの波形によって変化する。ここでは、検証プロパティ違反があった場合を例示しているため、エラー状態Ｓ９が波形データ３０４の一部に対応付けられている。検証プロパティ違反がない場合、このような対応付けはない。
【００４３】
例えば、波形データ３０２は、サイクル０、１、２、３・・・のサイクル毎に信号ａ、ｂ及びｃの値と、検証プロパティ３０１示すＰ１の状態値とを記憶している波形テキストファイルなどである。サイクル０、１、２、３・・・に対して状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３、Ｓ４及びＳ９を対応付けることによって状態機械−波形対応情報１１７を生成できる。
【００４４】
状態機械３０３のエラー状態Ｓ９が波形データ３０４と対応付けられた場合は、状態機械３０３のエラー状態Ｓ９と構文木３０２の要素への対応は、波形テキストファイルを参照して、エラー状態Ｓ９となる直前（１サイクル前）の状態Ｓ３から辿るようにすればよい。
【００４５】
次に、検証プロパティの条件記述に対応させて表示する方法について図５、図６及び図７で説明する。
【００４６】
図５は、検証プロパティの条件記述に応じた波形表示例を示す図である。図５に示すプロパティ表示４０１において、検証プロパティを示すＰ１によって、前提条件が実行されていることを示す前提条件範囲４０２で「pre」と示され、事後条件が実行されていることを示す事後条件範囲４０３で「post」と示され、違反が発生していることを示す違反発生範囲で「fire」と示されている。
【００４７】
また、前提条件範囲４０２と事後条件範囲４０３とが容易に区別できるように、それ以外の範囲とは異なる背景色で強調表示する。更に、前提条件範囲４０２が視覚的に判断できるように、検証プロパティの状態を示すＰ１、クロックｃｌｋ、信号「ａ」、「ｂ」及び「ｃ」において同じ背景色で前提条件範囲４０２であることを示し、その背景色とは別の背景色で事後条件範囲４０２であることを示す。
【００４８】
図６は、図５に示す表示方法においてプロパティ表示と波形表示とが連動して表示される表示例を示す図である。図６において、図５に示す波形表示４０１と、プロパティ表示５０１とが同時に表示され、かつ、プロパティ表示５０１の検証プロパティの記述のうち波形表示４０１の前提条件範囲４０２に対応する記述部分を示す前提条件５０２が波形表示４０１の前提条件範囲４０２と同じ背景色で強調表示され、プロパティ表示５０１の検証プロパティの記述のうち波形表示４０１の事後条件範囲４０２に対応する記述部分を示す事後条件５０２が波形表示４０１の事後条件範囲４０２と同じ背景色で強調表示される。
【００４９】
図７は、強調表示をプロパティ表示と波形表示とで連動させるための対応関係の例を示す図である。図７において、検証プロパティ６０１の記述は、図４に示す検証プロパティ３０１の記述と同様である。
【００５０】
プロパティ−構文木対応情報１１１−２は、検証プロパティ６０１の前提条件「〜ａ；ａ」の記述部分を示す前提条件６０５と構文木６０２の前提条件「〜ａ；ａ」の要素６０７−１及び６０７−２を含む分木部分を示す前提条件部分６０７とを対応けし、検証プロパティ６０１の事後条件「ｂ；ｃ」の記述部分を示す事後条件６０６と構文木６０２の前提条件の要素６０８−１及び６０８−２を含む分木部分を示す事後条件部分６０８とを対応けした情報である。
【００５１】
構文木６０２を生成する際に、プロパティ入力部１０８（図１）は、検証プロパティ６０１の記述形式に従って、前提条件６０５の記述部分に関して<ｐｒｅ>の分木の配下に前提条件６０５の各要素「〜ａ」及び「ａ」を生成し、事後条件６０６の記述部分に関して<ｐｏｓｔ>の分木の配下に事後条件６０６の各要素「ｂ」及び「ｃ」を生成する。従って、<ｐｒｅ>の分木配下の前提条件６０５の要素「〜ａ」及び「ａ」までを前提条件部分６０７と認識し、<ｐｏｓｔ>の分木配下の事後条件６０６の要素「ｂ」及び「ｃ」までを事後条件部分６０８と認識することによって、プロパティ−構文木対応情報１１１−２を生成することができる。
【００５２】
構文木−状態機械対応情報１１４−２は、構文木６０２の前提条件部分６０７と状態機械６０３の前提条件状態６０９とを対応付けし、構文木６０２の事後条件部分６０８と状態機械６０３の前提条件状態６１０とを対応付けした情報である。状態機械６０３の前提条件状態６０９には、構文木６０２の前提条件部分６０７における末端の要素６０７−１及び６０７−２が各々成立した場合の状態Ｓ１及びＳ２を含む状態部分である。同様に、状態機械６０３の事後条件状態６１０には、構文木６０２の事後条件部分６０８における末端の要素６０８−１及び６０８−２が各々成立した場合の状態Ｓ３及びＳ４を含む状態部分である。この場合、構文木−状態機械対応情報１１４−２では、初期状態Ｓ０及び違反発生状態６１１の構文木６０２への対応付けはない。
【００５３】
状態機械−波形対応情報１１７−２は、状態機械６０３の前提条件状態６０９と波形データ６０４の前提条件範囲６１２とを対応付けし、状態機械６０３の事後条件状態６１０と波形データ６０４の事後条件範囲６１３とを対応付けし、状態機械６０３の違反発生状態６１１と波形データ６０４の違反発生範囲６１４とを対応付けした情報である。ここでは、検証プロパティ違反があった場合を例示しているため、違反発生状態６１１が波形データ３０４の違反発生範囲６１３に対応付けられている。検証プロパティ違反がない場合、このような対応付けはない。
【００５４】
例えば、状態機械−波形対応情報１１７−２において、クロックｃｌｋのサイクル１から３までを前提条件範囲６１２、クロックｃｌｋのサイクル３から４までを事後条件範囲６１３、クロックｃｌｋのサイクル４から５までを違反発生範囲６１４と定義し、そして、上述したように状態機械６０３と波形データ６０４とを対応づければよい。
【００５５】
このように、前提条件、事後条件、違反発生を示す、論理検証によって検証プロパティ６０１が取り得る状態毎に対応付けされることによって、状態に対応させて波形表示４０１とプロパティ表示５０１とを連動させることができる。また、対応付けに従って前提条件及び事後条件に相当する箇所を波形表示４０１とプロパティ表示５０１との間で容易に識別可能な表示とすることができる。
【００５６】
異なる状態遷移を経て検証プロパティ違反が発生し、同じ遷移経路による検証プロパティ違反が複数回発生する場合には、別の遷移経路による検証プロパティ違反が紛れ込んでしまい、検証し難い場合がある。
【００５７】
このような場合には、論理検証実行部１１５が検証プロパティ違反への遷移経路毎にカウントしておき、カウンタが１（初回）を示す場合又は所定値以上を示す場合に、検証プロパティ違反を示すように波形データを生成する。つまり、カウンタが２以上を示す場合、検証プロパティ違反を示さないようにする。このような検証プロパティ違反の表示を間引く例について図８から図１１で説明する。
【００５８】
図８は、検証プロパティ違反が異なる状態遷移を経て発生する場合の対応関係の例を示す図である。図８中、プロパティ−構文木対応情報１１１及び構文木−状態機械対応情報１１４による対応関係は省略し、便宜的に検証プロパティ７０１と状態機械７０２との対応関係のみが示される。
【００５９】
図８において、検証プロパティ７０１は、前提条件として第一条件７０３又は第二条件７０４が成り立った場合、１サイクル後に事後条件７０５が行われる例を示している。例えば、検証プロパティ７０１は、信号ａがオン又は信号ｂがオンとなったら、１サイクル後に信号ｃがオンとなることを示している。
【００６０】
検証プロパティ７０１に対応付けられる状態機械７０２では、初期状態Ｓ０から検証プロパティ７０１の第一条件７０３に対応する第一条件状態７０６（状態Ｓ１）と、検証プロパティ７０１の第一条件７０４に対応する第二条件状態７０７（状態Ｓ３）とに分木する。
【００６１】
第一条件状態７０６（状態Ｓ１）からは、検証プロパティ７０１の事後条件７０５に対応する事後条件状態７０８へと遷移する。また、第二条件状態７０７（状態Ｓ３）からは、検証プロパティ違反となる違反発生状態７０５へと遷移する。
【００６２】
検証プロパティに従った論理検証において、論理検証実行部１１５が検証プロパティ違反の表示を間引く処理をしなかった場合、例えば、図９に示すような波形データ８０１が生成される。図９は、検証プロパティ違反の表示を間引く処理がなされなかった場合の波形データの例を示す図である。
【００６３】
図９に示す波形データ８０１では、同じ遷移経路による検証プロパティ違反８０２が複数回発生し、その中に別の遷移経路による検証プロパティ違反８０３が発生している状態を示している。このような波形データ８０１では、一見して検証プロパティ違反８０３を識別することができない。
【００６４】
論理検証実行部１１５は、図８に示す状態機械７０２に基づいて、違反発生状態７０９に遷移する直前の状態を抽出し、抽出した直前の状態に対応させてカウンタ値を記録するために、図１０に示すような遷移経路別カウンタを備えるようにする。図１０は、遷移経路別カウンタの例を示す図である。
【００６５】
図１０に示すように、図８に示す状態機械７０２に基づいて、違反発生状態７０９に遷移する直前の状態として、第一条件状態７０６となる状態Ｓ１と、第二条件状態７０７となる状態Ｓ３とが抽出され、遷移経路別カウンタ９０に記録される。論理検証実行部１１５は、違反発生状態７０９となる状態Ｓ４に遷移する度に、直前の状態を確認し、遷移経路別カウンタ９０の対応する状態のカウンタ値を１加算する。加算されたカウンタ値が１を示す場合のみ、論理検証実行部１１５は、波形データに記録する。
【００６６】
このようにして、図１１に示す波形データ９０１が生成される。図１１は、検証プロパティ違反の表示を間引いた処理がなされた場合の波形データの例を示す図である。図１１に示す波形データ９０１において、図９に示す同じ検証プロパティ違反には同一の符号を伏してある。波形データ９０１に基づいて波形表示された場合には、初回に発生した検証プロパティ違反８０２及び８０３のみが示される。
【００６７】
上述したように、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証結果によって表示される波形表示上で、ユーザが波形表示上の所望の波形部分を選択すると、選択された波形部分に連動させてその選択された波形部分に対応する検証プロパティの記述の一部分が視覚的に他記述部分と区別できるように表示することができる。
【００６８】
また、ユーザがプロパティ表示上で検証プロパティの記述を部分的に選択すると、選択された検証プロパティの記述部分と連動して、その選択された検証プロパティの記述部分に対応する波形部分が視覚的に他波形部分と区別できるように表示することができる。
【００６９】
このように波形表示とプロパティ表示との間でユーザによって選択された部分に対応させて視覚的に他部分と区別できるように表示されることにより、ユーザは、波形に対応する記述をユーザ自身の経験及び知識に依存することなく、検証プロパティ違反が発生した原因を容易に解析することができる。
【００７０】
また、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反が検出された検証プロパティの前提条件に対応する波形部分が波形表示上で他と区別できるように表示することができる。従って、ユーザは、検証プロパティの前提条件となる波形部分を容易に把握することができるため、検証プロパティ違反の解析をより正確に行うことができる。
【００７１】
更に、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反が検出された検証プロパティの前提条件の記述とその記述に対応する波形部分とが連動してプロパティ表示上及び波形表示上とで他と区別できるように表示することができる。従って、ユーザは、検証プロパティの前提条件と違反波形との対応関係を容易に把握することができ、ユーザ自身で対応関係を考察する必要がないため、検証プロパティ違反の解析をより効率的かつ正確に行うことができる。
【００７２】
また、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反の原因が同じものについては波形表示上に複数の検証プロパティ違反を示す情報を表示しないようにすることができる。従って、ユーザは、同じ原因の検証プロパティ違反を何度も解析する必要がなく、効率的に検証プロパティ違反の解析を行うことができる。
【００７３】
更に、同じ原因の検証プロパティ違反のうち初回に検出された違反を波形表示上に表示させることによって、ユーザは、大量の同じ原因による検証プロパティ違反の検出の中に埋もれている重大な検証プロパティ違反を見逃さないようにすることができる。
【００７４】
以上の説明に関し、更に以下の項を開示する。
（付記１）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法。
（付記２）
前記表示制御手順は、前記プロパティ表示手順によって表示された前記検証プロパティ上への前記操作入力に応じて、該操作入力によって選択された前記検証プロパティの記述部分に連動させて該記述部分に対応する前記波形表示手順によって表示された前記波形上の波形部分を他波形部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記１記載の論理検証方法。
（付記３）
前記表示制御手順は、
前記検証プロパティに基づいて生成された構文木の要素と該構文木に基づいて生成された状態機械によって示される前記検証プロパティの実行過程で遷移する状態との対応関係を示す構文木−状態機械対応情報と、前記状態機械の状態と前記生成された波形の波形状態との対応関係を示す状態機械−波形対応情報とを用いて、前記操作入力に応じて前記波形部分と前記記述部分とを関連づけて連動させることを特徴とする付記１又は２記載の論理検証方法。
（付記４）
前記プロパティ表示手順は、
前記検証プロパティの要素と該検証プロパティに基づいて生成された構文木の要素との対応関係を示すプロパティ−構文木対応情報を用いて、前記検証プロパティの前記記述部分と他記述部分とを区別して表示することを特徴とする付記１乃至３のいずれか一項記載の論理検証方法。
（付記５）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とする論理検証方法。
（付記６）
前記検証プロパティを表示するプロパティ表示手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記前提条件状態となる範囲に対応する前記検証プロパティの前提条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記５記載の論理検証方法。
（付記７）
前記論理検証実行手順は、前記状態機械によって示される事後条件状態となる範囲を前記波形データに設定し、
前記表示制御手順は、前記事後条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御することを特徴とする付記５又は６記載の論理検証方法。
（付記８）
前記表示制御手順は、前記波形表示手順によって表示された前記事後条件状態となる範囲に対応する前記検証プロパティの事後条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記７記載の論理検証方法。
（付記９）
前記論理検証実行手順は、前記状態機械によって示される違反発生状態となる範囲を前記波形データに設定し、
前記表示制御手順は、違反発生を示す情報を示すように前記波形表示手順を制御することを特徴とする付記５乃至８のいずれか一項記載の論理検証方法。
（付記１０）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とする論理検証方法。
（付記１１）
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、検出された初回の該違反発生状態に対応する部分を波形データに設定することを特徴とする付記１０記載の論理検証方法。
（付記１２）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とするコンピュータ実行可能なプログラム。
（付記１３）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とするコンピュータ実行可能なプログラム。
（付記１４）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とするコンピュータ実行可能なプログラム。
（付記１５）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置であって、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手段と、
前記検証プロパティを表示するプロパティ表示手段と、
操作入力に応じて前記波形表示手段と前記プロパティ表示手段とを制御する表示制御手段とを実行させ、
前記表示制御手段は、前記波形表示手段によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手段に表示させることを特徴とする論理検証装置。
本発明は、具体的に開示された実施例に限定されるものではなく、特許請求の範囲から逸脱することなく、種々の変形や変更が可能である。
【図面の簡単な説明】
【００７５】
【図１】本発明の一実施例に係る論理検証装置のハードウェア構成を示す図である。
【図２】論理検証処理の概要を説明するための図である。
【図３】表示操作に応じてプロパティ表示と波形表示とが連動する表示例を示す図である。
【図４】プロパティ内の記述と波形表示とを連動させるための対応関係の例を示す図である。
【図５】検証プロパティの条件記述に応じた波形表示例を示す図である。
【図６】図５に示す表示方法においてプロパティ表示と波形表示とが連動して表示される表示例を示す図である。
【図７】強調表示をプロパティ表示と波形表示とで連動させるための対応関係の例を示す図である。
【図８】検証プロパティ違反が異なる状態遷移を経て発生する場合の対応関係の例を示す図である。
【図９】検証プロパティ違反の表示を間引く処理がなされなかった場合の波形データの例を示す図である。
【図１０】遷移経路別カウンタの例を示す図である。
【図１１】検証プロパティ違反の表示を間引いた処理がなされた場合の波形データの例を示す図である。
【符号の説明】
【００７６】
１１ ＣＰＵ
１２ メモリユニット
１３ 表示ユニット
１５ 入力ユニット
１７ 記憶装置
１８ ドライバ
１９ 記憶媒体
９０ 遷移経路別カウンタ
１００ 論理検証装置
１０１ 論検証処理部
１０２ 論理プロパティ
１０３ 検証対象データ
１０４ 検証環境データ
１０５ プロパティ表示
１０６ 波形表示
１０７ 表示操作
１０８ プロパティ入力部
１０９ 構文木
１１０ プロパティ表示部
１１１ プロパティ−構文木対応情報
１１２ 状態機械生成部
１１３ 状態機械
１１４ 構文木−状態機械対応情報
１１５ 論理検証実行部
１１６ 波形データ
１１７ 状態機械−波形対応情報
１１８ 波形表示部
１１９ 表示操作部
１２０ プロパティ表示付加情報
１２１ 波形表示付加情報
２０１ プロパティ表示
２０３、２０４ 強調表示
３０１、６０１ 検証プロパティ
３０２、６０２ 構文木
３０３、６０３ 状態機械
３０４、６０４ 波形データ
４０１ 波形表示
４０２、６１２ 前提条件範囲
４０３、６１３ 事後条件範囲
４０４、６１４ 違反発生範囲
５０１ プロパティ表示
５０２ 前提条件
５０３ 事後条件
７０１ 検証プロパティ
７０２ 状態機械
７０３ 第一条件
７０４ 第二条件
７０５ 事後条件
７０６ 第一条件状態
７０７ 第二条件状態
７０８ 事後条件状態
７０９ 違反発生状態
８０１、９０１ 波形データ
８０２、８０３ 検証プロパティ違反
【技術分野】
【０００１】
本発明は、論理回路などの論理検証によって発見される検証プロパティ違反を波形上で解析する際に解析を容易化する論理検証方法に関する。
【背景技術】
【０００２】
従来より、論理回路などを設計する際には、設計対象の機能やタイミングなどが仕様を満たしているか否かを検証する論理検証と呼ばれる作業が行われている。論理検証では仕様を満たしているか否かを確認するために検証プロパティを作成し、検証プロパティを満たしているか否かをチェックするためのチェッカを組み込んだ環境で検証を行っている。一般に、検証プロパティ違反が発見された場合は波形を見ることで違反の原因を解析する手法が取られている。しかしながら、波形から違反の原因を特定するためには、経験と知識を要し容易に原因を特定できるものではなかった。
【０００３】
そこで、波形を用いた解析を容易とするために、検証結果に基づいてエラーメッセージ８０を表示すると共に、注釈情報付き波形データに格納されている信号値の期待値に基づいて、期待される信号波形が実際の波形に重ねて表示し、注釈情報付き波形データに格納されているイベントの情報に基づいて、イベントの論理的関係を示す矢印記号を表示することが提案されている（例えば、特許文献１参照。）。
【特許文献１】特開２００４−３２６５５０号公報（第８図）
【特許文献２】特開２００３−２１６６８３号公報
【特許文献３】特開２００１−２０９６６８号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかしながら、上記従来の論理検証方法では、ユーザは検証プロパティの記述と波形との対応に関する知識を要し、検証プロパティを頭の中に記憶しておいて表示装置に表示された波形との対応で解析を行う必要があった。検証プロパティが複雑な場合、また、信号線が多い場合では、検証プロパティと違反波形との対応関係を頭の中で構築することは困難な場合があり、また解析の際に間違いを生じやすい。
【０００５】
よって、本発明の目的は、検証プロパティと波形とを連動させて、一方を部分的に選択すると対応する他方の部分が視覚的に判別可能なように表示する論理検証方法を提供することである。
【課題を解決するための手段】
【０００６】
上記課題を解決するため、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、前記検証プロパティを表示するプロパティ表示手順と、操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させるように構成される。
【０００７】
また、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、前記波形データに基づいて生成された波形を表示する波形表示手順と、操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させるように構成される。
【０００８】
更に、本発明は、検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定するように構成される。
【０００９】
上記課題を解決するための手段として、本発明は、上記手順をコンピュータに実行させるためのプログラム、そのプログラムを記憶したコンピュータ読み取り可能な記憶媒体、及び、該プログラムによって上記手順を実行する論理検証装置とすることもできる。
【発明の効果】
【００１０】
本願発明は、検証プロパティと波形とを連動させて表示し、一方を部分的に選択すると対応する他方の部分が視覚的に容易に判別可能なようにし、検証プロパティと違反波形との対応関係を容易とすることによって、検証プロパティ違反の解析を容易に正確に行なうことができる。
【発明を実施するための最良の形態】
【００１１】
以下、本発明の実施の形態を図面に基づいて説明する。
【００１２】
本発明に係る論理検証方法を実現する論理検証装置は、コンピュータ装置であって、図１に示すようなハードウェア構成を有する。図１は、本発明の一実施例に係る論理検証装置のハードウェア構成を示す図である。
【００１３】
図１において、論理検証装置１００は、コンピュータによって制御される装置であって、ＣＰＵ（Central Processing Unit）１１と、メモリユニット１２と、表示ユニット１３と、入力ユニット１５と、記憶装置１７と、ドライバ１８とで構成され、システムバスＢに接続される。
【００１４】
ＣＰＵ１１は、メモリユニット１２に格納されたプログラムに従って論理検証装置１００を制御する。メモリユニット１２は、ＲＡＭ（Random Access Memory）及びＲＯＭ（Read-Only Memory）等にて構成され、ＣＰＵ１１にて実行されるプログラム、ＣＰＵ１１での処理に必要なデータ、ＣＰＵ１１での処理にて得られたデータ等を格納する。また、メモリユニット１２の一部の領域が、ＣＰＵ１１での処理に利用されるワークエリアとして割り付けられている。
【００１５】
表示ユニット１３は、ＣＰＵ１１の制御のもとに必要な各種情報を表示する。入力ユニット１５は、マウス、キーボード等を有し、利用者が論理検証装置１００が処理を行なうための必要な各種情報を入力するために用いられる。
【００１６】
記憶装置１７は、例えば、ハードディスクユニットにて構成され、各種処理を実行するプログラム等のデータを格納する。
【００１７】
論理検証装置１００によって行われる論理検証方法での処理を実現するプログラムは、例えば、ＣＤ−ＲＯＭ（Compact Disk Read-Only Memory）等の記憶媒体１９によって論理検証装置１００に提供される。即ち、プログラムが保存された記憶媒体１９がドライバ１８にセットされると、ドライバ１８が記憶媒体１９からプログラムを読み出し、その読み出されたプログラムがシステムバスＢを介して記憶装置１７にインストールされる。そして、プログラムが起動されると、記憶装置１７にインストールされたプログラムに従ってＣＰＵ１１がその処理を開始する。
【００１８】
尚、プログラムを格納する媒体としてＣＤ−ＲＯＭに限定するものではなく、コンピュータが読み取り可能な媒体であればよい。論理検証装置１００が外部とのネットワーク通信を行う通信ユニットを有する場合には、本発明に係る処理を実現するプログラムを通信ユニットによってネットワークを介してダウンロードし、記憶装置１７にインストールするようにしても良い。また、論理検証装置１００が外部記憶装置との接続を行うＵＳＢ（Universal Serial Bus）等のインタフェースを有する場合には、ＵＳＢ接続によって外部記憶媒体からプログラムを読み込んでもよい。
【００１９】
論理検証装置１００のＣＰＵ１１によって実行される論理検証処理について図２で説明する。図２は、論理検証処理の概要を説明するための図である。図２において、論理検証装置１００は、ＣＰＵ１１が検証プロパティ１０２に基づくシミュレーションを行うことによって論理検証を行う論理検証処理部１０１を備えている。
【００２０】
論理検証処理部１０１は、プロパティ入力部１０８と、プロパティ表示部１１０と、状態機械生成部１１２と、論理検証実行部１１５と、波形表示部１１８と、表示操作入力部１１９とを有する。論理検証処理部１０１において生成される情報は、メモリユニット１２又は記憶装置１７の記憶領域に格納される。
【００２１】
プロパティ入力部１０８は、検証プロパティ１０２を論理検証処理部１０１に入力して、検証プロパティ１０２から構文木１０９を生成して記憶領域に格納する。検証プロパティ１０２は、外部記憶装置又は論理検証装置１００内の記憶装置に格納されプロパティ入力部１０８によって論理検証処理部１０１に読み込まれる。
【００２２】
状態機械生成部１１２は、検証プロパティ１０２を検証するために、構文木１０９を用いて検証プロパティ１０２に従った状態遷移を示す状態機械１１３を生成する。また、状態機械生成部１１２は、構文木１０９の各要素と状態機械１１３の各要素との対応関係を示す構文木−状態機械対応情報１１４を生成して記憶領域に格納する。
【００２３】
論理検証実行部１１５は、検証対象となるモジュールソースを示す検証対象データ１０３と設定ファイルなどの検証環境データ１０４とを読み込み、検証対象データ１０３と検証環境データ１０４と状態機械１１３とを用いてモジュールソースに対して論理検証を行う。そして、論理検証実行部１１５は、論理検証結果に基づいて波形データ１１６を生成する。論理検証実行部１１５による論理検証によって違反が検出された場合、波形データ１１６には違反のデータが含まれる。
【００２４】
検証対象データ１０３とは、例えば、回路の動作をクロックに基づくレジスタ間の信号転送で記述したＲＴＬ（Register Transfer Level）などである。検証環境データ１０４とは、例えば、テストベンチなどである。
【００２５】
また、論理検証実行部１１５は、状態機械１１３の各要素と波形データ１１６の各要素との対応関係を示す状態機械−波形対応情報１１７を生成する。波形表示部１１８は、生成された波形データ１１６に基づく波形表示１０６を表示ユニット１３に表示する。
【００２６】
ユーザが波形表示１０６上で波形の一部又は全部を選択すると、ユーザによる入力ユニット１５を用いた表示操作１０７が表示操作入力部１１９に伝えられる。表示操作入力部１１９は、ユーザによる表示操作１０７に応じて、構文木−状態機械対応情報１１４と状態機械−波形対応情報１１７とを用いて、構文木１０９のうち波形表示１０６上での選択に対応する部分に関する情報としてプロパティ表示付加情報１２０を生成する。
【００２７】
プロパティ表示部１１０は、プロパティ−構文木対応情報１１１とプロパティ表示付加情報１２０とに基づいて、プロパティ表示１０５上で表示操作１０７に対応する部分を他の部分と区別できるように表示する。例えば、プロパティ表示部１１０は、表示操作１０７に対応する部分を他の部分とは異なる色、異なる文字の形状（太さ、文字スタイルなど）等によって強調して、プロパティ表示１０５を表示ユニットに表示する。
【００２８】
ユーザがプロパティ表示１０５上で検証プロパティの記述の一部又は全部を選択すると、表示操作入力部１１９に表示操作１０７が伝えられる。表示操作入力部１１９は、ユーザによる表示操作１０７に応じて、構文木−状態機械対応情報１１４と状態機械−波形対応情報１１７とを用いて、波形データ１１６のうちプロパティ表示１０５上での選択に対応する部分に関する情報として波形表示付加情報１２１を生成する。
【００２９】
波形表示部１１８は、波形表示付加情報１２１に基づいて、波形表示１０６上で表示操作１０７に対応する部分を他の部分と区別できるように表示する。例えば、波形表示部１１８は、表示操作１０７に対応する部分を他の部分とは異なる色、異なる線の形状（太さ、線の種類など）等によって強調して、波形表示１０６を表示ユニットに表示する。
【００３０】
図３は、表示操作に応じてプロパティ表示と波形表示とが連動する表示例を示す図である。図３において、ユーザがプロパティ表示２０１又は波形表示２０２の一方を部分的に選択すると、選択部分と連動部分とが強調して表示される。
【００３１】
例えば、ユーザがプロパティ表示２０１の検証プロパティの記述の一部分となる記述「ｂ」をマウスなどで選択すると、プロパティ表示部１１０は、プロパティ表示２０１上の表示操作１０７に応じて記述「ｂ」を強調的に表示し、表示操作入力部１１９は、プロパティ−構文木対応情報１１１を用いてプロパティ表示２０１の記述「ｂ」に対応する構文木１０９の要素「ｂ」を取得して、更に、構文木−状態機械対応情報１１４を用いて構文木１０９の要素「ｂ」に対応する状態機械１１３における要素「ｂ」が成り立つ時の状態データを取得し、状態機械−波形対応情報１１７を用いてこの状態に対応する波形データのうちのプロパティ表示２０１の記述「ｂ」の部分に関する波形表示付加情報１２１を生成する。
【００３２】
従って、波形表示２０２では、波形表示付加情報１２１に基づいて波形表示部１１８によって連動箇所に強調表示２０４が成される。
【００３３】
一方、ユーザが波形表示２０２の検証プロパティの記述の一部分をマウスなどで選択すると、波形表示部１１８は、波形表示２０２上の表示操作１０７に応じて波形部分を強調的に表示し、表示操作入力部１１９は、状態機械−波形対応情報１１７を用いて波形表示２０２上のユーザによって選択された波形部分に対応する状態を取得し、更に、構文木−状態機械対応情報１１４を用いて取得した状態に対応する構文木１０９の要素「ｂ」を取得し、選択された波形部分に対応する情報として構文木１０９の要素「ｂ」を示す情報を含むプロパティ表示付加情報１２０を生成する。
【００３４】
従って、プロパティ表示２０１では、プロパティ表示付加情報１２０に基づいてプロパティ表示部１１０によって連動箇所に強調表示２０３が成される。
【００３５】
プロパティ−構文木対応情報１１１と、構文木−状態機械対応情報１１４と、状態機械−波形対応情報１１７とによる対応関係について図４で説明する。図４は、プロパティ内の記述と波形表示とを連動させるための対応関係の例を示す図である。図４において、検証プロパティ３０１の記述を例にして対応関係を説明する。
【００３６】
検証プロパティ３０１は、｛〜ａ；ａ｝によって「ａがゼロの時１サイクル経過後にaを１にする」ことを前提条件として記述し、「ａがゼロから１」が成立したら、｛ｂ；ｃ｝によって「ｂが１になった１サイクル後にｃが１になる」ことを事後条件として記述している。
【００３７】
構文木３０２は、クロックに応じて変化する検証プロパティ３０１の要素「〜ａ」、「ａ」、「ｂ」及び「ｃ」を末端の要素３０２−１、３０２−２、３０２−３及び３０２−４として生成される。要素３０２−１及び３０２−２は、前提条件として分木する要素である。要素３０２−３及び３０２−４は、事後条件として分木する要素である。
【００３８】
状態機能３０３は、初期状態Ｓ０、構文木３０２の要素３０２−１、３０２−２、３０３−３及び３０４−４が成立する順に状態Ｓ１、Ｓ２、Ｓ３及びＳ４、構文木３０２に含まれないエラー状態Ｓ９を含むように生成される。
【００３９】
波形データ３０４は、基準となるクロックｃｌｋの波形と、論理検証実行部１１５によって生成される信号ａ、ｂ及びｃがとる値と、検証プロパティ３０１を示すＰ１の状態とによって生成される。
【００４０】
プロパティ−構文木対応情報１１１は、検証プロパティ３０１の要素「〜ａ」、「ａ」、「ｂ」及び「ｃ」と構文木３０２の要素３０２−１、３０２−２、３０２−３及び３０２−４とを互いに対応付けした情報である。
【００４１】
構文木−状態機械対応情報１１４は、構文木３０２の要素３０２−１、３０２−２、３０２−３及び３０２−４と状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３及びＳ４とを互いに対応付けした情報である。この場合、構文木−状態機械対応情報１１４では、初期状態Ｓ０及びエラー状態Ｓ９の構文木３０２への対応付けはない。
【００４２】
状態機械−波形対応情報１１７は、生成された波形データ３０４のクロックｃｌｋのサイクルに従った信号ａ、ｂ及びｃの波形と状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３及びＳ９とを互いに対応付けした情報である。状態機械−波形対応情報１１７による対応付けは、生成された波形データ３０４のクロックｃｌｋのサイクルに従った信号ａ、ｂ及びｃの波形によって変化する。ここでは、検証プロパティ違反があった場合を例示しているため、エラー状態Ｓ９が波形データ３０４の一部に対応付けられている。検証プロパティ違反がない場合、このような対応付けはない。
【００４３】
例えば、波形データ３０２は、サイクル０、１、２、３・・・のサイクル毎に信号ａ、ｂ及びｃの値と、検証プロパティ３０１示すＰ１の状態値とを記憶している波形テキストファイルなどである。サイクル０、１、２、３・・・に対して状態機械３０３の状態Ｓ１、Ｓ２、Ｓ３、Ｓ４及びＳ９を対応付けることによって状態機械−波形対応情報１１７を生成できる。
【００４４】
状態機械３０３のエラー状態Ｓ９が波形データ３０４と対応付けられた場合は、状態機械３０３のエラー状態Ｓ９と構文木３０２の要素への対応は、波形テキストファイルを参照して、エラー状態Ｓ９となる直前（１サイクル前）の状態Ｓ３から辿るようにすればよい。
【００４５】
次に、検証プロパティの条件記述に対応させて表示する方法について図５、図６及び図７で説明する。
【００４６】
図５は、検証プロパティの条件記述に応じた波形表示例を示す図である。図５に示すプロパティ表示４０１において、検証プロパティを示すＰ１によって、前提条件が実行されていることを示す前提条件範囲４０２で「pre」と示され、事後条件が実行されていることを示す事後条件範囲４０３で「post」と示され、違反が発生していることを示す違反発生範囲で「fire」と示されている。
【００４７】
また、前提条件範囲４０２と事後条件範囲４０３とが容易に区別できるように、それ以外の範囲とは異なる背景色で強調表示する。更に、前提条件範囲４０２が視覚的に判断できるように、検証プロパティの状態を示すＰ１、クロックｃｌｋ、信号「ａ」、「ｂ」及び「ｃ」において同じ背景色で前提条件範囲４０２であることを示し、その背景色とは別の背景色で事後条件範囲４０２であることを示す。
【００４８】
図６は、図５に示す表示方法においてプロパティ表示と波形表示とが連動して表示される表示例を示す図である。図６において、図５に示す波形表示４０１と、プロパティ表示５０１とが同時に表示され、かつ、プロパティ表示５０１の検証プロパティの記述のうち波形表示４０１の前提条件範囲４０２に対応する記述部分を示す前提条件５０２が波形表示４０１の前提条件範囲４０２と同じ背景色で強調表示され、プロパティ表示５０１の検証プロパティの記述のうち波形表示４０１の事後条件範囲４０２に対応する記述部分を示す事後条件５０２が波形表示４０１の事後条件範囲４０２と同じ背景色で強調表示される。
【００４９】
図７は、強調表示をプロパティ表示と波形表示とで連動させるための対応関係の例を示す図である。図７において、検証プロパティ６０１の記述は、図４に示す検証プロパティ３０１の記述と同様である。
【００５０】
プロパティ−構文木対応情報１１１−２は、検証プロパティ６０１の前提条件「〜ａ；ａ」の記述部分を示す前提条件６０５と構文木６０２の前提条件「〜ａ；ａ」の要素６０７−１及び６０７−２を含む分木部分を示す前提条件部分６０７とを対応けし、検証プロパティ６０１の事後条件「ｂ；ｃ」の記述部分を示す事後条件６０６と構文木６０２の前提条件の要素６０８−１及び６０８−２を含む分木部分を示す事後条件部分６０８とを対応けした情報である。
【００５１】
構文木６０２を生成する際に、プロパティ入力部１０８（図１）は、検証プロパティ６０１の記述形式に従って、前提条件６０５の記述部分に関して<ｐｒｅ>の分木の配下に前提条件６０５の各要素「〜ａ」及び「ａ」を生成し、事後条件６０６の記述部分に関して<ｐｏｓｔ>の分木の配下に事後条件６０６の各要素「ｂ」及び「ｃ」を生成する。従って、<ｐｒｅ>の分木配下の前提条件６０５の要素「〜ａ」及び「ａ」までを前提条件部分６０７と認識し、<ｐｏｓｔ>の分木配下の事後条件６０６の要素「ｂ」及び「ｃ」までを事後条件部分６０８と認識することによって、プロパティ−構文木対応情報１１１−２を生成することができる。
【００５２】
構文木−状態機械対応情報１１４−２は、構文木６０２の前提条件部分６０７と状態機械６０３の前提条件状態６０９とを対応付けし、構文木６０２の事後条件部分６０８と状態機械６０３の前提条件状態６１０とを対応付けした情報である。状態機械６０３の前提条件状態６０９には、構文木６０２の前提条件部分６０７における末端の要素６０７−１及び６０７−２が各々成立した場合の状態Ｓ１及びＳ２を含む状態部分である。同様に、状態機械６０３の事後条件状態６１０には、構文木６０２の事後条件部分６０８における末端の要素６０８−１及び６０８−２が各々成立した場合の状態Ｓ３及びＳ４を含む状態部分である。この場合、構文木−状態機械対応情報１１４−２では、初期状態Ｓ０及び違反発生状態６１１の構文木６０２への対応付けはない。
【００５３】
状態機械−波形対応情報１１７−２は、状態機械６０３の前提条件状態６０９と波形データ６０４の前提条件範囲６１２とを対応付けし、状態機械６０３の事後条件状態６１０と波形データ６０４の事後条件範囲６１３とを対応付けし、状態機械６０３の違反発生状態６１１と波形データ６０４の違反発生範囲６１４とを対応付けした情報である。ここでは、検証プロパティ違反があった場合を例示しているため、違反発生状態６１１が波形データ３０４の違反発生範囲６１３に対応付けられている。検証プロパティ違反がない場合、このような対応付けはない。
【００５４】
例えば、状態機械−波形対応情報１１７−２において、クロックｃｌｋのサイクル１から３までを前提条件範囲６１２、クロックｃｌｋのサイクル３から４までを事後条件範囲６１３、クロックｃｌｋのサイクル４から５までを違反発生範囲６１４と定義し、そして、上述したように状態機械６０３と波形データ６０４とを対応づければよい。
【００５５】
このように、前提条件、事後条件、違反発生を示す、論理検証によって検証プロパティ６０１が取り得る状態毎に対応付けされることによって、状態に対応させて波形表示４０１とプロパティ表示５０１とを連動させることができる。また、対応付けに従って前提条件及び事後条件に相当する箇所を波形表示４０１とプロパティ表示５０１との間で容易に識別可能な表示とすることができる。
【００５６】
異なる状態遷移を経て検証プロパティ違反が発生し、同じ遷移経路による検証プロパティ違反が複数回発生する場合には、別の遷移経路による検証プロパティ違反が紛れ込んでしまい、検証し難い場合がある。
【００５７】
このような場合には、論理検証実行部１１５が検証プロパティ違反への遷移経路毎にカウントしておき、カウンタが１（初回）を示す場合又は所定値以上を示す場合に、検証プロパティ違反を示すように波形データを生成する。つまり、カウンタが２以上を示す場合、検証プロパティ違反を示さないようにする。このような検証プロパティ違反の表示を間引く例について図８から図１１で説明する。
【００５８】
図８は、検証プロパティ違反が異なる状態遷移を経て発生する場合の対応関係の例を示す図である。図８中、プロパティ−構文木対応情報１１１及び構文木−状態機械対応情報１１４による対応関係は省略し、便宜的に検証プロパティ７０１と状態機械７０２との対応関係のみが示される。
【００５９】
図８において、検証プロパティ７０１は、前提条件として第一条件７０３又は第二条件７０４が成り立った場合、１サイクル後に事後条件７０５が行われる例を示している。例えば、検証プロパティ７０１は、信号ａがオン又は信号ｂがオンとなったら、１サイクル後に信号ｃがオンとなることを示している。
【００６０】
検証プロパティ７０１に対応付けられる状態機械７０２では、初期状態Ｓ０から検証プロパティ７０１の第一条件７０３に対応する第一条件状態７０６（状態Ｓ１）と、検証プロパティ７０１の第一条件７０４に対応する第二条件状態７０７（状態Ｓ３）とに分木する。
【００６１】
第一条件状態７０６（状態Ｓ１）からは、検証プロパティ７０１の事後条件７０５に対応する事後条件状態７０８へと遷移する。また、第二条件状態７０７（状態Ｓ３）からは、検証プロパティ違反となる違反発生状態７０５へと遷移する。
【００６２】
検証プロパティに従った論理検証において、論理検証実行部１１５が検証プロパティ違反の表示を間引く処理をしなかった場合、例えば、図９に示すような波形データ８０１が生成される。図９は、検証プロパティ違反の表示を間引く処理がなされなかった場合の波形データの例を示す図である。
【００６３】
図９に示す波形データ８０１では、同じ遷移経路による検証プロパティ違反８０２が複数回発生し、その中に別の遷移経路による検証プロパティ違反８０３が発生している状態を示している。このような波形データ８０１では、一見して検証プロパティ違反８０３を識別することができない。
【００６４】
論理検証実行部１１５は、図８に示す状態機械７０２に基づいて、違反発生状態７０９に遷移する直前の状態を抽出し、抽出した直前の状態に対応させてカウンタ値を記録するために、図１０に示すような遷移経路別カウンタを備えるようにする。図１０は、遷移経路別カウンタの例を示す図である。
【００６５】
図１０に示すように、図８に示す状態機械７０２に基づいて、違反発生状態７０９に遷移する直前の状態として、第一条件状態７０６となる状態Ｓ１と、第二条件状態７０７となる状態Ｓ３とが抽出され、遷移経路別カウンタ９０に記録される。論理検証実行部１１５は、違反発生状態７０９となる状態Ｓ４に遷移する度に、直前の状態を確認し、遷移経路別カウンタ９０の対応する状態のカウンタ値を１加算する。加算されたカウンタ値が１を示す場合のみ、論理検証実行部１１５は、波形データに記録する。
【００６６】
このようにして、図１１に示す波形データ９０１が生成される。図１１は、検証プロパティ違反の表示を間引いた処理がなされた場合の波形データの例を示す図である。図１１に示す波形データ９０１において、図９に示す同じ検証プロパティ違反には同一の符号を伏してある。波形データ９０１に基づいて波形表示された場合には、初回に発生した検証プロパティ違反８０２及び８０３のみが示される。
【００６７】
上述したように、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証結果によって表示される波形表示上で、ユーザが波形表示上の所望の波形部分を選択すると、選択された波形部分に連動させてその選択された波形部分に対応する検証プロパティの記述の一部分が視覚的に他記述部分と区別できるように表示することができる。
【００６８】
また、ユーザがプロパティ表示上で検証プロパティの記述を部分的に選択すると、選択された検証プロパティの記述部分と連動して、その選択された検証プロパティの記述部分に対応する波形部分が視覚的に他波形部分と区別できるように表示することができる。
【００６９】
このように波形表示とプロパティ表示との間でユーザによって選択された部分に対応させて視覚的に他部分と区別できるように表示されることにより、ユーザは、波形に対応する記述をユーザ自身の経験及び知識に依存することなく、検証プロパティ違反が発生した原因を容易に解析することができる。
【００７０】
また、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反が検出された検証プロパティの前提条件に対応する波形部分が波形表示上で他と区別できるように表示することができる。従って、ユーザは、検証プロパティの前提条件となる波形部分を容易に把握することができるため、検証プロパティ違反の解析をより正確に行うことができる。
【００７１】
更に、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反が検出された検証プロパティの前提条件の記述とその記述に対応する波形部分とが連動してプロパティ表示上及び波形表示上とで他と区別できるように表示することができる。従って、ユーザは、検証プロパティの前提条件と違反波形との対応関係を容易に把握することができ、ユーザ自身で対応関係を考察する必要がないため、検証プロパティ違反の解析をより効率的かつ正確に行うことができる。
【００７２】
また、本発明では、検証プロパティに基づいて状態機械を用いて行われた論理検証によって検証プロパティ違反が検出されると、違反の原因が同じものについては波形表示上に複数の検証プロパティ違反を示す情報を表示しないようにすることができる。従って、ユーザは、同じ原因の検証プロパティ違反を何度も解析する必要がなく、効率的に検証プロパティ違反の解析を行うことができる。
【００７３】
更に、同じ原因の検証プロパティ違反のうち初回に検出された違反を波形表示上に表示させることによって、ユーザは、大量の同じ原因による検証プロパティ違反の検出の中に埋もれている重大な検証プロパティ違反を見逃さないようにすることができる。
【００７４】
以上の説明に関し、更に以下の項を開示する。
（付記１）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法。
（付記２）
前記表示制御手順は、前記プロパティ表示手順によって表示された前記検証プロパティ上への前記操作入力に応じて、該操作入力によって選択された前記検証プロパティの記述部分に連動させて該記述部分に対応する前記波形表示手順によって表示された前記波形上の波形部分を他波形部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記１記載の論理検証方法。
（付記３）
前記表示制御手順は、
前記検証プロパティに基づいて生成された構文木の要素と該構文木に基づいて生成された状態機械によって示される前記検証プロパティの実行過程で遷移する状態との対応関係を示す構文木−状態機械対応情報と、前記状態機械の状態と前記生成された波形の波形状態との対応関係を示す状態機械−波形対応情報とを用いて、前記操作入力に応じて前記波形部分と前記記述部分とを関連づけて連動させることを特徴とする付記１又は２記載の論理検証方法。
（付記４）
前記プロパティ表示手順は、
前記検証プロパティの要素と該検証プロパティに基づいて生成された構文木の要素との対応関係を示すプロパティ−構文木対応情報を用いて、前記検証プロパティの前記記述部分と他記述部分とを区別して表示することを特徴とする付記１乃至３のいずれか一項記載の論理検証方法。
（付記５）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とする論理検証方法。
（付記６）
前記検証プロパティを表示するプロパティ表示手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記前提条件状態となる範囲に対応する前記検証プロパティの前提条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記５記載の論理検証方法。
（付記７）
前記論理検証実行手順は、前記状態機械によって示される事後条件状態となる範囲を前記波形データに設定し、
前記表示制御手順は、前記事後条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御することを特徴とする付記５又は６記載の論理検証方法。
（付記８）
前記表示制御手順は、前記波形表示手順によって表示された前記事後条件状態となる範囲に対応する前記検証プロパティの事後条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする付記７記載の論理検証方法。
（付記９）
前記論理検証実行手順は、前記状態機械によって示される違反発生状態となる範囲を前記波形データに設定し、
前記表示制御手順は、違反発生を示す情報を示すように前記波形表示手順を制御することを特徴とする付記５乃至８のいずれか一項記載の論理検証方法。
（付記１０）
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とする論理検証方法。
（付記１１）
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、検出された初回の該違反発生状態に対応する部分を波形データに設定することを特徴とする付記１０記載の論理検証方法。
（付記１２）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とするコンピュータ実行可能なプログラム。
（付記１３）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を該波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とするコンピュータ実行可能なプログラム。
（付記１４）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置としてコンピュータに機能させるためのコンピュータ実行可能なプログラムであって、該コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とするコンピュータ実行可能なプログラム。
（付記１５）
検証プロパティに基づいて状態機械を用いて論理検証を行なう論理検証装置であって、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手段と、
前記検証プロパティを表示するプロパティ表示手段と、
操作入力に応じて前記波形表示手段と前記プロパティ表示手段とを制御する表示制御手段とを実行させ、
前記表示制御手段は、前記波形表示手段によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手段に表示させることを特徴とする論理検証装置。
本発明は、具体的に開示された実施例に限定されるものではなく、特許請求の範囲から逸脱することなく、種々の変形や変更が可能である。
【図面の簡単な説明】
【００７５】
【図１】本発明の一実施例に係る論理検証装置のハードウェア構成を示す図である。
【図２】論理検証処理の概要を説明するための図である。
【図３】表示操作に応じてプロパティ表示と波形表示とが連動する表示例を示す図である。
【図４】プロパティ内の記述と波形表示とを連動させるための対応関係の例を示す図である。
【図５】検証プロパティの条件記述に応じた波形表示例を示す図である。
【図６】図５に示す表示方法においてプロパティ表示と波形表示とが連動して表示される表示例を示す図である。
【図７】強調表示をプロパティ表示と波形表示とで連動させるための対応関係の例を示す図である。
【図８】検証プロパティ違反が異なる状態遷移を経て発生する場合の対応関係の例を示す図である。
【図９】検証プロパティ違反の表示を間引く処理がなされなかった場合の波形データの例を示す図である。
【図１０】遷移経路別カウンタの例を示す図である。
【図１１】検証プロパティ違反の表示を間引いた処理がなされた場合の波形データの例を示す図である。
【符号の説明】
【００７６】
１１ ＣＰＵ
１２ メモリユニット
１３ 表示ユニット
１５ 入力ユニット
１７ 記憶装置
１８ ドライバ
１９ 記憶媒体
９０ 遷移経路別カウンタ
１００ 論理検証装置
１０１ 論検証処理部
１０２ 論理プロパティ
１０３ 検証対象データ
１０４ 検証環境データ
１０５ プロパティ表示
１０６ 波形表示
１０７ 表示操作
１０８ プロパティ入力部
１０９ 構文木
１１０ プロパティ表示部
１１１ プロパティ−構文木対応情報
１１２ 状態機械生成部
１１３ 状態機械
１１４ 構文木−状態機械対応情報
１１５ 論理検証実行部
１１６ 波形データ
１１７ 状態機械−波形対応情報
１１８ 波形表示部
１１９ 表示操作部
１２０ プロパティ表示付加情報
１２１ 波形表示付加情報
２０１ プロパティ表示
２０３、２０４ 強調表示
３０１、６０１ 検証プロパティ
３０２、６０２ 構文木
３０３、６０３ 状態機械
３０４、６０４ 波形データ
４０１ 波形表示
４０２、６１２ 前提条件範囲
４０３、６１３ 事後条件範囲
４０４、６１４ 違反発生範囲
５０１ プロパティ表示
５０２ 前提条件
５０３ 事後条件
７０１ 検証プロパティ
７０２ 状態機械
７０３ 第一条件
７０４ 第二条件
７０５ 事後条件
７０６ 第一条件状態
７０７ 第二条件状態
７０８ 事後条件状態
７０９ 違反発生状態
８０１、９０１ 波形データ
８０２、８０３ 検証プロパティ違反
【特許請求の範囲】
【請求項１】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法。
【請求項２】
前記表示制御手順は、前記プロパティ表示手順によって表示された前記検証プロパティ上への前記操作入力に応じて、該操作入力によって選択された前記検証プロパティの記述部分に連動させて該記述部分に対応する前記波形表示手順によって表示された前記波形上の波形部分を他波形部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項１記載の論理検証方法。
【請求項３】
前記表示制御手順は、
前記検証プロパティに基づいて生成された構文木の要素と該構文木に基づいて生成された状態機械によって示される前記検証プロパティの実行過程で遷移する状態との対応関係を示す構文木−状態機械対応情報と、前記状態機械の状態と前記生成された波形の波形状態との対応関係を示す状態機械−波形対応情報とを用いて、前記操作入力に応じて前記波形部分と前記記述部分とを関連づけて連動させることを特徴とする請求項１又は２記載の論理検証方法。
【請求項４】
前記プロパティ表示手順は、
前記検証プロパティの要素と該検証プロパティに基づいて生成された構文木の要素との対応関係を示すプロパティ−構文木対応情報を用いて、前記検証プロパティの前記記述部分と他記述部分とを区別して表示することを特徴とする請求項１乃至３のいずれか一項記載の論理検証方法。
【請求項５】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態なる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とする論理検証方法。
【請求項６】
前記検証プロパティを表示するプロパティ表示手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記前提条件状態となる範囲に対応する前記検証プロパティの前提条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項５記載の論理検証方法。
【請求項７】
前記論理検証実行手順は、前記状態機械によって示される事後条件状態となる範囲を前記波形データに設定し、
前記表示制御手順は、前記事後条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御することを特徴とする請求項５又は６記載の論理検証方法。
【請求項８】
前記表示制御手順は、前記波形表示手順によって表示された前記事後条件状態となる範囲に対応する前記検証プロパティの事後条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項７記載の論理検証方法。
【請求項９】
前記論理検証実行手順は、前記状態機械によって示される違反発生状態となる範囲を前記波形データに設定し、
前記表示制御手順は、違反発生を示す情報を示すように前記波形表示手順を制御することを特徴とする請求項５乃至８のいずれか一項記載の論理検証方法。
【請求項１０】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とする論理検証方法。
【請求項１】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理による論理検証結果に基づいて生成された波形を表示する波形表示手順と、
前記検証プロパティを表示するプロパティ表示手順と、
操作入力に応じて前記波形表示手順と前記プロパティ表示手順とを制御する表示制御手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記波形上への前記操作入力に応じて、該操作入力によって選択された波形部分に連動させて該波形部分に対応する前記検証プロパティの記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする論理検証方法。
【請求項２】
前記表示制御手順は、前記プロパティ表示手順によって表示された前記検証プロパティ上への前記操作入力に応じて、該操作入力によって選択された前記検証プロパティの記述部分に連動させて該記述部分に対応する前記波形表示手順によって表示された前記波形上の波形部分を他波形部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項１記載の論理検証方法。
【請求項３】
前記表示制御手順は、
前記検証プロパティに基づいて生成された構文木の要素と該構文木に基づいて生成された状態機械によって示される前記検証プロパティの実行過程で遷移する状態との対応関係を示す構文木−状態機械対応情報と、前記状態機械の状態と前記生成された波形の波形状態との対応関係を示す状態機械−波形対応情報とを用いて、前記操作入力に応じて前記波形部分と前記記述部分とを関連づけて連動させることを特徴とする請求項１又は２記載の論理検証方法。
【請求項４】
前記プロパティ表示手順は、
前記検証プロパティの要素と該検証プロパティに基づいて生成された構文木の要素との対応関係を示すプロパティ−構文木対応情報を用いて、前記検証プロパティの前記記述部分と他記述部分とを区別して表示することを特徴とする請求項１乃至３のいずれか一項記載の論理検証方法。
【請求項５】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される前提条件状態となる範囲を波形データに設定する論理検証実行手順と、
前記波形データに基づいて生成された波形を表示する波形表示手順と、
操作入力に応じて前記前提条件状態なる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御する表示制御手順とを実行させることを特徴とする論理検証方法。
【請求項６】
前記検証プロパティを表示するプロパティ表示手順とを実行させ、
前記表示制御手順は、前記波形表示手順によって表示された前記前提条件状態となる範囲に対応する前記検証プロパティの前提条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項５記載の論理検証方法。
【請求項７】
前記論理検証実行手順は、前記状態機械によって示される事後条件状態となる範囲を前記波形データに設定し、
前記表示制御手順は、前記事後条件状態となる範囲を他範囲と異なる表示方法で前記波形を表示させるように前記波形表示手順を制御することを特徴とする請求項５又は６記載の論理検証方法。
【請求項８】
前記表示制御手順は、前記波形表示手順によって表示された前記事後条件状態となる範囲に対応する前記検証プロパティの事後条件の記述部分を他記述部分と異なる表示方法で前記プロパティ表示手順に表示させることを特徴とする請求項７記載の論理検証方法。
【請求項９】
前記論理検証実行手順は、前記状態機械によって示される違反発生状態となる範囲を前記波形データに設定し、
前記表示制御手順は、違反発生を示す情報を示すように前記波形表示手順を制御することを特徴とする請求項５乃至８のいずれか一項記載の論理検証方法。
【請求項１０】
検証プロパティに基づいて状態機械を用いて論理検証処理を行う論理検証方法であって、コンピュータに、
前記論理検証処理を実行して波形データを生成し、該状態機械によって示される違反発生状態に対応する部分を波形データに設定する論理検証実行手順と、
前記波形データに基づいて波形を表示すると共に、前記違反発生状態を示す情報を該違反発生状態に対応する部分に表示する波形表示手順とを実行させ、
前記論理検証実行手順は、同じ原因による前記違反発生状態が複数回検出される場合、所定回数に対応する部分を波形データに設定することを特徴とする論理検証方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【公開番号】特開２００８−２５０８０８（Ｐ２００８−２５０８０８Ａ）
【公開日】平成２０年１０月１６日（２００８．１０．１６）
【国際特許分類】
【出願番号】特願２００７−９３０４７（Ｐ２００７−９３０４７）
【出願日】平成１９年３月３０日（２００７．３．３０）
【出願人】（３０８０１４３４１）富士通マイクロエレクトロニクス株式会社 (2,507)
【Ｆターム（参考）】
【公開日】平成２０年１０月１６日（２００８．１０．１６）
【国際特許分類】
【出願日】平成１９年３月３０日（２００７．３．３０）
【出願人】（３０８０１４３４１）富士通マイクロエレクトロニクス株式会社 (2,507)
【Ｆターム（参考）】
[ Back to top ]