(57)【要約】【課題】  論理システムの設計データを論理検証するための動作仕様記述を容易に作成する。【解決手段】  内部表現変換器２１でＲＴＬソースコード１１とテンプレートライブラリ１３内の動作仕様記述テンプレートとを内部表現に変換し、変換した内部表現を比較器・選択器２２で比較して論理的等価性を判定し、その判定に応じて当該動作仕様記述テンプレートを選択して出力する。【選択図】      図１
2006163599.tif 000002
【特許請求の範囲】
【請求項１】
論理システムの設計データを論理検証するための動作仕様記述に関する情報を出力する検証用情報出力方法であって、
論理システムを検証するための複数の動作仕様記述に関する情報を格納する工程と、
前記論理システムの設計データに基づいて前記格納された複数の動作仕様記述に関する情報から前記論理システムの設計データを論理検証するための動作仕様記述に関する情報を選択して出力する工程とを有することを特徴とする検証用情報出力方法。
【請求項２】
前記動作仕様記述は、前記論理システムの構成部品である機能ブロックに対応する記述であることを特徴とする請求項１記載の検証用情報出力方法。
【請求項３】
前記機能ブロックは、前記論理システムと動作仕様記述の等価性を判定し、論理検証を行う論理検証装置を用いた論理検証の有効性が予め確認された機能ブロックであることを特徴とする請求項２記載の検証用情報出力方法。
【請求項４】
前記選択して出力する工程は、前記論理システムの設計データ及び前記動作仕様記述に関する情報を所定の正規化論理表現に変換する工程と、
前記正規化論理表現に変換した論理システムの設計データと前記正規化論理表現に変換した複数の動作仕様記述に関する情報とを比較し、論理的等価性を判定する工程とを有し、
前記判定に応じて前記論理システムの設計データを論理検証するための動作仕様記述に関する情報を選択して出力することを特徴とする請求項１記載の検証用情報出力方法。
【請求項５】
前記正規化論理表現は、２分決定グラフであることを特徴とする請求項４記載の検証用情報出力方法。
【請求項６】
前記選択して出力する工程では、前記変換した設計データの正規化論理表現が動作仕様記述に関する情報の正規化論理表現と一致するか、或いは含む場合に、当該動作仕様記述に関する情報を出力することを特徴とする請求項４記載の検証用情報出力方法。
【請求項７】
論理システムの設計データを論理検証するための動作仕様記述に関する情報を出力する検証用情報出力装置であって、
論理システムを検証するための複数の動作仕様記述に関する情報を格納する手段と、
前記論理システムの設計データに基づいて前記格納された複数の動作仕様記述に関する情報から前記論理システムの設計データを論理検証するための動作仕様記述に関する情報を選択して出力する手段とを有することを特徴とする検証用情報出力装置。
【請求項８】
請求項１記載の検証用情報出力方法をコンピュータに実行させるためのプログラム。
【請求項９】
請求項８記載のプログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理システムの設計データを論理検証するための動作仕様記述に関する情報を出力する技術に関するものである。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年々増大している。これに伴い、論理システムの検証にかかる工数も増加している。一方、市場には消費者が欲するときに製品を投入しなければならず、ＬＳＩを始めとする論理システムの開発期間は短くなっている。そのため、論理システムの検証効率を向上させる必要が生じている。
【０００３】
このような状況において、ＬＳＩを含む論理システムの検証には、論理シミュレータを用いた動的検証が行われている。しかし、動的検証では、論理シミュレータを用いて論理システムを動作させて検証を行うため、検証にかかる時間が長い。そのため、全ての事象を実現するには膨大な時間を必要とする。例えば、32ビットの入力を持つ機能ブロックを検証する場合は、232 = 4294967296通りの入力を与える必要がある。しかし、実際の論理シミュレータの実行速度は、１秒あたり10000サイクルを越すことは稀である。
【０００４】
よって、上述の機能ブロックの入力に全ての状態を与えるだけで、4294967296/10000 = 429496.7 秒（約 119時間）必要である。更に、上述の機能ブロック内部の状態も含めて全事象を検証しようとすると、更に多くの時間が必要となる。即ち、開発期間中に全事象を網羅することは不可能であり、検証精度が低いことは否めない。
【０００５】
このような問題を解決するために、ランダム手法やカバレッジ手法が提案されている。ランダム手法とカバレッジ手法は共に、動的シミュレーションを効率良く実行し、短時間で検証精度を向上させる手法である。ランダム手法とカバレッジ手法導入以前と比較して検証精度は高まる。しかし、どちらの手法を用いても全事象を網羅した検証に必要な時間は短縮できない。即ち、開発期間中に検証精度を100％にすることはできない。
【０００６】
一方、論理シミュレータを用いないで論理システムを検証する手法として、静的検証がある。この静的検証手法は、論理システムの動作仕様と論理システムの設計データの等価性を数学的に判定することで検証を行うものである。そして、論理システムの状態を逐次的に生成する必要が無いため、全事象の検証に必要な時間は短い。
【０００７】
特許文献１には、論理システムのビヘイビアレベルの仕様記述と、前記仕様記述に対応したレジスタ転送レベル（ＲＴＬ）の記述とから、仕様記述とレジスタ転送レベルの記述との対応をとり、仕様記述を検証するためのテスト系列データをもとに、レジスタ転送レベルのテスト系列データを生成するテスト系列生成装置が開示されている。
【特許文献１】特開平07-254008号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかしながら、上述の静的検証手法では、動作仕様を正確に記述しないと正しく検証を行うことができない。また、動作仕様を記述した範囲のみが検証対象であり、動作仕様を記述していなければ検証対象にすらならない。
【０００９】
例えば、図２に示す機能ブロック３１を静的検証手法を用いて検証する際に、この機能ブロック３１内カウンタ３２の仕様が誤って仕様書に記載されていた場合、その仕様書に基づいてカウンタ３２の動作仕様を記述して静的検証を行うため、仕様と異なるカウンタになってしまう。
【００１０】
また、仕様書の記載が正しくとも動作仕様を記述する際に解釈を誤り間違った動作仕様を記述すると、上述の場合と同様に検証結果が誤ってしまう。或いは、機能ブロック３１の仕様書にＦＳＭ（Finite State Machine）３３の記述が無かった場合、ＦＳＭ３３の動作仕様を記述することはなく、ＦＳＭ３３の検証は実施されない。その結果、ＦＳＭ３３に誤りがあっても発見できない。
【００１１】
更に、論理システムの設計者が、意図せず機能ブロックや機能ブロック内の部品を作り込んでしまうことがある。例えば、信号Ａが有効な場合は機能Ａを選択し、また信号Ａが無効で、かつ信号Ｂが有効な場合は機能Ｂを選択するセレクタを設計し、このセレクタはアービタ機能も併せて持っているものとする。しかし、論理システムの設計者はアービタを設計しようと意図していたとは限らない。そのため、仕様書にはアービタ機能について記載されず、このような場合、アービタとしての検証は実施されない。
【００１２】
つまり、静的検証を用いて十分な検証精度を得るためには、機能ブロックを構成する部品の全てについて、詳細に記述された仕様書がなければならない。その上、仕様書に記載した仕様を十分理解して動作仕様を記述しなければならない。
【００１３】
ところが、論理システムの設計者が意図せず作り込んでしまった、機能ブロックや機能ブロック内の部品の仕様まで仕様書に記載することは不可能である。また、静的検証ツールに入力する動作仕様記述が必要かつ十分であるかを、客観的に判断する方法はこれまで存在しなかった。
【００１４】
そのため、検証対象から漏れる機能ブロックや機能ブロックの部品の存在を否定することができない。また、記述した動作仕様に誤りが無いとは言い切れない。
【００１５】
即ち、従来の方法では、十分な検証精度が得られるとは限らない。また、十分な検証精度が得られないことにより、精度を持つ論理システムを予定の期間内に完成させることができず、市場が欲するときに製品を投入できない、という問題や不十分な精度のまま製品を市場に投入してしまう、という問題が生じている。
【００１６】
本発明は、上述の課題を解決するためになされたもので、論理システムの設計データを論理検証するための動作仕様記述を容易に作成することを目的とする。
【課題を解決するための手段】
【００１７】
本発明は、論理システムの設計データを論理検証するための動作仕様記述に関する情報を出力する検証用情報出力方法であって、論理システムを検証するための複数の動作仕様記述に関する情報を格納する工程と、前記論理システムの設計データに基づいて前記格納された複数の動作仕様記述に関する情報から前記論理システムの設計データを論理検証するための動作仕様記述に関する情報を選択して出力する工程とを有することを特徴とする。
【００１８】
また、本発明は、論理システムの設計データを論理検証するための動作仕様記述に関する情報を出力する検証用情報出力装置であって、論理システムを検証するための複数の動作仕様記述に関する情報を格納する手段と、前記論理システムの設計データに基づいて前記格納された複数の動作仕様記述に関する情報から前記論理システムの設計データを論理検証するための動作仕様記述に関する情報を選択して出力する手段とを有することを特徴とする。
【発明の効果】
【００１９】
本発明によれば、論理システムの設計データを論理検証するための動作仕様記述を容易に作成することができる。
【発明を実施するための最良の形態】
【００２０】
以下、図面を参照しながら発明を実施するための最良の形態について詳細に説明する。尚、本実施形態では、論理検証装置が論理システムの論理検証を行う際に用いる動作仕様記述を出力する動作仕様記述出力装置の構成及び動作について説明する。
【００２１】
図１は、本実施形態における動作仕様記述出力装置の構成の一例を示す図である。図１に示すように、動作仕様記述出力装置１０は、内部表現変換器２１、比較器・選択器２２から構成されている。
【００２２】
ＲＴＬ（Register Transfer Level）ソースコード１１は、Verilog 或いはＶＨＤＬ（VHSIC Hardware Description Language）などのハードウェア記述言語で記述した論理システムの設計データである。テスト項目表１２は検証項目の一覧である。このテスト項目表１２は、開発する論理システムの全てに対して共通に使用するものであって、個々の論理システム毎に作成するものではない。尚、テスト項目表１２については図３を用いて更に後述する。
【００２３】
テンプレートライブラリ１３は、テンプレート生成手順２３によってテスト項目表１２から作成された動作仕様記述のテンプレートをライブラリとして保存しておくものである。尚、図１に示す例では、テンプレート生成手順２３及びテンプレートライブラリ１３は動作仕様記述出力装置１０の外部に接続されているが、動作仕様記述出力装置１０の内部に設けられていても良い。
【００２４】
内部表現変換器２１は、ＲＴＬソースコード１１とテンプレートライブラリ１３の動作仕様記述のテンプレートを内部で使用する内部表現（正規化論理表現）に変換する。比較器・選択器２２は、内部表現変換器２１でＲＴＬソースコード１１を変換した内部表現と動作仕様記述のテンプレートを変換した内部表現とを比較し、比較した結果が所定の条件（論理的等価性）を満たす場合、その動作仕様記述のテンプレートをＲＴＬソースコード１１の動作仕様記述テンプレート１４として出力する。
【００２５】
次に、本実施形態の内部表現変換器３２で変換される内部表現について説明する。上述した比較・選択器２２で内部表現の比較を行うために、本実施形態で使用する内部表現は同一の論理関数が同一の表現にならなければならない。また、容量が大きくならず、比較の手順が容易である必要がある。
【００２６】
同一の論理関数が同一の表現となる表現方法として、例えば二分決定グラフ（ＢＤＤ：Binary Decision Diagram）、真理値表、積和標準形が知られている。この真理値表は、入力数の指数乗の項を必要とする。また、積和標準形も最悪の場合、真理値表と同様に、入力数の指数乗の項を必要とする。しかし、ＢＤＤでは多くの場合、真理値表や積和標準形より少ない項で論理関数を表現可能である。また、真理値表と積和標準形では、内部表現への変換工数が論理関数の複雑度に影響し、複雑になるにつれて内部表現への変換工数が増加する。
【００２７】
一方、ＢＤＤでは、論理関数の複雑度に関係なく変換工数が決定するため、本実施形態では、内部表現としてＢＤＤを用いるものとする。勿論、内部表現はＢＤＤに限定されるものではなく、同一の論理関数が同一の表現になるならばどのような表現が用いられても良い。
【００２８】
ＢＤＤを内部表現に使用するプログラムや市販のツールでは、ＢＤＤ生成アルゴリズムとして、applyアルゴリズムが広く使用されている。このapplyアルゴリズムは、1984年にRandal E. Bryant氏により開発されたＢＤＤ生成アルゴリズムである。また、このapplyアルゴリズムは、既に数多く使用されており、公知の技術である。
【００２９】
そこで、上述した内部表現変換器３２は、ＲＴＬ１１やライブラリ１３をＢＤＤに変換する手法として、applyアルゴリズムを使用するものとする。
【００３０】
尚、本発明は、ＢＤＤ生成アルゴリズムに依存した発明ではないので、内部表現変換器２１が使用するアルゴリズムはapplyアルゴリズムに限定されるものではない。
【００３１】
次に、図３を用いて本実施形態におけるテスト項目表１２を説明し、更に図４を用いてテスト項目表１２から作成され、テンプレートライブラリ１３に保存される動作仕様記述のテンプレートについて説明する。
【００３２】
図３は、本実施形態におけるテスト項目表１２の一例を示す図である。図３に示す例では、項番3.1.2「リクエスト数３、ラウンド・ロビン型アービタ」と、項番4.1.2「初期値設定機能附きアップ・カウンタ」の項を抜き出している。
【００３３】
図４は、本実施形態における動作仕様記述テンプレートの一例を示す図である。図４に示すテンプレート５１は、テスト項目表１２の項番3.1.2「リクエスト数３、ラウンド・ロビン型アービタ」の動作仕様記述のテンプレートである。
【００３４】
ここで、テスト項目表１２の項番3.1.2のアービタは、リクエストＡ、リクエストＢ、リクエストＣの３つのリクエストの間の調停をラウンド・ロビンで行う。リクエストＡ、リクエストＢ、リクエストＣそれぞれの信号名をreq_a, req_b, req_cとする。
【００３５】
また、リクエスト数が３であるので、アービタの状態数も３である。そして、それぞれの状態名をstate_A, state_B, state_Cとする。state_Aは、リクエストＡに対して許可を与えているか、或いはリクエストＡが許可を得た後全てのリクエストが無効になっている状態を示している。state_B, state_Cも同様である。このアービタはラウンド・ロビン型であるため、現在の状態に依存し、リクエスト調停の優先順位が異なる。例えば、現在の状態がstate_Aならば、リクエストの優先順位は、以下のようである。
【００３６】
req_a ＜ req_c ＜ req_b
次に、動作仕様記述テンプレート５１で使用する記号の意味を以下に示す。
【００３７】
;         動作記述の区切り
a =＞ b   ａが成立するならばｂが成り立つ
&&        論理積
||        論理和
~         論理否定
'         次クロック・サイクルの状態
//        コメント
ここで、動作仕様記述テンプレート５１の中で、テンプレート（１）を例に動作記述の定義について説明する。
【００３８】
(state_A &&  req_a && ~req_b && ~req_c) =＞ '(state_A); // (1)
各項の意味を以下に示す。
【００３９】
state_A      :現在、アービタの状態は state_A
req_a        :リクエストＡは有効 
~req_b       :リクエストＢは無効
~req_c       :リクエストＣは無効
'(state_A)  : クロック・サイクルで state_A が有効
また、=＞の左辺  {(state_A &&  req_a && ~req_b && ~req_c)} は、「現在の状態が、state_A で、req_a のみ有効」を表し、=＞の右辺 {'(state_A)} は、「次クロック・サイクルの状態は state_A 」を表す。
【００４０】
従って、テンプレート（１）は、以下の動作記述を定義している。
【００４１】
「現在の状態が、state_A で、req_a のみ有効ならば、次クロック・サイクルの状態は state_A 」
以下、テンプレート（９）まで同様である。
【００４２】
テンプレート（１０）は以下の動作記述を定義している。
【００４３】
(state_A || state_B || state_C) =＞
'(state_A) || '(state_B) || '(state_C); // (10)
現在の状態が、state_A, state_B, state_Cの何れかならば、次クロック・サイクルでもstate_A, state_B, state_Cの何れかになる。つまり、このテンプレートは異常な状態に陥らないことを定義している。
【００４４】
このように、本実施形態では、テンプレート生成手順２３がテスト項目表１２から動作仕様記述テンプレート５１を生成する。この動作仕様記述テンプレート５１はテスト項目表１２を更新した場合に、更新した項目に関してのみ作成すれば良い。テストを実行する度に、或いは論理システム毎に生成する必要はない。また、作業量は少ないため、人手で動作仕様記述テンプレート５１を作成しても良いし、或いは自動生成ツールで作成しても良い。勿論、テストを実行する度に、或いは論理システム毎に生成するすることを妨げるものではない。
【００４５】
図５は、動作仕様記述テンプレート５１を内部表現変換器２１で変換したＢＤＤのうちstage_Aに関係する部分を示す図である。このＢＤＤは、次クロックサイクルのstage_Aを生成する論理関数を表している。即ち、図４に示す動作仕様記述テンプレート５１のうちテンプレート（１）〜（３）を変換すると、図５に示すＢＤＤになる。
【００４６】
次に、本実施形態における比較器・選択器２２の動作について説明する。この比較器・選択器２２は、ＲＴＬソースコード１１を内部表現変換器２１で変換したＢＤＤとテンプレートライブラリ１３の動作仕様記述テンプレートを内部表現変換器２１で変換したＢＤＤとの同形性を判定する。
【００４７】
つまり、両ＢＤＤが完全に一致するか、或いは、ＲＴＬソースコード１１から変換したＢＤＤが、動作仕様記述テンプレートから変換したＢＤＤを包含しているかを判定する。その結果、両ＢＤＤが完全に一致するか、或いは、ＲＴＬソースコード１１から変換したＢＤＤが動作仕様記述テンプレートから変換したＢＤＤを包含しているならば、動作仕様記述テンプレートが定義している機能ブロックや部品がＲＴＬソースコード１１中に存在する。即ち、テスト項目表１２に挙げた項目を検証する必要があることを示している。
【００４８】
ＢＤＤの同形性判定アルゴリズムは、従来より多くの提案が存在する。本発明は、同形性判定アルゴリズムに依存した発明ではないので、どの同形性判定アルゴリズムを用いても良い。例えば、ある節に注目し、'1'の枝の形と'0'の枝の形を再帰的に比較することで同形性を判定する手法を用いても良い。
【００４９】
次に、上述のＲＴＬソースコード１１の論理検証に用いられる動作仕様記述を出力する動作仕様記述出力装置１０の処理について説明する。
【００５０】
図６は、本実施形態における動作仕様記述を出力する処理を示すフローチャートである。尚、この処理は、ＲＴＬソースコード１１とテンプレートライブラリ１３とを入力したときから開始される。
【００５１】
ステップＳ６０１において、ＲＴＬソースコード１１を内部表現変換器２１でＢＤＤに変換し、内部で保持する。以下、変換後のＢＤＤを「ＢＤＤ（ＲＴＬ）」と呼ぶ。
【００５２】
次に、ステップＳ６０２において、テンプレートライブラリ１３から１つの動作仕様記述のテンプレートを取り出し、ステップＳ６０３では、その動作仕様記述のテンプレートを内部表現変換器２１でＢＤＤに変換する。以下、ステップＳ６０３で変換したＢＤＤを「ＢＤＤ（テンプレート）」と呼ぶ。
【００５３】
次に、ステップＳ６０４において、比較器・選択器２２が、ＢＤＤ（ＲＴＬ）とＢＤＤ（テンプレート）とを比較する。この比較結果に応じて、ステップＳ６０５とステップＳ６０６からステップＳ６０７へ処理を進める。
【００５４】
つまり、ステップＳ６０５で、ＢＤＤ（ＲＴＬ）とＢＤＤ（テンプレート）とが完全に同形であれば、ステップＳ６０７へ分岐する。また、完全に同形でなければ、ステップＳ６０６へ進み、ＢＤＤ（ＲＴＬ）がＢＤＤ（テンプレート）を包含しているか否かを判断する。ここで、包含していれば、ステップＳ６０７へ分岐するが、包含していなければ、ステップＳ６０８へ進む。
【００５５】
このステップＳ６０７では、ステップＳ６０２で選択した動作仕様記述のテンプレートをＲＴＬソースコード１１の動作仕様記述テンプレート１４として出力する。このステップへ進むことは、テスト項目表１２に挙げた項目をＲＴＬソースコード１１が含んでいることを示している。
【００５６】
次に、ステップＳ６０８において、テンプレートライブラリ１３内に未だ比較していない動作仕様記述のテンプレートが存在しているか否かを判定し、存在していないならば、上述した処理を終了する。また、未だ比較していない動作仕様記述のテンプレートが存在しているならば、ステップＳ６０２に戻り、上述の処理を繰り返す。
【００５７】
尚、上述したステップＳ６０７で出力した動作仕様記述テンプレート１４は、あくまで雛型（テンプレート）である。
【００５８】
従って、上述した生成処理を終了後、検証者は論理システムの仕様に基づき、動作仕様記述テンプレート１４から実際の動作仕様記述を作成する。そして、この動作仕様記述を使用して静的検証を行う。
【００５９】
このとき、仕様書に記載されていない機能ブロックの動作仕様記述テンプレートが存在する可能性がある。これは、仕様書の記載抜け、設計者が意図しない機能ブロックの生成が原因である。この動作仕様記述テンプレートが存在する場合は、仕様書とＲＴＬソースコード１１を再点検し、再点検した結果を仕様書の記述に反映させる。
【００６０】
［変形例］
次に、図面を参照しながら変形例における動作仕様記述出力装置の構成及び動作について説明する。
【００６１】
図７は、変形例における動作仕様記述出力装置の構成の一例を示す図である。尚、図１に示す動作仕様記述出力装置１０の構成と同様な機能を有するものには同一の符号を付し、その説明は省略する。
【００６２】
図７に示すように、変形例の動作仕様記述出力装置１００は、テンプレートライブラリ１３ではなく、ＢＤＤライブラリ１５を用いて動作仕様記述テンプレートを出力するものである。
【００６３】
また、テンプレートライブラリ１３の動作仕様記述のテンプレートはテスト項目表１２が更新された場合にのみ更新する。よって、内部表現変換器２１で、テンプレートライブラリ１３の動作仕様記述のテンプレートから毎回ＢＤＤを生成する必要は無く、動作仕様記述のテンプレートが更新された場合にのみ生成すれば、効率が良くなる。
【００６４】
そこで、変形例では、予め動作仕様記述のテンプレートを内部表現変換器２１で変換し、ＢＤＤライブラリ１５として保持しておく。このＢＤＤライブラリ１５を用いるため、変形例では処理の手順が変わる。
【００６５】
図８は、変形例における動作仕様記述を出力する処理を示すフローチャートである。まず、ステップＳ８０１において、本実施形態における図６に示すステップＳ６０１の処理と同様に、ＲＴＬソースコード１１を内部表現変換器２１でＢＤＤに変換し、内部で保持する。以下、このＢＤＤを「ＢＤＤ（ＲＴＬ）」と呼ぶ。
【００６６】
次に、ステップＳ８０２において、ＢＤＤライブラリ１５から１つの動作仕様記述テンプレートに対応したＢＤＤを取り出す。以下、このＢＤＤを「ＢＤＤ（テンプレート）」と呼ぶ。
【００６７】
次に、ステップＳ８０４〜Ｓ８０７において、本実施形態における図６に示すステップＳ６０４〜Ｓ６０７の処理と同様に、ステップＳ８０４で比較器・選択器２２が、ＢＤＤ（ＲＴＬ）とＢＤＤ（テンプレート）とを比較する。そして、ステップＳ８０５でＢＤＤ（ＲＴＬ）とＢＤＤ（テンプレート）とが完全に同形であれば、ステップＳ８０７へ分岐する。また、完全に同形でなければ、ステップＳ８０６へ進み、ＢＤＤ（ＲＴＬ）がＢＤＤ（テンプレート）を包含しているか否かを判断する。ここで、包含していれば、ステップＳ８０７へ分岐するが、包含していなければ、ステップＳ６０８へ進む。
【００６８】
このステップＳ８０７では、ステップＳ８０２でＢＤＤライブラリ１５から取り出したＢＤＤに対応する動作仕様記述のテンプレートをＲＴＬソースコード１１の動作仕様記述テンプレート１４として出力する。このステップへ進むことは、テスト項目表１２に挙げた項目をＲＴＬソースコード１１が含んでいることを示している。
【００６９】
次に、ステップＳ８０８において、ＢＤＤライブラリ１５内に未だ比較していないＢＤＤ、即ち、ＢＤＤ（テンプレート）が存在しているか否かを判定し、存在していないならば、上述した処理を終了する。また、未だ比較していないＢＤＤ、即ち、ＢＤＤ（テンプレート）が存在しているならば、ステップＳ８０２に戻り、上述の処理を繰り返す。
【００７０】
尚、本実施形態と同様に、ステップＳ８０７で出力した動作仕様記述テンプレート１４は、あくまで雛型（テンプレート）である。
【００７１】
よって、上述した生成処理を終了後、検証者は論理システムの仕様に基づき、動作仕様記述テンプレート１４から実際の動作仕様記述を作成する。そして、この動作仕様記述を使用して静的検証を行う。
【００７２】
このとき、仕様書に記載されていない機能ブロックの動作仕様記述テンプレートが存在する場合は、仕様書とＲＴＬソースコード１１とを再点検し、再点検した結果を仕様書の記述に反映させる。
【００７３】
以上説明した実施形態及び変形例によれば、テスト項目表１２に記載の機能ブロックが論理システム内に存在すれば、その機能ブロックを静的に検証する動作仕様記述テンプレートを出力し、その動作仕様記述テンプレートを用いることで、検証者は容易に静的検証に用いる動作仕様記述を作成することが可能となる。
【００７４】
また、仕様書に記載が無い機能ブロックや論理設計者が意図していない機能ブロックに対しても動作仕様記述テンプレートを出力でき、検証対象の機能ブロックを見逃す恐れが無くなる。
【００７５】
よって、十分な精度を持つ論理システムを予定の期間内に完成させることができ、市場が欲するときに製品を投入することが可能となる。
【００７６】
尚、本発明は複数の機器（例えば、ホストコンピュータ，インターフェース機器，リーダ，プリンタなど）から構成されるシステムに適用しても、１つの機器からなる装置（例えば、複写機，ファクシミリ装置など）に適用しても良い。
【００７７】
また、本発明の目的は、前述した実施形態の機能を実現するソフトウェアのプログラムコードを記録した記録媒体を、システム或いは装置に供給し、そのシステム或いは装置のコンピュータ（ＣＰＵ若しくはＭＰＵ）が記録媒体に格納されたプログラムコードを読出し実行することによっても、達成されることは言うまでもない。
【００７８】
この場合、記録媒体から読出されたプログラムコード自体が前述した実施形態の機能を実現することになり、そのプログラムコードを記憶した記録媒体は本発明を構成することになる。
【００７９】
このプログラムコードを供給するための記録媒体としては、例えばフロッピー（登録商標）ディスク，ハードディスク，光ディスク，光磁気ディスク，ＣＤ−ＲＯＭ，ＣＤ−Ｒ，磁気テープ，不揮発性のメモリカード，ＲＯＭなどを用いることができる。
【００８０】
また、コンピュータが読出したプログラムコードを実行することにより、前述した実施形態の機能が実現されるだけでなく、そのプログラムコードの指示に基づき、コンピュータ上で稼働しているＯＳ（オペレーティングシステム）などが実際の処理の一部又は全部を行い、その処理によって前述した実施形態の機能が実現される場合も含まれることは言うまでもない。
【００８１】
更に、記録媒体から読出されたプログラムコードが、コンピュータに挿入された機能拡張ボードやコンピュータに接続された機能拡張ユニットに備わるメモリに書込まれた後、そのプログラムコードの指示に基づき、その機能拡張ボードや機能拡張ユニットに備わるＣＰＵなどが実際の処理の一部又は全部を行い、その処理によって前述した実施形態の機能が実現される場合も含まれることは言うまでもない。
【図面の簡単な説明】
【００８２】
【図１】本実施形態における動作仕様記述出力装置の構成の一例を示す図である。
【図２】論理システムの機能ブロック３１の構成の一例を示す図である。
【図３】本実施形態におけるテスト項目表１２の一例を示す図である。
【図４】本実施形態における動作仕様記述テンプレートの一例を示す図である。
【図５】動作仕様記述テンプレート５１を内部表現変換器２１で変換したＢＤＤのうちstage_Aに関係する部分を示す図である。
【図６】本実施形態における動作仕様記述を出力する処理を示すフローチャートである。
【図７】変形例における動作仕様記述出力装置の構成の一例を示す図である。
【図８】変形例における動作仕様記述を出力する処理を示すフローチャートである。
【符号の説明】
【００８３】
１０  動作仕様記述出力装置
１１  ＲＴＬソースコード
１２  テスト項目表
１３  テンプレートライブラリ
１４  動作仕様記述テンプレート
１５  ＢＤＤライブラリ
２１  内部表現変換器
２２  比較器・選択器
２３  テンプレート生成手順
３１  機能ブロック
３２  カウンタ
３３  ＦＳＭ
３４  ランダム論理
３５  シーケンサ
５１  動作仕様記述テンプレート
【図１】
2006163599.tif 000003
【図２】
2006163599.tif 000004
【図３】
2006163599.tif 000005
【図４】
2006163599.tif 000006
【図５】
2006163599.tif 000007
【図６】
2006163599.tif 000008
【図７】
2006163599.tif 000009
【図８】
2006163599.tif 000010