(57)【要約】【課題】  機能ブロックや機能ブロックを構成する部品を抽出し、検証項目の追加および検証されたことを判断するカバレッジファイルを生成する手段を提供し、短期間で高精度な検証もれ防止手法を提供する。【解決手段】  テスト項目表に挙げた検証項目に係わる機能ブロックの機能・テンプレート・ライブラリを作成しておく。この機能・テンプレート・ライブラリと論理システムの RTL source code と比較し、機能ブロックが論理システム内に存在するかを判定する。存在する場合、検証項目とカバレッジファイルを出力する。【選択図】  図１
2007026177.tif 000002
【特許請求の範囲】
【請求項１】
ハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置において、
論理関数を論理表現に変換し最適化をおこない正規化論理表現を生成する正規化論理表現生成手段と、
論理システムの構成部品である機能ブロックの機能および対応する動作仕様記述を記録する機能ブロック保持手段と、
前記ハードウエア記述言語で記述された論理システムと前記機能ブロック保持手段内の動作仕様記述をそれぞれ前記正規化論理表現生成手段で正規化論理表現に変換する変換手段と、
前記変換手段で正規化論理表現に変換した前記ハードウエア記述言語で記述された論理システムと前記機能ブロック保持手段内の動作仕様記述の論理的等価性を判定する比較手段と、
前記比較手段で論理的に一致すると判定されたならば前記機能ブロック保持手段内の機能を検証項目として登録する手段と、
前記検証項目登録手段により出力された検証項目が、論理検証において検証されたか判定を行う検証判定手段とを具備することを特徴とするハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し、該当する検証項目を出力し、論理検証における検証判定手段を生成する装置。
【請求項２】
前記正規化論理表現は、２分決定グラフ (Binary Decision Diagram : BDD) であることを特徴とする請求項１記載のハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置。
【請求項３】
前記機能ブロック保持手段に記録する前記論理システムの構成部品である機能ブロックは、前記ハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置を用いた論理検証の有効性が予め確認された機能ブロックであることを特徴とする請求項１、あるいは請求項２記載のハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置。
【請求項４】
前記比論理的等価性を判定する比較手段は、前記機能ブロック保持手段から選択した正規化論理表現と前記正規化論理表現生成手段で生成した正規化論理表現が一致、あるいは前記機能ブロック保持手段から選択した正規化論理表現が前記正規化論理表現生成手段で生成した正規化論理表現を含むならば、論理的等価であると判定することを特徴とする、請求項１、請求項２、および請求項３記載のハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置。
【請求項５】
前記登録された検証項目が検証されたか判定するための検証判定手段は、前記機能ブロックの正規化論理表現に関わる条件の活性度を観測するカバレッジファイルを生成し、論理検証時に上記検証項目のカバレッジ結果を出力することを特徴とする、請求項１、請求項２、請求項３、および請求項４記載のハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し、等価な論理検証項目を登録し、検証項目の検証判定手段を生成する装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウエア記述言語により記述された論理システムと動作仕様記述の等価性を判定し、等価な論理検証項目を登録し、検証項目の検証判定手段を生成する装置に関する。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年毎に増加している。それに伴い、論理システムの複雑度は指数関数的に上昇し、要求仕様を満たす機能を検証する困難度も増加している。一方、市場では信頼性の高い商品が求められており、不具合が生じた場合は回収費等を伴い、ブランド力の低下を招き、競合他社に対する競争力の低下は事業存続に対する支障を伴う。そのため、論理システム検証の信頼性の向上を図る必要が生じている。
【０００３】
従来より、論理シミュレータを用いた動的検証や、動作仕様と設計データの等価性を数学的に判定する静的検証などが行われてきた。いずれの検証手法においても、ＬＳＩを含む論理システムが要求仕様を満たしていることを検証するためには、論理システムの仕様書等に記載された機能を検証項目として洗い出し、それぞれの検証項目の機能カバレッジアイテムを判断するファイルを作成して、それら検証項目が前記検証手法において検証されたことを確認する手法がとられてきた。たとえばreq_a，req_b，req_c３つの要求信号が発行され続けた場合にreq_a→req_b→req_c→req_aの順に公平な優先度で調停を行った結果、１つの要求信号に対して許可信号を与えることでstate_A, state_B, state_Cに移行するラウンドロビン型の調停回路の機能カバレッジを考えてみる。図１０において、req_a，req_b，req_c３つの要求信号が発行されたことの判断が行３〜１８、状態間の遷移が生じたかの判断が行１９〜２２を示している。行３において、req_a信号が変化した場合にreq_a_chgイベントが発生したら、行５においてreq_aの値がreq_a_chgカバレッジアイテムとして登録される。以下同様である。
【０００４】
又、従来例としては、例えば特許文献１と特許文献２と特許文献３をあげることが出来る。
【特許文献１】特登録2831816号公報
【特許文献２】特登録3373641号公報
【特許文献３】特開2001-142918号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
しかし、論理システムの仕様書等に機能が記述されていない場合、検証項目を抽出することができない。またたとえ要求仕様を満たした論理システムを設計した場合でも、設計支援ツール等を使用して設計することで設計者が意図しない機能ブロックが生成されることで不具合が生ずる場合がある。たとえば仕様書に記述されておらず、設計者が意図しない調停回路が機能ブロックとして生成されていた場合、調停回路の機能は正常であったとしても、調停回路に入力される信号に特定の制約条件があった場合、不具合が生じる場合があるにもかかわらず検出できない。req_a，req_b，req_c３つの要求信号が発行され続けた場合にreq_a→req_b→req_c→req_aの順に公平な優先度で調停を行った結果、１つの要求信号に対して許可信号を与えることでstate_A, state_B, state_Cに移行するラウンドロビン型の調停回路を考えてみる。req_cは要求信号を常に、状態がstate_Ａであり、かつreq_bと同時に発行し、かつ状態がstate_Bに移行すると発行を中止するといった制約条件があった場合、調停回路の機能が正常でありかつreq_cの要求信号が出力されているにもかかわらず、state_Ｃの状態になり得ないという不具合が生ずる。
【０００６】
このような場合、検証項目として抽出できないため不具合を検出することができず、市場にて欠陥として発覚する恐れがあるという課題が生じる。このように、仕様書に記述されてない、もしくは意図されない機能ブロックを、検証項目として抽出・登録する必要がある。
【０００７】
本発明は、上記課題を解決するためになされたもので、短時間で、正確に、漏れなく機能ブロックを構成する部品を抽出し、抽出された機能ブロックの論理検証項目を登録し、登録された検証項目が検証されたか判定するための検証判定手段を提供する。
【課題を解決するための手段】
【０００８】
本出願に係わる第１の発明は、論理システムの正規化論理表現を生成する正規化論理表現生成手段と、動作仕様記述の正規化論理表現を記録する機能ブロック保管手段と、論理的等価性を判定する比較手段と、論理検証項目を登録する論理検証項目登録手段と、論理検証において検証されたか判定するための検証判定手段を具備することを特徴とする。
【発明の効果】
【０００９】
以上説明したように、本発明によれば、テスト項目表に記載の機能ブロックが論理システム内に存在すれば、その機能ブロックの検証項目を追加する。またその検証項目が検証されたことを判断するためのカバレッジファイルを生成する。このカバレッジファイルを使用して論理シミュレーションを行えば、そのブロックの検証が行われているかを判断できる。
【００１０】
また、仕様書に記載が無い論理ブロックや、論理設計者が意図していない機能ブロックのに対しても検出できるため、仕様書のみからでは見逃す恐れが大きい機能ブロックの検証を見逃す恐れが無い。
【００１１】
その結果、本発明は、機能ブロックや機能ブロックを構成する部品を抽出し、検証項目の追加およびカバレッジファイルを作成することにより、短期間で高精度な検証確認が可能な論理検証装置を提供することができる。
【発明を実施するための最良の形態】
【００１２】
以下、図面を参照しながら本発明の実施形態を説明する。
【００１３】
図１は、本発明の一実施例を示す図である。RTL source code １１はVerilog あるいは VHDL で記述した論理システムの設計データである。テスト項目表１２は、検証項目の一覧である。この テスト項目表１２は、開発する論理システム全てに対して共通に使用するものであって、個々の論理システムごとに作成するものではない。テスト項目表１２から、動作記述のテンプレートをテンプレート生成手順２３で作成し、該当するテスト項目表１２の機能および生成されたテンプレートを機能・テンプレート・ライブラリ１３として保存する。内部表現変換器２１は、RTL source code １１と動作記述のテンプレートを本発明の内部で使用する内部表現に変換する。比較器・選択器２２は、内部表現で表した RTL source code と、動作記述のテンプレートを比較し、比較結果が条件を満たすならば、１４においてテスト項目表１２より該当するテスト項目を追加し、追加されたテスト項目１４が検証されたか判断するためのカバレッジファイル作成１５を行う。
【００１４】
比較・選択器２２で内部表現の比較をおこなうため、本発明で使用する内部表現は同一の論理関数が同一の表現にならなければならない。また、容量が大きくならず、比較の手順が容易である必要がある。同一の論理関数が同一の表現となる表現方法として、BDD (Binary Decision Diagram) 、真理値表、積和標準形がある。真理値表は入力数の指数乗の項数を必要とする。また、積和標準形も最悪の場合、真理値表と同じく入力数の指数乗の項数を必要とする。しかし、BDD では多くの場合、真理値表や積和標準形より少ない項数で論理関数を表現可能である。また、真理値表と積和標準形では、内部表現への変換工数が論理関数の複雑度に影響し、複雑になるにつれて内部表現への変換工数が増加する。一方、BDD では論理関数の複雑度に関係なく変換工数がきまる。そのこで、本実施例では、内部表現として BDD を用いることとする。勿論、内部表現をBDD に限定するのもではなく、同一の論理関数が同一の表現になるならばどのような表現を用いてよい。
【００１５】
内部表現変換器２１は、RTL source code １１あるいは動作記述のテンプレート１３をBDD に変換する手法として apply アルゴリズムを使用する。この apply アルゴリズムは 1984 に Randal E. Bryant 氏により開発された、BDD 生成アルゴリズムである。この apply アルゴリズムは、既に数多く使用されており、公知の技術である。
【００１６】
図２に、機能ブロック、その内部構成の一例を示す。
【００１７】
テスト項目表１２の一実施例を図３に示す。図３に示す実施例では、項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」と、項番 4.1.2 「初期値設定機能附きアップ・カウンタ」の項を抜き出している。
【００１８】
動作記述テンプレート５１の一実施例を図４に示す。図４に示す実施例は、テスト項目表１２の項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」の動作記述テンプレート５１の一実施例である。
【００１９】
テスト項目表１２の項番 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   a が成立するならば b が成り立つ
&&         論理積
||         論理和
~          論理否定
'          次クロック・サイクルの状態
//         コメント
動作記述中テンプレート５１中、テンプレート (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のいずれかになる。つまり、このテンプレートは異常な状態に陥らないことを定義している。
【００２７】
テンプレート生成手順３１でテスト項目表１２から動作記述テンプレート５１を生成する。この動作記述テンプレート５１はテスト項目表を更新した場合に、更新した項目に関してのみ作成すればよい。テストを実行するたび、あるいは論理システムごとに生成する必要はない。作業量は少ないため、人手で動作記述テンプレート５１を作成してもよいし、あるいは自動生成ツールで作成してもよい。
【００２８】
内部表現変換器２１は、RTL source code １１、あるいは機能・テンプレート・ライブラリ１３に登録した動作記述テンプレートをBDDに変換する。本実施例では、変換には公知の技術である apply アルゴリズムを使用する。
【００２９】
図５に、動作記述テンプレート５１を内部表現変換器２１で変換したBDDのうち、stage_Aに関係する部分を示す。このBDDは、次クロック・サイクルの stage_A を生成する論理関数を表している。すなわち、図４に示す動作記述テンプレート５１のうち、テンプレート (1)〜(3) を変換すると図５に示すBDDになる。
【００３０】
次に、比較・選択器２２の動作について説明する。比較・選択器２２は、RTL source code １１を内部表現変換器２１で変換した BDD と、動作記述テンプレートを内部表現変換器２１で変換した BDD の同形性を判定する。つまり、両 BDDが完全に一致するか、あるいは、RTL source code １１から変換した BDD が、動作記述テンプレートから変換した BDD を包含しているかを判定する。両 BDDが完全に一致するか、あるいは、RTL source code １１から変換した BDD が、動作記述テンプレートから変換した BDD を包含しているならば、動作記述テンプレートが定義している機能ブロックや部品が RTL source code １１中に存在する。すなわち、テスト項目表に挙げた項目を検証する必要があることを示している。
【００３１】
検証項目追加１４の動作は、比較・選択器２２により検出された機能ブロックの動作記述テンプレートより、該当する検証項目をテスト項目表１２から抽出し、検証項目として追加する。本実施例の場合、図３のテスト項目表の項番３．１．２が検証項目として抽出され、図９に示す検証項目リストの項番１００として追加される。
【００３２】
また、カバレッジファイル生成１５の動作は、比較・選択器２２により検出された機能ブロックが検証されたことを判断するための、図１０に示すカバレッジファイルとして出力する。本実施例のアービタの場合、検出された機能ブロックのBDDに関わる信号がありうる値をとったかどうかの判断が行３〜１８、状態間の遷移が生じたかの判断が行１９〜２２を示している。行３において、req_a信号が変化した場合にreq_a_chgイベントが発生したら、行５においてreq_aの値がreq_a_chgカバレッジアイテムとして登録される。以下同様である。たとえばこの実施例において、req_cは常に、状態がstate_Aのときに発行され、かつreq_bと同時に発行し、かつ状態がstate_Bに移行した場合は発行を中止するといった制約条件があった場合、アービタの機能が正常でも、state_Ｃの状態になり得ないという不具合が生ずる。この場合、図１０のカバレッジファイルの行１５〜１８のstate_machineがstate_Cの状態にならないこと、また行１９〜２２の状態遷移でstate_Cに遷移することがないことにより、上記不具合が確認される。
【００３３】
BDD の同形性判定アルゴリズムは、従来より多くの提案が存在する。本発明は、同形性判定アルゴリズムに依存した発明ではないので、どの手法を用いても構わない。例えば、ある節に注目し、'1' の枝の形と '0' の枝の形を再帰的に比較することで同形性を判定する手法を用いてもよい。
【００３４】
図６を用いて、本発明の動作を説明する。
【００３５】
Ｓ００１  RTL source code １１を内部表現変換器２１で BDD に変換
Ｓ００２  機能・テンプレート・ライブラリ１３から、１つの動作記述テンプレートを取り出す
Ｓ００３  Ｓ００１で取り出した動作記述テンプレートを内部表現変換器２１で
BDD に変換
Ｓ００４  比較器・選択器２２で、Ｓ００１で変換した BDD と、
Ｓ００３で変換した BDD を比較
Ｓ００５  両 BDD が一致したならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００６  Ｓ００３で変換した BDD がＳ００１で変換した BDD を包含している
ならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００７  Ｓ００２で選択した検証項目を出力
Ｓ００８  Ｓ００７の検証項目が検証されたことを判断するカバレッジファイルを出力
Ｓ００９  機能・テンプレート・ライブラリ１３内に未使用の動作記述テンプレートが
存在していないならば終了
未使用の動作記述テンプレートが存在しているならば、Ｓ００２に戻る。
【００３６】
機能・テンプレート・ライブラリ１３に登録した動作記述テンプレートの全てに対して比較をおこなうことで、RTL source code １１中にテスト項目表１２に挙げた項目に関わる機能ブロックや部品が存在するならば、対応する動作記述テンプレート１４を出力する。検証者は、この動作記述テンプレート１４を基に実際の動作記述を作成し、静的検証をおこなう。
【００３７】
図７に本発明に関わる別の実施例を示す。図７に示す実施例では、機能・テンプレート・ライブラリ１３ではなく、BDD ライブラリ１５を用いる。テスト項目表が更新された場合にのみ、動作記述テンプレートを更新する。よって、動作記述テンプレートの BDD は、毎回生成する必要は無く、動作記述テンプレートが更新された場合にのみ生成すれば、効率がよくなる。
【００３８】
動作記述テンプレートから生成した BDD をライブラリ化した、BDD ライブラリ１５を用いるため、本実施例では動作の手順が変わる。図７に示す実施例を用いた場合の動作手順を図８に示す。
【００３９】
Ｓ００１  RTL source code １１を内部表現変換器２１で BDD に変換
Ｓ０１１  BDD ライブラリ１５から、１つの動作記述テンプレートに対応した
BDD を取り出す
Ｓ００４  比較器・選択器２２で、Ｓ００１で変換した BDD と、
Ｓ０１１で取り出した BDD を比較
Ｓ００５  両 BDD が一致したならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００６  Ｓ０１１で取り出したBDD がＳ００１で変換した BDD を包含している
ならば、Ｓ００７で動作記述テンプレート１４を出力
Ｓ００７  Ｓ００２で選択した検証項目を出力
Ｓ００８  Ｓ００７の検証項目が検証されたことを判断するカバレッジファイルを出力
Ｓ０１２  BDDライブラリ１５内に未使用のBDDが存在していないならば終了
未使用のBDDが存在しているならば、Ｓ０１１に戻る。
【図面の簡単な説明】
【００４０】
【図１】本発明の一実施例を示す図である
【図２】機能ブロックと、その内部構成の一例を示す図である
【図３】テスト項目表の一実施例を示す図である
【図４】動作仕様記述テンプレートの一実施例を示す図である
【図５】動作仕様記述テンプレートから生成した BDD である
【図６】図１に示す本発明の一実施例の動作を示す図である
【図７】本発明の別の一実施例を示す図である
【図８】図７に示す本発明の一実施例の動作を示す図である
【図９】検証項目表の一実施例を示す図である
【図１０】カバレッジファイルの一実施例を示す図である
【符号の説明】
【００４１】
１１  RTL source code
１２  テスト項目表
１３  機能・テンプレート・ライブラリ
１４  検証項目の追加
１５  カバレッジファイルの生成
２１  内部表現変換器
２２  比較器・選択器
２３  動作仕様記述テンプレート生成
３１  機能ブロック
３２  カウンタ
３３  FSM
３４  ランダム論理
３５  シーケンサ
５１  動作仕様記述テンプレート
【図１】
2007026177.tif 000003
【図２】
2007026177.tif 000004
【図３】
2007026177.tif 000005
【図４】
2007026177.tif 000006
【図５】
2007026177.tif 000007
【図６】
2007026177.tif 000008
【図７】
2007026177.tif 000009
【図８】
2007026177.tif 000010
【図９】
2007026177.tif 000011
【図１０】
2007026177.tif 000012