(57)【要約】【課題】全体回路についての高位記述と検証対象記述との等価性検証方法において、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定する。【解決手段】等価性検証方法は、全体回路を複数のモジュールに分割し、高位モジュール記述群と検証対象モジュール記述群とを生成する第１ステップと、モジュール毎の等価性検証を実行する第２ステップと、全体回路についての等価性を判定する第３ステップを含んで構成される。ここで、第３ステップは、高位モジュール記述群と検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、全体回路についての等価性を判定する。【選択図】図１
2014081803.tif 000002
【特許請求の範囲】
【請求項１】
全体回路についての高位記述と検証対象記述との等価性を電子計算機上のソフトウェアによって検証する等価性検証方法であって、
前記全体回路を複数のモジュールに分割し、高位モジュール記述群と検証対象モジュール記述群とを生成する第１ステップと、
前記モジュール毎の等価性検証を実行する第２ステップと、
前記全体回路についての等価性を判定する第３ステップとを含み、
前記第３ステップは、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、前記全体回路についての等価性を判定する、等価性検証方法。
【請求項２】
請求項１において、前記第３ステップは、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが閉ループを含まず、前記複数のモジュール全てのそれぞれで前記レイテンシの差が一律であるという第１条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がなく、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律であるという第２条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含み、且つ、前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むか、又は、前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で、前記第１サブグラフから前記第２サブグラフへの有向辺が１つのみ存在し、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという第３条件のうちのいずれかが充足されるときに、前記全体回路の前記高位記述と前記検証対象記述が等価であると判定する、等価性検証方法。
【請求項３】
請求項２において、前記第１条件、前記第２条件及び前記第３条件のいずれも充足しない入出力信号があるとき、前記充足しない入出力信号についての情報を出力する第４ステップをさらに含む、等価性検証方法。
【請求項４】
請求項１において、前記第３ステップは、前記第２ステップで等価でないと判定された不等価モジュールがあるとき、前記不等価モジュールが等価であると仮定して、前記全体回路についての等価性を判定する、等価性検証方法。
【請求項５】
請求項１において、前記第１ステップは、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが、閉ループを含まないという第４条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという第５条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むという第６条件のうちのいずれかが充足されるように、前記モジュール分割を行う、等価性検証方法。
【請求項６】
全体回路についての高位記述とＲＴＬ記述とＲＴＬ回路実装情報が入力され、
前記全体回路を複数のモジュールに分割し、高位モジュール記述群とＲＴＬモジュール記述群とを生成する第１ステップと、
前記モジュールごとの等価性検証を実行する第２ステップと、
前記全体回路についての等価性を判定する第３ステップとを含み、
前記ＲＴＬ回路実装情報は、前記モジュールごとにＲＴＬ実装後のスループット及び／またはレイテンシのサイクル数の仕様情報を含み、
前記第３ステップは、前記ＲＴＬ回路実装情報に基づいて前記全体回路についての等価性を判定する、等価性検証装置。
【請求項７】
請求項６において、前記第３ステップは、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが、閉ループを含まず、前記レイテンシの差が一律であるという第１条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がなく、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律であるという第２条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含み、且つ、前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むか、又は、前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で、前記第１サブグラフから前記第２サブグラフへの有向辺が、入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしないという性質を満たし、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという第３条件のうちのいずれかが充足されるときに、前記全体回路の前記高位記述と前記ＲＴＬ記述が等価であると判定する、等価性検証装置。
【請求項８】
請求項７において、前記第１条件、前記第２条件及び前記第３条件のいずれも充足しない入出力信号があるとき、前記充足されない入出力信号についての情報を出力する第４ステップをさらに含む、等価性検証装置。
【請求項９】
請求項６において、前記第３ステップは、前記第２ステップで等価でないと判定された不等価モジュールがあるとき、前記不等価モジュールが等価であると仮定して、前記全体回路についての等価性を判定する、等価性検証装置。
【請求項１０】
請求項６において、前記高位記述と前記ＲＴＬ記述との等価性検証を、前記全体回路について一括して開始し、所定の時間内に終了しないときに、前記第１ステップを実行し、
前記第１ステップは、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが、閉ループを含まないという第４条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという第５条件、
または、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むという第６条件のうちのいずれかが充足されるように、前記モジュール分割を行う、等価性検証装置。
【請求項１１】
全体回路についての高位記述と検証対象記述との等価性を電子計算機上のソフトウェアによって検証する等価性検証方法であって、
前記全体回路を、分割条件を満たしながら複数のモジュールに分割する第１ステップと、
前記モジュールごとの等価性検証を実行する第２ステップと、
前記モジュール間のインターフェースについて、十分条件を満たすか否かを判定する第３ステップと、
前記十分条件を満たさないインターフェースを示す情報を出力する第４ステップとを含み、
前記十分条件は、前記全体回路についての高位記述と検証対象記述とが等価であるための十分条件であり、前記分割条件は前記十分条件が充足されるときに必ず充足される条件である、等価性検証方法。
【請求項１２】
請求項１１において、前記複数のモジュールのそれぞれを頂点とし、前記複数のモジュール間の信号線を有向辺としたグラフにおいて、
前記分割条件は、前記グラフが閉ループを含まないという第１条件と、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという第２条件と、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むという第３条件との論理和であり、
前記十分条件は、第４条件と第５条件と第６条件との論理和であり、
前記第４条件は、前記複数のモジュール全てのそれぞれで前記レイテンシの差が一律であるという条件と前記第１条件との論理積であり、
前記第５条件は、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律であるという条件と前記第２条件との論理積である
前記第６条件は、前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含むか、又は、前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で、前記第１サブグラフから前記第２サブグラフへの有向辺が、入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしないという性質を満たし、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差がないという条件と前記第３条件との論理積である、等価性検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、半導体集積回路ＬＳＩ (Large Scale Integrated Circuit) の設計に利用される、２つのハードウェア記述言語で記述された回路の等価性を検証する等価性検証に関し、特に回路を分割することにより、より高速に実行できる等価性検証に好適に利用できるものである。
【背景技術】
【０００２】
LSI (Large Scale Integrated Circuit) の設計では、例えばＣ言語などの高位記述言語で記述された回路から、RTL (Register Transfer Level) など、より中位・低位の記述言語で記述された回路を生成し、最終的にゲートレベルの回路を経て、素子レベルのレイアウト設計に至る工程が広く採用されている。高位言語記述とRTLなどより中低位言語記述とが等価であることは、EDA (Electronic Design Automation) ツールの一つである等価性検証装置により検証される。高位言語記述では例えばフィルタ特性など高位の機能的仕様を検証し、中低位言語記述ではより微視的な電気的仕様の検証を行う。記述言語が異なっても等価の回路であることが証明できれば、機能検証、動作検証を互いに補完的に実施すれば足りるため、設計の効率が向上する。RTL記述とゲート論理記述との等価性検証は、既に広く採用されている。これに対して、高位記述と中低位記述の間の高位等価性検証は、現実的な時間内で処理が完了できないなどの問題がある。
【０００３】
一般に、回路の等価性検証に要する処理時間は、回路規模に対して指数関数的に増加する。したがって、高位等価性検証を現実的な時間で完了させるためには、回路規模を適度に分割する必要があるため、大規模な回路を対象とする場合、モジュールに分割して、各モジュール毎に等価性検証を実施する事となる。ここで、モジュール分割とは、モジュール、スレッドやプロセスなど処理として機能が実装単位に分割することを指す。
【０００４】
特許文献１には、等価性検証を効率よく行うことができる等価性検証システムが開示されている。動作合成装置と密接な連携を取り、各中間レベル記述を出力させ、工程ごとに前後の中間レベル記述間の等価性検証を実施する。ここで、動作記述の変数とRTLのレジスタや、状態遷移の対応関係を動作合成システムが出力する。各状態遷移での実行条件及び実行動作は、それぞれの記述からモデル抽出を行い、前記モデル上で記号シミュレーション（Symbolic Simulation）を行う事で取得する。動作合成からの出力情報が正しいとの前提で、各遷移での、遷移条件と実行文が入力記述と合成結果RTLにて等価である事を、充足可能性判定問題に帰着する事で検証する。この検証にて、動作合成での変換履歴から、ある条件下で対応付けられる中間論理コーンを識別することで、論理コーンの分割を実施し、等価性検証の高速化を行う。
【０００５】
特許文献２には、検証対象の回路の一部をブラックボックス化して行う、論理等価性検証方法が開示されている。ブラックボックスを含む場合、ブラックボックスをまたいだ定数伝播が一般にできなくなるため、ブラックボックス後段の回路を対象とした、テスト合成前後での等価性検証では、擬似不一致が発生し得る。これを、解決する目的として、テスト合成にて挿入される回路構成に着目して正しく固定値伝播が可能なようにブラックボックス部を適宜選定・設定する手法が開示されている。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００７‐２６５１７５号公報
【特許文献２】特開２００７‐２５７４４０号公報
【非特許文献】
【０００７】
【非特許文献１】エル．ピー．カローニ、ケイ．エル．マクミラン、エー．エル．サンジョバンニ−ヴィンセンテリ（L.P. Carloni, K.L. McMillan, and A.L. Sangiovanni-Vincentelli）、「セオリ  オブ  レイテンシ−インセシティブ  デザイン」（Theory of Latency-Insensitive Design）、アイトリプルイー  トランザクションオンＣＡＤ  ヴォリウム２０  ナンバー９、（IEEE Trans. on CAD, Vol.20, No.9）、（米国）、米国電気電子学会（IEEE; The Institute of Electrical and Electronics Engineers, Inc.）、2001年9月
【発明の概要】
【発明が解決しようとする課題】
【０００８】
特許文献１及び２について本発明者が検討した結果、以下のような新たな課題があることがわかった。
【０００９】
特許文献１は、組合せ論理レベルでの分割による高速化手法を開示しているのであって、順序回路としてモジュール毎に分割して、等価性検証を実施する事での高速化手法を開示しているわけではない。
【００１０】
特許文献２に開示される技術は、固定値伝播にのみ着目しており、信号サイクルのズレには一切着目していないため、実行サイクル数が異なるが機能として一致するモジュールをブラックボックスとして扱う事ができない。
【００１１】
従来のRTL記述とゲート論理記述との等価性検証や、上記特許文献１及び２に開示される技術は、比較するRTL記述とゲート論理記述の信号サイクルが一致すること、即ちサイクル精度（Cycle Accurate）での一致を前提としている。例えば、特許文献１で組合せ論理レベルでの分割を前提としているのは、組合せ論理レベルではクロックサイクル単位での遅延は発生しないので、RTL記述とゲート論理記述の信号サイクルが一致すること（サイクル精度での一致）が保証されているからである。
【００１２】
しかし、高位等価性検証では、分割されたモジュールの高位記述とRTL記述でサイクル精度での一致が保証されるとは限らない。全てのモジュールがサイクル精度モデルであり、高位記述とRTL記述がサイクルレベルで一致する場合には、命題「全モジュールが各々等価 ∧ 接続関係が一対一対応 ⇒ 全体で等価」（「∧」は「且つ」、「⇒」は「ならば」を表す数学記号である。）が成立するが、あるモジュールにて、高位記述とRTL記述が、機能としては等価であるがサイクルレベルでは異なる振る舞いをする場合、前記命題は一般に不成立となる。即ち、各モジュール個々に等価性検証のみを行ったのでは、高位記述のモジュール間の信号受け渡しが、RTL記述で維持されているかに関しては未検証となる。このため、この部分での不整合が発生すると、全体として等価とならない場合がある。そのため、単純にモジュール分割して等価性検証を実施する事が出来ない。これが、分割検証での問題である。
【００１３】
このような課題を解決するための手段を以下に説明するが、その他の課題と新規な特徴は、本明細書の記述及び添付図面から明らかになるであろう。
【課題を解決するための手段】
【００１４】
一実施の形態によれば、下記の通りである。
【００１５】
すなわち、全体回路についての高位記述と検証対象記述との等価性を電子計算機上のソフトウェアによって検証する等価性検証方法であって以下の各ステップを含んで構成される。全体回路を複数のモジュールに分割し、高位モジュール記述群と検証対象モジュール記述群とを生成する第１ステップと、モジュール毎の等価性検証を実行する第２ステップと、全体回路についての等価性を判定する第３ステップである。ここで、第３ステップは、高位モジュール記述群と検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、全体回路についての等価性を判定する。
【発明の効果】
【００１６】
前記一実施の形態によって得られる効果を簡単に説明すれば下記のとおりである。
【００１７】
すなわち、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。
【図面の簡単な説明】
【００１８】
【図１】図１は、実施の形態の概要の等価検証システムの動作を表すフローチャートである。
【図２】図２は、実施形態１の等価検証システムの動作を表すフローチャートである。
【図３】図３は、参考例の等価検証システムの動作を表すフローチャートである。
【図４】図４は、モジュール分割における分割条件についての説明図である。
【図５】図５は、分割条件チェックＳ１の処理の一例を表すフローチャート（前半）である。
【図６】図６は、分割条件チェックＳ１の処理の一例を表すフローチャート（後半）である。
【図７】図７は、十分条件チェックＳ２の処理の一例を表すフローチャートである。
【図８】図８は、サイクル同期性チェックＳ２＿１３の処理の一例を表すフローチャートである。
【図９】図９は、サイクル同期性チェック例のモジュール構成を例示する説明図である。
【図１０】図１０は、サイクル同期性チェック例の高位記述での各モジュールの実行サイクル数を例示する説明図である。
【図１１】図１１は、サイクル同期性チェック例の合成結果ＲＴＬでの各モジュールの実行サイクル数を例示する説明図である。
【図１２】図１２は、サイクル同期性チェック例の高位記述での各モジュールの実行サイクル数を例示する表である。
【図１３】図１３は、サイクル同期性チェック例のＲＴＬ回路実装情報を例示する表である。
【図１４】図１４は、サイクル同期性チェック例のモジュール間のインターフェースにおける信号授受のサイクルずれの算出例を表す表である。
【図１５】図１５は、サイクル同期性チェック例のモジュール間のインターフェースにおけるサイクル同期性を満たさない信号の扱いについて説明するためのタイミングチャートである。
【図１６】図１６は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（前半）である（実施形態３）。
【図１７】図１７は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（後半）である（実施形態３）。
【図１８】図１８は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（前半）である（実施形態４）。
【図１９】図１９は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（後半）である（実施形態４）。
【発明を実施するための形態】
【００１９】
１．実施の形態の概要
先ず、本願において開示される代表的な実施の形態について概要を説明する。代表的な実施の形態についての概要説明で括弧を付して参照する図面中の参照符号はそれが付された構成要素の概念に含まれるものを例示するに過ぎない。
【００２０】
〔１〕＜十分条件による全体回路の等価性判定方法＞
全体回路についての高位記述（１１）と検証対象記述（１２）との等価性を電子計算機上のソフトウェアによって検証する等価性検証方法であって、以下の各ステップを含んで構成される。
【００２１】
前記全体回路を複数のモジュールに分割し、高位モジュール記述群（１４）と検証対象モジュール記述群（１５）とを生成する第１ステップ（Ｓ１）。
【００２２】
前記モジュール毎の等価性検証を実行する第２ステップ（Ｓ３）。
【００２３】
前記全体回路についての等価性を判定する第３ステップ（Ｓ２）。
【００２４】
前記第３ステップは、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、前記全体回路についての等価性を判定する。
【００２５】
これにより、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。
【００２６】
〔２〕＜十分条件の判定方法＞
項１において、前記第３ステップは、以下の第１条件、第２条件及び第３条件のうちのいずれかが充足されるときに、前記全体回路の前記高位記述と前記検証対象記述が等価であると判定する（Ｓ２＿４、Ｓ２＿８、Ｓ２＿９、Ｓ２＿１１、Ｓ２＿１４）。
【００２７】
前記第１条件は、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが閉ループを含まず、前記複数のモジュール全てのそれぞれで前記レイテンシの差が一律である（Ｓ２＿１，Ｓ２＿１３，Ｓ２＿１４）。
【００２８】
前記第２条件は、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がなく（Ｓ２＿５）、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律である（Ｓ２＿１３）。
【００２９】
前記第３条件は、以下の条件の論理和。前記グラフが閉ループを含み（Ｓ２＿１）、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含み（Ｓ２＿３）、且つ、前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ２＿４）。前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で（Ｓ２＿８）、前記第１サブグラフから前記第２サブグラフへの有向辺が１つのみ存在し（Ｓ２＿９）、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差が一律である（Ｓ２＿１２、Ｓ２＿１３）。
【００３０】
これにより、電子計算機上のモデルにより、全体回路が等価であるための十分条件を判定することができる。
【００３１】
〔３〕＜十分条件を充足しない入出力信号情報の出力＞
項２において、前記第１条件、前記第２条件及び前記第３条件のいずれも充足しない入出力信号があるとき、前記充足しない入出力信号についての情報（１６）を出力する第４ステップ（Ｓ２＿１６）をさらに含む。
【００３２】
これにより、全体回路が等価であることを検証するために、シミュレーションなどの方法を組合せる場合に注目すべき入出力信号が明確となり、設計効率を向上することができる。
【００３３】
〔４〕＜保証仮定推論＞
項１または項３において、前記第３ステップは、前記第２ステップで等価でないと判定された不等価モジュールがあるとき、前記不等価モジュールが等価であると仮定して、前記全体回路についての等価性を判定する。
【００３４】
これにより、等価でないモジュールの判定結果が他のモジュールに伝搬することなく、全体回路における全てのモジュールに関する処理を実施すことができる。
【００３５】
〔５〕＜分割条件＞
項１から項４のいずれか１項において、前記第１ステップは、第４条件、第５条件及び第６条件のうちのいずれかが充足されるように、前記モジュール分割を行う。
【００３６】
前記第４条件は、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが、閉ループを含まない（Ｓ１＿４）。
【００３７】
前記第５条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がない（Ｓ１＿１８）。
【００３８】
前記第６条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ１＿９，Ｓ１＿１０）。
【００３９】
これにより、分割による高速化に適しているか否かの判断を、等価性検証を行う前に判定することができる。等価性検証における高速化を図ることができる。さらに、等価性検証を予定している大規模システムの設計において、設計の初期段階から等価性検証の高速化を見越した設計が可能となる。
【００４０】
〔６〕＜十分条件による全体回路の等価性判定装置＞
全体回路についての高位記述（１１）とＲＴＬ記述（１２）とＲＴＬ回路実装情報（１３）が入力される等価性検証装置であって、以下の各ステップを実行可能に含んで構成される。
【００４１】
前記全体回路を複数のモジュールに分割し、高位モジュール記述群（１４）とＲＴＬモジュール記述群（１５）とを生成する第１ステップ（Ｓ１）。
【００４２】
前記モジュールごとの等価性検証を実行する第２ステップ（Ｓ３）。
【００４３】
前記全体回路についての等価性を判定する第３ステップ（Ｓ２）。
【００４４】
ここで、前記ＲＴＬ回路実装情報は、前記モジュールごとにＲＴＬ実装後のスループット及び／またはレイテンシのサイクル数の仕様情報を含む。前記第３ステップは、前記ＲＴＬ回路実装情報に基づいて前記全体回路についての等価性を判定する。
【００４５】
これにより、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。
【００４６】
〔７〕＜十分条件の判定装置＞
項６において、前記第３ステップは、以下の第１条件、第２条件及び第３条件のうちのいずれかが充足されるときに、前記全体回路の前記高位記述と前記ＲＴＬ記述が等価であると判定する（Ｓ２＿４、Ｓ２＿８、Ｓ２＿９、Ｓ２＿１１、Ｓ２＿１４）。
【００４７】
前記第１条件は、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが閉ループを含まず、前記複数のモジュール全てのそれぞれで前記レイテンシの差が一律である（Ｓ２＿１，Ｓ２＿１３，Ｓ２＿１４）。
【００４８】
前記第２条件は、前記グラフが閉ループを含み、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がなく（Ｓ２＿５）、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律である（Ｓ２＿１３）。
【００４９】
前記第３条件は、以下の条件の論理和。前記グラフが閉ループを含み（Ｓ２＿１）、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含み（Ｓ２＿３）、且つ、前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ２＿４）。前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で（Ｓ２＿８）、前記第１サブグラフから前記第２サブグラフへの有向辺が性質Ｃ「入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしない」を満たし（Ｓ２＿９）、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差が一律である（Ｓ２＿１２、Ｓ２＿１３）。ここで、前記性質が、プロパティ検査やモデル検査など既存技術で充足されるか否かを判定する事が出来るのは言うまでもない。
【００５０】
これにより、電子計算機上のモデルにより、全体回路が等価であるための十分条件を判定することができる。
【００５１】
〔８〕＜十分条件を充足しない入出力信号情報の出力＞
項７において、前記第１条件、前記第２条件及び前記第３条件のいずれも充足しない入出力信号があるとき、前記充足しない入出力信号についての情報（１６）を出力する第４ステップ（Ｓ２＿１６）をさらに含む。
【００５２】
これにより、全体回路が等価であることを検証するために、シミュレーションなどの方法を組合せる場合に注目すべき入出力信号が明確となり、設計効率を向上することができる。
【００５３】
〔９〕＜保証仮定推論＞
項６または項８において、前記第３ステップは、前記第２ステップで等価でないと判定された不等価モジュールがあるとき、前記不等価モジュールが等価であると仮定して、前記全体回路についての等価性を判定する。
【００５４】
これにより、等価でないモジュールの判定結果が他のモジュールに伝搬することなく、全体回路における全てのモジュールに関する処理を実施すことができる。
【００５５】
〔１０〕＜分割条件＞
請求項６から請求項９のいずれか１項において、前記高位記述と前記ＲＴＬ記述との等価性検証を、前記全体回路について一括して開始し（Ｓ１１）、所定の時間内に終了しないときに（Ｓ１２）、前記第１ステップを実行する。前記第１ステップは、第４条件、第５条件及び第６条件のうちのいずれかが充足されるように、前記モジュール分割を行う。
【００５６】
前記第４条件は、前記第１ステップは、前記モジュールを頂点とし前記入出力信号を有向辺として前記全体回路を表したグラフが、閉ループを含まない（Ｓ１＿４）。
【００５７】
前記第５条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がない（Ｓ１＿１８）。
【００５８】
前記第６条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ１＿９，Ｓ１＿１０）。
【００５９】
これにより、分割による高速化に適しているか否かの判断を、等価性検証を行う前に判定することができる。等価性検証における高速化を図ることができる。さらに、等価性検証を予定している大規模システムの設計において、設計の初期段階から等価性検証の高速化を見越した設計が可能となる。
【００６０】
〔１１〕＜分割条件によるモジュール分割＋十分条件による全体回路の等価性判定＋十分条件不充足入出力信号情報の出力＞
全体回路についての高位記述（１１）と検証対象記述（１２）との等価性を電子計算機上のソフトウェアによって検証する等価性検証方法であって、以下の各ステップを含んで構成される。
【００６１】
前記全体回路を、分割条件を満たしながら複数のモジュールに分割する第１ステップ（Ｓ１）。
【００６２】
前記モジュールごとの等価性検証を実行する第２ステップ（Ｓ３）。
【００６３】
前記モジュール間のインターフェースについて、十分条件を満たすか否かを判定する第３ステップ（Ｓ２）。
【００６４】
前記十分条件を満たさないインターフェースを示す情報（１６）を出力する第４ステップ（Ｓ２＿１６）。
【００６５】
ここで、前記十分条件は、前記全体回路についての高位記述（１１）と検証対象記述（１２）とが等価であるための十分条件であり、前記分割条件は前記十分条件が充足されるときに必ず充足される条件である。
【００６６】
これにより、分割による高速化に適しているか否かの判断を、等価性検証を行う前に判定することができる。等価性検証における高速化を図ることができ、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。さらに、等価であると判定することができない場合であっても、等価性検証のための全体シミュレーションなどの方法を組合せる場合に注目すべき入出力信号が明確となり、設計効率を向上することができる。
【００６７】
〔１２〕＜分割条件および十分条件の判定方法＞
項１１において、前記複数のモジュールのそれぞれを頂点とし、前記複数のモジュール間の信号線を有向辺としたグラフにおいて、前記分割条件と前記十分条件は以下のとおり規定される。
【００６８】
前記分割条件は、第１条件と第２条件と第３条件との論理和である。
【００６９】
前記第１条件は、前記グラフが閉ループを含まない（Ｓ１＿４）。
【００７０】
前記第２条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールで前記レイテンシの差がない（Ｓ１＿１８）。
【００７１】
前記第３条件は、前記グラフが閉ループを含み（Ｓ１＿４）、前記閉ループを構成する頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ１＿９，Ｓ１＿１０）。
【００７２】
前記十分条件は、第４条件と第５条件と第６条件との論理和である。
【００７３】
前記第４条件は、前記複数のモジュール全てのそれぞれで前記レイテンシの差が一律であるという条件と前記第１条件との論理積である（Ｓ２＿１，Ｓ２＿１３，Ｓ２＿１４）。
【００７４】
前記第５条件は、前記閉ループを構成する頂点以外の頂点で表される全てのモジュールで、前記レイテンシの差が一律であるという条件（Ｓ２＿１３）と前記第２条件（Ｓ１＿１８）との論理積である（Ｓ２＿１３、Ｓ２＿１４）。
【００７５】
前記第６条件は、下記の２条件の論理和で規定される条件と前記第３条件との論理積である。
【００７６】
前記閉ループを構成しない頂点で表される全てのモジュールが前記入出力信号のサイクル精度の遅延を整合させる回路を含む（Ｓ２＿３）。
【００７７】
前記グラフを入出力信号のサイクル精度の遅延を整合させる前記回路を含む第１サブグラフと含まない第２サブグラフに分割可能で（Ｓ２＿８）、前記第１サブグラフから前記第２サブグラフへの有向辺が性質Ｃ「入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしない」を満たし（Ｓ２＿９）、前記第２サブグラフを構成する頂点で表される全てのモジュールで前記レイテンシの差が一律である（Ｓ２＿１２、Ｓ２＿１３）。
【００７８】
これにより、電子計算機上のモデルにより、全体回路が等価であるための十分条件を判定することができる。
【００７９】
２．実施の形態の詳細
〔数学記号の説明〕
実施の形態及び図面で使用する各種数学記号は、この技術分野において慣用されている記号であるが、念の為に説明する。
記号「∧」は、「および」即ち論理積を表す。
記号「∨」は、「または」即ち論理和を表す。
記号「¬」は、「否定」を表す。
記号「⇒」は、「ならば」を表す。例えば「Ｐ⇒Ｑ」は、「命題Ｐが真ならば命題Ｑが真である」という命題を表す。
記号「∈」は、「集合に属すること」を表す。
記号「∀」は、「任意の」を表す。例えば「∀ｘ∈Ｓ；Ｐ（ｘ）」は、「集合Ｓの任意の要素ｘについて命題Ｐ（ｘ）が成立する」ことを表す。
記号「∃」は、「少なくとも」を表す。例えば「∃ｘ∈Ｓ；Ｐ（ｘ）」は、「集合Ｓには、命題Ｐ（ｘ）が成立する要素ｘが少なくとも１個存在する」ことを表す。
記号「φ」は、「空集合」を表す。
記号「s. t.」は、「such that」を表す。
【００８０】
〔参考例〕
実施形態についての説明に先立って、発明者によって事前に検討された等価検証技術について、参考例として説明する。
【００８１】
動作合成可能な高位記述を、システムレベル言語であるSystemCやプログラミング言語Cなどを用いて記述し、このレベルでの機能検証を行う。次に、どのような回路を合成するかの指定を行った動作合成スクリプトを作成し、動作合成ツールにて、動作合成を実施する。動作合成ツールからは、合成結果のRTLのハードウェア記述言語による記述（RTL記述）が生成される。ここで、高位等価性検証ツールの実行に必要となる情報が記述された雛形の検証スクリプトを合わせて生成することができる。検証スクリプトには、高位レベル記述とRTL記述での入力・出力ポートの対応関係や、双方の出力ポートの比較サイクルなどが記述されている。次いで、高位レベル記述と動作合成結果RTL、及び雛形検証スクリプトを高位等価性検証ツールに入力し、高位等価性検証を実施する。高位等価性検証では、実行時間が長大化するという問題があるため、現実的な時間で実行が完了しない場合には、検証スクリプトへの情報追加や設定変更を実施する必要があり、これは人手作業となる。ここで、情報追加としては、高位レベル記述内の変数とRTL記述内のFF（フリップフロップ）とを対応づける情報などがあり、変更設定内容としては、リセットサイクル期間などがある。
【００８２】
現実的な時間で実行が完了しない場合には、上述の検証スクリプトへの情報追加や設定変更に代えて、モジュール分割を実施することを検討する。ここで、モジュール分割とは、モジュール、スレッドやプロセスなど処理として機能が実装単位に分割することを指す。
【００８３】
図３は、参考例の等価検証システムの動作を表すフローチャートである。
【００８４】
高位言語で記述された全体記述１１と、RTL記述された全体記述１２を入力し、全体回路を対象に一括処理する、高位記述対RTL記述の高位等価性検証を実施する（Ｓ１１）。全体記述とは、等価性検証対象の回路全体を指すが、LSI全体とは限らない。全体記述を対象とした等価性検証において、現実的な処理時間で結果が出ない場合（Ｓ１２）、検証規模削減による高速化を実施する目的で、モジュール分割を実施し（Ｓ２１）、モジュール毎の高位等価性検証を実施する（Ｓ２２）。現実的な時間で処理が終了するようになるまで、適宜モジュール分割を繰り返す（Ｓ２３）。ここで、モジュール分割には、高位記述修正と、人手または動作合成再実行によるRTL記述修正が含まれるかも知れない。
【００８５】
次いで、分割されたモジュール毎の等価性検証（Ｓ２２）にて、全てのモジュールそれぞれで高位記述とRTL記述が等価であると判断されたとしても、上述の分割検証での問題点で指摘したように、全体記述の動作が一致するとは限らない。そこで、高位記述向けテストベンチ１８を流用して、RTL検証向けテストベンチ１９を作成し（Ｓ２４）、それを用いてRTLシミュレーション（Ｓ２５）を実施する事で、全体記述の動作が一致するかを確認する。
【００８６】
参考例の等価検証システムの問題点について説明する。
【００８７】
モジュール分割（Ｓ２１）を実施した場合、最終的には、高位記述向けテストベンチ１８から作成したRTL記述向けテストベンチ１９でのシミュレーション（Ｓ２５）を実施する事で、全体記述の動作が一致しているか否かの確認を行うため、全体記述が等価であることの数学的な（論理的な）証明は原理的に達成し得ない。高位等価検証の高速化のためにモジュール分割を行い、全てのモジュールそれぞれで等価であると判定されたとしても、信号サイクルが一致しない場合に全体回路として等価であるとは言えないという問題に対して、上述の参考例は、シミュレーションで解決を図ったものである。実用的には、全体回路が等価であることの検証には十分である場合が多いが、あくまでもシミュレーションであるために、等価の証明にまでは至っていない。また、高位記述とRTL記述で、サイクル動作が異なっている場合、高位記述向けテストベンチ１８を流用して、RTL検証向けテストベンチ１９を作成し（Ｓ２４）するために、テストベンチ自体のデバッグなどが必要となり、流用工数が無視できない。その上、規模が大きい場合、RTLシミュレーション（Ｓ２５）の処理時間が長大化する恐れがある。
【００８８】
仮に、検証確度向上を目的として、接続関係に着目したアサーション記述などを追加して検証を行うとしても、追加したアサーション記述が成立する事を示せば、本当に全体として動作一致するのかの証明戦略が存在しないため、結局は全体一致証明を成し得ない可能性が高い。しかも、どの部分に対してアサーション記述を作成すべきかの指針もないため、無駄なアサーション記述を作成してしまう可能性が否めず、アサーション記述挿入によるRTLシミュレーションの速度低下や、アサーション作成工数増大が懸念事項となる。ここで、アサーション記述とは、ソフトウェアにおいては、変数の仕様・性質など充足されるべき条件を記述し、実行時にその条件が満たされていないときにエラーを発生させるなどの機能を持つ記述である。一般には、プログラムの正当性確認のために使われる。ハードウェアのシミュレーションにおいても、回路ブロック間のインターフェース信号の満たすべき仕様を記述し、シミュレーションにおいてインターフェース信号に仕様違反がないかをチェックするために使われる記述である。
【００８９】
高位等価検証の高速化のためにモジュール分割を行い、全てのモジュールで等価であると判定されたとしても、信号サイクルが一致しない場合に全体回路として等価であるとは言えないという問題に対して、上述の参考例は、シミュレーションで解決を図ったものである。実用的には、全体回路が等価であることの検証には十分である場合が多いが、あくまでもシミュレーションであるために、等価の証明には至らないという問題がある。また、全体回路の等価性を検証するためのRTLシミュレーションのテストベンチ作成工数、アサーション記述作成工数、シミュレーション自体の処理時間の長大化などの問題がある。
【００９０】
〔実施の形態の概要〕
実施の形態の概要について説明する。図１は、実施の形態の概要の等価検証システムの動作を表すフローチャートである。実施の形態の概要の等価検証システムは、全体回路についての高位記述１１と検証対象記述１２との等価性を電子計算機上のソフトウェアによって検証する等価性検証システムであって、以下の各ステップを含んで構成される。
【００９１】
前記全体回路を複数のモジュールに分割し、高位モジュール記述群１４と検証対象モジュール記述群１５とを生成する第１ステップ（Ｓ１）。
【００９２】
前記モジュール毎の等価性検証を実行する第２ステップ（Ｓ３）。
【００９３】
前記全体回路についての等価性を判定する第３ステップ（Ｓ２）。
【００９４】
前記第３ステップは、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、前記全体回路についての等価性を判定する。
【００９５】
モジュール分割による等価性検証（Ｓ３）にて、全ての高位モジュール記述と検証対象モジュール記述が等価であると判断されたとしても、上述の分割検証での問題点で指摘したように全体動作が一致するとは限らない。上述の参考例では、全てのモジュールを結合した、全体回路記述についてシミュレーションを行うことによって全体回路での等価性を検証する。これに代えてあるいはこれに先立って、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、前記全体回路についての等価性を判定する。全体回路が等価であるための十分条件について検討する。この十分条件は、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、導出することができる。例えば、全てのモジュールにおいて、入出力信号におけるレイテンシの差がない場合、即ち、入出力信号の遅延がサイクル精度で一致している場合は、命題「全モジュールが各々等価∧接続関係が一対一対応⇒全体で等価」が成り立ち、全体回路は等価と判定することができる。また、例えば、全てのモジュールの入出力信号の受け渡しをハンドシェーク通信で行われる仕様となっている場合には、モジュール毎の入出力信号の遅延がサイクル精度で一致していなくても、全体回路は等価と判定することができる。モジュールごとの入出力信号のレイテンシに対する仕様は、必ずしもハンドシェーク通信である必要はなく、非特許文献１に開示されるような、レイテンシ非依存通信でも同様である。
【００９６】
以上のように、前記高位モジュール記述群と前記検証対象モジュール記述群のモジュールごとの入出力信号におけるレイテンシの差、及び／または、前記モジュールごとの入出力信号のレイテンシに対する仕様に基づいて、全体回路が等価であるための十分条件を導出することができ、その十分条件が充足されれば、全体回路は等価と判定することができる。
【００９７】
これにより、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。
【００９８】
実施の形態について更に詳述する。
【００９９】
〔実施形態１〕
図２は、実施形態１の等価検証システムの動作を表すフローチャートである。
【０１００】
全体記述を対象とした、高位記述１１対RTL記述１２の高位等価性検証を実施する（Ｓ１１）。ここで、現実的な処理時間で結果が出ない場合（Ｓ１２）、検証規模削減による高速化を実施する目的で、RTL回路実装情報１３を読み込んだ上で、分割条件を満たすモジュール分割を実施する（Ｓ１）。尚、分割条件については後述する。また、モジュール分割は与えられるものとし、モジュール分割後の構成が前記分割条件を満たすか否かの検証を実施するものとする。RTL回路実装情報１３は、概ね動作合成スクリプトのサイクル制約設定や等価性検証スクリプトのタイミング比較情報に対応する情報である。例えばサイクル精度合成、即ちサイクルレベルでの動作一致が必要なのか、スループット/レイテンシ・サイクル数指定を伴うパイプライン合成、即ちそのようなパイプライン回路に実装されている前提での動作一致が必要なのか、などのRTL回路のサイクル実装情報、即ちRTL実装後のスループット/レイテンシ・サイクル数情報が記載されている。現実的な時間で処理が終了するようになるまで（Ｓ１３）、適宜、後述する分割条件を満たすモジュール分割を実施する（Ｓ１）。ここで、前記分割条件を満たすモジュール分割では高位記述修正と（動作合成スクリプト修正と動作合成再実行による）RTL記述修正が含まれるかも知れない。
【０１０１】
次いで、分割による等価性検証（Ｓ３）にて、全てのモジュールそれぞれにて高位記述１４とＲＴＬ記述５が等価であると判定されたとしても（Ｓ４）、「発明が解決しようとする課題」にて指摘したように全体動作が一致するとは限らないため、十分条件を満たすか否かチェックし（Ｓ２）、前記十分条件を満たさないモジュール間I/Fを識別し、その情報１６を出力する。
【０１０２】
前記十分条件を満たさないモジュール間I/Fが識別された場合、当該I/Fが前記十分条件を満たすための条件割出しを実施し（Ｓ１４）、当該条件が満たされる事を検証する。ここで、割出し条件の導出は、一般化できる問題ではなく、自動導出は容易ではない。しかし、検証対象の全体回路における十分条件未充足インターフェースの仕様に基づいて、全体回路の等価性を判定する条件を導くことは可能である。例えば、割出した条件をアサーションで記述し、従来システムと同じくRTLシミュレーションを実施しても良いし、前記アサーション記述を対象としたプロパティ検査またはモデル検査を実施しても良い。
【０１０３】
高位等価性検証Ｓ１１で等価と判定された場合、または、モジュール分割後の等価性検証Ｓ３で全てのモジュールのそれぞれが等価と判定され（Ｓ４）、十分条件が満たされた（Ｓ２）とき、全体記述を対象とした高位記述１１とRTL記述１２とが等価であるという検証結果１７を出力して終了する。モジュール毎の高位等価性検証Ｓ３で等価でないモジュールがあるときは、全体として不等価であるという検証結果１７を出力して終了する。
【０１０４】
＜分割条件＞
図４は、モジュール分割における分割条件についての説明図である。
【０１０５】
全体回路の記述を、有向グラフG=(V,E)を用いて表す。ここで、Vは、モジュール（スレッド/プロセス）を頂点とみなした頂点集合、Eは、モジュール間の接続を信号方向込みで有向辺とした有向辺集合である。図４では、「CA」または「¬CA」の属性を付加されたモジュールを丸の頂点Vで表し、モジュール間の信号を矢印の有向辺Eで表す。頂点Vに付加された「CA」はそのモジュールがサイクル精度合成であることを、「¬CA」はそれ以外の合成であることを示している。有向辺Eでは、両端に矢印のある細かい破線がハンドシェーク通信を、一方のみの矢印の粗い破線がレイテンシ非依存通信を、実線の矢印がその他の通信を表している。レイテンシ非依存通信では、Back Pressure（例えば、受信側のモジュールが返信するビジー信号）が存在するため、一般には双方向通信となるが、有向グラフGの構成では、Back Pressureを除いた短方向通信として扱うものとする。有向辺Eの方向に順に頂点Vを辿って元の頂点Vに戻る経路は、有向グラフGに含まれる強連結成分であり、全体回路に含まれる閉路である。ハンドシェーク通信は双方向通信であるため、ハンドシェーク通信し合う２つの頂点は常に閉路内に含まれる。
【０１０６】
モジュール分割後の全体記述の有向グラフGが分割条件を充足するための必要十分条件は、Gが下記を満たすことである。即ち、「Gが閉路を含む ⇒ ｛閉路を構成する任意の頂点にて、その頂点を表すモジュール/スレッド/プロセスに対応する高位記述とRTL記述の入出力動作はサイクル精度で一致。∨ 閉路内の頂点の閉路内での通信が全てハンドシェーク通信または全てレイテンシ非依存通信（Latency Insensitive Protocol）で、閉路内の頂点と直接通信する前記閉路外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信｝」。一方、Gが閉路を含まない場合には、本条件は常に充足される。なお、サイクル精度合成の場合にのみ、「高位記述とRTL記述の入出力動作はサイクル精度で一致する事が互いに等価と成る条件」となる。
【０１０７】
分割条件は、以下の条件のいずれかを満たすことである。
条件「Gが閉路（強連結成分）を含まない」
条件A： Gが閉路を含む∧閉路を構成する任意の頂点にて、その頂点を表すモジュール/スレッド/プロセスに対応する高位記述とRTL記述の入出力動作はサイクル精度で一致する事が、互いに等価と成る条件
条件B： Gが閉路を含む∧閉路内の頂点の閉路内での通信が全てハンドシェーク通信または全てレイテンシ非依存通信（Latency Insensitive Protocol）で、閉路内の頂点と直接通信する前記閉路外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信。
【０１０８】
図４において、(a)は分割条件を満たすGの例である。閉路（強連結成分）を含まないので、分割条件が充足される。(b)は分割条件を満たす別の例である。閉路２３＿１を含み、閉路２３＿１内の全ての頂点V２１＿６、２１＿７、２１＿８が属性「CA」であり、対応する高位記述とRTL記述の入出力動作はサイクル精度で一致する。(c)は分割条件を満たさない例である。(b)と異なり閉路２３＿２内に属性「¬CA」の頂点V２１＿１３を含むからである。(d)に示すGは分割条件を満たす。閉路２３＿３内に属性「¬CA」の頂点V２１＿１８を含むが、閉路２３＿３内の頂点V２１＿１６、２１＿１７、２１＿１８の閉路内での通信が全てハンドシェーク通信であるからである。(e)に示すGも分割条件を満たす。閉路２３＿４内に属性「¬CA」の頂点V２１＿２３を含むが、閉路２３＿４内の頂点V２１＿２１、２１＿２２、２１＿２３の閉路内での通信が全てレイテンシ非依存通信であるからである。(f)に示すGも分割条件を満たす。閉路２３＿５内に属性「¬CA」の頂点V２１＿２８を含むが、閉路２３＿５内の頂点V２１＿２６、２１＿２７、２１＿２８の閉路内での通信が全てハンドシェーク通信またはレイテンシ非依存通信であるからである。
【０１０９】
＜十分条件＞
次に十分条件について説明する。モジュール（スレッド/プロセス）の接続構成の成す有向グラフGが、各強連結成分（閉路）にて上記分割条件を満たす事が前提である。その上で、十分条件は以下の通りである。
【０１１０】
条件C：  Gが閉路（強連結成分）を含まない場合、Gの各頂点が下記性質（サイクル同期性）を充足すること。
【０１１１】
全頂点での各入力・出力信号のスループット/レイテンシ・サイクルを高位記述とRTL記述で比較した場合、一律に変化すること。高位記述で同時に出力（入力）していた信号はRTL記述でも同時に出力（入力）され、且つ高位記述の信号間のサイクル差が、RTL記述では、全て一律に変化している。
【０１１２】
条件D：  全てで条件Aが満たされる場合、Gの各頂点がサイクル同期性を充足すること。
【０１１３】
条件E：  条件Bを満たす強連結成分が存在する場合、下記の何れかを満たすこと。
【０１１４】
全ての強連結成分が条件Bを満たし、強連結成分に含まれない各頂点の通信が全てレイテンシ非依存通信であること。Gをレイテンシ非依存通信を含むサブグラフと一切含まないサブグラフの２つに分割可能で、前者から後者への有向辺が性質Ｃ「入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしない」を満たし、一切含まないサブグラフでは、サイクル同期性が満たされること。
【０１１５】
なお、サイクル同期性のチェックでは、満たさない入力・出力信号群を各頂点毎に検出する。検出箇所に関しては「満たすと仮定」して処理を進める事で、全頂点の処理を実施する。これにより、「サイクル同期性を満たさない」という属性が伝搬することがなく、未充足インターフェースが容易に特定される。
【０１１６】
＜分割条件チェックと十分条件チェックの効果＞
分割条件チェック（Ｓ１）を行うことにより、モジュール（スレッド/プロセス）の構成が、等価性検証を分割して適用する事による高速化に適しているかの判断を、等価性検証を行う前に判定することができる。従って、規模の大きなシステムやモジュールの設計にて等価性検証を適用する場合、システムやモジュールの内部構成の定義を行う設計初期段階で、等価性検証の高速化を見越した設計が可能となる。
【０１１７】
十分条件チェック（Ｓ２）を行うことにより、分割した高位モジュール記述群と検証対象モジュール記述群の対応するモジュール毎の入出力信号がサイクル精度で一致していない場合であっても、全体回路での等価性を判定することができる。
【０１１８】
また、十分条件を満たさない入力・出力信号群を各頂点毎に検出することができる。ここで注意すべきは、上記十分条件が、高位記述とRTL記述が等価であるための十分条件に過ぎない点である。上記十分条件が満たされれば高位記述とRTL記述が等価であることが証明されるが、上記十分条件が満たされなくても等価でないとは限らない。そこで、十分条件を満たさない入力・出力信号群を検出し、全体シミュレーションなどの別の方法で、等価性を判断する。一般化した論理的・数学的な証明が困難であっても、回路や信号個別の仕様に基づいて、一定の境界条件の下では等価として扱って良い（実用的に等価）と判断することは、必ずしも困難ではない。
【０１１９】
十分条件未充足の検出箇所に関しては「満たすと仮定」して処理を進める事で、全頂点の処理を実施する。仮定した箇所に関しては、ユーザ責任でモジュール間I/F保存のために当該箇所が満たすべき条件を割出し、それを検証する事で実際に仮定が満たされることを示す、という保証仮定推論（Assume-Guarantee Reasoning）を採用する。この検証では、割出した条件をアサーションで記述し、従来システムと同じくRTLシミュレーションを実施しても良いし、前記アサーション記述を対象としたプロパティ検査またはモデル検査を実施しても良い。プロパティ検査またはモデル検査を用いた場合、完全一致証明が達成される。
【０１２０】
仮に、割出し条件の導出をユーザが行うとしても、ユーザがアサーション記述を作成すべき箇所が自動で導出されており、適切なアサーション記述作成と検証による全体一致証明が可能となる。
【０１２１】
仮に、作成したアサーション記述の検証を、RTLシミュレーションで行うとしても、以下の効果が得られる。余分なアサーションを作成する可能性が概ね排除されているため、アサーション作成工数が削減される。余分なアサーションが排除されているため、アサーション記述量増大によるシミュレーション速度低下が緩和される。作成したアサーションに対象を絞ったシミュレーション実行が可能であるため、シミュレーション時間の削減も可能となる。
【０１２２】
〔実施形態２〕
分割条件チェックＳ１と、十分条件チェックＳ２及びサイクル同期性チェックについて、さらに詳細な実施形態に説明する。
【０１２３】
＜分割条件チェックＳ１＞
まず、モジュール（スレッド/プロセス）分割後の高位記述から有向グラフGを構成する。次に、RTL回路実装情報を読み込み、G上の頂点に対して、属性「CA」と「¬CA」を付加する。「CA」は、「サイクル精度合成対象部」、または「高位記述とRTL記述の等価性検証ではサイクルレベルでの動作一致を示す事が必要な部分」を表し、「¬CA」でそれ以外である事を表す。
【０１２４】
次に、Gに対して、強連結成分への分割を実施し、各強連結成分に対して下記の何れかを確認すればよい。
【０１２５】
分割条件が充足：条件B∨条件A、条件B＝α∧β、条件A＝γ
α： 強連結成分で、その頂点間の通信が全てハンドシェーク通信か全てレイテンシ非依存通信
β： 強連結成分で、その頂点と前記強連結成分外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信
γ： 強連結成分に「¬CA」を伴う頂点が非存在。
【０１２６】
分割条件未充足：¬条件B∧¬条件A、¬条件B＝¬α∨¬β、¬条件A＝¬γ
¬α： 強連結成分内の頂点間の通信で、ハンドシェーク通信でないか、レイテンシ非依存通信でない通信が存在
¬β： 強連結成分内の頂点と前記強連結成分外の頂点との通信で、レイテンシ非依存通信でない通信が存在
¬γ： 強連結成分に「¬CA」を伴う頂点が存在。
【０１２７】
図５及び図６は、分割条件チェックＳ１の処理の一例を表すフローチャートである。図５は前半、図６は後半であり、端子CONTにより互いに接続される。
【０１２８】
モジュール（スレッド/プロセス）分割後の高位記述から有向グラフG=(V,E)を構成する（Ｓ１_１）。RTL回路実装情報１３を読み込み、G上の頂点Vに対して、スループット・サイクル数及び属性「CA」と「¬CA」を付加する（Ｓ１＿２）。有向グラフGを強連結成分へ分解する（Ｓ１＿３）。Gが強連結成分を含むか否か判定し（Ｓ１＿４）、Gが強連結成分を含まない場合は、判定結果「非巡回グラフ」と「分割条件充足」を出力して（Ｓ１＿７）、終了する。
【０１２９】
Gが強連結成分を含む場合は、Gで各強連結成分を頂点とした有向グラフG'=(V',E')を構成する（Ｓ１＿５）。G'を対象にトポロジカル・ソートを実施し、得られたトポロジカル順序でGの強連結成分に対応する頂点を並べた頂点集合をV'={v1,v2,…vn}とし、i=0とする（Ｓ１＿６）。これは十分条件チェックで用いるため、結果を記憶域に格納すると良い。
【０１３０】
頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次Ｓ１＿９以下のステップを実行するため、i==nの判定を実施し（Ｓ１＿８）、一致した場合、Ｓ１＿９へ、不一致の場合、Ｓ１＿１８へ処理を移行する。
【０１３１】
「∀w∈vi, in(w)とout(w)がハンドシェーク通信」、即ち条件αの一部である「強連結成分viで、その頂点間の通信が全てハンドシェーク通信」、が成立するか否か判定し（Ｓ１＿９）、成立した場合、Ｓ１＿１１へ、不成立の場合、Ｓ１＿１０へ、処理を移行する。ここで、in(w)は頂点wへの入力辺、out(w)は頂点wからの出力辺を取得するメソッドである。
【０１３２】
Ｓ１＿１０では、「∀w∈vi, in(w)とout(w)がレイテンシ非依存通信」、即ち条件αの残りの一部である「強連結成分viで、その頂点間の通信が全てレイテンシ非依存通信」、が成立するか否か判定し、成立した場合、Ｓ１＿１１へ、不成立の場合、Ｓ１＿１３へ、処理を移行する。
【０１３３】
Ｓ１＿１１では、「∃w∈vi, ∃u∈V';Gの非強連結成分, ∃e=(w,u)∈E ∨ ∃e'=(u,w)∈E ⇒ eとe'は（存在するなら）レイテンシ非依存通信またはハンドシェーク通信」、即ち条件β「強連結成分viで、その内部頂点とviの外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信」、が成立するか否か判定する。成立した場合、Ｓ１＿１２で「viが分割条件B充足」を結果出力し、不成立の場合、Ｓ１＿１３で「viが分割条件B未充足」を結果出力し、いずれも処理をＳ１＿１４へ移行する。
【０１３４】
Ｓ１＿１４では、「∃w∈vi s.t. label(w)=="¬CA"」、即ち条件¬γ「強連結成分viに"¬CA"を伴う頂点が存在」、が成立するか否か判定する。不成立の場合「viが分割条件A充足」を結果出力し（Ｓ１＿１５）、成立した場合「viが分割条件A未充足」を結果出力し（Ｓ１＿１６）、いずれもiをインクリメントして（Ｓ１＿１７）次の頂点viの処理に移行する。ここで、label(w)は、頂点wに付加された属性を取得するメソッドである。Ｓ１＿９からここまでの処理を、頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次実行する。
【０１３５】
全ての頂点viに対しての処理を終えた後、「∀ｖi∈V’, 条件A∨条件B」、即ち全強連結成分に対して、条件Aまたは条件Bが成立しているか判定し（Ｓ１＿１８）、成立していれば、「分割条件充足」を結果出力し（Ｓ１＿１９）、不成立なら「分割条件未充足」を結果出力し（Ｓ１＿２０）、いずれも処理を終了する。
【０１３６】
＜十分条件チェックＳ２＞
十分条件チェックＳ２は、分割条件を満たした後に実行されるステップであるから、上記の分割条件が従属されていることが前提となっている。
【０１３７】
強連結成分が存在しないか、全ての強連結成分で分割条件Aが満たされる場合、強連結成分が存在するなら、全ての強連結成分内の頂点は「CA」であるため、強連結成分への入力サイクル・タイミングに変化がなければ、出力サイクル・タイミングは高位記述とRTL記述で一致する事が判る。ここで、「強連結成分が存在しない」場合とは、分割条件のうち、条件「Gが閉路を含まない」を充足する場合であり、「全ての強連結成分で分割条件Aが満たされる場合」とは、条件A＝γ；  γ： 強連結成分に「¬CA」を伴う頂点が非存在の場合である。
【０１３８】
従って、サイクル同期性の判定では、下記を実施すれば良い。
【０１３９】
まず、初期化処理として以下の処理を実施する。全頂点がCAなら全体で等価と判定する。頂点がCAまたは強連結成分のとき、スループット・サイクル数＝１、レイテンシ・サイクル数＝１とする。頂点が¬CAなら、RTL実装情報１３を読込み、スループット・サイクル数とレイテンシ・サイクル数を取得する。RTL実装情報１３にて、全頂点のスループット・サイクル数が一致しない場合、全体では等価でないと判定し、処理を終了する。従って、強連結成分を含む場合、スループット・サイクル数≠１の頂点が存在すると、全体では等価でないと判定し、処理を終了する事となる。
【０１４０】
次に、非巡回グラフGまたは、強連結成分を頂点とした非巡回グラフG’の各頂点に対して、以下の処理を実施する。スループット・サイクル数の整合性判定が完了しているため、以下では、レイテンシ・サイクル数にのみ着目した判定を実施すれば良い。まず当該頂点に至るパス全てを列挙する。全パス上の頂点がCAなら、この頂点までサイクル同期性が満たされると判定する。パスに¬CAが含まれる場合、その頂点での高位記述とRTL記述とのレイテンシ・サイクル数の差を算出し、各パス毎にサイクル差分情報として、差の総和を求める。得られたサイクル差分情報が全パスにて一致するなら、その頂点までサイクル同期性が満たされたと判定し、そうでない場合、一致しない入力を頂点とともに、十分条件未充足I/Fとして情報を格納しておく。十分条件未充足I/Fが空集合なら、全頂点がサイクル同期性を満たすため、全体として一致と判定し、そうでないなら、十分条件未充足I/F情報を出力する。
【０１４１】
一方、分割条件Bを満たす強連結成分が存在する場合の十分条件チェックについて説明する。
【０１４２】
全ての強連結成分が分割条件Bを満たす場合、強連結成分ではない頂点が全てレイテンシ非依存通信を行う場合、全体で等価と判定する。そうではない場合、分割条件Aを満たす強連結成分が存在する場合の判定処理を実施する。
【０１４３】
分割条件Aを満たす強連結成分が存在する場合、以下の処理を実施する。Gをレイテンシ非依存通信を含むサブグラフと一切含まないサブグラフの２つに分割可能か判定する。分割可能な場合、前者から後者への有向辺が性質Ｃ「入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしない」を満たすか判定する。存在する場合、レイテンシ非依存通信を一切含まないサブグラフにてサイクル同期性が満たされるか判定する。この判定は、前記サブグラフに対して、強連結成分が存在しないか、全ての強連結成分で分割条件Aが満たされる場合に実施されるサイクル同期性判定処理にて実施する。全ての判定で真なら、全体として等価であり、そうでないなら不等価となる。
【０１４４】
図７は、十分条件チェックＳ２の処理の一例を表すフローチャートである。
【０１４５】
分割条件チェックＳ１の処理結果を読込み、モジュールを頂点としモジュール間接続を辺とした有向グラフGが非巡回グラフか否か判定し（Ｓ２_１）、非巡回グラフならＳ２＿１３へ、そうでないならＳ２＿２へ、処理を移行する。
【０１４６】
Ｓ２＿２では、強連結成分への分解を実施して得られた有向グラフG'=(V,E)を対象にトポロジカル・ソートを実施し、得られたトポロジカル順序でGの強連結成分に対応する頂点をV'={v1,v2,…vn}として、Ｓ１＿６で格納した有向グラフG'を読込む。
【０１４７】
Ｓ２＿３で、「∀v∈V’, 条件B充足」、即ちG'上のGでの強連結成分が全て条件Bを満たすか否か判定し、満たすならＳ２＿４へ、満たさないならＳ２＿５へ、処理を移行する。Ｓ２＿４で、「∀v∈V-V', in(v)とout(v)がレイテンシ非依存通信」、即ち強連結成分に含まれない全頂点の通信がレイテンシ非依存通信またはハンドシェーク通信か否か判定し、そうなら「全体として等価」を出力して（Ｓ２＿６）処理を終了し、そうでないならＳ２＿５へ、処理を移行する。Ｓ２＿５では、「∀v∈V', 条件A充足」、即ちG'上のGでの強連結成分が全て条件Aを満たすか否か判定し、満たすならＳ２＿７へ、満たさないならＳ２＿８へ、処理を移行する。Ｓ２＿７では、G=G'なる代入を実施し、サイクル同期性チェック（Ｓ２＿１３）へ移行する。
【０１４８】
Ｓ２＿８で、G'はレイテンシ非依存通信を含むサブグラフと一切含まないサブグラフの２つに分割可能か否か判定し、分割不可能なら「全体として不等価」を出力して（Ｓ２＿１０）処理を終了し、可能ならＳ２＿９へ処理を移行する。Ｓ２＿９では、レイテンシ非依存通信を含むサブグラフから一切含まないサブグラフへの有向辺が性質Ｃ「入力信号待ち要求信号も出力信号待ち要求信号も何れの信号もアサートしない」を満たすか否か判定し、存在しないなら「全体として不等価」を出力して（Ｓ２＿１０）処理を終了し、存在するならＳ２＿１１へ処理を移行する。Ｓ２＿１１では、レイテンシ非依存通信を一切含まないサブグラフが条件Aを満たすか否か判定し、満たさないなら「全体として不等価」を出力して（Ｓ２＿１０）処理を終了し、満たすならＳ２＿１２へ、処理を移行する。
【０１４９】
Ｓ２＿１２では、レイテンシ非依存通信を一切含まないサブグラフをGとし、有向グラフGを引数とし、十分条件未充足I/Fを戻り値とする、定義済み処理「サイクル同期性チェック」を呼出す（Ｓ２＿１３）。Ｓ２＿１４で、定義済み処理「サイクル同期性チェック」の戻り値である十分条件未充足I/Fが空集合か否か判定し、空なら「全体として等価」を出力して（Ｓ２＿６）処理を終了する。空でないなら「十分条件未充足I/Fを無視した場合、全体として等価」を出力（Ｓ２＿１５）し、さらに、十分条件未充足I/F１６を出力して、処理を終了する。
【０１５０】
図８は、サイクル同期性チェックＳ２＿１３の処理の詳細な一例を表すフローチャートである。
【０１５１】
有向グラフG=(V,E)にて、強連結成分への分解時に、強連結成分に対応していた頂点をV'={v1,v2,…vn}とし、これらの頂点のラベルを「CA」とする（Ｓ２＿１３＿１）。Gに対して、新たに頂点v0を加え、Gの入力頂点への有項辺を加えた有向グラフを改めてGとする（Ｓ２＿１３＿２）。「∀v∈V-V', label(v)==“CA”」、即ち強連結成分と対応しない頂点が全て属性「CA」を持つか否か判定し（Ｓ２＿１３＿３）、持つなら「全体として等価」を出力して（Ｓ２＿１３＿７）処理を終了し、持たないならＳ２＿１３＿４へ、処理を移行する。ここで、label(v)は、頂点vに付加された属性を取得するメソッドである。
【０１５２】
Ｓ２＿１３＿４では、「∀v∈V;label(v)==“CA”, lat(v)=th(v)=1」、即ち属性「CA」を伴う頂点のレイテンシ・サイクル数を１とし、スループット・サイクル数を１とする。ここで、lat(v)とth(v)は、それぞれ頂点vのレイテンシ・サイクル数とスループット・サイクル数を表す。
【０１５３】
Ｓ２＿１３＿５では、モジュール実装情報１３を読込み、「∀v∈V;label(v)==“¬CA”, lat(v)とth(v)の値を設定」、即ち属性「¬CA」を伴う頂点に対して、モジュール実装情報記載のレイテンシ・サイクル数とスループット・サイクル数を設定する。
【０１５４】
Ｓ２＿１３＿６で、「∀v,w∈V;v≠w, th(v)==th(w)」、即ち全ての頂点でスループット・サイクル数が一致するか否か判定し、一致しないなら「全体として不等価」を出力して（Ｓ２＿１３＿８）処理を終了し、一致するならＳ２＿１３＿９へ処理を移行する。
【０１５５】
Ｓ２＿１３＿９で、Vo=Vとする。Ｓ２＿１３＿１０で、入力頂点v0と異なる頂点v∈Voを一つ取得し、頂点集合Voから{v)を除去する。Ｓ２＿１３＿１１で、Vo=={v0}か否か判定し、一致するなら十分条件未充足インターフェース情報１６をファイル出力して（Ｓ２＿１３＿１８）処理を終了し、一致しないならＳ２＿１３＿１２へ、処理を移行する。
【０１５６】
Ｓ２＿１３＿１２で、v0からvに至るパス集合Pを取得する。Ｓ２＿１３＿１３で、「∀p∈P, ∀v∈p, lavel(v)==“CA”」、即ちパス集合P内のパス上の任意の頂点が属性「CA」を持つか否か判定し、持つならＳ２＿１３＿１６へ、持たないならＳ２＿１３＿１４へ、処理を移行する。
【０１５７】
Ｓ２＿１３＿１４では、モジュール実装情報を読込み、∀p∈Pに対して、label(p)==“¬CA”なる全てのv∈pで、高位記述とRTL記述とのレイテンシ・サイクル数の差を求め、差の総和sum_diff(p)を算出する。ここで、vの先行頂点の全入力までのパス上の頂点のレイテンシ・サイクル差は０であると仮定して算出するものとする。特に、前記先行頂点の全入力へのデータ到達サイクルが変化している場合は、その一律の変化差分サイクル分だけ、前記先行頂点の出力サイクルがずれるとして扱うものとする。Ｓ２＿１３＿１５で、「∀p,q∈P;p≠q, sum_diff(p)==sum_diff(q)」、即ちパス集合P内のパスが高位記述からRTL記述への実装で一律にサイクル変化しているか否かを判定し、そうならＳ２＿１３＿１６へ、そうでないならＳ２＿１３＿１７へ、処理を移行する。Ｓ２＿１３＿１６では、頂点vでサイクル同期性が充足されている事を、十分条件未充足I/F１６へ格納し、処理をＳ２＿１３＿１０へ戻す。Ｓ２＿１３＿１７で、最も一致した頂点vへの入力パス群を除いて、それ以外のパス上の頂点vへの入力辺を頂点vとともに、十分条件未充足I/F１６へ格納し、処理をＳ２＿１３＿１０へ戻す。
【０１５８】
図９から図１５を使って、サイクル同期性チェックの手法の一例について例題を使って説明する。
【０１５９】
図９は、サイクル同期性チェック例のモジュール構成を例示する説明図である。複数のモジュールａ〜ｇからなるシステムである。制御信号はモジュール間で単方向の通信である。vsは外部入力フレーム開始信号で、内部信号パラメータ設定のトリガ信号である。veは外部入力フレーム・イネーブル信号で、内部動作ストール制御信号である。onは内部モジュール制御信号である。データ信号data, data0, data1,…data4はモジュール間で単方向の通信である。フィードバック制御はないものとする。即ち、強連結成分（閉ループ）はない。
【０１６０】
図１０は高位記述での各モジュールの実行サイクル数を、図１１は合成結果ＲＴＬでの各モジュールの実行サイクル数を、それぞれ例示する説明図である。図１２は高位記述での各モジュールの実行サイクル数を、図１３はＲＴＬ回路実装情報を、それぞれ例示する表である。
【０１６１】
まず、以下の前提条件を確認する。
【０１６２】
前提条件１：  モジュール分割実施済みであり、各モジュールでの等価性検証は現実的な時間で完了する。本例題では満たしているとする。このとき、各モジュールが高位記述とRTL記述双方で、仕様として与えた入出力プロトコルも満たす事が同時に証明される。
【０１６３】
前提条件２：  複数のモジュールを含む閉路を一切含まない。これは、図９に示した例題の構成から明らかである。
【０１６４】
前提条件３：  全モジュールが一部の信号を除いてサイクル同期性を満たす。前提条件１と前提条件２を用いて、サイクル同期している信号群を識別し、それ以外と分離する。
【０１６５】
Ｓ２＿１３とは見かけ上、手順が異なるように見えるが、本例では、頂点毎での処理にて過去に得た情報の再利用を行う事で高速化した手法を用いている。この高速化は、論理式の充足可能性判定での再帰学習など、専門家にとっては一般的な高速化手法であるため、詳細は割愛する。
【０１６６】
次に、サイクル同期性を満たす信号群の識別を行う。示すべき性質は、合成前に同時に出力（入力）していた信号は合成後でも同時に出力（入力）され、且つ、合成前の信号間のサイクル差が、合成後では、全て一律に変化している事である。特に、複数のモジュールからの入力を持つモジュールで上記性質を確認する。また、サイクル同期性を満たさない信号に関しては、モジュール間I/Fの性質を保存すると仮定して扱う。
【０１６７】
まず、図１０と図１１に示したモジュールaに着目する。高位記述ではサイクル数＝１のサイクル精度モデルであり（図１２）、RTL記述では組合せ回路と出力FF（フリップフロップ）で記述されており、サイクル数＝１である（図１３）。高位記述とRTLがサイクルレベルで等価であるため、サイクル同期性を満たす事は明らかである。
【０１６８】
モジュールcに着目する。これもモジュールaと同様に、高位記述ではサイクル数＝１のサイクル精度モデルであり（図１２）、RTL記述では組合せ回路と出力FFで記述されており、サイクル数＝１である（図１３）。高位記述とRTLがサイクルレベルで等価であるため、サイクル同期性を満たす事は明らかである。
【０１６９】
モジュールbに着目する。高位記述ではスループット＝１／レイテンシ＝２のシフトレジスタであり（図１２）、RTL記述では、サイクル数＝１＋スループット＝１／レイテンシ＝６のシフトレジスタで実装されている（図１３）。モジュールaにて全出力がサイクル同期性を満たし、出力も一律にレイテンシ・サイクルが引き伸ばされた構成となっているため、サイクル同期性を満たす。
【０１７０】
モジュールdとモジュールeに着目する。いずれも高位記述ではサイクル数＝１のサイクル精度モデルであり（図１２）、RTL記述ではスループット＝１／レイテンシ＝６のパイプラインで実装されている（図１３）。モジュールaとモジュールcにて全出力がサイクル一致しており、出力も一律にレイテンシ・サイクルが引き伸ばされた構成となっているため、サイクル同期性を満たす。
【０１７１】
モジュールfに着目する。高位記述ではサイクル数＝１のサイクル精度モデルであり（図１２）、RTL記述では組合せ回路と出力FFで記述されており、サイクル数＝１である（図１３）。モジュールb、モジュールd及びモジュールeにて全出力が一律に引き伸ばされており、サイクル精度合成であるため、入力on信号の影響を除いてサイクル同期性を満たす。入力on信号は、モジュールaからレイテンシ１で出力されているので、他の信号と間でサイクル同期性がない。これを十分条件未充足インターフェース１６として一旦格納しておき、後に出力する。
【０１７２】
最後にモジュールｇに着目する。高位記述ではサイクル数＝１のサイクル精度モデルであり（図１２）、RTL記述ではスループット＝１／レイテンシ＝３のパイプラインで実装されている（図１３）。モジュールfにて全出力が入力on信号の影響を除いてサイクル同期性を満たしており、出力も一律にレイテンシ・サイクルが引き伸ばされた構成となっているため、入力on信号の影響を除いてサイクル同期性を満たす。
【０１７３】
＜サイクル同期性を満たさない信号（十分条件未充足インターフェース）の扱い＞
参考までに、サイクル同期性を満たさないon信号の扱いについて説明する。on信号はサイクル同期性を満たさないので、十分条件未充足インターフェース１６として出力される。そこで、モジュール間I/Fの性質を保存する条件を割出す。他の信号とのサイクルズレが発生しているため、そのサイクル数を算出する。本例題の場合、「on信号変化後、常に算出したサイクル期間以上on信号が不変」が条件となる。
【０１７４】
図１４は、サイクル同期性チェック例のモジュール間のインターフェースにおける信号授受のサイクルずれの算出例を表す表である。モジュールａからモジュールｆの経路、及び、モジュールａからモジュールｇの経路での信号授受のサイクルずれが算出されている。モジュールａからモジュールｆの経路では、高位記述であるSystemCでon信号の到達サイクル数を０としたとき、他の信号の到達サイクル数は２サイクルであるのに対し、RTL記述では７サイクルであるため、サイクルずれは５サイクルである。モジュールａからモジュールｇの経路では、SystemCでon信号の到達サイクル数を０としたとき、他の信号の到達サイクル数は３サイクルであるのに対し、RTL記述では８サイクルであるため、サイクルずれは５サイクルである。よって、「on信号変化後、常に５サイクル期間以上on信号が不変」が示すべき条件となる。
【０１７５】
入出力信号プロトコルを用いた、条件の簡約化について説明する。図１５は、モジュール間のインターフェースにおけるサイクル同期性を満たさない信号の扱いについて説明するためのタイミングチャートである。モジュールaにてon信号がどのように生成され、モジュールf、モジュールgにてどのように取り込まれているかに着目する。モジュールaはvs信号の立上りでon信号を変化させ、モジュールf、モジュールgはve=1の期間にon信号を取り込むものとする。
【０１７６】
上記からモジュール間I/Fの性質を保存する条件は下記に簡約化される。
モジュールf：「vsの立上りから、常に5サイクル期間以上ve2==0」。
モジュールg：「vsの立上りから、常に5サイクル期間以上ve3==0」。
【０１７７】
本例題の場合、入力信号vs,veが、「vsの立上りから、常に80サイクル期間以上ve=0」を満たすため、veからve2,ve3への信号伝播サイクルを考慮しても、上記２つの性質が満たされる事が分かる。よって、上記の入出力信号プロトコルを用いた条件の簡約化により、アサーション検証が不要であることがわかる。
【０１７８】
以上のように、前述の十分条件を満たさないインターフェースについて、一般化により全体回路の等価性を論理的または数学的に証明することは困難であっても、その情報を出力しておくことにより、別の方法で比較的容易に実用的に十分な等価性の検証を行うことができる。
【０１７９】
〔実施形態３〕
実施形態２では、仮に強連結成分内の全頂点が同一スループット・サイクルである場合であっても、分割条件を満たさない場合や、十分条件を満たさない場合があり、全体として不等価と判定される場合がある。これを緩和する目的で、分割条件の条件A（即ちγ）を下記γ'に変更する。
【０１８０】
分割条件が充足：条件B∨条件A、条件B＝α∧β、条件A＝γ'
α： 強連結成分で、その頂点間の通信が全てハンドシェーク通信か全てレイテンシ非依存通信
β： 強連結成分で、その頂点と前記強連結成分外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信
γ'： 強連結成分内の全ての頂点が同一スループット・サイクル数を伴う。
【０１８１】
分割条件未充足：¬条件B∧¬条件A、¬条件B＝¬α∨¬β、¬条件A＝¬γ'
¬α： 強連結成分内の頂点間の通信で、ハンドシェーク通信でないか、レイテンシ非依存通信でない通信が存在
¬β： 強連結成分内の頂点と前記強連結成分外の頂点との通信で、レイテンシ非依存通信でなくハンドシェーク通信でもない通信が存在
¬γ'： 強連結成分に、他の頂点と異なるスループット・サイクル数を伴う頂点が存在。
【０１８２】
変更の仕方から、分割条件チェックのみ修正すれば、十分条件チェックＳ２は実施形態２と全く同一のものを利用できる。図１６と図１７は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（図１６は前半、図１７は後半）である。
【０１８３】
モジュール（スレッド/プロセス）分割後の高位記述から有向グラフG=(V,E)を構成する（Ｓ１'_１）。RTL回路実装情報１３を読み込み、G上の頂点Vに対して、スループット・サイクル数を付加する（Ｓ１'＿２）。有向グラフGを強連結成分へ分解する（Ｓ１'＿３）。Gが強連結成分を含むか否か判定し（Ｓ１'＿４）、Gが強連結成分を含まない場合は、判定結果「非巡回グラフ」と「分割条件充足」を出力して（Ｓ１'＿７）、終了する。
【０１８４】
Gが強連結成分を含む場合は、Gで各強連結成分を頂点とした有向グラフG'=(V',E')を構成する（Ｓ１'＿５）。G'を対象にトポロジカル・ソートを実施し、得られたトポロジカル順序でGの強連結成分に対応する頂点を並べた頂点集合をV'={v1,v2,…vn}とし、i=0とする（Ｓ１'＿６）。これは十分条件チェックで用いるため、結果を記憶域に格納すると良い。
【０１８５】
頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次Ｓ１'＿９以下のステップを実行するため、i==nの判定を実施し（Ｓ１'＿８）、一致した場合、Ｓ１'＿９へ、不一致の場合、Ｓ１'＿１８へ処理を移行する。
【０１８６】
「∀w∈vi, in(w)とout(w)がハンドシェーク通信」、即ち条件αの一部である「強連結成分viで、その頂点間の通信が全てハンドシェーク通信」、が成立するか否か判定し（Ｓ１'＿９）、成立した場合、Ｓ１'＿１１へ、不成立の場合、Ｓ１'＿１０へ、処理を移行する。ここで、in(w)は頂点wへの入力辺、out(w)は頂点wからの出力辺を取得するメソッドである。
【０１８７】
Ｓ１'＿１０では、「∀w∈vi, in(w)とout(w)がレイテンシ非依存通信」、即ち条件αの残りの一部である「強連結成分viで、その頂点間の通信が全てレイテンシ非依存通信」、が成立するか否か判定し、成立した場合、Ｓ１'＿１１へ、不成立の場合、Ｓ１'＿１３へ、処理を移行する。
【０１８８】
Ｓ１'＿１１では、「∃w∈vi, ∃u∈V';Gの非強連結成分, ∃e=(w,u)∈E ∨ ∃e'=(u,w)∈E ⇒ eとe'は（存在するなら）レイテンシ非依存通信またはハンドシェーク通信」、即ち条件β「強連結成分viで、その内部頂点とviの外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信」、が成立するか否か判定する。成立した場合、Ｓ１'＿１２で「viが分割条件B充足」を結果出力し、不成立の場合、Ｓ１'＿１３で「viが分割条件B未充足」を結果出力し、いずれも処理をＳ１'＿１４へ移行する。
【０１８９】
Ｓ１'＿１４では、「∃w∈vi s.t. wのスループット・サイクル数が他と異なる」、即ち条件¬γ'「強連結成分に、他の頂点と異なるスループット・サイクル数を伴う頂点が存在」、が成立するか否か判定する。成立した場合、「viが分割条件A充足」を結果出力し（Ｓ１'＿１５）、不成立の場合、「viが分割条件A未充足」を結果出力し（Ｓ１'＿１６）、iをインクリメントして（Ｓ１'＿１７）次の頂点viの処理に移行する。ここで、label(w)は、頂点wに付加された属性を取得するメソッドである。Ｓ１'＿９からここまでの処理を、頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次実行する。
【０１９０】
全ての頂点viに対しての処理を終えた後、「∀ｖi∈V’, 条件A∨条件B」、即ち全強連結成分に対して、条件Aまたは条件Bが成立しているか判定し（Ｓ１'＿１８）、成立していれば、「分割条件充足」を結果出力し（Ｓ１'＿１９）、不成立なら「分割条件未充足」を結果出力し（Ｓ１'＿２０）、いずれも処理を終了する。
【０１９１】
これにより、実施形態２では、仮に強連結成分内の全頂点が同一スループット・サイクルである場合であっても、分割条件を満たさない場合や、十分条件を満たさない場合があり、全体として不等価と判定される場合があるが、これが緩和される。
【０１９２】
〔実施形態４〕
実施形態２、および実施形態３では、仮に強連結成分をモジュールとして扱い、高位記述とRTL記述で等価性が示せたとしても、分割条件を満たさないという理由で、全体として不等価であると判定する場合がある。これを緩和する目的で、分割条件の条件Aを下記のように変更する。
【０１９３】
分割条件が充足：条件B∨条件A、条件B＝α∧β、条件A＝γ''∨γ'∨γ
α： 強連結成分で、その頂点間の通信が全てハンドシェーク通信か全てレイテンシ非依存通信
β： 強連結成分で、その頂点と前記強連結成分外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信
γ''： 強連結成分がモジュール定義されており、当該モジュールに対するRTL回路実装情報が定義されている、即ち、高位記述からRTL記述の実装で、各入力・出力信号のスループット/レイテンシ・サイクル数が一律に変化している事が予め保証されている。
【０１９４】
分割条件未充足：¬条件B∧¬条件A
¬α： 強連結成分内の頂点間の通信で、ハンドシェーク通信でないか、レイテンシ非依存通信でない通信が存在
¬β： 強連結成分内の頂点と前記強連結成分外の頂点との通信で、レイテンシ非依存通信でなくハンドシェーク通信でもない通信が存在
¬γ''：強連結成分がモジュール定義されており、当該モジュールに対するRTL回路実装情報が未定義、即ち、高位記述からRTL記述の実装で、各入力・出力信号のスループット/レイテンシ・サイクル数が一律に変化している事が予め保証されていない。
【０１９５】
図１８と図１９は、緩和された分割条件チェックＳ１の処理の一例を表すフローチャート（図１８は前半、図１９は後半）である。
【０１９６】
モジュール（スレッド/プロセス）分割後の高位記述から有向グラフG=(V,E)を構成する（Ｓ１'_１）。RTL回路実装情報１３を読み込み、G上の頂点Vに対して、スループット・サイクル数及び属性「CA」と「¬CA」を付加する（Ｓ１'＿２＿１）。有向グラフGを強連結成分へ分解する（Ｓ１'＿３）。Gが強連結成分を含むか否か判定し（Ｓ１'＿４）、Gが強連結成分を含まない場合は、判定結果「非巡回グラフ」と「分割条件充足」を出力して（Ｓ１'＿７）、終了する。
【０１９７】
Gが強連結成分を含む場合は、Gで各強連結成分を頂点とした有向グラフG'=(V',E')を構成する（Ｓ１'＿５）。G’を対象にトポロジカル・ソートを実施し、得られたトポロジカル順序でGの強連結成分に対応する頂点から、予めRTL回路実装情報が与えられている頂点を除いて（十分条件チェックでも除外するものとする）、並べた頂点集合をV’={v1,v2,…vn}とし、i=0とする（Ｓ１'＿６＿１）。これは十分条件チェックで用いるため、結果を記憶域に格納すると良い。
【０１９８】
頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次Ｓ１'＿９以下のステップを実行するため、i==nの判定を実施し（Ｓ１'＿８）、一致した場合、Ｓ１'＿９へ、不一致の場合、Ｓ１'＿１８へ処理を移行する。
【０１９９】
「∀w∈vi, in(w)とout(w)がハンドシェーク通信」、即ち条件αの一部である「強連結成分viで、その頂点間の通信が全てハンドシェーク通信」、が成立するか否か判定し（Ｓ１'＿９）、成立した場合、Ｓ１'＿１１へ、不成立の場合、Ｓ１'＿１０へ、処理を移行する。ここで、in(w)は頂点wへの入力辺、out(w)は頂点wからの出力辺を取得するメソッドである。
【０２００】
Ｓ１'＿１０では、「∀w∈vi, in(w)とout(w)がレイテンシ非依存通信」、即ち条件αの残りの一部である「強連結成分viで、その頂点間の通信が全てレイテンシ非依存通信」、が成立するか否か判定し、成立した場合、Ｓ１'＿１１へ、不成立の場合、Ｓ１'＿１３へ、処理を移行する。
【０２０１】
Ｓ１'＿１１では、「∃w∈vi, ∃u∈V';Gの非強連結成分, ∃e=(w,u)∈E ∨ ∃e'=(u,w)∈E ⇒ eとe'は（存在するなら）レイテンシ非依存通信またはハンドシェーク通信」、即ち条件β「強連結成分viで、その内部頂点とviの外の頂点との通信がレイテンシ非依存通信またはハンドシェーク通信」、が成立するか否か判定する。成立した場合、Ｓ１'＿１２で「viが分割条件B充足」を結果出力し、不成立の場合、Ｓ１'＿１３で「viが分割条件B未充足」を結果出力し、いずれも処理をＳ１'＿１４＿１へ移行する。
【０２０２】
Ｓ１'＿１４＿１では、「∃w∈vi s.t. label(w)==“¬CA”」、即ち条件¬γ「強連結成分viに“¬CA”を伴う頂点が存在」、が成立するか否か判定する。成立した場合、Ｓ１'＿１５へ、不成立の場合、Ｓ１'＿１４＿２へ、処理を移行する。ここで、label(w)は、頂点wに付加された属性を取得するメソッドである。
Ｓ１'＿１４＿２で、「∃w∈vi s.t. wのスループット・サイクル数が他と異なる」、即ち条件¬γ'「強連結成分に、他の頂点と異なるスループット・サイクル数を伴う頂点が存在」、が成立するか否か判定する。成立した場合、「viが分割条件A充足」を結果出力し（Ｓ１'＿１５）、不成立の場合、「viが分割条件A未充足」を結果出力し（Ｓ１'＿１６）、iをインクリメントして（Ｓ１'＿１７）次の頂点viの処理に移行する。ここで、label(w)は、頂点wに付加された属性を取得するメソッドである。Ｓ１'＿９からここまでの処理を、頂点集合V'={v1,v2,…vn}に属する全ての頂点viに対して順次実行する。
【０２０３】
全ての頂点viに対しての処理を終えた後、「∀vi∈V’, 条件A∨条件B」、即ち全強連結成分に対して、条件Aまたは条件Bが成立しているか判定し（Ｓ１'＿１８）、成立していれば、「分割条件充足」を結果出力し（Ｓ１'＿１９）、不成立なら「分割条件未充足」を結果出力し（Ｓ１'＿２０）、いずれも処理を終了する。
【０２０４】
これにより、実施形態２、および実施形態３では、仮に強連結成分をモジュールとして扱い、高位記述とRTL記述で等価性が示せたとしても、分割条件を満たさないという理由で、全体として不等価であると判定する場合があるが、これが緩和される。
【０２０５】
以上本発明者によってなされた発明を実施形態に基づいて具体的に説明したが、本発明はそれに限定されるものではなく、その要旨を逸脱しない範囲において種々変更可能であることは言うまでもない。
【０２０６】
例えば、電子計算機上のソフトウェアによって検証する等価性検証システムとして実施形態を開示したが、電子計算機は、大型のスーパーコンピュータから、エンジニアリング・ワークステーション、パーソナル・コンピュータなど、如何なる電子計算機にも適用できる。また、ソフトウェアは、独立して動作するアプリケーション・ソフトウェアであっても、さらに大きな設計ツールの中にサブプログラムなどとして組み込まれた１機能であっても良い。
【符号の説明】
【０２０７】
１１  高位言語で記述された全体記述
１２  RTL記述された全体記述
１３  RTL回路実装情報
１４  高位言語で記述されたモジュール記述群
１５  RTL記述されたモジュール記述群
１６  十分条件未充足のインターフェース情報
１７  検証結果
１８  高位記述用テストベンチ
１９  RTL記述用テストベンチ
２０  有向グラフG
２１  頂点V（モジュール）
２２  有向辺E（モジュール間の接続）
２３  強連結成分（閉ループ）
Ｓ１  分割条件を満たすモジュール分割
Ｓ２  十分条件チェック
Ｓ３  モジュール毎に処理する高位等価性検証
Ｓ４  モジュール毎に処理した高位等価性検証の結果の判定
Ｓ１１  全体回路を対象に一括処理する高位等価性検証
Ｓ１２  高位等価性検証の全体一括処理（Ｓ１１）が現実的な時間で実行可能かの判断
Ｓ２１  モジュール分割（従来）
Ｓ２２  モジュール毎に処理する高位等価性検証（従来）
Ｓ２３  モジュール毎に処理した高位等価性検証の結果の判定（従来）
Ｓ２４  RTL検証向けのテストベンチ修正
Ｓ２５  RTLシミュレーション
【図１】
2014081803.tif 000003
【図２】
2014081803.tif 000004
【図３】
2014081803.tif 000005
【図４】
2014081803.tif 000006
【図５】
2014081803.tif 000007
【図６】
2014081803.tif 000008
【図７】
2014081803.tif 000009
【図８】
2014081803.tif 000010
【図９】
2014081803.tif 000011
【図１０】
2014081803.tif 000012
【図１１】
2014081803.tif 000013
【図１２】
2014081803.tif 000014
【図１３】
2014081803.tif 000015
【図１４】
2014081803.tif 000016
【図１５】
2014081803.tif 000017
【図１６】
2014081803.tif 000018
【図１７】
2014081803.tif 000019
【図１８】
2014081803.tif 000020
【図１９】
2014081803.tif 000021