"回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記第1の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出工程と、前記第2の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。前記決定工程は、前記第2の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との不一致が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする請求項1に記載の検証支援プログラム。前記決定工程は、前記第2の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との一致が検出された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする請求項1または2に記載の検証支援プログラム。前記第1の検出工程、前記更新工程、前記第2の検出工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする請求項1~3のいずれか一つに記載の検証支援プログラム。前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、前記選択工程によって選択されたアサーションごとに、前記レジスタの期待値の更新を指示する更新指示記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、前記第1の検出工程は、前記編集工程による編集後のアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、前記更新工程は、前記第1の検出工程によって検出されたアサーションに挿入されている前記更新指示記述に従って、前記レジスタの期待値を、前記第1の検出工程によって検出されたアサーションで定義されているレジスタの値に更新することを特徴とする請求項1~4のいずれか一つに記載の検証支援プログラム。回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記レジスタの値の変化を検出する第2の検出工程と、前記複数のクロックの各々のクロックにおいて、前記第2の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。前記決定工程は、前記判断工程によって、前記複数のクロックのいずれかのクロックにおいて前記アサーションで規定されたクロックと同一クロックであると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする請求項6に記載の検証支援プログラム。前記決定工程は、前記第1の検出工程によって、前記回路の模擬中に成立するアサーションが検出されておらず、かつ、前記第2の検出工程によって、前記レジスタの値の変化が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする請求項6または7に記載の検証支援プログラム。前記第2の検出工程によって前記レジスタの値の変化が検出された場合、前記レジスタについてクロックごとにアサーション成立を通知する成立通知を待ち受けるチェックプロセス群を生成する生成工程を前記コンピュータに実行させ、前記判断工程は、前記生成工程によって生成されたチェックプロセス群のうち、前記アサーションから前記成立通知を受けたチェックプロセスの有無を判断することを特徴とする請求項6に記載の検証支援プログラム。前記決定工程は、前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがあると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする請求項9に記載の検証支援プログラム。前記決定工程は、前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがないと判断された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする請求項9または10に記載の検証支援プログラム。前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、前記選択工程によって選択されたアサーションごとに、前記成立通知に関する記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、前記第1の検出工程は、前記編集工程による編集後のアサーション群の中から、前記回路の模擬中に成立するアサーションを検出することを特徴とする請求項8~10のいずれか一つに記載の検証支援プログラム。前記第1の検出工程、前記第2の検出工程、前記判断工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする請求項6~12のいずれか一つに記載の検証支援プログラム。回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出手段と、前記第1の検出手段によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新手段と、前記更新手段による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出手段と、前記第2の検出手段によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、前記決定手段によって決定された決定結果を出力する出力手段と、を備えることを特徴とする検証支援装置。回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出手段と、前記レジスタの値の変化を検出する第2の検出手段と、前記複数のクロックの各々のクロックにおいて、前記第2の検出手段によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出手段によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断手段と、前記判断手段によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、前記決定手段によって決定された決定結果を出力する出力手段と、を備えることを特徴とする検証支援装置。コンピュータが、回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記第1の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出工程と、前記第2の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、を実行することを特徴とする検証支援方法。コンピュータが、回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記レジスタの値の変化を検出する第2の検出工程と、前記複数のクロックの各々のクロックにおいて、前記第2の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、を実行することを特徴とする検証支援方法。しかしながら、上述した従来技術では、検証対象回路の仕様書に従って好適に振る舞う回路モデルを作成する場合、仕様書が複雑だと、正しい振る舞いをする回路モデルを作成するのに非常に時間がかかるという問題があった。一方、回路モデルの精度が低くても、検証対象回路についてのアサーションアサートプロパティ、検証プロパティとも呼ぶが仕様書から正しく記述できれば、回路モデルでの検証対象回路の振る舞いに誤りがあることを検出することができる。しかしながら、検証者が検証対象回路についてアサーションを記述する場合、1個のレジスタについて複数の検証シナリオが存在するときは、アサーションの記述が難しくなる。したがって、アサーションで定義した検証シナリオ外でレジスタの値が変化した場合は、アサーションでは検出することができないという問題があった。また、検証対象回路が複数のクロックで動作する場合は、回路モデルでの振る舞いもより複雑化するため、アサーションで定義した検証シナリオ外でレジスタの値の変化を検出するのは、より困難であるという問題があった。1つの側面では、本発明は、回路について定義したシナリオ外でのバグの特定の容易化を図ることができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。本発明の一態様として、回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新し、前記レジスタの値の変化を検出し、前記レジスタの値の変化が検出された場合、当該変化後の前記レジスタの値と更新後の前記レジスタの期待値とが、一致するか否かを判断し、判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定し、決定された決定結果を出力する検証支援プログラム、検証支援装置、および検証支援方法が提案される。また、回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出し、前記レジスタの値の変化を検出し、前記複数のクロックの各々のクロックにおいて、前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断し、判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定し、決定された決定結果を出力する検証支援プログラム、検証支援装置、および検証支援方法が提案される。本発明の一態様によれば、回路について定義したシナリオ外でのバグの特定の容易化を図ることができるという効果を奏する。以下に添付図面を参照して、本発明にかかる検証支援プログラム、検証支援装置、および検証支援方法の実施の形態を詳細に説明する。以降、単一クロックで動作する検証対象回路については実施の形態1で説明し、複数クロックで動作する検証対象回路については実施の形態2で説明する。また、検証対象回路内のレジスタ群のうちアサーションの対象となったレジスタをレジスタRとする。実施の形態1<アサーションによる検証対象回路のチェック例>図1は、実施の形態1にかかるアサーションによる検証対象回路のチェック例を示す説明図である。アサーションとは、検証対象回路の設計が満たすべき性質を定義したデータである。図1では、アサーションの一例として、アサーションA1,A2が定義されているものとする。アサーションA1は、たとえば、Verilogなどのハードウェア記述言語を用いて記述されている。アサーションA1は、クロックClkの立ち上がりにおいて、入力Iに1が入力されると1サイクル後にレジスタRの値が3に変化することをチェックするアサーションである。アサーションA2は、クロックClkの立ち上がりにおいて、入力Iに2が入力されると1サイクル後にレジスタRの値が4に変化することをチェックするアサーションである。また、アサーションA1,A2には、updateR_specが記述されている。updateR_specのように末尾に挿入された記述は、挿入先のアサーションが成立した場合に呼び出されるサブルーチンである。この場合の挿入記述であるupdateR_specは、期待値R_specの更新を指示する記述である。したがって、挿入先のアサーションをアサーションA1とし、アサーションA1が成立すると、期待値R_specをアサーションA1でのレジスタRの値3に更新することとなる。また、検証対象回路は、クロックClkで動作し、入力IとレジスタRの振る舞いが規定された回路モデルである。具体的には、入力Iは、クロックClkの立ち上がり時刻t1で5から1に変化する。また、レジスタRは、クロックClkの立ち上がり時刻t2で2から3に変化し、時刻t5で3から5に変化する。ここで、時刻t1で入力Iが5から1に変化した場合、その1サイクル後の立ち上がり時刻t2でレジスタRの値が2から3に変化しているため、アサーションA1が成立していることがチェックされる。このように、アサーションA1が成立することが確認された場合、その1サイクル後の立ち上がり時刻t3において、レジスタRの期待値R_specを2から3に更新する。これにより、立ち上がり時刻t3以降のレジスタRの期待値R_specは、R_spec=3となり、アサーションA1が成立した回路モデルでのレジスタRの値R=3と一致し、整合性を保つことができる。一方、クロックClkの立ち上がり時刻t5では、レジスタRの値が3から5に変化しているが、いずれのアサーションA1,A2どおりでもない予期しない変化である。具体的には、その1サイクル後の立ち上がり時刻t6において、レジスタRの値5と期待値R_specの3が不一致となるため、アサーション外でのレジスタRの値の変化であるとしてエラー検出される。このように、本実施の形態では、立ち上がり時刻t1~t2での振る舞いのように、アサーションA1,A2が成立した場合には、レジスタRの期待値R_specをアサーションA1,A2成立時のレジスタRの値に更新することで、アサーションA1,A2成立以降において、レジスタRの値とその期待値R_specとが一致する。したがって、アサーションA1,A2成立以降、レジスタRにおいて予期しない変化が発生するまで検証対象回路についてアサーションA1,A2外でレジスタRの値が変化しないことを保証することができる。一方、立ち上がり時刻t5でのレジスタRの予期しない変化のようにアサーションA1,A2外でレジスタRの値が変化した場合は、エラーとして通知することで、アサーションA1,A2で定義されていないにもかかわらず、バグの特定が容易となる。このように、アサーションA1,A2で定義されていないシナリオで発生するバグが検出できるため、アサーションにより検証対象回路の振る舞いを網羅できない場合であっても、バグの検出が可能となる。そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタRの値が変化しないことを保証することができる。<検証支援装置のハードウェア構成例>図2は、実施の形態1にかかる検証支援装置のハードウェア構成例を示すブロック図である。図2において、検証支援装置は、CPUCentralProcessingUnit201と、ROMReadOnlyMemory202と、RAMRandomAccessMemory203と、磁気ディスクドライブ204と、磁気ディスク205と、光ディスクドライブ206と、光ディスク207と、ディスプレイ208と、I/FInterface209と、キーボード210と、マウス211と、スキャナ212と、プリンタ213と、を備えている。また、各構成部はバス200によってそれぞれ接続されている。ここで、CPU201は、検証支援装置の全体の制御を司る。ROM202は、ブートプログラムなどのプログラムを記憶している。RAM203は、CPU201のワークエリアとして使用される。磁気ディスクドライブ204は、CPU201の制御にしたがって磁気ディスク205に対するデータのリード/ライトを制御する。磁気ディスク205は、磁気ディスクドライブ204の制御で書き込まれたデータを記憶する。光ディスクドライブ206は、CPU201の制御にしたがって光ディスク207に対するデータのリード/ライトを制御する。光ディスク207は、光ディスクドライブ206の制御で書き込まれたデータを記憶したり、光ディスク207に記憶されたデータをコンピュータに読み取らせたりする。ディスプレイ208は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ208は、たとえば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。インターフェース以下、I/Fと略する。209は、通信回線を通じてLANLocalAreaNetwork、WANWideAreaNetwork、インターネットなどのネットワーク214に接続され、このネットワーク214を介して他の装置に接続される。そして、I/F209は、ネットワーク214と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F209には、たとえばモデムやLANアダプタなどを採用することができる。キーボード210は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス211は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ212は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ212は、OCROpticalCharacterReader機能を持たせてもよい。また、プリンタ213は、画像データや文書データを印刷する。プリンタ213には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。<検証支援装置の機能的構成例>つぎに、実施の形態1にかかる検証支援装置の機能的構成例について説明する。図3は、実施の形態1にかかる検証支援装置の機能的構成例を示すブロック図である。検証支援装置は、編集処理部301とチェッカーモジュール群CMとを有する。編集処理部301は、選択部311と編集部312とを有する。編集処理部301選択部311および編集部312およびチェッカーモジュール群CMは、具体的には、たとえば、図2に示したROM202、RAM203、磁気ディスク205、光ディスク207などの記憶装置に記憶されたプログラムをCPU201に実行させることにより、または、I/F209により、その機能を実現する。アサーション群310,320は、検証対象回路についてのアサーションの集合である。アサーション群310は、編集処理部301による編集前のアサーション群である。アサーション群310内のアサーションとは、たとえば、図1のアサーションA1,A2において、updateR_specが挿入されていないアサーションである。一方、アサーション群320は、編集処理部301によりアサーション群310が編集された編集後のアサーション群である。アサーション群320内のアサーションとは、たとえば、図1のアサーションA1,A2である。選択部311は、アサーション群310の中から未選択のアサーションを選択する。選択部311は、未選択のアサーションがなくなるまで選択をつづける。編集部312は、選択部311によって選択されたアサーション選択アサーションに、検証対象回路内のレジスタの期待値の更新を指示する更新指示記述を挿入する。挿入された更新指示記述は期待値の更新サブルーチンを呼び出す記述である。更新指示記述とは、たとえば、図1に示したupdateR_specが挙げられる。updateR_specは、挿入先のアサーション内のR_specを更新するサブルーチンである。このように、編集部312では、選択アサーションごとに、更新指示記述を挿入することで、編集後のアサーション群320を生成することができる。編集済みのアサーション群320は、チェッカーモジュール群CMに参照される。チェッカーモジュール群CMは、検証対象回路内のレジスタごとに用意されたn個nはアサーションで定義されたレジスタ数のチェッカーモジュールCM1,...,CMi,...,CMnである。チェッカーモジュールCMiは、チェック対象のレジスタやアサーションアサーション群320内のアサーションが異なるだけで処理内容は同一である。図4は、チェッカーモジュールの機能的構成例を示すブロック図である。チェッカーモジュールCMiは、第1の検出部401と、更新部402と、第2の検出部403と、決定部404と、出力部405とを備えている。第1の検出部401~出力部405は、具体的には、たとえば、図2に示したROM202、RAM203、磁気ディスク205、光ディスク207などの記憶装置に記憶されたプログラムをCPU201に実行させることにより、または、I/F209により、その機能を実現する。第1の検出部401は、単一のクロックClkで動作する検証対象回路が満たすべきレジスタRの値を規定するアサーション群320の中から検証対象回路の模擬中に成立するアサーションを検出する。単一のクロックClkで動作すれば、検証対象回路全体でもよく、検証対象回路の一部の回路ブロックでもよい。第1の検出部401は、チェッカーモジュールCMiで対象となるレジスタRについて成立するアサーションアサーション群320内のアサーションを模擬中に検出する。たとえば、図1のように、第1の検出部401は、単一のクロックClkの時刻t2において、アサーションA1,A2のうちアサーションA1が成立したことを検出する。更新部402は、第1の検出部401によってアサーションが検出されたクロックタイミングの次のクロックタイミングで、レジスタRの期待値R_specをアサーションで規定されたレジスタRの値に更新する。具体的には、更新部402は、成立したアサーションの更新指示記述updateR_specを実行する期待値R_specの更新サブルーチンである。これにより、期待値R_specが、検出時刻の次の時刻で、模擬中のレジスタRの値すなわち、成立したアサーションでのレジスタRの値に更新される。したがって、更新部402による更新以降は、検証対象回路が正しく設計されていれば、アサーションが成立しない限り、レジスタRの値と期待値R_specは同一の値となるはずである。第2の検出部403は、更新部402による更新後におけるレジスタRの期待値R_specとレジスタRの値との不一致を検出する。具体的には、たとえば、第2の検出部403は、チェッカーモジュールCMiで対象となるレジスタRの値の変化をクロックClkの立ち上がり時刻ごとに立ち下がり時刻ごとでもよい監視する。これにより、検証対象回路が正しく設計されていれば、アサーション群320内のレジスタRについてのいずれのアサーションも成立しない限り、レジスタRの値と期待値R_specは一致するはずである。一方、不一致となる場合は、レジスタRは、アサーション群320で定義されていない変化をしたこととなる。決定部404は、第2の検出部403によって検出された検出結果に基づいて、レジスタRの値の変化の正否を決定する。具体的には、たとえば、決定部404は、第2の検出部403によって不一致が検出された場合、レジスタRの値の変化が、アサーション群320で規定されていない変化誤った変化であると決定する。一方、第2の検出部403によって一致が検出された場合、レジスタRの値の変化が、期待通りの変化正しい変化であると決定する。なお、決定部404は、第2の検出部403によって不一致が検出された場合のみ、決定処理を実行することとしてもよい。第2の検出部403は毎時刻検出処理を実行するが、不一致の検出回数は一致の検出回数よりも少ないと考えられるため、不一致の場合のみ決定処理を実行することで検証支援処理の高速化を図ることができる。出力部405は、決定部404によって決定された決定結果を出力する。具体的には、たとえば、出力部405は、決定部404によって誤った変化であると決定された場合、レジスタRの不一致が検出された時刻とレジスタRの識別情報を出力する。識別情報とは、レジスタRを一意に特定する情報であり、たとえば、レジスタ名である。たとえば、図1の例では、出力部405は、{NG,時刻t5,R}を出力する。また、出力部405は、レジスタRの不一致が検出された時刻の次サイクルとなる時刻とレジスタRの識別情報を出力する。たとえば、図1の例では、出力部405は、{NG,時刻t6,R}を出力する。このとき、レジスタRの値も出力してもよい。この場合、出力部405は、{NG,時刻t6,R=5}を出力する。なお、出力部405は、決定部404によって正しい変化であると決定された場合、一致が検出された時刻とレジスタRの識別情報を出力することとしてもよい。たとえば、図1の例では、出力部405は、{OK,時刻t3,R}を出力する。このような出力結果は、ディスプレイ208に表示してもよく、プリンタ213に印刷出力してもよく、通信可能なコンピュータに送信してもよい。また、検証支援装置内の記憶装置RAM203、磁気ディスク205に格納してもよい。<編集処理手順>図5は、実施の形態1にかかる検証支援装置によるアサーション群310の編集処理手順を示すフローチャートである。選択部311は、アサーション群310の中から未選択のアサーションがあるか否かを判断するステップS501。未選択のアサーションがある場合ステップS501:Yes、選択部311は、アサーション群310の中から未選択のアサーションを1つ選択するステップS502。そして、編集部312は、選択アサーションに期待値の更新サブルーチンを呼び出す更新指示記述を挿入するステップS503。このあと、編集部312は、挿入後の選択アサーションを検証支援装置内の記憶装置に保持しステップS504、ステップS501に戻る。ステップS501において、未選択のアサーションがない場合はステップS501:No、編集が完了したとして編集処理を終了する。これにより、未編集のアサーション群310から更新指示記述が挿入されたアサーション群320に編集されるため、チェッカーモジュール群CMでのチェック処理においてアサーション成立時に自動的に期待値R_specを更新することができる。<チェッカーモジュールCMiによる検証対象回路の模擬中での期待値更新処理手順>図6は、チェッカーモジュールCMiによる検証対象回路の模擬中での期待値更新処理手順を示すフローチャートである。まず、第1の検出部401が、チェッカーモジュールCMiで対象にしているレジスタRについて、検証対象回路の模擬中に成立するアサーションがアサーション群320の中から検出されるまで待ち受けるステップS601:No。検出された場合ステップS601:Yes、更新部402は、次のサイクル次のクロックタイミングで、検出アサーションのレジスタRの値を期待値R_specに更新するステップS602。そして、ステップS601に戻る。図6のフローチャートは、検証対象回路の模擬が終了することで終了する。<チェッカーモジュールCMiによる検証対象回路の模擬中での正否検出処理手順>図7は、チェッカーモジュールCMiによる検証対象回路の模擬中での正否検出処理手順を示すフローチャートである。図7では、例としてクロックClkの立ち上がり時刻を検出することとするが、立ち下がり時刻でもよい。まず、第2の検出部403は、クロックClkの立ち上がり時刻になるのを待ち受けステップS701:No、立ち上がり時刻になるとステップS701:Yes、レジスタRの値と期待値R_specとが一致するか否かを判断するステップS702。一致する場合ステップS702:Yes、ステップS701に戻る。一方、不一致である場合ステップS702:No、決定部404は、次のサイクル次のクロックタイミングで、レジスタRの値の変化はアサーション群320に規定されていない誤った変化であると決定するステップS703。そして、出力部405は、決定結果を出力しステップS704、ステップS701に戻る。図7のフローチャートは、検証対象回路の模擬が終了することで終了する。このように、実施の形態1によれば、アサーションが成立する都度、期待値R_specをレジスタRの値に更新するため、更新後は、設計が正しければレジスタRの値と期待値R_specの値は一致し続ける。このため、レジスタRの値と期待値R_specの値との不一致を検出すれば、アサーション群320のいずれのアサーションも成立していないにもかかわらず、レジスタRの値が変化したこととなる。したがって、アサーション群320のいずれのアサーションでも規定されていない変化であることが判明するため、アサーション群では検出できないバグを効率的に検出することができる。そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタRの値が変化しないことを保証することができる。また、上述した実施の形態1の検証対象回路は単一のクロックClkで動作する回路としたが、検証対象回路が複数のクロックで動作する場合であっても、クロックドメインごとに検証対象とすることで、実施の形態1を適用することもできる。実施の形態2つぎに、実施の形態2について説明する。実施の形態1では、対象となるレジスタRを動作させるクロックが1つだけである。このため、アサーションに更新指示記述を挿入すし、アサーション成立時に期待値R_specを更新することで、設計が正しければ、レジスタRの値と期待値R_specとは一致するという状態にする。これにより、レジスタRの値と期待値R_specとが不一致であれば、期待通りではないレジスタRの値の変化であるとして、アサーション群320のいずれのアサーションでも定義されていない誤った変化であることを検出していた。これに対し、対象となるレジスタRを動作させるクロックが複数ある場合、虚偽エラーが発生する。具体的には、実施の形態1のようにアサーション成立時刻の次の時刻で期待値R_specを更新しようとすると、当該次の時刻が、アサーション成立時刻のクロックとは異なるクロックの場合、レジスタRの値と期待値R_specとが不一致となる。以下、図8で説明する。<虚偽エラー発生例>図8は、複数クロックの場合の虚偽エラー発生例を示す説明図である。図8において、レジスタRについて、アサーションA11,A12が規定されているものとする。アサーションA11は、クロックClk1の立ち上がりにおいて、入力Iに1が入力されると1サイクル後にレジスタRの値が3に変化することをチェックするアサーションである。アサーションA12は、クロックClk2の立ち上がりにおいて、入力Iに2が入力されると1サイクル後にレジスタRの値が4に変化することをチェックするアサーションである。図8において、クロックClk2の立ち上がり時刻t21において入力Iの値が5から1に変化した場合、クロックClk2の立ち上がり時刻t22においてレジスタRの値が2から3に変化している。このため、アサーションA11が成立することとなる。そして、実施の形態1のように、レジスタRの期待値R_specを更新する次の時刻は、クロックClk2の立ち上がり時刻t23である。このため、クロックClk2の立ち上がり時刻t22~t23の間におけるクロックClk1の立ち上がり時刻t14~t17において、レジスタRの値と期待値R_specとの不一致3≠2が発生することとなる。すなわち、クロックClk2の立ち上がり時刻t22~t23の間では、アサーションA11どおりに動作しているにもかかわらず、アサーションA11を満たしていないとしてエラーを検出することとなる。このため、実施の形態2では、検証対象回路内のレジスタRが複数のクロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群320では検出できないバグを効率的に検出する例について説明する。なお、実施の形態2では、一例として、クロックの数を3Clk1~Clk3として説明する。また、図9~図13では、エラーが発生しない例を説明し、図14~図18では、エラーが検出できた例について説明する。<複数クロックでのエラー検出動作例1>図9~図13は、複数クロックでのエラー検出動作例1を示す説明図である。複数クロックでのエラー検出動作例1では、アサーションA20が成立した場合に上述した虚偽エラーを発生させることなく、アサーションA20の成立をチェックする動作例である。図9は、初期状態を示している。図9において、同一のレジスタRについてクロックごとに、相互チェッカーモジュールが用意されている。CoChecker1R,Clk1は、レジスタRがクロックClk1で動作するときのアサーション成立を検出する相互チェッカーモジュールCCMi1である。CoChecker2R,Clk2は、レジスタRがクロックClk2で動作するときのアサーション成立を検出する相互チェッカーモジュールCCMi2である。CoChecker3R,Clk3は、レジスタRがクロックClk3で動作するときのアサーション成立を検出する相互チェッカーモジュールCCMi3である。このように、相互チェッカーモジュールは、同一のレジスタRについてクロック数分生成される。また、図9~図13では、例としてアサーションA20が成立するか否かを検出するものとする。アサーションA20は、クロックClk2の立ち上がりにおいて、入力Iに1が入力されると1サイクル後にレジスタRの値が3に変化することをチェックするアサーションである。なお、アサーションA20に挿入されているCoChecker2.triggerOKは、挿入先のアサーションが成立した場合に呼び出されるサブルーチンである。CoChecker2.triggerOKは、相互チェッカーモジュールCCMi2に、そのチェックプロセスへアサーションA20の成立通知OKを通知させる成立通知サブルーチンである。図10は、図9からの遷移状態を示している。図10では、各相互チェッカーモジュールCCMi1~CCMi3において、チェックプロセスCPi1~CPi3が始動した状態を示している。チェックプロセスCPi1~CPi3は、レジスタRの値の変化が検出されると始動する。図10では、クロックClk2の立ち上がり時刻t21において入力Iの値が5から1に変化したため、クロックClk2の立ち上がり時刻t22においてレジスタRの値が2から3に変化する。この振る舞いは、アサーションA20を満たしている。クロックClk2の時刻t22でレジスタRの値が2から3に変化したため、チェックプロセスCPi1~CPi3は、クロックClk2の時刻t22で始動する。チェックプロセスCPi1~CPi3では、始動するとグローバル変数であるCをインクリメントする。本例では相互チェッカーモジュール数は3であるため、C=3となる。すなわち、グローバル変数であるCは、同一レジスタRを動作させるクロック数となる。なお、Cは順次デクリメントされていく。Cがデクリメントされて、C=0となる前に全チェックプロセスCPi1~CPi3が終了すると、図8に示した虚偽エラーが、アサーションA20の成立時刻であるクロックClk2の立ち上がり時刻t22から次の時刻t23までの間で発生することなく、アサーションA20が成立したことを適性にチェックすることができたこととなる。一方、全チェックプロセスCPi1~CPi3終了時にC=0になると、アサーション群のいずれのアサーションでも定義されていないレジスタRの値の変化を検出したこととなる。図11は、図10からの遷移状態を示している。図11において、アサーションA20の成立時刻であるt22の次にレジスタRを動作させる時刻は、クロックClk1の時刻t14である。したがって、クロックClk1での動作を監視している相互チェッカーモジュールCCMi1では、アサーションA20の成立通知OKを待ち受けるが、時刻t14では成立していない。このため、相互チェッカーモジュールCCMi1では、時刻t14で成立通知OKを受け付けられないため、チェックプロセスCPi1は、Cをデクリメントして、C=2となる。そして、チェックプロセスCPi1は終了する。図12は、図11からの遷移状態を示している。図12において、チェックプロセスCPi1の終了時刻となったクロックClk1の立ち上がり時刻t14の次にレジスタRを動作させる時刻は、クロックClk1の立ち上がり時刻t15~t17であるが、相互チェッカーモジュールCCMi1のチェックプロセスCPi1はすでに終了している。このため、クロックClk1の時刻t17の次にレジスタRを動作させる時刻は、クロックClk2の立ち上がり時刻t23となる。したがって、クロックClk2での動作を監視している相互チェッカーモジュールCCMi2では、アサーションA20の成立通知OKを待ち受ける。時刻t23は、アサーションA20の成立時刻t22の次の時刻であるため、相互チェッカーモジュールCCMi2の成立通知サブルーチンCoChecker2.triggerOKが呼び出される。これにより、相互チェッカーモジュールCCMi2は、チェックプロセスCPi2にアサーションA20の成立通知OKを発行することで、チェックプロセスCPi2は、アサーションA20の成立通知OKを受け付けることができる。成立通知OKを受け付けたチェックプロセスCPi2は、CをデクリメントせずC=2のまま終了する。図13は、図12からの遷移状態を示している。図13において、チェックプロセスCPi2の終了時刻となったクロックClk2の時刻t23の次にレジスタRを動作させる時刻は、クロックClk3の立ち上がり時刻t32である。したがって、クロックClk3での動作を監視している相互チェッカーモジュールCCMi3では、アサーションA20の成立通知OKを待ち受けるが、立ち上がり時刻t32では成立していない。このため、相互チェッカーモジュールCCMi3では、立ち上がり時刻t32で成立通知OKを受け付けられないため、チェックプロセスCPi3は、Cをデクリメントして、C=1となる。そして、チェックプロセスCPi3は終了する。したがって、C=0となる前に全チェックプロセスCPi1~CPi3が終了したこととなる。このように、実施の形態2では、図8に示した虚偽エラーが、アサーションA20の成立時刻であるクロックClk2の立ち上がり時刻t22~t23までの間で発生することなく、アサーションA20が成立したことを適性にチェックすることができる。<複数クロックでのエラー検出動作例2>図14~図18は、複数クロックでのエラー検出動作例2を示す説明図である。複数クロックでのエラー検出動作例2では、アサーションA20が不成立である場合に上述した虚偽エラーを発生させることなく、アサーション群のいずれのアサーションでも定義されていないレジスタRの値の変化を検出する動作例である。図14は、初期状態を示している。図14において、同一のレジスタRについてクロックごとに、相互チェッカーモジュールCCMi1~CCMi3が用意されている。図9の初期状態と図14の初期状態とで異なる箇所は、図9では、クロックClk2の立ち上がり時刻t22でレジスタRの値が2から3に変化するのに対し、図14では、クロックClk2の立ち上がり時刻t22でレジスタRの値が2から4に変化する点である。図15は、図14からの遷移状態を示している。図15では、各相互チェッカーモジュールCCMi1~CCMi3において、チェックプロセスCPi1~CPi3が始動した状態を示している。チェックプロセスCPi1~CPi3は、レジスタRの値の変化が検出されると始動する。図15では、クロックClk2の立ち上がり時刻t21において入力Iの値が5から1に変化したため、クロックClk2の立ち上がり時刻t22においてレジスタRの値が2から4に変化する。この振る舞いは、アサーションA20を満たしていない。クロックClk2の立ち上がり時刻t22でレジスタRの値が2から4に変化したため、チェックプロセスCPi1~CPi3は、クロックClk2の立ち上がり時刻t22で始動する。チェックプロセスCPi1~CPi3では、始動するとグローバル変数であるCをインクリメントする。本例では相互チェッカーモジュール数は3であるため、C=3となる。すなわち、グローバル変数であるCは、同一レジスタRを動作させるクロック数となる。なお、Cは順次デクリメントされていく。Cがデクリメントされて、C=0となる前に全チェックプロセスCPi1~CPi3が終了すると、図8に示した虚偽エラーが、アサーションA20の成立時刻であるクロックClk2の立ち上がり時刻t22から次の時刻t23までの間で発生することなく、アサーションA20が成立したことを適性にチェックすることができたこととなる。一方、全チェックプロセスCPi1~CPi3終了時にC=0になると、アサーション群のいずれのアサーションでも定義されていないレジスタRの値の変化を検出したこととなる。図16は、図15からの遷移状態を示している。図16において、レジスタRの値が変化した時刻t22の次にレジスタRを動作させる時刻は、クロックClk1の立ち上がり時刻t14である。したがって、クロックClk1での動作を監視している相互チェッカーモジュールCCMi1では、アサーションA20の成立通知OKを待ち受けるが、時刻t14では成立していない。このため、相互チェッカーモジュールCCMi1では、時刻t14で成立通知OKを受け付けられないため、チェックプロセスCPi1は、Cをデクリメントして、C=2となる。そして、チェックプロセスCPi1は終了する。図17は、図16からの遷移状態を示している。図17において、チェックプロセスCPi1の終了時刻となった時刻t14の次にレジスタRを動作させる時刻は、クロックClk1の時刻t15~t17であるが、相互チェッカーモジュールCCMi1のチェックプロセスCPi1はすでに終了している。このため、クロックClk1の立ち上がり時刻t17の次にレジスタRを動作させる時刻は、クロックClk2の立ち上がり時刻t23となる。したがって、クロックClk2での動作を監視している相互チェッカーモジュールCCMi2では、アサーションA20の成立通知OKを待ち受ける。時刻t23は、クロックClk2でレジスタRが変化した時刻t22の次の時刻であるが、アサーションA20が不成立である。したがって、相互チェッカーモジュールCCMi2では、時刻t23で成立通知OKを受け付けられないため、チェックプロセスCPi2は、Cをデクリメントして、C=1となる。そして、チェックプロセスCPi2は終了する。図18は、図17からの遷移状態を示している。図18において、チェックプロセスCPi2の終了時刻となった時刻t23の次にレジスタRを動作させる時刻は、クロックClk3の時刻t32である。したがって、クロックClk3での動作を監視している相互チェッカーモジュールCCMi3では、アサーションA20の成立通知OKを待ち受けるが、時刻t32では成立していない。このため、相互チェッカーモジュールCCMi3では、時刻t32で成立通知OKを受け付けられないため、チェックプロセスCPi3は、Cをデクリメントして、C=0となる。そして、チェックプロセスCPi3は終了する。このように、全チェックプロセスCPi1~CPi3終了時にC=0になったため、クロックClk2の立ち上がり時刻t22において、アサーション群のいずれのアサーションでも定義されていないレジスタRの値の変化を検出したこととなる。これにより、検証対象回路内のレジスタが複数クロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群では検出できないバグを効率的に検出することができる。<検証支援装置の機能的構成例>つぎに、実施の形態2にかかる検証支援装置の機能的構成例について説明する。なお、実施の形態1と同一構成には同一符号を付し、その説明を省略する。また、実施の形態2にかかる検証支援装置のハードウェア構成例は、図2と同一構成であるため省略する。図19は、実施の形態2にかかる検証支援装置の機能的構成例を示すブロック図である。検証支援装置は、編集/作成処理部1900と相互チェッカーモジュール群集合CCMとを有する。編集/作成処理部1900は、選択部1901と編集部1902と特定部1903と作成部1904とを有する。編集/作成処理部1900選択部1901~作成部1904および相互チェッカーモジュール群集合CCMは、具体的には、たとえば、図2に示したROM202、RAM203、磁気ディスク205、光ディスク207などの記憶装置に記憶されたプログラムをCPU201に実行させることにより、または、I/F209により、その機能を実現する。アサーション群1910は、編集/作成処理部1900による編集前のアサーション群である。アサーション群1910内のアサーションとは、たとえば、図9のアサーションA20において、CoChecker2.triggerOKが挿入されていないアサーションである。一方、アサーション群1920は、編集/作成処理部1900によりアサーション群1910が編集された編集後のアサーション群である。アサーション群1920内のアサーションとは、たとえば、図9のアサーションA20である。選択部1901は、アサーション群1910の中から未選択のアサーションを選択する。選択部1901は、未選択のアサーションがなくなるまで選択をつづける。編集部1902は、選択部1901によって選択されたアサーション選択アサーションに、アサーション成立を通知する成立通知に関する記述を挿入する。挿入された成立通知に関する記述は、アサーション成立をチェックプロセスに通知させるサブルーチンを呼び出す記述である。成立通知に関する記述とは、たとえば、図9に示したCoChecker2.triggerOKが挙げられる。CoChecker2.triggerOKは、挿入先のアサーションが成立した場合に、CoChecker2に、CoChecker2へOKを発行させるサブルーチンである。一般的に、クロックClkの立ち上がりまたは立ち下がりでのアサーション成立について相互チェッカーモジュールCCMiに通知させたい場合は、CoChecker.triggerOKとすればよい。このように、編集部1902では、アサーションごとに、成立通知に関する記述を挿入することで、編集後のアサーション群1920を生成することができる。編集済みのアサーション群1920は、相互チェッカーモジュール群集合CCMに参照される。特定部1903は、サブルーチン挿入後のアサーションから、レジスタの識別情報とクロックの識別情報とを特定する。レジスタの識別情報とは、レジスタを一意に特定する情報であり、たとえば、レジスタ名である。クロックの識別情報とは、クロックを一意に特定する情報であり、たとえば、クロック名である。たとえば、選択アサーションがアサーションA20の場合、レジスタ名としてR、クロック名としてClk2を特定する。作成部1904は、特定部1903によって特定されたレジスタの識別情報とクロックの識別情報に基づいて、相互チェッカーモジュール群を作成する。具体的には、たとえば、クロックの総数は既知ここでは、Clk1~Clk3の3個であるため、クロック名Clk2が特定されると、特定されたレジスタRについて、相互チェッカーモジュールCCMi1~CCMi3を作成する。なお、作成部1904は、あらかじめ相互チェッカーモジュールCCMiの動作記述をテンプレートして保持しているため、レジスタ名とクロック名をテンプレートに与えるだけで作成することができる。相互チェッカーモジュール群集合CCMは、相互チェッカーモジュール群CCM1,...,CCMi,...,CCMnである。nは、アサーションで定義されたレジスタ数である。相互チェッカーモジュール群CCMiは、チェック対象のレジスタやアサーションアサーション群1920内のアサーションが異なるだけで処理内容は同一である。<相互チェッカーモジュールの機能的構成例>図20は、相互チェッカーモジュール群CCMiの機能的構成例を示すブロック図である。相互チェッカーモジュール群CCMiは、第1の検出部2001と、第2の検出部2002と、判断部2003と、生成部2004と、決定部2005と、出力部2006とを備えている。第1の検出部2001~出力部2006は、具体的には、たとえば、図2に示したROM202、RAM203、磁気ディスク205、光ディスク207などの記憶装置に記憶されたプログラムをCPU201に実行させることにより、または、I/F209により、その機能を実現する。第1の検出部2001は、複数のクロックで動作する回路が回路内のレジスタRについて複数のクロックのうちいずれかのクロックのタイミングで満たすべきレジスタRの値を規定するアサーション群の中から、回路の模擬中に成立するアサーションを検出する。具体的には、たとえば、クロックClk1~Clk3という3つのクロックにより内部のレジスタRを動作させる検証対象回路についてのアサーション群1920の中から、シミュレーション中に成立するアサーションを検出する。たとえば、図20に示したように、第1の検出部2001は、アサーション群1920の中から、クロックClk2の時刻t22で成立するアサーションA20を検出する。第2の検出部2002は、レジスタRの値の変化を検出する。ここでいうレジスタRの値の変化は、アサーション成立の場合であるか否かを問わない。たとえば、第2の検出部2002は、図10に示したように、相互チェッカーモジュールCCMi2によりクロックClk2の時刻t22でのレジスタRの値の変化2→3を検出する。同様に、第2の検出部2002は、図15に示したように、相互チェッカーモジュールCCMi2によりクロックClk2の時刻t22でのレジスタRの値の変化2→4を検出する。判断部2003は、複数のクロックの各々のクロックにおいて、第2の検出部2002によってレジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該時刻となるクロックと第1の検出部2001によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する。具体的には、たとえば、判断部2003は、第1の検出部2001によってアサーションの成立を検出していない場合は、実行されない。すなわち、図14~図18の例では、判断部2003は実行されない。一方、図9~図13の例では、図10の状態でアサーションA20の成立が検出されている。したがって、判断部2003は、図11に示したように、クロックClk1において、レジスタRの値の変化が検出された時刻t22以降で最初に到来する時刻t14が、成立したアサーションA20で規定されたクロックClk2と同一クロックであるか否かを判断する。時刻t14はクロックClk1に属しているため、成立したアサーションA20で規定されたクロックClk2とは同一クロックではない。同様に、判断部2003は、図12に示したように、クロックClk2において、レジスタRの値の変化が検出された時刻t22以降で最初に到来する時刻t23が、成立したアサーションA20で規定されたクロックClk2と同一クロックであるか否かを判断する。時刻t23はクロックClk2に属しているため、成立したアサーションA20で規定されたクロックClk2とは同一クロックとなる。また、判断部2003は、図13に示したように、クロックClk3において、レジスタRの値の変化が検出された時刻t22以降で最初に到来する時刻t32が、成立したアサーションA20で規定されたクロックClk2と同一クロックであるか否かを判断する。時刻t32はクロックClk3に属しているため、成立したアサーションA20で規定されたクロックClk2とは同一クロックではない。生成部2004は、第2の検出部2002によってレジスタRの値の変化が検出された場合、レジスタRについてクロックごとにアサーション成立を通知する成立通知を待ち受けるチェックプロセス群を生成する。具体的には、たとえば、図9~図18に示したように、相互チェッカーモジュールCCMi1~CCMi3ごとにチェックプロセスCPi1~CPi3を生成する。チェックプロセスCPi1~CPi3が生成されると、それぞれグローバル変数Cをインクリメントする。これにより、クロックClk1~Clk3の総数m=Cとなる。このあと、図9~図13の場合、判断部2003によって同一クロックであると判断されると、判断されたアサーションに挿入されている成立通知に関する記述で指定されたサブルーチンが呼び出される。そして、相互チェッカーモジュールCCMi1~CCMi3のうち、同一クロックとなったクロックClk2に関する相互チェッカーモジュールCCMi2は、呼び出された成立通知サブルーチンが実行されることで、成立通知を受け付けることができる。なお、図14~図18の例では、アサーションが成立していないため判断部2003で同一クロックであると判断されることはない。なお、図9~図13の例および図14~図18の例のいずれにおいても、同一クロックでないと判断される都度、グローバル変数Cはデクリメントされる。決定部2005は、判断部2003によって判断された判断結果に基づいて、レジスタRの値の変化の正否を決定する。具体的には、たとえば、判断部2003による同一クロックの判断で、クロックClk1~ClkmのうちいずれかのクロックClkjで同一であると判断された場合、グローバル変数Cは、デクリメントされてもC=0にはならないため、レジスタRの値の変化は、期待通りの正しい変化であると決定する。たとえば、図9~図13の例で示したように、クロックClk2の時刻t23で成立したアサーションA20のクロックClk2と同一クロックと判断されるため、クロックClk2の時刻t22でのレジスタRの値の変化は、アサーションA20に従った期待通りの正しい変化であると決定する。一方、判断部2003による同一クロックの判断で、どのクロックClk1~Clkmも同一でないと判断された場合、グローバル変数Cは、デクリメントされて最終的にC=0にはなる。したがって、レジスタRの値の変化は、いずれのアサーションでも定義されていない誤った変化であると決定する。たとえば、図14~図18の例で示したように、クロックClk2の時刻t22でのレジスタRの値の変化ではアサーションA20が成立していないため、アサーションA20に挿入されている成立通知に関する記述から成立通知サブルーチンを呼び出せないこととなる。したがって、Cはその都度、デクリメントされ、最終的にC=0となる。これにより、クロックClk2の時刻t22でのレジスタRの値の変化は、いずれのアサーションでも定義されていない誤った変化であると決定する。出力部2006は、決定部2005によって決定された決定結果を出力する。具体的には、たとえば、出力部2006は、決定部2005によって誤った変化であると決定された場合、レジスタRの値の変化を検出したクロックおよび変化したクロックタイミングとレジスタRの識別情報を出力する。識別情報とは、レジスタRを一意に特定する情報であり、たとえば、レジスタ名である。たとえば、図14~図18の例では、出力部2006は、{NG,クロックClk2,時刻t22,R}を出力する。このとき、レジスタRの値も出力してもよい。この場合、出力部2006は、{NG,クロックClk2,時刻t22,R=4}を出力する。また、出力部2006は、決定部2005によって正しい変化であると決定された場合、レジスタRの値の変化を検出したクロックおよび変化したクロックタイミングとレジスタRの識別情報とを出力することとしてもよい。たとえば、図9~図13の例では、出力部2006は、{OK,クロックClk2,時刻t22,R}を出力する。このとき、レジスタRの値も出力してもよい。この場合、出力部2006は、{OK,クロックClk2,時刻t22,R=3}を出力する。また、出力部2006は、決定部2005によって正しい変化であると決定された場合、レジスタRの値の変化を検出したクロック、成立通知OKを受け付けた時刻と、レジスタRの識別情報とを出力することとしてもよい。たとえば、図9~図13の例では、出力部2006は、{OK,クロックClk2,時刻t23,R}を出力する。このとき、レジスタRの値も出力してもよい。この場合、出力部2006は、{OK,クロックClk2,時刻t23,R=3}を出力する。このような出力結果は、ディスプレイ208に表示してもよく、プリンタ213に印刷出力してもよく、通信可能なコンピュータに送信してもよい。また、検証支援装置内の記憶装置に格納してもよい。<編集/作成処理手順>図21は、実施の形態2にかかる検証支援装置による編集/作成処理手順を示すフローチャートである。選択部1901は、アサーション群1910の中から未選択のアサーションがあるか否かを判断するステップS2101。未選択のアサーションがある場合ステップS2101:Yes、選択部1901は、アサーション群1910の中から未選択のアサーションを1つ選択するステップS1902。そして、編集部1902は、成立通知を通知させる成立通知サブルーチンを呼び出す成立通知に関する記述を、選択アサーションに挿入するステップS2103。このあと、編集部1902は、挿入後の選択アサーションを検証支援装置内の記憶装置に保持するステップS2104。また、特定部1903は、選択アサーションから、選択アサーションで規定されているクロックの識別情報とレジスタの識別情報を特定するステップS2105。そして、作成部1904は、特定されたクロックの識別情報とレジスタの識別情報とについて、チェッカーモジュール群CCMiを作成済みであるか否かを判断するステップS2106。作成済みである場合ステップS2106:Yes、ステップS2101に戻る。一方、作成済みでない場合ステップS2106:No、作成部1904は、特定されたクロックの識別情報とレジスタの識別情報とについて、チェッカーモジュール群CCMiを作成し、記憶装置に保持するステップS2107。このあと、ステップS2101に移行する。そして、ステップS2101において、未選択のアサーションがない場合ステップS2101:No、編集/作成処理を終了する。これにより、未編集のアサーション群1910から成立通知に関する記述が挿入されたアサーション群1920に編集されるため、相互チェッカーモジュール群集合CCMでのチェック処理においてアサーションが成立した場合、虚偽エラーを発生することなく、レジスタRの値の変化の正否を特定することができる。<相互チェッカーモジュールCCMijによる検証対象回路の模擬中での成立通知処理手順>図22は、相互チェッカーモジュールCCMijによる検証対象回路の模擬中での成立通知処理手順を示すフローチャートである。まず、第1の検出部2001が、相互チェッカーモジュール群CCMiで対象にしているレジスタRについて、検証対象回路の模擬中に成立するアサーションがアサーション群1920の中から検出されるまで待ち受けるステップS2201:No。検出された場合ステップS2201:Yes、成立したアサーションに記述されている成立通知サブルーチンを読み出すことで、相互チェッカーモジュールCCMijは、自身のチェックプロセスCPijに、成立通知OKを通知するステップS2202。そして、ステップS2201に戻る。図22のフローチャートは、検証対象回路の模擬が終了することで終了する。<相互チェッカーモジュールCCMijによる検証対象回路の模擬中でのチェックプロセスCPijの始動処理手順>図23は、相互チェッカーモジュールCCMijによる検証対象回路の模擬中でのチェックプロセスCPijの始動処理手順を示すフローチャートである。まず、第2の検出部2002が、相互チェッカーモジュール群CCMiで対象にしているレジスタRの値が変化するまで待ち受けるステップS2301:No。レジスタRの値の変化が検出された場合ステップS2301:Yes、相互チェッカーモジュールCCMijはチェックプロセスCPijを始動するステップS2302。そして、グローバル変数CをインクリメントするステップS2303。相互チェッカーモジュールCCMijはクロック総数m個存在するため、各々の相互チェッカーモジュールCCMijでインクリメントされることで、C=mとなる。これにより、チェックプロセスCPijの始動処理が終了する。<チェックプロセスCPijの実行処理手順>図24は、図23で始動されたチェックプロセスCPijの実行処理手順を示すフローチャートである。図24では、例としてクロックClkの立ち上がり時刻を検出することとするが、立ち下がり時刻でもよい。まず、第2の検出部2002は、クロックClkの立ち上がり時刻になるのを待ち受けステップS2401:No、立ち上がり時刻になるとステップS2401:Yes、相互チェッカーモジュールCCMijから成立通知OKが受信されたか否かを判断するステップS2402。受信された場合ステップS2402:Yes、グローバル変数Cをデクリメントせずに、チェックプロセスCPijを終了するステップS2407。一方、受信されなかった場合ステップS2402:No、判断部2003は、グローバル変数CをデクリメントしステップS2403、デクリメント後のCがC>0であるか否かを判断するステップS2404。C>0である場合ステップS2404:Yes、ステップS2407に移行して、チェックプロセスCPijを終了するステップS2407。一方、C>0でない場合ステップS2404:No、決定部2005は、レジスタRの値の変化は、いずれのアサーションにも定義されていない誤った変化であると決定するステップS2405。そして、出力部2006は、決定部2005によって決定された決定結果を出力してステップS2406、チェックプロセスCPijを終了するステップS2407。このように、実施の形態2によれば、アサーションが成立する都度、相互チェッカーモジュールCCMijごとにチェックプロセスCPijを始動させて、成立通知を待ち受けさせる。そして、1つでも成立通知を受けたチェックプロセスCPijが存在する場合は、レジスタRの値の変化は、アサーションに従った期待通りの変化であることが保証される。一方、成立通知を受けたチェックプロセスCPijが1つも存在しない場合は、レジスタRの値の変化は、いずれのアサーションにも規定されていない誤った変化であることが判明する。このように、実施の形態2では、アサーションが成立した場合には、図8に示したような虚偽エラーが発生することなく、アサーションが成立したことを適性にチェックすることができる。また、アサーションが成立せずに、単にレジスタRの値が変化した場合には、アサーション群のいずれのアサーションでも定義されていないレジスタRの値の変化を検出することができる。これにより、検証対象回路内のレジスタRが複数のクロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群では検出できないバグを効率的に検出することができる。そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタRの値が変化しないことを保証することができる。なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナルコンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、CD-ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。上述した実施の形態に関し、さらに以下の付記を開示する。付記1回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記第1の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出工程と、前記第2の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記2前記決定工程は、前記第2の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との不一致が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記1に記載の検証支援プログラム。付記3前記決定工程は、前記第2の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との一致が検出された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記1または2に記載の検証支援プログラム。付記4前記出力工程は、前記レジスタの不一致が検出されたクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記1~3のいずれか一つに記載の検証支援プログラム。付記5前記出力工程は、前記レジスタの不一致が検出されたクロックタイミングの次のクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記1~3のいずれか一つに記載の検証支援プログラム。付記6前記第1の検出工程、前記更新工程、前記第2の検出工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする付記1~5のいずれか一つに記載の検証支援プログラム。付記7前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、前記選択工程によって選択されたアサーションごとに、前記レジスタの期待値の更新を指示する更新指示記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、前記第1の検出工程は、前記編集工程による編集後のアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、前記更新工程は、前記第1の検出工程によって検出されたアサーションに挿入されている前記更新指示記述に従って、前記レジスタの期待値を、前記第1の検出工程によって検出されたアサーションで定義されているレジスタの値に更新することを特徴とする付記1~6のいずれか一つに記載の検証支援プログラム。付記8回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記レジスタの値の変化を検出する第2の検出工程と、前記複数のクロックの各々のクロックにおいて、前記第2の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、をコンピュータに実行させることを特徴とする検証支援プログラム。付記9前記決定工程は、前記判断工程によって、前記複数のクロックのいずれかのクロックにおいて前記アサーションで規定されたクロックと同一クロックであると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記8に記載の検証支援プログラム。付記10前記決定工程は、前記第1の検出工程によって、前記回路の模擬中に成立するアサーションが検出されておらず、かつ、前記第2の検出工程によって、前記レジスタの値の変化が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記8または9に記載の検証支援プログラム。付記11前記第2の検出工程によって前記レジスタの値の変化が検出された場合、前記レジスタについてクロックごとにアサーション成立を通知する成立通知を待ち受けるチェックプロセス群を生成する生成工程を前記コンピュータに実行させ、前記判断工程は、前記生成工程によって生成されたチェックプロセス群のうち、前記アサーションから前記成立通知を受けたチェックプロセスの有無を判断することを特徴とする付記8に記載の検証支援プログラム。付記12前記決定工程は、前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがあると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記11に記載の検証支援プログラム。付記13前記決定工程は、前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがないと判断された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記11または12に記載の検証支援プログラム。付記14前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、前記選択工程によって選択されたアサーションごとに、前記成立通知に関する記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、前記第1の検出工程は、前記編集工程による編集後のアサーション群の中から、前記回路の模擬中に成立するアサーションを検出することを特徴とする付記10~12のいずれか一つに記載の検証支援プログラム。付記15前記出力工程は、前記レジスタの値の変化があったクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記8~14のいずれか一つに記載の検証支援プログラム。付記16前記出力工程は、前記レジスタの値の変化があったクロックタイミングの次のクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記8~14のいずれか一つに記載の検証支援プログラム。付記17前記第1の検出工程、前記第2の検出工程、前記判断工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする付記8~16のいずれか一つに記載の検証支援プログラム。付記18回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出手段と、前記第1の検出手段によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新手段と、前記更新手段による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出手段と、前記第2の検出手段によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、前記決定手段によって決定された決定結果を出力する出力手段と、を備えることを特徴とする検証支援装置。付記19回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出手段と、前記レジスタの値の変化を検出する第2の検出手段と、前記複数のクロックの各々のクロックにおいて、前記第2の検出手段によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出手段によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断手段と、前記判断手段によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、前記決定手段によって決定された決定結果を出力する出力手段と、を備えることを特徴とする検証支援装置。付記20コンピュータが、回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記第1の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第2の検出工程と、前記第2の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、を実行することを特徴とする検証支援方法。付記21コンピュータが、回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第1の検出工程と、前記レジスタの値の変化を検出する第2の検出工程と、前記複数のクロックの各々のクロックにおいて、前記第2の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第1の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、前記決定工程によって決定された決定結果を出力する出力工程と、を実行することを特徴とする検証支援方法。"