JP2000305977A - 論理データの検証方法、該論理検証方法を実行する論理検証システム及び前記論理検証方法を実行するプログラムを記憶した記録媒体 - Google Patents

Abstract

(57)【要約】 【課題】 チェック項目情報の作成精度の向上及び論理
変更の際に論理データがデグレードしていないことを容
易に確認すること。 【解決手段】 ハードウェア記述言語にて作成した半導
体集積回路の論理データ１０とテストパターンデータ１
１より論理シミュレーションにて波形データ１３を作成
し、この波形データ１３とユーザ指定部１５にて与えた
情報より、チェック項目情報１８を生成する。また、前
回生成したチェック項目情報１４を入力する手段を設
け、前記波形データ１３と前記ユーザ指定部１５にて与
えた情報より生成したチェック項目情報のうち、前回生
成したチェック項目情報１４に含まれない部分を前回生
成したチェック項目情報１８に追加し出力するもの。

Description

【発明の詳細な説明】

【０００１】

【発明の属する技術分野】本発明は、ハードウェア記述
言語にて作成した半導体集積回路の論理データの検証を
モデルチェッキングを利用して行う論理データの検証方
法、この論理検証方法を実行する論理検証システム及び
前記論理検証方法を実行するプログラムを記憶した記録
媒体に論理検証システムに関する。

【０００２】

【従来の技術】一般に半導体集積回路は、ハードウェア
記述言語にて回路の論理データを作成し、この論理デー
タをユーザが与えた論理仕様に関する命題を論理データ
が満足しているか否かを数学的に証明し検証する、モデ
ルチェッキング（Model Checking）を利用して検証する
形式的論理検証（Formal Verification）と、テストパ
ターンデータを入力し、それに伴う被検証論理の動作が
期待通りであるかの判定を行う論理シミュレーションと
を用いた検証が行われている。

【０００３】前記論理シミュレーションは、設計データ
をテストするための入力パターンを記載したテストパタ
ーンデータを入力し、それに伴う被検証論理の動作が期
待通りであるかの判定を行うものである。この論理シミ
ュレーションは、指定した入力パターンについては検証
可能であるものの、検証しようとする機能のすべてを確
認するためのテストパターンを作成し検証するには、多
大な工数を必要とする。

【０００４】これに対して前記モデルチェッキングを利
用し検証する形式的論理検証では、論理データの全ての
可能な入力パターンについて、ユーザが与えた論理仕様
に関する命題を被検証論理が満足しているかを数学的に
証明し、正当性を保証することができるため、論理シミ
ュレーションに比べ小さな工数で検証の完全化を実現す
ることができる。このモデルチェッキングを利用した形
式的論理検証方法としては、例えば特開平９−３２５９
７５号公報に開示されているような方法が知られてい
る。この検証方法は、図２に示す如く、検証の対象とな
る論理データ１０及び該論理データ１０の基礎となる論
理仕様書２０とを用い、ユーザが、モデルチェッキング
にて検証したい部分を抜粋してモデルチェッキングで入
力可能な形式のチェック項目情報１８に変換し、前記論
理データ１０と前記チェック項目情報１８より、モデル
チェッキング手段１９にてモデルチェッキングを行い
し、結果をモデルチェッキング結果１Ａに出力するもの
である。

【０００５】このようにモデルチェッキングによる検証
は、上記のような論理シミュレーションによる論理検証
に対する利点があるものの、一般的には両者による検証
を併用している。この理由は、ある特定の入力パター
ンにおける論理動作、いわゆるコーナーケースにおける
論理動作を検証する場合、論理シミュレーション用テス
トパターンデータによって上記入力パターンを定義し
て、その動作を確認する方が、モデルチェッキングを用
いる場合よりも検証が容易なため、モデルチェッキン
グでは被検証論理の動作を時刻を追って表示することが
困難であり、被検証論理の動作に不具合がありその原因
を解析したりする場合には、論理シミュレーションを用
いる方が便利なためである。

【０００６】従って、半導体集積回路は、前記モデルチ
ェッキングを利用した形式的論理検証及びテストパター
ンデータを利用した論理シミュレーションの長所・短所
を見極めたうえで併用することにより、効率良く且つ高
精度の論理検証が行われている。

【０００７】さて、現実の半導体集積回路の設計の過程
においては、論理の不具合の修正や仕様の変更が起こる
ために、被検証対象である回路の論理構成が頻繁に変更
される。この論理を変更した場合、変更した部分が期待
通り動作するか確認することは勿論であるが、この変更
に依存しない、これまで正常に動作していた機能が正し
く動作するか、つまりデグレードを起こしていないかを
確認することが重要である。これは、設計者が意図して
いないにも拘わらず論理変更内容が既存論理動作を壊し
ている恐れがあるためである。

【０００８】このため、一般的には、論理変更がなされ
た際、論理変更に依存しない過去に期待通り論理が動作
していることを確認した論理シミュレーション用テスト
パターンデータの全て、あるいはその一部を選び、変更
後の論理に対してそれらを用いて再度論理シミュレーシ
ョンを実施し、過去に実施した論理シミュレーション結
果と比較し確認を行い、少なくとも被検証論理が変更さ
れるまでに確認された機能についてデグレードしていな
いことを保証することが必要である。

【０００９】このデグレードについて図３を参照して説
明する。図３（ａ）は、論理変更前の論理データによる
論理構成の一例を示し、図３（ｂ）は論理変更後の論理
データによる論理構成の一例を示し、ここでは図３
（ａ）に示した入力側のＡＮＤ回路３４及び３２と、該
回路の出力側に各々接続されるフリップフロップ３３及
びＡＮＤ回路３０とから成る論理構成の内、図３（ｂ）
の如く前記ＡＮＤ回路３０をＯＲ回路３１に変更したも
のとする。

【００１０】この変更を行った場合、ＯＲ回路３１に変
更を行った回路部分３３については、当該変更した部分
が期待通り動作するかの確認を行うと共に、この変更に
依存しないはずの回路部分３２がデグレードを起こして
いないことの確認も行う必要がある。

【００１１】この変更に依存しない回路部分３２がデグ
レードを起こしていないかを確認する手法は、論理変更
に依存しない過去に期待通り論理が動作していることを
確認済みの論理シミュレーション用テストパターンデー
タ、具体的には各入力端子'INPUT0'、'INPUT1'、'CLK'
各々に対して入力パターンを与えるためのテストパター
ンデータを選び、そのテストパターンデータの全て、あ
るいはその一部を用いて再度論理シミュレーションを実
施し、過去に実施した論理シミュレーション結果と比較
し確認することにより行われている。

【００１２】

【発明が解決しようとする課題】従来のモデルチェッキ
ングを利用し検証する形式的論理検証方法は、上記の検
証を行う上で核となるチェック項目情報１８を作成する
際は、論理仕様書２０から必要検証部分の抜粋と、この
抜粋した部分をモデルチェッキングにより入力可能な形
式への変換を人手で行う必要があり、このため、モデル
チェッキングで入力可能な形式への変換ミスや論理仕様
の誤解によるチェック項目情報を作成する際のミスを招
く可能性があると言う不具合があった。

【００１３】また、従来の検証方法は、全く独立した論
理シミュレーションとモデルチェッキングを併用してい
るため、双方で論理データのどの機能に対し検証したか
対応がつかず、このため、論理変更時に論理データがデ
グレードしていないことを確認する場合には、論理変更
に依存しないテストパターンの再確認論理シミュレーシ
ョンと、論理変更に依存しないチェック項目情報を抽出
したモデルチェッキングの両方を実施する必要があり、
論理シミュレーションとモデルチェッキングで検証する
項目が重複し、本来は論理シミュレーションとモデルチ
ェッキングのどちらか一方で検証すれば十分なものに対
して両者で検証を行い、無駄な検証工数が発生すると言
う不具合もあった。

【００１４】更に従来の検証方法は、論理変更時にデグ
レードが発生していないことを確認するため、上記のよ
うに論理変更の都度、一旦検証済みのテストパターンに
ついて論理シミュレーションを行う必要があったため
に、検証が進むにつれ再確認すべきテストパターン量が
増大し、多大な工数と計算機資源が必要になると言う不
具合もあった。

【００１５】本発明の目的は、前記従来技術による不具
合を除去することであり、チェック項目情報への変換ミ
スの低減、チェック項目情報作成ミスの低減、論理シミ
ュレーション及びモデルチェッキングの両者を併用した
効率のよい論理検証により無駄な検証工数の低減、デグ
レード検証時の論理シミュレーション数を削減して検証
工数と計算機資源の低減を行うことができる論理データ
の検証方法、該論理検証方法を実行するプログラムを記
憶した記録媒体、及び前記論理検証方法を実行する論理
検証システムを提供することである。

【００１６】

【課題を解決するための手段】前記目的を達成するため
本発明による論理データの検証方法は、前記論理データ
と該論理データをテストするための論理シミュレーショ
ンのテストパターンとを定義したテストパターンデータ
よりタイムチャート形式の波形データを作成し、前記波
形データを元に入力されたモデルチェッキングの対象と
なる信号名及びその信号の確定条件並びに前記波形デー
タとよりモデルチェッキングで入力可能な形式のチェッ
ク項目情報を生成し、前記論理データが変更されたと
き、論理データ変更対象外の部分について前記チェック
項目情報を用いモデルチェッキングを実行することを特
徴とし、更に該特徴の検証方法において、前回生成した
チェック項目情報を入力し、前記波形データと前記入力
した信号名および確定条件より生成したチェック項目情
報のうち、前回生成したチェック項目情報に含まれない
部分のみを前回生成したチェック項目情報に追加するこ
とを特徴とする。

【００１７】また本発明による検証する論理検証システ
ムは、前記論理データと該論理データをテストするため
の論理シミュレーションのテストパターンを定義したテ
ストパターンデータとによりタイムチャート形式の波形
データを作成する論理シミュレーション手段と、前記波
形データを元にモデルチェッキングの対象となる信号名
及びその信号の確定条件を入力する入力手段と、前記波
形データと前記入力手段によって入力された信号名と確
定条件とによりモデルチェッキングで入力可能な形式の
チェック項目情報を生成するチェック項目生成手段と、
前記チェック項目情報を入力し、論理データのモデルチ
ェッキングを行う手段とを備え、前記論理データが変更
されたとき、論理データ変更対象外の部分について前記
チェック項目情報を用いモデルチェッキングを実行する
ことを特徴とし、更に該特徴の論理検証システムにおい
て、前記チェック項目生成手段に前回生成したチェック
項目情報を入力する手段を設け、前記波形データと前記
入力手段にて指定した信号名および確定条件より生成し
たチェック項目情報のうち、前回生成したチェック項目
情報に含まれない部分のみを前回生成したチェック項目
情報に追加し出力するチェック項目生成手段を備えたこ
とを特徴とする。

【００１８】また本発明による論理データの検証方法の
プログラムを格納する記録媒体は、前記プログラムが、
前記論理データと該論理データをテストするための論理
シミュレーションのテストパターンとを定義したテスト
パターンデータよりタイムチャート形式の波形データを
作成し、前記波形データを元に入力されたモデルチェッ
キングの対象となる信号名及びその信号の確定条件並び
に前記波形データとよりモデルチェッキングで入力可能
な形式のチェック項目情報を生成し、前記論理データが
変更されたとき、論理データ変更対象外の部分について
前記チェック項目情報を用いモデルチェッキングを実行
するプログラムであることを特徴とする。

【００１９】

【発明の実施の形態】以下、本発明による論理データの
検証方法、該論理検証方法を実行するプログラムを記憶
した記録媒体、及び前記理検証方法を実行する論理検証
システムの一実施形態を図面を参照して詳細に説明す
る。

【００２０】図１は本発明による理検証方法を実行する
論理検証システムの全体概略構成を説明するための図で
ある。本実施形態による論理検証システムは、論理変更
前のＶＨＤＬやＶｅｒｉｌｏｇ−ＨＤＬ等のハードウェ
ア記述言語によって記述された論理データ１０と該論理
データ１０を論理シミュレーションによって検証するた
めにハードウェア記述言語にて記述されたテストパター
ンデータ１１とを入力して論理シミュレーションを行
い、前記テストパターンデータ１１により記述されたテ
ストパターンに対する論理データ１０の動作が各信号ご
とに時刻を追って記述された波形データ１３を出力する
論理シミュレーション手段１２と、前記論理データ１０
に論理変更がなされる前の段階において作成され、無い
場合には新たに作成されるたチェック項目情報１４と前
記波形データ１３を基にユーザが指定するモデルチェッ
キングの対象となる信号名およびその信号の確定条件を
入力するためのユーザ指定部１５と、前記波形データ１
３及びユーザ指定部１５にて指定した信号名およびその
信号の確定条件よりモデルチェッキングで入力可能な形
式のチェック項目情報１８を生成するモデルチェッキン
グ用チェック項目生成手段１６と、前記論理データ１０
に対して変更が入った被検証論理となる論理データ１７
と、該論理変更後の論理データ１７と前記チェック項目
情報１８より、論理データのモデルチェッキングを行
い、チェッキング結果１Ａを出力するモデルチェッキン
グ手段１９とを備え、前記論理データが変更されたと
き、論理データ変更対象外の部分について前記チェック
項目情報を用いモデルチェッキングを実行するものであ
る。

【００２１】前記モデルチェッキング用チェック項目生
成手段１６は、チェック項目生成手段１６の入力に前回
生成したチェック項目情報１４を加えることにより、前
記波形データ１３と前記ユーザ指定部１５にて指定した
信号名および確定条件より生成したチェック項目情報の
うち、前回生成したチェック項目情報に含まれない部分
のみを前回生成したチェック項目情報１４に追加しチェ
ック項目情報１８を出力する。

【００２２】次に、チェック項目生成手段１６の処理方
法を図面を参照して説明する。図４は、チェック項目生
成手段１６の概略の流れ図を示す図であり、図５は、チ
ェック項目生成手段１６に関連するデータを示す図であ
る。

【００２３】このチェック項目生成手段１６は、前記論
理シミュレーション手段１２から出力されるタイムチャ
ート形式の波形データ１３を読み込み（ステップ４
０）、この波形データを基にユーザが指定するモデルチ
ェッキングの対象となる信号名およびその信号の確定条
件の入力手段となるＧＵＩ（Graphical User Interfac
e）としてユーザ指定部１５に提供する（ステップ４
１）。

【００２４】このユーザ指定部１５に提供したデータ
は、図５の符号１５として示した如く、波形データ１３
の内容を表示した画面と、ユーザが確定条件を指定する
ことをユーザ指定部１５に通知する確定条件ボタンＣ
０、確定条件入力の際に‘ＡＮＤ［論理積］’や‘ＯＲ
［論理和］’、‘（［かっこ］’、‘）［同左］’を指
定するためのボタン、Ｃ２、Ｃ７、Ｃ１０，Ｃ１１、確
定値となる信号を指定するための確定値ボタンＣ４とし
て表示される。

【００２５】この表示を見たユーザにより、確定条件と
なる信号名と条件、及び確定値となる信号名等をユーザ
指定部１５の画面上にてマウスのクリック等により指定
（ステップ４２）される。図５の例では、ＣＬＫの立ち
上がりにて信号Ａと信号ＢがＨｉｇｈのとき［確定条
件］、常に１サイクル後に信号ＣがＨｉｇｈになる［確
定値］という仕様と、ＣＬＫの立ち上がりにて信号Ａま
たは信号ＢがＬｏｗのとき［確定条件］、常に１サイク
ル後に信号ＣがＬｏｗになる［確定値］という仕様が与
えられているものとする。ユーザ指定部１５上にはこれ
らの仕様がともに満たされている状態の波形が表示され
ている（波形データ表示１３内の５１と５２）。

【００２６】これらの論理仕様をユーザ指定部１５によ
る指定は、例えば信号ＣがＨｉｇｈになる論理仕様（図
５中の符号５１）を指定するときは、確定条件ボタンＣ
０をクリックし、確定条件となる信号Ａの位置Ｃ１をク
リックし、ＡＮＤボタンＣ２をクリックし、確定条件と
なる信号Ｂの位置Ｃ３をクリックし、確定値ボタンＣ４
をクリックし、確定値となる信号Ｃの位置Ｃ５をクリッ
クする。同様に、信号ＣがＬｏｗになる論理仕様（図５
中の符号５２）を指定するときは、確定条件ボタンＣ０
をクリックし、確定条件となる信号Ａの位置Ｃ６をクリ
ックし、ＯＲボタンＣ７をクリックし、確定条件となる
信号Ｂの位置Ｃ８をクリックし、確定値ボタンＣ４をク
リックし、確定値となる信号Ｃの位置Ｃ９をクリックす
ることにより行われる。

【００２７】次にチェック項目生成手段１６は、前記ス
テップ４２によりユーザが指定した情報を基にユーザ指
定によるチェック項目情報５３を生成する（ステップ４
３）。このチェック項目情報５３は、図５中の符号５３
に示す如く、二つの項目５４及び５５が定義され、各項
目は確定条件を定義する部分と確定値を定義する部分に
分かれている。即ち、前記項目５４は、"always"が「後
続の'（'、'）'で囲まれた式が成り立つ場合常に」の意
味を持つ確定条件５４１と、"implies"が「上記確定条
件が成り立つならば、後続の'（'、'）'で囲まれた式が
成り立つ」ということを示している確定値５４４とから
成り、この例は「信号Ａが論理値１となり、かつ、信号
Ｂが論理値１となる場合［always ((A = '1') && (B =
'1'))］、常にその１サイクル後に信号Ｃの論理値が１
になる［implies (C = '1' at t+ 1)］」という意味（"
at t + 1"は確定条件が成立してから１サイクル後を表
す）である。項目５５も同様であり、この例は「信号Ａ
が論理値０となる、又は信号Ｂが論理値０となる場合
［always ((A = '0') ‖ (B = '0'))］、常にその１サ
イクル後に信号Ｃの論理値が０になる［implies (C = '
0' at t + 1)］」という意味である。

【００２８】これら前記ユーザ指定によるチェック項目
情報５３、前回生成したチェック項目情報１４、チェッ
ク項目情報１８ともに同じ仕様の言語によって、記述さ
れている。例えばチェック項目情報５３の生成を具体的
に説明すると、図５中の波形データ１３中の信号ＣがＨ
ｉｇｈになる論理仕様（符号５１）に対し、確定条件と
なる項目５４１を生成する場合、確定条件であることは
確定条件ボタンＣ０がクリックされた否かにより判断
し、信号名と信号値となる項目５４２はタイムチャート
上でユーザが指定したＣ１およびＣ３のクリック位置に
より判断し、条件となる項目５４３はＡＮＤまたはＯＲ
ボタンにより判断し、これら情報により生成する。

【００２９】また前記確定値となる項目５４４を生成す
る場合は、確定値であることは確定値ボタンＣ４がクリ
ックされたか否かにより判断し、信号名と信号値と確定
するまでの時間となる項目５４５はタイムチャート上で
ユーザが指定したＣ５のクリック位置により判断する。
信号ＣがＬｏｗになる論理仕様（符号５２）についても
同様に各項目についてクリック位置等より判断し、これ
らの情報を元に、チェック項目情報の記述フォーマット
に従い生成する。

【００３０】次いでチェック項目生成手段１６は、図４
のフローの如く、ユーザが処理実行時のコマンドのオプ
ション等により、前回生成したチェック項目情報１４を
入力指定したか判別し（ステップ４４）、入力指定した
場合（ステップ４５）は、ステップ４６以下の処理を行
い、入力指定されていない場合は、前記ステップ４３で
生成したユーザ指定によるチェック項目情報５３をその
ままチェック項目情報１８として出力し終了する（ステ
ップ４９）。

【００３１】前記ステップ４５において入力を指定した
場合は、前回生成したチェック項目情報１４を入力し
（ステップ４６）、前記ステップ４３で生成したユーザ
指定によるチェック項目情報５３のうち、前回生成した
チェック項目情報１４に含まれないチェック項目情報を
差分情報５６として抽出する（ステップ４７）。

【００３２】図５に示した例では、ユーザ指定によるチ
ェック項目情報５３のうち、項目５４は、前回生成した
チェック項目情報１４上に定義された項目５０の中に同
じ内容が定義され、これに対し項目５５は項目５０の中
に定義されているどの項目とも一致しないため、差分情
報５６は項目５５となる。

【００３３】次いでチェック項目生成手段１６は、ステ
ップ４７で抽出した差分情報５６のチェック項目情報５
５をステップ４６で入力した前回生成したチェック項目
情報１４のチェック項目情報５０に追加（ステップ４
８）し、この追加したチェック項目情報１８を生成及び
出力（ステップ４９）して終了する。以上が、チェック
項目生成手段１６による、チェック項目生成処理の流れ
である。

【００３４】次に、前述の構成の理検証方法を実行する
論理検証システムにおける変更された論理データを検証
する処理を図６のフローチャートを用いて説明する。ま
ず、本処理は、論理データ１０に変更を行い（ステップ
６０１）、論理変更後論理データ１７を作成した場合、
論理が変更された部分が期待通り動作することを論理シ
ミュレーション手段１２を用いて検証するためにテスト
パターンデータ１１を作成し（ステップ６０２）、これ
を用いて論理シミュレーションを実行し（ステップ６０
３）、次いで検証者が論理シミュレーション手段１２
（図１）の出力である波形データ１３（図５）を参照し
て論理が期待通り動作しているかどうかを判定する（ス
テップ６０４）。

【００３５】該ステップ６０４において期待通り論理が
動作している場合は、次回の論理変更時におけるデグレ
ード検証用に現存するチェック項目情報１４とチェック
項目生成手段１６を用いて、チェック項目情報１８を生
成（ステップ６０８）して処理を終了する。

【００３６】前記ステップ６０４において期待通り論理
が動作していない場合は、論理データの変更を行い（ス
テップ６０５）、次にモデルチェッキング手段１９（図
１）が今回の論理変更前に生成したチェック項目情報１
４を使用したデグレード検証を実施する（ステップ６０
６）。このステップ６０５において論理変更前に生成し
たチェック項目情報１４が無い場合は、従来通りの既存
テストパターンデータを用いた論理シミュレーションを
実施するか、今回の論理変更前に論理シミュレーション
を実行したときの波形データ１３からチェック項目情報
１４を生成する。

【００３７】次いで本処理は、前記ステップ６０５によ
るモデルチェッキング結果にデグレード発生によるエラ
ーの有無を判定し（ステップ６０７）、エラーがある場
合はステップ６０５に戻って再度論理を修正し、エラー
がない場合はステップ６０３に戻って再度の論理シミュ
レーションを実施し、ステップ６０４において論理が期
待通り動作していると判定するまで前記ステップ６０５
〜６０７の処理を繰り返す様に動作し、ステップ６０４
において論理が期待通り動作していると判定された際に
は前記同様に次回の論理変更時におけるデグレード検証
用に現存するチェック項目情報１４とチェック項目生成
手段１６を用いて、チェック項目情報１８を生成（ステ
ップ６０８）して処理を終了する。この詳細は図４と図
５を用いて説明した通りである。

【００３８】以上述べた如く本実施形態による論理デー
タの検証方法及び該検証方法を実行する論理検証システ
ムによれば、デグレード検証用に膨大なテストパターン
について、論理シミュレーションを繰り返し実施する必
要がなくなると言う効果を奏する。

【００３９】図７は、本発明による論理データの検証方
法を一般のコンピュータシステムにおいて実行するため
のハード構成の一例を示す図である。本実施形態による
システム構成は、ＣＰＵ７２、メモリ７６、ハードディ
スク７７及び記録媒体書き込み手段７３を含むコンピュ
ータ本体と、該コンピュータに接続するＣＲＴ等の表示
手段７１、入力手段７５、前記記録媒体書き込み手段７
３によりデータの記録再生が行われる、フロッピーディ
スク／光磁気記録ディスク等の記録媒体７０、出力結果
７４を出力するプリンタ等（図示せず）により構成さ
れ、前記ハードディスク７７には前述の実施形態で説明
した論理データの検証方法を実行するプログラム及び必
要なデータが記憶されている。

【００４０】本実施形態によるコンピュータシステム
は、ＣＰＵ７２がハードディスク７７に記録した論理デ
ータの検証方法を実行するプログラム並びに論理データ
及びテストパターン他のデータを読み出してメモリ７６
上に展開して実行し、前記実施形態で説明した論理検証
方法に従い、入力手段７５により処理実行コマンドおよ
び入力指定または出力指定を入力して処理を行うことに
より、処理結果を表示手段７１または出力結果７４に出
力する様に動作する。

【００４１】尚、本例では論理データの検証方法を実行
するプログラム並びにデータをハードディスク７７に記
憶しておく例を説明したが、本発明はこれに限られるも
のではなく、記憶媒体７０に前記プログラム及びデータ
を記憶しておき、この記憶された論理検証方法を記憶媒
体読み込み手段７３により読み込んで前述の処理を実行
することもできる。この場合の記憶媒体としては、フロ
ッピーディスク／光磁気記録ディスク／光ディスクの動
的記憶手段や半導体にデータを記憶するフラッシュメモ
リ等の静的記憶手段が考えられる。

【００４２】以上述べた如く本発明は、ハードウェア記
述言語にて作成した半導体集積回路の論理データと論理
シミュレーションのテストパターンを記載したテストパ
ターンデータとを元にタイムチャート形式の波形データ
を作成する論理シミュレーション手段と、前記波形デー
タを元にしてモデルチェッキングの対象とする信号名お
よびその信号の確定条件をユーザが指定するための入力
手段と、前記波形データと前記入力手段によって指定さ
れた信号名と確定条件を元にモデルチェッキングで入力
可能な形式のチェック項目情報を生成するチェック項目
生成手段と、前記チェック項目情報を入力し、論理デー
タのモデルチェッキングを行う手段と、前記チェック項
目生成手段に前回生成したチェック項目情報を入力する
手段とをを設け、前記波形データと前記入力手段にて指
定した信号名および確定条件より生成したチェック項目
情報のうち、前回生成したチェック項目情報に含まれな
い部分のみを前回生成したチェック項目情報に追加し出
力することにより、論理シミュレーションにて検証した
テストパターンの波形データをもとに、入力手段にてモ
デルチェッキングの対象とする信号名およびその信号の
確定条件をユーザが指定するだけで、チェック項目情報
を生成することができる。

【００４３】本発明によれば、チェック項目情報への変
換ミスを低減でき、また論理シミュレーションにて確認
した波形データをもとにチェック項目情報を生成するた
め、論理仕様の誤解によるチェック項目情報の作成ミス
を低減でき、チェック項目情報の作成精度も向上するこ
とができる。また、論理シミュレーションとモデルチェ
ッキングの双方にて、どの機能に対し検証したかの対応
がつくため、両者を併用した効率のよい論理検証を行う
ことができる。これにより、論理変更時に、この変更に
依存しない機能についてデグレードが起きていないかを
検証する際は、論理変更前に論理シミュレーションにて
検証した、この機能を実現するためのテストデータの波
形データをもとにチェック項目情報を生成し、これを用
いてモデルチェッキングを実行しエラーが指摘されてな
いことを確認することにより検証を行うことができる。

【００４４】従来まではデグレード検証のために膨大な
テストパターンについて論理シミュレーションを実施し
検証する必要があったが、デグレード検証をモデルチェ
ッキング主体にすることにより、これらのテストパター
ンの波形データからチェック項目情報を生成し蓄積して
おくことにより、蓄積したチェック項目情報を用いてモ
デルチェッキングを１度実施するだけでデグレード検証
が可能となる。

【００４５】これにより、デグレード検証時の論理シミ
ュレーション数を削減することができ、検証工数と計算
機資源の低減を図ることができる。

【００４６】尚、本発明は次に挙げる実施形態としても
表すことができる。

【００４７】＜実施形態１＞ ハードウェア記述言語に
て作成した半導体集積回路の論理データをモデルチェッ
キングを利用し検証する形式的論理検証方法において、
前記論理データとそれをテストするための論理シミュレ
ーションのテストパターンを定義したテストパターンデ
ータより、タイムチャート形式の波形データを作成する
論理シミュレーション手段と、前記波形データをもとに
してモデルチェッキングの対象となる信号名およびその
信号の確定条件をユーザが指定するための入力手段と、
前記波形データと前記入力手段によって指定された信号
名と確定条件より、モデルチェッキングで入力可能な形
式のチェック項目情報を生成するチェック項目生成手段
と、前記チェック項目情報を入力し、論理データのモデ
ルチェッキングを行う手段を備え、前記論理データが変
更されたとき、論理データ変更対象外の部分について前
記チェック項目情報を用いモデルチェッキングを実施す
ることにより、その部分についてデグレードがないこと
を確認することを特徴とする論理検証方法。

【００４８】＜実施形態２＞ 前記チェック項目生成手
段に前回生成したチェック項目情報を入力する手段を設
け、前記波形データと前記入力手段にて指定した信号名
および確定条件より生成したチェック項目情報のうち、
前回生成したチェック項目情報に含まれない部分のみを
前回生成したチェック項目情報に追加し出力するチェッ
ク項目生成手段を備えることを特徴とする実施形態１記
載のの論理検証方法。

【００４９】＜実施形態３＞ ハードウェア記述言語に
て作成した半導体集積回路の論理データをモデルチェッ
キングを利用し検証する形式的論理検証方法において、
前記論理データとそれをテストするための論理シミュレ
ーションのテストパターンを定義したテストパターンデ
ータより、タイムチャート形式の波形データを作成する
論理シミュレーション手段と、前記波形データをもとに
してモデルチェッキングの対象となる信号名およびその
信号の確定条件をユーザが指定するための入力手段と、
前記波形データと前記入力手段によって指定された信号
名と確定条件より、モデルチェッキングで入力可能な形
式のチェック項目情報を生成するチェック項目生成手段
と、前記チェック項目情報を入力し、論理データのモデ
ルチェッキングを行う手段を備え、前記論理データが変
更されたとき、論理データ変更対象外の部分について前
記チェック項目情報を用いモデルチェッキングを実施す
ることにより、その部分についてデグレードがないこと
を確認することを特徴とする論理検証方法を実現させる
ためのプログラムを記録した媒体。

【００５０】＜実施形態４＞ 前記チェック項目生成手
段に前回生成したチェック項目情報を入力する手段を設
け、前記波形データと前記入力手段にて指定した信号名
および確定条件より生成したチェック項目情報のうち、
前回生成したチェック項目情報に含まれない部分のみを
前回生成したチェック項目情報に追加し出力するチェッ
ク項目生成手段を備えることを特徴とする実施形態１記
載のの論理検証方法を実現させるためのプログラムを記
録した媒体。

【００５１】

【発明の効果】本発明によれば、一旦論理シミュレーシ
ョンにて検証されたテストパターンの波形データからチ
ェック項目情報を生成することができるので、チェック
項目情報の作成精度を向上することができる。

【００５２】また、論理変更時に論理データがデグレー
ドしていないことを確認する際、論理変更に依存しない
機能について、論理変更前に論理シミュレーションにて
確認した、この機能を実現するためのテストパターンの
波形データを元に、チェック項目情報を生成し、このチ
ェック項目情報によりモデルチェッキングを実施するこ
とにより、論理データがデグレードしていないことを検
証することが可能となるので、膨大なテストパターンに
ついて論理変更の度に論理シミュレーションを実施する
必要がなくなり、検証作業の効率を上げることができ
る。

【図面の簡単な説明】

【図１】本発明による論理検証方法を実行する論理検証
システムの全体概略構成の一実施形態を説明するための
図。

【図２】従来のモデルチェッキングを利用し検証する形
式的論理検証の処理構成を説明するための図。

【図３】本実施形態による変更前後の論理データを示す
論理図。

【図４】本実施形態によるチェック項目生成手段の概要
の流れ図。

【図５】本実施形態によるチェック項目生成手段に関連
するデータを示す図。

【図６】本実施形態による本発明を利用した論理検証フ
ローを示す図。

【図７】本実施形態によるモデルチェッキングを利用し
検証する形式的論理検証方法のハード構成図。

【符号の説明】

１０…論理データ、１１…テストパターンデータ、１２
…論理シミュレーション手段、１３…波形データ、１４
…前回生成したチェック項目情報、１５…ユーザ指定
部、１６…チェック項目生成手段、１７…論理変更後論
理データ、１８…チェック項目情報、１９…モデルチェ
ッキング手段、１Ａ…モデルチェッキング結果、２０…
論理仕様書、７０…記憶媒体、７１…表示手段、７２…
ＣＰＵ、７３…記憶媒体読み込み手段、７４…出力結
果、７５…入力手段、７６…メモリ、７７…ハードディ
スク。

Claims (5)

【特許請求の範囲】
1. 【請求項１】 ハードウェア記述言語にて作成した半導
   体集積回路の論理データをモデルチェッキングにより検
   証する論理データの検証方法であって、 前記論理データと該論理データをテストするための論理
   シミュレーションのテストパターンとを定義したテスト
   パターンデータよりタイムチャート形式の波形データを
   作成し、 前記波形データを元に入力されたモデルチェッキングの
   対象となる信号名及びその信号の確定条件並びに前記波
   形データとよりモデルチェッキングで入力可能な形式の
   チェック項目情報を生成し、 前記論理データが変更されたとき、論理データ変更対象
   外の部分について前記チェック項目情報を用いモデルチ
   ェッキングを実行することを特徴とする論理データの検
   証方法。
2. 【請求項２】 前回生成したチェック項目情報を入力
   し、前記波形データと前記入力した信号名および確定条
   件より生成したチェック項目情報のうち、前回生成した
   チェック項目情報に含まれない部分のみを前回生成した
   チェック項目情報に追加することを特徴とする請求項１
   記載の論理データの検証方法。
3. 【請求項３】 ハードウェア記述言語にて作成した半導
   体集積回路の論理データをモデルチェッキングにより検
   証する論理検証システムにおいて、 前記論理データと該論理データをテストするための論理
   シミュレーションのテストパターンを定義したテストパ
   ターンデータとによりタイムチャート形式の波形データ
   を作成する論理シミュレーション手段と、 前記波形データを元にモデルチェッキングの対象となる
   信号名及びその信号の確定条件を入力する入力手段と、 前記波形データと前記入力手段によって入力された信号
   名と確定条件とによりモデルチェッキングで入力可能な
   形式のチェック項目情報を生成するチェック項目生成手
   段と、 前記チェック項目情報を入力し、論理データのモデルチ
   ェッキングを行う手段とを備え、 前記論理データが変更されたとき、論理データ変更対象
   外の部分について前記チェック項目情報を用いモデルチ
   ェッキングを実行することを特徴とする論理検証システ
   ム。
4. 【請求項４】 前記チェック項目生成手段に前回生成し
   たチェック項目情報を入力する手段を設け、前記波形デ
   ータと前記入力手段にて指定した信号名および確定条件
   より生成したチェック項目情報のうち、前回生成したチ
   ェック項目情報に含まれない部分のみを前回生成したチ
   ェック項目情報に追加し出力するチェック項目生成手段
   を備えたことを特徴とする請求項３記載の論理検証シス
   テム。
5. 【請求項５】 ハードウェア記述言語にて作成した半導
   体集積回路の論理データをモデルチェッキングにより検
   証する論理データの検証方法のプログラムを格納する記
   録媒体であって、 前記論理データの検証方法のプログラムが、前記論理デ
   ータと該論理データをテストするための論理シミュレー
   ションのテストパターンとを定義したテストパターンデ
   ータよりタイムチャート形式の波形データを作成し、前
   記波形データを元に入力されたモデルチェッキングの対
   象となる信号名及びその信号の確定条件並びに前記波形
   データとよりモデルチェッキングで入力可能な形式のチ
   ェック項目情報を生成し、前記論理データが変更された
   とき、論理データ変更対象外の部分について前記チェッ
   ク項目情報を用いモデルチェッキングを実行するプログ
   ラムであることを特徴とする記録媒体。