JP5568779B2 - 論理検証方法及び論理検証システム - Google Patents

Description

本発明は、論理設計における論理の検証方法及び論理検証システムに関する。

論理回路の大規模化と多機能化に対処するために、検証の効率改善も重要な課題である。論理検証の方法の一つに、形式的論理検証が知られている。

形式的論理検証とは、論理回路に期待される動作や禁止される動作をプロパティとして定義し、検証対象の論理回路がプロパティに違反する動作を起こさないように設計されているかどうかを検査するものである。

プロパティとは、入力パタンとそれに伴う出力の期待値の動作を定義するものである。具体的には、「ある信号が入力された後、３サイクル以内に信号を出力する」、「２つの信号は決して同時に‘１’とならない」といったものである。

プロパティの検出機能を有した形式的論理検証の方法として、動作合成ツールが、動作レベル回路記述からＲＴＬ（Ｒｅｇｉｓｔｅｒ Ｔｒａｎｓｆｅｒ Ｌｅｖｅｌ）回路記述を合成する。また、プロパティ生成部が、動作レベル回路記述から動作レベルプロパティを生成する。続いて、プロパティ変換部が、生成された動作レベルプロパティをＲＴＬプロパティに変換する。そして、モデル検査部が、ＲＴＬ回路記述をＲＴＬプロパティを用いて、モデル検査技法により検証するプロパティ生成システムが知られている（特許文献１参照）。

特開２００９−２３０６７７

前述の従来技術は、動作合成ツールを使用する設計において、Ｃ言語などの抽象度の高い記述からプロパティを抽出し、抽出したプロパティをＲＴＬのプロパティに変換するものである。

しかし、従来技術は、論理の記述形式からプロパティを抽出することは可能であるが、抽出したプロパティだけでは全ての検証項目を満足させることはできず、検証回路に対して網羅的な検証をするためは不十分である。そのため、プロパティを網羅的に生成する必要があるが、これには時間的、人的なコストが多く発生する。

本発明はこのような問題点に鑑みてなされたものであり、論理検証における検査項目であるプロパティを効率的に生成できる論理検証方法及び論理検証装置を提供することを特徴とする。

本発明の一実施態様によれば、論理と、論理を検証する検証項目である第１のプロパティと、を取得する第１の手順と、第１のプロパティで発生する事象を時系列に並べた時系列表を作成する第２の手順と、第１のプロパティと時系列表とに基づいて、検証項目の逆、裏又は対偶を意味する第２のプロパティを作成する第３の手順と、第１のプロパティ及び作成された第２のプロパティを用いて、論理を検証する第４の手順と、を備える。

本発明によれば、検証者が作成する第１のプロパティを元にして、逆、裏、対偶を意味する第２のプロパティを作成するので、複数のプロパティを網羅的に生成することにより、論理検証の検証品質を向上させることができる。さらに、論理検証における時間的、人的なコストを削減することができる。

本発明の第１の実施形態の論理検証支援部のブロック図である。 本発明の第１の実施形態における論理デバイス設計のフローチャートである。 本発明の第１の実施形態の論理検証支援システムのハードウェア構成を示すブロック図である。 本発明の第１の実施形態のプロパティの一例の説明図である。 本発明の第１の実施形態のプロパティ言語の一例の説明図である。 本発明の第１の実施形態のプロパティで使用される演算子、関数の一例の説明図である。 本発明の第１の実施形態において、命題プロパティに対する逆、裏及び対偶の各プロパティによる検証内容の違いの説明図である。 本発明の第１の実施形態の論理検証処理のフローチャートである。 本発明の第１の実施形態の時系列表作成処理のフローチャートである。 本発明の第１の実施形態の遅延時間テーブルの一例の説明図である。 本発明の第１の実施形態の関数変換テーブルの一例を示す表である。 本発明の第１の実施形態の関数を変換した後の遅延時間テーブルを示す説明図である。 本発明の第１の実施形態の時系列表の一例の説明図である。 本発明の第１の実施形態の逆プロパティの生成方法を示すフローチャートである。 本発明の第１の実施形態の遅延時間テーブルの一例の説明図である。 本発明の第１の実施形態の遅延時間テーブルの一例の説明図である。 本発明の第１の実施形態の逆プロパティの生成の説明図である。 本発明の第１の実施形態の裏プロパティの生成の説明図である。 本発明の第１の実施形態の対偶プロパティの生成の説明図である。 本発明の第１の実施形態の形式的論理検証の説明図である。 本発明の第１の実施形態の形式的論理検証のフローチャートである。 本発明の第２の実施形態の論理検証支援部のブロック図である。 本発明の第３の実施形態の論理検証支援部のブロック図である。

以下、本発明の第１の実施の形態を、図面を参照して説明する。

図１は、本実施形態の論理検証支援部１０のブロック図である。

本実施形態の論理検証支援部１０は、オペレータが設計した論理デバイスの論理回路を、プロパティを用いて形式的論理検証を行う装置である。

形式的論理検証とは、論理回路に期待される動作や、禁止される動作をプロパティとして定義し、検証対象の論理回路がプロパティに違反する動作を起こさないように設計されているかどうかを検査するものである。

論理検証支援部１０は、入力受付部１０１、表作成部１０２、プロパティ生成部１０３、検証部１０４及び検証結果出力部１０５を備える。

入力受付部１０１は、オペレータからプロパティ等のデータや指令の入力を受付ける。表作成部１０２は、入力されたプロパティから後述する時系列表を作成する。

プロパティ生成部１０３は、オペレータが入力したプロパティを命題として逆、裏、対偶の意味を持つプロパティを生成する。

検証部１０４は、プロパティを検証する。検証結果出力部１０５は、プロパティの検証結果を出力する。

図２は、本実施形態における形式的論理検証が適用される論理デバイス設計のフローチャートである。

論理デバイス設計において、オペレータは、論理デバイスの方式を検討する方式検討（Ｓ３００）を実行し、方式を実現させるための機能を検討する機能検討（Ｓ３０１）を実行し、機能を実現するために論理を記述する論理設計（Ｓ３０２）を実行する。論理設計では、ＲＴＬ（Ｒｅｇｉｓｔｅｒ Ｔｒａｎｓｆｅｒ Ｌｅｖｅｌ；レジスタ転送レベル）によって記述された論理が作成される。

次に、オペレータは、作成されたＲＴＬを形式的論理検証するために、論理検証（Ｓ３０３）を実行する。このステップＳ３０３では、論理検証支援部１０において、後述するプロパティを用いた形式的論理検証を実行する。

論理検証が終了し、ＲＴＬの正当性が確認された後、ＲＴＬをゲートレベルに合成する論理合成（Ｓ３０４）を実行し、作成されたゲートを実際のデバイスに配置する実装（Ｓ３０５）を実行する。

このような手順により、論理デバイスの設計が行われる。

図３は、本実施形態の論理検証支援部１０を実現する論理検証支援システム１１のハードウェア構成を示すブロック図である。

論理検証支援システム１１は、ＣＰＵ１１１、メモリ１１２、ＨＤＤ１１３、入出力インタフェース１１４、表示部１１７及び入力部１１８を備える。ＣＰＵ１１１、メモリ１１２、ＨＤＤ１１３及び入出力インタフェース１１４は、バス１１５よって相互に接続される。

ＣＰＵ１１１は、論理検証支援システム１１の制御を司る制御部である。ＣＰＵ１１１は、ＨＤＤ１１３に格納される論理検証支援プログラム１１６を、メモリ１１２上に読み出し、これを実行する。ＣＰＵ１１１が論理検証支援プログラム１１６を実行することによって、論理検証支援部１０が実行される。

メモリ１１２は、例えばＤＲＡＭにより構成される。メモリ１１２は、論理検証支援プログラム１１６や、論理検証支援プログラム１１６が実行するために用いるデータやテーブル等を一時的に記録する。

ＨＤＤ１１３は、例えば磁気ディスクドライブにより構成される。ＨＤＤ１１３は、論理検証支援システム１１によって実行されるプログラム、データ等を記録する。例えば、論理検証の対象の論理回路のＲＴＬや、演算子、関数等のサイクル遅延を表す関数変換テーブル１３０等は、オペレータにより予め記憶される。これらメモリ１１２およびＨＤＤ１１３によって記憶部が構成される。

入出力インタフェース１１４は、論理検証支援部１０の動作に関わる情報を表示部１１７に表示する。また、入出力インタフェース１１４は、オペレータ等により入力部１１８に入力される情報を論理検証支援部１０に伝達する。

なお、表示部１１７及び入力部１１８は、ネットワーク等を経由して他のコンピュータやストレージ等にデータを送受信できるように構成されていてもよい。論理検証支援システム１１が、他のコンピュータからデータを入力したり、他のコンピュータに結果を表示するように構成されていてもよい。

次に、論理検証支援部１０が実行する形式的論理検証について説明する。

形式的論理検証は、図２のステップＳ３０２において作成した論理のＲＴＬに対して、プロパティと呼ばれる検証項目を作成し、この検証項目を用いてＲＴＬの論理を検証する。この結果、ＲＴＬの論理の正当性、等価性等が検証される。

図４は、本実施形態のプロパティの一例の説明図である。

プロパティとは、ある信号が仮定部に表される条件である場合に、帰結部に表された結果となることを記述するものである。

図４に示すテーブル６０は、自然言語により記述されたプロパティの一例を示し、列６１にプロパティの種類が、列６２にプロパティの内容が、記述されている。

このテーブル６０は、命題プロパティに対して、逆プロパティ、裏プロパティ又は対偶プロパティがどのようなものかを表す。なお、逆プロパティ、裏プロパティ及び対偶プロパティの定義は、数学の論理学における逆、裏及び対偶と同等のものである。

命題プロパティが「ＡならばＢである」とすると、逆プロパティは、命題プロパティの仮定部及び帰結部を入れ替えた「ＢならばＡである」という形式となる。

また、対偶プロパティは、命題プロパティの仮定部及び帰結部を入れ替え、かつ、仮定部及び帰結部それぞれを否定形とした「ＢでなければＡでない」という形式となる。

また、裏プロパティは、命題プロパティの仮定部及び帰結部をそれぞれ否定形とした「ＡでなければＢでない」という形式となる。

本実施形態における形式的論理検証では、このようなプロパティを用いることで、論理の検証を実行する。

図５は、本実施形態のプロパティ言語の一例の説明図である。

図４に示した例は、自然言語によるプロパティの記述である。一方で、論理検証支援部１０において、プロパティはプロパティ言語によって扱われる。

すなわち、プロパティは、ＳＶＡ（Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎ）やＰＳＬ（Ｐｒｏｐｅｒｔｙ Ｓｐｅｃｉｆｉｃ Ｌａｎｇｕａｇｅ）等のプロパティ言語によって記述される。なお本実施形態では、ＳＶＡ言語による記述を説明に用いるが、ＳＶＡ言語に依存するものではなく、その他のプロパティ言語を用いてもよい。

図５に示すテーブル７０は、列７１にプロパティの種類が、列７２に自然言語による表記のプロパティが、列７３にプロパティ言語によるプロパティの表記が、それぞれ記述される。

このテーブル７０において、自然言語における命題プロパティが「Ａならば１サイクル後にＢである」とすると、これをプロパティ言語で記述したものは、仮定部である「（Ａ＝＝１）」と、帰結部である「＃＃１ （Ｂ＝＝１）」とをインプリケーション演算子「｜−＞」で結合した表記となる。なお、「＃＃」（サイクル遅延演算子）、「｜−＞」（インプリケーション演算子）は、図６で説明する。

また、この命題プロパティの裏プロパティは、仮定部及び帰結部をそれぞれ否定形としたものであり、自然言語では「Ａでなければ１サイクル後にＢでない」となる。また、これをプロパティ言語で記述したものは、プロパティ言語の仮定部及び帰結部にそれぞれ否定を表す演算子「！」を付与した記述となる。

論理検証支援部１０は、オペレータにより入力されたプロパティ言語に基づいて処理を実行するが、本実施形態では説明の容易のため自然言語による表記もあわせて記載する。

図６は、本実施形態のプロパティで使用される演算子、関数の一例の説明図である。

プロパティ言語は、信号名と信号値とをインプリケーション演算子、関数、遅延時間等を用いて表したものである。

図６に示すテーブル９０は、列９１にプロパティ言語における記号が、列９２に記号の意味が、それぞれ記述される。

このテーブル９０において、インプリケーション演算子は、「｜−＞」又は「｜＝＞」の記号で表され、仮定部と帰結部とを表す演算子である。「｜−＞」は、「〜ならば、〜となる」を表す。また、「｜＝＞」は、「〜ならば、１サイクル後に〜となる」を表す。

また、サイクル遅延は、「＃＃ｎ」の形式で表され、「＃＃ｎ」は「ｎサイクル後」を表す演算子である。

また、関数は、信号の状態の変化を表すものである。例えば、「＄ｐａｓｔ」は過去を表し、「＄ｒｏｓｅ」は特定の信号の立ち上がりを表す。

また、「！」は、否定を表す演算子である。

プロパティは、このような演算子及び関数の組み合わせによって、仮定部に表す信号の条件によって、帰結部に信号がどのような結果となるかを表す。

論理検証は、このプロパティを用いて、設計回路のＲＴＬの検証を行う。

図７は、本実施形態において、命題プロパティに対する逆、裏及び対偶の各プロパティによる検証内容の違いの説明図である。

図７に示すテーブル８０は、列８１にプロパティ言語により行える検証の内容が、列８２に命題プロパティが、列８３に逆プロパティが、列８４に裏プロパティが、列８５に対偶プロパティが、それぞれ記述される。

このテーブル８０は、命題プロパティが「Ａ＝＝'１' ｜−＞ Ｂ＝＝'１'」である場合を例として、逆プロパティ、裏プロパティ及び対偶プロパティの検証内容の違いを説明する。

この命題プロパティは、「Ａ＝＝１」であるとき、Ｂの値の検証を行うことを表す。

しかし、形式的論理検証の性質上、そもそも「Ａ＝＝１」ではないときには、検証を実行しない。従って、「Ａ＝＝０」のときの検証は実行できない。

また、「Ａ＝＝１であればＢ＝＝１である」ことは証明できても、「Ｂ＝＝１のときにＡがどのような値であるか」ということは検証できない。すなわち、ＡでもＢでもない第３の信号による影響を検証できない。

そのため、「Ａ＝＝１でない」ときを検証するためには、裏プロパティを生成する必要がある。また、「Ｂ＝＝１」のときを検証するためには逆プロパティを生成する必要がある。

このように、一つの命題プロパティによって信号を網羅的に検証することは難しいため、論理検証のために多くのプロパティを作成する必要がある。

命題プロパティ、逆プロパティ、裏プロパティ及び対偶プロパティは、それぞれ検証の内容が異なるものである。そのため、従来は、網羅的な検証を実現するために、オペレータが、設計論理の性質に応じてこれらのプロパティを作成していた。これは多くの労力を伴うものであり、また、人手によってプロパティを作成した場合は、そのプロパティが正しいかという検証もさらに必要となるため、時間的、人的なコストが多く発生していた。

そこで、本実施形態では、オペレータが作成した命題プロパティに対して、逆、裏及び対偶を意味するプロパティを自動的に作成して、これら各プロパティによって論理検証を実行することによって、形式的論理検証を効率的に行えるように構成した。

次に、論理検証支援部１０の動作を説明する。

図８は、本実施形態の論理検証支援部１０が実行する論理検証処理のフローチャートである。

論理検証支援部１０は、検証者が作成したプロパティを命題として、逆、裏、対偶の意味を有するプロパティを生成し、生成されたプロパティを用いて形式的論理検証を行う機能を有する。

論理検証支援部１０は、論理検証処理が実行されると、検証対象となる論理とこの論理を検証する検証項目である命題プロパティと、変換指定値との入力を受付ける（Ｓ２０１）。

論理検証支援部１０の入力受付部１０１は、検証対象である論理回路のＲＴＬとオペレータが作成したプロパティと、逆、裏、対偶のいずれのプロパティを生成するのかという情報と、を受付ける。入力受付部１０１は、複数のプロパティの情報を入力として受付けることができる。これらはメモリ１１２に一時的に記録される。

なお、変換指定値とは、命題となるプロパティ（第１のプロパティ）に対して、逆、裏、対偶のいずれかのプロパティ（第２のプロパティ）に変換を行うか指定する値である。本実施形態では、逆プロパティへの変換を指定する場合は１を、対偶プロパティへの変換を指定する場合は２を、裏プロパティを指定する場合は３を、それぞれ指定する。なお、いずれのプロパティも指定しない場合は、０を指定する。

次に、論理検証支援部１０は、入力されたプロパティが複数である場合に、全てのプロパティが検証済みであるか否かを判定する（Ｓ２０２）。全てのプロパティが検証済みであると判定した場合は、論理検証支援部１０は、本フローチャートによる処理を終了する。

複数のプロパティの少なくとも一つの検証が済んでいないと判定した場合は、論理検証支援部１０は、ステップＳ２０２に移行して、入力されたプロパティのうち未検証のプロパティを一つ選択し、選択した命題プロパティと、選択したプロパティに対応する変換指定値と、を取得する。

次に、論理検証支援部１０は、時系列表を作成する（Ｓ２０３）。論理検証支援部１０の表作成部１０２が、取得したプロパティから信号を時間軸の変化に対応する表に変換する。この処理は図９で後述する。

次に、論理検証支援部１０は、時系列表を作成したプロパティに対応する変換指定値がいずれであるかを判定する（Ｓ２０４）。

変換指定値が１である場合、すなわち、逆プロパティの生成が指示された場合は、ステップＳ２０５に移行する。

変換指定値が２である場合、すなわち、対偶プロパティの生成が指示された場合は、ステップＳ２０６に移行する。

変換指定値が３である場合、すなわち、裏プロパティの生成が指示された場合は、ステップＳ２１４に移行する。

また、変換指定値が０である場合は、その命題プロパティに対して、いずれのプロパティへの変換も指示されていないことを意味する。この場合は、ステップＳ２０５、Ｓ２０６又はステップＳ２１４に移行することなく、ステップＳ２２０に移行する。

ステップＳ２０４で逆プロパティの生成が指示された場合は、ステップＳ２０５に移行し、論理検証支援部１０は、ステップＳ２０３で作成された時系列表を、時系列の逆から読み取る。この処理によって逆プロパティを作成する（Ｓ２１０）。

ステップＳ２０４で対偶プロパティの生成が指示された場合は、ステップＳ２０６に移行し、論理検証支援部１０は、ステップＳ２０３で作成された時系列表を、時系列の逆から読み取る。この処理によって逆プロパティを作成する（Ｓ２１０）。次に、論理検証支援部１０は、逆プロパティの仮定部及び帰結部それぞれを否定形に変換する（Ｓ２１２）。この処理によって対偶プロパティを生成する（Ｓ２１３）。

ステップＳ２０４で裏プロパティの生成が指示された場合は、ステップＳ２１４に移行し、論理検証支援部１０は、ステップＳ２０２で取得したプロパティについて、仮定部及び帰結部それぞれを否定形に変換する。この処理によって裏プロパティを作成する（Ｓ２１５）。

逆プロパティ、対偶プロパティ又は裏プロパティの作成後、ステップＳ２２０に移行し、論理検証支援部１０は、形式的論理検証を実行する。その後、ステップＳ２０１に戻り、Ｓ２０１以降の処理を繰り返す。この処理は図２０で後述する。

次に、表作成部１０２による時系列表の生成を説明する。

図９は、本実施形態の論理検証支援部１０の表作成部１０２が実行する時系列表作成処理のフローチャートである。

まず、表作成部１０２は、入力された命題プロパティのインプリケーション演算子とサイクル遅延を表すシーケンス演算子に注目し、それらに区切られる文字列を信号のイベントとみなして抽出する（Ｓ１）。

例えば、
（Ａ＝＝１）｜−＞ ＃＃１ （Ｂ＝＝１）；（Ａ＝＝'１'ならば１サイクル後にＢ＝＝'１'である）
というプロパティの場合は、インプリケーション演算子「｜−＞」とシーケンス演算子「＃＃１」を除く文字列は「Ａ＝＝１」と「Ｂ＝＝１」であるので、表作成部１０２は、これらを信号の状態の変化が発生するイベントとみなして抽出する。

次に、表作成部１０２は、ステップＳ１によって抽出されたイベントと、プロパティに記述されている遅延時間と、を抽出して、イベントと遅延時間との対応を表す遅延時間テーブル１２０を生成する（Ｓ２）。

図１０は、本実施形態の表作成部１０２が作成する遅延時間テーブル１２０の一例の説明図である。

なお、この図１０に表す例は、
＄ｒｏｓｅ（ｒｅａｄｙ） ＃＃１０ ＄ｒｏｓｅ（ｒｅｑｕｅｓｔ） ｜−＞ ＃＃１ ｃｎｔ＝＝＄ｐａｓｔ（ｃｎｔ，１）＋１；（ｒｅａｄｙの立ち上がりから１０サイクル後にｒｅｑｕｅｓｔが立ち上がる場合、ｒｅｑｕｅｓｔから１サイクル後のｃｎｔ値は１サイクル前のｃｎｔ値＋１となる。）
という命題プロパティを例に説明する。

図１０に示す遅延時間テーブル１２０は、列１２１にイベントの内容、すなわち、信号名とその値、関数、シーケンス演算子が記述される。列１２２はそのイベントの遅延時間、すなわち、そのイベントが検証開始時からどれくらいの遅延時間で発生するかのタイミングが記述される。

遅延時間テーブル１２０において、「＄ｒｏｓｅ（ｒｅａｄｙ）」という関数は、このイベントの検証開始から０及び１サイクル後に発生する。また、「＃＃１」という演算子は、このイベントの検証開始時から１１サイクル後に発生する。

このように、表作成部１０２は、命題プロパティから、イベントとイベントの発生タイミングとを遅延時間として対応させ、遅延時間テーブル１２０を作成する。

図９に戻り、表作成部１０２は、ステップＳ２で生成した遅延時間テーブル１２０の列１２１に関数が存在するかを検出する。関数が存在する場合は、関数を信号の変化による表記に変換する（Ｓ３）。この関数の変換には、関数変換テーブル１３０が用いられる。

論理検証支援部１０は、関数変換テーブル１３０を予め記憶している。関数変換テーブル１３０とは、関数と、サイクル遅延及び信号変化とを対応づけた表である。論理検証支援システム１１において、関数変換テーブル１３０は、ＨＤＤ１１３又はメモリ１１２に予め記憶されている。

図１１は、本実施形態の関数変換テーブル１３０の一例を示す表である。

図１１に示す関数変換テーブル１３０は、列１２１に関数表記を、列１３２に関数をサイクル遅延表記としたものが、それぞれ記述されている。

関数変換テーブル１３０において、立ち上がりを表す関数「＄ｒｏｓｅ（Ａ）」は、「Ａ＝＝０」と「＃＃１ Ａ＝＝１」との組合わせに対応付けられていることが示される。すなわち、関数「＄ｒｏｓｅ（Ａ）」は、開始時の信号Ａの値が０であり、１サイクル後に信号Ａの値が１に変化する関数であることが示されている。

また、立下りを表す「＄ｆｅｌｌ（Ａ）」は、「Ａ＝＝１」と「＃＃１ Ａ＝＝０」との組み合わせに対応づけられていることが示される。

表作成部１０２は、この関数変換テーブル１３０を参照して、命題プロパティに関数変換テーブルに記録されている関数が含まれている場合は、その関数をサイクル遅延の表記に変換する。

なお、関数変換テーブル１３０の内容は図１３のような関数に限られるものではない。［＊ｎ］（連続的繰り返し）や、［＝ｎ］（非連続的繰り返し）や、［−＞ｎ］（ｇｏｔｏ繰り返し）などのシーケンス演算子を変換対象としてもよい。

図１２は、本実施形態の表作成部１０２によって、関数を変換した後の遅延時間テーブル１２０を示す説明図である。

図１２の例は、図１０に示す遅延時間テーブルを、図１１に示す関数変換テーブルを参照して関数を変換し、新たな表として作成したものである。

図１０の列１２１に示される「＄ｒｏｓｅ（ｒｅａｄｙ）」という関数は、図１１の関数変換テーブル１３０に基づいて、「ｒｅａｄｙ＝＝０」と「ｒｅａｄｙ＝＝１」との二つの表記に変換され、それぞれ遅延時間を当てはめている。

同様に、「＄ｒｏｓｅ（ｒｅｑｕｅｓｔ）」という関数は、図１１の関数変換テーブル１３０に基づいて、「ｒｅｑｕｅｓｔ＝＝０」と「ｒｅｑｕｅｓｔ＝＝１」との二つの表記に変換され、それぞれ遅延時間を当てはめている。

このような処理によって、表作成部１０２は、プロパティを、図１２に示すような、イベントと遅延時間とを対応する遅延時間テーブル１２０に変換する。

図９に戻り、次に、表作成部１０２は、ステップＳ３で作成されたテーブルに基づいて、時系列表２０を生成する。

表作成部１０２は、プロパティから図１０に示す遅延時間テーブルを作成し、このテーブルの関数を分関して図１２に示す遅延時間テーブル１２０を作成する。表作成部１０２は、遅延時間テーブル１２０の遅延時間を時系列として、どのタイミングでどのイベントが発生するか時系列の表として表した時系列表２０を作成する。

図１３は、本実施形態の時系列表２０の一例の説明図である。

図１３は、図１２に示すテーブル１２０から生成された時系列表２０の例を示す。

テーブル１２０は、遅延時間が０から１２サイクルの間のイベントが示されている。そこで、この０から１２の間の時間を時系列とする。

時系列表２０は、項番２１と信号名２２とを含む。

表作成部１０２は、時系列順にイベントに含まれる信号名を当てはめる。テーブル１２０には、「ｒｅａｄｙ」、「ｒｅｑｕｅｓｔ」及び「ｃｎｔ」という信号が含まれているので、それぞれの信号名を、時系列表２０の信号が発生する時間に対応して記録する。また、発生するイベント順にそれぞれ項番を付与する。

図１３の例では、項番２１の「１」が「ｒｅａｄｙ」、項番２１の「２」が「ｒｅｑｕｅｓｔ」、項番２１の「３」が「ｃｎｔ」にそれぞれ当てはめている。

信号「ｒｅａｄｙ」は、時間０において値が「０」であり、時間１において値が「１」である。

また、信号「ｒｅｑｕｅｓｔ」は、時間１０において値が「０」であり、「時間１１において値が「１」である。

また、信号「ｃｎｔ」は、時間１１において値が自己参照「Ｘ」であり、時間１２においてこの値に１を加算したもの「Ｘ＋１」である。

表作成部１０２は、それぞれ対応する時間にイベントの結果である値を記録する。また、信号の変化がない部分は空欄としておく。

このような処理によって、表作成部１０２が時系列表２０を作成する。

図９に戻り、表作成部１０２は、時系列と信号とからなる時系列表２０の作成と平行して、仮定部と帰結部とを決定する処理を実行する（Ｓ５）。

仮定部と帰結部とは、インプリケーション演算子を検出することで決定する。表作成部は、プロパティからインプリケーション演算子を挟む右辺と左辺とを検出し、左辺を仮定部に、右辺を帰結部に、それぞれ決定する。

前述のプロパティ言語による記述は、インプリケーション演算子を挟んで、左辺は「＄ｒｏｓｅ（ｒｅａｄｙ） ＃＃１０ ＄ｒｏｓｅ（ｒｅｑｕｅｓｔ）」であり、これを仮定部とする。

また、右辺は「＃＃１ ｃｎｔ＝＝＄ｐａｓｔ（ｃｎｔ，１）＋１」であり、これを帰結部とする。

左辺は、前述のステップＳ２及び３の処理により、信号「ｒｅａｄｙ」と信号「ｒｅｑｕｅｓｔ」と、に変換されている。従って、表作成部１０２は、仮定部の因子は「ｒｅａｄｙ」と「ｒｅｑｕｅｓｔ」とであることを検出する。

また、右辺は、信号「ｃｎｔ」のみの記述であるため、表作成部１０２は、帰結部の因子は信号「ｃｎｔ」であることを検出する。

この検出結果から、表作成部１０２は、この検出結果から仮定部と帰結部との関係を信号による演算式で表す帰結式を作成する（Ｓ６）。

ステップＳ５により検出された例では、帰結式は「ｃｎｔ＝ｒｅａｄｙ＊ｒｅｑｕｅｓｔ」となる、これは、信号「ｃｎｔ」を検証する場合は、信号「ｒｅａｄｙ」と信号「ｒｅｑｕｅｓｔ」が仮定部であることを表す。

表作成部１０２は、このステップＳ６によって作成した帰結式を、時系列表２０の帰結式の行２３に記録する（Ｓ７）。このとき、表作成部１０２は、記入する際に、信号名に対応する項番で帰結式を表現する。

テーブル１２０において、信号「ｃｎｔ」は、信号「ｒｅａｄｙ」と信号「ｒｅｑｕｅｓｔ」との論理積であるので、帰結式は、それぞれの項番２１の数字によって「３＝１＊２」と記述される。

次に、表作成部１０２は、時系列表２０に逆時間２４を記録する（Ｓ８）。逆時間２４とは、時系列の最後のイベントが発生する時点を始点とし、検証開始時までの時系列を逆にカウントして記載したものである。この逆時間２４は、逆プロパティを生成する処理に用いられる。

以上のような処理によって、表作成部１０２は、命題プロパティから時系列表２０を作成する。作成された時系列表２０は、メモリ１１２に記録される。時系列表２０は、次に説明する逆プロパティ又は対偶プロパティの生成処理に用いられる。

次に、逆プロパティの生成を説明する。

プロパティ生成部１０３は、命題プロパティに基づいて表作成部１０２から出力された時系列表２０を元に、逆、裏、対偶を意味するプロパティを生成する。ここでは、逆プロパティの生成を説明する。

図１４は、本実施形態の逆プロパティの生成方法を示すフローチャートである。

プロパティ生成部１０３は、まず、時系列表２０を参照して、信号名２２と、信号値と、逆時間２４とを抽出する（Ｓ１１）。抽出した信号名２２、信号値、逆時間２４は、遅延時間テーブル１２０として作成される。

図１５は、本実施形態のステップＳ１１で作成されるイベントと遅延時間テーブル１２０の一例の説明図である。

プロパティ生成部１０３は、時系列表２０から取得したイベント及びその値と、そのイベントが発生する時間とを遅延時間テーブル１２０に記入する。

なお、遅延時間の列１２２は逆時間を抽出しているため、マイナスとなることがあってもよい。

次に、プロパティ生成部１０３は、作成した遅延時間テーブル１２０に対して、前述した図１１に示す関数変換テーブル１３０を参照して、信号のシーケンスを関数化できるか、すなわち、信号の変化を関数に変換できるかを判断する（Ｓ１２）。

プロパティ生成部１０３は、列１２１の信号の変化パターンと関数変換テーブル１３０とを照合することによって関数化が可能かを判断する。

プロパティ生成部１０３は、ステップＳ１２で関数化が可能であると判断された信号のシーケンスに対して関数化を行う（Ｓ１３）。

そして、プロパティ生成部１０３は、イベントを関数化した後、イベントと遅延時間との対応を表すテーブルを作成する（Ｓ１４）。

図１６は、本実施形態のプロパティ生成部がステップＳ１４で作成する遅延時間テーブル１２０の一例の説明図である。

プロパティ生成部１０３は、図１５に示す遅延時間テーブル１２０を参照して、イベントを関数化する。

具体的には、プロパティ生成部１０３は、遅延時間が「０」のとき「ｃｎｔ＝＝ｘ＋１」であることと、遅延時間が「−１」のとき「ｃｎｔ＝＝ｘ」であることから、関数変換テーブル１３０を参照して、「ｃｎｔ＝＝＄ｐａｓｔ（ｃｎｔ，１）＋１」（遅延時間「０」のときの「ｃｎｔ」は１サイクル前の「ｃｎｔ」を「＋１」インクリメントしたものである）と関数化する。

同様に、プロパティ生成部１０３は、遅延時間が「−１」のときに「ｒｅｑｕｅｓｔ＝＝１」であることと、遅延時間が「−２」のときに「ｒｅｑｕｅｓｔ＝＝０」であることから、関数変換テーブル１３０を参照して、「＄ｐａｓｔ（＄ｒｏｓｅ（ｒｅｑｕｅｓｔ），１）」（遅延時間が「−１」のときに「ｒｅｑｕｅｓｔ」が立ち上がること）と関数化する。

また、プロパティ生成部１０３は、遅延時間が「−１１」のときに「ｒｅａｄｙ＝＝０」であることと、遅延時間が「−１２」のときに「ｒｅａｄｙ＝＝０」であることから、関数変換テーブル１３０を参照して、「＄ｐａｓｔ（＄ｒｏｓｅ（ｒｅａｄｙ，１１））」（遅延時間が「−１１」のときに「ｒｅａｄｙ」が立ち上がること）と関数化する。

これら関数化されたイベントは、前述した図１１と同じ形式の遅延時間テーブル１２０（図１６）に記録する。

一方で、逆プロパティは命題プロパティに対して、仮定部と帰結部とを反転させたものであるため、時系列表２０の帰結式２３から得られる仮定部と帰結部との信号関係を反転させることで、逆プロパティを生成できる。

このことを利用して、プロパティ生成部１０３は、帰結式２３の仮定部と帰結部との信号関係を反転する処理を行う（Ｓ１５）。

図１３に示す時系列表２０を参照すると、帰結式は３＝１＊２であり、これは信号「ｃｎｔ」の値を検証する場合には、信号「ｒｅａｄｙ」と信号「ｒｅｑｕｅｓｔ」とが仮定となることを表している。

プロパティ生成部１０３は、この仮定部と帰結部とを反転して、帰結式「１＊２＝３」を得る。これは、信号「ｒｅａｄｙ」と信号「ｒｅｑｕｅｓｔ」との値を検証する場合に信号「ｃｎｔ」が仮定となるということを表している。

次に、プロパティ生成部１０３は、ステップＳ１４で作成したテーブルと、ステップＳ１５で得られる帰結式とを組み合わせることによって逆プロパティを生成する（Ｓ１６）。具体的には、テーブルに記載された各イベントとその遅延時間とを帰結式に当てはめ、これを逆プロパティとして記録する。

このステップＳ１６の処理によって、逆プロパティの生成が完了する。

図１７は、本実施形態のプロパティ生成部１０３によって実行される逆プロパティの生成の説明図である。

図１７（Ａ）は、命題プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

表作成部１０２は、このプロパティ言語を解析し、前述した図９の処理によって時系列表２０を作成する。図１７（Ｂ）は、図１７（Ａ）のプロパティ言語に対応する時系列表２０の一例である。

プロパティ生成部１０３は、この時系列表２０と命題プロパティのプロパティ言語とを参照して、前述の図１４の処理によって逆プロパティを生成する。

図１７（Ｃ）は、図１７（Ａ）に示す命題プロパティに対して生成された逆プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

次に、裏プロパティの生成を説明する。

プロパティ生成部１０３は、前述のように命題プロパティに基づいて表作成部１０２から出力された時系列表２０を元に、逆プロパティを生成する。

一方、裏プロパティは、否定を表す「！」を命題プロパティのプロパティ言語に付加することによって生成する。

図１８は、本実施形態のプロパティ生成部１０３が実行する裏プロパティの生成の説明図である。

図１８（Ａ）は、命題プロパティを、自然言語とそれに対応するプロパティ言語で記述したものである。

このプロパティ記述から裏プロパティを作成する場合は、プロパティ生成部１０３は、インプリケーション演算子によって仮定部と帰結部とを検出する。なお、既に作成されている時系列表２０を参照して仮定部と帰結部とを検出してもよい。

次に、プロパティ生成部１０３は、仮定部と帰結部とに記載されている各イベントに、否定を表す「！」を付加する。

図１８（Ｂ）は、図１８（Ａ）に示す命題プロパティに対して生成された裏プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

なお、否定の意味とは、該当イベントの動作以外の動作の指示である。

例えば、「＄ｒｏｓｅ（ｒｅａｄｙ）」（ｒｅａｄｙが立ち上がること）の否定形は、「！＄ｒｏｓｅ（ｒｅａｄｙ）」（ｒｅａｄｙが立ち上がらないこと）となる。

具体的には、「ｒｅａｄｙ」の値が「０」を維持している状態と、「１」を維持している状態と、「１」から「０」に立ち下がる状態と、を意味することとなる。

同様に、「ｃｎｔ＝＝＄ｐａｓｔ（ｃｎｔ，１）＋１」（ｃｎｔ値は１サイクル前のｃｎｔ値＋１であること）の否定形は、「！（ｃｎｔ＝＝＄ｐａｓｔ（ｃｎｔ，１）＋１）」（ｃｎｔ値は１サイクル前のｃｎｔ値＋１ではないこと）となる。これは、「ｃｎｔ」の値が１サイクル前の「ｃｎｔ」の値＋１以外の値であれば全て条件を満たすことになる。

次に、対偶プロパティの生成を説明する。

対偶プロパティは、命題プロパティに対して仮定部と帰結部とを反転させ、さらに、全てのイベントに対して否定形を表す「！」を付加することによって生成する。つまり、前述のように命題プロパティに基づいて表作成部１０２から出力された時系列表２０を元に、逆プロパティを生成し、この逆プロパティを裏プロパティに変換することによって、対偶プロパティを生成する。

図１９は、本実施形態のプロパティ生成部１０３が実行する対偶プロパティの生成の説明図である。

逆プロパティは、前述のように図９、図１４で示される処理によって生成される。また、裏プロパティは図１８に示すように、各イベントに対して否定形を表す「！」を付加することで生成する。

図１９（Ａ）は、命題プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

表作成部１０２は、このプロパティ言語を解析し、前述した図９の処理によって時系列表２０を作成する。図１９（Ｂ）は、図１９（Ａ）のプロパティ言語に対応する時系列表２０の一例である。

プロパティ生成部１０３は、この時系列表２０と命題プロパティのプロパティ言語とを参照して、前述の図１４の処理によって逆プロパティを生成する。

図１９（Ｃ）は、図１９（Ａ）に示す命題プロパティに対して生成された逆プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

さらに、生成された逆プロパティに対して、図１８において説明したように、プロパティ生成部１０３は、仮定部と帰結部とに記載されている各イベントに、否定を表す「！」を付加する。

図１９（Ｄ）は、図１９（Ａ）に示す命題プロパティに対して生成された対偶プロパティを、自然言語とそれに対応するプロパティ言語とで記述したものの一例である。

以上説明したような処理によって、論理検証支援部１０が、命題プロパティから逆、裏及び対偶を意味するプロパティを自動的に生成することができる。

次に、形式的論理検証について説明する。

検証部１０４は、オペレータが入力した命題プロパティ、又は、プロパティ生成部１０３が生成した逆プロパティ、裏プロパティ、対偶プロパティを入力し、形式的論理検証を行う機能である。

図２０は、本実施形態の検証部１０４が実行する形式的論理検証の説明図である。

形式的論理検証は、検証対象のネットリストから抽出されるロジックコーンと、検査対象の期待値から抽出されるロジックコーンとを比較し、これらの等価性を検証することによって、論理回路の正当性を数学的に証明する手法である。

ロジックコーンとは、論理を、ＦＦ（Ｆｌｉｐ Ｆｌｏｐ）を頂点とする組合せ回路網とする等価回路に置き換えたものである。

検証部１０４は、論理回路のＲＴＬを検査対象のネットリストとして、ロジックコーンを抽出する。また同様に、プロパティに基づく検査対象の期待値からロジックコーンを抽出する。

そして、検証部１０４は、これら検証対象のロジックコーンと期待値であるロジックコーンとを比較し、これらの等価性を検証する。

等価性の検証方法としては、従来周知であるＯＢＤＤ（Ｏｒｄｅｒｅｄ Ｂｉｎａｒｙ Ｄｅｃｉｓｉｏｎ Ｄｉａｇｒａｍ）等の手法を用いることができる。なお、形式的論理検証を行う手法は、これに限定されない。

図２０に示す例では、検証部１０４は、論理回路のＦＦ３０とＦＦ３０−１とＦＦ３０−２との組合せであるロジックコーン３１と、生成されたプロパティに基づいて、期待値を表すＦＦ３０−３とＦＦ３０−４とＦＦ３０−５との組合せであるロジックコーン３１−１との比較を検証する例を示す。

図２１は、本実施形態の検証部１０４が実行する形式的論理検証のフローチャートである。

形式的論理検証が開始されると、まず、検証部１０４は、入力部１１８から検証対象である論理のＲＴＬと、命題プロパティ又はプロパティ生成部１０３により生成された逆、裏、対偶プロパティとの入力を受付ける（Ｓ１０１）。

次に、検証部１０４は、プロパティから期待値であるロジックコーンを抽出する処理と論理回路のＲＴＬのロジックコーンを抽出する処理を実行する（Ｓ１０２）。

次に、検証部１０４は、ステップ１０２で抽出した期待値のロジックコーンと、設計回路のロジックコーンとの等価性を比較する（Ｓ１０３）。そして、比較の結果、ロジックコーンが等価であるか否かを判定する（Ｓ１０４）。

比較の結果、ロジックコーンが等価であると認めた場合は、ステップＳ１０５に移行し、検証部１０４は、設計された論理回路は期待通りの動作をしていることを確認する。この結果を検証結果出力部１０５に出力する。

一方、結果が等価でないと認めた場合は、設計された論理、又は、プロパティ自体に誤りがあることを意味する。この場合は、検証部１０４は、検証結果出力部１０５からエラーを通知する。このとき、ロジックコーンから期待値と整合性が取れない組合せの波形（反例となる波形）を生成することによって、デバック情報を検証結果出力部１０５を通じて提示することができる。

このような処理によって形式的論理検証が完了する。

以上のように本発明の実施形態では、論理検証支援部１０が、設計回路の論理と、論理を検証する検証項目である第１のプロパティである命題プロパティと、を取得する入力受付部１０１と、命題プロパティで発生する事象（イベント）を時系列に並べた時系列表２０を作成する表作成部１０２と、命題プロパティと時系列表２０とに基づいて、命題プロパティの逆、裏又は対偶を意味する第２のプロパティを作成するプロパティ生成部１０３と、命題プロパティ、逆プロパティ、裏プロパティ又は対偶プロパティを用いて論理を検証する検証部１０４と、検証部１０４の検証結果を出力する検証結果出力部１０５と、を備える。

このような構成により、オペレータが準備した命題プロパティから、逆、裏又は対偶を意味する第２のプロパティを作成することができる。これにより、複数のプロパティが自動的に生成でき、プロパティを網羅的に生成することができるので、論理検証の検証品質を向上させることができる。さらに、論理検証における時間的、人的なコストを削減して、効率的に論理検証を行うことができる。

次に、本発明の第２の実施形態を説明する。

第２の実施形態の論理検証支援部１０は、命題プロパティから逆、裏、対偶を表すプロパティを生成して、これを検証する機能だけではなく、命題プロパティを視覚的に確認できる機能を有する。

図２２は、本実施形態の論理検証支援部１０のブロック図である。なお、第１の実施形態と同一の構成は同一の符号を付し、その説明は省略する。

論理検証支援部１０は、図１で前述したように、入力受付部１０１、表作成部１０２、プロパティ生成部１０３、検証部１０４及び検証結果出力部１０５を備える。

論理検証支援部１０は、表出力部２０１を備える。表出力部２０１は、表作成部１０２により生成された時系列表２０を表示部１１７に表示する機能を有する。

表出力部２０１から出力される時系列表２０は、図２に例示した時系列表２０である。時系列表２０は、プロパティに宣言されない信号及びその値は表示しないため、オペレータが視覚的にプロパティの整合性を判断しやすい。

そのため、表出力部２０１によって時系列表２０を表示することによって、オペレータは、意図したプロパティが生成されているかどうかをデバックするための手法として用いることができる。

次に、本発明の第３の実施形態を説明する。

第３の実施形態の論理検証支援部１０は、前述した第２の実施形態のように命題プロパティを視覚的に確認できる機能に加え、生成された逆、裏、対偶プロパティの時系列表２０をも表示する機能を有する。

図２３は、本実施形態の論理検証支援部１０のブロック図である。なお、第１及び第２の実施形態と同一の構成は同一の符号を付し、その説明は省略する。

論理検証支援部１０は、表出力部２０１と表作成部２０２とを備える。表出力部２０１は、表作成部１０２により生成された時系列表２０を表示部１１７に表示する機能を有する。

表作成部２０２は、プロパティ生成部１０３により生成された逆、裏、対偶プロパティの時系列表２０を作成する機能を有する。

第２の実施形態と同様に、表出力部２０１は、命題プロパティを元に作成した時系列表２０を表示する。

さらに、表出力部２０１は、表作成部２０２により作成された、逆、裏、対偶プロパティの時系列表２０を表示する。

このようにすることで、オペレータは、論理検証支援部１０によって自動的に作成された逆、裏、対偶プロパティの時系列表２０を、視覚的に確認することができる。そのため、オペレータ間でプロパティの共有が容易になる。

また、表出力部２０１で出力される時系列表２０を生成されたプロパティと共に外部データベースに登録するようにしてもいい。これにより、時系列表２０の等価性を比較して、異なるプロパティ言語表記だが検証内容は等しいプロパティを摘出するといったプロパティの検証作業を行うことができる。

１０ 論理検証支援部
１１ 論理検証支援システム
２０ 時系列表
１０１ 入力受付部
１０２ 表作成部
１０３ プロパティ生成部
１０４ 検証部
１０５ 検証結果出力部
１１１ ＣＰＵ
１１２ メモリ
１１３ ＨＤＤ
１１４ 入出力インタフェース
１１５ バス
１１６ 論理検証支援プログラム
１１７ 表示部
１１８ 入力部
２０１ 表出力部
２０２ 表作成部

Claims (8)

1. プログラムを実行する制御部と、記憶部と、入力部と、情報を表示する表示部と、を備える論理検証システムにおいて、論理を検証する検証項目である第１のプロパティを用いて前記論理を検証する論理検証方法であって、
   前記入力部から入力された論理と、前記入力部から入力された前記第１のプロパティと、前記入力部から入力され、前記第１のプロパティから生成する命題を指定する変換指定値と、を取得し、前記記憶部に記録する第１の手順と、
   前記第１のプロパティから、当該第１のプロパティで発生する事象を時系列に表す時系列表を作成し、作成された前記時系列表を前記記憶部に記録する第２の手順と、
   前記変換指定値によって指定された命題に対応する第２のプロパティを生成し、前記生成された第２のプロパティを前記記憶部に記録する手順であって、前記変換指定値によって前記第１のプロパティの逆、又は対偶が指定された場合に前記第１のプロパティと前記時系列表とに基づき前記第２のプロパティを生成し、前記変換指定値によって前記第１のプロパティの裏が指定された場合に前記第１のプロパティに基づき前記第２のプロパティを生成する、第３の手順と、
   前記第１のプロパティ及び前記作成された第２のプロパティのそれぞれを用いて、前記論理を検証する第４の手順と、
   を備え、
   前記第２の手順は、
   前記第１のプロパティに含まれる演算子を検出することにより仮定部と帰結部とを抽出する手順と、
   抽出した前記仮定部及び前記帰結部それぞれについて、前記事象の内容である信号の変化と、前記変化が発生する時間と、を取得する手順と、
   前記信号の変化を前記時間に基づいた時系列に表す前記時系列表を作成し、作成した前記時系列表を前記記録部に記録する手順と、
   前記仮定部と前記帰結部との関係を表す帰結式を作成し、作成した前記帰結式を前記時系列表に記録する手順と、
   前記時系列に表された最終時間から開始時間への逆の時系列である逆時間を作成し、作成した前記逆時間を前記時系列表に記録する手順と、
   作成した前記時系列表を、前記表示部に表示する手順と、
   を含み、
   前記第３の手順は、
   生成した前記第２のプロパティにおける前記信号の変化を前記時間に基づいた時系列に表す新たな時系列表を作成し、作成した前記新たな時系列表を前記表示部に表示する手順
   を含むことを特徴とする論理検証方法。
2. 前記第２の手順は、さらに、前記第１のプロパティから取得した前記信号の変化が関数として表されている場合は、前記関数を、信号と前記信号の変化と前記時間との表記に変換する手順を含むことを特徴とする請求項１に記載の論理検証方法。
3. 前記第３の手順は、
   前記時系列表から、前記信号と前記信号の変化と前記時間と前記逆時間とを取得する手順と、
   前記時系列表から、前記帰結式を取得し、取得した前記帰結式の仮定部と帰結部とを入れ替えた新たな帰結式に変換する手順と、
   前記新たな帰結式に、前記信号と前記信号の変化と前記時間とを当てはめて逆を意味する前記第２のプロパティを作成し、作成した逆を意味する前記第２のプロパティを前記記憶部に記録する手順と、
   を含むことを特徴とする請求項１又は２に記載の論理検証方法。
4. 前記第３の手順は、前記第１のプロパティの仮定部と帰結部とをそれぞれ否定形に変換して裏を意味する前記第２のプロパティを作成し、作成した裏を意味する前記第２のプロパティを前記記憶部に記録する手順を含むことを特徴とする請求項１から３のいずれか一つに記載の論理検証方法。
5. 前記第３の手順は、
   前記時系列表から、前記信号と前記信号の変化と前記時間と前記逆時間とを取得する手順と、
   前記時系列表から、前記帰結式を取得し、取得した前記帰結式の仮定部と帰結部とを入れ替えた新たな帰結式に変換する手順と、
   前記新たな帰結式に、前記信号と前記信号の変化と前記時間とを当てはめて逆を意味する前記第２のプロパティを作成する手順と、
   作成した逆を意味する前記第２のプロパティの仮定部と帰結部とをそれぞれ否定形に変換して、対偶を意味する前記第２のプロパティを作成し、作成した対偶を意味する前記第２のプロパティを前記記憶部に記録する手順と、
   を含むことを特徴とする請求項１から４のいずれか一つに記載の論理検証方法。
6. 前記第４の手順は、
   前記論理に基づくロジックコーンと、前記第１又は第２のプロパティに基づく期待値のロジックコーンとを作成する手順と、
   前記ロジックコーンの結果と前記期待値のロジックコーンの結果とが等価であるか否かを判定する手順と、
   を含むことを特徴とする請求項１から５のいずれか一つに記載の論理検証方法。
7. 前記論理は、レジスタ転送レベルにより記述されていることを特徴とする請求項１から６のいずれか一つに記載の論理検証方法。
8. 制御部と、記憶部と、入力部と、出力部と、を備え、論理を検証する検証項目である第１のプロパティを用いて前記論理を検証する論理検証システムにおいて、
   前記制御部が前記記憶部に記録されているプログラムを実行することによって、表作成部、プロパティ生成部及び検証部が実現されており、
   前記入力部から入力された論理と、前記入力部から入力された前記第１のプロパティと、前記入力部から入力され、前記第１のプロパティから生成する命題を指定する変換指定値と、を取得し、前記記憶部に記録し、
   前記表作成部は、前記第１のプロパティから、当該第１のプロパティで発生する事象を時系列に表す時系列表を作成し、作成した前記時系列表を前記記憶部に記録し、
   前記プロパティ生成部は、前記変換指定値によって指定された命題に対応する第２のプロパティを生成し、生成した前記第２のプロパティを前記記憶部に記録し、
   前記プロパティ生成部は、前記変換指定値によって前記第１のプロパティの逆、又は対偶が指定された場合に前記第１のプロパティと前記時系列表とに基づき前記第２のプロパティを生成し、前記変換指定値によって前記第１のプロパティの裏が指定された場合、前記第１のプロパティに基づき前記第２のプロパティを生成し、
   前記検証部は、前記第１のプロパティと前記作成した第２のプロパティのそれぞれを用いて、前記論理を検証し、
   前記出力部は、前記検証部の検証結果を出力し、
   前記表作成部は、
   前記第１のプロパティに含まれる演算子を検出することにより仮定部と帰結部とを抽出し、
   抽出した前記仮定部及び前記帰結部それぞれについて、前記事象の内容である信号の変化と、前記変化が発生する時間と、を取得し、
   前記信号の変化を前記時間に基づいた時系列に表す前記時系列表を作成して、作成した前記時系列表を前記記録部に記録し、
   前記仮定部と前記帰結部との関係を表す帰結式を作成して、作成した前記帰結式を前記時系列表に記録し、
   前記時系列に表された最終時間から開始時間への逆の時系列である逆時間を作成して、作成した前記逆時間を前記時系列表に記録し、
   前記出力部は、前記表作成部によって作成した時系列表を表示し、
   前記プロパティ生成部は、生成した前記第２のプロパティにおける前記信号の変化を前記時間に基づいた時系列に表す新たな時系列表を作成し、
   前記出力部は、作成した前記新たな時系列表を表示することを特徴とする論理検証システム。

Images