(57)【要約】【課題】所定の言語が用いられた記述についての設計変更前後の等価性を効率よく検証できる設計検証装置を提供する。【解決手段】所定の言語で記述された第１の記述と、部分的に第１の記述と異なる第２の記述とを比較し、第２の記述と異なる第１の記述の部分である第１の差分記述及び第２の差分記述、並びに第１の記述と異なる第２の記述の部分である第３の差分記述を抽出する差分抽出手段と、第１の記述から第１の差分記述及び第２の差分記述に影響を与える第１の依存関係記述を抽出する依存関係抽出手段と、第１の差分記述、第２の差分記述、及び第１の依存関係記述を含む第１の比較記述、並びに第３の差分記述を含む第２の比較記述を生成する比較記述生成手段と、第１の比較記述と第２の比較記述との等価性を検証する等価性検証手段と、を備える。【選択図】  図１
2014120119.tif 000002
【特許請求の範囲】
【請求項１】
所定の言語で記述された第１の記述と、部分的に前記第１の記述と異なる第２の記述とを比較し、前記第２の記述と異なる前記第１の記述の部分である第１の差分記述及び第２の差分記述、並びに前記第１の記述と異なる前記第２の記述の部分である第３の差分記述を抽出する差分抽出手段と、
前記第１の記述から前記第１の差分記述及び前記第２の差分記述に影響を与える第１の依存関係記述を抽出する依存関係抽出手段と、
前記第１の差分記述、前記第２の差分記述、及び前記第１の依存関係記述を含む第１の比較記述、並びに前記第３の差分記述を含む第２の比較記述を生成する比較記述生成手段と、
前記第１の比較記述と前記第２の比較記述との等価性を検証する等価性検証手段と、
を備えたことを特徴とする設計検証装置。
【請求項２】
前記第１の差分記述及び前記第２の差分記述は、前記第１の記述中の、連続した部分的記述であり、
前記第３の差分記述は、前記第２の記述中の、連続した部分的記述である
ことを特徴とする請求項１に記載の設計検証装置。
【請求項３】
前記依存関係抽出手段は、
前記第１の差分記述にて代入される変数、及び前記第１の差分記述に後置される前記第２の差分記述にて参照される変数の両方に影響を与える文からなる部分記述を前記第１の依存関係記述として抽出する
ことを特徴とする請求項１又は２に記載の設計検証装置。
【請求項４】
前記差分抽出手段は、前記第１の記述と異なる前記第２の記述の部分である第４の差分記述を抽出し、
前記依存関係抽出手段は、前記第２の記述から前記第３の差分記述及び前記第４の差分記述に影響を与える第２の依存関係記述を抽出し、
前記比較記述生成手段は、前記第４の差分記述及び前記第２の依存関係記述を含む前記第２の比較記述を生成する
ことを特徴とする請求項１乃至３のいずれか１項に記載の設計検証装置。
【請求項５】
前記第１の差分記述と前記第２の差分記述との間の前記第１の記述と、前記第３の差分記述と前記第４の差分記述との間の前記第２の記述は、同一の記述である
ことを特徴とする請求項４に記載の設計検証装置。
【請求項６】
前記言語は、処理の手順を順次指定する言語である
ことを特徴とする請求項１乃至５のいずれか１項に記載の設計検証装置。
【請求項７】
前記言語は、ハードウェアの動作記述用言語若しくはＲＴＬ記述用言語、又はコンピュータのプログラム記述用言語である
ことを特徴とする請求項６に記載の設計検証装置。
【請求項８】
所定の言語で記述された第１の記述と、部分的に前記第１の記述と異なる第２の記述とを比較し、
前記第２の記述と異なる前記第１の記述の部分である第１の差分記述及び第２の差分記述、並びに前記第１の記述と異なる前記第２の記述の部分である第３の差分記述を抽出し、
前記第１の記述から前記第１の差分記述及び前記第２の差分記述に影響を与える第１の依存関係記述を抽出し、
前記第１の差分記述、前記第２の差分記述、及び前記第１の依存関係記述を含む第１の比較記述、並びに前記第３の差分記述を含む第２の比較記述を生成し、
前記第１の比較記述と前記第２の比較記述との等価性を検証する
ことを特徴とする設計検証方法。
【請求項９】
所定の言語で記述された複数の記述に所定の処理を行う記述処理システムが備えるコンピュータを、
前記言語で記述された第１の記述と、部分的に前記第１の記述と異なる第２の記述とを比較し、前記第２の記述と異なる前記第１の記述の部分である第１の差分記述及び第２の差分記述、並びに前記第１の記述と異なる前記第２の記述の部分である第３の差分記述を抽出する差分抽出手段と、
前記第１の記述から前記第１の差分記述及び前記第２の差分記述に影響を与える第１の依存関係記述を抽出する依存関係抽出手段と、
前記第１の差分記述、前記第２の差分記述、及び前記第１の依存関係記述を含む第１の比較記述、並びに前記第３の差分記述を含む第２の比較記述を生成する比較記述生成手段と、
前記第１の比較記述と前記第２の比較記述との等価性を検証する等価性検証手段と、
として機能させることを特徴とする設計検証用プログラム。
【請求項１０】
請求項９に記載の設計検証用プログラムと、
前記第１の記述又は前記第２の記述を、前記言語とは異なる言語又は所定の規則に従った第３の記述に変換する変換手段として、前記コンピュータを機能させるための記述変換プログラムを含む
ことを特徴とする記述変換用プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、設計検証システム、設計検証方法及び設計検証用プログラムに関し、特に、設計変更前後の等価性を検証できる設計検証システム、設計検証方法及び設計検証用プログラムに関する。
【背景技術】
【０００２】
近年、複雑なアルゴリズムを実現する半導体回路の設計の重要性が増している。画像処理、認識処理などの処理アルゴリズムでは、扱うデータ量が増え、かつ、リアルタイム処理への要求も大きくなってきている。そのため、汎用プロセッサ単体での処理では要求を満たせなくなってきており、これらのアルゴリズムを実現する半導体回路を専用回路として設計しなければならない。
【０００３】
複雑なアルゴリズムを実現する半導体回路の設計は、概略、以下のように行われる。
【０００４】
まず、設計者は、半導体回路として実現するために好適な処理手順を求めるための「アルゴリズム設計」を行う。一般に、アルゴリズム設計は、アルゴリズムを実現するプログラムのソースコードを、設計者がプログラム言語を用いて作成することによって行われる。そして、設計者は、ソースコードをコンパイルし、プロセッサ上でプログラムを実行することにより、アルゴリズムの動作を確認する。アルゴリズム設計の際には、半導体回路として実現する際のアーキテクチャ、例えばパイプラインアーキテクチャなどは考慮されない。アルゴリズムの設計には、Ｃ言語などのプログラミング言語、又はＣ言語等のプログラミング言語に回路設計のための拡張を施した、ハードウェア記述言語、システム記述言語等が用いられる。これらの言語を用いて、アルゴリズムが表現された記述を、以降、「アルゴリズム記述」という。
【０００５】
次に、設計者は、アルゴリズムを実現するための「動作レベル設計」を行う。一般に、動作レベル設計は、設計者が動作記述を作成することにより行われる。動作レベル設計において、半導体回路として実現する際のアーキテクチャが決定される。動作レベル設計における動作記述にも、アルゴリズム設計と同様に、プログラミング言語、ハードウェア記述言語、システム記述言語等が用いられる。これらの言語を用いて、アーキテクチャを表現した記述を、以降、「動作記述」という。
【０００６】
次に、設計者は、具体的な回路構成を決定するための「ハードウェアレベル設計」を行う。一般に、ハードウェアレベル設計は、動作合成処理を行う装置やシステム（以降、「動作合成ツール」という。）が動作記述から「ＲＴＬ（Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌ）記述」を作成することにより行われる。ハードウェアレベル設計において、動作レベル設計において決定されたアーキテクチャに応じて、必要な制御処理、例えばパイプライン制御などが実装される。
【０００７】
上記のような設計過程における動作レベル設計は、アルゴリズム設計で作成されたアルゴリズム記述に対し、同じ機能を保持したまま、アーキテクチャを決定するための変更を動作記述に加えることによってなされることが多い。
【０００８】
また、動作レベル設計においては、動作合成ツールにとって好適となるように、同じ機能を保持したまま動作記述に変更が加えられることも多い。なぜなら、一般に、動作合成ツールは、すべての動作記述に対して品質の良いＲＴＬ記述を生成できるわけではないからである。そこで、動作合成ツールが品質の良いＲＴＬを生成するために好適となるように、動作記述を変更する必要がある。
【０００９】
同じ機能を保持したまま動作記述の変更を行う際には、記述変更後の動作記述が、変更前の動作記述と同じ機能を維持していることを検証する必要がある。なぜなら、記述変更後の動作記述が変更前の動作記述と同じ機能を維持していないことは、設計不具合につながる可能性があるためである。「２つの動作記述のそれぞれが定義する機能が同一である」ことを、以降、「２つの動作記述に等価性がある」という。「等価」とは、論理的機能が同一であること、すなわち、同一の入力に対する出力が同一であることを意味する。
【００１０】
動作記述の、変更前後の等価性検証の方法の一例として、シミュレーションによる検証（以降、「シミュレーション法」という。）があげられる。シミュレーション法では、記述変更前及び変更後の動作記述に、同じ入力の系列が印加され、シミュレーションが実行される。そして、記述変更前及び変更後の動作記述のそれぞれについてのシミュレーションの実行の結果として得られる２つの出力の系列が同一であるか否かが比較され、記述の変更前後で同じ機能を有していることが検証される。
【００１１】
動作記述の、変更前後の等価性検証の他の例として、形式的手法による検証（以降、「形式的手法」という。）があげられる。形式的手法では、記述変更前及び変更後の動作記述を数学的にモデル化し、２つのモデルが等価であることを証明する手法である。
【００１２】
形式的手法は、例えば、非特許文献１に開示されている。非特許文献１に示される手法は、記述中の変数がとりうる値を調べることにより、２つの記述間で同じ値を持つ変数のペアを捜し、最終的に回路の出力となる変数が同じ値を持つ変数のペアとして見つかるか否かを調べるものである。しかしながら、形式的手法には回路規模の増大に伴い検証時間が増大するという問題が良く知られている。
【００１３】
形式的手法による検証における、検証時間の増大を抑制する手法として、記述変更前後の差分に注目し、差分のみの比較を行う方法が考えられる。しかしながら、差分のみを単純に比較する方法では、２つの記述中に差分が複数個存在し、それらの差分間の対応関係がわからない場合などでは、正しく検証できない可能性がある。
【００１４】
単純に差分のみを比較するのではない技術は、例えば、非特許文献２に記載されている。非特許文献２に記載された形式的手法では、２つの記述間で同一内容の行で代入、すなわち変更されている変数については、その変数がとりうる値の範囲は調べられることなく、同一の値を持つ変数のペアとして認識される。変数についてのこのような取り扱いにより、検証時間の増大が抑制される。
【００１５】
形式的手法による等価性検証を効率的に行うための技術は、特許文献１、２にも記載されている。特許文献１に記載された等価性検証法は、比較対象論理回路の一部を変更した場合の等価性検証の効率を高める技術である。特許文献１の等価性検証法では、比較対象論理回路の論理が一部変更されたときに論理の影響が及ぶ論理素子に対する部分回路（ファンインコーン）が抽出され、そのファンインコーンの入力を引数とする論理関数が相互に比較される。
【００１６】
特許文献２に記載された等価性検証法では、動作記述及びＲＴＬ記述からそれぞれ動作合成された二つの回路を比較し、「対応が取れなかった部分」、すなわち回路の差分について、形式的検証を行う。
【００１７】
また、特許文献３には、２つの動作記述の差分情報及び動作記述とＲＴＬ記述との対応情報を用いて、等価なＲＴＬ記述を生成する合成装置が記載されている。具体的には、特許文献３の合成装置は、第１の動作記述から、第１のＲＴＬ記述、及び第１の動作記述と第１のＲＴＬ記述との対応情報を生成する。そして、特許文献３の合成装置は、その対応情報、及び第１の動作記述と第２の動作記述との差分情報に基づいて第１のＲＴＬ記述を変更して、第２の動作記述と等価な第２のＲＴＬ記述を生成する。
【００１８】
なお、形式的手法では、動作記述を所定の言語で記述されたテキストを含む文章とみなし、２つの動作記述の、テキストの不一致箇所を発見する技術が必要とされることがある。このような技術は、例えば非特許文献３に記載されている。
【００１９】
また、形式的手法では、動作記述から、依存関係を持つ複数の動作についての記述を、抽出する技術が必要とされることがある。例えば、動作記述Ｘ中の部分記述Ｘ１によって表現された動作ｘ１に影響を与える、動作ｘ２を表現する部分記述Ｘ２を、動作記述Ｘから抽出する技術が求められることがある。このような技術は、例えば非特許文献４に記載されている。
【先行技術文献】
【特許文献】
【００２０】
【特許文献１】特開２００３−０５８５９７号公報  （第４−５頁、図３）
【特許文献２】特開２００７−２３３６４８号公報  （第５−６頁、図３）
【特許文献３】特開２００７−０３４５８４号公報  （第８−９頁、図２）
【非特許文献】
【００２１】
【非特許文献１】H.Saito, 他４名, "An equivalence checking methodology for hardware oriented C-based specifications", "Proc. International Workshop on High Level Design Validation and Test", フランス, IEEE, 2002年, pp. 139-144
【非特許文献２】T. Matsumoto, 他２名, "An Equivalence Checking Method for C Descriptions Based on Symbolic Simulation with Textual Differences", IEICE Trans. Fundamentals, 日本, 電子情報通信学会, 2005年, Vol. E88-A, No. 12, pp. 3315-3323
【非特許文献３】Paul Heckel, "A technique for isolating differences between files", Communications of the ACM, 米国, ACM, 1978年, 21(4), p. 264-268
【非特許文献４】M. Weiser, "Program Slicing", Ttrans. on Software Engineering, 米国, IEEE, 1984年, Issue 4, pp. 352-357
【発明の概要】
【発明が解決しようとする課題】
【００２２】
上記の各公知技術にはそれぞれ問題がある。
【００２３】
まず、シミュレーション法には、膨大な入力の系列に対してシミュレーション実行を行う必要があり、検証時間が増大するという問題がある。そのため、十分な検証時間を確保できない場合には、検証漏れが発生する危険がある。
【００２４】
非特許文献１に示される形式的手法は、記述の等価性の完全な検証を行うためには、記述中の変数がとりうるすべての値を調べる必要がある。そのため、検証対象となる動作記述の規模、例えば記述された行数などが増大すると、検証時間が増大するという問題がある。
【００２５】
非特許文献２に示される形式的手法は、単純に差分のみを比較するものではないので、検証時間の増大は抑制される。しかしながら、記述変更部分に全く影響を与えない部分についても検証を行う必要が残っているため、動作記述の規模が増大すると、検証時間も増大するという問題がある。
【００２６】
特許文献１に記載された等価性検証法では、論理回路の差分に影響を与えるファンインコーンが抽出される。そのため、特許文献１の検証法は、記述変更前及び変更後のそれぞれの記述中に差分が１個のみ存在し、差分間の対応関係が明らかである場合には対応できる。しかしながら、記述変更前及び変更後のそれぞれの記述中に差分が複数個存在し、それらの差分間の対応関係がわからない場合は、ファンインコーンの入力を引数とする論理関数間の対応関係も不明である。したがって、このような場合には論理関数を相互に比較することができず、等価性を検証することができない。
【００２７】
特許文献２に記載された等価性検証法は、回路の差分の、それぞれの機能が等価である場合の等価性検証には対応できる。しかし、差分のそれぞれの機能に違いがあり、複数の差分を組み合わせて初めて同じ機能を実現している場合の検証には対応することができない。
【００２８】
特許文献３に記載された合成装置では、第１の動作記述と第１のＲＴＬ記述との対応情報を生成する。その際、ある行の動作記述の記載内容によっては、対応するＲＴＬ記述が、広範囲の行に及ぶ可能性がある。また、対応情報と、第１の動作記述と第２の動作記述の差分情報とから、第１のＲＴＬ記述についての変更すべき箇所が特定されなければならない。しかし、対応情報が広範囲の行を含むときは、第１のＲＴＬ記述の変更すべき箇所の特定は容易ではない。また、第１の動作記述と第２の動作記述の差分が大きいとき、すなわち、第２の動作記述が、第１の動作記述に大幅な変更を加えたものであるときも、同様に、第１のＲＴＬ記述の変更すべき箇所の特定は容易ではない。このように、特許文献３の合成装置は、動作記述の内容や設計変更の規模に制約があるという課題がある。
（発明の目的）
本発明の目的は、所定の言語が用いられた記述についての設計変更前後の等価性を効率よく検証できる設計検証装置、設計検証方法、及び設計検証用プログラムを提供することにある。
【課題を解決するための手段】
【００２９】
本発明の設計検証装置は、所定の言語で記述された第１の記述と、部分的に第１の記述と異なる第２の記述とを比較し、第２の記述と異なる第１の記述の部分である第１の差分記述及び第２の差分記述、並びに第１の記述と異なる第２の記述の部分である第３の差分記述を抽出する差分抽出手段と、第１の記述から第１の差分記述及び第２の差分記述に影響を与える第１の依存関係記述を抽出する依存関係抽出手段と、第１の差分記述、第２の差分記述、及び第１の依存関係記述を含む第１の比較記述、並びに第３の差分記述を含む第２の比較記述を生成する比較記述生成手段と、第１の比較記述と第２の比較記述との等価性を検証する等価性検証手段と、を備えたことを特徴とする。
【００３０】
本発明の設計検証方法は、所定の言語で記述された第１の記述と、部分的に第１の記述と異なる第２の記述とを比較し、第２の記述と異なる第１の記述の部分である第１の差分記述及び第２の差分記述、並びに第１の記述と異なる第２の記述の部分である第３の差分記述を抽出し、第１の記述から第１の差分記述及び第２の差分記述に影響を与える第１の依存関係記述を抽出し、第１の差分記述、第２の差分記述、及び第１の依存関係記述を含む第１の比較記述、並びに第３の差分記述を含む第２の比較記述を生成し、第１の比較記述と第２の比較記述との等価性を検証することを特徴とする。
【００３１】
本発明の設計検証用プログラムは、所定の言語で記述された複数の記述に所定の処理を行う記述処理システムが備えるコンピュータを、その言語で記述された第１の記述と、部分的に第１の記述と異なる第２の記述とを比較し、第２の記述と異なる第１の記述の部分である第１の差分記述及び第２の差分記述、並びに第１の記述と異なる第２の記述の部分である第３の差分記述を抽出する差分抽出手段と、第１の記述から第１の差分記述及び第２の差分記述に影響を与える第１の依存関係記述を抽出する依存関係抽出手段と、第１の差分記述、第２の差分記述、及び第１の依存関係記述を含む第１の比較記述、並びに第３の差分記述を含む第２の比較記述を生成する比較記述生成手段と、第１の比較記述と第２の比較記述との等価性を検証する等価性検証手段と、として機能させることを特徴とする。
【発明の効果】
【００３２】
本発明の設計検証装置、設計検証方法、及び設計検証用プログラムには、所定の言語が用いられた記述の設計変更前後の等価性を効率よく検証できるという効果がある。その理由は、設計変更前後の記述における変更部分と該変更部分に依存関係がある部分のみが抽出され比較されるためである。
【図面の簡単な説明】
【００３３】
【図１】本発明の実施形態の、設計検証装置の構成を示すブロック図である。
【図２】本発明の実施形態の、設計検証装置の動作を示すフローチャートである。
【図３】本発明の実施形態の、設計検証装置の動作の具体例における動作記述Ａを示す図である。
【図４】本発明の実施形態の、設計検証装置の動作の具体例における動作記述Ｂを示す図である。
【図５Ａ】本発明の実施形態の、設計検証装置の動作の具体例における差分回路を示す図である。
【図５Ｂ】本発明の実施形態の、設計検証装置の動作の具体例における差分回路を示す図である。
【図５Ｃ】本発明の実施形態の、設計検証装置の動作の具体例における差分回路を示す図である。
【図５Ｄ】本発明の実施形態の、設計検証装置の動作の具体例における差分回路を示す図である。
【図６】本発明の実施形態の、設計検証装置の動作の具体例における依存関係回路を示す図である。
【図７】本発明の実施形態の、設計検証装置の動作の具体例における比較回路を示す図である。
【図８】本発明の実施形態の、設計検証装置の動作の具体例における依存関係回路を示す図である。
【図９】本発明の実施形態の、設計検証装置の動作の具体例における比較回路を示す図である。
【発明を実施するための形態】
【００３４】
（実施形態の構成）
本発明を実施するための形態について、図面を参照して詳細に説明する。
【００３５】
図１は、本発明の実施形態の、設計検証装置の構成を示すブロック図である。本実施形態は、プログラム制御により動作するコンピュータ１００と、記憶手段２００を備える。本発明における「コンピュータ」とは、一般的に、中央処理装置、プロセッサ、データ処理装置と呼ばれるものである。
【００３６】
コンピュータ１００は、プログラムを実行することにより、差分抽出手段１０１と、依存関係抽出手段１０２と、比較回路生成手段１０３と、等価性比較手段１０４とを実現する。
【００３７】
記憶手段２００は、検証対象回路記憶部２０１と、差分回路記憶部２０２と、依存関係回路記憶部２０３と、比較回路記憶部２０４と含む。
【００３８】
検証対象記憶部２０１は、プログラム言語で記述された記述であり、かつ、等価性検証の対象となる、２つの動作記述Ａ、Ｂをあらかじめ記憶している。
【００３９】
差分抽出手段１０１は、検証対象回路記憶部２０１から、動作記述Ａ、Ｂを読み出す。そして、差分抽出手段１０１は、動作記述Ａと動作記述Ｂとの差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１（ｎ１は１以上の整数）、及びＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２（ｎ２は１以上の整数）を抽出する。差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１は、動作記述Ａの中の連続する一部の記述であって、動作記述Ｂと異なる記述である。ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２は、動作記述Ｂの中の連続する一部の記述であって、動作記述Ａと異なる記述である。差分抽出手段１０１は、抽出した差分回路のそれぞれを差分回路記憶部２０２に格納する。
【００４０】
なお、差分回路ＤＩＦＦ＿Ａの個数であるｎ１と、差分回路ＤＩＦＦ＿Ｂの個数であるｎ２とは、必ずしも等しいとは限らない。なぜなら、一方の動作記述の複数の差分回路が、他方の動作記述の単一の差分回路に対応する可能性があるからである。
【００４１】
依存関係抽出手段１０２は、検証対象回路記憶部２０１から、動作記述Ａ、Ｂを読み出す。同時に、依存関係抽出手段１０２は、差分回路記憶部２０２から、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１、及びＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２を読み出す。そして、依存関係抽出手段１０２は、動作記述Ａ及び動作記述Ｂにおける、差分回路間の依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、 ＤＥＰＥＮＤ＿Ａｍ１（ｍ１は１以上の整数）、及びＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、 ＤＥＰＥＮＤ＿Ｂｍ２（ｍ２は１以上の整数）を抽出する。依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、 ＤＥＰＥＮＤ＿Ａｍ１は、動作記述Ａの一部である。ＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、 ＤＥＰＥＮＤ＿Ｂｍ２は、動作記述Ｂの一部である。依存関係抽出手段１０２は、抽出した依存関係回路を依存関係回路２０３に格納する。このように、依存関係抽出手段１０２は、依存関係回路の抽出動作を、回路Ａ及び回路Ｂのそれぞれに対して行う。
【００４２】
なお、依存関係回路ＤＥＰＥＮＤ＿Ａの個数であるｍ１と、依存関係回路ＤＥＰＥＮＤ＿Ｂの個数であるｍ２とも、必ずしも等しいとは限らない。なぜなら、差分回路ＤＩＦＦ＿Ａの個数であるｎ１と、差分回路ＤＩＦＦ＿Ｂの個数であるｎ２とが異なる場合があるからである。ｎ１とｎ２が異なる場合であっても、依存関係回路の抽出は、差分回路ＤＩＦＦ＿Ａ、ＤＩＦＦ＿Ｂのそれぞれについて行われるので、何ら差し支えない。
【００４３】
また、当然ながら、依存関係回路の個数は、差分回路の個数以下である。すなわち、ｍ１はｎ１以下であり、ｍ２はｎ２以下である。したがって、ｍ１又はｍ２が０、すなわち動作記述Ａ、Ｂのいずれかについては依存関係回路が抽出できないも場合もある。なお、動作記述Ａ、Ｂの両方について依存関係回路が抽出できない場合は、本発明の対象外である。
【００４４】
そして、後述のように、差分回路及び依存関係回路を含む比較回路が、動作記述Ａ又は動作記述Ｂのいずれかについて作成され、少なくとも差分回路を含む比較回路が他方の動作記述について作成される。動作記述Ａ、Ｂのそれぞれについて１個以上作成された差分回路を用いて、等価性検証が行われる。このように、ｎ１とｎ２が異なる場合についても、本実施形態は問題なく適用可能である。
【００４５】
比較回路生成手段１０３は、差分回路記憶部２０２から、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１、及びＤＩＦＦ＿ＢＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２を読み出す。同時に、比較回路生成手段１０３は、依存関係回路記憶部２０３から、依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍ１、及びＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、ＤＥＰＥＮＤ＿Ｂｍ２を読み出す。
【００４６】
そして、比較回路生成手段１０３は、差分回路と依存関係回路を含む比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋ（ｋは１以上の整数）及びＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋを生成する。具体的には、比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋは、それぞれ、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎの全部又は一部を含み、依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍの全部又は一部を含んでもよい。このとき、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎは、比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋのいずれかには必ず含まれる。比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋは、それぞれ、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎの全部又は一部を含み、依存関係回路ＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、ＤＥＰＥＮＤ＿Ｂｍの全部又は一部を含んでもよい。このとき、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎは、比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋのいずれかには必ず含まれる。
【００４７】
すなわち、比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋ、及び比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋのすべてが差分回路を含む。そして、比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋ、及び比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋの少なくとも一部は、依存関係回路を含む。比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋのすべてが依存関係回路を含まない場合は、比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋのいずれかが依存関係回路を含む。比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋのすべてが依存関係回路を含まない場合は、比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋのいずれかが依存関係回路を含む。
【００４８】
比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋ及びＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋは、それぞれ、動作記述Ａ、Ｂについての差分回路と依存関係回路のすべてを含んでいても差支えないし、差分回路と依存関係回路の一部が含まれていなくても差し支えない。
【００４９】
動作記述Ａ、Ｂそれぞれについてのｋ個の比較回路の、ｉ番目（ｉは１以上の整数）の比較回路ＣＭＰ＿ＡｉとＣＭＰ＿Ｂｉは、たとえば、それぞれ対応する差分回路と、その差分回路に対応する依存関係回路が含まれるように生成されることが望ましい。なぜなら、対応する差分回路を含むように生成された比較回路は等価である可能性が高いためである。
【００５０】
差分回路と依存関係回路の一部が含まれていない比較回路を用いた等価性検証では、差分回路と依存関係回路の全部が含まれている比較回路を用いた等価性検証よりも、等価性があるにもかかわらず、等価性がないと判定される可能性が高くなる。しかし、前者の等価性検証を用いることも可能である。
【００５１】
比較回路生成手段１０３は、生成された比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋ及びＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋを比較回路記憶部２０４に格納する。
【００５２】
等価性比較手段１０４は、比較回路記憶部２０４より動作記述Ａに対する比較回路ＣＭＰ＿Ａｉ、及び動作記述Ｂに対する比較回路ＣＭＰ＿Ｂｉを読み出す。そして、等価性比較手段１０４は、比較回路ＣＭＰ＿ＡｉとＣＭＰ＿Ｂｉとの比較を、ｉ＝１から、比較回路ＣＭＰ＿Ａ、ＣＭＰ＿Ｂの個数に対応するｉ＝ｋまで繰り返す。ｋ回のそれぞれの比較結果によって、比較回路ＣＭＰ＿Ａｉ、ＣＭＰ＿Ｂｉのそれぞれに含まれる差分回路同士の等価性を検証することができる。等価性比較手段１０４は、検証結果を、記憶手段２００又は外部に出力してもよい。
（実施形態の動作）
次に、図１及び図２のフローチャートを参照して、本実施形態の全体の動作について詳細に説明する。
【００５３】
前述の通り、検証対象記憶部２０１は、プログラム言語で記述され、かつ、等価性検証の対象となる、２つの動作記述Ａ、Ｂをあらかじめ記憶している。
【００５４】
まず、差分抽出手段１０１は、検証対象回路記憶部２０１から、等価性検証の対象とする動作記述Ａ、及び動作記述Ｂを読み出す。さらに、差分抽出手段１０１は動作記述Ａと動作記述Ｂを比較し、その差分回路を、動作記述Ａ、動作記述Ｂに対してそれぞれ抽出する。なお、差分回路は、動作記述Ａ、Ｂそれぞれについて、複数個所含まれるものとする。差分抽出手段１０１は、すべての差分回路を抽出する。動作記述Ｂに対する動作記述Ａの差分回路は、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎであり、動作記述Ａに対する動作記述Ｂの差分回路は、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎである。差分抽出手段１０１は、抽出したそれぞれの差分回路を差分回路記憶部２０２に格納する（図２のステップＳ１）。
【００５５】
動作記述Ａと動作記述Ｂとの差分は、例えば、動作記述Ａ、Ｂ中に含まれるテキストの違いにより認識される。テキストの違いの認識には、例えば、非特許文献３に開示された技術を利用することができる。
【００５６】
次に、動作記述Ａから比較回路ＣＭＰ＿Ａ１、ＣＭＰ＿Ａ２、・・・、ＣＭＰ＿Ａｋを抽出するために、以下のステップＳ２、Ｓ３の処理を行う。
【００５７】
まず、依存関係抽出手段１０２は、検証対象回路記憶部２０１から等価性検証の対象とする動作記述Ａを読み出す。同時に、依存関係抽出手段１０２は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎを読み出す。そして、依存関係抽出手段１０２は、動作記述Ａにおける差分回路間の依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍを抽出する。依存関係抽出手段１０２は、抽出した依存関係回路を依存関係回路２０３に格納する（ステップＳ２）。
【００５８】
差分回路間の「依存関係回路」とは、差分回路に影響を与える文を含む部分回路である。より具体的には、差分回路間の依存関係回路とは、前後して配置された２つの差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２がある場合、前に配置された差分回路ＤＩＦＦ＿Ａ１にて代入される変数と後ろに配置された差分回路ＤＩＦＦ＿Ａ２にて参照される変数との双方に影響を与える文を含む部分回路である。依存関係回路の抽出には、例えば、非特許文献４に開示される技術を利用することができる。
【００５９】
依存関係回路を抽出する対象となる差分回路は、２つの差分回路の組である。３つ以上の差分回路が存在する場合は、すべての差分回路がいずれかの組に含まれるように選択された、２つの差分回路からなる組について、依存関係回路が抽出される。
【００６０】
例えば、３つの差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、ＤＩＦＦ＿Ａ３が存在する場合は、２つの依存関係回路が抽出される。例えば、差分回路ＤＩＦＦ＿Ａ１とＤＩＦＦ＿Ａ２からなる組についての依存関係回路ＤＥＰＥＮＤ＿Ａ１２、差分回路ＤＩＦＦ＿Ａ２とＤＩＦＦ＿Ａ３からなる組についての依存関係回路ＤＥＰＥＮＤ＿Ａ２３が抽出される。このように、３つの差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、ＤＩＦＦ＿Ａ３のすべてが、いずれかの差分回路の組に含まれ、それぞれの差分回路の組から依存関係回路が抽出される。
【００６１】
次に、比較回路生成手段１０３は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎを読み出す。同時に、比較回路生成手段１０３は、依存関係回路記憶部２０３から依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍを読み出す。そして、比較回路生成手段１０３は、差分回路と依存関係回路から構成される比較回路ＣＭＰ＿Ａを生成する。比較回路生成手段１０３は、生成した比較回路を比較回路記憶部２０４に格納する（ステップＳ３）。
【００６２】
「比較回路」は、動作記述の部分回路であって、差分回路と依存関係回路とを含む回路である。すなわち、比較回路ＣＭＰ＿Ａｉは、すべての差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１と、すべての依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍ１を結合した回路である。あるいは、比較回路ＣＭＰ＿Ａｉは、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、・・・、ＤＩＦＦ＿Ａｎ１の一部と、すべての依存関係回路ＤＥＰＥＮＤ＿Ａ１、ＤＥＰＥＮＤ＿Ａ２、・・・、ＤＥＰＥＮＤ＿Ａｍ１の一部を結合した回路でもよい。
【００６３】
次に、動作記述Ｂから比較回路ＣＭＰ＿Ｂ１、ＣＭＰ＿Ｂ２、・・・、ＣＭＰ＿Ｂｋを抽出するために、以下のステップＳ４、Ｓ５の処理を行う。比較回路ＣＭＰ＿Ｂは、すべての差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２と、すべての依存関係回路ＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、 ＤＥＰＥＮＤ＿Ｂｍ２を結合した回路である。あるいは、比較回路ＣＭＰ＿Ｂｉは、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、・・・、ＤＩＦＦ＿Ｂｎ２の一部と、すべての依存関係回路ＤＥＰＥＮＤ＿Ｂ１、ＤＥＰＥＮＤ＿Ｂ２、・・・、ＤＥＰＥＮＤ＿Ｂｍ２の一部を結合した回路でもよい。ステップＳ４は、ステップＳ２と同じ操作を回路Ｂに対して行うステップである。ステップＳ５は、ステップＳ３と同じ操作を回路Ｂに対して行うステップである。
【００６４】
最後に、等価性比較手段１０４は、比較回路記憶部２０４より、動作記述Ａに対する比較回路ＣＭＰ＿Ａｉ、及び動作記述Ｂに対する比較回路ＣＭＰ＿Ｂｉを読み出す。そして、等価性比較手段１０４は、比較回路ＣＭＰ＿ＡｉとＣＭＰ＿Ｂｉを比較して等価性を検証し、必要に応じて検証結果を出力する（ステップＳ６）。Ｓ６における比較回路ＣＭＰ＿ＡｉとＣＭＰ＿Ｂｉとの比較は、ｉ＝１からｉ＝ｋのそれぞれについて行われる。すなわち、ｋ回の比較が繰り返される。そして、ｋ回のそれぞれの比較結果によって、比較回路ＣＭＰ＿Ａｉ、ＣＭＰ＿Ｂｉのそれぞれに含まれる差分回路同士の等価性を検証することができる。
【００６５】
等価性検証の方法は特に限定されない。等価性検証は、例えば、前述のシミュレーション法や、非特許文献１等に開示される形式的手法を利用して行うことができる。
（実施形態の効果）
次に、本実施形態の効果について説明する。
【００６６】
本実施形態では、差分抽出手段と、依存関係抽出手段と、比較回路生成手段と、等価性比較手段を備え、設計変更前後の動作記述における変更部分とその変更部分に依存関係がある部分のみを比較回路として抽出し、比較する。このように、等価性の検証対象とすべき回路はすべて検証対象となり、かつ、検証対象とする回路は必要な回路のみに絞られるため、等価性を検証する対象回路の規模の増大を抑制できる。したがって、動作記述の設計変更前後の等価性を効率よく検証することができる。
（実施形態の具体例）
次に、具体的な動作記述の例を用いて、本実施形態の動作を説明する。
【００６７】
図３は、動作記述の一例である動作記述Ａを示す。動作記述Ａには、ＡＮＳＩ−Ｃ言語を用いて、関数str_to_iの内容が記述されている。
【００６８】
動作記述Ａに記述された関数str_to_i（以降、「関数Ａ」という。）は、概略、次のような機能を有する。すなわち、関数Ａを、４桁の数字文字列str[]を引数として渡して呼び出すと、これ対応する整数が返り値として得られる。例えば、
str[0] = `1`
str[1] = `2`
str[2] = `8`
str[3] = `0` 
を引数として、呼び出されるとき、戻り値は整数”1280”となる。 
関数Ａは、概略、次のように動作する。
【００６９】
関数Ａを規定する動作記述Ａの２行目から３行目では、変数val_rが定義され、かつ変数val_rが動作合成ツールによってＲＴＬに変換される際には、レジスタとして実現されることが指定されている。
【００７０】
動作記述Ａの４行目から５行目では、変数val_tが定義され、かつ、変数val_tが動作合成ツールによってＲＴＬに変換される際には、配線として実現されることが指定されている。
【００７１】
６行目では変数valが定義され、その値が０に初期化されている。
【００７２】
７行目では、８行目から１１行目を３回繰り返すことが指定されている。
【００７３】
８行目では、引数str[i]の文字を整数に変換し、該整数に変数valの値を足したものを変数val_tに格納することが指定されている。
【００７４】
９行目では、変数val_t の値を１０倍したものが変数valに格納されることが指定されている。
【００７５】
１０行目では、変数valの値を変数val_r に格納することが指定されている。前記の通り、val_r は動作合成ツールによってレジスタとして実現されることが指定されている。したがって、１０行目は、変数valの値を一度レジスタに格納することを指定している。
【００７６】
１１行目では、変数val_rの値が変数valに再度格納されている。
【００７７】
１３行目では、まず引数str[3]の文字を整数に変換し、次にその整数に変数valの値を足したものを再度valに格納することが指定されている。
【００７８】
１４行目では、変数valの値を関数str_to_i() の返り値とすることが指定されている。
【００７９】
上述の通り、関数Ａは、引数str[]の上位の数字から順に整数に変換し、一文字ずつ１０倍しながら足し合わせることで、文字列str[]に格納された数字列を整数値に変換する。
【００８０】
動作記述Ａは、変数に対する実現方法を指定しており（２行目乃至４行目）、動作合成ツールに好適な動作記述である。
【００８１】
図４は、動作記述の一例である動作記述Ｂを示す。動作記述Ｂは、図３の動作記述Ａに対して、機能を保持したまま、動作合成ツールに好適となるように、変更が施されたものである。
【００８２】
動作記述Ｂに記述された関数str_to_i（以降、「関数Ｂ」という。）は、以下の点で、関数Ａと異なる。
【００８３】
まず、関数Ａを規定する動作記述Ａの９行目では、変数valに格納される値は変数val_tを１０倍したものであることが指定されている。これに対して、関数Ｂを規定する動作記述Ｂの９行目では、変数valに格納される値は変数val_tの値そのものであることが指定されている。
【００８４】
さらに、動作記述Ａの１１行目では、変数valに格納される値は変数val_rの値そのものであることが指定されている。これに対して、動作記述Ｂの１１行目から１３行目では、変数valに格納される値は、変数val_r を３ビットだけ左シフトした値tと、変数val_rを１ビットだけ左シフトした値uとが加算された値となっている。
【００８５】
動作記述Ｂは、以下の点で動作合成ツールに好適である。
【００８６】
まず、動作記述Ａにおける乗算が、動作記述Ｂでは定数シフトと加算によって実現されている。すなわち、１０倍の値の計算のために、動作記述Ａにおいては乗算器が使用されるのに対して、動作記述Ｂでは３ビットシフト（８倍）と２ビットシフト(２倍)の加算が使用される。
【００８７】
一般に、数値を固定のビット分だけシフトする、いわゆる定数シフト演算はハードウェアリソースを消費しない。また、加算器は、乗算器よりも少ないハードウェアリソースで実現でき、計算にかかる遅延も少ない。
【００８８】
したがって、１０倍の値を計算するために多くのハードウェアリソースや、長い演算遅延を要する乗算器を利用する動作記述Ａよりも、定数シフト演算及び加算を用いることにより、より少ないリソースで、かつ、短い演算遅延しか要しない動作記述Ｂのほうが、動作合成ツールに好適である。
【００８９】
動作記述Ａと動作記述Ａに対する動作記述Ｂの変更点を比較する。動作記述Ａの９行目と、対応する変更点である動作記述Ｂの９行目は同じ機能を有しない。そのため、上記の動作記述Ａ、Ｂの箇所のみを比較しても、両者は等価とは判定されない。同様に、動作記述Ａの１１行目と動作記述Ｂの１１行目乃至１３行目とは同じ機能を有しない。そのため、上記動作記述Ａ、Ｂの箇所のみを比較しても、両者は等価とは判定されない。このように、単純に、変更後の記載箇所とそれに対応する変更前の記載箇所のみを比較しても、２つの記述が等価であることを検証することはできない。
【００９０】
本実施形態では、動作記述Ａと動作記述Ｂは、記憶装置２００の検証対象回路記憶部２０１に、あらかじめ記憶されている。
【００９１】
まず、差分抽出手段１０１は、検証対象回路記憶部２０１から、等価性検証の対象とする動作記述Ａ、及び動作記述Ｂを読み出す。さらに、差分抽出手段１０１は動作記述Ａと動作記述Ｂを比較し、動作記述Ｂに対する動作記述Ａの差分回路ＤＩＦＦ＿Ａ、及び動作記述Ａに対する動作記述Ｂの差分回路ＤＩＦＦ＿Ｂを抽出する。なお、差分回路は、動作記述Ａ、Ｂそれぞれについて、複数個所含まれるものし、差分抽出手段１０１は、そのすべての差分回路を抽出する。
【００９２】
図５Ａ、図５Ｂは、それぞれ、動作記述Ａの差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２を例示する。図５Ｃ、図５Ｄは、それぞれ、動作記述Ｂの差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２を例示する。
【００９３】
差分抽出手段１０１は、抽出した差分回路ＤＩＦＦ＿Ａ、ＤＩＦＦ＿Ｂを、差分回路記憶部２０２に格納する（ステップＳ１）。
【００９４】
次に、動作記述Ａから比較回路ＣＭＰ＿Ａを抽出するために、以下のステップＡ２、Ａ３の処理を行う。
【００９５】
まず、依存関係抽出手段１０２は、検証対象回路記憶部２０１から等価性検証の対象とする動作記述Ａを読み出す。同時に、依存関係抽出手段１０２は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２を読み出す。そして、依存関係抽出手段１０２は、動作記述Ａにおける差分回路間の依存関係回路ＤＥＰＥＮＤ＿Ａを抽出する。依存関係抽出手段１０２は、抽出した依存関係回路ＤＥＰＥＮＤ＿Ａを依存関係回路記憶部２０３に格納する（ステップＳ２）。
【００９６】
図６に、抽出された依存関係回路ＤＥＰＥＮＤ＿Ａを例示する。
【００９７】
動作記述Ａの前後する差分回路ＤＩＦＦ＿Ａ１（動作記述Ａの９行目）、及び、ＤＩＦＦ＿Ａ２（動作記述Ａの１１行目）に対して、その間の記述であって、ＤＩＦＦ＿Ａ１において代入される変数valを参照し、かつ、ＤＩＦＦ＿Ａ２で参照される変数val_rに代入する記述は１０行目のみである。したがって、依存関係回路ＤＥＰＥＮＤ＿Ａとして、動作記述Ａの９行目が抽出される。
【００９８】
抽出された依存関係回路ＤＥＰＥＮＤ＿Ａは依存関係回路２０３に格納される。
【００９９】
次に、比較回路生成手段１０３は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２を読み出す。同時に、依存関係回路記憶部２０３から依存関係回路ＤＥＰＥＮＤ＿Ａを読み出す。そして、比較回路生成手段１０３は、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２と依存関係回路ＤＥＰＥＮＤ＿Ａを含む比較回路ＣＭＰ＿Ａを生成する。比較回路生成手段１０３は、生成した比較回路ＣＭＰ＿Ａを比較回路記憶部２０４に格納する（ステップＳ３）。
【０１００】
図７に、動作記述Ａに対して生成された比較回路ＣＭＰ＿Ａを例示する。比較回路ＣＭＰ＿Ａは、動作記述Ａの９行目〜１１行目で構成される部分回路であり、差分回路ＤＩＦＦ＿Ａ１、ＤＩＦＦ＿Ａ２、及び依存関係回路ＤＥＰＥＮＤ＿Ａより構成される。生成された比較回路ＣＭＰ＿Ａは比較回路記憶部２０４に格納される。
【０１０１】
次に、動作記述Ｂから比較回路ＣＭＰ＿Ｂを抽出するために、ステップＳ４、Ｓ５の処理を行う。
【０１０２】
まず、依存関係抽出手段１０２は、検証対象回路記憶部２０１から等価性検証の対象とする動作記述Ｂを読み出す。同時に、依存関係抽出手段１０２は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２を読み出す。そして、依存関係抽出手段１０２は、動作記述Ｂにおける差分回路間の依存関係回路ＤＥＰＥＮＤ＿Ｂを抽出する。依存関係抽出手段１０２は、抽出した依存関係回路ＤＥＰＥＮＤ＿Ｂを依存関係回路記憶部２０３に格納する（ステップＳ４）。
【０１０３】
図８に、抽出された依存関係回路ＤＥＰＥＮＤ＿Ｂを例示する。
【０１０４】
動作記述Ｂの前後する差分回路ＤＩＦＦ＿Ｂ１（動作記述Ｂの９行目）、及び、ＤＩＦＦ＿Ｂ２（動作記述Ｂの１１行目乃至１３行目）に対して、その間の記述であって、ＤＩＦＦ＿Ｂ１において代入されるvalを参照し、かつ、ＤＩＦＦ＿Ａ２で参照される変数val_rに代入する記述は１０行目のみである。したがって、依存関係回路ＤＥＰＥＮＤ＿Ｂとして、動作記述Ｂの１０行目が抽出される。
【０１０５】
抽出された依存関係回路ＤＥＰＥＮＤ＿Ｂは依存関係回路２０３に格納される。
【０１０６】
次に、比較回路生成手段１０３は、差分回路記憶部２０２から差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２を読み出す。同時に、依存関係回路記憶部２０３から依存関係回路ＤＥＰＥＮＤ＿Ｂを読み出す。そして、比較回路生成手段１０３は、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２と依存関係回路ＤＥＰＥＮＤ＿Ｂを含む比較回路ＣＭＰ＿Ｂを生成する。比較回路生成手段１０３は、生成した比較回路ＣＭＰ＿Ｂを比較回路記憶部２０４に格納する（ステップＳ５）。
【０１０７】
図９に、動作記述Ｂに対して生成された比較回路ＣＭＰ＿Ｂを例示する。比較回路ＣＭＰ＿Ｂは、動作記述Ｂの９行目〜１３行目で構成される部分回路であり、差分回路ＤＩＦＦ＿Ｂ１、ＤＩＦＦ＿Ｂ２、及び、依存関係回路ＤＥＰＥＮＤ＿Ｂより構成される。生成された比較回路ＣＭＰ＿Ｂは比較回路記憶部２０４に格納される。
【０１０８】
最後に、等価性比較手段１０４は、比較回路記憶部２０４より、動作記述Ａに対する比較回路ＣＭＰ＿Ａ、及び動作記述Ｂに対する比較回路ＣＭＰ＿Ｂを読み出す。そして、等価性比較手段１０４は、動作記述Ａ、動作記述Ｂのそれぞれに対する比較回路ＣＭＰ＿Ａ、ＣＭＰ＿Ｂを比較して等価性を検証し、検証結果を出力する（ステップＳ６）。
【０１０９】
具体的には、比較回路ＣＭＰ＿Ａと比較回路ＣＭＰ＿Ｂとが比較され、等価性が検証される。検証結果は、動作記述Ａと動作記述Ｂの等価性の検証結果として出力される。ＣＭＰ＿ＡとＣＭＰ＿Ｂとが等価な機能を持つとき、動作記述Ａと動作記述Ｂが等価であるとの旨の検証結果が出力される。
【０１１０】
図２の４つの手段、すなわち、差分抽出手段１０１、依存関係抽出手段１０２、比較回路生成手段１０３、等価性比較手段１０４は、記憶手段２００に格納された設計検証用プログラムを、コンピュータ１００が読み出して実行することによって実現される。設計検証用プログラムは、ＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）、フラッシュメモリ等の半導体記憶装置、光ディスク、磁気ディスク、光磁気ディスク等、非一時的な媒体に格納されてもよい。
【０１１１】
なお、差分抽出手段１０１、依存関係抽出手段１０２、比較回路生成手段１０３、等価性比較手段１０４の一部又は全部を実現する手段は、プログラムによるソフトウェア処理には限定されない。すなわち、差分抽出手段１０１、依存関係抽出手段１０２、比較回路生成手段１０３、等価性比較手段１０４の一部又は全部は、ハードウェアによって実現されてもよい。
【０１１２】
上記実施形態では、動作記述Ｂは、動作記述Ａの一部が変更されたものとして説明した。しかし、本発明の設計検証装置の処理対象は、動作記述Ａと、その一部を変更した動作記述Ｂには限定されない。すなわち、動作記述Ｂは、動作記述Ａとは独立して設計されたものであっても、動作記述Ａとの差分回路を２つ以上含み、差分回路以外の部分が動作記述Ａと共通であればよい。このような動作記述Ｂに対しても、差分回路及び依存関係回路の抽出、並びに比較回路の生成は可能であり、原理的に本発明を適用することができる。
【０１１３】
また、上記実施形態では、動作記述Ａ、Ｂは、回路、すなわちハードウェアの動作が記述されたものとして説明した。しかし、本実施形態の設計検証装置の処理対象は、ハードウェアの動作を記述する動作記述には限定されない。例えば、前述の、アルゴリズム記述、ＲＴＬ記述についても、本発明を適用することができる。
【０１１４】
さらに、本実施形態の設計検証装置の処理対象は、ハードウェアへは変換されない、一般のソフトウェアの記述にも適用可能である。ソフトウェアの記述についても、処理速度や使用資源の量を最適化するための変更が施される場合がある。このような場合にも、本実施形態の設計検証装置によれば、記述の変更の前後で、記述の等価性が保たれていることを検証することができる。したがって、記述の機能的なデバッグが完了した後、性能面や使用資源面での最適化を行うことができるので、ソフトウェアの開発を効率的に行うことができる。
【０１１５】
上記のように、本発明は、２つの記述の等価性の検証に有効である。したがって、動作合成若しくは論理合成、又は低級言語へのコンパイル等、元の記述に用いられていた言語とは異なる言語や所定の規則に従った記述に変換する変換処理に、本発明の等価性検証手段を付加することも有効である。このような変換処理に、本発明の等価性検証手段を付加することによって、２つの記述の等価性を検証した後、変換処理にスムーズに移行することができる。したがって、記述の等価性検証から、最終結果としてのＲＴＬ記述、ネットリスト、オブジェクトコードなどの生成までを、一貫して処理することができる。
【産業上の利用可能性】
【０１１６】
本発明の検証装置は、例えば、半導体回路設計において、動作合成又は論理合成に好適となるように、設計された記述を変更した場合に、変更の前後で同じ機能を有していることを検証するといった用途に適用できる。
【０１１７】
また、本発明の検証装置は、電子計算機用プログラムの設計においてコンパイラに好適になるようにプログラムを変更した場合に変更前後で同じ機能を要していることを検証するといった用途にも適用可能である。
【０１１８】
さらに、本発明の検証プログラムは、動作合成用ツールや論理合成ツールのようなハードウェア設計ツール、又はコンパイラなどのソフトウェア開発ツールの、付加機能として適用することができる。
【符号の説明】
【０１１９】
１００    コンピュータ
１０１    差分抽出手段
１０２    依存関係抽出手段
１０３    比較回路生成手段
１０４    等価性比較手段
２００    記憶手段
２０１    検証対象回路記憶部
２０２    差分回路記憶部
２０３    依存関係回路記憶部
２０４    比較回路記憶部
【図１】
2014120119.tif 000003
【図２】
2014120119.tif 000004
【図３】
2014120119.tif 000005
【図４】
2014120119.tif 000006
【図５Ａ】
2014120119.tif 000007
【図５Ｂ】
2014120119.tif 000008
【図５Ｃ】
2014120119.tif 000009
【図５Ｄ】
2014120119.tif 000010
【図６】
2014120119.tif 000011
【図７】
2014120119.tif 000012
【図８】
2014120119.tif 000013
【図９】
2014120119.tif 000014