(57)【要約】【課題】複数の条件分岐を含む順序回路の検証漏れを防ぎ、バグのないハードウェア設計を実現させる。【解決手段】検証支援装置１００は、検証対象となるＲＴＬ記述１０１を受け付けると、このＲＴＬ記述１０１に含まれる条件分岐の組み合わせを抽出する（ステップＳ１１０）。そして、検証シナリオ１０３によって各組み合わせに関するすべての実行パターンを検証しているか否かを判断するためのタイミング仕様１０２を満たすアサーション情報を生成する（ステップＳ１２０）。【選択図】図１
2010079727.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、
検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を受け付ける受付手段、
前記受付手段によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換手段、
前記変換手段によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定手段、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出手段、
前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述が、前記受付手段によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成する生成手段、
前記生成手段によって生成された各組み合わせのシミュレーションプログラムを前記検証対象となる順序回路のアサーション情報として出力する出力手段、
として機能させることを特徴とする検証支援プログラム。
【請求項２】
前記コンピュータを、さらに、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、あらかじめ指定された条件分岐記述の組み合わせを削除する削除手段として機能させ、
前記組み合わせ抽出手段は、前記削除手段によって特定の組み合わせが削除された後の条件分岐記述の組み合わせの中から、前記指定した条件が成立する可能性のある組み合わせを抽出することを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
前記生成手段は、前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述を同時に成立させるｃｏｖｅｒ文を前記タイミング仕様のタイミング制約を満たすように記述したシミュレーションプログラムを生成することを特徴とする請求項１または２に記載の検証支援プログラム。
【請求項４】
前記コンピュータを、さらに、
前記出力手段によって出力されたアサーション情報を用いて、組み合わせごとに対応付けられたシミュレーションプログラムを実行させた場合の出力値が期待値と等しいか否かに応じて前記検証対象となる順序回路を検証する請求項１〜３のいずれか一つに記載の検証支援プログラム。
【請求項５】
検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を受け付ける受付手段と、
前記受付手段によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換手段と、
前記変換手段によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定手段と、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出手段と、
前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述が、前記受付手段によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成する生成手段と、
前記生成手段によって生成された各組み合わせのシミュレーションプログラムを前記検証対象となる順序回路のアサーション情報として出力する出力手段と、
を備えることを特徴とする検証支援装置。
【請求項６】
入力装置、出力装置および記憶装置を備えるコンピュータが、
検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を前記入力装置から受け付けて前記記憶装置に記憶する受付工程と、
前記受付工程によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換工程と、
前記変換工程によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定工程と、
前記特定工程によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出工程と、
前記組み合わせ抽出工程によって抽出された組み合わせに含まれている条件分岐記述が、前記受付工程によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成して前記記憶装置に記憶する生成工程と、
前記記憶装置に記憶された各組み合わせのシミュレーションプログラムを、前記検証対象となる順序回路のアサーション情報として前記出力装置に出力する出力工程と、
を実行することを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、ハードウェア設計された検証対象回路に対する検証処理を支援する検証支援プログラム、検証支援装置および検証支援方法に関する。
【背景技術】
【０００２】
従来、所望の機能を実現するハードウェア（順序回路）を設計した場合には、実際のハードウェア製造に移行する前段階の処理として設計内容に漏れがないかの論理検証をおこなう作業が必須となる。具体的には、ハードウェアの設計内容に沿った検証シナリオを生成し、この検証シナリオを入力した場合の出力結果を用いて論理検証がおこなわれていた。
【０００３】
また、上述のようにして生成した検証シナリオによる検証処理を客観的に評価するために、検証カバレッジが求められる。検証カバレッジは、検証対象に対するシミュレーションのパターンが十分であるか否かの指標をあらわす情報である。具体的には、たとえば、検証を要するすべてのシミュレーションのパターンを母集団とした場合に、実行したシミュレーションのパターン数の割合によって求めた網羅率が検証カバレッジとして提供される。この場合、検証カバレッジ（網羅率）が高ければ検証精度も高いと判断される。
【０００４】
ここで問題になるのが、母集団となる“検証を要するシミュレーションの全パターン”の抽出の手法である。この母集団に相当するシミュレーションの全パターンをカバレッジ基準という。そして、このカバレッジ基準として、実質的に検証の役に立たないパターンを抽出してしまうと、たとえシミュレーションの網羅率が高くても実際の検証効率の向上にはつながらない場合がある。
【０００５】
そこで、現在は特定の基準に沿って、網羅的にパターンを抽出するパスカバレッジやコードカバレッジという手法が利用されている。パスカバレッジは、検証対象回路に含まれるレジスタにおいて状態遷移を生じるすべてのパスを検証するためのパターンとする。したがって、パスカバレッジでは、これらのパターンの集合がカバレッジ基準となる。また、コードカバレッジは、ラインカバレッジとも呼ばれ、検証対象回路に相当するソースコードの記述されたレジスタの入出力に関するパスを検証するためのパターンとする。コードカバレッジの場合も、これらのパターンの集合がカバレッジ基準となる。
【０００６】
【特許文献１】特開２００６−１９０２０９号公報
【特許文献２】特開２００６−２０１９８０号公報
【非特許文献１】Ｈａｒｒｙ．Ｄ．Ｆｏｓｔｅｒ，他２名「Ａｓｓｅｒｔｉｏｎ−Ｂａｓｅｄ  Ｄｅｓｉｇｎ」（２ｎｄ  Ｅｄｉｔｉｏｎ），「Ｐｒｏｇｒａｍｍｉｎｇ  Ｃｏｄｅ  ｍｅｔｒｉｃｓ」，ｐｐ．１２９−１３０，２００４
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、上述のようなカバレッジ基準を網羅するような検証シナリオを生成して検証をおこなった場合にも、実際に順序回路を動作させると、検証漏れによるバグが発生することがあった。これは、上述したカバレッジ基準が１００％となる検証シナリオであっても、ＲＴＬ記述に対応したハードウェアの仕様として課せられているタイミング制約についての検証を見落としてしまっていたことに起因する。
【０００８】
ここで、ハードウェア実装に課せられるタイミング制約について説明する。図２２は、ハードウェア実装に対する入出力情報を示す説明図である。図２２のように、ハードウェア実装２２００には、入力情報としてリクエスト（ｒｅｑ）２２０１と、条件Ａ２２０２と、条件Ｂ２２０３とが入力される。また、出力情報としてハードウェア実装２２００による処理結果をあらわすデータ２２０４と、ハードウェア実装２２００から正常にデータが出力された旨を通知するａｃｋ（ａｃｋｎｏｗｌｅｄｇｅｍｅｎｔ）信号２２０５が出力される。また、上述したようにハードウェア実装２２００は、順序回路である。したがって、ハードウェアの仕様として、入出力情報に関する制約に加えて、上述したようにタイミングに関する制約がある。
【０００９】
図２３は、ハードウェアの仕様の一例を示す図表である。図表２３００には、図２２のハードウェア実装に要求する仕様が示されている。図表２３００では、ハードウェア実装２２００に対してリクエスト２２０１が入力された場合（「１」の場合）、同じく入力されている条件Ａ２２０２、条件Ｂ２２０３に応じたデータ２２０４を、５サイクル以内に出力するような仕様が求められている。なお、ハードウェア実装２２００からデータ２２０４が出力されている場合には、データ２２０４の出力を報知するためのａｃｋ信号２２０５が出力される。また、リクエスト２２０１が入力されていない場合（「０」の場合）には、データ２２０４、ａｃｋ信号２２０５ともに出力されないため、条件Ａ２２０２、条件Ｂ２２０３ともにどのような値が入力されても出力には関与しない（ｄ．ｃ：ｄｏｎ’ｔ  ｃａｒｅ）。
【００１０】
そして、図２４は、ハードウェアの仕様に対応した動作例を示すタイミングチャートである。ハードウェア実装２２００にリクエスト２２０１が入力（「Ｈｉｇｈ状態」）されていると、ハードウェア記述に応じて、まずは最初のクロック開始タイミングＣ０にて条件Ａ２２０２の判定が開始され、所定のサイクル後（ここでは一例として、条件Ａ２２０２の判定には１サイクルかかるものとする）、つぎのクロック開始タイミングＣ１にて条件Ｂ２２０３の判定を開始する。そして、所定のサイクル後（ここでは一例として、条件Ｂ２２０３の判定には４サイクルかかるものとする）、条件Ｂ２２０３の判定が完了すると、ａｃｋ信号２２０５を出力させる。このａｃｋ信号２２０５に応答して、データ２２０４が出力されると共に、リクエスト２２０１の入力を終了（「Ｌｏｗ状態」）させる。図２４では、リクエスト２２０１の入力からデータ２２０４の出力まで、５サイクルかかっており、タイミング仕様を満たしていることになる。
【００１１】
従来の検証カバレッジのうち、パスカバレッジ基準では、上述のような仕様の下に設計されたハードウェアに対して、条件分岐に応じたパスごとに検証シナリオを生成して検証精度を向上させている。図２５は、検証シナリオごとのカバレッジ範囲を示す図表である。また、図２６は、検証対象回路をあらわすＣＦＧの一例を示す説明図である。検証対象となる回路が、図２６のＣＦＧ２６００のようにあらわされる場合、通常は図表２５００のような検証シナリオが生成される。なお、ＣＦＧ２６００を構成するブロック内の数字は処理に要するサイクル数をあらわしている。
【００１２】
生成された検証シナリオのうち、項ロ、ハ、ニの検証シナリオ２５１０を実行させると、図２６の波線のように、すべてのパスが網羅されていることになる。したがって、項イの検証シナリオ２５２０を利用しない場合や項イの検証シナリオ２５２０を生成しない場合であってもパスカバレッジ基準は網羅率１００％となる。
【００１３】
ハードウェア記述に誤りがなければ、上述のようなカバレッジ基準を満たす検証をおこなうことにより、漏らすことなくバグの発生を見つけることができる。しがしながら、ハードウェア記述に誤りがある場合には、仕様を満たさない場合など、検証の見落としが起こってしまう。
【００１４】
ここで、条件分岐についての検証の見落としが発生する場合について説明する。図２７は、条件分岐ミスの見落とし発生例を示す説明図である。たとえば、タイミング仕様として実装時に条件Ａ２２０２および条件Ｂ２２０３の判別結果を５サイクル以内に出力するような順序回路の設計をおこなう場合、図２７のように、タイミング仕様に準じた正しい記述例（ＣＦＧ２６００）が、設計者による修正ミスなどの何らかの理由によって誤った記述例（ＣＦＧ２７００）に変更されてしまうことがある。
【００１５】
図２８は、条件分岐に応じたサイクル数を示す図表である。図表２８００のように、正しい記述例の場合には、どのような条件分岐パスを辿っても、５サイクル以内にデータ２２０４が出力される。一方、誤った記述例の場合、項ロ、ハ、ニの検証シナリオ２８１０では、仕様通り５サイクル以内にデータ２２０４を出力できるが、項イの検証シナリオ２８２０では、データ２２０４の出力に６サイクルを要してしまう。結果として、誤った記述例では、条件Ａ、条件Ｂともに１のときはバグとなる（図２７のパス２７０１）。すなわち、項イの検証シナリオ２８２０は、バグを検出するために有用な検証シナリオであるが、上述したような従来のカバレッジ基準では、項イの検証シナリオ２８２０は生成されていない可能性が高かった。
【００１６】
また、上述したラインカバレッジをカバレッジ基準とした場合にも、正しい記述例であっても、誤った記述例であっても検証対象となる順序回路に相当するソースコードの記述に対応するパスの検証の有無が問題となる。したがって、図２８にて説明した項ロ、ハ、ニの検証シナリオ２８１０が生成されることにより、網羅率１００％のカバレッジとなってしまう。
【００１７】
このように、従来のカバレッジ基準では、網羅率１００％となるような検証シナリオを生成したとしても、検証対象回路内部の条件分岐に関するカバレッジすべてが網羅されていない場合もあった。
【００１８】
ところが、生成した検証シナリオによって条件分岐に関するカバレッジが網羅されているか否かを確認する技術は提供されていなかった。その結果、図２７にて説明したように、ハードウェア記述が誤った記述例に変更されてしまった場合に、検証処理によって問題点として抽出することができず、バグを含んだハードウェア設計を提供してしまうという問題があった。
【００１９】
この発明は、上述した従来技術による問題点を解消し、複数の条件分岐を含む順序回路の検証漏れを防ぎ、バグのないハードウェア設計を実現させる検証支援プログラム、検証支援装置および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【００２０】
上述した課題を解決し、目的を達成するため、この検証支援プログラム、検証支援装置および検証支援方法は、コンピュータにおいて、検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を受け付ける処理と、受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する処理と、変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する処理と、特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する処理と、抽出された組み合わせに含まれている条件分岐記述が、受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成する処理と、生成された各組み合わせのシミュレーションプログラムを前記検証対象となる順序回路のアサーション情報として出力する処理と、を含むことを要件とする。
【００２１】
この検証支援プログラム、検証支援装置および検証支援方法によれば、検証対象となる順序回路のハードウェア記述に含まれている条件分岐の組み合わせにおいて、指定された条件を成立させ、なおかつ、タイミング仕様を満たすアサーション情報（シミュレーションプログラム）が出力される。したがって、検証漏れの可能性のある条件を指定してアサーション情報を出力させれば、このアサーション情報を利用してシミュレーション検証を実行させ、実行結果から検証漏れの可能性のある条件の検証が網羅されているか否かを確認することができる。
【発明の効果】
【００２２】
この検証支援プログラム、検証支援装置および検証支援方法によれば、ハードウェア設計の検証精度を向上させるため、複数の条件分岐を含むハードウェアの検証漏れを防ぎ、バグのないハードウェア設計を実現させるという効果を奏する。
【発明を実施するための最良の形態】
【００２３】
以下に添付図面を参照して、この検証支援プログラム、検証支援装置および検証支援方法の好適な実施の形態を詳細に説明する。この検証支援プログラム、検証支援装置および検証支援方法では、検証対象となる順序回路に含まれる条件分岐について、検証者が指定した条件と、タイミング仕様とを満たす処理を実行させるためのシミュレーションプログラム（アサーション情報）を生成する。このシミュレーションプログラムを実行させることによって、検証シナリオによって指定した条件を満たし、なおかつ、タイミング仕様を満たす処理が実行されているか否かを判断することができ、検証漏れによるバグの発生を回避することができる。
【００２４】
（検証支援処理の概要）
まず、本実施の形態にかかる検証支援処理の概要について説明する。図１は、本実施の形態にかかる検証支援処理の概要を示す説明図である。検証支援装置１００は、検証対象となるＲＴＬ記述１０１を受け付けると、このＲＴＬ記述１０１に含まれる条件分岐の組み合わせを抽出する（ステップＳ１１０）。その後、検証支援装置１００は、さらにＲＴＬ記述１０１相当のハードウェアの動作に関するタイミング仕様１０２を受け付けて、検証シナリオ１０３によって各組み合わせに関するすべての実行パターンを検証しているか否かを判断するためのアサーション情報を生成する（ステップＳ１２０）。
【００２５】
ここで、図２は、正しい記述例から誤った記述例へ変更されてしまった例を示す説明図である。通常、設計者は、仕様書に基づいてハードウェア設計をおこなう。したがって、まずは、正しい記述例２１０が作成される。その後、設計者は、ハードウェア設計をより効率的なものに改善しようと、記述内容を変更することがある。
【００２６】
具体的には、クロック数の制約やディレイ調整を目的として、記述が示す処理の順序や階層関係を入れ換えることがある。たとえば、正しい記述例２１０において、条件Ａが処理負荷の軽い加算処理の判断であり、条件Ｂが処理負荷の重い乗算処理の判断である場合、設計者は、処理負荷の重い条件Ｂを先に実行させることによって記述全体のクリティカルパスを短くしようとする。ここで述べている処理負荷が重い軽いとは、処理を完了させるのに必要とするクロック数の多少を意味する。たとえば、条件Ａが１の場合は２クロック、０の場合は１クロック要し、条件Ｂが１の場合は４クロック、０の場合は３クロック要するように、処理負荷の重い処理であれば、クロック数も多く、判断処理の完了に時間がかかる。
【００２７】
そこで、図２の場合、設計者は、処理負荷の重い条件Ｂの判断を先に実行させることで、総クロック数を節約しようとする。正しい記述例２１０の場合には、条件Ａの処理負荷が軽いため、処理負荷の重い条件Ｂの判断を先に実行し、つぎに条件Ａの判断を実行させればクリティカルパスへの影響を与えることなく、短いクロック数ですべての処理を完了させられる。記述の内容によっては、内部の処理の順序を入れ換えても、そのまま仕様通りのサイクル数によって所定の機能を実現できる場合もある。しかしながら、正しい記述例２１０の条件Ａと条件Ｂとを入れ換えた場合は、条件Ａ、条件Ｂとが共に１の時に、仕様通りのサイクル数でデータを出力できない誤った記述例２２０となってしまう。
【００２８】
ここで、誤った記述例２２０のように、処理負荷の重い条件Ｂの判断を先に実行するために条件Ａと条件Ｂとの記述順序を入れ換えると、条件Ａ＝条件Ｂ＝１（条件Ａ、条件Ｂともに成立する）という分岐例は発生しないと勘違いしてしまうことがある。これは、正しい記述例２１０の場合には、条件Ａ＝条件Ｂ＝１となる分岐例が発生しなかったためである。
【００２９】
ところが、誤った記述例２２０へと記述を変更してしまった場合には、条件Ａ、条件Ｂが同時に成立するパターンを検証しなければ、条件判定ミスについての検証が漏れてしまう。そこで、本実施の形態の場合、検証者は、図１にて説明したステップＳ１１０において、条件Ａ、条件Ｂが同時に成立する条件分岐の組み合わせを抽出するように設定する。
【００３０】
そして、ステップＳ１１０にて抽出した条件Ａ、条件Ｂが同時に成立するアサーション情報、すなわち、条件Ａ、条件Ｂが同時に成立するようなシミュレーションプログラムを生成する。ここでいう、シミュレーションプログラムの生成とは、たとえば、条件Ａ＝Ｙｅｓかつ条件Ｂ＝Ｙｅｓとなるｃｏｖｅｒ文を生成することによって実現される。さらに、本実施の形態の場合、順序回路を検証対象とするため、タイミング仕様１０２を満たすことが必須となる。したがって、アサーション情報を生成する際には、条件Ａ、条件Ｂが同時に成立し、なおかつ、タイミング仕様１０２を満たすようなｃｏｖｅｒ文を生成する。
【００３１】
図３は、アサーション情報の生成例を示す説明図である。図３のように、本実施の形態の場合、ｃｏｖｅｒ文３００のようにクロックごとに、実行させる条件を記述する。具体的には、ｃｏｖｅｒ文３００では、クロックタイミングＣ１では、リクエスト要求中（Ｈｉｇｈ）かつ条件Ａ＝１となり、クロックタイミングＣ２では、リクエスト要求中となり、クロックタイミングＣ３では、リクエスト要求中かつ条件Ｂ＝１となるようなシミュレーションプログラムとなっている。
【００３２】
また上述したような、ｃｏｖｅｒ文以外にも条件Ａ、条件Ｂが同時に成立するようなシミュレーションを実現する記述であれば、利用するプログラム言語は特に限定されない。したがって、ハードウェア記述との親和性や、設計環境に応じて選択すればよい。このようにして生成されたｃｏｖｅｒ文を実行させることによって、検証対象となるハードウェアに検証者が指定した条件分岐が実行される。
【００３３】
したがって、このアサーション情報を実行した結果、指定した条件分岐が成立したか否かに応じて、検証者が指定した条件分岐（ここでは、条件Ａ、条件Ｂが同時に成立する条件分岐）に関する検証がおこなわれているか否かを判断することができる。検証者が指定した条件分岐の検証がおこなわれていなければ、この検証漏れとなっていた条件分岐に関する検証を実行することで、真の網羅率１００％の検証カバレッジとなる。
【００３４】
以下には、図１にて説明した本実施の形態にかかる検証支援処理を実現する検証支援装置１００と処理手順について説明する。本実施の形態にかかる検証支援処理では、図２にて説明したような正しい記述例２１０において、条件分岐（条件Ａと条件Ｂ）を入れ換えることによって出力結果が変わる条件分岐処理を対象としたアサーション情報が生成される。当然のことながら、記述例の内容が異なれば、検証者は、アサーション情報の生成対象として異なる条件分岐を指定することもできる。
【００３５】
なお、本実施の形態にかかる検証支援処理の場合、どのようなハードウェア記述の場合であっても、複数の条件分岐が含まれるケースがアサーション情報の生成対象となる。ただし、設計者が、個別に条件分岐の優先度を指定している場合には、その指定内容に準じる。なお、優先度の指定とは別に、ハードウェア記述の中の複数の条件分岐が同時に成立しないことがはじめから明らかである旨の指示が明記されている箇所についてもアサーション情報の生成対象外となる。
【００３６】
（検証支援装置のハードウェア構成）
まず、検証支援装置１００のハードウェア構成について説明する。図４は、検証支援装置のハードウェア構成を示すブロック図である。図４において、検証支援装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）４０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）４０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）４０３と、磁気ディスクドライブ４０４と、磁気ディスク４０５と、光ディスクドライブ４０６と、光ディスク４０７と、通信Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）４０８と、入力デバイス４０９と、出力デバイス４１０と、を備えている。また、各構成部はバス４２０によってそれぞれ接続されている。
【００３７】
ここで、ＣＰＵ４０１は、検証支援装置１００の全体の制御を司る。ＲＯＭ４０２は、ブートプログラムや、検証支援プログラムなどの各種プログラムを記憶している。ＲＡＭ４０３は、ＣＰＵ４０１のワークエリアとして使用される。磁気ディスクドライブ４０４は、ＣＰＵ４０１の制御にしたがって磁気ディスク４０５に対するデータのリード／ライトを制御する。磁気ディスク４０５は、磁気ディスクドライブ４０４の制御で書き込まれたデータを記憶する。なお、ＲＯＭ４０２には、検証支援プログラムによって生成されたアサーション情報や、アサーション情報と検証シナリオを用いた検証シミュレーションを実行する検証プログラムが記録されていてもよい。このような場合は、検証支援装置１００によって生成したアサーション情報に留まらず、実際の検証結果まで検証者に提供することができる。
【００３８】
光ディスクドライブ４０６は、ＣＰＵ４０１の制御にしたがって光ディスク４０７に対するデータのリード／ライトを制御する。光ディスク４０７は、光ディスクドライブ４０６の制御で書き込まれたデータを記憶したり、光ディスク４０７に記憶されたデータをコンピュータに読み取らせたりする。
【００３９】
通信インターフェース（以下、「Ｉ／Ｆ」と略する）４０８は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク４１１に接続され、このネットワーク４１１を介して他の装置に接続される。そして、通信Ｉ／Ｆ４０８は、ネットワーク４１１と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。通信Ｉ／Ｆ４０８には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００４０】
入力デバイス４０９は、検証支援装置１００に対しての外部からの入力を受け付ける。入力デバイス４０９としては、具体的には、キーボード、マウスなどが挙げられる。
【００４１】
キーボードの場合、たとえば、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウスの場合、たとえば、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。また、ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４２】
出力デバイス４１０は、検証支援装置１００によって生成された検証シナリオや、検証シナリオによる検証結果などを出力する。出力デバイス４１０としては、具体的には、ディスプレイ、プリンタなどが挙げられる。
【００４３】
ディスプレイの場合、たとえば、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイとしてさらに、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。また、プリンタの場合、たとえば、画像データや文書データを印刷する。さらに、レーザプリンタやインクジェットプリンタを採用することができる。
【００４４】
（検証支援装置の機能的構成）
つぎに、検証支援装置１００の機能的構成について説明する。図５は、検証支援装置の機能的構成を示すブロック図である。検証支援装置１００は、受付部５０１と、変換部５０２と、特定部５０３と、組み合わせ抽出部５０４と、生成部５０５と、出力部５０６と、削除部５０７と、を含む構成である。この制御部となる機能（受付部５０１〜削除部５０７）は、具体的には、たとえば、図４に示したＲＯＭ４０２、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶された検証プログラムをＣＰＵ４０１に実行させることにより、または、通信Ｉ／Ｆ４０８を介して接続された他の装置に実行させることにより、その機能を実現する。
【００４５】
受付部５０１は、検証対象となる順序回路のハードウェア記述の入力と、ハードウェア記述のタイミング制約をあらわすタイミング仕様１０２との入力とを受け付ける。したがって、ここでは、図１にて説明したＲＴＬ記述１０１が検証対象となる順序回路のハードウェア記述１０１として入力され、受付部５０１は、これを受け付ける。なお、受け付けられたハードウェア記述１０１は、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。
【００４６】
変換部５０２は、受付部５０１によって受け付けられたハードウェア記述１０１を、検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する。変換部５０２によって変換されたＣＦＧは、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。このように変換部５０２を用意してＣＦＧに変換することによって、容易に階層関係となる条件分岐記述の組み合わせを特定することができる。
【００４７】
特定部５０３は、変換部５０２によってハードウェア記述がＣＦＧに変換されると、このＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する。階層関係になっている条件分岐記述とは、たとえば、図２の正しい記述例２１０の条件Ａとその下位層に記述されている条件Ｂとの組み合わせである。当然のことながら、抽出された条件分岐のうち、階層関係をもつ組み合わせが複数ある場合は、これら複数の組み合わせをすべて特定する。また、条件Ａ−条件Ｂといった２層の他にさらに、上位もしくは下位に条件分岐がある場合には、３層または４層の組み合わせが特定される。
【００４８】
また、特定部５０３は、受付部５０１によって、ハードウェア記述１０１に含まれる複数の条件分岐について、他の条件分岐と比較した実行優先度をあらわす優先度情報を受け付けた場合には、この優先度情報に基づいて、階層関係となる条件分岐記述の組み合わせを特定してもよい。優先度情報とは、条件分岐の階層関係をあらわす情報であり、たとえば、条件Ａが条件Ｂよりも上位に記述されている場合には、条件Ａ＞条件Ｂと設定されている。特定部５０３は、条件Ａ＞条件Ｂという優先度情報を受け付けると、条件Ａと条件Ｂとの階層関係を特定して出力することができる。なお、いずれの手法によって特定された組み合わせも、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。
【００４９】
組み合わせ抽出部５０４は、特定部５０３によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する。ここで、検証者が指定した条件は、条件分岐がすべて成立する条件であるため、特定部５０３によって特定された条件分岐記述の組み合わせのうち、すべての条件が１（Ｙｅｓ）となる可能性のある組み合わせを抽出する。なお、抽出された組み合わせは、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。
【００５０】
生成部５０５は、組み合わせ抽出部５０４によって抽出された条件分岐記述が、受付部５０１によって受け付けられたタイミング仕様を満たすタイミングにて指定した条件を成立させるシミュレーションプログラムを生成する。ここでは、上述したように、条件分岐がすべて成立する条件が指定されているため、タイミング仕様にて指定されたクロック制約内において、抽出された組み合わせに含まれる条件の判断結果がすべて「１（Ｙｅｓ）」となるシミュレーションプログラムを生成する。ここで生成するシミュレーションプログラムは、上述の条件を成立させるものであれば、どのようなプログラムを用いてもよい。なお、生成されたシミュレーションプログラムは、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。
【００５１】
出力部５０６は、生成部５０５によって生成された各組み合わせのシミュレーションプログラムを検証対象となる順序回路のアサーション情報１０４として出力する。すなわち、抽出した組み合わせごとに、この組み合わせを同時に成立させるシミュレーションプログラムが対応付けられている。出力形式としては、たとえば、ディスプレイへの表示、プリンタへの印刷出力、通信Ｉ／Ｆ４０８による外部装置への送信がある。また、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶することとしてもよい。
【００５２】
以上説明した機能部５０１〜５０６は、本実施の形態にかかる検証支援処理を実現するための、必要最小限の構成となる。検証支援装置１００では、上述したアサーション生成処理を高速に実現するための機能部として、削除部５０７が用意されている。
【００５３】
削除部５０７は、特定部５０３によって特定された条件分岐記述の組み合わせの中から、あらかじめ指定された条件分岐記述の組み合わせを削除する。したがって、削除部５０７からは、削除後の条件分岐記述の組み合わせが出力され、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶される。削除部５０７を利用した場合、組み合わせ抽出部５０４には、削除部５０７によって特定の組み合わせが削除された後の条件分岐記述の組み合わせが入力され、これらの組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する。このように、削除部５０７を用意することによって、組み合わせ抽出部５０４にとって抽出対象となる組み合わせの数を削減できるため、組み合わせ抽出部５０４の処理負荷を軽減させることができる。
【００５４】
検証支援装置１００は、以上説明した機能部５０１〜５０７によって従来検証漏れの可能性があった条件分岐の検証の実行有無を確認するためのアサーション情報１０４を生成する。このアサーション情報１０４を用いて、従来の検証装置によって検証対象となる順序回路の検証をおこなってもよいし、検証支援装置１００にさらに、検証を実行するための機能部を設けてアサーション情報１０４を用いた検証を実現してもよい。したがって、以下には、検証支援装置１００に、図５にて説明したアサーション生成までの機能部と、生成したアサーション情報を用いて検証を実行する機能部との双方を備えた場合における一連の処理手順について説明する。
【００５５】
図６は、検証支援装置によって実行される処理を示す説明図である。図６のように、検証支援装置１００には、アサーション生成処理部６１０と、検証処理部６２０とが含まれている。アサーション生成処理部６１０は、図５にて説明した指定された条件を成立させるためのアサーション情報を生成する処理をおこなう機能部である。また、検証処理部６２０は、アサーション生成処理部６１０によって生成されたアサーション情報を用いて、指定された条件に関する検証が実行されているか否かを判断する機能部である。以下、各機能部６１０，６２０の処理手順について順番に説明する。
【００５６】
＜アサーション生成処理部＞
まず、検証支援装置１００によって実行される処理のうち、アサーション生成処理部６１０によって実行される処理について詳しく説明する。アサーション生成処理部６１０では、大きく分けて条件分岐を抽出する処理（ステップＳ６１１）と、アサーション情報を生成する処理（ステップＳ６１２）とが含まれる。
【００５７】
（ＣＦＧを用いた条件分岐抽出処理の手順）
まず、図６にて説明したアサーション生成処理部６１０における条件分岐を抽出する処理（ステップＳ６１１）の手順について説明する。図７は、条件分岐抽出処理の詳細な手順を示すフローチャートである。図７のフローチャートにおいて、まず、ＲＴＬ記述１０１が入力されたか否かを判断する（ステップＳ７０１）。ここで、ＲＴＬ記述１０１が入力されるまで待ち（ステップＳ７０１：Ｎｏのループ）、ＲＴＬ記述１０１が入力されると（ステップＳ７０１：Ｙｅｓ）、入力されたＲＴＬ記述１０１をＣＦＧに変換する（ステップＳ７０２）。
【００５８】
ここで、ＣＦＧへの変換について説明する。図８は、ＣＦＧの変換例を示す説明図である。ＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）とは、ハードウェア記述の制御の流れをあらわすグラフである。したがって、ＣＦＧ８００は、検証支援装置１００に入力されたＲＴＬ記述１０１における先頭（●）から末尾（◎）までの制御の流れを反映している。ＲＴＬ記述１０１をＣＦＧに変換することによって、各条件分岐同士の階層関係が明確になり、階層関係になっている条件分岐の組み合わせの特定が容易になる。
【００５９】
図７の説明に戻り、ステップＳ７０２において、変換されたＣＦＧから条件分岐の全組み合わせを抽出する（ステップＳ７０３）。そして、ステップＳ７０３において抽出した全組み合わせのうち、階層関係になっている組み合わせを特定する（ステップＳ７０４）。階層関係とは、ＣＦＧにおいて条件分岐同士が直列に接続されている状態を意味する。したがって、図８に例示したＣＦＧ８００の場合は、ＡとＢ、ＡとＢとＥ、ＡとＣ、ＡとＤ、ＢとＥとが階層関係になっていると特定される。そして、ステップＳ７０４によって特定された各組み合わせは、条件分岐情報６０１として出力され（ステップＳ７０５）、一連の条件分岐抽出処理を終了する。
【００６０】
（アサーション情報生成処理の手順）
つぎに、図６にて説明したアサーション生成処理部６１０におけるアサーション情報を生成する処理（ステップＳ６１２）の手順について説明する。図９は、アサーション情報生成処理の詳細な手順を示すフローチャートである。図９のフローチャートにおいて、まず、条件分岐情報６０１が入力されたか否かを判断する（ステップＳ９０１）。このステップＳ９０１では、図７にて説明した条件分岐抽出処理によって抽出された条件分岐情報６０１が入力されたか否かによって判断がおこなわれる。
【００６１】
ステップＳ９０１において、条件分岐情報６０１が入力されるまで待ち（ステップＳ９０１：Ｎｏのループ）、条件分岐情報６０１が入力されると（ステップＳ９０１：Ｙｅｓ）、つぎに、入力された条件分岐情報６０１に含まれている各組み合わせのうち、同時成立の可能性のある組み合わせを抽出する（ステップＳ９０２）。したがって、入力された組み合わせのうち、ＡとＤとの組み合わせは、Ａ＝Ｎｏとなり条件が同時成立しないため削除される。
【００６２】
そして、ステップＳ９０２にて抽出した組み合わせとタイミング仕様１０２から、クロック制約（５クロック以内に出力完了）を満たし、各条件を同時成立（条件Ａ＝条件Ｂ＝１）させるｃｏｖｅｒ文を生成すると（ステップＳ９０３）、最後に、各組み合わせとｃｏｖｅｒ文との情報をアサーション情報１０４として出力し（ステップＳ９０４）、一連のアサーション情報生成処理を終了する。なお、検証対象となる順序回路がＣＦＧ８００のような記述の場合、ＡとＢ、ＡとＣ、ＡとＢとＥ、ＢとＥについてのアサーション情報１０４が生成される。
【００６３】
（ＣＦＧを用いた条件分岐処理の抽出）
つぎに、上述した図７のステップＳ７０３のＣＦＧを用いた条件分岐処理の抽出について詳しく説明する。まず、図１０は、ＣＦＧのデータ構造の一例を示す説明図である。ＣＦＧに変換されたＲＴＬ記述１０１は、分岐ごとに分岐名、条件式、条件式の判断結果がｔｒｕｅまたはｆａｌｓｅの場合の飛び先に関する情報があらわされた、リスト構造１０１０〜１０１４に変換されている。また、検証対象となるＲＴＬ記述１０１に含まれるハードウェアによって並列動作が実行される場合には、分岐名Ａをあらわすリスト構造１０１０のｔｒｕｅの場合の飛び先に関する情報のように、複数の飛び先（分岐名Ｂをあらわすリスト構造１０１１と、分岐名Ｃをあらわすリスト構造１０１２）と分岐が用意されていることもある。
【００６４】
そして、図１１と図１２は、ＣＦＧを用いた優先度関係の抽出処理を示す説明図である。図７のステップ７０３では、各リスト構造１０１０〜１０１４の飛び先に関する情報を参照して、条件分岐記述同士の優先度関係を抽出する。
【００６５】
具体的に説明すると、リスト構造１０１０では、条件式の判断結果がｔｒｕｅまたはｆａｌｓｅの場合の飛び先を参照して、分岐名Ａの条件分岐から下位層に位置する条件分岐記述として分岐名Ｂ，Ｃ，Ｄが抽出される。同様に、リスト構造１０１１では、分岐名Ｂから下位層に位置する条件分岐記述として分岐名Ｅが抽出される。リスト構造１０１２，１０１３，１０１４でも、分岐名Ｃ，Ｄ，Ｅの条件分岐から下位層に位置する条件分岐記述を抽出しようとするが、ｔｒｕｅまたはｆａｌｓｅの場合の飛び先が終了に設定されているため、下位層に位置する条件分岐記述はないと判断される。
【００６６】
さらに、上述したように階層関係になっているとして抽出された組み合わせ同士について、さらに、お互いが階層関係になっているか否かを判断する。ここでは、図１２のように、分岐名Ａから下位層に位置する条件分岐記述として抽出された分岐名Ｂのさらに下位層に分岐名Ｅが位置するため、階層関係になっている条件分岐記述の組み合わせとして、ＡとＢとＥの組み合わせが抽出される。このように、ＣＦＧを用いてリスト構造を参照することによって、条件分岐記述のうち、階層関係をもつ組み合わせとして、ＡとＢ、ＡとＣ、ＡとＤ、ＢとＥ、ＡとＢとＥが抽出される。
【００６７】
（拡張処理：削除条件の採用）
また、上述した検証支援装置１００に拡張処理を加えることによって、処理負荷を軽減させることができる。検証支援装置１００の拡張処理としては、条件分岐の組み合わせの中からあきらかに同時に成立しない条件分岐の組み合わせを削除する処理がある。
【００６８】
図１３は、同時成立しない条件分岐の組み合わせを示す説明図である。検証対象となる順序回路に含まれる条件分岐の組み合わせのうち、同時に成立しないことが明確なものについては、あらかじめアサーション情報１０４の生成対象から除いてもよい。たとえば、ＣＦＧ１３００の場合は、条件Ａと条件Ｂとは排他的な関係にあるため、同時には成立しない。一般的に、ＣＦＧに含まれる条件分岐記述の組み合わせは、「同時に成立する」、「同時に成立するかわからない」、「同時に成立しない」のいずれかに該当する。したがって、記述からあきらかに「同時に成立しない」と判別される組み合わせについては、条件分岐の組み合わせの中から削除して処理負荷の軽減に役立ててもよい。
【００６９】
図１４は、削除条件を用いた拡張処理の手順を示すフローチャートである。削除条件を用いた拡張処理は、上述した条件分岐を抽出する処理（ステップＳ６１１）と、アサーション情報を生成する処理（ステップＳ６１２）との間に挿入され、条件分岐情報６０１の入力をトリガに実行される。図１４のフローチャートにおいて、条件分岐情報６０１の入力後、まず、削除条件を受け付けたか否かを判断する（ステップＳ１４０１）。ここで、削除条件を受け付けた場合（ステップＳ１４０１：Ｙｅｓ）、拡張処理を利用すると判断され、まず、入力された条件分岐情報６０１に含まれる条件分岐の組み合わせのうち、削除条件に該当する条件分岐を含む組み合わせを削除する（ステップＳ１４０２）。
【００７０】
なお、ステップＳ１４０１において、削除条件が受け付けられなかった場合（ステップＳ１４０１：Ｎｏ）、拡張処理を利用しないと判断され、そのまま、ステップＳ６１２の処理に移行する。そして、ステップＳ１４０２によって削除処理が終了した条件分岐の組み合わせを条件分岐情報６０１として出力して（ステップＳ１４０３）、ステップＳ６１２の処理に移行する。
【００７１】
このように、アサーション情報１０４の生成処理に移行する前段に、拡張処理を追加することによって、条件分岐情報６０１から、同時成立する可能性のない組み合わせはあらかじめ削除されるため、より効率的に同時成立する可能性のある組み合わせを特定することができる。
【００７２】
（アサーション情報を用いた検証）
つぎに、アサーション生成処理部６１０によって生成されたアサーション情報１０４を用いて検証対象回路の検証をおこなう検証処理部６２０について説明する。図６に示すように、検証処理部６２０は、アサーション生成処理部６１０によって生成されたアサーション情報１０４から検証したい条件分岐の組み合わせについてのｃｏｖｅｒ文記述６０２が抽出される。そして、検証対象回路のＲＴＬ記述１０１と、検証シナリオ６０３と、検証シナリオ６０３に応じた期待値６０４とを用いてシミュレーション検証が実行される（ステップＳ６２１）。
【００７３】
そして、ステップＳ６２１の検証結果からｃｏｖｅｒ文記述６０２が成立しているか否かを判断する（ステップＳ６２２）。ここで、ｃｏｖｅｒ文記述６０２が成立している（ステップＳ６２２：Ｙｅｓ）と判断された場合は、複数の条件分岐が同時に成立する箇所を含めて期待値６０４通りの動作をしたと判断される（ステップＳ６２３）。この判断は、すなわち、必要な検証シナリオ６０３をすべて有している状態であることを意味している。
【００７４】
一方、ｃｏｖｅｒ文記述６０２が成立していない（ステップＳ６２２：Ｎｏ）と判断された場合は、期待値６０４通りに動作するが、条件分岐が同時に成立する箇所については未検証状態であると判断される（ステップＳ６２４）。これは、検証シナリオ６０３が不足していることを意味する。したがって、ステップＳ６２４と判断された場合には、検証漏れがあるため、検証者は、複数の条件分岐が同時に成立する場合の検証シナリオ６０３を追加するなど、適宜処理をおこなうことができる。
【００７５】
図１５は、ｃｏｖｅｒ文を用いたシミュレーション検証を示す図表である。図表１５００には、上述したシミュレーション検証の結果に応じた検証対象回路の検証状態があらわされている。なお、期待値６０４とシミュレーションによる出力とが不一致の場合には、ＲＴＬ記述１０１自体に期待値通り動作しないバグが存在すると判断される。したがって、検証者は、このバグを解消するための処理をおこなうことができる。
【００７６】
このように、本実施の形態にかかる検証支援装置１００では、従来のラインカバレッジやパスカバレッジによって網羅率１００％となるような検証シナリオであっても依然として解決していなかった検証漏れを、条件分岐における特定の状態成立に着目することで、検出することができる。
【００７７】
（実行例）
つぎに、具体的な数値を挙げた場合の実行例について説明する。まず、仕様としては、条件Ａ、条件Ｂがいずれの値になっても、５サイクル以内にデータを出力するように設定されている。このとき、図１６は、正しい実装例を示す説明図である。検証対象回路１１０１のパスカバレッジを１００％にするには、下記のようなパスカバレッジ１００％となる検証シナリオを与えればよい。検証シナリオによって検証を実行した場合、図表１６００に示したように、いずれの場合も、５サイクル以内にデータを出力し、仕様を満たす順序回路であると判断される。
【００７８】
・入力：条件Ａ＝１、条件Ｂ＝０  期待値：５サイクル以内にデータを出力
・入力：条件Ａ＝０、条件Ｂ＝１  期待値：５サイクル以内にデータを出力
・入力：条件Ａ＝０、条件Ｂ＝０  期待値：５サイクル以内にデータを出力
【００７９】
一方、図１７は誤った実装例を示す説明図である。図２にて説明したように、検証対象回路１７０１は、設計対象回路１１０１の処理効率を上げようと、設計者によって記述を一部修正した誤った実装例（条件Ａと条件Ｂとの階層関係が変更）にされてしまっている。設計者は、誤りに気づいていないため、検証対象回路１７０１に対しても、上述した仕様（５サイクル以内にデータ出力）が要求されるため、同様の検証シナリオ６０３が与えられてしまう。
【００８０】
しかしながら、図表１７００のように、誤った実装例でありながら、上述した検証シナリオでは、パスカバレッジ１００％にもかかわらず、誤った実装箇所についての検証がなされずに、バグを見逃してしまう。そこで、検証対象回路１７０１のように、設計者が条件分岐を修正した回路については、アサーション情報１０４を生成して検証漏れがあるか否かを確認する必要がある。
【００８１】
図１８は、同時成立の可能性のある条件分岐の抽出例を示す説明図である。図１８のように、誤った実装のＣＦＧをあらわす検証対象回路１７０１から、条件Ｂのデータの流れをあらわすリスト構造１と、条件Ａのデータの流れをあらわすリスト構造２とを取得し、直列に接続されている条件分岐を階層関係になっている組み合わせであると特定する。また、あらかじめ、条件Ｂ＞条件Ａのような、条件分岐記述同士の優先度が指定されている場合には、この優先度を参照して、条件Ｂと条件Ａとの階層関係を特定することができる。
【００８２】
図１８にて説明したようにＣＦＧから階層関係になっている条件分岐の組み合わせを特定すると、つぎに、条件Ａ，Ｂが同時に成立する条件のアサーション情報１０４を生成する。図１９は、ｃｏｖｅｒ文の生成例を示す説明図である。まず、階層関係になっていると特定された条件分岐の組み合わせを同時成立させるためのｃｏｖｅｒ文１９０１を生成する。その後、生成されたｃｏｖｅｒ文１９０１に、タイミング仕様１０２を追加することによって条件分岐の組み合わせを同時成立させ、なおかつタイミング仕様１０２を満たすｃｏｖｅｒ文１９０２が生成される。
【００８３】
ｃｏｖｅｒ文１９０２に記述された「ｒｏｓｅ（ｒｅｑ）＆＆条件Ｂ」は、最初の１サイクル目において、リクエスト（ｒｅｑ）入力を示す立ち上がりと同時に条件Ｂ＝１とさせるＳＰＬ記述である。また、つぎに記述された「ｒｅｑ」は、２サイクル目において、リクエスト（ｒｅｑ）の入力状態を保持させるＳＰＬ記述である。そして、「ｒｅｑ＆＆条件Ａ」は、３サイクル目において、条件Ａ＝１とさせるＳＰＬ記述である。このように、アサーション文法を用いて、条件分岐の組み合わせごとに、指定した条件を成立させ、なおかつタイミング仕様１０２を満たすアサーション情報１０４を生成することができる。
【００８４】
つぎに、図２０は、ｃｏｖｅｒ文を用いたシミュレーション検証の実施例を示す図表である。図１９にて説明した手順によってアサーション情報１０４が生成されると、検証対象となる順序回路のＲＴＬ記述１０１、検証シナリオ６０３、期待値６０４、アサーション情報１０４から抽出したｃｏｖｅｒ文記述６０２（ここでは、ｃｏｖｅｒ｛ｒｏｓｅ（ｒｅｑ）＆＆条件Ｂ；ｒｅｑ；（ｒｅｑ＆＆条件Ａ）｝）を用いて、シミュレーション検証をおこなう（ステップＳ６２１）。
【００８５】
なお、ステップＳ６２１によるシミュレーション検証は、図６にて説明したシミュレーション検証と同様の処理であるが、図６の処理に、ステップＳ６２１の処理後、シミュレーション出力が期待値６０４と等しいか否かの判断（ステップＳ６３０）を追加してもよい。このステップＳ６３０によって、シミュレーション出力が期待値６０４と等しいと判断された場合（ステップＳ６３０：Ｙｅｓ）、そのままステップＳ６２２の処理に移行し、シミュレーション出力が期待値６０４と等しくないと判断された場合（ステップＳ６３０：Ｎｏ）、ＲＴＬ記述１０１に期待値６０４通りに動作しない原因となるバグが有ると判断される（ステップＳ６３１）。なお、ステップＳ６２２以降の処理は図６にて説明したため、ここでは省略する。
【００８６】
そして、図２１は、シミュレーション結果の出力例を示す図表である。図２０にて説明したシミュレーション検証の結果に応じた出力例に応じて、それぞれ図表２１００のように判定される。検証者は、この判定結果を参照して、検証シナリオ６０３の漏れを特定し、不足している検証シナリオ６０３を補完することによって、真の網羅率１００％となる検証カバレッジを実現することができる。
【００８７】
以上説明したように、本実施の形態によれば、検証者が指定した条件分岐が検証されているか否かを確認するためのアサーション情報を生成する。具体的には、入力されたＲＴＬ記述から、階層関係になっている条件分岐の組み合わせを抽出し、これら抽出した組み合わせが指定した条件を成立させるためのシミュレーションプログラムを生成して、このシミュレーションプログラムの成立状態に応じて検証の有無を判断することができる。結果として、従来の検証カバレッジでは漏れてしまっていた条件分岐に関する検証も網羅可能となり、ハードウェア設計の検証精度をより向上させることができる。
【００８８】
また、検証支援装置１００では、アサーション情報を生成する機能と、生成したアサーション情報を用いてシミュレーション検証をおこなう機能との双方を搭載した構成になっているが、アサーション情報を生成する機能のみを搭載した装置であってもよい。検証支援装置１００によって生成したアサーション情報を他の検証装置によってどのように利用させてもよい。
【００８９】
なお、本実施の形態で説明した検証支援方法は、あらかじめ用意されたプログラムをパーソナル・コンピュータやワークステーションなどのコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤなどのコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また、このプログラムは、インターネットなどのネットワークを介して配布することが可能な媒体であってもよい。
【００９０】
また、本実施の形態で説明した検証支援装置１００は、スタンダードセルやストラクチャードＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）などの特定用途向けＩＣ（以下、単に「ＡＳＩＣ」と称す。）やＦＰＧＡなどのＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）によっても実現することができる。具体的には、たとえば、上述した検証支援装置１００の機能（受付部５０１〜削除部５０７）をＨＤＬ記述によって機能定義し、そのＨＤＬ記述を論理合成してＡＳＩＣやＰＬＤに与えることにより、検証支援装置１００を製造することができる。
【００９１】
上述した実施の形態に関し、さらに以下の付記を開示する。
【００９２】
（付記１）コンピュータを、
検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を受け付ける受付手段、
前記受付手段によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換手段、
前記変換手段によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定手段、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出手段、
前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述が、前記受付手段によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成する生成手段、
前記生成手段によって生成された各組み合わせのシミュレーションプログラムを前記検証対象となる順序回路のアサーション情報として出力する出力手段、
として機能させることを特徴とする検証支援プログラム。
【００９３】
（付記２）前記コンピュータを、さらに、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、あらかじめ指定された条件分岐記述の組み合わせを削除する削除手段として機能させ、
前記組み合わせ抽出手段は、前記削除手段によって特定の組み合わせが削除された後の条件分岐記述の組み合わせの中から、前記指定した条件が成立する可能性のある組み合わせを抽出することを特徴とする付記１に記載の検証支援プログラム。
【００９４】
（付記３）前記特定手段は、前記受付手段によって、前記条件分岐記述を他の条件分岐と比較した実行優先度をあらわす優先度情報が受け付けられた場合、当該優先度情報に基づいて、階層関係となる条件分岐記述の組み合わせを特定することを特徴とする付記１または２に記載の検証支援プログラム。
【００９５】
（付記４）前記生成手段は、前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述を同時に成立させるｃｏｖｅｒ文を前記タイミング仕様のタイミング制約を満たすように記述したシミュレーションプログラムを生成することを特徴とする付記１〜３のいずれか一つに記載の検証支援プログラム。
【００９６】
（付記５）前記生成手段は、前記受付手段において、前記検証対象となる順序回路の動作に関するクロック数の制限が前記タイミング仕様として受け付けられた場合、当該クロック数の制約を満たすシミュレーションプログラムを生成することを特徴とする付記１〜４のいずれか一つに記載の検証支援プログラム。
【００９７】
（付記６）前記コンピュータを、さらに、
前記出力手段によって出力されたアサーション情報を用いて、組み合わせごとに対応付けられたシミュレーションプログラムを実行させた場合の出力値が期待値と等しいか否かに応じて前記検証対象となる順序回路を検証する付記１〜５のいずれか一つに記載の検証支援プログラム。
【００９８】
（付記７）検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を受け付ける受付手段と、
前記受付手段によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換手段と、
前記変換手段によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定手段と、
前記特定手段によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出手段と、
前記組み合わせ抽出手段によって抽出された組み合わせに含まれている条件分岐記述が、前記受付手段によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成する生成手段と、
前記生成手段によって生成された各組み合わせのシミュレーションプログラムを前記検証対象となる順序回路のアサーション情報として出力する出力手段と、
を備えることを特徴とする検証支援装置。
【００９９】
（付記８）入力装置、出力装置および記憶装置を備えるコンピュータが、
検証対象となる順序回路のハードウェア記述と、当該ハードウェア記述のタイミング制約をあらわすタイミング仕様との入力を前記入力装置から受け付けて前記記憶装置に記憶する受付工程と、
前記受付工程によって受け付けられたハードウェア記述を、前記検証対象となる順序回路の制御の流れをあらわすＣＦＧ（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ）に変換する変換工程と、
前記変換工程によって変換されたＣＦＧの中から、並列に接続されている条件分岐記述同士を階層関係となる条件分岐記述の組み合わせとして特定する特定工程と、
前記特定工程によって特定された条件分岐記述の組み合わせの中から、指定した条件が成立する可能性のある組み合わせを抽出する組み合わせ抽出工程と、
前記組み合わせ抽出工程によって抽出された組み合わせに含まれている条件分岐記述が、前記受付工程によって受け付けられたタイミング仕様を満たすタイミングにて前記指定した条件を成立させるシミュレーションプログラムを生成して前記記憶装置に記憶する生成工程と、
前記記憶装置に記憶された各組み合わせのシミュレーションプログラムを、前記検証対象となる順序回路のアサーション情報として前記出力装置に出力する出力工程と、
を実行することを特徴とする検証支援方法。
【図面の簡単な説明】
【０１００】
【図１】本実施の形態にかかる検証支援処理の概要を示す説明図である。
【図２】正しい記述例から誤った記述例へ変更されてしまった例を示す説明図である。
【図３】アサーション情報の生成例を示す説明図である。
【図４】検証支援装置のハードウェア構成を示すブロック図である。
【図５】検証支援装置の機能的構成を示すブロック図である。
【図６】検証支援装置によって実行される処理を示す説明図である。
【図７】条件分岐抽出処理の詳細な手順を示すフローチャートである。
【図８】ＣＦＧの変換例を示す説明図である。
【図９】アサーション情報生成処理の詳細な手順を示すフローチャートである。
【図１０】ＣＦＧのデータ構造の一例を示す説明図である。
【図１１】ＣＦＧを用いた優先度関係の抽出処理を示す説明図（その１）である。
【図１２】ＣＦＧを用いた優先度関係の抽出処理を示す説明図（その２）である。
【図１３】同時成立しない条件分岐の組み合わせを示す説明図である。
【図１４】削除条件を用いた拡張処理の手順を示すフローチャートである。
【図１５】ｃｏｖｅｒ文を用いたシミュレーション検証を示す図表である。
【図１６】正しい実装例を示す説明図である。
【図１７】誤った実装例を示す説明図である。
【図１８】同時成立の可能性のある条件分岐の抽出例を示す説明図である。
【図１９】ｃｏｖｅｒ文の生成例を示す説明図である。
【図２０】ｃｏｖｅｒ文を用いたシミュレーション検証の実施例を示す説明図である。
【図２１】シミュレーション結果の出力例を示す図表である。
【図２２】ハードウェア実装に対する入出力情報を示す説明図である。
【図２３】ハードウェアの仕様の一例を示す図表である。
【図２４】ハードウェアの仕様に対応した動作例を示すタイミングチャートである。
【図２５】検証シナリオごとのカバレッジ範囲を示す図表である。
【図２６】検証対象回路をあらわすＣＦＧの一例を示す説明図である。
【図２７】条件分岐ミスの見落とし発生例を示す説明図である。
【図２８】条件分岐に応じたサイクル数を示す図表である。
【符号の説明】
【０１０１】
１００  検証支援装置
１０１  ＲＴＬ記述
１０２  タイミング仕様
１０３  検証シナリオ
１０４  アサーション情報
５０１  受付部
５０２  変換部
５０３  特定部
５０４  組み合わせ抽出部
５０５  生成部
５０６  出力部
５０７  削除部
６０１  条件分岐情報
６０２  ｃｏｖｅｒ文記述
６０３  検証シナリオ
６０４  期待値
６１０  アサーション生成処理部
６２０  検証処理部
【図１】
2010079727.tif 000003
【図２】
2010079727.tif 000004
【図３】
2010079727.tif 000005
【図４】
2010079727.tif 000006
【図５】
2010079727.tif 000007
【図６】
2010079727.tif 000008
【図７】
2010079727.tif 000009
【図８】
2010079727.tif 000010
【図９】
2010079727.tif 000011
【図１０】
2010079727.tif 000012
【図１１】
2010079727.tif 000013
【図１２】
2010079727.tif 000014
【図１３】
2010079727.tif 000015
【図１４】
2010079727.tif 000016
【図１５】
2010079727.tif 000017
【図１６】
2010079727.tif 000018
【図１７】
2010079727.tif 000019
【図１８】
2010079727.tif 000020
【図１９】
2010079727.tif 000021
【図２０】
2010079727.tif 000022
【図２１】
2010079727.tif 000023
【図２２】
2010079727.tif 000024
【図２３】
2010079727.tif 000025
【図２４】
2010079727.tif 000026
【図２５】
2010079727.tif 000027
【図２６】
2010079727.tif 000028
【図２７】
2010079727.tif 000029
【図２８】
2010079727.tif 000030