(57)【要約】【課題】  仕様書に記述されている機能ブロックすべてが、ハードウェア記述言語で実装されているかどうかを確かめるための手段を得る。【解決手段】  識別子を用いて記述した論理回路の仕様書から自動抽出した論理検証項目と、ハードウェア記述言語により記述した論理システムおよび動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動抽出した論理検証項目を比較する装置。【選択図】  図１
2007026369.tif 000002
【特許請求の範囲】
【請求項１】
識別子を用いて記述した論理回路の仕様書から自動抽出した論理検証項目と、ハードウェア記述言語により記述した論理システムおよび動作仕様記述の等価性を判定し論理検証をおこなう論理検証装置が用いる動作仕様記述を生成する装置から自動抽出した論理検証項目を比較する装置であって、
識別子を用いて記述された論理回路の仕様書から論理検証項目を抽出する検証項目抽出手段と、
前記ハードウェア記述言語で記述された論理システムを論理表現に変換し最適化をおこない正規化論理表現を生成する正規化論理表現生成手段と、
論理システムの構成部品である機能ブロックに対応する動作仕様記述の正規化論理表現を記録する機能ブロック保持手段と、
前記機能ブロック保持手段から正規化論理表現を選択し前記正規化論理表現生成手段で生成した正規化論理表現と比較をおこない論理的等価性を判定する比較手段と、
前記比較手段で論理的に一致すると判定されたならば前記機能ブロック保持手段内の機能を検証項目として登録する手段と、
前記検証項目抽出手段と検証項目登録手段により出力された検証項目を比較する検証項目比較手段と、
前記検証項目比較手段において前記検証項目抽出手段により出力された検証項目が検証項目登録手段によって抽出された検証項目に含まれない場合、前記検証項目比較手段において一致しなかった検証項目に対するハードウェア記述言語の不足を示唆する表示手段を持つことを特徴とする、
仕様書から自動抽出した論理検証項目とハードウェア記述言語から自動抽出した論理検証項目比較し、前記ハードウェア記述言語の不足を示唆する論理検証補助装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は集積回路の論理検証装置および方法に関するものである。
【背景技術】
【０００２】
ＬＳＩを含む論理システムの規模は、年毎に増加している。それに伴い、論理システムの検証にかかる工数も増加している。一方、市場には消費者が欲するときに製品を投入しなければならず、ＬＳＩを始めとした論理システムの開発期間は短くなっている。そのため、論理システム検証の効率向上を図る必要が生じている。
【０００３】
そのような中、LSI開発を含むシステム開発においては仕様レベルの上流工程から下流工程までを自動的に行う手法が研究されており、システムLSIの検証における分野でも論理回路の仕様書から論理回路の論理検証項目を自動で作成する手法が考案されている。これは識別子（タグ）を用いて論理回路の仕様書と論理検証項目の一覧表（以下、検証項目リスト）とを記述し、該仕様書と該論理検証項目リストのタグを解析するプログラム（以下、パーサ）を用いて該論理回路の論理検証項目を作成するものである。このように仕様書から作成された検証項目に基づいて検証が行われている。
【０００４】
また、システムの大規模化に対応するためハードウェア記述言語を自動生成する設計支援ツールを用いた設計手法が開発されている。
【０００５】
又、従来例としては、例えば特許文献１をあげることが出来る。
【特許文献１】特開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 アルゴリズムは、既に数多く使用されており、公知の技術である。
【００１７】
仕様検証項目１４と機能検証項目１５が抽出されたならば、比較器２２を用いて仕様検証項目１４と機能検証項目１５に含まれる検証項目の違いを表示３１する。この時、仕様検証項目１４に含まれて機能検証項目１５の方に含まれない検証項目があったならば、機能ブロックに対応するRTLの不足の可能性が高いので、ユーザが確認し、設計したRTLのソースコードを修正する３２。
【００１８】
仕様書１０の一実施例を図２に示す。本発明で用いる仕様書はタグを用いて記述されている。例えば図２左において１行目から３０行目のタグ<Design Spec>〜</Design Spec>は、論理回路の仕様が記述されていることを示す。２行目はProjectA_Counterの仕様書であることを示す。３行目から２９行目のタグ<Register>〜</Register>は、レジスタに関する記述であることを示す。４行目のタグ<BaseAddress>〜</BaseAddress>はレジスタのベースアドレスが0x1000であることを示す。５行目から２８行目のタグ<Field>〜</Field>はレジスタのフィールド記述を示す。６行目から２７行目のタグ<Function>〜</Function>はレジスタがカウンター機能の設定であることを示す。７行目から１３行目のタグ<Item>〜</Item>はレジスタの項目がEnableであることを示す。８行目から１２行目の各タグは、Enable項目の各設定内容を示し、８行目のタグ<offset>〜/offset>は４行目のベースアドレス0x1000に対する相対アドレス0x1000を、９行目のタグ<default>〜</default>はビットフィールド[0:0]および初期値0を、１０行目から１１行目のタグ<bits>〜<bits>は0の時はDisableで1の時はEnableを、１２行目のタグ<Read_Write>〜</Read_Write>は読み書き可能であることを示す。Enableの項目と同様に、１４行目から２０行目はUp_Downの項目を、２１行目から２６行目はLoadの項目を示す。図２右側はアービターの仕様書の一例を示している。このように機能ブロックのすべてが仕様の中でタグを用いて記述されている。
【００１９】
検証項目表１２の一実施例を図３に示す。本発明で用いる検証項目表は仕様書と同様にタグを用いて記述されている。例えば図３の１行目から３１行目のタグ＜Test_Plan_Check_List＞〜＜/Test_Plan_Check_List＞は、論理検証項目のリストが記述されていることを示す。２行目からのタグ＜Function＞〜＜/Function＞はArbiterに関する検証項目表を示す。３行目からのタグ＜Item＞〜＜/Item＞は検証項目StateMachineに関することを示す。このように論理システムの検証において必要な項目全てがあらかじめタグを用いた表として定義されている。
【００２０】
仕様検証項目１４の一実施例を図４に示す。仕様検証項目１４は仕様書１０と検証項目表１２からパーサ２０によって自動生成されるものであり、図４に示す一実施例では、項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」と、項番 4.1.2 「初期値設定機能附きアップ・カウンタ」の項を抜き出している。パーサはまず仕様書１０と検証項目表１２を読み込み、そこに記述されている識別子から仕様検証項目１４を作成する。仕様書１０に書かれている＜Function＞タグの内容が検証項目表１２の＜Function＞タグの内容と一致することを検索したならば、＜Item＞の内容を仕様検証項目１４に書き出す。例えば図４の項番3.1.2は図２、図３の＜Funtion＞Arbiterから＜Item＞State_Machineが抽出されて生成されたものである。
【００２１】
動作記述テンプレートの一実施例を図５に示す。図５に示す実施例は、検証項目表の項番 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のいずれかになる。つまり、このテンプレートは異常な状態に陥らないことを定義している。
【００２９】
機能検証項目１５の一実施例を図６に示す。機能検証項目１５はRTLから抽出された検証項目である。図６に示す実施例では、項番 3.1.2 「リクエスト数 3、ラウンド・ロビン型アービタ」の項のみが抽出されているが、図４の仕様検証項目と比較した場合、仕様検証項目にある、項番 4.1.2 「初期値設定機能附きアップ・カウンタ」が抜けており、RTLソースコードにアップ・カウンタの実装がなされていないことがわかる。
【００３０】
図７を用いて、本発明の動作を説明する。
【００３１】
Ｓ００１  仕様書１０から仕様検証項目１４を抽出
Ｓ００２  RTL source code１１を内部表現変換器２１で BDD に変換
Ｓ００３  テンプレート・ライブラリ１３から、１つの動作記述テンプレートを取り出す
Ｓ００４  S００１で取り出した動作記述テンプレートを内部表現変換器２１でBDD に変換
Ｓ００５  比較器２２で、Ｓ００２で変換した BDD と、Ｓ００４で変換した BDD を比較する。
【００３２】
Ｓ００６  両 BDD が一致したならば、対応する機能ブロックの検証項目を機能検証項目１５に追加する。
【００３３】
Ｓ００７  出力Ｓ００４で変換した BDD がＳ００２で変換した BDD を包含しているならば、対応する機能ブロックの検証項目を機能検証項目１５に追加する。
【００３４】
Ｓ００８  このステップに進むことは、検証項目表１２に挙げた項目を RTL source code１１が含んでいることを示している。
Ｓ００９  Ｓ００１で作成した仕様検証項目１４とＳ００８で作成した機能検証項目１５を比較する
Ｓ０１０  仕様検証項目１４にあるのに機能検証項目１５にない場合はＳ０１１でＲＴＬの不足の確認３２を行い、逆に機能検証項目１５が多い場合は仕様の不備の可能性もあるので仕様書の確認を行う。
【００３５】
Ｓ０１１  Ｓ０１０の比較結果に応じてユーザが論理システムの設計の不足を見直す。
【図面の簡単な説明】
【００３６】
【図１】本発明における論理検証補助装置の構成を示す図である。
【図２】本発明における識別子付きの仕様書を示す図である。
【図３】本発明における識別子付きの検証項目表を示す図である。
【図４】本発明における自動で抽出された一般的な検証項目表を示す図である。
【図５】本発明における動作記述テンプレートを示す図である。
【図６】本発明におけるＲＴＬから抽出された検証項目を示す図である。
【図７】本発明における論理検証補助装置の動作を示す図である。
【符号の説明】
【００３７】
１０  仕様書
１１  RTL source code
１２  検証項目表
１３  機能・テンプレート・ライブラリ
１４  仕様検証項目
１５  機能検証項目
２１  内部表現変換器
２２  比較器
３０  テンプレート生成
３１  結果の表示
３２  RTLの実装抜け確認
【図１】
2007026369.tif 000003
【図２】
2007026369.tif 000004
【図３】
2007026369.tif 000005
【図４】
2007026369.tif 000006
【図５】
2007026369.tif 000007
【図６】
2007026369.tif 000008
【図７】
2007026369.tif 000009