"プログラムを実行する制御部と、記憶部と、入力部と、を備える論理検証システムにおいて、論理を検証する検証項目である第1のプロパティを用いて前記論理を検証する論理検証方法であって、前記入力部から入力された論理と、前記入力部から入力された前記第1のプロパティと、を取得し、前記記憶部に記録する第1の手順と、前記第1のプロパティから、当該第1のプロパティで発生する事象を時系列に表す時系列表を作成し、作成された前記時系列表を前記記憶部に記録する第2の手順と、前記第1のプロパティと前記時系列表とに基づいて、前記第1のプロパティの逆、裏又は対偶を意味する第2のプロパティを生成し、前記生成された第2のプロパティを前記記憶部に記録する第3の手順と、前記第1のプロパティ又は前記作成された第2のプロパティを用いて、前記論理を検証する第4の手順と、を備えることを特徴とする論理検証方法。前記第2の手順は、前記第1のプロパティに含まれる演算子を検出することにより仮定部と帰結部とを抽出する手順と、抽出した前記仮定部及び前記帰結部それぞれについて、前記事象の内容である信号の変化と、前記変化が発生する時間と、を取得する手順と、前記信号の変化を前記時間に基づいた時系列に表す前記時系列表を作成し、作成した前記時系列表を前記記録部に記録する手順と、前記仮定部と前記帰結部との関係を表す帰結式を作成し、作成した前記帰結式を前記時系列表に記録する手順と、前記時系列に表された最終時間から開始時間への逆の時系列である逆時間を作成し、作成した前記逆時間を前記時系列表に記録する手順と、を含むことを特徴とする請求項1に記載の論理検証方法。前記第2の手順は、さらに、前記第1のプロパティから取得した前記信号の変化が関数として表されている場合は、前記関数を、信号と前記信号の変化と前記時間との表記に変換する手順を含むことを特徴とする請求項2に記載の論理検証方法。前記第3の手順は、前記時系列表から、前記信号と前記信号の変化と前記時間と前記逆時間とを取得する手順と、前記時系列表から、前記帰結式を取得し、取得した前記帰結式の仮定部と帰結部とを入れ替えた新たな帰結式に変換する手順と、前記新たな帰結式に、前記信号と前記信号の変化と前記時間とを当てはめて逆を意味する前記第2のプロパティを作成し、作成した逆を意味する前記第2のプロパティを前記記憶部に記録する手順と、を含むことを特徴とする請求項2又は3に記載の論理検証方法。前記第3の手順は、前記第1のプロパティの仮定部と帰結部とをそれぞれ否定形に変換して裏を意味する前記第2のプロパティを作成し、作成した裏を意味する前記第2のプロパティを前記記憶部に記録する手順を含むことを特徴とする請求項2から4のいずれか一つに記載の論理検証方法。前記第3の手順は、前記時系列表から、前記信号と前記信号の変化と前記時間と前記逆時間とを取得する手順と、前記時系列表から、前記帰結式を取得し、取得した前記帰結式の仮定部と帰結部とを入れ替えた新たな帰結式に変換する手順と、前記新たな帰結式に、前記信号と前記信号の変化と前記時間とを当てはめて逆を意味する前記第2のプロパティを作成する手順と、作成した逆を意味する前記第2のプロパティの仮定部と帰結部とをそれぞれ否定形に変換して、対偶を意味する前記第2のプロパティを作成し、作成した逆を意味する前記第2のプロパティを前記記憶部に記録する手順と、を含むことを特徴とする請求項2から5のいずれか一つに記載の論理検証方法。前記第4の手順は、前記論理に基づくロジックコーンと、前記第1又は第2のプロパティに基づく期待値のロジックコーンとを作成する手順と、前記ロジックコーンの結果と前記期待値のロジックコーンの結果とが等価であるか否かを判定する手順と、を含むことを特徴とする請求項1から6のいずれか一つに記載の論理検証方法。前記論理は、レジスタ転送レベルにより記述されていることを特徴とする請求項1から7のいずれか一つに記載の論理検証方法。前記論理検証システムは、情報を表示する表示部を備え、前記第2の手順は、作成した前記時系列表を、前記表示部に表示する手順を含むことを特徴とする請求項1から8のいずれか一つに記載の論理検証方法。前記論理検証システムは、情報を表示する表示部を備え、前記第3の手順は、生成した前記第2のプロパティにおける前記信号の変化を前記時間に基づいた時系列に表す新たな時系列表を作成し、作成した前記新たな時系列表を前記表示部に表示する手順を含むことを特徴とする請求項1から9のいずれか一つに記載の論理検証方法。制御部と、記憶部と、入力部と、出力部と、を備え、論理を検証する検証項目である第1のプロパティを用いて前記論理を検証する論理検証システムにおいて、前記制御部が前記記憶部に記録されているプログラムを実行することによって、表作成部、プロパティ生成部及び検証部が実現されており、前記入力部から入力された論理と、前記入力部から入力された前記第1のプロパティと、を取得し、前記記憶部に記録し、前記表作成部は、前記第1のプロパティから、当該第1のプロパティで発生する事象を時系列に表す時系列表を作成し、作成した前記時系列表を前記記憶部に記録し、前記プロパティ生成部は、前記第1のプロパティと前記時系列表とに基づいて、前記第1のプロパティの逆、裏又は対偶を意味する第2のプロパティを生成し、生成した前記第2のプロパティを前記記憶部に記録し、前記検証部は、前記第1のプロパティ又は前記作成した第2のプロパティを用いて、前記論理を検証し、前記出力部は、前記検証部の検証結果を出力することを特徴とする論理検証システム。前記表作成部は、前記第1のプロパティに含まれる演算子を検出することにより仮定部と帰結部とを抽出し、抽出した前記仮定部及び前記帰結部それぞれについて、前記事象の内容である信号の変化と、前記変化が発生する時間と、を取得し、前記信号の変化を前記時間に基づいた時系列に表す前記時系列表を作成して、作成した前記時系列表を前記記録部に記録し、前記仮定部と前記帰結部との関係を表す帰結式を作成して、作成した前記帰結式を前記時系列表に記録し、前記時系列に表された最終時間から開始時間への逆の時系列である逆時間を作成して、作成した前記逆時間を前記時系列表に記録することを特徴とする請求項11に記載の論理検証システム。前記出力部は、前記表作成部によって作成した時系列表を表示することを特徴とする請求項11又は12に記載の論理検証システム。前記プロパティ生成部は、生成した前記第2のプロパティにおける前記信号の変化を前記時間に基づいた時系列に表す新たな時系列表を作成し、前記表示部は、作成した前記新たな時系列表を表示することを特徴とする請求項11から13のいずれか一つに記載の論理検証システム。前述の従来技術は、動作合成ツールを使用する設計において、C言語などの抽象度の高い記述からプロパティを抽出し、抽出したプロパティをRTLのプロパティに変換するものである。しかし、従来技術は、論理の記述形式からプロパティを抽出することは可能であるが、抽出したプロパティだけでは全ての検証項目を満足させることはできず、検証回路に対して網羅的な検証をするためは不十分である。そのため、プロパティを網羅的に生成する必要があるが、これには時間的、人的なコストが多く発生する。本発明はこのような問題点に鑑みてなされたものであり、論理検証における検査項目であるプロパティを効率的に生成できる論理検証方法及び論理検証装置を提供することを特徴とする。本発明の一実施態様によれば、論理と、論理を検証する検証項目である第1のプロパティと、を取得する第1の手順と、第1のプロパティで発生する事象を時系列に並べた時系列表を作成する第2の手順と、第1のプロパティと時系列表とに基づいて、検証項目の逆、裏又は対偶を意味する第2のプロパティを作成する第3の手順と、第1のプロパティ及び作成された第2のプロパティを用いて、論理を検証する第4の手順と、を備える。本発明によれば、検証者が作成する第1のプロパティを元にして、逆、裏、対偶を意味する第2のプロパティを作成するので、複数のプロパティを網羅的に生成することにより、論理検証の検証品質を向上させることができる。さらに、論理検証における時間的、人的なコストを削減することができる。以下、本発明の第1の実施の形態を、図面を参照して説明する。図1は、本実施形態の論理検証支援部10のブロック図である。本実施形態の論理検証支援部10は、オペレータが設計した論理デバイスの論理回路を、プロパティを用いて形式的論理検証を行う装置である。形式的論理検証とは、論理回路に期待される動作や、禁止される動作をプロパティとして定義し、検証対象の論理回路がプロパティに違反する動作を起こさないように設計されているかどうかを検査するものである。論理検証支援部10は、入力受付部101、表作成部102、プロパティ生成部103、検証部104及び検証結果出力部105を備える。入力受付部101は、オペレータからプロパティ等のデータや指令の入力を受付ける。表作成部102は、入力されたプロパティから後述する時系列表を作成する。プロパティ生成部103は、オペレータが入力したプロパティを命題として逆、裏、対偶の意味を持つプロパティを生成する。検証部104は、プロパティを検証する。検証結果出力部105は、プロパティの検証結果を出力する。図2は、本実施形態における形式的論理検証が適用される論理デバイス設計のフローチャートである。論理デバイス設計において、オペレータは、論理デバイスの方式を検討する方式検討S300を実行し、方式を実現させるための機能を検討する機能検討S301を実行し、機能を実現するために論理を記述する論理設計S302を実行する。論理設計では、RTLRegisterTransferLevel;レジスタ転送レベルによって記述された論理が作成される。次に、オペレータは、作成されたRTLを形式的論理検証するために、論理検証S303を実行する。このステップS303では、論理検証支援部10において、後述するプロパティを用いた形式的論理検証を実行する。論理検証が終了し、RTLの正当性が確認された後、RTLをゲートレベルに合成する論理合成S304を実行し、作成されたゲートを実際のデバイスに配置する実装S305を実行する。このような手順により、論理デバイスの設計が行われる。図3は、本実施形態の論理検証支援部10を実現する論理検証支援システム11のハードウェア構成を示すブロック図である。論理検証支援システム11は、CPU111、メモリ112、HDD113、入出力インタフェース114、表示部117及び入力部118を備える。CPU111、メモリ112、HDD113及び入出力インタフェース114は、バス115よって相互に接続される。CPU111は、論理検証支援システム11の制御を司る制御部である。CPU111は、HDD113に格納される論理検証支援プログラム116を、メモリ112上に読み出し、これを実行する。CPU111が論理検証支援プログラム116を実行することによって、論理検証支援部10が実行される。メモリ112は、例えばDRAMにより構成される。メモリ112は、論理検証支援プログラム116や、論理検証支援プログラム116が実行するために用いるデータやテーブル等を一時的に記録する。HDD113は、例えば磁気ディスクドライブにより構成される。HDD113は、論理検証支援システム11によって実行されるプログラム、データ等を記録する。例えば、論理検証の対象の論理回路のRTLや、演算子、関数等のサイクル遅延を表す関数変換テーブル130等は、オペレータにより予め記憶される。これらメモリ112およびHDD113によって記憶部が構成される。入出力インタフェース114は、論理検証支援部10の動作に関わる情報を表示部117に表示する。また、入出力インタフェース114は、オペレータ等により入力部118に入力される情報を論理検証支援部10に伝達する。なお、表示部117及び入力部118は、ネットワーク等を経由して他のコンピュータやストレージ等にデータを送受信できるように構成されていてもよい。論理検証支援システム11が、他のコンピュータからデータを入力したり、他のコンピュータに結果を表示するように構成されていてもよい。次に、論理検証支援部10が実行する形式的論理検証について説明する。形式的論理検証は、図2のステップS302において作成した論理のRTLに対して、プロパティと呼ばれる検証項目を作成し、この検証項目を用いてRTLの論理を検証する。この結果、RTLの論理の正当性、等価性等が検証される。図4は、本実施形態のプロパティの一例の説明図である。プロパティとは、ある信号が仮定部に表される条件である場合に、帰結部に表された結果となることを記述するものである。図4に示すテーブル60は、自然言語により記述されたプロパティの一例を示し、列61にプロパティの種類が、列62にプロパティの内容が、記述されている。このテーブル60は、命題プロパティに対して、逆プロパティ、裏プロパティ又は対偶プロパティがどのようなものかを表す。なお、逆プロパティ、裏プロパティ及び対偶プロパティの定義は、数学の論理学における逆、裏及び対偶と同等のものである。命題プロパティがAならばBであるとすると、逆プロパティは、命題プロパティの仮定部及び帰結部を入れ替えたBならばAであるという形式となる。また、対偶プロパティは、命題プロパティの仮定部及び帰結部を入れ替え、かつ、仮定部及び帰結部それぞれを否定形としたBでなければAでないという形式となる。また、裏プロパティは、命題プロパティの仮定部及び帰結部をそれぞれ否定形としたAでなければBでないという形式となる。本実施形態における形式的論理検証では、このようなプロパティを用いることで、論理の検証を実行する。図5は、本実施形態のプロパティ言語の一例の説明図である。図4に示した例は、自然言語によるプロパティの記述である。一方で、論理検証支援部10において、プロパティはプロパティ言語によって扱われる。すなわち、プロパティは、SVASystemVerilogAssertionやPSLPropertySpecificLanguage等のプロパティ言語によって記述される。なお本実施形態では、SVA言語による記述を説明に用いるが、SVA言語に依存するものではなく、その他のプロパティ言語を用いてもよい。図5に示すテーブル70は、列71にプロパティの種類が、列72に自然言語による表記のプロパティが、列73にプロパティ言語によるプロパティの表記が、それぞれ記述される。このテーブル70において、自然言語における命題プロパティがAならば1サイクル後にBであるとすると、これをプロパティ言語で記述したものは、仮定部であるA==1と、帰結部である1B==1とをインプリケーション演算子|->で結合した表記となる。なお、サイクル遅延演算子、|->インプリケーション演算子は、図6で説明する。また、この命題プロパティの裏プロパティは、仮定部及び帰結部をそれぞれ否定形としたものであり、自然言語ではAでなければ1サイクル後にBでないとなる。また、これをプロパティ言語で記述したものは、プロパティ言語の仮定部及び帰結部にそれぞれ否定を表す演算子を付与した記述となる。論理検証支援部10は、オペレータにより入力されたプロパティ言語に基づいて処理を実行するが、本実施形態では説明の容易のため自然言語による表記もあわせて記載する。図6は、本実施形態のプロパティで使用される演算子、関数の一例の説明図である。プロパティ言語は、信号名と信号値とをインプリケーション演算子、関数、遅延時間等を用いて表したものである。図6に示すテーブル90は、列91にプロパティ言語における記号が、列92に記号の意味が、それぞれ記述される。このテーブル90において、インプリケーション演算子は、|->又は|=>の記号で表され、仮定部と帰結部とを表す演算子である。|->は、~ならば、~となるを表す。また、|=>は、~ならば、1サイクル後に~となるを表す。また、サイクル遅延は、nの形式で表され、nはnサイクル後を表す演算子である。また、関数は、信号の状態の変化を表すものである。例えば、pastは過去を表し、roseは特定の信号の立ち上がりを表す。また、は、否定を表す演算子である。プロパティは、このような演算子及び関数の組み合わせによって、仮定部に表す信号の条件によって、帰結部に信号がどのような結果となるかを表す。論理検証は、このプロパティを用いて、設計回路のRTLの検証を行う。図7は、本実施形態において、命題プロパティに対する逆、裏及び対偶の各プロパティによる検証内容の違いの説明図である。図7に示すテーブル80は、列81にプロパティ言語により行える検証の内容が、列82に命題プロパティが、列83に逆プロパティが、列84に裏プロパティが、列85に対偶プロパティが、それぞれ記述される。このテーブル80は、命題プロパティがA==1|->B==1である場合を例として、逆プロパティ、裏プロパティ及び対偶プロパティの検証内容の違いを説明する。この命題プロパティは、A==1であるとき、Bの値の検証を行うことを表す。しかし、形式的論理検証の性質上、そもそもA==1ではないときには、検証を実行しない。従って、A==0のときの検証は実行できない。また、A==1であればB==1であることは証明できても、B==1のときにAがどのような値であるかということは検証できない。すなわち、AでもBでもない第3の信号による影響を検証できない。そのため、A==1でないときを検証するためには、裏プロパティを生成する必要がある。また、B==1のときを検証するためには逆プロパティを生成する必要がある。このように、一つの命題プロパティによって信号を網羅的に検証することは難しいため、論理検証のために多くのプロパティを作成する必要がある。命題プロパティ、逆プロパティ、裏プロパティ及び対偶プロパティは、それぞれ検証の内容が異なるものである。そのため、従来は、網羅的な検証を実現するために、オペレータが、設計論理の性質に応じてこれらのプロパティを作成していた。これは多くの労力を伴うものであり、また、人手によってプロパティを作成した場合は、そのプロパティが正しいかという検証もさらに必要となるため、時間的、人的なコストが多く発生していた。そこで、本実施形態では、オペレータが作成した命題プロパティに対して、逆、裏及び対偶を意味するプロパティを自動的に作成して、これら各プロパティによって論理検証を実行することによって、形式的論理検証を効率的に行えるように構成した。次に、論理検証支援部10の動作を説明する。図8は、本実施形態の論理検証支援部10が実行する論理検証処理のフローチャートである。論理検証支援部10は、検証者が作成したプロパティを命題として、逆、裏、対偶の意味を有するプロパティを生成し、生成されたプロパティを用いて形式的論理検証を行う機能を有する。論理検証支援部10は、論理検証処理が実行されると、検証対象となる論理とこの論理を検証する検証項目である命題プロパティと、変換指定値との入力を受付けるS201。論理検証支援部10の入力受付部101は、検証対象である論理回路のRTLとオペレータが作成したプロパティと、逆、裏、対偶のいずれのプロパティを生成するのかという情報と、を受付ける。入力受付部101は、複数のプロパティの情報を入力として受付けることができる。これらはメモリ112に一時的に記録される。なお、変換指定値とは、命題となるプロパティ第1のプロパティに対して、逆、裏、対偶のいずれかのプロパティ第2のプロパティに変換を行うか指定する値である。本実施形態では、逆プロパティへの変換を指定する場合は1を、対偶プロパティへの変換を指定する場合は2を、裏プロパティを指定する場合は3を、それぞれ指定する。なお、いずれのプロパティも指定しない場合は、0を指定する。次に、論理検証支援部10は、入力されたプロパティが複数である場合に、全てのプロパティが検証済みであるか否かを判定するS202。全てのプロパティが検証済みであると判定した場合は、論理検証支援部10は、本フローチャートによる処理を終了する。複数のプロパティの少なくとも一つの検証が済んでいないと判定した場合は、論理検証支援部10は、ステップS202に移行して、入力されたプロパティのうち未検証のプロパティを一つ選択し、選択した命題プロパティと、選択したプロパティに対応する変換指定値と、を取得する。次に、論理検証支援部10は、時系列表を作成するS203。論理検証支援部10の表作成部102が、取得したプロパティから信号を時間軸の変化に対応する表に変換する。この処理は図9で後述する。次に、論理検証支援部10は、時系列表を作成したプロパティに対応する変換指定値がいずれであるかを判定するS204。変換指定値が1である場合、すなわち、逆プロパティの生成が指示された場合は、ステップS205に移行する。変換指定値が2である場合、すなわち、対偶プロパティの生成が指示された場合は、ステップS206に移行する。変換指定値が3である場合、すなわち、裏プロパティの生成が指示された場合は、ステップS214に移行する。また、変換指定値が0である場合は、その命題プロパティに対して、いずれのプロパティへの変換も指示されていないことを意味する。この場合は、ステップS205、S206又はステップS214に移行することなく、ステップS220に移行する。ステップS204で逆プロパティの生成が指示された場合は、ステップS205に移行し、論理検証支援部10は、ステップS203で作成された時系列表を、時系列の逆から読み取る。この処理によって逆プロパティを作成するS210。ステップS204で対偶プロパティの生成が指示された場合は、ステップS206に移行し、論理検証支援部10は、ステップS203で作成された時系列表を、時系列の逆から読み取る。この処理によって逆プロパティを作成するS210。次に、論理検証支援部10は、逆プロパティの仮定部及び帰結部それぞれを否定形に変換するS212。この処理によって対偶プロパティを生成するS213。ステップS204で裏プロパティの生成が指示された場合は、ステップS214に移行し、論理検証支援部10は、ステップS202で取得したプロパティについて、仮定部及び帰結部それぞれを否定形に変換する。この処理によって裏プロパティを作成するS215。逆プロパティ、対偶プロパティ又は裏プロパティの作成後、ステップS220に移行し、論理検証支援部10は、形式的論理検証を実行する。その後、ステップS201に戻り、S201以降の処理を繰り返す。この処理は図20で後述する。次に、表作成部102による時系列表の生成を説明する。図9は、本実施形態の論理検証支援部10の表作成部102が実行する時系列表作成処理のフローチャートである。まず、表作成部102は、入力された命題プロパティのインプリケーション演算子とサイクル遅延を表すシーケンス演算子に注目し、それらに区切られる文字列を信号のイベントとみなして抽出するS1。例えば、A==1|->1B==1;A==1ならば1サイクル後にB==1であるというプロパティの場合は、インプリケーション演算子|->とシーケンス演算子1を除く文字列はA==1とB==1であるので、表作成部102は、これらを信号の状態の変化が発生するイベントとみなして抽出する。次に、表作成部102は、ステップS1によって抽出されたイベントと、プロパティに記述されている遅延時間と、を抽出して、イベントと遅延時間との対応を表す遅延時間テーブル120を生成するS2。図10は、本実施形態の表作成部102が作成する遅延時間テーブル120の一例の説明図である。なお、この図10に表す例は、roseready10roserequest|->1cnt==pastcnt,11;readyの立ち上がりから10サイクル後にrequestが立ち上がる場合、requestから1サイクル後のcnt値は1サイクル前のcnt値1となる。という命題プロパティを例に説明する。図10に示す遅延時間テーブル120は、列121にイベントの内容、すなわち、信号名とその値、関数、シーケンス演算子が記述される。列122はそのイベントの遅延時間、すなわち、そのイベントが検証開始時からどれくらいの遅延時間で発生するかのタイミングが記述される。遅延時間テーブル120において、rosereadyという関数は、このイベントの検証開始から0及び1サイクル後に発生する。また、1という演算子は、このイベントの検証開始時から11サイクル後に発生する。このように、表作成部102は、命題プロパティから、イベントとイベントの発生タイミングとを遅延時間として対応させ、遅延時間テーブル120を作成する。図9に戻り、表作成部102は、ステップS2で生成した遅延時間テーブル120の列121に関数が存在するかを検出する。関数が存在する場合は、関数を信号の変化による表記に変換するS3。この関数の変換には、関数変換テーブル130が用いられる。論理検証支援部10は、関数変換テーブル130を予め記憶している。関数変換テーブル130とは、関数と、サイクル遅延及び信号変化とを対応づけた表である。論理検証支援システム11において、関数変換テーブル130は、HDD113又はメモリ112に予め記憶されている。図11は、本実施形態の関数変換テーブル130の一例を示す表である。図11に示す関数変換テーブル130は、列121に関数表記を、列132に関数をサイクル遅延表記としたものが、それぞれ記述されている。関数変換テーブル130において、立ち上がりを表す関数roseAは、A==0と1A==1との組合わせに対応付けられていることが示される。すなわち、関数roseAは、開始時の信号Aの値が0であり、1サイクル後に信号Aの値が1に変化する関数であることが示されている。また、立下りを表すfellAは、A==1と1A==0との組み合わせに対応づけられていることが示される。表作成部102は、この関数変換テーブル130を参照して、命題プロパティに関数変換テーブルに記録されている関数が含まれている場合は、その関数をサイクル遅延の表記に変換する。なお、関数変換テーブル130の内容は図13のような関数に限られるものではない。[n]連続的繰り返しや、[=n]非連続的繰り返しや、[->n]goto繰り返しなどのシーケンス演算子を変換対象としてもよい。図12は、本実施形態の表作成部102によって、関数を変換した後の遅延時間テーブル120を示す説明図である。図12の例は、図10に示す遅延時間テーブルを、図11に示す関数変換テーブルを参照して関数を変換し、新たな表として作成したものである。図10の列121に示されるrosereadyという関数は、図11の関数変換テーブル130に基づいて、ready==0とready==1との二つの表記に変換され、それぞれ遅延時間を当てはめている。同様に、roserequestという関数は、図11の関数変換テーブル130に基づいて、request==0とrequest==1との二つの表記に変換され、それぞれ遅延時間を当てはめている。このような処理によって、表作成部102は、プロパティを、図12に示すような、イベントと遅延時間とを対応する遅延時間テーブル120に変換する。図9に戻り、次に、表作成部102は、ステップS3で作成されたテーブルに基づいて、時系列表20を生成する。表作成部102は、プロパティから図10に示す遅延時間テーブルを作成し、このテーブルの関数を分関して図12に示す遅延時間テーブル120を作成する。表作成部102は、遅延時間テーブル120の遅延時間を時系列として、どのタイミングでどのイベントが発生するか時系列の表として表した時系列表20を作成する。図13は、本実施形態の時系列表20の一例の説明図である。図13は、図12に示すテーブル120から生成された時系列表20の例を示す。テーブル120は、遅延時間が0から12サイクルの間のイベントが示されている。そこで、この0から12の間の時間を時系列とする。時系列表20は、項番21と信号名22とを含む。表作成部102は、時系列順にイベントに含まれる信号名を当てはめる。テーブル120には、ready、request及びcntという信号が含まれているので、それぞれの信号名を、時系列表20の信号が発生する時間に対応して記録する。また、発生するイベント順にそれぞれ項番を付与する。図13の例では、項番21の1がready、項番21の2がrequest、項番21の3がcntにそれぞれ当てはめている。信号readyは、時間0において値が0であり、時間1において値が1である。また、信号requestは、時間10において値が0であり、時間11において値が1である。また、信号cntは、時間11において値が自己参照Xであり、時間12においてこの値に1を加算したものX1である。表作成部102は、それぞれ対応する時間にイベントの結果である値を記録する。また、信号の変化がない部分は空欄としておく。このような処理によって、表作成部102が時系列表20を作成する。図9に戻り、表作成部102は、時系列と信号とからなる時系列表20の作成と平行して、仮定部と帰結部とを決定する処理を実行するS5。仮定部と帰結部とは、インプリケーション演算子を検出することで決定する。表作成部は、プロパティからインプリケーション演算子を挟む右辺と左辺とを検出し、左辺を仮定部に、右辺を帰結部に、それぞれ決定する。前述のプロパティ言語による記述は、インプリケーション演算子を挟んで、左辺はroseready10roserequestであり、これを仮定部とする。また、右辺は1cnt==pastcnt,11であり、これを帰結部とする。左辺は、前述のステップS2及び3の処理により、信号readyと信号requestと、に変換されている。従って、表作成部102は、仮定部の因子はreadyとrequestとであることを検出する。また、右辺は、信号cntのみの記述であるため、表作成部102は、帰結部の因子は信号cntであることを検出する。この検出結果から、表作成部102は、この検出結果から仮定部と帰結部との関係を信号による演算式で表す帰結式を作成するS6。ステップS5により検出された例では、帰結式はcnt=readyrequestとなる、これは、信号cntを検証する場合は、信号readyと信号requestが仮定部であることを表す。表作成部102は、このステップS6によって作成した帰結式を、時系列表20の帰結式の行23に記録するS7。このとき、表作成部102は、記入する際に、信号名に対応する項番で帰結式を表現する。テーブル120において、信号cntは、信号readyと信号requestとの論理積であるので、帰結式は、それぞれの項番21の数字によって3=12と記述される。次に、表作成部102は、時系列表20に逆時間24を記録するS8。逆時間24とは、時系列の最後のイベントが発生する時点を始点とし、検証開始時までの時系列を逆にカウントして記載したものである。この逆時間24は、逆プロパティを生成する処理に用いられる。以上のような処理によって、表作成部102は、命題プロパティから時系列表20を作成する。作成された時系列表20は、メモリ112に記録される。時系列表20は、次に説明する逆プロパティ又は対偶プロパティの生成処理に用いられる。次に、逆プロパティの生成を説明する。プロパティ生成部103は、命題プロパティに基づいて表作成部102から出力された時系列表20を元に、逆、裏、対偶を意味するプロパティを生成する。ここでは、逆プロパティの生成を説明する。図14は、本実施形態の逆プロパティの生成方法を示すフローチャートである。プロパティ生成部103は、まず、時系列表20を参照して、信号名22と、信号値と、逆時間24とを抽出するS11。抽出した信号名22、信号値、逆時間24は、遅延時間テーブル120として作成される。図15は、本実施形態のステップS11で作成されるイベントと遅延時間テーブル120の一例の説明図である。プロパティ生成部103は、時系列表20から取得したイベント及びその値と、そのイベントが発生する時間とを遅延時間テーブル120に記入する。なお、遅延時間の列122は逆時間を抽出しているため、マイナスとなることがあってもよい。次に、プロパティ生成部103は、作成した遅延時間テーブル120に対して、前述した図11に示す関数変換テーブル130を参照して、信号のシーケンスを関数化できるか、すなわち、信号の変化を関数に変換できるかを判断するS12。プロパティ生成部103は、列121の信号の変化パターンと関数変換テーブル130とを照合することによって関数化が可能かを判断する。プロパティ生成部103は、ステップS12で関数化が可能であると判断された信号のシーケンスに対して関数化を行うS13。そして、プロパティ生成部103は、イベントを関数化した後、イベントと遅延時間との対応を表すテーブルを作成するS14。図16は、本実施形態のプロパティ生成部がステップS14で作成する遅延時間テーブル120の一例の説明図である。プロパティ生成部103は、図15に示す遅延時間テーブル120を参照して、イベントを関数化する。具体的には、プロパティ生成部103は、遅延時間が0のときcnt==x1であることと、遅延時間が-1のときcnt==xであることから、関数変換テーブル130を参照して、cnt==pastcnt,11遅延時間0のときのcntは1サイクル前のcntを1インクリメントしたものであると関数化する。同様に、プロパティ生成部103は、遅延時間が-1のときにrequest==1であることと、遅延時間が-2のときにrequest==0であることから、関数変換テーブル130を参照して、pastroserequest,1遅延時間が-1のときにrequestが立ち上がることと関数化する。また、プロパティ生成部103は、遅延時間が-11のときにready==0であることと、遅延時間が-12のときにready==0であることから、関数変換テーブル130を参照して、pastroseready,11遅延時間が-11のときにreadyが立ち上がることと関数化する。これら関数化されたイベントは、前述した図11と同じ形式の遅延時間テーブル120図16に記録する。一方で、逆プロパティは命題プロパティに対して、仮定部と帰結部とを反転させたものであるため、時系列表20の帰結式23から得られる仮定部と帰結部との信号関係を反転させることで、逆プロパティを生成できる。このことを利用して、プロパティ生成部103は、帰結式23の仮定部と帰結部との信号関係を反転する処理を行うS15。図13に示す時系列表20を参照すると、帰結式は3=12であり、これは信号cntの値を検証する場合には、信号readyと信号requestとが仮定となることを表している。プロパティ生成部103は、この仮定部と帰結部とを反転して、帰結式12=3を得る。これは、信号readyと信号requestとの値を検証する場合に信号cntが仮定となるということを表している。次に、プロパティ生成部103は、ステップS14で作成したテーブルと、ステップS15で得られる帰結式とを組み合わせることによって逆プロパティを生成するS16。具体的には、テーブルに記載された各イベントとその遅延時間とを帰結式に当てはめ、これを逆プロパティとして記録する。このステップS16の処理によって、逆プロパティの生成が完了する。図17は、本実施形態のプロパティ生成部103によって実行される逆プロパティの生成の説明図である。図17Aは、命題プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。表作成部102は、このプロパティ言語を解析し、前述した図9の処理によって時系列表20を作成する。図17Bは、図17Aのプロパティ言語に対応する時系列表20の一例である。プロパティ生成部103は、この時系列表20と命題プロパティのプロパティ言語とを参照して、前述の図14の処理によって逆プロパティを生成する。図17Cは、図17Aに示す命題プロパティに対して生成された逆プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。次に、裏プロパティの生成を説明する。プロパティ生成部103は、前述のように命題プロパティに基づいて表作成部102から出力された時系列表20を元に、逆プロパティを生成する。一方、裏プロパティは、否定を表すを命題プロパティのプロパティ言語に付加することによって生成する。図18は、本実施形態のプロパティ生成部103が実行する裏プロパティの生成の説明図である。図18Aは、命題プロパティを、自然言語とそれに対応するプロパティ言語で記述したものである。このプロパティ記述から裏プロパティを作成する場合は、プロパティ生成部103は、インプリケーション演算子によって仮定部と帰結部とを検出する。なお、既に作成されている時系列表20を参照して仮定部と帰結部とを検出してもよい。次に、プロパティ生成部103は、仮定部と帰結部とに記載されている各イベントに、否定を表すを付加する。図18Bは、図18Aに示す命題プロパティに対して生成された裏プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。なお、否定の意味とは、該当イベントの動作以外の動作の指示である。例えば、rosereadyreadyが立ち上がることの否定形は、rosereadyreadyが立ち上がらないこととなる。具体的には、readyの値が0を維持している状態と、1を維持している状態と、1から0に立ち下がる状態と、を意味することとなる。同様に、cnt==pastcnt,11cnt値は1サイクル前のcnt値1であることの否定形は、cnt==pastcnt,11cnt値は1サイクル前のcnt値1ではないこととなる。これは、cntの値が1サイクル前のcntの値1以外の値であれば全て条件を満たすことになる。次に、対偶プロパティの生成を説明する。対偶プロパティは、命題プロパティに対して仮定部と帰結部とを反転させ、さらに、全てのイベントに対して否定形を表すを付加することによって生成する。つまり、前述のように命題プロパティに基づいて表作成部102から出力された時系列表20を元に、逆プロパティを生成し、この逆プロパティを裏プロパティに変換することによって、対偶プロパティを生成する。図19は、本実施形態のプロパティ生成部103が実行する対偶プロパティの生成の説明図である。逆プロパティは、前述のように図9、図14で示される処理によって生成される。また、裏プロパティは図18に示すように、各イベントに対して否定形を表すを付加することで生成する。図19Aは、命題プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。表作成部102は、このプロパティ言語を解析し、前述した図9の処理によって時系列表20を作成する。図19Bは、図19Aのプロパティ言語に対応する時系列表20の一例である。プロパティ生成部103は、この時系列表20と命題プロパティのプロパティ言語とを参照して、前述の図14の処理によって逆プロパティを生成する。図19Cは、図19Aに示す命題プロパティに対して生成された逆プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。さらに、生成された逆プロパティに対して、図18において説明したように、プロパティ生成部103は、仮定部と帰結部とに記載されている各イベントに、否定を表すを付加する。図19Dは、図19Aに示す命題プロパティに対して生成された対偶プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。以上説明したような処理によって、論理検証支援部10が、命題プロパティから逆、裏及び対偶を意味するプロパティを自動的に生成することができる。次に、形式的論理検証について説明する。検証部104は、オペレータが入力した命題プロパティ、又は、プロパティ生成部103が生成した逆プロパティ、裏プロパティ、対偶プロパティを入力し、形式的論理検証を行う機能である。図20は、本実施形態の検証部104が実行する形式的論理検証の説明図である。形式的論理検証は、検証対象のネットリストから抽出されるロジックコーンと、検査対象の期待値から抽出されるロジックコーンとを比較し、これらの等価性を検証することによって、論理回路の正当性を数学的に証明する手法である。ロジックコーンとは、論理を、FFFlipFlopを頂点とする組合せ回路網とする等価回路に置き換えたものである。検証部104は、論理回路のRTLを検査対象のネットリストとして、ロジックコーンを抽出する。また同様に、プロパティに基づく検査対象の期待値からロジックコーンを抽出する。そして、検証部104は、これら検証対象のロジックコーンと期待値であるロジックコーンとを比較し、これらの等価性を検証する。等価性の検証方法としては、従来周知であるOBDDOrderedBinaryDecisionDiagram等の手法を用いることができる。なお、形式的論理検証を行う手法は、これに限定されない。図20に示す例では、検証部104は、論理回路のFF30とFF30-1とFF30-2との組合せであるロジックコーン31と、生成されたプロパティに基づいて、期待値を表すFF30-3とFF30-4とFF30-5との組合せであるロジックコーン31-1との比較を検証する例を示す。図21は、本実施形態の検証部104が実行する形式的論理検証のフローチャートである。形式的論理検証が開始されると、まず、検証部104は、入力部118から検証対象である論理のRTLと、命題プロパティ又はプロパティ生成部103により生成された逆、裏、対偶プロパティとの入力を受付けるS101。次に、検証部104は、プロパティから期待値であるロジックコーンを抽出する処理と論理回路のRTLのロジックコーンを抽出する処理を実行するS102。次に、検証部104は、ステップ102で抽出した期待値のロジックコーンと、設計回路のロジックコーンとの等価性を比較するS103。そして、比較の結果、ロジックコーンが等価であるか否かを判定するS104。比較の結果、ロジックコーンが等価であると認めた場合は、ステップS105に移行し、検証部104は、設計された論理回路は期待通りの動作をしていることを確認する。この結果を検証結果出力部105に出力する。一方、結果が等価でないと認めた場合は、設計された論理、又は、プロパティ自体に誤りがあることを意味する。この場合は、検証部104は、検証結果出力部105からエラーを通知する。このとき、ロジックコーンから期待値と整合性が取れない組合せの波形反例となる波形を生成することによって、デバック情報を検証結果出力部105を通じて提示することができる。このような処理によって形式的論理検証が完了する。以上のように本発明の実施形態では、論理検証支援部10が、設計回路の論理と、論理を検証する検証項目である第1のプロパティである命題プロパティと、を取得する入力受付部101と、命題プロパティで発生する事象イベントを時系列に並べた時系列表20を作成する表作成部102と、命題プロパティと時系列表20とに基づいて、命題プロパティの逆、裏又は対偶を意味する第2のプロパティを作成するプロパティ生成部103と、命題プロパティ、逆プロパティ、裏プロパティ又は対偶プロパティを用いて論理を検証する検証部104と、検証部104の検証結果を出力する検証結果出力部105と、を備える。このような構成により、オペレータが準備した命題プロパティから、逆、裏又は対偶を意味する第2のプロパティを作成することができる。これにより、複数のプロパティが自動的に生成でき、プロパティを網羅的に生成することができるので、論理検証の検証品質を向上させることができる。さらに、論理検証における時間的、人的なコストを削減して、効率的に論理検証を行うことができる。次に、本発明の第2の実施形態を説明する。第2の実施形態の論理検証支援部10は、命題プロパティから逆、裏、対偶を表すプロパティを生成して、これを検証する機能だけではなく、命題プロパティを視覚的に確認できる機能を有する。図22は、本実施形態の論理検証支援部10のブロック図である。なお、第1の実施形態と同一の構成は同一の符号を付し、その説明は省略する。論理検証支援部10は、図1で前述したように、入力受付部101、表作成部102、プロパティ生成部103、検証部104及び検証結果出力部105を備える。論理検証支援部10は、表出力部201を備える。表出力部201は、表作成部102により生成された時系列表20を表示部117に表示する機能を有する。表出力部201から出力される時系列表20は、図2に例示した時系列表20である。時系列表20は、プロパティに宣言されない信号及びその値は表示しないため、オペレータが視覚的にプロパティの整合性を判断しやすい。そのため、表出力部201によって時系列表20を表示することによって、オペレータは、意図したプロパティが生成されているかどうかをデバックするための手法として用いることができる。次に、本発明の第3の実施形態を説明する。第3の実施形態の論理検証支援部10は、前述した第2の実施形態のように命題プロパティを視覚的に確認できる機能に加え、生成された逆、裏、対偶プロパティの時系列表20をも表示する機能を有する。図23は、本実施形態の論理検証支援部10のブロック図である。なお、第1及び第2の実施形態と同一の構成は同一の符号を付し、その説明は省略する。論理検証支援部10は、表出力部201と表作成部202とを備える。表出力部201は、表作成部102により生成された時系列表20を表示部117に表示する機能を有する。表作成部202は、プロパティ生成部103により生成された逆、裏、対偶プロパティの時系列表20を作成する機能を有する。第2の実施形態と同様に、表出力部201は、命題プロパティを元に作成した時系列表20を表示する。さらに、表出力部201は、表作成部202により作成された、逆、裏、対偶プロパティの時系列表20を表示する。このようにすることで、オペレータは、論理検証支援部10によって自動的に作成された逆、裏、対偶プロパティの時系列表20を、視覚的に確認することができる。そのため、オペレータ間でプロパティの共有が容易になる。また、表出力部201で出力される時系列表20を生成されたプロパティと共に外部データベースに登録するようにしてもいい。これにより、時系列表20の等価性を比較して、異なるプロパティ言語表記だが検証内容は等しいプロパティを摘出するといったプロパティの検証作業を行うことができる。"