(57)【特許請求の範囲】
【請求項１】
タイミングダイアグラムに、検証対象となる論理回路の端子および内部ピンを介して入出力する信号の波形間の論理的関係と、前記論理的関係が少なくとも１回は成立するかを示す生起情報とが入力される第１の手段と、
前記波形間の論理的関係と、前記生起情報とを基に前記検証対象となる論理回路の機能を検証する為の検証記述を前記タイミングダイアグラムから生成する第２の手段とを有し、
前記第１の手段は、前記検証対象となる論理回路の端子および内部ピンの情報を取得する端子情報抽出手段と、前記端子情報抽出手段で取得された前記検証対象となる論理回路の端子および内部ピンの情報から前記波形間の論理的関係や前記生起情報を入力されることで前記タイミングダイアグラムを編集可能とされるタイミングダイアグラム編集手段とを含み、
前記第１の手段において、前記タイミングダイアグラムに前記検証対象となる論理回路の動作内容や検証したい信号の遷移を記載する為に前記波形間の論理的関係や前記生起情報を含むオブジェクトを用いることを特徴とする機能検証記述生成装置。
【請求項２】
請求項１に記載の機能検証記述生成装置において、
前記端子情報抽出手段は、設計データに備わる前記端子および前記内部ピンに関して、少なくとも端子名、内部ピン名、入出力の別、および入出力する前記信号と内部ピン名のビット数の各端子および内部ピン情報を取得し、
前記タイミングダイアグラム編集手段は、前記端子情報抽出手段に接続され、前記端子情報抽出手段にて取得した前記端子および前記内部ピン情報を選択し、前記端子および内部ピンを介して入出力する前記信号について、前記信号の波形、セットアップタイムおよびホールドタイムを含むタイミング制約情報、前記信号の波形間の論理的関係情報、および前記生起情報を入力されることで、前記設計データにおける前記タイミングダイアグラムを編集可能とされることを特徴とする機能検証記述生成装置。
【請求項３】
請求項２に記載の機能検証記述生成装置において、
前記第２の手段は、
前記タイミングダイアグラム編集手段に接続され、前記タイミングダイアグラム編集手段から前記各端子および内部ピン情報、前記タイミング制約情報、前記波形間の論理的関係情報、および前記論理的関係の生起情報からなる検証対象動作情報を抽出する検証対象動作抽出手段と、
前記検証対象動作抽出手段に接続され、前記検証対象動作情報に基づき検証記述言語で表現された前記検証対象動作が満足されているかの検証を目的とする機能検証記述やＨＤＬ形式の前記検証対象動作が満足されているかの検証を目的とする機能検証記述を生成する検証記述生成手段と、を含むことを特徴とする機能検証記述生成装置。
【請求項４】
請求項１に記載の機能検証記述生成装置において、
前記オブジェクトは、前記タイミングダイアグラムに描かれた信号波形間の論理的関係を表す為のオブジェクトであるリレーションオブジェクトの始点または終点となった所の値と、その値がタイミングダイアグラム上の何サイクル目かを表すオブジェクトであるシグナルオブジェクトを含むことを特徴とする機能検証記述生成装置。
【請求項５】
請求項１に記載の機能検証記述生成装置において、
前記オブジェクトは、前記タイミングダイアグラムに描かれた信号波形上に設定され、前記タイミングダイアグラムに描かれた信号波形間の論理的関係を表す為のオブジェクトであるリレーションオブジェクトの始点または終点となった所の信号値に対して、信号値比較などの比較演算を記述するオブジェクトであるコンペアオブジェクトを含むことを特徴とする機能検証記述生成装置。
【請求項６】
請求項１に記載の機能検証記述生成装置において、
前記オブジェクトは、前記タイミングダイアグラムに描かれたクロック信号の立ち上がりエッジに対して指定され、所定の条件が成立するまで、その前のサイクルの信号値が繰り返し実行されることを表すオブジェクトであるウェイトオブジェクトを含むことを特徴とする機能検証記述生成装置。
【請求項７】
請求項１に記載の機能検証記述生成装置において、
前記オブジェクトは、前記タイミングダイアグラムに描かれた信号波形間の論理的関係を表すオブジェクトであるリレーションオブジェクトを含むことを特徴とする機能検証記述生成装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、機能検証装置に関し、特にハードウェア機能記述言語の形式で記述された、たとえばＣＰＵ（中央演算処理装置）やＤＳＰ（デジタル信号処理装置）などのデジタル回路全般の機能検証における機能検証記述の生成装置に適用して有効な技術に関する。
【０００２】
【従来の技術】
本発明者が検討したところによれば、機能検証装置に関しては、たとえば特開平６−３３２９７１号公報に記載される技術などが挙げられる。前記特開平６−３３２９７１号公報には、端子情報と、この端子の入出力信号波形と、この入出力信号波形のタイミング制約情報を伴うタイミングダイアグラムからＨＤＬ（ハードウェア機能記述言語）形式の機能モデルを生成するＨＤＬ生成手段を有する機能モデル生成装置が開示されている。
【０００３】
【発明が解決しようとする課題】
ところで、前記特開平６−３３２９７１号公報の機能モデル生成装置では、タイミングダイアグラム上に検証項目を明確に記述する手段が提供されておらず、さらに明確化された機能検証項目を検証するための機能検証記述の生成も行っていない。特に、ＨＤＬ以外の検証記述言語による記述生成は行っていない。
【０００４】
また、本発明者が、前記のような機能検証装置に関して検討した結果、以下のようなことが明らかとなった。
【０００５】
たとえば、論理回路からなる回路素子について、近年、ＨＤＬを入力する高性能の機能シミュレータの出現に伴い、ハードウェアの機能設計をＨＤＬで行うという設計スタイルが定着してきた。また、近年、検証すべき論理回路の大規模化に伴い、機能シミュレータを用いた機能検証を効率的に行うための検証記述言語や時相論理や時区間論理に基づいた検証記述言語を用いるモデル検査法による網羅的な機能検証技術も定着してきた。特に、論理回路の機能検証においては、設計者や検証担当者はタイミングダイアグラムを用いて回路動作の検証内容の明確化を行うが、作成したタイミングダイアグラムから直接に検証対象論理回路の検証を行うための手段が提供されず、マニュアルでＨＤＬやＨＤＬ以外の検証記述言語による機能検証記述を整備する必要がある。
【０００６】
しかしながら、機能検証記述を作成するためには、たとえば検証担当者がＨＤＬやＨＤＬ以外の機能記述言語を記述できなければならず、そのため検証担当者はＨＤＬやＨＤＬ以外の検証記述言語を学習しなければならず、検証担当者にとって負担が大きいという問題がある。また、ＨＤＬを学習済みの設計者がＨＤＬで機能検証記述を作成する場合であっても、ＨＤＬで記述した機能検証記述自体の検証を行わねばならず、さらに大規模な論理回路においては機能検証項目が多いことから、同様にＨＤＬを学習済みの設計者にとって負担が大きいという問題がある。
【０００７】
そこで、本発明は、このような問題を解決するためになされたもので、検証担当者が新たにＨＤＬやＨＤＬ以外の検証記述言語を学習しなくても、ＨＤＬを学習済みの設計者がＨＤＬ以外の検証記述言語を学習したり、ＨＤＬで記述した機能検証記述自体の検証を行わなくても、検証対象回路の機能検証項目を検証するための機能検証記述を作成可能とする機能検証記述生成装置を提供することを目的とするものである。
【０００８】
また、設計者や検証担当者はタイミングダイアグラムを用いて回路動作の検証内容の明確化を行う場合、タイミングダイアグラム上に検証項目を明確に記述する手段が与えられておらず、検証項目を表現する手段が曖昧になり、設計者や検証担当者の間で正確な情報の交換ができず、人的ミスによる検証効率の低下が起こるという問題がある。
【０００９】
そこで、本発明は、このような問題をも解決するためになされており、設計者や検証担当者がタイミングダイアグラムを用いて回路動作の検証内容を明確にかつ統一的に記述する記述法を提供することも目的とするものである。
【００１０】
本発明の前記ならびにその他の目的と新規な特徴は、本明細書の記述および添付図面から明らかになるであろう。
【００１１】
【課題を解決するための手段】
本願において開示される発明のうち、代表的なものの概要を簡単に説明すれば、次のとおりである。
【００１２】
すなわち、本発明による機能検証装置は、タイミングダイアグラムに波形間の論理的関係と、前記論理的関係の生起情報とを入力する手段と、前記波形間の論理的関係と、前記論理的関係の生起情報とを基に検証記述をタイミングダイアグラムから生成する手段と、を有することを特徴とするものである。特に、タイミングダイアグラムの作成時に、予め用意されたオブジェクトを挿入しながら記述可能とし、かつ作成データから機能検証に用いる動作仕様チェッカＨＤＬ記述、およびモデル検査法で用いられるプロパティ言語記述を自動生成し、内部動作のチェック、外部入力信号が満たすべき信号遷移を守っているかのチェックを可能とするものである。
【００１３】
具体的に、本発明による機能検証装置は、検証対象のＨＤＬ形式の設計データを読み込んで、この読み込んだ検証対象のＨＤＬ形式の設計データに備わる端子および内部ピンに関して、少なくとも端子名、内部ピン名、入出力の別、および入出力信号と内部ピン名のビット数の各端子および内部ピン情報を取得する端子情報抽出手段と、前記端子情報抽出手段に接続され、端子情報抽出手段にて取得した各端子および内部ピン情報を選択し、前記端子および内部ピンを介して入出力する信号について、この信号と波形を含みタイミングに関するタイミング制約情報、この波形間の論理的関係、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報を入力することで、前記検証対象のＨＤＬの設計データにおけるタイミングダイアグラムを編集するタイミングダイアグラム編集手段と、前記タイミングダイアグラム編集手段に接続され、前記タイミングダイアグラム編集手段から前記各端子および内部ピン情報、前記タイミング制約情報、前記波形間の論理的関係情報、および前記論理的関係の生起情報からなる検証対象動作情報を抽出する検証対象動作抽出手段と、前記検証対象動作抽出手段に接続され、前記検証対象動作情報に基づき検証記述言語で表現された前記検証対象動作が満足されているかの検証を目的とする機能検証記述やＨＤＬ形式の前記検証対象動作が満足されているかの検証を目的とする機能検証記述を生成する検証記述生成手段と、を備えたことを特徴とする。
【００１４】
このように構成することで、設計者や検証担当者は検証対象の比較的操作可能なタイミングダイアグラム編集手段上でＨＤＬの記述から得られた端子および内部ピン情報を選択し、タイミングダイアグラム編集手段上で、この選択後の端子や内部ピンの信号の波形、この波形間の論理的関係、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報を入力しながら、タイミングダイアグラム編集手段上でタイミングダイアグラムを作成編集する。よって、タイミングダイアグラム編集手段は、タイミングダイアグラム上に検証項目を明確に記述することが可能となるように作用し、よって検証項目の表現の曖昧さを排除するように作用する。よって、設計者や検証担当者の間で正確な情報の交換が可能となるように作用し、人的ミスを排除するように作用する。
【００１５】
さらに、検証対象動作抽出手段は、前記タイミングダイアグラム編集手段を使用し、設計者や検証担当者によって編集されたタイミングダイアグラム編集手段から送出されるタイミングダイアグラム情報から波形間の論理的関係、この論理的関係が指定された波形を含む端子や内部ピン情報、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報などを抽出し、検証記述生成手段は前記検証対象動作抽出手段から供給される前記波形の論理的関係、この論理的関係が指定された波形を含む端子や内部ピン情報、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報などに基づき機能検証記述を自動生成する。よって、検証記述生成手段などは、設計者や検証担当者がＨＤＬやＨＤＬ以外の検証記述言語を知らなくとも、タイミングダイアグラム編集手段を使用してタイミングダイアグラムを編集して回路動作の検証内容の明確化を行うという設計者や検証担当者が従来より行っている操作を行うことで、機能検証記述を生成する。よって、検証記述生成手段などは、設計者や検証担当者の機能検証作業負担を軽減するように作用し、機能検証効率の向上による設計コストの低減、さらには製品の生産コストを低減するように作用する。
【００１６】
なお、本発明の技術と、前記特開平６−３３２９７１号公報の技術とを比較した場合には、以下のような違いがある。前記特開平６−３３２９７１号公報の技術は、ＨＤＬにより設計記述が存在しない機能ブロックではあるが、シミュレーションによる検証を行う際に何らかのＨＤＬ記述が必要となるものに対して、ＨＤＬの動作モデル記述を生成する技術であり、本発明の技術はＨＤＬによる設計記述が存在し、その設計データの検証を行うためのＨＤＬ記述を生成する技術である。その違いは、入力データの違いに現れていると言える。すなわち、特開平６−３３２９７１号公報の技術がタイミングダイアグラムを編集する手段から始まっているのに対して、本発明の技術が設計データの読み込み手段から始まっている。
【００１７】
以下において、両者の技術の違いを図６５および図６６にて簡単に説明する。たとえば、メモリインターフェースのＨＤＬ記述を作成し、その検証を行おうとすると、メモリをＨＤＬで記述する必要があるが、公報の技術（図６５）によれば、メモリの動作モデルを記述したＨＤＬがタイミングダイアグラムから生成可能である。ただし、メモリアクセスの動作が正しいかの検証はシミュレータがサポートする波形ビューワで目視による動作確認を行うか、動作が正しいかを検証するためのＨＤＬのチェッカを記述する必要がある。
【００１８】
これに対して、本発明の技術（図６６）を適用すると、メモリの動作モデルが不要となるばかりでなく、動作が正しく行われているかを検証するためのＨＤＬ記述が自動生成できるため、動作が正しく行われているかの確認が自動化される。また、前記の例では、入力と出力の両方を見ているが、入力のみ、出力のみをチェックする記述を生成することも可能であり、前者は、たとえば前段の論理回路ＨＤＬが正しい出力信号を検証対象ＨＤＬに送出しているかを検証する目的で用いることができ、後者は検証対象ＨＤＬが正しい出力信号の系列を出力しているかを検証する目的で用いることができる。
【００１９】
【発明の実施の形態】
以下、本発明の実施の形態を図面に基づいて詳細に説明する。なお、実施の形態を説明するための全図において、同一部材には同一の符号を付し、その繰り返しの説明は省略する。
【００２０】
また、本発明の実施の形態では、１．機能検証記述生成装置の構成、２．オブジェクトの説明、３．検証対象動作木の構成とその変形、４．ＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍ、５．ＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍ、の順に説明する。
【００２１】
１．機能検証記述生成装置の構成
図１により、本発明の一実施の形態の機能検証記述生成装置の構成の一例を説明する。図１は本実施の形態の機能検証記述生成装置を示す構成図である。
【００２２】
本実施の形態の機能検証記述生成装置は、大きく分類すると、端子情報抽出手段である端子情報抽出装置１と、タイミングダイアグラム編集手段であるタイミングダイアグラム編集装置２と、検証対象動作抽出手段である検証対象動作抽出装置３と、検証記述生成手段である検証記述生成装置４などからなり、検証記述生成装置４により生成された検証記述は検証記述ファイル５に格納されるような構成となっている。
【００２３】
端子情報抽出装置１は、ＨＤＬ読み込み装置１１、このＨＤＬ読み込み装置１１の出力側に接続されるＨＤＬ記憶装置１２、このＨＤＬ記憶装置１２の出力側に接続される端子情報抽出装置１３、この端子情報抽出装置１３の出力側に接続される端子情報記憶装置１４から構成される。この端子情報抽出装置１は、検証対象のＨＤＬ形式の設計データを読み込んで、この読み込んだ検証対象のＨＤＬ形式の設計データに備わる端子および内部ピンに関して、少なくとも端子名、内部ピン名、入出力の別、および入出力信号と内部ピン名のビット数の各端子および内部ピン情報を取得する端子情報抽出手段である。
【００２４】
タイミングダイアグラム編集装置２は、上記端子情報抽出装置１、すなわち上記端子情報記憶装置１４の出力側に接続される。このタイミングダイアグラム編集装置２は、上記端子情報抽出装置１にて取得した各端子および内部ピン情報を選択し、端子および内部ピンを介して入出力する信号について、この信号と波形を含みタイミングに関するタイミング制約情報、この波形間の論理的関係、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報を入力することで、検証対象のＨＤＬの設計データにおけるタイミングダイアグラムを編集するタイミングダイアグラム編集手段である。
【００２５】
検証対象動作抽出装置３は、上記タイミングダイアグラム編集装置２の出力側に接続されるタイミングダイアグラム記憶装置３１、このタイミングダイアグラム記憶装置３１の出力側に接続される検証対象動作情報抽出装置３２、この検証対象動作情報抽出装置３２の出力側に接続される検証対象動作情報記憶装置３３から構成される。この検証対象動作抽出装置３は、タイミングダイアグラム編集装置２から各端子および内部ピン情報、タイミング制約情報、波形間の論理的関係情報、および論理的関係の生起情報からなる検証対象動作情報を抽出する検証対象動作抽出手段である。
【００２６】
検証記述生成装置４は、上記検証対象動作抽出装置３、すなわち上記検証対象動作情報記憶装置３３の出力側に接続される。この検証記述生成装置４は、検証対象動作情報に基づき検証記述言語で表現された検証対象動作が満足されているかの検証を目的とする機能検証記述やＨＤＬ形式の検証対象動作が満足されているかの検証を目的とする機能検証記述を生成する検証記述生成手段である。
【００２７】
２．オブジェクトの説明
図２〜図５により、本実施の形態の機能検証記述生成装置において、オブジェクトの一例を説明する。図２はコンペアオブジェクトを説明するための回路例の説明図、図３はコンペアオブジェクトを説明するためのタイミングダイアグラム例の説明図、図４はウェイトオブジェクトを説明するためのタイミングダイアグラム例の説明図、図５はウェイトオブジェクトを説明するためのチェックボックス例の説明図である。
【００２８】
タイミングダイアグラムに動作内容や、検証したい信号遷移を明示的に記述することを可能とする目的で、シグナルオブジェクト（ｓｉｇｎａｌ  ｏｂｊｅｃｔ）、コンペアオブジェクト（ｃｏｍｐａｒｅ  ｏｂｊｅｃｔ）、ウェイトオブジェクト（ｗａｉｔ  ｏｂｊｅｃｔ）、リレーションオブジェクト（ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ）の４種類のオブジェクトを導入する。
【００２９】
２−１．シグナルオブジェクト（ｓｉｇｎａｌ  ｏｂｊｅｃｔ）
タイミングダイアグラムに描かれた信号波形のｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔの始点または終点となった所の値とその値がタイミングダイアグラム上の何サイクル目かを表す。特に、値としては、信号値と信号変化を取ることができる。また、信号変化は、特定の信号値から特定の信号値、特定の信号値からの変化、特定の信号値への変化、および特定の信号値が与えられている分けではないが信号値の変化、何れかを表現可能とする。さらに、ｅｘｉを指定することで、たとえば「指定サイクルで信号変化する、ということが少なくとも１回は起こる」や「指定サイクルで信号値がある値になる、ということが少なくとも１回は起こる」などを表現可能とする。
【００３０】
２−２．コンペアオブジェクト（ｃｏｍｐａｒｅ  ｏｂｊｅｃｔ）
タイミングダイアグラムに描かれた信号波形上に設定することで、設定された信号値に対して、信号値比較などの比較演算を記述することが可能である。特に、比較を行う際に左辺にはｃｏｍｐａｒｅ  ｏｂｊｅｃｔが指定された信号のみからなる、ビット切り出しやシフト、インクリメント、デクリメントなどの算術論理演算が記述可能である。また、右辺には、タイミングダイアグラムに描かれた任意の信号、信号：ｎ形式にて与えられるｃｏｍｐａｒｅ  ｏｂｊｅｃｔが指定されたサイクルからｎサイクル前の信号値を表す信号、およびそれらのビット切り出しからなる算術論理演算式が記述可能である。比較演算としては、＜、≦、＝＝、≠、≧、＞の何れかが記述可能である。さらに、ｅｘｉを指定することで、「指定サイクルでｃｏｍｐａｒｅ  ｏｂｊｅｃｔに設定された比較演算が成立する、ということが少なくとも１回は起こる」を表現可能とする。
【００３１】
たとえば、図２に示す回路例では、マルチサイクルの加算器（レイテンシー＝３サイクル）において、ＣＬＫ、Ｖａｌｉｄ、Ａ［７：０］、Ｂ［７：０］の入力に対してＤ［８：０］を出力する場合である。機能は、Ｖａｌｉｄ立ち上がりで入力データＡ［７：０］とＢ［７：０］を取り込み、３サイクル後に加算結果を出力する。正しく加算が行われているかを検証対象とする。
【００３２】
この図２のマルチサイクルの加算器において、タイミングダイアグラム例は、たとえば図３に示すように、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔのｒｅｌ＿Ｈ１の始点αと終点βにおける、ｃｏｍｐａｒｅ  ｏｂｊｅｃｔのｃｏｍｐａｒｅ（Ｄ＝＝Ａ：３＋Ｂ：３）を示している。
【００３３】
２−３．ウェイトオブジェクト（ｗａｉｔ  ｏｂｊｅｃｔ）
タイミングダイアグラムに描かれたクロック信号の立ち上がりエッジに対して指定可能であり、ある条件（以降、ｗａｉｔ解除条件という）が成立するまで、その前のサイクルの信号値が繰り返し実行されることを表す。特に、ｗａｉｔ解除条件はタイミングダイアグラム上の任意の信号、およびそのビット切り出しからなる算術論理演算式を指定可能である。また、繰り返し実行において、チェックされるべき信号名を指定可能である。特に、繰り返し実行でチェックする信号を指定しなければ、「何時かｗａｉｔ解除条件が成立」を表す。さらに、ｅｘｉを指定することで、「何時かｗａｉｔ解除条件が成立する、ということが少なくとも１回は起こる」や「何時かｗａｉｔ解除条件が成立し、それまでは指定信号が繰り返し同じ値を取る、ということが少なくとも１回は起こる」を表現可能である。
【００３４】
たとえば、複数のｗａｉｔ  ｏｂｊｅｃｔを設定する場合、特にｏｂｊｅｃｔ間の順番だけが規定可能で、サイクル差を指定できない場合がある。これに対応するため、図４に示すような特殊仕様を設ける。このタイミングダイアグラム例では、Ａ立ち上がりの１サイクル後にｗａｉｔ（（Ｂ＝＝Ｃ）＆Ｂ＆！Ｅ）が成立後、最低０サイクル経過した後、ｗａｉｔ（（Ｂ＝＝Ｃ）＆＆！Ｅ）が成立し、その最低０サイクル後、ｗａｉｔ（Ａ＝＝１）が成立することを意味している。なお、ｗａｉｔ（Ａ＝＝１）成立後の１サイクル後にＤが０から１に変化することも示している。
【００３５】
また、チェックボックス例は、たとえば図５に示すように、信号名Ａ〜Ｅの繰り返しとＷａｉｔ解除のボックスに対して、チェックでチェック対象、ノンチェックで非対象とし、またデフォルトはノンチェックとする。ただし、信号値がＤｏｎ’ｔ  ｃａｒｅの場合は、デフォルトでチェックし、ユーザによる変更不可とする。
【００３６】
２−４．リレーションオブジェクト（ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ）
タイミングダイアグラムに描かれた信号波形間の論理的関係を表す。つまり、ある信号があるサイクルである値を取ったなら、ある信号があるサイクルである値を取るということを表現するためのものである。−＞を”ならば”とすると、Ａ−＞Ｂなる命題の−＞を表現するのがｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔの役目である。なお、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔの始点・終点としては、全てのｏｂｊｅｃｔを取ることが可能である。また、終点が一致する場合、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士の論理演算を指定可能であり、たとえば（Ａ−＞Ｂ）△（Ｃ−＞Ｂ）の場合、Ａ△Ｃ−＞Ｂと解釈する。特に、△は論理ＡＮＤ、論理ＯＲ、論理ＥＯＲの何れかを表す。さらに、（Ａ−＞Ｂ）−＞Ｃは、Ａ−＞（Ｂ−＞Ｃ）＝Ａ＆Ｂ−＞Ｃと解釈され、一般に、ｎ個のｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔにより直列に構成される命題式は括弧の付け方によらず、
Ａ１−＞Ａ２−＞・・・Ａｎ−＞Ａｎ＋１    式（１）
と解釈され、その意味は下記で与えられる。
【００３７】
Ａ１＆Ａ２＆・・・＆Ａｎ−＞Ａｎ＋１
特に、Ａ１−＞Ａ２、Ａ２−＞Ａ３とｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔと指定した場合は、個別に、
Ａ１−＞Ａ２
Ａ２−＞Ａ３
の命題が描かれたものとして解釈を行う。すなわち、式（１）に示す命題を得るためには、必ず、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔを始点または終点にして描く必要がある。たとえば、
Ａ１−＞Ａ２、（Ａ１とＡ２を結ぶｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ）−＞Ａ３
と描くと、
（Ａ１−＞Ａ２）−＞Ａ３
となり、結局、
Ａ１＆Ａ２−＞Ａ３
と解釈される。また、
Ａ２−＞Ａ３、Ａ１−＞（Ａ２とＡ３を結ぶｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ）
と描くと、
Ａ１−＞（Ａ２−＞Ａ３）＝Ａ１＆Ａ２−＞Ａ３
と解釈される。
【００３８】
さらに、ｅｘｉの指定は、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔにより構成された命題の−＞に対応する部分に指定したときのみ有効であり、それ以外は無視され、指定が有効な場合、「命題が成立する、ということが少なくとも１回は起こる」と解釈される。
【００３９】
３．検証対象動作木の構成とその変形
図６〜図２７により、検証対象動作木の構成とその変形の一例を説明する。図６は検証対象動作木の構成とその変形を示すフロー図、図７はＨＤＬの端子情報の格納における階層ツリーを示す説明図、図８は図７の階層ツリーに付随する端子情報を示す説明図、図９〜図１９はタイミングダイアグラムの格納におけるタイミングダイアグラム例を示す説明図、図２０はタイミングダイアグラム分割例を示す説明図、図２１および図２２はタイミングダイアグラムの記憶イメージを示す説明図、図２３はタイミングダイアグラム分割手段の動作を示すフロー図、図２４は検証対象動作の切り出しにおける検証対象動作情報取得手段の動作を示すフロー図、図２５は検証対象動作情報の記憶イメージを示す説明図、図２６および図２７は検証対象動作から作成される木構造の記憶イメージを示す説明図である。
【００４０】
図６に示すように、検証対象動作木の構成とその変形は、まず、入力ＨＤＬの端子情報の格納方式を述べ（ステップＳ１０１）、次いで、入力したタイミングダイアグラムをどのような形式で記憶装置に格納するかを述べ（ステップＳ１０２）、最後に、そこから検証対象動作をどのように識別して切り出し、どのような形式で記憶装置に格納するかを述べる（ステップＳ１０３）。
【００４１】
３−１．ＨＤＬの端子情報の格納（図７および図８）
ＨＤＬを読み込み、解析する手段に関しては既知であるので、端子情報の記憶イメージのみを下記に示す。ＨＤＬの階層ツリーに付随して、入力・出力・入出力の別に端子の名前およびビット幅を格納する。なお、階層ツリー自体も下位階層のインスタンス名を保持する。
【００４２】
前述した図１に示す、端子情報抽出装置１のＨＤＬ読み込み装置１１には、たとえばＨＤＬ形式で記述された、たとえばＣＰＵなどのデジタル回路が入力される。また、ＨＤＬ読み込み装置１１が送出するＨＤＬ形式のデジタル回路の情報は、図１に示すように、ＨＤＬ記憶装置１２に格納するようにしてもよいし、ＨＤＬ読み込み装置１１の出力側を端子情報抽出装置１３に接続してもよい。この端子情報抽出装置１３により、ＨＤＬ読み込み装置１１またはＨＤＬ記憶装置１２から送出されるＨＤＬ形式のデジタル回路情報から、たとえば図７および図８に示す”名前”、”方向”などの端子情報が抽出され、抽出された端子情報は端子情報記憶装置１４に記憶される。なお、図７および図８は端子情報が端子情報記憶装置１４に記憶される際のイメージを示した図である。なお、上述したような端子情報抽出装置１は、従来より存在する、いわゆるＨＤＬパーサが生成する記号表から容易に作成されるものであり、特に本発明の機能検証記述生成装置用に開発したものではない。
【００４３】
すなわち、図７に示す階層ツリー例では、最上位階層−サブ階層（名前：ｐｃｐｕｎ，ｐｍａｓｎ，・・・）−サブ階層（名前：ＤＷ０１，ＹＸ０１，・・・，ＤＷ０１，・・・）・・・を示している。また、図８の端子情報例では、最上位階層−入力−出力−入出力、入力−端子１−端子２・・・、端子１−名前：ＣＭＤ／ビット幅：３、端子２−名前：ＲＥＡＤ＿ｎ／ビット幅：１、出力−端子１・・・、端子１−名前：ＷＡＩＴ／ビット幅：１、入出力−端子１・・・、端子１−名前：ＤＡＴＡ／ビット幅：３２を示している。さらに、サブ階層についても同様に図８の通りである。
【００４４】
３−２．タイミングダイアグラムの格納（図９〜図２３）
前述した図１に示す、タイミングダイアグラム編集装置２は、端子情報抽出装置１に接続され、ＧＵＩなどにより端子情報抽出装置１にて取得した端子名や内部ピン名が設計者や検証担当者により選択され、ならびに各端子や内部ピンのたとえば入出力波形、セットアップ、ホールドタイムなどのタイミング制約情報、この波形間の論理的関係、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報が設計者や検証担当者により入力される。このように被選択端子情報、およびタイミング制約情報、入出力波形、波形間の論理的関係、およびこの論理的関係の生起情報が供給されるタイミングダイアグラム編集装置２は、被選択端子情報、およびタイミング制約情報、入出力波形、波形間の論理的関係、およびこの論理的関係の生起情報に基づき、たとえば図９〜図１９に示すようなタイミングダイアグラムを編集する。
【００４５】
なお、図９〜図１９において、たとえば”ＣＭＤ［０：１］”は信号が入出力する端子名または内部ピン名およびビット数を示し、”（ｉｎ）”はその端子が入力端子であることを示している。また、図９〜図１９において、矢印”→”は始点と終点の論理的関係を表し、始点および終点として信号または矢印または記号”ＷＡＩＴ”をとることができ、この記号”ＷＡＩＴ”は信号が同期するクロックエッジに付加することができ、この記号”ＷＡＩＴ”には信号変化を監視する条件、すなわち条件成立までタイミングダイアグラムの進行を上記”ＷＡＩＴ”が付加されたクロックエッジで停止させるためのタイミングダイアグラムの制御条件をこの記号”ＷＡＩＴ”が付加された信号値を用いて設計者または検証担当者が指定することができ、上記始点および終点および上記矢印に記号”ｅｘｉ”を付加することができ、この記号”ｅｘｉ”はこの記号”ｅｘｉ”が付加された始点または終点または始点と終点を結ぶ矢印が表す論理的関係が少なくとも１回は起こるという生起情報を表し、矢印同士の論理演算を定義することができ、この矢印同士の論理演算は被演算矢印の表す論理的関係同士の論理的関係を表す。なお、上記論理的関係は以降の説明で明らかとなる。また、上記論理的関係は１つのタイミングダイアグラム上に複数設定可能である。
【００４６】
図９において、信号”ＣＭＤ［０：１］”を始点とし、信号”ＴＡＧ”を終点とするｒｅｌ＿Ａ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならばＴＡＧは１サイクル後に立ち上がる”という命題Ａ１を表す。また、ｒｅｌ＿Ａ２とラベルの付けられた上記ｒｅｌ＿Ａ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ａ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、ＴＡＧがその１サイクル後に立ち上がるならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ａ２を表す。
【００４７】
図１０において、記号”ｅｘｉ”が付加されたクロックサイクル１での信号”ＣＭＤ［０：１］”は”少なくとも１回はＣＭＤ［０：１］が２‘ｂ０１に等しくなることがある”を表し、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｂ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”少なくとも１回はＣＭＤ［０：１］が２‘ｂ０１に等しくなることがあるならＴＡＧはその１サイクル後に立ち上がる”という命題Ｂ１を表す。また、ｒｅｌ＿Ｂ２とラベルの付けられた上記ｒｅｌ＿Ｂ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ｂ１”と信号”Ｄ［０：７］”の論理的関係を表し、”少なくとも１回はＣＭＤ［０：１］が２’ｂ０１に等しくなる事があり、かつＴＡＧがその１サイクル後に立ち上がるならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｂ２を表す。
【００４８】
図１１において、記号”ｅｘｉ”が付加されたクロックサイクル２での信号”ＴＡＧ”は”少なくとも１回はＴＡＧが立ち上がることがある”を表し、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｃ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならその１サイクル後に少なくとも１回はＴＡＧが立ち上がることがある”という命題Ｃ１を表す。また、ｒｅｌ＿Ｃ２とラベルの付けられた上記ｒｅｌ＿Ｃ１とラベルの付けられた矢印を始点とする矢印は、上記矢印”ｒｅｌ＿Ｃ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、その１サイクル後にＴＡＧが立ち上がる事がすくなくとも１回はあるならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｃ２を表す。
【００４９】
図１２において、記号”ｅｘｉ”が付加されたクロックサイクル３に同期して出力される信号”Ｄ［０：７］”は”少なくとも１回はＤ［０：７］が８‘ｂｘｘ１１０１ｘｘに等しくなることがある”を表し、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｄ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならＴＡＧは１サイクル後に立ち上がる”という命題Ｄ１を表す。また、ｒｅｌ＿Ｄ２とラベルの付けられた上記ｒｅｌ＿Ｄ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ｄ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、ＴＡＧがその１サイクル後に立ち上がるならその２サイクル後に少なくとも１回はＤ［０：７］が８‘ｂｘｘ１１０１ｘｘに等しくなることがある”という命題Ｄ２を表す。
【００５０】
図１３において、記号”ｅｘｉ”が付加された信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするラベルｒｅｌ＿Ｅ１は”ラベルｒｅｌ＿Ｅ１が表す命題が少なくとも１回は成立することがある”を表し、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とする上記ｒｅｌ＿Ｅ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならＴＡＧは１サイクル後に立ち上がるという命題が少なくとも１回は成立することがある”という命題Ｅ１を表す。また、ｒｅｌ＿Ｅ２とラベルの付けられた上記ｒｅｌ＿Ｅ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ｅ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、ＴＡＧがその１サイクル後に立ち上がるならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｅ２を表す。ここで、”ｅｘｉ”が無視されている事に注意したい。
【００５１】
図１４において、記号”ｅｘｉ”が付加された信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｆ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とするラベルｒｅｌ＿Ｆ２は”少なくとも１回はラベルｒｅｌ＿Ｆ２が表す命題が少なくとも１回は成立することがある”を表し、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とする上記ｒｅｌ＿Ｆ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならＴＡＧは１サイクル後に立ち上がる”という命題Ｆ１を表す。また、ｒｅｌ＿Ｇ２とラベルの付けられた上記ｒｅｌ＿Ｆ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ｆ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、ＴＡＧがその１サイクル後に立ち上がるならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しいという命題が少なくとも１回は成立することがある”という命題Ｆ２を表す。
【００５２】
図１５において、信号”ＣＭＤ［０：１］”を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｇ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”ＴＡＧ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならＴＡＧは１サイクル後に立ち上がる”という命題Ｇ１を表す。また、ｒｅｌ＿Ｇ２とラベルの付けられた信号”Ｄ［０：７］”を始点とし上記ｒｅｌ＿Ｇ１とラベルの付けられた矢印を終点とする矢印は、上記矢印”ｒｅｌ＿Ｇ１”と信号”Ｄ［０：７］”の論理的関係を表し、”Ｄ［０：７］が８‘ｂｘｘ１１０１ｘｘに等しくかつ、３サイクル前にＣＭＤ［０：１］が２’ｂ０１に等しいなら、２サイクル前にＴＡＧが立ち上がる”という命題Ｇ２を表す。
【００５３】
図１６において、ｒｅｌ＿Ｈ１とラベルの付けられた矢印”→”の終点であるクロックサイクル２の信号”ＴＡＧ”に付加された記号”ＷＡＩＴ”は”条件ＴＡＧ＝１‘ｂ１が成立するまでの間クロックサイクル１からクロックサイクル２までの波形を繰り返す”、すなわち”条件ＴＡＧ＝１‘ｂ１が成立するまでの間ＴＡＧが０に等しくかつＤ［０：７］が８‘ｂｘｘ００１０１ｘｘに等しい”を表し、信号”ＣＭＤ［０：１］”を始点とし上記記号”ＷＡＩＴ”を終点とするｒｅｌ＿Ｈ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と上記記号”ＷＡＩＴ”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいなら条件ＴＡＧ＝１‘ｂ１が成立するまでの間ＴＡＧが０に等しくかつＤ［０：７］が８‘ｂｘｘ００１０１ｘｘに等しい”という命題Ｈ１を表す。また、ｒｅｌ＿Ｈ２とラベルの付けられた上記ｒｅｌ＿Ｈ１とラベルの付けられた矢印を始点とし信号”Ｄ［０：７］”を終点とする矢印は、上記矢印”ｒｅｌ＿Ｈ１”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２’ｂ０１に等しくかつ、条件ＴＡＧ＝＝１’ｂ１が成立する迄の間ＴＡＧが０に等しくかつ、Ｄ［０：７］が８’ｂｘｘ００１０１ｘｘに等しいならその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｈ２を表す。
【００５４】
図１７において、ｒｅｌ＿Ｉ２とラベルの付けられた矢印”→”の始点であるクロックサイクル２の信号”ＴＡＧ”に付加された記号”ＷＡＩＴ”は”条件ＴＡＧ＝１‘ｂ１が成立するまでの間クロックサイクル１からクロックサイクル２までの波形を繰り返す”、すなわち”いつかはＴＡＧが０から１に変化しかつＤ［０：７］がＴＡＧが０と等しい間８‘ｂｘｘ００１０１ｘｘを繰り返し保持した後それ以外の値に変化する”を表し、上記記号”ＷＡＩＴ”を始点とし信号”Ｄ［０：７］”を終点とするｒｅｌ＿Ｉ２とラベルの付けられた矢印”→”は上記記号”ＷＡＩＴ”と信号”Ｄ［０：７］”との論理的関係を表し、”いつかはＴＡＧが０から１に変化しかつＤ［０：７］が８‘ｂｘｘ００１０１ｘｘからそれ以外の値に変化するならばその２サイクル後に［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｉ１を表す。また、ｒｅｌ＿Ｉ１とラベルの付けられた信号”ＣＭＤ［０：１］”を始点とし上記ｒｅｌ＿Ｉ２とラベルの付けられた矢印を始点とする矢印は、信号”ＣＭＤ［０：１］”と上記矢印”ｒｅｌ＿Ｉ２”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいなら上記命題Ｉ１が成立する”という命題Ｉ２を表す。
【００５５】
図１８において、ｒｅｌ＿Ｊ２とラベルの付けられた矢印”→”の始点であるクロックサイクル２の信号”ＴＡＧ”に付加された記号”ＷＡＩＴ”は”条件ＴＡＧ＝１‘ｂ１が成立するまでの間クロックサイクル１からクロックサイクル２までの波形を繰り返す”、すなわち”いつかはＴＡＧが０から１に変化する”を表し、上記記号”ＷＡＩＴ”を始点とし信号”Ｄ［０：７］”を終点とするｒｅｌ＿Ｊ２とラベルの付けられた矢印”→”は上記記号”ＷＡＩＴ”と信号”Ｄ［０：７］”との論理的関係を表し、”いつかはＴＡＧが０から１に変化するならばその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｊ１を表す。また、ｒｅｌ＿Ｊ１とラベルの付けられた信号”ＣＭＤ［０：１］”を始点とし上記ｒｅｌ＿Ｊ２とラベルの付けられた矢印を始点とする矢印は、信号”ＣＭＤ［０：１］”と上記矢印”ｒｅｌ＿Ｊ２”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいなら上記命題Ｊ１が成立する”という命題Ｊ２を表す。
【００５６】
図１９において、信号”ＣＭＤ［０：１］”を始点とし信号”Ｄ［０：７］”を終点とするｒｅｌ＿Ｋ１とラベルの付けられた矢印”→”は信号”ＣＭＤ［０：１］”と信号”Ｄ［０：７］”の論理的関係を表し、”ＣＭＤ［０：１］が２‘ｂ０１に等しいならＤ［０：７］は４サイクル後に８‘ｂｘｘ１１０１ｘｘと等しくなる”という命題Ｋ１を表す。また、ｒｅｌ＿Ｋ２とラベルの付けられた矢印”→”の始点であるクロックサイクル２の信号”ＴＡＧ”に付加された記号”ＷＡＩＴ”は”条件ＴＡＧ＝１‘ｂ１が成立するまでの間クロックサイクル１からクロックサイクル２までの波形を繰り返す”、すなわち”いつかはＴＡＧが０から１に変化しかつＤ［０：７］が８‘ｂｘｘ００１０１ｘｘからそれ以外の値に変化する”を表し、上記記号”ＷＡＩＴ”を始点とし信号”Ｄ［０：７］”を終点とするｒｅｌ＿Ｋ２とラベルの付けられた矢印”→”は上記記号”ＷＡＩＴ”と信号”Ｄ［０：７］”との論理的関係を表し、”いつかはＴＡＧが０から１に変化しかつＤ［０：７］がＴＡＧが０と等しい間８‘ｂｘｘ００１０１ｘｘを繰り返し保持した後８‘ｂｘｘ００１０１ｘｘからそれ以外の値に変化するならばその２サイクル後にＤ［０：７］は８‘ｂｘｘ１１０１ｘｘに等しい”という命題Ｋ２を表す。また、ｒｅｌ＿Ｋ３とラベルの付けられたこのラベルｒｅｌ＿Ｋ１とこのラベルｒｅｌ＿Ｋ２の論理和は、”命題Ｋ１か命題Ｋ２の何れかが成立する”という命題Ｋ３を表す。また、上記ラベルｒｅｌ＿Ｋ２を始点とし信号”ＴＡＧ”を終点とするｒｅｌ＿Ｋ４とラベルの付けられた矢印”→”は上記ラベルｒｅｌ＿Ｋ２と信号”ＴＡＧ”との論理的関係を表し、”いつかはＴＡＧが０から１に変化し、かつＴＡＧが０と等しい間Ｄ［０：７］が８‘ｂｘｘ００１０１ｘｘを繰り返し保持した後、その２サイクル後にＤ［０：７］が８’ｂｘｘ１１０１ｘｘに等しいならＴＡＧが０から１に変化しかつＤ［０：７］が８‘ｂｘｘ００１０１ｘｘからそれ以外の値に変化した時点から１サイクル後に信号ＴＡＧが立ち下がる”という命題Ｋ４を表す。
【００５７】
前述した図１に示す、タイミングダイアグラム記憶装置３１は、タイミングダイアグラム編集装置２にて設計者または検証対象者が入力および編集した、たとえば前述した図９〜図１９に示すようなタイミングダイアグラムの情報を記憶する。なお、図２１および図２２はタイミングダイアグラム編集装置２にて設計者または検証対象者が入力および編集したタイミングダイアグラム情報がタイミングダイアグラム記憶装置３１に記憶される際のイメージを示した図である。
【００５８】
すなわち、図２１および図２２に示すタイミングダイアグラムの記憶イメージ例では、端子１−端子２−端子３、端子１−名前／方向／ビット幅／対象クロック−ハイ期間／ロウ期間／立ち上がりエッジ／立ち下がりエッジ−０−０→１・・・、０−値／セットアップ値／ホールド値／出力遅延／ＷＡＩＴ設定／ｅｘｉ設定／矢印−始終点／ｅｘｉ設定／矢印を示している。さらに、０→１・・・、端子２、端子３についても同様に図２１および図２２の通りである。
【００５９】
タイミングダイアグラム情報の取得においては、まず図２３に示す動作フローチャートが示すタイミングダイアグラム分割手段に従い、クロックサイクルが０、０から１に変化、１などのようにタイミングダイアグラムを分割する。すなわち、以下の通りである。
【００６０】
（１）ステップＳ２０１において、ダイアグラムの端子を１つ選択し、ステップＳ２０２にて端子に定義された波形の左からのスキャンを開始し、ステップＳ２０３にて変数ｆｌｇを０に設定し、ステップＳ２０４にてスキャンしているこの波形が信号変化を表している所まで到達したか否かを判定し、到達している場合は処理をステップＳ２０５に移し、到達していない場合は処理をステップＳ２０６に移す。
【００６１】
（２）次いで、ステップＳ２０５では上記変数ｆｌｇに１を代入し、処理をステップＳ２０６へ移す。
【００６２】
（３）ステップＳ２０６では、ステップＳ２０４にてスキャンしているこの波形がセットアップ、ホールドや出力遅延などのタイミング制約を設定している個所に到達したか否かを判定し、到達している場合は処理をステップＳ２０７に移し、到達していない場合は処理をステップＳ２０９に移す。
【００６３】
（４）ステップＳ２０７では、タイミング制約が関連付けられている信号名および信号エッジを取得し、この端子が同期しているクロックとして識別し、ステップＳ２０８では識別したこのクロックおよびこのクロックのエッジを分割点として、ステップＳ２０４にてスキャンしているこの波形を分割し、処理をステップＳ２０９に移す。
【００６４】
（５）次いで、ステップＳ２０９では、ステップＳ２０４にて行っているスキャンが終了したか否かを判定し、終了していれば処理をステップＳ２１０へ、終了していなければ処理をステップＳ２０４へ移す。
【００６５】
（６）ステップＳ２１０では、上記記号ｆｌｇが０に一致するか否かを判定し、一致した場合は処理をステップＳ２１１へ、一致しなかった場合は処理をステップＳ２１３へ移す。
【００６６】
（７）ステップＳ２１１では、上記端子が同期すべきクロック信号とクロックエッジをユーザに問い合わせ、ユーザ情報を取得し、ステップＳ２１２にてこのユーザ情報に基づきこの端子に定義されている波形を分割し、処理をステップＳ２１６へ移す。
【００６７】
（８）また、ステップＳ２１３では、上記端子に定義されている波形を信号変化の所で分割し、ステップＳ２１４でこの信号変化の所からの距離が最短のこの同期クロックエッジにより与えられた分割点でかつこの距離が半サイクル周期未満の分割点を排除し、ステップＳ２１５ではこの波形を再び左からスキャンし、隣接し合う分割区間であって互いの区間調和が１サイクル周期未満のものを併合し、処理をステップＳ２１６へ移す。
【００６８】
（９）ステップＳ２１６では、再びこの波形を左からスキャンしながら上記各分割区間に対してサイクル数を割り当てる。
【００６９】
（１０）最後に、ステップＳ２１７にて全ての端子を処理したか否かを判定し、処理した場合は終了し、処理していない場合は処理をステップＳ２０１へ移す。
【００７０】
なお、図２０は上記タイミングダイアグラム分割手段により得られたタイミングダイアグラムのイメージを示した図である。すなわち、図２０に示すタイミングダイアグラム分割例では、ＣＬＫ（ｉｎ）に同期する、ＣＭＤ［０：１］（ｉｎ）、ＴＡＧ（ｉｎ）、Ｄ［０：７］（ｏｕｔ）の変化をサイクル０、サイクル１、サイクル２、サイクル３への分割を示している。
【００７１】
次いで、上記タイミングダイアグラム分割手段にて得られた分割区間内での端子または内部ピンの波形情報、たとえば記号”ＷＡＩＴ”が設定されているかの情報、記号”ＷＡＩＴ”が設定されていた場合はこの分割の１つ前の分割区間内での全ての端子または内部ピンの波形情報、記号”ｅｘｉ”が設定されているかの情報、矢印”→”の始点または終点となっているかの情報、上記矢印の始点または終点となっていた場合はこの矢印のラベル名、この矢印には記号”ｅｘｉ”が設定されているかの情報、またこの矢印が別の矢印の始点または終点となっているかの情報、この端子または内部ピンの信号値、このクロックに対するセットアップ、ホールド、出力遅延などのタイミング制約情報を取得することでタイミングダイアグラム情報の取得を行う。
【００７２】
また、出力端子の場合は信号変化に設定された出力遅延制約をその次の分割区間内の波形情報にも設定し、入力端子の場合は信号変化に設定されたセットアップタイミング制約を１つ前の分割区間内の波形情報にも設定する。分割区間内に端子または内部ピンの波形情報が存在しない場合は、前述した図２１および図２２に示すように記号”ｎｕｌｌ”を取得したものとする。なお、タイミングダイアグラム情報の取得においては、信号値として０、１や２進数値以外の立ち上がり、立ち下がり、変化なども値として識別する。
【００７３】
３−３．検証対象動作の切り出し（図２４〜図２７）
前述した図１に示す、検証対象動作情報抽出装置３２は、図２４に示す動作フローチャートに示すように動作し、タイミングダイアグラム記憶装置３１に格納されたタイミングダイアグラム情報から検証対象動作情報を取得し、結果を検証対象動作情報記憶装置３３に格納する。すなわち、以下の通りである。
【００７４】
（１）ステップＳ３０１において、変数ｊに０を代入し、ステップＳ３０２にてこの変数ｊに１を加える。
【００７５】
（２）次いで、ステップＳ３０３において、タイミングダイアグラム記憶装置３１内に格納されているタイミングダイアグラム情報からｊ番目の端子または内部ピンの波形情報を取得し、ステップＳ３０４において、上記ｊ番目の端子または内部ピンの波形情報に設定されている端子名または内部ピンの名前、方向、および同期クロックとこの同期クロックの同期エッジの情報を取得し、ステップＳ３０５で変数ｉに１を代入し、ステップＳ３０６にて上記ｊ番目の端子または内部ピンの波形情報からｉ番目に対応する分割区間内波形情報を取得する。ただし、本ステップにおいて取得したこの分割区間内波形情報内の値が変化である場合は、前後のサイクルの分割区間内波形情報も合わせて取得する。
【００７６】
（３）ステップＳ３０７において、上記ｉ番目に対応する分割区間内波形情報内に矢印が設定されているか否かを判定し、設定されている場合は処理をステップＳ３１１へ移し、設定されていない場合は処理をステップＳ３０８へ移す。
【００７７】
（４）ステップＳ３０８では、上記ｉ番目に対応する分割区間内波形情報内に記号”ＷＡＩＴ”が設定されているか否かを判定し、設定されている場合は処理をステップＳ３０９へ移し、設定されていない場合は処理をステップＳ３１６へ移す。
【００７８】
（５）ステップＳ３０９において、設定されたこの記号”ＷＡＩＴ”の条件、およびこの記号”ＷＡＩＴ”に関連付けられている端子または内部ピンの波形情報内の端子名または内部ピン名の情報とこの端子または内部ピンの波形情報内のｉ−１、ｉ＋１番目の分割区間内波形情報の取得を行い、ステップＳ３１０にて上記ｊ番目の端子または内部ピンの波形情報に設定されている上記ｉ番目に対応する分割区間内波形情報の記号”ＷＡＩＴ”設定個所を参照し、処理をステップＳ３１３へ移す。
【００７９】
（６）ステップＳ３１１では、上記ｊ番目の端子または内部ピンの波形情報に設定されている上記ｉ番目に対応する分割区間内波形情報内の波形に対する記号”ｅｘｉ”の設定情報と矢印に対する記号”ｅｘｉ”の設定情報を取得し、次いでステップＳ３１２にて上記ｊ番目の端子または内部ピンの波形情報に設定されている上記ｉ番目に対応する分割区間内波形情報内に設定されている矢印が始点であるか終点であるかの情報を取得し、処理をステップＳ３１３へ移す。
【００８０】
（７）ステップＳ３１３からステップＳ３１５では、上記ｊ番目の端子または内部ピンの波形情報が設定されている上記ｉ番目に対応する分割区間内波形情報内の記号”ＷＡＩＴ”または”ｅｘｉ”から辿って得られるリストに矢印が設定されているか否かを判定し、設定されている場合は矢印の始点か終点かの情報と矢印への記号”ｅｘｉ”設定情報を取得し、リストがなくなるまでこの処理を続け、設定されていない場合やリストがなくなった場合は処理をステップＳ３１６へ移す。
【００８１】
（８）ステップＳ３１４では、この矢印の記号”ｅｘｉ”の設定情報を取得し、ステップＳ３１５ではこの矢印が始点であるか終点であるかの情報取得を行い、この矢印の始点か終点かの情報が格納されたリストを参照するように設定してから処理をステップＳ３１３へ移す。
【００８２】
（９）ステップＳ３１６において、上記記号ｉに１を加え、ステップＳ３１７にて上記記号ｉが上記ｊ番目の端子または内部ピンの波形情報に設定されている分割区間内波形情報の総数を超えたか否かを判定し、越えている場合は処理をステップＳ３１８へ、越えていない場合は処理をステップＳ３１８へ移す。
【００８３】
（１０）さらに、ステップＳ３１８では、上記記号ｊが上記タイミングダイアグラム情報内の端子または内部ピンの波形情報の総数を超えたか否かを判定し、越えている場合は処理を終了し、越えていない場合は処理をステップＳ３０２へ移す。
【００８４】
前述した図１に示す、検証対象動作情報記憶装置３３は、検証対象動作情報抽出装置３２の出力に接続されており、上記タイミングダイアグラム情報内に設計者または検証担当者が設定した検証対象動作、すなわち波形間の論理的関係の情報を格納する。なお、図２５は上記タイミングダイアグラム情報から抽出した検証対象動作が上記検証対象動作情報記憶装置３３に記憶される際のイメージを示した図である。
【００８５】
すなわち、図２５に示す検証対象動作情報の記憶イメージ例では、ｒｅｌ＿Ｋ１−ｒｅｌ＿Ｋ２−ｒｅｌ＿Ｋ３−ｒｅｌ＿Ｋ４、ｒｅｌ＿Ｋ１−始点／終点／ｅｘｉ設定／論理式、始点−方向／値／セットアップ値／ホールド値／出力遅延／クロック／サイクル／ｅｘｉ設定／ＷＡＩＴ設定を示している。さらに、終点、ｒｅｌ＿Ｋ２、ｒｅｌ＿Ｋ３、ｒｅｌ＿Ｋ４についても同様に図２５の通りである。ただし、ＷＡＩＴ設定がｎｕｌｌでない場合は、条件／端子１波形情報／端子２波形情報／端子３波形情報につながる。
【００８６】
上記検証対象動作情報記憶装置３３に格納された検証対象動作情報を各矢印ラベルと矢印ラベルの関連付けられた始点および終点のなすグラフの隣接リストと見なして、各隣接リストの親のみからなる矢印ラベルの集合１と各隣接リストの子のみからなる矢印ラベルの集合２を作成し、集合１と集合２の要素数の多い方の集合から少ない方の集合を集合演算の意味で引き、その結果を集合３とする。
【００８７】
次いで、上記集合３に含まれる矢印ラベルを１つ取り出し、たとえば隣接リストを幅優先で探索することで木を構築し、この操作を上記集合３が空となるまで繰り返すことで、上記検証対象動作情報記憶装置３３に格納された検証対象動作情報から木構造を構築する。なお、図２６および図２７は前記図２５に示した検証対象動作の記憶イメージから作成される木構造、以下検証対象動作木と呼び、このイメージを示した図である。
【００８８】
すなわち、図２６および図２７に示す、前記図２５の検証対象動作から作成される木構造の記憶イメージ例では、ｒｅｌ＿Ｋ３／ｅｘｉ設定−ｒｅｌ＿Ｋ１｜ｒｅｌ＿Ｋ２−ｒｅｌ＿Ｋ１／始終点／ｅｘｉ設定−ＣＭＤ［０：１］／始終点／ｅｘｉ設定−方向／値／セットアップ値／ホールド値／出力遅延／クロック／サイクル／ｅｘｉ設定／ＷＡＩＴ設定を示している。さらに、Ｄ［０：７］／始終点／ｅｘｉ設定、ｒｅｌ＿Ｋ２／始終点／ｅｘｉ設定−ＴＡＧ／始終点／ｅｘｉ設定、Ｄ［０：７］／始終点／ｅｘｉ設定や、ｒｅｌ＿Ｋ４についてもほぼ同様に図２６および図２７の通りである。
【００８９】
４．ＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍ
図２８〜図６２により、ＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍの一例を説明する。図２８はＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍを示すフロー図、図２９は格納変数の割り当てを示すフロー図、図３０は格納サイクル数の算出を示すフロー図、図３１は格納サイクル数の算出におけるテーブル構造を示す説明図、図３２はＷａｉｔ制御用フラグ生成・初期値決定を示すフロー図、図３３はＷａｉｔ制御用フラグ生成・初期値決定におけるテーブル構造を示す説明図、図３４は初期値決定を示すフロー図、図３５は変数宣言ＨＤＬ記述生成を示すフロー図、図３６は変数値格納ＨＤＬ記述生成を示すフロー図、図３７はグラフ変形を示すフロー図、図３８〜図５４はグラフ変形を示す説明図、図５５は検証ＨＤＬの生成を示すフロー図、図５６はＰｒｏｐｅｒｔｙ＿ｓｉｍｐｌｅを示すフロー図、図５７はＰｒｏｐｅｒｔｙ＿ｗａｉｔを示すフロー図、図５８および図５９はＷａｉｔＢｌｏｃｋを示すフロー図、図６０および図６１はＷａｉｔＯＲＢｌｏｃｋを示すフロー図、図６２はＣｏｎｓｅｑＢｌｏｃｋを示すフロー図である。
【００９０】
図２８に示すように、ＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍは、まず、各信号に対して何サイクル前までの値を格納するかを識別して格納変数を割り当て、初期値を決定する手段、および信号値を格納する記述を生成する手段を述べ（ステップＳ４０１）、次いで、検証対象動作木の変形方式を述べ（ステップＳ４０２）、最後に、最終的に得られた検証対象動作木からのＨＤＬ検証記述生成手段を述べる（ステップＳ４０３）。
【００９１】
４−１．格納変数の割り当て（図２９〜図３６：図２９）
（１）ステップＳ５０１において、検証対象動作木の信号名を格納しているノードの信号に対して、何サイクルまでの信号を格納すべきかを決定し、各信号にサイクル数と同じ数の信号値格納用レジスタを割り当て、その情報をテーブルに格納する。
【００９２】
（２）ステップＳ５０２において、検証対象動作木がｗａｉｔ  ｏｂｊｅｃｔを含むか判定し、もし含んでいるなら処理をステップＳ５０３に移し、そうでなければ処理をステップＳ５０４に移す。
【００９３】
（３）ステップＳ５０３において、検証対象動作木に含まれるｗａｉｔ  ｏｂｊｅｃｔの数だけｗａｉｔ制御用のフラグを生成する。
【００９４】
（４）ステップＳ５０４において、各信号に割り当てたレジスタのリセット時の初期値を決定する。これは、初期化の段階で検証ＨＤＬが誤動作を起こさないために行う。
【００９５】
（５）ステップＳ５０５において、各信号に割り当てたレジスタ、およびｗａｉｔ制御用フラグの変数宣言のＨＤＬ記述を生成する。
【００９６】
（６）ステップＳ５０６において、各信号に割り当てたレジスタに対する、リセット時の初期化、および信号値代入のＨＤＬ記述を生成する。
【００９７】
４−１−１．格納サイクル数の算出（図３０および図３１）
（１）ステップＳ６０１において、検証対象動作木の信号名を格納しているノードのサイクル数を全て取得し、最大値を決定する。この値がテーブルのサイクル数の最大値となる。
【００９８】
（２）ステップＳ６０２において、全ての信号に対して、１からステップＳ６０１で得られた最大値までのサイクルで、ｗａｉｔ設定、格納要・不要、初期値の情報を格納可能とするテーブルを作成する。
【００９９】
（３）ステップＳ６０３において、検証対象動作木の信号名を格納しているノードのサイクル数を取得し、その信号の格納サイクル数をステップＳ６０１で得た最大値−取得したサイクル数、として求め、格納要・不要の欄の１から前記演算で得られた値まで、１を立てる（初期状態では０が格納されているものとする）。
【０１００】
（４）ステップＳ６０４において、検証対象動作木上の信号名を格納しているノードを全て探索したのであれば処理を終了し、そうでなければ処理をステップＳ６０３へ移す。
【０１０１】
なお、この格納サイクル数の算出におけるテーブル構造は、たとえば図３１のようになる。すなわち、図３１のテーブル構造例では、信号名、信号値を格納する領域、さらにレジスタ要・不要、Ｗａｉｔ設定、初期値に対するサイクル数を格納する領域がそれぞれ設けられている。
【０１０２】
４−１−２．Ｗａｉｔ制御用フラグ生成・初期値決定（図３２および図３３）
（１）ステップＳ７０１において、検証対象動作木のｗａｉｔ  ｏｂｊｅｃｔが設定されているノードを識別する。
【０１０３】
（２）ステップＳ７０２において、ステップＳ７０１で識別されたノードが、繰り返しチェックを表すものであれば、処理をステップＳ７０３へ、そうでなければ処理をステップＳ７０４へ移す。
【０１０４】
（３）ステップＳ７０３において、テーブルの該当信号の該当サイクルのｗａｉｔ設定部に文字列ｉｔｒ［Ｉ］を格納し、対応するレジスタ要・不要フラグを１にセットする（初期値はＮＵＬＬであるとする。また、配列インデックスＩはフラグ数に対応して増加していく変数である）。
【０１０５】
（４）ステップＳ７０４において、ステップＳ７０１で識別されたノードが、終了条件に用いられているものであれば、処理をステップＳ７０５へ、そうでなければ処理をステップＳ７０６へ移す。
【０１０６】
（５）ステップＳ７０５において、テーブルの該当信号の該当サイクルのｗａｉｔ設定部に文字列ｃｏｎｄ［Ｉ］を格納し、対応するレジスタ要・不要フラグを１にセットする（初期値はＮＵＬＬであるとする。また、配列インデックスＩはフラグ数に対応して増加していく変数である）。
【０１０７】
（６）ステップＳ７０６において、ｗａｉｔ制御フラグの数をカウントアップする（初期値は０であるとする）。なお、フラグ名は、ｗａｉｔ＿ｆｌｇ［２：０］とし、ｗａｉｔ＿ｆｌｇ［０］が繰り返し開始フラグであり、１で開始、０で未開始を表す。また、ｗａｉｔ＿ｆｌｇ［１］が繰り返し継続フラグであり、１で継続、０で未継続を表す。最後に、ｗａｉｔ＿ｆｌｇ［２］が繰り返し終了フラグであり、１で終了、０で未終了を表す。初期値は全て０である。特に、複数存在する場合は、ｒｅｇ［２：０］ｗａｉｔ＿ｆｌｇ［フラグ数−１：０］のような二次元配列として宣言することで、複数のフラグを割り当てる。たとえば、Ｉ番目のフラグは、ｗａｉｔ＿ｆｌｇ［Ｉ］［２：０］となる。
【０１０８】
（７）ステップＳ７０７において、全てのｗａｉｔ  ｏｂｊｅｃｔが設定されているノードを探索したのであれば処理を終了し、そうでなければ処理をステップＳ７０１へ移す。
【０１０９】
なお、このＷａｉｔ制御用フラグ生成・初期値決定におけるテーブル構造は、たとえば図３３のようになる。すなわち、図３３のテーブル構造例では、信号名、信号値を格納する領域、さらにレジスタ要・不要、Ｗａｉｔ設定、初期値に対するサイクル数を格納する領域がそれぞれ設けられている。
【０１１０】
４−１−３．初期値決定（図３４）
（１）ステップＳ８０１において、検証対象動作木の信号名が設定されているノードを識別する。
【０１１１】
（２）ステップＳ８０２において、ステップＳ８０１で識別した全ての信号に対して、対応するビット幅の０を割り当てる。
【０１１２】
４−１−４．変数宣言ＨＤＬ記述生成（図３５）
（１）ステップＳ９０１において、テーブル上の信号名に対するレジスタ要・不要フラグが１の個数を算出する。
【０１１３】
（２）ステップＳ９０２において、ステップＳ９０１で識別された信号が、１ビットであれば、処理をステップＳ９０３へ、そうでなければ処理をステップＳ９０４へ移す。
【０１１４】
（３）ステップＳ９０３において、一次元配列として、ステップＳ９０１で取得した個数のビット幅を持つ、変数名＿ｔｍｐのｒｅｇ宣言を行う。すなわち、
ｒｅｇ［（１）で取得した個数−１：０］変数名＿ｔｍｐ；
なる記述を生成する。ステップＳ９０５へ処理を移す。
【０１１５】
（４）ステップＳ９０４において、二次元配列として、ステップＳ９０１で取得した配列数の、変数名＿ｔｍｐのｒｅｇ宣言を行う。すなわち、
ｒｅｇ［ビット幅−１：０］変数名＿ｔｍｐ［（１）で取得した個数−１：０］；
なる記述を生成する。
【０１１６】
（５）ステップＳ９０５において、ｗａｉｔカウント数分のｗａｉｔフラグの二次元配列のｒｅｇ宣言を行う。すなわち、
ｒｅｇ［２：０］ｗａｉｔ＿ｆｌｇ［ｗａｉｔカウント数−１：０］；
なる記述を生成する。
【０１１７】
（６）ステップＳ９０６において、テーブル上の全ての信号を取得したのであれば処理をステップＳ９０７へ、そうでなければ処理をステップＳ９０１へ移す。
【０１１８】
（７）ステップＳ９０７において、［Ｌｏｇ２最大個数＋１］を算出し、そのビット幅のｃｎｔ＿ｔｍｐをｒｅｇ宣言し、ｆｌｇ＿ｔｍｐもｒｅｇ宣言する。すなわち、
ｒｅｇ［［ｌｏｇ２（（１）で取得した個数の最大値）］＋１：０］ｃｎｔ＿ｔｍｐ；
ｒｅｇ  ｆｌｇ＿ｔｍｐ；
なる記述を生成する。ここで、［ｌｏｇ２（（１）で取得した個数の最大値）］は、ｌｏｇ２（（１）で取得した個数の最大値）を越えない最大の整数を表す。
【０１１９】
４−１−５．変数値格納ＨＤＬ記述生成（図３６）
（１）ステップＳ１００１において、ｒｅｇ宣言した変数の数だけＩｎｔｅｇｅｒ変数を宣言する。すなわち、
Ｉｎｔｅｇｅｒ［変数の数−１：０］Ｉ；
なる記述を生成する。
【０１２０】
（２）ステップＳ１００２において、下記
ａｌｗａｙｓ＠（ｐｏｓｅｄｇｅ  クロック信号名  ｏｒ  ｎｅｇｅｄｇｅ  リセット信号名）ｂｅｇｉｎ
ｉｆ（！リセット信号名）ｂｅｇｉｎ
なる記述を生成する。
【０１２１】
（３）ステップＳ１００３において、ｒｅｇ宣言した全ての変数の初期化記述を、信号名＿ｔｍｐの配列番号とテーブルのサイクル番号との対応を取りながら、信号名＿ｔｍｐへの初期値代入を行う記述を生成する。たとえば、下記
信号名＿ｔｍｐ［０］＜＝１’ｂ０；
などの記述を生成する。
【０１２２】
（４）ステップＳ１００４において、下記
ｅｎｄ
ｅｌｓｅ  ｂｅｇｉｎ
なる記述を生成する。
【０１２３】
（５）ステップＳ１００５において、ｒｅｇ宣言した変数全てに対して、１ビットか多ビットかに従い、下記
信号名＿ｔｍｐ［０］＜＝信号名；／／１ビットの場合
信号名＿ｔｍｐ［０］［ビット幅−１：０］＜＝信号名［ビット幅−１：０］；／／多ビットの場合
なる記述の何れかを生成する。
【０１２４】
（６）ステップＳ１００６において、ｒｅｇ宣言した変数全てに対して、１ビットか多ビットかに従い、下記記述の何れかを生成する。ただし、ｋは信号名が変わる毎に０から１ずつ増加させる。
【０１２５】
0004153699.tif 000002
（７）ステップＳ１００７において、下記
0004153699.tif 000003
なる記述を生成する。
【０１２６】
（８）ステップＳ１００８において、下記
ｅｎｄ
ｅｎｄ
なる記述を生成する。
【０１２７】
４−２．検証対象動作木の変形（図３７〜図５４：図３７）
（１）検証対象動作木の頂点であってｓｉｇｎａｌ  ｏｂｊｅｃｔのみが設定されている頂点は、全てテーブルを参照して、対応するインデックスを持つ、変数名＿ｔｍｐに置き換える。また、それ以外の頂点であっても、信号名を有する場合はこの変換を行う。
【０１２８】
（２）ステップＳ１１０１において、検証対象動作木上のｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算を表す頂点を取得する。
【０１２９】
（３）ステップＳ１１０２において、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算頂点以下の部分木に対して、その木の信号頂点の左方向への深さ優先探索によるトポロジカルソートを実施し、得られた順番と逆順に信号頂点を並べることで、
（Ａ−＞Ｂ）−＞ＣをＡ−＞（Ｂ−＞Ｃ）とし、Ａ＆Ｂ−＞Ｃ
となるようにグラフを変形する。また、一般には、括弧を全て外して、Ａ１＆Ａ２＆・・・＆Ａｎ−＞Ａｎ＋１となるようにグラフを変形する。特に、この処理はｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算を下位の部分木が含まない条件でまず行い、次いで、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算以下の部分木を固定したものとして、再帰的に処理を実施するものとする。
【０１３０】
（４）ステップＳ１１０３において、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算が＆を含むか判定し、含む場合は、処理をステップＳ１１０４へ、そうでない場合は処理をステップＳ１１０５へ移行する。
【０１３１】
（５）ステップＳ１１０４において、その下位の部分木にｗａｉｔ  ｏｂｊｅｃｔが設定されているか判定し、されている場合は処理をステップＳ１１０７へ、そうでない場合は処理をステップＳ１１０６へ移行する。
【０１３２】
（６）ステップＳ１１０５において、その下位の部分木にｗａｉｔ  ｏｂｊｅｃｔが設定されているか判定し、されている場合は処理をステップＳ１１０８へ、そうでない場合は処理をステップＳ１１０６へ移行する。
【０１３３】
（７）ステップＳ１１０６において、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔのブール演算を用いたグラフ変形を実施し、処理をステップＳ１１０９へ移行する。
【０１３４】
（８）ステップＳ１１０７において、ユーザにｗａｉｔ  ｏｂｊｅｃｔの設定が不正であると通知し、処理を終了する。
【０１３５】
（９）ステップＳ１１０８において、木のｗａｉｔ  ｏｂｊｅｃｔ以外の信号をマージすることでグラフ変形を行い、木の最下位に位置するｗａｉｔ  ｏｂｊｅｃｔをマーキングする。
【０１３６】
（１０）ステップＳ１１０９において、全てのｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔのブール演算を取得したかを判定し、取得した場合は処理をステップＳ１１１０へ、そうでない場合は処理をステップＳ１１０１へ移行する。
【０１３７】
（１１）ステップＳ１１１０において、ｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔ同士のブール演算以下の部分木を固定したものとして、ステップＳ１１０２の処理を検証対象動作木に対して行い、処理を終了する。
【０１３８】
図３８の例を通して、グラフ変形を説明する。四角で囲まれたｒはｒｅｌａｔｉｏｎ  ｏｂｊｅｃｔを表す頂点であり、それ以外は信号頂点である。特に、ｍ、ｙの信号頂点はｗａｉｔ  ｏｂｊｅｃｔが設定されていることを表す。すなわち、図３８の例では、ｒ−ｒ−（ｒ１‖ｒ２）＆ｒ３−ｒ１，ｒ２，ｒ３−・・・−ａ，ｂ，ｃ，ｄ，ｅ，ｆ，ｇ，ｉ，ｊ，ｋ、ｒ−ｒ−ａ４、ｒ−ｒ−ｒ４‖ｒ５−ｒ４−・・・−ｈ，ｌ，ｍ，ａ１、ｒ−ｒ−ｒ４‖ｒ５−ｒ５−ａ５、ｒ−ｒ−ｒ４‖ｒ５−ｒ５−ｒ−ｒ６‖ｒ７＆ｒ８−ｒ６，ｒ７，ｒ８−・・・−ｏ，ｐ，ｑ，ｒ，ｓ，ｔ，ｕ，ｖ，ｗ、ｒ−ｒ−ｒ４‖ｒ５−ｒ５−ｒ−ｒ−・・・−ｘ，ｙ，ｚ，ａ１、ｒ−ｒ−ｒ−ａ２，ａ３の階層ツリーを示している。
【０１３９】
この図３８のグラフ変形は、図３９〜図５４に従って以下のように行われる。
【０１４０】
（１）図３９において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎの識別を表す。（ｒ１‖ｒ２）＆ｒ３−・・・、ｒ６‖ｒ７＆ｒ８−・・・、ｒ４‖ｒ５−・・・を識別する。
【０１４１】
（２）図４０において、（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形を表す。ｒ１−・・・−ａ，ｂ，ｃ，ｋの順番を、（ａ）のようにａ▲１▼，ｂ▲２▼，ｃ▲３▼，ｋ▲４▼に決定して、（ｂ）のように変形する。
【０１４２】
（３）図４１において、（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形（続き）を表す。同様に、ｒ２−・・・−ｄ，ｅ，ｆ，ｇ，ｈの順番、ｒ３−・・・−ｉ，ｊ，ｋの順番を（ａ）のように決定して、（ｂ）のように変形する。
【０１４３】
（４）図４２において、Ａ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形を表す。（ａ）から（ｂ）のように、（ｒ１‖ｒ２）＆ｒ３−ｒ１−ａ＆ｂ＆ｃ，ｋ、（ｒ１‖ｒ２）＆ｒ３−ｒ２−ｄ＆ｅ＆ｆ＆ｇ，ｋ、（ｒ１‖ｒ２）＆ｒ３−ｒ３−ｉ＆ｊ，ｋに変形する。
【０１４４】
（５）図４３において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎを用いた変形を表す。（ａ）から（ｂ）のように、ｒ−（ａ＆ｂ＆ｃ‖ｄ＆ｅ＆ｆ＆ｇ）＆ｉ＆ｊに変形する。
【０１４５】
（６）図４４において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎ（残り）を用いた変形を表す。（ａ）のような、ｒ６‖ｒ７＆ｒ８−ｒ６，ｒ７，ｒ８−・・・−ｏ，ｐ，ｑ，ｒ，ｓ，ｔ，ｕ，ｖ，ｗを、（ｂ）のように変形する。
【０１４６】
（７）図４５において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎ（残り）を用いた変形（続き）を表す。同様に、（ａ）から（ｂ）のように、ｒ６‖ｒ７＆ｒ８−ｒ６−ｏ＆ｐ＆ｑ，ｗ、ｒ６‖ｒ７＆ｒ８−ｒ７−ｒ＆ｓ＆ｔ，ｗ、ｒ６‖ｒ７＆ｒ８−ｒ８−ｕ＆ｖ，ｗに変形する。さらに、（ｃ）のように、ｒ−ｏ＆ｐ＆ｑ＆ｒ＆ｓ＆ｔ‖ｕ＆ｖ，ｗに変形する。
【０１４７】
（８）図４６において、グラフ変形の途中結果を表す。上記図４３と図４５の結果をまとめると図４６のようになる。
【０１４８】
（９）図４７において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎを再び用いた変形を表す。同様に再び、ｒ４‖ｒ５−ｒ４−・・・−ｈ，ｌ，ｍ，ａ１、ｒ４‖ｒ５−ｒ５−ａ５、ｒ４‖ｒ５−ｒ５−ｒ−・・・−ｏ＆ｐ＆ｑ＆ｒ＆ｓ＆ｔ‖ｕ＆ｖ，ｗ，ｘ，ｙ，ｚ，ａ１を変形する。
【０１４９】
（１０）図４８において、ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎの処理の再帰的実行を表す。（ａ）のように順番を決定して、（ｂ）のように変形する。
【０１５０】
（１１）図４９において、ｗａｉｔ  ｏｂｊｅｃｔが入っている場合のＡ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形を表す。（ａ）から（ｂ）のように、ｒ４‖ｒ５−ｒ４−・・・−ｈ，ｌ，ｍ，ａ１、ｒ４‖ｒ５−・・・−ａ５＆（ｏ＆ｐ＆ｑ＆ｒ＆ｓ＆ｔ‖ｕ＆ｖ）＆ｗ＆ｘ，ｙ，ｚ，ａ１に変形する。
【０１５１】
（１２）図５０において、部分木の最下位のｗａｉｔ  ｏｂｊｅｃｔの識別を表す。ｗａｉｔ  ｏｂｊｅｃｔはｍとｙである。
【０１５２】
（１３）図５１において、グラフ変形の途中結果を表す。上記図４６と図５０の結果をまとめると図５１のようになる。
【０１５３】
（１４）図５２において、検証対象動作木全体でのグラフ変形（順番決定）を表す。検証対象動作木全体について、図５２のように順番を決定する。
【０１５４】
（１５）図５３において、検証対象動作木全体でのグラフ変形（（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形）を表す。上記図５２のように順番を決定して変形すると図５３のようになる。
【０１５５】
（１６）図５４において、検証対象動作木全体でのグラフ変形（Ａ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形）を表す。最終的に、検証対象動作木全体でのグラフ変形は図５４のようになる。すなわち、ｒ−（（ａ＆ｂ＆ｃ‖ｄ＆ｅ＆ｆ＆ｇ）＆ｉ＆ｊ）＆ｋ＆ａ４、ｒ−ｒ−ｒ４‖ｒ５−ｒ４−・・・−ｈ，ｉ，ｍ，ａ１、ｒ−ｒ−ｒ４‖ｒ５−ｒ５−ａ５＆（ｏ＆ｐ＆ｑ＆ｒ＆ｓ＆ｔ‖ｕ＆ｖ）＆ｗ＆ｘ、ｒ−ｒ−ｒ４‖ｒ５−ｒ５−ｒ−・・・ｙ，ｚ，ａ１、ｒ−ｒ−ｒ−ａ２，ａ３となる。
【０１５６】
４−３．検証ＨＤＬの生成（図５５〜図６２：図５５）
（１）ステップＳ１２０１において、ｄｅｌａｙＣｎｔ＝１とし、検証対象動作木の一番左の頂点を取得し、ｍｏｓｔ＿ｌｅｆｔとする。
【０１５７】
（２）ステップＳ１２０２において、木がｗａｉｔを含まないか否かを判定し、そうならステップＳ１２０３へ、そうでないならステップＳ１２０４へ処理を移行する。
【０１５８】
（３）ステップＳ１２０３において、Ｐｒｏｐｅｒｔｙ＿ｓｉｍｐｌｅを実行し、処理を終了する。
【０１５９】
（４）ステップＳ１２０４において、Ｐｒｏｐｅｒｔｙ＿ｗａｉｔを実行し、処理をステップＳ１２０５へ移行する。
【０１６０】
（５）ステップＳ１２０５において、ＣｏｎｓｅｑＢｌｏｃｋを実行し、処理を終了する。
【０１６１】
４−３−１．Ｐｒｏｐｅｒｔｙ＿ｓｉｍｐｌｅ（図５６）
（１）ステップＳ１３０１において、検証対象動作木の頂点から右方向に深さ優先探索の手順で次の頂点を取得する。
【０１６２】
（２）ステップＳ１３０２において、下記
0004153699.tif 000004
なる記述を生成する。
【０１６３】
（３）ステップＳ１３０３において、木がｅｘｉを含むか判定し、そうなら処理をステップＳ１３０５へ、そうでないなら処理をステップＳ１３０４へ移行する。
【０１６４】
（４）ステップＳ１３０４において、下記
ｉｆ（！（ｍｏｓｔ＿ｌｅｆｔが表すブール式））
なる記述を生成する。
【０１６５】
（５）ステップＳ１３０５において、下記
0004153699.tif 000005
なる記述を生成する。
【０１６６】
（６）ステップＳ１３０６において、下記
ｅｎｄ
ｅｎｄ
なる記述を生成し、処理を終了する。
【０１６７】
４−３−２．Ｐｒｏｐｅｒｔｙ＿ｗａｉｔ（図５７）
（１）ステップＳ１４０１において、ｆｌｏｗ＿ｆｌｇ＝０とする。
【０１６８】
（２）ステップＳ１４０２において、検証対象動作木の頂点から右方向に深さ優先探索の手順で次の頂点を取得する。
【０１６９】
（３）ステップＳ１４０３において、ステップＳ１４０２で取得した頂点が、ｍｏｓｔ＿ｌｅｆｔか否か判定し、そうなら処理を終了し、そうでないならステップＳ１４０４へ処理を移行する。
【０１７０】
（４）ステップＳ１４０４において、ステップＳ１４０２で取得した頂点が、ｒｅｌａｔｉｏｎか否か判定し、そうならステップＳ１４０５へ、そうでないならステップＳ１４０６へ処理を移行する。
【０１７１】
（５）ステップＳ１４０５において、Ｐｒｏｐｅｒｔｙ＿ｗａｉｔを実行する。
【０１７２】
（６）ステップＳ１４０６において、ステップＳ１４０２で取得した頂点が、ｂｏｏｌ式のｒｅｌａｔｉｏｎか否か判定し、そうならステップＳ１４０７へ、そうでないならステップＳ１４０８へ処理を移行する。
【０１７３】
（７）ステップＳ１４０７において、Ｗａｉｔ＿Ｂｌｏｃｋを実行する。
【０１７４】
（８）ステップＳ１４０８において、ステップＳ１４０２で取得した頂点が、信号からなるブール式か否か判定し、そうならステップＳ１４０９へ、そうでないならステップＳ１４１３へ処理を移行する。
【０１７５】
（９）ステップＳ１４０９において、ｆｌｏｗ＿ｆｌｇ＝＝０か否か判定し、そうならステップＳ１４１０へ、そうでないならステップＳ１４１２へ処理を移行する。
【０１７６】
（１０）ステップＳ１４１０において、ｆｌｏｗ＿ｆｌｇ＝１とする。
【０１７７】
（１１）ステップＳ１４１１において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎに下記
ｆｌｇ＿ｔｍｐ＆取得した頂点の表すブール式
を代入する。
【０１７８】
（１２）ステップＳ１４１２において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎに下記
取得した頂点の表すブール式
を代入する。
【０１７９】
（１３）ステップＳ１４１３において、ステップＳ１４０２で取得した頂点が、ｗａｉｔか否か判定し、そうならステップＳ１４１４へ処理を移行する。
【０１８０】
（１４）ステップＳ１４１４において、ＷａｉｔＢｌｏｃｋを実行する。
【０１８１】
４−３−３．ＷａｉｔＢｌｏｃｋ（図５８および図５９）
（１）ステップＳ１５０１において、下記
ａｌｗａｙｓ＠（ｐｏｓｅｄｇｅクロック名）
＃ｄｅｌａｙＣｎｔ
なる記述を生成する。
【０１８２】
（２）ステップＳ１５０２において、Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１５０３へ、そうでないならステップＳ１５０６へ処理を移行する。
【０１８３】
（３）ステップＳ１５０３において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１５０４へ、そうでないならステップＳ１５０５へ処理を移行する。
【０１８４】
（４）ステップＳ１５０４において、下記
ｉｆ（！ｗａｉｔ解除条件）ｗａｉｔ＿ｆｌｇ［ｋ］［０］＝１’ｂ１；
ｅｌｓｅ                  ｗａｉｔ＿ｆｌｇ［ｋ］［０］＝１’ｂ０；
なる記述を生成する。
【０１８５】
（５）ステップＳ１５０５において、下記
ｉｆ（Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎ）ｗａｉｔ＿ｆｌｇ［ｋ］［０］＝１’ｂ１；
ｅｌｓｅ                          ｗａｉｔ＿ｆｌｇ［ｋ］［０］＝１’ｂ０；
なる記述を生成する。
【０１８６】
（６）ステップＳ１５０６において、下記
ｉｆ（Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ）ｂｅｇｉｎ
ｗａｉｔ（Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ）ｂｅｇｉｎ
なる記述を生成する。
【０１８７】
（７）ステップＳ１５０７において、ｌａｓｔＷａｉｔＦｌｇが空か判定し、そうならステップＳ１５０８へ、そうでないならステップＳ１５０９へ処理を移行する。
【０１８８】
（８）ステップＳ１５０８において、下記
ｗａｉｔ＿ｆｌｇ［ｋ］［２］＝１’ｂ０；
なる記述を生成する。
【０１８９】
（９）ステップＳ１５０９において、ｌａｓｔＷａｉｔＦｌｇ内の全てのｗａｉｔ＿ｆｌｇを全て１’ｂ０にセットする。
【０１９０】
（１０）ステップＳ１５１０において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１５１１へ、そうでないならステップＳ１５１２へ処理を移行する。
【０１９１】
（１１）ステップＳ１５１１において、下記
ｗａｉｔ＿ｆｌｇ［ｋ］［０］＝１’ｂ１；
ｅｎｄ
ｅｎｄ
なる記述を生成する。
【０１９２】
（１２）ステップＳ１５１２において、下記
0004153699.tif 000006
なる記述を生成する。
【０１９３】
（１３）ステップＳ１５１３において、ｄｅｌａｙＣｎｔをインクリメントする。
【０１９４】
（１４）ステップＳ１５１４において、下記
0004153699.tif 000007
なる記述を生成する。
【０１９５】
（１５）ステップＳ１５１５において、Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎに下記
ｗａｉｔ＿ｆｌｇ［ｋ］［２］
を代入する。
【０１９６】
（１６）ステップＳ１５１６において、ｄｅｌａｙＣｎｔをインクリメントし、ｋをインクリメントして、処理を終了する。
【０１９７】
４−３−４．ＷａｉｔＯＲＢｌｏｃｋ（図６０および図６１）
（１）ステップＳ１６０１において、ｒｅｌａｔｉｏｎのブール式の下位に存在する最も上位のｒｅｌａｔｉｏｎの数を取得し、ＲｏｏｔＲｅｌＣｎｔとする。
【０１９８】
（２）ステップＳ１６０２において、ｒｅｌａｔｉｏｎのブール式の下位に存在する最も左端の頂点を取得し、ｓｕｂ＿ｍｏｓｔ＿ｌｅｆｔとする。
【０１９９】
（３）ステップＳ１６０３において、ｊ＝１とする。
【０２００】
（４）ステップＳ１６０４において、左からｊ番目の最上位ｒｅｌａｔｉｏｎを取得する。
【０２０１】
（５）ステップＳ１６０５において、下記
ｓｕｂｄｅｌａｙＣｎｔ＝ｄｅｌａｙＣｎｔ
ｓｕｂＩＦ＿ｅｘｐｒｅｓｓｉｏｎ＝Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎ
ｓｕｂＷａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ＝Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ
の代入を行う。
【０２０２】
（６）ステップＳ１６０６において、Ｐｒｏｐｅｒｔｙ＿ｗａｉｔを実行する。
【０２０３】
（７）ステップＳ１６０７において、ｊをインクリメントする。
【０２０４】
（８）ステップＳ１６０８において、ｊ＞ＲｏｏｔＲｅｌＣｎｔか判定し、そうならステップＳ１６０９へ、そうでなければステップＳ１６０４へ処理を移す。
【０２０５】
（９）ステップＳ１６０９において、ｓｕｂｄｅｌａｙＣｎｔの最大値をｄｅｌａｙＣｎｔとする。
【０２０６】
（１０）ステップＳ１６１０において、Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎを上記処理で得られた
ｓｕｂＩＦ＿ｅｘｐｒｅｓｓｉｏｎ＆＆ｓｕｂＷａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ
のＯＲ表現とする。すなわち、下記式
Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ＝‖ＩｓｕｂＩＦ＿ｅｘｐｒｅｓｓｉｏｎ［Ｉ］＆＆ｓｕｂＷａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ［Ｉ］
をＷａｉｔ＿ｅｘｐｒｅｓｓｉｏｎに代入する。
【０２０７】
（１１）ステップＳ１６１１において、ｌａｓｔＷａｉｔＦｌｇにｓｕｂＷａｉｔ＿ｅｘｐｒｅｓｓｉｏｎを全て格納する。
【０２０８】
（１２）ステップＳ１６１２において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎを空にする。
【０２０９】
（１３）ステップＳ１６１３において、ｓｕｂ＿ｍｏｓｔ＿ｌｅｆｔ！＝ｍｏｓｔ＿ｌｅｆｔを判定し、もしそうならステップＳ１６１４へ、そうでなければ処理を終了する。
【０２１０】
（１４）ステップＳ１６１４において、頂点が信号かを識別し、もしそうならステップＳ１６１５へ、そうでないならステップＳ１６１６へ処理を移す。
【０２１１】
（１５）ステップＳ１６１５において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎに信号からなるブール式を代入する。
【０２１２】
（１６）ステップＳ１６１６において、頂点がｗａｉｔかを識別し、処理をステップＳ１６１７へ移行する。
【０２１３】
（１７）ステップＳ１６１７において、ＷａｉｔＢｌｏｃｋを実行し、処理を終了する。
【０２１４】
４−３−５．ＣｏｎｓｅｑＢｌｏｃｋ（図６２）
（１）ステップＳ１７０１において、ｍｏｓｔ＿ｌｅｆｔがｗａｉｔか判定し、そうならステップＳ１７０２へ、そうでないならステップＳ１７０４へ処理を移す。
【０２１５】
（２）ステップＳ１７０２において、ＷａｉｔＢｌｏｃｋを実行する。
【０２１６】
（３）ステップＳ１７０３において、下記
0004153699.tif 000008
なる記述を生成し、処理を終了する。
【０２１７】
（４）ステップＳ１７０４において、下記
ａｌｗａｙｓ＠（ｐｏｓｅｄｇｅ）
＃ｄｅｌａｙＣｎｔ
なる記述を生成する。
【０２１８】
（５）ステップＳ１７０５において、Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１７０８へ、そうでないならステップＳ１７０６へ処理を移す。
【０２１９】
（６）ステップＳ１７０６において、下記
0004153699.tif 000009
なる記述を生成する。
【０２２０】
（７）ステップＳ１７０７において、ｌａｓｔＷａｉｔＦｌｇが空か判定し、そうならステップＳ１７０８へ、そうでないならステップＳ１７０９へ処理を移す。
【０２２１】
（８）ステップＳ１７０８において、下記
ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎ＝１’ｂ０；
なる記述を生成する。
【０２２２】
（９）ステップＳ１７０９において、ＬａｓｔＷａｉｔＦｌｇに含まれる全ｆｌｇに対してｆｌｇ＝１’ｂ０；なる記述を生成する。
【０２２３】
（１０）ステップＳ１７１０において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１７１２へ、そうでないならステップＳ１７１１へ処理を移行する。
【０２２４】
（１１）ステップＳ１７１１において、下記
ｉｆ（Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎ）ｂｅｇｉｎ
なる記述を生成し、処理をステップＳ１７１２へ移行する。
【０２２５】
（１２）ステップＳ１７１２において、検証対象動作木がｅｘｉを含むか判定し、そうならステップＳ１７１３へ、そうでないならステップＳ１７１４へ処理を移す。
【０２２６】
（１３）ステップＳ１７１３において、下記
0004153699.tif 000010
なる記述を生成し、処理をステップＳ１７１５へ移行する。
【０２２７】
（１４）ステップＳ１７１４において、下記
ｉｆ（！（ｍｏｓｔ＿ｌｅｆｔの表す信号のブール式））
なる記述を生成し、処理をステップＳ１７１５へ移行する。
【０２２８】
（１５）ステップＳ１７１５において、Ｗａｉｔ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１７１７へ、そうでないならステップＳ１７１６へ処理を移す。
【０２２９】
（１６）ステップＳ１７１６において、下記
ｅｎｄ
なる記述を生成し、処理をステップＳ１７１７へ移す。
【０２３０】
（１７）ステップＳ１７１７において、Ｉｆ＿ｅｘｐｒｅｓｓｉｏｎが空か判定し、そうならステップＳ１７１９へ、そうでないならステップＳ１７１８へ処理を移す。
【０２３１】
（１８）ステップＳ１７１８において、下記
ｅｎｄ
なる記述を生成し、処理をステップＳ１７１９へ移行する。
【０２３２】
（１９）ステップＳ１７１９において、下記
ｅｎｄ
なる記述を生成し、処理を終了する。
【０２３３】
５．ＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍ
図６３および図６４により、ＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍの一例を説明する。図６３はＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍを示すフロー図、図６４はＣＴＬ生成可能性判定を示すフロー図である。
【０２３４】
図６３に示すように、ＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍは、まず、検証対象動作木がＣＴＬ生成可能かの判定チェックを行う方法を述べ（ステップＳ１８０１）、次いで、検証対象動作木の変形アルゴリズムの変更点に触れ（ステップＳ１８０２）、最終的に得られた検証対象動作木からＣＴＬを生成するアルゴリズムを述べる（ステップＳ１８０３）。ただし、前述したＶｅｒｉｌｏｇ−ＨＤＬ生成と同様な部分が多いため、詳しくは述べない。
【０２３５】
５−１．ＣＴＬ生成可能性判定（図６４）
（１）ステップＳ１９０１において、検証対象動作木の信号頂点で、左側より過去のサイクルが指定されている右側の頂点が存在するか否かを判定し、そうならステップＳ１９０４へ、そうでなければステップＳ１９０２へ処理を移行する。
【０２３６】
（２）ステップＳ１９０２において、ＡＮＤを含むｒｅｌａｔｉｏｎのブール式頂点の下位にｗａｉｔ頂点があるか判定し、もしあればステップＳ１９０４へ、なければステップＳ１９０３へ処理を移行する。
【０２３７】
（３）ステップＳ１９０３において、検証対象動作木の最右端頂点（ｍｏｓｔ＿ｌｅｆｔと呼ぶ）が接続されているｒｅｌａｔｉｏｎの頂点にｅｘｉが指定されていて、かつ片側の頂点の時刻が最右端頂点の時刻と一致するか判定し、そうならステップＳ１９０４へ、そうでないならステップＳ１９０５へ処理を移行する。
【０２３８】
（４）ステップＳ１９０４において、ＣＴＬ生成不能である旨、ユーザに通知し、処理を終了する。
【０２３９】
（５）ステップＳ１９０５において、Ｍｏｓｔ＿ｌｅｆｔに最も近い、ブール式でないｒｅｌａｔｉｏｎ頂点以外のｅｘｉ指定は全て削除し、処理を終了する。
【０２４０】
５−２．検証対象動作木の変形
検証対象動作木の変形における変更・追加点のみを述べる。検証対象動作木の変形において、まず最初に全てのｗａｉｔ頂点に対して、ｗａｉｔ頂点情報を
ＡＸ：ｎ｛Ａ（繰り返し条件＆！ｗａｉｔ解除条件Ｕｗａｉｔ解除条件）｝
に置換する。特に、ＡＸ：ｎのｎはｗａｉｔ  ｏｂｊｅｃｔの波形上でのサイクル数に対応する。
【０２４１】
次いで、各信号頂点をサイクル数ｎを用いて、ＡＸ：ｎ（信号名）に置換する。そして、トポロジカルソートを行い、一番順番の若いｗａｉｔ頂点またはｅｘｉが付加された信号頂点を検索し、検索された頂点がｒｅｌａｔｉｏｎのブール演算頂点の下位にある場合とそうでない場合とに分けて下記操作を行う。基本的に、左方向の深さ優先探索の手順で木を辿りながら処理を行う。
【０２４２】
１）検索された頂点がｒｅｌａｔｉｏｎのブール演算頂点の下位にある場合
その頂点が含まれる部分木を以下の方法で取得する。
【０２４３】
（１）ｒｅｌａｔｉｏｎのブール演算頂点の直下に位置するｒｅｌａｔｉｏｎ頂点で、今対象としているｗａｉｔ頂点を下位に含む頂点を選択する。
【０２４４】
（２）（１）で選択したｒｅｌａｔｉｏｎ頂点の下位全てからなる部分木を取得する。
【０２４５】
次いで、そのｗａｉｔ頂点よりも、トポロジカルソートで得られた順番が大きい信号頂点のサイクル情報を順番に従った相対サイクル情報に置き換える。これを木の範囲内で行う。他のｒｅｌａｔｉｏｎのブール演算頂点の直下に位置するｒｅｌａｔｉｏｎ頂点を頂点とする木に対しても、ｗａｉｔかｅｘｉ付き頂点が含まれているなら同じことをする。
【０２４６】
さらに、ｒｅｌａｔｉｏｎのブール演算頂点より順番が大きいものに対しても、同様に相対サイクル情報への置換を行うが、これは２）の手順を用いる。
【０２４７】
２）そうでない場合
その頂点よりも、トポロジカルソートで得られた順番が大きい信号頂点のサイクル情報を順番に従った相対サイクル情報に置き換える。操作がｒｅｌａｔｉｏｎのブール演算頂点に辿り着くと、ｒｅｌａｔｉｏｎのブール演算頂点の下位のｒｅｌａｔｉｏｎ頂点を頂点とする木夫々に対して独立に相対サイクル情報への置き換えを行う。この操作が終わると、また木を辿りながら相対サイクル情報への置換をｒｅｌａｔｉｏｎのブール演算頂点に辿り着くまで行う。
【０２４８】
なお、相対サイクル情報への置換では、ＡＸ：ｎ（信号名）をＡＹ：ｍ（信号名）に置換し、ｍは相対サイクル情報とする。
【０２４９】
次に、ｅｘｉが付加されている頂点情報のＡをＥに置換する。
【０２５０】
次に、（Ａ−＞Ｂ）−＞ＣをＡ＆Ｂ−＞Ｃに変換する操作では、ＡＹやＥＸ、ＥＹが含まれない場合は、たとえば
ＡＸ（ａ）＆ＡＸ（ｂ）＆ＡＸ：２（ｃ）＝ＡＸ（ａ＆ｂ＆ＡＸ（Ｃ））
のようにサイクル数による括り出しを行う。含まれる場合は、以下の式変形ルールを適時用いて求める。
【０２５１】
Ｐ＆ＡＹ（Ｑ）＝Ｐ＆ＡＸ（Ｑ）
Ｐ＆ＥＹ（Ｑ）＝Ｐ＆ＥＸ（Ｑ）
ＡＸ（Ｐ）＆ＡＹ（Ｑ）＝ＡＸ（Ｐ＆ＡＸ（Ｑ））
ＡＸ（Ｐ）＆ＥＹ（Ｑ）＝ＡＸ（Ｐ＆ＥＸ（Ｑ））
ＡＹ（Ｐ）＆ＡＹ（Ｑ）＝ＡＹ（Ｐ＆ＡＸ（Ｑ））
ＡＹ（Ｐ）＆ＥＹ（Ｑ）＝ＡＹ（Ｐ＆ＥＸ（Ｑ））
ＥＸ（Ｐ）＆ＡＹ（Ｑ）＝ＥＸ（Ｐ＆ＡＸ（Ｑ））
ＥＸ（Ｐ）＆ＥＹ（Ｑ）＝ＥＸ（Ｐ＆ＥＸ（Ｑ））
ＥＹ（Ｐ）＆ＡＹ（Ｑ）＝ＥＹ（Ｐ＆ＡＸ（Ｑ））
ＥＹ（Ｐ）＆ＥＹ（Ｑ）＝ＥＹ（Ｐ＆ＥＸ（Ｑ））
特に、式変形は左から行う。たとえば、下記のようである。
【０２５２】
ＡＹ（Ｐ）＆ＥＹ（Ｑ）＆ＡＹ：２（Ｒ）＆ＥＹ：３（Ｓ）
＝ＡＹ（Ｐ）＆ＥＹ（Ｑ）＆ＡＹ：２（Ｒ＆ＥＸ：３（Ｓ））
＝ＡＹ（Ｐ）＆ＥＹ（Ｑ＆ＡＸ：２（Ｒ＆ＥＸ：３（Ｓ）））
＝ＡＹ（Ｐ＆ＥＸ（Ｑ＆ＡＸ：２（Ｒ＆ＥＸ：３（Ｓ）））
また、‖が含まれている場合などは、それを‖の両辺を固まりと見なして扱う。たとえば下記のようである。
【０２５３】
ＡＹ（Ｐ）＆ＥＹ（Ｑ）＆（ＡＹ：２（Ｒ）‖ＥＹ：３（Ｓ））
＝ＡＹ（Ｐ）＆ＥＹ（Ｑ＆（ＡＸ：２（Ｒ）‖ＥＸ：３（Ｓ）））
＝ＡＹ（Ｐ＆ＥＸ（Ｑ＆（ＡＸ：２（Ｒ）‖ＥＸ：３（Ｓ）））
なお、ＡＮＤ−ＯＲ式の扱いは、分配法則を適用して右側を扱ってから、ＯＲ内部の＆から変形して上記のように扱えばよい。たとえば下記のようである。
【０２５４】
0004153699.tif 000011
次に、ｒｅｌａｔｉｏｎのブール式の扱いであるが、これはＶｅｒｉｌｏｇ−ＨＤＬ生成と同様である。
【０２５５】
以上が、検証対象動作木での変更・追加処理である。
【０２５６】
５−３．ＣＴＬの生成
基本的にＶｅｒｉｌｏｇ−ＨＤＬのｃｈｅｃｋｅｒ生成と同じく、変形後の検証対象動作木を辿りながら処理を行う。これに関しても概略のみを述べる。
【０２５７】
まず、木での最左端の頂点を取得する。その頂点以外の部分の処理を以下に述べる。木を辿りながら頂点情報を＆で単純に結合していき、ｒｅｌａｔｉｏｎのＯＲ演算に辿り着くと、以下の処理を行い、それを終了して続きがあるなら、また＆で単純に結合していく。これを最左端の頂点に辿り着くまで行い、得られた＆結合式−＞最左端頂点の式なる式を構成して、全体式変形処理を行う。
【０２５８】
ｒｅｌａｔｉｏｎのＯＲ演算での処理
本頂点下位の部分木を識別し、夫々の木の最左端を取得する。それらが一致していなければ、処理を中断し、一致していれば、それが先に取得した最左端頂点と一致するか識別する。
【０２５９】
１）最左端と一致した場合
夫々の部分木の頂点の＆を左方向の深さ優先探索の順番で最左端頂点の手前まで＆で結合していく。得られた式−＞最左端頂点の式の形式を各部分木に対して構成し、たとえば部分木が３つあったとすると、
（部分木１の＆結合式‖部分木２の＆結合式‖部分木３の＆結合式）−＞
最左端頂点の式
を構成し、これを今まで得た＆結合式に＆で結合し全体式変形処理へ進む。
【０２６０】
２）一致しない場合
夫々の部分木の頂点の＆を左方向の深さ優先探索の順番で＆で結合していく。たとえば部分木が３つあったとすると、
（部分木１の＆結合式‖部分木２の＆結合式‖部分木３の＆結合式）
を構成し、これを今まで得た＆結合式に＆で結合する。
【０２６１】
全体式変形処理では、最左端頂点の式にＹがある場合、得られた＆結合式−＞最左端頂点の式を、
得られた＆結合式−＞（得られた＆結合式）＆最左端頂点の式
に変形し、−＞の前後の式に対して頂点での式変形同様右側から式変形処理を行う。このとき、頂点の式変形で用いた変形規則および下記式変形規則を適宜適用し、Ｙを除去する。得られた変形式を対応する−＞の両端の式に代入し、これで、ＣＴＬが得られる。Ｙが無い場合は、そのまま出力すればよい。
【０２６２】
Ａ（Ｐ１ＵＰ２）＆ＡＹ（Ｑ）＝Ａ（Ｐ１Ｕ（Ｐ２＆ＡＸ（Ｑ））
Ａ（Ｐ１ＵＰ２）＆ＥＹ（Ｑ）＝Ａ（Ｐ１Ｕ（Ｐ２＆ＥＸ（Ｑ））
Ｅ（Ｐ１ＵＰ２）＆ＡＹ（Ｑ）＝Ｅ（Ｐ１Ｕ（Ｐ２＆ＡＸ（Ｑ））
Ｅ（Ｐ１ＵＰ２）＆ＥＹ（Ｑ）＝Ｅ（Ｐ１Ｕ（Ｐ２＆ＥＸ（Ｑ））
たとえば、以下のようである。
【０２６３】
Ｐ＆ＡＹ（Ｑ）＆ＡＹ：２（Ａ（Ｐ１ＵＰ２））＆ＥＹ（Ｓ）＆ＥＹ（Ａ（Ｐ３ＵＰ４）＆ＡＹ（Ｔ）−＞ＡＹ：２（Ｏ）
から、
Ｐ＆ＡＹ（Ｑ）＆ＡＹ：２（Ａ（Ｐ１ＵＰ２））＆ＥＹ（Ｓ）＆ＥＹ（Ａ（Ｐ３ＵＰ４）＆ＡＹ（Ｔ）
および
Ｐ＆ＡＹ（Ｑ）＆ＡＹ：２（Ａ（Ｐ１ＵＰ２））＆ＥＹ（Ｓ）＆ＥＹ（Ａ（Ｐ３ＵＰ４）＆ＡＹ（Ｔ）＆ＡＹ：２（Ｏ）
を構成する。さらに、
0004153699.tif 000012
0004153699.tif 000013
なるＣＴＬを得る。
【０２６４】
従って、本実施の形態の機能検証記述生成装置によれば、設計者や検証担当者は検証対象の比較的操作可能なタイミングダイアグラム編集装置２上でＨＤＬの記述から得られた端子および内部ピン情報を選択し、タイミングダイアグラム編集装置２上で、この選択後の端子や内部ピンの信号の波形、この波形間の論理的関係、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報を入力しながら、タイミングダイアグラム編集装置２上でタイミングダイアグラムを作成編集することができる。
【０２６５】
よって、タイミングダイアグラム編集装置２は、タイミングダイアグラム上に検証項目を明確に記述することが可能となり、これによって検証項目の表現の曖昧さを排除することができる。従って、設計者や検証担当者の間で正確な情報の交換が可能となり、人的ミスを排除することができる。
【０２６６】
さらに、検証対象動作抽出装置３は、タイミングダイアグラム編集装置２を使用し、設計者や検証担当者によって編集されたタイミングダイアグラム編集装置２から送出されるタイミングダイアグラム情報から波形間の論理的関係、この論理的関係が指定された波形を含む端子や内部ピン情報、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報などを抽出し、検証記述生成装置４は検証対象動作抽出装置３から供給される波形の論理的関係、この論理的関係が指定された波形を含む端子や内部ピン情報、およびこの論理的関係が常に成立するのか少なくとも１回は成立するのかの生起情報などに基づき機能検証記述を自動生成することができる。
【０２６７】
よって、検証記述生成装置４などは、設計者や検証担当者がＨＤＬやＨＤＬ以外の検証記述言語を知らなくとも、タイミングダイアグラム編集装置２を使用してタイミングダイアグラムを編集して回路動作の検証内容の明確化を行うという設計者や検証担当者が従来より行っている操作を行うことで、機能検証記述を生成することができる。従って、検証記述生成装置４などは、設計者や検証担当者の機能検証作業負担を軽減し、機能検証効率の向上による設計コストの低減、さらには製品の生産コストを低減することができる。
【０２６８】
以上、本発明者によってなされた発明をその実施の形態に基づき具体的に説明したが、本発明は前記実施の形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能であることはいうまでもない。
【０２６９】
たとえば、本発明は、前記実施の形態に記述したような技術に限らず、デジタル回路全般に適用することが可能であり、さらに設計仕様書、機能検査仕様書の作成からＨＤＬ、コーディング後に行うデバッグ作業などまで幅広い技術に応用することができる。
【０２７０】
【発明の効果】
本願において開示される発明のうち、代表的なものによって得られる効果を簡単に説明すれば、以下のとおりである。
【０２７１】
（１）タイミングダイアグラム編集手段は、タイミングダイアグラム上に検証項目を明確に記述することが可能となり、これによって検証項目の表現の曖昧さを排除することができるので、設計者や検証担当者の間で正確な情報の交換が可能となり、人的ミスを排除することができる。
【０２７２】
（２）検証記述生成手段などは、設計者や検証担当者がＨＤＬやＨＤＬ以外の検証記述言語を知らなくとも、タイミングダイアグラム編集手段を使用してタイミングダイアグラムを編集して回路動作の検証内容の明確化を行うという設計者や検証担当者が従来より行っている操作を行うことで、機能検証記述を生成することができるので、設計者や検証担当者の機能検証作業負担を軽減し、機能検証効率の向上による設計コストの低減、さらには製品の生産コストを低減することができる。
【０２７３】
（３）検証担当者が新たにＨＤＬやＨＤＬ以外の検証記述言語を学習しなくても、ＨＤＬを学習済みの設計者がＨＤＬ以外の検証記述言語を学習したり、ＨＤＬで記述した機能検証記述自体の検証を行わなくても、検証対象回路の機能検証項目を検証するための機能検証記述を作成可能とする機能検証記述生成装置を提供することが可能となる。
【０２７４】
（４）設計者や検証担当者がタイミングダイアグラムを用いて回路動作の検証内容を明確にかつ統一的に記述する記述法を提供することが可能となる。
【図面の簡単な説明】
【図１】本発明の一実施の形態の機能検証記述生成装置を示す構成図である。
【図２】本発明の一実施の形態の機能検証記述生成装置において、コンペアオブジェクトを説明するための回路例の説明図である。
【図３】本発明の一実施の形態の機能検証記述生成装置において、コンペアオブジェクトを説明するためのタイミングダイアグラム例の説明図である。
【図４】本発明の一実施の形態の機能検証記述生成装置において、ウェイトオブジェクトを説明するためのタイミングダイアグラム例の説明図である。
【図５】本発明の一実施の形態の機能検証記述生成装置において、ウェイトオブジェクトを説明するためのチェックボックス例の説明図である。
【図６】本発明の一実施の形態の機能検証記述生成装置において、検証対象動作木の構成とその変形を示すフロー図である。
【図７】本発明の一実施の形態の機能検証記述生成装置において、ＨＤＬの端子情報の格納における階層ツリーを示す説明図である。
【図８】本発明の一実施の形態の機能検証記述生成装置において、図７の階層ツリーに付随する端子情報を示す説明図である。
【図９】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（１）を示す説明図である。
【図１０】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（２）を示す説明図である。
【図１１】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（３）を示す説明図である。
【図１２】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（４）を示す説明図である。
【図１３】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（５）を示す説明図である。
【図１４】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（６）を示す説明図である。
【図１５】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（７）を示す説明図である。
【図１６】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（８）を示す説明図である。
【図１７】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（９）を示す説明図である。
【図１８】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（１０）を示す説明図である。
【図１９】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの格納におけるタイミングダイアグラム例（１１）を示す説明図である。
【図２０】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラム分割例を示す説明図である。
【図２１】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラムの記憶イメージを示す説明図である。
【図２２】本発明の一実施の形態の機能検証記述生成装置において、図２１に続くタイミングダイアグラムの記憶イメージを示す説明図である。
【図２３】本発明の一実施の形態の機能検証記述生成装置において、タイミングダイアグラム分割手段の動作を示すフロー図である。
【図２４】本発明の一実施の形態の機能検証記述生成装置において、検証対象動作の切り出しにおける検証対象動作情報取得手段の動作を示すフロー図である。
【図２５】本発明の一実施の形態の機能検証記述生成装置において、検証対象動作情報の記憶イメージを示す説明図である。
【図２６】本発明の一実施の形態の機能検証記述生成装置において、検証対象動作から作成される木構造の記憶イメージを示す説明図である。
【図２７】本発明の一実施の形態の機能検証記述生成装置において、図２６に続く検証対象動作から作成される木構造の記憶イメージを示す説明図である。
【図２８】本発明の一実施の形態の機能検証記述生成装置において、ＴＤＯ２Ｖｅｒｉｌｏｇ  Ａｌｇｏｒｉｔｈｍを示すフロー図である。
【図２９】本発明の一実施の形態の機能検証記述生成装置において、格納変数の割り当てを示すフロー図である。
【図３０】本発明の一実施の形態の機能検証記述生成装置において、格納サイクル数の算出を示すフロー図である。
【図３１】本発明の一実施の形態の機能検証記述生成装置において、格納サイクル数の算出におけるテーブル構造を示す説明図である。
【図３２】本発明の一実施の形態の機能検証記述生成装置において、Ｗａｉｔ制御用フラグ生成・初期値決定を示すフロー図である。
【図３３】本発明の一実施の形態の機能検証記述生成装置において、Ｗａｉｔ制御用フラグ生成・初期値決定におけるテーブル構造を示す説明図である。
【図３４】本発明の一実施の形態の機能検証記述生成装置において、初期値決定を示すフロー図である。
【図３５】本発明の一実施の形態の機能検証記述生成装置において、変数宣言ＨＤＬ記述生成を示すフロー図である。
【図３６】本発明の一実施の形態の機能検証記述生成装置において、変数値格納ＨＤＬ記述生成を示すフロー図である。
【図３７】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形を示すフロー図である。
【図３８】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形を示す説明図である。
【図３９】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎの識別）を示す説明図である。
【図４０】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形）を示す説明図である。
【図４１】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形（続き））を示す説明図である。
【図４２】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（Ａ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形）を示す説明図である。
【図４３】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎを用いた変形）を示す説明図である。
【図４４】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎ（残り）を用いた変形）を示す説明図である。
【図４５】（ａ），（ｂ），（ｃ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎ（残り）を用いた変形（続き））を示す説明図である。
【図４６】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（グラフ変形の途中結果）を示す説明図である。
【図４７】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎを再び用いた変形）を示す説明図である。
【図４８】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｒｅｌａｔｉｏｎ  ｂｏｏｌｅａｎの処理の再帰的実行）を示す説明図である。
【図４９】（ａ），（ｂ）は本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（ｗａｉｔ  ｏｂｊｅｃｔが入っている場合のＡ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形）を示す説明図である。
【図５０】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（部分木の最下位のｗａｉｔ  ｏｂｊｅｃｔの識別）を示す説明図である。
【図５１】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（グラフ変形の途中結果）を示す説明図である。
【図５２】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（検証対象動作木全体でのグラフ変形（順番決定））を示す説明図である。
【図５３】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（検証対象動作木全体でのグラフ変形（（Ａ−＞Ｂ）−＞ＣのＡ−＞（Ｂ−＞Ｃ）への変形））を示す説明図である。
【図５４】本発明の一実施の形態の機能検証記述生成装置において、グラフ変形（検証対象動作木全体でのグラフ変形（Ａ−＞（Ｂ−＞Ｃ）のＡ＆Ｂ−＞Ｃへの変形））を示す説明図である。
【図５５】本発明の一実施の形態の機能検証記述生成装置において、検証ＨＤＬの生成を示すフロー図である。
【図５６】本発明の一実施の形態の機能検証記述生成装置において、Ｐｒｏｐｅｒｔｙ＿ｓｉｍｐｌｅを示すフロー図である。
【図５７】本発明の一実施の形態の機能検証記述生成装置において、Ｐｒｏｐｅｒｔｙ＿ｗａｉｔを示すフロー図である。
【図５８】本発明の一実施の形態の機能検証記述生成装置において、ＷａｉｔＢｌｏｃｋを示すフロー図である。
【図５９】本発明の一実施の形態の機能検証記述生成装置において、図５８に続くＷａｉｔＢｌｏｃｋを示すフロー図である。
【図６０】本発明の一実施の形態の機能検証記述生成装置において、ＷａｉｔＯＲＢｌｏｃｋを示すフロー図である。
【図６１】本発明の一実施の形態の機能検証記述生成装置において、図６０に続くＷａｉｔＯＲＢｌｏｃｋを示すフロー図である。
【図６２】本発明の一実施の形態の機能検証記述生成装置において、ＣｏｎｓｅｑＢｌｏｃｋを示すフロー図である。
【図６３】本発明の一実施の形態の機能検証記述生成装置において、ＴＤＯ２ＣＴＬ  Ａｌｇｏｒｉｔｈｍを示すフロー図である。
【図６４】本発明の一実施の形態の機能検証記述生成装置において、ＣＴＬ生成可能性判定を示すフロー図である。
【図６５】本発明の技術と公開公報の技術とを比較するための、公開公報の技術の概要を示す説明図である。
【図６６】本発明の技術と公開公報の技術とを比較するための、本発明の技術の概要を示す説明図である。
【符号の説明】
１  端子情報抽出装置
２  タイミングダイアグラム編集装置
３  検証対象動作抽出装置
４  検証記述生成装置
５  検証記述ファイル
１１  ＨＤＬ読み込み装置
１２  ＨＤＬ記憶装置
１３  端子情報抽出装置
１４  端子情報記憶装置
３１  タイミングダイアグラム記憶装置
３２  検証対象動作情報抽出装置
３３  検証対象動作情報記憶装置
【図１】
0004153699.tif 000014
【図２】
0004153699.tif 000015
【図３】
0004153699.tif 000016
【図４】
0004153699.tif 000017
【図５】
0004153699.tif 000018
【図６】
0004153699.tif 000019
【図７】
0004153699.tif 000020
【図８】
0004153699.tif 000021
【図９】
0004153699.tif 000022
【図１０】
0004153699.tif 000023
【図１１】
0004153699.tif 000024
【図１２】
0004153699.tif 000025
【図１３】
0004153699.tif 000026
【図１４】
0004153699.tif 000027
【図１５】
0004153699.tif 000028
【図１６】
0004153699.tif 000029
【図１７】
0004153699.tif 000030
【図１８】
0004153699.tif 000031
【図１９】
0004153699.tif 000032
【図２０】
0004153699.tif 000033
【図２１】
0004153699.tif 000034
【図２２】
0004153699.tif 000035
【図２３】
0004153699.tif 000036
【図２４】
0004153699.tif 000037
【図２５】
0004153699.tif 000038
【図２６】
0004153699.tif 000039
【図２７】
0004153699.tif 000040
【図２８】
0004153699.tif 000041
【図２９】
0004153699.tif 000042
【図３０】
0004153699.tif 000043
【図３１】
0004153699.tif 000044
【図３２】
0004153699.tif 000045
【図３３】
0004153699.tif 000046
【図３４】
0004153699.tif 000047
【図３５】
0004153699.tif 000048
【図３６】
0004153699.tif 000049
【図３７】
0004153699.tif 000050
【図３８】
0004153699.tif 000051
【図３９】
0004153699.tif 000052
【図４０】
0004153699.tif 000053
【図４１】
0004153699.tif 000054
【図４２】
0004153699.tif 000055
【図４３】
0004153699.tif 000056
【図４４】
0004153699.tif 000057
【図４５】
0004153699.tif 000058
【図４６】
0004153699.tif 000059
【図４７】
0004153699.tif 000060
【図４８】
0004153699.tif 000061
【図４９】
0004153699.tif 000062
【図５０】
0004153699.tif 000063
【図５１】
0004153699.tif 000064
【図５２】
0004153699.tif 000065
【図５３】
0004153699.tif 000066
【図５４】
0004153699.tif 000067
【図５５】
0004153699.tif 000068
【図５６】
0004153699.tif 000069
【図５７】
0004153699.tif 000070
【図５８】
0004153699.tif 000071
【図５９】
0004153699.tif 000072
【図６０】
0004153699.tif 000073
【図６１】
0004153699.tif 000074
【図６２】
0004153699.tif 000075
【図６３】
0004153699.tif 000076
【図６４】
0004153699.tif 000077
【図６５】
0004153699.tif 000078
【図６６】
0004153699.tif 000079