(57)【要約】【課題】  本発明の課題は、非同期クロック間のデータ伝播において、複数の信号が再収斂される受信側の再収斂信号に伝播障害が発生しない回路構造であるか否かを判断可能な回路検証方法を提供することを目的とする。【解決手段】  上記課題は、回路検証装置における回路検証方法であって、該回路検証装置が、一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、を実行することにより達成される。【選択図】  図６
2011034475.tif 000002
【特許請求の範囲】
【請求項１】
回路検証装置における回路検証方法であって、該回路検証装置が、
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、
を実行することを特徴とする回路検証方法。
【請求項２】
前記信号値算出手順は、前記信号変化の組み合わせ毎に、前記複数の信号を再収斂する論理演算を用いて、変化タイミングの違いによる前記再収斂ポイントの論理値を算出することを特徴とする請求項１記載の回路検証方法。
【請求項３】
前記信号値算出手順は、
前記再収斂信号毎に、前記複数の信号から２つの信号を特定してペアを作成するペア作成手順と、
２つの信号の前記信号変化の組み合わせと該組み合わせ毎に前記変化タイミングの違いとを示す信号変化表を参照することによって、前記ペアとなる２つの信号に対して前記再収斂ポイントの論理値を算出する再収斂ポイント値算出手順と、
を有することを特徴とする請求項１又は２記載の回路検証方法。
【請求項４】
前記検証プロパティ作成手順は、
送信側送信側クロックドメインにおいて、送信側クロックの１クロックサイクル内で前記複数の信号が変化しないことを検証する第一検証プロパティを作成する第一作成手順と、
受信側クロックの１クロックサイクル時間に相当する送信側クロックのサイクル数を算出するサイクル数算出手順と、
前記送信側クロックドメインにおいて、現在から前記サイクル数前までの時間で前記複数の信号が変化しないことを検証する第二検証プロパティを作成する第二作成手順と、
を有することを特徴とする請求項１乃至３のいずれか一項記載の回路検証方法。
【請求項５】
コンピュータを回路検証装置として機能させる回路検証プログラムであって、該コンピュータに、
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、
を実行させることを特徴とするコンピュータ実行可能な回路検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＬＳＩ設計における回路検証方法であり、特に、非同期クロック間における再収斂信号に係る回路検証方法及び回路検証プログラムに関する。
【背景技術】
【０００２】
ＬＳＩ設計における論理回路の検証において、従来より、周期が異なる複数のクロックによって非同期で動作する論理回路では、非同期クロック間のデータの受け渡し箇所が複数ありそのデータが受信側において再収斂する場合、再収斂ポイントの値は一定の結果を得られない可能性があった。その理由は、非同期クロック間のクロックドメインの境界でのデータ受け渡しでは、ラッチ回路やフリップフロップ回路における入力信号のセットアップ時間やホールド時間が満たされないことにより、受信側出力信号に対してメタスタビリティが発生する場合があり、そのメタスタビリティによって出力信号が不安定な状態になり、他の回路に対して誤動作を引き起こす原因となる可能性があるからである。メタスタビリティの発生により受信側における複数の信号の変化タイミングが変わってしまい、再収斂ポイントの値は一定の結果を得られない場合がある。
【０００３】
このような問題に対して、検証対象において隣接する一対のクロックドメインのうち一方のクロックドメインからそれぞれデータを出力する２以上のレジスタを指定し、入力された検証対象の論理回路記述情報と、指定された２以上のレジスタとに基づいて、他方のクロックドメインにおいて収斂する単一のレジスタを検出すること等が提案されている（例えば、特許文献１、２を参照）。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２００６−２５２４３８号公報
【特許文献２】特開平６−１８０７３５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
上述した従来技術では、メタスタビリティが発生しそうなレジスタを検出するが、検証プロパティによって受信側のクロックドメインにて伝播する信号の変化タイミングにズレがあると一律に検証プロパティ違反として処理される。検証プロパティ違反によってメタスタビリティが発生すると判断された場合、例えば、送信側のクロックドメインの２以上のレジスタから送出される信号を同期させて受信側のクロックドメインへと供給させる仕組みを持たせるように、論理回路の設計を見直すこととなる。
【０００６】
しかしながら、非同期クロック間でデータ伝播する論理回路部分は膨大にあり、従来技術のように、受信側のクロックドメインに伝播する際の送信側のクロックドメインの信号の変化タイミングのズレを検出し論理回路の設計を見直した場合、変化タイミングのズレが必ずしも動作に影響しない場合であっても、動作保証するための余分な回路設計が行われてしまうと言った問題があった。
【課題を解決するための手段】
【０００７】
開示の回路検証装置における回路検証方法は、該回路検証装置が、一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの値を算出する信号値算出手順と、前記変化タイミングの違いにより前記再収斂ポイントの値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順とを実行する。
【発明の効果】
【０００８】
開示の回路検証方法において、非同期クロック間のデータ伝播において、複数の信号が再収斂される受信側の再収斂信号に伝播障害が発生しない回路構造であるか否かを検証できるため、メタスタビリティ起因の再収斂信号の値にばらつきが発生しないことを判断可能とする。
【図面の簡単な説明】
【０００９】
【図１】周期が異なる複数のクロックによって非同期で動作する回路構成例を示す図である。
【図２】再収斂信号にばらつきのあるラッチタイミングの例を示す図である。
【図３】変化タイミング間隔を説明するための図である。
【図４】再収斂信号にばらつきがないラッチタイミングの例を示す図である。
【図５】回路検証装置のハードウェア構成を示す図である。
【図６】回路検証装置の機能構成例を示す図である。
【図７】再収斂信号に係る処理を説明するためのフローチャート図である。
【図８】２つのソース信号のサイクルずれを説明するための図（その１）である。
【図９】２つのソース信号のサイクルずれを説明するための図（その２）である。
【図１０】信号変化表の例を示す図である。
【図１１】再収斂ポイント値算出部で行われる処理を説明するためのフローチャート図である。
【図１２】検証プロパティ作成処理を説明するためのフローチャート図である。
【図１３】再収斂ポイント値算出結果を示す図である。
【図１４】変化タイミングずれによって再収斂ポイントの論理値が異なる例を説明する図である。
【発明を実施するための形態】
【００１０】
以下、本発明の実施の形態を図面に基づいて説明する。発明者は、ＬＳＩ設計における周期が異なる複数のクロックによって非同期で動作する回路検証において、受信側のクロックドメインにて再収斂ポイントの論理値のばらつきを発生させる可能性のある複数の送信側信号間において、受信側クロックの１クロックサイクル時間内の信号変化がない場合に、メタスタビリティ起因の再収斂信号の値にばらつきが発生しないことに着目した。この着目点に基づいた回路検証方法が以下に説明される。
【００１１】
先ず、検証対象となる回路構成例について図１で説明する。図１は、周期が異なる複数のクロックによって非同期で動作する論理回路の構成例を示す図である。図１に示す回路構成３は、クロックＣＬＫ１で論理回路が動作する第１クロックドメインと、クロックＣＬＫ２で論理回路が動作する第２クロックドメインとを有し、第１クロックドメインから第２クロックドメインへと信号が伝播する構成となる。例えば、クロックＣＬＫ１は、クロックＣＬＫ２より周期が短く、第１クロックドメインでの動作は、第２クロックドメインでの動作より高速であるとする。
【００１２】
この構成例では、第１クロックドメインには、レジスタ３−Ａと、レジスタ３−Ｂとが配置され、第２クロックドメインには、レジスタ３−Ａ１及び３−Ａ２と、レジスタ３−Ｂ１及び３−Ｂ２と、ＡＮＤ回路４と、レジスタ３−Ｃとが配置される。
【００１３】
第１クロックドメインのレジスタ３−Ａから信号Ａが、第２クロックドメインのレジスタ３−Ａ１へ伝播し、第２クロックドメイン内にてレジスタ３−Ａ１からレジスタ３−Ａ２へ信号Ａ１として伝播して、レジスタ３−Ａ２からＡＮＤ回路４に信号Ａ２として入力される。
【００１４】
一方、第１クロックドメインのレジスタ３−Ｂから信号Ｂが、第２クロックドメインのレジスタ３−Ｂ１へ伝播し、第２クロックドメイン内にてレジスタ３−Ｂ１からレジスタ３−Ｂ２へ信号Ｂ１として伝播して、レジスタ３−Ｂ２からＡＮＤ回路４に信号Ｂ２として反転して入力される。ＡＮＤ回路４は信号Ａ２と反転された信号Ｂ２との論理積をレジスタＣ−３に出力する。この論理積が再収斂信号ＣでありレジスタＣ−３に伝播する。ＡＮＤ回路４により第１クロックドメインの元の信号Ａと信号Ｂとが収斂されたポイントを再収斂ポイントＰｃで示される。
【００１５】
このような回路構成３におけるクロックＣＬＫ１に於ける信号Ａと信号Ｂの変化が、クロックＣＬＫ２による受信側の第２クロックドメインにおいてメタスタビリティにより発生する再収斂信号Ｃのばらつきについて説明する。
【００１６】
図２は、再収斂信号にばらつきのあるラッチタイミングの例を示す図である。図２（Ａ）に示すラッチタイミング１の例では、第１クロックドメインにおける信号Ａの立ち上がりａは、第２クロックドメインにおいて時刻ｔ＋１の信号Ａ１の立ち上がりと時刻ｔ＋２の信号Ａ２の立ち上がりによって伝播され、第１クロックドメインにおける信号Ｂの立ち上がりｂは、第２クロックドメインにおいて時刻ｔ＋２の信号Ｂ１の立ち上がりと時刻ｔ＋３の信号Ｂ２の立ち上がりによって伝播される。その結果、時刻ｔ＋２からｔ＋３の期間、信号Ａ２のＨｉｇｈの状態と信号Ｂ２のＬｏｗの状態とにより再収斂信号Ｃはこの期間だけＨｉｇｈの状態となる。
【００１７】
一方、図２（Ｂ）に示すラッチタイミング２の例では、第１クロックドメインにおける信号Ａの立ち上がりａは、第２クロックドメインにおいて時刻ｔ＋２の信号Ａ１の立ち上がりと時刻ｔ＋３の信号Ａ２の立ち上がりによって伝播され、第１クロックドメインにおける信号Ｂの立ち上がりｂは、第２クロックドメインにおいて時刻ｔ＋２の信号Ｂ１の立ち上がりと時刻ｔ＋３の信号Ｂ２の立ち上がりによって伝播される。その結果、信号Ａ２と信号Ｂ２とが同時刻にＨｉｇｈの状態又はＬｏｗの状態となるため、いずれの時刻においても再収斂信号ＣはＬｏｗの状態を維持する。
【００１８】
このように、受信側の第２クロックドメインにおいて複数の信号の変化順序が一定とならないのは、送信側の第１クロックドメインにおいて受信側のクロックＣＬＫ２の１クロックサイクル時間内に送信側の信号が変化してしまうためである。
【００１９】
図３は、変化タイミング間隔を説明するための図である。図３において、第１クロックドメインにおける信号Ａと信号Ｂの変化タイミング間隔４ｃが受信側の第２クロックドメインの１クロックサイクル未満であることを示している。つまり、送信側の信号Ａ及びＢが、受信側のクロックＣＬＫ２の１クロックサイクル時間内に変化しなければ、受信側の第２クロックドメインにおける信号Ａ１、Ａ２の変化順序及び信号Ｂ１、Ｂ２の変化順序は一定となり、メタスタビリティ起因の再収斂信号の値のばらつきは発生しない。
【００２０】
また、受信側のクロックＣＬＫ２の１クロックサイクル時間内に送信側の信号Ａ及びＢが変化しても、受信側の再収斂ポイントＰｃにて論理的に値が変化しないのであれば、この状態もまたメタスタビリティ起因の再収斂信号値のばらつきは発生しないといえる。図１に示す回路構成３で、再収斂信号Ｃのばらつきが発生しない例を図４で説明する。
【００２１】
図４は、再収斂信号にばらつきがないラッチタイミングの例を示す図である。図４（Ａ）に示すラッチタイミング１−２の例では、第１クロックドメインにおける信号Ａの立ち下がりａ−２は、第２クロックドメインにおいて時刻ｔ＋１の信号Ａ１の立ち下がりと時刻ｔ＋２の信号Ａ２の立ち下がりによって伝播され、第１クロックドメインにおける信号Ｂの立ち下がりｂ−２は、第２クロックドメインにおいて時刻ｔ＋２の信号Ｂ１の立ち下がりと時刻ｔ＋３の信号Ｂ２の立ち下がりによって伝播される。その結果、時刻ｔ＋２からｔ＋３の期間、信号Ａ２のＨｉｇｈの状態と信号Ｂ２のＬｏｗの状態とにより再収斂信号Ｃはこの期間だけＨｉｇｈの状態となる。その結果、信号Ａ２のＨｉｇｈの状態と信号Ｂ２のＬｏｗの状態とが重なることがないため、いずれの時刻においても再収斂信号ＣはＬｏｗの状態を維持する。
【００２２】
一方、図４（Ｂ）に示すラッチタイミング２−２の例では、第１クロックドメインにおける信号Ａの立ち下がりａ−２は、第２クロックドメインにおいて時刻ｔ＋２の信号Ａ１の立ち下がりと時刻ｔ＋３の信号Ａ２の立ち下がりによって伝播され、第１クロックドメインにおける信号Ｂの立ち下がりｂ−２は、第２クロックドメインにおいて時刻ｔ＋２の信号Ｂ１の立ち下がりと時刻ｔ＋３の信号Ｂ２の立ち下がりによって伝播される。その結果、信号Ａ２と信号Ｂ２とが同時刻にＨｉｇｈの状態又はＬｏｗの状態となるため、いずれの時刻においても再収斂信号ＣはＬｏｗの状態を維持する。
【００２３】
このように、ラッチタイミング１−２及び２−２の間で、信号Ａのサイクルずれが第２クロックドメインにおいて発生しているが、再収斂信号Ｃは同じ値を取っている。
【００２４】
従って、「受信側の再収斂ポイントＰｃにて論理的に値のばらつきを発生させる可能性のある送信側での複数の信号Ａ及びＢとの間において、受信側のクロックＣＬＫ２の１クロックサイクル時間内の信号変化がない」ことが保証されれば、対象となる非同期回路の構造には問題ないと言える。
【００２５】
つまり、ＬＳＩ内の同期関係にない複数のクロックを持つ構造の回路において、非同期クロック間のデータ受け渡し箇所がありそのデータが受信側において再収斂したとしても、再収斂ポイントＰｃの論理値が一定の結果を得ることができることが保証できれば、検証対象となる非同期構造の回路を包含していたとしてもＬＳＩ全体として回路構造的に問題はないと言える。以下に、この再収斂ポイントＰｃの論理値が一定の結果を得られることを証明するための論理回路の検証方法について説明する。
【００２６】
本実施例に係る論理回路の検証方法を実行する回路検証装置は、例えば、図５に示すハードウェア構成を成す。図５は、回路検証装置のハードウェア構成を示す図である。図５において、回路検証装置１００は、コンピュータによって制御される装置であって、ＣＰＵ（Central Processing Unit）１１と、メモリユニット１２と、表示ユニット１３と、出力ユニット１４と、入力ユニット１５と、通信ユニット１６と、記憶装置１７と、ドライバ１８とを有し 、システムバスＢに接続される。
【００２７】
ＣＰＵ１１は、メモリユニット１２に格納されたプログラムに従って回路検証装置１００を制御する。メモリユニット１２には、ＲＡＭ（Random Access Memory）及びＲＯＭ（Read-Only Memory）等が用いられ、ＣＰＵ１１にて実行されるプログラム、ＣＰＵ１１での処理に必要なデータ、ＣＰＵ１１での処理にて得られたデータ等を格納する。また、メモリユニット１２の一部の領域が、ＣＰＵ１１での処理に利用されるワークエリアとして割り付けられている。
【００２８】
表示ユニット１３は、ＣＰＵ１１の制御のもとに必要な各種情報を表示する。出力ユニット１４は、プリンタ等を有し、利用者からの指示に応じて各種情報を出力するために用いられる。入力ユニット１５は、マウス、キーボード等を有し、利用者が回路検証装置１００が処理を行なうための必要な各種情報を入力するために用いられる。通信ユニット１６は、例えばインターネット、ＬＡＮ（Local Area Network）等に接続し、他装置との間の通信制御をするための装置である。記憶装置１７には、例えば、ハードディスクユニットが用いられ、各種処理を実行するプログラム等のデータを格納する。
【００２９】
回路検証装置１００よって行われる処理を実現するプログラムは、例えば、ＣＤ−ＲＯＭ（Compact Disc Read-Only Memory）等の記憶媒体１９によって回路検証装置１００に提供される。即ち、プログラムが保存された記憶媒体１９がドライバ１８にセットされると、ドライバ１８が記憶媒体１９からプログラムを読み出し、その読み出されたプログラムがシステムバスＢを介して記憶装置１７にインストールされる。そして、プログラムが起動されると、記憶装置１７にインストールされたプログラムに従ってＣＰＵ１１がその処理を開始する。尚、プログラムを格納する媒体としてＣＤ−ＲＯＭに限定するものではなく、コンピュータが読み取り可能な媒体であればよい。本実施例に係る処理を実現するプログラムは、通信ユニット１６によってネットワークを介してダウンロードし、記憶装置１７にインストールするようにしても良い。また、ＵＳＢ対応の回路検証装置１００であれば、ＵＳＢ接続可能な外部記憶装置からインストールするようにしても良い。更に、ＳＤカード等のフラッシュメモリ対応の回路検証装置１００であれば、そのようなメモリカードからインストールするようにしても良い。
【００３０】
図６は、回路検証装置の機能構成例を示す図である。図６において、回路検証装置１００は、回路記述部２１と、再収斂信号解析部２２と、論理演算抽出部２３と、再収斂ポイント値算出部２４と、検証プロパティ作成部２５と、形式的検証部２６とを有する。回路検証装置１００は、ＣＰＵ１１が本実施例に係るプログラムを実行することによって各処理部２１〜２６として機能する。また、回路検証装置１００は、回路記述情報５１と、クロックドメインＤＢ５２と、再収斂信号ＤＢ５３と、論理回路ＤＢ５４と、異値信号ペアＤＢ５５と、検証プロパティＤＢ５６とを有し、各データベース（ＤＢ）５１〜５６はメモリユニット１２又は記憶装置１７の記憶領域に格納される。
【００３１】
回路記述部２１は、設計者によるＲＴＬ（Register Transfer Level）などのハードウェア記述言語を用いた回路記述を支援する処理部であり、ハードウェア記述言語を用いて設計されたＬＳＩは回路記述情報５１に出力される。
【００３２】
再収斂信号解析部２２は、回路記述情報５１とクロックドメインＤＢ５２とを参照して、あるクロックドメインから他のクロックドメインへと伝播する信号を解析して、２以上の信号が伝播した受信側のクロックドメインにて再収斂する再収斂信号を特定し、特定した再収斂信号の識別情報と再収斂信号が属するクロックドメインを示すドメイン情報とを含む再収斂信号情報を再収斂信号ＤＢ５３に出力する。クロックドメインＤＢ５２は、クロック信号毎に１クロックサイクル値を含む属性等を格納するデータベースである。
【００３３】
論理演算抽出部２３は、再収斂信号ＤＢ５３に格納されている再収斂信号情報に対して、回路記述情報５１を参照することによって、伝播される２以上の信号を収斂する論理演算を抽出し、再収斂信号情報に対応させて抽出した論理演算に係る回路情報を論理回路ＤＢ５４に出力する。
【００３４】
再収斂ポイント値算出部２４は、再収斂信号ＤＢ５３に格納されている再収斂信号情報毎に、再収斂信号が属するクロックドメインにおいて、論理回路ＤＢ５４に格納される回路情報から論理演算を試行することによって、再収斂される２つのソース信号の変化の組み合わせ毎に、サイクルずれの発生による再収斂ポイントＰｃでの論理的な変化値を算出する。再収斂ポイント値算出部２４は、サイクルずれによって再収斂ポイントＰｃの論理値が異なる信号変化の組み合わせ毎に、２つのソース信号の識別情報を異値信号ペアＤＢ５５に出力する。
【００３５】
検証プロパティ作成部２５は、サイクルずれによって再収斂ポイントＰｃでの論理値が一致しない信号変化の組み合わせに対して検証プロパティを生成して、検証プロパティＤＢ５６に出力する。
【００３６】
形式的検証部２６は、回路記述情報５１を読み込んで、検証プロパティＤＢ５６を用いて設計した論理回路を検証する。検証プロパティＤＢ５６には、サイクルずれによって再収斂ポイントＰｃでの論理値が一致しない信号変化の組み合わせに対する検証プロパティが含まれていることにより、非同期クロック間のデータ受け渡し箇所がありそのデータが受信側において再収斂したとしても、再収斂ポイントＰｃの論理値が一定の結果を得ることができるか否かを検証することができ、一定の結果を得られた場合に、検証対象となった非同期回路の構造には問題がないことを示したことになる。
【００３７】
次に、再収斂信号解析部２２から形式的検証部２６によって行われる再収斂信号に係る処理について図７で説明する。図７は、再収斂信号に係る処理を説明するためのフローチャート図である。図７において、再収斂信号解析部２２によって、回路記述情報５１とクロックドメインＤＢ５２とを参照して再収斂信号を特定し、特定した再収斂信号の識別情報と再収斂信号が属するクロックドメインを示すドメイン情報とを含む再収斂信号情報を再収斂信号ＤＢ５３に出力する（ステップＳ１１）。
【００３８】
再収斂信号ＤＢ５３を参照して、再収斂信号が有ったか否かを判断し（ステップＳ１２）、再収斂信号が無かった場合、この処理を終了する。一方、再収斂信号が有った場合、論理演算抽出部２３によって、再収斂信号ＤＢ５３に格納されている再収斂信号情報に対して、回路記述情報５１を参照することによって、２以上の信号が伝播されて再収斂信号に到達する論理演算を抽出し、再収斂信号情報に対応させて抽出した論理演算に係る回路情報を論理回路ＤＢ５４に出力する（ステップＳ１３）。
【００３９】
再収斂ポイント値算出部２４によって、再収斂される２つのソース信号の変化の組み合わせ毎に、サイクルずれの発生による再収斂ポイントＰｃでの論理的な変化値を算出して、サイクルずれによって再収斂ポイントＰｃの論理値が異なる信号変化の組み合わせ毎に、２つのソース信号の識別情報を異値信号ペアＤＢ５５に出力する（ステップＳ１４）。
【００４０】
異値信号ペアＤＢ５５を参照して、信号変化の組み合わせに寄っては異なる値となるソース信号のペアが有ったか否かを判断し（ステップＳ１５）、ソース信号のペアが無かった場合、この処理を終了する。一方、ソース信号のペアが有った場合、検証プロパティ作成部２５によって、サイクルずれによって再収斂ポイントＰｃでの論理値が一致しない信号変化の組み合わせに対して検証プロパティを生成して、検証プロパティＤＢ５６に出力する（ステップＳ１６）。
【００４１】
そして、形式的検証部２６は、検証プロパティＤＢ５６を用いて、回路記述情報５１の論理回路を検証する形式的検証を実施する（ステップＳ１７）。形式的検証部２６は、形式的検証の結果、非同期に対する回路構造に違反が有ったか否かを判断し（ステップＳ１８）、違反が無かった場合、この処理を終了する。一方、違反が有った場合、非同期に対する回路構造に違反が有ったことを示すメッセージを表示ユニット１３に表示して（ステップＳ１９）、この処理を終了する。
【００４２】
以下に、再収斂ポイント値算出部２４での処理について説明する。図８は、２つのソース信号のサイクルずれを説明するための図（その１）である。図８（Ａ）では、受信側における２つのソース信号ｘ及び信号ｙの立ち上がりの変化タイミングにサイクルずれある場合を説明するための図である。図８（Ａ）において、信号ｘが０→１の立ち上がり変化、及び信号ｙが０→１の立ち上がり変化をする場合である。信号ｘが１サイクルずれを発生した場合が点線で示される。この場合の再収斂ポイントＰｃにおける信号ｘと信号ｙとの論理値の組み合わせが図８（Ｂ）に示される。
【００４３】
論理回路ＤＢ５４を参照することによって、図８（Ｂ）に示す変化タイミングａ及びｂ毎の再収斂ポイントＰｃの論理に通して、変化タイミングａ及びｂの各論理の結果、すなわち、再収斂値が変化タイミングａとｂとで同じ値であれば、この信号変化においてメタスタビリティによる値のばらつきは発生しないと言える。逆に異なる値であれば、この信号変化においてはメタスタビリティによる値のばらつきが発生する可能性があると言え、この信号変化は検証対象となり、異値信号ペアＤＢ５５に格納される。
【００４４】
図９は、２つのソース信号のサイクルずれを説明するための図（その２）である。図９（Ａ）において、信号ｘが０→１の立ち上がり変化、及び信号ｙが０→１の立ち上がり変化をする場合である。信号ｙが１サイクルずれを発生した場合が点線で示される。この場合の再収斂ポイントＰｃにおける信号ｘと信号ｙとの値の組み合わせが図９（Ｂ）に示される。
【００４５】
同様に、論理回路ＤＢ５４を参照することによって、図９（Ｂ）に示す変化タイミングａ及びｂ毎の再収斂ポイントＰｃの論理に通して、変化タイミングａ及びｂの各論理の結果、すなわち、再収斂値が変化タイミングａ及びｂで同じ値であれば、この信号変化においてメタスタビリティによる値のばらつきは発生しないと言える。逆に異なる値であれば、この信号変化においてはメタスタビリティによる値のばらつきが発生する可能性があると言え、この信号変化は検証対象となり、異値信号ペアＤＢ５５に格納される。
【００４６】
上述したように、２つのソース信号変化（０→１、１→０）の値の組み合わせは、例えば、図１０に示すような信号変化表で示される。図１０は、信号変化表の例を示す図である。図１０に示す信号変化表６は、ソース信号ｘの０→１への変化とソース信号ｙの０→１への変化の一の組み合わせにおいて、ソース信号ｘが１サイクルずれで変化する場合と、ソース信号ｙが１サイクルずれで変化する場合の２通りがある。従って、この一の組み合わせにおいて、信号変化表６では、ソース信号ｘが１サイクルずれで変化する場合を含み、ソース信号ｘ及びｙ両方にずれがない場合の再収斂ポイントＰｃの論理値を比較するものを組合番号１とし、また、ソース信号ｙが１サイクルずれで変化する場合を含み、ソース信号ｘ及びｙ両方にずれがない場合の再収斂ポイントＰｃの論理値を比較するものを組合番号２で管理されるものとする。
【００４７】
同様に、ソース信号ｘの０→１への変化とソース信号ｙの１→０への変化の組み合わせ、ソース信号ｘの１→０への変化とソース信号ｙの０→１への変化の組み合わせ、ソース信号ｘの１→０への変化とソース信号ｙの１→０への変化の組み合わせ毎に変化タイミングのずれにより２通りずつ有り、組合は全体で８通りとなる。
【００４８】
この信号変化表６を用いて、再収斂ポイントＰｃの論理値の比較を行い、異なる値が算出された組合番号の信号変化に対してプロパティ記述が行われる。異なる値の組み合わせに対して行うことにより、擬似的なエラー検出を防ぐことができる。
【００４９】
次に、再収斂ポイント値算出部２４で行われる処理について図１１で説明する。図１１は、再収斂ポイント値算出部で行われる処理を説明するためのフローチャート図である。図１１において、再収斂ポイント値算出部２４は、再収斂信号ＤＢ５３から順に再収斂信号の情報を取り出して、各再収斂ポイントＰｃに対して複数のソース信号から２つの信号を特定してペアを作成する（ステップＳ４１）。例えば、再収斂信号ＤＢ５３の識別情報で識別される再収斂信号を出力する論理回路へ入力される２つの信号を、回路記述情報５１を参照することによって特定すればよい。
【００５０】
再収斂ポイント値算出部２４は、信号変化表６に基づき、２つのソース信号の再収斂ポイントＰｃでの論理値を論理回路ＤＢ５４を参照して算出する（ステップＳ４２）。そして、信号変化表６の組み合わせを全て実施したか否かを判断し（ステップＳ４３）、全て実施していない場合は、ステップＳ４２へと戻り上述同様の処理を繰り返す。
【００５１】
一方、信号変化表６の組み合わせを全て実施した場合、再収斂ポイント値算出部２４は、全てのペアを作成したか否かを判断し（ステップＳ４４）、全てのペアを作成していない場合、ステップＳ４１へ戻り上述同様の処理を繰り返す。一方、全てのペアを作成した場合、再収斂ポイント値算出部２４は、この処理を終了する。
【００５２】
再収斂ポイントＰｃの論理値が一致しない信号変化の組み合わせと、その組み合わせのペアとの全てが論理回路ＤＢ５４に出力した後、「受信側の再収斂ポイントＰｃにて論理的に値のばらつきを発生させる可能性のある複数の送信側の第２のクロックドメインでの信号間において、受信側のクロックＣＬＫ２の１クロックサイクル時間内の信号変化がない」ことをチェックするために、複数のソース信号に対して２つの信号をペアとした場合のプロパティ記述が検証プロパティ作成部２５によって行われる。
【００５３】
検証プロパティ作成部２５は、例えば、ＰＳＬ（Property Specification Language）等の検証プロパティ言語を用いてペア信号に対して、下記のような検証プロパティを作成する。
（１）送信側の第１クロックドメインにおいて、クロックＣＬＫ１における信号ｘの変化に対して、信号ｙの変化が同クロックサイクルで起こらないことをチェックするプロパティ式（１）を作成する。
【００５４】
never ((X != prev(X, 1)) && (Y != prev(Y, 1)))  ・・・・プロパティ式（１）
このプロパティ式（１）において、信号ｘに係る記述「(X != prev(X, 1))」は、現在の信号値と１サイクル前の信号値とが異なっているか否かを検証し、信号ｙに係る記述「(Y != prev(Y, 1))」も同様に、現在の信号値と１サイクル前の信号値とが異なっているか否かを検証する。そして、記述「&&」と記述「never」とによって、送信側の第１クロックドメインにおいてクロックＣＬＫ１の１サイクル内で信号ｘと信号ｙとが共に変化しないこと、つまり、少なくとも一方の信号で変化がないことを検証する。
（２）送信側の第１クロックドメインにおいて、送信側のクロックＣＬＫ１における信号ｘの変化に対して、信号ｙが先行するクロックサイクル、つまり、受信側のクロックＣＬＫ２の１クロックサイクル内で変化しないことをチェックするプロパティ式（２）を作成する。
【００５５】
never ((X != prev(X, 1)) && (prev(Y, n) != prev(Y, n+1)))・・・プロパティ式（２）
このプロパティ式（２）において、信号ｘに係る記述「(X != prev(X, 1))」は、現在の信号値と１サイクル前の信号値とが異なっているか否かを検証し、信号ｙに係る記述「(prev(Y, n) != prev(Y, n+1))」は、受信側のクロックＣＬＫ２の１クロックサイクル時間に相当する送信側のクロックＣＬＫ１のサイクル数Ｎまでのｎサイクルを用いて、送信側の第１クロックドメインにおいてｎサイクル前の信号値と更に１サイクル前の信号値とが異なっているか否かを検証する。そして、記述「&&」と記述「never」とによって、送信側の第１クロックドメインにおいて信号ｘの変化に対して信号ｙが受信側のクロックＣＬＫ２の１サイクル内で変化しないことを検証する。
【００５６】
プロパティ式（２）内のサイクル数ｎは、
１＜＝ｎ＜＝Ｎ
Ｎ＝((ＣＬＫ２の１サイクル周期)／(ＣＬＫ１の１サイクル周期))の切り上げ
・・・・・式（３）
によって決定される。
【００５７】
上述したプロパティ式（１）及び（２）は、信号変化に対するプロパティ記述であるが、これらを信号の立ち上がり及び立ち下がり毎に記述を展開する。信号の立ち上がり及び立ち下がりに対する一般的なプロパティ記述は下記のようになる。
【００５８】
立ち上がり：rose(X) = (X && !prev(X))
立ち下がり：fell(X) = (!X && prev(X))  ・・・・・プロパティ式（４）
上記プロパティ記述を挿入した論理回路に対して形式的検証を実施し正常に終了することによって、非同期に対する回路構造に問題がないことが保証される。
【００５９】
検証プロパティ作成部２５によって行なわれる検証プロパティ作成処理について図１２で説明する。図１２は、検証プロパティ作成処理を説明するためのフローチャート図である。図１２において、検証プロパティ作成部２５は、異なる値が算出されたソース信号のペアを異値信号ペアＤＢ５５から順に取得して（ステップＳ７１）、上記プロパティ式（１）をペアのソース信号に適用して変数ｘ及びｙに取得したペアのソース信号の識別情報を代入し、検証プロパティを作成する（ステップＳ７１）。
【００６０】
そして、検証プロパティ作成部２５は、上記式（３）を用いて、受信側のクロックＣＬＫ２の１クロックサイクル時間に相当する送信側のクロックＣＬＫ１のサイクル数Ｎを算出して（ステップＳ７３）、サイクル変数ｎに１を設定して初期化する（ステップＳ７４）。
【００６１】
検証プロパティ作成部２５は、サイクル変数ｎがサイクル数Ｎと一致するか否かを判断する（ステップＳ７５）。サイクル変数ｎがサイクル数Ｎと一致しない場合、つまりサイクル数Ｎ以下である場合、上記プロパティ式（２）をペアのソース信号に適用して変数ｘ及びｙにペアのソース信号の識別情報をそれぞれ代入し、検証プロパティを作成する（ステップＳ７６）。その後、検証プロパティ作成部２５は、サイクル変数ｎを１インクリメントし、ステップＳ７５へ戻り上述同様の処理を繰り返す。
【００６２】
一方、ステップＳ７５にて、サイクル変数ｎがサイクル数Ｎと一致する場合、検証プロパティ作成部２５は、異なる値が算出された信号変化の組み合わせに対応する信号の立ち上がり又は立ち下がりを示すプロパティ記述を、ステップＳ７２でプロパティ式（１）を適用して作成した検証プロパティ内と、ステップ７６でプロパティ式（２）を適用して作成した検証プロパティ内とに記述する（ステップＳ７８）。
【００６３】
異値信号ペアＤＢ５５に格納されている全てのペアについて作成したか否かを判断する（ステップＳ７９）。全てのペアについて作成していない場合、検証プロパティ作成部２５は、ステップＳ７１へ戻り上述同様の処理を繰り返す。一方、全てのペアについて作成した場合、検証プロパティ作成部２５は、作成した検証プロパティを検証プロパティＤＢ５６に格納するこの処理を終了する。
【００６４】
上述したプロパティ記述例及び検証プロパティ作成処理において、ＰＳＬを用いた場合で説明したが、ＰＳＬに限定されるものではない。
【００６５】
検証プロパティ作成処理にて作成された検証プロパティは、送信側の第１クロックドメインにおけるソース信号の回路に組み込まれ、形式的検証部２６によって形式的検証が実行される。形式的検証において、再収斂信号のソースとなる信号群の変化タイミングを保証することで再収斂信号の適切な伝播を保証し、これにより対象となる非同期構造の回路を包含していたとしてもＬＳＩ全体としては、回路構造的に問題がないと判断できる。
【００６６】
図１に示す回路構成３の再収斂信号Ｃに対して、再収斂ポイント値算出部２４による再収斂ポイントＰｃの算出結果例を図１３に示す。図１３は、再収斂ポイント値算出結果を示す図である。図１３に示す再収斂ポイント値算出結果７では、組合番号１、３、４、及び８において、変化タイミングずれによって再収斂ポイントＰｃでの論理値が異なることが示されている。
【００６７】
異なる値が算出された組合番号１について図１４で説明する。図１４は、変化タイミングずれによって再収斂ポイントの論理値が異なる例を説明する図である。図１４中、信号Ａ２が立ち上がり（０→１）で変化し、信号Ｂ２も立ち上がり（０→１）で変化するときのメタスタビリティによる再収斂信号Ｃのばらつきを示している。図１４（Ａ）では、信号Ｂ２に対して信号Ａ２が先行して変化した場合に再収斂信号Ｃが「１」の論理値１４ａを示となることを示している。一方、図１４（Ｂ）では、信号Ａ２と信号Ｂ２が同時に変化した場合の再収斂信号Ｃが「０」から変化しない論理値１４ｂであることを示している。
【００６８】
次に、検証プロパティ作成部２５によって作成されるプロパティ記述の例を説明する。プロパティ記述は、送信側の第１クロックドメインの回路に組み込まれるため、動作クロックはクロックＣＬＫ１である。
【００６９】
クロックの周期がそれぞれ、クロックＣＬＫ１が「６ｎｓ」、そしてクロックＣＬＫ２が「１１ｎｓ」の場合、クロックＣＬＫ２の１クロックサイクル時間に相当するクロックＣＬＫ１のサイクル数Ｎは、
サイクル数Ｎ  ＝  １１ｎｓ／６ｎｓ  ＝  １．８３  →  ２
となる。
【００７０】
上記プロパティ式（１）を用いて、
never ((B != prev(B, 1)) && (A != prev(A, 1)))
を作成し、上記プロパティ式（２）を用いて、
ｎ＝１の場合、
never ((B != prev(B, 1)) && (prev(A, 1) != prev(A, 2)))
ｎ＝２（＜＝サイクル数Ｎ）の場合、
never ((B != prev(B, 1)) && (prev(A, 2) != prev(A, 3)))
を作成する。この展開を組合番号１と同様に組合番号３、組合番号４、及び組合番号８に対しても実施する。
【００７１】
上述した、信号Ａ２（０−＞１：立ち上がり変化）及び信号Ｂ２（０−＞１：立ち上がり変化）の場合の記述を行う場合には、立ち上がり記述 rose(X) = X && !prev(X) より上記プロパティ記述を展開すれば、新しく得られるプロパティ記述は、上述した組合番号１であれば、次のようになる。
【００７２】
never ((B && !prev(B, 1)) && (A && !prev(A, 1)))
never ((B && !prev(B, 1)) && (prev(A, 1) && !prev(A, 2)))
never ((B && !prev(B, 1)) && (prev(A, 2) && !prev(A, 3)))
この展開を組合番号１と同様に組合番号３、組合番号４、及び組合番号８に対しても実施する。
【００７３】
上記のプロパティ記述を回路記述に埋め込み、形式的検証部２６によって形式的な検証処理が行われる。その結果、形式的検証においてプロパティ記述に違反がなければ、検証された変化タイミングにおいて、非同期構造に対してこの回路構造はメタスタビリティ起因の問題ないと判断することができる。
【００７４】
以上の説明に関し、更に以下の項を開示する。
（付記１）
回路検証装置における回路検証方法であって、該回路検証装置が、
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、
を実行することを特徴とする回路検証方法。
（付記２）
前記信号値算出手順は、前記信号変化の組み合わせ毎に、前記複数の信号を再収斂する論理演算を用いて、変化タイミングの違いによる前記再収斂ポイントの論理値を算出することを特徴とする付記１記載の回路検証方法。
（付記３）
前記信号値算出手順は、
前記再収斂信号毎に、前記複数の信号から２つの信号を特定してペアを作成するペア作成手順と、
２つの信号の前記信号変化の組み合わせと該組み合わせ毎に前記変化タイミングの違いとを示す信号変化表を参照することによって、前記ペアとなる２つの信号に対して前記再収斂ポイントの論理値を算出する再収斂ポイント値算出手順と、
を有することを特徴とする付記１又は２記載の回路検証方法。
（付記４）
前記検証プロパティ作成手順は、
送信側送信側クロックドメインにおいて、送信側クロックの１クロックサイクル内で前記複数の信号が変化しないことを検証する第一検証プロパティを作成する第一作成手順と、
受信側クロックの１クロックサイクル時間に相当する送信側クロックのサイクル数を算出するサイクル数算出手順と、
前記送信側クロックドメインにおいて、現在から前記サイクル数前までの時間で前記複数の信号が変化しないことを検証する第二検証プロパティを作成する第二作成手順と、
を有することを特徴とする付記１乃至３のいずれか一項記載の回路検証方法。
（付記５）
前記検証プロパティ作成手順は、前記第一検証プロパティ及び前記第二検証プロパティ内に前記信号変化を示す検証プロパティを記述する信号変化記述手順を更に有することを特徴とする付記４記載の回路検証方法。
（付記６）
前記回路検証装置が、
前記検証プロパティ作成手順によって作成された前記検証プロパティを、前記複数の信号が伝播される送信側クロックドメイン内の回路記述に埋め込んで形式的検証を行う形式的検証手順を更に実行することを特徴とする回路検証方法。
（付記７）
コンピュータを回路検証装置として機能させる回路検証プログラムであって、該コンピュータに、
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、
を実行させることを特徴とするコンピュータ実行可能な回路検証プログラム。
（付記８）
コンピュータを回路検証装置として機能させる回路検証プログラムを記憶した記憶媒体であって、該コンピュータに、
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手順と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手順と、
を実行させることを特徴とするコンピュータ読取可能な記憶媒体。
（付記９）
一の再収斂信号に収斂される複数の信号の前記信号変化の組み合わせ毎に、変化タイミングの違いによる再収斂ポイントの論理値を算出する信号値算出手段と、
前記変化タイミングの違いにより前記再収斂ポイントの論理値が異なる前記信号変化の組み合わせに対して、受信側クロックの１クロックサイクル内で信号変化の発生を検証するための検証プロパティを作成する検証プロパティ作成手段と、
を有することを特徴とする回路検証装置。
【００７５】
本発明は、具体的に開示された実施例に限定されるものではなく、特許請求の範囲から逸脱することなく、種々の変形や変更が可能である。
【符号の説明】
【００７６】
３            回路構成
３−Ａ、３−Ａ１、３−Ａ２  レジスタ
３−Ｂ、３−Ｂ１、３−Ｂ２  レジスタ
３−Ｃ        レジスタ
４            ＡＮＤ回路
１１          ＣＰＵ
１２          メモリユニット
１３          表示ユニット
１４          出力ユニット
１５          入力ユニット
１６          通信ユニット
１７          記憶装置
１８          ドライバ
１９          記憶媒体
２１          回路記述部
２２          再収斂信号解析部
２３          論理演算抽出部
２４          再収斂ポイント値算出部
２５          検証プロパティ作成部
２６          形式的検証部
５１          回路記述情報
５２          クロックドメインＤＢ
５３          再収斂信号ＤＢ
５４          論理回路ＤＢ
５５          異値信号ペアＤＢ
５６          検証プロパティＤＢ
１００        検証装置
【図１】
2011034475.tif 000003
【図２】
2011034475.tif 000004
【図３】
2011034475.tif 000005
【図４】
2011034475.tif 000006
【図５】
2011034475.tif 000007
【図６】
2011034475.tif 000008
【図７】
2011034475.tif 000009
【図８】
2011034475.tif 000010
【図９】
2011034475.tif 000011
【図１０】
2011034475.tif 000012
【図１１】
2011034475.tif 000013
【図１２】
2011034475.tif 000014
【図１３】
2011034475.tif 000015
【図１４】
2011034475.tif 000016