"第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出する検出手段と、前記検出手段により前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定する設定手段と、前記設定手段による設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較する比較手段と、前記比較手段による比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定する特定手段と、を備えることを特徴とする検証支援装置。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得する取得手段と、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記取得手段により取得されたシミュレーション結果時の論理値と異なる論理値に設定する設定手段と、前記設定手段による設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較する比較手段と、前記比較手段による比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定する特定手段と、を備えることを特徴とする検証支援装置。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出する検出手段と、前記検出手段により前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行する実行手段と、前記実行手段による実行結果を出力する出力手段と、を備えることを特徴とする検証装置。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出し、前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定する、処理をコンピュータに実行させることを特徴とする検証支援プログラム。第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得し、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、取得されたシミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較し、比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定する処理をコンピュータに実行させることを特徴とする検証支援プログラム。第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出し、前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行し、実行結果を出力する処理をコンピュータに実行させることを特徴とする検証プログラム。コンピュータによって実行される検証支援方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出し、前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定することを特徴とする検証支援方法。コンピュータによって実行される検証支援方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得し、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、取得されたシミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較し、比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定することを特徴とする検証支援方法。コンピュータによって実行される検証方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出し、前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行し、実行結果を出力することを特徴とする検証方法。CDCシミュレーションにおいてのエラー要因はCDC箇所である。CDC箇所とは、第1のクロックドメインのFFから第2のクロックドメインのFFにデータが受け渡されている箇所である。エラー要因箇所からエラー判定箇所までには、複数のFFや組み合わせ回路などがあるため、距離が離れており、かつ出力されるまでに時間がかかる。たとえば、すべてのCDCジッタの組み合わせを網羅するためには、2^CDCジッタ数^は乗数を示す通りのシミュレーションを実行させなければならず、シミュレーションに時間がかかるという問題点があった。さらに、すべてのCDCジッタの組み合わせをシミュレーションしない場合には、検証者が手作業で出バックしながら任意に選んだCDCジッタの組み合わせのみをシミュレーションするため、エラー要因の分析に時間がかかるという問題点がある。従来では、出力端子やCDCモデルの後段の観測点にCDCジッタの影響があるか否かが判断されていたが、該観測点を後段に設定すると、上流に多くのCDC箇所を持つこととなる。すなわち、どのCDC箇所のテストになっているかを判別することができないという問題点がある。1つの側面では、本発明は、CDCジッタによるエラー要因の特定を容易化することができる検証支援装置、検証支援プログラム、および検証支援方法を提供することを目的とする。また、他の側面では、本発明は、上述した従来技術による問題点を解消するため、シミュレーション回数を減少させることで、検証時間を短縮することができる検証装置、検証プログラム、および検証方法を提供することを目的とする。本発明の一の観点によれば、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出し、前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定する特定する検証支援装置、検証支援プログラム、および検証支援方法が提供される。本発明の他の観点によれば、第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得し、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、取得されたシミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較し、比較結果に基づいて前記一部の出力値の影響が前記観測点に伝播されているか否かを特定する検証支援装置、検証支援プログラム、および検証支援方法が提供される。本発明の他の観点によれば、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出し、前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行し、実行結果を出力する検証装置、検証プログラム、および検証方法が提供される。本検証支援装置、検証支援プログラム、および検証支援方法によれば、CDCジッタによるエラー要因の特定を容易化することができる。また、本検証装置、検証プログラム、および検証方法によれば、シミュレーション回数を減少させることで、検証時間を短縮することができる。つぎに、本発明にかかる検証支援装置、検証支援プログラム、および検証支援方法の好適な実施の形態1~実施の形態3を詳細に説明する。実施の形態1~3では、エラー要因分析が自動化される例について示す。さらに、本発明にかかる検証装置、検証プログラム、および検証方法の好適な実施の形態4を詳細に説明する。実施の形態4では、実施の形態1~3におけるシミュレーションを容易化するシミュレータについて示す。実施の形態1では、所定の入力パターンを用いたCDCシミュレーションにおいて、期待値と一致しないCDCジッタの論理値の組み合わせを用いて、いずれのCDCジッタでエラーが発生しているのかを特定する例について説明する。実施の形態2では、あるCDCジッタの出力値を、所定入力パターンでCDCシミュレーションしたシミュレーション結果時のCDCジッタの論理値と異なる論理値に設定する。そして、実施の形態2では、該シミュレーション結果と設定後でのシミュレーション結果とに基づき所定入力パターンにおいて各CDCジッタの影響が観測点まで伝播されているかを特定する。実施の形態3では、CDCジッタがN個の場合、2N2回のシミュレーションによって、どの3個のCDCジッタが選択されても、該選択された3個のCDCジッタの論理値の組み合わせが網羅される例について説明する。実施の形態4では、実施の形態1~3で示した1ビットだけ異なる複数の実行パターンのシミュレーションにおいて、共通部分を再シミュレーションさせることなく、該複数の実行パターンに関するシミュレーション結果が得られるシミュレーション例を示す。実施の形態1図1は、実施の形態1の一の例を示す説明図である。図1で示す検証対象回路の回路情報は、第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有している。検証支援装置は、回路情報に入力パターンを与えた1回目の観測点のシミュレーション結果と期待値との不一致を検出する。非同期で信号を受信する第2のクロックドメイン内のCDCモデルに置き換えられたFFは入力パターンに応じたタイミングでCDCジッタを出力する。図1中J1~J4がCDCジッタである。検証支援装置は、CDCジッタ群J1~J4のうちの一部のCDCジッタを1回目のシミュレーション結果時の論理値と異なる論理値に設定する。1回目のシミュレーションではJ1,J2,J3,J4が0,1,0,1であるため、2回目のシミュレーションでは、J1とJ2を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、2回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を1,0,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を1,0,0,1に設定後での観測点のシミュレーション結果2回目のシミュレーション結果と期待値とを比較する。2回目のシミュレーション結果と期待値とは同一値である。すなわち、J1とJ2が変更されると、シミュレーション結果に変化が生じる。よって、検証支援装置が、J1とJ2のうちのいずれか一方のCDCジッタ、またはJ1とJ2との2個のCDCジッタがエラー要因であることを特定する。つぎに、3回目のシミュレーションでは、J3とJ4を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、3回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を0,1,1,0に設定する。そして、検証支援装置は、J1,J2,J3,J4を0,1,1,0に設定後での観測点のシミュレーション結果3回目のシミュレーション結果と期待値とを比較する。3回目のシミュレーション結果と期待値とは不一致である。そして、検証支援装置は、3回目のシミュレーション結果と1回目のシミュレーション結果とを比較する。3回目のシミュレーション結果と1回目のシミュレーション結果とが一致している。すなわち、J3とJ4が変更されても、シミュレーション結果に変化が生じない。よって、検証支援装置が、J3とJ4との2個のCDCジッタはエラー要因でないことを特定する。図2は、実施の形態1の他の例を示す説明図である。図2で示す検証対象回路の回路情報は、第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有している。検証支援装置は、回路情報に入力パターンを与えた1回目の観測点のシミュレーション結果と期待値との不一致を検出する。非同期で信号を受信する第2のクロックドメイン内のCDCモデルに置き換えられたFFは入力パターンに応じたタイミングでCDCジッタを出力する。図中J1~J4がCDCジッタである。検証支援装置は、CDCジッタ群J1~J4のうちの任意の1個のCDCジッタを1回目のシミュレーション結果時の論理値と異なる論理値に設定する。1回目のシミュレーションではJ1,J2,J3,J4が0,1,0,1であるため、2回目のシミュレーションでは、J1を1回目のシミュレーション結果時の論理値と異なる論理値に設定する。すなわち、2回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を1,1,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を1,1,0,1に設定後での観測点のシミュレーション結果2回目のシミュレーション結果と期待値とを比較する。2回目のシミュレーション結果と期待値とは同一値である。すなわち、2回目のシミュレーション結果と1回目のシミュレーション結果が異なるため、J1が変更されると、シミュレーション結果に変化が生じる。よって、検証支援装置が、J1がエラー要因であることを特定する。つぎに、3回目のシミュレーションでは、J2を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、3回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を0,0,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を0,0,0,1に設定後での観測点のシミュレーション結果3回目のシミュレーション結果と期待値とを比較する。3回目のシミュレーション結果と期待値とは不一致である。そして、検証支援装置は、3回目のシミュレーション結果と1回目のシミュレーション結果とを比較する。3回目のシミュレーション結果と1回目のシミュレーション結果とが一致している。すなわち、1回目のシミュレーションと3回目のシミュレーションとでは同一エラーが発生しており、J2が変更されても、シミュレーションに変化が生じない。よって、検証支援装置が、J2はエラー要因でないことを特定する。つぎに、4回目のシミュレーションでは、J3を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、4回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を0,1,1,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を0,1,1,1に設定後での観測点のシミュレーション結果4回目のシミュレーション結果と期待値とを比較する。4回目のシミュレーション結果と期待値とは不一致である。そして、検証支援装置は、4回目のシミュレーション結果と1回目のシミュレーション結果とを比較する。4回目のシミュレーション結果と1回目のシミュレーション結果とは不一致である。すなわち、1回目のシミュレーションと4回目のシミュレーションとでは異なるエラーが発生しており、J3が変更されると、シミュレーションに変化が生じる。よって、検証支援装置が、J3はエラー要因であることを特定する。検証支援装置のハードウェア図3は、実施の形態1にかかる検証支援装置のハードウェアを示すブロック図である。図3において、検証支援装置300は、CPUCentralProcessingUnit301と、ROMRead‐OnlyMemory302と、RAMRandomAccessMemory303と、磁気ディスクドライブ304と、磁気ディスク305と、光ディスクドライブ306と、光ディスク307と、ディスプレイ308と、I/FInterface309と、キーボード310と、マウス311と、スキャナ312と、プリンタ313と、を備えている。また、各部はバス315によってそれぞれ接続されている。ここで、CPU301は、検証支援装置300の全体の制御を司る。ROM302は、ブートプログラムなどのプログラムを記憶している。RAM303は、CPU301のワークエリアとして使用される。磁気ディスクドライブ304は、CPU301の制御にしたがって磁気ディスク305に対するデータのリード/ライトを制御する。磁気ディスク305は、磁気ディスクドライブ304の制御で書き込まれたデータを記憶する。光ディスクドライブ306は、CPU301の制御にしたがって光ディスク307に対するデータのリード/ライトを制御する。光ディスク307は、光ディスクドライブ306の制御で書き込まれたデータを記憶したり、光ディスク307に記憶されたデータをコンピュータに読み取らせたりする。ディスプレイ308は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ308は、たとえば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。I/F309は、通信回線を通じてLANLocalAreaNetwork、WANWideAreaNetwork、インターネットなどのネットワーク314に接続され、このネットワーク314を介して他の装置に接続される。そして、I/F309は、ネットワーク314と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F309には、たとえばモデムやLANアダプタなどを採用することができる。キーボード310は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス311は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ312は、画像を光学的に読み取り、検証支援装置300内に画像データを取り込む。なお、スキャナ312は、OCROpticalCharacterreader機能を持たせてもよい。また、プリンタ313は、画像データや文書データを印刷する。プリンタ313には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。検証支援装置300の機能ブロック図図4は、検証支援装置300の機能ブロック図である。検証支援装置300は、検出部401と、設定部402と、比較部403と、特定部404と、を有している。検出部401から特定部404は、たとえば、後述のテストベンチ500内にコーディングされていることとする。検出部401は、第1のクロックドメインと、第1のクロックドメインから非同期で信号CDC信号を受信する第2のクロックドメインと、を有する回路情報に、所定入力パターンが与えられた第1のシミュレーション結果と期待値との不一致を検出する。設定部402は、検出部401により不一致が検出された場合、CDC信号を受信する第2のクロックドメイン内のFFの出力であるCDCジッタ群のうちの一部のCDCジッタを、第1のシミュレーション結果時の論理値と異なる論理値に設定する。比較部403は、設定部402による設定後の第2のシミュレーション結果と期待値とを比較する。特定部404は、比較部403による比較結果に基づいて、一部のCDCジッタが不一致の要因であるか否かを特定する。具体的には、特定部404は、比較部403による第2のシミュレーション結果と期待値との比較結果と、第1のシミュレーション結果と期待値との比較結果と、が同一である場合、一部のCDCジッタが不一致の要因でないことを特定する。特定部404は、比較部403による第2のシミュレーション結果と期待値とが同一である場合、一部のCDCジッタに不一致の要因が含まれることを特定する。また、設定部402は、CDCジッタ群のうち、任意の1個のCDCジッタをシミュレーション結果時の論理値と異なる論理値に設定する。そして、比較部403は、設定部402による設定後の第2のシミュレーション結果と期待値とを比較する。そして、特定部404は、比較部403により第2のシミュレーション結果と期待値とが一致すると判断された場合、任意の1個のCDCジッタが不一致の要因であることを特定する。図5は、テストベンチ500の一例を示す説明図である。テストベンチ500は、検証対象回路の回路情報501と、入力パターン発生器502と、エラー検出器503と、を有している。さらに、回路情報501は、第1のクロックドメイン510と、第1のクロックドメイン510から非同期で信号を受け渡される第2のクロックドメイン511とを有している。テストベンチ500は論理シミュレータによってシミュレーションされる。論理シミュレータによりテストベンチ500がシミュレーションを開始すると、入力パターン発生器502が入力パターンを発生し、回路情報501に入力パターンが与えられて、該入力パターンに沿って回路情報501がシミュレーションされる。回路情報501から検証に必要な信号がシミュレーション結果として出力される。そして、エラー検出器503がシミュレーション結果と期待値とを比較することにより、エラーを検出する。テストベンチ500の各部は、具体的には、たとえば、ハードウェア記述言語で記述されている。テストベンチ500は、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶されている。実施の形態1では、検証支援装置300の検出部401~特定部404はテストベンチ500内の入力パターン発生器502やエラー検出器503内にコーディングされているとする。具体的には、たとえば、CPU301が、記憶装置からテストベンチ500を読み出す。そして、CPU301が、論理シミュレータを実行し、読み出したテストベンチ500をシミュレーションすることにより、入力パターン発生器502やエラー検出器503にコーディングされた検出部401~特定部404の処理が実行される。図6は、回路情報501内の第2のクロックドメイン511の一例を示す説明図である。第2のクロックドメイン511では、enableの値が1となったときのdata_inの値を保持する。そして、第2のクロックドメイン511では、該保持したdata_inの値をreadの値が1になったときに、data_outの値として出力する。enableとdata_inとreadとのうち、enableとdata_inとが第1のクロックドメイン510から第2のクロックドメイン511へ非同期で受け渡される信号である。第2のクロックドメイン511は、CDCモデル601と、CDCモデル602と、FF603と、FF604と、選択回路605と、FF606と、AND回路607と、を有している。CDCモデルの出力がAである。CDCモデル601は、enableの入力タイミングとSEL0の入力値に沿ってCDCジッタが出力される。CDCモデル602の出力がBであり、data_inの入力タイミングとSEL0の入力値に沿って、CDCジッタが出力される。FF603の入力はAであり、FF603の出力はCであり、FF603はCLK2の立ち上がり時にAの値を取り込む。FF604の入力はBであり、FF604の出力はDであり、FF604はCLK2の立ち上がり時にBの値を取り込む。選択回路605の入力はDとFとCとであり、選択回路605の出力はEである。選択回路605は、Cの値に沿ってDまたはFの値を出力する。具体的には、選択回路605は、Cの値が1の場合にDの値を出力し、Cの値が0の場合にFの値を出力する。FF606の入力はEであり、FF606の出力はFであり、FF606はCLK2の立ち上がり時にEの値を取り込む。AND回路607の出力がdata_outであり、Fの値とreadの値に沿ってAND回路607から0または1が出力される。data_outは出力端子である。実施の形態1では、enableの値と、data_inの値と、readの値と、A~Fのそれぞれの値と、data_outの値と、がシミュレーション結果として保持される。図7は、実施の形態1で用いるCDCモデルの一例を示す説明図である。CDCモデル700では、入力信号に応じて、1サイクル分のランダムな論理値CDCジッタを出力することで、メタステーブル状態を再現する。CDCモデル700は、JitterDetector701と、FF702と、FF703と、選択回路704と、選択回路705と、を有している。JitterDetector701は、CDCモデル700への入力信号INの値の変化を検出し、該変化の検出時から一定時間経過するまで1を出力する。FF702はCLK2の立ち上がり時のJitterDetector701の出力値を保持して、該保持した値を選択回路704へ出力する。たとえば、CLK2の立ち上がり時に、JitterDetector701が1を出力すれば、FF702が選択回路704へ1を出力する。たとえば、CLK2の立ち上がり時に、JitterDetector701が0を出力すれば、選択回路704はFF703の出力値を出力する。FF703は、CLK2の立ち上がり時にINの値を保持し、該保持した値を選択回路704へ出力する。選択回路704は、FF702の出力値が0であれば、FF703の出力値を出力し、FF702の出力値が1であれば、選択回路705の出力値が出力される。選択回路705は、SEL[1:0]への入力値が002進数であれば、randomランダム値を出力する。選択回路705は、SEL[1:0]への入力値が012進数であれば、0を出力する。選択回路705は、SEL[1:0]への入力値が102進数であれば、1を出力する。実施の形態1では、たとえば、入力パターン発生器502が各CDCモデル700からCDCジッタが出力されるタイミングに沿って、SELへの入力値を制御することにより、CDCジッタの論理値を設定することができる。図7で示すCDCモデル700は、たとえば、ライブラリとしてRAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶されている。回路情報501では、該ライブラリ内に記憶された該CDCモデル700を指定する。論理シミュレータが該ライブラリからCDCモデル700を読み出して、CDCモデル700に記述された処理を実行する。図8は、JitterDetectorの一例を示す説明図である。JitterDetector800701では、入力であるTが0から1または1から0に変化すると、出力であるEはPERIOD分の時間が経過するまで1となる。JitterDetector800701は、たとえば、ライブラリとしてRAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶されている。回路情報501では、該ライブラリ内に記憶されたJitterDetector800701を指定する。論理シミュレータは、該ライブラリからJitterDetector800701に記述された処理を読み出して、JitterDetector800701に記述された処理を実行する。図9は、入力パターン1を示す説明図である。図9では、CLK2の立ち上がりから次の立ち上がりの直前までを1周期として、CLK2の上に0~10まで順に番号を付している。たとえば、1クロック目の立ち上がりとは、図中0と1との番号の間のCLK2の立ち上がりを示している。1クロック目の立ち上がりと3クロック目の立ち上がりで、CLK2に対して、enableとdata_inとがデータセットアップを違反している。入力パターン1においては、1クロック目と3クロック目とのそれぞれの期間で、AとBとの出力がCDCジッタとなる。入力パターン1においては、1クロック目のAのCDCジッタをJ1とし、1クロック目のBのCDCジッタをJ2とし、3クロック目のAのCDCジッタをJ3とし、3クロック目のBのCDCジッタをJ4とする。8クロック目で、readが1となると、data_outが1を出力する。テストベンチ500へ入力パターンを与えると、J1~J4の組み合わせによって、2^4^は乗数を示す。通りの実行パターンが得られる。実行パターンの組み合わせについては、P=J1,J2,J3,J4で示す。ここで、たとえば、論理シミュレータがテストベンチ500をシミュレーションすると、CDCジッタはランダム値となり、P0=0,1,1,0となったとする。また、以下に示す詳細例では、検証支援装置300がJ1~J4のうちの1個のCDCジッタを順に選択する。そして、検証支援装置300が該選択したCDCジッタの論理値をP0と異なる論理値に設定する例を示す。図10は、P0でのシミュレーション結果例を示す説明図である。たとえば、検証支援装置300が、検出部401により、data_outにおける期待値と、P0=0,1,1,0でのdata_outにおけるシミュレーション結果とを比較する。data_outが8クロック目に1でないため、検証支援装置300が、検出部401により、P0でのシミュレーション結果と、期待値とが一致しないことを検出する。つぎに、検証支援装置300が、J1~J4から、順にCDCジッタを選択する。まず、J1が選択されることとする。検証支援装置300が、設定部402により、あらたな実行パターンのJ1の論理値をP0でのJ1の論理値と異なる論理値に設定する。ここで、設定されたあらたな実行パターンがP1=1,1,1,0である。具体的には、たとえば、入力パターン発生器502が1クロック目のAの値が1となるように、1クロック目にSEL0に102進数を与え、1クロック目のBの値が1となるように、1クロック目にSEL1に102進数を与える。入力パターン発生器502が3クロック目のAの値が1となるように、3クロック目にSEL0に102進数を与え、3クロック目のBの値が0となるように、3クロック目にSEL1に012進数を与える。図11は、P1でのシミュレーション結果例を示す説明図である。検証支援装置300が、比較部403により、data_outの期待値と、P1でのdata_outのシミュレーション結果とを比較する。data_outが8クロック目に1を出力しないため、検証支援装置300が、P0と同様に、P1でもエラーが発生すると判断する。検証支援装置300は、特定部404により、J1の論理値の変化によって、シミュレーション結果に変化が発生しないため、J1がエラー要因でないことを特定する。つぎに、検証支援装置300が、J2~J4からJ2を選択する。検証支援装置300が、設定部402により、あらたな実行パターンのJ2の論理値をP0でのJ2の論理値と異なる論理値に設定する。ここで、設定されたあらたな実行パターンがP2=0,0,1,0である。具体的には、たとえば、入力パターン発生器502が、1クロック目のAの値が0となるように、1クロック目にSEL0に012進数を与え、1クロック目のBの値が0となるように、1クロック目にSEL1に012進数を与える。入力パターン発生器502が3クロック目のAの値が1となるように、3クロック目にSEL0に102進数を与え、3クロック目のBの値が0となるように、3クロック目にSEL1に012進数を与える。図12は、P2でのシミュレーション結果例を示す説明図である。検証支援装置300が、比較部403により、data_outの期待値と、P2でのdata_outのシミュレーション結果とを比較する。data_outが8クロック目に1を出力しないため、検証支援装置300が、P0と同様に、P2でもエラーが発生すると判断する。検証支援装置300は、特定部404により、J2の論理値の変化によって、シミュレーション結果に変化が発生しないため、J2がエラー要因でないことを特定する。つぎに、検証支援装置300が、J3~J4からJ3を選択する。検証支援装置300が、設定部402により、あらたな実行パターンのJ3の論理値をP0でのJ3の論理値と異なる論理値に設定する。ここで、設定されたあらたな実行パターンがP3=0,1,0,0である。具体的には、入力パターン発生器502が1クロック目のAの値に0が出力されるように、1クロック目にSEL0に012進数を与え、1クロック目のBの値が1となるように、1クロック目にSEL1に102進数を与える。入力パターン発生器502が3クロック目のAの値が0となるように、3クロック目にSEL0に012進数を与え、3クロック目のBの値が0となるように、3クロック目にSEL1に012進数を与える。図13は、P3でのシミュレーション結果例を示す説明図である。検証支援装置300が、比較部403により、data_outの期待値と、P3でのdata_outのシミュレーション結果と、を比較する。data_outが8クロック目に1を出力するため、検証支援装置300が、P3でのシミュレーション結果が期待値と一致すると判断する。検証支援装置300は、特定部404により、J3の論理値の変化によって、シミュレーション結果に変化が発生したため、J3をエラー要因に特定する。つぎに、検証支援装置300が、J4を選択する。検証支援装置300が、設定部402により、あらたな実行パターンのJ4の論理値をP0でのJ4の論理値と異なる論理値に設定する。ここで、設定されたあらたな実行パターンがP4=0,1,1,1である。具体的には、入力パターン発生器502が1クロック目のAの値0となるように、1クロック目にSEL0に012進数を与え、1クロック目のBの値が1となるように、1クロック目にSEL1に10を与える。入力パターン発生器502が3クロック目のAの値が1となるように、3クロック目にSEL0に102進数を与え、3クロック目のBの値が1となるように、3クロック目にSEL1に10を与える。図14は、P4でのシミュレーション結果例を示す説明図である。検証支援装置300が、比較部403により、data_outの期待値と、P4でのdata_outのシミュレーション結果と、を比較する。data_outが8クロック目に1を出力するため、検証支援装置300が、P4でのシミュレーション結果が期待値と一致すると判断する。検証支援装置300は、特定部404により、J4の論理値の変化によって、シミュレーション結果に変化が発生したため、J4をエラー要因に特定する。図15は、5つの実行パターン例を示す説明図である。表1500では、J1~J4の16通りの組み合わせと、実行パターンとが対応付けられている。P0=0,1,1,0:エラーP1=1,1,1,0:エラーP2=0,0,1,0:エラーP3=0,1,0,0:期待値と一致P4=0,1,1,1:期待値と一致したがって、複数のCDCジッタからJ3とJ4とがエラー要因であることを自動で特定できる。検証支援装置300による検証支援処理手順図16は、検証支援装置300による検証支援処理手順のフローチャートを示す説明図である。まず、検証支援装置300が、エラーが検出された実行パターンがあるか否かを判断するステップS1601。検証支援装置300が、エラーが検出された実行パターンがないと判断した場合ステップS1601:No、ステップS1601へ戻る。検証支援装置300が、エラーが検出された実行パターンがあると判断した場合ステップS1601:Yes、P0=エラーが検出された実行パターンとしステップS1602、n=P0の実行中に発生したCDCジッタの数としステップS1603、i=1とするステップS1604。検証支援装置300が、i>nであるか否かを判断するステップS1605。検証支援装置300が、i>nでないと判断した場合ステップS1605:No、Jii番目のCDCジッタに対する選択値のみがP0と異なっているPiに関するシミュレーションを実行するステップS1606。つぎに、検証支援装置300が、Piでのシミュレーション結果にP0でのシミュレーション結果と同一のエラーがあるか否かを判断するステップS1607。検証支援装置300が、Piでのシミュレーション結果にP0でのシミュレーション結果と同一のエラーがないと判断した場合ステップS1607:No、エラーはJiに関連していることを出力するステップS1608。そして、検証支援装置300が、i=i1としステップS1609、ステップS1605へ戻る。検証支援装置300が、Piでのシミュレーション結果にP0でのシミュレーション結果と同一のエラーがあると判断した場合ステップS1607:Yes、ステップS1609へ移行する。検証支援装置300が、i>nであると判断した場合ステップS1605:Yes、一連の処理を終了する。実施の形態2実施の形態2では、各CDCジッタの影響が観測点まで伝播しているか否かを検証する例について説明する。図17は、実施の形態2の一の例を示す説明図である。図2で示す検証対象回路の回路情報は、第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有している。非同期で信号を受信する第2のクロックドメイン内のCDCモデルに置き換えられたFFは入力パターンに応じたタイミングでCDCジッタを出力する。図中J1~J4がCDCジッタである。回路情報に入力パターンを与えた1回目の観測点のシミュレーションではJ1,J2,J3,J4が0,1,0,1である。つぎに、検証支援装置は、CDCジッタ群J1~J4のうちの一部のCDCジッタを1回目のシミュレーション結果時の論理値と異なる論理値に設定する。たとえば、2回目のシミュレーションでは、J1とJ2を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、2回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を1,0,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を1,0,0,1に設定後での観測点のシミュレーション結果2回目のシミュレーション結果と1回目のシミュレーション結果とを比較する。2回目のシミュレーション結果と1回目のシミュレーション結果とは不一致である。すなわち、J1およびJ2の論理値が変更されると、シミュレーション結果に変化が生じる。よって、検証支援装置が、J1とJ2のうちのいずれか一方のCDCジッタの影響が観測点に伝播されている、またはJ1とJ2との2個のCDCジッタの影響が観測点に伝播されていることを特定する。つぎに、3回目のシミュレーションでは、J3とJ4を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、3回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を0,1,1,0に設定する。そして、検証支援装置は、J1,J2,J3,J4を0,1,1,0に設定後での観測点のシミュレーション結果3回目のシミュレーション結果と1回目のシミュレーション結果とを比較する。3回目のシミュレーション結果と1回目のシミュレーション結果とは同一値である。すなわち、J3およびJ4の論理値が変更されても、シミュレーション結果に変化が生じない。よって、検証支援装置が、J3とJ4との2個のCDCジッタの影響が観測点まで伝播しないことを特定する。図18は、実施の形態2の他の例を示す説明図である。図18で示す検証対象回路の回路情報は、第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有している。非同期で信号を受信する第2のクロックドメイン内のCDCモデルに置き換えられたFFは入力パターンに応じたタイミングでCDCジッタを出力する。図18中J1~J4がCDCジッタである。回路情報に入力パターンを与えた1回目の観測点のシミュレーションではJ1,J2,J3,J4が0,1,0,1である。検証支援装置は、CDCジッタ群J1~J4のうちの任意の1個のCDCジッタを1回目のシミュレーション結果時の論理値と異なる論理値に設定する。1回目のシミュレーションではJ1,J2,J3,J4が0,1,0,1であるため、2回目のシミュレーションでは、J1を1回目のシミュレーション結果時の論理値と異なる論理値に設定する。すなわち、2回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を1,1,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を1,1,0,1に設定後での観測点のシミュレーション結果2回目のシミュレーション結果と観測点の1回目のシミュレーション結果とを比較する。2回目のシミュレーション結果と1回目のシミュレーション結果とは不一致である。すなわち、2回目のシミュレーション結果と1回目のシミュレーション結果が異なるため、J1が変更されると、シミュレーション結果に変化が生じる。よって、検証支援装置が、J1の影響が伝播されていると特定する。つぎに、3回目のシミュレーションでは、J2を1回目のシミュレーション結果時の論理値と異なる論理値とする。すなわち、3回目のシミュレーションでは、検証支援装置はJ1,J2,J3,J4を0,0,0,1に設定する。そして、検証支援装置は、J1,J2,J3,J4を0,0,0,1に設定後での観測点のシミュレーション結果3回目のシミュレーション結果と観測点の1回目のシミュレーション結果とを比較する。3回目のシミュレーション結果と1回目のシミュレーション結果とは同一値である。すなわち、J2の論理値が変更されても、シミュレーションに変化が生じない。よって、検証支援装置が、J2の影響は伝播されないと特定する。実施の形態2にかかる検証支援装置の機能ブロック図図19は、実施の形態2にかかる検証支援装置の機能ブロック図である。検証支援装置1900は、取得部1901と、選択部1902と、設定部1903と、比較部1904と、特定部1905と、を有している。取得部1901は、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた第1のシミュレーション結果を取得する。設定部1903は、信号を受信する第2のクロックドメイン内のFFが出力するCDCジッタ群のうちの一部のCDCジッタを、取得部1901により取得された第1のシミュレーション結果時の論理値と異なる論理値に設定する。比較部1904は、設定部1903による設定後での検証対象回路内の観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とを比較する。特定部1905は、比較部1904による比較結果に基づいて、一部のCDCジッタの影響が観測点に伝播されているか否かを特定する。特定部1905は、比較部1904によって設定後の第2のシミュレーション結果と第1のシミュレーション結果とが一致すると判断された場合、一部の出力値の影響は伝播されていないと特定する。また、特定部1905は、比較部1904によって設定後の第2のシミュレーション結果と第1のシミュレーション結果とが一致しないと判断された場合、一部のCDCジッタの中に、影響が観測点に伝播されている出力値が含まれていることを特定する。また、設定部1903は、CDCジッタ群のうちの任意の1個のCDCジッタをシミュレーション結果時の論理値と異なる論理値に設定する。比較部1904は、設定部1903による設定後での観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とを比較する。特定部1905は、比較部1904により観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とが一致しないと判断された場合、任意の1個のCDCジッタの影響が観測点に伝播されていることを特定する。また、選択部1902は、CDCジッタ群から1個のCDCジッタを順に選択する。そして、設定部1903は、CDCジッタ群のうち、選択部1902により選択される都度、選択された1個のCDCジッタを第1のシミュレーション結果時の論理値と異なる論理値に設定する。比較部1904は、選択された1個のCDCジッタごとに、設定部1903による設定後の観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とを比較する。特定部1905は、比較部1904により設定後の観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とが一致しないと判断された場合、選択された1個のCDCジッタの影響が観測点に伝播されていることを特定する。以上を踏まえて、詳細例を説明する。実施の形態2では、実施の形態1と同一の構成については同一符号を付し、その説明を省略する。また、実施の形態2では、検証支援装置1900の取得部1901~特定部1905は上述のテストベンチ500内の入力パターン発生器502やエラー検出器503内にコーディングされているとする。具体的には、たとえば、CPU301が、記憶装置からテストベンチ500を読み出す。そして、CPU301が、論理シミュレータを実行し、読み出したテストベンチ500をシミュレーションすることにより、入力パターン発生器502やエラー検出器503にコーディングされた取得部1901~特定部1905の処理が実行される。図20は、入力パターン2を示す説明図である。図20では、CLK2の立ち上がりから次の立ち上がりの直前までを1周期として、CLK2の上に0~10まで順に番号を付している。たとえば、1クロック目の立ち上がりとは、図中0と1との番号の間のCLK2の立ち上がりを示している。1クロック目の立ち上がりと3クロック目の立ち上がりで、CLK2に対して、enableとdata_inとがデータセットアップを違反している。よって、1クロック目と3クロック目とのそれぞれの期間で、AとBとがCDCジッタとなる。ここでは、1クロック目のAのCDCジッタをJ1とし、1クロック目のBのCDCジッタをJ2とし、3クロック目のAのCDCジッタをJ3とし、3クロック目のBのCDCジッタをJ4とする。4クロック目で、readが1となると、data_outが1を出力する。テストベンチ500へ入力パターンを与えると、J1~J4の組み合わせによって、2^4^は乗数を示す。通りの実行パターンが得られる。実行パターンの組み合わせについては、Q=J1,J2,J3,J4で示す。図21は、Q0でのシミュレーション結果を示す説明図である。CPUが、任意の実行パターンQ0を選択する。ここでは、Q0=1,0,1,1が選択される。そして、検証支援装置1900が、取得部1901により、Q0でのシミュレーション結果を取得する。具体的には、たとえば、検証支援装置1900が、論理シミュレータにQ0でのシミュレーションを実行させる。検証支援装置1900が、論理シミュレータによるシミュレーション結果を取得する。Q0でのシミュレーション結果では、図20で示したdata_outと同様に、data_outが4クロック目で1となる。検証支援装置1900が、選択部1902により、CDCジッタ群J1~J4から1個のCDCジッタを順に選択する。ここでは、まずJ1が選択されることとする。検証支援装置1900が、設定部1903により、選択されたJ1の論理値をQ0でのJ1の論理値と異なる論理値に設定する。ここで、特定のCDCジッタの論理値の変更方法は、実施の形態1と同様の方法によって変更可能であるため、実施の形態2では詳細な説明を省略する。そして、設定された実行パターンがQ1=0,0,1,1である。検証支援装置1900が、CDCジッタ群の各CDCジッタの論理値がQ1となるように論理シミュレータを用いてシミュレーションを実行する。図22は、Q1でのシミュレーション結果を示す説明図である。検証支援装置1900が、比較部1904により、Q1でのシミュレーション結果と、Q0でのシミュレーション結果とを比較する。いずれのシミュレーション結果も4クロック目でdata_outが1となるため、検証支援装置1900が、Q1でのシミュレーション結果とQ0でのシミュレーション結果とが同一であると判断する。そして、検証支援装置1900が、特定部1905により、J1の論理値の変化によって、シミュレーション結果に変化が発生したため、J1による影響がdata_outまで伝播されていないと特定する。つぎに、検証支援装置1900が、選択部1902により、CDCジッタ群J1~J4から、J2を選択する。検証支援装置1900が、設定部1903により、選択されたJ2の論理値をQ0でのJ2の論理値と異なる論理値に設定する。そして、設定された実行パターンがQ2=1,1,1,1である。検証支援装置1900が、CDCジッタ群の各CDCジッタの論理値がQ2となるようにシミュレーションを実行する。図23は、Q2でのシミュレーション結果を示す説明図である。検証支援装置1900が、比較部1904により、Q2でのシミュレーション結果と、Q0でのシミュレーション結果とを比較する。いずれのシミュレーション結果も4クロック目でdata_outが1となるため、検証支援装置1900が、Q2でのシミュレーション結果とQ0でのシミュレーション結果とが同一であると判断する。そして、検証支援装置1900が、特定部1905により、J2の論理値の変化によって、シミュレーション結果に変化が発生したため、J2による影響がdata_outまで伝播されていないと特定する。つぎに、検証支援装置1900が、選択部1902により、CDCジッタ群J1~J4から、J3を選択する。検証支援装置1900が、設定部1903により、選択されたJ3の論理値をQ0でのJ3の論理値と異なる論理値に設定する。そして、設定された実行パターンがQ3=1,0,0,1である。検証支援装置1900が、CDCジッタ群の各CDCジッタの論理値がQ3となるようにシミュレーションを実行する。図24は、Q3でのシミュレーション結果を示す説明図である。検証支援装置1900が、比較部1904により、Q3でのシミュレーション結果と、Q0でのシミュレーション結果とを比較する。いずれのシミュレーション結果も4クロック目でdata_outが1となるため、検証支援装置1900が、Q3でのシミュレーション結果とQ0でのシミュレーション結果とが同一であると判断する。そして、検証支援装置1900が、特定部1905により、J3の論理値の変化によって、シミュレーション結果に変化が発生したため、J3による影響がdata_outまで伝播されていないと特定する。つぎに、検証支援装置1900が、CDCジッタ群J1~J4からJ4を選択する。検証支援装置1900が、選択されたJ4の論理値をQ0でのJ4の論理値と異なる論理値に設定する。そして、設定された実行パターンがQ4=1,0,1,0である。検証支援装置1900が、CDCジッタ群の各CDCジッタの論理値がQ4となるようにシミュレーションを実行する。図25は、Q4でのシミュレーション結果を示す説明図である。検証支援装置1900が、Q4でのシミュレーション結果と、Q0でのシミュレーション結果とを比較する。いずれのシミュレーション結果も4クロック目でdata_outが1となるため、検証支援装置1900が、Q4でのシミュレーション結果とQ0でのシミュレーション結果とが同一であると判断する。そして、検証支援装置1900が、特定部1905により、J4の論理値の変化によって、シミュレーション結果に変化が発生したため、J4による影響がdata_outまで伝播されていないと特定する。図26は、Q0~Q4を示す説明図である。表2600では、J1~J4のすべての論理値の組み合わせが示されている。実施の形態2では、2のCDCジッタ数乗通りの組み合わせがあり、入力パターンにおいて、各CDCジッタの影響が観測点まで伝播されているか否かを特定するために、少ないシミュレーション回数で容易に特定することができる。実施の形態2における検証支援装置1900による検証支援処理手順図27は、実施の形態2における検証支援装置1900による検証支援処理手順の一例を示すフローチャートである。検証支援装置1900が、CDCシミュレーションを実行しステップS2701、Q0=実行した実行パターンとするステップS2702。検証支援装置1900が、n=Q0の実行中に発生したCDCジッタの数としステップS2703、i=1とするステップS2704。検証支援装置1900が、i>nであるか否かを判断しステップS2705、i>nでないと判断した場合ステップS2705:No、Jiの論理値がQ0と異なるQiを設定しステップS2706、Qiに関するシミュレーションを実行するステップS2707。検証支援装置1900が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致しているか否かを判断するステップS2708。検証支援装置1900が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致していないと判断した場合ステップS2708:No、Jiの影響が観測点まで伝播したことを出力するステップS2709。出力形式としては、たとえば、ディスプレイ308への表示、プリンタ313への印刷出力、I/F309による外部装置への送信がある。また、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶することとしてもよい。そして、検証支援装置1900が、i=i1としステップS2710、ステップS2705へ戻る。ステップS2708において、検証支援装置1900が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致していないと判断した場合ステップS2708:Yes、ステップS2705において、検証支援装置1900が、i>nであると判断した場合ステップS2705:Yes、一連の処理を終了する。実施の形態3実施の形態3では、どの3個のCDCジッタが選択されても、該選択された3個のCDCジッタの論理値の組み合わせが網羅されるシミュレーション例について説明する。CDCジッタは数千から数万個あるため、数千から数万個のCDCジッタの論理値の組み合わせを網羅するには、検証に時間がかかる。たとえば、CDCジッタが1000個あれば、2^1000^は乗数を示す。通りのCDCジッタの論理値の組み合わせがある。ある入力パターンにおいてCDCシミュレーションが行われた場合、エラー要因となるCDCジッタは2~3個程度であるが、数千から数万個のCDCジッタのうちのいずれのCDCジッタによる影響でエラーとなるかは不明確である。そこで、実施の形態3では、検証者がどの3個のCDCジッタを選択しても、該3個のCDCジッタの論理値の組み合わせだけを必ず検証することができ、検証時間を短縮化することができる。また、実施の形態3では、実施の形態1および実施の形態2と同一構成については同一符号とし、該同一構成に関する詳細な説明は省略する。さらに、実施の形態3における検証支援装置は、実施の形態2で示した検証支援装置1900と同一とする。ここでは、設定部1903から特定部1905において、実施の形態2と異なる動作のみ説明する。設定部1903は、選択部1902により選択される都度、さらに、CDCジッタ群のすべてのCDCジッタがシミュレーション結果時の論理値と異なる論理値から、CDCジッタ群のうちの選択部により選択された出力値のみが異なる論理値に設定する。比較部1904は、CDCジッタ群のすべてのCDCジッタがシミュレーション結果時の論理値と異なる論理値の場合のシミュレーション結果と、設定部1903による設定後のシミュレーション結果とを比較する。特定部1905は、比較部1904により設定後のシミュレーション結果とシミュレーション結果とが一致しないと判断された場合、選択された1個のCDCジッタの影響が観測点に伝播されていることを特定する。以上を踏まえて、詳細に説明する。図28は、Q0~Q4とQ0’~Q4’とを示す説明図である。表2800では、Q0~Q4とQ0’~Q4’とのそれぞれのJ1~J4の値を示している。Q0~Q4までは、実施の形態2で説明しているため、詳細な説明を省略する。検証支援装置が、設定部1903により、J1~J4のすべての論理値がQ0と異なる実行パターンを設定する。設定された実行パターンはQ0’=0,1,0,0である。そして、検証支援装置が、Q0’に関するシミュレーションを実行し、実行結果を出力する。さらに、検証支援装置が、J1~J4から順に1個のCDCジッタを選択する。そして、検証支援装置が、CDCジッタを選択する都度、あらたな実行パターンの選択したCDCジッタの論理値をQ0’で選択したCDCジッタの論理値と異なる論理値に設定する。そして、あらたな実行パターンがQ1’~Q4’である。そして、検証支援装置が、比較部1904により、あらたな各実行パターンでのシミュレーション結果と、Q0’でのシミュレーション結果とを比較し、特定部1905により、各CDCジッタの影響が伝播されているか否かを特定する。Q0~Q4とQ0’~Q4’との10の実行パターンがシミュレーションされることにより、J1~J4の中で、任意に選ばれた3個のCDCジッタの組み合わせにおいて、2の3乗の実行パターンをすべて網羅することができる。図29は、3個のCDCジッタの選択例を示す説明図である。図29では、J1~J4のうち、1J1,J2,J3が選択された例では、J1,J2,J3=0,0,0~1,1,1までのすべてのパターンが網羅されている。図29では、J1~J4のうち、2J1,J2,J4が選択された例では、J1,J2,J4=0,0,0~1,1,1までのすべてのパターンが網羅されている。図29では、J1~J4のうち、3J1,J3,J4が選択された例では、J1,J3,J4=0,0,0~1,1,1までのすべてのパターンが網羅されている。図29では、J1~J4のうち、4J2、J3、J4が選択された例では、J2,J3,J4=0,0,0~1,1,1までのすべてのパターンが網羅されている。実施の形態3における検証支援装置による検証支援処理手順図30,31は、実施の形態3における検証支援装置による検証支援処理手順の一例を示すフローチャートである。検証支援装置が、CDCシミュレーションを実行しステップS3001、Q0=実行した実行パターンとするステップS3002。検証支援装置が、n=Q0の実行中に発生したCDCジッタの数としステップS3003、i=1とするステップS3004。検証支援装置が、i>nであるか否かを判断しステップS3005、i>nでないと判断した場合ステップS3005:No、Jiの論理値がQ0と異なるQiを設定しステップS3006、Qiに関するシミュレーションを実行するステップS3007。検証支援装置が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致しているか否かを判断するステップS3008。検証支援装置が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致していないと判断した場合ステップS3008:No、Jiの影響が観測点まで伝播したことを出力するステップS3009。出力形式としては、たとえば、ディスプレイ308への表示、プリンタ313への印刷出力、I/F309による外部装置への送信がある。また、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶することとしてもよい。そして、検証支援装置が、i=i1としステップS3010、ステップS3005へ戻る。ステップS3008において、検証支援装置が、Q0に関するシミュレーション結果とQiに関するシミュレーション結果が一致したと判断した場合ステップS3008:Yes、ステップS3010へ戻る。ステップS3005において、検証支援装置が、i>nであると判断した場合ステップS3005:Yes、すべてのCDCジッタの論理値がQ0と異なっているQ0’を設定するステップS3011。そして、検証支援装置が、Q0’に関するシミュレーションを実行しステップS3012、i=1としステップS3013、i>nであるか否かを判断するステップS3014。検証支援装置が、i>nでないと判断した場合ステップS3014:No、CDCジッタのうち、Jiの論理値がQ0’と異なっている実行パターンQi’を設定しステップS3015、Qi’に関するシミュレーションを実行するステップS3016。そして、検証支援装置が、Qi’に関するシミュレーション結果と、Q0’に関するシミュレーション結果と、が一致するか否かを判断するステップS3017。検証支援装置が、Qi’に関するシミュレーション結果と、Q0’に関するシミュレーション結果と、が一致しないと判断した場合ステップS3017:No、Jiの影響が観測点まで伝播したことを出力するステップS3018。そして、検証支援装置が、i=i1としステップS3019、ステップS3014へ戻る。検証支援装置が、Qi’に関するシミュレーション結果と、Q0’に関するシミュレーション結果と、が一致すると判断した場合ステップS3017:Yes、ステップS3019へ移行する。検証支援装置が、i>nであると判断した場合ステップS3014:Yes、一連の処理を終了する。実施の形態4実施の形態4では、実施の形態1~3で示した1ビットだけ異なる複数の実行パターンのシミュレーションにおいて、共通部分を再シミュレーションさせることなく、該複数の実行パターンに関するシミュレーション結果が得られるシミュレーション例を示す。実施の形態4では、具体的には、たとえば、1ビットだけ異なる5通りの実行パターンをそれぞれ独立して5回シミュレーションさせるのではなく、1実行パターンによるシミュレーション結果を用いて1実行パターンとの差分のみをシミュレーションさせる。これにより、実施の形態4では、残余の実行パターンのシミュレーション結果が得られる。また、似通ったN個の回路情報をシミュレーションする場合に、それらを同時に実行して共通部分の再計算を避けるコンカレントシミュレーション例については公知であるため、詳細については省略する。たとえば、E.G.UlrichandT.BakerTheConcurrentSimulationofNearlyIdenticalDigitalNetworksinProc.10thDesignAutomationWorkshop,pp.145-150,1973を参照。図32は、実施の形態4の一例を示す説明図である。検証装置は、所定入力パターンを用いて論理シミュレーションにおいて、CDCモデルからCDCジッタが出力されるのを検出する。そして、検証装置は、CDCジッタを検出すると、CDCモデルの後段と同一回路にCDCジッタの論理値と異なる論理値を与えて、コンカレントシミュレーションを実行する。検証装置は、コンカレントシミュレーションの実行が終了すると、実行結果を出力する。検証装置の機能ブロック図図33は、検証装置の機能ブロック図である。検証装置3300は、検出部401と、実行部3302と、出力部3303と、を有している。検出部401~出力部3303は、具体的には、たとえば、論理シミュレータに含まれているとしてもよい。また、検出部3301~出力部3303は、たとえば、コンカレントシミュレーションの処理を有する論理シミュレーション用のプログラムにコーディングされているとする。具体的には、たとえば、CPUが、図3に示したROM302、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶された論理シミュレーション用のプログラムを読み出す。そして、CPUが、該論理シミュレーション用のプログラムにコーディングされている処理を実行することにより、検出部3301~出力部3303の処理が実行される。検証対象回路の回路情報は第1のクロックドメインと、第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有している。検出部3301は、回路情報に所定入力パターンが与えられるシミュレーションにおいて、該信号を受信する第2のクロックドメイン内の素子からのCDCジッタの出力を検出する。実行部3302は、検出部3301によりCDCジッタが検出された場合、検証対象回路内の素子の後段の回路に対して、検出されたCDCジッタの論理値と異なる論理値を与えたコンカレントシミュレーションを実行する。出力部3303は、実行部3302による実行結果を出力する。検証装置3300による検証処理手順図34は、検証装置3300による検証処理手順の一の例を示すフローチャートである。まず、検証装置3300が、CDCシミュレーションを実行しステップS3401、CDCジッタを検出したか否かを判断するステップS3402。検証装置3300が、CDCジッタを検出していないと判断した場合ステップS3402:No、ステップS3402へ戻る。検証装置3300が、CDCジッタを検出したと判断した場合ステップS3402:Yes、検出したCDCジッタの論理値と異なる論理値を与えたコンカレントシミュレーションを実行するステップS3403。そして、検証装置3300が、実行終了したか否かを判断しステップS3404、実行終了していないと判断した場合ステップS3404:No、ステップS3404へ戻る。検証装置3300が、実行終了したと判断した場合ステップS3404:Yes、実行結果を出力しステップS3405、一連の処理を終了する。出力形式としては、たとえば、ディスプレイ308への表示、プリンタ313への印刷出力、I/F309による外部装置への送信がある。また、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶することとしてもよい。つぎに、コンカレントシミュレーションの詳細も含めた例について、実施の形態1で用いた入力パターン1におけるP0~P4を用いて説明する。実施の形態4では、実施の形態1~3の構成と同一構成については同一符号を付し、詳細な説明を省略する。ここでは、P0に関するシミュレーション結果を基準とし、P0と結果が異なる箇所だけのモデルが変更され、P1~P4までのシミュレーション結果が同時に算出される。P0とP1との違いはJ1の論理値が異なっており、J1は1クロック目のAの値である。P0とP2との違いはJ2の論理値が異なっており、J2は1クロック目のBの値である。P0とP3との違いはJ3の論理値が異なっており、J3は3クロック目のAの値である。P0とP4との違いはJ4の論理値が異なっており、J4は3クロック目のBの値である。まず、検証装置3300が、回路情報を複製する。複製した各回路情報内の素子群基準モデルと称する。をP0に関するシミュレーション結果に基づいてクロックの立ち上がりごとに動作させる。さらに、CDCジッタが発生する都度、基準モデル時のCDCジッタの論理値と異なる論理値が入力される素子群CDCeffectモデルが追加される。そして、基準モデルとCDCeffectモデルとの差異を、任意の1個のCDCジッタの論理値がP0と異なる場合のシミュレーション結果とする。図35は、実施の形態4における1クロック目の処理例を示す説明図である。ここで、図中、P0が付されているモデルが基準モデルである。図の各FFには、クロックとしてCLK2が入力されているが、省略している。まず、検証装置3300が、1クロック目の立ち上がりを検出すると、1クロック目の立ち上がりに属するすべてのFFの値を更新する。これにより、FF3501の出力であるCの値が0となり、FF3502の出力であるDの値が0となり、FF3504の出力であるFの値が0となる。つぎに、検証装置3300が、CDCジッタに関するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、J1に関するCDCeffectモデルとして、CDCモデル3506から次段のFF3501までを回路情報から複製する。ここでは、J1に関するCDCeffectモデルとして、J1=1をデータ入力とするFF3511が挿入される。J1の論理値がP0と異なる実行パターンはP1であるため、図35中J1に関するCDCeffectモデルにはP1が付されている。検証装置3300が、J2に関するCDCeffectモデルとして、CDCモデル3507から次段のFFまでを回路情報から複製する。具体的には、たとえば、J2に関するCDCeffectモデルとして、J2=1をデータ入力とするFF3521が挿入される。J2の論理値がP0と異なる実行パターンはP2であるため、図35中J2に関するCDCeffectモデルにはP2が付されている。J3とJ4については、1クロック目では発生していないため、J3およびJ4に関するCDCeffectモデルは追加されない。そして、検証装置3300が、組み合わせ回路部分の信号値を更新する。これにより、選択回路3503の出力であるEが0となり、AND回路3505の出力であるdata_outが0となる。つぎに、検証装置3300が、各CDCeffectモデルP1が付された素子群とP2が付された素子群の素子のうち、基準モデルP0が付された素子群の対応する素子と同一値である素子を削除する。ここでは、CDCeffectモデルと基準モデルとが同一値でないため、いずれのCDCeffectモデルも削除されない。そして、検証装置3300が、CDCeffectモデルの出力と、基準モデルの出力との差異を出力する。出力形式としては、たとえば、ディスプレイ308への表示、プリンタ313への印刷出力、I/F309による外部装置への送信がある。また、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶することとしてもよい。図36は、1クロック目においての出力結果の一例である。0クロック目ではFF3の出力値はFF3501の出力であるAの値と同様に0であり、1クロック目ではFF3の出力値は1となる。0クロック目ではFF3521の出力値はFF3502の出力であるBの値と同様に0であり、1クロック目ではFFの出力値は0となる。図37は、実施の形態4における2クロック目の処理例を示す説明図である。つぎに、検証装置3300が、2クロック目の立ち上がりを検出すると、2クロック目の立ち上がりに属するすべてのFFの出力値を更新する。これにより、FF3501の出力であるCの値が0となり、FF3502の出力であるDの値が1となり、FF3504の出力であるFの値が0となる。さらに、J1に関するCDCeffectモデルP1が付された素子群のうちのFF3の出力値が1となる。J2に関するCDCeffectモデルP2が付された素子群のうちのFF3521の出力値が0となる。そして、検証装置3300が、J1に関するCDCジッタに対するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、FF3に対応するFF3501から次段のFF3504までを複製する。そして、具体的には、たとえば、検証装置3300が、FF3の出力を複製した回路へ与える。これにより、選択回路3512とFF3513が追加されている。そして、検証装置3300が、J2に関するCDCジッタに対するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、FF3521に対応するFF3502から次段のFF3504までを複製する。そして、具体的には、たとえば、検証装置3300が、FF3521の出力を複製した回路へ与える。これにより、選択回路3522とFF3523が追加されている。そして、たとえば、検証装置3300が、組み合わせ回路部分の信号値を更新する。これにより、選択回路3503の出力であるEが0となり、AND回路3505の出力であるdata_outが0となる。J1に関するCDCジッタに対するCDCeffectモデルのうち、選択回路3512の出力値が1となる。J2に関するCDCジッタに対するCDCeffectモデルのうち、選択回路3522の出力値が0となる。つぎに、検証装置3300が、各CDCeffectモデルP1が付された素子群とP2が付された素子群の素子のうち、基準モデルP0が付された素子群の対応する素子と同一値である素子を削除する。CDCeffectモデルの素子の入力値と出力値とが、それぞれ基準モデルの対応する素子の入力値と出力値と同一であるか否かに基づいてCDCeffectモデルの素子が削除される。具体的には、たとえば、選択回路3522の出力値と、該選択回路3522に対応する選択回路3503との出力値が同一値であるが、FF3521の入力値と該FF3521に対応するFF3502の入力値とが異なるため、削除されない。そして、検証装置3300が、J1に関するCDCeffectモデルの出力と基準モデルの出力との差異を出力し、J2に関するCDCeffectモデルの出力と基準モデルの出力との差異を出力する。図38は、実施の形態4における3クロック目の処理例を示す説明図である。つぎに、検証装置3300が、3クロック目の立ち上がりを検出すると、3クロック目の立ち上がりに属するすべてのFFの出力値を更新する。これにより、FF3501の出力であるCの値が1となり、FF3502の出力であるDの値が1となり、FF3504の出力であるFの値が0となる。さらに、J1に関するCDCeffectモデルP1が付された素子群のうち、FF3511の出力値が1となり、FF3513の出力値が1となる。J2に関するCDCeffectモデルP2が付された素子群のうち、FF3521の出力値が1となり、FF3523の出力値が1となる。つぎに、検証装置3300が、CDCジッタに対するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、J1に関するCDCeffectモデルとして、FF3513に対応するFF3504から次段のFFまでを複製する。ここでは、次段のFFがないため、出力端子までが複製される。そして、たとえば、検証装置3300が、FF3513の出力を複製した回路に与える。AND回路3514が追加され、FF3513の出力がAND回路3514に入力されている。つぎに、具体的には、たとえば、検証装置3300が、J2に関するCDCeffectモデルとして、FF3523に対応するFF3504から次段のFFまでを複製する。ここでは、次段のFFがないため、出力端子までが複製される。そして、たとえば、検証装置3300が、FF3523の出力を複製した回路に与える。AND回路3524が追加され、FF3523の出力がAND回路3524に入力されている。つぎに、具体的には、たとえば、検証装置3300が、J3に関するCDCeffectモデルとして、CDCモデル3506から次段のFF3501までを複製する。そして、たとえば、検証装置3300が、CDCモデル3506の出力値と異なる論理値を複製した回路に与える。FF3531が追加され、FF3531に0が入力される。J3の論理値がP0と異なる実行パターンはP3であるため、J3に関するCDCeffectモデルにはP3が付されている。つぎに、具体的には、たとえば、検証装置3300が、J4に関するCDCeffectモデルとして、CDCモデル3507から次段のFF3502までを複製する。そして、たとえば、検証装置3300が、CDCモデル3507の出力値と異なる論理値を複製した回路に与える。FF3541が追加され、FF3541に1が入力される。J4の論理値がP0と異なる実行パターンはP4であるため、J4に関するCDCeffectモデルにはP4が付されている。つぎに、具体的には、たとえば、検証装置3300が、組み合わせ回路部の信号値を更新する。これにより、選択回路3503の出力であるEが1となり、AND回路3505の出力であるdata_outが0となる。J1に関するCDCジッタに対するCDCeffectモデルのうち、選択回路3512の出力値が1となり、AND回路3514の出力値が0となる。J2に関するCDCジッタに対するCDCeffectモデルのうち、選択回路3522の出力値が0となり、AND回路3524の出力値が0となる。つぎに、検証装置3300が、各CDCeffectモデルP1が付された素子群~P4が付された素子群の素子のうち、基準モデルP0が付された素子群の対応する素子と同一値である素子を削除する。ここでは、J2に関するCDCeffectモデルの各素子と標準モデルの各素子とが同一値であるため、J2に関するCDCeffectモデルがすべて削除される図中×で示す。。さらに、J1に関するCDCeffectモデルのうち、FF3511の入力値と出力値とが、FF3501の入力値と出力値とがそれぞれ同一値であるため、FF3511が削除される。そして、選択回路3512にはFF3511の出力に代わってFF3501の出力が入力される。そして、検証装置3300が、J1,J3,J4に関するCDCeffectモデルの出力と基準モデルの出力との差異をそれぞれ出力する。図39は、実施の形態4における4クロック目の処理例を示す説明図である。つぎに、検証装置3300が、4クロック目の立ち上がりを検出すると、4クロック目の立ち上がりに属するすべてのFFの出力値を更新する。これにより、FF3501の出力であるCの値が1となり、FF3502の出力であるDの値が0となり、FF3504の出力であるFの値が1となる。さらに、J1に関するCDCeffectモデルP1が付された素子群のうちの、FF3513の出力値が1となる。J3に関するCDCeffectモデルP3が付された素子群のうちのFF3531の出力値が1となる。J4に関するCDCeffectモデルP4が付された素子群のうちのFF3541の出力値が1となる。つぎに、検証装置3300が、CDCジッタに対するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、J3に関するCDCeffectモデルとして、FF3531に対応するFF3501から次段のFF3504までを複製する。そして、検証装置3300が、FF3531の出力を複製した回路に与える。ここで、選択回路3532とFF3533が追加され、選択回路3532にはFF3531の出力が入力されている。つぎに、具体的には、たとえば、検証装置3300が、J4に関するCDCeffectモデルとして、FF3541に対応するFF3502から次段のFF3504までを複製する。そして、具体的には、たとえば、検証装置3300が、FF3541の出力を複製した回路に与える。ここで、選択回路3542とFF3543が追加され、選択回路3542にはFF3541の出力が入力されている。つぎに、検証装置3300が、組み合わせ回路部の信号値を更新する。これにより、選択回路3503の出力であるEが0となり、AND回路3505の出力であるdata_outが0となる。J1に関するCDCeffectモデルのうちの選択回路3512の出力値が0となり、AND回路3514の出力値が0となり、AND回路3514の出力値が0となる。J3に関するCDCeffectモデルのうち、選択回路3532の出力値が1となる。J4に関するCDCeffectモデルのうち、選択回路3542の出力値が1となる。つぎに、検証装置3300が、J1,J3,J4に関する各CDCeffectモデルP1,P3,P4が付された素子群のうち、基準モデルP0が付された素子群と同一値であるCDCeffectモデルを削除する。ここでは、J1に関するCDCeffectモデルが、基準モデルと同一値であるため、J1に関するCDCeffectモデルが削除される図中×で示す。。そして、検証装置3300が、J3,J4に関する各CDCeffectモデルの出力と基準モデルの出力との差異を出力する。図40は、実施の形態4における5クロック目の処理例を示す説明図である。つぎに、検証装置3300が、5クロック目の立ち上がりを検出すると、5クロック目の立ち上がりに属するすべてのFFの出力値を更新する。これにより、FF3501の出力であるCの値が0となり、FF3502の出力であるDの値が0となり、FF3504の出力であるFの値が0となる。さらに、J3に関するCDCeffectモデルP3が付された素子群のうち、FF3531の出力値が0となり、FF3533の出力値が1となる。J4に関するCDCeffectモデルP4が付された素子群のうち、FF3541の出力値が0となり、FF3543の出力値が1となる。つぎに、具体的には、たとえば、検証装置3300が、CDCジッタに対するCDCeffectモデルを追加する。具体的には、たとえば、検証装置3300が、J3に関するCDCeffectモデルとして、FF3533に対応するFF3504から次段のFFまでを複製する。ここでは、次段のFFがないため、出力端子までが複製される。そして、具体的には、たとえば、検証装置3300が、FF3533の出力を複製した回路に与える。AND回路3534が追加され、FF3533の出力がAND回路3534に入力されている。具体的には、たとえば、検証装置3300が、J4に関するCDCeffectモデルとして、FF3543に対応するFF3504から次段のFFまでを複製する。ここでは、次段のFFがないため、出力端子までが複製される。そして、具体的には、たとえば、検証装置3300が、FF3543の出力を複製した回路に与える。AND回路3544が追加され、FF3543の出力がAND回路3544に入力されている。つぎに、検証装置3300が、組み合わせ回路部分の信号値を更新する。これにより、選択回路3503の出力であるEが0となり、AND回路3505の出力であるdata_outが0となる。J3に関するCDCeffectモデルのうち、選択回路3532の出力値が1となり、AND回路3534の出力値が0となる。J4に関するCDCeffectモデルのうち、選択回路3542の出力値が1となり、AND回路3544の出力値が0となる。つぎに、検証装置3300が、J3,J4に関する各CDCeffectモデルP3,4が付された素子群のうち、基準モデルP0が付された素子群と同一値であるCDCeffectモデルを削除する。FF3531の入力値と出力値とがFF3501の入力値と出力値とそれぞれ同一値であるため、FF3531は削除される。選択回路3532にはFF3531の出力に代わってFF3501の出力が入力される。FF3541の入力値と出力値とがFF3502の入力値と出力値とそれぞれ同一値であるため、FF3541は削除される。選択回路3542にはFF3541の出力に代わってFF3502の出力が入力される。そして、検証装置3300が、J3,J4に関するCDCeffectモデルの出力と基準モデルの出力との差異を出力する。図41は、実施の形態4における6クロック目と7クロック目の処理例を示す説明図である。図41では、FF3531とFF3541とが削除されている。6クロック目と7クロック目との標準モデルの各素子の出力およびCDCeffectモデルの各素子の出力は、それぞれ5クロック目と同一となるため、詳細な説明を省略する。図42は、実施の形態4における8クロック目の処理例を示す説明図である。つぎに、検証装置3300が、8クロック目の立ち上がりを検出すると、8クロック目の立ち上がりに属するすべてのFFの出力値を更新する。これにより、FF3501の出力であるCの値が0となり、FF3502の出力であるDの値が0となり、FF3504の出力であるFの値が0となる。さらに、J3に関するCDCeffectモデルP3が付された素子群のうち、FF3533の出力値が1となる。J4に関するCDCeffectモデルP4が付された素子群のうち、FF3543の出力値が1となる。つぎに、具体的には、たとえば、検証装置3300が、CDCジッタに対するCDCeffectモデルを追加する。J3に関するCDCeffectモデルとJ4に関するCDCeffectモデルとはいずれも出力端子まで追加済であるため、ここでは、いずれの素子も追加されない。つぎに、検証装置3300が、組み合わせ回路部の信号値を更新する。これにより、選択回路3503の出力であるEが0となり、AND回路3505の出力であるdata_outが0となる。J3に関するCDCeffectモデルのうちの選択回路3533の出力値が1となり、AND回路3534の出力値が1となる。J4に関するCDCeffectモデルのうちの選択回路3543の出力値が1となり、AND回路3544の出力値が1となる。観測点は出力端子である。J3に関するCDCeffectモデルの出力端子の出力値およびJ4に関するCDCeffectモデルの出力端子の出力値は1であるが、標準モデルの出力端子data_outの出力値は1である。すなわち、観測点での値が標準モデルと、CDCeffectモデルとで異なる。検証装置3300が、J3の影響とJ4の影響が出力端子まで伝播したことを出力する。出力形式としては、たとえば、ディスプレイ308への表示、プリンタ313への印刷出力、I/F309による外部装置への送信がある。また、RAM303、磁気ディスク305、光ディスク307などの記憶装置に記憶することとしてもよい。そして、検証装置3300が、J3,J4に関するCDCeffectモデルの出力と基準モデルの出力との差異を出力する。そして、シミュレーションが終了するまで処理を繰り返す。また、実施の形態4で示した検証装置3300は、カバレッジ情報と、デバッグ支援情報と、を出力する。図43は、カバレッジ情報例を示す説明図である。カバレッジ情報4301は、発生箇所と観測回数とが記述されている。たとえば、発生箇所とはCDCモデルの名称であり、観測回数とは観測点における観測回数である。カバレッジ情報4302では、発生箇所と、該発生箇所ごとに複数の観測箇所および観測回数とが記述されている。たとえば、発生箇所とはCDCモデルの名称であり、観測箇所は出力端子などの観測点であり、観測回数は該観測箇所において該CDCモデルが出力するCDCジッタによる影響が観測された回数である。図44は、デバッグ支援情報例を示す説明図である。デバッグ支援情報4400は、検出箇所と検出時刻とに関連付けて、複数の発生箇所および発生時刻とが記述されている。たとえば、検出箇所は出力端子などの観測点であり、検出時刻はシミュレーションにおける開始からの経過時間や何クロック目であるかなどである。たとえば、発生箇所はCDCジッタの名称であり、発生時刻はCDCジッタが発生したシミュレーションにおける開始からの経過時間や何クロック目かである。たとえば、図35~図42の例では、検出箇所がdata_outであり、検出時刻が8クロック目である。発生箇所はJ3とJ4であり、発生時刻はそれぞれ3クロック目である。検証装置3300による検証処理手順図45は、検証装置3300による検証処理手順の他の例を示すフローチャートである。まず、検証装置3300が、各信号の初期値を設定しステップS4501、クロックイベントが発生したか否かを判断するステップS4502。クロックイベントの発生とは、具体的には、クロックの立ち上がりで同期をとるFFを検証対象回路に用いていれば、クロックの立ち上がりを検出したか否かである。また、クロックイベントの発生とは、具体的には、クロックの立ち下がりで同期をとるFFを検証対象回路に用いていれば、クロックの立ち下がりを検出したか否かである。検証装置3300が、クロックイベントが発生していないと判断した場合ステップS4502:No、ステップS4502へ戻る。検証装置3300が、クロックイベントが発生したと判断した場合ステップS4502:Yes、発生したクロックイベントに属するすべてのFFの出力値を更新するステップS4503。たとえば、FFへのデータ入力が0となっていれば、FFの出力値が0となり、FFへのデータ入力が01となっていれば、FFの出力値が1となる。そして、検証装置3300が、CDCジッタに対するCDCeffectモデルを追加しステップS4504、組み合わせ回路の信号値を更新するステップS4505。つぎに、検証装置3300が、CDCeffectモデルの素子で基準モデルの対応する素子と同じ値を持つものを削除するステップS4506。そして、検証装置3300が、基準モデルとCDCeffectモデルの出力の差異を出力しステップS4507、シミュレーションが終了であるか否かを判断するステップS4508。検証装置3300が、シミュレーションが終了でないと判断した場合ステップS4508:No、ステップS4502へ戻る。検証装置3300が、シミュレーションが終了であると判断した場合ステップS4508:Yes、一連の処理を終了する。図46は、観測点の例を示す説明図である。実施の形態1~4では、観測点Aのように、観測点をすべて出力端子として説明したが、他の箇所であってもよい。たとえば、観測点Bと観測点Cは、検証対象回路の状態を表すFFの出力State0とState1である。たとえば、観測点はCDCモデルの後段の素子の出力であってもよく、あるFFの出力から次段のFFまでを1段として、観測点DはCDCモデルから2段先のFFの出力である。たとえば、観測点が第1のクロックドメインから第2のクロックドメインへ受け渡される複数のCDC信号が合流する箇所であってもよく、観測点Eは、2個のCDCモデルの出力の合流点である。また、観測点はアサーションであってもよい。アサーションとは、検証対象の設計が満たすべき性質が定義された箇所である。実施の形態1で説明したように、検証支援装置、検証支援プログラム、および検証支援方法によれば、第1のシミュレーション結果が期待値と一致しない場合、CDCジッタのうちの一部のCDCジッタを第1のシミュレーション結果時の値と異なる値に設定する。そして、設定後での観測点における第2のシミュレーション結果と前記期待値との比較に基づいて、一部のCDCジッタの影響が観測点までに伝播するか否かを自動で検証することにより、CDCジッタによるエラー要因の特定を容易化することができる。設定後での観測点における第2のシミュレーション結果と期待値との比較結果と、観測点における第1のシミュレーション結果と期待値との比較結果と、が同一である場合、一部の出力値が不一致の要因でないことを特定する。これにより、エラー要因でないCDCジッタを容易に判別することができる。設定後での観測点におけるシミュレーション結果と期待値とが同一である場合、一部のCDCジッタに不一致の要因が含まれることを特定する。これにより、CDCジッタは実際には数千~数万個あるが、エラー要因となるCDCジッタは数個であるため、数千~数万個のCDCジッタをいくつかのグループに分割して、各グループに不一致の要因が含まれているか否かを判断することができる。これにより、検証時間の短縮化を図ることができる。CDCジッタのうちの任意の1個のCDCジッタを第1のシミュレーション結果時の値と異なる値に設定する。そして、設定後での観測点における第2のシミュレーション結果と期待値とを比較する。そして、比較結果により一致すると判断された場合、任意の1個のCDCジッタが不一致の要因であることを特定する。これにより、不一致要因の特定が正確となり、検証時間を短縮することができる。実施の形態2で説明したように、検証支援装置、検証支援プログラム、および検証支援方法によれば、CDCジッタのうちの一部のCDCジッタを第1のシミュレーション結果時の値と異なる値に設定する。そして、設定後での観測点における第2のシミュレーション結果と観測点における第1のシミュレーション結果とが一致するか否かに基づいて、各入力パターンにおいて一部のCDCジッタの影響が観測点まで伝播されているか否かを判断する。各入力パターンにおけるCDCジッタの影響を容易に特定でき、該入力パターンにおいて、各CDCジッタの検証が行われているか否かを容易に判断することができる。また、設定後での観測点における第2のシミュレーション結果と第1のシミュレーション結果とが一致すると判断された場合、一部のCDCジッタの影響は伝播されていないと特定する。これにより、所定入力パターンでは一部のCDCジッタの検証が行われていないことを容易に判断することができる。また、設定後での観測点における第2のシミュレーション結果と第1のシミュレーション結果とが一致しないと判断された場合、一部のCDCジッタの中に、影響が伝播されているCDCジッタが含まれていることを特定する。これにより、数千~数万個あるCDCジッタをいくつかのグループに分割して、各グループに影響が伝播しているCDCジッタが含まれているかを判断することで、所定入力パターンがいずれのCDCジッタの検証を行うことができるかを判断することができる。したがって、検証時間の短縮化を図ることができる。また、CDCジッタ群のうちの任意の1個のCDCジッタを第1のシミュレーション結果時の論理値と異なる論理値に設定する。そして、設定後での観測点における第2のシミュレーション結果と第1のシミュレーション結果とが一致しないと判断された場合、任意の1個のCDCジッタの影響が観測点に伝播されていることを特定する。また、CDCジッタ群から任意の1個のCDCジッタを順に選択する。選択された1個のCDCジッタごとに、1個のCDCジッタを第1のシミュレーション結果時の論理値と異なる論理値に設定する。そして、選択された1個のCDCジッタごとに、設定後での観測点における第2のシミュレーション結果と第1のシミュレーション結果とが一致しないと判断された場合、選択された1個のCDCジッタの影響が観測点に伝播されていることを特定する。これにより、すべてのCDCジッタの影響が伝播されるかを網羅することができる。実施の形態3で説明したように、検証支援装置、検証支援プログラム、および検証支援方法によれば、CDCジッタ群から任意の1個のCDCジッタを順に選択する。そして、選択された1個のCDCジッタごとに、CDCジッタ群のすべてのCDCジッタが第1のシミュレーション結果時の論理値と異なる論理値から、選択されたCDCジッタのみを異なる論理値に設定する。そして、選択されたCDCジッタごとに、設定後での観測点における第2のシミュレーション結果と第1のシミュレーション結果とが一致しないと判断された場合、選択された1個の出力値の影響が前記観測点に伝播されていることを特定する。これにより、ある入力パターンにおいてCDCシミュレーションを行うと、エラー要因となるのはCDCジッタ全体のうちの2~3個程度である。数千から数万個のCDCジッタうちの、どのCDCジッタによる影響でエラーとなっているかは不明確である。実施の形態2で示した実行パターンに加えて、実施の形態3で示した実行パターンをシミュレーションすれば、どの3個のCDCジッタの組み合わせを検証者が選択しても、該3個のCDCジッタの論理値の組み合わせを必ず検証することができる。これにより、検証時間を短縮化することができる。実施の形態1~3で説明したように、観測点が検証対象回路の出力端子であることにより、CDC箇所から最も離れた箇所までCDCジッタの影響が伝播するか否かを特定することができる。また、観測点が検証対象回路内の状態を表す素子の出力である。すなわち、観測点が状態変数である。状態変数は検証対象回路の状態を示す重要な変数であるため、該状態変数にCDCジッタの影響が伝播された場合、該影響が該状態変数以降の回路に伝播される可能性が高く、出力端子まで伝播される可能性がある。よって、状態変数でCDCジッタの影響が観測された時点で、CDCジッタがエラー要因であるか否かを特定することにより、計算量を削減することができ、検証時間の短縮化を図ることができる。また、観測点が、第1のクロックドメインから第2のクロックドメインへ非同期で渡される複数の信号の合流点である。複数の信号の合流点とはリコンバージェンスポイントである。CDC障害の多くが、リコンバージェンスポイントの設計誤りが原因である可能性が高い。よって、CDCモデルに近い回路で判定することができるため、計算量を削減することができる。また、観測点が、素子の後段の素子の出力である。CDCジッタの影響はCDCモデルに近い回路で消滅することが多いため、CDCモデルから一定段数以内の回路を観測点とすることにより、CDCモデルに近い回路で判定でき、計算量を削減することができる。また、観測点が、アサーションである。アサーションは、出力端子と同等とみなすことができるため、適切なカバレッジを得ることができる。また、カバー判定する箇所が増えることで、それぞれのCDC箇所により近い箇所でカバー判定される可能性が高くなる。カバー判定がされたら、シミュレーションを打ち切っても良いので、計算量を削減することができる。実施の形態4で説明したように、検証装置、検証プログラム、および検証方法によれば、CDCシミュレーション中に、CDCジッタを検出すると、検出したCDCジッタの論理値と異なる論理値を該CDCジッタを出力する素子以降に与える。そして、CDCシミュレーションにおけるシミュレーション結果との差異のみをシミュレーションするコンカレントシミュレーションを実行することにより、計算量を削減することができる。さらに、CDCジッタの論理値が異なる複数のシミュレーション結果を得ることができるため、検証時間を短縮することができる。なお、本実施の形態1~4で説明した検証支援方法および検証方法は、予め用意されたプログラムをパーソナルコンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムおよび検証プログラムは、ハードディスク、フレキシブルディスク、CD-ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検証支援プログラムおよび検証プログラムは、インターネット等のネットワークを介して配布してもよい。以上の実施の形態1~4に関し、さらに以下の付記を開示する。付記1第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出する検出手段と、前記検出手段により前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定する設定手段と、前記設定手段による設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較する比較手段と、前記比較手段による比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定する特定手段と、を備えることを特徴とする検証支援装置。付記2前記特定手段は、前記比較手段による前記設定後での前記観測点におけるシミュレーション結果と前記期待値との比較結果と、前記観測点におけるシミュレーション結果と前記期待値との比較結果と、が同一である場合、前記一部の出力値が不一致の要因でないことを特定することを特徴とする付記1に記載の検証支援装置。付記3前記特定手段は、前記比較手段による前記設定後での前記観測点におけるシミュレーション結果と前記期待値とが同一である場合、前記一部の出力値に前記不一致の要因が含まれることを特定することを特徴とする付記1に記載の検証支援装置。付記4前記設定手段は、前記出力値群のうちの任意の1個の出力値を前記シミュレーション結果時の論理値と異なる論理値に設定し、前記比較手段は、前記設定手段による設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、前記特定手段は、前記設定後での前記観測点におけるシミュレーション結果と前記期待値とが前記比較手段により一致すると判断された場合、前記任意の1個の出力値が前記不一致の要因であることを特定することを特徴とする付記1に記載の検証支援装置。付記5前記観測点が、前記検証対象回路の出力端子であることを特徴とする付記1~4のいずれか一つに記載の検証支援装置。付記6前記観測点が、前記検証対象回路内の状態を表す素子の出力であることを特徴とする付記1~4のいずれか一つに記載の検証支援装置。付記7前記観測点が、前記第1のクロックドメインから前記第2のクロックドメインへ非同期で渡される複数の信号の合流点であることを特徴とする付記1~4のいずれか一つに記載の検証支援装置。付記8前記観測点が、前記素子の後段の素子の出力であることを特徴とする付記1~4のいずれか一つに記載の検証支援装置。付記9前記観測点がアサーションであることを特徴とする付記1~4のいずれか一つに記載の検証支援装置。付記10第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得する取得手段と、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記取得手段により取得されたシミュレーション結果時の論理値と異なる論理値に設定する設定手段と、前記設定手段による設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較する比較手段と、前記比較手段による比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定する特定手段と、を備えることを特徴とする検証支援装置。付記11前記特定手段は、前記比較手段によって前記設定後の前記観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とが一致すると判断された場合、前記一部の出力値の影響は伝播されていないと特定することを特徴とする付記10に記載の検証支援装置。付記12前記特定手段は、前記比較手段によって前記設定後の前記観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とが一致しないと判断された場合、前記一部の出力値の中に、影響が前記観測点に伝播されている出力値が含まれていることを特定することを特徴とする付記10に記載の検証支援装置。付記13前記設定手段は、前記出力値群のうちの任意の1個の出力値を前記シミュレーション結果時の論理値と異なる論理値に設定し、前記比較手段は、前記設定手段による設定後のシミュレーション結果と前記シミュレーション結果とを比較し、前記特定手段は、前記比較手段により前記設定後での前記観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とが一致しないと判断された場合、前記任意の1個の出力値の影響が前記観測点に伝播されていることを特定することを特徴とする付記10に記載の検証支援装置。付記14さらに、前記出力値群から1個の出力値を順に選択する選択手段を備え、前記設定手段は、前記出力値群のうち、前記選択手段により選択される都度、前記選択された1個の出力値を前記シミュレーション結果時の論理値と異なる論理値に設定し、前記比較手段は、前記選択された1個の出力値ごとに、前記設定手段による設定後での前記観測点におけるシミュレーション結果と前記観測点におけるシミュレーション結果とを比較し、前記特定手段は、前記比較手段により前記設定後での前記観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とが一致しないと判断された場合、前記選択された1個の出力値の影響が前記観測点に伝播されていることを特定することを特徴とする付記10に記載の検証支援装置。付記15前記設定手段は、前記選択手段により選択される都度、前記出力値群のすべての出力値が前記シミュレーション結果時の論理値と異なる論理値から、前記出力値群のうちの前記選択手段により選択された出力値のみを異なる論理値に設定し、前記比較手段は、前記出力値群のすべての出力値が前記シミュレーション結果時の論理値と異なる論理値の場合のシミュレーション結果と、前記設定手段による設定後のシミュレーション結果とを比較し、前記特定手段は、前記すべての出力値が前記シミュレーション結果時の論理値と異なる論理値の場合の前記観測点におけるシミュレーション結果と、前記比較手段により前記設定後での前記観測点におけるシミュレーション結果と、が一致しないと判断された場合、前記選択された1個の出力値の影響が前記観測点に伝播されていることを特定することを特徴とする付記14に記載の検証支援装置。付記16前記観測点が、前記検証対象回路の出力端子であることを特徴とする付記10~15のいずれか一つに記載の検証支援装置。付記17前記観測点が、前記検証対象回路内の状態を表す素子の出力であることを特徴とする付記10~15のいずれか一つに記載の検証支援装置。付記18前記観測点が、前記第1のクロックドメインから前記第2のクロックドメインへ非同期で渡される複数の信号の合流点であることを特徴とする付記10~15のいずれか一つに記載の検証支援装置。付記19前記観測点が、前記素子の後段の素子の出力であることを特徴とする付記10~15のいずれか一つに記載の検証支援装置。付記20前記観測点がアサーションであることを特徴とする付記10~15のいずれか一つに記載の検証支援装置。付記21第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出する検出手段と、前記検出手段により前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行する実行手段と、前記実行手段による実行結果を出力する出力手段と、を備えることを特徴とする検証装置。付記22第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出し、前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定する処理をコンピュータに実行させることを特徴とする検証支援プログラム。付記23第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得し、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、取得されたシミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較し、比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定する処理をコンピュータに実行させることを特徴とする検証支援プログラム。付記24第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出し、前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行し、実行結果を出力する処理をコンピュータに実行させることを特徴とする検証プログラム。付記25コンピュータによって実行される検証支援方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられた、前記検証対象回路内の観測点におけるシミュレーション結果と期待値との不一致を検出し、前記不一致が検出された場合、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、前記シミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記観測点におけるシミュレーション結果と前記期待値とを比較し、比較結果に基づいて、前記一部の出力値が前記不一致の要因であるか否かを特定することを特徴とする検証支援方法。付記26コンピュータによって実行される検証支援方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられたシミュレーション結果を取得し、前記信号を受信する前記第2のクロックドメイン内の素子の出力がランダム値である出力値群のうちの一部の出力値を、取得されたシミュレーション結果時の論理値と異なる論理値に設定し、設定後での前記検証対象回路内の観測点におけるシミュレーション結果と前記観測点における前記シミュレーション結果とを比較し、比較結果に基づいて、前記一部の出力値の影響が前記観測点に伝播されているか否かを特定することを特徴とする検証支援方法。付記27コンピュータによって実行される検証方法であって、第1のクロックドメインと、前記第1のクロックドメインから非同期で信号を受信する第2のクロックドメインと、を有する検証対象回路の回路情報に、所定入力パターンが与えられるシミュレーションにおいて、前記信号を受信する前記第2のクロックドメイン内の素子からのランダム値の出力を検出し、前記ランダム値が前記素子から検出された場合、前記検証対象回路内の前記素子の後段の回路に対して、前記素子の出力値と異なる論理値を与えたコンカレントシミュレーションを実行し、実行結果を出力することを特徴とする検証方法。"