(57)【要約】【課題】コードカバレッジの上限を見積もることにより、検証シナリオの機能に関する検証網羅性の向上を図り、ＬＳＩの設計障害の正確かつ効率的な検出を図ること。【解決手段】検証支援装置２００は、取得部２０１で検証シナリオＳが取得された場合、置換部２０２で検証シナリオＳ内の可変の値を不定値ｘに置換する。第１の実行部２１１で入力パターンＰＸを用いて論理シミュレーションを実行する。この実行結果から決定部２０５でコードカバレッジ上限情報ＣＭを生成する。設定部２０３で検証シナリオＳ内の可変の値に任意の論理値を与えることによって入力パターンＰ１，Ｐ２を設定する。第２の実行部２１２で入力パターンＰ１，Ｐ２を用いて論理シミュレーションを実行する。生成部２０６で入力パターンＰ１，Ｐ２からコードカバレッジＣＣを生成し、算出部２０７でコードカバレッジ上限情報ＣＭに対するコードカバレッジＣＣの達成度を算出する。【選択図】        図２
2006190209.tif 000002
【特許請求の範囲】
【請求項１】
検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得させる取得工程と、
前記取得工程によって取得された回路情報に前記取得工程によって取得された検証シナリオを与えることによって、論理シミュレーションを実行させる第１の実行工程と、
前記第１の実行工程によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定させる決定工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【請求項２】
前記検証シナリオの可変の値に任意の論理値を与えることによって入力パターンを設定させる設定工程と、
前記設定工程によって設定された入力パターンを前記回路情報に与えることによって、論理シミュレーションを実行させる第２の実行工程と、
前記第２の実行工程によって実行された実行結果に基づいて、前記回路情報に関するコードカバレッジを生成させる生成工程と、
前記決定工程によって決定されたコードカバレッジ上限情報に対する、前記生成工程によって生成されたコードカバレッジの達成度を算出させる算出工程と、
をコンピュータに実行させることを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
請求項１または２に記載の検証支援プログラムを記録したコンピュータに読み取り可能な記録媒体。
【請求項４】
検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得する取得手段と、
前記取得手段によって取得された回路情報に前記取得手段によって取得された検証シナリオを与えることによって、論理シミュレーションを実行する実行手段と、
前記実行手段によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定する決定手段と、
を備えることを特徴とする検証支援装置。
【請求項５】
検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得する取得工程と、
前記取得工程によって取得された回路情報に前記取得工程によって取得された検証シナリオを与えることによって、論理シミュレーションを実行する実行工程と、
前記実行工程によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定する決定工程と、
を含んだことを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、ハードウェアが正しく論理設計されていることを確認する論理シミュレーションにおける論理検証を支援する検証支援プログラム、記録媒体、検証支援装置、および検証支援方法に関し、特に、シミュレーションパターンが十分であるか否かの指標である検証カバレッジを導出し、そのカバレッジに基づいた論理検証を支援する検証支援プログラム、記録媒体、検証支援装置、および検証支援方法に関する。
【背景技術】
【０００２】
従来から、論理シミュレーションのパターンが十分であるか否かの指標である検証カバレッジには、大きく分類して２種類のものが広く使われている。一つは検証対象の外部仕様を基準にしたもので、検証対象が持つべき機能を網羅しようとする「機能カバレッジ」である。
【０００３】
もう一つは検証対象のソースコードを基準にした「コードカバレッジ」である。コードカバレッジとしては、ソースコードのすべての行を実行しようとするラインカバレッジ、ソースコードに記載されたすべての信号線を変化させようとするトグルカバレッジ、ソースコードから有限状態機械（ＦＳＭ）を決定してその状態や状態遷移を網羅しようとするＦＳＭカバレッジなどが知られている。
【０００４】
また従来から、上述した機能カバレッジやコードカバレッジが用いられている。機能カバレッジを用いた従来例としては、たとえば、特許文献１のカバレッジ算出方法が挙げられる。このカバレッジ算出方法では、カバレッジの基準となるプロパティと実際に実行されたテストパターンとを入力し、プロパティに対応する有効テストパターンがどれだけカバーされたかを算出する。
【０００５】
また、機能カバレッジを計測する方法としては、下記特許文献２の算出方法が挙げられる。論理シミュレーションにおいて機能カバレッジを１００％にすることで、外部から見て要求されるすべての機能が一通り正しく実装されているかどうかを確かめることができる。
【０００６】
また、コードカバレッジを用いた従来例としては、特許文献３のカバレッジ方式が挙げられる。このカバレッジ方式は、論理シミュレーション中の信号変化に関する情報を記録し、全信号を動作させる。
【０００７】
【特許文献１】特開２００４−７０４５７号公報
【特許文献２】特開平３−０６２１７２号公報
【特許文献３】特開昭６３−２０５７６０号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかしながら、上述した機能カバレッジにおいて外部から見ると区別されないケースでも、実際のハードウェアの内部実装では、サブケースに細分化されて処理されている可能性がある。本来はそれらをすべてカバーするべきであるが、機能カバレッジではそれらの一つをカバーするだけになり、他のサブケースでも機能が正しく実装されているかどうかの検証が十分ではないという問題があった。
【０００９】
たとえば、つぎのような外部仕様を持った論理回路があるとする。
（１）回路は５つの入力端子Ａ，Ｂ，Ｃ，Ｄ，Ｅと１つの出力端子Ｆを持つ。
（２）Ａの値が０のときは、ＢとＣの２つの入力値に論理関数ｆ１を適用した結果ｆ１（Ｂ，Ｃ）をＦに出力する機能（機能１）を持つ。
（３）Ａの値が１のときは、ＤとＥの２つの入力値に論理関数ｆ２を適用した結果ｆ２（Ｄ，Ｅ）をＦに出力する機能（機能２）を持つ。
【００１０】
この外部仕様から、機能カバレッジとして「機能１を実行するパターンと機能２を実行するパターンをそれぞれ１回以上実行する」という基準が考えられる。ところが、この基準では、たとえば機能１を実行する（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，０，０，０，０）と、機能２を実行する（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（１，０，０，０，０）の２パターンについてシミュレーションするだけで、１００％のカバレッジを達成することができる。
【００１１】
これは達成すべき最低限のカバレッジ基準ではあるが、これだけで十分とは考え難い。そこで、より細分化された基準を考えるとすれば、「機能１を実行するパターンをＢとＣの値のすべての組み合わせについて、機能２を実行するパターンをＤとＥの値のすべての組み合わせについて実行する」といったものになる。この例の場合は、それも可能であるが、実際の大規模な（内部状態を持ち入力端子数の多い）論理回路では、そのようにすべての組み合わせについて実行することは現実的ではない。したがって、それらの中間的なカバレッジ基準を設定する必要がある。
【００１２】
一方、コードカバレッジを１００％にすることでソースコードの実行を一通り確認することができる。しかしながら、検証として意味を持つためには、単に実行するだけではなく最終結果に影響を与える場面で実行する必要があるが、コードカバレッジにはそのような観点からの基準が含まれていなかった。
【００１３】
たとえば、上記の論理回路について具体的に説明する。図２２は、上述した論理回路を示す回路図である。図２２において、論理回路２２００に、コードカバレッジの一種であるトグルカバレッジを導入してみる。トグルカバレッジでは、シミュレーション中に回路上のそれぞれの信号線に値の変化が起こったかどうかが算出基準になる。この例ではＡ〜Ｊの１０個の信号線があるため、カバレッジの母数は１０ということになる。
【００１４】
機能カバレッジを１００％にする２パターン（０，０，０，０，０），（１，０，０，０，０）についてシミュレーションすると、図２３および図２４のシミュレーション結果が得られる。図２３および図２４は、論理回路２２００のシミュレーション結果を示す説明図である。図２３および図２４において、値が変化した信号線はＡ，Ｈ，Ｆの３つであり、トグルカバレッジは３０％しか達成されていない。そこでパターン（１，１，１，１，１）を追加してシミュレーションすると、図２５のシミュレーション結果が得られる。図２５は、論理回路２２００のシミュレーション結果を示す説明図である。図２５においては、残りの信号線の値も変化し、トグルカバレッジ１００％を達成することができる。
【００１５】
ところがこの論理回路２２００は、Ａ＝１のときＢ、Ｃ、Ｇの値が出力Ｆに影響を与えない構成になっている。したがって、最後に追加したパターン（１，１，１，１，１）でカバーされたＢ、Ｃ、Ｇの値変化は検証の役目を果たしていない。このように、機能カバレッジやコードカバレッジを個別に達成しようとするだけでは、上記のような検証漏れを避けることができないという問題があった。
【００１６】
一方で、単純に機能カバレッジとコードカバレッジの組み合わせを網羅しようとすると、組み合わせの中には理論的に達成不可能なものが含まれる可能性があるため、どこまで網羅すれば十分であるかが判断できないという問題があった。したがって、機能カバレッジとコードカバレッジの組み合わせという考え方も実用的ではなかった。
【００１７】
たとえば、前述の例では機能カバレッジの母数が２、トグルカバレッジの母数が１０であるから２０通りの組み合わせが考えられる。しかしながら、実際には、機能１を実行する際は常にＡ＝０であるため、機能１の実行と信号Ａの値変化の組み合わせは達成不可能である。さらにＡ＝０によって信号Ｉの値も０に固定されるため、機能１の実行と信号線Ｉの値変化の組み合わせも達成不可能である。同様に、機能１と信号線Ｊの値変化、機能２と信号線ＡおよびＨの値変化の組み合わせも達成不可能である。実際の大規模回路に対しては、このように一つ一つ確認することは困難であり、現実的ではないという問題があった。
【００１８】
この発明は、上述した従来技術による問題点を解消するため、コードカバレッジの上限を見積もることにより、検証シナリオの機能に関する検証網羅性の向上を図り、ＬＳＩの設計障害の正確かつ効率的な検出を図ることができる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【００１９】
上述した課題を解決し、目的を達成するため、この発明にかかる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法は、検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得し、取得された検証シナリオを取得された回路情報に与えることによって、前記検証対象回路の論理シミュレーションを実行し、実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定することを特徴とする。
【００２０】
この発明によれば、検証シナリオに含まれているすべての入力パターンを実行した場合に達成可能と想定されるコードカバレッジを網羅することができる。したがって、コードカバレッジ上限情報を、検証対象回路の機能とソースコードの組み合わせパターンをどれだけテストしたかという検証網羅性の評価に用いることができる。
【００２１】
また、前記検証シナリオの可変の値を不定値に置換し、不定値に置換された検証シナリオを前記検証対象回路の回路情報に与えることによって、論理シミュレーションを実行し、前記回路情報内において前記不定値が伝搬した箇所を示すコードカバレッジ上限情報を決定することとしてもよい。
【００２２】
この発明によれば、不定値が伝搬した回路情報内の箇所を示すコードカバレッジ上限情報によって、検証シナリオに含まれているすべての入力パターンを実行した場合に達成可能と想定されるコードカバレッジを網羅することができる。したがって、コードカバレッジ上限情報を、検証対象回路の機能とソースコードの組み合わせパターンをどれだけテストしたかという検証網羅性の評価に用いることができる。
【００２３】
また、前記回路情報として、前記検証対象回路のＲＴＬ記述を取得し、前記検証シナリオを前記ＲＴＬ記述に与えることによって、論理シミュレーションを実行し、前記ＲＴＬ記述内において前記不定値が伝搬した箇所を示すコードカバレッジ上限情報を決定することとしてもよい。
【００２４】
この発明によれば、回路情報の選択における自由度の向上を図ることができる。したがって、検証網羅性の評価を効率的におこなうことができる。
【００２５】
また、論理シミュレーション中に、前記ＲＴＬ記述に含まれている条件分岐文において条件不成立となった場合、前記条件分岐文の分岐先となる他の条件分岐文の実行結果を不定値に変換し、変換された不定値を用いて論理シミュレーションを継続実行することとしてもよい。
【００２６】
この発明によれば、回路情報がＲＴＬ記述であってもコードカバレッジ上限情報を正確に決定することができる。したがって、コードカバレッジ上限情報を、検証対象回路の機能とソースコードの組み合わせパターンをどれだけテストしたかという検証網羅性の評価に用いることができる。
【００２７】
また、前記ＲＴＬ記述に条件分岐文がある場合、前記条件分岐文のいずれの分岐先も実行できるように前記ＲＴＬ記述を変換し、変換されたＲＴＬ記述を用いて論理シミュレーションを実行することとしてもよい。
【００２８】
この発明によれば、論理シミュレーション前にあらかじめＲＴＬ記述を検証網羅性の評価に適合するように変換することができる。したがって、論理シミュレーションの効率化およびコードカバレッジ上限情報の正確性の向上を図ることができる。
【００２９】
また、前記検証シナリオの可変の値を記号に置換し、記号に置換された検証シナリオを前記検証対象回路の回路情報に与えることによって、論理シミュレーションを実行することとしてもよい。
【００３０】
この発明によれば、論理シミュレーションにおいて記号を用いた論理式によって、伝搬箇所をあらわすことができ、コードカバレッジ上限情報の内容をより正確にあらわすことができる。これにより、検証シナリオに含まれているすべての入力パターンを実行した場合に達成可能と想定されるコードカバレッジをより正確に網羅することができる。したがって、コードカバレッジ上限情報を、検証対象回路の機能とソースコードの組み合わせパターンをどれだけテストしたかという検証網羅性の評価に用いることができる。
【００３１】
また、論理シミュレーション中に、所定数の記号からなる論理式が出現した場合、当該論理式を、当該論理式の記号数よりも少ない数の記号に変換し、変換された記号を用いて論理シミュレーションを継続実行し、前記回路情報内において前記記号が伝搬した箇所を示すコードカバレッジ上限情報を決定することとしてもよい。
【００３２】
この発明によれば、記号を用いた論理シミュレーションの高速化を図ることができる。したがって、コードカバレッジ上限情報を、検証対象回路の機能とソースコードの組み合わせパターンをどれだけテストしたかという検証網羅性の評価に用いることができる。
【００３３】
また、前記検証シナリオの可変の値に任意の論理値を与えることによって入力パターンを設定し、設定された入力パターンを前記回路情報に与えることによって、論理シミュレーションを実行し、その実行結果に基づいて、前記回路情報に関するコードカバレッジを生成し、決定されたコードカバレッジ上限情報に対する、生成されたコードカバレッジの達成度を算出することとしてもよい。
【００３４】
この発明によれば、コードカバレッジ上限情報に対するコードカバレッジの達成度を定量的に算出することができ、コードカバレッジの検証網羅性の判定基準として用いることができる。したがって、検証対象回路の設計障害を効率的に検出することができる。
【００３５】
また、算出された達成度に基づいて、コードカバレッジによる検証網羅性を判定することとしてもよい。
【００３６】
この発明によれば、判定結果からコードカバレッジの検証網羅性を評価することができる。したがって、検証対象回路の設計障害を効率的に検出することができる。
【００３７】
また、判定された判定結果に基づいて、前記検証シナリオの可変の値に前記任意の論理値とは異なる論理値を与えることによって前記入力パターンとは異なる他の入力パターンを設定し、設定された他の入力パターンを前記回路情報に与えることによって、論理シミュレーションを実行し、入力パターンを用いた実行結果と他の入力パターンを用いた実行結果とに基づいて、前記コードカバレッジとは異なる他のコードカバレッジを生成し、前記コードカバレッジ上限情報に対する、生成された他のコードカバレッジの達成度を算出することとしてもよい。
【００３８】
この発明によれば、コードカバレッジを更新して、達成度の上昇を認識することができる。したがって、達成度の上昇から、論理シミュレーションの終了時期を的確に予測することができる。
【発明の効果】
【００３９】
本発明にかかる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法によれば、コードカバレッジの上限を見積もることにより、検証シナリオの機能に関する検証網羅性の向上を図り、ＬＳＩの設計障害の正確かつ効率的な検出を図ることができるという効果を奏する。
【発明を実施するための最良の形態】
【００４０】
以下に添付図面を参照して、この発明にかかる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法の好適な実施の形態を詳細に説明する。
【００４１】
（検証支援装置のハードウェア構成）
まず、この発明の実施の形態にかかる検証支援装置のハードウェア構成について説明する。図１は、この発明の実施の形態にかかる検証支援装置のハードウェア構成を示すブロック図である。
【００４２】
図１において、検証支援装置は、ＣＰＵ１０１と、ＲＯＭ１０２と、ＲＡＭ１０３と、ＨＤＤ（ハードディスクドライブ）１０４と、ＨＤ（ハードディスク）１０５と、ＦＤＤ（フレキシブルディスクドライブ）１０６と、着脱可能な記録媒体の一例としてのＦＤ（フレキシブルディスク）１０７と、ディスプレイ１０８と、Ｉ／Ｆ（インターフェース）１０９と、キーボード１１０と、マウス１１１と、スキャナ１１２と、プリンタ１１３と、を備えている。また、各構成部はバス１００によってそれぞれ接続されている。
【００４３】
ここで、ＣＰＵ１０１は、検証支援装置の全体の制御を司る。ＲＯＭ１０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ１０３は、ＣＰＵ１０１のワークエリアとして使用される。ＨＤＤ１０４は、ＣＰＵ１０１の制御にしたがってＨＤ１０５に対するデータのリード／ライトを制御する。ＨＤ１０５は、ＨＤＤ１０４の制御で書き込まれたデータを記憶する。
【００４４】
ＦＤＤ１０６は、ＣＰＵ１０１の制御にしたがってＦＤ１０７に対するデータのリード／ライトを制御する。ＦＤ１０７は、ＦＤＤ１０６の制御で書き込まれたデータを記憶したり、ＦＤ１０７に記憶されたデータを検証支援装置に読み取らせたりする。
【００４５】
また、着脱可能な記録媒体として、ＦＤ１０７のほか、ＣＤ−ＲＯＭ（ＣＤ−Ｒ、ＣＤ−ＲＷ）、ＭＯ、ＤＶＤ（Ｄｉｇｉｔａｌ  Ｖｅｒｓａｔｉｌｅ  Ｄｉｓｋ）、メモリーカードなどであってもよい。ディスプレイ１０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ１０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００４６】
Ｉ／Ｆ１０９は、通信回線を通じてインターネットなどのネットワーク１１４に接続され、このネットワーク１１４を介して他の装置に接続される。そして、Ｉ／Ｆ１０９は、ネットワーク１１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ１０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００４７】
キーボード１１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス１１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４８】
スキャナ１１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ１１２は、ＯＣＲ機能を持たせてもよい。また、プリンタ１１３は、画像データや文書データを印刷する。プリンタ１１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００４９】
（検証支援装置の機能的構成）
つぎに、この発明の実施の形態にかかる検証支援装置の機能的構成について説明する。図２は、この発明の実施の形態にかかる検証支援装置の機能的構成を示すブロック図である。図２において、検証支援装置２００は、取得部２０１と、置換部２０２と、設定部２０３と、実行部２０４と、決定部２０５と、生成部２０６と、算出部２０７と、判定部２０８と、変換部２０９と、から構成されている。
【００５０】
取得部２０１は、検証対象回路の回路情報と、検証対象回路の機能を検証する可変の値を含んだ検証シナリオＳと、を取得する。ここで、検証対象回路とは、検証対象となるＬＳＩなどの論理回路である。また、回路情報とは、検証対象回路に関する情報であり、たとえば、ネットリストやＲＴＬ記述などを適用することができる。
【００５１】
図３は、上述した検証対象回路の回路情報の一例を示す説明図である。図３において、回路情報３００は、ネットリストを元にしてあらわされており、入力Ａ〜Ｅ、出力Ｆのほか、内部信号線Ｇ〜Ｊを備えている。以下、これらＡ〜Ｊを単に「信号線Ａ〜Ｊ」と呼ぶ場合もある。
【００５２】
また、検証シナリオＳとは、検証対象回路の任意の機能の検証を目的とした入力シミュレーションパターン（以下、単に「入力パターン」という）の集合である。入力パターンとは、具体的には、論理シミュレーションの実行のために回路情報３００に与えられる値（パラメータ）の集合であり、少なくとも可変の値が含まれている。また、可変の値とは、「０」または「１」のいずれかの論理値となり得る値である。
【００５３】
たとえば、図３に示した回路情報３００においては、検証シナリオＳは、下記の通りとなる。なお、ｂ，ｃ，ｄ，ｅは任意の可変の値である。この検証シナリオＳは、入力ＡがＡ＝０の場合の検証対象回路の機能を検証するシナリオである。
【００５４】
検証シナリオＳ：
『下記の入力パターンＰＶを検証対象回路に入力して出力Ｆを観測することで、当該検証対象回路の機能を検証する。
ＰＶ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｂ，ｃ，ｄ，ｅ）』
【００５５】
なお、取得部２０１は、図１に示したキーボード１１０やマウス１１１を操作したり、ネットワーク１１４を介して外部のサーバから受信したり、データベースから抽出したりすることで、回路情報３００や検証シナリオＳを取得することができる。この取得部２０１は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、または、Ｉ／Ｆ１０９によって、その機能を実現する。
【００５６】
また、図２において、置換部２０２は、検証シナリオＳの可変の値を不定値または記号に置換する。具体的には、置換部２０２は、不定値または記号への置換により、検証シナリオＳ内の入力パターンを、不定値または記号を含む入力パターンに変更する。
【００５７】
たとえば、上述した検証シナリオＳを用いて、不定値に置換する場合を例に挙げて説明すると、置換部２０２は、検証シナリオＳの入力パターン（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｂ，ｃ，ｄ，ｅ）について、可変の値（ｂ，ｃ，ｄ，ｅ）を不定値ｘに置換することにより、下記の入力パターンＰＸを得る。
【００５８】
ＰＸ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｘ，ｘ，ｘ，ｘ）
【００５９】
また、記号に置換する場合を例に挙げて説明すると、設定部２０３は、入力パターンＰＶについて、可変の値（ｂ，ｃ，ｄ，ｅ）を記号（ｐ，ｑ，ｒ，ｓ）に置換することにより、下記の入力パターンＰＳを得る。
【００６０】
ＰＳ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｐ，ｑ，ｒ，ｓ）
【００６１】
この置換部２０２は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００６２】
また、設定部２０３は、検証シナリオＳの可変の値に任意の論理値を与えることによって入力パターンを設定する。具体的には、設定部２０３は、検証シナリオＳであらわされる入力パターンの集合から、信号変化前後をあらわす具体的な入力パターンを用意する。たとえば、設定部２０３は、入力パターンＰＶについて、可変の値（ｂ，ｃ，ｄ，ｅ）を任意の論理値「０」に置換（ｂ＝０，ｃ＝０，ｄ＝０，ｅ＝０）することにより、下記の入力パターンＰ１を得る。
【００６３】
Ｐ１＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，０，０，０，０）
【００６４】
また、入力パターンＰＶについて、可変の値（ｂ，ｃ，ｄ，ｅ）を任意の論理値「１」に置換（ｂ＝１，ｃ＝１，ｄ＝１，ｅ＝１）することにより、下記の入力パターンＰ２を得る。
【００６５】
Ｐ２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，１，１，１，１）
【００６６】
すなわち、入力パターンＰ１は検証対象回路に入力される信号変化前の入力パターンをあらわしており、入力パターンＰ２は入力パターンＰ１からの信号変化後の入力パターンをあらわしている。
【００６７】
この設定部２０３は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００６８】
実行部２０４は、入力パターンを回路情報３００に与えることによって論理シミュレーションを実行する。実行部２０４は、第１の実行部２１１と第２の実行部２１２とを備えている。第１の実行部２１１は、検証シナリオＳ、具体的には入力パターンＰＸ（またはＰＳ）を回路情報３００に与えることによって、検証対象回路の論理シミュレーションを実行する。
【００６９】
また、第２の実行部２１２は、設定部２０３によって設定された入力パターンＰ１，Ｐ２を回路情報３００に与えることによって、検証対象回路の論理シミュレーションを実行する。この実行部２０４は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００７０】
また、決定部２０５は、実行部２０４によって実行された実行結果に基づいて、コードカバレッジ上限情報を決定する。ここで、コードカバレッジ上限情報とは、回路情報３００内において任意の値が伝搬した箇所によって示され、検証シナリオＳに含まれているすべての入力パターンを実行した場合に達成可能と想定されるコードカバレッジをあらわしている。具体的には、決定部２０５は、第１の実行部２１１による論理シミュレーションの実行結果からコードカバレッジ上限情報を決定することができる。このコードカバレッジ上限情報は、検証対象回路の検証網羅性の評価に用いることができる。
【００７１】
たとえば、不定値ｘを含む入力パターンＰＸを回路情報３００に与えた論理シミュレーションを例に挙げて説明すると、その実行結果は、回路情報３００内の信号線に伝搬された値（０，１，ｘ）の集合となる。したがって、実行結果の中から、伝搬された値が不定値ｘである信号線の集合を抽出する。
【００７２】
より具体的には、図３に示した検証対象回路の回路情報３００において、入力パターンＰＸは、（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｘ，ｘ，ｘ，ｘ）であるから、入力Ｂ，Ｃ，Ｄ，Ｅには不定値ｘが伝搬している。また、出力Ｆおよび内部信号線Ｇ，Ｈに不定値ｘが伝搬し、内部信号線Ｉ，Ｊには伝搬していないとすると、決定部２０５は、コードカバレッジ上限情報ＣＭを、以下のように決定することができる。
【００７３】
ＣＭ＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ）
【００７４】
また、コードカバレッジ上限情報ＣＭは、不定値ｘが伝搬している信号線の数を集計することによって決定してもよい。上述した例では、不定値ｘが伝搬している信号線は、Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇであるため、コードカバレッジ上限情報ＣＭは、ＣＭ＝６と決定される。なお、この決定部２０５は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００７５】
また、生成部２０６は、第２の実行部２１２によって実行された実行結果に基づいて、回路情報３００に関するコードカバレッジＣＣを生成する。ここで、コードカバレッジＣＣについて説明する。コードカバレッジＣＣとは、検証対象回路のソースコードを基準にしたカバレッジである。コードカバレッジＣＣとしては、ソースコードのすべての行を実行しようとするラインカバレッジ、ソースコードに記載されたすべての信号線を変化させようとするトグルカバレッジ、ソースコードから有限状態機械（ＦＳＭ）を決定してその状態や状態遷移を網羅しようとするＦＳＭカバレッジなどが知られている。
【００７６】
コードカバレッジＣＣは、第２の実行部２１２において入力パターンＰ１を与えた場合の論理シミュレーションの実行結果Ｒ１と、第２の実行部２１２において入力パターンＰ２を与えた場合の論理シミュレーションの実行結果Ｒ２とを比較することによって算出される。具体的には、実行結果Ｒ１から得られる各信号線Ａ〜Ｊの値と、実行結果Ｒ２から得られる各信号線Ａ〜Ｊの値と、を比較して、値が変化した信号線の集合を、コードカバレッジＣＣとする。
【００７７】
たとえば、入力パターンＰ１を回路情報３００に与えたときの実行結果Ｒ１が以下の信号線の値の集合であるとする。
【００７８】
Ｒ１＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（０，０，０，０，０，１，０，１，０，０）
【００７９】
同様に、入力パターンＰ２を回路情報３００に与えたときの実行結果Ｒ２が以下の信号線の値の集合であるとする。
【００８０】
Ｒ２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（０，１，１，１，１，０，１，０，０，０）
【００８１】
両者Ｒ１，Ｒ２を比較すると、値が変化した信号線は、Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈである。したがって、この場合のコードカバレッジＣＣは、以下の通りとなる。
【００８２】
ＣＣ＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ）
【００８３】
なお、この生成部２０６は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００８４】
また、算出部２０７は、決定部２０５によって決定されたコードカバレッジ上限情報ＣＭに対する、生成部２０６によって生成されたコードカバレッジＣＣの達成度を算出する。たとえば、上述したコードカバレッジＣＣでは、コードカバレッジ上限情報ＣＭ内の値の数は「６」、コードカバレッジ上限情報ＣＭの信号変化と一致しているコードカバレッジＣＣの値の数も「６」であるため、達成度は６／６、すなわち１００［％］と算出する。
【００８５】
また、算出部２０７は、コードカバレッジ上限情報ＣＭが変化した信号線の数によって決定された場合、達成度も、コードカバレッジＣＣも変化した信号線の数を用いて算出する。上述の例の場合、コードカバレッジ上限情報ＣＭはＣＭ＝６であり、コードカバレッジＣＣの信号線数も６となるため、達成度は６／６、すなわち１００［％］と算出することができる。なお、この算出部２０７は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００８６】
また、判定部２０８は、算出部２０７によって算出された達成度に基づいて、コードカバレッジＣＣによる検証網羅性を判定する。具体的には、判定基準となるしきい値（たとえば、１００［％］）を設定しておき、算出部２０７によって算出された達成度と比較することで、生成部２０６によって生成されたコードカバレッジＣＣが、検証シナリオＳの機能を検証するあらゆる入力パターンを与えた場合の実行結果をすべて網羅しているか否かを判定する。
【００８７】
また、判定部２０８によって検証シナリオＳの機能を検証するあらゆる入力パターンを与えた場合の実行結果をすべて網羅していると判定された場合、検証対象回路の設計障害がないと評価することができる。一方、すべて網羅していないと判定された場合、設定部２０３は、検証シナリオＳの可変の値に任意の論理値とは異なる論理値を与えることによって入力パターンＰ１，Ｐ２とは異なる他の入力パターンを設定する。
【００８８】
そして、第２の実行部２１２は、他の入力パターンを回路情報３００に与えることによって、論理シミュレーションを実行し、生成部２０６は、第２の実行部２１２によって実行された実行結果に基づいて、コードカバレッジＣＣとは異なる他のコードカバレッジを生成する。この他のコードカバレッジは、コードカバレッジＣＣを含んでおり、さらに、他の入力パターンによってあらたに信号変化した値も含んでいる。そして、算出部２０７は、コードカバレッジ上限情報ＣＭに対する、他のコードカバレッジの達成度を算出することで、前回算出されたコードカバレッジＣＣの達成度の上昇を図ることができる。
【００８９】
したがって、算出部２０７によって算出される達成度がしきい値以上になるまで、第２の実行部２１２に与える入力パターンを自動的に設定して、第２の実行部２１２による論理シミュレーションを自動的に実行することができる。したがって、達成度の変化を参照することにより、論理シミュレーションの終了時期を的確に判断することができる。
【００９０】
なお、この判定部２０８は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【００９１】
また、変換部２０９は、回路情報３００がＲＴＬ記述で取得されたとき、第１の実行部２１１による論理シミュレーション中に、ＲＴＬ記述に含まれている条件分岐文において条件不成立となった場合、条件分岐文の分岐先となる他の条件分岐文の実行結果を不定値に変換する。具体的には、ＲＴＬ記述に含まれている条件分岐文の実行結果が不定値ｘとなった場合、条件分岐文の分岐先となる他の条件分岐文の実行結果を不定値ｘに変換する。そして、変換されたＲＴＬ記述を用いて第１の実行部２１１による論理シミュレーションを実行する。
【００９２】
すなわち、その分岐先の候補すべてが実行されたと記録することにより、分岐先の実行によって影響を受けるすべての変数に不定値ｘを代入する変換処理である。たとえば、つ
ぎの文では、Ａの値がｘであれば（この文全体が実行されたと記録した上で）ＢにもＣに
もｘを代入するような動作を実行する。
【００９３】
ｉｆ（Ａ＝＝１）Ｂ＜＝１；
ｅｌｓｅＣ＜＝１；
【００９４】
なお、より厳密に、ＡがｘかつＢが１でないときだけＢにｘを代入し、ＡがｘかつＣが
１でないときだけＣにｘを代入するような動作であってもよい。この変換部２０９では、
変換されたＲＴＬ記述を用いて第１の実行部２１１による論理シミュレーションを実行することにより、回路情報３００がＲＴＬ記述であっても、その実行結果からコードカバレッジ上限情報ＣＭを正確に決定することができる。
【００９５】
また、変換部２０９は、回路情報３００がＲＴＬ記述であり、当該ＲＴＬ記述に条件分岐文がある場合、条件分岐文のいずれの分岐先も実行できるようにＲＴＬ記述を変換することとしてもよい。たとえば、使用する論理シミュレータではＶｅｒｉｌｏｇ−ＨＤＬの文法規約に従った動作、すなわち上の例の場合ｉｆの条件が不成立となりｅｌｓｅの文が実行される動作しか選択できない場合には、ｅｌｓｅ以外の文も選択できるように、あらかじめＲＴＬ記述を書き換える。
【００９６】
この変換部２０９でも、変換されたＲＴＬ記述を用いて第３の論理シミュレーションを実行することにより、回路情報３００がＲＴＬ記述であっても、その実行結果からコードカバレッジ上限情報ＣＭを正確に決定することができる。
【００９７】
また、変換部２０９は、第１の実行部２１１において与えられる入力パターンが記号に置換された入力パターンＰＳであるとき、第１の実行部２１１による論理シミュレーション中に、所定数の記号からなる論理式が出現した場合、当該論理式を、当該論理式の記号数よりも少ない数の記号に変換する。
【００９８】
具体的には、第１の実行部２１１による論理シミュレーション中に、入力パターンＰＳの記号は、ＡＮＤ回路、ＯＲ回路、インバータ、ＮＡＮＤ回路、ＮＯＲ回路、ＥＯＲ回路などの論理回路セルに入力された場合、ブール代数の論理演算によって他の記号や論理式となって伝搬していく。
【００９９】
たとえば、回路情報３００内に３入力ＡＮＤ回路が存在する場合、入力（０，ｐ，ｑ）を与えたときの論理シミュレーションの実行結果は０となるが、入力（１，ｐ，ｑ）を与えたときの論理シミュレーションの実行結果はｐ・ｑという論理式なる。この場合の論理式内の記号数は２個であるが、値が伝搬するにつれて、記号数が増加する。
【０１００】
このような場合、論理式を構成する記号の数が所定数以上となった場合、別の単一記号に変換することによってその後の計算量を低減することができ、論理シミュレーションの高速化を図ることができる。なお、変換部２０９は、具体的には、たとえば、図１に示したＲＯＭ１０２、ＲＡＭ１０３、ＨＤ１０５、ＦＤ１０７などの記録媒体に記録されたプログラムを、ＣＰＵ１０１が実行することによって、その機能を実現する。
【０１０１】
（検証支援装置２００の検証支援処理手順）
つぎに、この発明の実施の形態にかかる検証支援装置２００の検証支援処理手順について説明する。図４は、この発明の実施の形態にかかる検証支援装置２００の検証支援処理手順を示すフローチャートである。
【０１０２】
図４において、取得部２０１により、検証シナリオＳおよび回路情報３００が取得された場合（ステップＳ４０１：Ｙｅｓ）、入力パターンＰＶ内の可変の値を、不定値ｘまたは記号に置換して（ステップＳ４０２）、第１の実行部２１１により、置換によって得られた入力パターンＰＸ（またはＰＳ）を回路情報３００に与えて論理シミュレーションを実行する（ステップＳ４０３）。そして、この実行結果から、決定部２０５により、コードカバレッジ上限情報ＣＭを決定する（ステップＳ４０４）。
【０１０３】
また、設定部２０３により、入力パターンＰＶの可変の値に任意の論理値を与えることによって入力パターンＰ１，Ｐ２を設定する（ステップＳ４０５）。そして、第２の実行部２１２により、回路情報３００に入力パターンＰ１，Ｐ２を与えて論理シミュレーションを実行する（ステップＳ４０６）。
【０１０４】
そして、生成部２０６により、入力パターンＰ１，Ｐ２からコードカバレッジＣＣを生成し（ステップＳ４０７）、算出部２０７により、コードカバレッジ上限情報ＣＭに対するコードカバレッジＣＣの達成度を算出する（ステップＳ４０８）。そして、算出された達成度がしきい値以上であるか否かを判定する（ステップＳ４０９）。
【０１０５】
しきい値以上でない場合（ステップＳ４０９：Ｎｏ）、ステップＳ４０５に移行して、入力パターンの再設定をおこなう。一方、しきい値以上である場合（ステップＳ４０９：Ｙｅｓ）、一連の処理を終了する。なお、変換部２０９による変換処理は、ステップＳ４０３の論理シミュレーションの実行中におこなうことができる。
【０１０６】
このように、上述した実施の形態によれば、ユーザ（設計者または検証者）は、算出部２０７によって算出された達成度を用いて、検証網羅性を評価することができる。達成度がしきい値以上である場合、コードカバレッジＣＣはその検証シナリオＳの機能を示すすべての入力パターンを網羅していることとなる。したがって、コードカバレッジＣＣを適用することにより検証漏れを防止することができ、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１０７】
また、達成度がしきい値以上でない場合、コードカバレッジＣＣがその検証シナリオＳの機能を示すすべての入力パターンを網羅していないこととなる。したがって、コードカバレッジ上限情報ＣＭとコードカバレッジＣＣとの不一致の値の信号線を参照することにより、検証対象回路の設計障害を効率よく検出することができるという効果を奏する。
【０１０８】
また、達成度がしきい値以上でない場合、第２の実行部２１２に与える入力パターンを再設定して、第２の実行部２１２による論理シミュレーションを実行する。そして、達成度がしきい値以上になるまで自動的に論理シミュレーションを実行することにより、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【実施例１】
【０１０９】
つぎに、上述した実施の形態にかかる検証支援装置２００の実施例１について説明する。実施例１は、検証シナリオに含まれている可変の値を不定値ｘに置換する例である。また、コードカバレッジＣＣとしてトグルカバレッジを用いるため、一例として、図３に示した回路情報３００を適用する。
【０１１０】
（検証支援装置の概略構成）
まず、実施例１にかかる検証支援装置の概略構成について説明する。図５は、実施例１にかかる検証支援装置の概略構成図である。検証シナリオＳは、検証対象回路の機能を検証する。検証シナリオＳとしては、図５において、たとえば、下記の検証シナリオＳ１，Ｓ２が挙げられる。
【０１１１】
検証シナリオＳ１:
『下記の入力パターンＰＶ１を入力して出力Ｆを観測することで、機能Ｆ１を検証する。
ＰＶ１＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｂ，ｃ，ｄ，ｅ）』
【０１１２】
検証シナリオＳ２：
『下記の入力パターンＰＶ２を入力して出力Ｆを観測することで、機能Ｆ２を検証する。
ＰＶ２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（１，ｂ，ｃ，ｄ，ｅ）』
【０１１３】
ここで、（ｂ，ｃ，ｄ，ｅ）は「０」または「１」の任意の値を割り当てることができる可変の値である。検証シナリオＳ１に対して、可変の値（ｂ，ｃ，ｄ，ｅ）に不定値ｘ
を割り当てることにより、不定値ｘを含む入力パターンＰＸ１を下記の通り設定する。
【０１１４】
ＰＸ１＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（０，ｘ，ｘ，ｘ，ｘ）
【０１１５】
そして、この入力パターンＰＸ１を回路情報３００に与えることによって、論理シミュレータ５０１により、３値（０，１，ｘ）の論理シミュレーションを実行する。論理シミ
ュレータ５０１は、上述した第１の実行部２１１に相当する。この３値（０，１，ｘ）の
論理シミュレーションの実行結果ＲＸ１を図６に示す。図６は、３値（０，１，ｘ）の論
理シミュレーションの実行結果ＲＸ１を示す説明図である。図６において、実行結果ＲＸ１は、以下の通りとなる。
【０１１６】
ＲＸ１＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（０，ｘ，ｘ，ｘ，ｘ，ｘ，ｘ，ｘ，０，０）
【０１１７】
この実行結果ＲＸ１から、信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈに不定値ｘが伝播したこ
とがわかるため、検証シナリオＳ１に関するコードカバレッジ上限情報ＣＭ１は、以下の通りとなる。
【０１１８】
ＣＭ１＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ）
【０１１９】
すなわち、検証シナリオＳ１では、この７つの信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈに関する信号値変化が達成可能と見積もることができる。同様に、検証シナリオＳ２についても、入力パターンＰＸ２を下記の通り設定する。
【０１２０】
ＰＸ２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（１，ｘ，ｘ，ｘ，ｘ）
【０１２１】
そして、この入力パターンＰＸ２を回路情報３００に与えることによって、論理シミュレータ５０１により、３値（０，１，ｘ）の論理シミュレーションを実行する。この３値
（０，１，ｘ）の論理シミュレーションの実行結果ＲＸ２を図７に示す。図７は、３値（
０，１，ｘ）の論理シミュレーションの実行結果ＲＸ２を示す説明図である。図７におい
て、実行結果ＲＸ２は、以下の通りとなる。
【０１２２】
ＲＸ２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（１，ｘ，ｘ，ｘ，ｘ，ｘ，ｘ，０，ｘ，ｘ）
【０１２３】
この実行結果ＲＸ２から、信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊに不定値ｘが伝播し
たことがわかるため、コードカバレッジ上限情報ＣＭ２は、下記の通りとなる。
【０１２４】
ＣＭ２＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊ）
【０１２５】
すなわち、検証シナリオＳ２では、この８つの信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊに関する信号値変化が達成可能と見積もることができる。
【０１２６】
また、実際の検証では、検証シナリオＳ１，Ｓ２の可変の値（ｂ，ｃ，ｄ，ｅ）に「０」または「１」の値を割り当てて具体化することにより、信号値変化が起こりうる入力パターンを設定し、論理シミュレータ５０２により２値の論理シミュレーションをおこない、実際の信号値変化を観測する。論理シミュレータ５０２は、上述した第２の実行部２１２に相当する。
【０１２７】
そして、上述したコードカバレッジ上限情報ＣＭ１，ＣＭ２をどれだけ達成したかで検証の網羅性を評価する。ここで、たとえば、検証シナリオＳ１に関する具体的な入力パターンＰ１（Ｐ１ａ，Ｐ１ｂ）を下記のように設定する。
【０１２８】
［入力パターンＰ１］
Ｐ１ａ＝（０，０，０，０，０）
Ｐ１ｂ＝（０，１，１，１，１）
【０１２９】
入力パターンＰ１ａを用いた２値（０，１）の論理シミュレーションの実行結果Ｒ１ａを図８に示す。図８は、２値（０，１）の論理シミュレーションの実行結果Ｒ１ａを示す説明図である。図８において、実行結果Ｒ１ａは、以下の通りとなる。
【０１３０】
Ｒ１ａ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（０，０，０，０，０，１，０，１，０，０）
【０１３１】
また、入力パターンＰ１ｂを用いた２値（０，１）の論理シミュレーションの実行結果Ｒ１ｂを図９に示す。図９は、２値（０，１）の論理シミュレーションの実行結果Ｒ１ｂを示す説明図である。図９において、実行結果Ｒ１ｂは、以下の通りとなる。
【０１３２】
Ｒ１ｂ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（０，１，１，１，１，０，１，０，０，０）
【０１３３】
この図８および図９に示した論理シミュレーションの実行結果Ｒ１ａ，Ｒ１ｂを比較すると、検証シナリオＳ１に関するコードカバレッジＣＣ１は、以下の通りとなる。
【０１３４】
ＣＣ１＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ）
【０１３５】
このコードカバレッジＣＣ１の信号線（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ）は、実行結果Ｒ１ａから実行結果Ｒ１ｂへの信号値変化をあらわしている。このコードカバレッジＣＣ１とコードカバレッジ上限情報ＣＭ１とを比較すると、コードカバレッジＣＣ１は、コードカバレッジ上限情報ＣＭ１のすべての信号線と一致するため、達成度が１００［％］であるということが分かる。したがって、検証シナリオＳ１に関する基準を達成したことになる。
【０１３６】
また、検証シナリオＳ２についても同様に処理することができる。たとえば、検証シナリオＳ２に関する具体的な入力パターンＰ２（Ｐ２ａ，Ｐ２ｂ）を下記のように設定する。
【０１３７】
［入力パターンＰ２］
Ｐ２ａ＝（０，０，０，０，０）
Ｐ２ｂ＝（０，１，１，１，１）
【０１３８】
そして、入力パターンＰ２ａを用いた２値（０，１）の論理シミュレーションの実行結果Ｒ２ａを図１０に示す。図１０は、２値（０，１）の論理シミュレーションの実行結果Ｒ２ａを示す説明図である。図１０において、実行結果Ｒ２ａは、以下の通りとなる。
【０１３９】
Ｒ２ａ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（１，０，０，０，０，０，０，０，０，０）
【０１４０】
また、入力パターンＰ２ｂを用いた２値（０，１）の論理シミュレーションの実行結果Ｒ２ｂを図１１に示す。図１１は、２値（０，１）の論理シミュレーションの実行結果Ｒ２ｂを示す説明図である。図１１において、実行結果Ｒ２ｂは、以下の通りとなる。
【０１４１】
Ｒ２ｂ＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ，Ｉ，Ｊ）
＝（１，１，１，１，１，１，１，０，１，１）
【０１４２】
この図１０および図１１に示した論理シミュレーションの実行結果Ｒ２ａ，Ｒ２ｂを比較すると、検証シナリオＳ２に関するコードカバレッジＣＣ２は、以下の通りとなる。
【０１４３】
ＣＣ２＝（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊ）
【０１４４】
このコードカバレッジＣＣ２の信号線（Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊ）は、実行結果Ｒ２ａから実行結果Ｒ２ｂへの信号値変化をあらわしている。このコードカバレッジＣＣ２とコードカバレッジ上限情報ＣＭ２とを比較すると、コードカバレッジＣＣ２は、コードカバレッジ上限情報ＣＭ２のすべての信号線と一致するため、達成度が１００［％］であるということが分かる。したがって、検証シナリオＳ２に関するコードカバレッジ上限情報ＣＭ２を達成したことになる。
【０１４５】
（検証支援装置の検証支援処理手順）
つぎに、上述した実施例１にかかる検証支援装置の検証支援処理手順について説明する。図１２−１および図１２−２は、実施例１にかかる検証支援装置の検証支援処理手順を示すフローチャートである。
【０１４６】
図１２−１において、回路情報３００が入力された場合（ステップＳ１２０１：Ｙｅｓ）、ｉをｉ＝１にセットする（ステップＳ１２０２）。つぎに、検証シナリオＳｉが入力
された場合（ステップＳ１２０３：Ｙｅｓ）、検証シナリオＳｉ内の入力パターンＰＶｉの可変の値を、不定値ｘに置換した入力パターンＰＸｉに設定する（ステップＳ１２０４）。
【０１４７】
つぎに、回路情報３００に入力パターンＰＸｉを与えて３値（０，１，ｘ）の論理シミュレーションを実行し（ステップＳ１２０５）、コードカバレッジ上限情報ＣＭｉを決定する（ステップＳ１２０６）。このあと、検証シナリオＳｉ内の入力パターンＰＶｉの可変の値を任意の論理値に置換することによって、入力パターンＰｉ（Ｐｉａ，Ｐｉｂ）を設定する（ステップＳ１２０７）。そして、回路情報３００に入力パターンＰｉａを与えて２値（０，１）の論理シミュレーションを実行する（ステップＳ１２０８）。
【０１４８】
また、図１２−２において、回路情報３００に入力パターンＰｉｂを与えて２値（０，１）の論理シミュレーションを実行する（ステップＳ１２０９）。そして、ステップＳ１２０８およびステップＳ１２０９の実行結果から、コードカバレッジＣＣｉを生成する（ステップＳ１２１０）。そして、コードカバレッジ上限情報ＣＭｉに対するコードカバレッジＣＣｉの達成度を算出する（ステップＳ１２１１）。
【０１４９】
この達成度がしきい値以上である場合（ステップＳ１２１２：Ｙｅｓ）、ステップＳ１２１４に移行する。一方、達成度がしきい値以上でない場合（ステップＳ１２１２：Ｎｏ）、コードカバレッジＣＣｉがその検証シナリオＳｉの機能を示すすべての入力パターンを網羅していないこととなる。このすべての入力パターンが設定されていない場合（ステップＳ１２１３：Ｎｏ）、ステップＳ１２０７に移行して、入力パターンＰｉを再設定する。一方、このすべての入力パターンが設定された場合（ステップＳ１２１３：Ｙｅｓ）、ステップＳ１２１４に移行する。
【０１５０】
また、ステップＳ１２１４において、ｎを検証シナリオの数とすると、ｉ＝ｎである場合（ステップＳ１２１４：Ｙｅｓ）、一連の処理を終了する。一方、ｉ＝ｎでない場合（ステップＳ１２１４：Ｎｏ）、ｉをインクリメントして（ステップＳ１２１５）、ステップＳ１２０３に移行する。これにより、つぎの検証シナリオＳｉについて検証網羅性を評価することができる。
【０１５１】
この実施例１によれば、ユーザ（設計者または検証者）は、コードカバレッジ上限情報ＣＭ１に対するコードカバレッジＣＣ１の達成度を用いて、検証網羅性を評価することができる。達成度がしきい値以上である場合、コードカバレッジＣＣ１はその検証シナリオＳ１の機能を示すすべての入力パターンを網羅していることとなる。したがって、コードカバレッジＣＣ１を適用することにより検証漏れを防止することができ、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１５２】
また、達成度がしきい値未満である場合、コードカバレッジＣＣ１がその検証シナリオＳ１の機能を示すすべての入力パターンを網羅していないこととなる。したがって、コードカバレッジ上限情報ＣＭとコードカバレッジＣＣとの不一致の値の信号線を参照することにより、検証対象回路の設計障害を効率よく検出することができる。またこれにより、検出された設計障害の数から、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１５３】
また、達成度がしきい値以上でない場合、論理シミュレータ５０２に与える入力パターンを再設定して、論理シミュレータ５０２による論理シミュレーションを実行する。そして、達成度がしきい値以上になるまで自動的に論理シミュレーションを実行することにより、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【実施例２】
【０１５４】
つぎに、実施例２にかかる検証支援装置について説明する。実施例１では、ネットリストを用いた回路情報３００を用いているが、実施例２では、回路情報として、ＲＴＬ（レジスタ転送レベル）記述を用いる例である。これにより、入力する回路情報がネットリストで表現される回路情報３００に限定されず汎用性が向上し、検証支援の効率化を図ることができる。なお、検証支援処理の仕組みは、上述した実施例１とほぼ同様である。
【０１５５】
（回路情報）
まず、実施例２にかかる回路情報について説明する。図１３は、実施例２にかかる回路情報を示す説明図である。図１３において、回路情報は、検証対象回路のＲＴＬ記述１３００によって表現されている。このＲＴＬ記述１３００は入力信号ｃｌｋの立ち上がりに同期した同期式順序回路を表現している。
【０１５６】
（検証支援装置の概略構成）
つぎに、実施例２にかかる検証支援装置の概略構成について説明する。図１４は、実施例２にかかる検証支援装置の概略構成図である。検証シナリオは、図１３に示したＲＴＬ記述１３００で表現されている検証対象回路の機能を検証する。たとえば、検証シナリオとしては、下記の例が挙げられる。
【０１５７】
検証シナリオＳ２１:
『最初のサイクル（以下「サイクル１」）に（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）を与え、次のサイクル（以下「サイクル２」）に（ｏｐ，ｄａｔａ）＝（２’ｂ０１，ｐ２）を与える。』
【０１５８】
検証シナリオＳ２２:
『サイクル１に（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）を与え、サイクル２に（ｏｐ，ｄａｔａ）＝（２’ｂ１０，ｐ２）を与え、その次のサイクル（以下「サイクル３」）に（ｏｐ，ｄａｔａ）＝（２’ｂ１１，ｐ３）を与える。』
【０１５９】
なお、上記検証シナリオＳ２１，Ｓ２２において、ｐ１〜ｐ３は、検証シナリオＳ２１，Ｓ２２の可変の値であり、ここでは、任意の８ビットを割り当てることにより、入力パターンを設定することができる。ここでは、サイクル１およびサイクル２に対して、可変の値ｐ１，ｐ２に不定値ｘを割り当てることで、検証シナリオＳ２１の入力パターンＰＸ
２１を、下記のように設定する。
【０１６０】
［入力パターンＰＸ２１］
サイクル１：（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）
＝（２’ｂ００，８’ｂｘｘｘｘｘｘｘｘ）
サイクル２：（ｏｐ，ｄａｔａ）＝（２’ｂ０１，ｐ２）
＝（２’ｂ０１，８’ｂｘｘｘｘｘｘｘｘ）
【０１６１】
そして、論理シミュレータ１４０１は、ＲＴＬ記述１３００に入力パターンＰＸ２１を与えて、論理シミュレーションを実行する。論理シミュレータ１４０１は、上述した第１の実行部２１１に相当する。この論理シミュレーションによる実行結果ＲＸ２１は、実行文が記述された行［０１３］，［０１５］，［０１８］，［０２１］，［０２５］のうち、検証シナリオＳ２１で実行可能な行［０１３］，［０１５］である。この検証シナリオＳ２１に関する実行結果ＲＸ２１（［０１３］，［０１５］）が検証シナリオＳ２１に関するコードカバレッジ上限情報ＣＭ２１（［０１３］，［０１５］）となる。
【０１６２】
また、検証シナリオＳ２２についても同様に、サイクル１〜３に対して、可変の値ｐ１〜ｐ３に不定値ｘを割り当てることで、検証シナリオＳ２２の入力パターンＰＸ２２を、
下記のように設定する。
【０１６３】
［入力パターンＰＸ２２］
サイクル１：（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）
＝（２’ｂ００，８’ｂｘｘｘｘｘｘｘｘ）
サイクル２：（ｏｐ，ｄａｔａ）＝（２’ｂ１０，ｐ２）
＝（２’ｂ１０，８’ｂｘｘｘｘｘｘｘｘ）
サイクル３：（ｏｐ，ｄａｔａ）＝（２’ｂ１１，ｐ３）
＝（２’ｂ１１，８’ｂｘｘｘｘｘｘｘｘ）
【０１６４】
そして、論理シミュレータ１４０１は、ＲＴＬ記述１３００に入力パターンＰＸ２２を与えて、論理シミュレーションを実行する。この論理シミュレーションによる実行結果ＲＸ２２は、実行文が記述された行［０１３］，［０１５］，［０１８］，［０２１］，［０２５］のうち、検証シナリオＳ２２で実行可能な行である。この検証シナリオＳ２２に関する実行結果ＲＸ２２（［０１３］，［０１８］，［０２１］，［０２５］）が、検証シナリオＳ２２に関するコードカバレッジ上限情報ＣＭ２２（［０１３］，［０１８］，［０２１］，［０２５］）となる。
【０１６５】
また、論理シミュレータ１４０２は、ＲＴＬ記述１３００に検証シナリオＳ２１に対する具体的な入力パターンＰ１１を与えて、論理シミュレーションを実行する。論理シミュレータ１４０２は、上述した第２の実行部２１２に相当する。ここで、入力パターンＰ１１の一例を示す。
【０１６６】
［入力パターンＰ１１］
サイクル１：（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）
＝（２’ｂ００，８’ｂ１０１０１０１０）
サイクル２：（ｏｐ，ｄａｔａ）＝（２’ｂ０１，ｐ２）
＝（２’ｂ０１，８’ｂ１１００１１００）
【０１６７】
ＲＴＬ記述１３００に入力パターンＰ１１を与えると、サイクル１で行［０１３］が、サイクル２で行［０１５］が実行される。これにより、カバーされた行の集合、すなわち、検証シナリオＳ２１に関するコードカバレッジＣＣ２１は、下記の通りである。
【０１６８】
ＣＣ２１＝（［０１３］，［０１５］）
【０１６９】
このコードカバレッジＣＣ２１とコードカバレッジ上限情報ＣＭ２１と比較すると、コードカバレッジＣＣ２１とすべて一致するため、コードカバレッジＣＣ２１の達成度は、２／２、すなわち、１００［％］となる。
【０１７０】
また、論理シミュレータ１４０２は、ＲＴＬ記述１３００に検証シナリオＳ２２に対する具体的な入力パターンＰ１２を与えて、論理シミュレーションを実行する。ここで、入力パターンＰ１２ａの一例を示す。
【０１７１】
［入力パターンＰ１２ａ］
サイクル１：（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）
＝（２’ｂ００，８’ｂ１１１１００００）
サイクル２：（ｏｐ，ｄａｔａ）＝（２’ｂ１０，ｐ２）
＝（２’ｂ１０，８’ｂ１１１１１１１１）
サイクル３：（ｏｐ，ｄａｔａ）＝（２’ｂ１１，ｐ３）
＝（２’ｂ１１，８’ｂ０１０１０１０１）
【０１７２】
ここで、この入力パターンＰ１２ａをＲＴＬ記述１３００に与えると、サイクル１で行［０１３］が、サイクル２で行［０２１］が実行される。一方、サイクル３ではどの行も実行されない。これにより、カバーされた行の集合、すなわち、検証シナリオＳ２２に関するコードカバレッジＣＣ２２ａは、下記の通りである。
【０１７３】
ＣＣ２２ａ＝（［０１３］，［０２１］）
【０１７４】
このコードカバレッジＣＣ２２ａとコードカバレッジ上限情報ＣＭ２２と比較すると、コードカバレッジ上限情報ＣＭ２２は、（［０１３］，［０１８］，［０２１］，［０２５］）であるため、コードカバレッジ上限情報ＣＭ２２中、実行文［０１３］，［０２１］がカバーされている。したがって、コードカバレッジＣＣ２２ａの達成度は、２／４、すなわち、５０［％］となる。
【０１７５】
このことから、達成度が１００［％］ではないので、検証シナリオＳ２２については、さらに別の入力パターンを追加する必要がある。ここで、検証シナリオＳ２２に関する他の入力パターンＰ１２ｂの一例を示す。
【０１７６】
［入力パターンＰ１２ｂ］
サイクル１：（ｏｐ，ｄａｔａ）＝（２’ｂ００，ｐ１）
＝（２’ｂ００，８’ｂ００１１００１１）
サイクル２：（ｏｐ，ｄａｔａ）＝（２’ｂ１０，ｐ２）
＝（２’ｂ１０，８’ｂ００００００００）
サイクル３：（ｏｐ，ｄａｔａ）＝（２’ｂ１１，ｐ３）
＝（２’ｂ１１，８’ｂ００００１１１１）
【０１７７】
この入力パターンＰ１２ｂをＲＴＬ記述１３００に与えると、サイクル１で行［０１３］が、サイクル２で行［０１８］が、サイクル３で行［０２５］が実行される。これにより、カバーされた行の集合、すなわち、検証シナリオＳ２２に関するコードカバレッジＣＣ２２ｂは、下記の通りである。
【０１７８】
ＣＣ２２ｂ＝（［０１３］，［０１８］，［０２５］）
【０１７９】
したがって、このコードカバレッジＣＣ２２ｂと入力パターンＰ１２ａを与えた場合のコードカバレッジＣＣ２２ａとをあわせると、カバーされた行の集合、すなわち、検証シナリオＳ２２に関するコードカバレッジＣＣ２２は、以下の通りとなる。
【０１８０】
ＣＣ２２＝（［０１３］，［０１８］，［０２１］，［０２５］）
【０１８１】
したがって、このコードカバレッジＣＣ２２とコードカバレッジ上限情報ＣＭ２２とを比較すると、コードカバレッジＣＣ２２とすべて一致するため、コードカバレッジＣＣ２２の達成度は、２／２、すなわち、１００［％］となる。
【０１８２】
また、変換ツール１４１０は、この論理シミュレータ１４０１に特別な動作をおこなわせる。具体的には、ＲＴＬ記述１３００に、ｉｆやｃａｓｅなどの条件分岐文で条件式を評価した結果が不定値ｘになったとき、その分岐先の候補すべてが実行されたと記録して
、分岐先の実行によって影響を受けるすべての変数に不定値ｘを代入する。たとえば、つ
ぎの文では、Ａの値がｘであれば（この文全体が実行されたと記録した上で）ＢにもＣに
もｘを代入するような動作をおこなわせる。
【０１８３】
ｉｆ（Ａ＝＝１）Ｂ＜＝１；
ｅｌｓｅＣ＜＝１；
【０１８４】
また、より厳密に、ＡがｘかつＢが１でないときだけＢにｘを代入し、ＡがｘかつＣが
１でないときだけＣにｘを代入するような動作であってもよい。なお、変換ツール１４１
０は、上述した変換部２０９に相当する。
【０１８５】
（検証支援処理手順）
つぎに、この実施例２にかかる検証支援装置の検証支援処理手順について説明する。図１５−１および図１５−２は、実施例２にかかる検証支援装置の検証支援処理手順を示すフローチャートである。図１５−１において、ＲＴＬ記述１３００が入力された場合（ステップＳ１５０１：Ｙｅｓ）、ｉをｉ＝１にセットする（ステップＳ１５０２）。つぎに
、検証シナリオＳ２ｉが入力された場合（ステップＳ１５０３：Ｙｅｓ）、検証シナリオＳ２ｉ内の可変の値（検証シナリオＳ２１では、ｐ１，ｐ２に相当）を不定値ｘに置換することによって、入力パターンＰＸ２ｉを設定する（ステップＳ１５０４）。
【０１８６】
つぎに、ＲＴＬ記述１３００に入力パターンＰＸ２ｉを与えて３値（０，１，ｘ）の論理シミュレーションを実行する（ステップＳ１５０５）。ここで、ＲＴＬ記述１３００において条件分岐文が検出されない場合（ステップＳ１５０６：Ｎｏ）、ステップＳ１５０８に移行する。一方、ＲＴＬ記述１３００において条件分岐文が検出された場合（ステップＳ１５０６：Ｙｅｓ）、分岐先に不定値ｘを代入し（ステップＳ１５０７）、ステップＳ１５０８に移行する。
【０１８７】
そして、論理シミュレーションが終了していない場合（ステップＳ１５０８：Ｎｏ）、ステップＳ１５０６に移行する。一方、論理シミュレーションが終了した場合（ステップＳ１５０８：Ｙｅｓ）、図１５−２において、コードカバレッジ上限情報ＣＭ２ｉを決定する（ステップＳ１５０９）。このあと、検証シナリオＳ２ｉ内の可変の値を任意の論理値に置換した入力パターンＰ２ｉを設定する（ステップＳ１５１０）。
【０１８８】
そして、ＲＴＬ記述１３００に入力パターンＰ２ｉを与えて２値（０，１）の論理シミュレーションを実行し（ステップＳ１５１１）、その実行結果から、コードカバレッジＣＣ２ｉを生成する（ステップＳ１５１２）。
【０１８９】
そして、コードカバレッジ上限情報ＣＭ２ｉに対するコードカバレッジＣＣ２ｉの達成度を算出する（ステップＳ１５１３）。この達成度がしきい値以上である場合（ステップＳ１５１４：Ｙｅｓ）、ステップＳ１５１６に移行する。一方、達成度がしきい値以上でない場合（ステップＳ１５１４：Ｎｏ）、コードカバレッジＣＣ２ｉがその検証シナリオＳ２ｉの機能を示すすべての入力パターンを網羅していないこととなる。このすべての入力パターンが設定されていない場合（ステップＳ１５１５：Ｎｏ）、ステップＳ１５１０に移行して、入力パターンＰ２ｉを再設定する。一方、このすべての入力パターンが設定された場合（ステップＳ１５１５：Ｙｅｓ）、ステップＳ１５１６に移行する。
【０１９０】
また、ステップＳ１５１６において、ｎを検証シナリオの数とすると、ｉ＝ｎである場合（ステップＳ１５１６：Ｙｅｓ）、一連の処理を終了する。一方、ｉ＝ｎでない場合（ステップＳ１５１６：Ｎｏ）、ｉをインクリメントして（ステップＳ１５１７）、ステップＳ１５０３に移行する。これにより、つぎの検証シナリオＳ２ｉについて検証網羅性を評価することができる。
【０１９１】
この実施例２によれば、ユーザ（設計者または検証者）は、コードカバレッジ上限情報ＣＭ２ｉに対するコードカバレッジＣＣ２ｉの達成度を用いて、検証網羅性を評価することができる。達成度がしきい値以上である場合、コードカバレッジＣＣ２ｉはその検証シナリオＳ２ｉの機能を示すすべての入力パターンを網羅していることとなる。したがって、コードカバレッジＣＣ２ｉを適用することにより検証漏れを防止することができ、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１９２】
また、達成度がしきい値未満である場合、コードカバレッジＣＣ２ｉがその検証シナリオＳ２ｉの機能を示すすべての入力パターンを網羅していないこととなる。したがって、コードカバレッジ上限情報ＣＭ２ｉとコードカバレッジＣＣ２ｉとの不一致の値の信号線を参照することにより、検証対象回路の設計障害を効率よく検出することができる。またこれにより、検出された設計障害の数から、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１９３】
また、達成度がしきい値以上でない場合、論理シミュレータ１４０２に与える入力パターンを再設定して、論理シミュレータ１４０２による論理シミュレーションを実行する。そして、達成度がしきい値以上になるまで自動的に論理シミュレーションを実行することにより、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０１９４】
また、回路情報として、ＲＴＬ記述１３００を用いることができるため、回路情報の選択における自由度の向上を図ることができる。したがって、検証網羅性の評価を効率的におこなうことができる。またこれにより、回路情報がＲＴＬ記述であってもコードカバレッジ上限情報を正確に決定することができる。
【０１９５】
また、上述した変換ツール１４１０により、使用する論理シミュレータ１４０１ではＶｅｒｉｌｏｇ−ＨＤＬの文法規約に従った動作、すなわち上述したｉｆの条件が不成立となりｅｌｓｅ部分が実行される動作しか選択できない場合には、あらかじめＲＴＬ記述１３００を書き換える処理をおこなうこととしてもよい。書き換えをおこなった後のＲＴＬ記述を図１６に示す。図１６は、書き換え後のＲＴＬ記述を示す説明図である。
【０１９６】
図１６に示したＲＴＬ記述１６００において、新しく追加された行が論理シミュレーションの際に実行された場合には、その行に対応する元の一つまたは複数の行が実行されたとみなす。可変部分に「０」または「１」の値を割り当てた実際の検証作業は、通常のシミュレータ動作（元のＲＴＬ記述１３００）を使用して良い。そして、検証シナリオＳ２１については行［０１３］,［０１５］を実行したかどうかで検証網羅性を判定し、検証シナリオＳ２２については行［０１３］，［０１８］，［０２１］，［０２５］を実行したかどうかで検証網羅性を判定する。
【０１９７】
つぎに、この実施例２にかかる検証支援装置の他の検証支援処理手順について説明する。図１７は、実施例２にかかる検証支援装置の他の検証支援処理手順を示すフローチャートである。図１７において、ＲＴＬ記述１３００が入力された場合（ステップＳ１７０１：Ｙｅｓ）、ＲＴＬ記述１３００において条件分岐文が検出されたときは（ステップＳ１７０２：Ｙｅｓ）、変換ツール１４１０によりＲＴＬ記述１３００を書き換える（ステップＳ１７０３）。これにより、ＲＴＬ記述１６００を生成する。
【０１９８】
一方、ステップＳ１７０２において条件分岐文が検出されなかった場合（ステップＳ１７０２：Ｎｏ）、または、ＲＴＬ記述１３００の書き換えをおこなった後は、図１５−１に示したステップＳ１５０２に移行する。
【０１９９】
このように、ＲＴＬ記述１３００に条件分岐文がある場合、条件分岐文のいずれの分岐先も実行できるようにＲＴＬ記述１３００を変換（書き換え）し、変換されたＲＴＬ記述１６００を用いて論理シミュレーションを実行する。これにより、論理シミュレーション前にあらかじめＲＴＬ記述１３００を検証網羅性の評価に適合するように変換することができる。したがって、論理シミュレーションの効率化およびコードカバレッジ上限情報の正確性の向上を図ることができる。
【実施例３】
【０２００】
つぎに、実施例３にかかる検証支援装置について説明する。図１８は、実施例３にかかる検証支援装置の概略構成を示す説明図である。なお、図５に示した構成と同一構成には同一符号を付しその説明を省略する。実施例１では、検証シナリオＳ１（Ｓ２）の可変の値（ｂ，ｃ，ｄ，ｅ）を不定値ｘに置換して入力パターンＰＸ１（ＰＸ２）を設定した。
【０２０１】
一方、実施例３では、可変の値（ｂ，ｃ，ｄ，ｅ）を記号（ｐ，ｑ，ｒ，ｓ）に置換して入力パターンＰＸ３１，ＰＸ３２を設定する。そして、論理シミュレーションにおいては、入力パターンＰＸ３１，ＰＸ３２の記号（ｐ，ｑ，ｒ，ｓ）を用いた記号シミュレーションを実行する。これにより、信号伝搬ごとに記号を用いた論理演算をおこなうことができ、正確な伝搬情報を得ることができる。
【０２０２】
なお、実施例３では、実施例１で用いた検証シナリオＳ１，Ｓ２と、入力パターンＰ１，Ｐ２と、コードカバレッジＣＣ１，ＣＣ２を用いて説明するが、これらの説明に関しては実施例１と同様であるため、実施例３では省略する。まず、実施例３において、検証シナリオＳ１に関する入力パターンＰＸ３１は、以下の通りとなる。
【０２０３】
ＰＸ３１＝（０，ｐ，ｑ，ｒ，ｓ）
【０２０４】
具体的には、検証シナリオＳ１において、図３に示した回路情報３００に入力パターンＰＸ３１を与えて論理シミュレータ５０１により記号シミュレーションを実行する。その実行結果を図１９に示す。図１９は、入力パターンＰＸ３１を与えた場合の記号シミュレーションの実行結果を示す説明図である。図１９において、実行結果ＲＸ３１は、以下の通りとなる。
【０２０５】
【数１】
2006190209.tif 000003
【０２０６】
この式（１）に示した実行結果ＲＸ３１から、信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈに記号（ｐ，ｑ，ｒ，ｓ）が伝播したことがわかるため、コードカバレッジ上限情報ＣＭ３１は、下記の通りとなる。
【０２０７】
【数２】
2006190209.tif 000004
【０２０８】
すなわち、検証シナリオＳ１では、この６つの信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈに関する信号値変化が達成可能と見積もることができる。同様に、検証シナリオＳ２についても、入力パターンＰＸ３２を下記の通り設定する。
【０２０９】
ＰＸ３２＝（Ａ，Ｂ，Ｃ，Ｄ，Ｅ）＝（１，ｐ，ｑ，ｒ，ｓ）
【０２１０】
そして、この入力パターンＰＸ３２を回路情報３００に与えることによって、論理シミュレータ５０１により、記号シミュレーションを実行する。この記号シミュレーションの実行結果ＲＸ３２を図２０に示す。図２０は、入力パターンＰＸ３２を与えた場合の記号シミュレーションの実行結果ＲＸ３２を示す説明図である。図２０において、実行結果ＲＸ３２は、以下の通りとなる。
【０２１１】
【数３】
2006190209.tif 000005
【０２１２】
この式（３）に示した実行結果ＲＸ３２から、信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊに記号（ｐ，ｑ，ｒ，ｓ）が伝播したことがわかるため、コードカバレッジ上限情報ＣＭ３２は、下記の通りとなる。
【０２１３】
【数４】
2006190209.tif 000006
【０２１４】
すなわち、検証シナリオＳ２では、この８つの信号線Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｉ，Ｊに関する信号値変化が達成可能と見積もることができる。
【０２１５】
記号シミュレーションによって得られたコードカバレッジ上限情報ＣＭ３１，ＣＭ３２は、上述した式（２）および式（４）に示したように、記号によって信号変化をあらわすことができる。したがって、実施例１の不定値ｘを用いたコードカバレッジ上限情報ＣＭ１，ＣＭ２よりも正確な情報となり、検証網羅性の向上を図ることができる。
【０２１６】
また、図１８において、変換ツール１８０１は、論理シミュレータ５０１の実行中において、信号線に伝搬した複数の記号から構成される論理式が、所定の記号数以上の論理式となった場合、当該論理式を他の記号に変換する、論理シミュレータ５０１は変換された記号を用いて記号シミュレーションを実行する。
【０２１７】
すなわち、検証対象回路が大規模な回路である場合、論理式が膨大な記号数から構成される場合があり、計算量が増大するため、演算処理時間が長期化する。したがって、この変換ツール１８０１で単一の記号に変換することにより、計算量の増加を防止し、演算処理を簡素化して演算処理時間の短縮化を図ることができる。
【０２１８】
（検証支援処理手順）
つぎに、この実施例３にかかる検証支援処理手順について説明する。図２１−１および図２１−２は、実施例３にかかる検証支援処理手順を示すフローチャートである。図２１−１において、回路情報３００が入力された場合（ステップＳ２１０１：Ｙｅｓ）、ｉを
ｉ＝１にセットする（ステップＳ２１０２）。つぎに、検証シナリオＳｉが入力された場
合（ステップＳ２１０３：Ｙｅｓ）、検証シナリオＳｉ内の入力パターンＰＶｉの可変の値を、記号に置換した入力パターンＰＸ３ｉに設定する（ステップＳ２１０４）。
【０２１９】
つぎに、回路情報３００に入力パターンＰＸ３ｉを与えて３値（０，１，ｘ）の論理シミュレーション、すなわち記号シミュレーションを実行する（ステップＳ２１０５）。記号シミュレーション中に所定の記号数以上の論理式が出現しない場合（ステップＳ２１０６：Ｎｏ）、ステップＳ２１０８に移行する。
【０２２０】
一方、記号シミュレーション中に所定の記号数以上の論理式が出現した場合（ステップＳ２１０６：Ｙｅｓ）、変換ツール１８０１によりその論理式をあらたな記号に変換する（ステップＳ２１０７）。そして、ステップＳ２１０８において、記号シミュレーションが終了していなければ（ステップＳ２１０８：Ｎｏ）、ステップＳ２１０６に移行する。
【０２２１】
また、ステップＳ２１０８において、記号シミュレーションが終了した場合（ステップＳ２１０８：Ｙｅｓ）、コードカバレッジ上限情報ＣＭ３ｉを決定する（ステップＳ２１０９）。このあと、検証シナリオＳｉ内の入力パターンＰＶｉの可変の値を任意の論理値に置換することにより、入力パターンＰｉ（Ｐｉａ，Ｐｉｂ）を設定する（ステップＳ２１１０）。
【０２２２】
そして、図２１−２において、回路情報３００に入力パターンＰｉａを与えて２値（０，１）の論理シミュレーションを実行し（ステップＳ２１１１）、また、回路情報３００に入力パターンＰｉｂを与えて２値（０，１）の論理シミュレーションを実行する（ステップＳ２１１２）。そして、ステップＳ２１１１およびステップＳ２１１２の実行結果から、コードカバレッジＣＣｉを生成する（ステップＳ２１１３）。
【０２２３】
そして、コードカバレッジ上限情報ＣＭ３ｉに対するコードカバレッジＣＣｉの達成度を算出する（ステップＳ２１１４）。この達成度がしきい値以上である場合（ステップＳ２１１５：Ｙｅｓ）、ステップＳ２１１７に移行する。一方、達成度がしきい値以上でない場合（ステップＳ２１１５：Ｎｏ）、コードカバレッジＣＣｉがその検証シナリオＳｉの機能を示すすべての入力パターンを網羅していないこととなる。したがって、そのすべての入力パターンが設定されていない場合（ステップＳ２１１６：Ｎｏ）、ステップＳ２１１０に移行して、入力パターンＰｉを再設定する。一方、このすべての入力パターンが設定された場合（ステップＳ２１１６：Ｙｅｓ）、ステップＳ２１１７に移行する。
【０２２４】
また、ステップＳ２１１７において、ｎを検証シナリオの数とすると、ｉ＝ｎである場合（ステップＳ２１１７：Ｙｅｓ）、一連の処理を終了する。一方、ｉ＝ｎでない場合（ステップＳ２１１７：Ｎｏ）、ｉをインクリメントして（ステップＳ２１１８）、ステップＳ２１０３に移行する。これにより、つぎの検証シナリオＳｉについて検証網羅性を評価することができる。
【０２２５】
この実施例３によれば、上述した実施例１と同様の作用効果を奏することができる。特に記号シミュレーションにおいて記号を用いた論理式によって、伝搬箇所をあらわすことができ、コードカバレッジ上限情報の内容をより正確にあらわすことができる。これにより、検証シナリオＳｉに含まれているすべての入力パターンを実行した場合に達成可能と想定されるコードカバレッジをより正確に網羅することができる。また、変換ツール１８０１を適用することにより、記号シミュレーション中の計算量の増加を防止し、演算処理を簡素化して演算処理時間の短縮化を図ることができる。
【０２２６】
以上説明したように、この発明の実施の形態および実施例１〜３にかかる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法によれば、検証シナリオ毎のコードカバレッジ達成度が十分であるかどうかを定量的に評価できるという効果を奏する。これにより、検証シナリオ毎のコードカバレッジ上限情報を、従来の機能カバレッジやコードカバレッジと同様、検証網羅性の判定に利用できるという効果を奏する。
【０２２７】
特に、検証シナリオ毎のコードカバレッジは、機能とコードの組み合わせパターンをどれだけテストしたかを示しており、機能カバレッジやコードカバレッジを個別に達成するという基準を使うよりも洩れの少ない検証を実現することができるという効果を奏する。
【０２２８】
以上のことから、この発明の検証支援プログラム、記録媒体、検証支援装置、および検証支援方法によれば、コードカバレッジの達成度を見積もることにより、検証シナリオの機能に関する検証網羅性の向上を図り、ＬＳＩの設計障害を正確かつ効率的な検出を図ることができるという効果を奏する。またこれにより、論理シミュレーションの終了時期を的確に判断することができるという効果を奏する。
【０２２９】
なお、本実施の形態および実施例１〜３で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーションなどのコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤなどのコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネットなどのネットワークを介して配布することが可能な伝送媒体であってもよい。
【０２３０】
（付記１）検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得させる取得工程と、
前記取得工程によって取得された回路情報に前記取得工程によって取得された検証シナリオを与えることによって、論理シミュレーションを実行させる第１の実行工程と、
前記実行工程によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定させる決定工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。
【０２３１】
（付記２）前記検証シナリオの可変の値を不定値に置換させる置換工程をコンピュータに実行させ、
前記第１の実行工程は、
前記置換工程によって不定値に置換された検証シナリオを前記検証対象回路の回路情報に与えることによって、論理シミュレーションを実行させ、
前記決定工程は、
前記回路情報内において前記不定値が伝搬した箇所を示すコードカバレッジ上限情報を決定させることを特徴とする付記１に記載の検証支援プログラム。
【０２３２】
（付記３）前記取得工程は、
前記回路情報として、前記検証対象回路のＲＴＬ記述を取得させ、
前記第１の実行工程は、
前記検証シナリオを前記ＲＴＬ記述に与えることによって、論理シミュレーションを実行させ、
前記決定工程は、
前記ＲＴＬ記述内において前記不定値が伝搬した箇所を示すコードカバレッジ上限情報を決定させることを特徴とする付記２に記載の検証支援プログラム。
【０２３３】
（付記４）前記第１の実行工程による論理シミュレーション中に、前記ＲＴＬ記述に含まれている条件分岐文において条件不成立となった場合、前記条件分岐文の分岐先となる他の条件分岐文の実行結果を不定値に変換させる変換工程をコンピュータに実行させ、
前記第１の実行工程は、
前記変換工程によって変換された不定値を用いて論理シミュレーションを継続実行させることを特徴とする付記３に記載の検証支援プログラム。
【０２３４】
（付記５）前記ＲＴＬ記述に条件分岐文がある場合、前記条件分岐文のいずれの分岐先も実行できるように前記ＲＴＬ記述を変換させる変換工程をコンピュータに実行させ、
前記第１の実行工程は、
前記検証シナリオを前記変換工程によって変換されたＲＴＬ記述に与えることによって、論理シミュレーションを実行させることを特徴とする付記３に記載の検証支援プログラム。
【０２３５】
（付記６）前記検証シナリオの可変の値を記号に置換させる置換工程をコンピュータに実行させ、
前記第１の実行工程は、
前記置換工程によって記号に置換された検証シナリオを前記検証対象回路の回路情報に与えることによって、論理シミュレーションを実行させることを特徴とする付記１に記載の検証支援プログラム。
【０２３６】
（付記７）前記第１の実行工程による論理シミュレーション中に、所定数の記号からなる論理式が出現した場合、当該論理式を、当該論理式の記号数よりも少ない数の記号に変換する変換工程をコンピュータに実行させ、
前記第１の実行工程は、
前記変換工程によって変換された記号を用いて論理シミュレーションを継続実行させ、
前記決定工程は、
前記回路情報内において前記記号が伝搬した箇所を示すコードカバレッジ上限情報を決定させることを特徴とする付記６に記載の検証支援プログラム。
【０２３７】
（付記８）前記検証シナリオの可変の値に任意の論理値を与えることによって入力パターンを設定させる設定工程と、
前記設定工程によって設定された入力パターンを前記回路情報に与えることによって、論理シミュレーションを実行させる第２の実行工程と、
前記第２の実行工程によって実行された実行結果に基づいて、前記回路情報に関するコードカバレッジを生成させる生成工程と、
前記決定工程によって決定されたコードカバレッジ上限情報に対する、前記生成工程によって生成されたコードカバレッジの達成度を算出させる算出工程と、
をコンピュータに実行させることを特徴とする付記１〜７のいずれか一つに記載の検証支援プログラム。
【０２３８】
（付記９）前記算出工程によって算出された達成度に基づいて、前記コードカバレッジによる検証網羅性を判定する判定工程をコンピュータに実行させることを特徴とする付記８に記載の検証支援プログラム。
【０２３９】
（付記１０）前記設定工程は、
前記判定工程によって判定された判定結果に基づいて、前記検証シナリオの可変の値に前記任意の論理値とは異なる論理値を与えることによって前記入力パターンとは異なる他の入力パターンを設定させ、
前記第２の実行工程は、
前記設定工程によって設定された他の入力パターンを前記回路情報に与えることによって、前記検証対象回路の論理シミュレーションを実行させ、
前記生成工程は、
前記第２の実行工程によって前記入力パターンを用いて実行された実行結果と前記第２の実行工程によって前記他の入力パターンを用いて実行された実行結果とに基づいて、前記コードカバレッジとは異なる他のコードカバレッジを生成させ、
前記算出工程は、
前記コードカバレッジ上限情報に対する、前記生成工程によって生成された他のコードカバレッジの達成度を算出させることを特徴とする付記９に記載の検証支援プログラム。
【０２４０】
（付記１１）付記１〜１０のいずれか一つに記載の検証支援プログラムを記録したコンピュータに読み取り可能な記録媒体。
【０２４１】
（付記１２）検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得する取得手段と、
前記取得手段によって取得された回路情報に前記取得手段によって取得された検証シナリオを与えることによって、論理シミュレーションを実行する実行手段と、
前記実行手段によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定する決定手段と、
を備えることを特徴とする検証支援装置。
【０２４２】
（付記１３）検証対象回路の回路情報と、前記検証対象回路の機能を検証する可変の値を含んだ検証シナリオと、を取得する取得工程と、
前記取得工程によって取得された回路情報に前記取得工程によって取得された検証シナリオを与えることによって、論理シミュレーションを実行する実行工程と、
前記実行工程によって実行された実行結果に基づいて、前記回路情報内において前記可変の値が伝搬した箇所を示すコードカバレッジ上限情報を決定する決定工程と、
を含んだことを特徴とする検証支援方法。
【産業上の利用可能性】
【０２４３】
以上のように、本発明にかかる検証支援プログラム、記録媒体、検証支援装置、および検証支援方法は、半導体回路の検証に有用であり、特に、大規模回路の検証に適している。
【図面の簡単な説明】
【０２４４】
【図１】この発明の実施の形態にかかる検証支援装置のハードウェア構成を示すブロック図である。
【図２】この発明の実施の形態にかかる検証支援装置の機能的構成を示すブロック図である。
【図３】検証対象回路の回路情報の一例を示す説明図である。
【図４】この発明の実施の形態にかかる検証支援装置の検証支援処理手順を示すフローチャートである。
【図５】実施例１にかかる検証支援装置の概略構成を示す説明図である。
【図６】３値の論理シミュレーションの実行結果ＲＸ１を示す説明図である。
【図７】３値の論理シミュレーションの実行結果ＲＸ２を示す説明図である。
【図８】２値の論理シミュレーションの実行結果Ｒ１ａを示す説明図である。
【図９】２値の論理シミュレーションの実行結果Ｒ１ｂを示す説明図である。
【図１０】２値の論理シミュレーションの実行結果Ｒ２ａを示す説明図である。
【図１１】２値の論理シミュレーションの実行結果Ｒ２ｂを示す説明図である。
【図１２−１】実施例１にかかる検証支援装置の検証支援処理手順を示すフローチャート（その１）である。
【図１２−２】実施例１にかかる検証支援装置の検証支援処理手順を示すフローチャート（その２）である。
【図１３】実施例２にかかる回路情報を示す説明図である。
【図１４】実施例２にかかる検証支援装置の概略構成を示す説明図である。
【図１５−１】実施例２にかかる検証支援装置の検証支援処理手順を示すフローチャート（その１）である。
【図１５−２】実施例２にかかる検証支援装置の検証支援処理手順を示すフローチャート（その２）である。
【図１６】書き換え後のＲＴＬ記述を示す説明図である。
【図１７】実施例２にかかる検証支援装置の他の検証支援処理手順を示すフローチャートである。
【図１８】実施例３にかかる検証支援装置の概略構成を示す説明図である。
【図１９】入力パターンＰＸ３１を与えた場合の記号シミュレーションの実行結果ＲＸ３１を示す説明図である。
【図２０】入力パターンＰＸ３２を与えた場合の記号シミュレーションの実行結果ＲＸ３２を示す説明図である。
【図２１−１】実施例３にかかる検証支援処理手順を示すフローチャート（その１）である。
【図２１−２】実施例３にかかる検証支援処理手順を示すフローチャート（その２）である。
【図２２】論理回路を示す回路図である。
【図２３】論理回路のシミュレーション結果（その１）を示す説明図である。
【図２４】論理回路のシミュレーション結果（その２）を示す説明図である。
【図２５】論理回路のシミュレーション結果（その３）を示す説明図である。
【符号の説明】
【０２４５】
２００  検証支援装置
２０１  取得部
２０２  置換部
２０３  設定部
２０４  実行部
２０５  決定部
２０６  生成部
２０７  算出部
２０８  判定部
２０９  変換部
２１１  第１の実行部
２１２  第２の実行部
３００  回路情報
ＣＣ  コードカバレッジ
ＣＭ  コードカバレッジ上限情報
Ｓ  検証シナリオ
【図１】
2006190209.tif 000007
【図２】
2006190209.tif 000008
【図３】
2006190209.tif 000009
【図４】
2006190209.tif 000010
【図５】
2006190209.tif 000011
【図６】
2006190209.tif 000012
【図７】
2006190209.tif 000013
【図８】
2006190209.tif 000014
【図９】
2006190209.tif 000015
【図１０】
2006190209.tif 000016
【図１１】
2006190209.tif 000017
【図１２−１】
2006190209.tif 000018
【図１２−２】
2006190209.tif 000019
【図１３】
2006190209.tif 000020
【図１４】
2006190209.tif 000021
【図１５−１】
2006190209.tif 000022
【図１５−２】
2006190209.tif 000023
【図１６】
2006190209.tif 000024
【図１７】
2006190209.tif 000025
【図１８】
2006190209.tif 000026
【図１９】
2006190209.tif 000027
【図２０】
2006190209.tif 000028
【図２１−１】
2006190209.tif 000029
【図２１−２】
2006190209.tif 000030
【図２２】
2006190209.tif 000031
【図２３】
2006190209.tif 000032
【図２４】
2006190209.tif 000033
【図２５】
2006190209.tif 000034