"コンピュータに、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンを与える第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行する、処理を実行させることを特徴とする検証支援プログラム。前記第2のシミュレーションの実行終了後の前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第3のシミュレーションを、前記第1のシミュレーションと排他的に実行し、前記回路情報のうちの所定の素子の状態が、前記第2のシミュレーションと前記第3のシミュレーションの同一時刻で一致するか否かを判断し、前記所定の素子の状態が同一時刻で一致すると判断された場合、前記第3のシミュレーションを終了させる、処理を実行させることを特徴とする請求項1に記載の検証支援プログラム。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた第1のシミュレーションの時刻ごとの前記回路情報のうちの所定の素子の状態を含むシミュレーション結果を記憶する記憶装置にアクセス可能なコンピュータに、前記第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行し、前記第2のシミュレーションの実行中において、前記所定の素子の状態が、前記記憶装置に記憶された前記シミュレーション結果と前記第2のシミュレーションの同一時刻で一致するか否かを判断し、同一時刻で一致すると判断された場合に、前記第2のシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記第2のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づき前記第2のシミュレーションを実行する、処理を実行させることを特徴とする検証支援プログラム。前記所定の素子の状態が、前記記憶装置に記憶された前記シミュレーション結果と前記第2のシミュレーションの同一時刻で一致すると判断されてから一定時間以内に、前記ランダム値である出力値が検出されない場合、前記第2のシミュレーションを終了させる、処理を実行させることを特徴とする請求項3に記載の検証支援プログラム。コンピュータが、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンを与える第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行する、処理を実行することを特徴とする検証支援方法。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた第1のシミュレーションの時刻ごとの前記回路情報のうちの所定の素子の状態を含むシミュレーション結果を記憶する記憶装置にアクセス可能なコンピュータが、前記第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行し、前記第2のシミュレーションの実行中において、前記所定の素子の状態が、前記記憶装置に記憶された前記シミュレーション結果と前記第2のシミュレーションの同一時刻で一致するか否かを判断し、同一時刻で一致すると判断された場合に、前記第2のシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記第2のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づき前記第2のシミュレーションを実行する、処理を実行することを特徴とする検証支援方法。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンを与える第1のシミュレーションを実行する第1の実行手段と、前記第1の実行手段による前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出する検出手段と、前記ランダム値である出力値の前記検出手段による検出時の前記第1のシミュレーションの実行状態を複製する複製手段と、前記複製手段によって複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定する設定手段と、前記設定手段による設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行する第2の実行手段と、を備えることを特徴とする検証支援装置。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた第1のシミュレーションの時刻ごとの前記回路情報のうちの所定の素子の状態を含むシミュレーション結果を記憶する記憶装置にアクセス可能な検証支援装置であって、前記第1のシミュレーションを実行する第1の実行手段と、前記第1の実行手段による前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出する第1の検出手段と、前記ランダム値である出力値の前記第1の検出手段による検出時の前記第1のシミュレーションの実行状態を複製する複製手段と、前記複製手段により複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定する第1の設定手段と、前記第1の設定手段による設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行する第2の実行手段と、前記第2の実行手段による前記第2のシミュレーションの実行中において、前記所定の素子の状態が、前記記憶装置に記憶された前記シミュレーション結果と前記第2のシミュレーションの同一時刻で一致するか否かを判断する判断手段と、前記判断手段により同一時刻で一致すると判断された場合に、前記第2のシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出する第2の検出手段と、前記第2のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、前記第2の検出手段により検出された出力値と異なる論理値に設定する第2の設定手段と、を備え、前記第2の実行手段は、前記第2の設定手段による設定後の実行状態に基づき前記第2のシミュレーションを実行することを特徴とする検証支援装置。通常の論理シミュレーションが行われて半導体集積回路の機能にエラーがないことが検証されてから、CDCシミュレーションが行われる。そのため、CDCシミュレーションにおいてのエラーの要因となる箇所はCDC箇所である。CDC箇所とは、第1のクロックドメインのFFから第2のクロックドメインのFFにデータが受け渡されている箇所である。エラーの要因となる箇所からエラーの発生が判定される箇所までには、複数のFFや組み合わせ回路などがあるため、距離が離れており、かつ出力されるまでに時間がかかる。エラーの発生が判定される箇所とは、たとえば、検証対象回路の出力端子が挙げられる。すべてのCDCジッタの組み合わせを網羅するためには、2^CDCジッタ数^は乗数を示す通りのシミュレーションを実行させなければならず、シミュレーションに時間がかかる。1つの側面では、本発明は、シミュレーション時間を短縮することができる検証支援プログラム、検証支援方法、および検証支援装置を提供することを目的とする。本発明の一の観点によれば、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンを与える第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行する、検証支援プログラム、検証支援方法、および検証支援装置が提供される。本発明の他の観点によれば、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた第1のシミュレーションを実行し、前記第1のシミュレーションの実行中に、前記信号を受信する前記第2のクロックドメイン内の素子の出力が前記ランダム値である出力値を検出し、前記ランダム値である出力値の検出時の前記第1のシミュレーションの実行状態を複製し、複製された前記第1のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づく第2のシミュレーションを、前記第1のシミュレーションと排他的に実行し、前記第2のシミュレーションの実行中において、前記回路情報のうちの所定の素子の状態が、前記第1のシミュレーションの時刻ごとの前記所定の素子の状態を含むシミュレーション結果を記憶する記憶装置に記憶された前記シミュレーション結果と前記第2のシミュレーションの同一時刻で一致するか否かを判断し、同一時刻で一致すると判断された場合に、前記第2のシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値を検出し、前記第2のシミュレーションの実行状態のうちの前記第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定し、設定後の実行状態に基づき前記第2のシミュレーションを実行する、検証支援プログラム、検証支援方法、および検証支援装置が提供される。本検証支援プログラム、検証支援方法、および検証支援装置によれば、シミュレーション時間の短縮化を図ることができる。本実施の形態では、CDCを含む論理設計に対する検証効率の向上を図る手法の一例について説明する。以下に添付図面を参照して、本発明にかかる検証支援プログラム、検証支援方法、および検証支援装置の実施の形態を詳細に説明する。図1は、本発明のシミュレーション例を示す説明図である。まず、検証対象回路の回路情報や入力パターンにもよるが、CDCジッタは、何百個~何万個発生する。上述したようにすべてのCDCジッタの組み合わせを網羅するためには、2^総CDCジッタ数通りのシミュレーションを実行させなければならず、シミュレーションに時間がかかる。図1の例のように、CDCジッタ数がJ1~J3の3個の場合には、J1~J3の論理値の組み合わせがJ1,J2,J3=0,0,0~1,1,1までの8種類あるため、8通りのシミュレーションを行わなければならない。そこで、論理シミュレータにより回路情報に所定入力パターンを与えるシミュレーションと、該シミュレーションで発生する複数のCDCジッタのうちの1個のCDCジッタの論理値が異なるシミュレーションとで、重複する実行を省略する。これにより、シミュレーション時間を短縮することができる。図1の例では、3個のCDCジッタが発生する場合、検証支援装置が、3個のCDCジッタをそれぞれ選択して順にCDCジッタの影響が伝播するか否かを特定する。通常のCDCシミュレーションでは、4回のシミュレーションを行わなければならない。論理シミュレータでは、同時に複数のシミュレーションを行えないため、4回分のシミュレーション時間がかかる。そこで、本実施の形態では、重複するシミュレーションを行わないようにすることで、シミュレーション時間を短縮する。まず、検証支援装置が、検証対象回路の回路情報に所定入力パターンを与えるシミュレーション101のうちの1の実行中に、CDCジッタJ1を検出する。そして、検証支援装置が、CDCジッタJ1の検出時のシミュレーション101の実行状態を複製する。そして、検証支援装置が、複製されたシミュレーション101の実行状態のうちの第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定する。つぎに、検証支援装置が、設定後の実行状態に基づくシミュレーション102第2のシミュレーションをシミュレーション101と排他的に実行する。論理シミュレータは複数のシミュレーションを並列実行できないため、論理シミュレータがいずれか一方のシミュレーションを実行中には他方のシミュレーションの実行は待機する。つぎに、検証支援装置が、シミュレーション101の3の実行中に、CDCジッタJ2を検出する。そして、検証支援装置が、CDCジッタJ2の検出時のシミュレーション101の実行状態を複製する。そして、検証支援装置が、複製されたシミュレーション101の実行状態のうちの第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定する。つぎに、検証支援装置が、設定後の実行状態に基づくシミュレーション103第2のシミュレーションをシミュレーション101と排他的に実行する。図1の例では、シミュレーション103を先に行い、つづいて、シミュレーション101を行う。最後に、検証支援装置が、シミュレーション101のうちの5の実行中に、CDCジッタJ3を検出する。そして、検証支援装置が、CDCジッタJ3の検出時のシミュレーション101の実行状態を複製する。そして、検証支援装置が、複製されたシミュレーション101の実行状態のうちの第2のクロックドメイン内の素子の出力を、検出された出力値と異なる論理値に設定する。つぎに、検証支援装置が、設定後の実行状態に基づくシミュレーション104第2のシミュレーションをシミュレーション101と排他的に実行する。図1の例では、検証支援装置が、シミュレーション104の実行を先に行い、つづいて、シミュレーション101の実行の続きを行う。図1のCDCシミュレーション例では、通常のCDCシミュレーションシミュレーション111~114例と比較して、1×3のシミュレーション時間と、3×2のシミュレーション時間と、5のシミュレーション時間が短縮される。本実施の形態に関する詳細な説明に先立って、理解の容易化のため、CDCとCDCシミュレーションについてより詳細に説明する。図2は、CDCの一例を示す説明図である。図2では、第1のクロックドメイン内のFFFlipFlopの出力信号である信号S1が第2のクロックドメイン内のFFの入力信号となっている。第1のクロックドメイン内のFFはCLK1に同期して動作し、第2のクロックドメイン内のFFはCLK2に同期して動作している。第1のクロックドメイン内のFFから第2のクロックドメイン内のFFへデータが受け渡されると、第2のクロックドメイン内のFFのクロックのタイミングに関わらず該データが入力される。各FFにはセットアップタイムとホールドタイムが定義されており、セットアップタイムとホールドタイムが違反されると、メタステーブル状態が発生する。メタステーブル状態とは出力が不安定な状態であり、0か1のいずれが出力されるか不明確な状態である。第1のクロックドメイン内のFFの出力である信号S1がCLK2の立ち上がり付近で変化すると、タイミングチャート200で示すように、第2のクロックドメイン内のFFのセットアップタイムまたはホールドタイムが違反される場合がある。この違反により、第2のクロックドメイン内のFFの出力である信号S2がメタステーブル状態となる場合がある。メタステーブル状態の影響が論理値の差異として後段のFFや組み合わせ回路に伝播し、半導体集積回路が誤動作することがある。そのため、メタステーブル状態が発生しても半導体集積回路が誤動作しないことを検証しなければならない。つぎに、通常のFFのモデルを用いた論理シミュレーションについて説明する。図3は、通常のFFのモデルが使用されたシミュレーション結果の一例を示す説明図である。通常のFFのモデルが使用されたシミュレーションでは、タイミングチャート300で示すようにS1の変化がCLK2の立ち上がり付近で発生しても、CLK2の立ち上がり時の信号S1の値が信号S2へ出力される。すなわち、セットアップタイムやホールドタイムの違反があっても、この違反による影響をシミュレーションすることができない。そこで、第1のクロックドメインのFFから非同期で信号を受け渡される第2のクロックドメインのFFのモデルがメタステーブル状態の影響を模擬するモデル以下CDCモデルに変更される。つぎに、CDCモデルを用いたCDCシミュレーションについて説明する。図4は、CDCモデルが使用されたシミュレーション結果の一例を示す説明図である。回路情報401では、第1のクロックドメインからのS1信号を受信するFFがCDCモデルに変更されている。タイミングチャート402では、S1の変化がCLK2の立ち上がり付近で発生すると、CLK2の立ち上がり時にS2には0または1のランダム値が1クロックサイクル期間中に出力される。ここでは、1クロックサイクル期間中のランダムな値をCDCジッタと称する。図5は、CDC検証の一連の流れを示すフローチャートである。論理シミュレータを有し、論理シミュレーションが可能なコンピュータが、検証対象回路の回路情報に所定入力パターンを与えてCDCシミュレーションを実行するステップS501。そして、コンピュータが、論理障害以降、エラーと称する。を検出したか否かを判断するステップS502。コンピュータが、エラーを検出したと判断した場合ステップS502:Yes、検証者が、手作業でデバッグしステップS503、ステップS501へ戻ることで、コンピュータが、デバッグ後の回路情報を用いてCDCシミュレーションを実行する。デバッグとは、具体的には、論理障害要因以降、エラー要因と称する。分析や論理修正を示している。コンピュータが、エラーを検出していないと判断した場合ステップS502:No、検証者が、カバレッジ情報を用いてカバレッジ不足であるか否かを判断するステップS504。検証者が、カバレッジ不足であると判断した場合ステップS504:Yes、実行条件を変更しステップS505、ステップS501へ戻る。ここで、実行条件の変更とは、乱数系列の変更や、入力パターンの変更である。検証者が、カバレッジ不足でないと判断した場合ステップS504:No、CDC検証を終了する。CDCシミュレーションでは、メタステーブル状態の影響がシミュレーション結果に含まれているため、障害要因エラー要因の分析が難しい。そのため、まず、検証者は、CDCモデルへの変更前の通常の論理シミュレーションにより通常の機能に問題が無いことを確認する。その後、検証者は、通常の論理シミュレーションで用いたのと同じ入力パターンを用いてCDCシミュレーションを行い、メタステーブル状態の影響に起因する問題が無いかを検査する。CDCのカバレッジ判定基準としては、通常のCDCシミュレーションの実行結果を用いてCDCジッタの影響が観測点まで現れているか否かによって、カバレッジの不足を判断する。たとえば、観測点は、出力端子、検証対象回路の状態を表すFFの出力、CDCモデルの後段の素子の出力であってもよい。また、たとえば、観測点は、第1のクロックドメインから第2のクロックドメインへ受け渡される複数のCDC信号が合流する箇所、アサーションであってもよい。アサーションとは、検証対象の設計が満たすべき性質が定義された箇所である。上述したように、すべてのCDCジッタの組み合わせを網羅するためには、2^CDCジッタ数^は乗数を示す通りのシミュレーションを実行させなければならず、シミュレーションに時間がかかるという問題点がある。さらに、すべてのCDCジッタの組み合わせをシミュレーションしない場合には、検証者が手作業でデバックしながら任意に選んだCDCジッタの組み合わせのみをシミュレーションするため、エラー要因の分析に時間がかかるという問題点がある。図6は、CDCジッタの影響伝播の観測例を示す説明図である。図6では、検証者によるエラー要因の分析を容易化するために、検証支援装置が、各CDCの影響が観測点まで伝播しているか否かを検証する例を示す。図6では、検証支援装置が、あるCDCジッタの出力値を、所定入力パターンでCDCシミュレーションしたシミュレーション結果時のCDCジッタの論理値と異なる論理値に設定する。そして、検証支援装置が、該シミュレーション結果と設定後でのシミュレーション結果とに基づき所定入力パターンにおいて各CDCジッタの影響が観測点まで伝播されているかを特定する。図6では、検証支援装置が、テストベンチへ入力パターンを与えると、第2のクロックドメインのCDCモデルからCDCジッタJ1,J2が発生する。CDCジッタJ1,2の論理値の組み合わせによって、4通りの実行パターンが得られる。実行パターンの組み合わせについては、P=J1,J2で示す。図6の実行パターンP0は、J1,J2=0,1である。そして、検証支援装置が、実行パターンP0のCDCジッタJ0の論理値と異なる論理値に設定した実行パターンP1=J1,J2=1,1のシミュレーションを行う。そして、図6では、観測点のP0のシミュレーション結果と観測点のP1のシミュレーション結果とが異なるため、検証支援装置が、観測点にCDCジッタJ1の影響が伝播していると判断する。そして、検証支援装置が、実行パターンP0のCDCジッタJ1の論理値と異なる論理値に設定した実行パターンP2=J1,J2=0,0のシミュレーションを行う。そして、図6では、観測点のP0のシミュレーション結果と観測点のP2のシミュレーション結果とが異なるため、検証支援装置が、観測点にCDCジッタJ2の影響が伝播していないと判断する。したがって、CDCジッタJ1,2の組み合わせは4通りであるが、検証支援装置が、3通りの組み合わせを検証すれば、どのCDCジッタの影響が伝播したか否かを判断することができる。さらに、影響の伝播によって、検証者が、どのCDCジッタの影響がエラーに関係するかを判定することができる。これにより、検証支援装置が、シミュレーション回数を減らしつつ、CDCジッタによるエラー要因の特定を容易化することができる。そして、本実施の形態1,2では、図6で示すような複数のCDCジッタのうちの1個のCDCジッタの論理値のみが異なるシミュレーションの重複するシミュレーションを省くことで、シミュレーション時間を短縮する。つぎに、本実施の形態1,2における検証支援装置のハードウェア構成例と、実施の形態1と実施の形態2とで用いるシミュレーションモデルについて説明する。検証支援装置のハードウェア構成例図7は、検証支援装置のハードウェア構成例を示すブロック図である。図7において、検証支援装置700は、CPUCentralProcessingUnit701と、ROMRead‐OnlyMemory702と、RAMRandomAccessMemory703と、を有している。さらに、検証支援装置700は、磁気ディスクドライブ704と、磁気ディスク705と、光ディスクドライブ706と、光ディスク707と、ディスプレイ708と、I/FInterface709と、を有している。さらに、検証支援装置700は、キーボード710と、マウス711と、スキャナ712と、プリンタ713と、を有している。また、各部はバス715によってそれぞれ接続されている。ここで、CPU701は、検証支援装置700の全体の制御を司る。ROM702は、ブートプログラムなどのプログラムを記憶している。RAM703は、CPU701のワークエリアとして使用される。磁気ディスクドライブ704は、CPU701の制御にしたがって磁気ディスク705に対するデータのリード/ライトを制御する。磁気ディスク705は、磁気ディスクドライブ704の制御で書き込まれたデータを記憶する。光ディスクドライブ706は、CPU701の制御にしたがって光ディスク707に対するデータのリード/ライトを制御する。光ディスク707は、光ディスクドライブ706の制御で書き込まれたデータを記憶したり、光ディスク707に記憶されたデータをコンピュータに読み取らせたりする。ディスプレイ708は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ708は、たとえば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。I/F709は、通信回線を通じてLANLocalAreaNetwork、WANWideAreaNetwork、インターネットなどのネットワーク714に接続され、このネットワーク714を介して他の装置に接続される。そして、I/F709は、ネットワーク714と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F709には、たとえばモデムやLANアダプタなどを採用することができる。キーボード710は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス711は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ712は、画像を光学的に読み取り、検証支援装置700内に画像データを取り込む。なお、スキャナ712は、OCROpticalCharacterReader機能を持たせてもよい。また、プリンタ713は、画像データや文書データを印刷する。プリンタ713には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。シミュレーションモデル図8は、シミュレーションモデルの一例を示す説明図である。シミュレーションモデル800では、テストベンチ812とシミュレーションプロセス制御部811を有している。シミュレーションモデル800は、具体的には、たとえば、Verilog-HDLHardwareDescriptionLanguageやSystem-Verilogなどのハードウェア記述言語で記述されている。シミュレーションモデル800は、RAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶されている。まず、シミュレーションプロセス制御部811は、テストベンチ812を制御するモデルである。シミュレーションプロセス制御部811の詳細については、後述する。つぎに、テストベンチ812は、検証対象回路モデル822と、入力パターン発生器821と、エラー検出器823と、を有している。論理シミュレータによりテストベンチ812のシミュレーションの実行が開始すると、入力パターン発生器821が入力パターンを発生する。そして、論理シミュレータにより検証対象回路モデル822に入力パターンが与えられて、該入力パターンに沿って検証対象回路モデル822がシミュレーションされる。検証対象回路モデル822から検証に用いる信号がシミュレーション結果として出力される。そして、エラー検出器823がシミュレーション結果と期待値とを比較することにより、エラーを検出する。そして、検証対象回路モデル822は、検証対象回路の回路情報であり、本実施の形態で用いる詳細例は図9に示す。検証対象回路モデル822図9は、検証対象回路モデル822の第2のクロックドメイン一例を示す説明図である。図9で示したように検証対象回路モデル822は、第1のクロックドメイン901と第2のクロックドメイン902とを有している。第2のクロックドメイン902は、CDCモデル921と、CDCモデル922と、アップダウン回路923と、を有している。第1のクロックドメイン901のFF911から信号UPがCDCモデル921に入力されている。第1のクロックドメイン901のFF912から信号DOWNがCDCモデル922に入力されている。たとえば、アップダウン回路923は、アップダウンカウンタである。より具体的には、アップダウン回路923では、信号UPがHighになると信号AがHighになるため、信号Cの値をカウントアップし、信号DownがHighになると信号BがHighになるため、信号Cの値をカウントダウンする。ここでは、信号UPと信号Downが同時にHighにならないこととする。CDCモデル図10は、図9で示したCDCモデルの一例を示す説明図である。図10のCDCモデル1000では、入力信号の変化を検出し、該変化の検出時から一定時間経過以内にクロックイベントが発生すると、該クロックイベントの期間にランダム値を出力する動作が記述されている。CDCモデル1000では、JitterDetector1001と、FF1002と、FF1003と、選択回路1004と、を有している。JitterDetector1001は、入力信号の値の変化を検出し、該変化の検出時から一定時間経過するまで1を出力する。FF1002は、JitterDetector1001の出力をCLK2の立ち上がりで取り込む。選択回路1004は、FF1002の出力信号が0であれば、FF1003の出力信号を出力し、FF1002の出力信号が1であれば、外部から入力された値が出力される。ここでは、外部から入力された値とは、たとえば、ランダム値、0、1のいずれかが入力される。通常のCDCモデルであれば、ランダム値だけであるが、本実施の形態では、シミュレーションプロセス制御部811またはテストベンチ812によってランダム値、0または1が入力される。これにより、検証支援装置700が、図9で示したCDCモデル921やCDCモデル922が出力する論理値と異なる論理値を設定することができる。CDCモデル1000は、たとえば、ライブラリとしてRAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶されている。検証対象回路モデル822では、該ライブラリ内に記憶された該CDCモデルを指定する。論理シミュレータが該ライブラリからCDCモデルを読み出して、CDCモデルに記述された処理を実行する。つぎに、図11を用いてJitterDetector1001の詳細例を説明する。図11は、JitterDetectorの一例を示す説明図である。JitterDetector1100では、入力信号がTであり、出力信号がEである。JitterDetector1100では、Tの値が0から1または1から0に変化すると、Eの値はPERIOD分の時間が経過するまで1となる。JitterDetector1100は、たとえば、ライブラリとしてRAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶されている。CDCモデル1000では、該ライブラリ内に記憶されたJitterDetector1100を指定する。論理シミュレータは、該ライブラリからJitterDetector1100に記述された処理を読み出して、JitterDetector1100に記述された処理を実行する。図12は、入力パターンと期待値の一例を示す説明図である。図12のタイミングチャート1200では、CLK2の立ち上がりから次の立ち上がりの直前までを1周期として、理解の容易化のために、CLK2の上に順に番号を付している。たとえば、1クロック目の立ち上がりは、図中矢印の箇所である。まず、入力パターンにおいて、2クロック目の立ち上がりで信号UPがセットアップタイムまたはホールドタイムを違反しているため、期待値において、信号AがCDCジッタJ1となる。つぎに、入力パターンにおいて、8クロック目の立ち上がりで信号UPと信号DOWNがセットアップタイムまたはホールドタイムを違反しているため、期待値において、信号AがCDCジッタJ2となり、信号BがCDCジッタJ3となる。そして、入力パターンにおいて、18クロック目の立ち上がりで信号UPと信号DONWがセットアップタイムまたはホールドタイムを違反しているため、期待値において、信号AがCDCジッタJ4となり、信号BがCDCジッタJ5となる。実施の形態1では、CDCジッタJ1~J3を用いて説明し、実施の形態2では、CDCジッタJ1~J5を用いて説明する。実施の形態1まず、実施の形態1では、重複するシミュレーションを減らすために、基本実行パターンのシミュレーションを実行中にCDCジッタを検出し、検出したCDCジッタの影響が伝播するか否かを確認するシミュレーションを行う。これにより、シミュレーション時間を減少させることができる。実施の形態1にかかる検証支援装置700の機能例を示すブロック図図13は、実施の形態1にかかる検証支援装置700の機能例を示すブロック図である。検証支援装置700は、親プロセス1300と、子プロセス1320-ii=1~総CDCジッタ数と、を有している。親プロセス1300は、基準実行パターンに関する第1のシミュレーションを実行し、1以上の子プロセス1320-iを生成する。子プロセス1320-iは、複数のCDCジッタのうちの1個のCDCジッタの論理値が基準実行パターンでの論理値と異なる論理値となる反転実行パターンに関する第2のシミュレーションを実行する。親プロセス1300が、実行部1301と、検出部1302と、生成部1303と、算出部1304と、受信部1305と、判断部1306と、制御部1307と、出力部1308と、を有している。子プロセス1320-iが、実行部1321-iと、算出部1322-iと、送信部1323-iと、を有している。親プロセス1300の実行部1301から出力部1308の処理は、たとえば、上述したシミュレーションモデル800のシミュレーションプロセス制御部811にコーディングされている。さらに、子プロセス1320-iの実行部1321-iと送信部1323-iの処理とは、たとえば、上述したシミュレーションモデル800のシミュレーションプロセス制御部811にコーディングされている。CPU701が、論理シミュレータを起動し、論理シミュレータにシミュレーションモデル800を与えることで、論理シミュレータが、シミュレーションモデル800のシミュレーションプロセス制御部811に記述されているコードを処理する。つぎに、各部について図13を用いて詳細に説明する。図14は、実施の形態1にかかるシミュレーション例を示す説明図である。図14のタイミングチャート1400における1~5は実行順である。図14の例では、上述した入力パターンのうちの17クロック目までを示すため、総CDCジッタ数は3であり、iは1~3である。まず、たとえば、実行部1301は、入力パターンを与えるシミュレーション1401を実行する。たとえば、シミュレーション1401では、実行パターンP0=J1,J2,J3=1,0,0とする。実行パターンP0については、CDCジッタでランダム値を発生させてもよいし、検証者があらかじめ指定してもよい。また、たとえば、算出部1304は、シミュレーション1401の実行中に所定時間ごとに所定の素子の状態と観測点の状態に関するハッシュ値を算出する。所定時間は、たとえば、シミュレーションモデル800内で定義された実行単位であってもよい。所定の素子としては、たとえば、FFが挙げられる。検証対象回路モデル822では、所定の素子がCDCモデル921と、CDCモデル922と、アップダウン回路923である。ハッシュ値を用いることで、検索を高速化させることができる。ハッシュ値については、公知技術たとえば、AnImprovedProtocolReachabilityAnalysisTechnique,GERARDJ,HOLZMANN,BellLaboratoriesまたはRelieableHashingwithoutCollisionDetection,PierreWolperandDenisLeroy,ComputerAidedVerification,Proc,Int.WorkShop,Elounda,Crete,LectureNotesinComputerScience,Vol.697,SpringerVerlag,June,1993に基づいて算出してもよい。そして、出力部1308は、シミュレーション時刻と算出した所定の素子の状態に関するハッシュ値との組み合わせを実行パターンP1に関連付けて出力する。出力形式としては、たとえば、I/F709による外部装置への送信がある。また、たとえば、RAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶することとしてもよい。つぎに、たとえば、検出部1302は、実行部1301によるシミュレーション1401の実行中に、CDCジッタを検出する。具体的には、検出部1302は、シミュレーション1401の実行中にランダム値が発生したか否かを判断することで、CDCジッタを検出してもよい。または、たとえば、検出部1302は、図10で示したCDCモデル1000内の選択回路1004に入力される選択信号が1であるか否かを監視することでCDCジッタを検出してもよい。または、実行パターンP0があらかじめ検証者によって指定されている場合には、いずれのタイミングでCDCジッタが発生するか親プロセス1300が把握しているとし、検出部1302が、何クロック目であるかに基づいてCDCジッタを検出してもよい。まずは、検出部1302が、2クロック目の立ち上がりでCDCジッタJ1を検出する。つぎに、たとえば、生成部1303は、検出部1302により検出されたCDCジッタJ1を出力する素子の出力値が検出部1302で検出された論理値と異なる論理値であるシミュレーション1402を実行する子プロセス1320-1を生成する。具体的には、生成部1303は、複製部1311と設定部1312と起動部1313とを有している。たとえば、複製部1311は、検出部1302による検出時のシミュレーション1401の実行状態を複製する。実行状態とは、具体的には、たとえば、メモリイメージである。メモリイメージは、たとえば、RAM703内で確保されるシミュレーション1401に関する情報であり、シミュレーションモデル800のコードや検証対象回路モデル822内の各信号の値である。そして、たとえば、設定部1312は、複製部1311により複製されたシミュレーション1401の実行状態のうちの検出部1302で検出されたCDCジッタJ1を出力する素子の出力値を検出部1302による検出時の論理値と異なる論理値に設定する。これにより、シミュレーション1402では、実行パターンP1=J1,J2,J3=0,0,0となる。そして、たとえば、起動部1313は、設定部1312により設定後の実行状態を子プロセス1320-1の実行状態に指定し、子プロセス1320-1を起動する。生成部1203により子プロセス1320-1が生成されると、子プロセス1320-1の実行部1321-1は、設定後の実行状態に基づいてシミュレーション1402をシミュレーション1401と排他的に実行する。論理シミュレータでは、同時に2つのシミュレーションを実行させることができないため、シミュレーション1401とシミュレーション1402とは排他的に実行される。図14の例では、シミュレーション1402がシミュレーション1401のうちのCDCジッタJ1の発生以降のシミュレーションよりも先に行われている。そして、たとえば、送信部1323-1は、所定時間ごとに所定の素子の状態および観測点の状態に関するハッシュ値を算出する。そして、たとえば、送信部1323-1は、所定時間ごとにシミュレーション時刻と算出したハッシュ値との組み合わせを親プロセス1300に対して送信する。そして、たとえば、受信部1305は、子プロセス1320-1からのシミュレーション時刻とハッシュ値の組み合わせを受信する。そして、たとえば、判断部1306は、出力部1308によって実行パターンP0に関連付けられて記憶装置に記憶された組み合わせのうち、受信部1305により受信された組み合わせと同一の組み合わせがあるか否かを判断する。ここでは、シミュレーション1402がシミュレーション1401のCDCジッタJ1の発生以降よりも先に実行されているため、シミュレーション1401での所定素子の状態が不明である。そのため、たとえば、出力部1308は、シミュレーション時刻とハッシュ値とを組み合わせとして実行パターンP1に関連付けて出力する。出力形式としては、たとえば、RAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶される。つぎに、実行部1301は、シミュレーション1402が終了することで、子プロセス1320-1が終了すると、シミュレーション1401のCDCジッタJ1の発生以降を実行する。そして、たとえば、検出部1302は、8クロック目の立ち上がりでCDCジッタJ2とCDCジッタJ3を検出する。まず、たとえば、生成部1303は、検出部1302により検出されたCDCジッタJ2を出力する素子の出力値が検出部1302による検出時の論理値と異なる論理値であるシミュレーション1403を実行する子プロセス1320-2を生成する。生成部1303による具体的なシミュレーション1403を実行する子プロセス1320-2の生成処理は、シミュレーション1402を実行する子プロセス1320-1の生成処理と同一処理であるため、詳細な説明を省略する。これにより、シミュレーション1403では、実行パターンP2=J1,J2,J3=1,1,0となる。そして、実行部1321-2は、設定後の実行状態に基づいてシミュレーション1403を実行する。そして、たとえば、算出部1322-2は、所定時間ごとに所定の素子の状態および観測点の状態に関するハッシュ値を算出する。そして、送信部1323-2は、シミュレーション時刻と算出部1322-2により算出されたハッシュ値との組み合わせを親プロセス1300に対して送信する。そして、たとえば、受信部1305は、子プロセス1320-2から、シミュレーション時刻とハッシュ値との組み合わせを受信する。そして、たとえば、判断部1306は、出力部1308によって出力された実行パターンP1,P2に関連付けられたシミュレーション時刻とハッシュ値の組み合わせのうち、受信部1305により受信された組み合わせと同一の組み合わせがあるか否かを判断する。図14では、たとえば、16クロック目の子プロセス1320-2によるシミュレーション1403の信号A,B,Cは、子プロセス1320-1によるシミュレーション1402の信号A,B,Cと同一である。そのため、判断部1306は、受信部1305により受信された組み合わせと同一の組み合わせがあると判断する。つぎに、制御部1307は、判断部1306により受信された組み合わせと同一の組み合わせがあると判断された場合、子プロセス1320-2を強制終了する。すなわち、17クロック目以降の子プロセス1320-2によるシミュレーション1403は、子プロセス1320-1によるシミュレーション1402と同一となるため、実行させなくてもよい。そのため、制御部1307が子プロセス1320-2を強制終了することで、シミュレーション時間を短縮することができる。つぎに、生成部1303は、CDCジッタJ1,2に関する子プロセス1320-1,2の生成と同様にCDCジッタJ3に関する反転パターンのシミュレーション1404を実行する子プロセス1320-3を生成する。そして、実行部1321-3は、シミュレーション1404を実行する。これにより、シミュレーション1403では、実行パターンP3=J1,J2,J3=1,0,1となる。また、シミュレーション1404の9クロック目での信号A,B,Cの論理値がシミュレーション1404の9クロック目での信号A,B,Cの論理値とそれぞれ同一となっている。そのため、シミュレーション1404の10クロック目以降はシミュレーション1402と同一となるので、たとえば、制御部1307が、子プロセス1320-3を強制終了させる。そして、実行部1301は、シミュレーション1401のCDCジッタJ3の発生以降を実行する。実施の形態1にかかる検証支援装置700が行う処理手順図15は、実施の形態1にかかる検証支援装置700の親プロセス1300が行う処理手順を示すフローチャートである。まず、親プロセス1300が、実行部1301により、第1のシミュレーションを開始しステップS1501、第1のシミュレーションが終了したか否かを判断するステップS1502。親プロセス1300が、第1のシミュレーションが終了していないと判断した場合ステップS1502:No、第1のシミュレーションを1ステップ実行するステップS1503。ここで、1ステップとは、シミュレーションモデル800で定義された時間であり、シミュレーションを行う際の実行時間の単位となる。1ステップは、検証者が任意に設定する時間であるが、たとえば、いずれかのクロックの1サイクル分の時間や半サイクル分の時間である。つぎに、親プロセス1300が、所定の素子に関するハッシュ値を算出しステップS1504、シミュレーション時刻とハッシュ値との組み合わせを基本実行パターンに関連付けて出力するステップS1505。親プロセス1300が、検出部1302により、CDCジッタの発生を検出したか否かを判断するステップS1506。親プロセス1300が、CDCジッタの発生を検出していないと判断した場合ステップS1506:No、ステップS1502へ戻る。また、親プロセス1300が、CDCジッタの発生を検出したと判断した場合ステップS1506:Yes、複製部1311により、検出時の第1のシミュレーションの実行状態を複製するステップS1507。そして、親プロセス1300が、設定部1312により、複製された第1のシミュレーションの実行状態のうち、検出したCDCジッタを出力する素子の出力を、検出時の出力値と異なる論理値に設定するステップS1508。親プロセス1300が、起動部1313により、設定後の実行状態に基づく子プロセス1320を起動するステップS1509。つぎに、親プロセス1300が、子プロセス1320が終了したか否かを判断するステップS1510。親プロセス1300が、子プロセス1320が終了したと判断した場合ステップS1510:Yes、ステップS1502へ戻る。また、親プロセス1300が、子プロセス1320が終了していないと判断した場合ステップS1510:No、受信部1305により、子プロセス1320からシミュレーション時刻と所定の素子の状態に関するハッシュ値の組み合わせを受信するステップS1511。つぎに、親プロセス1300が、判断部1306により、受信した組み合わせが新しいか否かを判断するステップS1512。そして、親プロセス1300が、組み合わせが新しいと判断した場合ステップS1512:Yes、出力部1308により、組み合わせを子プロセス1320の実行パターンに関連付けて出力しステップS1513、ステップS1510へ戻る。また、親プロセス1300が、組み合わせが新しくないと判断した場合ステップS1512:No、制御部1307により、子プロセス1320を強制終了させステップS1514、ステップS1502へ戻る。そして、ステップS1502において、親プロセス1300が、第1のシミュレーションが終了したと判断した場合ステップS1502:Yes、一連の処理を終了する。図16は、実施の形態1にかかる検証支援装置700の子プロセス1320-iが行う処理手順を示すフローチャートである。まず、子プロセス1320-iが、実行部1321-iにより、第2のシミュレーションの実行を開始しステップS1601、第2のシミュレーションが終了したか否かを判断するステップS1602。つぎに、子プロセス1320-iが、第2のシミュレーションが終了していないと判断した場合ステップS1602:No、実行部1321-iにより、所定時間分の第2のシミュレーションを実行するステップS1603。そして、子プロセス1320-iが、送信部1323-iにより、所定の素子に関するハッシュ値を算出するステップS1604。そして、子プロセス1320-iが、1322-iにより、シミュレーション時刻とハッシュ値との組み合わせを親プロセス1300に送信しステップS1605、ステップS1602へ戻る。ステップS1602において、子プロセス1320-iが、第2のシミュレーションが終了したと判断した場合ステップS1602:Yes、一連の処理を終了する。実施の形態1によれば、異なる実行パターンのシミュレーションのうち、重複するシミュレーションを省くことで、シミュレーション時間を短縮することができる。実施の形態2つぎに、実施の形態2では、基準実行パターンと、基準実行パターンと1個のCDCジッタの論理値が異なる実行パターンと、が同一シミュレーション時刻で同一状態となってもシミュレーションを止めずに、他の実行パターンのシミュレーションに再利用する。これにより、実行状態の複製にかかる時間と論理値の設定にかかる時間とを併せたシミュレーションの起動にかかる時間を省略することで、シミュレーション時間を短縮することができる。図17は、実施の形態2によるシミュレーションの起動回数削減例を示す説明図である。実施の形態2の例では、実行パターンP1のシミュレーションが基準実行パターンP0のシミュレーションと一致しても、実行パターンP1のシミュレーションを継続し、あらたに実行パターンP4のシミュレーションとして再利用する。さらに、実施の形態2の例では、実行パターンP4のシミュレーションが基準実行パターンP0のシミュレーションと一致したら、あらたに実行パターンP6のシミュレーションとして再利用する。さらに、実施の形態2の例では、実行パターンP2のシミュレーションが基準実行パターンP0のシミュレーションと一致しても、実行パターンP2のシミュレーションを継続し、あらたに実行パターンP3のシミュレーションとして再利用する。そして、実施の形態2の例では、実行パターンP3のシミュレーションが基準実行パターンP0のシミュレーションと一致したら、あらたに実行パターンP5のシミュレーションとして再利用する。一方、実施の形態1の例では、実行パターンP1~P9の各シミュレーションが基準実行パターンP0のシミュレーションと一致したら、実行パターンP1~P9のシミュレーションを終了する。たとえば、検証対象回路の素子数が大きければ、実行状態の複製処理にかかる時間も長くなる。上述したように、CDCジッタの数が何百個や何千個もある場合には、実施の形態1では何百回や何千回も複製処理を行わなければならないが、実施の形態2では、実施の形態1と比較して実行状態の複製処理の回数を削減することができる。これにより、実施の形態2では、シミュレーション時間を短縮することができる。実施の形態2にかかる検証支援装置700の機能例を示すブロック図図18は、実施の形態2にかかる検証支援装置700の機能例を示すブロック図である。検証支援装置700は、親プロセス1800と、子プロセス1820と、子プロセス1830-jと、を有している。親プロセス1800は、基本実行パターンに関する第1のシミュレーションを実行し、子プロセス1820や子プロセス1830-jを起動する。子プロセス1820は、基本実行パターンに関するシミュレーションを実行する。子プロセス1830-jは、反転実行パターンに関する第2のシミュレーションを実行する。検証支援装置700の親プロセス1800は、実行部1801と、検出部1802と、生成部1803と、算出部1804と、受信部1805と、判断部1806と、制御部1807と、出力部1808と、送信部1809と、を有している。検証支援装置700の基本実行パターンに関するシミュレーションを実行する子プロセス1820は、実行部1821と、算出部1822と、送信部1823と、を有している。検証支援装置700の反転実行パターンに関するシミュレーションを実行する子プロセス1830-jは、実行部1831-jと、算出部1832-jと、送信部1833-jと、受信部1834-jと、判断部1835-jと、を有している。さらに、子プロセス1830-jは、制御部1836-jと、検出部1837-jと、設定部1838-jと、を有している。親プロセス1800の実行部1801から送信部1809の処理は、たとえば、上述したシミュレーションモデル800のシミュレーションプロセス制御部811にコーディングされている。さらに、子プロセス1820の実行部1821から送信部1823の処理と、子プロセス1830-jの実行部1831-jと設定部1838-jの処理とは、たとえば、上述したシミュレーションモデル800のシミュレーションプロセス制御部811にコーディングされている。CPU701が、論理シミュレータを起動し、論理シミュレータにシミュレーションモデル800を与えることで、論理シミュレータが、シミュレーションモデル800のシミュレーションプロセス制御部811に記述されているコードを処理する。これにより各部の処理が実現される。つぎに、各部について図13を用いて詳細に説明する。図19は、実施の形態2によるシミュレーション例を示す説明図である。図19のタイミングチャート1900における1~7は実行順である。図19の例では、総CDCジッタ数は5であり、iは1~5である。まず、たとえば、実行部1801は、基準実行パターンに関するシミュレーション1901を実行する。たとえば、シミュレーション1901では、基準実行パターンである実行パターンP0=J1,J2,J3,J4,J5=1,0,0,0,0とする。実行パターンP0については、CDCジッタでランダム値を発生させてもよいし、検証者があらかじめ指定してもよい。まず、実行部1801は、シミュレーション1901を実行する。つぎに、検出部1802は、シミュレーション1901の実行中に、CDCジッタを検出する。CDCジッタの検出処理については、実施の形態1で説明した検出処理と同一である。まずは、検出部1802が、CDCジッタJ1を検出する。生成部1803は、検出部1802によりCDCジッタJ1が検出されると、基本実行パターンに関するシミュレーションが実行済か否かを判断する。そして、生成部1803は、基本実行パターンに関するシミュレーションを実行する子プロセス1820が実行済でないと判断した場合、基本実行パターンに関するシミュレーションを実行する子プロセス1820を生成する。たとえば、生成部1803は、複製部1811と起動部1813を有している。たとえば、複製部1811は、CDCジッタJ1の検出時のシミュレーション1901の実行状態を複製する。そして、起動部1813は、複製されたシミュレーション1901の実行状態を子プロセス1820の実行状態として指定し、子プロセス1820を起動する。そして、子プロセスの実行部1821は、シミュレーション1902を実行する。たとえば、算出部1822は、所定時間ごとに所定の素子に関するハッシュ値を算出する。そして、たとえば、送信部1823は、シミュレーション時刻と算出部1822により算出されたハッシュ値との組み合わせを親プロセス1800に送信する。たとえば、受信部1805は、子プロセス1820からのシミュレーション時刻とハッシュ値の組み合わせを受信する。たとえば、出力部1808は、受信部1805によって受信された子プロセス1820からの組み合わせを実行パターンP0と関連付けて出力する。出力形式としては、たとえば、RAM703、磁気ディスク705、光ディスク707などの記憶装置に記憶される。つぎに、子プロセス1820が終了すると、生成部1803は、検出されたCDCジッタJ1を出力する素子の出力値が、検出時の論理値と異なる論理値である実行パターンP1に関するシミュレーション1903を実行する子プロセス1830-1を生成する。具体的には、生成部1803は、複製部1811と、設定部1812と、起動部1813と、を有している。たとえば、複製部1811は、CDCジッタJ1の検出時のシミュレーション1901の実行状態を複製する。そして、設定部1812は、複製されたシミュレーション1901の実行状態のうちの検出されたCDCジッタを出力する素子の出力を、検出時の論理値と異なる論理値に設定する。そして、起動部1813は、設定部1812による設定後の実行状態を子プロセス1830-1の実行状態として指定し、子プロセス1830-1を起動する。これにより、シミュレーション1903では、実行パターンP1=J1,J2,J3,J4,J5=0,0,0,0,0となる。そして、実行部1831-1は、シミュレーション1903を実行する。つぎに、算出部1832-1は、所定時間ごとに所定の素子に関するハッシュ値を算出する。そして、たとえば、送信部1833-1は、シミュレーション時刻と算出部1822により算出されたハッシュ値との組み合わせを親プロセス1800に送信する。そして、受信部1805は、子プロセス1830-1からの組み合わせを受信する。そして、判断部1806は、すでにシミュレーション済の基本実行パターンに関連付けられたシミュレーション時刻とハッシュ値との組み合わせのうち、受信部1805により受信された組み合わせと同一の組み合わせがあるか否かを判断する。たとえば、子プロセス1830-1から送信された組み合わせのシミュレーション時刻が、14クロック目を示すシミュレーション時刻である場合、実行パターンP1の状態と、実行パターンP0の状態とが、一致している。そのため、判断部1806は、同一の組み合わせがあると判断する。そして、送信部1809が、判断結果を子プロセス1830-1に送信する。つぎに、たとえば、受信部1834-1は、親プロセス1800から判断結果を受信する。判断部1835-1は、判断結果が子プロセス1830-1から送信された組み合わせと同一の組み合わせが基本実行パターンに関連付けられた組み合わせであるか否かを判断する。たとえば、検出部1837-1が、判断部1835-1により判断結果が基本実行パターンに関連付けられた組み合わせである場合、シミュレーション1903を継続し、あらたなCDCジッタを検出する。そして、たとえば、制御部1836-1は、検出部1837-1があらたなCDCジッタを一定時間以内に検出しなければ、シミュレーション1903の実行を終了させる。具体的には、制御部1836-1は、判断部1835-1による判断後、タイムアウト時刻を設定する。そして、制御部1836-1は、検出部1837-1がタイムアウト時刻までにあらたなCDCジッタを検出しなければ、実行部1831-1を制御することで、シミュレーション1903を終了させる。ここで、判断部1835-1による判断時のシミュレーション時刻からタイムアウト時刻までの時間は、たとえば、メモリイメージを複製するのにかかる時間程度とする。これにより、メモリイメージを複製するのにかかる時間よりも長い時間に渡って、CDCジッタが検出されない場合、親プロセス1800のシミュレーション1901の実行を再開させた方が、複数のシミュレーションの合計時間が短くなる。メモリイメージを複製するのにかかる時間は検証対象回路の回路規模や入力パターンにもよるので、該時間は固定値ではない。そのため、検証者がタイムアウト時刻を定めることとしてもよい。図19の例では、検出部1837-1が、18クロック目でCDCジッタJ4を検出する。そして、検出部1837-1が、検出したCDCジッタJ4の論理値を反転させた反転実行パターンに関するシミュレーションが実行済か否かを判断する。図19の例では、CDCジッタJ4の論理値を反転させた反転実行パターンに関するシミュレーションが実行されていない。そこで、設定部1838-1は、シミュレーション1903の実行状態のうち、CDCジッタJ4を出力する素子の出力を、検出部1837-1による検出時の論理値と異なる論理値に設定する。そして、実行部1831-1が、設定部1838-1による設定後の実行状態に基づいてシミュレーション1903を実行する。これにより、つづきのシミュレーション1903では、実行パターンP4=J1,J2,J3,J4,J5=1,0,0,1,0となる。また、図19では、子プロセス1830-2が、実行パターンP2=J1,J2,J3,J4,J5=1,1,0,0,0と実行パターンP5=J1,J2,J3,J4,J5=1,0,0,0,1に関するシミュレーション1904を実行する。また、図19の例では、子プロセス1830-3が、実行パターンP3に関してシミュレーション1905を実行する。たとえば、判断部1835-3が、受信部1834-3により受信された判断結果が、送信部1833-3により送信された組み合わせが、基本実行パターンでない他の実行パターンの組み合わせと同一であることを示すか否かを判断する。判断部1835-3により判断結果が、組み合わせが基本実行パターンでない他の実行パターンの組み合わせと同一であることを示すと判断された場合、制御部1836-3は実行部1831-3を制御して、シミュレーション1905を終了する。基本実行パターンでなく他の実行パターンに関する実行済のシミュレーションと実行中のシミュレーションとが同一のシミュレーション時刻で同一状態となれば、以降のシミュレーションも同一となる。そのため、以降のシミュレーションで発生するCDCジッタも実行済のシミュレーションで検出されている可能性が高いため、実行中のシミュレーションを終了させる。これにより、シミュレーション時間を短縮させることができる。実施の形態2にかかる検証支援装置700が行う処理手順図20および図21は、実施の形態2にかかる検証支援装置700の親プロセス1800が行う処理手順を示すフローチャートである。まず、親プロセス1800が、シミュレーションの実行を開始しステップS2001、シミュレーションが終了したか否かを判断するステップS2002。親プロセス1800が、シミュレーションが終了していないと判断した場合ステップS2002:No、シミュレーションを1ステップ実行するステップS2003。そして、親プロセス1800が、ハッシュ値を算出しステップS2004、シミュレーション時刻とハッシュ値の組み合わせに基本実行パターンを関連付けて出力するステップS2005。親プロセス1800が、CDCジッタの発生を検出したか否かを判断するステップS2006。親プロセス1800が、CDCジッタの発生を検出していないと判断した場合ステップS2006:No、ステップS2002へ戻る。つぎに、親プロセス1800が、CDCジッタの発生を検出したと判断した場合ステップS2006:Yes、基本実行パターンを実行済か否かを判断するステップS2007。親プロセス1800が、基本実行パターンを実行済でないと判断した場合ステップS2007:No、シミュレーションの実行状態を複製するステップS2008。そして、親プロセス1800が、複製したシミュレーションの実行状態を子プロセス1820の実行状態に指定して子プロセス1820を起動するステップS2009。つぎに、親プロセス1800が、基本実行パターンを実行する子プロセス1820が終了したか否かを判断するステップS2010。つぎに、親プロセス1800が、基本実行パターンを実行する子プロセス1820が終了していないと判断した場合ステップS2010:No、子プロセス1820から、シミュレーション時刻とハッシュ値の組み合わせを受信するステップS2011。そして、親プロセス1800が、シミュレーション時刻とハッシュ値の組み合わせを基本実行パターンに関連付けて出力しステップS2012、ステップS2010へ戻る。また、ステップS2007において、親プロセス1800が、基本実行パターンを実行済であると判断した場合ステップS2007:Yes、ステップS2013へ移行する。ステップS2010において、親プロセス1800が、基本実行パターンを実行する子プロセス1820が終了したと判断した場合ステップS2010:Yes、ステップS2013へ移行する。そして、親プロセス1800が、検出したCDCジッタに関する反転パターンを実行済か否かを判断するステップS2013。そして、親プロセス1800が、検出したCDCジッタに関する反転パターンを実行済でないと判断した場合ステップS2013:No、シミュレーションの実行状態を複製するステップS2014。つぎに、親プロセス1800が、複製した実行状態のうちのCDCジッタを出力する素子の出力を、検出時の出力値と異なる論理値に設定するステップS2015。そして、親プロセス1800が、複製したシミュレーションの実行状態を子プロセス1830-jの実行状態に指定して子プロセス1830-jを起動するステップS2016。つぎに、親プロセス1800が、子プロセス1830-jが終了したか否かを判断するステップS2017。そして、親プロセス1800が、子プロセス1830-jが終了していないと判断した場合ステップS2017:No、子プロセス1830-jから、シミュレーション時刻とハッシュ値の組み合わせを受信するステップS2018。つぎに、親プロセス1800が、受信した組み合わせが基本実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したか否かを判断するステップS2019。つぎに、親プロセス1800が、基本実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致していないと判断した場合ステップS2019:No、ステップS2020へ移行する。親プロセス1800が、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したか否かを判断するステップS2020。親プロセス1800が、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致していないと判断した場合ステップS2020:No、受信したシミュレーション時刻とハッシュ値の組み合わせに実行パターンを関連付けて出力するステップS2021。そして、親プロセス1800が、いずれにも一致しない旨を子プロセス1830-jに送信しステップS2022、ステップS2017へ移行する。ステップS2019において、親プロセス1800が、受信した組み合わせが基本実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したと判断した場合ステップS2019:Yes、ステップS2023へ移行する。そして、親プロセス1800が、基本実行パターンと一致した旨を子プロセスに送信しステップS2023、ステップS2017へ戻る。ステップS2020において、親プロセス1800が、受信した組み合わせが他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したと判断した場合ステップS2020:Yes、他の実行パターンと一致した旨を子プロセス1830-jに送信しステップS2024、ステップS2017へ戻る。また、ステップS2013において、親プロセス1800が、検出したCDCジッタに関する反転パターンを実行済であると判断した場合ステップS2013:Yes、ステップS2002へ戻る。また、ステップS2017において、親プロセス1800が、子プロセス1830-jが終了したと判断した場合ステップS2017:Yes、ステップS2002へ戻る。ステップS2002において、親プロセス1800が、シミュレーションが終了したと判断した場合ステップS2002:Yes、一連の処理を終了する。図22は、実施の形態2にかかる検証支援装置700の基本実行パターンを実行する子プロセス1820が行う処理手順を示すフローチャートである。基本実行パターンを実行する子プロセス1820が、設定後の実行状態に基づいてシミュレーションの実行を開始しステップS2201、シミュレーションが終了したか否かを判断するステップS2202。子プロセス1820が、シミュレーションが終了していないと判断した場合ステップS2202:No、次のサンプリング時刻までのシミュレーションを実行するステップS2203。子プロセス1820が、ハッシュ値を算出しステップS2204、シミュレーション時刻と、ハッシュ値の組み合わせを親プロセス1800に送信しステップS2205、ステップS2202へ戻る。ステップS2202において、子プロセス1820が、シミュレーションが終了したと判断した場合ステップS2202:Yes、一連の処理を終了する。図23および図24は、実施の形態2にかかる検証支援装置700の反転パターンを実行する子プロセス1830-jが行う処理手順を示すフローチャートである。まず、子プロセス1830-jが、設定後の実行状態に基づいてシミュレーションの実行を開始するステップS2301。そして、子プロセス1830-jが、シミュレーションが終了したか否かを判断するステップS2302。子プロセス1830-jが、シミュレーションが終了していないと判断した場合ステップS2302:No、次のサンプリング時刻までのシミュレーションを実行するステップS2303。子プロセス1830-jが、ハッシュ値を算出しステップS2304、シミュレーション時刻とハッシュ値の組み合わせを親プロセスに送信するステップS2305。子プロセス1830-jが、判断結果を受信しステップS2306、基本実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したか否かを判断するステップS2307。子プロセス1830-jが、基本実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致していないと判断した場合ステップS2307:No、ステップS2308へ移行する。子プロセス1830-jが、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したか否かを判断するステップS2308。子プロセス1830-jが、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致していないと判断した場合ステップS2308:No、ステップS2302に戻る。子プロセス1830-jが、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したと判断した場合ステップS2308:Yes、一連の処理を終了する。子プロセス1830-jが、他の実行パターンに関するシミュレーション時刻とハッシュ値の組み合わせと一致したと判断した場合ステップS2307:Yes、タイムアウト時刻を設定するステップS2309。子プロセス1830-jが、シミュレーションが終了したか、またはタイムアウトであるか否かを判断するステップS2310。子プロセス1830-jが、シミュレーションが終了していない、およびタイムアウトでないと判断した場合ステップS2310:No、シミュレーションを1ステップ実行するステップS2311。そして、子プロセス1830-jが、CDCジッタの発生を検出したか否かを判断するステップS2312。そして、子プロセス1830-jが、CDCジッタの発生を検出していないと判断した場合ステップS2312:No、ステップS2310へ戻る。そして、子プロセス1830-jが、CDCジッタの発生を検出したと判断した場合ステップS2312:Yes、検出したCDCジッタに関する反転パターンを実行済か否かを判断するステップS2313。つぎに、子プロセス1830-jが、検出したCDCジッタに関する反転パターンを実行済であると判断した場合ステップS2313:Yes、ステップS2310へ戻る。つぎに、子プロセス1830-jが、検出したCDCジッタに関する反転パターンを実行済でないと判断した場合ステップS2313:No、実行状態のうちのCDCジッタを出力する素子の出力を検出時の出力値と異なる論理値に設定するステップS2314。そして、子プロセス1830-jが、設定後の実行状態でシミュレーションを実行しステップS2315、ステップS2302へ戻る。また、ステップS2302において、子プロセス1830-jが、シミュレーションが終了したと判断した場合ステップS2302:Yes、一連の処理を終了する。また、子プロセス1830-jが、シミュレーションが終了した、またはタイムアウトであると判断した場合ステップS2310:Yes、一連の処理を終了する。実施の形態2によれば、基本実行パターンに関するシミュレーションの状態と現在実行中のシミュレーションの状態と、が同一シミュレーション時刻で一致したとしても、実行を継続して、他の実行パターンに関するシミュレーションとして再利用する。これにより、シミュレーションの起動に関する時間を短縮することができ、シミュレーション時間を短縮することができる。図25は、シミュレーションに要した時間の一例を示す説明図である。図25では、ある検証対象回路の回路情報にある入力パターンを与えた場合における、図6に示すような基準実行パターンから各CDCジッタの論理値を順に変更させたすべてのシミュレーション結果を得るのに要した時間を示している。図25の例では、CDCジッタの発生回数が、376199の場合に、従来の逐次処理でシミュレーションされた場合、シミュレーションに700時間要し、実施の形態1の検証支援処理でシミュレーションされた場合、シミュレーションに8時間要する。そして、実施の形態2の検証支援処理でシミュレーションされた場合、シミュレーションに7分要する。検証対象回路や入力パターンにもよるが、実施の形態1や実施の形態2によるシミュレーション時間を短縮することができる。以上説明した実施の形態1によれば、検証支援装置が、第1のシミュレーションを実行中にCDCジッタを検出し、検出時のCDCジッタの論理値と異なる論理値での第2のシミュレーションを、第1のシミュレーションと排他的に実行する。これにより、CDCジッタの発生までの第1,2のシミュレーションで重複するシミュレーションを省け、シミュレーション時間の短縮化を図ることができる。また、シミュレーションモデルに検証支援装置の機能を加えればよく、汎用の論理シミュレータを用いてシミュレーションを行うことができる。また、検証支援装置が、第2のシミュレーションの実行終了後の第1のシミュレーションの実行中にあらたにCDCジッタを検出した場合、検出時のCDCジッタの論理値と異なる論理値での第3のシミュレーションを、第1のシミュレーションと排他的に実行する。そして、検証支援装置が、第3のシミュレーションの実行中に、所定の素子の状態が、第2のシミュレーションと第3のシミュレーションの同一シミュレーション時刻で一致する場合には、第3のシミュレーションを終了させる。これにより、第2のシミュレーションと第3のシミュレーションで重複する実行を省略することができ、シミュレーション時間の短縮化を図ることができる。以上説明した実施の形態2によれば、検証支援装置が、所定の素子の状態が、実行済の第1のシミュレーションと実行中の第2のシミュレーションとで、同一時刻で同一となっても、第2のシミュレーションを止めずに、他の実行パターンに再利用する。これにより、実行状態の複製にかかる時間と論理値の設定にかかる時間とのシミュレーションの起動にかかる時間を省略することで、シミュレーション時間を短縮することができる。また、シミュレーションモデルに検証支援装置の機能を加えればよく、汎用の論理シミュレータを用いてシミュレーションを行うことができる。また、所定時間以上たっても、あらたなCDCジッタが検出されない場合には、第2のシミュレーションを終了させることで、第1のシミュレーションの続きを実行でき、シミュレーション時間を短縮することができる。なお、本実施の形態で説明した検証支援方法は、あらかじめ用意されたプログラムをパーソナルコンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、CD-ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムは、インターネット等のネットワークを介して配布してもよい。"