(57)【要約】【課題】  機能ブロックを構成する部品まで詳細にかつ正確に記述された仕様書があれば、静的検証を容易に使用可能である。しかし、機能ブロックを構成する部品までの詳細な記述が仕様書になされていない場合、静的検証ツールに入力する動作仕様を抽出することができない。また、機能ブロックを構成する部品の抽出が困難になり、個々の部品ごとに静的検証を適応することが不可能になる。【解決手段】  ハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動生成された動作仕様記述と別途入力した動作仕様記述を比較する論理検証補助装置であり、動作仕様記述の不足、冗長性を示すことで、客観的な動作仕様記述の評価を下す手段を提供する。【選択図】  図２
2007026370.tif 000002
【特許請求の範囲】
【請求項１】
ハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動生成された動作仕様記述と別途入力した動作仕様記述を比較する論理検証補助装置であって、
前記ハードウエア記述言語で記述された論理システムを論理表現に変換し最適化をおこない正規化論理表現を生成する正規化論理表現生成手段と、
論理システムの構成部品である機能ブロックに対応する動作仕様記述の正規化論理表現を記録する機能ブロック保持手段と、
前記機能ブロック保持手段から正規化論理表現を選択し前記正規化論理表現生成手段で生成した正規化論理表現と比較をおこない論理的等価性を判定する比較手段と、
前記比較手段で論理的に一致すると判定されたならば,前記機能ブロック保持手段から選択した正規化論理手段を記録する正規化論理表現保持手段と、
別途入力した動作仕様記述を正規化論理表現に変換する手段と、
前記別途入力した動作仕様記述から生成された正規化論理表現と前記正規化論理表現保持手段で保持している正規化論理表現を比較する動作仕様記述比較手段と、
前記動作仕様記述比較手段において動作仕様の違いを表示する手段とを持つことを特徴とするハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動生成された動作仕様記述と別途入力した動作仕様記述を比較する論理検証補助装置。
【請求項２】
請求項１に記載された動作仕様記述比較手段は、
前記別途入力した動作仕様記述から生成された正規化論理表現と前記正規化論理表現保持手段で保持している正規化論理表現とを前記論理的等価性を判定する比較手段を用いての各項の比較において、
正規化論理表現の違いを把握し、
前記別途入力した動作仕様記述から生成された正規化論理表現が前記正規化論理表現保持手段で保持している正規化論理表現に含まれる場合、
検証者にその差分を表示し、検証者が別途入力した動作仕様記述へ差分の追加を指示したならば、動作仕様記述を追加することを特徴とする論理検証補助装置。
【請求項３】
請求項１に記載された動作仕様記述比較手段は、
前記別途入力した動作仕様記述から生成された正規化論理表現と前記正規化論理表現保持手段で保持している正規化論理表現とを前記論理的等価性を判定する比較手段を用いての各項の比較において、
正規化論理表現の違いを把握し、
前記正規化論理表現保持手段で保持している正規化論理表現が前記別途入力した動作仕様記述から生成された正規化論理表現に含まれる場合、
検証者にその差分を表示し、別途入力した動作仕様記述の冗長性をユーザに確認することを特徴とする論理検証補助装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は集積回路の論理検証装置および方法に関するものである。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年毎に増加している。それに伴い、論理システムの検証にかかる工数も増加している。一方、市場には消費者が欲するときに製品を投入しなければならず、ＬＳＩを始めとした論理システムの開発期間は短くなっている。そのため、論理システム検証の効率向上を図る必要が生じている。
【０００３】
従来より、ＬＳＩを含む論理システムの検証には、論理シミュレータを用いた動的検証が使用されてきた。動的検証は、論理シミュレータを用いて論理システムを動作させて検証をおこなうため、検証にかかる時間が長い。そのため、全ての事象を実現するためには膨大な時間を必要とする。例えば、３２ｂｉｔの入力を持つ機能ブロックを検証する場合、2 ^ 32 = 4294967296 通りの入力を与える必要がある。しかし、論理シミュレータの実行速度は、1秒あたり１００００サイクルを越すことは稀である。よって、上記機能ブロックの入力に全ての状態を与えるだけで、4294967296/10000 = 429496.7 秒（約 119 時間）必要である。さらに、上記機能ブロック内部の状態も含めて全事象を検証しようとすると、更に多くの時間が必要となる。すなわち、開発期間中に全事象を網羅することは不可能であり、検証精度が低いことは否めない。
【０００４】
この課題を解決するために、ランダム手法やカバレッジ手法が提案されている。ランダム手法とカバレッジ手法は共に、動的シミュレーションを効率よく実行して、短時間で検証精度を高める手法である。ランダム手法とカバレッジ手法導入以前と比較して、検証精度は高まる。しかし、どちらの手法を用いても全事象を網羅した検証に必要な時間は短縮できない。すなわち、開発期間中に検証精度を 100 % にすることはできない。
【０００５】
一方、論理シミュレータを用いずに論理システムを検証する手法として、静的検証がある。この静的検証手法は、論理システムの動作仕様と論理システムの設計データの等価性を数学的に判定することで検証をおこなう。論理システムの状態を逐次的に生成する必要が無いため、全事象の検証に必要な時間は短い。
【０００６】
図３にある機能ブロック３１を静的検証を用いて検証する場合の例を示す。機能ブロック３１を検証する場合、機能ブロック３１全てに静的検証を適応するのではなく、機能ブロック３１を構成する、カウンタ３２、FSM（Finite State Machine）３３、ランダム論理回路３４、シーケンサ３５といった部品ごとに静的検証を実施する。個々の部品の検証は終了したので、最後に各部品間と接続、および各部品と機能ブロック３１間の接続を確認すれば、ブロック３１の検証は終了する。各部品間と接続、および各部品と機能ブロック３１間の接続確認は、動的シミュレーション手法と静的検証手法のいずれかを用いることになる。
【０００７】
又、従来例としては、例えば特許文献１をあげることが出来る。
【特許文献１】特開2001-101250号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
機能ブロックを構成する部品まで詳細にかつ正確に記述された仕様書があれば、静的検証を容易に使用可能である。しかし、機能ブロックを構成する部品までの詳細な記述が仕様書になされていない場合、静的検証ツールに入力する動作仕様を抽出することができない。また、機能ブロックを構成する部品の抽出が困難になり、個々の部品ごとに静的検証を適応することが不可能になる。すなわち、十分な精度を持つ動作仕様記述を作成することができなくなり、動作仕様記述に不足が生じる可能性がある。動作仕様記述が不足すると機能ブロックの検証精度が低下し、その結果、不十分な精度のままの製品を市場に投入してしまう可能性がある。
【０００９】
また、仕様書が詳細に書かれていたとしても、ユーザが仕様の解釈を間違えて動作仕様記述が不足する可能性があり、この場合正しい検証は行えない。また、冗長な動作仕様記述を作成した場合、可読性が悪くなり保守が困難になるといった問題も生じる。
【００１０】
上記問題を解決するためには、不足がなく、冗長でない動作仕様記述を用いる必要があるが、動作仕様記述に不足、冗長性があっても客観的に判断できる手段がないといった課題が存在する。
【課題を解決するための手段】
【００１１】
本発明に係わる論理検証補助装置はハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動生成された動作仕様記述と別途入力した動作仕様記述とを比較する論理検証補助装置であって、
前記ハードウエア記述言語で記述された論理システムを論理表現に変換し最適化をおこない正規化論理表現を生成する正規化論理表現生成手段と、
論理システムの構成部品である機能ブロックに対応する動作仕様記述の正規化論理表現を記録する機能ブロック保持手段と、
前記機能ブロック保持手段から正規化論理表現を選択し前記正規化論理表現生成手段で生成した正規化論理表現と比較をおこない論理的等価性を判定する比較手段と、
前記比較手段で論理的に一致すると判定されたならば,前記機能ブロック保持手段から選択した正規化論理手段を記録する正規化論理表現保持手段と、
正規化論理表現を動作仕様記述に変換する手段と、
別途入力した動作仕様記述を正規化論理表現に変換する手段と、
前記別途入力した動作仕様記述から生成された正規化論理表現と前記正規化論理表現保持手段で保持している正規化論理表現を比較する動作仕様記述比較手段と、
前記動作仕様記述比較手段において動作仕様の違いを表示する手段とを持つことを特徴とする。
【発明の効果】
【００１２】
以上、本発明によれば予め登録された動作仕様記述と別途入力した動作仕様記述の違いを調べ表示することで、別途入力した動作仕様記述の漏れ、冗長性を示唆することができ、動作仕様記述の客観的な品質評価判断の補助手段となり、明らかな不足に関しては動作仕様記述のテンプレートを補完することで動作仕様記述の作成における省力化に貢献できる。本発明により論理システム開発の検証工程においてバグの早期発見に繋げることができる。
【発明を実施するための最良の形態】
【００１３】
（実施例１）
以下、図面を参照しながら本発明の実施形態を説明する。
【００１４】
図１は請求項１で記載のハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置を利用した本発明の一実施例を示す図である。Register Transfer Level(以下RTL) source code １１はVerilog あるいは VHDL で記述した論理システムの設計データである。テスト項目表１２は、検証項目の一覧である。この テスト項目表１２は、開発する論理システム全てに対して共通に使用するものであって、個々の論理システムごとに作成するものではない。テスト項目表１２から、動作記述のテンプレートをテンプレート生成手順２３で作成し、内部表現変換器２１を用いて動作記述のテンプレートを本発明の内部で使用する内部表現に変換する。変換した内部表現は内部表現ライブラリ１３に保存する。RTL source code １１を内部表現変換器２１を用いて内部表現に変換する。比較器・選択器２２は、内部表現で表した RTL source code と、動作記述のテンプレートを比較し、比較結果が条件を満たすならばその内部表現を比較一致内部表現１４に格納する。
【００１５】
比較・選択器２２で内部表現の比較をおこなうため、本発明で使用する内部表現は同一の論理関数が同一の表現にならなければならない。本実施例では同一の論理関数が同一の表現となる表現方法の一例として、BDD (Binary Decision Diagram) を用いる。
【００１６】
内部表現変換器２１は、RTL source code １１あるいは動作記述のテンプレート１３をBDD に変換する手法として apply アルゴリズムを使用する。この apply アルゴリズムは 1984 に Randal E. Bryant 氏により開発された、BDD 生成アルゴリズムである。この apply アルゴリズムは、既に数多く使用されており、公知の技術である。
【００１７】
評価対象動作仕様記述１５は別途入力した動作仕様記述である。本装置では比較一致内部表現１４中のBDDと評価対象動作仕様記述１５を内部表現変換器２１を用いてBDDに変換したものとを比較器２４を用いて比較し、その結果の表示２５を行う。
【００１８】
テスト項目表１２の一実施例を図４に示す。図４に示す実施例では、項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」と、項番 4.1.2 「初期値設定機能附きアップ・カウンタ」の項を抜き出している。
【００１９】
動作記述テンプレート１４の一実施例５１を図５に示す。図５に示す実施例は、テスト項目表１２の項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」の動作記述テンプレートである。
【００２０】
動作仕様記述テンプレート５１中、テンプレート (1) を例に取る。
【００２１】
(state_A &&  req_a && ~req_b && ~req_c) => '(state_A);
各項の意味を以下に示す。
【００２２】
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 」
を表す。
【００２４】
よって、テンプレート (1) は、以下の動作記述を定義している。
【００２５】
「現在の状態が、state_A で、req_a のみ有効ならば、
次クロック・サイクルの状態は state_A 」
以下、テンプレート (9) まで同様である。
【００２６】
テンプレート (10) は以下の動作記述を定義している。
【００２７】
(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のいずれかになる。つまり、このテンプレートは異常な状態に陥らないことを定義している。
【００２８】
評価対象動作仕様記述１５の一実施例６１を図６に示す。図６に示す実施例は、テスト項目表１２の項番3.1.2「リクエスト数 3、ラウンド・ロビン型アービタ」の動作仕様記述をユーザが書いた一実施例６１である。
【００２９】
図５で示した動作仕様テンプレート１４を内部表現変換器２１にかけると以下の４つのBDDが作成される。
【００３０】
１．次のステージがState_Aであることを示す（１）〜（３）までをまとめたBDD
２．次のステージがState_Bであることを示す（４）〜（６）までをまとめたBDD
３．次のステージがState_Cであることを示す（７）〜（９）までをまとめたBDD
４．次のステージで異常な状態に陥らないことを示す（１０）BDD
図６で示した評価対象動作仕様記述１５を内部表現変換器２１にかけると以下の３つのBDDが作成される。
【００３１】
１．次のステージがMaster０であることを示す（１）〜（３）までをまとめたBDD
２．次のステージがMaster１であることを示す（４）〜（６）までをまとめたBDD
３．次のステージがMaster２であることを示す（７）〜（９）までをまとめたBDD
動作仕様テンプレート５１と評価対象動作仕様記述６１では内部表現変換器２１を用いて生成されるBDDが違うことがわかる。図５と図６を比較器２４を用いて比較すると、BDDの違いからユーザに対して評価対象動作仕様記述の差分を表示する。図５の動作記述テンプレート５１の最終行には前記異常な状態に陥らないことを示したデッドロックを判定する動作仕様（１０）が記述されているが、図６の評価対象動作仕様記述６１には記述されていない。これは、評価対象の記述漏れの可能性が高いと考えられるが、本装置では、動作記述テンプレートにある論理が、評価対象動作仕様記述にない場合にはその旨を表示する。
【００３２】
（実施例２）
請求項２、３に記載された比較一致内部表現１４と評価対象動作仕様記述１５の正規化論理表現との比較結果の違いから生じるテンプレートの補完機能についての実施例を示す。
【００３３】
図２は請求項２，３で記載の動作仕様記述の不足、冗長性を表示する機能を有したハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置を示す図である。
【００３４】
図２中の結果の表示２５は別途入力した動作仕様記述が不足している可能性のある不足可能性動作仕様記述１６と別途入力した動作仕様記述が冗長な可能性のある冗長可能性動作仕様記述１７の２つに分けることができる。この比較の結果を、ユーザ判断２６にてユーザが動作仕様記述の不足、冗長性を判断し、ユーザがテンプレートの補完の必要性を認めた場合は動作記述テンプレートを評価対象動作仕様記述１５に補完する２７。
【００３５】
図７は32ビット・カウンタ７１、１６ビット・カウンタ７２、8ビットカウンタ７３を構成要素として持つDUTに対してのRTLソースコードから自動生成された動作記述テンプレート７４とユーザが仕様から生成した評価対象動作仕様記述７５を示したものである。動作記述テンプレート７４では３２ビット・カウンタ７１、１６ビット・カウンタ７２、８ビット・カウンタ７３それぞれについての動作仕様が記述されているが、ユーザが記述した評価対象動作仕様記述７５では８ビット・カウンタ７３に対する動作仕様が記述されていない。この場合、比較器２４において論理表現の不一致が起きるため、本装置はユーザに対して動作仕様記述不足を問いかける。ここで、ユーザが自身の動作仕様記述の不足を認めた場合には該当する動作記述テンプレートを評価対象動作仕様記述７６に補完する。この違いの原因として評価対象の動作仕様記述に漏れが生じている可能性が考えられるが、一方で、RTLソースコードに冗長な部分がある可能性もあり、その判断は検証者であるユーザ自身に任せる必要がある。
【００３６】
次に動作仕様記述テンプレート１４と評価対象動作仕様記述１５を比較し、その結果、評価対象動作仕様記述に冗長な記述がある実施例を示す。図８はある32ビット・カウンタ８１、１６ビット・カウンタ８２を構成要素として持つDUTに対してのRTLソースコードから自動生成された動作記述テンプレート８３とユーザが仕様から生成した評価対象動作仕様記述８４を示したものである。動作記述テンプレート７３では３２ビット・カウンタ８１、１６ビット・カウンタ８２の2つのカウンタについて動作仕様が記述されているが、ユーザが記述した評価対象動作仕様記述８４では不要な８ビット・カウンタの動作仕様が記述されている。この場合、比較器２４において動作仕様記述の不一致が起きるため、本装置はユーザに対して評価対象動作仕様記述８４の冗長性を問いかける。ユーザはこの警告を受けて、自身の評価対象動作仕様記述８４と動作記述テンプレート８３を検討し、自身の評価対象動作仕様記述８４が冗長であると認めた場合は、該当する動作仕様記述（この例では８ビット・カウンタの動作仕様）を削除し、冗長性を無くした評価対象動作仕様記述８５を作成する。この例では評価対象動作仕様記述が冗長である可能性が考えられるが、一方で、RTLソースコードに不足している部分がある可能性もあり、その判断は検証者であるユーザ自身に任せられる。
【００３７】
図９を用いて本装置の動作を説明する。
【００３８】
Ｓ００１  RTL source code １１を内部表現変換器２１で BDD に変換
Ｓ００２  テンプレート・ライブラリ１３から、１つの動作記述テンプレートを取り出す
Ｓ００３  Ｓ００１で取り出した動作記述テンプレートを内部表現変換器２１でBDD に変換
Ｓ００４  比較器・選択器２２で、Ｓ００１で変換した BDD と、Ｓ００３で変換した BDD を比較
Ｓ００５  両 BDD が一致したならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００６  Ｓ００３で変換した BDD がＳ００１で変換した BDD を包含しているならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００７  Ｓ００２で選択した動作記述テンプレートを出力
このステップに進むことは、テスト項目表１２に挙げた項目を RTL source code １１が含んでいることを示している。
【００３９】
Ｓ００８  テンプレート・ライブラリ１３内に未使用の動作記述テンプレートが存在していないならば動作記述テンプレート作成作業を終了
未使用の動作記述テンプレートが存在しているならば、Ｓ００２に戻る。
【００４０】
テンプレート・ライブラリ１３に登録した動作記述テンプレートの全てに対して比較をおこなうことで、RTL source code １１中にテスト項目表１２に挙げた項目に関わる機能ブロックや部品が存在するならば、対応する動作記述テンプレート１４を出力する。検証者は、この動作記述テンプレート１４を基に実際の動作記述を作成し、静的検証をおこなうことが可能である。
【００４１】
このとき、仕様書に記載の無い機能ブロックの動作仕様記述テンプレートが存在する可能性がある。これは、仕様書の記載抜け、設計者が意図しない機能ブロックの生成が原因である。この動作仕様記述テンプレートが存在する場合は、仕様書とRTL source code １１を再点検する。再点検した結果は仕様書の記述に反映させる。
【００４２】
ここまでの手順において動作仕様記述テンプレートが作成される。以下の手順は動作仕様記述テンプレートと別途入力した動作仕様記述との比較手順である。
【００４３】
Ｓ００９  ユーザ等が評価対象動作仕様記述１５を作成
Ｓ０１０  Ｓ００７で作成された動作記述テンプレート１４をBDDに変換
Ｓ０１１  Ｓ００９で作成された評価対象動作仕様記述１５をBDDに変換
Ｓ０１２  比較器２４で、Ｓ０１０で変換したBDDと、Ｓ０１１で変換したBDDを比較
Ｓ０１３  両BDDが一致したならば、評価対象動作仕様記述１５に誤りはないのでそのまま終了
Ｓ０１４  両BDDが一致しないならば、不一致情報を表示する。
【００４４】
Ｓ０１５  Ｓ０１４において機能ブロックを構成する部品の数の違いがある場合、動作記述テンプレート１４を補完するかどうかユーザに尋ねる。ユーザが補完を望まなければそのまま終了。
【００４５】
Ｓ０１６  Ｓ０１５で指定した動作記述テンプレート１４を評価対象動作仕様記述１５に貼り付ける。
【図面の簡単な説明】
【００４６】
【図１】本発明における論理検証補助装置の構成を示す図である。
【図２】一般的な検証項目の機能ブロックの構成を示す図である。
【図３】一般的なテスト項目リストを示す図である。
【図４】本発明における動作記述テンプレートを示す図である。
【図５】本発明における評価対象動作仕様記述を示す図である。
【図６】本発明におけるテンプレートの補完機能を示す図である。
【図７】本発明における評価対象動作仕様記述の冗長性を確認する図である。
【図８】本発明における評価対象動作仕様記述の冗長性を確認する図である。
【図９】本発明における論理検証補助装置の動作を示す図である。
【符号の説明】
【００４７】
１１  RTL source code
１２  テスト項目表
１３  内部表現ライブラリ
１４  比較一致内部表現
１５  評価対象動作仕様記述
２１  内部表現変換器
２２  比較器・選択器
２３  動作仕様記述テンプレート生成
２４  比較器
２５  結果の表示
２６  ユーザ判断
２７  テンプレート補完
３１  機能ブロック
３２  カウンタ
３３  FSM
３４  ランダム論理
３５  シーケンサ
５１  動作仕様記述テンプレート
６１  評価対象動作仕様記述
７１  ３２ビット・カウンタ
７２  １６ビット・カウンタ
７３  ８ビット・カウンタ
７４  自動生成された動作仕様記述テンプレート
７５  評価対象動作仕様記述
７６  テンプレート補完済み評価対象動作仕様記述
８１  ３２ビット・カウンタ
８２  １６ビット・カウンタ
８３  自動生成された動作仕様記述テンプレート
８４  評価対象動作仕様記述
８５  冗長なものを削除した評価対象動作仕様記述
【図１】
2007026370.tif 000003
【図２】
2007026370.tif 000004
【図３】
2007026370.tif 000005
【図４】
2007026370.tif 000006
【図５】
2007026370.tif 000007
【図６】
2007026370.tif 000008
【図７】
2007026370.tif 000009
【図８】
2007026370.tif 000010
【図９】
2007026370.tif 000011