JP3941336B2 - 論理回路検証装置 - Google Patents

Description

【０００１】
【発明の属する技術分野】
本発明は、ハードウェア記述言語を用いた論理回路設計の検証方法に関する。
【０００２】
【従来の技術】
ＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ Ｓｐｅｃｉｆｉｃ Ｉｎｔｅｇｒａｔｅｄ Ｃｉｒｃｕｉｔ）などＬＳＩの設計において回路の大規模化が進み、設計の効率化が重要視されてきている。このような状況において、論理回路の設計データを記述できるハードウェア記述言語（以下、ＨＤＬ記述と称す）を用いた論理回路の設計方法が一般的になってきている。ＨＤＬ記述はｖｅｒｉｌｏｇＨＤＬとＶＨＤＬが標準化により実際の設計現場で中心的に用いられている。図２にｖｅｒｉｌｏｇＨＤＬ記述の例を示す。図２（ｂ）は図２（ａ）の回路シンボルをハードウェア記述で表現したものであり、図２（ｂ）の左側の行番号と右側のコメントは、説明のために書き加えたものである。各行および複数行のＨＤＬ記述の意味は、コメントに示す内容を表すものであるが、モジュールの定義に始まって、回路のポートの宣言や信号の変化によって記述ブロックの実行を制御する順次処理文などで構成される。ＨＤＬ記述は可読性と記述性に優れ、設計のみならず検証においても効率の向上に寄与するものである。
【０００３】
一般に論理回路の検証の方法は、大きく分けて論理シミュレーションと形式的検証がある。論理シミュレーションは、検証の対象回路に適切な入力パターンを与えて動作をシミュレーションし、得られた出力パターンが元の論理回路から得られるべき出力パターンと一致するか否かを調べることにより正当性を検証する方法である。一方、形式的検証は回路を数学的に解析することで、その結果を検証するものであり、形式的検証は更に等価性検証とプロパティ検証に分けられる。等価性検証は２つの回路が論理的に等しいかどうかを検証し、プロパティ検証は設計した論理回路が設計仕様（プロパティ）を満たしているかどうかを検証するものである。プロパティとは、例えば、ある信号が「１」になるまでデータの信号が入力されない、とか、あるレジスタに値が書き込まれたらそのデータの使用前にデータが書換えられることはない、と言ったものである。
【０００４】
実際のプロパティ検証においては、ＨＤＬ記述から変換した回路データと検証しようとする回路の動作事象等を記述したプロパティとを用いて検証を実行し、検証結果に示されるプロパティに記述した信号の状態を見て回路の正当性を判断する。本発明はプロパティ検証に係わるものである。
【０００５】
【発明が解決しようとする課題】
一般に検証は設計者と異なる検証者によって実施され、検証者は設計の基となる仕様書から検証に必要な情報を得て検証を行うが、次のような問題がある。
【０００６】
１）検証者は検証する回路動作の事象や入力信号の制約条件をプロパティとして記述する必要があり、煩雑な作業を強いられる。また、検証者のプロパティ作成のスキル如何により検証品質にバラツキがでる恐れがある。
【０００７】
２）回路規模と複雑性の増大により仕様書も同様にボリュームが多くなり、検証に必要な情報の取得に多大の時間を必要とする。また、見過ごし等による検証漏れも増大する。
【０００８】
３）仕様書が概念レベルの仕様まで規定し、詳細仕様を設計者に依存した仕様となっている場合に検証に必要な情報の取得が困難となる。
【０００９】
特に３）は、検証者が設計者に問い合わせて詳細仕様を確認する作業が必要となり、検証工数の増大をもたらす。
【００１０】
このように、複雑性が増し大規模の論理回路の検証においては、検証の効率と品質が問題となっている。
【００１１】
【課題を解決するための手段】
上記の問題を解決するため、本発明は予め設計者によってＨＤＬ記述中にチェッカーのような形で検証情報を挿入して置くことにより、装置がこれらの情報を抽出してプロパティ検証の環境を生成するもので、検証者は検証情報を指示するだけでプロパティ検証が行えるよう考案したものある。検証の効率と品質とを向上する論理回路検証装置を提供することを目的にしている。
【００１２】
この目的を達成するために、本発明は、図１に示すような構成手段を持つ。
【００１３】
まず検証対象のＨＤＬ記述３１は、設計者が予め検証すべきと考えている回路動作の事象に対応した検証情報をＨＤＬ記述中に挿入してあるものである。検証情報抽出手段１は、このＨＤＬ記述３１のモジュールの中に含まれている検証情報を抽出し、併せてこの検証情報の位置を定めるモジュール名、挿入行などの関連情報を記憶して置く。続いて、検証情報作成手段２では、抽出した各々の検証情報に対応する検証用の信号を設定し、その信号にユニークな信号名を付与して検証情報データベース２１として記憶して置く。検証用の信号は、検証の際に論理回路の動作事象を信号の変化として見るためのものであり、元の論理回路の持つ機能に影響を与えるものではない。次のＨＤＬ記述変換手段３では、検証情報が含まれているモジュールのＨＤＬ記述に対して、検証情報作成手段２で付与した信号の宣言文や信号値の初期化の命令文などを挿入し、挿入後のＨＤＬ記述を検証実行手段５が読める形に変換を行い回路データベース２２として記憶しておく。一方、プロパティ作成手段４では検証情報データベース２１の中の検証情報の一部または全部を用いて検証指示のためのプロパティを作成する。次に、このプロパティと回路データベース２２とを用いて検証実行手段５で検証の実行を行い、指示された信号の変化の状態を見て論理回路が仕様通りの動作が行われているかどうかを判断する。
【００１４】
上記の構成により、第一と第三の発明では、装置はＨＤＬ記述に含まれる検証情報に基づいてプロパティ検証のための動作記述をＨＤＬ記述中に生成するため、検証者がプロパティ作成のための記述を作成することなく容易に論理回路の動作事象の検証を実施できる。従って、検証者が設計仕様から検証用の情報を取得しプロパティ作成のために記述する時間の大幅な短縮が図れるとともに、検証者のスキルに依存することなく品質の高い検証を行うことができる。
【００１５】
また、第二の発明によれば、回路の入力信号の制約条件に対する検証を行うことができる。当然のことながら、回路の動作事象の検証と入力信号の制約条件を同時に検証することも可能である。
【００１６】
【発明の実施の形態】
本発明の実施例として、構成例および動作を図３から図１０を用いて順次説明する。
【００１７】
図３は本発明の実施構成例を示すブロック図である。
【００１８】
ＨＤＬ記述３１は検証対象のＨＤＬ記述であり、１つ以上のモジュールより構成されている。また、これらのＨＤＬ記述には設計者が検証すべきと考えている論理回路の動作事象や入力信号の制約条件が検証情報という形で挿入されている。
【００１９】
検証情報抽出部１１ではＨＤＬ記述３１を読取り、ＨＤＬ記述中に含まれている検証情報を抽出し、さらに検証情報の挿入位置を定めるモジュール名やモジュール内の行位置などの関連情報を抽出テーブル２３に記憶しておく。この処理を全てのモジュールに対して実施する。
【００２０】
次に、信号付与部１２で抽出テーブル２３に記憶してある検証情報に対応する検証用の信号を設定し、この信号にユニークな信号名を付け、検証情報データベース２１に格納して置く。
【００２１】
続いて、ＨＤＬ記述挿入部１３で検証情報データベース２１に記憶されているＨＤＬ記述のモジュールに対して、検証用信号の宣言文やその信号に対する初期化命令文の挿入、更に異常な動作をした場合の検証用信号の信号代入文を検証情報の記述行に対して置き換えを行う。このように挿入したＨＤＬ記述３２を変換部１４において検証実行部が読める形式に変換し、回路データベース２２を作成する。
【００２２】
一方、検証項目選択部１５において、検証者が検証情報データベース２１の中から実際に検証を実施する検証情報を選択し、次のプロパティ作成部１６において選択された検証情報に対して検証実行部１７への指示情報とするプロパティ３３の作成を行う。
【００２３】
以上で得られた回路データベース２２とプロパティ３３とを入力データとして、検証実行部１７においてプロパティ検証を行う。検証者は、この検証結果を見て設計した回路が正しく動作しているかどうかを判断する。
【００２４】
次に、図４を用いて処理の流れを示しながら、より詳細に発明の実施例を説明する。
【００２５】
まず装置は、ＨＤＬ記述３１の１モジュールを取り出し、そのモジュールの中に検証情報が含まれているか調べる。最初の１モジュールの例として図５を用いる。図５の８行目の＄ｆｉｎｉｓｈと１８行目の＄ｓｔｏｐとが検証情報として挿入されたものである。本来ｖｅｒｉｌｏｇＨＤＬにおける＄ｆｉｎｉｓｈは、シミュレーションの実行を終了する組み込みタスクであり、また＄ｓｔｏｐはシミュレーションの実行を停止しデバッグモードに入ることを表す組み込みタスクであるが、本装置ではこの２つの組み込みタスクが検証情報であると認識するようにしている。本例では、＄ｆｉｎｉｓｈを制約条件とし、＄ｓｔｏｐを回路の動作事象を検証するものとして使い分けている。即ち、ここでの＄ｆｉｎｉｓｈは、７行目の記述文によってｉ０は「１」以外の値をとってはならない、という制約条件をチェックするものである。更に＄ｓｔｏｐは、１３〜１７行目において記述されているｉ０とｉ１が「０、０」もしくは「１、１」の場合にｏ１が「０」となり、ｉ０とｉ１が「０、１」もしくは「１、０」の場合にｏ１が「１」となること以外の場合の動作事象をチェックすることを示すものである。この検証情報と検証情報が存在するファイル名やモジュール名、モジュール内の検証情報の行位置など検証情報に関連する情報も併せて図７に示すデータ構造で抽出テーブル２３に記憶させて置く。図７のインスタンスパスは、下位モジュールにインスタンスが在る場合のパスを記憶して置くが、本例では自身のモジュールで閉じているため空白としている。引数は検証情報に引数が在る場合に記憶できるようにしている。また、「変換後の信号名」は検証情報毎に付与された信号の名称であり、次のステップで信号名の付与を行うので、この時点では「変換後の信号名」欄は空白である。抽出テーブル２３は１つの検証情報に対して１つのテーブルを作成する。従って１つのモジュールに複数の検証情報が挿入されていれば、複数のテーブル作成されることになる。検証情報の抽出から抽出テーブル２３の作成までは全てのモジュールに対して実施する（Ｌ１、Ｓ１、Ｓ２）。
【００２６】
次に、抽出テーブル２３の各検証情報に対して検証用の信号を設定し、この信号に対してユニークな信号名を付与する。図７の抽出テーブル２３の検証情報＄ｆｉｎｉｓｈに対してはＡＳＳＥＲＴ＿ＳＩＧＮＡＬ０と言う信号名を付与し、＄ｓｔｏｐに対してはＡＳＳＥＲＴ＿ＳＩＧＮＡＬ１と言う信号名を付与している。付与した信号名は抽出テーブル２３の「変換後の信号名」欄に記憶しておく。抽出テーブル２３の全ての検証情報に対して信号名の付与が終わった段階で抽出テーブル２３を検証情報データベース２１に格納して置く。検証情報データベース２１には抽出テーブル２３のデータに加えて、「検証実行の選択」欄を設けており、図８にそのデータ構造例を示す。図８の「検証実行の選択」欄のチェックマークは、Ｓ７のステップで記入されるものでありこの時点では空白である（Ｌ２、Ｓ３、Ｓ４）。
【００２７】
続いて、検証情報データベース２１に記憶してある全てのモジュールのＨＤＬ記述に対して、それぞれの検証情報に与えられた信号を宣言文として挿入し、更にこの信号の初期値として「０」を与える初期化の命令文を挿入する。また、検証情報の記述行に対しては検証用の信号が期待とは異なった振る舞いをした時、即ち異常値となった時の信号値として、初期値とは異なる数値を与える信号代入文に置き換える。本例では、初期値として「０」を与えたので、異常値として「１」を与える。以上の動作を実際の例で説明する。まず、検証情報データベース２１にｔｅｓｔと言うモジュールが存在するので、このモジュール、即ち図５のモジュールを取り出す。続いて、検証情報データベース２１にはｔｅｓｔモジュールには＄ｆｉｎｉｓｈと＄ｓｔｏｐの２個の検証情報があり、それぞれにＡＳＳＥＲＴ＿ＳＩＧＮＡＬ０とＡＳＳＥＲＴ＿ＳＩＧＮＡＬ１の信号が付与されているので、この２つの信号の宣言を図５のＨＤＬ記述に対して図６のＨＤＬ記述の４行目のように挿入する。次に、これら２つの信号に対して初期値として０を与える命令文として図６の２１〜２４行目のように挿入する。最後に、検証情報が記述されている８行目と１８行目に異常値として１を示すように信号代入文を置きかえる。ｔｅｓｔというモジュールに対しては、これでＨＤＬ記述の挿入を終了したことになる。抽出テーブル２３に示される全てのモジュールに対して同様の処理実行し、挿入後のＨＤＬ記述３２を得る（Ｌ３、Ｓ５）。
【００２８】
次に、挿入後のＨＤＬ記述３２を用いて検証が行える形式に変換し、回路データベース２２として格納しておく。回路データベース２２のデータ構造例を図９に示す（Ｓ６）。
【００２９】
続いて、検証情報の選択を行う。これは、設計者が挿入した多くの検証情報の中から、検証者が検証したい項目を選択できるようにしているものである。具体的には、ＨＤＬ記述３１と検証情報データベース２１とを画面に表示させ、選択した検証情報に対して検証情報データベース２１の「検証実行の選択」欄にチェックマークを付ける。図８の「検証実行の選択」欄は検証者が選択したことを示している（Ｓ７）。
【００３０】
検証情報の選択が終わった段階で、装置は検証情報データベース２１のチェックマークの有無を調べ、チェックマークのある検証情報について検証実行指示としての情報をプロパティ３３として出力する。プロパティ３３のデータ例を図１０に示す。ここでは、制約条件を検証する信号ＡＳＳＥＲＴ＿ＳＩＧＮＡＬ０と回路の動作事象を検証する信号ＡＳＳＥＲＴ＿ＳＩＧＮＡＬ１とについて検証することを示している（Ｓ８）。
【００３１】
次に、回路データベース２２とプロパティ３３とを用いてプロパティ検証の実行を行う。検証者は指定した検証情報の信号の変化に注目して検証結果を調べ、回路動作の良否判断を行う（Ｓ９）。
【００３２】
本実施例では、ｖｅｒｉｌｏｇＨＤＬについて説明したが、ＶＨＤＬについても同様の考えで検証を行うことができる。図１１は前述した図５のｖｅｒｉｌｏｇＨＤＬと同じ回路をＶＨＤＬで記述したものである。ＶＨＤＬではアサート文を検証情報として用いている。例えば図１１の１２行目と２２行目が検証情報であり、図１２のように変換される。検証の抽出およびＨＤＬ記述の挿入後の処理はｖｅｉｌｏｇＨＤＬと同様であるので、詳細は省略する。
【００３３】
このように検証情報は通常使用されているＨＤＬ記述文を用いているため、元のＨＤＬ記述を用いて論理シミュレーションを行うことができる。即ち、図５の記述で論理シミュレーションを実行すれば、組み込みタスクとして本来の機能で動作する。
【００３４】
【発明の効果】
以上説明したように、本発明によれば検証者はＨＤＬ記述に挿入してある回路の動作事象や制約条件の検証情報を指定するだけでプロパティ検証が行える。このため、検証者はプロパティ作成の記述に必要な知識や種々の記述規約を知ることなしに検証を行うことができる。また、設計仕様書からの検証に必要な情報を取り出す作業は大幅に軽減でき、検証の効率化、品質の向上に寄与するものである。更に、検証情報の記述は通常用いられている記述文を流用しているため、そのままで論理シミュレーションへの適用が可能である。
【図面の簡単な説明】
【図１】本発明の原理図である。
【図２】ｖｅｒｉｌｏｇＨＤＬ記述による表現例
【図３】実施構成例である。
【図４】処理フローである。
【図５】ｖｅｒｉｌｏｇＨＤＬ記述例である。
【図６】検証用信号挿入後のｖｅｒｉｌｏｇＨＤＬ記述例である。
【図７】抽出テーブルのデータ構造例である。
【図８】検証情報データベースのデータ構造例である。
【図９】回路データベースのデータ構造例である。
【図１０】プロパティのデータ例である。
【図１１】ＶＨＤＬ記述例である。
【図１２】検証用信号挿入後のＶＨＤＬ記述例である。
【符号の説明】
１：検証情報抽出手段
２：検証情報作成手段
３：ＨＤＬ記述変換手段
４：プロパティ作成手段
５：検証実行手段
１１：検証情報抽出部
１２：信号付与部
１３：ＨＤＬ記述挿入部
１４：変換部
１５：検証項目選択部
１６：プロパティ作成部
１７：検証実行部
２１：検証情報データベース
２２：回路データベース
２３：抽出テーブル
３１：ＨＤＬ記述
３２：挿入後のＨＤＬ記述
３３：プロパティ

Claims (3)

1. 論理回路動作の検証情報が含まれているハードウェア記述から検証情報を抽出する検証情報抽出手段と、
   抽出した検証情報に対応する検証用の信号を設定し、信号名を付与して検証情報データベースを作成する検証情報作成手段と、
   検証情報データベースを用いてハードウェア記述に検証用の信号情報を挿入し、検証用信号挿入後のハードウェア記述を回路データベースに変換するハードウェア記述変換手段と、
   検証情報データベースに含まれる検証情報の一部または全部を用いてプロパティを作成するプロパティ作成手段と、
   プロパティと回路データベースとを用いて検証を実施する検証実行手段と、
   を備えていることを特徴とする論理回路検証装置。
2. 請求項１記載の検証情報抽出手段は、入力信号の制約条件に対応した検証情報が含まれるハードウェア記述から検証情報を抽出する手段であること、
   を特徴とする論理回路検証装置。
3. 論理回路動作の検証情報が含まれているハードウェア記述から検証情報を抽出する検証情報抽出モジュールと、
   抽出した検証情報に対して検証用の信号を設定し、検証用の信号にユニークな信号名を付与して検証情報データベースを作成する検証情報作成モジュールと、
   検証情報データベースを用いてハードウェア記述に検証用の信号情報を挿入し、検証用信号挿入後のハードウェア記述を回路データベースに変換するハードウェア記述変換モジュールと、
   検証情報データベースに含まれる検証情報の一部または全部を用いてプロパティを作成するプロパティ作成モジュールと、
   プロパティと回路データベースとを用いて検証を実施する検証実行モジュールと、
   を含むことを特徴とした論理回路を検証するプログラムを格納したコンピュータ読み取り可能な記録媒体。

Images