(57)【要約】【課題】回路規模が大きくても、高い検証精度で、回路動作が正常であるかどうかを検証することができるようにする。【解決手段】回路分割部３０によって、検証対象の非同期回路を分割した複数のブロック回路に分割する。第１形式検証部３２によって、ブロック回路データに対して、回路動作の形式検証を行う。モデル生成部３４によって、回路動作が正常であることが検証された複数のブロック回路データの各々について、入力端に接続されている２段分のフリップフロップと、出力端に接続されている１段分のフリップフロップと、残りの回路部分を表わす不明回路部とを用いて記述された検証用モデルを生成する。第２形式検証部３６によって、検証用モデルを組み合わせた、検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う。【選択図】図２
2011002903.tif 000002
【特許請求の範囲】
【請求項１】
検証対象の非同期回路を分割した複数の分割回路の各々を記述した、クロック情報を含む分割回路データに対して、回路動作の形式検証を行う第１形式検証手段と、
前記第１形式検証手段によって回路動作が正常であることが検証された前記複数の分割回路データの各々について生成された、前記分割回路の入力部に２段以上のフリップフロップが接続されている場合の前記２段以上のフリップフロップと、出力部に１段以上のフリップフロップが接続されている場合の前記１段以上のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述され、前記２段以上のフリップフロップ及び前記１段以上のフリップフロップに入力されるクロック情報と、前記不明回路部に入力される信号と同期したクロック情報とを含む検証用モデルを組み合わせた、前記検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う第２形式検証手段と、
を含む非同期回路検証装置。
【請求項２】
前記第２形式検証手段は、前記非同期検証用モデルに対して、回路動作の形式検証を行うことにより、回路動作が正常でない前記分割回路を特定する請求項１記載の非同期回路検証装置。
【請求項３】
前記複数の分割回路データの各々に基づいて、前記２段以上のフリップフロップと、前記１段以上のフリップフロップと、前記不明回路部とを用いて記述され、前記２段以上のフリップフロップ及び前記１段以上のフリップフロップに入力されるクロック情報を含む前記検証用モデルを生成するモデル生成手段と、
入力操作部を介して、検証実行者から、前記検証用モデルの各々について、前記不明回路部に入力される信号のクロック情報を受け付けるクロック情報受付手段とを更に含み、
前記第２形式検証手段は、前記クロック情報受付手段によって受け付けた前記不明回路部に入力される信号のクロック情報を含んだ、前記検証用モデルを組み合わせて、前記非同期検証用モデルを生成し、生成した非同期検証用モデルに対して、回路動作の形式検証を行う請求項１又は２記載の非同期回路検証装置。
【請求項４】
前記検証用モデルは、前記分割回路の入力部に２段のフリップフロップが接続されている場合の前記２段のフリップフロップと、出力部に１段のフリップフロップが接続されている場合の前記１段のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述される請求項１〜請求項３の何れか１項記載の非同期回路検証装置。
【請求項５】
コンピュータを、
検証対象の非同期回路を分割した複数の分割回路の各々を記述した、クロック情報を含む分割回路データに対して、回路動作の形式検証を行う第１形式検証手段、及び
前記第１形式検証手段によって回路動作が正常であることが検証された前記複数の分割回路データの各々について生成された、前記分割回路の入力部に２段以上のフリップフロップが接続されている場合の前記２段以上のフリップフロップと、出力部に１段以上のフリップフロップが接続されている場合の前記１段以上のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述され、前記２段以上のフリップフロップ及び前記１段以上のフリップフロップに入力されるクロック情報と、前記不明回路部に入力される信号と同期したクロック情報とを含む検証用モデルを組み合わせた、前記検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う第２形式検証手段
として機能させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、非同期回路検証装置及びプログラムに係り、特に、非同期回路に対して、回路動作の形式検証を行う非同期回路検証装置及びプログラムに関する。
【背景技術】
【０００２】
従来より、非同期回路の検証方法として、形式検証が知られている。形式検証とは、検証する回路データが取り得る全ての論理値に対して網羅的な解析を実行する検証手法である。形式検証では、一般的に、図１０に示すように、回路データに対して、形式検証ツールを適用することにより、回路動作の検証を行う。形式検証では、不具合の見逃しがないという利点がある。
【０００３】
また、規模の大きい回路データの非同期検証として、論理シミュレータを使用した論理シミュレーションが実施されている。図１１に示すように、回路データに対して、論理シミュレータを適用することにより、テストデータを用いたシミュレーションを行って、検証を行っている。
【０００４】
また、回路規模が大きな回路のシミュレーションを行うマルチ回路シミュレータ装置が知られている（特許文献１）。このマルチ回路シミュレータ装置では、分割された回路についてシミュレーションを行うことにより、効率よく回路検証を行っている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開平１０−６３７０１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
しかしながら、従来の形式検証では、回路規模が大きい場合、解析する論理値のパターンが増大して、形式検証ツールの解析容量を超えてしまうため、検証が実行することができない、という問題がある。
【０００７】
また、従来の論理シミュレータを使用した論理シミュレーションで非同期検証を実施する場合、検証の網羅性は論理シミュレータに入力するテストデータの論理値に依存してしまうため、検証精度が低下し、不具合の見落としが発生する可能性がある、という問題点がある。
【０００８】
また、上記の特許文献１に記載の技術では、検証の網羅性が、回路シミュレータに入力するテストデータの論理値に依存してしまうため、検証精度が劣化し、不具合の見落としが発生する可能性がある、という問題点がある。
【０００９】
本発明は、上記の問題点を解決するためになされたもので、回路規模が大きくても、高い検証精度で、回路動作が正常であるかどうかを検証することができる非同期回路検証装置及びプログラムを提示することを目的とする。
【課題を解決するための手段】
【００１０】
上記の目的を達成するために本発明に係る非同期回路検証装置は、検証対象の非同期回路を分割した複数の分割回路の各々を記述した、クロック情報を含む分割回路データに対して、回路動作の形式検証を行う第１形式検証手段と、前記第１形式検証手段によって回路動作が正常であることが検証された前記複数の分割回路データの各々について生成された、前記分割回路の入力部に２段以上のフリップフロップが接続されている場合の前記２段以上のフリップフロップと、出力部に１段以上のフリップフロップが接続されている場合の前記１段以上のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述され、前記２段以上のフリップフロップ及び前記１段以上のフリップフロップに入力されるクロック情報と、前記不明回路部に入力される信号と同期したクロック情報とを含む検証用モデルを組み合わせた、前記検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う第２形式検証手段と、を含んで構成されている。
【００１１】
本発明に係るプログラムは、コンピュータを、検証対象の非同期回路を分割した複数の分割回路の各々を記述した、クロック情報を含む分割回路データに対して、回路動作の形式検証を行う第１形式検証手段、及び前記第１形式検証手段によって回路動作が正常であることが検証された前記複数の分割回路データの各々について生成された、前記分割回路の入力部に２段以上のフリップフロップが接続されている場合の前記２段以上のフリップフロップと、出力部に１段以上のフリップフロップが接続されている場合の前記１段以上のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述され、前記２段以上のフリップフロップ及び前記１段以上のフリップフロップに入力されるクロック情報と、前記不明回路部に入力される信号と同期したクロック情報とを含む検証用モデルを組み合わせた、前記検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う第２形式検証手段として機能させるためのプログラムである。
【００１２】
本発明によれば、第１形式検証手段によって、検証対象の非同期回路を分割した複数の分割回路の各々を記述した、クロック情報を含む分割回路データに対して、回路動作の形式検証を行う。
【００１３】
そして、第２形式検証手段によって、第１形式検証手段によって回路動作が正常であることが検証された複数の分割回路データの各々について生成された検証用モデルを組み合わせた、検証対象の非同期回路を表わす非同期検証用モデルに対して、回路動作の形式検証を行う。
【００１４】
このように、分割回路について生成された、入力部に接続された２段以上のフリップフロップと、出力部に接続された１段以上のフリップフロップと、残りの回路部分を表わす回路構成を不明とした不明回路部とを用いて記述された検証用モデルを組み合わせて、回路動作の形式検証を行うことにより、回路規模が大きくても、高い検証精度で、回路動作が正常であるかどうかを検証することができる。
【００１５】
本発明に係る第２形式検証手段は、非同期検証用モデルに対して、回路動作の形式検証を行うことにより、回路動作が正常でない分割回路を特定することができる。これによって、修正すべき分割回路を特定することができる。
【００１６】
本発明に係る非同期回路検証装置は、複数の分割回路データの各々に基づいて、２段以上のフリップフロップと、１段以上のフリップフロップと、不明回路部とを用いて記述され、２段以上のフリップフロップ及び１段以上のフリップフロップに入力されるクロック情報を含む検証用モデルを生成するモデル生成手段と、入力操作部を介して、検証実行者から、検証用モデルの各々について、不明回路部に入力される信号のクロック情報を受け付けるクロック情報受付手段とを更に含み、第２形式検証手段は、クロック情報受付手段によって受け付けた不明回路部に入力される信号のクロック情報を含んだ、検証用モデルを組み合わせて、非同期検証用モデルを生成し、生成した非同期検証用モデルに対して、回路動作の形式検証を行うことができる。
【００１７】
上記の検証用モデルは、分割回路の入力部に２段のフリップフロップが接続されている場合の２段のフリップフロップと、出力部に１段のフリップフロップが接続されている場合の１段のフリップフロップと、残りの回路部分を表わし、かつ、回路構成を不明とした不明回路部とを用いて記述されるものとすることができる。これによって、検証用モデルを、より簡素化することができる。
【発明の効果】
【００１８】
以上説明したように、本発明の非同期回路検証装置及びプログラムによれば、分割回路について生成された、入力部に接続された２段以上のフリップフロップと、出力部に接続された１段以上のフリップフロップと、残りの回路部分を表わす回路構成を不明とした不明回路部とを用いて記述された検証用モデルを組み合わせて、回路動作の形式検証を行うことにより、回路規模が大きくても、高い検証精度で、回路動作が正常であるかどうかを検証することができる、という効果が得られる。
【図面の簡単な説明】
【００１９】
【図１】本発明の実施の形態に係る非同期回路検証装置の構成を示す概略図である。
【図２】本発明の実施の形態に係る非同期回路検証装置の構成を示すブロック図である。
【図３】ブロック回路の例を示す回路図である。
【図４】検証用モデルの例を示す図である。
【図５】ブロック回路の例を示す回路図である。
【図６】検証用モデルの例を示す図である。
【図７】複数のブロック回路からなる非同期回路の例を示す回路図である。
【図８】複数の検証用モデルを組み合わせた非同期検証用モデルの例を示す図である。
【図９】本発明の実施の形態に係る非同期回路検証装置における非同期検証処理ルーチンの内容を示すフローチャートである。
【図１０】従来例における形式検証を示すイメージ図である。
【図１１】従来例における論理シミュレータを用いた回路動作の検証を示すイメージ図である。
【発明を実施するための形態】
【００２０】
以下、図面を参照して、本発明の好適な実施の形態について説明する。本実施の形態では、半導体集積回路である非同期回路の回路動作を検証する非同期回路検証装置に、本発明を適用した場合を例に説明する。
【００２１】
本発明の実施の形態に係る非同期回路検証装置１０は、従来既知のパーソナルコンピュータによって構成されており、ＲＯＭ１２、ＣＰＵ１４、ＲＡＭ１６、後述する非同期検証処理ルーチンを実現するためのプログラムや形式検証プログラム、回路データなどの各種データを記憶したＨＤＤ１８、キーボード２０、マウス２２、ディスプレイ２４、及びこれらを互いに接続する入出力ポート２６を備えている。なお、キーボード２０及びマウス２２は、本発明の入力操作部に対応している。
【００２２】
ＨＤＤ１８には、検証対象となる非同期回路の回路データが記憶されており、記憶されている回路データは、素子の種類を示す素子情報と、素子の各端子の接続先を示す回路接続情報とを含んでいる。また、回路データには、各素子に入力されるクロック情報も含まれている。
【００２３】
非同期回路検証装置１０を機能ブロックで表すと、図２に示すように、ＨＤＤ１８に記憶された検証対象の非同期回路の回路データを、予め分類されたブロック単位に応じて、複数のブロック回路のブロック回路データに分割する回路分割部３０と、各ブロック回路データに対して形式検証プログラムを実行して形式検証を行う第１形式検証部３２と、回路動作が正しいと検証された全てのブロック回路データの各々について、後述する検証用モデルを生成するモデル生成部３４と、検証用モデルを組み合わせた非同期検証用モデルに対して、形式検証プログラムを実行して形式検証を行う第２形式検証部３６とを備えている。
【００２４】
また、非同期回路検証装置１０は、第１形式検証部３２及び第２形式検証部３６の検証結果を示す表示画面を、ディスプレイ２４に表示させる検証結果出力部３８と、第１形式検証部３２及び第２形式検証部３６の検証結果に応じて、検証に失敗したブロック回路のブロック回路データを修正する回路修正部４０とを備えている。
【００２５】
回路分割部３０では、検証実行者が、キーボード２０及びマウス２２を操作することにより、ＨＤＤ１８に記憶された回路データが表わす検証対象の非同期回路を、回路設計段階で予め分類されたブロック単位に応じて、複数のブロック回路に分割する。回路分割部３０は、分割結果に応じて、検証対象の非同期回路の回路データを、分割した複数のブロック回路のブロック回路データに分割する。
【００２６】
第１形式検証部３２は、各ブロック回路データに対して、形式検証プログラムを実行することにより、回路動作が正常であるかどうかの検証を行う。
【００２７】
形式検証プログラムによる形式検証では、まず、ブロック回路データに基づいて、ブロック回路データが示すブロック回路の論理式を数学的モデルで表現し、その論理式全体を１とするような変数値の組み合わせが存在するか否かを体系的判定する。解析において、出力されるべき論理値と違う論理値が出力される状態が存在すると判定された場合には、回路動作が正常でないとして、検証結果“Ｆａｉｌ”が出力されると共に、違う論理値が出力されると判定された状態および箇所が特定される。また、出力されるべき論理値と等しい論理値のみが出力されると判定された箇所については、検証結果“Ｐａｓｓ”が出力され、網羅的な解析において検証結果“Ｆａｉｌ”が出力されなかった場合には、回路動作が正常であるであることが検証される。例えば、非同期転送箇所において、データが転送されるときに、次のクロックにおいて出力された論理値が、正しい論理値とは異なる論理値が出力される状態がある、と判定された場合には、問題のある非同期転送箇所として、Ｆａｉｌという検証結果が出力される。一方、データが転送されるときに、次のクロックにおいて出力される論理値が、正しい論理値のみである、と判定された場合には、問題のない非同期転送箇所として、Ｐａｓｓという検証結果が出力される。
【００２８】
第１形式検証部３２で回路動作が正常でないと判定されたブロック回路については、回路修正部４０で、検証実行者が、キーボード２０及びマウス２２を操作することにより、“Ｆａｉｌ”が出力された箇所の回路を修正する。
【００２９】
第１形式検証部３２において、各ブロック回路データについて、“Ｆａｉｌ”が出力された箇所が、“Ｐａｓｓ”の判定になるまで形式検証が繰り返されると共に、回路修正部４０において、回路の修正が繰り返される。
【００３０】
モデル生成部３４は、回路動作が正常であることが検証された全てのブロック回路データの各々について、以下に説明するように、検証用モデルを生成する。
【００３１】
まず、図３に示すようなブロック回路データが示すブロック回路について、入力端に接続された２段分のフリップフロップと、出力端に接続された１段分のフリップフロップとを抽出する。図４に示すように、抽出された、入力端に接続された２段分のフリップフロップと、出力端に接続された１段分のフリップフロップと、残りの回路部分を表わし、かつ、内部の回路構成に関する情報を持たない（内部の回路構成がブラックボックスとなっている）不明回路部と、を用いて記述した検証用モデルを生成する。
【００３２】
上記の残りの回路部分については、以下のように特定する。
【００３３】
まず、ブロック回路の入力端から出力端への経路において、入力端に接続された２段分のフリップフロップと出力端に接続された１段分のフリップフロップ以外を、残りの回路部分として特定する。また、ブロック回路の入力端から見て、入力端がそのまま出力端に接続されている箇所（フリップフロップが存在しない箇所）、及び入力端から出力端の経路でフリップフロップが１段しかない箇所があれば、該当する部分（図５の（１）及び（２）参照）を、例外箇所として特定する。また、ブロック回路の出力端から見て、入力端がそのまま出力端に接続されている箇所（フリップフロップが存在しない箇所）、異なるクロックで動作する経路同士が論理素子で収束して、そのまま出力端に接続されている箇所、及び入力端同士が論理素子で収束して、そのまま出力端に接続されている箇所、及びあるクロックで動作している経路と入力端とが収束して、そのまま出力端に接続されている箇所があれば、該当する部分（図５の丸印付きの番号１〜４）を、例外箇所として特定する。この例外箇所の特定作業の段階でスルーネットや再収斂箇所の検出が可能となる。例外箇所は残りの回路部分に属し、入力端と出力端以外の内部の回路構成に関する情報を持たない。
【００３４】
また、ブロック回路データから、入力端に接続された２段分のフリップフロップに入力されるクロック情報、及び出力端に接続された１段分のフリップフロップに入力されるクロック情報を抽出し、図６に示すように、検証用モデルに含まれるデータとして格納する。また、不明回路部における例外箇所については、Ｕｎｋｎｏｗｎというクロック情報を格納する。
【００３５】
このＵｎｋｎｏｗｎというクロック情報をもった不明回路部は、形式検証において、そのままでは問題があると判定され、“Ｆａｉｌ”という検証結果が出力されてしまう。
【００３６】
そこで、モデル生成部３４では、検証実行者が、注目の検証用モデルのブロック回路の入力端と他のブロック回路との接続状況を参照して、キーボード２０及びマウス２２を操作することにより、注目の検証用モデルの不明回路部に入力される信号と同期したクロック情報を入力する。
【００３７】
以上説明したように、モデル生成部３４によって生成される検証用モデルでは、入力端に接続された２段分のフリップフロップのクロック情報を有することにより、ブロック回路による非同期転送を行う場合の入力部のクロック情報を知ることができる。これは、非同期転送を行う場合には、一般的に、入力段に２段分のフリップフロップを設けることが約束されているからである。また、検証用モデルでは、出力端に接続された１段分のフリップフロップのクロック情報を有することにより、ブロック回路からの出力のクロック情報を知ることができる。また、ブロック回路単体については、形式検証により回路動作が正常であることが検証済みであるため、残りの回路部分については、検証対象外とすることができ、検証用モデルにおいて、不明回路部として、内部の回路構成に関する情報を持たないようにすることにより、モデルを簡素化している。
【００３８】
第２形式検証部３６は、まず、各ブロック回路の検証用モデルを組み合わせることにより、検証対象の非同期回路を表わす非同期検証用モデルを生成する。例えば、図７に示すような検証対象の非同期回路の各ブロック回路についてモデル生成部３４で各々生成された検証用モデルを、各ブロック回路の接続関係に従って接続して組み合わせることにより、図８に示すような検証対象の非同期回路の非同期検証用モデルを生成する。
【００３９】
第２形式検証部３６は、生成された非同期検証用モデルに対して、形式検証プログラムを実行することにより、回路動作が正しいかどうかの検証を行う。
【００４０】
このとき、非同期検証用モデルでは、各ブロック回路における不明回路部で、回路の内部情報を持たないようにしているため、モデルが簡素化され、そのままでは形式検証が実施できない規模の非同期回路に対しても、形式検証を実施することができる。
【００４１】
第２形式検証部３６による形式検証では、例えば、ブロック回路によりデータが転送されるとき、次のクロックにおいて出力される論理値が、正しい論理値とは異なる論理値が出力される状態が存在する、と判定された場合には、問題のあるブロック回路として特定されると共に、“Ｆａｉｌ”という検証結果が出力される。一方、ブロック回路によりデータが転送されるとき、次のクロックにおいて出力される論理値が、正しい論理値のみである、と判定された場合には、問題のないブロック回路として、“Ｐａｓｓ”という検証結果が出力される。
【００４２】
第２形式検証部３６によって問題のある箇所として特定された（“Ｆａｉｌ”が出力された）ブロック回路については、回路修正部４０で、検証実行者が、キーボード２０及びマウス２２を操作することにより、“Ｆａｉｌ”が出力された箇所の回路を修正する。例えば、入力端に接続された２段のフリップフロップや、出力端に接続された１段のフリップフロップの、追加、削除、又は変更が行われる。
【００４３】
修正されたブロック回路については、再び、第１形式検証部３２による形式検証が行われ、修正されたブロック回路のブロック回路データについて、回路動作が正常であると検証されるまで形式検証が繰り返されると共に、回路修正部４０による回路の修正が繰り返される。
【００４４】
次に、本実施の形態に係る非同期回路検証装置１０の作用について説明する。
【００４５】
まず、非同期回路検証装置１０において、ＨＤＤ１８から検証対象の非同期回路の回路データを読み出し、回路データに基づいて、回路データが示す非同期回路を表わす表示画面を、ディスプレイ２４に表示させる。
【００４６】
そして、検証実行者がキーボード２０又はマウス２２を操作して、検証対象の非同期回路について、設計段階で予め分類されたブロック単位に従って、非同期回路を、複数のブロック回路に分割する。非同期回路検証装置１０の回路分割部３０は、上記の分割結果に応じて、検証対象の非同期回路の回路データを、分割した複数のブロック回路のブロック回路データに分割する。
【００４７】
次に、第１形式検証部３２は、ブロック回路データの各々に対して、形式検証プログラムを実行して、ブロック回路の回路動作が正常であるか否かを検証する。そして、検証結果出力部３８によって、形式検証の結果を表わす画面が、ディスプレイ２４に表示される。回路動作が正しくないと判定されたブロック回路については、回路修正部４０で、検証実行者が、キーボード２０及びマウス２２を操作することにより、“Ｆａｉｌ”と判定された箇所の回路を修正する。
【００４８】
全てのブロック回路データについて、第１形式検証部３２によって回路動作が正常であると検証されるまで、第１形式検証部３２による形式検証、及び回路修正部４０による回路の修正が繰り返される。
【００４９】
全てのブロック回路データについて、形式検証によって回路動作が正常であると検証されると、非同期回路検証装置１０において、図９に示す非同期検証処理ルーチンが実行される。
【００５０】
まず、ステップ１００において、形式検証済みの各ブロック回路データに基づいて、各ブロック回路について検証用モデルを生成する。ここでは、ブロック回路の入力端に２段分のフリップフロップが接続されている場合の２段分のフリップフロップと、出力端に１段分のフリップフロップが接続されている場合の１段分のフリップフロップと、残りの回路部分を表わす内部の回路構成を不明とした不明回路部とを用いて記述された検証用モデルを生成する。また、生成される検証用モデルは、２段分のフリップフロップ及び１段分のフリップフロップに入力されるクロック情報と、特定された不明回路部における例外箇所のＵｎｋｎｏｗｎのクロック情報とを含んでいる。
【００５１】
そして、ステップ１０２において、各ブロック回路における不明回路部のクロック情報を入力するための入力画面をディスプレイ２４に表示させる。ステップ１０４で、各ブロック回路における不明回路部のクロック情報の入力を受け付けたか否かを判定し、まだ入力されていない場合には、ステップ１０２へ戻って、引き続き、クロック情報の入力画面を表示させる。一方、検証実施者が、各ブロック回路の入力端に接続されたブロック回路の回路構成を見て、各ブロック回路の不明回路部に入力される信号と同期したクロック情報を調べ、キーボード２０及びマウス２２を操作して、全てのブロック回路について、不明回路部に与えるクロック情報が入力されると、入力されたクロック情報を受け付け、ステップ１０６へ進む。
【００５２】
ステップ１０６では、上記ステップ１０４で入力された不明回路部に与えるクロック情報を含む、各ブロック回路の検証用モデルを組み合わせて、検証対象の非同期回路を表わす非同期検証用モデルを生成する。
【００５３】
次のステップ１０８では、上記ステップ１０６で生成された非同期検証用モデルに対して、形式検証プログラムを実行して、非同期回路の回路動作が正常であるか否かを検証する。
【００５４】
そして、ステップ１１０では、非同期回路の回路動作が正常であることが検証されたか否かを判定し、形式検証の網羅的な解析において、検証結果“Ｆａｉｌ”が出力されなかった場合には、ステップ１１２へ移行し、非同期回路の回路動作が正常であることが検証されたことを示すメッセージをディスプレイ２４に表示させて、非同期検証処理ルーチンを終了する。一方、何れかのブロック回路について、検証結果“Ｆａｉｌ”が出力された場合には、ステップ１１４へ移行し、非同期回路の回路動作が正常であることが検証されなかったことを示すメッセージと共に、“Ｆａｉｌ”が出力されたブロック回路を特定した情報をディスプレイ２４に表示させて、非同期検証処理ルーチンを終了する。
【００５５】
上記の非同期検証処理ルーチンにおいて、非同期回路の回路動作が正常であることが検証されなかった場合には、検証結果“Ｆａｉｌ”が出力されたブロック回路について、回路修正部４０で、検証実行者が、キーボード２０及びマウス２２を操作することにより、当該ブロック回路を修正する。
【００５６】
修正したブロック回路データについて、第１形式検証部３２によって回路動作が正常であると検証されるまで、第１形式検証部３２による形式検証、及び回路修正部４０による回路の修正が繰り返される。
【００５７】
以上説明したように、本実施の形態に係る非同期回路検証装置によれば、形式検証済みのブロック回路について生成された、入力端に接続された２段分のフリップフロップと、出力端に接続された１段分のフリップフロップと、残りの回路部分を表わす不明回路部とを用いて記述された検証用モデルを組み合わせて、非同期検証用モデルを生成し、非同期検証用モデルに対して、回路動作の形式検証を行うことにより、回路規模が大きくても、高い検証精度で、回路動作が正常であるかどうかを検証することができる。従来の論理シミュレーションを用いて非同期検証を実施する場合に比べ、高い検証精度で、回路動作の検証を行うことができる。従来手法では形式検証が実施できなかった規模の回路データに対しても、形式検証を実施することができるようになるため、精度の高い検証が実施可能となり、不具合の見逃しを防止することができる。
【００５８】
また、生成した検証用モデルを組み合わせて構成した非同期検証用モデルを使用して形式検証を実施する。生成した検証用モデルは、元のブロック回路データに比べて解析にかかる負荷が小さい。そのため、検証用モデルを組み合わせて構成した非同期検証用モデルについても解析負荷が小さいため、形式検証の実施が可能となる。
【００５９】
なお、上記の実施の形態では、ブロック回路データから、入力端に接続された２段分のフリップフロップ、及び出力端に接続された１段分のフリップフロップを自動的に抽出して、検証用モデルを生成する場合を例に説明したが、これに限定されるものではなく、検証実行者が、マウスを操作して、ブロック回路データから、入力端に接続された２段分のフリップフロップ、及び出力端に接続された１段分のフリップフロップを特定し、これに応じて検証用モデルを生成するようにしてもよい。
【００６０】
また、入力端に接続された２段分のフリップフロップを用いて記述した検証用モデルを生成する場合を例に説明したが、これに限定されるものではなく、入力端に接続された２段以上のフリップフロップを用いて記述した検証用モデルを生成してもよい。また、出力端に接続された１段分のフリップフロップを用いて記述した検証用モデルを生成する場合を例に説明したが、これに限定されるものではなく、出力端に接続された１段以上のフリップフロップを用いて記述した検証用モデルを生成してもよい。
【００６１】
本発明のプログラムを、記録媒体に格納して提供するようにしてもよい。
【符号の説明】
【００６２】
１０  非同期回路検証装置
２０  キーボード
２２  マウス
２４  ディスプレイ
３０  回路分割部
３２  第１形式検証部
３４  モデル生成部
３６  第２形式検証部
３８  検証結果出力部
４０  回路修正部
【図１】
2011002903.tif 000003
【図２】
2011002903.tif 000004
【図３】
2011002903.tif 000005
【図４】
2011002903.tif 000006
【図５】
2011002903.tif 000007
【図６】
2011002903.tif 000008
【図７】
2011002903.tif 000009
【図８】
2011002903.tif 000010
【図９】
2011002903.tif 000011
【図１０】
2011002903.tif 000012
【図１１】
2011002903.tif 000013