(57)【要約】      （修正有）【課題】プロパティのデバッグ方法の確立によって適切なプロパティの効率的な作成方法を提供する。【解決手段】複数のプロパティの検証データ３２を使用して実行される論理プログラム３１の論理検証の結果として仮定部にエラーが含まれると示されているエラープロパティを取得し、上記論理検証の結果としてエラーを含まないと示されている複数の非エラープロパティを取得する。上記複数の非エラープロパティのそれぞれと上記エラープロパティとを比較し、上記エラープロパティとの共通箇所の数が予め定められた値に達している非エラープロパティを、上記エラープロパティのデバッグにおいて参考とされる参考プロパティと決定する。システムが、参考プロパティと上記エラープロパティとの比較結果を出力装置において提示する。【選択図】図５
2014021817.tif 000002
【特許請求の範囲】
【請求項１】
それぞれが仮定部と帰結部とを含む複数のプロパティを使用して実行される論理回路プログラムの論理検証を支援するシステムによる、論理検証支援方法であって、
前記システムが、前記論理回路プログラムの前記論理検証の結果として仮定部にエラーが含まれると示されているエラープロパティを、記憶装置に格納されている前記複数のプロパティから取得し、
前記システムが、前記論理回路プログラムの前記論理検証の結果としてエラーを含まないと示されている複数の非エラープロパティを、前記記憶装置に格納されている前記複数のプロパティから取得し、
前記システムが、前記複数の非エラープロパティのそれぞれと前記エラープロパティとを比較し、
前記システムが、前記複数の非エラープロパティにおいて、前記エラープロパティとの共通箇所の数が予め定められた値に達している非エラープロパティを、前記エラープロパティのデバッグにおいて参考とされる参考プロパティと決定し、
前記システムが、前記決定した参考プロパティと前記エラープロパティとの比較結果を、出力装置においてユーザに提示する、論理検証支援方法。
【請求項２】
請求項１に記載の論理検証支援方法であって、
前記システムが、前記複数の非エラープロパティのそれぞれ及び前記エラープロパティを細分化して、それぞれが複数の変数と当該複数変数間の関係を示す複数の項を生成し、
前記システムが、細分化された前記複数非エラープロパティのそれぞれの複数の項と、細分化された前記エラープロパティの複数の項と、を比較し、
前記複数の非エラープロパティのそれぞれと前記エラープロパティとの間の共通箇所の数は、前記複数の非エラープロパティのそれぞれと前記エラープロパティとの間の共通項の数である、論理検証支援方法。
【請求項３】
請求項２に記載の論理検証支援方法であって、
前記システムが、演算子と変換後の遅延時間表記とを関連づける演算子変換情報を参照して、前記複数の非エラープロパティ及び前記エラープロパティのそれぞれのプロパティにおいて、前記遅延時間表記と異なる演算子を前記遅延時間表記に変換し、
前記複数の項のそれぞれは、前記変数間の関係を当該変数間の遅延時間で示す、論理検証支援方法。
【請求項４】
請求項２又は３に記載の論理検証支援方法であって、
前記システムが、前記複数の非エラープロパティのそれぞれの細分化において、仮定部と帰結部との間の境界を除去し、前記仮定部の変数と前記帰結部の変数とを含む項を作成する、論理検証支援方法。
【請求項５】
請求項２又は３に記載の論理検証支援方法であって、
前記システムが、前記複数の非エラープロパティ及び前記エラープロパティのそれぞれの細分化において、変数値を削除した後に前記複数の項に細分化する、論理検証支援方法。
【請求項６】
請求項１、２又は３に記載の論理検証支援方法であって、
前記システムが、前記エラープロパティにおける、前記参考プロパティとの間の共通箇所を、前記エラープロパティにおける推定エラー箇所として、前記出力装置において前記ユーザに提示する、論理検証支援方法。
【請求項７】
請求項１、２又は３に記載の論理検証支援方法であって、
前記システムが、複数の参考プロパティにおける優先度を、前記複数の参考プロパティのそれぞれと前記エラープロパティとの間の共通箇所の数に応じて決定し、
前記システムが、前記出力装置において前記複数の参考プロパティの優先度を前記ユーザに提示する、論理検証支援方法。
【請求項８】
請求項１、２又は３に記載の論理検証支援方法であって、
前記システムが、前記出力装置において、各変数間の遅延時間の情報を含む、前記複数の項の生成過程を示す図を、前記ユーザに提示する、論理検証支援方法。
【請求項９】
それぞれが仮定部と帰結部とを含む複数のプロパティを使用して実行される論理回路プログラムの検証を支援する処理を、論理検証支援システムに実行させるためのプログラムであって、
前記論理回路プログラムの前記検証の結果として仮定部にエラーが含まれると示されているエラープロパティを、記憶装置に格納されている前記複数のプロパティから取得し、
前記論理回路プログラムの前記検証の結果としてエラーを含まないと示されている複数の非エラープロパティを、前記記憶装置に格納されている前記複数のプロパティから取得し、
前記複数の非エラープロパティのそれぞれと前記エラープロパティとを比較し、
前記複数の非エラープロパティにおいて、前記エラープロパティとの共通箇所の数が予め定められた値に達している非エラープロパティを、前記エラープロパティのデバッグにおいて参考とされる参考プロパティと決定し、
前記決定した参考プロパティと前記エラープロパティとの比較結果を、出力装置においてユーザに提示する、
ことを含む処理を、前記論理検証支援システムに実行させるためのプログラム。
【請求項１０】
プロセッサ、記憶装置及び出力装置を含み、それぞれが仮定部と帰結部とを含む複数のプロパティを使用して実行される論理回路プログラムの検証を支援する、論理検証支援システムであって、
前記記憶装置は、前記複数のプロパティを格納し、
前記プロセッサは、前記論理回路プログラムの前記検証の結果として仮定部にエラーが含まれると示されているエラープロパティを、前記記憶装置に格納されている前記複数のプロパティから取得し、
前記プロセッサは、前記論理回路プログラムの前記検証の結果としてエラーを含まないと示されている複数の非エラープロパティを、前記記憶装置に格納されている前記複数のプロパティから取得し、
前記プロセッサは、前記複数の非エラープロパティのそれぞれと前記エラープロパティとを比較し、
前記プロセッサは、前記複数の非エラープロパティにおいて、前記エラープロパティとの共通箇所の数が予め定められた値に達している非エラープロパティを、前記エラープロパティのデバッグにおいて参考とされる参考プロパティと決定し、
前記出力装置は、前記決定した参考プロパティと前記エラープロパティとの比較結果を、ユーザに提示する、論理検証支援システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路の論理設計における論理検証を支援する技術に関する。
【背景技術】
【０００２】
回路の大規模化と多機能化に対処するためには、回路の検証の効率改善も重要な課題であり、有効な方法の１つとして、形式的論理検証（以下、形式検証）が知られている。形式検証は、論理回路に期待される動作や禁止される動作をプロパティとして定義し、検証対象の論理回路がプロパティに違反する動作を起こさないように設計されているかを検証するものである。プロパティは、入力パタンとそれに伴う出力の期待値動作とを定義するものである。プロパティの例は、「ある入力の３サイクル以内に別の信号を出力する」、「特定の二つの信号は決して同時に'１'とならない」である。
【０００３】
形式検証により、従来の論理シミュレーションに比べ効率的に検証を実施できる。しかし、形式検証は、定義されたプロパティに対する十分な検証を保証するが、必要十分なプロパティを定義できるか否かは、別の問題である。プロパティのよる回路の網羅検証のために、不足しているプロパティを補う技術が、特開２００６−２２８０６５（特許文献１）に開示されている。
【０００４】
同技術は、全事象のリストに基づいて、仕様からユーザが予め定義したプロパティにおいて不足している事象を補うための補集合のプロパティを生成する。このプロパティ生成工程は、全事象のリストから未定義の状態の事象を抽出し、抽出した未定義の状態の事象が成立しないことを表すプロパティを補集合のプロパティとして生成する。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００６−２２８０６５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
特許文献１に開示された技術は、検証者が定義したプロパティ以外を論理的に成立しないプロパティとみなし、同内容のプロパティを自動生成することでプロパティの不足を補う。これにより、回路の網羅的な検証を行い、検証の質と効率を向上させる。
【０００７】
しかし、同技術を適用するためには、必要なプロパティを検証者が適切に作成していることが前提である。プロパティを作成する際には、プロパティを作成する検証者の技術不足、検証者による仕様書の誤認、検証者（論理設計者）の思い込み等により、仮定部が論理的に成立しない誤り（以下、ｖａｃｕｏｕｓエラー）を、作成されたプロパティが含むことがある。
【０００８】
このようなｖａｃｕｏｕｓエラーを含むプロパティのデバッグ方法は、未だ確立されていないため、プロパティのデバッグに多くの時間を要することが新たな課題となっている。本発明はこの点に鑑みてなされたものであって、論理回路の検証者が適切なプロパティを効率良く作成することができるように支援することを目的とする。
【課題を解決するための手段】
【０００９】
本発明の一態様は、それぞれが仮定部と帰結部とを含む複数のプロパティを使用して実行される論理回路プログラムの論理検証を支援するシステムによる、論理検証支援方法である。前記システムが、前記論理回路プログラムの前記論理検証の結果として仮定部にエラーが含まれると示されているエラープロパティを、記憶装置に格納されている前記複数のプロパティから取得する。前記システムが、前記論理回路プログラムの前記論理検証の結果としてエラーを含まないと示されている複数の非エラープロパティを、前記記憶装置に格納されている前記複数のプロパティから取得する。前記システムが、前記複数の非エラープロパティのそれぞれと前記エラープロパティとを比較する。前記システムが、前記複数の非エラープロパティにおいて、前記エラープロパティとの共通箇所の数が予め定められた値に達している非エラープロパティを、前記エラープロパティのデバッグにおいて参考とされる参考プロパティと決定する。前記システムが、前記決定した参考プロパティと前記エラープロパティとの比較結果を、出力装置においてユーザに提示する。
【発明の効果】
【００１０】
本発明の一態様によれば、論理回路の設計者が適切なプロパティを効率良く作成することができるように支援するができる。
【図面の簡単な説明】
【００１１】
【図１】実施例１における論理回路設計例のフローチャートである。
【図２】実施例１のプロパティの一例の説明図である。
【図３】関連技術の問題点を説明する図である。
【図４】関連技術におけるｖａｃｕｏｕｓエラーの原因を説明する図である。
【図５】実施例１の論理検証支援を説明する図である。
【図６】実施例１の論理検証支援システムの構成を模式的に示すブロック図である。
【図７Ａ】実施例１のｖａｃｕｏｕｓエラープロパティにおけるエラー箇所を特定するための参考情報を生成し、出力する処理の例を示すフローチャートである。
【図７Ｂ】実施例１のｖａｃｕｏｕｓエラープロパティにおけるエラー箇所を特定するための参考情報を生成し、出力する処理の例を示すフローチャートである。
【図８】実施例１の参考プロパティの出力例を示す図である。
【図９】実施例１の推定されるプロパティの修正箇所の出力例を示す図である。
【図１０】実施例１のプロパティの細分化の例を説明するフローチャートである。
【図１１】実施例１のプロパティで使用される演算子の一例を説明する図である。
【図１２】実施例１の遅延時間テーブルの一例の説明図である。
【図１３】実施例１のプロパティからのインプリケーション演算子の削除を説明する図である。
【図１４】実施例１のプロパティからの変数の値の削除を説明する図である。
【図１５】実施例１のプロパティの細分化による項の生成を説明する図である。
【図１６】実施例１の細分化したプロパティを格納するパスプロパティＤＢの例を説明する図である。
【図１７】実施例２の論理検証の例を説明するフローチャートである。
【図１８】実施例２の論理検証支援を説明する図である。
【発明を実施するための形態】
【００１２】
以下、添付図面を参照して本発明の実施形態について説明する。以下の説明及び添付図面は本発明の原理に則った具体的な実施形態と実装例を示しているが、これらは本発明の理解のためのものであり、決して本発明を限定的に解釈するために用いられるものではない。
【００１３】
本実施形態では、当業者が本発明を実施するのに十分詳細にその説明がなされているが、他の実装・形態も可能で、本発明の技術的思想の範囲と精神を逸脱することなく構成・構造の変更や多様な要素の置き換えが可能であることを理解する必要がある。例えば、本発明の範囲内において、実施例の構成の一部を他の実施例の構成に置き換えることが可能であり、実施例の構成に他の実施例の構成を加えることも可能である。従って、以降の記述をこれに限定して解釈してはならない。
【実施例１】
【００１４】
図１は、実施例１における論理装置設計のフローチャートである。論理装置設計において、方式設計者は、方式検討（Ｓ１０）を実行し、論理装置の方式を検討する。次に、論理設計者は、機能検討（Ｓ１１）を実行し、方式検討により決定した方式を実現させるための機能を検討する。次に、論理設計者は、論理設計（Ｓ１２）を実行し、機能を実現するための論理を記述する。以下において、設計者をユーザとも呼ぶ。
【００１５】
論理設計（Ｓ１２）は、ＲＴＬ（Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌ：レジスタ転送レベル）によって記述された論理回路を作成する。ＲＴＬ設計は、ハードウェア記述言語（ＨＤＬ）により論理回路を記述する。次に、論理設計者は論理検証（Ｓ１３）を実行し、作成されたＲＴＬの論理回路を検証する。一般的に、論理検証は、論理シミュレーションと形式検証に分類される。
【００１６】
論理シミュレーションは、動的検証と呼ばれ、論理回路の機能やタイミングを模擬的に動作せることで検証する方法である。一方、形式検証は、静的検証と呼ばれ、論理回路に期待される動作や禁止される動作をプロパティとして定義し、検証対象の論理回路がプロパティに違反する動作を起こさない設計がされているかを検査する方法である。本例は、論理検証（Ｓ１３）において、形式検証を使用する。
【００１７】
次に、論理設計者は、論理合成（Ｓ１４）を実行し、ＲＴＬ論理回路からゲートレベルの論理回路を合成する。次に、論理設計者は、実装（Ｓ１５）を実行し、作成されたゲートレベルの論理回路を、物理装置に配置する。以上の作業により、論理装置設計を行う。
【００１８】
本実施例は、ステップＳ１３における形式検証を対象とする。図２は、本実施例１のプロパティの一例を説明する図である。図２に示すテーブル２０は、検証項目（プロパティ）を、自然言語とプロパティ言語（アサーション言語とも呼ばれる）で記述した例を示している。行２１は、自然言語で記述された検証項目（プロパティ）を記述しており、行２２は、自然言語で記述された検証項目（プロパティ）を、プロパティ言語で記述した場合を示している。
【００１９】
プロパティ言語は、論理回路の形式検証で参照されるプロパティ（検証項目）を記述するための専用言語であり、ＳＶＡ（Ｓｙｓｔｅｍ  Ｖｅｒｉｌｏｇ  Ａｓｓｅｒｔｉｏｎ）やＰＳＬ（Ｐｒｏｐｅｒｔｙ  Ｓｐｅｃｉｆｉｃ  Ｌａｎｇｕａｇｅ）、ＯＶＬ（Ｏｐｅｎ  Ｖｅｒｉｆｉｃａｔｉｏｎ  Ｌｉｂｒａｒｙ）等がある。
【００２０】
本実施例は、ＳＶＡによる記述を用いるが、本発明はプロパティ言語に依存するものではなく、その他のプロパティ言語を用いることができる。行２２の「｜−＞」は、インプリケーション演算子であり、同演算子を境に、左辺は仮定条件を表す仮定部、右辺は仮定に対する結果を表す帰結部である。
【００２１】
行２１における「ｒｅｑ＝'１'の５ｃｌｋ後にｐｍｔ＝'１'を受信する場合」は、行２２における「ｒｅｑ＝＝１ ＃＃５ ｐｍｔ＝＝１」に対応し、行２１における「ｐｍｔ＝'１'を受信してから１ｃｌｋ後にｔｏｐ＝'１'を送信する」は、行２２における「ｔｏｐ＝＝0 ＃＃１ ｔｏｐ＝＝１」に対応する（図１１の演算子の定義を参照）。「ｒｅｑ」、「ｐｍｔ」、「ｔｏｐ」は、内部信号の変数名であり、プロパティにおける変数である。
【００２２】
図３は、本実施例が解決する問題点を説明する図である。図３に示す機能仕様書３０は、ステップＳ１１（機能検討）により作成される機能仕様書である。論理プログラム３１は、機能仕様書３０を元にして、ステップＳ１２（論理設計）により作成される論理プログラムである。ここで示す論理プログラム３１は、ＲＴＬの回路記述を意味する。
【００２３】
検証データ３２は、機能仕様書３０を元にしてステップＳ１３（論理検証）により作成される検証データである。ここで示す検証データは、図２の行２２に示すようなプロパティ言語で記述された検証項目（プロパティ）の集合を意味する。形式検証ツール３３は、論理プログラム３１の形式検証を行う検証ツールである。形式検証ツールは広く知られた技術である。
【００２４】
波形３４は、形式検証において、プロパティにおける帰結部に対して論理プログラム３１に誤り（矛盾）がある場合に形式検証ツール３３が出力する入力パタンの波形である。形式検証ツール３３は、論理プログラム３１がプロパティで規定されている仮定部に対して規定されている帰結部と異なる動作を行う場合に、波形３４を出力する。
【００２５】
形式検証は、機能仕様書３０を元に作成された論理プログラム３１と検証データ３２とを、形式検証ツール３３に入力することで検証を行う。形式検証ツール３３は、論理プログラム３１が、プロパティが規定した通りの動作（仮定部と帰結部に一致した動作）をすると確認した場合に、ＰＡＳＳを出力する（Ｓ３０）。論理プログラム３１が、プロパティにおいて規定されている仮定部に対して規定された帰結部の動作を行う場合に、ＰＡＳＳと判定される。
【００２６】
形式検証ツール３３は、論理プログラム３１の論理検証において、論理プログラム３１がプロパティの帰結部に違反すると判定した場合に、違反する場合の入力パタンを波形３４で出力する（Ｓ３１）。論理プログラム３１が、プロパティで規定されている仮定部に対して規定されている帰結部と矛盾する動作を行う場合に、波形３４が出力される。論理設計者は、この波形３４の情報を元に、論理プログラム３１を修正する（Ｓ３２）。
【００２７】
また、形式検証ツール３３は、プロパティの仮定部が論理プログラム３１の回路構成上起こり得ないと判定した場合に、ｖａｃｕｏｕｓエラーを出力し、論理プログラム３１の検証を中止する（Ｓ３３）。論理設計者は、ｖａｃｕｏｕｓエラーの通知により、プロパティの仮定部に問題があることを認識出来る。しかし、プロパティの帰結部に問題がある場合に比べてデバッグの助けとなる情報がなく、プロパティの修正に時間を要する。
【００２８】
図４は、ｖａｃｕｏｕｓエラーの原因の一例を説明する図である。図４に示すテーブル４０は、機能仕様書３０から検証データ（プロパティ）３２を作成する際に含まれる可能性のある誤りの一例を示している。行４１は、機能仕様書３０に記載されている動作を示している。行４２と行４３は、行４１に対する誤認の例を示している。
【００２９】
機能仕様書３０に「リセット後にａｃｔ＝'１'とすること」と記載されている場合（ａｃｔは内部信号変数名）、検証データ３２を作成する際に「リセット後」の「後」とはどの時刻を指しているのか不明確である。また、「ａｃｔ＝'１'とすること」の「ａｃｔ＝'１'」は、どれだけの時間その状態を保持するか不明確である。このため、論理検証者は、エラーを含むプロパティを作成してしまうことがある。この他、論理検証者の技術不足、確認漏れ等により、ｖａｃｕｏｕｓエラーとなるプロパティを作成してしまうことがある。
【００３０】
本実施例１は、このようなプロパティにおけるエラーのデバッグを支援する技術を提供する。以下において、本例の技術を使用したｖａｃｕｏｕｓエラーの効率的なデバッグ方法について説明する。図５は、本実施例１の論理検証方法を説明する図である。図５に示す論理検証支援ツール６０は、形式検証時にｖａｃｕｏｕｓエラーと判定されたプロパティを効率良くデバッグするためのツール（プログラム、又は、ハードウェア若しくはハードウェアとソフトウェアの組合せにより実現される機能部）である。
【００３１】
図５に示すように、論理検証支援ツール６０は、論理検証データ３２に含まれるプロパティのうち、論理プログラム３１の形式検証においてＰＡＳＳと判定されたプロパティを、パスプロパティＤＢ（データベース）６１に格納する。論理検証支援ツール６０は、形式検証ツール３３がｖａｃｕｏｕｓエラーと判定したプロパティ（ｖａｃｕｏｕｓエラープロパティ）と、パスプロパティＤＢ６１に格納されているプロパティとを比較し、その比較結果を出力する。
【００３２】
一例において、論理検証支援ツール６０は、比較結果の出力において、ｖａｃｕｏｕｓエラープロパティプロパティの推定修正箇所を出力する。論理検証者は、この推定情報を元にプロパティの修正を行うことが出来る（Ｓ６０）。
【００３３】
図６は、本実施例１において、論理検証の支援を行う論理検証支援システム５０の構成例を示すブロック図である。図６に示す論理検証支援システム５０は、一つの計算機で構成されており、プロセッサであるＣＰＵ５１、主記憶装置であるメモリ５２、二次記憶装置であるＨＤＤ（Ｈａｒｄ  Ｄｉｓｋ  Ｄｒｉｖｅ）５３、入出力インタフェース５６、表示装置５７及び入力装置５８を備える。論理検証支援システム５０は、２以上の計算機で構成することができる。
【００３４】
ＣＰＵ５１、メモリ５２、ＨＤＤ５３、及び入出力インタフェース５６は、バス５５を介して相互に通信可能に接続される。出力装置５７及び入力装置５８は、入出力インタフェース５６を介して、他の要素と通信する。入力装置５８は、例えば、マウスとキーボードであり、表示装置５７の典型例は液晶表示装置やプリンタである。例えば、ＨＤＤ５３、出力装置５７及び入力装置５８は、ネットワークを介して接続されていてもよい。論理検証支援システム５０は、一部の構成要素を有していなくともよい。
【００３５】
図６において、メモリ５２は、不図示のＯＳ（Ｏｐｅｒａｔｉｎｇ  Ｓｙｓｔｅｍ）の他、論理検証支援プログラム５４を格納している。ＨＤＤ５３は、パスプロパティＤＢ６１、検証データ３２、形式検証結果１００及び遅延時間テーブル１２０を格納している。これらの詳細は後述する。
【００３６】
本実施例においては、論理検証支援に使用される情報は、テーブル又はＤＢに格納されている。必要な情報を含むテーブルの数及び各テーブルが格納する情報は、システム設計に依存する。本実施形態において、データ記憶領域に格納される情報はデータ構造に依存せず、どのようなデータ構造で表現されていてもよい。例えば、テーブル、リスト若しくはＤＢが情報を示すことができる。
【００３７】
図６は、説明の便宜上、メモリ５２内にプログラムを示し、ＨＤＤ５３内にプログラムが使用する情報を示しているが、論理検証支援システム５０の処理において必要とされるデータ（プログラムを含む）は、典型的に、二次記憶装置であるＨＤＤ５３からメモリ５２にロードされる。
【００３８】
ＣＰＵ５１は、論理検証支援システム５０の制御を司る制御部である。ＣＰＵ５１は、ＨＤＤ５３に格納される論理検証支援プログラム５４をメモリ５２上に読み出し、これを実行する。ＣＰＵ５１は、論理検証支援プログラム５４に従って動作することで、論理検証支部として機能する。このように、ＣＰＵ５１は、プログラムに従って動作することで、その機能を実現する機能部として動作する。従って、プログラムの行う処理は、ＣＰＵ５１及びそのＣＰＵ５１を含む計算機（システム）の処理である。
【００３９】
メモリ５２は、例えばＤＲＡＭにより構成される。メモリ５２は、論理検証支援プログラム５４や論理検証支援プログラム５４が参照する情報や生成する情報を一時的に記憶する。論理検証支援プログラム５４が生成する情報は、必要に応じて、ＨＤＤ５３に保存される。
【００４０】
ＨＤＤ５３は、論理検証支援システム５０によって実行されるプログラム及びプログラムが参照する情報及びプログラムが生成する情報を記憶する不揮発性の記憶媒体を有する記憶装置である。二次記憶装置は、ＨＤＤに限定されず、他の種類の記憶装置、例えば、ＳＳＤ（Ｓｏｌｉｄ  Ｓｔａｔｅ  Ｄｒｉｖｅ）を使用してもよい。メモリ５２及びＨＤＤ５３によって記憶部（記憶装置）が構成される。
【００４１】
論理検証支援システム５０は、他の機能を有していてもよい。例えば、ＨＤＤ５３は、形式検証プログラム、論理検証の対象の論理プログラム３１（論理回路のＲＴＬデータ）や、検証データ３２（プロパティの集合）を格納する。これらはメモリ５２にロードされ、ＣＰＵ５１は、形式検証プログラムに従って動作して、検証データ３２を使用して、論理プログラム３１の形式検証を実行する。
【００４２】
入出力インタフェース５６は、論理検証支援プログラム５４の動作に関わる情報を出力装置５７に出力する。また、入出力インタフェース５６は、論理設計者により入力装置５８を使用して入力される情報を、論理検証支援プログラム５４に転送する。論理検証支援システム５０は、他の計算機からデータを受信し、他の計算機に結果を出力してもよい。
【００４３】
論理検証支援プログラム５４は、ｖａｃｕｏｕｓエラーを引き起こしたプロパティ（ｖａｃｕｏｕｓエラープロパティ又はエラープロパティと呼ぶ）のエラー箇所（修正すべき箇所）を論理設計者が特定するために参考となる支援情報を提供する。論理検証支援プログラム５４は、参考となる支援情報を、出力装置５７に出力する。論理設計者は、出力装置５７が提示する情報を参照して、エラープロパティにおける修正箇所を特定し、プロパティのデバッグを行うことができる。
【００４４】
本例において、論理検証支援プログラム５４は、ｖａｃｕｏｕｓエラーを引き起こしたプロパティと形式検証においてそれ自体にエラーが存在しないと検証されたプロパティ（非エラーパスプロパティ）とを比較し、ｖａｃｕｏｕｓエラーを引き起こしたプロパティと予め定められた個数以上の共通箇所を有する非エラープロパティを選択する。
【００４５】
論理検証支援プログラム５４は、エラープロパティと選択した非エラープロパティの比較結果の情報を出力する。論理設計者は、出力された情報を参照して、ｖａｃｕｏｕｓエラープロパティの修正箇所を特定し、そのデバッグを行うことができる。
【００４６】
図７Ａ、図７Ｂは、論理検証支援プログラム５４（論理検証支援システム５０）による、ｖａｃｕｏｕｓエラープロパティにおけるエラー箇所を特定するための参考情報を生成し、出力する処理の例を示すフローチャートである。図７Ａは、形式検証においてＰＡＳＳと判定されたプロパティ（パスプロパティ）をパスプロパティＤＢ６１に格納する処理のフローチャートである。パスプロパティは、形式検証においてエラーを有していないと検証された、非エラープロパティである。なお、本例は、論理回路プログラムが帰結部に矛盾するプロパティは、エラーを有していない非エラープロパティと判定する。
【００４７】
図５を参照して説明したように、本例の形式検証においてプロパティの帰結部と論理回路プログラム３１との間に不一致があると、論理プログラム３１が修正され、形式検証が再実行される。形式検証において仮定部にエラーを有するプロパティが検出されると、形式検証ツール３３は、形式検証を中止する。したがって、形式検証の中止までに検証されたプロパティは、全てパスプロパティである。
【００４８】
図７Ｂは、ｖａｃｕｏｕｓエラープロパティとパスプロパティとを比較し、その比較結果を出力する処理のフローチャートである。論理検証支援プログラム５４は、検証データ３２の各プロパティについて、図７Ａのフローを実行する。図７Ａにおいて、ｖａｃｕｏｕｓエラープロパティの検出により論理プログラム３１の形式検証が中止されると、論理検証支援プログラム５４は、検証データ３２からプロパティを取得する（Ｓ７０）。次に、論理検証支援プログラム５４は、形式検証結果１００を参照し、選択したプロパティが、ＰＡＳＳ判定されたプロパティであるか否か判定する（Ｓ７１）。
【００４９】
選択したプロパティがＰＡＳＳ判定されたプロパティである場合（Ｓ７１：Ｙ）、論理検証支援プログラム５４は、そのプロパティを細分化し（Ｓ７２）、パスプロパティＤＢ６１に格納する（Ｓ７３）。プロパティを細分化の詳細は後述する。選択したプロパティがＰＡＳＳ判定されたプロパティでない場合（Ｓ７１：Ｎ）、当該プロパティは、パスプロパティＤＢ６１に格納されない。
【００５０】
なお、形式検証ツール３３により検証されるプロパティは、その設計に依存する。形式検証ツール３３は、ｖａｃｕｏｕｓエラーの検出後に、他のプロパティについて論理プログラム３１の検証を行ってもよい。また、形式検証は、プロパティの帰結部における論理プログラム３１のエラーを検出した場合に、そのエラーを修正することなく他のプロパティについて検証を進めてもよい。検証結果が、帰結部が論理プログラム動作と矛盾するプロパティを示す場合、論理検証支援プログラム５４は、当該プロパティをパスプロパティと共に非エラープロパティとしてパスプロパティＤＢ６１に格納してもよい。
【００５１】
次に、論理検証支援プログラム５４は、図７Ｂのフローを実行する。論理検証支援プログラム５４は、検証データ３２の各プロパティについて、図７Ｂのフローを実行する。図７Ｂにおいて、論理検証支援プログラム５４は、検証データ３２から、プロパティを取得する（Ｓ７４）。次に、論理検証支援プログラム５４は、形式検証の結果を参照し、選択したプロパティが、形式検証で、ｖａｃｕｏｕｓエラーと判定されたプロパティであるか否か判定する（Ｓ７５）。
【００５２】
選択したプロパティが、ｖａｃｕｏｕｓエラープロパティではない場合（Ｓ７５：Ｎ）、論理検証支援プログラム５４は、選択したプロパティについてのこのフローを終了し、次のプロパティを選択する（Ｓ７４）。
【００５３】
選択したプロパティが、ｖａｃｕｏｕｓエラープロパティである場合（Ｓ７５：Ｙ）、論理検証支援プログラム５４は、ｖａｃｕｏｕｓエラープロパティを細分化する（Ｓ７６）。論理検証支援プログラム５４は、さらに、当該ｖａｃｕｏｕｓエラープロパティとパスプロパティＤＢ６１に格納されているプロパティのそれぞれとを、比較する（Ｓ７７）。プロパティの細分化及びプロパティの比較方法の詳細は後述するが、論理検証支援プログラム５４は、細分化した項毎に比較を行う。
【００５４】
論理検証支援プログラム５４は、ステップＳ７７における比較結果として、エラー箇所を特定するために参考とされる情報を出力する（Ｓ７８）。本例において、出力される参考情報は、修正の際に参考とするべきプロパティ及びｖａｃｕｏｕｓエラープロパティの推定修正箇所を含む。参考情報は、出力装置５７より論理設計者に提示される。論理設計者は、参考情報を参照して、ｖａｃｕｏｕｓエラープロパティのエラー箇所を特定し、修正する。
【００５５】
図８は、論理検証支援プログラム５４（論理検証支援システム５０）により出力される参考情報の一例８０を示している。本例において、参考情報は、テーブル８０で表されている、参考プロパティのリストを示す。参考情報８０は、細分化されていない各プロパティの内容を示すことで、参考プロパティとエラープロパティの比較結果を示す。論理検証支援プログラム５４は、参考情報８０を表示するためのデータを生成し、画像データを出力装置５７に出力する。
【００５６】
参考プロパティは、論理検証支援プログラム５４により、ｖａｃｕｏｕｓエラープロパティを修正するために参考とするべきと判定されたパスプロパティである。論理検証支援プログラム５４は、エラープロパティとパスプロパティとを順次比較し、エラープロパティに対して、予め定められた閾値以上の共通箇所を有するパスプロパティを、参考プロパティとして選択する。参考情報８０は、閾値以上の共通箇所を有する全て又は一部のパスプロパティを表示する。
【００５７】
共通箇所の特定方法の詳細は後述するが、論理検証支援プログラム５４は、規定の方法に従ってプロパティを細分化し、細分化により得られた各項を比較して、同一の項を共通箇所と特定する。共通性が高い二つのプロパティは、関連性が高いプロパティであり、論理設計者は、それらプロパティにおける共通部分及び／又は異なる部分を比較することで、ｖａｃｕｏｕｓエラープロパティにおける修正すべきエラーを特定し、修正することができる。
【００５８】
参考情報テーブル８０は、プロパティＩＤカラム８１、プロパティ内容カラム８２、そして共通箇所数カラム８３を有する。参考情報テーブル８０は、ｖａｃｕｏｕｓエラープロパティのエントリ８５と、参考プロパティのエントリ８６〜８８を含む。
【００５９】
プロパティＩＤカラム８１は、ｖａｃｕｏｕｓエラープロパティ及び参考プロパティの識別子を格納（表示）する。プロパティ内容カラム８２は、細分化されていない各プロパティの内容を格納（表示）する。共通箇所数カラム８３は、各参考プロパティとｖａｃｕｏｕｓエラープロパティとの間の共通箇所の数を格納（表示）する。図８において、「！」は否定の演算子であり、「！ｐｍｔ[＊６]」は、「！ｐｍｔ」が六回続くことを意味する。
【００６０】
本例において、論理検証支援プログラム５４は、ｖａｃｕｏｕｓエラープロパティと共通箇所のより多い参考プロパティをより優先度が高いプロパティと判定し、参考プロパティを優先度が高い順に並べて出力する。共通箇所の数は表示しなくともよい。優先度が高い参考プロパティが、ｖａｃｕｏｕｓエラープロパティのより正確な修正情報を含んでおり、優先度を明示することで論理設計者によるより効率的なデバッグ（形式検証）を適切に支援できる。優先度は順序や符号により示すことができるが、明示しなくともよい。
【００６１】
論理設計者は、表示されているｖａｃｕｏｕｓエラープロパティと各参考プロパティとを比較し、それらの共通部分と異なる部分とを比較することで、ｖａｃｕｏｕｓエラープロパティにおいて修正すべきエラー箇所を特定し、修正することができる。例えば、図８の例において、論理設計者は、ｖａｃｕｏｕｓエラープロパティにおける「ｔｏｐ＝＝０」と参考プロパティ１における「ｔｏｐ＝＝１」とから、ｖａｃｕｏｕｓエラープロパティにおける「ｔｏｐ＝＝０」がエラー箇所であり、「ｔｏｐ＝＝１」に修正すべきことを推定することができる。
【００６２】
図８の例は、ｖａｃｕｏｕｓエラープロパティと１以上の共通箇所を有する全てのパスプロパティを表示する（閾値が１の例）。これと異なり、予め定められている閾値は、２以上の数値でもよい。
【００６３】
本例において、論理検証支援プログラム５４は、さらに、ｖａｃｕｏｕｓエラープロパティにおいて修正すべきエラー箇所を推定した結果を、参考情報として表示する。図９は、推定修正箇所（推定エラー箇所）の表示例を示している。図９の参考情報テーブルは、プロパティＩＤのカラム９１と、細分化したプロパティのカラム９２を有する。
【００６４】
図９の参考情報９０は、細分化したｖａｃｕｏｕｓエラープロパティと細分化した参考プロパティ１との比較を示す。図８が、細分化していないｖａｃｕｏｕｓエラープロパティと参考プロパティとの比較を示すのとは異なる。図９において、楕円で囲まれた項（箇所）は、両プロパティの共通項（共通箇所）を示している。楕円で囲まれてない項（箇所）は、両プロパティの異なる項（箇所）である。この例において、各項は、二つの変数（信号識別子）と遅延表記の演算子で構成されている。
【００６５】
例えば、論理設計者が入力装置５８を使用して、図８における参考プロパティ１を選択すると、論理検証支援プログラム５４は、図９に示す画像データを生成し、出力装置５７に出力する。図７Ａ、図７Ｂを参照して説明したように、論理検証支援プログラム５４は、細分化されたパスプロパティ（パスプロパティＤＢ６１）と細分化されたｖａｃｕｏｕｓエラープロパティを記憶部に保持している。論理検証支援プログラム５４は、論理設計者が他の参考プロパティを選択すると、細分化したｖａｃｕｏｕｓエラープロパティと選択した参考プロパティの比較結果を出力する。
【００６６】
図９に示すテーブル９０は、細分化したｖａｃｕｏｕｓエラープロパティと参考プロパティ１との比較結果において、推定修正箇所を表示している。ｖａｃｕｏｕｓエラープロパティは、仮定部にエラーを有するプロパティであり、参考プロパティは、形式検証でＰＡＳＳと判定されたプロパティである。そこで、本例の論理検証支援プログラム５４は、細分化したｖａｃｕｏｕｓエラープロパティにおける項において、参考プロパティとの間における共通項にエラーが存在していると推定する。
【００６７】
参考プロパティの動作内容は、形式検証ツール３３により論理回路上の動作が可能なことが保証されている。すなわち、参考プロパティの動作内容との差分を抽出することでｖａｃｕｏｕｓエラーの原因を特定することが出来る。本例では、より多くのプロパティを参考プロパティとして抽出し、エラープロパティのデバック効率を向上させるため、項による比較をおこなう。
【００６８】
図９の例においては、推定エラー箇所は、ｖａｃｕｏｕｓエラープロパティの項のうち楕円で囲まれた項である。推定エラー箇所が明示されることで、論理設計者（検証者）は、より効率的に、ｖａｃｕｏｕｓエラープロパティの修正箇所を特定することができ、適切なプロパティを効率良く作成することができる。
【００６９】
図９の例は、細分化したｖａｃｕｏｕｓエラープロパティと選択された一つの細分化された参考プロパティを表示するが、論理検証支援プログラム５４は、複数の細分化された参考プロパティを表示してもよい。論理検証支援プログラム５４は、細分化された参考プロパティを表示することなく、細分化したｖａｃｕｏｕｓエラープロパティと、それにおける推定エラー箇所を明示してもよい。
【００７０】
論理検証支援プログラム５４は、テーブル８０とテーブル９０を同時に表示してもよい。本例において、論理検証支援プログラム５４は、テーブル８０及びテーブル９０の双方を表示するが、その一方のみを表示するように構成されていてもよい。
【００７１】
論理検証支援プログラム５４は、推定エラー箇所を明示することなく（図９において楕円を示すことなく）、細分化されたｖａｃｕｏｕｓエラープロパティと１又は複数の細分化された参考プロパティを出力装置５７によって提示してもよい。
【００７２】
以下において、プロパティの細分化を説明する。プロパティは、複数の項に細分化される。以下に説明する例は、プロパティにおける変数間の関係を示す項を作成する。特に、以下の例において、論理検証支援プログラム５４は、二つの変数（のイベント）及びそれらの間の遅延時間の要素からなる項を作成する。これらの項をプロパティ間で比較することで、ｖａｃｕｏｕｓエラープロパティと共通性が高い参考プロパティ（非エラープロパティ）を適切に選択することができる。
【００７３】
図１０は、本実施例１のプロパティの細分化の例を説明するフローチャートである。形式検証終了後、論理検証支援プログラム５４は、検証データ３２から、プロパティを取得する（Ｓ１００）。次に、論理検証支援プログラム５４は、取得したプロパティの演算子が、単純遅延表記のみで記述されているかを判定する（Ｓ１０１）。単純遅延表記は、「＃＃ｎ」（ｎは任意の数値）で表される関数であり、ｎサイクル（クロック）の遅延（時間経過）を意味する。
【００７４】
ここで、図１１を参照して、プロパティ言語における演算子（関数を含む）について説明する。図１１は、プロパティ言語で使用される演算子を説明するためのテーブル１１０を示している。テーブル１１０は、演算子の記号を示すカラム１１１と、演算子の意味を示すカラム１１２を有する。テーブル１１０は、プロパティで使用される演算子の一部のみを表示している。テーブル１１０が示す演算子の定義情報は、論理検証支援プログラム５４内に組み込まれている。
【００７５】
図１１において、「｜−＞」及び「｜＝＞」は、それぞれインプリケーション演算子である。それぞれの意味は、図１１に示す通りであり、プロパティの仮定部と帰結部の境界である。また、上述のように、「＃＃ｎ」は、ｎサイクル（クロック）の単純遅延表記である。図１１は、これらの他、＄ｐａｓｔや＄ｒｏｓｅ等の関数を例示している。関数は、信号の特定の動作を定義する演算子である。
【００７６】
図１０に戻って、取得したプロパティの演算子が、単純遅延表記のみで記述されている場合、論理検証支援プログラム５４は、ステップＳ１０４に進む。取得したプロパティの演算子が、単純遅延表記のみで記述されていない場合（Ｓ１０１：Ｎ）、論理検証支援プログラム５４は、プロパティ内の各関数（存在すれば）を単純遅延表記に変換する（Ｓ１０２）。関数を単純遅延表記に変換する方法は後述する。
【００７７】
論理検証支援プログラム５４は、全ての関数が単純遅延表記に変換されたプロパティにおいて、単純遅延表記以外の演算子（存在すれば）を、単純遅延表記に変換する（Ｓ１０３）。変換される演算子は、インプリケーション演算子（「｜−＞」又は「｜＝＞」）を含む。変換方法の詳細は後述する。インプリケーション演算子の変換により、プロパティにおける仮定部と帰結部の境（概念）が無効化される。この結果、プロパティの演算子は、単純遅延表記のみで構成される。
【００７８】
このように、演算子を遅延表記演算子に変換し、抽象化することで、プロパティを明確に細分化して、信号（変数）間の関係を示す項を作成することができる。仮定部と帰結部との境を除去することで、エラープロパティと仮定部又は帰結部が部分的に共通する参考プロパティを、適切に選択することができる。
【００７９】
論理検証支援プログラム５４は、さらに、変換したプロパティにおいて、変数の値を削除する（Ｓ１０４）。これにより、プロパティ間の比較を変数の値（信号の値）から独立して行うことができ、非エラープロパティとエラープロパティとの共通性をより適切に決定することができる。
【００８０】
以上の変換により、プロパティは、変数名（変数のイベント）と単純遅延表記のみの式に変換される。最後に、論理検証支援プログラム５４は、変数名と単純遅延表記からなるプロパティから、変数の組合せ及びそれらの間の遅延時間からなる項を抽出する（Ｓ１０５）。項の構成及びその抽出方法の詳細は後述する。以上説明したフローにより、プロパティが複数の項に細分化される。
【００８１】
以下において、演算子（関数を含む）を単純遅延表記に変換する（Ｓ１０２、Ｓ１０３）方法を説明する。図１２は、遅延時間テーブル１２０の構成例を示す。論理検証支援プログラム５４は、遅延時間テーブル１２０を参照して、演算子を単純遅延表記に変換する。遅延時間テーブル１２０は、演算子表記カラム１２１と、単純遅延表記カラム１２２とを有する。
【００８２】
演算子表記カラム１２１は、プロパティ言語で使用される演算子を格納している。単純遅延表記カラム１２２は、演算子表記カラム１２１における各演算子に対応する（各演算子を表す）単純遅延表記を格納している。遅延時間テーブル１２０は、ＨＤＤ５３に予め記憶されている。論理検証支援プログラム５４は、取得したプロパティから選択した演算子を遅延時間テーブル１２０において検索し、対応する単純遅延表記に当該演算子を変換する。
【００８３】
例えば、関数「＄ｒｏｓｅ（Ａ）」は、信号Ａの立ち上がりを表す関数であり、単純遅延表記により「Ａ＝＝０＃＃１Ａ＝＝１」と表される。インプリケーション演算子「｜−＞」は、サイクル遅延を含まないため、＃＃０に置き換えられる。また、インプリケーション演算子「｜＝＞」が記述されている場合は、１サイクル遅延を含むため、＃＃１に置き換えられる。否定演算子「!」は、「＃＃０」に置き換えられる。
【００８４】
図１３は、インプリケーション演算子の変換の一例を説明する図である。図１３に示すテーブル１３０の行１３１は、プロパティを自然言語で示したものである。行１３２は、同じプロパティをプロパティ言語で表記したものである。行１３３は、行１３２のプロパティのインプリケーション演算子を単純遅延表記に変換した式ある。インプリケーション演算子を単純遅延表記に変換することで、インプリケーション演算子が削除され、仮定部と帰結部の境が無効になる。
【００８５】
図１４は、本実施例１における変数の値の削除の一例を説明する図である。図１４に示すテーブル１４０の行１４１は、インプリケーション演算子を削除した後、各変数が値を有している状態の式（プロパティ）である。行１４２は、行１４１の式から変数の値を削除した式である。論理検証支援プログラム５４は、「＝＝」で結合された変数と値の組合せを検索し、「＝＝」の後の値を削除する。
【００８６】
図１５は、本実施例１の複数項の生成（抽出）の方法（過程）（Ｓ１０５）を説明する図である。図１５は、式「ｒｅｑ＃＃５ｐｍｔ＃＃７ｔｏｐ＃＃０ｅｒｒ」から、項１５３Ａ〜１５３Ｆを生成する例を示している。式「ｒｅｑ＃＃５ｐｍｔ＃＃７ｔｏｐ＃＃０ｅｒｒ」は、四つの変数１５０Ａ〜１５０Ｄを有する。変数１５０Ａ〜１５０Ｄの変数名はそれぞれ、「ｒｅｑ」、「ｐｍｔ」、「ｔｏｐ」、「ｅｒｒ」である。
【００８７】
変数「ｒｅｑ」１５０Ａと変数「ｐｍｔ」１５０Ｂとの間の遅延時間１５１Ａは、５サイクル（＃５）である。変数「ｐｍｔ」１５０Ｂと変数「ｔｏｐ」１５０Ｃとの間の遅延時間１５１Ｂは、７サイクル（＃７）である。変数「ｔｏｐ」１５０Ｃと変数「ｅｒｒ」１５０Ｄとの間の遅延時間１５１Ｃは、０サイクル（＃０）である。
【００８８】
変数「ｒｅｑ」１５０Ａと変数「ｐｍｔ」１５０Ｂとの間の遅延時間の総和（総遅延時間又は結合遅延時間と呼ぶ）１５２Ａは、５サイクル（＃５）である。変数「ｒｅｑ」１５０Ａと変数「ｔｏｐ」１５０Ｃとの間の結合遅延時間１５２Ｂは、１２（５＋７）サイクル（＃１２）である。変数「ｒｅｑ」１５０Ａと変数「ｅｒｒ」１５０Ｄとの間の結合遅延時間１５２Ｃは、１２（５＋７＋０）サイクル（＃１２）である。
【００８９】
変数「ｐｍｔ」１５０Ｂと変数「ｔｏｐ」１５０Ｃとの間の結合遅延時間１５２Ｄは、７サイクル（＃７）である。変数「ｐｍｔ」１５０Ｂと変数「ｅｒｒ」１５０Ｄとの間の結合遅延時間１５２Ｅは、７（７＋０）サイクル（＃７）である。最後に、変数「ｔｏｐ」１５０Ｃと変数「ｅｒｒ」１５０Ｄとの間の結合遅延時間１５２Ｆは、０サイクル（＃０）である。
【００９０】
項１５３Ａ〜１５３Ｆは、それぞれ、変数１５０Ａ〜変数１５０Ｄの各組合せから生成されている。項１５３Ａ〜１５３Ｆは、それぞれ、変数の組合せとそれらの間の結合遅延時間で構成されている。従って、四つの変数１５０Ａ〜１５０Ｄから、六つの項１５３Ａ〜１５３Ｆが生成される。
【００９１】
このように、論理検証支援プログラム５４は、プロパティを変換して生成した、変数と単純遅延表記からなる式から、全ての変数の組合せを抽出し、さらに、各変数の組合せにおける変数間の遅延時間の総和（結合遅延時間）を算出する。検証支援プログラム５４は、結合遅延時間を伴う変数の組合せのそれぞれを、プロパティを細分化して得られた項として使用する。
【００９２】
なお、式における変数の組合せの導き方は、各変数とその遅延時間を明確にすることが出来れば、どんな手法を用いてもよい。検証支援プログラム５４は、ｖａｃｕｏｕｓエラープロパティ及び参考プロパティの図１５に示す図を、ｖａｃｕｏｕｓエラーのデバッグ情報のとして、出力装置５７に出力してもよい。
【００９３】
図１５は、各変数間の遅延時間（総遅延時間を含む）を伴う変数間の関係及び総遅延時間とその遅延時間構成要素（隣接変数間の遅延時間）との関係を示す。論理設計者は、各変数間の関係及び各遅延時間の間の関係を示す図を参照することで、各項の生成の過程を知ることができる。これにより、ｖａｃｕｏｕｓエラープロパティ及び参考プロパティの構造を容易に把握することができ、ｖａｃｕｏｕｓエラープロパティのデバッグを、より容易に行うことができる。
【００９４】
図１６は、パスプロパティＤＢ６１に格納されている細分化されたプロパティの一例を示している。格納されているプロパティは、プロパティＩＤで識別される。プロパティＩＤの値は、検証データに格納されている同一プロパティのプロパティＩＤの値と同一である。図１６に示すように、各プロパティは細分化され、各プロパティを構成する項が格納されている。論理検証支援プログラム５４は、入力装置５８からの要求に応じて、パスプロパティＤＢ６１の内容の一部又は全てを、出力装置５７において提示してもよい。
【００９５】
本実施例は、仮定部にエラーを有するｖａｃｕｏｕｓエラープロパティのデバッグの参考となる情報を、エラーを有していないと判定されｖａｃｕｏｕｓエラープロパティと共通性が高いプロパティから取得し、提示することで、論理設計者（検証者）によるｖａｃｕｏｕｓエラープロパティにおけるエラー箇所（修正箇所）の推定及び特定を適切に支援することができる。これにより、従来では多くの時間を費やしていたプロパティのデバッグ作業を効率化することが出来る。
【００９６】
上記例において、パスプロパティＤＢ６１は、細分化されたパスプロパティを格納するが、それらに代えて又はそれらに加えて、細分化されていないパスプロパティを格納してもよい。パスプロパティＤＢ６１は、細分化されてないプロパティを格納し、論理検証支援システム５０は、パスプロパティＤＢ６１からプロパティを選択して、細分化した後にｖａｃｕｏｕｓエラープロパティと比較してもよい。
【００９７】
論理検証支援プログラム５４は、比較のために細分化して複数のパスプロパティをパスプロパティＤＢ６１に格納することなく、検証データ３２から取得したパスプロパティを細分化して、エラープロパティと比較し、その結果を記憶部に保持してもよい。
【００９８】
論理検証支援プログラム５４は、上記プロパティ細分化の例と異なる方法でプロパティを細分化してもよい。上記例は、変数（論理回路における信号）間の関係を示す項を、二つの変数とそれらの間の総遅延時間の要素で構成するが、例えば、論理検証支援プログラム５４は、３以上の変数とそれらの間の総遅延時間の要素を含む項を作成してもよい。
【００９９】
例えば、プロパティ細分化により生成される項は、遅延時間の要素を含まなくともよく、遅延演算子以外の演算子を含んでいてもよい。項は、変数の値を含んでいてもよい。例えば、論理検証支援プログラム５４は、エラープロパティの細分化において、仮定部のみから項を作成してもよい。
【実施例２】
【０１００】
本実施例２は、本実施形態の論理回路の検証支援を、静的検証である形式検証ではなく、動的検証におけるアサーションベースの検証に適応する例を説明する。本実施例２における論理検証支援システム５０のハードウェア構成及びソフトウェア構成は実施例１における図６の構成と同様であり、その説明は省略する。
【０１０１】
図１８は、本例の論理検証支援を説明するブロック図である。実施例１において形式検証ツール３３が形式検証を実行するが（例えば図５参照）、本例において、論理シミュレーションツール１８５が、実施例１の形式検証に代えて、論理プログラム３１のアサーションベースの動的検証を実行する。以下において、主に実施例１との相違点を説明する。
【０１０２】
図１７は、本実施例２の論理検証を説明するフローチャートである。以下において、図１８を参照しつつ、図１７のフローチャートを説明する。論理回路の機能検証終了後、論理設計者は、機能仕様書３０を元にＲＴＬの論理プログラム３１を作成する（Ｓ１７０）。次に、論理設計者は、機能仕様書３０を元に、アサーションにおけるプロパティを作成する（Ｓ１７１）。
【０１０３】
アサーションは、プロパティを使用した論理シミュレーションにおける検証方法（論理シミュレーションツールにおける検証機能）である。アサーションは、検証対象の設計が満たすべきプロパティを規定し、論理シミュレーション中に検証対象とプロパティの関係を調べてプロパティが満たされているかチェックする。
【０１０４】
本実施例２と実施例１との違いは、論理検証の方法にある。実施例１は、ＲＴＬの論理プログラム３１の検証に、静的検証である形式検証を用いる。一方、実施例２は、動的検証である論理シミュレーションを用いる。形式検証と論理シミュレーションにおいて、プロパティにおける構文上の違いはない。アサーションのためのプロパティ作成（Ｓ１７１）の後、論理シミュレーションツール（不図示）は、作成されたプロパティを使用して、論理シミュレーションを行う（Ｓ１７２）。
【０１０５】
論理設計者は、論理シミュレーション結果を参照して、プロパティを分類する。具体的には、論理設計者は、論理シミュレーション結果から、プロパティを３種類に分類する。それぞれ、シミュレーション動作が帰結部に矛盾し、アサーションが発火したプロパティ、正常にシミュレーション動作したプロパティ、そして、プロパティの仮定部にエラーが存在するプロパティである。論理設計者は、プロパティの分類リスト１８２を作成し、ＨＤＤ５３に格納する。
【０１０６】
論理検証支援プログラム５４（論理検証支援ツール６０）はプロパティ分類リストを参照し、プロパティＩＤとその分類を示すデータを順次選択する。選択したプロパティがアサーションの発火を引き起こしたプロパティである場合（Ｓ１７４：Ｙ）、論理検証支援プログラム５４は、検証データ３２が当該プロパティを取得し、細分化して非エラープロパティＤＢ１８４に格納する（Ｓ１７５）。
【０１０７】
アサーションは、組込まれているポイントにおける信号が、プロパティにおける帰結部と矛盾する場合に、発火する。アサーションが発火している場合（Ｓ１７４：Ｙ）、当該プロパティの帰結部と論理プログラム３１との間に矛盾がある。アサーション自体は有効に発火しているため、プロパティにエラーは存在しない。論理設計者は、論理プログラム３１における当該プロパティに対応する箇所を修正する（Ｓ１７６）。
【０１０８】
選択したプロパティがアサーションの発火を引き起こしたプロパティではなく（Ｓ１７４：Ｎ）、プロパティに問題がない場合（Ｓ１７７：Ｎ）、論理プログラムはプロパティ通りに正常に動作していることを意味するため、論理検証支援プログラム５４は、検証データ３２が当該プロパティを取得し、細分化して非エラープロパティＤＢ１８４に格納する（Ｓ１７８）。
【０１０９】
プロパティの仮定部に問題がある場合（Ｓ１７７：Ｙ）、論理検証支援プログラム５４は、検証データ３２が当該プロパティを取得し、細分化してエラープロパティＤＢ１８３に格納する（Ｓ１７９）。
【０１１０】
論理検証支援プログラム５４は、プロパティ分類リスト１８２の全てのプロパティについて細分化及びＤＢへの格納を実行したか判定し（Ｓ１８０）、未選択プロパティが残っている場合（Ｓ１８０：Ｎ）、論理検証支援プログラム５４は、ステップＳ１７３に戻る。
【０１１１】
全てのプロパティの細分化を完了している場合（Ｓ１８０：Ｙ）、論理検証支援プログラム５４は、エラープロパティＤＢ１８３からエラープロパティを順次選択して、非エラープロパティＤＢ１８４のエラープロパティのそれぞれと比較する（Ｓ１８１）。プロパティの構成は、論理シミュレーションと形式検証との間において同じであり、エラープロパティと非エラープロパティとの細分化による比較及びデバッグのための参考情報の提示は、実施例１と同様である。論理設計者（検証者）は、ステップＳ１８１における比較結果で得られた参考情報を参照して、各エラープロパティを修正する（Ｓ１８２）。
【０１１２】
本実施例によれば、動的論理検証において効率的にデバッグを行うための支援を行うことができる。上記例において、アサーション発火を引き起こしたプロパティが、エラープロパティと比較するプロパティに含まれるが、これらを比較する非エラープロパティから除外してもよい。その他、実施例１で説明した、デバッグのための参考情報の異なる複数の提示方法や、細分化における項の異なる複数の作成方法を本例の論理回路設計支援に適用することができる。
【０１１３】
本実施形態の上記実施例は、例えば、上記機能を実現するソフトウェアのプログラムコードを記憶したＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ等の非一時的記憶媒体をシステム又は装置に供給し、そのシステム又は装置のコンピュータ（又はＣＰＵやＭＰＵ）が非一時的記憶媒体に格納されたプログラムコードを読み出して実行することにより実現することができる。上記機能を実現するソフトウェアのプログラムコードは、ネットワークを介して配信されてもよい。上記実施例は、汎用コンピュータ上で稼動するソフトウェアで実装してもよいし専用ハードウェア又はソフトウェアとハードウェアの組み合わせで実装してもよい。
【符号の説明】
【０１１４】
５０  論理検証支援システム
５１  ＣＰＵ
５２  メモリ
５３  ＨＤＤ
５４  論理検証支援プログラム
５６  入出力インタフェース
５７  表示装置
５８  入力装置
【図１】
2014021817.tif 000003
【図２】
2014021817.tif 000004
【図３】
2014021817.tif 000005
【図４】
2014021817.tif 000006
【図５】
2014021817.tif 000007
【図６】
2014021817.tif 000008
【図７Ａ】
2014021817.tif 000009
【図７Ｂ】
2014021817.tif 000010
【図８】
2014021817.tif 000011
【図９】
2014021817.tif 000012
【図１０】
2014021817.tif 000013
【図１１】
2014021817.tif 000014
【図１２】
2014021817.tif 000015
【図１３】
2014021817.tif 000016
【図１４】
2014021817.tif 000017
【図１５】
2014021817.tif 000018
【図１６】
2014021817.tif 000019
【図１７】
2014021817.tif 000020
【図１８】
2014021817.tif 000021