(57)【特許請求の範囲】
【請求項１】
コンピュータに、
回路を第１のフリップフロップモデルによってモデル化した第１の回路モデルの入力端子に対して外部から入力データを与えてシミュレーションすることによって、前記第１の回路モデル内の状態変数の状態変化を検出する第１の検出手順と、
前記第１の検出手順により状態変化が検出される都度、前記第１の回路モデル内の状態と検出時刻とを順に保持する第１の保持手順と、
前記第１のフリップフロップモデルと異なる第２のフリップフロップモデルであってメタステーブル状態による影響を模擬可能な第２のフリップフロップモデルによって前記回路をモデル化した第２の回路モデルの入力端子に外部から前記入力データを与えてシミュレーションすることによって、前記第２の回路モデル内の状態変数の状態変化を検出する第２の検出手順と、
前記第２の検出手順により状態変化が検出される都度、前記第２の回路モデル内の状態と検出時刻とを順に保持する第２の保持手順と、
前記第１および第２の保持手順により保持されている順に各状態に違いがあるか否かを判断し、さらに、違いがないと判断された場合、前記第１の保持手順により保持されている各状態での検出時刻から前記第２の保持手順により保持されている各状態での検出時刻までの時間が、指定時間以内であるかを判断する判断手順と、
前記判断手順により判断された判断結果を出力する出力手順と、
を実行させることを特徴とする検証支援プログラム。
【請求項２】
第１の変数の変化を検出し、第２の変数の変化を検出し、検出した前記第１の変数の変化の系列と検出した前記第２の変数の変化の系列とに違いがあるか否かを判断し、判断結果を出力する比較器モデルを記憶する記憶装置にアクセス可能なコンピュータに、
回路を第１のフリップフロップモデルによってモデル化した第１の回路モデル内で状態を表す変数と前記変数のビット幅を、指定ビット幅および指定条件に基づいて検出する検出手順と、
前記比較器モデル内の前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記検出手順により検出された変数のビット幅に設定する設定手順と、
前記設定手順による設定後の比較器モデルにおいて、前記第１の変数に、前記第１の回路モデル内の前記変数を与え、前記第２の変数に、前記第１のフリップフロップモデルと異なる第２のフリップフロップモデルであってメタステーブル状態による影響を模擬可能な第２のフリップフロップモデルによって前記回路をモデル化した第２の回路モデル内で前記変数と同一変数を与えることにより、前記第１の回路モデルと前記第２の回路モデルと前記比較器モデルとが組み合わさったシミュレーションモデルを構築する構築手順と、
を実行させることを特徴とする検証支援プログラム。
【請求項３】
前記コンピュータに、
前記第１の回路モデル内の各変数に対応するノードを生成してグラフを生成するノード生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の回路モデル内の代入文における右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成する第１のエッジ生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の回路モデル内の条件文に含まれる変数に対応するノードから前記条件文により実行される代入文の左辺の変数に対応するノードへの有向エッジを生成する第２のエッジ生成手順と、
前記第１および第２のエッジ生成手順により有向エッジが生成されたグラフ内の指定変数に対応するノードから前記有向エッジを辿って前記検出手順により検出された変数に対応するノードを探索する探索手順と、を実行させ、
前記設定手順は、
前記探索手順により探索された場合、前記比較器モデルの前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記変数のビット幅に設定することを特徴とする請求項２に記載の検証支援プログラム。
【請求項４】
前記探索手順は、
前記第１および第２のエッジ生成手順により有向エッジが生成されたグラフ内の指定変数に対応するノードから前記有向エッジを辿って前記検出手順により検出された変数に対応するノードを指定回数以内で探索し、
前記設定手順は、
前記探索手順により探索された場合、前記比較器モデルの前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記変数のビット幅に設定することを特徴とする請求項３に記載の検証支援プログラム。
【請求項５】
回路を第１のフリップフロップモデルによってモデル化した第１の回路モデルの入力端子に対して外部から入力データを与えてシミュレーションすることによって、前記第１の回路モデル内の状態変数の状態変化を検出する第１の検出手段と、
前記第１の検出手段により状態変化が検出される都度、前記第１の回路モデル内の状態と検出時刻とを順に保持する第１の保持手段と、
前記第１のフリップフロップモデルと異なる第２のフリップフロップモデルであってメタステーブル状態による影響を模擬可能な第２のフリップフロップモデルによって前記回路をモデル化した第２の回路モデルの入力端子に外部から前記入力データを与えてシミュレーションすることによって、前記第２の回路モデル内の状態変数の状態変化を検出する第２の検出手段と、
前記第２の検出手段により状態変化が検出される都度、前記第２の回路モデル内の状態と検出時刻とを順に保持する第２の保持手段と、
前記第１および第２の保持手段により保持されている順に各状態に違いがあるか否かを判断し、さらに、違いがないと判断された場合、前記第１の保持手段により保持されている各状態での検出時刻から前記第２の保持手段により保持されている各状態での検出時刻までの時間が、指定時間以内であるかを判断する判断手段と、
前記判断手段により判断された判断結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。
【請求項６】
第１の変数の変化を検出し、第２の変数の変化を検出し、検出した前記第１の変数の変化の系列と検出した前記第２の変数の変化の系列とに違いがあるか否かを判断し、判断結果を出力する比較器モデルを記憶する記憶装置にアクセス可能な検証支援装置であって、
回路を第１のフリップフロップモデルによってモデル化した第１の回路モデル内で状態を表す変数と前記変数のビット幅を、指定ビット幅および指定条件に基づいて検出する検出手段と、
前記比較器モデル内の前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記検出手段により検出された変数のビット幅に設定する設定手段と、
前記設定手段による設定後の比較器モデルにおいて、前記第１の変数に、前記第１の回路モデル内の前記変数を与え、前記第２の変数に、前記第１のフリップフロップモデルと異なる第２のフリップフロップモデルであってメタステーブル状態による影響を模擬可能な第２のフリップフロップモデルによって前記回路をモデル化した第２の回路モデル内で前記変数と同一変数を与えることにより、前記第１の回路モデルと前記第２の回路モデルと前記比較器モデルとが組み合わさったシミュレーションモデルを構築する構築手段と、
を備えることを特徴とする検証支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、半導体集積回路の検証を支援する検証支援プログラム、検証支援方法、および検証支援装置に関する。
【背景技術】
【０００２】
従来、半導体集積回路には、何種類ものクロックが存在し、一般的に、クロック供給の対象となるブロック単位はクロックドメインと呼ばれている。そして、異なるクロックドメイン間でデータが受け渡されることは、ＣＤＣ（Ｃｌｏｃｋ  Ｄｏｍａｉｎ  Ｃｒｏｓｓｉｎｇ）と呼ばれている。
【０００３】
１つのクロックドメイン（以下、「送信クロックドメイン」と称す。）のデータが、異なるクロックドメイン（以下、「受信クロックドメイン」と称す。）で用いられるクロックのタイミングに関わらず、受信クロックドメインへ受け渡される。
【０００４】
受信クロックドメイン内のクロックのタイミングに関わらずデータが入力されるため、セットアップタイムまたはホールドタイム違反となりフリップフロップ（以下、「ＦＦ（Ｆｌｉｐ  Ｆｌｏｐ）」と称す。）の出力にメタステーブル状態が発生することがある。
【０００５】
メタステーブル状態は、論理値０とも論理値１とも判定される可能性を持った、不安定な状態である。メタステーブル状態の影響が論理値の差異として後段のＦＦや組合せ回路に伝播し、半導体集積回路が誤動作することがある。
【０００６】
したがって、半導体集積回路内にＣＤＣが存在する限りメタステーブル状態を無くすことはできないが、メタステーブル状態が発生しても半導体集積回路に誤動作が発生しないことを検証する必要があった。しかしながら、通常のＦＦのモデルを使用した論理検証では、メタステーブル状態の影響が考慮されない。
【０００７】
図２５は、通常のＦＦモデルによる論理検証の一例を示す説明図である。回路モデル１では、送信クロックドメイン内の送信ＦＦの出力と受信クロックドメイン内の受信ＦＦの入力とが接続されている。そして、タイミングチャートでは、送信ＦＦから出力されるデータ（Ｓ１）が、受信ＦＦに受け渡される際にｃｌｋ２のセットアップタイムを違反している場合を示している。しかしながら、受信ＦＦの出力データ（Ｓ２）は、論理値１を出力している。
【０００８】
図２５で示すようにメタステーブル状態の影響が考慮されないため、受信ＦＦのモデルをメタステーブル状態による影響を模擬可能なモデル（以下、「ＣＤＣモデル」）に変更して検証（以下、「ＣＤＣ検証」と称する。）が行われていた（たとえば、下記特許文献１を参照。）。
【０００９】
図２６は、ＣＤＣモデルによる論理検証の一例を示す説明図である。回路モデル２では、送信クロックドメイン内の送信ＦＦの出力と受信クロックドメイン内の受信ＦＦの入力とが接続されている。受信ＦＦが、ＣＤＣモデルとなっている。そして、タイミングチャートでは、送信ＦＦから出力されるデータ（Ｓ１）が、受信ＦＦに受け渡される際にｃｌｋ２のセットアップタイムを違反している場合を示している。
【００１０】
セットアップタイムを違反しているため受信ＦＦの出力データ（Ｓ２）は、メタステーブル状態を出力している。したがって、ｃｌｋ２の次の立ち上がりでは、Ｓ２を入力データとするＦＦがメタステーブル状態を取り込み予測不能な論理値（０または１）が現れる。
【００１１】
また、ＣＤＣ検証では、メタステーブル状態の影響が検証結果に含まれているため、障害要因の分析が難しい。したがって、通常では、まず、モデル変更前の論理検証（以下、「機能検証」と称する。）により通常の機能に問題が無いことが確認される。つぎに、ＣＤＣ検証により機能検証で用いた入力パターンと同一パターンを用いてＣＤＣモデルによってランダム動作が加わっても設計仕様に違反する動作が発生しないことが確認される。
【００１２】
また、テストにおいて、ＣＤＣで発生する故障を検出するか突き止めるＤＦＴ（Ｄｅｓｉｇｎ  Ｆｏｒ  Ｔｅｓｔ）システムが知られている（たとえば、下記特許文献２を参照。）。
【先行技術文献】
【特許文献】
【００１３】
【特許文献１】特開２００９−９３１８号公報
【特許文献２】特表２００４−５３０８６５号公報
【発明の概要】
【発明が解決しようとする課題】
【００１４】
しかしながら、入力パターンは、あくまで機能検証に特化して作成されたパターンであって、ＣＤＣ検証に適した入力パターンであるとは限らなかった。よって、従来では、ＣＤＣに起因する障害により誤った内部状態に遷移した場合であっても、入力パターンによっては、障害による影響が外部出力まで伝播しない可能性があり、誤動作の検出に漏れが発生する可能性があるという問題点があった。
【００１５】
また、ＣＤＣは半導体集積回路内に何千箇所とあり、各ＣＤＣから障害を判定する箇所（たとえば、出力端子）までの論理回路上での距離が離れているため、障害原因であるＣＤＣの特定が困難であるという問題点があった。
【００１６】
さらに、正しく設計された論理回路であっても、障害を判定する箇所とＣＤＣとの距離が複数のＦＦや組み合わせ回路を介すなどして離れているため、信号変化タイミング（サイクル単位）のずれとして現れる。したがって、通常の機能検証との結果とＣＤＣ検証との結果を単純にサイクルごとに比較すると、数多くの不一致が検出されてしまい、正常動作であっても誤動作であると誤判定してしまうという問題点があった。
【００１７】
本発明は、上述した従来技術による問題点を解消するため、メタステーブル状態の影響により発生する誤動作を正確に検証でき、状態変化の系列を用いて誤判定を抑制することができる検証支援プログラム、検証支援方法、および検証支援装置を提供することを目的とする。
【課題を解決するための手段】
【００１８】
本発明の一観点によれば、入力データが対象回路に与えられた場合における前記対象回路内の状態変化を検出する第１の検出手段と、前記入力データの一部が変更されて前記対象回路に与えられた場合における前記対象回路内の状態変化を検出する第２の検出手段と、前記第１の検出手段により検出された状態変化と前記第２の検出手段により検出された状態変化とに違いがあるか否かを判断する判断手段と、前記判断手段により判断された判断結果を出力する出力手段と、を備える検証支援装置が提供される。
【発明の効果】
【００１９】
本検証支援プログラム、検証支援方法、および検証支援装置によれば、メタステーブル状態の影響により発生する誤動作を正確に検証でき、状態変化の系列を用いて誤判定を抑制することができるという効果を奏する。
【図面の簡単な説明】
【００２０】
【図１】本発明の一実施例を示す説明図（その１）である。
【図２】検証対象回路のＲＴＬ記述の一例を示す説明図である。
【図３】比較器のテンプレートの一例を示す説明図である。
【図４】検証支援装置のハードウェア構成を示すブロック図である。
【図５】実施の形態１にかかる検証支援装置の機能的構成を示すブロック図である。
【図６】状態変数として検出された検出結果の一例を示す説明図である。
【図７】実施の形態１にかかる検証支援装置５００による検証支援処理手順の一例を示すフローチャートである。
【図８】図７で示した検出処理（ステップＳ７０２）の詳細な説明を示すフローチャートである。
【図９】図７で示した検出処理（ステップＳ７０３）の詳細な説明を示すフローチャートである。
【図１０】図７で示した検出処理（ステップＳ７０４）の詳細な説明を示すフローチャートである。
【図１１】図７で示した構築処理（ステップＳ７０５）の詳細な説明を示すフローチャートである。
【図１２】受信ＦＦリストの一例を示す説明図である。
【図１３】ノード生成結果の一例を示す説明図である。
【図１４】第１のエッジ生成部５０３による有向エッジ生成結果の一例を示す説明図である。
【図１５】第２のエッジ生成部５０４による有向エッジ生成結果の一例を示す説明図である。
【図１６】実施の形態２にかかる検証支援装置５００による検証支援処理手順の一例を示すフローチャートである。
【図１７】図１６で示したグラフ生成処理（ステップＳ１６０３）の詳細な説明を示すフローチャートである。
【図１８】図１６で示した決定処理（ステップＳ１６０４）の詳細な説明を示すフローチャートである。
【図１９】図１８で示した探索処理（ステップＳ１８０６）の詳細な説明を示すフローチャートである。
【図２０】図１６で示した構築処理（ステップＳ１６０５）の詳細な説明を示すフローチャートである。
【図２１】実施の形態３にかかる検証支援装置の機能的構成を示すブロック図である。
【図２２】本発明の一実施例を示す説明図（その２）である。
【図２３】本発明の一実施例を示す説明図（その３）である。
【図２４】実施の形態３にかかる検証支援装置２１００による検証支援処理手順の一例を示すフローチャートである。
【図２５】通常のＦＦモデルによる論理検証の一例を示す説明図である。
【図２６】ＣＤＣモデルによる論理検証の一例を示す説明図である。
【発明を実施するための形態】
【００２１】
以下に添付図面を参照して、本発明にかかる検証支援プログラム、検証支援方法、および検証支援装置の好適な実施の形態を詳細に説明する。
【００２２】
図１は、本発明の一実施例を示す説明図（その１）である。テストベンチ１００は、シミュレーションモデルである。テストベンチ１００では、回路モデル１と、回路モデル２と、回路内の状態を表す変数（以下、「状態変数」と称する。）ごとに比較器と、入力パターンと、出力チェックとを備えている。出力チェックとは、出力端子や機能検証にて注目すべき変数などのシミュレーション結果が出力されていることを示している。また、入力パターンは、機能検証で用いた入力パターンと同一の入力パターンである。
【００２３】
各比較器は、第１の検出器と、第１のＦＩＦＯ（Ｆｉｒｓｔ  Ｉｎ  Ｆｉｒｓｔ  Ｏｕｔ）バッファと、第２の検出器と、第２のＦＩＦＯバッファと、判断器と、出力器を備えている。ここでは、回路モデル１内の受信クロックドメインと回路モデル２内の受信クロックドメインとからｒｓｔａｔｅが引き出され、１つ目の比較器に入力されている。
【００２４】
回路モデル１では、受信クロックドメイン内の受信ＦＦが通常のＦＦモデルであり、回路モデル２では、受信クロックドメイン内の受信ＦＦがＣＤＣモデルである。
【００２５】
テストベンチ１００では、回路モデル１および回路モデル２に同一の入力パターンを与えている。テストベンチ１００を用いてシミュレーションを実行することで比較器では、第１の検出器が回路モデル１内の状態変数の変化を検出し、第２の検出器が回路モデル２内の状態変数の変化を検出する。
【００２６】
そして、第１の検出器により状態変数の変化が検出された時の状態を第１のＦＩＦＯバッファで保持し、第２の検出器により状態変数の変化が検出された時の状態を第２のＦＩＦＯバッファで保持する。第１のＦＩＦＯバッファおよび第２のＦＩＦＯバッファでは、順に状態が保持されている。
【００２７】
ここで、状態変化の系列（以下、「状態遷移系列」と称する。）とは、たとえば、第１のＦＩＦＯバッファが保持している一連の状態と、第２のＦＩＦＯバッファが保持している一連の状態である。
【００２８】
そして、判断器が、第１のＦＩＦＯバッファにより保持されている状態と第２のＦＩＦＯバッファにより保持されている状態とに違いがあるか否かを判断する。
【００２９】
ｃｌｋ２の立ち上がりごとの状態変数の一例を下記に示す。
・回路モデル１内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・回路モデル２内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【００３０】
上記の場合における第１のＦＩＦＯバッファと第２のＦＩＦＯバッファが保持している状態を下記に示す。
・第１のＦＩＦＯバッファ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・第２のＦＩＦＯバッファ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【００３１】
よって、上記例の場合、いずれも同一の状態が第１および第２のＦＩＦＯバッファに保持されているため判断器により違いがないと判断される。
【００３２】
ｃｌｋ２の立ち上がりごとの状態変数の一例を下記に示す。
・回路モデル１内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・回路モデル２内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ０→Ｓｔａｔｅ２→Ｓｔａｔｅ２
【００３３】
上記の場合における第１のＦＩＦＯバッファと第２のＦＩＦＯバッファが保持している状態を下記に示す。
・第１のＦＩＦＯバッファ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・第２のＦＩＦＯバッファ：Ｓｔａｔｅ０→Ｓｔａｔｅ２
【００３４】
よって、上記例の場合、第１のＦＩＦＯバッファと第２のＦＩＦＯバッファに保持されている状態が異なるため判断器により違いがあると判断され、出力器が不一致情報を出力する。
【００３５】
これにより、ＣＤＣに起因する障害により誤った内部状態に遷移しても、誤動作を正確に検出できる。
【００３６】
つぎに、本実施の形態の詳細な説明については、実施の形態１〜３を用いて説明する。まず、実施の形態１〜２を用いてシミュレーションモデル（ここでは、「テストベンチ」と称する。）を生成する例を示す。つぎに、実施の形態３を用いて実施の形態１または２で生成したシミュレーションモデルを用いてシミュレーションを行う例を示す。
【００３７】
（実施の形態１）
まず、実施の形態１では、検証対象回路内から状態変数を検出し、比較器のテンプレートを用いて状態変数ごとに比較器を生成して、テストベンチを構築する例を示す。
【００３８】
（検証対象回路のＲＴＬ記述情報）
図２は、検証対象回路のＲＴＬ記述の一例を示す説明図である。回路情報２００は、検証対象回路である回路モデル１のＲＴＬ記述情報のうち受信クロックドメインのＲＴＬ記述情報である。回路情報２００では、クロック信号としてｃｌｋ２が用いられている。また、他のクロックドメインまたはグローバル信号として、ｒｅｓｅｔと、ｒｅｑと、ａｄｄｒとが、入力されている。なお、回路情報２００は、コンピュータがアクセス可能な記憶装置に記憶されていることとする。また、回路モデル１および回路モデル２もコンピュータがアクセス可能な記憶装置に記憶されていることとする。
【００３９】
（比較器のテンプレート）
図３は、比較器のテンプレートの一例を示す説明図である。テンプレート３００は、比較器のテンプレートであって、第１の検出器３０１と、第１のＦＩＦＯバッファ３０３と、第２の検出器３０２と、第２のＦＩＦＯバッファ３０４と、判断器３０５と、出力器３０６と、を備えている。テンプレート３００は、具体的には、たとえば、図２のようにハードウェア記述言語などで記述された情報であり、シミュレーションのみで用いられるモデルである。
【００４０】
第１の検出器３０１は、第１の状態変数が入力され、第１の状態変数の変化が検出される。第１のＦＩＦＯバッファ３０３は、第１の検出器３０１により検出された状態変化時の状態を保持する。第２の検出器３０２は、第２の状態変数が入力され、第２の状態変数の変化が検出される。第１のＦＩＦＯバッファ３０４は、第２の検出器３０２により検出された状態変化時の状態を保持する。そして、判断器３０５は、第１のＦＩＦＯバッファ３０３と第２のＦＩＦＯバッファ３０４に記憶されている状態の系列を比較する。そして、出力器３０６は、判断器３０５により判断された判断結果を出力する。なお、テンプレート３００は、コンピュータがアクセス可能な記憶装置に記憶されていることとする。
【００４１】
（検証支援装置のハードウェア構成）
図４は、検証支援装置のハードウェア構成を示すブロック図である。図４において、検証支援装置は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）４０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）４０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）４０３と、磁気ディスクドライブ４０４と、磁気ディスク４０５と、光ディスクドライブ４０６と、光ディスク４０７と、ディスプレイ４０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）４０９と、キーボード４１０と、マウス４１１と、スキャナ４１２と、プリンタ４１３と、を備えている。また、各構成部はバス４００によってそれぞれ接続されている。
【００４２】
ここで、ＣＰＵ４０１は、検証支援装置の全体の制御を司る。ＲＯＭ４０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ４０３は、ＣＰＵ４０１のワークエリアとして使用される。磁気ディスクドライブ４０４は、ＣＰＵ４０１の制御にしたがって磁気ディスク４０５に対するデータのリード／ライトを制御する。磁気ディスク４０５は、磁気ディスクドライブ４０４の制御で書き込まれたデータを記憶する。
【００４３】
光ディスクドライブ４０６は、ＣＰＵ４０１の制御にしたがって光ディスク４０７に対するデータのリード／ライトを制御する。光ディスク４０７は、光ディスクドライブ４０６の制御で書き込まれたデータを記憶したり、光ディスク４０７に記憶されたデータをコンピュータに読み取らせたりする。
【００４４】
ディスプレイ４０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ４０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００４５】
インターフェース（以下、「Ｉ／Ｆ」と略する。）４０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク４１４に接続され、このネットワーク４１４を介して他の装置に接続される。そして、Ｉ／Ｆ４０９は、ネットワーク４１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ４０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００４６】
キーボード４１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス４１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４７】
スキャナ４１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ４１２は、ＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ４１３は、画像データや文書データを印刷する。プリンタ４１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００４８】
（実施の形態１にかかる検証支援装置の機能的構成）
図５は、実施の形態１にかかる検証支援装置の機能的構成を示すブロック図である。検証支援装置５００は、検出部５０１と、ノード生成部５０２と、第１のエッジ生成部５０３と、第２のエッジ生成部５０４と、探索部５０５と、設定部５０６と、構築部５０７と、出力部５０８と、を含む構成である。各機能（検出部５０１〜出力部５０８）は、具体的には、たとえば、図４に示したＲＯＭ４０２、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶装置に記憶されたプログラムをＣＰＵ４０１に実行させることにより、または、Ｉ／Ｆ４０９により、各機能を実現する。
【００４９】
なお、ノード生成部５０２と、第１のエッジ生成部５０３と、第２のエッジ生成部５０４と、探索部５０５の詳細な処理については、実施の形態２で説明する。
【００５０】
まず、検出部５０１は、対象回路の第１の記述情報から対象回路の状態を表す状態変数を検出する。ここで、第１の記述情報が、回路モデル１である。具体的には、たとえば、ＣＰＵ４０１が、回路情報２００からクロック同期代入文を検出し、当該代入文の左辺に表れる変数を候補変数として検出する。
【００５１】
クロック同期とは、回路情報２００では「ｐｏｓｅｄｇｅ  ｃｌｋ２」であり、クロック同期代入文とは、クロック同期文の中に含まれている代入文である。たとえば、「ｒｅｑ１＜＝ｒｅｑ；」である。
【００５２】
下記が候補変数として検出される。
・ｒｅｑ１
・ｒｅｑ２
・ａｃｋ
・ａｂｔ
・ｒｓｔａｔｅ
・ｒａｄｄｒ
【００５３】
つぎに、具体的には、たとえば、ＣＰＵ４０１が、候補変数の中からビット幅が２以上である候補変数を検出する。下記が検出される。
・ｒｓｔａｔｅ
・ｒａｄｄｒ
【００５４】
そして、検出された候補変数から状態変数を検出する例を示す。
【００５５】
（例１）
つぎに、具体的には、たとえば、ＣＰＵ４０１が、候補変数の中から、候補変数への代入文の右辺が定数である候補変数を状態変数として検出する。よって、ｒｓｔａｔｅが状態変数として検出される。
【００５６】
（例２）
つぎに、具体的には、たとえば、ＣＰＵ４０１が、候補変数の中から、定数との比較の形で参照されている候補変数を状態変数として検出する。よって、ｒｓｔａｔｅが状態変数として検出される。
【００５７】
（例３）
つぎに、具体的には、たとえば、ＣＰＵ４０１が、候補変数の中から、名称に「ｓｔａｔｅ」が含まれている候補変数を状態変数として検出する。よって、ｒｓｔａｔｅが状態変数として検出される。
【００５８】
図６は、状態変数として検出された検出結果の一例を示す説明図である。状態変数リストは、検出部５０１により検出された検出結果を示している。回路情報２００内には、ｒｓｔａｔｅのみが記述されているが、受信クロックドメイン内には複数の状態変数が存在する。
【００５９】
つぎに、設定部５０６は、比較器に入力される状態変数のビット幅を、検出部５０１により検出された状態変数のビット幅に設定する。具体的には、たとえば、ＣＰＵ４０１が、比較器のテンプレートを読み出し、テンプレートの入力のビット幅をｒｓｔａｔｅのビット幅である２ビットとし、ｒｓｔａｔｅ用の比較器を生成する。
【００６０】
そして、構築部５０７は、第１の記述情報内の状態変数を第１の検出器内の第１の変数とし、第１の記述情報のうち一部の情報が異なる第２の記述情報内で当該状態変数と同一の状態変数を第２の検出器の第２の変数として設定部５０６により設定された設定後の比較器に与えることにより、第１の記述情報と第２の記述情報と比較器モデルとが組み合わさったシミュレーションモデルを構築する。ここで、第２の記述情報は、回路モデル２であり、回路モデル２は、回路モデル１と比較して受信クロックドメイン内の受信ＦＦのモデルが異なる。具体的には、たとえば、ＣＰＵ４０１が、回路モデル１内のｒｓｔａｔｅを比較器の第１の状態変数に接続し、回路モデル２内のｒｓｔａｔｅを比較器の第２の状態変数に接続する。なお、さらに、テストベンチ１００とのように入力パターンとを組み合わせシミュレーションモデルであってもよい。
【００６１】
出力部５０８は、構築部５０７により構築された構築結果を出力する機能を有する。具体的には、たとえば、図１で示したテストベンチ１００が出力される。出力形式としては、たとえば、ディスプレイ４０８への表示、プリンタ４１３への印刷出力、Ｉ／Ｆ４０９による外部装置への送信がある。また、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶装置に記憶することとしてもよい。
【００６２】
従来では、検証者がＣＤＣ検証用に入力パターンをあらたに作成することもできるが、膨大な時間と手間がかかり、コストがかかるという問題点があった。実施の形態１では、機能検証用の入力パターンを流用し、さらに、自動でシミュレーションモデルを生成しているため、検証期間の短縮化および検証者の手間を省くことができる。
【００６３】
図７は、実施の形態１にかかる検証支援装置５００による検証支援処理手順の一例を示すフローチャートである。まず、検証支援装置５００が、回路情報を取得し（ステップＳ７０１）、検出処理を実施し（ステップＳ７０２（Ｓ７０３、またはＳ７０４））、構築処理を実施し（ステップＳ７０５）、一連の処理を終了する。検出処理については、ステップＳ７０２、ステップＳ７０３、またはステップＳ７０４のいずれかが実施される。
【００６４】
図８は、図７で示した検出処理（ステップＳ７０２）の詳細な説明を示すフローチャートである。まず、検証支援装置５００が、検出部５０１によりクロック同期代入文の左辺に表れる変数を候補変数として検出し（ステップＳ８０１）、未選択の候補変数があるか否かを判断する（ステップＳ８０２）。
【００６５】
そして、未選択の候補変数があると判断した場合（ステップＳ８０２：Ｙｅｓ）、検証支援装置５００が、未選択の候補変数から任意の候補変数を選択し（ステップＳ８０３）、候補変数のビット幅が２以上か否かを判断する（ステップＳ８０４）。
【００６６】
そして、候補変数のビット幅が２以上であると判断された場合（ステップＳ８０４：Ｙｅｓ）、検証支援装置５００が、候補変数への代入文の右辺が定数であるか否かを判断する（ステップＳ８０５）。そして、変数であると判断された場合（ステップＳ８０５：Ｙｅｓ）、候補変数を状態変数に設定し（ステップＳ８０６）、ステップＳ８０２へ戻る。
【００６７】
一方、検証支援装置５００が、候補変数のビット幅が２以上でないと判断した場合（ステップＳ８０４：Ｎｏ）、または右辺が定数でないと判断した場合（ステップＳ８０５：Ｎｏ）、ステップＳ８０２へ戻る。
【００６８】
一方、検証支援装置５００が、未選択の候補変数がないと判断した場合（ステップＳ８０２：Ｎｏ）、ステップＳ７０５へ移行する。
【００６９】
図９は、図７で示した検出処理（ステップＳ７０３）の詳細な説明を示すフローチャートである。図９のステップＳ９０１〜９０４は、図８のステップＳ８０１〜８０４とそれぞれ同一の処理であり、図９のステップＳ９０６と図８のステップＳ８０６とは、同一の処理であるため、詳細な説明を省略する。ここでは、ステップＳ９０５についてのみ説明する。
【００７０】
ステップＳ９０４のつぎに、検証支援装置５００が、候補変数が定数との比較の形で参照されているか否かを判断する（ステップＳ９０５）。検証支援装置５００が、候補変数が定数との比較の形で参照されていると判断した場合（ステップＳ９０５：Ｙｅｓ）、ステップＳ９０６へ移行する。一方、検証支援装置５００が、候補変数が定数との比較の形で参照されていないと判断した場合（ステップＳ９０５：Ｎｏ）、ステップＳ９０２へ戻る。
【００７１】
図１０は、図７で示した検出処理（ステップＳ７０４）の詳細な説明を示すフローチャートである。図１０のステップＳ１００１〜１００４は、図８のステップＳ８０１〜８０４とそれぞれ同一の処理であり、さらに、図１０のステップＳ１００６と図８のステップＳ８０６とは、同一の処理であるため、詳細な説明を省略する。ここでは、ステップＳ１００５についてのみ説明する。
【００７２】
ステップＳ１００４のつぎに、検証支援装置５００が、候補変数の変数名に“ｓｔａｔｅ”を含むか否かを判断する（ステップＳ１００５）。検証支援装置５００が、候補変数の変数名に“ｓｔａｔｅ”を含むと判断した場合（ステップＳ１００５：Ｙｅｓ）、ステップＳ１００６へ移行する。一方、検証支援装置５００が、候補変数の変数名に“ｓｔａｔｅ”を含まないと判断した場合（ステップＳ１００５：Ｎｏ）、ステップＳ１００２へ戻る。
【００７３】
図１１は、図７で示した構築処理（ステップＳ７０５）の詳細な説明を示すフローチャートである。まず、検証支援装置５００が、未選択の状態変数があるか否かを判断し（ステップＳ１１０１）、あると判断した場合（ステップＳ１１０１：Ｙｅｓ）、比較器のテンプレートを読み出す（ステップＳ１１０２）。
【００７４】
そして、検証支援装置５００が、テンプレートを用いて当該状態変数のビット幅に基づく比較器を生成し（ステップＳ１１０３）、回路モデル１および回路モデル２内の各状態変数を生成した比較器に与える（ステップＳ１１０４）。そして、検証支援装置５００が、出力処理を実施し（ステップＳ１１０５）、ステップＳ１１０１へ戻る。
【００７５】
一方、ステップＳ１１０１において、検証支援装置５００が、未選択の状態変数がないと判断した場合（ステップＳ１１０１：Ｎｏ）、一連の処理を終了する。
【００７６】
（実施の形態２）
つぎに、実施の形態２では、受信クロックドメイン内の受信ＦＦに近い状態変数を検出する例を示す。また、実施の形態２では、実施の形態１で示した構成と同一構成には、同一の符号を付し、同一符号が付された構成の説明は省略する。
【００７７】
（受信ＦＦリスト）
図１２は、受信ＦＦリストの一例を示す説明図である。受信ＦＦリスト１２００は、回路情報２００内に記述されているＦＦの中で、どのＦＦが受信ＦＦであるかを示す情報である。ここでは、ｒｅｑ１とｒａｄｄｒとが受信ＦＦである。なお、受信ＦＦリストは、ＣＰＵ４０１がアクセス可能な記憶装置に記憶されている。
【００７８】
まず、実施の形態１で示した検出部５０１の処理のつぎに、ノード生成部５０２は、検証対象回路内の各変数に対応するノードを生成する。具体的には、たとえば、ＣＰＵ４０１が、回路情報２００内に記載されている変数をすべて検出し、それぞれに対応するノードを生成する。なお、クロックに関する変数に対応するノードは、不要である。
【００７９】
図１３は、ノード生成結果の一例を示す説明図である。回路情報２００内の変数は、ｒｅｑと，ｒｅｑ１と、ｒｅｑ２と、ａｄｄｒと、ａｃｋと、ａｂｔと、ｄａｔａと、ｄａｔａｒｅａｄｙと、ｔｉｍｅｏｕｔと、ｒｓｔａｔｅと、ｒａｄｄｒと、ｒｄａｔａと、ｒｅｓｅｔである。○がノードを示し、グラフ１３００には、各変数に対応するノードが配置されている。
【００８０】
つぎに、第１のエッジ生成部５０３は、ノード生成部５０２により生成されたノードのうち、対象回路内の代入文における右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成する。具体的には、たとえば、ＣＰＵ４０１が、回路情報２００内の代入文を検出する。
【００８１】
検出結果は、下記である。
・ｒｅｑ１＜＝ｒｅｑ；
・ｒｅｑ２＜＝ｒｅｑ１；
・ｒａｄｄｒ＜＝ａｄｄｒ；
・ｄａｔａ＜＝ｒｄａｔａ；
【００８２】
つぎに、具体的には、たとえば、ＣＰＵ４０１が、検出された代入文における右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成する。
【００８３】
図１４は、第１のエッジ生成部５０３による有向エッジ生成結果の一例を示す説明図である。「ｒｅｑ１＜＝ｒｅｑ」を例に挙げて説明すると、グラフ１４００内のｒｅｑに対応するノードからｒｅｑ１に対応するノードへ有向エッジ（→）が記述されている。
【００８４】
グラフ１４００には、同様にｒｅｑ１に対応するノードからｒｅｑ２に対応するノードへの有向エッジと、ａｄｄｒに対応するノードからｒａｄｄｒに対応するノードへの有向エッジが記述されている。さらに、グラフ１４００には、ｒｄａｔａに対応するノードからｄａｔａに対応するノードへの有向エッジが記述されている。
【００８５】
つぎに、第２のエッジ生成部５０４は、ノード生成部５０２により生成されたノードのうち、対象回路内の条件文に含まれる変数に対応するノードから条件文により実行される代入文の左辺の変数に対応するノードへの有向エッジを生成する。
【００８６】
ここで、回路情報２００内の以下の条件付き実行文を例に挙げて説明する。
「ｉｆ（ｒｅｓｅｔ）ｂｅｇｉｎ
ａｃｋ  ＜＝  １‘ｂ０；
ａｂｔ  ＜＝  １‘ｂ０；
ｒｓｔａｔｅ  ＜＝  ２‘ｂ００；
ｅｎｄ」
【００８７】
「ｉｆ（ｒｅｓｅｔ）」が、実行条件であり、実行条件に含まれる変数とは、ｒｅｓｅｔである。そして、実行される代入文の左辺変数が、ａｃｋと、ａｂｔと、ｒｓｔａｔｅである。よって、たとえば、第２のエッジ生成部５０４が、ｒｅｓｅｔに対応するノードからａｃｋに対応するノードへの有向エッジと、ｒｅｓｅｔに対応するノードからａｂｔに対応するノードへの有向エッジと、ｒｅｓｅｔに対応するノードからｒｓｔａｔｅに対応するノードへの有向エッジとを生成する。
【００８８】
また、下記の記述は、「ｉｆ（！ｒｅｓｅｔ）」と同等の意味であるため、実行条件に含まれる変数とは、ｒｅｓｅｔである。
「ｉｆ（ｒｅｓｅｔ）ｂｅｇｉｎ
・・・・
ｅｌｓｅ  ｂｅｇｉｎ」
【００８９】
図１５は、第２のエッジ生成部５０４による有向エッジ生成結果の一例を示す説明図である。グラフ１５００では、第２のエッジ生成部５０４による有向エッジ生成結果を示している。ｄａｔａｒｅａｄｙと、ｔｉｍｅｏｕｔと、ｒｄａｔａについては、回路情報２００には記載されていないが、何らかのデータを受けているため、それぞれに対応するノードに対して有向エッジが記載されている。
【００９０】
つぎに、探索部５０５は、第１のエッジ生成部５０３および第２のエッジ生成部５０４により有向エッジが生成されたグラフ内の指定変数に対応するノードから有向エッジを辿って検出部５０１により検出された変数に対応するノードを指定回数以内で探索する。
【００９１】
また、指定ノードから１回有向エッジを辿って到達可能なノードのことを指定ノードから距離１のノードとし、指定ノードからｎ回有向エッジを辿って到達可能なノードのことを指定ノードから距離ｎのノードとする。よって、具体的には、たとえば、探索部５０５は、指定ノードから距離ｎ以内のノードをすべて探索し、探索されたノードの中で検出部５０１により検出された変数に対応するノードを状態変数とする。ここでは、距離ｎを、２とし、実際には、検証者が距離ｎを設定する。実施の形態２では、指定ノードとは、受信ＦＦに対応するノードである。
【００９２】
具体的には、たとえば、ＣＰＵ４０１が、集合Ｓに空集合をいれる。
・Ｓ＝｛φ｝
【００９３】
つぎに、具体的には、たとえば、ＣＰＵ４０１が、受信ＦＦリスト１２００内の受信ＦＦを選択し、集合Ｓに選択された受信ＦＦ名をいれる。ここでは、たとえば、ｒｅｑ１が選択される。集合Ｓは、下記のようになる。
・Ｓ＝｛ｒｅｑ１｝
【００９４】
つぎに、具体的には、たとえば、ＣＰＵ４０１が、ｒｅｑ１に対応するノードから有向エッジｅ１を辿ってｒｅｑ２に対応するノードに到達する。ｒｅｑ２に対応するノードは、ｒｅｑ１に対応するノードからの距離が１である。そして、集合Ｓには、ｒｅｑ２が含まれていないため、探索部５０５は、集合Ｓにｒｅｑ２を入れる。
・Ｓ＝｛ｒｅｑ１，ｒｅｑ２｝
【００９５】
つぎに、具体的には、たとえば、ＣＰＵ４０１が、ｒｅｑ２に対応するノードから有向エッジｅ２を辿ってｒａｄｄｒに対応するノードに到達する。そして、集合Ｓには、ｒａｄｄｒが含まれていないため、探索部５０５は、集合Ｓにｒａｄｄｒを入れる。
・Ｓ＝｛ｒｅｑ１，ｒｅｑ２，ｒａｄｄｒ｝
【００９６】
ｒａｄｄｒに対応するノードは、ｒｅｑ１に対応するノードからの距離が２であるため、たとえば、ＣＰＵ４０１が、ｒａｄｄｒに対応するノードからｒｅｑ２に対応するノードへ戻る。そして、具体的には、たとえば、ＣＰＵ４０１が、ｒｅｑ２に対応するノードから有向エッジｅ３を辿ってｒｓｔａｔｅに対応するノードに到達する。そして、集合Ｓには、ｒｓｔａｔｅが含まれていないため、探索部５０５は、集合Ｓにｒｓｔａｔｅを入れる。
・Ｓ＝｛ｒｅｑ１，ｒｅｑ２，ｒａｄｄｒ，ｒｓｔａｔｅ｝
【００９７】
ｒｓｔａｔｅに対応するノードは、ｒｅｑ１に対応するノードからの距離が２であるため、たとえば、ＣＰＵ４０１が、ｒｓｔａｔｅに対応するノードからｒｅｑ２に対応するノードへ戻る。有向エッジｅ３と同様に有向エッジｅ４，ｅ５を辿って、集合Ｓに含まれていない変数であれば、探索部５０５は、集合Ｓに当該変数を入れる。
・Ｓ＝｛ｒｅｑ１，ｒｅｑ２，ｒａｄｄｒ，ｒｓｔａｔｅ，ａｂｔ，ａｃｋ｝
【００９８】
そして、ｒｅｑ２に対応するノードからの有向エッジはすべて探索済であるため、ここで、探索が終了される。つぎに、たとえば、ＣＰＵ４０１が、集合Ｓの中から検出部５０１により検出された状態変数を探索する。ここでは、ｒｓｔａｔｅが集合Ｓの中から探索される。
【００９９】
つぎに、設定部５０６は、比較器のテンプレート内の第１および第２の変数のビット幅を探索部５０５により探索された状態変数のビット幅に設定する。設定部５０６の具体的な処理については、実施の形態１で示した処理と同一であるため説明を省略する。
【０１００】
そして、構築部５０７および出力部５０８の処理に関しても実施の形態１で示した処理と同一であるため説明を省略する。
【０１０１】
図１６は、実施の形態２にかかる検証支援装置５００による検証支援処理手順の一例を示すフローチャートである。まず、検証支援装置５００が、回路情報を取得し（ステップＳ１６０１）、検出処理を実行し（ステップＳ１６０２）、グラフ生成処理を実行する（ステップＳ１６０３）。つぎに、検証支援装置５００が、決定処理を実行し（ステップＳ１６０４）、構築処理を実行し（ステップＳ１６０５）、一連の処理を終了する。
【０１０２】
ステップＳ１６０２については、図７に示したステップＳ７０２（Ｓ７０３、Ｓ７０４）と同一の処理であるため説明を省略する。
【０１０３】
図１７は、図１６で示したグラフ生成処理（ステップＳ１６０３）の詳細な説明を示すフローチャートである。まず、検証支援装置５００が、回路情報内の各変数に対応するノードを生成し（ステップＳ１７０１）、右辺が変数で左辺が変数の代入文を検出する（ステップＳ１７０２）。
【０１０４】
つぎに、検証支援装置５００が、検出した代入文の中で未選択の代入文があるか否かを判断し（ステップＳ１７０３）、あると判断された場合（ステップＳ１７０３：Ｙｅｓ）、未選択の代入文から１つの代入文を選択する（ステップＳ１７０４）。
【０１０５】
そして、検証支援装置５００が、右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成し（ステップＳ１７０５）、ステップＳ１７０３へ戻る。
【０１０６】
一方、ステップＳ１７０３において、検証支援装置５００が、未選択の代入文がないと判断した場合（ステップＳ１７０３：Ｎｏ）、条件付き実行文を検出する（ステップＳ１７０６）。そして、検証支援装置５００が、検出した実行文の中で未選択の実行文があるか否かを判断し（ステップＳ１７０７）、あると判断した場合（ステップＳ１７０７：Ｙｅｓ）、未選択の実行文から１つの実行文を選択する（ステップＳ１７０８）。
【０１０７】
つぎに、検証支援装置５００が、実行文において実行条件内の変数に対応するノードから実行される代入文の左辺変数に対応するノードへの有向エッジを生成し（ステップＳ１７０９）、ステップＳ１７０７へ戻る。
【０１０８】
一方、ステップＳ１７０７において、検証支援装置５００が、検出した実行文の中で未選択の実行文がないと判断した場合（ステップＳ１７０７：Ｎｏ）、ステップＳ１６０４へ移行する。
【０１０９】
図１８は、図１６で示した決定処理（ステップＳ１６０４）の詳細な説明を示すフローチャートである。まず、検証支援装置５００が、受信ＦＦリストを取得し（ステップＳ１８０１）、ＳＳ←φとする（ステップＳ１８０２）。
【０１１０】
つぎに、検証支援装置５００が、受信ＦＦリストから未選択の受信ＦＦがあるか否かを判断し（ステップＳ１８０３）、あると判断した場合（ステップＳ１８０３：Ｙｅｓ）、未選択の受信ＦＦから１つの受信ＦＦを変数ｖとして選択する（ステップＳ１８０４）。
【０１１１】
そして、検証支援装置５００が、変数ｖから距離ｎ以内にある変数の集合Ｓ←φとし（ステップＳ１８０５）、探索処理（ｖ，ｎ，ｓ）を実施し（ステップＳ１８０６）、ＳＳ←ＳＳ∪Ｓとし（ステップＳ１８０７）、ステップＳ１８０３へ戻る。
【０１１２】
ここでの距離ｎとは、グラフ上での距離であって、変数ｖから距離１以内にある変数とは、変数ｖに対応するノードから有向エッジを１つ辿って到達可能なノードの変数である。ステップＳ１８０６については、検証支援装置５００が、（ｖ，ｎ，ｓ）を引数として探索処理を実施する。
【０１１３】
一方、ステップ１８０３において、検証支援装置５００が、未選択の受信ＦＦがないと判断した場合（ステップＳ１８０３：Ｎｏ）、ステップＳ１６０５へ移行する。
【０１１４】
図１９は、図１８で示した探索処理（ステップＳ１８０６）の詳細な説明を示すフローチャートである。探索処理（ステップＳ１８０６）については、（ｖ，ｎ，Ｓ）が引数として与えられている。まず、検証支援装置５００が、Ｓ←Ｓ∪｛ｖ｝とし（ステップＳ１９０１）、ｎ≧１であるか否かを判断する（ステップＳ１９０２）。そして、検証支援装置５００が、ｎ≧１であると判断した場合（ステップＳ１９０２：Ｙｅｓ）、ｖを始点とする有向エッジの中で未処理のエッジがあるか否かを判断する（ステップＳ１９０３）。
【０１１５】
そして、検証支援装置５００が、未処理のエッジがあると判断した場合（ステップＳ１９０３：Ｙｅｓ）、未選択のエッジから任意のエッジを選択し（ステップＳ１９０４）、エッジの終点ｗ∈Ｓであるか否かを判断する（ステップＳ１９０５）。
【０１１６】
検証支援装置５００が、ｗ∈Ｓでないと判断した場合（ステップＳ１９０５：Ｎｏ）、探索処理（ｗ，ｎ−１，Ｓ）を実行し（ステップＳ１９０６）、ステップＳ１９０３へ戻る。探索処理については、再帰関数となっており、ステップＳ１９０６については、（ｗ，ｎ−１，Ｓ）を引数としてステップＳ１８０６が実行される。
【０１１７】
一方、ステップＳ１９０５において、検証支援装置５００が、エッジの終点ｗ∈Ｓであると判断した場合（ステップＳ１９０５：Ｙｅｓ）、ステップＳ１９０３へ戻る。
【０１１８】
一方、ステップＳ１９０２において、検証支援装置５００が、ｎ≧１でないと判断した場合（ステップＳ１９０２：Ｎｏ）、または未処理のエッジがないと判断した場合（ステップＳ１９０３：Ｎｏ）、元に戻る。
【０１１９】
たとえば、ｎが１の場合、ステップＳ１９０６において、ｎ−１をｎとして再度ステップＳ１８０６が実行される。ｎ−１は、０であるため、ステップＳ１９０２によってｎ≧１でないと判断され、ＲＥＴＵＲＮとなり、ｎが１の場合におけるステップＳ１９０３へ移行する。なお、再帰関数については、公知であるため詳細な説明は省略する。
【０１２０】
つぎに、図２０は、図１６で示した構築処理（ステップＳ１６０５）の詳細な説明を示すフローチャートである。まず、検証支援装置５００が、未選択の状態変数があるか否かを判断し（ステップＳ２００１）、未選択の状態があると判断した場合（ステップＳ２００１：Ｙｅｓ）、未選択の状態変数から任意の状態変数を選択する（ステップＳ２００２）。
【０１２１】
そして、検証支援装置５００が、状態変数∈ＳＳであるか否かを判断し（ステップＳ２００３）、状態変数∈ＳＳであると判断した場合（ステップＳ２００３：Ｙｅｓ）、比較器のテンプレートを読み出す（ステップＳ２００４）。つぎに、検証支援装置５００が、テンプレートを用いて状態変数のビット幅に基づく比較器を生成し（ステップＳ２００５）、各状態変数を比較器に与え（ステップＳ２００６）、出力処理を実施し（ステップＳ２００７）、ステップＳ２００１へ戻る。
【０１２２】
また、ステップＳ２００３において、検証支援装置５００が、状態変数∈ＳＳでないと判断した場合（ステップＳ２００３：Ｎｏ）、ステップＳ２００１へ戻る。
【０１２３】
一方、ステップＳ２００１において、検証支援装置５００が、未選択の状態変数がないと判断した場合（ステップＳ２００１：Ｎｏ）、一連の処理を終了する。これにより図１に示すようなテストベンチ１００が生成される。
【０１２４】
（実施の形態３）
最後に、実施の形態３では、実施の形態１または２により生成されたシミュレーションモデルを用いてシミュレーションを行い、状態変化の系列に違いがあるか否かを検出する例を示す。また、実施の形態３では、実施の形態１または２で示した構成と同一構成には、同一の符号を付し、同一符号が付された構成の説明は省略する。
【０１２５】
（実施の形態３にかかる検証支援装置の機能的構成）
図２１は、実施の形態３にかかる検証支援装置の機能的構成を示すブロック図である。検証支援装置２１００は、第１の検出部２１０１と、第２の検出部２１０２と、第１の保持部２１０３と、第２の保持部２１０４と、判断部２１０５と、出力部２１０６と、を含む構成である。各機能（第１の検出部２１０１〜出力部２１０６）は、具体的には、たとえば、図４に示したＲＯＭ４０２、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶装置に記憶されたプログラムをＣＰＵ４０１に実行させることにより、または、Ｉ／Ｆ４０９により、その機能を実現する。
【０１２６】
まず、ここでは、２ビットのｒｓｔａｔｅを状態変数として説明する。
【０１２７】
・Ｓｔａｔｅ０：ｒｓｔａｔｅ＝２’ｂ００
・Ｓｔａｔｅ１：ｒｓｔａｔｅ＝２’ｂ０１
・Ｓｔａｔｅ２：ｒｓｔａｔｅ＝２’ｂ１０
・Ｓｔａｔｅ３：ｒｓｔａｔｅ＝２’ｂ１１
【０１２８】
まず、第１の検出部２１０１は、入力データが対象回路に与えられた場合における当該対象回路の状態変化を検出する。具体的には、たとえば、ＣＰＵ４０１が、回路モデル１内のｒｓｔａｔｅの変化を検出する。
【０１２９】
そして、第２の検出部２１０２は、入力データの一部がＣＤＣモデルによりランダムに変更されて対象回路に与えられた場合における当該対象回路の状態変化を検出する。具体的には、たとえば、ＣＰＵ４０１が、回路モデル２内のｒｓｔａｔｅの変化を検出する。
【０１３０】
第１の保持部２１０３は、第１の検出部２１０１により状態変化が検出される都度、検出時の状態を順に保持する。具体的には、たとえば、ＦＩＦＯバッファであって、ＣＰＵ４０１が、検出時の状態を順にＦＩＦＯバッファに格納する。
【０１３１】
第２の保持部２１０４は、第２の検出部２１０２により状態変化が検出される都度、検出時の状態を順に保持する。具体的には、たとえば、ＦＩＦＯバッファであって、ＣＰＵ４０１が、検出時の状態を順にＦＩＦＯバッファに格納する。
【０１３２】
したがって、第１の保持部２１０３および第２の保持部２１０４により保持されている一連の状態が、状態遷移系列である。
【０１３３】
判断部２１０５は、第１の保持部２１０３により保持された状態と、第２の保持部２１０４により保持された状態とに違いがあるか否かを判断する。具体的には、たとえば、ＣＰＵ４０１が、ＦＩＦＯバッファ内に保持されている順に値を比較して違いがあるか否かを判断する。
【０１３４】
つぎに、出力部２１０６は、判断結果を出力する機能を有する。具体的には、たとえば、ＣＰＵ４０１が、違うと判断された場合に不一致情報を出力する。出力形式としては、たとえば、ディスプレイ４０８への表示、プリンタ４１３への印刷出力、Ｉ／Ｆ４０９による外部装置への送信がある。また、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶することとしてもよい。
【０１３５】
ここで、ｒｓｔａｔｅの変化について例１および例２を用いて説明する。
【０１３６】
（例１）
ｃｌｋ２の立ち上がりごとのｒｓｔａｔｅの例を示す。
・ｃｌｋ２の立ち上がりごとの回路モデル１内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・ｃｌｋ２の立ち上がりごとの回路モデル２内のｒｓｔａｔｅ：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【０１３７】
よって、第１の検出部２１０１により検出された検出結果は、下記である。
・回路モデル１内の状態変数の状態遷移：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【０１３８】
そして、第２の検出部２１０２により検出された検出結果は、下記である。
・回路モデル２内の状態変数の状態遷移：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【０１３９】
なお、第１の検出部２１０１および第２の検出部２１０２では、状態変化のみを検出しているため、どの状態であるかについては検出してない。よって、Ｓｔａｔｅ０が続いていても、状態は変化していないため第１の検出部２１０１および第２の検出部２１０２は、何も検出しない。
【０１４０】
そして、第１の保持部２１０３は、まず、Ｓｔａｔｅ０を保持し、つぎに、Ｓｔａｔｅ１を保持し、最後にＳｔａｔｅ２を保持する。
【０１４１】
そして、第２の保持部２１０４は、まず、Ｓｔａｔｅ０を保持し、つぎに、Ｓｔａｔｅ１を保持し、最後にＳｔａｔｅ２を保持する。
【０１４２】
つぎに、判断部２１０５は、第１の保持部２１０３および第２の保持部２１０４に保持されている順に違いがあるかを判断する。まず、第１の保持部２１０３および第２の保持部２１０４はＳｔａｔｅ０を保持しているため判断部２１０５は、同一であると判断する。つぎに、第１の保持部２１０３および第２の保持部２１０４はＳｔａｔｅ１を保持しているため判断部２１０５は、同一であると判断する。最後に、第１の保持部２１０３および第２の保持部２１０４はＳｔａｔｅ２を保持しているため判断部２１０５は、同一であると判断する。よって、判断部２１０５は、違いがないと判断する。
【０１４３】
（例２）
ｃｌｋ２の立ち上がりごとのｒｓｔａｔｅの例を示す。
・ｃｌｋ２の立ち上がりごとの回路モデル１内の状態変数：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ２
・ｃｌｋ２の立ち上がりごとの回路モデル２内の状態変数：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ１→Ｓｔａｔｅ３
【０１４４】
よって、第１の検出部２１０１により検出された一連の検出結果は、下記である。
・回路モデル１内の状態変数の状態遷移：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ２
【０１４５】
そして、第２の検出部２１０２により検出された一連の検出結果は、下記である。
・回路モデル２内の状態変数の状態遷移：Ｓｔａｔｅ０→Ｓｔａｔｅ１→Ｓｔａｔｅ３
【０１４６】
第１の保持部２１０３は、まず、Ｓｔａｔｅ０を保持し、つぎに、Ｓｔａｔｅ１を保持し、最後にＳｔａｔｅ２を保持する。
【０１４７】
そして、第２の保持部２１０４は、まず、Ｓｔａｔｅ０を保持し、つぎに、Ｓｔａｔｅ１を保持し、最後にＳｔａｔｅ３を保持する。
【０１４８】
つぎに、判断部２１０５は、第１の保持部２１０３および第２の保持部２１０４に保持されている順に違いがあるかを判断する。まず、第１の保持部２１０３および第２の保持部２１０４はＳｔａｔｅ０を保持しているため判断部２１０５は、同一であると判断する。つぎに、第１の保持部２１０３および第２の保持部２１０４はＳｔａｔｅ１を保持しているため判断部２１０５は、同一であると判断する。最後に、第１の保持部２１０３はＳｔａｔｅ２を保持し、第２の保持部２１０４は、Ｓｔａｔｅ３を保持しているため判断部２１０５では、違いがあると判断する。よって、判断部２１０５は、違いがあると判断する。
【０１４９】
つぎに、出力部２１０６は、判断結果を出力する機能を有する。具体的には、たとえば、ＣＰＵ４０１が、違うと判断された場合に不一致情報を出力する。出力形式としては、たとえば、ディスプレイ４０８への表示、プリンタ４１３への印刷出力、Ｉ／Ｆ４０９による外部装置への送信がある。また、ＲＡＭ４０３、磁気ディスク４０５、光ディスク４０７などの記憶領域に記憶することとしてもよい。
【０１５０】
ＣＤＣの影響は、正しく設計された論理回路でも信号変化タイミング（サイクル単位）のずれとして現れる。したがって、通常の機能検証との結果とＣＤＣ検証との結果を単純にサイクルごとに比較すると、数多くの不一致（誤判定）が検出されてしまう。従来では、通常の機能検証との結果とＣＤＣ検証との結果とを、出力端子で単純に比較していた。
【０１５１】
実施の形態３では、ＣＤＣ検証の結果と機能検証の結果とを単純に同一の状態に何サイクル留まるかではなく、例１および例２で示したように状態変化のみを検出している。これにより、メタステーブル状態によって発生する障害の誤判定を避けることができる。
【０１５２】
さらに、状態変化の検出時刻も同時に比較することで検証精度を向上させることができる。第１の保持部２１０３は、第１の検出部２１０１により状態変化が検出される都度、対象回路内の状態と検出時刻とを順に保持する。
【０１５３】
そして、第２の保持部２１０４は、第２の検出部２１０２により状態変化が検出される都度、対象回路内の状態と検出時刻とを順に保持する。
【０１５４】
判断部２１０５は、第１の保持部２１０３により保持された検出結果と、第２の保持部２１０４により保持された検出結果とに違いがあるか否かを判断する。具体的には、たとえば、ＣＰＵ４０１が、ＦＩＦＯバッファ内に保持されている順に値を比較して違いがあるか否かを判断する。
【０１５５】
さらに、判断部２１０５は、第１の保持部２１０３により保持された検出時刻から第２の保持部２１０４により保持された検出時刻までの時間が指定時間以内であるか否かを判断する。
【０１５６】
出力部２１０６は、判断部２１０５により指定時間以内でないと判断された場合、不一致情報を出力する。
【０１５７】
これにより、状態遷移系列が同じであっても、変化時刻が離れすぎていれば、誤動作として検出される。
【０１５８】
また、判断部２１０５は、第１の保持部２１０３により保持されたデータ量と、第２の保持部２１０４により保持されたデータ量とに指定数以上の差があれば、状態変化の系列に違いがあると判断する。データ量に大きな差があれば、状態ごとに比較しなくとも、違いがあると判断できる。よって、検証を容易化することができ、検証時間を短縮することができる。
【０１５９】
上述では、状態変数の系列は一連の状態であると説明したが、一連の状態に限らず、状態変数に関連している変数の一連の値であってもよい。よって、第１の保持部２１０３および第２の保持部２１０４は、状態変化が検出される都度、状態変数に関連する変数を保持してもよい。そして、判断部２１０５は、第１の保持部２１０３に保持されている変数と第２の保持部２１０３に保持されている変数に違いがあるか否かを判断し、メタステーブル状態による誤動作が発生しているか否かを判断してもよい。
【０１６０】
回路情報２００内のｒｓｔａｔｅを例に挙げると、状態変数に関連している変数とは、ｒｓｔａｔｅに関連しているデータ信号であり、具体的には、クロック同期代入文の中でｒｓｔａｔｅの代入文を除く代入文の左辺の変数である。ここでは、ａｃｋと、ｒａｄｄｒと、ａｂｔと、ａｃｋとが状態変数以外の変数である。
【０１６１】
実施の形態３では、図１を例に挙げて説明したが、機能検証については何度もシミュレーションを実行する必要がないため、図２２に示すような構成にしてもよい。
【０１６２】
図２２は、本発明の一実施例を示す説明図（その２）である。回路モデル２のようにＣＤＣモデルが含まれる場合、ランダムに論理値を出力するため１つの入力パターンに対して数百から数千回シミュレーションを実行しなければならない。一方、回路モデル１のように通常のＦＦモデルの場合、１つの入力パターンに対して１回のシミュレーションを実行すればよい。
【０１６３】
テストベンチ２２００では、回路モデル１に関しては２回目以降のシミュレーションを実行せずに１回目のシミュレーション結果を用いている。状態変数の時間的変化には、各状態変数のシミュレーション結果が含まれている。なお、テストベンチ２２００は、シミュレーションモデルである。
【０１６４】
また、図１では、ＣＤＣを例に挙げているがこれに限らず、たとえば、図２３に示すような周辺環境が変更された場合の影響をテストするような構成であってもよい。
【０１６５】
図２３は、本発明の一実施例を示す説明図（その３）である。テストベンチ２３００では、検証対象に接続されていたモジュールＡがモジュールＡ’に置き換えられた場合にモジュールＡの場合と同様に動作するかを検証することができる。モジュールＡとモジュールＡ’とは、出力するデータは同一であるが出力のタイミングが異なる。なお、テストベンチ２３００は、シミュレーションモデルである。
【０１６６】
ここでは、第１の検出部２１０１は、入力データが第１のタイミングで対象回路に与えられた場合における当該対象回路の状態変化を検出する。具体的には、たとえば、ＣＰＵ４０１が、検証対象内の状態変化を検出する。
【０１６７】
そして、第２の検出部２１０２は、入力データが第１のタイミングとは異なる第２のタイミングで対象回路に与えられた場合における当該対象回路の状態変化を検出する。具体的には、たとえば、ＣＰＵ４０１が、検証対象内の状態変化を検出する。
【０１６８】
第１の保持部２１０３と、第２の保持部２１０４と、判断部２１０５との処理は、上述と同一であるため説明を省略する。
【０１６９】
つぎに、図２４は、実施の形態３にかかる検証支援装置２１００による検証支援処理手順の一例を示すフローチャートである。まず、検証支援装置２１００が、モデル変更前の回路内の状態変数の変化を検出し（ステップＳ２４０１）、検出結果を保持する（ステップＳ２４０３）。
【０１７０】
そして、検証支援装置２１００が、モデル変更後の回路内の状態変数の変化を検出する（ステップＳ２４０２）、検出結果を保持する（ステップＳ２４０４）。
【０１７１】
つぎに、検出結果から状態遷移系列に違いがあるか否かを判断し（ステップＳ２４０５）、あると判断された場合（ステップＳ２４０５：Ｙｅｓ）、不一致情報を出力し（ステップＳ２４０６）、一連の処理を終了する。
【０１７２】
一方、ステップＳ２４０５において、検証支援装置が、違いがないと判断した場合（ステップＳ２４０５：Ｎｏ）、一連の処理を終了する。
【０１７３】
以上説明したように、検証支援プログラム、検証支援方法、および検証支援装置によれば、入力データが与えられる対象回路内の状態変化の系列と、当該入力データの一部が変更されて与えられる対象回路内の状態変化の系列とに違いがあるか否かを判断する。したがって、内部状態を観測することで誤動作を正確に検証でき、サイクルごとに状態を比較するのではなく、状態変化の系列に違いがあるかに基づいて誤動作か否かを判断することで誤判定を抑制できる。
【０１７４】
また、メタステーブル状態によって入力データの一部が変更されて与えられる対象回路内の状態変化を検出できる。これにより、ＣＤＣに起因する障害により誤った内部状態に遷移しても、誤動作を正確に検出できる。
【０１７５】
また、入力データが与えられる対象回路内の状態変化を保持し、当該入力データの一部が変更されて与えられる対象回路内の状態変化を保持することでそれぞれの状態遷移系列が特定できる。これにより、状態遷移系列に違いがあるかに基づいて誤動作を正確に検出できる。
【０１７６】
また、入力データが与えられる対象回路内の状態変化と検出時刻を保持し、当該入力データの一部が変更されて与えられる対象回路内の状態変化と検出時刻を保持することで時間差が大きすぎれば状態遷移系列が同一であっても、誤動作であると判断する。これにより、誤動作を正確に検出できる。
【０１７７】
また、入力データが第１のタイミングで対象回路に与えられた場合における対象回路内の状態変化と、入力データが第１のタイミングと異なる第２のタイミングで対象回路に与えられた場合における対象回路内の状態変化とに違いがあるか否かを判断する。したがって、内部状態を観測することで誤動作を正確に検証でき、サイクルごとに状態を比較するのではなく、状態変化の系列に違いがあるかに基づいて誤動作か否かを判断することで誤判定を抑制できる。
【０１７８】
以上説明したように、検証支援プログラム、検証支援方法、および検証支援装置によれば、対象回路内から状態変数を検出し、シミュレーション可能なテストベンチを自動で生成する。これにより、機能検証で用いた検証環境を流用して内部状態を観測可能なシミュレーションモデルを容易に生成できる。
【０１７９】
また、メタステーブル状態の影響が伝播する可能性のある状態変数を特定してシミュレーションモデルを容易に構築することができる。
【０１８０】
また、メタステーブル状態の影響が伝播する可能性のある状態変数であり、かつ受信ＦＦからの距離が近い状態変数を特定することで、メタステーブル状態によって生じる故障を受信ＦＦの近くで検出できるシミュレーションモデルを自動で生成することができる。これにより、検証の容易化を図ることができ、検証精度を向上させることができる。
【０１８１】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムは、インターネット等のネットワークを介して配布してもよい。
【０１８２】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０１８３】
（付記１）コンピュータに、
入力データが回路に与えられた場合における前記回路内の状態変化を検出する第１の検出手順、
前記入力データの一部が変更されて前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出手順、
前記第１の検出手順により検出された状態変化の系列と前記第２の検出手順により検出された状態変化の系列とに違いがあるか否かを判断する判断手順、
前記判断手順により判断された判断結果を出力する出力手順、
を実行させることを特徴とする検証支援プログラム。
【０１８４】
（付記２）前記第２の検出手順は、
前記入力データの一部が、メタステーブル状態による影響で変更されて前記回路に与えられた場合における前記回路内の状態変化を検出することを特徴とする付記１に記載の検証支援プログラム。
【０１８５】
（付記３）前記コンピュータに、
前記第１の検出手順により状態変化が検出される都度、前記回路内の状態を順に保持する第１の保持手順と、
前記第２の検出手順により状態変化が検出される都度、前記回路内の状態を順に保持する第２の保持手段と、を実行させ、
前記判断手順は、
前記第１および第２の保持手順により保持されている順に各状態に違いがあるか否かを判断し、
前記出力手順は、
前記判断手順により判断された判断結果を出力することを特徴とする付記１または２に記載の検証支援プログラム。
【０１８６】
（付記４）前記第１の保持手順は、
前記第１の検出手順により状態変化が検出される都度、前記回路内の状態と検出時刻とを順に保持し、
前記第２の保持手順は、
前記第２の検出手順により状態変化が検出される都度、前記回路内の状態と検出時刻とを順に保持し、
前記判断手順は、
前記第１および第２の保持手順により保持されている順に各状態に違いがあるか否かを判断し、さらに、違いがないと判断された場合、前記第１の保持手順により保持されている各状態での検出時刻から前記第２の保持手順により保持されている各状態での検出時刻までの時間が、指定時間以内であるかを判断し、
前記出力手順は、
前記判断手順により判断された判断結果を出力することを特徴とする付記３に記載の検証支援プログラム。
【０１８７】
（付記５）コンピュータに、
入力データが第１のタイミングで回路に与えられた場合における前記回路内の状態変化を検出する第１の検出手順、
前記入力データが前記第１のタイミングと異なる第２のタイミングで前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出手順、
前記第１の検出手順により検出された状態変化の系列と前記第２の検出手順により検出された状態変化の系列とに違いがあるか否かを判断する判断手順、
前記判断手順により判断された判断結果を出力する出力手順、
を実行させることを特徴とする検証支援プログラム。
【０１８８】
（付記６）前記コンピュータに、
前記第１の記述情報内の各変数に対応するノードを生成してグラフを生成するノード生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の記述情報内の代入文における右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成する第１のエッジ生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の記述情報内の条件文に含まれる変数に対応するノードから前記条件文により実行される代入文の左辺の変数に対応するノードへの有向エッジを生成する第２のエッジ生成手順と、
前記第１および第２のエッジ生成手順により有向エッジが生成されたグラフ内の指定変数に対応するノードから前記有向エッジを辿って前記検出手順により検出された変数に対応するノードを探索する探索手順と、を実行させ、
前記設定手順は、
前記探索手順により探索された場合、前記比較器モデルの前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記変数のビット幅に設定することを特徴とする請求項５に記載の検証支援プログラム
【０１８９】
（付記７）前記コンピュータに、
前記第１の記述情報内の各変数に対応するノードを生成してグラフを生成するノード生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の記述情報内の代入文における右辺の変数に対応するノードから左辺の変数に対応するノードへの有向エッジを生成する第１のエッジ生成手順と、
前記ノード生成手順により生成されたグラフ内のノードのうち、前記第１の記述情報内の条件文に含まれる変数に対応するノードから前記条件文により実行される代入文の左辺の変数に対応するノードへの有向エッジを生成する第２のエッジ生成手順と、
前記第１および第２のエッジ生成手順により有向エッジが生成されたグラフ内の指定変数に対応するノードから前記有向エッジを辿って前記検出手順により検出された変数に対応するノードを探索する探索手順と、を実行させ、
前記設定手順は、
前記探索手順により探索された場合、前記比較器モデルの前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記変数のビット幅に設定することを特徴とする付記６に記載の検証支援プログラム。
【０１９０】
（付記８）前記探索手順は、
前記第１および第２のエッジ生成手順により有向エッジが生成されたグラフ内の指定変数に対応するノードから前記有向エッジを辿って前記検出手順により検出された変数に対応するノードを指定回数以内で探索し、
前記設定手順は、
前記探索手順により探索された場合、前記比較器モデルの前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記変数のビット幅に設定することを特徴とする付記７に記載の検証支援プログラム。
【０１９１】
（付記９）入力データが回路に与えられた場合における前記回路内の状態変化を検出する第１の検出手段と、
前記入力データの一部が変更されて前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出手段と、
前記第１の検出手段により検出された状態変化の系列と前記第２の検出手段により検出された状態変化の系列とに違いがあるか否かを判断する判断手段と、
前記判断手段により判断された判断結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。
【０１９２】
（付記１０）入力データが第１のタイミングで回路に与えられた場合における前記回路内の状態変化を検出する第１の検出手段と、
前記入力データが前記第１のタイミングと異なる第２のタイミングで前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出手段と、
前記第１の検出手段により検出された状態変化の系列と前記第２の検出手段により検出された状態変化の系列とに違いがあるか否かを判断する判断手段と、
前記判断手段により判断された判断結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。
【０１９３】
（付記１１）第１の変数の変化を検出し、第２の変数の変化を検出し、検出した前記第１の変数の変化の系列と検出した前記第２の変数の変化の系列とに違いがあるか否かを判断し、判断結果を出力する比較器モデルを記憶する記憶装置にアクセス可能な検証支援装置であって、
回路に関する第１の記述情報内で状態を表す変数と前記変数のビット幅を、指定ビット幅および指定条件に基づいて検出する検出手段と、
前記比較器モデル内の前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記検出手段により検出された変数のビット幅に設定する設定手段と、
前記設定手段による設定後の比較器モデルにおいて、前記第１の変数に、前記第１の記述情報内の前記変数を与え、前記第２の変数に、前記第１の記述情報のうち一部の情報が異なる第２の記述情報内で前記変数と同一変数を与えることにより、前記第１の記述情報と前記第２の記述情報と前記比較器モデルとが組み合わさったシミュレーションモデルを構築する構築手段と、
を備えることを特徴とする検証支援装置。
【０１９４】
（付記１２）コンピュータが、
入力データが回路に与えられた場合における前記回路内の状態変化を検出する第１の検出工程、
前記入力データの一部が変更されて前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出工程、
前記第１の検出工程により検出された状態変化の系列と前記第２の検出工程により検出された状態変化の系列とに違いがあるか否かを判断する判断工程、
前記判断工程により判断された判断結果を出力する出力工程、
を実行することを特徴とする検証支援方法。
【０１９５】
（付記１３）コンピュータが、
入力データが第１のタイミングで回路に与えられた場合における前記回路内の状態変化を検出する第１の検出工程、
前記入力データが前記第１のタイミングと異なる第２のタイミングで前記回路に与えられた場合における前記回路内の状態変化を検出する第２の検出工程、
前記第１の検出工程により検出された状態変化の系列と前記第２の検出工程により検出された状態変化の系列とに違いがあるか否かを判断する判断工程、
前記判断工程により判断された判断結果を出力する出力工程、
を実行することを特徴とする検証支援方法。
【０１９６】
（付記１４）第１の変数の変化を検出し、第２の変数の変化を検出し、検出した前記第１の変数の変化の系列と検出した前記第２の変数の変化の系列とに違いがあるか否かを判断し、判断結果を出力する比較器モデルを記憶する記憶装置にアクセス可能なコンピュータが、
回路に関する第１の記述情報内で状態を表す変数と前記変数のビット幅を、指定ビット幅および指定条件に基づいて検出する検出工程と、
前記比較器モデル内の前記第１の変数のビット幅と前記第２の変数のビット幅とを、前記検出工程により検出された変数のビット幅に設定する設定工程と、
前記設定工程による設定後の比較器モデルにおいて、前記第１の変数に、前記第１の記述情報内の前記変数を与え、前記第２の変数に、前記第１の記述情報のうち一部の情報が異なる第２の記述情報内で前記変数と同一変数を与えることにより、前記第１の記述情報と前記第２の記述情報と前記比較器モデルとが組み合わさったシミュレーションモデルを構築する構築工程と、
を実行することを特徴とする検証支援方法。
【符号の説明】
【０１９７】
２００  回路情報
３００  テンプレート
３０１  第１の検出器
３０２  第２の検出器
３０３  第１のＦＩＦＯバッファ
３０４  第２のＦＩＦＯバッファ
３０５  判断器
３０６  出力器
５００  検証支援装置
５０１  検出部
５０２  ノード生成部
５０３  第１のエッジ生成部
５０４  第２のエッジ生成部
５０５  探索部
５０６  設定部
５０７  構築部
５０８  出力部
２１００  検証支援装置
２１０１  第１の検出部
２１０２  第２の検出部
２１０３  第１の保持部
２１０４  第２の保持部
２１０５  判断部
２１０６  出力部
【図１】
0005471432.tif 000002
【図２】
0005471432.tif 000003
【図３】
0005471432.tif 000004
【図４】
0005471432.tif 000005
【図５】
0005471432.tif 000006
【図６】
0005471432.tif 000007
【図７】
0005471432.tif 000008
【図８】
0005471432.tif 000009
【図９】
0005471432.tif 000010
【図１０】
0005471432.tif 000011
【図１１】
0005471432.tif 000012
【図１２】
0005471432.tif 000013
【図１３】
0005471432.tif 000014
【図１４】
0005471432.tif 000015
【図１５】
0005471432.tif 000016
【図１６】
0005471432.tif 000017
【図１７】
0005471432.tif 000018
【図１８】
0005471432.tif 000019
【図１９】
0005471432.tif 000020
【図２０】
0005471432.tif 000021
【図２１】
0005471432.tif 000022
【図２２】
0005471432.tif 000023
【図２３】
0005471432.tif 000024
【図２４】
0005471432.tif 000025
【図２５】
0005471432.tif 000026
【図２６】
0005471432.tif 000027