(57)【特許請求の範囲】
【請求項１】
コンピュータを、
検証対象の実装記述を取得する取得手段、
前記取得手段によって取得された実装記述に基づいて、入力信号が入力される前記検証対象の入力ゲートの組み合わせを特定する特定手段、
前記特定手段によって特定された前記入力ゲートの組み合わせを構成する各入力ゲートから前記各入力信号が前記検証対象の出力ゲートに到達するまでのゲートの集合となる一対の出力コーンを、前記入力ゲートの組み合わせごとに検出する第１の検出手段、
前記第１の検出手段によって検出された前記一対の出力コーンに共通するゲートの集合となる共通出力コーンを、前記入力ゲートの組み合わせごとに検出する第２の検出手段、
前記第２の検出手段によって検出された共通出力コーンに基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出する算出手段、
前記算出手段によって算出された算出結果に応じた関連性強度を、前記入力ゲートの組み合わせごとに決定する決定手段、
前記検証対象の仕様に基づく前記入力ゲートの組み合わせに対して特定の関連性強度を設定する設定手段、
前記入力ゲートの組み合わせごとに、前記設定手段によって設定された特定の関連性強度と、前記決定手段によって決定された関連性強度とが一致するか否かを判断する判断手段、
前記判断手段によって判断された判断結果を出力する出力手段、
として機能させることを特徴とする検証支援プログラム。
【請求項２】
前記算出手段は、
前記共通出力コーン内に存在する特定の種類のゲートの数に基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出することを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
前記特定の種類のゲートは、記憶素子であることを特徴とする請求項２に記載の検証支援プログラム。
【請求項４】
前記算出手段は、
前記各入力ゲートから前記共通出力コーン内の最前段のゲートまでのゲート段数に基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出することを特徴とする請求項１に記載の検証支援プログラム。
【請求項５】
前記設定手段は、
前記特定の関連性強度を、前記入力ゲートの組み合わせ群のうち前記関連度が最大となる前記入力ゲートの組み合わせの関連性強度と同一強度に設定することを特徴とする請求項１〜４のいずれか一つに記載の検証支援プログラム。
【請求項６】
検証対象の実装記述を取得する取得手段と、
前記取得手段によって取得された実装記述に基づいて、入力信号が入力される前記検証対象の入力ゲートの組み合わせを特定する特定手段と、
前記特定手段によって特定された前記入力ゲートの組み合わせを構成する各入力ゲートから前記各入力信号が前記検証対象の出力ゲートに到達するまでのゲートの集合となる一対の出力コーンを、前記入力ゲートの組み合わせごとに検出する第１の検出手段と、
前記第１の検出手段によって検出された前記一対の出力コーンに共通するゲートの集合となる共通出力コーンを、前記入力ゲートの組み合わせごとに検出する第２の検出手段と、
前記第２の検出手段によって検出された共通出力コーンに基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出する算出手段と、
前記算出手段によって算出された算出結果に応じた関連性強度を、前記入力ゲートの組み合わせごとに決定する決定手段と、
前記検証対象の仕様に基づく前記入力ゲートの組み合わせに対して特定の関連性強度を設定する設定手段と、
前記入力ゲートの組み合わせごとに、前記設定手段によって設定された特定の関連性強度と、前記決定手段によって決定された関連性強度とが一致するか否かを判断する判断手段と、
前記判断手段によって判断された判断結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。
【請求項７】
制御手段および記憶手段を備えるコンピュータが、
前記制御手段により、検証対象の実装記述を取得して前記記憶手段に記憶する取得工程と、
前記制御手段により、前記取得工程によって取得された実装記述に基づいて、入力信号が入力される前記検証対象の入力ゲートの組み合わせを特定する特定工程と、
前記制御手段により、前記特定工程によって特定された前記入力ゲートの組み合わせを構成する各入力ゲートから前記各入力信号が前記検証対象の出力ゲートに到達するまでのゲートの集合となる一対の出力コーンを、前記入力ゲートの組み合わせごとに検出する第１の検出工程と、
前記制御手段により、前記第１の検出工程によって検出された前記一対の出力コーンに共通するゲートの集合となる共通出力コーンを、前記入力ゲートの組み合わせごとに検出する第２の検出工程と、
前記制御手段により、前記第２の検出工程によって検出された共通出力コーンに基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出する算出工程と、
前記制御手段により、前記算出工程によって算出された算出結果に応じた関連性強度を、前記入力ゲートの組み合わせごとに決定する決定工程と、
前記制御手段により、前記検証対象の仕様に基づく前記入力ゲートの組み合わせに対して特定の関連性強度を設定する設定工程と、
前記制御手段により、前記入力ゲートの組み合わせごとに、前記設定工程によって設定された特定の関連性強度と、前記決定工程によって決定された関連性強度とが一致するか否かを判断する判断工程と、
前記制御手段により、前記判断工程によって判断された判断結果を出力する出力工程と、
を実行することを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、検証対象となるハードウェアの論理検証を支援する検証支援プログラム、検証支援装置、および検証支援方法に関する。
【背景技術】
【０００２】
ハードウェア設計の論理検証においては、検証対象の入力となるパラメータに与える値の組み合わせを変えることで複数のテストパターンを作成する。従来においては、複数のパラメータ間の関連性の有無に応じて、試験する値の組み合わせ方を変えている。一般には関連性があるパラメータは、ないパラメータに比べてより多くの組み合わせをテストする。そして、仕様書から機能ごとに関連するパラメータを抽出し、その機能の振る舞い（アルゴリズムなど）から、パラメータ間の関連性の強弱を判断し、それにより組み合わせ方を変えている。
【０００３】
また、従来から、テストパターンの作成については、入力端子の相関を制約条件として与えてその条件を満足するような入力パターンを生成する手法や、入力端子の依存関係からシミュレーション結果が正当かどうかを判定する手法など、さまざまな論理検証ツールが開示されている（たとえば、下記特許文献１，下記特許文献２を参照。）。
【０００４】
【特許文献１】特開平７−３５８２８号公報
【特許文献２】特開平７−４９８８７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
しかしながら、上述した従来の論理検証では、仕様と実装との間で、あるパラメータの境界条件が異なってしまうという障害がある。また、仕様では関連がないパラメータ間について、実装では関連が生じたり、または逆に、仕様では関連があるパラメータ間について、実装では関連がなかったりするという障害がある。さらに、実装に対する時間的、面積的な制約から、仕様と実装で計算順序が異なる（たとえば、演算子が共有されたり、順序が入れ替わる）場合があり、テストすべきポイントを外してしまう可能性が大きいという問題がある。
【０００６】
従来ではこのような障害を見落としていたため、検証対象の入力となるパラメータに与える値の組み合わせの選択が不十分であり、組み合わせ自体の正当性が不明確であるという問題があった。これにより、検証対象内部の信号変化や検証対象が実現する機能の動作を網羅することができず、論理検証の信頼性が低下するという問題があった。
【０００７】
この発明は、上述した従来技術による問題点を解消するため、効率的かつ信頼性の高い論理検証作業をおこなうことができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上述した課題を解決し、目的を達成するため、この検証支援プログラム、検証支援装置、および検証支援方法は、検証対象の実装記述の入力を受け付け、入力された実装記述に基づいて、入力信号が入力される前記検証対象の入力ゲートの組み合わせを特定し、特定された前記入力ゲートの組み合わせを構成する各入力ゲートから前記各入力信号が前記検証対象の出力ゲートに到達するまでのゲートの集合となる一対の出力コーンを、前記入力ゲートの組み合わせごとに検出し、検出された前記一対の出力コーンに共通するゲートの集合となる共通出力コーンを、前記入力ゲートの組み合わせごとに検出し、検出された共通出力コーンに基づいて、前記入力ゲートの組み合わせを構成する各入力ゲートの関連度を、前記入力ゲートの組み合わせごとに算出し、算出結果に応じた関連性強度を、前記入力ゲートの組み合わせごとに決定し、前記検証対象の仕様書に基づく前記入力ゲートの組み合わせに対して特定の関連性強度を設定し、前記入力ゲートの組み合わせごとに、特定の関連性強度と、決定された関連性強度とが一致するか否かを判断し、判断結果を出力することを要件とする。
【０００９】
この検証支援プログラム、検証支援装置、および検証支援方法によれば、仕様と実装との間での入力ゲートの組み合わせの一貫性を判定することができるため、入力ゲートの組み合わせ自体の依存関係の正当性を確認することができる。
【発明の効果】
【００１０】
この検証支援プログラム、検証支援装置、および検証支援方法によれば、効率的かつ信頼性の高い論理検証作業をおこなうことができるという効果を奏する。
【発明を実施するための最良の形態】
【００１１】
以下に添付図面を参照して、この検証支援プログラム、検証支援装置、および検証支援方法の好適な実施の形態を詳細に説明する。この検証支援プログラム、検証支援装置、および検証支援方法では、パラメータの組み合わせ自体の依存関係の正当性を判定する。したがって、仕様と実装との間での入力ゲートの組み合わせの一貫性を判定することができ、一貫性のない組み合わせについて警告する。
【００１２】
これにより、入力ゲートの組み合わせ自体の依存関係の正当性を確認することができ、仕様を元に作成したパラメータの組み合わせを、実装から抽出した情報を用いて改善することができる。なお、パラメータとは、入力信号が与えられる入力ゲート（たとえば、入力端子）である。
【００１３】
本実施の形態では、（１）実装上の入力ゲートの組み合わせを構成する入力ゲート間の実装上の関連性の見積もりと、（２）仕様の関連性と（１）から見積もられた実装の関連性との一貫性チェックとをおこなう。
【００１４】
まず、（１）の実装上の関連性の見積もりについて説明する。入力信号が与えられる入力ゲートの組み合わせにおいて、入力ゲートから出力ゲート（出力端子）方向に向かって信号をたどり、出力ゲートまでのゲートの集合となる部分回路を入力ゲートごとに検出する。この部分回路を出力コーンと称す。また、一対の出力コーンに共通するゲート集合を共通出力コーンと称す。共通出力コーンの大きさから入力ゲートの組み合わせを構成する入力ゲート間の関連性を見積もる。
【００１５】
図１は、実装上の関連性の見積もり（その１）を示す説明図である。図１の左側は、入力ゲートＧａ，Ｇｂ間の実装上の関連性を示している。入力ゲートＧａには入力信号ｓ１が与えられる。入力信号ｓ１は、入力ゲートＧａから出力ゲート方向に伝播して出力ゲートに到達する。これにより、出力コーンＣａが得られる。同様に、入力ゲートＧｂには入力信号ｓ２が与えられる。入力信号ｓ２は、入力ゲートＧｂから出力ゲート方向に伝播して出力ゲートに到達する。これにより、出力コーンＣｂが得られる。共通出力コーンＣａｂ（図１中、ハッチングで表記）は、出力コーンＣａと出力コーンＣｂとの間でゲートを共有する領域である。
【００１６】
図１の右側は、入力ゲートＧａ，Ｇｃ間の実装上の関連性を示している。入力ゲートＧａには入力信号ｓ１が与えられる。入力信号ｓ１は、入力ゲートＧａから出力ゲート方向に伝播して出力ゲートに到達する。これにより、出力コーンＣａが得られる。同様に、入力ゲートＧｃには入力信号ｓ３が与えられる。入力信号ｓ３は、入力ゲートＧｃから出力ゲート方向に伝播して出力ゲートに到達する。これにより、出力コーンＣｃが得られる。共通出力コーンＣａｃ（図１中、ハッチングで表記）は、出力コーンＣａと出力コーンＣｃとの間でゲートを共有する領域である。
【００１７】
図１では、共通出力コーンＣａｂ，Ｃａｃは、その面積の大きさにより内部に存在するゲート数の多さを表現している。したがって、共通出力コーンＣａｂが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｂ）が、共通出力コーンＣａｃが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｃ）よりも関連性が強いこととなる。
【００１８】
図２は、実装上の関連性の見積もり（その２）を示す説明図である。図２の右側において、入力ゲートＧｄには入力信号ｓ４が与えられる。入力信号ｓ４は、入力ゲートＧｄから出力ゲート方向に伝播して出力ゲートに到達する。これにより、出力コーンＣｄが得られる。共通出力コーンＣａｄ（図２中、ハッチングで表記）は、出力コーンＣａと出力コーンＣｄとの間でゲートを共有する領域である。図２では、共通出力コーンＣａｂ，Ｃａｄを取る際の基底として、指定ゲートに限定している。指定ゲートとは、レジスタのような記憶素子や有限状態機械のほか、ゲート種に限らずユーザにより指定されたゲートでもよい。図２中、黒点は指定ゲートを示している。
【００１９】
図２でも、共通出力コーンＣａｂ，Ｃａｄは、その面積の大きさにより内部に存在するゲート数の多さを表現している。共通出力コーンＣａｄは共通出力コーンＣａｂよりもゲート数が多いが、指定ゲート数は共通出力コーンＣａｂの方が多いため、共通出力コーンＣａｂが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｂ）が、共通出力コーンＣａｄが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｄ）よりも関連性が強いこととなる。
【００２０】
図３は、実装上の関連性の見積もり（その３）を示す説明図である。図３では、両入力ゲートから共通出力コーン内の最前段のゲートまでのゲート段数により、関連性を見積もる。左側において、入力ゲートＧａ，Ｇｂからの入力信号ｓ１，ｓ２が到達する共通出力コーンＣａｂ内の最前段のゲートＧａｂまでのゲート段数はそれぞれ、５と４である。このうち、ゲート段数が大きい方となる入力ゲートＧａ〜ゲートＧａｂのゲート段数：５を採用する。
【００２１】
右側も同様に、入力ゲートＧａ，Ｇｃからの入力信号ｓ１，ｓ３が到達する共通出力コーンＣａｃ内の最前段のゲートＧａｃまでのゲート段数はそれぞれ、３と２である。このうち、ゲート段数が大きい方となる入力ゲートＧａ〜ゲートＧａｃのゲート段数：３を採用する。ゲート段数の場合、少ない方が関連性が強くなる。図３の場合、共通出力コーンＣａｃが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｃ）が、共通出力コーンＣａｂが得られた入力ゲートの組み合わせ（Ｇａ，Ｇｂ）よりも関連性が強いこととなる。
【００２２】
つぎに、（２）仕様の関連性と実装の関連性との一貫性チェックについて説明する。一貫性チェックでは、仕様から求めた入力ゲートの組み合わせの関連性と実装から求めた入力ゲートの組み合わせの関連性とを入力ゲートの同一の組み合わせで比較する。
【００２３】
図４は、仕様の関連性と実装の関連性との一貫性チェックを示す説明図である。図４では、関連性強度を『強』、『弱』、『無し』の３パターンに分けている。なお、仕様から求めた入力ゲートの組み合わせの関連性強度は、『強』、『弱』、『無し』の３パターンから選択される。どのパターンを選択するかは仕様の内容に応じてユーザが決定する。
【００２４】
図４において、仕様と実装で、関連性強度が一致する場合、仕様と実装とで一貫性があることがわかる。また、仕様と実装のうち一方が『強』で他方が『弱』である場合、一貫性がないため、警告する。また、仕様が『強』または『弱』で実装が『無し』の場合、実装に漏れがある可能性があるため、警告する。一方、実装が『強』または『弱』で仕様が『無し』の場合、仕様には記載がなくても実装すると関連する場合もあるため、参考程度に警告する。
【００２５】
（検証支援装置の概略構成）
図５は、本実施の形態の検証支援装置の概略構成を示す説明図である。検証支援装置５００は、上述した（１）実装上の入力ゲートの組み合わせを構成する入力ゲート間の実装上の関連性の見積もりと、（２）仕様の関連性と（１）から見積もられた実装の関連性との一貫性チェックとを実行する。そのため、検証対象の実装記述５０１と検証対象の仕様に基づく入力ゲートの組み合わせが記述されたパラメータファイル５０２を入力する。そして、図１〜図４に示した処理を実行して、検証結果５０３として図４の比較結果を出力する。
【００２６】
（検証支援装置５００のハードウェア構成）
図６は、実施の形態にかかる検証支援装置５００のハードウェア構成を示すブロック図である。図６において、検証支援装置５００は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）６０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）６０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）６０３と、磁気ディスクドライブ６０４と、磁気ディスク６０５と、光ディスクドライブ６０６と、光ディスク６０７と、ディスプレイ６０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）６０９と、キーボード６１０と、マウス６１１と、スキャナ６１２と、プリンタ６１３と、を備えている。また、各構成部はバス６００によってそれぞれ接続されている。
【００２７】
ここで、ＣＰＵ６０１は、検証支援装置５００の全体の制御を司る。ＲＯＭ６０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ６０３は、ＣＰＵ６０１のワークエリアとして使用される。磁気ディスクドライブ６０４は、ＣＰＵ６０１の制御にしたがって磁気ディスク６０５に対するデータのリード／ライトを制御する。磁気ディスク６０５は、磁気ディスクドライブ６０４の制御で書き込まれたデータを記憶する。
【００２８】
光ディスクドライブ６０６は、ＣＰＵ６０１の制御にしたがって光ディスク６０７に対するデータのリード／ライトを制御する。光ディスク６０７は、光ディスクドライブ６０６の制御で書き込まれたデータを記憶したり、光ディスク６０７に記憶されたデータをコンピュータに読み取らせたりする。
【００２９】
ディスプレイ６０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ６０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００３０】
インターフェース（以下、「Ｉ／Ｆ」と略する。）６０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク６１４に接続され、このネットワーク６１４を介して他の装置に接続される。そして、Ｉ／Ｆ６０９は、ネットワーク６１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ６０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００３１】
キーボード６１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス６１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００３２】
スキャナ６１２は、画像を光学的に読み取り、検証支援装置５００内に画像データを取り込む。なお、スキャナ６１２は、ＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ６１３は、画像データや文書データを印刷する。プリンタ６１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００３３】
図７は、図５に示した検証対象の実装記述５０１の記述例を示す説明図である。この実装記述は、Ｖｅｒｉｌｏｇ−ＨＤＬ（Ｈａｒｄｗａｒｅ  Ｄｅｓｃｒｉｐｔｉｏｎ  Ｌａｎｇｕａｇｅ）により記述されている。図７中、Ｇ０〜Ｇ１８は、ゲートを示している。特に、Ｇ０〜Ｇ３は入力ゲート、Ｇ７，Ｇ１６，Ｇ１８は出力ゲートを示している。ｗ４，ｗ５，ｗ８〜１４はゲート間の信号線を示している。
【００３４】
図８は、図５に示したパラメータファイル５０２の記述例を示す説明図である。パラメータファイル５０２には、検証対象の仕様に基づく入力ゲートの組み合わせとして、パラメータセットＰ１〜Ｐ３が記述されている。パラメータセットＰ１は、仕様に基づく入力ゲートＧ０，Ｇ１の組み合わせであり、パラメータセットＰ２は、仕様に基づく入力ゲートＧ２，Ｇ３の組み合わせであり、パラメータセットＰ３は、仕様に基づく入力ゲートＧ０，Ｇ２の組み合わせである。
【００３５】
（検証支援装置５００の機能的構成）
図９は、本実施の形態にかかる検証支援装置５００の機能的構成を示すブロック図である。検証支援装置５００は、取得部９０１と、特定部９０２と、第１の検出部９０３と、第２の検出部９０４と、算出部９０５と、決定部９０６と、設定部９０７と、判断部９０８と、出力部９０９と、を含む構成である。この制御部となる機能（取得部９０１〜出力部９０９）は、具体的には、たとえば、図６に示したＲＯＭ６０２、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶されたプログラムをＣＰＵ６０１に実行させることにより、または、Ｉ／Ｆ６０９により、その機能を実現する。
【００３６】
取得部９０１は、検証対象の実装記述５０１やパラメータファイル５０２を取得する機能を有する。具体的には、たとえば、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶された実装記述を読み出したり、実装記述５０１が外部から受信する。
【００３７】
図１０は、実装記述５０１およびパラメータファイル５０２の取得例を示す説明図である。図１０において、ゲートＧ０〜Ｇ３は入力ゲート群ＩＧである。ゲートＧ４，Ｇ５，Ｇ９，Ｇ１０は、第１の論理演算ブロックＬＢ１である。ゲートＧ６，Ｇ８，Ｇ１１は、第１の記憶素子（レジスタ）群Ｒ１である。ゲートＧ１２〜Ｇ１４は、第２の論理演算ブロックＬＢ２である。ゲートＧ１５，Ｇ１７は、第２の記憶素子（レジスタ）群Ｒ２である。ゲートＧ７，Ｇ１６，Ｇ１８は出力ゲート群ＯＧである。
【００３８】
特定部９０２は、取得部９０１によって取得された実装記述５０１に基づいて、入力信号が入力される検証対象の入力ゲートの組み合わせを特定する機能を有する。具体的には、たとえば、実装記述５０１の“ｉｎｐｕｔ”の行に記述されている“Ｇ０，Ｇ１，Ｇ２，Ｇ３”から入力ゲートの組み合わせを特定する。この場合では、（Ｇ０，Ｇ１），（Ｇ０，Ｇ２），（Ｇ０，Ｇ３），（Ｇ１，Ｇ２），（Ｇ１，Ｇ３），（Ｇ２，Ｇ３）が特定される。特定された組み合わせ（Ｇ０，Ｇ１）〜（Ｇ２，Ｇ３）は、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００３９】
第１の検出部９０３は、特定部９０２によって特定された入力ゲートの組み合わせを構成する各入力ゲートから各入力信号が検証対象の出力ゲートに到達するまでのゲートの集合となる一対の出力コーンを、入力ゲートの組み合わせごとに検出する機能を有する。具体的には、図１〜図３に示したように、入力ゲートＧａ〜Ｇｄごとに出力コーンＣａ〜Ｃｄを検出する。より具体的には、記憶領域から入力ゲートの組み合わせ（Ｇ０，Ｇ１）〜（Ｇ２，Ｇ３）を読み出し、１つ選択する。そして、選択された組み合わせを構成する入力ゲートから出力ゲート方向に向かって、出力先となるゲートをたどることにより、出力コーンを特定する。
【００４０】
たとえば、図１０において、入力ゲートＧ０の出力先を順次たどると、Ｇ０→Ｇ５→Ｇ６→Ｇ７となる。したがって、ゲート集合｛Ｇ５，Ｇ６，Ｇ７｝が入力ゲートＧ０の出力コーンとなる。同様に、入力ゲートＧ１の場合、Ｇ１→Ｇ５→Ｇ６→Ｇ７というルートと、Ｇ１→Ｇ４→Ｇ８→Ｇ１２→Ｇ１３→Ｇ１５→Ｇ１６というルートと、Ｇ１→Ｇ４→Ｇ８→Ｇ１２→Ｇ１３→Ｇ１４→Ｇ１７→Ｇ１８というルートとが検出される。これにより、ゲート集合｛Ｇ４，Ｇ５，Ｇ６，Ｇ７，Ｇ８，Ｇ１２，Ｇ１３，Ｇ１４，Ｇ１５，Ｇ１６，Ｇ１７，Ｇ１８｝が入力ゲートＧ１の出力コーンとなる。検出された出力コーンは、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００４１】
図９において、第２の検出部９０４は、第１の検出部９０３によって検出された一対の出力コーンに共通するゲートの集合となる共通出力コーンを、入力ゲートの組み合わせごとに検出する機能を有する。具体的には、図１〜図３に示したように、出力コーンＣａ，Ｃｂから共通出力コーンＣａｂを検出したり、出力コーンＣａ，Ｃｃから共通出力コーンＣａｃを検出したり、出力コーンＣａ，Ｃｄから共通出力コーンＣａｄを検出する。
【００４２】
より具体的には、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶された入力ゲートの組み合わせに対応する１対の出力コーンを読み出す。たとえば、先の例では、入力ゲートＧ０の出力コーンと入力ゲートＧ１の出力コーンとを読み出す。そして、両出力コーンの論理積をとることで、共通出力コーンが得られる。この場合の共通出力コーンは、ゲート集合｛Ｇ５，Ｇ６，Ｇ７｝となる。検出された共通出力コーンは、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００４３】
算出部９０５は、第２の検出部９０４によって検出された共通出力コーンに基づいて、入力ゲートの組み合わせを構成する各入力ゲートの関連度を、入力ゲートの組み合わせごとに算出する機能を有する。関連度は、具体的には、たとえば、図１に示したように、共通出力コーン内のゲートの数を計数することにより得られる。また、図２に示したように、レジスタなどの記憶素子や有限状態機械、その他ユーザが指定した特定のゲートの数を計数することとしてもよい。
【００４４】
現在では、ハードウェアは一般にＲＴＬ（レジスタ転送レベル）と呼ばれる抽象度（ＡＮＤゲートやＯＲゲートといったゲートレベル（またはネットリストレベル）より一段抽象度が高い）で記述される。ＲＴＬ記述は、論理合成ツールを用いて、ゲートレベルに変換される。変換された回路に含まれるゲート（特にレジスタ以外の論理素子（組合せ論理素子））の数は論理合成ツールに与える（面積や遅延の）制約に依存して大きく変わる可能性を持つ。
【００４５】
しかし、レジスタとなるゲートは、ＲＴＬ記述上でその構造が明示されたものに限られており、レジスタに変換されるＲＴＬ記述上のゲートは特定しやすく、論理合成の制約の影響を受けにくい。また、そのようなゲートは、仕様上で、回路の動作を定義する際に使われることが多い。一様の制約で論理合成を行った場合、元のＲＴＬ記述の論理の複雑度と合成結果のゲート数とに相関（論理が複雑なほどゲート数が多い）があるため、関連度を、単純に共通出力コーンに含まれるゲートの数とする。
【００４６】
一方、大きく異なる制約で合成された部分回路を含む場合、単純なゲートの数で比較するよりも、ＲＴＬ記述上のゲートと対応が取れるレジスタに着目して関連度を算出する方が実際の関連度をより良く表現していることとなる。
【００４７】
また、図３に示したように、両入力ゲートから共通出力コーン内の最前段のゲートまでのゲート段数を計数することにより、関連度を算出することとしてもよい。共通出力コーン内の最前段のゲートまでのゲート段数が少ない方が、両入力ゲートの影響を受けやすいこととなるため、両入力ゲート間の関連度が強いこととなる。すなわち、関連度が小さいほど関連度が強いこととなる。以下、関連度の算出方法について詳細に説明する。
【００４８】
図１１−１〜図１１−６は、入力ゲート間の関連度の算出方法（その１）を示す説明図である。図１１−１〜図１１−６では、共通出力コーン内のゲート数により算出する。図１１−１では、入力ゲートＧ０，Ｇ１の関連度を求めている。共通出力コーンＣ０１内には、ゲートＧ５〜Ｇ７が存在するため、この場合の関連度は「３」である。
【００４９】
図１１−２では、入力ゲートＧ１，Ｇ２の関連度を求めている。共通出力コーンＣ１２内には、ゲートＧ８，Ｇ１２〜Ｇ１８が存在するため、この場合の関連度は「８」である。図１１−３では、入力ゲートＧ１，Ｇ３の関連度を求めている。共通出力コーンＣ１３内には、ゲートＧ１２〜Ｇ１８が存在するため、この場合の関連度は「７」である。図１１−４では、入力ゲートＧ２，Ｇ３の関連度を求めている。共通出力コーンＣ２３内には、ゲートＧ１０〜Ｇ１８が存在するため、この場合の関連度は「９」である。
【００５０】
図１１−５では、入力ゲートＧ０，Ｇ２の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ２に対する出力コーンＣ２とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「０」である。図１１−６では、入力ゲートＧ０，Ｇ３の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ３に対する出力コーンＣ３とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「０」である。
【００５１】
図１２−１〜図１２−６は、入力ゲート間の関連度の算出方法（その２）を示す説明図である。図１２−１〜図１２−６では、共通出力コーン内の特定のゲートであるレジスタの数により算出する。なお、図１２−１〜図１２−６では、レジスタ（Ｆｌｉｐ−Ｆｌｏｐ）の図形には、その右上に＊が表記されている。
【００５２】
図１２−１では、入力ゲートＧ０，Ｇ１の関連度を求めている。共通出力コーンＣ０１内には、レジスタとなるゲートＧ６が存在するため、この場合の関連度は「１」である。図１２−２では、入力ゲートＧ１，Ｇ２の関連度を求めている。共通出力コーンＣ１２内には、レジスタとなるゲートＧ８，Ｇ１５，Ｇ１７が存在するため、この場合の関連度は「３」である。
【００５３】
図１２−３では、入力ゲートＧ１，Ｇ３の関連度を求めている。共通出力コーンＣ１３内には、レジスタとなるゲートＧ１５，Ｇ１７が存在するため、この場合の関連度は「２」である。図１２−４では、入力ゲートＧ２，Ｇ３の関連度を求めている。共通出力コーンＣ２３内には、ゲートＧ１１，Ｇ１５，Ｇ１７が存在するため、この場合の関連度は「３」である。
【００５４】
図１２−５では、入力ゲートＧ０，Ｇ２の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ２に対する出力コーンＣ２とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「０」である。
【００５５】
図１２−６では、入力ゲートＧ０，Ｇ３の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ３に対する出力コーンＣ３とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「０」である。
【００５６】
図１３−１〜図１３−６は、入力ゲート間の関連度の算出方法（その３）を示す説明図である。図１３−１〜図１３−６では、共通出力コーン内の最前段のゲートまでのゲート段数により算出する。なお、図１３−１〜図１３−６では、入力ゲートから最前段までのゲートの図形には、その右上に＊が表記されている。また、対象となる入力ゲートは２つあるため、入力ゲートからのゲート段数も２とおり算出されるが、ゲート段数が多いほうを採用する。
【００５７】
図１３−１では、入力ゲートＧ０，Ｇ１の関連度を求めている。共通出力コーンＣ０１内には、最前段のゲートＧ５が存在するため、入力ゲートＧ０からのゲート段数は「１」、入力ゲートＧ１からのゲート段数も「１」である。したがって、この場合の関連度は「１」である。
【００５８】
図１３−２では、入力ゲートＧ１，Ｇ２の関連度を求めている。共通出力コーンＣ１２内には、最前段のゲートＧ８が存在するため、入力ゲートＧ１からのゲート段数は「２」、入力ゲートＧ２からのゲート段数は「１」である。したがって、この場合の関連度は「２」である。
【００５９】
図１３−３では、入力ゲートＧ１，Ｇ３の関連度を求めている。共通出力コーンＣ１３内には、最前段のゲートＧ１２が存在するため、入力ゲートＧ１からのゲート段数は「３」、入力ゲートＧ３からのゲート段数は「４」である。したがって、この場合の関連度は「４」である。
【００６０】
図１３−４では、入力ゲートＧ２，Ｇ３の関連度を求めている。共通出力コーンＣ２３内には、最前段のゲートＧ１０が存在するため、入力ゲートＧ２からのゲート段数は「１」、入力ゲートＧ３からのゲート段数は「２」である。したがって、この場合の関連度は「２」である。
【００６１】
図１３−５では、入力ゲートＧ０，Ｇ２の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ２に対する出力コーンＣ２とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「∞」である。
【００６２】
図１３−６では、入力ゲートＧ０，Ｇ３の関連度を求めている。入力ゲートＧ０に対する出力コーンＣ０と入力ゲートＧ３に対する出力コーンＣ３とは交差しないため、共通出力コーンは存在しない。したがって、この場合の関連度は「∞」である。なお、算出された関連度は、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００６３】
また、図９において、決定部９０６は、算出部９０５によって算出された算出結果に応じた関連性強度を、入力ゲートの組み合わせごとに決定する機能を有する。関連性強度とは、各関連度を基にした相対的な評価指標である。具体的には、たとえば、注目する関連度を他の関連度と比較して、関連性の有無を判断する。たとえば、関連性がない場合、その入力ゲートの組み合わせについて、関連性強度：『無し』とする。
【００６４】
一方、関連性強度がある場合、関連度が最大となる入力ゲートの組み合わせについて、関連性強度：『強』とする。なお、それ以外の入力ゲートの組み合わせについては、関連性強度：『弱』とする。また、関連性の有無については、関連度の値により判断する。
【００６５】
図１４は、関連性強度の決定結果を示す説明図である。図１４中、（Ａ）は図１１−１〜図１１−６の例についての関連性強度を示すグラフであり、（Ｂ）は図１２−１〜図１２−６の例についての関連性強度を示すグラフであり、（Ｃ）は図１３−１〜図１３−６の例についての関連性強度を示すグラフである。
【００６６】
グラフ１４０１では、ゲートの数が多いほど関連度が高くなる。したがって、関連度の値が「０」の入力ゲートの組み合わせ（Ｇ０，Ｇ２），（Ｇ０，Ｇ３）については、関連性強度：『無し』とする。そして、関連度の値が最大となる入力ゲートの組み合わせ（Ｇ２，Ｇ３）については、関連性強度：『強』とする。また、それ以外の残余の入力ゲートの組み合わせ（Ｇ０，Ｇ１），（Ｇ１，Ｇ２），（Ｇ１，Ｇ３）については、関連性強度：『弱』とする。
【００６７】
同様に、グラフ１４０２でも、レジスタの数が多いほど関連度が高くなる。したがって、関連度の値が「０」の入力ゲートの組み合わせ（Ｇ０，Ｇ２），（Ｇ０，Ｇ３）については、関連性強度：『無し』とする。そして、関連度の値が最大となる入力ゲートの組み合わせ（Ｇ０，Ｇ１），（Ｇ１，Ｇ２）については、関連性強度：『強』とする。また、それ以外の残余の入力ゲートの組み合わせ（Ｇ１，Ｇ３），（Ｇ２，Ｇ３）については、関連性強度：『弱』とする。
【００６８】
一方、グラフ１４０３では、ゲート段数が少ないほど関連度が高くなる。したがって、関連度の値が「∞」の入力ゲートの組み合わせ（Ｇ０，Ｇ２），（Ｇ０，Ｇ３）については、関連性強度：『無し』とする。そして、関連度の値が最小となる入力ゲートの組み合わせ（Ｇ０，Ｇ１）については、関連性強度：『強』とする。また、それ以外の残余の入力ゲートの組み合わせ（Ｇ１，Ｇ２），（Ｇ１，Ｇ３），（Ｇ２，Ｇ３）については、関連性強度：『弱』とする。なお、決定された関連性強度は、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００６９】
また、図９において、設定部９０７は、検証対象の仕様に基づく入力ゲートの組み合わせに対して特定の関連性強度を設定する機能を有する。具体的には、パラメータファイル５０２に記述されている仕様に基づく入力ゲートの組み合わせＰ１〜Ｐ３については、自動的に特定の関連性強度を付与する。
【００７０】
ここでは、パラメータファイル５０２に記述された仕様に基づく入力ゲートの組み合わせＰ１〜Ｐ３は、ユーザが仕様を分析した結果、重要な組み合わせであると判断したため、入力ゲートの組み合わせＰ１〜Ｐ３については、すべて、関連性強度：『強』とする。なお、ユーザが、“関連性はあるけれどもそれほど重要ではない”と分析した場合は、関連性強度：『弱』に設定することもできる。
【００７１】
さらに、“関連性はありえない”と分析した場合は、関連性強度：『無し』とすることもできる。いずれにしても、ユーザが任意に設定することができる。なお、設定された関連性強度は、仕様に基づく入力ゲートの組み合わせＰ１〜Ｐ３とともに、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００７２】
また、図９において、判断部９０８は、入力ゲートの組み合わせごとに、設定部９０７によって設定された特定の関連性強度と、決定部９０６によって決定された関連性強度とが一致するか否かを判断する機能を有する。具体的には、たとえば、図４に示したように、同一の入力ゲートの組み合わせごとに、関連性強度の一致判定をおこなう。
【００７３】
一致する場合（図４の「ＯＫ」）、その入力ゲートの組み合わせについては、仕様と実装とで一貫性があることがわかる。一方、不一致の場合（図４の「警告」）、その入力ゲートの組み合わせについては、仕様と実装とで一貫性がないことがわかる。なお、判断結果は、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域に記憶される。
【００７４】
出力部９０９は、判断部９０８によって判断された判断結果を出力する機能を有する。出力形式としては、ディスプレイ６０８への表示、プリンタ６１３からの印刷出力、Ｉ／Ｆ６０９を介した外部装置への送信、ＲＡＭ６０３、磁気ディスク６０５、光ディスク６０７などの記憶領域への格納がある。
【００７５】
図１５は、仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ａ）に示した関連性強度との一致判定および出力内容を示す説明図である。図１５中、（Ａ）は、仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ａ）に示した関連性強度との一致判定を示している。グラフ１５００は、仕様に基づく入力ゲートの組み合わせの関連性強度を示している。
【００７６】
両グラフ１４０１，１５００を比較すると、（Ｇ２，Ｇ３）が関連性強度：『強』で一致、（Ｇ０，Ｇ３）が関連性強度：『無し』で一致、それ以外の組み合わせは不一致であることがわかる。（Ｂ）は、出力部９０９からの出力データ１５０１を示している。出力データは、所定のフォーマットに、（Ａ）の一致判定結果を反映した内容がはめ込まれて、出力部９０９により出力される。
【００７７】
図１６は、仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ｂ）に示した関連性強度との一致判定および出力内容を示す説明図である。図１６中、（Ａ）は、仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ｂ）に示した関連性強度との一致判定を示している。
【００７８】
両グラフ１４０２，１５００を比較すると、（Ｇ０，Ｇ１）が関連性強度：『強』で一致、（Ｇ０，Ｇ３）が関連性強度：『無し』で一致、それ以外の組み合わせは不一致であることがわかる。（Ｂ）は、出力部９０９からの出力データ１６０１を示している。出力データは、所定のフォーマットに、（Ａ）の一致判定結果を反映した内容がはめ込まれて、出力部９０９により出力される。
【００７９】
（検証支援処理手順）
図１７および図１８は、本実施の形態にかかる検証支援装置５００による検証支援処理手順を示すフローチャートである。まず、図１７において、取得部９０１により検証対象の実装記述５０１を取得する（ステップＳ１７０１）。つぎに、実装記述５０１の記述内容から入力ゲートの組み合わせを生成する（ステップＳ１７０２）。そして、生成された入力ゲートの組み合わせ群のうち未選択の組み合わせがあるか否かを判断する（ステップＳ１７０３）。
【００８０】
未選択の組み合わせがある場合（ステップＳ１７０３：Ｙｅｓ）、未選択の組み合わせを１つ選択する（ステップＳ１７０４）。そして、第１の検出部９０３により、選択された入力ゲートの組み合わせを構成する各入力ゲートの出力コーンを検出する（ステップＳ１７０５）。このあと、第２の検出部９０４により、第１の検出部９０３により検出された両出力コーンの共通出力コーンの検出処理を実行する（ステップＳ１７０６）。
【００８１】
そして、算出部９０５により、検出された共通出力コーンに基づいて、選択された入力ゲートの組み合わせの関連度を算出して（ステップＳ１７０７）、ステップＳ１７０３に戻る。一方、ステップＳ１７０３において、未選択の組み合わせがない場合（ステップＳ１７０３：Ｎｏ）、決定部９０６により、各入力ゲートの組み合わせについて関連性強度を決定して（ステップＳ１７０８）、図１８のステップＳ１８０１に移行する。
【００８２】
ステップＳ１７０８のあと、図１８において、仕様に基づく入力ゲートの組み合わせを取得する（ステップＳ１８０１）。そして、設定部９０７により、取得された仕様に基づく入力ゲートの組み合わせに対し、特定の関連性強度（たとえば、『強』）を設定する（ステップＳ１８０２）。そして、未選択の入力ゲートの組み合わせがあるか否かを判断する（ステップＳ１８０３）。
【００８３】
未選択の組み合わせがある場合（ステップＳ１８０３：Ｙｅｓ）、未選択の組み合わせを１つ選択する（ステップＳ１８０４）。そして、判断部９０８により、選択された組み合わせについて、実装から求めた関連性強度（ステップＳ１７０８で得た関連性強度）と仕様から求めた関連性強度（ステップＳ１８０２で得た関連性強度）との一致判定をおこなう（ステップＳ１８０５）。
【００８４】
このあと、判定結果を記憶領域に保存して（ステップＳ１８０６）、ステップＳ１８０３に戻る。一方、ステップＳ１８０３において、未選択の組み合わせがない場合（ステップＳ１８０３：Ｎｏ）、図１７や図１８に示したような出力データを生成し（ステップＳ１８０７）、出力部９０９により出力する（ステップＳ１８０８）。これにより、一連の処理を終了する。
【００８５】
このように、本実施の形態によれば、パラメータとなる入力ゲートの組み合わせ自体の依存関係の正当性を判定することができる。したがって、仕様と実装との間での入力ゲートの組み合わせの一貫性を判定することができ、一貫性のない組み合わせについて警告することができる。これにより、入力ゲートの組み合わせ自体の依存関係の正当性を確認することができ、仕様を元に作成した入力ゲート（に与えられる信号）の組み合わせを、実装から抽出した情報を用いて改善することができる。したがって、効率的かつ信頼性の高い論理検証作業をおこなうことができる。
【００８６】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な媒体であってもよい。
【図面の簡単な説明】
【００８７】
【図１】実装上の関連性の見積もり（その１）を示す説明図である。
【図２】実装上の関連性の見積もり（その２）を示す説明図である。
【図３】実装上の関連性の見積もり（その３）を示す説明図である。
【図４】仕様の関連性と実装の関連性との一貫性チェックを示す説明図である。
【図５】本実施の形態の検証支援装置の概略構成を示す説明図である。
【図６】実施の形態にかかる検証支援装置のハードウェア構成を示すブロック図である。
【図７】図５に示した検証対象の実装記述の記述例を示す説明図である。
【図８】図５に示したパラメータファイルの記述例を示す説明図である。
【図９】本実施の形態にかかる検証支援装置の機能的構成を示すブロック図である。
【図１０】実装記述およびパラメータファイルの取得例を示す説明図である。
【図１１−１】入力ゲートＧ０，Ｇ１間の関連度の算出方法（その１）を示す説明図である。
【図１１−２】入力ゲートＧ１，Ｇ２間の関連度の算出方法（その１）を示す説明図である。
【図１１−３】入力ゲートＧ１，Ｇ３間の関連度の算出方法（その１）を示す説明図である。
【図１１−４】入力ゲートＧ２，Ｇ３間の関連度の算出方法（その１）を示す説明図である。
【図１１−５】入力ゲートＧ０，Ｇ２間の関連度の算出方法（その１）を示す説明図である。
【図１１−６】入力ゲートＧ０，Ｇ３間の関連度の算出方法（その１）を示す説明図である。
【図１２−１】入力ゲートＧ０，Ｇ１間の関連度の算出方法（その２）を示す説明図である。
【図１２−２】入力ゲートＧ１，Ｇ２間の関連度の算出方法（その２）を示す説明図である。
【図１２−３】入力ゲートＧ１，Ｇ３間の関連度の算出方法（その２）を示す説明図である。
【図１２−４】入力ゲートＧ２，Ｇ３間の関連度の算出方法（その２）を示す説明図である。
【図１２−５】入力ゲートＧ０，Ｇ２間の関連度の算出方法（その２）を示す説明図である。
【図１２−６】入力ゲートＧ０，Ｇ３間の関連度の算出方法（その２）を示す説明図である。
【図１３−１】入力ゲートＧ０，Ｇ１間の関連度の算出方法（その３）を示す説明図である。
【図１３−２】入力ゲートＧ１，Ｇ２間の関連度の算出方法（その３）を示す説明図である。
【図１３−３】入力ゲートＧ１，Ｇ３間の関連度の算出方法（その３）を示す説明図である。
【図１３−４】入力ゲートＧ２，Ｇ３間の関連度の算出方法（その３）を示す説明図である。
【図１３−５】入力ゲートＧ０，Ｇ２間の関連度の算出方法（その３）を示す説明図である。
【図１３−６】入力ゲートＧ０，Ｇ３間の関連度の算出方法（その３）を示す説明図である。
【図１４】関連性強度の決定結果を示す説明図である。
【図１５】仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ａ）に示した関連性強度との一致判定および出力内容を示す説明図である。
【図１６】仕様に基づく入力ゲートの組み合わせの関連性強度と図１４の（Ｂ）に示した関連性強度との一致判定および出力内容を示す説明図である。
【図１７】本実施の形態にかかる検証支援装置による検証支援処理手順を示すフローチャート（前半）である。
【図１８】本実施の形態にかかる検証支援装置による検証支援処理手順を示すフローチャート（後半）である。
【符号の説明】
【００８８】
５００  検証支援装置
５０１  実装記述
５０２  パラメータファイル
５０３  検証結果
９０１  取得部
９０２  特定部
９０３  第１の検出部
９０４  第２の検出部
９０５  算出部
９０６  決定部
９０７  設定部
９０８  判断部
９０９  出力部
【図１】
0004957641.tif 000002
【図２】
0004957641.tif 000003
【図３】
0004957641.tif 000004
【図４】
0004957641.tif 000005
【図５】
0004957641.tif 000006
【図６】
0004957641.tif 000007
【図７】
0004957641.tif 000008
【図８】
0004957641.tif 000009
【図９】
0004957641.tif 000010
【図１０】
0004957641.tif 000011
【図１１−１】
0004957641.tif 000012
【図１１−２】
0004957641.tif 000013
【図１１−３】
0004957641.tif 000014
【図１１−４】
0004957641.tif 000015
【図１１−５】
0004957641.tif 000016
【図１１−６】
0004957641.tif 000017
【図１２−１】
0004957641.tif 000018
【図１２−２】
0004957641.tif 000019
【図１２−３】
0004957641.tif 000020
【図１２−４】
0004957641.tif 000021
【図１２−５】
0004957641.tif 000022
【図１２−６】
0004957641.tif 000023
【図１３−１】
0004957641.tif 000024
【図１３−２】
0004957641.tif 000025
【図１３−３】
0004957641.tif 000026
【図１３−４】
0004957641.tif 000027
【図１３−５】
0004957641.tif 000028
【図１３−６】
0004957641.tif 000029
【図１４】
0004957641.tif 000030
【図１５】
0004957641.tif 000031
【図１６】
0004957641.tif 000032
【図１７】
0004957641.tif 000033
【図１８】
0004957641.tif 000034