検証装置、検証方法及びプログラム
【課題】検証する範囲を少なくして、検証コストや検証時間の増大を抑制する。
【解決手段】抽出部１２が、第１のクロック信号で動作する回路部２１と、第２のクロック信号で動作する回路部２２とを含む検証対象回路（論理回路２０）から、ハンドシェイクの手順に従って回路部２１と回路部２２間でのデータの送受信を行うハンドシェイク部２３を抽出し、検証部１３が抽出されたハンドシェイク部２３の信号が、その手順を満たすかを検証し、手順を満たさない信号があるとき、回路部２１と回路部２２のうち当該信号を出力する側で、当該信号が手順を満たさなくなる条件が回路動作時に起こり得るか検証する。
【解決手段】抽出部１２が、第１のクロック信号で動作する回路部２１と、第２のクロック信号で動作する回路部２２とを含む検証対象回路（論理回路２０）から、ハンドシェイクの手順に従って回路部２１と回路部２２間でのデータの送受信を行うハンドシェイク部２３を抽出し、検証部１３が抽出されたハンドシェイク部２３の信号が、その手順を満たすかを検証し、手順を満たさない信号があるとき、回路部２１と回路部２２のうち当該信号を出力する側で、当該信号が手順を満たさなくなる条件が回路動作時に起こり得るか検証する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検証装置、検証方法及びプログラムに関する。
【背景技術】
【０００２】
異なるクロック信号で動作する回路部間で、複数ビットの信号のやり取りを行う際、ハンドシェイクと呼ばれる手順が行われる。
第１のクロック信号で動作する回路部（以下Ａクロックドメインと呼ぶ）のデータ（Ａ＿ＤＡＴＡ）を、第２のクロック信号で動作する回路部（以下Ｂクロックドメインと呼ぶ）に渡す場合、たとえば、以下のようなハンドシェイクの手順が行われる。
【０００３】
まず、Ａクロックドメイン側で、データを送信するためのリクエスト信号（Ａ＿ＲＥＱ）がアサートされる。次に、Ｂクロックドメインのフリップフロップ（以下ＦＦと略す）を２回介したＡ＿ＲＥＱであるＡ＿ＲＥＱ＿ｑ２がアサートされる。Ａ＿ＲＥＱ＿ｑ２がアサートされると、Ｂクロックドメイン側がＡ＿ＤＡＴＡをＢ＿ＤＡＴＡとして受信する。
【０００４】
その後、Ｂクロックドメイン側で、受信が行われたことを示す信号（Ｂ＿ＡＣＫ）がアサートされる。次に、ＡクロックドメインのＦＦを２回介したＢ＿ＡＣＫであるＢ＿ＡＣＫ＿ｑ２がアサートされる。続いて、Ａクロックドメイン側で、Ａ＿ＲＥＱがデアサートされる。そして、ＢクロックドメインのＦＦを２回介したＡ＿ＲＥＱであるＡ＿ＲＥＱ＿ｑ２がデアサートされる。
【０００５】
その後、Ｂクロックドメイン側で、Ｂ＿ＡＣＫがデアサートされ、ＡクロックドメインのＦＦを２回介したＢ＿ＡＣＫであるＢ＿ＡＣＫ＿ｑ２がデアサートされる。
このような手順の際に、たとえば、Ｂクロックドメインで、Ｂ＿ＡＣＫをアサートすべきときに、Ｂクロックドメインだけのリセットや、ある条件などによりＢ＿ＡＣＫがアサートされなくなった場合、ＡクロックドメインはＢ＿ＡＣＫ＿ｑ２がアサートされることを待ち続けることになり、デッドロックが発生する可能性がある。
【０００６】
一方、非同期検証を行う手法としては、従来、回路全体に対する動的検証が行われていた。たとえば、上記のようなハンドシェイクを行う部分では、各クロック線あるいは信号線に対して任意のジッター値がランダムに与えられ、動的検証が実施され、その結果から回路の妥当性が確認されていた。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開２００６−２５２４３８号公報
【特許文献２】特開２０１１−３４４７５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、従来の手法では、回路全体に対して検証を行うことになるため、ハンドシェイクを行う部分以外の機能検証も同時に行うことになる。そのため、検証を実施する条件の組み合わせが膨大なものになり、検証コストや、検証時間が増加する問題があった。
【課題を解決するための手段】
【０００９】
発明の一観点によれば、以下に示すような検証装置が提供される。
この検証装置は、第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を備える。
【発明の効果】
【００１０】
開示の検証装置、検証方法及びプログラムによれば、検証する範囲を少なくでき、検証コストや検証時間の増大を抑制することができる。
【図面の簡単な説明】
【００１１】
【図１】第１の実施の形態の検証装置の一例を示す図である。
【図２】ハンドシェイクの手順の一例を示す図である。
【図３】ハンドシェイク部のＲＴＬ（Register Transfer Level）の回路記述の一つ目の例である。
【図４】ハンドシェイク部のＲＴＬの回路記述の二つ目の例である。
【図５】第２の実施の形態の検証装置の一例を示す図である。
【図６】第２の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
【図７】検証プロパティＡの例を示す図である。
【図８】検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図９】検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図１０】検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図１１】本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。
【発明を実施するための形態】
【００１２】
以下、本発明の実施の形態を、図面を参照しつつ説明する。
（第１の実施の形態）
図１は、第１の実施の形態の検証装置の一例を示す図である。
【００１３】
検証装置１０は、記憶部１１、抽出部１２、検証部１３を有している。
記憶部１１は、検証対象データＤ１を記憶している。検証対象データＤ１は、検証対象回路（図１の例では論理回路２０）を、たとえば、Ｖｅｒｉｌｏｇや、ＶＨＤＬ（Very high speed integrated circuit Hardware Description Language）などのハードウェア記述言語などで記述したデータである。
【００１４】
論理回路２０は、互いに異なるクロックで動作する回路部２１，２２を有するものである。すなわち、回路部２１，２２は、異なるクロックで動作するクロックドメインとなる。
【００１５】
回路部２１，２２間でハンドシェイクの手順に従ってデータの送受信を行う部分が、ハンドシェイク部２３である。ハンドシェイク部２３には、複数のＦＦが含まれる。
抽出部１２は、論理回路２０から、ハンドシェイク部２３を抽出する。たとえば、抽出部１２は、検証対象データＤ１に含まれる論理回路２０の回路記述から、ハンドシェイク部２３の回路記述を抽出する。
【００１６】
検証部１３は、抽出されたハンドシェイク部２３に対して、シミュレーションを行い、ハンドシェイク部２３の信号が、ハンドシェイクの手順を満たすか検証する。ハンドシェイクの手順を満たさない信号があるとき、検証部１３は、回路部２１，２２のうち、その信号を出力する側で、その信号がハンドシェイクの手順を満たさなくなる条件が、回路動作時に起こり得るか検証する。
【００１７】
図２は、ハンドシェイクの手順の一例を示す図である。
図２では、回路部２１がＡ＿ＤＡＴＡ［＊：０］というデータを回路部２２に送信するときのハンドシェイクの手順の一例が示されている。ＦＦ３０，３１は、ハンドシェイク部２３の回路部２２側に含まれるＦＦであり、回路部２２で用いられるクロック信号がクロック端子に入力される。ＦＦ３２，３３は、ハンドシェイク部２３の回路部２１側に含まれるＦＦであり、回路部２１で用いられるクロック信号がクロック端子に入力される。
【００１８】
回路部２１がＡ＿ＤＡＴＡ［＊：０］というデータを回路部２２に送信するとき、回路部２２は、リクエスト信号（Ａ＿ＲＥＱ）をアサートする（図２の例では“１”とすることを示す）。
【００１９】
Ａ＿ＲＥＱは、回路部２２のＦＦ３０に入力される。回路部２２で用いられるクロック信号に同期して、Ａ＿ＲＥＱはＦＦ３０からＦＦ３１に伝達され、ＦＦ３１の出力信号であるＡ＿ＲＥＱ＿ｑ２がアサートされる。Ａ＿ＲＥＱ＿ｑ２がアサートされると、回路部２２側で、Ａ＿ＤＡＴＡがＢ＿ＤＡＴＡとして受信される。
【００２０】
その後、回路部２２側で、受信が行われたことを示す信号（Ｂ＿ＡＣＫ）がアサートされる。Ｂ＿ＡＣＫは、回路部２１のＦＦ３２に入力される。回路部２１で用いられるクロック信号に同期して、Ｂ＿ＡＣＫはＦＦ３２からＦＦ３３に伝達され、ＦＦ３３の出力信号であるＢ＿ＡＣＫ＿ｑ２がアサートされる。
【００２１】
Ｂ＿ＡＣＫ＿ｑ２がアサートされると、回路部２１は、Ａ＿ＲＥＱをデアサートする（図２の例では“０”とすることを示す）。
Ａ＿ＲＥＱの変化は、回路部２２のＦＦ３０，３１を介して伝わり、Ａ＿ＲＥＱ＿ｑ２がデアサートされる。
【００２２】
Ａ＿ＲＥＱ＿ｑ２がデアサートされると、回路部２２は、Ｂ＿ＡＣＫをデアサートする。
Ｂ＿ＡＣＫの変化は、回路部２１のＦＦ３２，３３を介して伝わり、Ｂ＿ＡＣＫ＿ｑ２がデアサートされる。
【００２３】
図３は、ハンドシェイク部のＲＴＬ（Register Transfer Level）の回路記述の一つ目の例である。回路記述は、Ｖｅｒｉｌｏｇで記述されており、前述したハンドシェイク部２３の回路部２２側で出力される信号であるＢ＿ＡＣＫが変化する条件が示されている。
【００２４】
図３の１行目では、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジ、または、論理回路２０のリセット信号（ＲＳＴ）の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。２，３行目では、ＲＳＴが０のとき、Ｂ＿ＡＣＫが０（Ｂ＿ＡＣＫ＜＝１’ｂ０）となることが示されている。なお、１’は１ビットを示し、ｂは２進数であることを示している。
【００２５】
４，５行目では、ＲＳＴが０でないとき、回路部２２のみのリセット信号（Ｂ＿ＲＳＴ）が０、回路部２２内のカウンタ値（Ｂ＿ＣＮＴ）が１５のとき、もしくはＡ＿ＲＥＱ＿ｑ２が０で、かつＢ＿ＣＮＴが０のとき、Ｂ＿ＡＣＫが０となることが示されている。なお、４’は４ビット、ｈは１６進数であることを示している。
【００２６】
６，７行目では、Ａ＿ＲＥＱ＿ｑ２が１のときに、Ｂ＿ＡＣＫが１となることが示されている。
図４は、ハンドシェイク部のＲＴＬの回路記述の二つ目の例である。回路記述は、Ｖｅｒｉｌｏｇで記述されており、前述したハンドシェイク部２３の回路部２１側で出力される信号であるＡ＿ＲＥＱが変化する条件が示されている。
【００２７】
図４の１行目では、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジ、または、論理回路２０のリセット信号（ＲＳＴ）の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。２，３行目では、ＲＳＴが０のとき、Ａ＿ＲＥＱが０となることが示されている。４，５行目では、ＲＳＴが０でないとき、回路部２１内のカウンタ値（Ａ＿ＣＮＴ）が２、かつＢ＿ＡＣＫ＿ｑ２が１のとき、Ａ＿ＲＥＱが０となることが示されている。６，７行目では、Ａ＿ＣＮＴが０のときに、Ａ＿ＲＥＱが１となることが示されている。
【００２８】
検証部１３は、抽出された、図３、図４のようなハンドシェイク部２３の回路記述において、Ａ＿ＲＥＱやＢ＿ＡＣＫなどの信号が、図２に示したようなハンドシェイクの手順を満たすか検証する。
【００２９】
たとえば、検証部１３は、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらず、回路部２２だけのリセットや、ある条件などによりＢ＿ＡＣＫがアサートされなくなった場合、Ｂ＿ＡＣＫがハンドシェイクの手順を満たさないと判定する。
【００３０】
このとき、検証部１３は、Ｂ＿ＡＣＫを出力する側の回路部２２で、Ｂ＿ＡＣＫがアサートされない条件が、回路動作時に起こり得るか検証する。
このように、本実施の形態の検証装置１０によれば、ハンドシェイク部２３の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制することができる。
【００３１】
（第２の実施の形態）
図５は、第２の実施の形態の検証装置の一例を示す図である。
第１の実施の形態の検証装置１０と同様の要素については同一符号を付し、説明を省略する。
【００３２】
第２の実施の形態の検証装置１０ａは、検証用情報生成部１４を有している。検証用情報生成部１４は、抽出部１２で抽出されたハンドシェイク部２３の信号をもとに、検証部１３で検証を行うための検証用情報（以下検証プロパティと呼ぶ）を生成する。
【００３３】
検証用情報生成部１４は、検証部１３が行う２段階の検証、すなわち、前述したハンドシェイク部２３の検証と、ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証の、それぞれの検証用の検証プロパティを生成する。検証プロパティは、たとえば、Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ、ｅ言語、ＰＳＬ（Property Specification Language）などの検証記述言語で記述される。
【００３４】
ハンドシェイク部２３の検証用に生成される検証プロパティには、データ送受信時に、ハンドシェイク部２３の信号が満たすべき条件（つまりハンドシェイクの手順を満たすような条件）が記述される。
【００３５】
ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証時に生成される検証プロパティには、手順を満たさないと判定された信号が、その回路部において、データ送受信時に手順を満たす場合の条件が記述される。
【００３６】
そして、検証部１３は、この２種類の検証プロパティを用いて検証を行う。２番目の検証では、検証部１３は、検証プロパティＢに記述された条件が偽になる場合が、回路動作時において存在するか否かによって、回路部２１，２２間のデータ送受信時にデッドロックが発生するか否か検証する。
【００３７】
図６は、第２の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
なお、以下では、図１に示したような論理回路２０に対して検証を行う場合を例にして説明する。
【００３８】
まず、抽出部１２は、論理回路２０から、ハンドシェイク部２３を抽出する（ステップＳ１０）。たとえば、抽出部１２は、論理回路２０の回路記述から、図３や図４に示したようなハンドシェイク部２３の回路記述を抽出する。
【００３９】
さらに、抽出部１２は、ハンドシェイク部２３の信号（Ａ＿ＲＥＱ，Ａ＿ＲＥＱ＿ｑ２，Ｂ＿ＡＣＫ，ＢＡＣＫ＿ｑ２）を抽出する（ステップＳ１１）。
ステップＳ１０，Ｓ１１の処理において、抽出部１２は、０−Ｉｎ ＣＤＣ（Clock Domain Crossing）などの検証ツールを適用してもよい。
【００４０】
その後、検証用情報生成部１４は、抽出されたハンドシェイク部２３とその信号をもとに、ハンドシェイク部２３の検証を行うための検証プロパティ（以下検証プロパティＡと呼ぶ）を生成する（ステップＳ１２）。
【００４１】
図７は、検証プロパティＡの例を示す図である。
図７では、検証プロパティＡとして、アサーション（設計対象の論理回路で期待されている動作などを記述した文）をＳｙｓｔｅｍ Ｖｅｒｉｌｏｇで記述した、３つの検証プロパティの例が示されている。
【００４２】
各検証プロパティの１行目の１＿ｂ＿ａｃｋ＿ａｓｔ、２＿ａ＿ｒｅｑ＿ｄａｓｔ、３＿ｂ＿ａｃｋ＿ｄａｓｔが、それぞれの検証プロパティ名である。
検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ａ＿ＲＥＱ＿ｑ２がアサートされるとＢ＿ＡＣＫがアサートされるかどうかを検証するためのものである。
【００４３】
２行目には、この検証プロパティの内容が記述されている。回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＢ＿ＡＣＫが１（アサート）になることが示されている。
【００４４】
３行目では、検証プロパティの終わりが示されており、４行目では、１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ｂ＿ＡＣＫ＿ｑ２がアサートされるとＡ＿ＲＥＱがデアサートされるかどうかを検証するためのものである。
【００４５】
２行目には、この検証プロパティの内容として、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ｂ＿ＡＣＫ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＡ＿ＲＥＱが０（デアサート）になることが示されている。
【００４６】
３行目では、検証プロパティの終わりが示されており、４行目では、２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ａ＿ＲＥＱ＿ｑ２がデアサートされるとＢ＿ＡＣＫがデアサートされるかどうかを検証するためのものである。
【００４７】
２行目には、この検証プロパティの内容として、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＢ＿ＡＣＫが０（デアサート）になることが示されている。
【００４８】
３行目では、検証プロパティの終わりが示されており、４行目では、３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証部１３は、上記のような検証プロパティＡを用いてハンドシェイク部２３の形式的検証を行い（ステップＳ１３）、エラーが発生するか否かを判定する（ステップＳ１４）。
【００４９】
図７に示した、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを適用した形式検証では、Ａ＿ＲＥＱ＿ｑ２がアサートされるとＢ＿ＡＣＫがアサートされるかどうかが検証される。たとえば、図３に示したように記述されているハンドシェイク部２３の場合、回路部２２のリセット信号（Ｂ＿ＲＳＴ）が０になっていたりすると、Ａ＿ＲＥＱ＿ｑ２がアサートの状態にもかかわらず、Ｂ＿ＡＣＫは０となり、アサートされない。このような場合、検証部１３はエラーが発生したと判定する。
【００５０】
検証部１３は、同様に、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔ，３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡについても検証を行い、エラーが発生するか否かを判定する。
【００５１】
検証の結果、エラーが生じたと判定された場合、検証用情報生成部１４は、ハンドシェイクの手順を満たさない信号を出力する側の回路部を検証するための検証プロパティ（以下検証プロパティＢと呼ぶ）を生成する（ステップＳ１５）。
【００５２】
検証用情報生成部１４は、たとえば、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＢ＿ＡＣＫ部分の論理をトレースし、Ｂ＿ＡＣＫが１にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路部２２の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００５３】
図８は、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
図８では、検証プロパティＢとして、アサーションをＳｙｓｔｅｍ Ｖｅｒｉｌｏｇで記述した、２つの検証プロパティの例が示されている。
【００５４】
各検証プロパティの１行目の４＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ，５＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ２が、それぞれの検証プロパティ名である。
検証プロパティ名が４＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅの検証プロパティＢでは、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続したとき、Ｂ＿ＲＳＴが１になっていることが示されている。
【００５５】
検証プロパティ名が５＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ２の検証プロパティＢでも、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続したときには、回路部２２のカウンタ値（Ｂ＿ＣＮＴ）は１５ではないことが示されている。
【００５６】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部１４は、たとえば、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＡ＿ＲＥＱ部分の論理をトレースし、Ａ＿ＲＥＱが０にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００５７】
図９は、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
１行目の６＿ａ＿ｒｅｑ＿ａｓｔ＿ｐｒａｃｔｉｃｅが、検証プロパティ名である。
【００５８】
２行目には、この検証プロパティＢの内容が記述されており、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティＢが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ｂ＿ＡＣＫ＿ｑ２が１（アサート）の状態が１サイクル以上連続するとき、次のサイクルでＡ＿ＣＮＴが２になることが示されている。
【００５９】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部１４は、たとえば、検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＢ＿ＡＣＫ部分の論理をトレースし、Ｂ＿ＡＣＫが１にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００６０】
図１０は、検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
１行目の７＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅが、検証プロパティ名である。
【００６１】
２行目には、この検証プロパティＢの内容が記述されており、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティＢが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続するとき、次のサイクルでＢ＿ＣＮＴが０になることが示されている。
【００６２】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証部１３は、上記のような検証プロパティＢを用いて、ハンドシェイクの手順を満たさない信号を出力する側の回路部の動作レベル（実使用レベル）の検証（形式検証または動的検証）を行い（ステップ１６）、その結果を出力する（ステップＳ１７）。なお、ステップＳ１４の処理で、エラーが発生しないと判定された場合には、ハンドシェイク部２３でデッドロックは発生しない旨の検証結果が出力される。
【００６３】
ステップＳ１６では、たとえば、以下のような検証が行われる。
たとえば、図８に示した検証プロパティＢが生成された場合、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらずＢ＿ＡＣＫがアサートされない条件があるということを示している。このとき検証部１３は、Ｂ＿ＡＣＫを出力する回路部２２において、検証プロパティＢを用いて、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらずＢ＿ＡＣＫがアサートされない条件が回路動作時に起こり得るか検証する。
【００６４】
検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続したとき、Ｂ＿ＲＳＴが１でなく、回路部２２がリセット状態のままである場合が回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６５】
また、検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続したとき、回路部２２のカウンタ値（Ｂ＿ＣＮＴ）が１５のままである場合が回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６６】
一方、図９に示した検証プロパティＢが生成された場合、Ｂ＿ＡＣＫ＿ｑ２がアサートされたにもかかわらずＡ＿ＲＥＱがデアサートされない条件があるということを示している。このとき検証部１３は、Ａ＿ＲＥＱに変化を与える側の回路部２１において、検証プロパティＢを用いて、Ｂ＿ＡＣＫ＿ｑ２がアサートされたにもかかわらずＡ＿ＲＥＱがデアサートされない条件が回路動作時に起こり得るか検証する。
【００６７】
検証部１３は、Ｂ＿ＡＣＫ＿ｑ２が１の状態が１サイクル以上連続しても、Ａ＿ＣＮＴが２にならない場合が、回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６８】
また、図１０に示した検証プロパティＢが生成された場合、Ａ＿ＲＥＱ＿ｑ２がデアサートされたにもかかわらずＢ＿ＡＣＫがデアサートされない条件があるということを示している。このとき検証部１３は、Ｂ＿ＡＣＫを出力する側の回路部２２において、検証プロパティＢを用いて、Ａ＿ＲＥＱ＿ｑ２がデアサートされたにもかかわらずＢ＿ＡＣＫがデアサートされない条件が回路動作時に起こり得るか検証する。
【００６９】
検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続しても、Ｂ＿ＣＮＴが０にならない場合が、回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００７０】
以上のように第２の実施の形態の検証装置１０ａ及び検証方法によれば、検証プロパティＡを生成して、検証することで、論理回路の非同期部分であるハンドシェイク部２３の検証漏れを抑制できる。
【００７１】
また、検証プロパティＡを用いてハンドシェイク部２３の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証プロパティＢを用いて検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制できる。
【００７２】
また、ハンドシェイク部２３のデッドロックを見逃さなくなるので、各クロックドメイン別に検証を進めることも可能となる。
なお、上記のような第１及び第２の実施の形態の検証装置１０，１０ａは、以下のようなコンピュータにより実現可能である。
【００７３】
図１１は、本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。
コンピュータ１００は、ＣＰＵ（Central Processing Unit）１０１によって装置全体が制御されている。ＣＰＵ１０１には、バス１０８を介してＲＡＭ（Random Access Memory）１０２と複数の周辺機器が接続されており、検証装置１０，１０ａの各部の機能を実現する。
【００７４】
ＲＡＭ１０２は、コンピュータ１００の主記憶装置として使用される。ＲＡＭ１０２には、ＣＰＵ１０１に実行させるＯＳ（Operating System）のプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、ＲＡＭ１０２には、ＣＰＵ１０１による処理に用いる各種データが格納される。
【００７５】
バス１０８に接続されている周辺機器としては、ハードディスクドライブ（ＨＤＤ:Hard Disk Drive）１０３、グラフィック処理装置１０４、入力インタフェース１０５、光学ドライブ装置１０６、及び通信インタフェース１０７がある。
【００７６】
ＨＤＤ１０３は、内蔵したディスクに対して、磁気的にデータの書き込み及び読み出しを行う。ＨＤＤ１０３は、コンピュータ１００の二次記憶装置として使用される。ＨＤＤ１０３には、ＯＳのプログラム、各種検証ツールなどのアプリケーションプログラム、及び図１に示した検証対象データＤ１などの各種データが格納される。なお、二次記憶装置としては、フラッシュメモリなどの半導体記憶装置を使用することもできる。
【００７７】
グラフィック処理装置１０４には、モニタ１０４ａが接続されている。グラフィック処理装置１０４は、ＣＰＵ１０１からの命令に従って、検証結果などの画像をモニタ１０４ａの画面に表示させる。モニタ１０４ａとしては、ＣＲＴ（Cathode Ray Tube）を用いた表示装置や液晶表示装置などがある。
【００７８】
入力インタフェース１０５には、キーボード１０５ａとマウス１０５ｂとが接続されている。入力インタフェース１０５は、キーボード１０５ａやマウス１０５ｂから送られてくる信号をＣＰＵ１０１に送信する。なお、マウス１０５ｂは、ポインティングデバイスの一例であり、他のポインティングデバイスを使用することもできる。他のポインティングデバイスとしては、タッチパネル、タブレット、タッチパッド、トラックボールなどがある。
【００７９】
光学ドライブ装置１０６は、レーザ光などを利用して、光ディスク１０６ａに記録されたデータの読み取りを行う。光ディスク１０６ａは、光の反射によって読み取り可能なようにデータが記録された可搬型の記録媒体である。光ディスク１０６ａには、ＤＶＤ（Digital Versatile Disc）、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ（Compact Disc Read Only Memory）、ＣＤ−Ｒ（Recordable）／ＲＷ（ReWritable）などがある。
【００８０】
通信インタフェース１０７は、ネットワーク１０７ａに接続されている。通信インタフェース１０７は、ネットワーク１０７ａを介して、他のコンピュータまたは通信機器との間でデータの送受信を行う。
【００８１】
以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。
また、検証装置１０，１０ａが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータ（たとえば、図１１のようなコンピュータ１００）で実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記憶装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記憶装置には、ＨＤＤ、フレキシブルディスク（ＦＤ）、磁気テープなどがある。光ディスクには、ＤＶＤ、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ／ＲＷなどがある。光磁気記録媒体には、ＭＯ（Magneto-Optical disk）などがある。
【００８２】
プログラムを流通させる場合には、たとえば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００８３】
プログラムを実行するコンピュータは、たとえば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、ネットワークを介して接続されたサーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムにしたがった処理を実行することもできる。
【００８４】
また、上記の処理機能の少なくとも一部を、ＤＳＰ（Digital Signal Processor）、ＡＳＩＣ（Application Specific Integrated Circuit）、ＰＬＤ（Programmable Logic Device）などの電子回路で実現することもできる。
【００８５】
以上、実施の形態に基づき、本発明の検証装置、検証方法及びプログラムの一観点について説明してきたが、これらは一例にすぎず、上記の記載に限定されるものではない。
【符号の説明】
【００８６】
１０ 検証装置
１１ 記憶部
１２ 抽出部
１３ 検証部
２０ 論理回路
２１，２２ 回路部
２３ ハンドシェイク部
Ｄ１ 検証対象データ
【技術分野】
【０００１】
本発明は、検証装置、検証方法及びプログラムに関する。
【背景技術】
【０００２】
異なるクロック信号で動作する回路部間で、複数ビットの信号のやり取りを行う際、ハンドシェイクと呼ばれる手順が行われる。
第１のクロック信号で動作する回路部（以下Ａクロックドメインと呼ぶ）のデータ（Ａ＿ＤＡＴＡ）を、第２のクロック信号で動作する回路部（以下Ｂクロックドメインと呼ぶ）に渡す場合、たとえば、以下のようなハンドシェイクの手順が行われる。
【０００３】
まず、Ａクロックドメイン側で、データを送信するためのリクエスト信号（Ａ＿ＲＥＱ）がアサートされる。次に、Ｂクロックドメインのフリップフロップ（以下ＦＦと略す）を２回介したＡ＿ＲＥＱであるＡ＿ＲＥＱ＿ｑ２がアサートされる。Ａ＿ＲＥＱ＿ｑ２がアサートされると、Ｂクロックドメイン側がＡ＿ＤＡＴＡをＢ＿ＤＡＴＡとして受信する。
【０００４】
その後、Ｂクロックドメイン側で、受信が行われたことを示す信号（Ｂ＿ＡＣＫ）がアサートされる。次に、ＡクロックドメインのＦＦを２回介したＢ＿ＡＣＫであるＢ＿ＡＣＫ＿ｑ２がアサートされる。続いて、Ａクロックドメイン側で、Ａ＿ＲＥＱがデアサートされる。そして、ＢクロックドメインのＦＦを２回介したＡ＿ＲＥＱであるＡ＿ＲＥＱ＿ｑ２がデアサートされる。
【０００５】
その後、Ｂクロックドメイン側で、Ｂ＿ＡＣＫがデアサートされ、ＡクロックドメインのＦＦを２回介したＢ＿ＡＣＫであるＢ＿ＡＣＫ＿ｑ２がデアサートされる。
このような手順の際に、たとえば、Ｂクロックドメインで、Ｂ＿ＡＣＫをアサートすべきときに、Ｂクロックドメインだけのリセットや、ある条件などによりＢ＿ＡＣＫがアサートされなくなった場合、ＡクロックドメインはＢ＿ＡＣＫ＿ｑ２がアサートされることを待ち続けることになり、デッドロックが発生する可能性がある。
【０００６】
一方、非同期検証を行う手法としては、従来、回路全体に対する動的検証が行われていた。たとえば、上記のようなハンドシェイクを行う部分では、各クロック線あるいは信号線に対して任意のジッター値がランダムに与えられ、動的検証が実施され、その結果から回路の妥当性が確認されていた。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開２００６−２５２４３８号公報
【特許文献２】特開２０１１−３４４７５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、従来の手法では、回路全体に対して検証を行うことになるため、ハンドシェイクを行う部分以外の機能検証も同時に行うことになる。そのため、検証を実施する条件の組み合わせが膨大なものになり、検証コストや、検証時間が増加する問題があった。
【課題を解決するための手段】
【０００９】
発明の一観点によれば、以下に示すような検証装置が提供される。
この検証装置は、第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を備える。
【発明の効果】
【００１０】
開示の検証装置、検証方法及びプログラムによれば、検証する範囲を少なくでき、検証コストや検証時間の増大を抑制することができる。
【図面の簡単な説明】
【００１１】
【図１】第１の実施の形態の検証装置の一例を示す図である。
【図２】ハンドシェイクの手順の一例を示す図である。
【図３】ハンドシェイク部のＲＴＬ（Register Transfer Level）の回路記述の一つ目の例である。
【図４】ハンドシェイク部のＲＴＬの回路記述の二つ目の例である。
【図５】第２の実施の形態の検証装置の一例を示す図である。
【図６】第２の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
【図７】検証プロパティＡの例を示す図である。
【図８】検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図９】検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図１０】検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
【図１１】本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。
【発明を実施するための形態】
【００１２】
以下、本発明の実施の形態を、図面を参照しつつ説明する。
（第１の実施の形態）
図１は、第１の実施の形態の検証装置の一例を示す図である。
【００１３】
検証装置１０は、記憶部１１、抽出部１２、検証部１３を有している。
記憶部１１は、検証対象データＤ１を記憶している。検証対象データＤ１は、検証対象回路（図１の例では論理回路２０）を、たとえば、Ｖｅｒｉｌｏｇや、ＶＨＤＬ（Very high speed integrated circuit Hardware Description Language）などのハードウェア記述言語などで記述したデータである。
【００１４】
論理回路２０は、互いに異なるクロックで動作する回路部２１，２２を有するものである。すなわち、回路部２１，２２は、異なるクロックで動作するクロックドメインとなる。
【００１５】
回路部２１，２２間でハンドシェイクの手順に従ってデータの送受信を行う部分が、ハンドシェイク部２３である。ハンドシェイク部２３には、複数のＦＦが含まれる。
抽出部１２は、論理回路２０から、ハンドシェイク部２３を抽出する。たとえば、抽出部１２は、検証対象データＤ１に含まれる論理回路２０の回路記述から、ハンドシェイク部２３の回路記述を抽出する。
【００１６】
検証部１３は、抽出されたハンドシェイク部２３に対して、シミュレーションを行い、ハンドシェイク部２３の信号が、ハンドシェイクの手順を満たすか検証する。ハンドシェイクの手順を満たさない信号があるとき、検証部１３は、回路部２１，２２のうち、その信号を出力する側で、その信号がハンドシェイクの手順を満たさなくなる条件が、回路動作時に起こり得るか検証する。
【００１７】
図２は、ハンドシェイクの手順の一例を示す図である。
図２では、回路部２１がＡ＿ＤＡＴＡ［＊：０］というデータを回路部２２に送信するときのハンドシェイクの手順の一例が示されている。ＦＦ３０，３１は、ハンドシェイク部２３の回路部２２側に含まれるＦＦであり、回路部２２で用いられるクロック信号がクロック端子に入力される。ＦＦ３２，３３は、ハンドシェイク部２３の回路部２１側に含まれるＦＦであり、回路部２１で用いられるクロック信号がクロック端子に入力される。
【００１８】
回路部２１がＡ＿ＤＡＴＡ［＊：０］というデータを回路部２２に送信するとき、回路部２２は、リクエスト信号（Ａ＿ＲＥＱ）をアサートする（図２の例では“１”とすることを示す）。
【００１９】
Ａ＿ＲＥＱは、回路部２２のＦＦ３０に入力される。回路部２２で用いられるクロック信号に同期して、Ａ＿ＲＥＱはＦＦ３０からＦＦ３１に伝達され、ＦＦ３１の出力信号であるＡ＿ＲＥＱ＿ｑ２がアサートされる。Ａ＿ＲＥＱ＿ｑ２がアサートされると、回路部２２側で、Ａ＿ＤＡＴＡがＢ＿ＤＡＴＡとして受信される。
【００２０】
その後、回路部２２側で、受信が行われたことを示す信号（Ｂ＿ＡＣＫ）がアサートされる。Ｂ＿ＡＣＫは、回路部２１のＦＦ３２に入力される。回路部２１で用いられるクロック信号に同期して、Ｂ＿ＡＣＫはＦＦ３２からＦＦ３３に伝達され、ＦＦ３３の出力信号であるＢ＿ＡＣＫ＿ｑ２がアサートされる。
【００２１】
Ｂ＿ＡＣＫ＿ｑ２がアサートされると、回路部２１は、Ａ＿ＲＥＱをデアサートする（図２の例では“０”とすることを示す）。
Ａ＿ＲＥＱの変化は、回路部２２のＦＦ３０，３１を介して伝わり、Ａ＿ＲＥＱ＿ｑ２がデアサートされる。
【００２２】
Ａ＿ＲＥＱ＿ｑ２がデアサートされると、回路部２２は、Ｂ＿ＡＣＫをデアサートする。
Ｂ＿ＡＣＫの変化は、回路部２１のＦＦ３２，３３を介して伝わり、Ｂ＿ＡＣＫ＿ｑ２がデアサートされる。
【００２３】
図３は、ハンドシェイク部のＲＴＬ（Register Transfer Level）の回路記述の一つ目の例である。回路記述は、Ｖｅｒｉｌｏｇで記述されており、前述したハンドシェイク部２３の回路部２２側で出力される信号であるＢ＿ＡＣＫが変化する条件が示されている。
【００２４】
図３の１行目では、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジ、または、論理回路２０のリセット信号（ＲＳＴ）の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。２，３行目では、ＲＳＴが０のとき、Ｂ＿ＡＣＫが０（Ｂ＿ＡＣＫ＜＝１’ｂ０）となることが示されている。なお、１’は１ビットを示し、ｂは２進数であることを示している。
【００２５】
４，５行目では、ＲＳＴが０でないとき、回路部２２のみのリセット信号（Ｂ＿ＲＳＴ）が０、回路部２２内のカウンタ値（Ｂ＿ＣＮＴ）が１５のとき、もしくはＡ＿ＲＥＱ＿ｑ２が０で、かつＢ＿ＣＮＴが０のとき、Ｂ＿ＡＣＫが０となることが示されている。なお、４’は４ビット、ｈは１６進数であることを示している。
【００２６】
６，７行目では、Ａ＿ＲＥＱ＿ｑ２が１のときに、Ｂ＿ＡＣＫが１となることが示されている。
図４は、ハンドシェイク部のＲＴＬの回路記述の二つ目の例である。回路記述は、Ｖｅｒｉｌｏｇで記述されており、前述したハンドシェイク部２３の回路部２１側で出力される信号であるＡ＿ＲＥＱが変化する条件が示されている。
【００２７】
図４の１行目では、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジ、または、論理回路２０のリセット信号（ＲＳＴ）の立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。２，３行目では、ＲＳＴが０のとき、Ａ＿ＲＥＱが０となることが示されている。４，５行目では、ＲＳＴが０でないとき、回路部２１内のカウンタ値（Ａ＿ＣＮＴ）が２、かつＢ＿ＡＣＫ＿ｑ２が１のとき、Ａ＿ＲＥＱが０となることが示されている。６，７行目では、Ａ＿ＣＮＴが０のときに、Ａ＿ＲＥＱが１となることが示されている。
【００２８】
検証部１３は、抽出された、図３、図４のようなハンドシェイク部２３の回路記述において、Ａ＿ＲＥＱやＢ＿ＡＣＫなどの信号が、図２に示したようなハンドシェイクの手順を満たすか検証する。
【００２９】
たとえば、検証部１３は、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらず、回路部２２だけのリセットや、ある条件などによりＢ＿ＡＣＫがアサートされなくなった場合、Ｂ＿ＡＣＫがハンドシェイクの手順を満たさないと判定する。
【００３０】
このとき、検証部１３は、Ｂ＿ＡＣＫを出力する側の回路部２２で、Ｂ＿ＡＣＫがアサートされない条件が、回路動作時に起こり得るか検証する。
このように、本実施の形態の検証装置１０によれば、ハンドシェイク部２３の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制することができる。
【００３１】
（第２の実施の形態）
図５は、第２の実施の形態の検証装置の一例を示す図である。
第１の実施の形態の検証装置１０と同様の要素については同一符号を付し、説明を省略する。
【００３２】
第２の実施の形態の検証装置１０ａは、検証用情報生成部１４を有している。検証用情報生成部１４は、抽出部１２で抽出されたハンドシェイク部２３の信号をもとに、検証部１３で検証を行うための検証用情報（以下検証プロパティと呼ぶ）を生成する。
【００３３】
検証用情報生成部１４は、検証部１３が行う２段階の検証、すなわち、前述したハンドシェイク部２３の検証と、ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証の、それぞれの検証用の検証プロパティを生成する。検証プロパティは、たとえば、Ｓｙｓｔｅｍ Ｖｅｒｉｌｏｇ、ｅ言語、ＰＳＬ（Property Specification Language）などの検証記述言語で記述される。
【００３４】
ハンドシェイク部２３の検証用に生成される検証プロパティには、データ送受信時に、ハンドシェイク部２３の信号が満たすべき条件（つまりハンドシェイクの手順を満たすような条件）が記述される。
【００３５】
ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証時に生成される検証プロパティには、手順を満たさないと判定された信号が、その回路部において、データ送受信時に手順を満たす場合の条件が記述される。
【００３６】
そして、検証部１３は、この２種類の検証プロパティを用いて検証を行う。２番目の検証では、検証部１３は、検証プロパティＢに記述された条件が偽になる場合が、回路動作時において存在するか否かによって、回路部２１，２２間のデータ送受信時にデッドロックが発生するか否か検証する。
【００３７】
図６は、第２の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。
なお、以下では、図１に示したような論理回路２０に対して検証を行う場合を例にして説明する。
【００３８】
まず、抽出部１２は、論理回路２０から、ハンドシェイク部２３を抽出する（ステップＳ１０）。たとえば、抽出部１２は、論理回路２０の回路記述から、図３や図４に示したようなハンドシェイク部２３の回路記述を抽出する。
【００３９】
さらに、抽出部１２は、ハンドシェイク部２３の信号（Ａ＿ＲＥＱ，Ａ＿ＲＥＱ＿ｑ２，Ｂ＿ＡＣＫ，ＢＡＣＫ＿ｑ２）を抽出する（ステップＳ１１）。
ステップＳ１０，Ｓ１１の処理において、抽出部１２は、０−Ｉｎ ＣＤＣ（Clock Domain Crossing）などの検証ツールを適用してもよい。
【００４０】
その後、検証用情報生成部１４は、抽出されたハンドシェイク部２３とその信号をもとに、ハンドシェイク部２３の検証を行うための検証プロパティ（以下検証プロパティＡと呼ぶ）を生成する（ステップＳ１２）。
【００４１】
図７は、検証プロパティＡの例を示す図である。
図７では、検証プロパティＡとして、アサーション（設計対象の論理回路で期待されている動作などを記述した文）をＳｙｓｔｅｍ Ｖｅｒｉｌｏｇで記述した、３つの検証プロパティの例が示されている。
【００４２】
各検証プロパティの１行目の１＿ｂ＿ａｃｋ＿ａｓｔ、２＿ａ＿ｒｅｑ＿ｄａｓｔ、３＿ｂ＿ａｃｋ＿ｄａｓｔが、それぞれの検証プロパティ名である。
検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ａ＿ＲＥＱ＿ｑ２がアサートされるとＢ＿ＡＣＫがアサートされるかどうかを検証するためのものである。
【００４３】
２行目には、この検証プロパティの内容が記述されている。回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＢ＿ＡＣＫが１（アサート）になることが示されている。
【００４４】
３行目では、検証プロパティの終わりが示されており、４行目では、１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ｂ＿ＡＣＫ＿ｑ２がアサートされるとＡ＿ＲＥＱがデアサートされるかどうかを検証するためのものである。
【００４５】
２行目には、この検証プロパティの内容として、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ｂ＿ＡＣＫ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＡ＿ＲＥＱが０（デアサート）になることが示されている。
【００４６】
３行目では、検証プロパティの終わりが示されており、４行目では、２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティは、前述したハンドシェイクの手順のように、Ａ＿ＲＥＱ＿ｑ２がデアサートされるとＢ＿ＡＣＫがデアサートされるかどうかを検証するためのものである。
【００４７】
２行目には、この検証プロパティの内容として、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続して成り立つ場合、次のサイクルでＢ＿ＡＣＫが０（デアサート）になることが示されている。
【００４８】
３行目では、検証プロパティの終わりが示されており、４行目では、３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティが偽と判断された場合、エラーとすることが示されている。
検証部１３は、上記のような検証プロパティＡを用いてハンドシェイク部２３の形式的検証を行い（ステップＳ１３）、エラーが発生するか否かを判定する（ステップＳ１４）。
【００４９】
図７に示した、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを適用した形式検証では、Ａ＿ＲＥＱ＿ｑ２がアサートされるとＢ＿ＡＣＫがアサートされるかどうかが検証される。たとえば、図３に示したように記述されているハンドシェイク部２３の場合、回路部２２のリセット信号（Ｂ＿ＲＳＴ）が０になっていたりすると、Ａ＿ＲＥＱ＿ｑ２がアサートの状態にもかかわらず、Ｂ＿ＡＣＫは０となり、アサートされない。このような場合、検証部１３はエラーが発生したと判定する。
【００５０】
検証部１３は、同様に、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔ，３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡについても検証を行い、エラーが発生するか否かを判定する。
【００５１】
検証の結果、エラーが生じたと判定された場合、検証用情報生成部１４は、ハンドシェイクの手順を満たさない信号を出力する側の回路部を検証するための検証プロパティ（以下検証プロパティＢと呼ぶ）を生成する（ステップＳ１５）。
【００５２】
検証用情報生成部１４は、たとえば、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＢ＿ＡＣＫ部分の論理をトレースし、Ｂ＿ＡＣＫが１にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路部２２の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００５３】
図８は、検証プロパティ名が１＿ｂ＿ａｃｋ＿ａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
図８では、検証プロパティＢとして、アサーションをＳｙｓｔｅｍ Ｖｅｒｉｌｏｇで記述した、２つの検証プロパティの例が示されている。
【００５４】
各検証プロパティの１行目の４＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ，５＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ２が、それぞれの検証プロパティ名である。
検証プロパティ名が４＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅの検証プロパティＢでは、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続したとき、Ｂ＿ＲＳＴが１になっていることが示されている。
【００５５】
検証プロパティ名が５＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅ２の検証プロパティＢでも、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続したときには、回路部２２のカウンタ値（Ｂ＿ＣＮＴ）は１５ではないことが示されている。
【００５６】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部１４は、たとえば、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＡ＿ＲＥＱ部分の論理をトレースし、Ａ＿ＲＥＱが０にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００５７】
図９は、検証プロパティ名が２＿ａ＿ｒｅｑ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
１行目の６＿ａ＿ｒｅｑ＿ａｓｔ＿ｐｒａｃｔｉｃｅが、検証プロパティ名である。
【００５８】
２行目には、この検証プロパティＢの内容が記述されており、回路部２１のクロック信号（ＡＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティＢが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ｂ＿ＡＣＫ＿ｑ２が１（アサート）の状態が１サイクル以上連続するとき、次のサイクルでＡ＿ＣＮＴが２になることが示されている。
【００５９】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証用情報生成部１４は、たとえば、検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときには、ハンドシェイク部２３からＢ＿ＡＣＫ部分の論理をトレースし、Ｂ＿ＡＣＫが１にならない条件を抽出する。そして、検証用情報生成部１４は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティＢを生成する。
【００６０】
図１０は、検証プロパティ名が３＿ｂ＿ａｃｋ＿ｄａｓｔの検証プロパティＡを用いた検証でエラーが発生したときに生成される検証プロパティＢの例である。
１行目の７＿ｂ＿ａｃｋ＿ａｓｔ＿ｐｒａｃｔｉｃｅが、検証プロパティ名である。
【００６１】
２行目には、この検証プロパティＢの内容が記述されており、回路部２２のクロック信号（ＢＣＬＫ）の立ち上がりエッジに同期してこの検証プロパティＢが動作することが示されている。さらに、ＲＳＴが０のとき、この検証プロパティＢを無効にすること、Ａ＿ＲＥＱ＿ｑ２が１（アサート）の状態が１サイクル以上連続するとき、次のサイクルでＢ＿ＣＮＴが０になることが示されている。
【００６２】
３行目では、検証プロパティＢの終わりが示されており、４行目では、上記の検証プロパティＢの内容が偽と判断された場合、エラーとすることが示されている。
検証部１３は、上記のような検証プロパティＢを用いて、ハンドシェイクの手順を満たさない信号を出力する側の回路部の動作レベル（実使用レベル）の検証（形式検証または動的検証）を行い（ステップ１６）、その結果を出力する（ステップＳ１７）。なお、ステップＳ１４の処理で、エラーが発生しないと判定された場合には、ハンドシェイク部２３でデッドロックは発生しない旨の検証結果が出力される。
【００６３】
ステップＳ１６では、たとえば、以下のような検証が行われる。
たとえば、図８に示した検証プロパティＢが生成された場合、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらずＢ＿ＡＣＫがアサートされない条件があるということを示している。このとき検証部１３は、Ｂ＿ＡＣＫを出力する回路部２２において、検証プロパティＢを用いて、Ａ＿ＲＥＱ＿ｑ２がアサートされたにもかかわらずＢ＿ＡＣＫがアサートされない条件が回路動作時に起こり得るか検証する。
【００６４】
検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続したとき、Ｂ＿ＲＳＴが１でなく、回路部２２がリセット状態のままである場合が回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６５】
また、検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続したとき、回路部２２のカウンタ値（Ｂ＿ＣＮＴ）が１５のままである場合が回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６６】
一方、図９に示した検証プロパティＢが生成された場合、Ｂ＿ＡＣＫ＿ｑ２がアサートされたにもかかわらずＡ＿ＲＥＱがデアサートされない条件があるということを示している。このとき検証部１３は、Ａ＿ＲＥＱに変化を与える側の回路部２１において、検証プロパティＢを用いて、Ｂ＿ＡＣＫ＿ｑ２がアサートされたにもかかわらずＡ＿ＲＥＱがデアサートされない条件が回路動作時に起こり得るか検証する。
【００６７】
検証部１３は、Ｂ＿ＡＣＫ＿ｑ２が１の状態が１サイクル以上連続しても、Ａ＿ＣＮＴが２にならない場合が、回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００６８】
また、図１０に示した検証プロパティＢが生成された場合、Ａ＿ＲＥＱ＿ｑ２がデアサートされたにもかかわらずＢ＿ＡＣＫがデアサートされない条件があるということを示している。このとき検証部１３は、Ｂ＿ＡＣＫを出力する側の回路部２２において、検証プロパティＢを用いて、Ａ＿ＲＥＱ＿ｑ２がデアサートされたにもかかわらずＢ＿ＡＣＫがデアサートされない条件が回路動作時に起こり得るか検証する。
【００６９】
検証部１３は、Ａ＿ＲＥＱ＿ｑ２が１の状態が１サイクル以上連続しても、Ｂ＿ＣＮＴが０にならない場合が、回路部２２の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部１３は、ハンドシェイク部２３でデッドロックが発生する可能性があることを検証結果として出力する。
【００７０】
以上のように第２の実施の形態の検証装置１０ａ及び検証方法によれば、検証プロパティＡを生成して、検証することで、論理回路の非同期部分であるハンドシェイク部２３の検証漏れを抑制できる。
【００７１】
また、検証プロパティＡを用いてハンドシェイク部２３の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証プロパティＢを用いて検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制できる。
【００７２】
また、ハンドシェイク部２３のデッドロックを見逃さなくなるので、各クロックドメイン別に検証を進めることも可能となる。
なお、上記のような第１及び第２の実施の形態の検証装置１０，１０ａは、以下のようなコンピュータにより実現可能である。
【００７３】
図１１は、本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。
コンピュータ１００は、ＣＰＵ（Central Processing Unit）１０１によって装置全体が制御されている。ＣＰＵ１０１には、バス１０８を介してＲＡＭ（Random Access Memory）１０２と複数の周辺機器が接続されており、検証装置１０，１０ａの各部の機能を実現する。
【００７４】
ＲＡＭ１０２は、コンピュータ１００の主記憶装置として使用される。ＲＡＭ１０２には、ＣＰＵ１０１に実行させるＯＳ（Operating System）のプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、ＲＡＭ１０２には、ＣＰＵ１０１による処理に用いる各種データが格納される。
【００７５】
バス１０８に接続されている周辺機器としては、ハードディスクドライブ（ＨＤＤ:Hard Disk Drive）１０３、グラフィック処理装置１０４、入力インタフェース１０５、光学ドライブ装置１０６、及び通信インタフェース１０７がある。
【００７６】
ＨＤＤ１０３は、内蔵したディスクに対して、磁気的にデータの書き込み及び読み出しを行う。ＨＤＤ１０３は、コンピュータ１００の二次記憶装置として使用される。ＨＤＤ１０３には、ＯＳのプログラム、各種検証ツールなどのアプリケーションプログラム、及び図１に示した検証対象データＤ１などの各種データが格納される。なお、二次記憶装置としては、フラッシュメモリなどの半導体記憶装置を使用することもできる。
【００７７】
グラフィック処理装置１０４には、モニタ１０４ａが接続されている。グラフィック処理装置１０４は、ＣＰＵ１０１からの命令に従って、検証結果などの画像をモニタ１０４ａの画面に表示させる。モニタ１０４ａとしては、ＣＲＴ（Cathode Ray Tube）を用いた表示装置や液晶表示装置などがある。
【００７８】
入力インタフェース１０５には、キーボード１０５ａとマウス１０５ｂとが接続されている。入力インタフェース１０５は、キーボード１０５ａやマウス１０５ｂから送られてくる信号をＣＰＵ１０１に送信する。なお、マウス１０５ｂは、ポインティングデバイスの一例であり、他のポインティングデバイスを使用することもできる。他のポインティングデバイスとしては、タッチパネル、タブレット、タッチパッド、トラックボールなどがある。
【００７９】
光学ドライブ装置１０６は、レーザ光などを利用して、光ディスク１０６ａに記録されたデータの読み取りを行う。光ディスク１０６ａは、光の反射によって読み取り可能なようにデータが記録された可搬型の記録媒体である。光ディスク１０６ａには、ＤＶＤ（Digital Versatile Disc）、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ（Compact Disc Read Only Memory）、ＣＤ−Ｒ（Recordable）／ＲＷ（ReWritable）などがある。
【００８０】
通信インタフェース１０７は、ネットワーク１０７ａに接続されている。通信インタフェース１０７は、ネットワーク１０７ａを介して、他のコンピュータまたは通信機器との間でデータの送受信を行う。
【００８１】
以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。
また、検証装置１０，１０ａが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータ（たとえば、図１１のようなコンピュータ１００）で実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記憶装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記憶装置には、ＨＤＤ、フレキシブルディスク（ＦＤ）、磁気テープなどがある。光ディスクには、ＤＶＤ、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ／ＲＷなどがある。光磁気記録媒体には、ＭＯ（Magneto-Optical disk）などがある。
【００８２】
プログラムを流通させる場合には、たとえば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００８３】
プログラムを実行するコンピュータは、たとえば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、ネットワークを介して接続されたサーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムにしたがった処理を実行することもできる。
【００８４】
また、上記の処理機能の少なくとも一部を、ＤＳＰ（Digital Signal Processor）、ＡＳＩＣ（Application Specific Integrated Circuit）、ＰＬＤ（Programmable Logic Device）などの電子回路で実現することもできる。
【００８５】
以上、実施の形態に基づき、本発明の検証装置、検証方法及びプログラムの一観点について説明してきたが、これらは一例にすぎず、上記の記載に限定されるものではない。
【符号の説明】
【００８６】
１０ 検証装置
１１ 記憶部
１２ 抽出部
１３ 検証部
２０ 論理回路
２１，２２ 回路部
２３ ハンドシェイク部
Ｄ１ 検証対象データ
【特許請求の範囲】
【請求項１】
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、
を有することを特徴とする検証装置。
【請求項２】
前記信号が、前記データの送受信時に満たすべき条件を記述した第１の検証用情報を生成する検証用情報生成部を有し、
前記検証部は、生成された前記第１の検証用情報を用いて、前記信号が前記手順を満たすか否か検証することを特徴とする請求項１に記載の検証装置。
【請求項３】
前記検証用情報生成部は、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記データの送受信時に前記手順を満たす場合の条件を記述した第２の検証用情報を生成し、
前記検証部は、生成された前記第２の検証用情報を用いて、前記信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証することを特徴とする請求項２に記載の検証装置。
【請求項４】
コンピュータによって実行される検証方法であって、
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、
前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、
ことを特徴とする検証方法。
【請求項５】
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、
前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、
処理をコンピュータに実行させるプログラム。
【請求項１】
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、
を有することを特徴とする検証装置。
【請求項２】
前記信号が、前記データの送受信時に満たすべき条件を記述した第１の検証用情報を生成する検証用情報生成部を有し、
前記検証部は、生成された前記第１の検証用情報を用いて、前記信号が前記手順を満たすか否か検証することを特徴とする請求項１に記載の検証装置。
【請求項３】
前記検証用情報生成部は、前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記データの送受信時に前記手順を満たす場合の条件を記述した第２の検証用情報を生成し、
前記検証部は、生成された前記第２の検証用情報を用いて、前記信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証することを特徴とする請求項２に記載の検証装置。
【請求項４】
コンピュータによって実行される検証方法であって、
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、
前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、
ことを特徴とする検証方法。
【請求項５】
第１のクロック信号で動作する第１の回路部と、第２のクロック信号で動作する第２の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第１の回路部と前記第２の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、
抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、
前記手順を満たさない前記信号があるとき、前記第１の回路部と前記第２の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、
処理をコンピュータに実行させるプログラム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【公開番号】特開２０１３−３７６０７（Ｐ２０１３−３７６０７Ａ）
【公開日】平成２５年２月２１日（２０１３．２．２１）
【国際特許分類】
【出願番号】特願２０１１−１７４６７５（Ｐ２０１１−１７４６７５）
【出願日】平成２３年８月１０日（２０１１．８．１０）
【出願人】（３０８０１４３４１）富士通セミコンダクター株式会社 (2,507)
【Ｆターム（参考）】
【公開日】平成２５年２月２１日（２０１３．２．２１）
【国際特許分類】
【出願日】平成２３年８月１０日（２０１１．８．１０）
【出願人】（３０８０１４３４１）富士通セミコンダクター株式会社 (2,507)
【Ｆターム（参考）】
[ Back to top ]