JP5640790B2 - 検証支援プログラム、検証支援装置、および検証支援方法 - Google Patents

Description

本発明は、回路の検証を支援する検証支援プログラム、検証支援装置、および検証支援方法に関する。

従来から、検証対象回路についてのアサーションを用いたシミュレーションや、検証対象回路のレジスタを監視するシミュレーションが開示されている。

特開２００８−１８１２２７号公報

しかしながら、上述した従来技術では、検証対象回路の仕様書に従って好適に振る舞う回路モデルを作成する場合、仕様書が複雑だと、正しい振る舞いをする回路モデルを作成するのに非常に時間がかかるという問題があった。

一方、回路モデルの精度が低くても、検証対象回路についてのアサーション（アサートプロパティ、検証プロパティとも呼ぶ）が仕様書から正しく記述できれば、回路モデルでの検証対象回路の振る舞いに誤りがあることを検出することができる。しかしながら、検証者が検証対象回路についてアサーションを記述する場合、１個のレジスタについて複数の検証シナリオが存在するときは、アサーションの記述が難しくなる。

したがって、アサーションで定義した検証シナリオ外でレジスタの値が変化した場合は、アサーションでは検出することができないという問題があった。また、検証対象回路が複数のクロックで動作する場合は、回路モデルでの振る舞いもより複雑化するため、アサーションで定義した検証シナリオ外でレジスタの値の変化を検出するのは、より困難であるという問題があった。

１つの側面では、本発明は、回路について定義したシナリオ外でのバグの特定の容易化を図ることができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。

本発明の一態様として、回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新し、前記レジスタの値の変化を検出し、前記レジスタの値の変化が検出された場合、当該変化後の前記レジスタの値と更新後の前記レジスタの期待値とが、一致するか否かを判断し、判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定し、決定された決定結果を出力する検証支援プログラム、検証支援装置、および検証支援方法が提案される。

また、回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出し、前記レジスタの値の変化を検出し、前記複数のクロックの各々のクロックにおいて、前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断し、判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定し、決定された決定結果を出力する検証支援プログラム、検証支援装置、および検証支援方法が提案される。

本発明の一態様によれば、回路について定義したシナリオ外でのバグの特定の容易化を図ることができるという効果を奏する。

図１は、実施の形態１にかかるアサーションによる検証対象回路のチェック例を示す説明図である。 図２は、実施の形態１にかかる検証支援装置のハードウェア構成例を示すブロック図である。 図３は、実施の形態１にかかる検証支援装置の機能的構成例を示すブロック図である。 図４は、チェッカーモジュールの機能的構成例を示すブロック図である。 図５は、実施の形態１にかかる検証支援装置によるアサーション群３１０の編集処理手順を示すフローチャートである。 図６は、チェッカーモジュールＣＭｉによる検証対象回路の模擬中での期待値更新処理手順を示すフローチャートである。 図７は、チェッカーモジュールＣＭｉによる検証対象回路の模擬中での正否検出処理手順を示すフローチャートである。 図８は、複数クロックの場合の虚偽エラー発生例を示す説明図である。 図９は、複数クロックでのエラー検出動作例を示す説明図（その１）である。 図１０は、複数クロックでのエラー検出動作例を示す説明図（その２）である。 図１１は、複数クロックでのエラー検出動作例を示す説明図（その３）である。 図１２は、複数クロックでのエラー検出動作例を示す説明図（その４）である。 図１３は、複数クロックでのエラー検出動作例を示す説明図（その５）である。 図１４は、複数クロックでのエラー検出動作例２を示す説明図（その１）である。 図１５は、複数クロックでのエラー検出動作例２を示す説明図（その２）である。 図１６は、複数クロックでのエラー検出動作例２を示す説明図（その３）である。 図１７は、複数クロックでのエラー検出動作例２を示す説明図（その４）である。 図１８は、複数クロックでのエラー検出動作例２を示す説明図（その５）である。 図１９は、実施の形態２にかかる検証支援装置の機能的構成例を示すブロック図である。 図２０は、相互チェッカーモジュール群ＣＣＭｉの機能的構成例を示すブロック図である。 図２１は、実施の形態２にかかる検証支援装置による編集／作成処理手順を示すフローチャートである。 図２２は、相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中での成立通知処理手順を示すフローチャートである。 図２３は、相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中でのチェックプロセスＣＰｉｊの始動処理手順を示すフローチャートである。 図２４は、図２３で始動されたチェックプロセスＣＰｉｊの実行処理手順を示すフローチャートである。

以下に添付図面を参照して、本発明にかかる検証支援プログラム、検証支援装置、および検証支援方法の実施の形態を詳細に説明する。以降、単一クロックで動作する検証対象回路については実施の形態１で説明し、複数クロックで動作する検証対象回路については実施の形態２で説明する。また、検証対象回路内のレジスタ群のうちアサーションの対象となったレジスタを「レジスタＲ」とする。

（実施の形態１）
＜アサーションによる検証対象回路のチェック例＞
図１は、実施の形態１にかかるアサーションによる検証対象回路のチェック例を示す説明図である。アサーションとは、検証対象回路の設計が満たすべき性質を定義したデータである。図１では、アサーションの一例として、アサーションＡ１，Ａ２が定義されているものとする。アサーションＡ１は、たとえば、Ｖｅｒｉｌｏｇなどのハードウェア記述言語を用いて記述されている。

アサーションＡ１は、『クロックＣｌｋの立ち上がりにおいて、入力Ｉに「１」が入力されると１サイクル後にレジスタＲの値が「３」に変化する』ことをチェックするアサーションである。アサーションＡ２は、『クロックＣｌｋの立ち上がりにおいて、入力Ｉに「２」が入力されると１サイクル後にレジスタＲの値が「４」に変化する』ことをチェックするアサーションである。

また、アサーションＡ１，Ａ２には、「ｕｐｄａｔｅＲ＿ｓｐｅｃ」が記述されている。「ｕｐｄａｔｅＲ＿ｓｐｅｃ」のように末尾に挿入された記述は、挿入先のアサーションが成立した場合に呼び出されるサブルーチンである。この場合の挿入記述である「ｕｐｄａｔｅＲ＿ｓｐｅｃ」は、期待値Ｒ＿ｓｐｅｃの更新を指示する記述である。したがって、挿入先のアサーションをアサーションＡ１とし、アサーションＡ１が成立すると、期待値Ｒ＿ｓｐｅｃをアサーションＡ１でのレジスタＲの値「３」に更新することとなる。

また、検証対象回路は、クロックＣｌｋで動作し、入力ＩとレジスタＲの振る舞いが規定された回路モデルである。具体的には、入力Ｉは、クロックＣｌｋの立ち上がり時刻ｔ１で「５」から「１」に変化する。また、レジスタＲは、クロックＣｌｋの立ち上がり時刻ｔ２で「２」から「３」に変化し、時刻ｔ５で「３」から「５」に変化する。

ここで、時刻ｔ１で入力Ｉが「５」から「１」に変化した場合、その１サイクル後の立ち上がり時刻ｔ２でレジスタＲの値が「２」から「３」に変化しているため、アサーションＡ１が成立していることがチェックされる。

このように、アサーションＡ１が成立することが確認された場合、その１サイクル後の立ち上がり時刻ｔ３において、レジスタＲの期待値Ｒ＿ｓｐｅｃを「２」から「３」に更新する。これにより、立ち上がり時刻ｔ３以降のレジスタＲの期待値Ｒ＿ｓｐｅｃは、Ｒ＿ｓｐｅｃ＝３となり、アサーションＡ１が成立した回路モデルでのレジスタＲの値（Ｒ＝３）と一致し、整合性を保つことができる。

一方、クロックＣｌｋの立ち上がり時刻ｔ５では、レジスタＲの値が「３」から「５」に変化しているが、いずれのアサーションＡ１，Ａ２どおりでもない予期しない変化である。具体的には、その１サイクル後の立ち上がり時刻ｔ６において、レジスタＲの値「５」と期待値Ｒ＿ｓｐｅｃの「３」が不一致となるため、アサーション外でのレジスタＲの値の変化であるとしてエラー検出される。

このように、本実施の形態では、立ち上がり時刻ｔ１〜ｔ２での振る舞いのように、アサーションＡ１，Ａ２が成立した場合には、レジスタＲの期待値Ｒ＿ｓｐｅｃをアサーションＡ１，Ａ２成立時のレジスタＲの値に更新することで、アサーションＡ１，Ａ２成立以降において、レジスタＲの値とその期待値Ｒ＿ｓｐｅｃとが一致する。したがって、アサーションＡ１，Ａ２成立以降、レジスタＲにおいて予期しない変化が発生するまで検証対象回路についてアサーションＡ１，Ａ２外でレジスタＲの値が変化しないことを保証することができる。

一方、立ち上がり時刻ｔ５でのレジスタＲの予期しない変化のようにアサーションＡ１，Ａ２外でレジスタＲの値が変化した場合は、エラーとして通知することで、アサーションＡ１，Ａ２で定義されていないにもかかわらず、バグの特定が容易となる。このように、アサーションＡ１，Ａ２で定義されていないシナリオで発生するバグが検出できるため、アサーションにより検証対象回路の振る舞いを網羅できない場合であっても、バグの検出が可能となる。

そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタＲの値が変化しないことを保証することができる。

＜検証支援装置のハードウェア構成例＞
図２は、実施の形態１にかかる検証支援装置のハードウェア構成例を示すブロック図である。図２において、検証支援装置は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）２０１と、ＲＯＭ（Ｒｅａｄ Ｏｎｌｙ Ｍｅｍｏｒｙ）２０２と、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）２０３と、磁気ディスクドライブ２０４と、磁気ディスク２０５と、光ディスクドライブ２０６と、光ディスク２０７と、ディスプレイ２０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）２０９と、キーボード２１０と、マウス２１１と、スキャナ２１２と、プリンタ２１３と、を備えている。また、各構成部はバス２００によってそれぞれ接続されている。

ここで、ＣＰＵ２０１は、検証支援装置の全体の制御を司る。ＲＯＭ２０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ２０３は、ＣＰＵ２０１のワークエリアとして使用される。磁気ディスクドライブ２０４は、ＣＰＵ２０１の制御にしたがって磁気ディスク２０５に対するデータのリード／ライトを制御する。磁気ディスク２０５は、磁気ディスクドライブ２０４の制御で書き込まれたデータを記憶する。

光ディスクドライブ２０６は、ＣＰＵ２０１の制御にしたがって光ディスク２０７に対するデータのリード／ライトを制御する。光ディスク２０７は、光ディスクドライブ２０６の制御で書き込まれたデータを記憶したり、光ディスク２０７に記憶されたデータをコンピュータに読み取らせたりする。

ディスプレイ２０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ２０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。

インターフェース（以下、「Ｉ／Ｆ」と略する。）２０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク２１４に接続され、このネットワーク２１４を介して他の装置に接続される。そして、Ｉ／Ｆ２０９は、ネットワーク２１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ２０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。

キーボード２１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス２１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。

スキャナ２１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ２１２は、ＯＣＲ（Ｏｐｔｉｃａｌ Ｃｈａｒａｃｔｅｒ Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ２１３は、画像データや文書データを印刷する。プリンタ２１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。

＜検証支援装置の機能的構成例＞
つぎに、実施の形態１にかかる検証支援装置の機能的構成例について説明する。

図３は、実施の形態１にかかる検証支援装置の機能的構成例を示すブロック図である。検証支援装置は、編集処理部３０１とチェッカーモジュール群ＣＭとを有する。編集処理部３０１は、選択部３１１と編集部３１２とを有する。編集処理部３０１（選択部３１１および編集部３１２）およびチェッカーモジュール群ＣＭは、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。

アサーション群３１０，３２０は、検証対象回路についてのアサーションの集合である。アサーション群３１０は、編集処理部３０１による編集前のアサーション群である。アサーション群３１０内のアサーションとは、たとえば、図１のアサーションＡ１，Ａ２において、「ｕｐｄａｔｅＲ＿ｓｐｅｃ」が挿入されていないアサーションである。一方、アサーション群３２０は、編集処理部３０１によりアサーション群３１０が編集された編集後のアサーション群である。アサーション群３２０内のアサーションとは、たとえば、図１のアサーションＡ１，Ａ２である。

選択部３１１は、アサーション群３１０の中から未選択のアサーションを選択する。選択部３１１は、未選択のアサーションがなくなるまで選択をつづける。編集部３１２は、選択部３１１によって選択されたアサーション（選択アサーション）に、検証対象回路内のレジスタの期待値の更新を指示する更新指示記述を挿入する。挿入された更新指示記述は期待値の更新サブルーチンを呼び出す記述である。

更新指示記述とは、たとえば、図１に示した「ｕｐｄａｔｅＲ＿ｓｐｅｃ」が挙げられる。「ｕｐｄａｔｅＲ＿ｓｐｅｃ」は、挿入先のアサーション内の「Ｒ＿ｓｐｅｃ」を更新するサブルーチンである。このように、編集部３１２では、選択アサーションごとに、更新指示記述を挿入することで、編集後のアサーション群３２０を生成することができる。編集済みのアサーション群３２０は、チェッカーモジュール群ＣＭに参照される。

チェッカーモジュール群ＣＭは、検証対象回路内のレジスタごとに用意されたｎ個（ｎはアサーションで定義されたレジスタ数）のチェッカーモジュールＣＭ１，…，ＣＭｉ，…，ＣＭｎである。チェッカーモジュールＣＭｉは、チェック対象のレジスタやアサーション（アサーション群３２０内のアサーション）が異なるだけで処理内容は同一である。

図４は、チェッカーモジュールの機能的構成例を示すブロック図である。チェッカーモジュールＣＭｉは、第１の検出部４０１と、更新部４０２と、第２の検出部４０３と、決定部４０４と、出力部４０５とを備えている。第１の検出部４０１〜出力部４０５は、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。

第１の検出部４０１は、単一のクロックＣｌｋで動作する検証対象回路が満たすべきレジスタＲの値を規定するアサーション群３２０の中から検証対象回路の模擬中に成立するアサーションを検出する。単一のクロックＣｌｋで動作すれば、検証対象回路全体でもよく、検証対象回路の一部の回路ブロックでもよい。第１の検出部４０１は、チェッカーモジュールＣＭｉで対象となるレジスタＲについて成立するアサーション（アサーション群３２０内のアサーション）を模擬中に検出する。たとえば、図１のように、第１の検出部４０１は、単一のクロックＣｌｋの時刻ｔ２において、アサーションＡ１，Ａ２のうちアサーションＡ１が成立したことを検出する。

更新部４０２は、第１の検出部４０１によってアサーションが検出されたクロックタイミングの次のクロックタイミングで、レジスタＲの期待値Ｒ＿ｓｐｅｃをアサーションで規定されたレジスタＲの値に更新する。具体的には、更新部４０２は、成立したアサーションの更新指示記述「ｕｐｄａｔｅＲ＿ｓｐｅｃ」を実行する期待値Ｒ＿ｓｐｅｃの更新サブルーチンである。これにより、期待値Ｒ＿ｓｐｅｃが、検出時刻の次の時刻で、模擬中のレジスタＲの値（すなわち、成立したアサーションでのレジスタＲの値）に更新される。したがって、更新部４０２による更新以降は、検証対象回路が正しく設計されていれば、アサーションが成立しない限り、レジスタＲの値と期待値Ｒ＿ｓｐｅｃは同一の値となるはずである。

第２の検出部４０３は、更新部４０２による更新後におけるレジスタＲの期待値Ｒ＿ｓｐｅｃとレジスタＲの値との不一致を検出する。具体的には、たとえば、第２の検出部４０３は、チェッカーモジュールＣＭｉで対象となるレジスタＲの値の変化をクロックＣｌｋの立ち上がり時刻ごとに（立ち下がり時刻ごとでもよい）監視する。これにより、検証対象回路が正しく設計されていれば、アサーション群３２０内のレジスタＲについてのいずれのアサーションも成立しない限り、レジスタＲの値と期待値Ｒ＿ｓｐｅｃは一致するはずである。一方、不一致となる場合は、レジスタＲは、アサーション群３２０で定義されていない変化をしたこととなる。

決定部４０４は、第２の検出部４０３によって検出された検出結果に基づいて、レジスタＲの値の変化の正否を決定する。具体的には、たとえば、決定部４０４は、第２の検出部４０３によって不一致が検出された場合、レジスタＲの値の変化が、アサーション群３２０で規定されていない変化（誤った変化）であると決定する。一方、第２の検出部４０３によって一致が検出された場合、レジスタＲの値の変化が、期待通りの変化（正しい変化）であると決定する。

なお、決定部４０４は、第２の検出部４０３によって不一致が検出された場合のみ、決定処理を実行することとしてもよい。第２の検出部４０３は毎時刻検出処理を実行するが、不一致の検出回数は一致の検出回数よりも少ないと考えられるため、不一致の場合のみ決定処理を実行することで検証支援処理の高速化を図ることができる。

出力部４０５は、決定部４０４によって決定された決定結果を出力する。具体的には、たとえば、出力部４０５は、決定部４０４によって誤った変化であると決定された場合、レジスタＲの不一致が検出された時刻とレジスタＲの識別情報を出力する。識別情報とは、レジスタＲを一意に特定する情報であり、たとえば、レジスタ名である。たとえば、図１の例では、出力部４０５は、｛ＮＧ，時刻ｔ５，Ｒ｝を出力する。

また、出力部４０５は、レジスタＲの不一致が検出された時刻の次サイクルとなる時刻とレジスタＲの識別情報を出力する。たとえば、図１の例では、出力部４０５は、｛ＮＧ，時刻ｔ６，Ｒ｝を出力する。このとき、レジスタＲの値も出力してもよい。この場合、出力部４０５は、｛ＮＧ，時刻ｔ６，Ｒ＝５｝を出力する。なお、出力部４０５は、決定部４０４によって正しい変化であると決定された場合、一致が検出された時刻とレジスタＲの識別情報を出力することとしてもよい。たとえば、図１の例では、出力部４０５は、｛ＯＫ，時刻ｔ３，Ｒ｝を出力する。

このような出力結果は、ディスプレイ２０８に表示してもよく、プリンタ２１３に印刷出力してもよく、通信可能なコンピュータに送信してもよい。また、検証支援装置内の記憶装置（ＲＡＭ２０３、磁気ディスク２０５）に格納してもよい。

＜編集処理手順＞
図５は、実施の形態１にかかる検証支援装置によるアサーション群３１０の編集処理手順を示すフローチャートである。選択部３１１は、アサーション群３１０の中から未選択のアサーションがあるか否かを判断する（ステップＳ５０１）。

未選択のアサーションがある場合（ステップＳ５０１：Ｙｅｓ）、選択部３１１は、アサーション群３１０の中から未選択のアサーションを１つ選択する（ステップＳ５０２）。そして、編集部３１２は、選択アサーションに期待値の更新サブルーチンを呼び出す更新指示記述を挿入する（ステップＳ５０３）。このあと、編集部３１２は、挿入後の選択アサーションを検証支援装置内の記憶装置に保持し（ステップＳ５０４）、ステップＳ５０１に戻る。

ステップＳ５０１において、未選択のアサーションがない場合は（ステップＳ５０１：Ｎｏ）、編集が完了したとして編集処理を終了する。これにより、未編集のアサーション群３１０から更新指示記述が挿入されたアサーション群３２０に編集されるため、チェッカーモジュール群ＣＭでのチェック処理においてアサーション成立時に自動的に期待値Ｒ＿ｓｐｅｃを更新することができる。

＜チェッカーモジュールＣＭｉによる検証対象回路の模擬中での期待値更新処理手順＞
図６は、チェッカーモジュールＣＭｉによる検証対象回路の模擬中での期待値更新処理手順を示すフローチャートである。

まず、第１の検出部４０１が、チェッカーモジュールＣＭｉで対象にしているレジスタＲについて、検証対象回路の模擬中に成立するアサーションがアサーション群３２０の中から検出されるまで待ち受ける（ステップＳ６０１：Ｎｏ）。検出された場合（ステップＳ６０１：Ｙｅｓ）、更新部４０２は、次のサイクル（次のクロックタイミング）で、検出アサーションのレジスタＲの値を期待値Ｒ＿ｓｐｅｃに更新する（ステップＳ６０２）。そして、ステップＳ６０１に戻る。図６のフローチャートは、検証対象回路の模擬が終了することで終了する。

＜チェッカーモジュールＣＭｉによる検証対象回路の模擬中での正否検出処理手順＞
図７は、チェッカーモジュールＣＭｉによる検証対象回路の模擬中での正否検出処理手順を示すフローチャートである。図７では、例としてクロックＣｌｋの立ち上がり時刻を検出することとするが、立ち下がり時刻でもよい。

まず、第２の検出部４０３は、クロックＣｌｋの立ち上がり時刻になるのを待ち受け（ステップＳ７０１：Ｎｏ）、立ち上がり時刻になると（ステップＳ７０１：Ｙｅｓ）、レジスタＲの値と期待値Ｒ＿ｓｐｅｃとが一致するか否かを判断する（ステップＳ７０２）。一致する場合（ステップＳ７０２：Ｙｅｓ）、ステップＳ７０１に戻る。

一方、不一致である場合（ステップＳ７０２：Ｎｏ）、決定部４０４は、次のサイクル（次のクロックタイミング）で、レジスタＲの値の変化はアサーション群３２０に規定されていない誤った変化であると決定する（ステップＳ７０３）。そして、出力部４０５は、決定結果を出力し（ステップＳ７０４）、ステップＳ７０１に戻る。図７のフローチャートは、検証対象回路の模擬が終了することで終了する。

このように、実施の形態１によれば、アサーションが成立する都度、期待値Ｒ＿ｓｐｅｃをレジスタＲの値に更新するため、更新後は、設計が正しければレジスタＲの値と期待値Ｒ＿ｓｐｅｃの値は一致し続ける。このため、レジスタＲの値と期待値Ｒ＿ｓｐｅｃの値との不一致を検出すれば、アサーション群３２０のいずれのアサーションも成立していないにもかかわらず、レジスタＲの値が変化したこととなる。

したがって、アサーション群３２０のいずれのアサーションでも規定されていない変化であることが判明するため、アサーション群では検出できないバグを効率的に検出することができる。そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタＲの値が変化しないことを保証することができる。

また、上述した実施の形態１の検証対象回路は単一のクロックＣｌｋで動作する回路としたが、検証対象回路が複数のクロックで動作する場合であっても、クロックドメインごとに検証対象とすることで、実施の形態１を適用することもできる。

（実施の形態２）
つぎに、実施の形態２について説明する。実施の形態１では、対象となるレジスタＲを動作させるクロックが１つだけである。このため、アサーションに更新指示記述を挿入すし、アサーション成立時に期待値Ｒ＿ｓｐｅｃを更新することで、『設計が正しければ、レジスタＲの値と期待値Ｒ＿ｓｐｅｃとは一致する』という状態にする。これにより、レジスタＲの値と期待値Ｒ＿ｓｐｅｃとが不一致であれば、期待通りではないレジスタＲの値の変化であるとして、アサーション群３２０のいずれのアサーションでも定義されていない誤った変化であることを検出していた。

これに対し、対象となるレジスタＲを動作させるクロックが複数ある場合、虚偽エラーが発生する。具体的には、実施の形態１のようにアサーション成立時刻の次の時刻で期待値Ｒ＿ｓｐｅｃを更新しようとすると、当該次の時刻が、アサーション成立時刻のクロックとは異なるクロックの場合、レジスタＲの値と期待値Ｒ＿ｓｐｅｃとが不一致となる。以下、図８で説明する。

＜虚偽エラー発生例＞
図８は、複数クロックの場合の虚偽エラー発生例を示す説明図である。図８において、レジスタＲについて、アサーションＡ１１，Ａ１２が規定されているものとする。アサーションＡ１１は、『クロックＣｌｋ１の立ち上がりにおいて、入力Ｉに「１」が入力されると１サイクル後にレジスタＲの値が「３」に変化する』ことをチェックするアサーションである。アサーションＡ１２は、『クロックＣｌｋ２の立ち上がりにおいて、入力Ｉに「２」が入力されると１サイクル後にレジスタＲの値が「４」に変化する』ことをチェックするアサーションである。

図８において、クロックＣｌｋ２の立ち上がり時刻ｔ２１において入力Ｉの値が「５」から「１」に変化した場合、クロックＣｌｋ２の立ち上がり時刻ｔ２２においてレジスタＲの値が「２」から「３」に変化している。このため、アサーションＡ１１が成立することとなる。そして、実施の形態１のように、レジスタＲの期待値Ｒ＿ｓｐｅｃを更新する次の時刻は、クロックＣｌｋ２の立ち上がり時刻ｔ２３である。

このため、クロックＣｌｋ２の立ち上がり時刻ｔ２２〜ｔ２３の間におけるクロックＣｌｋ１の立ち上がり時刻ｔ１４〜ｔ１７において、レジスタＲの値と期待値Ｒ＿ｓｐｅｃとの不一致（「３」≠「２」）が発生することとなる。すなわち、クロックＣｌｋ２の立ち上がり時刻ｔ２２〜ｔ２３の間では、アサーションＡ１１どおりに動作しているにもかかわらず、アサーションＡ１１を満たしていないとしてエラーを検出することとなる。

このため、実施の形態２では、検証対象回路内のレジスタＲが複数のクロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群３２０では検出できないバグを効率的に検出する例について説明する。なお、実施の形態２では、一例として、クロックの数を３（Ｃｌｋ１〜Ｃｌｋ３）として説明する。また、図９〜図１３では、エラーが発生しない例を説明し、図１４〜図１８では、エラーが検出できた例について説明する。

＜複数クロックでのエラー検出動作例１＞
図９〜図１３は、複数クロックでのエラー検出動作例１を示す説明図である。複数クロックでのエラー検出動作例１では、アサーションＡ２０が成立した場合に上述した虚偽エラーを発生させることなく、アサーションＡ２０の成立をチェックする動作例である。

図９は、初期状態を示している。図９において、同一のレジスタＲについてクロックごとに、相互チェッカーモジュールが用意されている。ＣｏＣｈｅｃｋｅｒ１（Ｒ，Ｃｌｋ１）は、レジスタＲがクロックＣｌｋ１で動作するときのアサーション成立を検出する相互チェッカーモジュールＣＣＭｉ１である。ＣｏＣｈｅｃｋｅｒ２（Ｒ，Ｃｌｋ２）は、レジスタＲがクロックＣｌｋ２で動作するときのアサーション成立を検出する相互チェッカーモジュールＣＣＭｉ２である。

ＣｏＣｈｅｃｋｅｒ３（Ｒ，Ｃｌｋ３）は、レジスタＲがクロックＣｌｋ３で動作するときのアサーション成立を検出する相互チェッカーモジュールＣＣＭｉ３である。このように、相互チェッカーモジュールは、同一のレジスタＲについてクロック数分生成される。

また、図９〜図１３では、例としてアサーションＡ２０が成立するか否かを検出するものとする。アサーションＡ２０は、『クロックＣｌｋ２の立ち上がりにおいて、入力Ｉに「１」が入力されると１サイクル後にレジスタＲの値が「３」に変化する』ことをチェックするアサーションである。

なお、アサーションＡ２０に挿入されている「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」は、挿入先のアサーションが成立した場合に呼び出されるサブルーチンである。「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」は、相互チェッカーモジュールＣＣＭｉ２に、そのチェックプロセスへアサーションＡ２０の成立通知『ＯＫ』を通知させる成立通知サブルーチンである。

図１０は、図９からの遷移状態を示している。図１０では、各相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３において、チェックプロセスＣＰｉ１〜ＣＰｉ３が始動した状態を示している。チェックプロセスＣＰｉ１〜ＣＰｉ３は、レジスタＲの値の変化が検出されると始動する。

図１０では、クロックＣｌｋ２の立ち上がり時刻ｔ２１において入力Ｉの値が「５」から「１」に変化したため、クロックＣｌｋ２の立ち上がり時刻ｔ２２においてレジスタＲの値が「２」から「３」に変化する。この振る舞いは、アサーションＡ２０を満たしている。クロックＣｌｋ２の時刻ｔ２２でレジスタＲの値が「２」から「３」に変化したため、チェックプロセスＣＰｉ１〜ＣＰｉ３は、クロックＣｌｋ２の時刻ｔ２２で始動する。

チェックプロセスＣＰｉ１〜ＣＰｉ３では、始動するとグローバル変数であるＣをインクリメントする。本例では相互チェッカーモジュール数は３であるため、Ｃ＝３となる。すなわち、グローバル変数であるＣは、同一レジスタＲを動作させるクロック数となる。なお、Ｃは順次デクリメントされていく。

Ｃがデクリメントされて、Ｃ＝０となる前に全チェックプロセスＣＰｉ１〜ＣＰｉ３が終了すると、図８に示した虚偽エラーが、アサーションＡ２０の成立時刻であるクロックＣｌｋ２の立ち上がり時刻ｔ２２から次の時刻ｔ２３までの間で発生することなく、アサーションＡ２０が成立したことを適性にチェックすることができたこととなる。一方、全チェックプロセスＣＰｉ１〜ＣＰｉ３終了時にＣ＝０になると、アサーション群のいずれのアサーションでも定義されていないレジスタＲの値の変化を検出したこととなる。

図１１は、図１０からの遷移状態を示している。図１１において、アサーションＡ２０の成立時刻であるｔ２２の次にレジスタＲを動作させる時刻は、クロックＣｌｋ１の時刻ｔ１４である。したがって、クロックＣｌｋ１での動作を監視している相互チェッカーモジュールＣＣＭｉ１では、アサーションＡ２０の成立通知『ＯＫ』を待ち受けるが、時刻ｔ１４では成立していない。このため、相互チェッカーモジュールＣＣＭｉ１では、時刻ｔ１４で成立通知『ＯＫ』を受け付けられないため、チェックプロセスＣＰｉ１は、Ｃをデクリメントして、Ｃ＝２となる。そして、チェックプロセスＣＰｉ１は終了する。

図１２は、図１１からの遷移状態を示している。図１２において、チェックプロセスＣＰｉ１の終了時刻となったクロックＣｌｋ１の立ち上がり時刻ｔ１４の次にレジスタＲを動作させる時刻は、クロックＣｌｋ１の立ち上がり時刻ｔ１５〜ｔ１７であるが、相互チェッカーモジュールＣＣＭｉ１のチェックプロセスＣＰｉ１はすでに終了している。このため、クロックＣｌｋ１の時刻ｔ１７の次にレジスタＲを動作させる時刻は、クロックＣｌｋ２の立ち上がり時刻ｔ２３となる。したがって、クロックＣｌｋ２での動作を監視している相互チェッカーモジュールＣＣＭｉ２では、アサーションＡ２０の成立通知『ＯＫ』を待ち受ける。

時刻ｔ２３は、アサーションＡ２０の成立時刻ｔ２２の次の時刻であるため、相互チェッカーモジュールＣＣＭｉ２の成立通知サブルーチン「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」が呼び出される。これにより、相互チェッカーモジュールＣＣＭｉ２は、チェックプロセスＣＰｉ２にアサーションＡ２０の成立通知『ＯＫ』を発行することで、チェックプロセスＣＰｉ２は、アサーションＡ２０の成立通知『ＯＫ』を受け付けることができる。成立通知『ＯＫ』を受け付けたチェックプロセスＣＰｉ２は、Ｃをデクリメントせず（Ｃ＝２のまま）終了する。

図１３は、図１２からの遷移状態を示している。図１３において、チェックプロセスＣＰｉ２の終了時刻となったクロックＣｌｋ２の時刻ｔ２３の次にレジスタＲを動作させる時刻は、クロックＣｌｋ３の立ち上がり時刻ｔ３２である。したがって、クロックＣｌｋ３での動作を監視している相互チェッカーモジュールＣＣＭｉ３では、アサーションＡ２０の成立通知『ＯＫ』を待ち受けるが、立ち上がり時刻ｔ３２では成立していない。

このため、相互チェッカーモジュールＣＣＭｉ３では、立ち上がり時刻ｔ３２で成立通知『ＯＫ』を受け付けられないため、チェックプロセスＣＰｉ３は、Ｃをデクリメントして、Ｃ＝１となる。そして、チェックプロセスＣＰｉ３は終了する。したがって、Ｃ＝０となる前に全チェックプロセスＣＰｉ１〜ＣＰｉ３が終了したこととなる。

このように、実施の形態２では、図８に示した虚偽エラーが、アサーションＡ２０の成立時刻であるクロックＣｌｋ２の立ち上がり時刻ｔ２２〜ｔ２３までの間で発生することなく、アサーションＡ２０が成立したことを適性にチェックすることができる。

＜複数クロックでのエラー検出動作例２＞
図１４〜図１８は、複数クロックでのエラー検出動作例２を示す説明図である。複数クロックでのエラー検出動作例２では、アサーションＡ２０が不成立である場合に上述した虚偽エラーを発生させることなく、アサーション群のいずれのアサーションでも定義されていないレジスタＲの値の変化を検出する動作例である。

図１４は、初期状態を示している。図１４において、同一のレジスタＲについてクロックごとに、相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３が用意されている。図９の初期状態と図１４の初期状態とで異なる箇所は、図９では、クロックＣｌｋ２の立ち上がり時刻ｔ２２でレジスタＲの値が「２」から「３」に変化するのに対し、図１４では、クロックＣｌｋ２の立ち上がり時刻ｔ２２でレジスタＲの値が「２」から「４」に変化する点である。

図１５は、図１４からの遷移状態を示している。図１５では、各相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３において、チェックプロセスＣＰｉ１〜ＣＰｉ３が始動した状態を示している。チェックプロセスＣＰｉ１〜ＣＰｉ３は、レジスタＲの値の変化が検出されると始動する。

図１５では、クロックＣｌｋ２の立ち上がり時刻ｔ２１において入力Ｉの値が「５」から「１」に変化したため、クロックＣｌｋ２の立ち上がり時刻ｔ２２においてレジスタＲの値が「２」から「４」に変化する。この振る舞いは、アサーションＡ２０を満たしていない。クロックＣｌｋ２の立ち上がり時刻ｔ２２でレジスタＲの値が「２」から「４」に変化したため、チェックプロセスＣＰｉ１〜ＣＰｉ３は、クロックＣｌｋ２の立ち上がり時刻ｔ２２で始動する。

チェックプロセスＣＰｉ１〜ＣＰｉ３では、始動するとグローバル変数であるＣをインクリメントする。本例では相互チェッカーモジュール数は３であるため、Ｃ＝３となる。すなわち、グローバル変数であるＣは、同一レジスタＲを動作させるクロック数となる。なお、Ｃは順次デクリメントされていく。

Ｃがデクリメントされて、Ｃ＝０となる前に全チェックプロセスＣＰｉ１〜ＣＰｉ３が終了すると、図８に示した虚偽エラーが、アサーションＡ２０の成立時刻であるクロックＣｌｋ２の立ち上がり時刻ｔ２２から次の時刻ｔ２３までの間で発生することなく、アサーションＡ２０が成立したことを適性にチェックすることができたこととなる。一方、全チェックプロセスＣＰｉ１〜ＣＰｉ３終了時にＣ＝０になると、アサーション群のいずれのアサーションでも定義されていないレジスタＲの値の変化を検出したこととなる。

図１６は、図１５からの遷移状態を示している。図１６において、レジスタＲの値が変化した時刻ｔ２２の次にレジスタＲを動作させる時刻は、クロックＣｌｋ１の立ち上がり時刻ｔ１４である。したがって、クロックＣｌｋ１での動作を監視している相互チェッカーモジュールＣＣＭｉ１では、アサーションＡ２０の成立通知『ＯＫ』を待ち受けるが、時刻ｔ１４では成立していない。このため、相互チェッカーモジュールＣＣＭｉ１では、時刻ｔ１４で成立通知『ＯＫ』を受け付けられないため、チェックプロセスＣＰｉ１は、Ｃをデクリメントして、Ｃ＝２となる。そして、チェックプロセスＣＰｉ１は終了する。

図１７は、図１６からの遷移状態を示している。図１７において、チェックプロセスＣＰｉ１の終了時刻となった時刻ｔ１４の次にレジスタＲを動作させる時刻は、クロックＣｌｋ１の時刻ｔ１５〜ｔ１７であるが、相互チェッカーモジュールＣＣＭｉ１のチェックプロセスＣＰｉ１はすでに終了している。このため、クロックＣｌｋ１の立ち上がり時刻ｔ１７の次にレジスタＲを動作させる時刻は、クロックＣｌｋ２の立ち上がり時刻ｔ２３となる。したがって、クロックＣｌｋ２での動作を監視している相互チェッカーモジュールＣＣＭｉ２では、アサーションＡ２０の成立通知『ＯＫ』を待ち受ける。

時刻ｔ２３は、クロックＣｌｋ２でレジスタＲが変化した時刻ｔ２２の次の時刻であるが、アサーションＡ２０が不成立である。したがって、相互チェッカーモジュールＣＣＭｉ２では、時刻ｔ２３で成立通知『ＯＫ』を受け付けられないため、チェックプロセスＣＰｉ２は、Ｃをデクリメントして、Ｃ＝１となる。そして、チェックプロセスＣＰｉ２は終了する。

図１８は、図１７からの遷移状態を示している。図１８において、チェックプロセスＣＰｉ２の終了時刻となった時刻ｔ２３の次にレジスタＲを動作させる時刻は、クロックＣｌｋ３の時刻ｔ３２である。したがって、クロックＣｌｋ３での動作を監視している相互チェッカーモジュールＣＣＭｉ３では、アサーションＡ２０の成立通知『ＯＫ』を待ち受けるが、時刻ｔ３２では成立していない。このため、相互チェッカーモジュールＣＣＭｉ３では、時刻ｔ３２で成立通知『ＯＫ』を受け付けられないため、チェックプロセスＣＰｉ３は、Ｃをデクリメントして、Ｃ＝０となる。そして、チェックプロセスＣＰｉ３は終了する。

このように、全チェックプロセスＣＰｉ１〜ＣＰｉ３終了時にＣ＝０になったため、クロックＣｌｋ２の立ち上がり時刻ｔ２２において、アサーション群のいずれのアサーションでも定義されていないレジスタＲの値の変化を検出したこととなる。これにより、検証対象回路内のレジスタが複数クロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群では検出できないバグを効率的に検出することができる。

＜検証支援装置の機能的構成例＞
つぎに、実施の形態２にかかる検証支援装置の機能的構成例について説明する。なお、実施の形態１と同一構成には同一符号を付し、その説明を省略する。また、実施の形態２にかかる検証支援装置のハードウェア構成例は、図２と同一構成であるため省略する。

図１９は、実施の形態２にかかる検証支援装置の機能的構成例を示すブロック図である。検証支援装置は、編集／作成処理部１９００と相互チェッカーモジュール群集合ＣＣＭとを有する。編集／作成処理部１９００は、選択部１９０１と編集部１９０２と特定部１９０３と作成部１９０４とを有する。

編集／作成処理部１９００（選択部１９０１〜作成部１９０４）および相互チェッカーモジュール群集合ＣＣＭは、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。

アサーション群１９１０は、編集／作成処理部１９００による編集前のアサーション群である。アサーション群１９１０内のアサーションとは、たとえば、図９のアサーションＡ２０において、「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」が挿入されていないアサーションである。一方、アサーション群１９２０は、編集／作成処理部１９００によりアサーション群１９１０が編集された編集後のアサーション群である。アサーション群１９２０内のアサーションとは、たとえば、図９のアサーションＡ２０である。

選択部１９０１は、アサーション群１９１０の中から未選択のアサーションを選択する。選択部１９０１は、未選択のアサーションがなくなるまで選択をつづける。編集部１９０２は、選択部１９０１によって選択されたアサーション（選択アサーション）に、アサーション成立を通知する成立通知に関する記述を挿入する。挿入された成立通知に関する記述は、アサーション成立をチェックプロセスに通知させるサブルーチンを呼び出す記述である。

成立通知に関する記述とは、たとえば、図９に示した「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」が挙げられる。「ＣｏＣｈｅｃｋｅｒ２．ｔｒｉｇｇｅｒＯＫ」は、挿入先のアサーションが成立した場合に、「ＣｏＣｈｅｃｋｅｒ２」に、「ＣｏＣｈｅｃｋｅｒ２」へ「ＯＫ」を発行させるサブルーチンである。

一般的に、クロックＣｌｋ＃の立ち上がり（または立ち下がり）でのアサーション成立について相互チェッカーモジュールＣＣＭｉ＃に通知させたい場合は、「ＣｏＣｈｅｃｋｅｒ＃．ｔｒｉｇｇｅｒＯＫ」とすればよい。このように、編集部１９０２では、アサーションごとに、成立通知に関する記述を挿入することで、編集後のアサーション群１９２０を生成することができる。編集済みのアサーション群１９２０は、相互チェッカーモジュール群集合ＣＣＭに参照される。

特定部１９０３は、サブルーチン挿入後のアサーションから、レジスタの識別情報とクロックの識別情報とを特定する。レジスタの識別情報とは、レジスタを一意に特定する情報であり、たとえば、レジスタ名である。クロックの識別情報とは、クロックを一意に特定する情報であり、たとえば、クロック名である。たとえば、選択アサーションがアサーションＡ２０の場合、レジスタ名として「Ｒ」、クロック名として「Ｃｌｋ２」を特定する。

作成部１９０４は、特定部１９０３によって特定されたレジスタの識別情報とクロックの識別情報に基づいて、相互チェッカーモジュール群を作成する。具体的には、たとえば、クロックの総数は既知（ここでは、Ｃｌｋ１〜Ｃｌｋ３の３個）であるため、クロック名「Ｃｌｋ２」が特定されると、特定されたレジスタＲについて、相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３を作成する。なお、作成部１９０４は、あらかじめ相互チェッカーモジュールＣＣＭｉの動作記述をテンプレートして保持しているため、レジスタ名とクロック名をテンプレートに与えるだけで作成することができる。

相互チェッカーモジュール群集合ＣＣＭは、相互チェッカーモジュール群ＣＣＭ１，…，ＣＣＭｉ，…，ＣＣＭｎである。ｎは、アサーションで定義されたレジスタ数である。相互チェッカーモジュール群ＣＣＭｉは、チェック対象のレジスタやアサーション（アサーション群１９２０内のアサーション）が異なるだけで処理内容は同一である。

＜相互チェッカーモジュールの機能的構成例＞
図２０は、相互チェッカーモジュール群ＣＣＭｉの機能的構成例を示すブロック図である。相互チェッカーモジュール群ＣＣＭｉは、第１の検出部２００１と、第２の検出部２００２と、判断部２００３と、生成部２００４と、決定部２００５と、出力部２００６とを備えている。

第１の検出部２００１〜出力部２００６は、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。

第１の検出部２００１は、複数のクロックで動作する回路が回路内のレジスタＲについて複数のクロックのうちいずれかのクロックのタイミングで満たすべきレジスタＲの値を規定するアサーション群の中から、回路の模擬中に成立するアサーションを検出する。

具体的には、たとえば、クロックＣｌｋ１〜Ｃｌｋ３という３つのクロックにより内部のレジスタＲを動作させる検証対象回路についてのアサーション群１９２０の中から、シミュレーション中に成立するアサーションを検出する。たとえば、図２０に示したように、第１の検出部２００１は、アサーション群１９２０の中から、クロックＣｌｋ２の時刻ｔ２２で成立するアサーションＡ２０を検出する。

第２の検出部２００２は、レジスタＲの値の変化を検出する。ここでいうレジスタＲの値の変化は、アサーション成立の場合であるか否かを問わない。たとえば、第２の検出部２００２は、図１０に示したように、相互チェッカーモジュールＣＣＭｉ２によりクロックＣｌｋ２の時刻ｔ２２でのレジスタＲの値の変化（「２」→「３」）を検出する。同様に、第２の検出部２００２は、図１５に示したように、相互チェッカーモジュールＣＣＭｉ２によりクロックＣｌｋ２の時刻ｔ２２でのレジスタＲの値の変化（「２」→「４」）を検出する。

判断部２００３は、複数のクロックの各々のクロックにおいて、第２の検出部２００２によってレジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該時刻となるクロックと第１の検出部２００１によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する。具体的には、たとえば、判断部２００３は、第１の検出部２００１によってアサーションの成立を検出していない場合は、実行されない。すなわち、図１４〜図１８の例では、判断部２００３は実行されない。

一方、図９〜図１３の例では、図１０の状態でアサーションＡ２０の成立が検出されている。したがって、判断部２００３は、図１１に示したように、クロックＣｌｋ１において、レジスタＲの値の変化が検出された時刻ｔ２２以降で最初に到来する時刻ｔ１４が、成立したアサーションＡ２０で規定されたクロックＣｌｋ２と同一クロックであるか否かを判断する。時刻ｔ１４はクロックＣｌｋ１に属しているため、成立したアサーションＡ２０で規定されたクロックＣｌｋ２とは同一クロックではない。

同様に、判断部２００３は、図１２に示したように、クロックＣｌｋ２において、レジスタＲの値の変化が検出された時刻ｔ２２以降で最初に到来する時刻ｔ２３が、成立したアサーションＡ２０で規定されたクロックＣｌｋ２と同一クロックであるか否かを判断する。時刻ｔ２３はクロックＣｌｋ２に属しているため、成立したアサーションＡ２０で規定されたクロックＣｌｋ２とは同一クロックとなる。

また、判断部２００３は、図１３に示したように、クロックＣｌｋ３において、レジスタＲの値の変化が検出された時刻ｔ２２以降で最初に到来する時刻ｔ３２が、成立したアサーションＡ２０で規定されたクロックＣｌｋ２と同一クロックであるか否かを判断する。時刻ｔ３２はクロックＣｌｋ３に属しているため、成立したアサーションＡ２０で規定されたクロックＣｌｋ２とは同一クロックではない。

生成部２００４は、第２の検出部２００２によってレジスタＲの値の変化が検出された場合、レジスタＲについてクロックごとにアサーション成立を通知する成立通知を待ち受けるチェックプロセス群を生成する。具体的には、たとえば、図９〜図１８に示したように、相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３ごとにチェックプロセスＣＰｉ１〜ＣＰｉ３を生成する。チェックプロセスＣＰｉ１〜ＣＰｉ３が生成されると、それぞれグローバル変数Ｃをインクリメントする。これにより、クロックＣｌｋ１〜Ｃｌｋ３の総数ｍ＝Ｃとなる。

このあと、図９〜図１３の場合、判断部２００３によって同一クロックであると判断されると、判断されたアサーションに挿入されている成立通知に関する記述で指定されたサブルーチンが呼び出される。そして、相互チェッカーモジュールＣＣＭｉ１〜ＣＣＭｉ３のうち、同一クロックとなったクロックＣｌｋ２に関する相互チェッカーモジュールＣＣＭｉ２は、呼び出された成立通知サブルーチンが実行されることで、成立通知を受け付けることができる。

なお、図１４〜図１８の例では、アサーションが成立していないため判断部２００３で同一クロックであると判断されることはない。なお、図９〜図１３の例および図１４〜図１８の例のいずれにおいても、同一クロックでないと判断される都度、グローバル変数Ｃはデクリメントされる。

決定部２００５は、判断部２００３によって判断された判断結果に基づいて、レジスタＲの値の変化の正否を決定する。具体的には、たとえば、判断部２００３による同一クロックの判断で、クロックＣｌｋ１〜ＣｌｋｍのうちいずれかのクロックＣｌｋｊで同一であると判断された場合、グローバル変数Ｃは、デクリメントされてもＣ＝０にはならないため、レジスタＲの値の変化は、期待通りの正しい変化であると決定する。

たとえば、図９〜図１３の例で示したように、クロックＣｌｋ２の時刻ｔ２３で成立したアサーションＡ２０のクロックＣｌｋ２と同一クロックと判断されるため、クロックＣｌｋ２の時刻ｔ２２でのレジスタＲの値の変化は、（アサーションＡ２０に従った）期待通りの正しい変化であると決定する。

一方、判断部２００３による同一クロックの判断で、どのクロックＣｌｋ１〜Ｃｌｋｍも同一でないと判断された場合、グローバル変数Ｃは、デクリメントされて最終的にＣ＝０にはなる。したがって、レジスタＲの値の変化は、いずれのアサーションでも定義されていない誤った変化であると決定する。

たとえば、図１４〜図１８の例で示したように、クロックＣｌｋ２の時刻ｔ２２でのレジスタＲの値の変化ではアサーションＡ２０が成立していないため、アサーションＡ２０に挿入されている成立通知に関する記述から成立通知サブルーチンを呼び出せないこととなる。したがって、Ｃはその都度、デクリメントされ、最終的にＣ＝０となる。これにより、クロックＣｌｋ２の時刻ｔ２２でのレジスタＲの値の変化は、いずれのアサーションでも定義されていない誤った変化であると決定する。

出力部２００６は、決定部２００５によって決定された決定結果を出力する。具体的には、たとえば、出力部２００６は、決定部２００５によって誤った変化であると決定された場合、レジスタＲの値の変化を検出したクロックおよび変化したクロックタイミングとレジスタＲの識別情報を出力する。識別情報とは、レジスタＲを一意に特定する情報であり、たとえば、レジスタ名である。たとえば、図１４〜図１８の例では、出力部２００６は、｛ＮＧ，クロックＣｌｋ２，時刻ｔ２２，Ｒ｝を出力する。このとき、レジスタＲの値も出力してもよい。この場合、出力部２００６は、｛ＮＧ，クロックＣｌｋ２，時刻ｔ２２，Ｒ＝４｝を出力する。

また、出力部２００６は、決定部２００５によって正しい変化であると決定された場合、レジスタＲの値の変化を検出したクロックおよび変化したクロックタイミングとレジスタＲの識別情報とを出力することとしてもよい。たとえば、図９〜図１３の例では、出力部２００６は、｛ＯＫ，クロックＣｌｋ２，時刻ｔ２２，Ｒ｝を出力する。このとき、レジスタＲの値も出力してもよい。この場合、出力部２００６は、｛ＯＫ，クロックＣｌｋ２，時刻ｔ２２，Ｒ＝３｝を出力する。

また、出力部２００６は、決定部２００５によって正しい変化であると決定された場合、レジスタＲの値の変化を検出したクロック、成立通知『ＯＫ』を受け付けた時刻と、レジスタＲの識別情報とを出力することとしてもよい。たとえば、図９〜図１３の例では、出力部２００６は、｛ＯＫ，クロックＣｌｋ２，時刻ｔ２３，Ｒ｝を出力する。このとき、レジスタＲの値も出力してもよい。この場合、出力部２００６は、｛ＯＫ，クロックＣｌｋ２，時刻ｔ２３，Ｒ＝３｝を出力する。

このような出力結果は、ディスプレイ２０８に表示してもよく、プリンタ２１３に印刷出力してもよく、通信可能なコンピュータに送信してもよい。また、検証支援装置内の記憶装置に格納してもよい。

＜編集／作成処理手順＞
図２１は、実施の形態２にかかる検証支援装置による編集／作成処理手順を示すフローチャートである。選択部１９０１は、アサーション群１９１０の中から未選択のアサーションがあるか否かを判断する（ステップＳ２１０１）。

未選択のアサーションがある場合（ステップＳ２１０１：Ｙｅｓ）、選択部１９０１は、アサーション群１９１０の中から未選択のアサーションを１つ選択する（ステップＳ１９０２）。そして、編集部１９０２は、成立通知を通知させる成立通知サブルーチンを呼び出す成立通知に関する記述を、選択アサーションに挿入する（ステップＳ２１０３）。このあと、編集部１９０２は、挿入後の選択アサーションを検証支援装置内の記憶装置に保持する（ステップＳ２１０４）。

また、特定部１９０３は、選択アサーションから、選択アサーションで規定されているクロックの識別情報とレジスタの識別情報を特定する（ステップＳ２１０５）。そして、作成部１９０４は、特定されたクロックの識別情報とレジスタの識別情報とについて、チェッカーモジュール群ＣＣＭｉを作成済みであるか否かを判断する（ステップＳ２１０６）。

作成済みである場合（ステップＳ２１０６：Ｙｅｓ）、ステップＳ２１０１に戻る。一方、作成済みでない場合（ステップＳ２１０６：Ｎｏ）、作成部１９０４は、特定されたクロックの識別情報とレジスタの識別情報とについて、チェッカーモジュール群ＣＣＭｉを作成し、記憶装置に保持する（ステップＳ２１０７）。このあと、ステップＳ２１０１に移行する。

そして、ステップＳ２１０１において、未選択のアサーションがない場合（ステップＳ２１０１：Ｎｏ）、編集／作成処理を終了する。これにより、未編集のアサーション群１９１０から成立通知に関する記述が挿入されたアサーション群１９２０に編集されるため、相互チェッカーモジュール群集合ＣＣＭでのチェック処理においてアサーションが成立した場合、虚偽エラーを発生することなく、レジスタＲの値の変化の正否を特定することができる。

＜相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中での成立通知処理手順＞
図２２は、相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中での成立通知処理手順を示すフローチャートである。

まず、第１の検出部２００１が、相互チェッカーモジュール群ＣＣＭｉで対象にしているレジスタＲについて、検証対象回路の模擬中に成立するアサーションがアサーション群１９２０の中から検出されるまで待ち受ける（ステップＳ２２０１：Ｎｏ）。検出された場合（ステップＳ２２０１：Ｙｅｓ）、成立したアサーションに記述されている成立通知サブルーチンを読み出すことで、相互チェッカーモジュールＣＣＭｉｊは、自身のチェックプロセスＣＰｉｊに、成立通知『ＯＫ』を通知する（ステップＳ２２０２）。そして、ステップＳ２２０１に戻る。図２２のフローチャートは、検証対象回路の模擬が終了することで終了する。

＜相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中でのチェックプロセスＣＰｉｊの始動処理手順＞
図２３は、相互チェッカーモジュールＣＣＭｉｊによる検証対象回路の模擬中でのチェックプロセスＣＰｉｊの始動処理手順を示すフローチャートである。まず、第２の検出部２００２が、相互チェッカーモジュール群ＣＣＭｉで対象にしているレジスタＲの値が変化するまで待ち受ける（ステップＳ２３０１：Ｎｏ）。レジスタＲの値の変化が検出された場合（ステップＳ２３０１：Ｙｅｓ）、相互チェッカーモジュールＣＣＭｉｊはチェックプロセスＣＰｉｊを始動する（ステップＳ２３０２）。

そして、グローバル変数Ｃをインクリメントする（ステップＳ２３０３）。相互チェッカーモジュールＣＣＭｉｊはクロック総数ｍ個存在するため、各々の相互チェッカーモジュールＣＣＭｉｊでインクリメントされることで、Ｃ＝ｍとなる。これにより、チェックプロセスＣＰｉｊの始動処理が終了する。

＜チェックプロセスＣＰｉｊの実行処理手順＞
図２４は、図２３で始動されたチェックプロセスＣＰｉｊの実行処理手順を示すフローチャートである。図２４では、例としてクロックＣｌｋの立ち上がり時刻を検出することとするが、立ち下がり時刻でもよい。

まず、第２の検出部２００２は、クロックＣｌｋの立ち上がり時刻になるのを待ち受け（ステップＳ２４０１：Ｎｏ）、立ち上がり時刻になると（ステップＳ２４０１：Ｙｅｓ）、相互チェッカーモジュールＣＣＭｉｊから成立通知『ＯＫ』が受信されたか否かを判断する（ステップＳ２４０２）。受信された場合（ステップＳ２４０２：Ｙｅｓ）、グローバル変数Ｃをデクリメントせずに、チェックプロセスＣＰｉｊを終了する（ステップＳ２４０７）。

一方、受信されなかった場合（ステップＳ２４０２：Ｎｏ）、判断部２００３は、グローバル変数Ｃをデクリメントし（ステップＳ２４０３）、デクリメント後のＣがＣ＞０であるか否かを判断する（ステップＳ２４０４）。Ｃ＞０である場合（ステップＳ２４０４：Ｙｅｓ）、ステップＳ２４０７に移行して、チェックプロセスＣＰｉｊを終了する（ステップＳ２４０７）。

一方、Ｃ＞０でない場合（ステップＳ２４０４：Ｎｏ）、決定部２００５は、レジスタＲの値の変化は、いずれのアサーションにも定義されていない誤った変化であると決定する（ステップＳ２４０５）。そして、出力部２００６は、決定部２００５によって決定された決定結果を出力して（ステップＳ２４０６）、チェックプロセスＣＰｉｊを終了する（ステップＳ２４０７）。

このように、実施の形態２によれば、アサーションが成立する都度、相互チェッカーモジュールＣＣＭｉｊごとにチェックプロセスＣＰｉｊを始動させて、成立通知を待ち受けさせる。そして、１つでも成立通知を受けたチェックプロセスＣＰｉｊが存在する場合は、レジスタＲの値の変化は、アサーションに従った期待通りの変化であることが保証される。一方、成立通知を受けたチェックプロセスＣＰｉｊが１つも存在しない場合は、レジスタＲの値の変化は、いずれのアサーションにも規定されていない誤った変化であることが判明する。

このように、実施の形態２では、アサーションが成立した場合には、図８に示したような虚偽エラーが発生することなく、アサーションが成立したことを適性にチェックすることができる。また、アサーションが成立せずに、単にレジスタＲの値が変化した場合には、アサーション群のいずれのアサーションでも定義されていないレジスタＲの値の変化を検出することができる。

これにより、検証対象回路内のレジスタＲが複数のクロックで動作する場合であっても、上述した虚偽エラーを発生させずに、アサーション群では検出できないバグを効率的に検出することができる。そして、検証者が、特定されたバグについてデバッグをおこなうことで、検証対象回路についてアサーション外でレジスタＲの値が変化しないことを保証することができる。

なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本検証支援プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。

上述した実施の形態に関し、さらに以下の付記を開示する。

（付記１）回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
前記第１の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、
前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出工程と、
前記第２の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
前記決定工程によって決定された決定結果を出力する出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。

（付記２）前記決定工程は、
前記第２の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との不一致が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記１に記載の検証支援プログラム。

（付記３）前記決定工程は、
前記第２の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との一致が検出された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記１または２に記載の検証支援プログラム。

（付記４）前記出力工程は、
前記レジスタの不一致が検出されたクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記１〜３のいずれか一つに記載の検証支援プログラム。

（付記５）前記出力工程は、
前記レジスタの不一致が検出されたクロックタイミングの次のクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記１〜３のいずれか一つに記載の検証支援プログラム。

（付記６）前記第１の検出工程、前記更新工程、前記第２の検出工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする付記１〜５のいずれか一つに記載の検証支援プログラム。

（付記７）前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、
前記選択工程によって選択されたアサーションごとに、前記レジスタの期待値の更新を指示する更新指示記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、
前記第１の検出工程は、
前記編集工程による編集後のアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、
前記更新工程は、
前記第１の検出工程によって検出されたアサーションに挿入されている前記更新指示記述に従って、前記レジスタの期待値を、前記第１の検出工程によって検出されたアサーションで定義されているレジスタの値に更新することを特徴とする付記１〜６のいずれか一つに記載の検証支援プログラム。

（付記８）回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
前記レジスタの値の変化を検出する第２の検出工程と、
前記複数のクロックの各々のクロックにおいて、前記第２の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第１の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、
前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
前記決定工程によって決定された決定結果を出力する出力工程と、
をコンピュータに実行させることを特徴とする検証支援プログラム。

（付記９）前記決定工程は、
前記判断工程によって、前記複数のクロックのいずれかのクロックにおいて前記アサーションで規定されたクロックと同一クロックであると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記８に記載の検証支援プログラム。

（付記１０）前記決定工程は、
前記第１の検出工程によって、前記回路の模擬中に成立するアサーションが検出されておらず、かつ、前記第２の検出工程によって、前記レジスタの値の変化が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記８または９に記載の検証支援プログラム。

（付記１１）前記第２の検出工程によって前記レジスタの値の変化が検出された場合、前記レジスタについてクロックごとにアサーション成立を通知する成立通知を待ち受けるチェックプロセス群を生成する生成工程を前記コンピュータに実行させ、
前記判断工程は、
前記生成工程によって生成されたチェックプロセス群のうち、前記アサーションから前記成立通知を受けたチェックプロセスの有無を判断することを特徴とする付記８に記載の検証支援プログラム。

（付記１２）前記決定工程は、
前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがあると判断された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする付記１１に記載の検証支援プログラム。

（付記１３）前記決定工程は、
前記判断工程によって、前記アサーションから前記成立通知を受けたチェックプロセスがないと判断された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする付記１１または１２に記載の検証支援プログラム。

（付記１４）前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、
前記選択工程によって選択されたアサーションごとに、前記成立通知に関する記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、
前記第１の検出工程は、
前記編集工程による編集後のアサーション群の中から、前記回路の模擬中に成立するアサーションを検出することを特徴とする付記１０〜１２のいずれか一つに記載の検証支援プログラム。

（付記１５）前記出力工程は、
前記レジスタの値の変化があったクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記８〜１４のいずれか一つに記載の検証支援プログラム。

（付記１６）前記出力工程は、
前記レジスタの値の変化があったクロックタイミングの次のクロックタイミングと前記レジスタの識別情報を出力することを特徴とする付記８〜１４のいずれか一つに記載の検証支援プログラム。

（付記１７）前記第１の検出工程、前記第２の検出工程、前記判断工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする付記８〜１６のいずれか一つに記載の検証支援プログラム。

（付記１８）回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出手段と、
前記第１の検出手段によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新手段と、
前記更新手段による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出手段と、
前記第２の検出手段によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、
前記決定手段によって決定された決定結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。

（付記１９）回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第１の検出手段と、
前記レジスタの値の変化を検出する第２の検出手段と、
前記複数のクロックの各々のクロックにおいて、前記第２の検出手段によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第１の検出手段によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断手段と、
前記判断手段によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、
前記決定手段によって決定された決定結果を出力する出力手段と、
を備えることを特徴とする検証支援装置。

（付記２０）コンピュータが、
回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
前記第１の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、
前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出工程と、
前記第２の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
前記決定工程によって決定された決定結果を出力する出力工程と、
を実行することを特徴とする検証支援方法。

（付記２１）コンピュータが、
回路内の複数のクロックで動作するレジスタについて前記複数のクロックのうちいずれかのクロックのクロックタイミングで満たすべき前記レジスタの値を規定するアサーション群の中から、前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
前記レジスタの値の変化を検出する第２の検出工程と、
前記複数のクロックの各々のクロックにおいて、前記第２の検出工程によって前記レジスタの値の変化が検出されたクロックタイミング以降で最初に到来するクロックタイミングごとに、当該クロックタイミングとなるクロックと前記第１の検出工程によって検出されたアサーションで規定されたクロックとが同一クロックであるか否かを判断する判断工程と、
前記判断工程によって判断された判断結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
前記決定工程によって決定された決定結果を出力する出力工程と、
を実行することを特徴とする検証支援方法。

３０１ 編集処理部
３１１ 選択部
３１２ 編集部
４０１ 第１の検出部
４０２ 更新部
４０３ 第２の検出部
４０４ 決定部
４０５ 出力部
１９００ 編集／作成処理部
１９０１ 選択部
１９０２ 編集部
１９０３ 特定部
１９０４ 作成部
２００１ 第１の検出部
２００２ 第２の検出部
２００３ 判断部
２００４ 生成部
２００５ 決定部
２００６ 出力部

Claims (7)

1. 回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
   前記第１の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、
   前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出工程と、
   前記第２の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
   前記決定工程によって決定された決定結果を出力する出力工程と、
   をコンピュータに実行させることを特徴とする検証支援プログラム。
2. 前記決定工程は、
   前記第２の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との不一致が検出された場合、前記レジスタの値の変化が、前記アサーション群で規定されていない変化であると決定することを特徴とする請求項１に記載の検証支援プログラム。
3. 前記決定工程は、
   前記第２の検出工程によって、前記更新後における前記レジスタの期待値と前記レジスタの値との一致が検出された場合、前記レジスタの値の変化が、期待通りの変化であると決定することを特徴とする請求項１または２に記載の検証支援プログラム。
4. 前記第１の検出工程、前記更新工程、前記第２の検出工程、および前記決定工程を前記回路内のレジスタごとに前記コンピュータに実行させることを特徴とする請求項１〜３のいずれか一つに記載の検証支援プログラム。
5. 前記アサーション群の中から未選択のアサーションを順次選択する選択工程と、
   前記選択工程によって選択されたアサーションごとに、前記レジスタの期待値の更新を指示する更新指示記述を挿入することにより、前記アサーション群を編集する編集工程と、を前記コンピュータに実行させ、
   前記第１の検出工程は、
   前記編集工程による編集後のアサーション群の中から前記回路の模擬中に成立するアサーションを検出し、
   前記更新工程は、
   前記第１の検出工程によって検出されたアサーションに挿入されている前記更新指示記述に従って、前記レジスタの期待値を、前記第１の検出工程によって検出されたアサーションで定義されているレジスタの値に更新することを特徴とする請求項１〜４のいずれか一つに記載の検証支援プログラム。
6. 回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出手段と、
   前記第１の検出手段によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新手段と、
   前記更新手段による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出手段と、
   前記第２の検出手段によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定手段と、
   前記決定手段によって決定された決定結果を出力する出力手段と、
   を備えることを特徴とする検証支援装置。
7. コンピュータが、
   回路が満たすべきレジスタの値を規定するアサーション群の中から前記回路の模擬中に成立するアサーションを検出する第１の検出工程と、
   前記第１の検出工程によって前記アサーションが検出されたクロックタイミングの次のクロックタイミングで、前記レジスタの期待値を前記アサーションで規定された前記レジスタの値に更新する更新工程と、
   前記更新工程による更新後における前記レジスタの期待値と前記レジスタの値との不一致を検出する第２の検出工程と、
   前記第２の検出工程によって検出された検出結果に基づいて、前記レジスタの値の変化の正否を決定する決定工程と、
   前記決定工程によって決定された決定結果を出力する出力工程と、
   を実行することを特徴とする検証支援方法。

Images