"電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証するための検証装置であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとが入力される入力手段と、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する動作合成手段と、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成する対応関係記述生成手段と、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換するプロパティ変換手段と、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するプロパティ検証手段とを有する検証装置。前記検証装置は記憶手段を更に有し、前記記憶手段は、前記第1のプロパティを、前記抽象インタフェイスとの対応関係とともに予め記憶しており、前記入力手段は、検証対象の前記動作記述中で利用されている前記抽象インタフェイスを特定し、特定された抽象インタフェイスに対応する前記第1のプロパティを前記記憶手段から取得する請求項1記載の検証装置。前記検証装置は記憶手段及びRTL選択手段を更に有し、前記記憶手段は、前記抽象インタフェイスと前記第1のプロパティとの組を複数含むライブラリを記憶しており、前記ライブラリに含まれる前記抽象インタフェイスと前記第1のプロパティとの組のそれぞれについて、前記入力手段は、前記抽象インタフェイスと前記第1のプロパティの組を前記記憶手段から取得し、前記動作合成手段は、前記入力手段が取得した前記抽象インタフェイスと前記動作記述とを前記RTL記述に変換し、前記対応関係生成手段は、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記プロパティ変換手段は、前記入力手段が取得した前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記プロパティ検証手段は、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証し、前記RTL選択手段は、前記プロパティ手段が正常に動作すると判断した前記RTL記述であって、所定の評価関数による評価結果が所定のしきい値を満足する前記RTL回路を選択する請求項1記載の検証装置。前記検証装置は、前記検証結果を、前記電子回路の入出力動作を時系列に表示した波形図として出力する出力手段を更に有する請求項1乃至3いずれか1項に記載の検証装置。前記検証装置は、前記検証結果を、前記電子回路の時系列の入出力データとして出力する出力手段を更に有する請求項1乃至3いずれか1項に記載の検証装置。前記検証装置は、前記検証結果を、前記電子回路の動作を再現するためのテストベンチとして出力する出力手段を更に有する請求項1乃至3いずれか1項に記載の検証装置。電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証する方法であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証する検証方法。検証対象の前記動作記述中で利用されている前記抽象インタフェイスを特定し、前記第1のプロパティを前記抽象インタフェイスとの対応関係とともに予め記憶している記憶手段から、前記特定された抽象インタフェイスに対応する前記第1のプロパティを取得する請求項7記載の検証方法。記憶手段に複数記憶されている、前記抽象インタフェイスと前記第1のプロパティとの組のそれぞれについて、前記抽象インタフェイスと前記第1のプロパティの組を前記記憶手段から取得し、前記記憶手段から取得した前記抽象インタフェイスと前記動作記述とを前記RTL記述に変換し、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記記憶手段から取得した前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証し、前記プロパティ手段が正常に動作すると判断した前記RTL記述であって、所定の評価関数による評価結果が所定のしきい値を満足する前記RTL回路を選択する請求項7記載の検証方法。電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かをコンピュータに検証させるプログラムであって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、前記コンピュータを、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するよう動作させる検証プログラム。多くの場合、抽象インタフェイスの開発においては、性能向上や開発工数の節約が要請されるため、動作記述との適合性が十分に担保されない抽象インタフェイスが作成されてしまうことがある。このような抽象インタフェイスを利用すると、例えば、動作記述aと組合せた場合には正しい回路が生成されるとしても、動作記述bと組合せた場合には正常に動作しない回路が生成されてしまうという問題が生じ得る。以下に、この問題が顕在化する状況を具体的に示す。図21は、動作記述を示している。この動作記述は、SystemC言語を用いて表記されているが、本発明の説明に関連のない部分は一部省略されている。この動作記述は概略以下のように動作をする。入力有効端子in0_enの値が真である時に入力端子in0の値が読み出され、その値は、出力有効端子out0_enの値が真である時に出力端子out0へ書出される。この動作は、2つのスレッドini及びtarによって実現されている。そして、これらスレッド間の通信は、後述する抽象インタフェイスのデータ送出関数putとデータ取得関数getを用いて記述されている。以下に、これらスレッドの動作の概略を示す。スレッドiniは、入力有効端子in0_enの値を1つ読み出し、その値が真になるまで待つ。端子in0_enの値が真になったところで、スレッドiniは、入力端子in0の値を一つ読み出し、抽象インタフェイスinf_t型のインスタンスinfのデータ送出関数putを用いて、その値をスレッドtarに送出する。一方、スレッドtarは、出力有効端子out0_enの値を一つ読み出し、その値が真になるまで待つ。端子out0_enの値が真になったところで、スレッドtarは、infのデータ取得関数getを用いて、スレッドiniからの値を取得し、出力端子out0へ書出す。このように、動作記述内で抽象インタフェイスの関数を呼出すことで、設計者は、2つのスレッドiniとtarがどのようにスレッド間の通信を実現するかについては考慮することなく、いかにして入力端子in0の値を出力端子out0へ書き出すかという本来の動作の設計に注力することができる。図22は、抽象インタフェイスを示している。この抽象インタフェイスinf_t型は、2つの端子dat及びvldを有し、データ送出関数put及びデータ取得関数getを含んでいる。データ送出関数putは概略以下のような動作をする。putは、送出すべき値を端子datに書き出すとともに、端子vldに値1を書出す。さらに、putは、クロック境界に同期して、端子datおよび端子vldにそれぞれ値0を書出す。一方、データ取得関数getは概略以下のような動作をする。getは、端子vldの値が真になるまで待ち、真になったところで端子datの値を読出す。そして、getは、読出した値を通信路から取得した値として動作記述に出力する。図21の動作記述、図22の抽象インタフェイスは、動作合成装置によって組合され、RTL記述に変換される。動作合成装置の動作は概略以下のとおりである。動作合成装置は、図21の動作記述中に含まれるデータ送出関数、データ取得関数の呼出し部分を、図22の抽象インタフェイス中に含まれるデータ送出関数、データ取得関数の定義でそれぞれ置き換える。さらに、動作合成装置は、スケジューリング処理及びバインディング処理等を経て、RTL記述を生成する。図23に、動作合成装置が生成するRTL記述の例を示す。このRTL記述は、データパス付拡張有限状態機械FiniteStateMachinewithDatapath;FSMD形式で表現されている。FSMDとは、RTLの回路を有限状態機械FSMで表現される制御と、FSMの各状態での動作で表現する形式である。図23の1行目から21行目は、スレッドiniに対応するRTL記述である。スレッドiniに対応するRTL記述は、ST1、ST2及びST3の3つの状態を持つ。22行目から44行目は、スレッドtarに対応するRTL記述である。スレッドtarに対応するRTL記述は、ST4、ST5及びST6の3つの状態を持つ。スレッドiniに対応するRTL記述の状態ST1では、端子in0_enから読み出した値が真になるまで待ち、端子in0_enの値が真になったところで、端子in0から値を読み出して状態ST2に遷移する。状態ST2,状態ST3では、それぞれ、データ送出関数putの処理を実行する。状態ST2では、端子inf_datに送出する値を書き出し、端子inf_vldに値trueを書き出す。状態ST3では、端子inf_datに値0を書き出し、端子inf_vldの値をfalseとする。一方、スレッドtarに対応するRTL記述の状態ST4では、端子out0_enから読み出した値が真になるまで待ち、端子out0_enの値が真になったところで、状態ST5に遷移する。状態ST5,状態ST6では、それぞれデータ取得関数getの処理を実行する。状態ST5では、端子inf_vldから読み出した値が真になるまで待ち、端子inf_vldの値が真になったところで、端子inf_datの値を読み出し状態ST6に遷移する。状態ST6では、読み出した値を端子out0に書き出す。ここで、図24に、このRTL記述の一動作例としての波形図を示す。この動作例は、図23のRTL記述が動作するとき、設計者の意図どおりにデータ転送が行われない場合を示している。このRTL記述において、スレッドiniからスレッドtarへのデータ転送が正しく行われるためには、スレッドiniの状態ST2とスレッドtarの状態ST5が同時に実行される必要がある。これは、状態ST2で端子inf_datに書き出した値を状態ST5で読み出さなければならないためである。しかしながら、図24の波形を参照すると、時刻1で端子in0_enの値がtrueになり、遅れて、時刻3で端子out0_enの値がtrueになっている。そのため、スレッドiniが時刻2で状態ST2を実行するのに対して、スレッドtarが状態ST5を実行するのは時刻4以降である。よって、スレッドiniからスレッドtarへのデータ転送は正しく行われないこととなる。以上の実証から、動作記述と抽象インタフェイスとの分離は、設計の効率化等のメリットをもたらす一方、間違った組合せによる設計不具合という新たなデメリットを引き起こす場合があることが明らかとなった。そこで、設計者は、抽象インタフェイスと動作記述とが正しく組み合わせられているかを検証する必要がある。しかしながら、検証時には抽象インタフェイスが動作記述から分離されていることがマイナスに働く。すなわち、抽象インタフェイスを用意する側から考えると、設計不具合が動作記述との組み合わせで生じてしまうことから、インタフェイスそのものをいくら検証しても不具合をなくすことはできない。他方、抽象インタフェイスを利用する側から考えると、抽象インタフェイスの内部構造が外部から隠ぺいされているため、検証は抽象インタフェイスを利用しない場合に比べて難しい。そこで、抽象インタフェイスを用意する側にとっては、抽象インタフェイスをどのような動作記述と組合せた場合であっても、適合性を容易に検証できる手法が望まれる。また、抽象インタフェイスを利用する側にとっても、抽象インタフェイスの内部構造に関知することなく適合性の検証を行うことができる手法が望まれる。なお、動作記述の動作を論理的に検証する方法としては、プロパティアサーションを用いた検証方法が広く知られている例として、特開2006-285333号公報参照。しかしながら、この方法では、動作記述に対応するプロパティをその都度作成する必要がある。そのうえ、上述のように抽象インタフェイスの内容構造は一般に隠ぺいされているから、動作記述の設計者がプロパティを作成することは容易ではない。そこで、抽象インタフェイスの利点を生かしながら、プロパティを利用した設計検証が行える手法の確立が望まれる。本発明は、このような問題点を解決するためになされたものであり、動作記述と抽象インタフェイスの組み合わせによって起こり得る設計間違いを効率的に検出することができる検証装置、検証方法及び検証プログラムを提供することを目的とする。本発明に係る検証装置は、電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証するための検証装置であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとが入力される入力手段と、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する動作合成手段と、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成する対応関係記述生成手段と、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換するプロパティ変換手段と、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するプロパティ検証手段とを有するものである。また、本発明にかかる検証方法は、電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証する方法であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するものである。また、本発明に係るプログラムは、電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かをコンピュータに検証させるプログラムであって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、前記コンピュータを、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するよう動作させるものである。本発明により、動作記述と抽象インタフェイスの組み合わせによって起こり得る設計間違いを効率的に検出することができる検証装置、検証方法及び検証プログラムを提供することができる。<実施の形態1>まず、図1を用いて、本発明の実施の形態1にかかる検証装置100の構成について説明する。検証装置100は、入力手段101、動作合成手段102、対応関係記述生成手段103、プロパティ変換手段104、プロパティ検証手段105を備えている。検証装置100は、例えばサーバコンピュータ、パーソナルコンピュータPC、シンクライアント端末、ワークステーション、メインフレーム、スーパーコンピュータ等であり、典型的には処理装置CPU、マイクロプロセッサ等、記憶装置ROM、RAM、フラッシュメモリ、ハードディスク、SSD、CD、DVD、メモリカード等を有し、入出力装置ディスプレイ、キーボード、マウス等を備えていてもよい。記憶装置は、コンピュータ本体に内蔵された記憶装置に限らず、外付け周辺機器や外部のストレージサーバ等に設置された記憶装置、或いは、NASNetworkAttachedStorageであっても良い。また、検証装置100は、物理的に単一である必要はなく、複数のコンピュータで分散的に処理を行う構成であってもよい。入力手段101、動作合成手段102、対応関係記述生成手段103、プロパティ変換手段104、プロパティ検証手段105及び出力手段107は、プログラムに基づいて各種制御を実行する機能を有し、具体的には、処理装置、記憶装置、入出力ポート等により実現され得る。つぎに、図2を用いて、本発明の実施の形態1における各手段の動作について説明する。はじめに、入力手段101は、検証対象である動作記述及び抽象インタフェイスの入力を受付けるステップS101。動作記述及び抽象インタフェイスは、図示しない記憶装置に予め記憶されているものを読み出してもよく、図示しない入出力装置や通信回線等の任意の手段により検証装置100の外部から供給されてもよい。動作記述とは、電子回路の動作を記述したものである。動作記述の作成には、例えばVerilog-HDLVerilogHardwareDiscriptionLanguage、VHDLVeryHighSpeedHardwareDiscriptionLanguage、SystemVerilog等のハードウェア記述言語、C、C、C、JAVA登録商標、Perl、Scheme、Lisp等のプログラム言語及びSystemC、SpecC等のプログラミング言語に回路設計のための拡張を施した言語が用いられる以下、総じて単にプログラミング言語という。この動作記述は、入出力に関する処理は、抽象インタフェイスを利用して記述されているものとする。抽象インタフェイスとは、モジュール間及びスレッド間の通信処理を予め定義したデータ送出関数、データ取得関数等を1つのパッケージとしてまとめたソフトウェアモジュールである。設計者は、動作記述の中でこれらの関数を呼び出すことにより、上記通信処理を動作記述のプログラムに含める。つぎに、動作合成手段102は、動作記述をRTL記述に変換するステップS102。この変換処理を動作合成という。RTLRegisterTransferLevel記述とは、電子回路のハードウェアレベルの構成を記述したものである。RTL記述の作成においても、動作記述と同様のプログラミング言語が用いられる。動作合成は、以下の処理を含む。動作合成手段102は、動作記述中のデータ送出関数の呼び出し、データ取得関数の呼び出しを、抽象インタフェイス内に記述されたデータ送出関数、データ取得関数の定義でそれぞれ置き換えるとともに、不要コードの削除、言語レベルの最適化等を行う変形処理。また、動作合成手段102は、動作記述に記載された、端子アクセス読み出しや書き出し等、信号アクセス、変数アクセス、演算式算術演算論理演算比較演算等、文、ブロック、プラグマ、イベントを実行するコントロールステップを決定するスケジューリング処理。さらに、動作合成手段102は、動作記述に記載された端子や信号を、RTL記述の端子や信号に割り当てるとともに、動作記述の変数のデータを格納するRTL記述のレジスタや信号線wireを決定し、動作記述の演算式を行う演算器を決定し、動作記述の文をRTL記述の文に割り当て、動作記述のプラグマをRTL記述のプラグマに割り当てる。また、動作記述のイベントを、端子へのアクセスなどに割り当てるバインディング処理。加えて、動作合成手段102は、スケジューリング処理にて決定されたステップを制御する制御論理を備えた制御回路を作成する制御回路作成処理。最後に、動作合成手段102は、スケジューリング処理及びバインディング処理にて決定された演算器とレジスタからデータパスを作成し、そのデータパスと制御回路作成処理において作成された制御回路とを備えたRTL記述を作成するRTL記述生成処理。つぎに、対応関係記述生成手段103が、対応関係記述を生成するステップS103。対応関係記述とは、例えば、動作記述とその動作記述から生成されたRTL記述との間の、端子の対応関係、信号の対応関係、変数とレジスタの対応関係、変数と信号線の対応関係、演算式と演算器の対応関係、文の対応関係、プラグマの対応関係、イベントの対応関係等を記述したものである。対応関係記述は、動作記述に応じて生成される。そのため、異なる動作記述を基に動作合成すれば、生成される対応関係記述の内容も異なるものとなり得る。対応関係記述は、より具体的には、例えば上掲の特開2006-285333号公報において非特許文献2として示されている、若林一敏、他1名、アイイーイーイートランザクションズオンコンピュータエイディドデザインIEEETransactionsonComputerAidedDesign,2000年11月、第1507-1522頁に記載の既存の技術を用いて作成することが可能である。つづいて、入力手段101は、第1のプロパティの入力を受付けるステップS104。第1のプロパティは、抽象インタフェイスに応じて、抽象インタフェイスの設計者によって、予め用意される。作成された第1のプロパティは、図示しない記憶装置等に予め記録し、これを読み出してもよく、図示しない入出力装置や通信回線等の任意の手段により検証装置100の外部から供給されてもよい。ここで、第1のプロパティとは、抽象インタフェイスが正しく動作するための条件を所定のプログラミング言語を用いて記述したものである。この条件とは、抽象インタフェイスの設計者が望ましいと考える、抽象インタフェイス内に記述された端子、信号、変数、演算式、文、ブロック、プラグマ、イベント等の要素の状態、換言すれば、電子回路が設計者の意図どおりに動作するための前提条件となるべき上記要素の状態を指定したものである。より具体的には、設計者は、例えば上掲の特開2006-285333号公報において非特許文献1として示されている、ハリーフォスター他、アサーションベースドデザイン、クルーワーアカデミックパブリッシャーズ、2003年、第1-20頁に記載された手法を用いて、第1のプロパティを作成することが可能である。ついで、プロパティ変換手段104は、上述の対応関係記述に基づいて、第1のプロパティを第2のプロパティに変換するステップS105。これをプロパティ変換という。プロパティ変換は、プロパティ変換手段104が、第1のプロパティ内に記述されている端子、信号、変数、演算式、文、ブロック、プラグマ、イベント等の要素を、上述の対応関係記述をもとに置き換えることにより、第2のプロパティを生成して実現される。第2のプロパティは、対応関係記述に基づいて生成される。そのため、同じ第1のプロパティから変換した場合であっても、異なる対応関係記述を用いて変換した場合の変換結果は異なるものとなり得る。そして、上述のように、対応関係記述は、基となる動作記述に応じて内容が異なるものであり得る。すなわち、第2のプロパティは、原則的に、検証対象である動作記述に応じてユニークな内容となる。プロパティ変換は、より具体的には、例えば上掲の特開2006-285333号公報記載の技術により実施することができる。最後に、プロパティ検証手段105は、RTL記述が第2のプロパティに記述された条件を満たしているかどうかを検証するステップS106。この検証処理をプロパティ検証という。プロパティ検証は、例えば、J.R.Burch他,SymbolicModelChecking:10^{20}StatesandBeyond,ProceedingsofFifthAnnualIEEESymposiumonLogicinComputerScience,1990,第428-439頁に記載の技術を利用することにより、実施することができる。図3乃至図9を用いて、上記ステップS101乃至S106において用いられる動作記述、抽象インタフェイス及び第1のプロパティ、これらのステップにおいて作成されるRTL記述、対応関係記述及び第2のプロパティ、並びにプロパティ検証の結果の具体例を示す。ステップS101において、入力手段101が入力を受付ける動作記述及び抽象インタフェイスの例を、図3乃至図4に示す。図3に、動作記述の例動作記述Aを示す。動作記述Aは、SystemC言語を用いて表記されているが、本実施の形態の説明に関連のない部分は一部省略されている。動作記述Aにはモジュールfooの動作が記述されている。モジュールfooは、概略以下のような動作をする。入力有効端子in0_enの値が真である時に入力端子in0の値を読み出し、それをそのまま、出力端子out0へ、出力有効端子out0_enの値が真である時に、書き出す。図3の1行目乃至7行目は、fooという名前のモジュールを定義するコードである。2行目乃至5行目では、入出力端子の宣言がなされている。モジュールfooは、入力端子in0とその入力有効信号端子in0_en、及び出力端子out0とその出力有効信号端子out0_enを有する。さらに、6行目では、抽象インタフェイスinf_t型の通信路infを有することが宣言されている。モジュールfooは、2つのスレッドSC_CTHREADiniとtarを有し、抽象インタフェイスの通信路infを介して通信する。この通信は、データ送出関数putとデータ取得関数getを用いて記述されている。8行目乃至18行目は、スレッドiniの定義を示している。10行目では、スレッドiniは、11行目乃至16行目までの動作を永遠に繰り返すことが指定されている。11行目乃至14行目では、入力有効信号端子in0_enから値を一つ読み出し、その値が真trueでない間は12行目記載のクロック境界を待つwait文を繰り返すことが指定されている。さらに、端子in0_enから読みだした値が真trueであれば、入力端子in0から値を一つ読みだして変数vに格納することが指定されている。15行目では、変数vの値を、データ送出関数putにより、通信路infを介して、スレッドtarに送出することが指定されている。値の送出が完了すると、16行目のwait文で、クロック境界を待つことが示されている。19行目乃至29行目は、スレッドtarの定義を示している。21行目では、スレッドtarは、スレッドiniと同様に、22行目乃至27行目の動作を永遠に繰り返すことが指定されている。22行目乃至24行目では、出力有効信号端子out0_enから値を一つ読み出し、その値が真trueでない間は23行目記載のクロック境界を待つwait文を繰り返すことが指定されている。さらに、端子out0_enから読み出した値が真trueであれば、25行目で、通信路infからデータ取得関数getを用いて値を取得し、変数vに格納することが指定されている。26行目では、通信路infからの値の取得が完了すると、出力端子out0へ変数vの値を書き出すことが指定されている。その後、27行目のwait文で、クロック境界を待つことが示されている。図4に、抽象インタフェイスの例抽象インタフェイスAを示す。抽象インタフェイスAは、抽象インタフェイスinf_t型として定義されている。図4の3行目乃至4行目では、抽象インタフェイスinf_t型は、内部の変数として、転送される値を保持する端子dat及び値を転送可能かどうかを示す端子vldを有することが示されている。5行目乃至14行目は、抽象インタフェイスinf_t型のデータ送出関数putの定義を示している。6行目では、データ送出関数putを実行するときに、同時にイベントini.transfer=1が発生することが示されている。このイベントは、第1のプロパティを作成する際に使用される。7行目乃至9行目では、端子vldに値1を、端子datに変数valの値を書き出し、クロック境界を待つことが指定されている。10行目乃至13行目では、端子vld及び端子datに、ともに値0を書き出し、クロック境界を待つことが指定されている。また、同時にイベントini.transfer=0が発生することが示されている。15行目乃至24行目は、抽象インタフェイスinf_t型のデータ取得関数getの定義を示している。17行目では、データ取得関数getを実行するときに、同時にイベントtar.wait=1が発生することが示されている。このイベントは、第1のプロパティを指定する際に使用される。18行目乃至20行目では、端子vldから値を一つ読み出し、その値が真trueでない間は19行目のクロック境界を待つ関数waitを繰り返すことが指定されている。さらに、端子vldの値が真trueであれば、21行目で、端子datから値を一つ読み出し、変数valに格納することが指定されている。23行目では、変数valの値を、通信路から取得した値として返すことが指定されている。また、同時にイベントtar.wait=0が発生することが示されている。ステップS102において、動作合成手段102が動作合成を行うことによって作成するRTL記述の例を、図6に示す。図6は、図3の動作記述Aと図4に示された抽象インタフェイスAとを用い、動作合成して作成した、RTL記述の例RTL記述Aを示している。RTL記述Aは、SystemC言語を用いて表記されているが、本実施の形態の説明に関連が薄い部分は一部省略されている。また、RTL記述Aは、データパス付拡張有限状態機械FiniteStateMachinewithDatapath:FSMDの形式で表現されている。FSMDは、RTLの回路を、有限状態機械FSMで表現される制御とFSMの各状態での動作で表現する形式である。図6の1行目乃至23行目は、スレッドiniに対応するRTL記述を示している。スレッドiniに対応するRTL記述は、ST1、ST2及びST3の3つの状態を持つ。3行目乃至10行目は、状態ST1の動作を示している。状態ST1の動作は、図3の11行目乃至14行目に示されている動作記述Aの動作に対応している。状態ST1では、入力端子in0_enから値がひとつ読み出され、その値が真trueであれば入力端子in0から値が読みだされる。読み出された値はレジスタRG_vに格納される。その後、クロック境界に同期して状態ST2に遷移する。一方、端子in0_enから読み出した値が真でない場合は、クロック境界に同期して再度状態ST1に遷移する。端子in0_enから読み出した値が真trueとなるまで状態ST1の実行が繰り返される。11行目乃至15行目は、状態ST2の動作を示している。状態ST2の動作は、図3の15行目に示されている動作記述Aのデータ送出関数putの動作に対応している。また、図4の抽象インタフェイスAのデータ送出関数putの定義における、6行目乃至9行目に対応している。状態ST2では、端子inf_vldに値trueが書き出され、端子inf_datにレジスタRG_vの値が書き出される。同時に、端子inf_ini_transfer_flgに値1が書き出される。その後、クロック境界に同期して状態ST3に遷移する。16行目乃至21行目は、状態ST3の動作を示している。状態ST3の動作は、図3の15行目に示されている動作記述Aのデータ送出関数putの動作に対応している。また、図4のデータ送出関数putの定義における、10行目乃至13行目に対応している。状態ST3では、端子inf_vldおよび端子inf_datに、値falseおよび0がそれぞれ書き出される。その後、クロック境界に同期して状態ST3に遷移する。24行目乃至48行目は、スレッドtarに対応するRTL記述を示している。スレッドtarに対応するRTL記述は、ST4、ST5及びST6の3つの状態を持つ。26行目乃至32行目は、状態ST4の動作を示している。状態ST4の動作は、図3の22行目乃至24行目に示されている動作記述Aの動作に対応している。状態ST4では、入力端子out0_enから値が一つ読み出され、その値が真trueであれば、クロック境界に同期して状態ST5に遷移する。一方、端子out0_enから読み出された値が真でない場合は、クロック境界に同期して再度状態ST4に遷移する。端子out0_enから読み出された値が真trueとなるまで状態ST4の実行が繰り返される。33行目乃至41行目は、状態ST5の動作を示している。状態ST5の動作は、図3の25行目に示されている動作記述Aのデータ取得関数getの動作に対応している。また、図4の抽象インタフェイスAのデータ取得関数getの定義における17行目乃至21行目に対応している。状態ST5では、端子inf_vldから値が一つ読み出され、その値が真trueであれば、さらに端子inf_datから値が一つ読み出され、その値がレジスタRG_wに格納される。その後、クロック境界に同期して状態ST5に遷移する。この時、同時に、端子inf_tar_wait_flgに値1が書き出される。端子inf_vldから読み出された値が真trueでなければ、クロック境界に同期して再度状態ST5に遷移する。端子inf_vldから読み出された値が真trueとなるまで状態ST5の実行が繰り返される。42行目乃至46行目は、状態ST6の動作を示している。状態ST6の動作は、図3の25行目に示されている動作記述Aのデータ取得関数getの動作に対応している。また、図4の抽象インタフェイスAのデータ取得関数getの定義における22行目乃至23行目に対応している。さらに、状態ST6の動作は、図3の26行目乃至27行目に示されている動作記述Aの動作にも対応している。状態ST6では、レジスタRG_wの値が出力端子out0に書き出される。同時に、端子inf_tar_wait_flgに値0が書き出される。その後、クロック境界に同期して状態ST4に遷移する。ステップS103において、対応関係記述生成手段103が作成する対応関係記述の例を、図7に示す。図7に、対応関係記述の例対応関係記述Aを示す。対応関係記述Aでは、動作記述中のイベント名とRTL記述中の端子名の対応関係が特定されている。対応関係記述Aは、動作記述中の抽象インタフェイスinf_t型の通信路infにおけるイベントini_transferinf.ini_transferが、RTL記述中の端子inf_ini_transfer_flgに対応していることを示している。同様に、動作記述中の抽象インタフェイスinf_t型の通信路infにおけるイベントtar_waitinf.tar_waitが、RTL記述中の端子inf_tar_wait_flgに対応していることを示している。ステップS104において、入力手段101が入力を受付ける第1のプロパティの例を、図5に示す。図5に、第1のプロパティの例第1のプロパティAを示す。第1のプロパティは、図4の抽象インタフェイスA中に定義されているイベントini.transferとtar.waitを使用して定義されている。図5の第1のプロパティAは、ini.transfer=1であるときには、必ず、同時に、tar.wait=1であるべきことを示している。これは、すなわち、抽象インタフェイスinf_t型の通信路を通じて値の授受をする場合、値の送出側が値を送出しようとしたときに、値の受け取り側は信号vldの値が真trueになるまで待つ状態になければならないことを意味している。より具体的には、送出側が値の送出をするために送出関数putを呼び出したときに、値の受け取り側は値を取得するための取得関数getをあらかじめ呼び出していなければならないことを意味している。ステップS105において、プロパティ変換手段104がプロパティ変換を行うことによって生成する第2のプロパティの例を、図8に示す。図8に、第2のプロパティの例第2のプロパティAを示す。第2のプロパティAは、図5の第1のプロパティAに記述された動作記述A中のイベントを、図7の対応関係Aに基づいて、RTL記述A中の端子に置き換えることにより作成される。第2のプロパティAは、端子inf_ini_transfer_flgの値が1の時は、同時に端子inf_tar_transfer_flgの値が1であるという性質を示している。すなわち、図6に示したRTL記述Aにおいて、端子inf_ini_transfer_flgには状態ST2で値1が書き込まれること、端子inf_tar_wait_flgには状態ST5で値1が書き込まれることを勘案すると、スレッドiniに対応するFSMが状態ST2に到達しデータ送出動作を行うときにはスレッドtarに対応するFSMが状態ST5にあらかじめ到達していなければならないことを指定していることになる。ステップS106において、プロパティ検証手段105がプロパティ検証を行った結果の一出力例を、図9に示す。図9に、プロパティ検証の結果を波形図として出力した例を示す。図9の波形図は、プロパティ検証手段105が発見した反例、すなわち図6に示されたRTL記述Aが、図8に示された第2のプロパティAを満たさない場合を示すものである。図9の波形図を参照すると、時刻1で入力端子in0_enが真trueであるにもかかわらず、入力端子out0_enが真trueでない場合が発生する。そのため、スレッドiniに対応するFSMが状態ST2に到達するにもかかわらず、スレッドtarに対応するFSMが状態ST4にとどまったままとなる。結果として、端子inf_ini_transfer_flgの値が1になっていても、端子inf_tar_wait_flgの値が0のままとなる。これは、図8に示された第2のプロパティAに違反した結果である。これにより、図4の動作記述Aと図5の抽象インタフェイスAとを組合せて使用すると、データ転送が正しく行われない場合があることがわかる。なお、このように、動作記述と抽象インタフェイスとの組合せが適切でないという問題が判明したならば、設計者は、動作記述又は抽象インタフェイスのいずれかを修正することにより、かかる問題に対処することができる。図10乃至図15を用いて、設計者がとり得る対処方法と、かかる対処を行った後に再度プロパティ検証を行った結果の例を示す。第1の対処方法は、動作記述を修正することである。図10に、設計者が動作記述Aを修正することにより作成した、動作記述の例動作記述Bを示す。動作記述Bは、動作記述Aに比べて、出力有効信号端子out0_enがなく、22行目乃至24行目の端子out0_enの値が真になるまで待つ動作がないことが異なる。図11に、動作合成手段102が、図10の動作記述Bと図4に示された抽象インタフェイスAとを用い、動作合成して作成した、RTL記述の例RTL記述Bを示す。RTL記述Bは、RTL記述Aに比べて、出力有効信号端子out0_enがなく、26行目乃至32行目までの状態ST4がないことが異なる。すなわち、端子out0_enの値が真になるまで待つ動作がないことが異なる。また、対応関係記述生成手段103は、動作記述Bと抽象インタフェイスAとに基づいて、対応関係記述を作成する。この対応関係記述は、図7に示した対応関係記述Aと同一内容となる。図12に、プロパティ検証手段105がプロパティ検証を実施した結果の出力例を示す。図12は、RTL記述Bの実行例を波形図として出力したものである。今回は、プロパティ検証手段105は、図11のRTL記述Bは、図8の第2のプロパティAを満たすと判定している。図12では、時刻2において、端子inf_ini_transfer_flgの値が1となるときに、端子inf_tar_wait_flgの値も1である。よって、第2のプロパティAが満たされていることがわかる。確かに、スレッドiniが状態ST2に到達したときに、スレッドtarの状態があらかじめST5に到達しているため、正しくデータ転送が行われている。第2の対処方法は、抽象インタフェイスを修正することである。図13に、抽象インタフェイスの設計者が抽象インタフェイスAを修正して作成した、抽象インタフェイスの例抽象インタフェイスBを示す。抽象インタフェイスBは、図4の抽象インタフェイスAと比較して、端子enが追加されていることが異なる。また、データ送出関数putの8行目乃至10行目において、端子enから値を読み出し、その値が真trueになるまで待つ動作が追加されていることが異なる。さらに、データ取得関数getの24行目において、端子vldから読み出した値が真trueになるまで待つ間に端子enに値trueを書き出す動作が追加されていること、及び端子vldから読み出した値が真trueであれば、端子enに値falseを書き出す動作が追加されていることが異なる。これらの違いにより、抽象インタフェイスBの送出関数putは、データ取得側が値の取得ができる状態になるまで待つように動作する点で、抽象インタフェイスAの送出関数と異なる。図14に、動作合成手段102が、図3に示された動作記述Aと図13に示された抽象インタフェイスBとを用い、動作合成して作成した、RTL記述の例RTL記述Cを示す。RTL記述Cは、RTL記述Aに比べて、スレッドiniに対応するRTL記述の状態ST2の動作内容が異なる。具体的には、端子inf_enの値が真trueになるまで状態ST2を繰り返すことが異なる。すなわち、端子inf_enから値を一つ読み出し、その値が真trueであるかどうかを検査する。端子inf_enの値が真trueである場合は、端子inf_vldに値trueを書き出し、端子inf_datにレジスタRG_vの値を書き出す。同時に、端子inf_ini_transfer_flgに値1を書き出す。さらに、クロック境界に同期して状態ST3に遷移する。端子inf_enの値が真でない場合には、クロック境界に同期して、再度状態ST2に遷移する。これらの違いにより、RTL記述Cは、データ取得側が値の取得ができる状態になるまでデータ送出側が待ち合わせるように動作する点で、RTL記述Aと異なる。また、対応関係記述生成手段103は、動作記述Aと抽象インタフェイスBとに基づいて、対応関係記述を作成する。この対応関係記述は、図7に示した対応関係記述Aと同一内容となる。図15に、プロパティ検証手段105がプロパティ検証を実施した結果の出力例を示す。図15は、RTL記述Cの実行例を波形図として出力したものである。この例でも、プロパティ検証手段105は、図14のRTL記述Cは、図8の第2のプロパティAを満たすと判定している。図15では、時刻4において、端子inf_ini_transfer_flgの値が1となるときに、端子inf_tar_wait_flgの値も1である。よって、第2のプロパティAが満たされていることがわかる。確かに、スレッドスレッドtarの状態があらかじめST5に到達し端子inf_enの値が真trueになるまで、スレッドiniが状態ST2で待つため、正しくデータ転送が行われている。本実施の形態においては、抽象インタフェイスに対応する第1のプロパティが予め用意され、検証装置100が、この第1のプロパティを、動作記述をRTL記述に変換する際にともに生成される対応関係記述に基づいて第2のプロパティに変換し、この第2のプロパティを用いてRTL記述のプロパティ検証を行う構成とした。これにより、動作記述の設計者は、動作記述を作成するたびに、動作記述に応じたプロパティを作成する必要がなく、動作記述と抽象インタフェイスの組み合わせによって起こり得る設計間違いを効率的に検出することができる。また、抽象インタフェイスの設計者は、抽象インタフェイスに対応する第1のプロパティを一度用意すれば、この第1のプロパティをどのような動作記述と組み合わせる場合であっても、同じ方法で、動作記述と抽象インタフェイスの組み合わせによって起こり得る設計間違いを効率的に検出することができる。<実施の形態2>図16を用いて、本発明の実施の形態2にかかる検証装置100の構成について説明する。検証装置100は、記憶手段106を備える点で、実施の形態1と異なる。その余の構成については、実施の形態1と同様である。記憶手段106は、予め所与のデータを記憶し、他の手段の要求に応じてデータを記憶及び出力する機能を有する。具体的には、ROM、RAM、フラッシュメモリ、ハードディスク、SSD、CD、DVD、メモリカード等により実現され得る。つぎに、図17を用いて、本発明の実施の形態2における各手段の動作について説明する。ステップS101乃至S103は、実施の形態1と同様である。すなわち、入力手段101は、検証対象である動作記述及び抽象インタフェイスの入力を受付けるステップS101。つぎに、動作合成手段102は、動作記述をRTL記述に変換する動作合成ステップS102。また、対応関係記述生成手段103は、対応関係記述を生成するステップS103。かかる処理の後、入力手段101は、動作記述の中で使用されている抽象インタフェイスを特定するステップS201。例えば、図3の動作記述Aでは、6行目の記述から、inf_t型の抽象インタフェイスが使用されていることが特定できる。つづいて、入力手段101は、記憶手段106を参照して、ステップS201で特定された抽象インタフェイスに対応する第1のプロパティを取得する。例えば、動作記述Aで使用されている抽象インタフェイスはinf_t型であった。図16の記憶手段106を参照すると、inf_t型に対応する第1のプロパティとして、alwaysini.tranfer==1->tar.wait==1;が記憶されている。よって、入力手段101は、この第1のプロパティを取得し、つづくステップの処理において使用する。これらの処理の後、ステップS105乃至S106が実行される。ステップS105乃至S106は、実施の形態1と同様である。すなわち、プロパティ変換手段104は、対応関係記述に基づいて、ステップS202において記憶手段106から取得した第1のプロパティを、第2のプロパティに変換するプロパティ変換ステップS105。最後に、プロパティ検証手段105は、RTL記述が第2のプロパティに記述された条件を満たしているかどうかを検証するプロパティ検証ステップS106。本実施の形態においては、抽象インタフェイスに対応する第1のプロパティが予め記憶手段106に記録され、入力手段101は、プロパティ変換を行う際に自動的に第1のプロパティを取得するので、設計者はプロパティ変換の都度第1のプロパティを入力する必要がなく、動作記述と抽象インタフェイスの組み合わせによって起こり得る設計間違いを効率的に検出することができる。<実施の形態3>図18を用いて、本発明の実施の形態3にかかる検証装置100の構成について説明する。検証装置100は、出力手段107を備える点で、実施の形態1又は2と異なる。その余の構成については、実施の形態1又は2と同様である。出力手段107は、CRT、液晶ディスプレイ、プリンタ等によって構成され得る。出力手段107は、プロパティ検証の結果を、例えば図9、図15及び図24に示すようなRTL記述の実行結果の波形図として出力することができる。また、出力手段107は、RTL記述の実行結果を、時系列の入出力データとして出力するものであってもよい。すなわち、各端子毎に、端子に入出力されるビット値を、クロック毎に並べた数列として出力することができる。さらに、出力手段107は、RTL記述の動作を再現するためのテストベンチを出力するものであってもよい。<実施の形態4>本発明の実施の形態4にかかる検証装置100は、複数の抽象インタフェイスが予め用意されている場合に、これらの抽象インタフェイスから生成されるRTL記述を比較して、最も設計者の意図に沿うRTL記述を選択することを可能とするものである。図19を用いて、本発明の実施の形態4にかかる検証装置100の構成について説明する。検証装置100は、記憶装置106及びRTL選択手段108を備える点で、実施の形態1と異なる。その余の構成については、実施の形態1と同様である。記憶手段106は、予め所与のデータを記憶し、他の手段の要求に応じてデータを記憶及び出力する機能を有する。具体的には、ROM、RAM、フラッシュメモリ、ハードディスク、SSD、CD、DVD、メモリカード等により実現され得る。RTL選択手段108は、プログラムに基づいて各種制御を実行する機能を有し、具体的には、処理装置、記憶装置、入出力ポート等により実現され得る。つぎに、図20を用いて、本発明の実施の形態4における各手段の動作について説明する。記憶手段106は、抽象インタフェイスとその抽象インタフェイスに対応する第1のプロパティとの組を複数含むライブラリを予め記憶しているものとする。この複数の抽象インタフェイスは、RTL回路に変換されたとき、回路の面積、遅延、スループット等の点においてそれぞれ異なるパフォーマンスを示すものである。はじめに、入力手段101は、記憶手段106のライブラリから抽象インタフェイス及び第1のプロパティの組を1組取得するステップS301。以降、ステップS101、S102、S103、S105、S106及びS302の処理が、ここで取得した抽象インタフェイス及び第1のプロパティの組に対して実施される。この組に対する上記処理が完了したならば、入力手段101は、記憶手段106のライブラリから、既に取得したものとは異なる抽象インタフェイス及び第1のプロパティの組を1組取得し、この組に対し、上記ステップS101乃至S302の処理が再び実行される。同様の処理が、記憶手段106から、比較対象となるすべての抽象インタフェイス及び第1のプロパティの組が取得されるまで繰り返される。上記ステップS101乃至S302の処理の内容を以下に示す。まず、ステップS101乃至ステップS106の処理が行われる。各ステップにおける処理の内容は、実施の形態1と同様である。すなわち、入力手段101は、動作記述の入力を受付けるステップS101。動作合成手段102は、ステップS101で入力された動作記述と、ステップS301で取得された抽象インタフェイスとを、RTL記述に変換するステップS102。対応関係記述生成手段103は、対応関係記述を生成するステップS103。プロパティ変換手段104は、上述の対応関係記述に基づいて、ステップS301で取得された第1のプロパティを、第2のプロパティに変換するステップS105。プロパティ検証手段105は、RTL記述が第2のプロパティに記述された条件を満たしているかどうかを検証するステップS106。ここで、プロパティ検証手段105が、RTL記述は第2のプロパティを満たすと判定した場合、RTL選択手段108は、そのRTL記述を所定の評価関数により評価するステップS302。この評価関数とは、RTL記述を入力すると、そのRTL記述のパフォーマンス、例えば面積、遅延、スループット等について、定量的な評価値を出力することが可能な関数である。この評価関数は、回路設計者の設計意図に応じて適切なものが選択されるべきである。評価関数が出力した評価値は、所定の記憶領域に保持され、後の処理に利用される。比較対象となるすべての抽象インタフェイス及び第1のプロパティの組について上述の処理が完了したならば、RTL選択手段108は、ステップS302において出力された各RTL記述の評価値に基づいて、設計者の設計意図に最も適合したRTL記述を選択するステップS303。すなわち、評価関数による評価結果が所定の条件を満足するRTL記述を選択する。ここで、所定の条件は、回路設計者の設計意図に基づいて適宜決定することができる。例えば、回路設計者が、最もスループットの大きい回路を設計することを意図している場合であれば、RTL選択手段108を、ステップS302では、スループットが大きいほど大きな評価値を出力する評価関数を利用し、ステップS303においては、かかる評価関数の評価値が最も大きいRTL記述を選択するよう設計することができる。本実施の形態においては、抽象インタフェイスと第1のプロパティとの複数の組が予め記憶手段106に記録され、入力手段101、動作合成手段102、対応関係記述生成手段103、プロパティ変換手段104及びプロパティ検証手段105が、その抽象インタフェイス及び第1のプロパティに基づいて正常に動作するRTL記述を複数出力し、RTL選択手段108が、それらのRTL記述の中から所定の評価関数による評価結果が所定の条件を満足するRTL記述を選択するので、設計者は、設計意図に最も適合するRTL記述を効率的に得ることができる。特に、本実施の形態においては、抽象インタフェイスと第1のプロパティとが予め対応付けられて記憶手段106に格納されているため、設計者は容易に複数のRTL記述を生成し、それらのRTL記述を比較検討することが可能である。なお、本発明は上述した実施の形態のみに限定されるものではなく、本発明の要旨を逸脱しない範囲において種々の変更が可能であることは勿論である。例えば、上述の実施の形態において示した処理の手順は、処理結果に影響を与えない範囲内において、適宜順序を変更して実施することが可能である。また、上述の実施の形態では、ハードウェアの構成として説明したが、これに限定されるものではなく、任意の処理を、CPUCentralProcessingUnitにコンピュータプログラムを実行させることにより実現することも可能である。この場合、コンピュータプログラムは、様々なタイプの非一時的なコンピュータ可読媒体non-transitorycomputerreadablemediumを用いて格納され、コンピュータに供給することができる。非一時的なコンピュータ可読媒体は、様々なタイプの実体のある記録媒体tangiblestoragemediumを含む。非一時的なコンピュータ可読媒体の例は、磁気記録媒体例えばフレキシブルディスク、磁気テープ、ハードディスクドライブ、光磁気記録媒体例えば光磁気ディスク、CD-ROMReadOnlyMemory、CD-R、CD-R/W、半導体メモリ例えば、マスクROM、PROMProgrammableROM、EPROMErasablePROM、フラッシュROM、RAMrandomaccessmemoryを含む。また、プログラムは、様々なタイプの一時的なコンピュータ可読媒体transitorycomputerreadablemediumによってコンピュータに供給されてもよい。一時的なコンピュータ可読媒体の例は、電気信号、光信号、及び電磁波を含む。一時的なコンピュータ可読媒体は、電線及び光ファイバ等の有線通信路、又は無線通信路を介して、プログラムをコンピュータに供給できる。上記実施の形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。付記1電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証するための検証装置であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとが入力される入力手段と、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する動作合成手段と、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成する対応関係記述生成手段と、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換するプロパティ変換手段と、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するプロパティ検証手段とを有する検証装置。付記2前記検証装置は記憶手段を更に有し、前記記憶手段は、前記第1のプロパティを、前記抽象インタフェイスとの対応関係とともに予め記憶しており、前記入力手段は、検証対象の前記動作記述中で利用されている前記抽象インタフェイスを特定し、特定された抽象インタフェイスに対応する前記第1のプロパティを前記記憶手段から取得する付記1記載の検証装置。付記3前記検証装置は記憶手段及びRTL選択手段を更に有し、前記記憶手段は、前記抽象インタフェイスと前記第1のプロパティとの組を複数含むライブラリを記憶しており、前記ライブラリに含まれる前記抽象インタフェイスと前記第1のプロパティとの組のそれぞれについて、前記入力手段は、前記抽象インタフェイスと前記第1のプロパティの組を前記記憶手段から取得し、前記動作合成手段は、前記入力手段が取得した前記抽象インタフェイスと前記動作記述とを前記RTL記述に変換し、前記対応関係生成手段は、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記プロパティ変換手段は、前記入力手段が取得した前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記プロパティ検証手段は、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証し、前記RTL選択手段は、前記プロパティ手段が正常に動作すると判断した前記RTL記述であって、所定の評価関数による評価結果が所定のしきい値を満足する前記RTL回路を選択する付記1記載の検証装置。付記4前記検証装置は、前記検証結果を、前記電子回路の入出力動作を時系列に表示した波形図として出力する出力手段を更に有する付記1乃至3いずれか1項に記載の検証装置。付記5前記検証装置は、前記検証結果を、前記電子回路の時系列の入出力データとして出力する出力手段を更に有する付記1乃至3いずれか1項に記載の検証装置。付記6前記検証装置は、前記検証結果を、前記電子回路の動作を再現するためのテストベンチとして出力する出力手段を更に有する付記1乃至3いずれか1項に記載の検証装置。付記7電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かを検証する方法であって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証する検証方法。付記8検証対象の前記動作記述中で利用されている前記抽象インタフェイスを特定し、前記第1のプロパティを前記抽象インタフェイスとの対応関係とともに予め記憶している記憶手段から、前記特定された抽象インタフェイスに対応する前記第1のプロパティを取得する付記7記載の検証方法。付記9記憶手段に複数記憶されている、前記抽象インタフェイスと前記第1のプロパティとの組のそれぞれについて、前記抽象インタフェイスと前記第1のプロパティの組を前記記憶手段から取得し、前記記憶手段から取得した前記抽象インタフェイスと前記動作記述とを前記RTL記述に変換し、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記記憶手段から取得した前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証し、前記プロパティ手段が正常に動作すると判断した前記RTL記述であって、所定の評価関数による評価結果が所定のしきい値を満足する前記RTL回路を選択する付記7記載の検証方法。付記10前記検証結果を、前記電子回路の入出力動作を時系列に表示した波形図として出力する付記7乃至9いずれか1項に記載の検証方法。付記11前記検証結果を、前記電子回路の時系列の入出力データとして出力する付記7乃至9いずれか1項に記載の検証方法。付記12前記検証結果を、前記電子回路の動作を再現するためのテストベンチとして出力する付記7乃至9いずれか1項に記載の検証方法。付記13電子回路の動作をプログラミング言語により記述した動作記述が、正常に動作するものか否かをコンピュータに検証させるプログラムであって、前記動作記述は、所定のプログラミング言語で記述され、入出力処理をモジュール化した抽象インタフェイスを利用して記述されたものであり、前記コンピュータを、検証対象の前記動作記述と、前記抽象インタフェイスが正常に動作するための条件が記述されたものであって、前記抽象インタフェイスに対応して予め用意された第1のプロパティとの入力を受けると、前記動作記述を、前記電子回路の構成を記述したRTL記述に変換する際、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証するよう動作させる検証プログラム。付記14前記コンピュータを、検証対象の前記動作記述中で利用されている前記抽象インタフェイスを特定し、前記第1のプロパティを前記抽象インタフェイスとの対応関係とともに予め記憶している記憶手段から、前記特定された抽象インタフェイスに対応する前記第1のプロパティを取得するよう動作させる付記13記載の検証プログラム。付記15前記コンピュータを、記憶手段に複数記憶されている、前記抽象インタフェイスと前記第1のプロパティとの組のそれぞれについて、前記抽象インタフェイスと前記第1のプロパティの組を前記記憶手段から取得し、前記記憶手段から取得した前記抽象インタフェイスと前記動作記述とを前記RTL記述に変換し、前記動作記述と前記RTL記述との対応関係を記述した対応関係記述を生成し、前記記憶手段から取得した前記第1のプロパティを、前記対応関係記述に記述された対応関係に従って、第2のプロパティに変換し、前記第2のプロパティに基づき、前記RTL記述が正常に動作するか否かを検証し、前記プロパティ手段が正常に動作すると判断した前記RTL記述であって、所定の評価関数による評価結果が所定のしきい値を満足する前記RTL回路を選択するよう動作させる付記13記載の検証プログラム。付記16前記コンピュータを、前記検証結果を、前記電子回路の入出力動作を時系列に表示した波形図として出力するよう動作させる付記13乃至15いずれか1項に記載の検証プログラム。付記17前記コンピュータを、前記検証結果を、前記電子回路の時系列の入出力データとして出力するよう動作させる付記13乃至15いずれか1項に記載の検証プログラム。付記18前記コンピュータを、前記検証結果を、前記電子回路の動作を再現するためのテストベンチとして出力するよう動作させる付記13乃至15いずれか1項に記載の検証プログラム。"