JP4973392B2 - 回路検証方法および回路検証プログラム - Google Patents

Description

本発明は、回路情報に基づいて回路動作をコンピュータにより検証する回路検証方法および回路検証プログラムに関する。

半導体集積回路の回路設計において、設計者は回路設計後に論理合成を行い、回路動作上問題となる箇所が無いか検証を行う。近年の高機能な半導体集積回路には、信号の送信側と受信側で異なるクロックにより動作する非同期回路を有するものがある。非同期回路ではメタステーブル等の非同期回路特有の現象が生じる。かかる現象が障害の原因になることもあるため、設計段階で非同期回路の検証をすることが重要となる。ここで、メタステーブルとは、信号送信レジスタと異なるクロックで駆動される信号受信レジスタの受信タイミングにより、受信側レジスタの出力レベルが不安定になる現象をいう。

特許文献１の図３には、半導体集積回路を設計する場合の、タイミング検証が必要なセルの抽出方法について記載されている。具体的には、信号送信レジスタのクロックと信号受信レジスタのクロックとが異なる場合に、それぞれのレジスタをタイミング検証が必要な対象セルとして抽出する。

しかし、特許文献１にかかる従来技術では、ある一つの非同期パスを伝播する信号の送受信タイミングが、他の非同期パスを伝播する信号の送受信タイミングに与える影響等を抽出することはできない。したがって回路検証において例えばタイミング検証の結果エラーとなった場合、問題となるのはセル単体なのか、セル間の非同期パスなのか、それとも非同期パス間の信号伝播タイミングに問題があるのかの判断は設計者が手作業で行う必要がある。
特開２０００−１１０３１号公報

本発明は、ある一つの非同期パスを伝播する信号の送受信タイミングが、他の非同期パスを伝播する信号の送受信タイミングに与える影響等を検証情報として出力することのできる、回路検証方法および回路検証プログラムの提供を目的とする。

前記の課題を解決するために、本発明では、ライブラリを参照することによってある一つの非同期パスを伝播する信号の送受信タイミングが、他の非同期パスを伝播する信号の送受信タイミングに与える影響等を抽出する回路検証方法および回路検証プログラムを採用する。具体的には、回路情報に基づいて回路の動作を検証するコンピュータによる回路検証方法であって、コンピュータが、それぞれ異なるクロックが供給されるレジスタ間を配線により接続した非同期回路に関する非同期回路情報を、前記回路情報から複数検出し、異なる回路構成を有する複数の非同期回路パーツ情報を含む、記憶装置に格納されたライブラリから、前記非同期回路情報のうち１つに対応する第一非同期回路パーツ情報を検出し、前記非同期回路情報のうち他の１つに対応する第二非同期回路パーツ情報を前記ライブラリから検出し、前記第一非同期回路パーツ情報及び前記第二非同期回路パーツ情報に基づいて、第一非同期回路と第二非同期回路とを含む回路に対応する第三非同期回路パーツ情報を前記ライブラリから検出し、前記第三非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第三非同期回路の回路動作を検証する第三検証情報を抽出することを特徴とする。

本発明によれば、それぞれの非同期回路および複数の非同期回路間の検証情報を自動的に抽出することができる。これにより、非同期回路を含む論理回路の検証効率および検証精度を向上させることができる。

以下、本発明の実施形態を、以下に詳細に説明する。なお、実施形態は例示であり、本発明はこの実施形態に限定されるものではない。

図１は任意の回路から検証対象である非同期回路を抽出することを説明するための、非同期回路の一例である。本実施例は、非同期回路の設計情報から非同期パスを探し、当該非同期パス間のタイミング情報等を検証情報として出力するものである。図１に基づいて本実施例の概要を説明する。４２１から４３０はレジスタを示している。レジスタとは、入力信号をクロックに同期させて出力する回路である。４３１および４３２はセレクタを示している。４０１から４０９は、後述するライブラリとの照合単位を示している。４５０から４５８は配線を示している。信号４６０および４６１は入力信号であり、クロック信号４６２と同期している。信号４６４は出力信号を示している。信号４６２および４６３はそれぞれ異なる周期または異なる位相を有する非同期クロック信号である。配線４５０の送受端に接続されたレジスタに着目すると、送信端のレジスタ４２１は、クロック４６２に同期している。一方、受信端のレジスタ４２６は、クロック４６３に同期している。このように、配線４５０の送受端に接続されたレジスタにそれぞれ供給されるクロック情報をチェックすることにより、それぞれのレジスタに異なるクロックが供給される配線４５０を非同期配線として検出することができる。配線４５１および４５２も同様に非同期配線として検出することができる。

図１の回路において、それぞれの非同期配線は密接に関連している。例えば非同期配線４５１の受信端に接続された論理回路４０６は、非同期配線４５０の受信端に接続された論理回路４０２から出力される信号４６４の出力タイミングを制御している。このような非同期配線間の関連性に基づいてタイミング検証条件等の検証情報を出力することにより、非同期回路の検証精度を向上させることができる。

図２は非同期検証方法のフローである。図２のフローに従って、関連する非同期配線の抽出から、非同期配線間の検証情報の出力までの処理の流れを説明する。図２の論理合成ステップＳ１０１では、レジスタ・トランスファー・レベル（Ｒｅｇｉｓｔｅｒ Ｔｒａｎｓｆｅｒ Ｌｅｖｅｌ、ＲＴＬ）等で記述された回路設計情報に基づいて論理合成を実行し、論理回路の情報と配線との情報とを有する回路配線情報を出力する。ＲＴＬとは、回路をフリップフロップ等のレジスタと組み合わせ論理回路とで表現したレベルをいう。クロックネット抽出ステップＳ１０２では、当該回路配線情報に記述されたレジスタを駆動するクロック情報をそれぞれ抽出する。パス抽出ステップＳ１０３では、ドメインクロス、すなわち送信側レジスタと受信側レジスタでクロックドメインの異なる配線が存在するかチェックし、存在している場合はステップＳ１０４において、その配線を非同期配線と判断して抽出する。最下層パーツ抽出ステップＳ１０５では、回路配線情報に記述された回路情報であって、ライブラリ１０５に登録された最下位パーツ情報と一致するものを検索し、一致するものがあればステップＳ１０５において最下層パーツとして抽出する。ここでライブラリ１０５とは、非同期回路を構成する回路パーツ情報をスタイルチェック情報、動的チェック情報等と共に階層化して登録したものであり、詳細については後述する。中間／上位階層パーツ情報抽出ステップＳ１０６では、ステップＳ１０４で抽出した非同期配線を基点として下位階層パーツ情報の種類、下位階層パーツ情報間の接続関係、クロックドメインのパス情報を元に該当する中間階層パーツ情報をライブラリより検索し、一致するものがあればステップＳ１０７において中間階層パーツ情報として抽出し、検証情報を出力する。ここで検証情報とは、ライブラリ１０５に定義された回路パーツ情報に対応した、回路動作を検証するための情報である。検証情報には、ステップＳ１０１で処理の対象とした回路配線情報に記述されている信号名などを出力することで、設計者の検証が容易になる。さらに、中位階層パーツ情報の種類、中位階層パーツ情報同士をつなぐ信号のパス等の情報を元に該当する上位の階層をステップＳ１０８においてライブラリ１０５より検索し、一致するものがあればステップＳ１０７において上位階層パーツ情報として抽出し、検証情報をステップＳ１０９において出力する。同様に、さらに上位の階層に該当するパーツが無いかステップＳ１０８においてライブラリより検索し、一致するものがあればステップＳ１０７においてパーツとして抽出し、ステップＳ１０９において検証情報を出力する。なければパーツ抽出処理を終了する。以下において、各ステップを詳細に説明する。なおここでは各階層パーツ抽出ごとに検証情報を出力しているが、最上位階層パーツの検証情報のみ抽出してもよい。

図３および図４は、ライブラリ１０５に格納されている回路パーツ情報を概念的に図示したものである。ライブラリ１０５に登録されている回路パーツ情報は、その回路規模ごとに階層化されて登録されている。階層が上位になるほど、回路パーツ情報の回路規模は大きくなる。図３および図４を用いて、各階層の内容および階層間の関係を説明する。

図３の最下層２０１には、1以上の論理回路からなる論理ブロックを回路パーツ情報として定義している。最下層２０１を用いることにより、非同期回路を構成する最小論理ブロックを抽出することができる。図３の中間階層２０２には、非同期配線とその両端に接続された最下層２０１のパーツとの組み合わせを回路パーツ情報として定義している。中間階層２０２を用いることにより、非同期回路を構成する最小単位を抽出することができる。

図４の上位階層２０３には、中間階層以下の各階層２０１および２０２のパーツの組み合わせを回路パーツ情報として定義している。さらに同図の最上位階層２０４には、上位階層以下の各階層２０１、２０２および２０３のパーツの組み合わせを回路パーツ情報として定義している。上位階層２０３または最上位階層２０４を用いることにより、複数の非同期回路の組合せを抽出することができる。

ライブラリには、使用頻度の高い回路構成を回路パーツ情報として登録しておくことが望ましい。またライブラリには、同一機能であって回路構成の異なるパーツを、同一カテゴリで定義することが望ましい。例えば図３の最下層回路パーツ情報２０１であれば、マルチプレクサ２１１ａのパーツ群として回路パーツ情報２１５と回路パーツ情報２１６が登録されている。回路パーツ情報２１５は、セレクタへの入力信号２１５ａおよび制御信号２１５ｂがレジスタのクロック２１５ｃと同期しており、出力信号２１５ｄを出力する。これに対し回路パーツ情報２１６は、レジスタのクロック２１６ｃと非同期のクロックに同期するセレクタの入力信号２１６ａおよび制御信号２１６ｂを有し、出力信号２１６ｄを出力する。このように、回路構成が同じだがレジスタとセレクタとが同期して動作しているものと非同期で動作しているものを同一カテゴリのパーツとして定義する。同一カテゴリに属するパーツの種類が多いほど、検証対象回路とライブラリとが一致する確率を向上させることができる。同様に、組み合わせ回路２１２ａは回路パーツ情報２５０を、レジスタ２１３ａは回路パーツ情報２５１を、シンクロナイザ２１４ａは回路パーツ情報２５２から２５４をパーツ群としてそれぞれ有している。ここで組み合わせ回路とは、複数の入力の論理の組み合わせを出力するレジスタを有さない回路である。レジスタとは、入力信号をクロックに同期させて出力する回路である。シンクロナイザとは、信号の同期化のために、同一のクロックで動作する１以上のレジスタを接続した回路である。

図３の中間階層２０２では、データ転送非同期パス２２１ａ、およびコントロール転送非同期パス２２２ａを回路パーツ情報として定義している。またパーツ群として回路パーツ情報２５５および２５６をそれぞれ定義している。ここでデータ転送非同期パスとは、送信側レジスタと受信側レジスタとがそれぞれ異なるクロックに同期するデータ信号転送パスである。コントロール転送非同期パスとは、送信側レジスタと受信側レジスタとがそれぞれ異なるクロックに同期する制御信号転送パスである。２１１ｂおよび２１１ｃはマルチプレクサを、２１３ｂはレジスタを、２１４ｂはシンクロナイザをそれぞれ表しており、下位階層２０１の回路パーツ情報にそれぞれ対応している。

図４の上位層２０３ではコントロールデータ転送構造２３１ａを、最上位階層２０４ではハンドシェイク構造２４１をそれぞれ定義している。またライブラリ２３１ａ回路パーツ情報２５７を、ライブラリ２４１は回路パーツ情報２５８および２５９をパーツ群としてそれぞれ有している。ここでコントロールデータ転送構造とは、前記データ転送非同期パスの出力を前記コントロール転送非同期パスの出力により制御する構造をいう。ハンドシェイク構造とは、複数の非同期パスが組み合わせ回路により結合している構造をいう。２２１ｂはデータ転送非同期パスを、２２２ｂおよび２２２ｃはコントロール転送非同期パスをあらわしている。また２１２ｂから２１２ｅは組み合わせ回路を、２１３ｃから２１３ｆはレジスタを、２３１ｂから２３１ｄはコントロールデータ転送構造をあらわしている。これらはすべて下位の階層２０１、２０２および２０３に定義された回路パーツ情報に対応している。

なお、本実施例ではライブラリの階層数を４として記載しているが、これに限定するものではなく、照合する論理回路規模を更に細かく階層化しても良い。

図５に、図２のライブラリ１０５に記載されたそれぞれのパーツが持つ回路パーツ情報３０１と、回路パーツ情報３０１を基に生成される検証情報３０２との対応関係を示す。検証情報３０２はパーツ検出される度に生成され、パーツ毎の検証を容易にする。図５ではパーツに関するすべての検証情報３０２を１つのテーブルに記載するように表現しているが、素子定義テーブル、結線定義テーブルのようにパーツの情報ごとに複数のテーブルで検証情報を定義してもよい。回路パーツ情報３０１には、パーツの固有識別情報３１１、パーツの構成要素３１２が定義されており、さらにスタイルチェック項目３１３、パーツの動的チェック情報３１４、およびパーツの個別情報３１５等が定義されている。パーツの固有識別情報３１１には、パーツの属するカテゴリの名称と、パーツの固有名が記述されている。パーツの構成要素３１２には、そのパーツを構成する下位階層パーツ情報の固有情報、下位階層パーツ情報およびパーツ間の配線情報、当該パーツに供給されるクロックドメイン情報、および当該パーツ内のクロックネット情報が定義されている。これらの情報は検証対象である回路設計情報からライブラリ１０５に登録されているパーツを抽出するのに用いる。

また、スタイルチェック項目３１３には、本パーツが満たすべきスタイルルールチェック項目、各ルールの重要度、各ルールを守らなかった場合に予測されるリスク情報等を記述する。パーツの動的チェック情報３１４には、本パーツが期待する入力信号の変化タイミング条件、本パーツの動作条件に該当するアサーション情報、カバレッジ情報等を記述する。ここでアサーション情報とは、論理回路が期待通りに動作しているかを検証するための情報である。また、カバレッジ情報とは、クロックの位相ずれにより非同期パス間に起こりうる周期ずれの範囲情報等、検証すべき時間的ばらつきの範囲である。

また、パーツの個別情報３１５には、パーツに接続されたパスの信号名、信号のビット幅、信号のクロック名を回路設計情報から抽出し出力する。さらに本パーツ内の情報だけでは判断できないため上位階層へ委ねるべきチェック項目等を定義してもよい。

回路パーツ情報３０１と検証情報３０２との対応関係は下記の通りである。論理合成後の回路から検索対象となる回路情報を選択し、ライブラリのパーツ構成要素情報３１２と照合する。ライブラリに検索対象と同一の回路構成を有する回路パーツ情報が存在する場合は、当該パーツを対象に回路パーツ情報３０１に基づいて検証情報３０２を出力する。スタイルチェック項目３１３とスタイルチェック結果３１８との対応については、検証情報３０２の出力時にスタイルチェック項目３１３に基づいてチェックを実行し、スタイルチェック結果３１８を検証情報３０２に出力する。これにより、非同期回路を構成するパーツ単位でスタイルチェックを行い、その結果をパーツ単位で管理することが可能となる。また、パーツの個別情報３２０は、検証対象である回路設計情報を参照し、回路パーツ情報３０１に定義された個別情報３１５に基づいて必要な情報を出力する。

図６に、回路パーツ情報検出から検証情報出力までの処理における、スタイルチェック処理の詳細をフローチャートで示す。図６のフローチャートは図１のフローチャートのステップＳ１０５またはＳ１０７のパーツ抽出ステップに該当する。コンピュータは回路配線情報１５０から任意の回路情報１５１をステップＳ２００において抽出し、ライブラリ１０５に同一の回路パーツ情報が登録されているかステップＳ２０１において検索する。ステップＳ２０２において同一の回路パーツ情報が存在すると判断されれば、ステップＳ２０３において回路パーツ情報の定義に基づいて実際の回路情報から個別情報３２０を抽出し、ステップＳ２０３において検証情報３０２を作成する。ステップＳ２０２においてライブラリに同一の回路パーツ情報が無いと判断した場合は、ステップＳ２０４において回路配線情報の別の回路情報を抽出し、ステップＳ２０１において再度ライブラリから検索する。つづいてステップＳ２０５においてライブラリ１０５の回路パーツ情報に定義されているスタイルチェック項目３１３を抽出し、ステップＳ２０３で生成した検証情報３０２に記述されている個別情報３２０に対してステップＳ２０６においてスタイルチェックを実行する。スタイルチェック項目３１３には、各項目の重要度（Ｓｅｖｅｒｉｔｙ）も併せて記載されている。ステップＳ２０６におけるスタイルチェック実行の結果、ライブラリの定義どおりに設計されていればその旨をステップＳ２０７においてスタイルチェック結果３１８として抽出し、ライブラリの定義どおりに設計されていなければその旨をスタイルチェック結果３１８として、ステップＳ２０７において当該チェック項目の重要度と併せて出力する。各チェック項目の重要度を併せて出力することで、チェック項目に違反した設計をしている場合の危険度を設計者に通知することができる。ステップＳ２０８においてスタイルチェック項目が残っているかどうかを判断し、残っていれば再度ステップＳ２０６を実行する。スタイルチェック項目が残っていなければ、処理を終了する。

図１の回路情報４０１を例に図６のフローの具体的な処理を説明する。回路情報４０１は、セレクタ４３１とレジスタ４２１で構成されているが、これと同一の構成を有する回路パーツ情報が図３の最下層２０１にマルチプレクサ２１５として定義されている。そうすると回路情報４０１を対象として、ＤＭＵＸというパーツ名をつけ、回路パーツ情報を基に検証情報３０２が出力される。検証情報３０２として出力すべき情報は、図５に示すとおり回路パーツ情報ごとに定義されている。したがって回路パーツ情報３０１に基づいて実際の回路から抽出した個別情報３２０が検証情報３０２として出力される。以上説明した検証情報３０２の出力処理は、後述する図１２の検証情報抽出手段１００３ｃにより実行される。抽出した回路情報４０１の検証情報として、例えば以下の情報が出力される。

・ パーツ種類カテゴリ：マルチプレクサ
・ パーツ名：ＤＭＵＸ
・ レジスタクロック：クロック４６２
・ セレクト入力信号：配線４５３伝播信号
・ セレクト信号ビット幅：１
・ セレクト信号同期クロック：クロック４６２
・ データ入力信号：信号４６０
・ データ入力信号ビット幅：３２
・ データ入力信号同期クロック：クロック４６２
・ データ出力信号：配線４５０伝播信号
・ データ出力信号ビット幅：３２
・ データ出力信号同期クロック：クロック４６２
さらに、検証情報出力の際には、図３の回路パーツ情報２１５のスタイルチェック項目３１３を抽出し、実際の回路情報４０１に基づいてスタイルチェックを行い、スタイルチェック結果３１８を検証情報３０２として出力する。回路パーツ情報２１５のスタイルチェック項目３１３として、例えばデータ入力信号はレジスタのクロックと同期している、とライブラリに規定されている場合、データ入力信号の生成元のレジスタに供給されているクロックと検証対象である回路情報のレジスタに供給されているクロックとを比較し、同一であればその結果をスタイルチェック結果３１８として検証情報３０２に記述する。また、回路情報４０１については当該チェックをパスしている旨を検証情報３０２に出力する。

一方、回路情報４０２についてチェックすると、データ入力信号はクロック４６２に同期しており、レジスタ４２６はクロック４６３に同期している。したがって、回路情報４０２のスタイルチェック結果３１８としてクロックが異なる旨を検証情報３０２として出力する。また、当該チェック結果の重要度が確認レベルである旨も合わせて検証情報３０２として出力する。これにより、非同期回路を構成する論理回路のチェック結果を設計者が容易に確認できるようになり、検証効率の向上につながる。

回路パーツ情報２１１ａの論理は、セレクタの入力信号が有効な期間だけ、データ入力信号をレジスタクロック同期でデータ出力するというものである。回路情報の動的チェック項目として、例えばセレクト入力信号が有効な期間はデータ入力信号を変化させない、と回路パーツ情報２１１ａに定義されている場合、その内容を非同期回路の動的チェック情報として検証情報に記述する。

回路情報４０６は２つのレジスタ４２７および４２８で構成されている。またレジスタ４２７の入力信号４５１はレジスタ４２３から出力されており、レジスタ４２３と４２７の動作クロックは異なる。したがって回路情報４０６は図３のライブラリの最下層回路パーツ情報２１４として抽出され、回路情報４０１の場合と同様に検証情報３０２が出力される。例えば回路情報４０１の検証情報として以下の情報が出力される。

・ パーツ種類カテゴリ：シンクロナイザ
・ パーツ名：２−ＤＦＦ
・ レジスタクロック：クロック４６３
・ 入力信号：配線４５１伝播信号
・ 入力信号ビット幅：１
・ 入力信号同期クロック：クロック４６２
・ 出力信号：配線４５４伝播信号
・ 出力信号ビット幅：１
・ 出力信号同期クロック：クロック４６２
また、回路パーツ情報２１４ａのスタイルチェック項目として２つのレジスタ間に組み合わせ回路が入っていないこと、２つのレジスタ間の配線に分岐が無いこと、等を登録しておき、そのチェック結果をスタイルチェック結果として検証情報に出力する。また、回路情報４０６がシンクロナイザとして有効に動作するには配線４５１から入力される信号がクロック４６３で２周期以上連続して有効となる必要がある。そこでこのアサーション情報を回路パーツ情報２１４ａから取得し検証情報に出力しておくことにより、回路情報４０６の論理検証が可能となる。また、回路情報４０６の配線４５１を伝播する信号と配線４５４を伝播する信号との間にはメタスタビリティにより２，３周期の変域がある。かかる情報も回路パーツ情報２１４ａから取得し、回路情報４０６の動的チェック情報として出力する。

さらに回路情報４０３の抽出について説明する。回路情報４０３はレジスタを含んでいない。このようなパーツは組み合わせ論理として回路パーツ情報２１２ａに基づいて抽出され、以下の通り検証情報が出力される。

・ 入力信号１：信号４６１
・ 入力信号１の同期クロック：クロック４６２
・ 入力信号２：配線４５６伝播信号
・ 入力信号２の同期クロック：クロック４６３
また、出力信号の生成条件は、回路パーツ情報２１２ａに基づいて検証情報として出力する。他のパーツについても同様に検証情報を出力する。

以上の通り回路情報ごとのスタイルチェック結果および動的チェック情報を検証情報に出力しておくことにより、回路情報ごとのスタイルチェックの効率を上げるだけでなく、非同期回路全体を論理検証および動作検証する際の条件を定義することができるため、非同期回路検証の効率を向上させることができる。

図７に、図１の非同期回路について下位階層ライブラリを参照することにより抽象化した結果を示す。図中の５０１から５０９はライブラリの下位階層パーツ情報に基づいて抽出された検証情報を示している。中間階層パーツ情報の検出は、図６のフローに従い、非同期パスを基点として下位階層パーツ情報の種類、下位階層パーツ情報をつなぐパス、クロックドメインのパス情報等を基にライブラリの中間階層に一致するものが無いか検索することにより行う（Ｓ２０１）。図７の回路と図３のライブラリの中間階層パーツ情報２０２とを照合すると、５１１に示す領域が回路パーツ情報２２１ａとして検出される。これをＤＡＴＡ＿Ａｓｙｎｃ＿Ｐａｔｈと名づけし、検証情報を出力する。検証情報として回路パーツ情報２２１ａから取得した情報を格納する。また、回路情報５１１を構成する回路情報５０１および５０２との結合関係を検証情報として出力する。検証情報の出力処理は回路情報４０１の出力処理と同様である。例えば、抽出した回路情報５１１の検証情報として以下の情報が出力される。

・ パーツ種類カテゴリ：データ転送非同期パス
・ パーツ名：ＤＡＴＡ＿Ａｓｙｎｃ＿Ｐａｔｈ
・ 入力データ信号：信号４６０
・ 入力データビット幅：３２
・ 入力データ同期クロック：クロック４６２
・ 入力制御信号：配線４５３伝播信号
・ 入力制御信号ビット幅：１
・ 入力制御信号同期クロック：クロック４６２
・ 出力データ信号：信号４６４
・ 出力データビット幅：３２
・ 出力データ同期クロック：クロック４６３
・ 出力制御信号：配線４５４伝播信号
・ 出力制御信号ビット幅：１
・ 出力制御信号同期クロック：クロック４６３
・ 送信側回路情報：５０１
・ 受信側回路情報：５０２
・ 非同期配線：４５０
さらにライブラリに登録されている回路パーツ情報２２１ａのスタイルチェック項目に従ってチェックした結果を検証情報として出力する。回路パーツ情報２２１ａのスタイルチェック項目として、例えば信号配線中に組み合わせ回路を用いない、と規定してあるとする。送信側、受信側回路情報である回路情報５０１および５０２はレジスタを有しているが、組み合わせ回路はレジスタを持たない。従って、レジスタを有する論理回路間の配線途中に、レジスタを有さない論理回路があれば、それは組み合わせ回路であると判断できる。本実施例においては組み合わせ回路を有さないので、その結果が検証情報に出力される。

図８は組み合わせ回路が非同期配線中に存在する回路の一例である。非同期配線４５１ａ、４５１ｂの経路中に組み合わせ回路６０１が存在する。組み合わせ回路６０１はクロック４６２に同期した制御信号４６５により制御されている。図８を用いて非同期配線中に組合せ回路が存在する場合の検証情報の出力について説明する。図８のように組み合わせ回路６０１が配線４５１ａおよび４５１ｂの経路に存在している場合、その旨がスタイルチェック結果として重要度と併せて出力される。組み合わせ回路６０１が存在しても、制御信号４６５が配線４５１ａ伝播信号のデータ転送シーケンス中に変化しなければ、回路動作上問題は無い。したがって、出力する検証情報の重要度を低く設定しておいても良い。このように、回路設計ミスではないが、組み合わせ回路が存在する旨を検証情報として出力し、設計者に確認を促すことで検証効率を向上させることができる。

図７の説明に戻る。回路パーツ情報２２１ａの動的チェック情報として、受信側回路パーツ情報２１１ｃのセレクト信号は送信側回路パーツ情報２１１ｂのセレクト信号を非同期コントロール転送パーツで受け渡したものとする旨がライブラリに登録されているとする。この場合、その情報を本パーツの検証情報として出力する。この検証情報はこの階層レベルでは確認できないが、上位の階層において非同期コントロール転送回路情報５１２との接続関係が明らかになった場合に有用な情報となる。したがってその旨を個別情報として検証情報に出力する。領域５１２、５１３も同様に抽出する。

図９に、図７の非同期回路について図３の中位階層回路パーツ情報により抽象化した結果を示す。図中の７０１から７０３はライブラリの中位階層パーツ情報に基づいて抽出された検証情報を示している。上位階層パーツ情報２０３の検出は、図２のフローに従い、中間階層以下のパーツの種類、中間階層以下のパーツ同士を接続する配線、クロックドメインの情報等を元にライブラリの上位階層パーツ情報に一致するものが無いか検索する。図９の７０１と７０２の接続関係を検証情報に記述されたパラメータにより確認すると、７０１の入力制御信号は７０２の入力信号であり、７０１の出力制御信号は７０２の出力信号であることがわかる。また、７０１は非同期データ転送パーツ情報であり、７０２は非同期コントロール転送パーツ情報であるから、これらの情報と図４に示すライブラリの上位階層パーツ情報とを比較すると、７１１に示す回路情報と一致する回路パーツ情報がライブラリの上位階層に存在する回路パーツ情報２３１ａだと判断できる。従って７１１をパーツ名ＤＡＴＡ＿Ｃｔｒｌ＿Ａｓｙｎｃ＿Ｐａｔｈとして検出する。ライブラリから該当する回路パーツ情報が検出されると、図５に基づいて回路パーツ情報２３１の記述に対応した検証情報３０２が出力される。検証情報には回路パーツ情報２３１から取得した情報を格納する。検証情報の具体的な出力処理は回路情報４０１についての出力処理と同様である。検出された回路情報７１１の検証情報として、例えば以下の情報が格納される。

・ パーツ種類カテゴリ：コントロールデータ転送構造
・ パーツ名：ＤＡＴＡ＿Ｃｔｒｌ＿Ａｓｙｎｃ＿Ｐａｔｈ
・ 入力データ信号名：信号４６０
・ 入力データ信号ビット幅：３２
・ 入力データ信号同期クロック：クロック４６２
・ 入力制御信号名：配線４５３伝播信号
・ 入力制御信号ビット幅：１
・ 入力制御信号同期クロック：クロック４６２
・ 出力データ信号名：信号４６４
・ 出力データ信号ビット幅：３２
・ 出力データ信号同期クロック：クロック４６３
・ 出力制御信号名：配線４５４伝播信号
・ 出力制御信号ビット幅：１
・ 出力制御信号同期クロック：クロック４６３
・ 下位階層パーツ情報（データ）１：７０１
・ 下位階層パーツ情報（制御）１：７０２
上位の階層が回路パーツ情報として検出できると、それよりも下位の階層でチェックできなかった項目もチェックできるようになる。例えば、図７の中間階層において、回路情報５１１のセレクト信号の接続関係は確認できなかったが、図９の上位階層において配線４５４がパーツ情報７０２に接続されていることが確認できるので、その情報を検証情報として出力する。

また、回路情報７１１の非同期配線４５０と４５１は同じ信号伝播方向を有する非同期配線である。配線４５０と４５１を伝播する信号はそれぞれクロック４６２で０サイクルのずれをもって出力される。これらの信号がクロック４６３に非同期乗り換えを行う際に周期ずれが発生する可能性がある。この変域はクロック４６３側で観測される配線４５０を伝播する信号の変化点を基点に、配線４５４を伝播する信号が有効になるまでのクロック４６３の周期差として存在する。かかる情報は回路パーツ情報に固有に登録されている。そして検証情報出力時に、ライブラリから回路パーツ情報２３１ａのデータを参照し、回路パーツ情報の動的チェック情報であるカバレッジ情報として検証情報に出力する。

さらに上位の階層の検索は、上位階層がライブラリ中になくなるまで続けられる。図９において、回路情報７０２から出力されたクロック４６３に同期した配線４５４を伝播する信号は、レジスタ５０９を介して配線４５５を伝播する信号の生成に使われている。また、この信号は回路情報７０３によりクロック４６２同期の非同期配線４５２に非同期乗り換えが行われる。配線４５６を伝播する信号は回路情報７０４、７０５を介して配線４５３を伝播する信号の生成に使われる。このように制御信号が制御信号用の回路情報を用いて非同期パス中を往復する構造から、回路情報７１２は最上位階層のハンドシェイク構造２４１と同一の構成であることがわかる。検証情報の出力処理は、回路情報４０１に対する処理と同様に実行される。検出した回路情報７１２の検証情報として、例えば以下の情報が格納される。

・ パーツ種類カテゴリ：ハンドシェイク構造
・ パーツ名：ＤＡＴＡ＿ＨａｎｄＳｈａｋｅ＿Ｐａｒｔ
・ 入力データ信号名：信号４６０
・ 入力データ信号ビット幅：３２
・ 入力データ信号同期クロック：クロック４６２
・ 入力制御信号名：信号４６１
・ 入力制御信号ビット幅：１
・ 入力制御信号同期クロック：クロック４６２
・ 出力データ信号名：信号４６４
・ 出力データ信号ビット幅：３２
・ 出力データ信号同期クロック：クロック４６３
・ 下位階層回路情報（往路）１：７１１
・ 下位階層回路情報（復路）１：７０３
非同期回路構造が判明すると、その非同期回路構造が満たすべき動作も決まってくる。その動作をモニタするアサーション情報を、ライブラリに登録された回路パーツ情報に基づいて検証情報として出力することにより、論理検証シミュレーション等の非同期検証において非同期回路構造が動作を保障できない入力をその周囲の同期論理回路から得ることがあるか否かを確認することができる。アサーション情報とは、論理回路の入出力信号間で成立すべき条件を定義したものである。このようなアサーション情報を定義する言語として、ＰＳＬ（Ｐｒｏｐｅｒｔｙ Ｓｐｅｃｉｆｉｃａｔｉｏｎ Ｌａｎｇｕａｇｅ）、ＳＶＡ（Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ Ａｓｓｅｒｔｉｏｎ）等がある。

図１０に、回路情報７１２のアサーション情報をアサーション言語であるＰＳＬで記述した例を示す。図１０において、ＳＴＢ＿ＣＤＣは配線４５１を伝播する信号を、ＲＤＹ＿ＣＤＣは配線４５２を伝播する信号を表している。図１０には、非同期配線４５１および４５２を伝播する信号がそれぞれ有効になったときの他の信号のアサーション情報が定義されている。ＳＴＢ＿ＳＹＮＣは配線４５４を伝播する信号を、ＲＤＹ＿ＰＲＥは配線４５５を伝播する信号を表している。このような記述をライブラリに登録しておき、該当する非同期回路パーツ情報が検出された際に、回路パーツ情報の動的チェック情報として検証情報へ出力する。これにより、非同期回路構造に適したアサーション情報を与えることができ、非同期回路の検証を効率よく行うことができる。

また図４の回路パーツ情報２４１は、非同期の影響が他の論理回路に及ばない、非同期の論理構造としての最小単位である。非同期回路の最小単位である旨を回路パーツ情報２４１の回路情報として登録しておき、検証情報として出力することにより、設計者による非同期回路の検証範囲を明確にすることができる。この結果、設計者の検証効率を向上させることができる。

図１１に、本実施例により抽出された各階層における検証情報同士の結合関係を示す。下位階層９０１、中間階層９０２、上位階層９０３、および最上位階層９０４に属する検証情報９１０から９２２は、それぞれ固有のｐｏｉｎｔｅｒすなわち検証情報に対応するアドレスを有している。それぞれの検証情報に記載されているＣａｔ．はパーツ種類カテゴリを示している。またＮａｍｅはパーツ名を示している。検証情報間の結線は、アドレスの参照関係を表している。例えば中位階層パーツ情報９１８のパーツ構成要素に、下位階層パーツ情報９１０および９１１のアドレス情報（ｐｏｉｎｔｅｒ）を記述することで、検証情報間の結合関係を明確にする。このように、各階層の回路パーツ情報のみならず、上下の階層との結合関係も検証情報として定義しておくことにより非同期回路全体の構造を把握することができ、非同期回路の検証を効率よく進めることができる。

図１２に、コンピュータのハードウェア構成例を示す。コンピュータは表示装置１００１、入力手段１００２、ＣＰＵ１００３、ＲＡＭ１００４、画像処理部１００５、および記憶装置１００７等によって構成され、これらはバス１００６を介して接続されている。また、非同期検証プログラム１００８、ライブラリ１００９、検証情報１０１０、および検証対象の回路配線情報１０１１等が記憶装置１００７に格納されている。

このようなハードウェア構成を有するコンピュータ上で非同期検証プログラム１００８を実行することにより、プログラム中に記載された回路配線検出手段１００３ａ、パーツ情報検出手段１００３ｂ、および検証情報抽出手段１００３ｃがＣＰＵで具体化される。回路配線検出手段１００３ａは図２のステップＳ１０４を実行する。パーツ情報検出手段１００３ｂおよび検証情報抽出手段１００３ｃは図２のステップＳ１０５およびＳ１０７を実行する。

また、処理内容を記述した非同期検証プログラム１００８は、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記録装置、光ディスク、半導体メモリなどがある。

プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭ等の可搬型記憶媒体を用いる。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。

以上説明したように、本発明の非同期回路検証方法および非同期回路検証プログラムでは、論理合成後のスタイルチェック段階において、非同期回路を検出し、ライブラリを参照することで非同期回路をパーツとして抽象化した。そしてパーツごとのスタイルチェック項目、動的チェック情報等を検証情報として出力するようにした。この結果、非同期パス間の動作検証が可能となり、非同期回路の検証効率、検証精度の向上を図ることができる。

図１３は、非同期パスのメタスタビリティにより、出力信号に不安定な期間があることを示している。１１０１から１１０３まではそれぞれレジスタを表している。１１５１ａから１１５３ａまではレジスタ間の信号を示している。１１５４ａおよび１１５５ａはそれぞれ周期および位相の異なる非同期クロックを示している。１１５４ｂはクロック１１５４ａの波形を、１１５１ｂは信号１１５１ａの波形を、１１５５ｂはクロック１１５５ａの波形を、１１５２ｂは信号１１５２ａの波形を、１１５３ｂおよび１１５３ｃは信号１１５３ａで発生し得る波形をそれぞれ示している。図１３の波形図のようにクロック波形１１５４ｂと１１５５ｂとの立ち上がりがほぼ同じタイミングとなった場合、レジスタ１１０２の出力信号１１５２ａは波形１１５２ｂの通り不安定なものとなる。この場合、レジスタ１１０２からの出力信号１１５２ａがハイレベルになったことを、レジスタ１１０３が時刻Ｔ１で判定するかＴ２で判定するかによって、レジスタ１１０３からの出力信号１１５３ａのタイミングは波形１１５３ｂまたは１１５３ｃとなる可能性がある。

図１４はこのような非同期パスが問題を引き起こす一例である。１２０１から１２０４はレジスタを、１２０５はＡＮＤ回路を表している。１２５０ａから１２５３ａはレジスタ１２０１から１２０４の出力信号を表している。１２７０および１２７１は非同期回路である。クロック１２５４ａと１２５５ａとはそれぞれ周期および位相の異なる非同期のクロックである。１２５６ａはＡＮＤ回路１２０５の出力信号である。波形１２５４ｂはクロック１２５４ａを、波形１２５０ｂは信号１２５０ａを、波形１２５１ｂは信号１２５１ａを、波形１２５５ｂはクロック１２５５ａを、波形１２５２ｂは信号１２５２ａを、波形１２５３ｂは信号１２５３ａを示している。メタスタビリティにより、レジスタ１２０２からの出力信号１２５２ａが、レジスタ１２０４からの出力信号１２５３ａに対して波形１２５２ｂと１２５３ｂのように位相ずれを起こすと、ＡＮＤ回路１２０５の出力信号波形１２５６ｂには意図しないパルス１２６３が出力される。このような予期しないパルス１２６３により、回路が誤動作することとなる。非同期回路間の結合関係が不明だと、１つの非同期回路に対して他のすべての非同期回路が関連すると仮定して検証する必要があり、この事実が非同期回路の検証時間の増大、および検証精度の低下の原因となっている。

図１４の回路に対して本実施例を適用する。図１４の非同期回路１２７０および１２７１について、それぞれ回路パーツ情報を参照して検証情報を出力する。さらに上位階層の回路パーツ情報を参照し、ライブラリに回路パーツ情報が登録されていれば２つの非同期回路の関連性を検証情報として出力する。具体的には、信号１２５０と１２５１とがクロック１２５５ａで動作するレジスタ１２０２および１２０４に受け渡された後の信号は信号１２５２ａと１２５３ａである。したがって信号１２５２ａに対し信号１２５３ａは、クロック１２５５ａの入力タイミングで−１、０、または＋１の３通りの周期差が生じうることをカバレッジ情報として、検証情報に出力する。

図１５は前記３通りの周期差を時間波形で図示したものである。１３０１は信号１２５２ａに対し信号１２５３ａが１周期遅れた時の時間波形を、１３０２は信号１２５２ａと信号１２５３ａが同一のタイミングとなったときの時間波形を、１３０３は信号１２５２ａに対し信号１２５３ａが１周期進んだ時の時間波形を示している。

以上の通り、非同期パス間の信号伝播タイミング条件を出力した検証情報をタイミング検証に用いることにより、非同期回路を含む論理回路の検証効率および検証精度を向上させることができる。

以下に本発明の特徴を付記する。
（付記１）
論理回路と該論理回路間を接続する配線とを有する回路情報の回路動作を検証する装置による回路検証方法であって、
レジスタ間が配線により接続され、該レジスタにはそれぞれ異なるクロックが供給される非同期回路情報を前記回路情報から複数検出し、
異なる回路構成を有する複数の非同期回路パーツ情報を記憶したライブラリから前記非同期回路情報の１つである第一非同期回路情報と一致する第一非同期回路パーツ情報を検出し、
前記非同期回路情報の１つである第二非同期回路情報と一致する第二非同期回路パーツ情報を前記ライブラリから検出し、
前記第一非同期回路情報と前記第二非同期回路情報とを含む第三非同期回路情報と一致する第三非同期回路パーツ情報を前記ライブラリから検出すると共に該第三非同期回路情報の回路動作を検証する第三検証情報を抽出する
ことを特徴とする回路検証方法。
（付記２）
前記第一非同期パーツ情報の検出は、前記第一非同期回路情報の回路動作を検証する第二検証情報を抽出することを含み、
前記第二非同期パーツ情報の検出は、前記第二非同期回路情報の回路動作を検証する第二検証情報を抽出することを含む、付記１に記載の回路検証方法。
（付記３）
前記第三非同期回路パーツ情報の検出は、前記第一非同期回路情報と前記第二非同期回路情報とを合わせて新たな非同期回路情報が構成される場合に行うことを特徴とする、付記１に記載の回路検証方法。
（付記４）
前記第三検証情報は、検証済みの前記第一非同期回路情報と前記第二非同期回路情報とをそれぞれ１つの検証済み回路情報として置き換え、該検証済み回路情報を除いた前記第三非同期回路情報を検証する検証情報であることを特徴とする、付記２に記載の回路検証方法。
（付記５）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、該非同期回路情報に対応する前記非同期回路パーツ情報に基づいて行われることを特徴とする、付記１に記載の回路検証方法。
（付記６）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、前記レジスタ間に接続され、かつレジスタを含まない論理回路情報を組み合わせ回路情報として抽出することを含む、付記１に記載の回路検証方法。
（付記７）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、前記非同期回路情報が期待値通りに論理動作することを検証するアサーション情報を抽出することを含む、付記１に記載の回路検証方法。
（付記８）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、前記非同期回路情報間のカバレッジ情報を抽出することを含む、付記１に記載の回路検証方法。
（付記９）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、前記非同期回路パーツ情報に含まれるスタイルチェック項目情報に基づいてスタイルチェック結果情報を抽出することを含む、付記１に記載の回路検証方法。
（付記１０）
論理回路の情報と配線の情報とを有する回路配線情報の回路動作を検証するコンピュータを動作させる回路検証プログラムであって、
コンピュータを
レジスタ間が配線により接続され、該レジスタにはそれぞれ異なるクロックが供給される非同期回路情報を前記回路情報から複数検出する回路配線検出手段、
異なる回路構成を有する複数の非同期回路パーツ情報を記憶したライブラリから前記非同期回路情報の１つである第一非同期回路情報と一致する第一非同期回路パーツ情報を検出し、前記非同期回路情報の１つである第二非同期回路情報と一致する第二非同期回路パーツ情報を前記ライブラリから検出し、前記第一非同期回路情報と前記第二非同期回路情報とを含む第三非同期回路情報と一致する第三非同期回路パーツ情報を前記ライブラリから検出するパーツ情報検出手段、
前記第三非同期回路情報の回路動作を検証する第三検証情報を抽出する検証情報抽出手段、
として機能させるための回路検証プログラム。
（付記１１）
前記検証情報抽出手段は、さらに前記第一非同期回路情報の回路動作を検証する第一検証情報を抽出し、前記第二非同期回路情報の回路動作を検証する第二検証情報を抽出することを特徴とする、付記１０に記載の回路検証プログラム。
（付記１２）
前記検証情報抽出手段は、前記第一非同期回路情報と前記第二非同期回路情報とを合わせて新たな非同期回路情報が構成される場合に実行することを特徴とする、付記１０に記載の回路検証プログラム。
（付記１３）
前記検証情報抽出手段は、検証済みの前記第一非同期回路情報と前記第二非同期回路情報とをそれぞれ１つの検証済み回路情報として置き換え、該検証済み回路情報を除いた前記第三非同期回路情報を検証する検証情報を抽出することを特徴とする、付記１１に記載の回路検証プログラム。
（付記１４）
前記非同期回路情報の回路動作を検証する検証情報の抽出は、該非同期回路情報に対応する前記非同期回路パーツ情報に基づいて行われることを特徴とする、付記１０に記載の回路検証プログラム。
（付記１５）
前記検証情報抽出手段は、前記レジスタ間に接続され、かつレジスタを含まない論理回路情報を組み合わせ回路情報として抽出することを含む、付記１０に記載の回路検証プログラム。
（付記１６）
前記検証情報抽出手段は、前記非同期回路情報が期待値通りに論理動作することを検証するアサーション情報を抽出することを含む、付記１０に記載の回路検証プログラム。
（付記１７）
前記検証情報抽出手段は、前記非同期回路情報間のカバレッジ情報を抽出することを含む、付記１０に記載の回路検証プログラム。
（付記１８）
前記検証情報抽出手段は、前記非同期回路パーツ情報に含まれるスタイルチェック項目情報に基づいてスタイルチェック結果情報を抽出することを含む、付記１０に記載の回路検証プログラム。

非同期検証対象である非同期回路の一例である。 非同期検証方法のフローである。 ライブラリの概念図（最下層および中間層）である。 ライブラリの概念図（上位層および最上位層）である。 ライブラリの回路パーツ情報と検証情報の対応関係図である。 回路パーツ情報抽出から検証情報出力までのフローである。 非同期回路を下位階層パーツ情報により抽象化したものである。 非同期配線経路に組み合わせ回路が存在する非同期回路の一例である。 非同期回路を中間階層パーツ情報により抽象化したものである。 ライブラリに登録されているアサーション情報の一例である。 本実施例により抽出された検証情報間の関係を示したものである。 本実施例を実行するためのコンピュータの一例である。 非同期回路のメタステーブルを説明するための図である。 非同期回路のメタステーブルにより生じる問題を説明するための図である。 非同期回路に生じうるタイミングのずれを説明するための図である。

符号の説明

１０５ ライブラリ
１５０ 回路配線
１５１ 回路情報
２０１〜２０４ ライブラリの各階層
２１１ａ〜２１１ｃ マルチプレクサ
２１２ａ〜２１２ｅ 組み合わせ回路
２１３ａ〜２１３ｆ レジスタ
２１４ａ、２１４ｂ シンクロナイザ
２１５、２１６ ライブラリの各回路パーツ情報
２５０〜２５７ ライブラリの各回路パーツ情報
２２１ａ，２２１ｂ データ転送非同期パス情報
２２２ａ〜２２２ｃ コントロール転送非同期パス情報
２３１ａ〜２３１ｄ コントロールデータ転送構造
２４１ ハンドシェイク構造
３０１ 回路パーツ情報
３０２ 検証情報
３１１、３１６ パーツの固有識別情報
３１２、３１７ パーツの構成要素
３１３ パーツのスタイルチェック項目
３１４、３１９ パーツの動的チェック情報
３１５、３２０ パーツの個別情報
３１８ パーツのスタイルチェック結果
４０１〜４０９ ライブラリ参照対象回路情報
４２１〜４３０ レジスタ
４３１、４３２ セレクタ
４５０〜４５８ 配線
４５１ａ、４５１ｂ 配線
４６０〜４６５ 信号
５０１〜５０９ 検証情報出力後の回路情報
５１１〜５１３ ライブラリ参照対象回路情報
６０１ 組み合わせ回路
７０１〜７０３ 検証情報出力後の回路情報
９０１〜９０４ テーブルの各階層
９０１ａ、９０１ｂ 下位階層に属するテーブル
９０２ａ 中間階層に属するテーブル
１００１ 表示装置
１００２ 入力手段
１００３ ＣＰＵ
１００３ａ 回路配線検出手段
１００３ｂ パーツ情報検出手段
１００３ｃ 検証情報抽出手段
１００４ ＲＡＭ
１００５ 画像処理部
１００６ バス
１００７ 記憶装置
１００８ 非同期検証プログラム
１００９ ライブラリ
１０１０ 検証情報
１０１１ 回路配線情報
１１０１〜１１０３ レジスタ
１２０１〜１２０４ レジスタ
１２０５ ＡＮＤ回路
１２５０ａ〜１２５６ａ 信号
１２５０ｂ〜１２５６ｂ 信号波形
１２７０、１２７１ 非同期回路
１３０１〜１３０３ 非同期回路における周期差の組み合わせ
１２５２ｃ〜１２５２ｅ 信号１２５２ａの信号波形
１２５３ｃ〜１２５３ｅ 信号１２５３ａの信号波形

Claims (10)

1. 回路情報に基づいて回路の動作を検証するコンピュータによる回路検証方法であって、
   前記コンピュータが、それぞれ異なるクロックが供給されるレジスタ間を配線により接続した非同期回路に関する非同期回路情報を、前記回路情報から複数検出し、
   前記コンピュータが、異なる回路構成を有する複数の非同期回路パーツ情報を含む、記憶装置に格納されたライブラリから、前記非同期回路情報のうち１つに対応する第一非同期回路パーツ情報を検出し、
   前記コンピュータが、前記非同期回路情報のうち他の１つに対応する第二非同期回路パーツ情報を前記ライブラリから検出し、
   前記コンピュータが、前記第一非同期回路パーツ情報及び前記第二非同期回路パーツ情報に基づいて、第一非同期回路と第二非同期回路とを含む回路に対応する第三非同期回路パーツ情報を前記ライブラリから検出し、
   前記コンピュータが、前記第三非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第三非同期回路の回路動作を検証する第三検証情報を抽出する
   ことを特徴とする回路検証方法。
2. 前記第一非同期回路パーツ情報の検出は、前記第一非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第一非同期回路の回路動作を検証する第一検証情報を抽出することを含み、
   前記第二非同期回路パーツ情報の検出は、前記第二非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第二非同期回路の回路動作を検証する第二検証情報を抽出することを含む、請求項１に記載の回路検証方法。
3. 前記第三非同期回路パーツ情報の検出は、前記第一非同期回路と前記第二非同期回路とを合わせて新たな非同期回路が構成される場合に行うことを特徴とする、請求項１に記載の回路検証方法。
4. 前記第三検証情報は、検証済みの前記第一非同期回路と前記第二非同期回路とをそれぞれ１つの検証済み回路として置き換え、該検証済み回路を除いた前記第三非同期回路を検証する検証情報であることを特徴とする、請求項２に記載の回路検証方法。
5. 前記非同期回路の回路動作を検証する検証情報の抽出は、前記レジスタ間に接続され、かつレジスタを含まない論理回路に関する論理回路情報を組み合わせ回路情報として抽出することを含む、請求項１に記載の回路検証方法。
6. 回路情報に基づいて回路の回路動作を検証するコンピュータを動作させる回路検証プログラムであって、
   コンピュータを
   それぞれ異なるクロックが供給されるレジスタ間を配線により接続した非同期回路に関する非同期回路情報を、前記回路情報から複数検出する回路配線検出手段と、
   異なる回路構成を有する複数の非同期回路パーツ情報を含む、記憶装置に格納されたライブラリから、前記非同期回路情報のうち１つに対応する第一非同期回路パーツ情報を検出し、前記非同期回路情報のうち他の１つに対応する第二非同期回路パーツ情報を前記ライブラリから検出し、前記第一非同期回路パーツ情報及び前記第二非同期回路パーツ情報に基づいて、第一非同期回路と第二非同期回路とを含む回路に対応する第三非同期回路パーツ情報を前記ライブラリから検出するパーツ情報検出手段と、
   前記第三非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第三非同期回路の回路動作を検証する第三検証情報を抽出する検証情報抽出手段、
   として機能させるための回路検証プログラム。
7. 前記検証情報抽出手段は、さらに前記第一非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第一非同期回路の回路動作を検証する第一検証情報を抽出し、前記第二非同期回路パーツ情報に対応付けて記憶装置に格納された、前記第二非同期回路の回路動作を検証する第二検証情報を抽出することを特徴とする、請求項６に記載の回路検証プログラム。
8. 前記パーツ情報検出手段は、前記第一非同期回路と前記第二非同期回路とを合わせて新たな非同期回路が構成される場合に前記第三非同期回路パーツ情報の検出を実行することを特徴とする、請求項６に記載の回路検証プログラム。
9. 前記検証情報抽出手段は、検証済みの前記第一非同期回路と前記第二非同期回路とをそれぞれ１つの検証済み回路として置き換え、該検証済み回路を除いた前記第三非同期回路を検証する検証情報を抽出することを特徴とする、請求項７に記載の回路検証プログラム。
10. 前記検証情報抽出手段は、前記レジスタ間に接続され、かつレジスタを含まない論理回路に関する論理回路情報を組み合わせ回路情報として抽出することを特徴とする、請求項６に記載の回路検証プログラム。

Images