(57)【特許請求の範囲】
【請求項１】
第１の記述と第２の記述間の等価性を、各記述についての検証対象信号線に関する論理コーンを比較することで検証する等価性検証システムにおいて、
前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出する中間コーン抽出手段と、
中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定する論理コーン比較部と、
前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化する中間点結果反映部とを備え、
前記中間点結果反映部は、前記論理コーンの簡単化では、前記中間コーンを、
２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、
ことを特徴とする等価性検証システム。
【請求項２】
第１の記述と第２の記述間の等価性を、各記述についての検証対象信号線に関する論理コーンを比較することで検証する等価性検証システムにおいて、
前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出する中間コーン抽出手段と、
中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定する論理コーン比較部と、
前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化する中間点結果反映部とを備え、
前記中間結果反映部は、前記論理コーンの簡単化では、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、
ことを特徴とする等価性検証システム。
【請求項３】
前記第１及び第２の記述が、それぞれ、ソフトウエア記述、又は、ハードウエア記述である、請求項１又は２に記載の等価性検証システム。
【請求項４】
前記等価条件を入力し前記等価条件記憶部に記憶する入力装置を更に備える、請求項１又は２に記載の等価性検証システム。
【請求項５】
前記第１の記述が動作記述であり、前記第２の記述がＲＴＬ（レジスタ転送レベル）記述である、請求項１又は２に記載の等価性検証システム。
【請求項６】
前記動作記述を動作合成して前記ＲＴＬ記述を生成する動作合成装置を更に備える、請求項５に記載の等価性検証システム。
【請求項７】
前記動作合成装置が、前記等価条件を等価条件記憶部に記憶する、請求項６に記載の等価性検証システム。
【請求項８】
前記第１の記述がＲＴＬ記述であり、前記第２の記述がゲートレベル記述である、請求項１又は２に記載の等価性検証システム。
【請求項９】
前記ＲＴＬ記述を論理合成して前記ゲートレベル記述を生成する論理合成装置を更に備える、請求項８に記載の等価性検証システム。
【請求項１０】
前記論理合成装置が、前記等価条件を等価条件記憶部に記憶する、請求項９に記載の等価性検証システム。
【請求項１１】
コンピュータを用いて、第１の記述と第２の記述との等価性を検証する方法であって、
前記コンピュータが、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、
前記コンピュータが、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、
前記コンピュータが、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、
前記コンピュータが、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを備え、
前記簡単化するステップでは、前記コンピュータは、前記中間コーンを、
２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、
ことを特徴とする方法。
【請求項１２】
コンピュータを用いて、第１の記述と第２の記述との等価性を検証する方法であって、
前記コンピュータが、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、
前記コンピュータが、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、
前記コンピュータが、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、
前記コンピュータが、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを備え、
前記簡単化するステップでは、前記コンピュータは、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、  
ことを特徴とする方法。
【請求項１３】
前記第１及び第２の記述が、それぞれ、ソフトウエア記述、又は、ハードウエア記述である、請求項１１又は１２に記載の方法。
【請求項１４】
前記コンピュータが、入力された等価条件を前記等価条件記憶部に記憶するステップを更に有する、請求項１１又は１２に記載の方法。
【請求項１５】
前記第１の記述が動作記述であり、前記第２の記述がＲＴＬ（レジスタ転送レベル）記述である、請求項１１又は１２に記載の方法。
【請求項１６】
前記コンピュータが、前記動作記述を動作合成して前記ＲＴＬ記述を生成するステップを更に備える、請求項１５に記載の方法。
【請求項１７】
前記ＲＴＬ記述を生成するステップでは、前記コンピュータは、前記等価条件を等価条件記憶部に記憶する、請求項１６に記載の方法。
【請求項１８】
前記第１の記述がＲＴＬ記述であり、前記第２の記述がゲートレベル記述である、請求項１１又は１２に記載の方法。
【請求項１９】
前記コンピュータが、前記ＲＴＬ記述を論理合成して前記ゲートレベル記述を生成するステップを更に備える、請求項１８に記載の方法。
【請求項２０】
前記ゲートレベル記述を生成するステップでは、前記コンピュータは、前記等価条件を等価条件記憶部に記憶する、請求項１９に記載の方法。
【請求項２１】
コンピュータに、第１の記述と第２の記述との等価性を検証させるプログラムであって、 前記コンピュータに、
前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、
中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、
前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、
前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを実行させるものであり、
前記簡単化するステップでは、前記中間コーンを、
２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、
ことを特徴とするプログラム。
【請求項２２】
コンピュータに、第１の記述と第２の記述との等価性を検証させるプログラムであって、 前記コンピュータに、
前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、
中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、
前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、
前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを実行させるものであり、
前記簡単化するステップでは、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、
ことを特徴とするプログラム。
【請求項２３】
前記第１及び第２の記述が、それぞれ、ソフトウエア記述、又は、ハードウエア記述である、請求項２１又は２２に記載のプログラム。
【請求項２４】
前記コンピュータに、入力された等価条件を前記等価条件記憶部に記憶するステップを更に実行させる、請求項２１又は２２に記載のプログラム。
【請求項２５】
前記第１の記述が動作記述であり、前記第２の記述がＲＴＬ（レジスタ転送レベル）記述である、請求項２１又は２２に記載のプログラム。
【請求項２６】
前記コンピュータに、前記動作記述を動作合成して前記ＲＴＬ記述を生成するステップを更に実行させる、請求項２５に記載のプログラム。
【請求項２７】
前記ＲＴＬ記述を生成するステップでは、前記等価条件を等価条件記憶部に記憶する、請求項２６に記載のプログラム。
【請求項２８】
前記第１の記述がＲＴＬ記述であり、前記第２の記述がゲートレベル記述である、請求項２１又は２２に記載のプログラム。
【請求項２９】
前記コンピュータに、前記ＲＴＬ記述を論理合成して前記ゲートレベル記述を生成するステップを更に実行させる、請求項２８に記載のプログラム。
【請求項３０】
前記ゲートレベル記述を生成するステップでは、前記等価条件を等価条件記憶部に記憶する、請求項２９に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、等価性検証システム、動作合成装置、方法、及び、プログラムに関し、更に詳しくは、２つの記述間の等価性を検証する等価性検証システム、方法、及び、プログラム、並びに、そのような等価性検証システムに使用する動作合成装置、方法、及び、プログラムに関する。
【背景技術】
【０００２】
近年、ＬＳＩ設計では、抽象度の高い動作記述から、動作合成システムによって論理合成可能なＲＴＬ（register-transfer level）記述を合成することがしばしば行われる。この設計手法では、抽象度の高い動作レベルでの設計を行うことで記述量を少なくすることができ、設計・検証の生産性を大きく向上させることが可能になる。動作記述には、例えばＣ言語を拡張した言語や、ＳｙｓｔｅｍＣ言語、或いは、ＳｐｅｃＣ言語などが用いられる。
【０００３】
一般に、動作合成システムはソフトウエアで構成されており、ソフトウエアである以上は、細心の注意を払っても、システム自体にバグが含まれる可能性を無くすことが困難である。動作合成の適用範囲の拡大に伴って、全ての検証やメンテナンスを、動作記述上で行う場合も現れつつあるが、動作合成システムのバグによって、誤ったＲＴＬ記述が生成されると、動作記述上で行った検証が無意味になるばかりではなく、後工程におけるリワークを発生させる原因ともなり得る。後工程におけるリワークの発生は、開発期間や工数の増大をもたらし、結果として大きな損失につながる。このような理由から、動作合成システムを実際のＬＳＩ設計に適用する際は、合成されたＲＴＬ記述の正しさを確認すること、すなわち、動作記述とＲＴＬ記述が等価であることを検証することが重要である。
【０００４】
動作記述とＲＴＬ記述との間の等価性検証は、所定のテストパターンを用いるシミュレーションによって行うことができる。しかしながら、テストパターンを用いたシミュレーションでは、テストパターン生成に膨大な時間及びコストを要することや、検証の網羅性がテストパターンに依存することから、十分な検証が行うことが難しいという問題がある。等価性検証の手法としては、形式的手法に基づく検証手法がある。形式的手法に基づく動作記述とＲＴＬ記述との等価性検証は、テストパターン等を用いることなく、入力である動作記述と動作合成システムが出力したＲＴＬ記述との等価性を、保証することができる。従って、合成された回路の正しさを確かめる上では、非常に有効な手法である。
【０００５】
従来の形式的手法に基づく動作記述とＲＴＬ記述の間の等価性検証システムの一例が非特許文献１に記載されている。図１５は、非特許文献１に記載された等価性検証システムの構成を示している。従来の等価性検証システム２００は、動作記述記憶部２０１と、動作合成装置２０２と、ＲＴＬ記述記憶部２０３と、モデル構築部２０４と、モデル記憶部２０５と、論理コーン抽出部２０６と、論理コーン記憶部２０７と、動作記述とＲＴＬ記述の対応関係を記憶する対応関係記憶部２０８と、論理コーン比較部２０９とから構成される。
【０００６】
図１６は、非特許文献１に記載された等価性検証システムの動作手順を示している。動作合成装置２０２は、動作記述記憶部２０１から動作記述を読み出して動作合成し（ステップＳ２１）、動作合成により得られたＲＴＬ記述をＲＴＬ記述記憶部２０３に格納する。モデル構築部２０４は、動作記述記憶部２０１に記憶された動作記述と、ＲＴＬ記述記憶部２０３に記憶されたＲＴＬ記述とを読み出し、動作記述とＲＴＬ記述とについて、それぞれ検証のためのモデルを構築する（ステップＳ２２）。検証モデルには、例えば、制御構造と信号値の変化とを表現できる拡張有限状態機械に基づくモデルなどがある。
【０００７】
動作合成装置２０２は、動作合成の際に生成した対応関係を、対応関係記憶部２０８に記憶する（ステップＳ２３）。この対応関係には、動作記述中の記述が、ＲＴＬ記述中のどの部分に変換されたかを示す情報や、動作記述中の変数とＲＴＬ記述中のレジスタとの対応関係が示す情報が含まれる。論理コーン抽出部２０６は、モデル記憶部２０５からステップＳ２２で構築されたモデルを読み出し、対応関係記憶部２０８からステップＳ２３で記憶された、前記２つのモデルから、項書換えやシンボリックシミュレーションなどによって、対応関係にある検証対象信号線の信号値に関する論理コーンを抽出し、論理コーン記憶部２０７に記憶する（ステップＳ２４）。論理コーンとは、実行系列における信号の変化を表す式である。
【０００８】
論理コーン比較部２０９は、論理コーン記憶部２０７から、ステップＳ２４で抽出された論理コーンを読み出し、検証対象信号線に関する２つの記述の論理コーンの比較を行う（ステップＳ２５）。論理コーン比較部２０９は、比較の結果、全ての実行系列に対して、全ての検証対象信号線に関する２つの記述の論理コーンが一致すると、動作記述とＲＴＬ記述が等価であると判断する。
【０００９】
従来の形式的手法に基づく動作記述とＲＴＬ記述の間の等価性検証システムに関する高速化技術としては、特許文献１に記載された技術がある。特許文献１では、動作合成装置が等価であると考えられる中間点のペアを指定し、論理検証装置がこれらの中間点が確かに等価であることを確認して、信号値関数を中間端子を用いて簡単化する。一般に、形式的等価性検証においては、信号値関数が複雑になることで比較に要する時間が増大する。特許文献１では、中間点の対応関係を用いて検証を分割することによって、検証を高速化する。
【００１０】
図１７は、特許文献１に記載された等価性検証システムの構成を示している。この等価性検証システム３００は、図１５に示す構成に加えて、中間コーン抽出部３０９、中間コーン記憶部３１０、中間点結果反映部３１１、中間点簡単化コーン記憶部３１２、及び、中間点結果記憶部３１４を有する。動作記述記憶部３０１〜対応関係記憶部３０８は、図１５における動作記述記憶部２０１〜対応関係記憶部２０８と対応し、論理コーン比較部３１３は、図１５における論理コーン比較部２０９に対応する。中間コーン抽出部３０９は、対応関係記憶部３０８を参照して、動作合成装置３０２が出力した対応関係から、等価であると考えられる中間点に関する中間コーンを抽出し、中間コーン記憶部３１０に記憶する。
【００１１】
特許文献１では、論理コーン比較部３１３は、検証対象信号線に関する論理コーンだけでなく、中間コーンに関する等価性の検証を行う。論理コーン比較部３１３は、中間コーンに関する等価性を検証し、中間コーンが等価である場合には、等価であるという結果を、中間点結果記憶部３１４に記憶する。中間点結果反映部３１１は、中間点結果記憶部３１４に等価である旨の結果が記憶された中間点が存在する場合には、検証対象信号線の信号値に関する論理コーンを、中間端子を用いて簡単化し、中間点簡単化コーン記憶部３１２に記憶する。論理コーン比較部３１３は、中間コーンが簡単化された論理コーンが中間点簡単化コーン記憶部３１２に記憶されているときには、その簡単化された論理コーン同士を比較して、動作記述とＲＴＬ記述の等価性を検証する。
【００１２】
図１８は、特許文献１に記載された等価性検証システムの動作手順を示している。動作合成から検証モデル構築、対応関係の取得、論理コーンの抽出までの動作は、図１６のステップＳ２１〜Ｓ２４までの動作と同様である（ステップＳ４０１〜Ｓ４０４）。論理コーンの抽出後、中間コーン抽出部３０９は、信号値関数に関して対応関係のある中間点があるか否かを調べ（ステップＳ４０５）、中間点が存在する場合には中間点に関する中間コーンを抽出する（ステップＳ４０６）。中間コーンが抽出されると、論理コーン比較部３１３は、中間点に関する中間コーンの比較を行う（ステップＳ４０７）。
【００１３】
論理コーン比較部３１３は、中間点が等価であるか否かを判断し（ステップＳ４０８）、等価である場合は、論理コーンを中間端子を用いて簡単化すべく、等価であるという結果を等価条件保持部に記憶する（ステップ４０９）。等価でない場合には、その中間点は簡単化できないため、特に処理を行わない。対応する中間点が他にあるか否かを調べ（ステップＳ４１０）、ある場合には、ステップＳ４０６へ戻り、全ての対応関係のある中間点に対して上記動作を繰り返し行う。
【００１４】
ステップＳ４１０で、対応する中間点がないと判断されると、中間点結果反映部３１１は、等価であった中間点に関しては、検証対象信号線に関する論理コーンを、中間端子を用いて簡単化する（ステップＳ４１１）。等価であると判定できなかった中間点に関しては簡単化は行わない。最後に、論理コーン比較部３１３は、検証対象信号線に関する論理コーンの比較を行う（ステップＳ４１２）。このとき、等価な中間点に関して簡単化されている場合には、中間点簡単化コーン記憶部３１２に記憶された、簡単化された論理コーンにて比較を行う。
【００１５】
【特許文献１】特開２００３−１４１２０２号公報
【非特許文献１】竹中  崇、他５名、“動作合成前後の動作記述とＲＴＬ記述の論理等価性検証”、第１７回回路とシステム（軽井沢）ワークショップ、２００４年、５５５〜５６０頁
【特許文献２】特開２０００−２５９６９６号公報
【発明の開示】
【発明が解決しようとする課題】
【００１６】
ところで、昨今の設計規模の増大は、当然の帰結として検証時間の増加をもたらしている。このため、動作合成装置の合成前後の記述間の等価性検証においても、一層の高速化の要求が高まっている。一方で、設計される回路が高速動作し、かつ、回路面積を小さくするため、回路のある一部分に着目し、その部分が参照される条件の下でのみ等価になるような最適化を、出力信号線の出力値に影響を与えない範囲で行う場合がある。
【００１７】
図１９（ａ）は、設計対象の回路部分の一例を示し、同図（ｂ）は、（ａ）と等価な回路部分を示している。同図（ａ）を参照すると、加算器ＡＤＤの入力であるマルチプレクサｍｕｘ１は、条件ｃ１が成立する場合にはｘを、条件ｃ２が成立する場合にはｙを、それ以外の場合にはｚを出力する。しかしながら、この回路の動作を解析すると、加算器ＡＤＤの出力にはマルチプレクサｍｕｘ２が接続されており、加算器ＡＤＤの出力ｏｕｔは、条件ｃ１又はｃ２が成立する場合に限り参照されることから、ｍｕｘ１がｚを出力する動作は、ｍｕｘ２の出力であるｏｕｔには影響を与えないことがわかる。従って、同図（ｂ）に示すように、マルチプレクサｍｕｘ１を、条件ｃ１が成立する場合にはｘを、それ以外の場合にはｙを出力するように変形しても、ｏｕｔの値は変形前と等価であるといえる。このように、回路の一部分と、その参照される条件に着目し、回路全体の出力に影響しない範囲で、着目した部分を、参照される条件下でのみ等価となる最適化を行うことで、より高速で面積の小さな回路を生成することができる。
【００１８】
上記最適化は、人手によって行われる場合があるのは無論のこと、昨今の動作合成システムにおいても、より高品質な合成結果を得るために、積極的に行われるようになりつつある。しかしながら、上記最適化は、動作記述とＲＴＬ記述との等価性検証においては、信号値に関する論理コーンを、等価と判定できる中間点において簡単化して検証を高速化する上での障害となり得る。以下、この点について説明する。
【００１９】
特許文献１に記載された技術では、動作合成装置が等価であると考えられる中間点のペアを指定し、論理検証装置がこれらの中間点が確かに等価であることを確認し、更に、信号値に関する論理コーンを中間端子を用いて簡単化する。この場合、例えば図１９（ａ）を動作記述から抽出された論理コーンと考え、同図（ｂ）をＲＴＬ記述から抽出された論理コーンと考えて、ｏｕｔの等価性を検証しようとすると、中間点としてｍｕｘ１の出力を選択したとしても、非等価であるため、この出力に関して簡単化することはできない。つまり、上記のような最適化が中間点に施された場合には、その中間点自体は非等価であるから中間端子として扱うことができない。その結果、高速な検証を行うことが困難となる。
【００２０】
ところで、このような課題を解決するための一見類似した技術として、特許文献２に記載された技術がある。特許文献２は、回路の一部を中間端子を用いて簡単化して検証する際に生じる問題を回避するための技術であり、回路の一部を中間端子を用いて簡単化する際に、２以上の中間端子のとりうる値について成立する条件を求め、その条件を考慮して、検証対象信号線の信号値の等価性を検証する。
【００２１】
特許文献２に記載の技術を、図２０（ａ）及び（ｂ）を用いて説明する。同図（ａ）に示す論理コーンでは、検証対象信号線ｏｕｔに対して、２つの中間信号線ｍｏｕｔ０、ｍｏｕｔ１が存在する。これら中間信号線は、回路接続状況を参照すると、設計上、同時には“１”にならない。この場合に、同図（ｂ）に示すように、中間信号線ｍｏｕｔ０、ｍｏｕｔ１を中間端子化して、単に、検証対象信号線ｏｕｔの検証を行うと、起こりえない組み合わせのｍｏｕｔ０とｍｏｕｔ１に対して検証を行うことで、検証に失敗することになる。特許文献２では、このような中間端子に、(mout0 xor mout1 == 1)なる条件式を設定する。検証対象信号線ｏｕｔの信号値は、この条件を考慮した上で、比較を進める。つまり、ｍｏｕｔ０とｍｏｕｔ１の値の組が、（０、１）と（１、０）の２通りの場合について信号値比較を行う。
【００２２】
特許文献２では、上記のようにして、２以上の中間端子のとりうる値に制約を加えて検証を行うことで、中間端子が実際にとりうる値の組だけを、検証対象として考慮することで、誤った検証結果を防いでいる。しかしながら、特許文献２では、中間点のとりうる値に対する制約を加え、２つ以上の中間端子に関して、特定の値の組の検証を省略させるのみである。すなわち、形式的検証では、複数の中間端子に対して何らの制約も存在しないとき、中間点の動作によって実際には起こり得ない値の組が検証対象信号線の論理コーンの比較で考慮され、誤った検証結果を出力する場合があるが、特許文献２に記載された技術では、このような誤検証の発生を回避すべく、中間点のとり得る値に対する制約を与え、２つ以上の中間端子に関して特定の値の組の検証を省略させるものである。しかし、本発明で課題とする、最適化されたために等価ではなくなった中間点について、このような条件が一般に存在するわけではない。したがって、このような条件を考慮することが可能となったとしても、非等価な中間点を等価であると確かめて、中間端子として扱うことが可能になるわけではない。
【００２３】
本発明は、上記従来技術の問題点を解消し、２つの記述が等価であることを検証する等価性検証を、効率的に行うことができる等価性検証システム、方法、及び、プログラムを提供することを目的とする。
【００２４】
また、本発明は、上記等価性検証システム、方法、及び、プログラムで使用される動作合成装置、方法、及び、プログラムを提供することを目的とする。
【課題を解決するための手段】
【００２５】
上記目的を達成するために、本発明の等価性検証システムは、第１の記述と第２の記述間の等価性を、各記述についての検証対象信号線に関する論理コーンを比較することで検証する等価性検証システムにおいて、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出する中間コーン抽出手段と、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定する論理コーン比較部と、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化する中間点結果反映部とを備え、前記中間点結果反映部は、前記論理コーンの簡単化では、前記中間コーンを、２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、ことを特徴とする。
また、本発明の等価性検証システムは、第１の記述と第２の記述間の等価性を、各記述についての検証対象信号線に関する論理コーンを比較することで検証する等価性検証システムにおいて、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出する中間コーン抽出手段と、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定する論理コーン比較部と、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化する中間点結果反映部とを備え、前記中間結果反映部は、前記論理コーンの簡単化では、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、ことを特徴とする。
【００２６】
本発明の等価性検証方法は、コンピュータを用いて、第１の記述と第２の記述との等価性を検証する方法であって、前記コンピュータが、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、前記コンピュータが、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、前記コンピュータが、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、前記コンピュータが、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを備え、前記簡単化するステップでは、前記コンピュータは、前記中間コーンを、２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、ことを特徴とする。
また、本発明の等価性検証方法は、コンピュータを用いて、第１の記述と第２の記述との等価性を検証する方法であって、前記コンピュータが、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、前記コンピュータが、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、前記コンピュータが、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、前記コンピュータが、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを備え、前記簡単化するステップでは、前記コンピュータは、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、ことを特徴とする。
【００２７】
本発明のプログラムは、コンピュータに、第１の記述と第２の記述との等価性を検証させるプログラムであって、前記コンピュータに、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを実行させるものであり、前記簡単化するステップでは、前記中間コーンを、２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換える、ことを特徴とする。
また、本発明のプログラムは、コンピュータに、第１の記述と第２の記述との等価性を検証させるプログラムであって、前記コンピュータに、前記第１及び第２の記述のそれぞれについて検証対象信号線に関する論理コーンを記憶する論理コーン記憶部を参照し、前記第１の記述と前記第２の記述についての論理コーンから、前記第１の記述と前記第２の記述とで対応関係にある中間信号線に関する中間コーンをそれぞれ抽出するステップと、中間コーンが参照される条件を示す等価条件を記憶した等価条件記憶部を参照し、前記抽出された中間コーンに対応して前記等価条件が記憶されているときには、該等価条件が成立する状況下で、前記第１の記述と前記第２の記述についての中間コーンを比較し等価か否かを判定するステップと、前記論理コーン比較部が等価であると判定すると、前記論理コーンのうちの中間コーンに対応する部分を簡単化するステップと、前記簡単化された論理コーンに基づいて、前記第１の記述と前記第２の記述との等価性を判断するステップとを実行させるものであり、前記簡単化するステップでは、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定する、ことを特徴とする。
【００２８】
本発明の等価性検証システム、方法、及び、プログラムでは、第１の記述と第２の記述とで対応する中間信号線（中間点）の中間コーンを比較する際に、等価条件記憶部に、その中間点が参照される条件が記憶されているときには、その条件が成立する条件下で、中間コーンを比較する。比較の結果、等価であると判定したときには、論理コーンのうちで、等価であると判定された中間コーン部分を簡単化する。このようにすることで、中間点に対して、回路全体の出力に影響しない範囲で、少なくともその中間点が参照される場合には等価になるような最適化が行われた場合についても、その中間コーンを簡単化することができ、論理コーンを小さくすることで、第１の記述と第２の記述との等価性の検証を、効率的に行うことができる。
しかも、本発明の等価性検証システム、方法、及び、プログラムでは、前記論理コーンの簡単化では、前記中間コーンを、２つの出力を有し、等価条件が成立する時は共通のコーンからそれぞれに同じ値を出力し、等価条件が成立しない時はそれぞれに異なる値を出力する論理コーンで置き換えることを特徴とする。或いは、前記論理コーンの簡単化では、前記中間コーンを、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとで、異なる中間端子に置き換え、前記第１の記述についての論理コーンと、前記第２の記述についての論理コーンとに、前記中間端子が前記等価条件が成立する条件下で等価である旨を設定することを特徴とする。このような簡単化を行うことにより、比較対象の論理コーンを小さくできる。
【００３０】
本発明の等価性検証システム、方法、及び、プログラムでは、前記第１及び第２の記述が、それぞれ、ソフトウエア記述、又は、ハードウエア記述である構成を採用できる。第１の記述と第２の記述との組み合わせとしては、双方がソフトウエア記述又はハードウエア記述である場合と、一方がソフトウエア記述、他方がハードウエア記述の場合とが考えられる。
【００３１】
本発明の等価性検証システムは、前記等価条件を入力し前記等価条件記憶部に記憶する入力装置を更に備える構成を採用できる。また、本発明の等価性検証方法及びプログラムでは、入力された等価条件を前記等価条件記憶部に記憶するステップを更に有する構成を採用できる。
【００３２】
本発明の等価性検証システム、方法、及び、プログラムでは、前記第１の記述が動作記述であり、前記第２の記述がＲＴＬ（レジスタ転送レベル）記述である構成を採用できる。この場合、等価性の検証では、ソフトウエア記述である動作記述と、ハードウエア記述であるＲＴＬ記述との等価性が検証される。
【００３３】
本発明の等価性検証システムは、前記動作記述を動作合成して前記ＲＴＬ記述を生成する動作合成装置を更に備える構成を採用できる。また、本発明の等価性検証方法及びプログラムは、前記動作記述を動作合成して前記ＲＴＬ記述を生成するステップを更に備える構成を採用できる。この場合、等価性の検証では、動作合成前後に対応する動作記述と、ＲＴＬ記述との等価性が検証される。
【００３４】
本発明の等価性検証システムでは、前記動作合成装置が、前記等価条件を等価条件記憶部に記憶する構成を採用できる。また、本発明の等価性検証方法及びプログラムは、前記ＲＴＬ記述を生成するステップでは、前記等価条件を等価条件記憶部に記憶する構成を採用できる。動作合成の際に得られた等価条件を等価条件記憶部に記憶し、その等価条件を等価性検証に利用することで、等価性検証の効率を上げることができる。
【００３５】
本発明の等価性検証システム、方法、及び、プログラムでは、前記第１の記述がＲＴＬ記述であり、前記第２の記述がゲートレベル記述である構成を採用できる。この場合、等価性の検証では、ハードウエア記述であるＲＴＬ記述と、同じくハードウエア記述であるゲートレベル記述との等価性が検証される。
【００３６】
本発明の等価性検証システムは、前記ＲＴＬ記述を論理合成して前記ゲートレベル記述を生成する論理合成装置を更に備える構成を採用できる。また、本発明の等価性検証方法及びプログラムは、前記ＲＴＬ記述を論理合成して前記ゲートレベル記述を生成するステップを更に備える構成を採用できる。この場合、等価性の検証では、論理合成前後に対応するＲＴＬ記述と、ゲートレベル記述との等価性が検証される。
【００３７】
本発明の等価性検証システムでは、前記論理合成装置が、前記等価条件を等価条件記憶部に記憶する構成を採用できる。また、本発明の等価性検証方法及びプログラムでは、前記ゲートレベル記述を生成するステップでは、前記等価条件を等価条件記憶部に記憶する構成を採用できる。論理合成の際に得られた等価条件を等価条件記憶部に記憶し、その等価条件を等価性検証に利用することで、等価性検証の効率を上げることができる。
【発明の効果】
【００４２】
本発明の等価性検証システム、方法、及び、プログラムでは、第１の記述と第２の記述とで対応する中間信号線（中間点）の中間コーンを比較する際に、等価条件記憶部に、その中間点が参照される条件が記憶されているときには、その条件が成立する条件下で、中間コーンを比較し、比較の結果、等価であると判定したときには、論理コーンのうちで、等価であると判定された中間コーン部分を簡単化する。このようにすることで、出力に影響しない範囲で中間部分が参照される条件下で等価になるような最適化が行われた部分についても、その中間コーンを簡単化することができ、比較の対象となる論理コーンを小さくすることで、第１の記述と第２の記述との等価性の検証を効率的に行うことができる。
【００４３】
本発明の動作合成装置、方法、及び、プログラムでは、動作合成の際に、回路出力に影響しない範囲で中間部分が参照される条件下で等価になるような最適化を行い、等価条件記憶部に、中間条件が参照される条件を記憶する。等価性検証装置がこの条件を参照することにより、動作合成と等価性検証とを連携させることができ、等価性検証の効率を上げることができる。
【発明を実施するための最良の形態】
【００４４】
以下、図面を参照し、本発明の実施の形態を詳細に説明する。図１は、本発明の第１実施形態の等価性検証システムの構成を示している。等価性検証システム１００は、等価性検証装置１０と、記憶装置２０と、動作合成装置１０２とを備える。等価性検証装置１０は、モデル構築部１０４、論理コーン抽出部１０６、中間コーン抽出部１０９、等価条件設定部１１２、中間点結果反映部１１３、及び、論理コーン比較部１１５を備える。記憶装置２０は、動作記述記憶部１０１、ＲＴＬ記述記憶部１０３、モデル記憶部１０５、論理コーン記憶部１０７、対応関係記憶部１０８、中間コーン記憶部１１０、等価条件記憶部１１１、中間点簡単化コーン記憶部１１４、中間点結果記憶部１１６、及び、条件付中間コーン記憶部１１７を備える。
【００４５】
動作記述記憶部１０１は、設計者が作成した動作レベル記述を記憶する。動作レベル記述には、Ｃ言語を拡張した言語や、ＳｙｓｔｅｍＣ言語、或いは、ＳｐｅｃＣ言語などを用いることができる。動作合成装置１０２は、動作レベル記述を動作合成して、ＲＴＬ記述を出力する。ＲＴＬ記述には、例えば、Ｖｅｒｉｌｏｇ−ＨＤＬ言語やＶＨＤＬ言語を用いることができる。ＲＴＬ記述記憶部１０３は、動作合成装置１０２が出力するＲＴＬ記述を記憶する。動作合成装置１０２は、動作合成の際に、入力である動作レベル記述と出力であるＲＴＬ記述について、両者間の対応関係及び等価条件を出力する。対応関係記憶部１０８及び等価条件記憶部１１１は、それぞれ動作合成装置１０２が出力する対応関係及び等価条件を記憶する。
【００４６】
対応関係記憶部１０８が記憶する対応関係は、動作合成過程における合成前後の記述の間の対応を示すものであり、動作記述中のどの記述がＲＴＬ記述のどの記述に変換されたかや、どの変数がどのレジスタに変換されたかといった情報を含む。また、等価であると考えられる中間端子の情報が含まれる。等価条件記憶部１１１が記憶する等価条件は、中間端子が等価となる条件を示しており、動作合成過程において、回路の一部分が参照される条件に着目し、回路全体の出力に影響しない範囲で、少なくとも着目した部分が参照される場合には等価となるような最適化を行った場合において、その参照される条件を示すものである。
【００４７】
モデル構築部１０４は、動作レベル記述及びＲＴＬ記述のそれぞれに基づいて、等価性検証装置１０内部で利用する検証用のモデルを構築する。構築するモデルの例としては、有限状態機械をベースとする、制御構造と信号値構造とを表現できるモデル等がある。モデル記憶部１０５は、モデル構築部１０４が構築したモデルを記憶する。論理コーン抽出部１０６は、モデル記憶部１０５が記憶する、動作レベル記述及びＲＴＬ記述のそれぞれについて構築されたモデルと、対応関係記憶部１０８が記憶する対応関係とを入力し、それぞれのモデルから、対応関係にある検証対象信号線の信号値に関する論理コーンを抽出する。論理コーン記憶部１０７は、論理コーン抽出部１０６が抽出した論理コーンを記憶する。
【００４８】
中間コーン抽出部１０９は、論理コーン記憶部１０７が記憶する論理コーンと、対応関係記憶部１０８が記憶する対応関係とを入力し、対応関係の中の等価であると考えられる中間点の情報に基づいて、論理コーンから、中間点の信号値に関する中間コーンを抽出する。この中間コーンの抽出は、論理コーン内の中間点に関する対応関係が存在するときに行われる。また、中間コーン抽出部１０９自体が、等価であると考えられる中間点を推定して抽出してもよい。中間コーン記憶部１１０は、中間コーン抽出部１０９が抽出した中間コーンを記憶する。等価条件設定部１１２は、中間コーン記憶部１１０に保持された中間コーンと等価条件記憶部１１１に保持された等価条件とを入力し、中間コーンが等価条件の下でのみ等価になる場合は、その等価条件を、中間コーンが等価になる前提条件として対応付ける。条件付中間コーン記憶部１１７は、等価条件設定部１１２によって等価条件が付された中間コーンを記憶する。
【００４９】
論理コーン比較部１１５は、動作レベル記述とＲＴＬ記述との間で対応関係にある２つのコーンを比較し、それらが等価であるかを検証する。すなわち、検証対象信号線に関する論理コーン、中間点に関する中間コーン、等価条件が付された中間コーン、又は、その中間点に関して簡単化された論理コーン若しくは中間コーンの比較を行う。中間点に関する中間コーンについて比較を行う場合であって、等価条件が与えられている場合には、等価条件を前提条件として中間コーンが等価であるかどうかを比較する。すなわち、等価条件をcnd、動作記述側の中間コーンが表す信号値関数をm(sig1, sig2,…,sign)、ＲＴＬ記述側の中間コーンが表す信号値関数をm’(sig1’, sig2’,…,sign’)とすると、cnd→(((sig1 == sig1’) ∧ (sig2 == sig2’) ∧ … ∧(sign == sign’)) → (m(sig1, sig2,…,sign) == m’(sig1’, sig2’,…,sign’)))なる判定式が成立するか否かを調べる。
【００５０】
論理コーン比較部１１５は、中間点に関し、等価条件が与えられていない場合には、条件を考慮せず、動作記述とＲＴＬ記述とで中間コーンが一致するか否かを比較する。中間コーンに対して、さらにその中間点に関する対応関係が存在して比較が行われ、一致することが確認できている場合には、その中間点に関して簡単化するなどしてから比較を行ってもよい。論理コーン比較部１１５は、検証対象信号線に関する論理コーン又は中間点に関して簡単化されたコーンに関する比較である場合は、比較結果を出力する。中間コーンに関する比較であって、一致することが確認できた場合には、比較結果を、中間点結果記憶部１１６に記憶する。このとき、等価条件を付された中間コーンである場合には、その等価条件についても合わせて記憶する。
【００５１】
中間点結果反映部１１３は、中間点結果記憶部１１６に記憶された中間コーンに対する比較結果に基づき、動作記述とＲＴＬ記述との中間コーンの一致が確認できている場合には、その中間点を含む論理コーンを、論理コーン記憶部１０７から読み出して簡単化する。中間点結果反映部１１３は、中間点に等価条件が付されていない場合で、中間点が一致するという比較結果が得られている場合は、中間点に関する論理コーンを、中間端子を用いて簡単化する。等価条件が付された中間点に関しては、等価条件が成立する場合には、動作記述とＲＴＬ記述で同じ値を出力し、成立しない場合には、異なる値を返す共通のコーンで置き換える。或いは、その中間点を動作記述とＲＴＬ記述で異なる中間端子を用いて論理コーンを簡単化すると共に、等価条件の下で２つの中間端子が等しくなる、という前提条件を論理コーンに付加してもよい。すなわち、等価条件が付された中間点を含む検証対象信号線の検証においては、中間信号線の等価条件をcnd、動作記述側の中間端子をx、ＲＴＬ記述側の中間端子をx’とし、動作記述側の論理コーンが表す信号値関数とＲＴＬ記述側の論理コーンが表す信号値関数を、中間端子を用いてそれぞれf(sig1, sig2,…,sign, x)、f’(sig1’, sig2’,…,sign’,x’)とすると、(cnd→(x == x’))→(((sig1 == sig1’) ∧ (sig2 == sig2’) ∧ … ∧(sign == sign’)) → (f(sig1, sig2,…,sign, x)== f’(sig1’, sig2’,…,sign’,x’)))なる判定式が成立するか否か検査してもよい。なお、等価条件は、一般に、中間点のとり得る値に制約を与えるものではないことに注意する。中間点簡単化コーン記憶部１１４は、中間点結果反映部１１３によって簡単化された論理コーンを記憶する。
【００５２】
図２は、等価性検証システムの動作手順を示している。ユーザは、動作記述を作成し、動作記述記憶部１０１に記憶しておく。動作合成装置１０２は、動作記述記憶部１０１から動作記述を読み出して動作合成を行い、動作合成により得られたＲＴＬ記述をＲＴＬ記述記憶部１０３に記憶する（ステップＡ１）。動作合成が終了すると、等価性検証装置１０が起動する。モデル構築部１０４は、動作記述記憶部１０１に記憶された動作記述と、ＲＴＬ記述記憶部１０３に記憶されたＲＴＬ記述とを読み出し、それぞれについて、検証のためのモデルを構築する（ステップＡ２）。モデル構築部１０４は、検証モデルを構築すると、構築した検証モデルを、モデル記憶部１０５に記憶する。
【００５３】
動作合成装置１０２は、動作合成の際に得られた、動作記述とＲＴＬ記述との対応関係、及び、中間信号線が等価となるべき条件を、それぞれ対応関係記憶部１０８及び等価条件記憶部１１１に記憶する。論理コーン抽出部１０６は、対応関係記憶部１０８から対応関係を読み出し（ステップＡ３）、モデル記憶部１０５から、ステップＡ２で構築された検証用のモデルを読み出して、対応関係に基づいて、検証対象信号線の信号値に関する論理コーンを抽出する（ステップＡ４）。論理コーン抽出部１０６は、抽出した論理コーンを、論理コーン記憶部１０７に記憶する。
【００５４】
中間コーン抽出部１０９は、論理コーン記憶部１０７に記憶された論理コーンと、対応関係記憶部１０８に記憶された対応関係とを参照し、論理コーンの中間信号線に対する対応関係が存在するか否かを判断する（ステップＡ５）。中間コーン抽出部１０９は、論理コーンの中間信号線に対する対応関係が存在する場合には、その対応関係に基づいて、中間信号線に関する中間コーンを抽出する（ステップＡ６）。中間コーン抽出部１０９は、抽出した中間コーンを、中間コーン記憶部１１０に記憶する。等価条件設定部１１２は、等価条件記憶部１１１を参照して、ステップＡ６で抽出された中間コーンに対して、等価条件が存在するか否かを検査する（ステップＡ７）。等価条件設定部１１２は、等価条件が存在する場合には、中間コーンについて、等価条件を設定し（ステップＡ８）、条件付中間コーン記憶部１１７に記憶する。
【００５５】
論理コーン比較部１１５は、中間コーン記憶部１１０又は条件付中間コーン記憶部１１７を参照し、動作記述とＲＴＬ記述とで対応関係にある中間コーンの比較を行う（ステップＡ９）。この比較では、ステップＡ７で等価条件設定部１１２によって等価条件が設定されている場合には、その等価条件を条件付中間コーン記憶部１１７から読み出して、読み出した等価条件を前提条件として与えた上で、中間コーンの等価性を検証する。また、等価条件が設定されていない場合には、特に条件を考慮することなく、中間コーンの等価性を検証する。中間コーンについて、更に、その中間点に関して比較が行われている場合は、その結果に基づいて、中間コーンを簡単化してから比較を行ってもよい。
【００５６】
論理コーン比較部１１５は、中間コーンの等価性検証の結果、中間点が等価であるか否かを判断する（ステップＡ１０）。中間点が等価である場合には、その結果を、中間点結果記憶部１１６に記憶する（ステップＡ１１）。ステップＡ１１では、等価である中間点が、ステップＡ７で等価条件が設定された中間コーンに対応するものであれば、その等価条件も合わせて記憶する。中間点が等価ではないと判断された場合には、その中間点を中間端子等に置き換える等の簡単化はできないため、特に処理は行わない。
【００５７】
中間コーン抽出部１０９は、中間点に関する対応関係が他にも存在するか否かを判断する（ステップＡ１２）。存在する場合には、ステップＡ６に戻って、中間コーンの抽出を行う。全ての中間点に関する対応関係について、ステップＡ６〜Ａ１１までの処理を行うと、中間点結果反映部１１３は、中間点結果記憶部１１６を参照して、検証対象信号線の信号値に関する論理コーンを、中間点の比較結果に基づいて簡単化する（ステップＡ１３）。この簡単化では、等価条件が設定されていない中間点については、中間点に関する中間コーンを、中間端子を用いて簡単化する。等価条件が設定されている場合には、条件が成立する場合に等価になるような共通のコーンで置き換えるなどして簡単化する。中間点結果反映部１１３は、中間点を簡単化した論理コーンを、中間点簡単化コーン記憶部１１４に記憶する。
【００５８】
最後に、論理コーン比較部１１５は、検証対象信号線に対する動作記述の論理コーンと、ＲＴＬ記述の論理コーンとを比較する（ステップＡ１４）。ステップＡ１４では、ステップＡ５で対応する中間点が存在しないと判断された場合や、ステップＡ１３で何れの中間点についても中間コーンが簡単化されなかった場合には、論理コーン記憶部１０７に記憶された論理コーンを参照して、比較を行う。また、ステップＡ１３で、中間点について、何らかの簡単化がされている場合には、中間点簡単化コーン記憶部１１４に記憶された論理コーンを参照して、比較を行う。
【００５９】
以下、具体例を用いて説明する。図３は、動作記述記憶部１０１に記憶された動作記述の具体例を示している。この動作記述では、“ｍｏｄｅ＿ｉｎ”、“ｉｎ０”、“ｉｎ１”は入力信号線を表し、“ｏｕｔ０”は出力信号線を表している。この動作記述の動作は、まず、ｍｏｄｅ＿ｉｎの値をｍｏｄｅに保持し、ｍｏｄｅの値に応じて参照する配列ａｒｙの要素ａｄｒを決定する。続いて、ｍｏｄｅの値に応じて、出力信号線ｏｕｔ０へ出力する値を決定する。出力される値は、先の動作で参照することが決定された配列ａｄｒの値、又は、定数値の何れかである。
【００６０】
動作合成装置１０２は、上記動作記述を入力して、動作合成処理を行う。図４は、図３に示す動作記述を動作合成して得られたＲＴＬ記述の具体例を示している。図３に示す動作記述における出力信号線（変数）ｏｕｔ０は、動作合成後のＲＴＬ記述（図４）では、同名の出力信号線ｏｕｔ０に対応する。また、動作記述における出力信号線ｏｕｔ０に関する中間信号線ａｄｒは、ＲＴＬ記述では、同名の中間信号線ａｄｒに対応する。図３を参照すると、ａｄｒは、配列ａｒｙの要素を指定するが、ａｒｙは、ｍｏｄｅの値が０又は１の場合にのみ参照される。ｍｏｄｅが０の場合には、ａｄｒにはｉｎ０が、ｍｏｄｅが１の場合にはａｄｒにはｉｎ１が代入されるため、ａｄｒに対する０の代入は、ｏｕｔ０の出力値に影響を与えることはない。このため、動作合成後のＲＴＬ記述では、ａｄｒに０が代入される場合が除去され、ｍｏｄｅが０でない場合には常にｉｎ１を代入するような最適化が施されている。
【００６１】
動作合成装置１０２は、動作合成によりＲＴＬ記述を生成すると、生成したＲＴＬ記述を出力すると共に、動作記述とＲＴＬ記述との間の入出力信号線又は中間信号線に関する対応関係と、対応関係にある中間信号線が等価になる条件を出力する。動作合成により得られたＲＴＬ記述は、ＲＴＬ記述記憶部１０３に記憶される。また、動作合成の際に得られた対応関係及び等価条件は、それぞれ、対応関係記憶部１０８及び等価条件記憶部１１１に記憶される。具体的には、対応関係記憶部１０８には、出力信号線ｏｕｔ０及び中間信号線ａｄｒに関する対応関係が記憶される。また、ＲＴＬ記述（図４）では、中間信号線ａｄｒがｍｏｄｅの値が０又は１の場合に参照されることを条件に最適化がされているため、等価条件記憶部１１１には、中間信号線ａｄｒについて、この条件（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１）が等価条件として記憶される。
【００６２】
動作合成装置１０２によって、ＲＴＬ記述、対応関係、及び、等価条件が出力されると、等価性検証装置１０が起動して、動作記述とＲＴＬ記述との等価性の検証が開始される。モデル構築部１０４は、動作記述とＲＴＬ記述とについて、それぞれに対応する検証モデルを構築する。その後、論理コーン抽出部１０６は、構築された動作合成前後の検証モデルのそれぞれから、検証対象信号に関する論理コーンを抽出する。対応関係記憶部１０８には、出力信号線ｏｕｔ０が、動作記述とＲＴＬ記述とで対応する出力信号線である旨が記憶されており、論理コーン抽出部１０６は、出力信号線ｏｕｔ０についての論理コーンを抽出する。抽出された論理コーンの具体例を、図５に示す。同図（ａ）は、動作記述（図３）に対応する論理コーンを示し、同図（ｂ）は、ＲＴＬ記述（図４）に対応する論理コーンを示している。
【００６３】
ステップＡ５（図２）で、対応する中間点があるか否かを調べると、対応関係記憶部１０８には、動作記述とＲＴＬ記述について、中間信号線ａｄｒが、双方の記述で対応関係にある中間信号線として記憶されている。このため、ステップＡ６に移行して中間コーン抽出部１０９により、動作記述に対応する論理コーン（図５（ａ））及びＲＴＬ記述に対応する論理コーン（図５（ｂ））から、中間信号線ａｄｒに対する論理コーンが、それぞれ中間コーンとして抽出される。これら抽出された中間コーンは、中間コーン記憶部１１０に記憶される。抽出された中間コーンを図６に示す。同図（ａ）は、動作記述の論理コーンから抽出された中間コーンを示し、同図（ｂ）は、ＲＴＬ記述の論理コーンから抽出された中間コーンを示している。
【００６４】
ステップＡ７で、中間点に等価条件が付されているか否かを調べると、対応関係記憶部１０８には、ステップＡ５で対応すると判断された中間信号線ａｄｒについて、この中間点が等価になる条件として、（（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１））が記憶されている。このため、ステップＡ８へ移行して、等価条件設定部１１２により、抽出された中間コーン及び等価条件が、条件付中間コーン記憶部１１７に記憶される。ステップＡ９では、論理コーン比較部１１５により、等価条件設定部１１２によって設定された（（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１））という条件が成立する下で、中間信号線ａｄｒについて、動作記述に対応すする中間コーン（図６（ａ））と、ＲＴＬ記述に対応する中間コーン（図６）との等価性を検証する。
【００６５】
前述のように、中間信号線ａｄｒについての動作記述に対応する中間コーンと、ＲＴＬ記述に対する中間コーンとでは、動作合成の際の最適化の動作により、常に等価な動作とはならないため、単純に中間コーンを比較する場合には、等価とは判定されない。しかしながら、設定された等価条件の下で中間コーンを比較する場合には、等価であると判定される。ステップＡ９で設定された条件下で中間コーンを比較することにより、ステップＡ１０では、中間点は等価であると判断される。このため、ステップＡ１１に移行して、中間信号線ａｄｒが等価である旨が、中間点結果記憶部１１６に記憶される。
【００６６】
中間信号線に関する中間コーンの等価性の検証が終わると、ステップＡ１３で、検証対象信号線ｏｕｔ０の信号値に関する論理コーンについて、等価であると判断された中間コーン部分を簡単化する。図７及び図８は、中間コーンの簡単化の具体例を示している。これらの例では、動作記述に対する論理コーンと、ＲＴＬ記述に対する論理コーンとにおける中間信号線ａｄｒについての中間コーンを、共通の論理コーンＣ１で、置き換えている。この共通の論理コーンＣ１は、（（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１））という条件が成立する場合には、ｍｏｄｅの値に応じてｉｎ０又はｉｎ１を出力する（図７）。或いは、図８に示すように、単に中間端子として取り扱ってもよい。また、条件不成立の場合には、動作記述に対する論理コーンに対して、中間端子ａｄｒbehavioralを出力し、ＲＴＬ記述に対する論理コーンに対して、中間端子ａｄｒRTLを出力する。
【００６７】
中間コーンの簡単化では、上記に代えて、等価であると判定できた中間信号線については動作記述とＲＴＬ記述で異なる中間端子として扱ったうえで、等価条件の下でそれぞれの中間端子が等価になるという条件を前提条件として論理コーンに付加してもよい。この簡単化の例を図９に示す。この例では、動作記述に対する論理コーン（同図（ａ））における信号線ａｄｒの中間コーンを、中間端子ａｄｒbehavioralで置き換え、ＲＴＬ記述に対する論理コーン（同図（ｂ））における信号線ａｄｒの中間コーンを、中間端子ａｄｒRTLで置き換える。そのうで、２つの記述の中間端子が（（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１））という条件で等価になることを示す（（ｍｏｄｅ＝＝０）∨（ｍｏｄｅ＝＝１））→（ａｄｒｂｅｈａｖｉｏｒａｌ＝＝ａｄｒＲＴＬ）という条件を、論理コーンの前提条件として設定する。
【００６８】
最後に、ステップＡ１４で、論理コーン比較部１１５により、検証対象信号線ｏｕｔ０の論理コーンを比較する。この比較では、中間点簡単化コーン記憶部１１４に記憶された、図７又は図９に示すような中間信号線ａｄｒの中間コーンが簡単化された論理コーンを用いて、検証対象信号線ｏｕｔ０の等価性を検証する。この検証では、動作記述とＲＴＬ記述のそれぞれについて中間信号線ａｄｒの中間コーンは参照されず、簡単化された論理コーンにて、検証対象信号線ｏｕｔ０の比較を行うことができる。このように、比較対象となる個々の論理コーンを小さくすることができるため、効率的にｏｕｔ０が等価であることを確認することができる。
【００６９】
動作合成で、回路の部分が参照される特定の条件においてのみ論理的に等価になるような最適化が施された部分については、その回路部分が参照される特定の条件を等価性検証時に前提条件として与えることで、その回路部分の動作記述とＲＴＬ記述が、その条件の下では等価となることを判定することは可能である。動作合成装置１０２は、その回路部分が参照される条件を把握した上で最適化を行うわけであるから、その条件はその内部に保持しており、その条件を等価性検証装置１０に提供することは可能である。等価性検証装置１０は、提供された等価条件を参照することにより、動作記述とＲＴＬ記述との等価性を検証する際に、信号値に関する論理コーンを等価と判定できる中間点について簡単化しようとするに当たって、中間点が参照される条件下でのみ等価になるような最適化が施されていたか否かを知ることができる。
【００７０】
等価性検証装置１０は、ある信号値に関する論理コーンにおける中間点が特定の条件においてのみ参照されることに着目して、その条件下でのみ等価になる最適化がされる場合については、その条件が成立する場合に中間点が等価になることを確認する。等価である場合には、例えば、その条件の下では同じ値を表すような共通のコーンで置き換えることで論理コーンの簡単化を行う。このようにすることで、回路の部分が参照される特定の条件においてのみ論理的に等価になるような最適化が施され、従来では等価であると判定できなかった中間点についても中間コーンを簡単化することができ、検証対象となる個々の論理コーンを小さくすることができる。このため、動作記述とＲＴＬ記述の間の等価性を、従来と比較して高速かつ少ない記憶域で行うことができる。
【００７１】
本実施形態では、動作合成装置１０２は、合成の際に利用した中間点が参照される条件を等価条件として等価条件記憶部１１１に記憶する。この等価条件は、一般には容易に知ることができない場合があるが、上述のように、動作合成装置１０２が合成情報の一環として持っているものであり、等価性検証装置１０に提供できる。動作合成装置１０２と等価性検証装置１０とを密接に連携させ、等価性の検証にこの情報を利用することで、等価性検証の効率を向上させることができる。
【００７２】
図１０は、本発明の第２実施形態の等価性検証システムの構成を示している。本実施形態の等価性検証システム１００ａは、動作合成装置１０２（図１）に代えて、入力装置１１８を用いる点で、第１実施形態と相違する。本実施形態では、ユーザ（設計者）は、入力装置１１８を用いて、動作記述記憶部１０１に動作記述を記憶させ、ＲＴＬ記述記憶部１０３に、動作記述に基づいて設計したＲＴＬ記述を記憶させる。また、対応関係及び等価条件を、入力装置１１８を用いて、それぞれ対応関係記憶部１０８及び等価条件記憶部１１１に記憶させる。対応関係については、モデル構築部１０４がモデルを構築する際に、動作記述とＲＴＬ記述とにおける信号線名や記述に付加された情報から推測して得てもよい。
【００７３】
図１１は、本実施形態の等価性検証システムの動作手順を示している。設計者は、入力装置１１８により、動作記述、動作記述に基づいて作成されたＲＴＬ記述、及び、動作記述とＲＴＬ記述との対応関係を入力する（ステップＢ１）。ステップＢ１では、ＲＴＬ記述において、参照される条件で最適化を行った場合には、等価となるべき条件をあわせて入力する。その後、図２のステップＡ２〜Ａ１４と同様な手順で、対応する中間点について、等価条件が設定されている場合には、その等価条件を考慮して、中間コーン部分を簡単化し、中間コーンを簡単化した論理コーンを用いて、動作記述とＲＴＬ記述との等価性を検証する（ステップＢ２〜Ｂ１４）。
【００７４】
本実施形態では、動作合成装置が等価条件を出力しない場合や、ＲＴＬ記述を人手で直接最適化した場合、或いは、動作記述から人手でＲＴＬ記述を作成した場合など、出力に影響しない範囲で、回路部分が参照される条件下でのみ等価となるような最適化が行われ、かつ、動作合成装置から等価条件を得ることが不可能な場合についても、必要な条件を入力装置１１８から与えることにより、最適化された部分についても中間コーンを簡単化できる。従って、そのような場合でも、等価性の検証の効率化を図ることができる。
【００７５】
図１２は、本発明の第３実施形態の等価性検証システムの構成を示している。本実施形態の等価性検証システム１００ｂは、動作合成装置１０２（図１）に代えて、論理合成装置１１９を用いる点で、第１実施形態と相違する。本実施形態では、記憶装置２０ｂは、ゲートレベル記述記憶部１２０を有する。ＲＴＬ記述記憶部１０３は、設計者が記述するなどして得られたＲＴＬ記述を記憶する。論理合成装置１１９は、ＲＴＬ記述記憶部１０３からＲＴＬ記述を読み出し、読み出したＲＴＬ記述に対して論理合成を行う。論理合成装置１１９は、論理合成により得られたゲートレベル記述を、ゲートレベル記述記憶部１２０に記憶すると共に、等価条件記憶部１１１に、中間信号線が等価になるべき条件を記憶する。
【００７６】
モデル構築部１０４は、ＲＴＬ記述とゲートレベル記述とについて、検証のためのモデルを構築すると共に、２つの記述の信号線名や記述に付加された情報などから、２つの記述間の対応関係を決定する。モデル構築後の等価性検証装置１０の動作は、検証対象がＲＴＬ記述とゲートレベル記述との等価性に代わる点を除いて、第１実施形態で説明した検証の手順と同様である。
【００７７】
本実施形態では、論理合成前後のＲＴＬ記述とゲートレベル記述との間の等価性検証で、論理合成時に、出力に影響しない範囲で回路部分が参照される条件の下でのみ等価となるような最適化が行われた場合についても、論理合成装置から最適化に関する条件を取得することによって、中間コーンを簡単化できる。このため、ＲＴＬ記述とゲートレベル記述との等価性の検証を効率よく行うことができる。
【００７８】
図１３は、本発明の第４実施形態の等価性検証システムの構成を示している。本実施形態の等価性検証システム１００ｃは、記憶装置２０ｃが第１ハードウエア記述記憶部１２１と第２ハードウエア記述記憶部１２２とを備える点で、第２実施形態の等価性検証システム１００ａ（図１０）と相違する。第１及び第２ハードウエア記述記憶部１２１、１２２には、それぞれ、例えばアルゴリズムや実現すべきハードウエアを機能で記述したハードウエア記述が記憶される。ハードウエア記述には、例えば、ＲＴＬ記述又はゲートレベル記述がある。例えば、第１及び第２ハードウエア記述記憶部１２１、１２２の双方には、ＲＴＬ記述又はゲートレベル記述が記憶される。或いは、何れか一方にＲＴＬ記述が記憶され、他方にはゲートレベル記述が記憶される。これらＲＴＬ記述やゲートレベル記述は、入力装置１１８により入力される。
【００７９】
本実施形態では、等価性検証装置１０は、モデル構築部１０４によって、第１ハードウエア記述記憶部１２１に記憶されたハードウエア記述と、第２ハードウエア記述記憶部１２２に記憶されたハードウエア記述について、検証用のモデルをそれぞれ生成し、そのモデルを用いて、２つのハードウエア記述間の等価性を検証する。本実施形態では、ハードウエア記述について、出力に影響しない範囲で回路部分が参照される条件の下でのみ等価となるような最適化が行われた場合についても、最適化に関する条件を人手で直接与えることによって、中間コーンを簡単化することができ、最適化の前後において、ハードウエア記述が等価であるか否かを、効率よく検証することができる。
【００８０】
図１４は、本発明の第５実施形態の等価性検証システムの構成を示している。本実施形態の等価性検証システム１００ｄは、記憶装置２０ｄが、第１ソフトウエア記述記憶部１２３と第２ソフトウエア記述記憶部１２４とを備える点で、第４実施形態と相違する。第１及び第２ソフトウエア記述記憶部１２３、１２４には、それぞれ、ソフトウエア記述が記憶される。ソフトウエア記述は、例えばアルゴリズムや実現すべきハードウエアを動作で記述したものである。或いは、ドライバ、オペレーティングシステム、各種アプリケーション等を何らかのプログラム言語で記述したものであってもよい。ソフトウエア記述は、入力装置１１８により入力される。等価性検証装置１０は、モデル構築部１０４は、第１ソフトウエア記述記憶部１２３に記憶されたソフトウエア記述と、第２ソフトウエア記述記憶部１２４に記憶されたソフトウエア記述について、検証用のモデルをそれぞれ生成し、そのモデルを用いて、２つのソフトウエア記述間の等価性を検証する。
【００８１】
入力である記述が２つのソフトウエア記述であっても、モデル構築部１０４によって、制御構造や変数値の変化を表現できるモデルなどを用いて検証のためのモデルを構築し、そのモデルから、変数値の関数に関する論理コーンを抽出することによって、２つのソフトウエア記述間の等価性を検証することができる。ソフトウエア記述においても、出力に影響しない範囲で、部分の記述が参照される条件が成立する場合に等価となるような最適化を施すことによって、動作の高速化やオブジェクトコードの小型化が期待できることから、この最適化はハードウエア記述に限られるものではない。本実施形態では、２つのソフトウエア記述の等価性を検証する場合に、結果の出力に影響しない範囲で、参照される条件下でのみ等価となるような最適化がなされた中間点を等価として扱うことにより、検証の効率化を図ることができる。
【００８２】
以上、本発明をその好適な実施形態に基づいて説明したが、本発明の等価性検証システム、動作合成装置、方法、及び、プログラムは、上記実施形態例にのみ限定されるものではなく、上記実施形態の構成から種々の修正及び変更を施したものも、本発明の範囲に含まれる。
【産業上の利用可能性】
【００８３】
本発明は、動作記述とＲＴＬ記述の間の等価性をはじめとする、２つのハードウエア記述又はソフトウエア記述の等価性を形式的に検証する等価性検証装置に適用できる。
【図面の簡単な説明】
【００８４】
【図１】本発明の第１実施形態の等価性検証システムの構成を示すブロック図。
【図２】第１実施形態の等価性検証システムの動作手順を示すフローチャート。
【図３】動作記述記憶部１０１に記憶された動作記述の具体例を示す図。
【図４】図３に示す動作記述を動作合成して得られたＲＴＬ記述の具体例を示す図。
【図５】（ａ）及び（ｂ）は、それぞれ出力信号線ｏｕｔ０についての論理コーンを示す図。
【図６】（ａ）及び（ｂ）は、それぞれ論理コーンから抽出された中間コーンを示す図。
【図７】中間コーンの簡単化の具体例を示す図。
【図８】中間コーンの簡単化の別の具体例を示す図。
【図９】（ａ）及び（ｂ）は、それぞれ中間コーンの簡単化の別の具体例を示す図。
【図１０】本発明の第２実施形態の等価性検証システムの構成を示すブロック図。
【図１１】第２実施形態の等価性検証システムの動作手順を示すフローチャート。
【図１２】本発明の第３実施形態の等価性検証システムの構成を示すブロック図。
【図１３】本発明の第４実施形態の等価性検証システムの構成を示すブロック図。
【図１４】本発明の第５実施形態の等価性検証システムの構成を示すブロック図。
【図１５】非特許文献１に記載された等価性検証システムの構成を示すブロック図。
【図１６】非特許文献１に記載された等価性継承システムの動作手順を示すフローチャート。
【図１７】特許文献１に記載された等価性検証システムの構成を示すブロック図。
【図１８】特許文献１に記載された等価性検証システムの動作手順を示すフローチャート。
【図１９】（ａ）は、設計対象の回路部分の一例を示し、（ｂ）は、（ａ）と等価な回路部分を示すブロック図。
【図２０】動作検証に用いられる論理コーンを示す図。
【符号の説明】
【００８５】
１０：等価性検証装置
２０：記憶装置
１００：等価性検証システム
１０１：動作記述記憶部
１０２：動作合成装置
１０３：ＲＴＬ記述記憶部
１０４：モデル構築部
１０５：モデル記憶部
１０６：論理コーン抽出部
１０７：論理コーン記憶部
１０８：対応関係記憶部
１０９：中間コーン抽出部
１１０：中間コーン記憶部
１１１：等価条件記憶部
１１２：等価条件設定部
１１３：中間点結果反映部
１１４：中間点簡単化コーン記憶部
１１５：論理コーン比較部
１１６：中間点結果記憶部
１１７：条件付中間コーン記憶部
１１８：入力装置
１１９：論理合成装置
１２０：ゲートレベル記述記憶部
１２１、１２２：ハードウエア記述記憶部
１２３、１２４：ソフトウエア記述記憶部
【図１】
0004784368.tif 000002
【図２】
0004784368.tif 000003
【図３】
0004784368.tif 000004
【図４】
0004784368.tif 000005
【図５】
0004784368.tif 000006
【図６】
0004784368.tif 000007
【図７】
0004784368.tif 000008
【図８】
0004784368.tif 000009
【図９】
0004784368.tif 000010
【図１０】
0004784368.tif 000011
【図１１】
0004784368.tif 000012
【図１２】
0004784368.tif 000013
【図１３】
0004784368.tif 000014
【図１４】
0004784368.tif 000015
【図１５】
0004784368.tif 000016
【図１６】
0004784368.tif 000017
【図１７】
0004784368.tif 000018
【図１８】
0004784368.tif 000019
【図１９】
0004784368.tif 000020
【図２０】
0004784368.tif 000021