(57)【要約】【課題】  論理システムの検証において非活性コードに対応する機能を含む非活性動作仕様記述を生成し、コードカバレッジ結果の解析を容易化する手段を提供する。【解決手段】  論理システム内の非活性コードを検出する手段と、論理システムにおける、検出された非活性コードを含む論理機能ブロックを抽出する手段と、論理機能ブロックにおいて非活性コードに至る論理関数を導出する手段と、非活性コードを含む論理機能ブロックの機能を特定する手段と、導出された論理関数と特定された機能の内容とを出力する出力手段とを有する。【選択図】図１
2006221473.tif 000002
【特許請求の範囲】
【請求項１】
ハードウェア記述言語で記述された論理システムの検証装置であって、
前記論理システム内の非活性コードを検出する検出手段と、
前記論理システムにおける、検出された前記非活性コードを含む論理機能ブロックを抽出する抽出手段と、
前記論理機能ブロックにおいて前記非活性コードに至る論理関数を導出する論理関数導出手段と、
前記非活性コードを含む論理機能ブロックの機能を特定する機能特定手段と、
導出された前記論理関数と特定された前記機能の内容とを出力する出力手段と、
を含む論理システムの検証装置。
【請求項２】
前記機能特定手段は、
前記非活性コードを含む論理機能ブロックと１以上の汎用的な論理機能ブロックとについての論理的等価性を判断することにより、前記非活性コードを含む論理機能ブロックの機能を特定することを特徴とする請求項１に記載の論理システムの検証装置。
【請求項３】
前記論理システムを、正規化論理表現による論理システムに変換する第１の変換手段と、
前記汎用的な論理機能ブロックを、正規化論理表現による汎用的な論理機能ブロックに変換する第２の変換手段と、
をさらに含み、
前記機能特定手段は、
前記正規化論理表現による論理システムと１以上の前記正規化論理表現による汎用的な論理機能ブロックとについての論理的等価性を判断することにより、前記非活性コードを含む論理機能ブロックの機能を特定することを特徴とする請求項１に記載の論理システムの検証装置。
【請求項４】
前記正規化論理表現は、２分決定グラフによる表現であることを特徴とする、請求項３に記載の論理システムの検証装置。
【請求項５】
ハードウェア記述言語で記述された論理システムの検証装置であって、
前記論理システムに対応した１以上の論理経路を、前記論理システム内の位置情報と共に導出する経路導出手段と、
前記論理システムを構成している１以上の論理機能ブロックの機能を、該機能ブロック毎に特定する機能特定手段と、
導出された前記論理経路および特定された前記機能の内容から１以上の動作記述を出力する動作記述出力手段と、
前記論理システム内の非活性コードを、前記論理システム内の位置情報と共に検出する検出手段と、
検出された前記非活性コードの位置情報に対応する前記動作記述を選択し出力する出力手段と、
を含む論理システムの検証装置。
【請求項６】
前記位置情報は論理システム内の行番号であることを特徴とする、請求項５に記載の論理システムの検証装置。
【請求項７】
ハードウェア記述言語で記述された論理システムの検証方法であって、
前記論理システム内の非活性コードを検出する検出工程と、
前記論理システムにおける、検出された前記非活性コードを含む論理機能ブロックを抽出する抽出工程と、
前記論理機能ブロックにおいて前記非活性コードに至る論理関数を導出する論理関数導出工程と、
前記非活性コードを含む論理機能ブロックの機能を特定する機能特定工程と、
導出された前記論理関数と特定された前記機能の内容とを出力する出力工程と、
を含む論理システムの検証方法。
【請求項８】
制御装置と記憶装置とを含むコンピュータに対し、
前記論理システム内の非活性コードを検出するステップと、
前記論理システムにおける、検出された前記非活性コードを含む論理機能ブロックを抽出するステップと、
前記論理機能ブロックにおいて前記非活性コードに至る論理関数を導出するステップと、
前記非活性コードを含む論理機能ブロックの機能を特定するステップと、
導出された前記論理関数と特定された前記機能の内容とを出力するステップと、
を実行させるためのハードウェア記述言語で記述された論理システムの検証するプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウェア記述言語で記述した論理システムの論理検証技術に関するものである。
【背景技術】
【０００２】
従来、論理システムの検証は論理シミュレーションを実施することにより行われており、その際の、検証確度に関する情報としては、コードカバレッジ情報が広く利用されている。コードカバレッジ情報とは、論理シミュレーション時に、回路記述内のどの記述が活性化されたかを記録した情報である。コードカバレッジ情報を参照することにより、設計者は、論理シミュレーションによってどの程度の回路記述が実行されたかを数値的に認識可能となり、検証確度を図る目安を得ることができる。なお、最近では、回路記述の各行が活性化されたか否かを判断する単純なステートカバレッジ情報に加え、各条件式が実行されているか否かを示すブランチカバレッジ情報等、複数種のコードカバレッジ情報を取得することが可能となり、より精度の高い検証確度に関する情報を得ることができるようになっている（特許文献１参照）。
【０００３】
設計者は、これらのコードカバレッジ情報に基づいて、マニュアルで回路記述の解析を行うことにより、論理シミュレーションで活性化されなかった記述（非活性コード）が以下に列挙する3つのコードのいずれであるかを判断する必要がある。
【０００４】
１つめは、論理的に活性化が不可能なコードである。このコードは、活性化されていない場合でも、再度論理シミュレーションをする必要はない。活性化が不可能なコードの例を図１４に示す。なお、各行の先頭の数字は行番号を示す。この例では、1ビットの信号sel が0の場合は6行目および7行目、1の場合は8行目および9行目に分岐するので、10行目、11行目はいずれの場合でも活性化できない。
【０００５】
２つめは、論理的に活性化が可能であり、システム仕様でサポートされている機能に関するコードである。このコードは、本来検証されるべき機能が検証されていないコードであり、検証項目の抽出もれ、あるいは論理シミュレーションの不足が原因と考えられる。この場合には、非活性コードを実行するためのテストを追加し、再度論理シミュレーションを実行する必要がある。なお、テスト追加および、論理シミュレーションは、設計者とは異なる検証担当者が行うのが一般的である。
【０００６】
３つめは、論理的に活性化が可能であるが、システム仕様ではサポートされない機能に関するコードである。このコードは、再利用したコードの一部の機能しか使わない場合などに起こる可能性があるコードである。この場合は、非活性コードを実行するためのテストを追加して再度論理シミュレーションを実行する必要はない。
【０００７】
活性化されていない機能およびその原因を特定した後、必要であれば追加でテストおよび、論理シミュレーションを行う。この工程を論理システムの全機能が十分検証されたと判断されるまで繰り返し行うことで、論理システムの品質を高めている。
【特許文献１】特開２００３−１９６３４２号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
上記手法によるコードカバレッジ情報を基にした結果解析では、設計者が回路記述をマニュアルで直接解析し、活性化されていない機能およびその原因の特定をしなければならないため多くの工数が必要である。
【０００９】
例えば、ある非活性コードに対応する機能が、回路記述の複数箇所にわたって記述されている場合、非活性コードに対応する機能を抽出するためには、非活性コードだけではなく、関連するコードをも読まねばならない。また、テスト追加のために必要となる、非活性コードを実行させるための条件は回路記述中の非活性コードとは異なる場所に書かれている場合も多いため、条件の抽出には困難性を伴う。
【００１０】
特に、近年の回路の大規模化、複雑化に伴い、設計者が解析する回路記述の量が膨大となり、より多くの工数が必要になっていることから、活性化されていない機能およびその原因の特定の容易化が課題となっている。
【課題を解決するための手段】
【００１１】
本発明は、たとえば、ハードウェア記述言語で記述された論理システムの検証装置であって、前記論理システム内の非活性コードを検出する検出手段と、前記論理システムにおける、検出された前記非活性コードを含む論理機能ブロックを抽出する抽出手段と、前記論理機能ブロックにおいて前記非活性コードに至る論理関数を導出する論理関数導出手段と、前記非活性コードを含む論理機能ブロックの機能を特定する機能特定手段と、導出された前記論理関数と特定された前記機能の内容とを出力する出力手段とを含む。
【００１２】
また、前記機能特定手段は、
前記非活性コードを含む論理機能ブロックと１以上の汎用的な論理機能ブロックとについての論理的等価性を判断することにより、前記非活性コードを含む論理機能ブロックの機能を特定することを特徴とする。
【００１３】
あるいは、前記論理システムを、正規化論理表現による論理システムに変換する第１の変換手段と、前記汎用的な論理機能ブロックを、正規化論理表現による汎用的な論理機能ブロックに変換する第２の変換手段とをさらに含み、前記機能特定手段は、前記正規化論理表現による論理システムと１以上の前記正規化論理表現による汎用的な論理機能ブロックとについての論理的等価性を判断することにより、前記非活性コードを含む論理機能ブロックの機能を特定することを特徴とする。
【００１４】
さらに、前記正規化論理表現は、２分決定グラフによる表現であることを特徴とする。
【発明の効果】
【００１５】
本発明によれば、論理システム内の機能ブロックの中で、論理シミュレーションで活性化されなかったコードに対する非活性動作仕様記述の出力が可能となる。その結果、コードカバレッジ情報を基にした結果解析を容易に行うことが可能となる。なお、ここで、非活性動作仕様記述とは、非活性コードを含む論理機能ブロックに対応する機能および非活性コードを活性化させるための条件を含む記述のことをいう。
【発明を実施するための最良の形態】
【００１６】
以下に、図面を参照して、この発明の好適な実施の形態を例示的に詳しく説明する。ただし、この実施の形態に記載されている構成要素はあくまで例示であり、この発明の範囲をそれらのみに限定する趣旨のものではない。
【００１７】
（第１実施形態）
＜装置構成＞
図１は、本発明の第１の実施形態における論理検証装置１００の装置構成および入力または出力されるデータを示す図である。
【００１８】
論理シミュレータ１０１はＲＴＬソースコード１１１に対し、論理シミュレーションを実行することにより、コードカバレッジを計測し、コードカバレッジ結果リストを出力する。コードカバレッジ結果リストは、ＲＴＬソースコード１１１の各行が論理シミュレーション中に活性化された回数を集計したリストである。コードカバレッジの計測およびコードカバレッジ結果リストの出力は、例えばMentor Graphics社のModelSim（Ｒ）などの既存の市販論理シミュレータをモジュールとして組み込んで実現してもよい。
【００１９】
なお、ＲＴＬ (Register Transfer Level) ソースコード１１１とはVerilog 、VHDLなどのハードウェア記述言語を用い記述された論理システムの設計データを意味する。
【００２０】
内部表現変換部１０３は、ＲＴＬソースコード１１１を本装置の内部で使用する内部表現に変換する。なお、内部表現とは装置内部で使用される後述する２分決定グラフなどの表現形式のことを意味する。また、内部表現変換部１０３内の論理関数導出部１０２は、コードカバレッジ結果リスト内の非活性コードに至る論理関数の導出を行う。内部表現変換部１０４は、論理システムにおいて共通・汎用的に使用される動作（カウンタやアービタなど）の１以上の動作仕様記述を含むテンプレート・ライブラリ１１２を、本装置の内部で使用する内部表現に変換する。
【００２１】
比較・選択部１０５は、内部表現で表したＲＴＬソースコード１１１と、内部表現で表したテンプレート・ライブラリ１１２内にある１以上のテンプレートとを比較し、出力部１０６では比較・選択部１０５における比較結果、および、論理関数導出部１０２で導出された論理関数を用いて、非活性コードに対する非活性動作仕様記述１１３を出力する。
【００２２】
ここで、非活性動作仕様記述とは、非活性コードに対応する機能および機能を活性化させるための条件を含む記述のことをいう。
【００２３】
＜論理表現方法およびその生成アルゴリズム＞
比較・選択部１０５で内部表現の比較をおこなうためには、同一の論理関数について同一の表現であることが望ましい。このような表現方法として２分決定グラフ：ＢＤＤ(Binary Decision Diagram)、真理値表、積和標準形がある。
【００２４】
ただし、真理値表は入力数の指数乗の項数を必要とし、積和標準形も最悪の場合、真理値表と同じく入力数の指数乗の項数を必要とする。また、真理値表と積和標準形では、内部表現への変換工数が論理関数の複雑度に影響し、複雑になるにつれて内部表現への変換工数が増加する。
【００２５】
しかし、ＢＤＤでは多くの場合、真理値表や積和標準形より少ない項数で論理関数を表現可能であるとともに、論理関数の複雑度に関係なく変換工数が決定できるという性質がありより好適である。
【００２６】
そのため、本実施形態においては容量が肥大化せず、比較の手順も容易な内部表現であるＢＤＤを用いて説明することとする。ただし、内部表現はＢＤＤには限定されず、同一の論理関数が同一の表現となる表現方法ならばいかなる表現を用いてもよい。
【００２７】
ＢＤＤを内部表現に使用するプログラムや市販のツールでは、ＢＤＤ生成アルゴリズムとして、applyアルゴリズムが広く使用されている。このapplyアルゴリズムは1984年にRandal E. Bryant氏により開発されたＢＤＤ生成アルゴリズムである。このapplyアルゴリズムは、既に数多く使用されている技術である。そこで、内部表現変換部１０３、および内部表現変換部１０４は、ＲＴＬソースコード１１１あるいは動作記述テンプレート１１２をＢＤＤに変換する手法としてapplyアルゴリズムを使用する。ただし、内部表現変換部１０３および内部表現変換部１０４が使用するＢＤＤ生成アルゴリズムをapplyアルゴリズムに限定するものではない。
【００２８】
＜機能ブロックおよびその動作仕様記述の一例＞
図２は、ＲＴＬソースコード１１１が表す機能ブロックの一例を示す図である。ここでは、機能ブロック２００は内部にカウンタ２０１、アービタ２０２、ランダム論理２０３、およびシーケンサ２０４を含んでいる。以下ではアービタ２０２を例に動作仕様記述を説明する。
【００２９】
図３は、カウンタやアービタなど論理システムにおいて共通・汎用的に使用される動作の一覧表である回路ブロック表の一例を示す図である。この図において、項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」と、項番 4.1.2 「初期値設定機能付アップ・カウンタ」の項のみ抜き出して表示している。
【００３０】
図４は、回路ブロック表の項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」のテンプレート１１２の一例を示す図である。
【００３１】
回路ブロック表の項番 3.1.2 のアービタは、リクエストＡ、リクエストＢ、リクエストＣの３リクエスト間の調停を、ラウンド・ロビンでおこなう。リクエストＡ、リクエストＢ，リクエストＣそれぞれの信号名を、rｅｑ＿ａ，ｒｅｑ＿ｂ，ｒｅｑ＿ｃとする。また、リクエスト数が３であるので、アービタの状態数も３である。それぞれの状態名を、ｓｔａｔｅ＿Ａ，ｓｔａｔｅ＿Ｂ，ｓｔａｔｅ＿Ｃとする。state_A は、リクエストＡに対して許可を与えているか、あるいはリクエストＡが許可を得たのち全てのリクエストが無効になっている状態を示している。state_B, state_C も同様である。この、アービタはラウンド・ロビン型であるため、現在の状態に依存して、リクエスト調停の優先順位が異なる。例えば、現在の状態がｓｔａｔｅ＿Ａならば、リクエストの優先順位は、
ｒｅｑ＿ａ  ＜  ｒｅｑ＿ｃ  ＜  ｒｅｑ＿ｂ
である。
【００３２】
なお、動作仕様記述テンプレート１１２で使用している記号の意味は以下の通りである。
【００３３】
；        動作記述の区切り
ａ＝＞ｂ  aが成り立つならばbが成り立つ
＆＆      論理積
｜｜      論理和
￣        論理否定
’        次クロック・サイクルの状態
記号“／／”より右の部分はコメント部である。
【００３４】
動作仕様記述テンプレート１１２の中の、行(1) 
（ｓｔａｔｅ＿Ａ＆＆ｒｅｑ＿ａ＆＆￣ｒｅｑ＿ｂ＆＆  ￣ｒｅｑ＿ｃ）＝＞’（ｓｔａｔｅ＿Ａ）；
を例に取ると、各項の意味は以下の通りである。
【００３５】
ｓｔａｔｅ＿Ａ        : 現在、アービタの状態はｓｔａｔｅ＿Ａ
ｒｅｑ＿ａ            : リクエストＡは有効 
￣ｒｅｑ＿ｂ          : リクエストＢは無効
￣ｒｅｑ＿ｃ          : リクエストＣは無効
’（ｓｔａｔｅ＿Ａ）  : 次クロック・サイクルでｓｔａｔｅ＿Ａが有効
よって、行(1) は、以下の動作記述を定義している。
【００３６】
「現在の状態が、ｓｔａｔｅ＿Ａかつｒｅｑ＿ａのみ有効ならば、次クロック・サイクルの状態はｓｔａｔｅ＿Ａ」
以下、行(9) までほぼ同様であり、行(10) 
（ｓｔａｔｅ＿Ａ｜｜ｓｔａｔｅ＿Ｂ｜｜ｓｔａｔｅ＿Ｃ）＝＞’（ｓｔａｔｅ＿Ａ）｜｜’（ｓｔａｔｅ＿Ｂ）｜｜’（ｓｔａｔｅ＿Ｃ）；
は以下の動作記述を定義している。
【００３７】
「現在の状態が、ｓｔａｔｅ＿Ａ，ｓｔａｔｅ＿Ｂ，ｓｔａｔｅ＿Ｃのいずれかならば、次クロック・サイクルでもｓｔａｔｅ＿Ａ，ｓｔａｔｅ＿Ｂ，ｓｔａｔｅ＿Ｃのいずれかになる」
つまり、この動作仕様記述テンプレート１１２は異常な状態に陥らないことを定義している。
【００３８】
動作仕様記述テンプレート１１２は回路ブロック表を元に生成され、回路ブロック表を更新した場合に、更新した項目に関してのみ作成すればよい。つまり、テストを実行するたび、あるいは論理システムごとに生成する必要はない。動作仕様記述テンプレート１１２生成は容易であるため、マニュアルで作成してもよいし、あるいは自動生成ツールで作成してもよい。
【００３９】
図５は、テンプレート・ライブラリ１１２内のテンプレートを内部表現変換部１０４で変換したＢＤＤのうち、ｓｔａｇｅ＿Ａに関係する部分を示す図である。このＢＤＤは、次クロック・サイクルのｓｔａｇｅ＿Ａを生成する論理関数を表している。すなわち、図４に示す動作仕様記述テンプレート１１２のうち、行(1)〜(3) を変換すると図５に示すＢＤＤになる。
【００４０】
＜非活性コードに至る論理関数の導出＞
次に論理関数導出部１０２（図１では内部表現変換部１０３の内部に存在）で行われる、非活性コードに至る論理関数の導出について説明する。
【００４１】
図６はコードカバレッジ結果リストの一部を抜き出した例を示す図である。各行の最初の数字は、ＲＴＬソースコード１１１の行番号である。そして、各行の2番目の数は論理シミュレーション中にその行が活性化された回数を示している。行38および行39はこの数字が０なので、非活性コードに相当する。次に、行38および行39に対応する論理関数を導出する。ＲＴＬソースコード１１１からの論理関数導出については、ソフトウェアコンパイラに用いられている構文解析技術を用いることが可能である。例えば、行39から論理関数の導出は以下のように行われてもよい。
【００４２】
まず、行39から行を遡り、行39を実施するための条件分岐を探索する。この場合は行38のelse文が発見できる。さらに行を遡り、else文に対応するif文、elsif文を求める。この場合は行34および行36が発見できる。そこで、行34,36からelse文に到達する条件を求める。さらにprocess文の開始まで行を遡り、if文に到達する条件を求める。この場合は行33のcase文が発見できる。こうして発見された条件の論理積を計算する。ここでは、結果として
Ｍａｓｔｅｒ０  ＊  ｈｂｕｓｒｅｑ１＝’０’  ＊ｈｂｕｓｒｅｑ２＝’０’
が得られる。
【００４３】
続いて、内部表現変換部１０３では、内部表現変換部１０４と同様の手法により、ＲＴＬソースコード１１１をＢＤＤに変換する。なお、生成されたＢＤＤに上記の方法で求めた論理関数を入力することにより、非活性コードに対応したＢＤＤの経路を求めることが出来る。
【００４４】
図７に図６に示される非活性コードを含む動作ブロックに対応するＢＤＤを示す。なお、太線は非活性コードに対応するＢＤＤの経路である。
【００４５】
＜比較・選択部の動作＞
次に、比較・選択部１０５の動作について説明する。比較・選択部１０５は、ＲＴＬソースコード１１１を内部表現変換部１０３で変換した ＢＤＤ と、動作仕様記述テンプレートを内部表現変換部１０４で変換した ＢＤＤ の同形性を判定する。ここで、同型性の判定とは両ＢＤＤが完全に一致するか、あるいは、ＲＴＬソースコード１１１から変換した ＢＤＤ が、動作仕様記述テンプレートから変換した ＢＤＤ を包含しているかを判定することである。両 ＢＤＤが完全に一致するか、あるいは、ＲＴＬソースコード１１１から変換した ＢＤＤ が、動作仕様記述テンプレートから変換した ＢＤＤ を包含しているならば、動作仕様記述テンプレートが定義している機能ブロックや部品が ＲＴＬソースコード１１１中に存在し、対応するテンプレートの機能を有することが分かる。
【００４６】
この場合には、ＲＴＬソースコード１１１から変換した ＢＤＤに、非活性コードに対応する経路が含まれているか判定する。含まれていた場合には、非活性コードに対応する経路について、両ＢＤＤの比較から、動作仕様記述テンプレート１１２の各信号に対応するＲＴＬソースコード１１１における信号名を求める。そして、動作仕様記述テンプレート１１２の各信号をＲＴＬソースコード１１１中の信号に置き換えることにより、非活性コードに対応する非活性動作仕様記述１１３を出力する。
【００４７】
図８は、図４に示した動作仕様記述テンプレートから生成された非活性動作仕様記述１１３の例を示す図である。これは、現在の状態が、Master0 で、hbusreq0 のみ有効ならば、次クロック・サイクルの状態は Master0であることを示している。
【００４８】
ＢＤＤ の同形性判定アルゴリズムは、多くの提案が存在するが、いずれの同形性判定アルゴリズムを用いてもよい。例えば、ある節に注目し、'1' の枝の形と '0' の枝の形を再帰的に比較することで同形性を判定する手法を用いてもよい。
【００４９】
＜全体動作＞
図９は本実施形態における論理検証装置の動作を説明するフローチャートである。この処理は、ＲＴＬソースコード１１１と動作記述仕様テンプレート１１２を読み込んだ時点から開始される。なお、各機能部分の動作の詳細については既に述べたため、ここでは、動作の流れを中心に説明する。
ステップＳ９０１では、論理シミュレータ１０１はＲＴＬソースコード１１１を読み込むと共に、論理シミュレーションを実行し、コードカバレッジを計測する。
【００５０】
ステップＳ９０２では、論理シミュレータ１０１はコードカバレッジ計測の結果として、ＲＴＬソースコード１１１中のコードカバレッジ結果リストを出力する。
【００５１】
ステップＳ９０３では、コードカバレッジ結果リストの中に、非活性コード（参照回数がゼロのコード）が存在するか否かを調べる。一箇所も存在しない場合には、ＲＴＬソースコード１１１ を解析する必要はないと判断しフローを終了する。一方、非活性コードが存在する場合にはステップＳ９０４に進む。
【００５２】
ステップＳ９０４はＲＴＬソースコード１１１を内部表現変換部１０３で ＢＤＤ に変換し、内部で保持する。さらに、前述したように、非活性コードに対応したＢＤＤの経路を求め保持しておく。なお、このステップで変換されたＢＤＤ を以降では“ＢＤＤ(ＲＴＬ)”と表記することとする。
【００５３】
ステップＳ９０５では、動作仕様記述テンプレート１１２から１つのテンプレートを取り出す。
【００５４】
ステップＳ９０６では、ステップＳ９０２で取り出したテンプレートを内部表現変換部１０４でＢＤＤ に変換する。以降ではステップＳ９０６で変換した ＢＤＤ を ”ＢＤＤ(template) ”と表記することとする。
【００５５】
ステップＳ９０７では、比較・選択部１０５で、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) を比較する。比較した結果により、ステップＳ９０８とステップＳ９０９の動作が変化する。
【００５６】
ステップＳ９０８で、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) が完全に同形と判断しならば、ステップＳ９１０に分岐する。このステップに進むことは、動作仕様記述テンプレート１１２（回路ブロック表に挙げた項目）を ＲＴＬソースコード１１１が含んでいることを示している。完全に同形で無いならば、ステップＳ９０９に進む。
【００５７】
ステップＳ９０９で、ＢＤＤ(ＲＴＬ) がＢＤＤ(template) を包含していると判断したならば、ステップＳ９１０に分岐する。包含していないならば、ステップＳ９１２に進む。
【００５８】
ステップＳ９１０では、出力部１０６においてＢＤＤ(ＲＴＬ)が非活性コードに対応した経路を含むか否かを判定する。含んでいると判定された場合はステップＳ９１１へ進む。含んでいないと判定された場合にはステップＳ９１２に進む。
【００５９】
ステップＳ９１１では、選択した動作仕様記述テンプレート１１２を用いて非活性動作仕様記述１１３を導出する。これは図４に示した動作仕様記述テンプレート１１２のうち、非活性コードに対応した経路に対応して、信号名をＢＤＤ(ＲＴＬ)の信号名に置き換えることにより行われる。
【００６０】
ステップＳ９１２では、動作終了条件を判定する。テンプレート・ライブラリ１１２内に未だ比較していないテンプレートが存在していないならば、動作を終了する。未だ比較していないテンプレートが存在しているならば、ステップＳ９０５に戻り動作を続ける。
【００６１】
以上の動作によって、入力されたＲＴＬソースコード１１１に対応する、非活性動作仕様記述１１３が導出される。非活性動作仕様記述を利用することにより、活性化されていないコードの機能およびその原因の特定のための大量のソースコードを読む作業の多くを省略可能となる。また、非活性動作仕様記述を解析することで、論理シミュレーションで活性化されなかった機能に内在するバグを発見しやすくなるという効果もある。
【００６２】
本実施形態では、非活性動作仕様のみを出力する構成としたが、非活性動作仕様を求める過程で得られた情報をあわせて出力することも可能である。例えば、非活性コードに対応する論理式やＢＤＤなどを同時に出力する構成にしてもよい。
【００６３】
また、非活性コードを含むＲＴＬソースコード１１１内の機能ブロックが、テンプレート１１２（または、元となる回路ブロック表）に予め登録されていない場合には、非活性動作仕様を出力しない構成としたが、この場合にも該当する非活性コード、または非活性コードに対応する論理式を出力する構成にしてもよい。
【００６４】
＜コンピュータによる実施＞
図１０は、実施形態に係る検証方法を実行可能なコンピュータの一例を示す図である。本発明に係る検証装置は、上述の検証機能に特化した検証装置として実現することもできるが、図１０で説明するようなコンピュータ１０００で検証用のコンピュータプログラムを実行することによっても実現できる。
【００６５】
ＣＰＵ１００１は、コンピュータ１０００の各部を統括的に制御する制御装置である。ＲＯＭ１００２は、ブートプログラムなどを記憶する不揮発性の記憶装置である。ＲＡＭ１００３は、ワークエリアとして機能する揮発性の記憶装置である。ハードディスクドライブ（ＨＤＤ）１００４は、大容量の記憶装置であり、ＲＴＬソースコード１０１１、テンプレート・ライブラリ１０１２、非活性コード検出プログラム１０１３、論理関数導出プログラム１０１４、内部表現変換プログラム１０１５、非活性動作仕様出力プログラム１０１６などが記憶される。表示制御部１００５は、表示装置１００６の表示制御を実行する制御回路である。表示装置１００６は、ＣＲＴや液晶表示装置等である。
【００６６】
なお、ＲＴＬソースコード１０１１は上述のＲＴＬソースコード１１１に相当し、テンプレート・ライブラリ１０１２は上述のテンプレート・ライブラリ１１２に相当し、非活性コード検出プログラム１０１３は上述の論理シミュレータ１０１にほぼ相当し、論理関数導出プログラム１０１４は上述の論理関数導出部１０２に相当し、内部表現変換プログラム１０１５は上述の内部表現変換部１０３、１０４に相当し、非活性動作仕様出力プログラム１０１６は上述の出力部１０６に相当することは言うまでもない。
【００６７】
コンピュータ１０００における、ＲＴＬソースコード１０１１の検証の処理については、上述した処理フローと同様であるので、以下図９を参照して説明する。
【００６８】
ステップＳ９０１において、ＣＰＵ１００１は、ＲＴＬソースコード１０１１を読み出し、コードカバレッジ計測などの機能を持つ非活性コード検出プログラム１０１３を実行する。
【００６９】
ステップＳ９０２では、ＣＰＵ１００１は、非活性コード検出プログラム１０１３の実行結果として、ＲＴＬソースコード１１１中のコードカバレッジ結果リストなどにより非活性コードの検出結果を出力する。
【００７０】
ステップＳ９０３では、ＣＰＵ１００１は、ＲＴＬソースコード１０１１の中に非活性コードが存在したか否かを調べる。一箇所も存在しない場合には、ＲＴＬソースコード１０１１ を解析する必要はないと判断しフローを終了する。一方、非活性コードが存在する場合にはステップＳ９０４に進む。
【００７１】
ステップＳ９０４では、ＣＰＵ１００１は、ＲＴＬソースコード１０１１を内部表現変換プログラム１０１５を実行することによりＢＤＤに変換し、内部で保持する。さらに、論理関数導出プログラム１０１４を実行することにより、非活性コードに至る論理関数を導出し保持しておく。なお、このステップで変換されたＢＤＤ を以降では“ＢＤＤ(ＲＴＬ)”と表記することとする。
【００７２】
ステップＳ９０５では、ＣＰＵ１００１は、テンプレート・ライブラリ１０１２から１つのテンプレートを読み出す。
【００７３】
ステップＳ９０６では、ＣＰＵ１００１は、ステップＳ９０５で取り出したテンプレートに対して内部表現変換プログラム１０１５を実行することによりＢＤＤ に変換する。以降ではステップＳ９０６で変換した ＢＤＤ を ”ＢＤＤ(template) ”と表記することとする。
【００７４】
ステップＳ９０７では、ＣＰＵ１００１は、非活性動作仕様出力プログラム１０１６内の比較・選択機能を実行することにより、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) を比較する。比較した結果により、ステップＳ９０８とステップＳ９０９の動作が変化する。
【００７５】
ステップＳ９０８で、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) が完全に同形と判断しならば、ステップＳ９１０に分岐する。このステップに進むことは、テンプレート（回路ブロック表に挙げた項目）を ＲＴＬソースコード１１１が含んでいることを示している。完全に同形で無いならば、ステップＳ９０９に進む。
【００７６】
ステップＳ９０９で、ＢＤＤ(ＲＴＬ) がＢＤＤ(template) を包含していると判断したならば、ステップＳ９１０に分岐する。包含していないならば、ステップＳ９１２に進む。
【００７７】
ステップＳ９１０では、ＣＰＵ１００１は、ステップＳ９０４で導出した論理関数を用いて、ＢＤＤ(ＲＴＬ)が非活性コードに対応した経路を含むか否かを判定する。含んでいると判定された場合はステップＳ９１１へ進む。含んでいないと判定された場合にはステップＳ９１２に進む。
【００７８】
ステップＳ９１１では、ＣＰＵ１００１は、非活性動作仕様出力プログラム１０１６内の非活性動作仕様記述生成機能を実行することにより、選択したテンプレートを用いて非活性動作仕様記述１１３を導出する。これは図４に示したテンプレートのうち、非活性コードに対応した経路に対応して、信号名をＢＤＤ(ＲＴＬ)の信号名に置き換えることにより行われる。
【００７９】
ステップＳ９１２では、ＣＰＵ１００１は、動作終了条件を判定する。テンプレート・ライブラリ１１２内に未だ比較していないテンプレートが存在していないならば、動作を終了する。未だ比較していないテンプレートが存在しているならば、ステップＳ９０５に戻り動作を続ける。
【００８０】
以上の動作によって、入力されたＲＴＬソースコード１０１１に対応する、非活性動作仕様記述１１３が導出される。非活性動作仕様記述を利用することにより、活性化されていないコードの機能およびその原因の特定のための大量のソースコードを読む作業の多くを省略可能となる。また、非活性動作仕様記述を解析することで、論理シミュレーションで活性化されなかった機能に内在するバグを発見しやすくなるという効果もある。
【００８１】
（第２実施形態）
以下、本発明の第２の実施形態を図面を参照しながら説明する。なお、装置構成および動作フローにおいて第１実施形態との相違が存在する。ただし、装置構成内の個々の構成部の動作に関しては、第１実施形態における同様の構成部名の動作とほぼ同一であるため詳細な説明は省略する。
【００８２】
＜装置構成＞
図１１に本実施形態における装置構成図を示す。第１実施形態においてはコードカバレッジ結果リストを内部表現変換部１０３へ入力し、内部表現で表現された非活性コードと動作仕様記述テンプレートを照らし合わせることにより非活性動作仕様記述１１３を出力していた。一方、本実施形態においては、コードカバレッジ結果リストを選択・出力部１１０２へ入力し、予め導出しておいたＲＴＬソースコード１１１１に対応する動作仕様記述と、ＲＴＬソースコードにおける位置（行番号など）を比較することにより、非活性動作仕様記述１１１３を出力する。動作仕様記述はＲＴＬソースコード１１１１あるいは、テンプレート・ライブラリ１１１２が更新された場合にのみ更新が必要となる。よって、ＲＴＬソースコード１１１１およびテンプレート・ライブラリ１１１２に変更を加えずにシミュレーション条件のみを変化させる場合、ＢＤＤを１回のシミュレーション毎に、生成、比較する必要がないため、論理シミュレーションの回数が多くなる場合において、第１実施形態における装置に比較し動作効率の向上が期待される。
【００８３】
内部表現変換部１１０３においては、第１実施形態と同様、ＲＴＬソースコード１１１の各行に対応するＢＤＤの経路を算出する。
【００８４】
比較・選択部１１０５においては、ＢＤＤ（ＲＴＬ）がＢＤＤ（template）と完全に一致するか、あるいは、包含しているならば、両ＢＤＤの比較から、テンプレートの各信号に対応するＲＴＬソースコード１１１１内での信号名、および行番号を求める。そして、テンプレートの各信号をＲＴＬソースコード１１１１中の信号に置き換えることにより、動作仕様記述を出力する。この際に選択・出力部１１０２での非活性コードとの対応付けを容易にするために、各動作仕様に対応する行番号を含めておく。図１２に、比較・選択部１１０５から出力される動作仕様記述の例を示す。
【００８５】
選択・出力部１１０２では動作仕様記述に含まれる行番号と、コードカバレッジ結果リストに含まれる非活性コードの行番号から、非活性コードに対応する動作仕様のみを選択し、非活性動作仕様記述１１１３として出力する。
【００８６】
＜全体動作＞
図１３は本発明の第２実施形態に係る装置の動作を説明するフローチャートである。この処理は、ＲＴＬソースコード１１１１とテンプレート・ライブラリ１１１２を入力から開始される。
【００８７】
ステップＳ１３０１では、ＲＴＬソースコード１１１１を内部表現変換部１１０３でＢＤＤに変換し、内部で保持する。この際に、ＲＴＬソースコードの各行に対応したＢＤＤの経路についても保存しておく。このステップで変換されたＢＤＤをＢＤＤ(ＲＴＬ)と呼ぶことにする。
【００８８】
ステップＳ１３０２では、テンプレート・ライブラリ１１１２から１つのテンプレートを取り出す。
【００８９】
ステップＳ１３０３では、ステップＳ１３０２で取り出したテンプレートを内部表現変換部１１０４でＢＤＤに変換する。ステップＳ１３０３で変換したＢＤＤをＢＤＤ(template)と呼ぶことにする。
【００９０】
ステップＳ１３０４では、比較器・選択部１１０５で、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) の同型性について判定する。判定した結果により、ステップＳ１３０５またはステップＳ１３０６においてフローが分岐する。
【００９１】
ステップＳ１３０５で、ＢＤＤ(ＲＴＬ) とＢＤＤ(template) が完全に同型と判断しならば、ステップＳ１３０７に分岐する。このステップに進むことは、テンプレート・ライブラリ１１１２、つまり、元々は回路ブロック表に挙げた回路をＲＴＬソースコード１１１１が含んでいることを示している。完全に同型で無いならば、ステップＳ１３０６に進む。
【００９２】
ステップＳ１３０６で、ＢＤＤ(ＲＴＬ) がＢＤＤ(template) を包含していると判断したならば、ステップＳ１３０７に分岐する。包含していないならば、ステップＳ１３０８に進む。
【００９３】
ステップＳ１３０７で選択したテンプレートを用いて動作仕様記述を導出する。動作仕様記述は、図４に示したテンプレートの信号名をＢＤＤ(ＲＴＬ)の信号名に置き換えることにより生成される。また、各動作仕様記述に対応するＲＴＬソースコードの行番号をステップＳ１３０１で保存したＢＤＤの経路から求め、動作仕様記述とあわせて出力する。
【００９４】
ステップＳ１３０８では、テンプレート・ライブラリ１１１２内のテンプレートについて全て比較が終了するとステップＳ１３０９へ進む。比較していないテンプレートが存在しているならば、ステップＳ１３０２に戻り、比較していないテンプレートの１つを選択し、ステップＳ１３０３〜ステップＳ１３０７に示した動作と同様の動作を実行する。
【００９５】
ステップＳ１３０９はＲＴＬソースコード１１１１を論理シミュレータ１１０１に入力し、論理シミュレーションを実行し、コードカバレッジを計測する。
【００９６】
ステップＳ１３１０では、論理シミュレータ１１０１はコードカバレッジ計測の結果として、ＲＴＬソースコード１１１１中のコードカバレッジ結果リストを出力する。
【００９７】
ステップＳ１３１１では、コードカバレッジ結果リストの中に、非活性コードが存在するか否かを調べる。一箇所も存在しない場合には、ＲＴＬソースコード１１１１ を解析する必要はないと判断し終了する。一方、１以上の非活性コードが存在する場合にはステップＳ１３１２に進む。
【００９８】
ステップＳ１３１２では、選択・出力部１１０２において、非活性コードの行番号と一致している動作仕様記述を選択して非活性動作仕様記述として出力する。
【００９９】
以上説明したとおり本実施形態によれば、論理システムの検証を、ＲＴＬソースコード１１１１およびテンプレート・ライブラリ１１１２に変更を加えずにシミュレーション条件のみを変化させて行う場合、２回目以降はステップＳ１３０１からステップＳ１２０８に相当する動作の省略が可能となる。そのため、論理シミュレーションの回数が多い場合、第１実施形態における装置に比較し、より短時間で非活性動作仕様記述の出力が可能となる。
【０１００】
（他の実施形態）
以上、本発明の実施形態について詳述したが、本発明は、複数の機器から構成されるシステムに適用しても良いし、また、一つの機器からなる装置に適用しても良い。
【０１０１】
なお、本発明は、前述した実施形態の機能を実現するプログラムを、システム或いは装置に直接或いは遠隔から供給し、そのシステム或いは装置が、供給されたプログラムコードを読み出して実行することによっても達成される。従って、本発明の機能処理をコンピュータで実現するために、コンピュータにインストールされるプログラムコード自体も本発明の技術的範囲に含まれる。
【０１０２】
その場合、プログラムの機能を有していれば、オブジェクトコード、インタプリタにより実行されるプログラム、ＯＳに供給するスクリプトデータ等、プログラムの形態を問わない。
【０１０３】
プログラムを供給するための記録媒体としては、例えば、フロッピー（登録商標）ディスク、ハードディスク、光ディスク、光磁気ディスク、ＭＯ、ＣＤ−ＲＯＭ、ＣＤ−Ｒ、ＣＤ−ＲＷ、磁気テープ、不揮発性のメモリカード、ＲＯＭ、ＤＶＤ（ＤＶＤ−ＲＯＭ，ＤＶＤ−Ｒ）などがある。
【０１０４】
その他、プログラムの供給方法としては、クライアントコンピュータのブラウザを用いてインターネットのホームページに接続し、ホームページから本発明のコンピュータプログラムそのもの、もしくは圧縮され自動インストール機能を含むファイルをハードディスク等の記録媒体にダウンロードすることによっても供給できる。また、本発明のプログラムを構成するプログラムコードを複数のファイルに分割し、それぞれのファイルを異なるホームページからダウンロードすることによっても実現可能である。つまり、本発明の機能処理をコンピュータで実現するためのプログラムファイルを複数のユーザに対してダウンロードさせるＷＷＷサーバも、本発明のクレームに含まれるものである。
【０１０５】
また、本発明のプログラムを暗号化してＣＤ−ＲＯＭ等の記憶媒体に格納してユーザに配布し、所定の条件をクリアしたユーザに対し、インターネットを介してホームページから暗号化を解く鍵情報をダウンロードさせ、その鍵情報を使用することにより暗号化されたプログラムを実行してコンピュータにインストールさせて実現することも可能である。
【０１０６】
また、コンピュータが、読み出したプログラムを実行することによって、前述した実施形態の機能が実現される他、そのプログラムの指示に基づき、コンピュータ上で稼動しているＯＳなどが、実際の処理の一部または全部を行い、その処理によっても前述した実施形態の機能が実現され得る。
【０１０７】
さらに、記録媒体から読み出されたプログラムが、コンピュータに挿入された機能拡張ボードやコンピュータに接続された機能拡張ユニットに備わるメモリに書き込まれた後、そのプログラムの指示に基づき、その機能拡張ボードや機能拡張ユニットに備わるＣＰＵなどが実際の処理の一部または全部を行い、その処理によっても前述した実施形態の機能が実現される。
【図面の簡単な説明】
【０１０８】
【図１】第１実施形態における論理検証装置の装置構成図である。
【図２】機能ブロックの一例を示す図である。
【図３】回路ブロック表の一実施例を示す図である。
【図４】テンプレートの一例を示す図である。
【図５】テンプレートから生成したＢＤＤの一例を示す図である。
【図６】コードカバレッジ結果リストの一例を示す図である。
【図７】非活性コードを含む動作ブロックに対応するＢＤＤの一例を示す図である。
【図８】非活性動作仕様記述の一例を示す図である。
【図９】第１実施形態の論理検証装置の動作フローである。
【図１０】第１実施形態をコンピュータにより実現する際の構成を示す図である。
【図１１】第２実施形態における論理検証装置の装置構成図である。
【図１２】動作仕様記述の一例を示す図である。
【図１３】第２実施形態の論理検証装置の動作フローである。
【図１４】活性化不可能なコードの一例を示す図である。
【図１】
2006221473.tif 000003
【図２】
2006221473.tif 000004
【図３】
2006221473.tif 000005
【図４】
2006221473.tif 000006
【図５】
2006221473.tif 000007
【図６】
2006221473.tif 000008
【図７】
2006221473.tif 000009
【図８】
2006221473.tif 000010
【図９】
2006221473.tif 000011
【図１０】
2006221473.tif 000012
【図１１】
2006221473.tif 000013
【図１２】
2006221473.tif 000014
【図１３】
2006221473.tif 000015
【図１４】
2006221473.tif 000016