(57)【要約】      （修正有）【課題】論理検証結果の漏れを低減するための論理検証装置を提供する。【解決手段】論理検証装置１０は、検証対象回路の策定動作の第１前提記述と第１前提に基づく策定動作の第１仕様記述とを含む第１アサーション９２と、検証対象回路の策定動作を検証するための第１テストパタンと、を受け付ける入力部１１と、第１アサーション９２を解析することにより、検証対象回路の信号の値の確定条件を示す確定ルールアサーションと、検証対象回路の信号の値の保持条件を示す保持ルールアサーションと、を抽出する抽出部１２と、抽出された確定ルールアサーション及び保持ルールアサーションに基づいて、確定条件と検証対象回路の信号との関係を示すテーブル生成部１３と、これに基づいて、第１アサーション９２及び第１テストパタンに含まれていない検証対象回路の非策定動作を検証するための検証情報を生成する検証情報生成部１４と、を備える。【選択図】図２
2011186817.tif 000002
【特許請求の範囲】
【請求項１】
検証対象回路の策定動作の第１前提を示す第１前提記述と前記第１前提に基づく策定動作の第１仕様を示す第１仕様記述とを含む第１アサーションと、前記検証対象回路の策定動作を検証するための第１テストパタンと、を受け付ける入力部と、
前記入力部により受け付けられた第１アサーションを解析することにより、前記検証対象回路の信号の値を確定させるための確定条件を示す確定ルールアサーションと、前記検証対象回路の信号の値を保持するための保持条件を示す保持ルールアサーションと、を抽出する抽出部と、
前記抽出部により抽出された確定ルールアサーション及び保持ルールアサーションに基づいて、前記確定条件と前記検証対象回路の信号との関係を示すルールテーブルを生成するテーブル生成部と、
前記テーブル生成部により生成されたルールテーブルに基づいて、前記第１アサーション及び前記第１テストパタンに含まれていない前記検証対象回路の非策定動作を検証するための検証情報を生成する検証情報生成部と、
を備えることを特徴とする論理検証装置。
【請求項２】
前記テーブル生成部は、前記確定条件の有効条件及び無効条件を登録し、前記確定ルールアサーションに基づいて信号を送信する送信デバイスについて前記有効条件下の信号の値及び前記無効条件下の信号の値を登録し、前記保持ルールアサーションに基づいて信号を受信する受信デバイスについて前記有効条件下の信号の値及び前記無効条件下の信号の値を登録する、請求項１記載の論理検証装置。
【請求項３】
前記検証情報生成部は、前記テーブル生成部によって生成されたルールテーブルに基づいて、前記第１前提に含まれていない前記検証対象回路の非策定動作の前提を示す第２前提記述と、前記第２前提に基づく非策定動作の第２仕様を示す第２仕様記述と、を含む第２アサーションを生成する、請求項１又は２記載の論理検証装置。
【請求項４】
前記検証情報生成部は、前記テーブル生成部によって生成されたルールテーブルに基づいて、前記第１テストパタンにおいて前記信号が無効であるときの前記信号の値がランダムに定められている第２テストパタンを生成する、請求項１乃至３の何れか１項記載の論理検証装置。
【請求項５】
検証対象回路の策定動作の第１前提を示す第１前提記述と前記第１前提に基づく策定動作の第１仕様を示す第１仕様記述とを含む第１アサーションと、前記検証対象回路の策定動作を検証するための第１テストパタンと、を受け付け、
前記第１アサーションを解析することにより、前記検証対象回路の信号の値を確定させるための確定条件を示す確定ルールアサーションと、前記検証対象回路の信号の値を保持するための保持条件を示す保持ルールアサーションと、を抽出し、
前記確定ルールアサーション及び前記保持ルールアサーションに基づいて、前記確定条件と前記検証対象回路の信号との関係を示すルールテーブルを生成し、
前記ルールテーブルに基づいて、前記第１アサーション及び前記第１テストパタンに含まれていない前記検証対象回路の非策定動作を検証するための検証情報を生成する、
ことを特徴とする論理検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理検証装置及び論理検証方法に関し、より詳しくは、半導体装置の設計に用いられる論理検証装置及び論理検証方法に関する。
【背景技術】
【０００２】
近年、ＯＣＰ(Open Core Protocol)やＡＭＢＡ（Advanced Microcontroller Bus Architecture）等のカスタム可能なオンチップバスが広く利用されている。
【０００３】
そのようなオンチップバスには、半導体装置の機能が記述された仕様書と、機能毎に定められた仕様が記述されたコンプライアンス等のチェックリストと、が用意されている。一般的には、コンプライアンスは、汎用的なアサーションを作成するベンダから提供される。従って、ユーザは、ベンダから提供されるチェックリストを用いることにより、自らチェックリストを作成することとなく、ＲＴＬ（Register Transfer Level）記述を論理検証するためのシミュレーション、エミュレーション、及びフォーマルチェックを実行することができる。
【０００４】
しかしながら、ベンダから提供される仕様書には、信号を送信する送信デバイスの有効条件下の動作（以下、「策定動作」という）は記述されているが、送信デバイスの無効条件下の動作、信号を受信する受信デバイスの有効条件下の動作、及び受信デバイスの無効条件下の動作（以下、「非策定動作」という）は記述されていない。
【０００５】
一方、アサーションを生成する技術（特許文献１を参照）も知られている。
【０００６】
しかしながら、特許文献１に開示されている技術を用いたとしても、非策定動作の違反を検出するためのアサーションを生成することはできない。
【０００７】
従って、従来の汎用的なアサーションを使用したとしても、非策定動作の違反を検出することはできない。すなわち、従来の汎用的なアサーションを使用するＲＴＬ記述の論理検証結果には、非策定動作の論理検証結果は含まれない。換言すると、従来のアサーションを使用した場合には、論理検証結果に漏れが生じる。それにより、半導体装置の設計の時間的損失及び経済的損失が増加する。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２００７−２６４９９４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
本発明の目的は、論理検証結果の漏れを低減するための論理検証装置及び論理検証方法を提供することである。
【課題を解決するための手段】
【００１０】
本発明の第１態様によれば、
検証対象回路の策定動作の第１前提を示す第１前提記述と前記第１前提に基づく策定動作の第１仕様を示す第１仕様記述とを含む第１アサーションと、前記検証対象回路の策定動作を検証するための第１テストパタンと、を受け付ける入力部と、
前記入力部により受け付けられた第１アサーションを解析することにより、前記検証対象回路の信号の値を確定させるための確定条件を示す確定ルールアサーションと、前記検証対象回路の信号の値を保持するための保持条件を示す保持ルールアサーションと、を抽出する抽出部と、
前記抽出部により抽出された確定ルールアサーション及び保持ルールアサーションに基づいて、前記確定条件と前記検証対象回路の信号との関係を示すルールテーブルを生成するテーブル生成部と、
前記テーブル生成部により生成されたルールテーブルに基づいて、前記第１アサーション及び前記第１テストパタンに含まれていない前記検証対象回路の非策定動作を検証するための検証情報を生成する検証情報生成部と、
を備えることを特徴とする論理検証装置、
が提供される。
【００１１】
本発明の第２態様によれば、
検証対象回路の策定動作の第１前提を示す第１前提記述と前記第１前提に基づく策定動作の第１仕様を示す第１仕様記述とを含む第１アサーションと、前記検証対象回路の策定動作を検証するための第１テストパタンと、を受け付け、
前記第１アサーションを解析することにより、前記検証対象回路の信号の値を確定させるための確定条件を示す確定ルールアサーションと、前記検証対象回路の信号の値を保持するための保持条件を示す保持ルールアサーションと、を抽出し、
前記確定ルールアサーション及び前記保持ルールアサーションに基づいて、前記確定条件と前記検証対象回路の信号との関係を示すルールテーブルを生成し、
前記ルールテーブルに基づいて、前記第１アサーション及び前記第１テストパタンに含まれていない前記検証対象回路の非策定動作を検証するための検証情報を生成する、
ことを特徴とする論理検証方法、
が提供される。
【発明の効果】
【００１２】
本発明によれば、論理検証結果の漏れを低減することができる。それにより、半導体装置の設計の時間的損失及び経済的損失を低減することができる。
【図面の簡単な説明】
【００１３】
【図１】本発明の第１実施形態に係る論理検証装置１０を含むシステムの構成を示すブロック図である。
【図２】図１の論理検証装置１０の構成を示すブロック図である。
【図３】第１実施形態に係る論理検証処理の手順を示すフローチャートである。
【図４】図３のテーブル生成ステップ（Ｓ３０３）の手順を示すフローチャートである。
【図５】図４のＳ４０１及びＳ４０３で生成される確定ルールテーブルの構造を示す概略図である。
【図６】図４のＳ４０４〜Ｓ４０７で生成される保持ルールテーブルの構造を示す概略図である。
【図７】図４のＳ４０８及びＳ４０９で生成される確定ルールテーブルの構造を示す概略図である。
【図８】図７の確定ルールテーブルに対応する第２アサーション９４の一例を示す概略図である。
【図９】図６の保持ルールテーブルに対応する第２アサーション９４の一例を示す概略図である。
【図１０】本発明の第２実施形態に係る論理検証装置１０を含むシステムの構成を示すブロック図である。
【図１１】第２実施形態に係る検証情報生成ステップ（Ｓ３０４）の手順を示すフローチャートである。
【図１２】図１１のテストパタン生成ステップ（Ｓ１１０４）において用いられる第１アサーション９２の一例を示す概略図である。
【図１３】図１２の第１アサーション９２に対応する第２テストパタン９７の一例を示す概略図である。
【図１４】（Ａ）は第１テストパタン９３の信号波形を示す概略図であり、（Ｂ）は第２テストパタン９７の信号波形を示す概略図である。
【発明を実施するための形態】
【００１４】
以下、本発明の実施形態について、図面を参照して詳細に説明する。
【００１５】
（第１実施形態）
本発明の第１実施形態について説明する。第１実施形態は、策定動作に関する第１アサーションから、非策定動作に関する第２アサーションを生成する論理検証装置の例である。
【００１６】
第１実施形態に係る論理検証装置の構成について説明する。図１は、本発明の第１実施形態に係る論理検証装置１０を含むシステムの構成を示すブロック図である。図２は、図１の論理検証装置１０の構成を示すブロック図である。
【００１７】
図１のシステムは、論理検証装置１０と、入力装置２０と、チェッカ３０と、出力装置４０と、を備える。
【００１８】
図１の入力装置２０は、ユーザにより入力されるＲＴＬ記述９１、第１アサーション９２、及び第１テストパタン９３を受け付けるように構成される。ＲＴＬ記述９１は、検証対象回路を示す回路記述である。第１アサーション９２は、検証対象回路の策定動作を規定する複数の動作条件を含む。各動作条件は、検証対象回路の策定動作の第１前提を示す第１前提記述と、第１前提に基づく策定動作の第１仕様を示す第１仕様記述と、を含む。例えば、入力装置２０は、キーボード又は通信装置である。例えば、第１アサーション９２は、ベンダから提供されるコンプライアンスに含まれる。例えば、第１テストパタン９３は、検証対象回路の策定動作を検証するためのテストパタンである。
【００１９】
図１の論理検証装置１０は、入力装置２０により受け付けられた第１アサーション９２に基づいて第２アサーション９４を生成するように構成される。第２アサーション９４は、検証対照回路の非策定動作を規定する複数の動作条件を含む。各動作条件は、検証対象回路の動作のうち第１前提に含まれていない非策定動作の前提を示す第２前提記述と、第２前提に基づく非策定動作の第２仕様を示す第２仕様記述と、を含む。図２に示すように、論理検証装置１０は、入力部１１と、抽出部１２と、テーブル生成部１３と、検証情報生成部１４と、出力部１５と、を備える。
【００２０】
図２の入力部１１は、入力装置２０により受け付けられたＲＴＬ記述９１と、第１アサーション９２と、第１テストパタン９３と、を受け付けるように構成される。すなわち、入力部１１は、論理検証装置１０と入力装置２０との間のインタフェースである。
【００２１】
図２の抽出部１２は、入力部１１により受け付けられた第１アサーション９２を解析することにより、確定ルールアサーションと、保持ルールアサーションと、を抽出するように構成される。確定ルールアサーションは、検証対象回路の信号の値を０又は１に確定させるための条件（以下、「確定条件」という）を示す。保持ルールアサーションは、検証対象回路の信号の値を保持するための条件（以下、「保持条件」という）を示す。
【００２２】
図２のテーブル生成部１３は、抽出部１２により抽出された確定ルールアサーション及び保持ルールアサーションに基づいて、確定条件と検証対象回路の信号との関係を示すルールテーブルを生成するように構成される。具体的には、テーブル生成部１３は、「有効条件」及び「無効条件」を含む確定条件をルールテーブルに登録する。有効条件は、信号が有効であることを他のデバイスへ知らせるための条件である。無効条件は、信号が無効であることを他のデバイスへ知らせるための条件である。有効条件及び無効条件は、信号名及び信号の値を含む。次いで、テーブル生成部１３は、確定ルールアサーションに基づいて信号を送信する送信デバイスについて、「有効条件」下の信号の値及び「無効条件」下の信号の値をルールテーブルに登録する。次いで、テーブル生成部１３は、保持ルールアサーションに基づいて信号を受信する受信デバイスについて、「有効条件」下の信号の値及び「無効条件」下の信号の値をルールテーブルに登録する。例えば、プロセッサがメモリにデータを書き込む場合には、プロセッサが送信デバイスであり、メモリが受信デバイスである。
【００２３】
図２の検証情報生成部１４は、テーブル生成部１３により生成されたルールテーブルに基づいて、第１アサーション９２及び第１テストパタン９３に含まれていない検証対象回路の非策定動作を検証するための検証情報を生成するように構成される。具体的には、検証情報生成部１４は、第２アサーション９４を生成する。
【００２４】
図２の出力部１５は、検証情報生成部１４により生成された第２アサーション９４を含む検証情報をチェッカ３０に供給するように構成される。すなわち、出力部１５は、論理検証装置１０と出力装置４０との間のインタフェースである。
【００２５】
図１のチェッカ３０は、入力装置２０により受け付けられた第１アサーション９２及び第１テストパタン９３に基づいて、ＲＴＬ記述９１の策定動作の論理検証を行う。それにより、第１論理検証結果９５が生成される。また、チェッカ３０は、入力装置２０により受け付けられた第１テストパタン９３及び論理検証装置１０により生成された第２アサーション９４に基づいて、ＲＴＬ記述９１の非策定動作の論理検証を行う。それにより、第２論理検証結果９６が生成される。例えば、チェッカ３０は、シミュレータ、エミュレータ、及びフォーマルチェッカ等の既存ツールである。
【００２６】
図１の出力装置４０は、チェッカ３０により生成された第１論理検証結果９５及び第２論理検証結果９６を出力するように構成される。例えば、出力装置４０は、ディスプレイ又は通信装置である。
【００２７】
第１実施形態に係る論理検証装置のオペレーションについて説明する。図３は、第１実施形態に係る論理検証処理の手順を示すフローチャートである。図４は、図３のテーブル生成ステップ（Ｓ３０３）の手順を示すフローチャートである。図５は、図４のＳ４０１及びＳ４０３で生成される確定ルールテーブルの構造を示す概略図である。図６は、図４のＳ４０４〜Ｓ４０７で生成される保持ルールテーブルの構造を示す概略図である。図７は、図４のＳ４０８及びＳ４０９で生成される確定ルールテーブルの構造を示す概略図である。図８は、図７の確定ルールテーブルに対応する第２アサーション９４の一例を示す概略図である。図９は、図６の保持ルールテーブルに対応する第２アサーション９４の一例を示す概略図である。
【００２８】
＜図３：入力ステップ（Ｓ３０１）＞  入力部１１が、ＲＴＬ記述９１と、第１アサーション９２と、第１テストパタン９３と、を受け付ける。それにより、論理検証処理に必要な情報が論理検証装置１０に供給される。
【００２９】
＜図３：抽出ステップ（Ｓ３０２）＞  抽出部１２が、入力ステップ（Ｓ３０１）において受け付けられた第１アサーション９２を解析することにより、確定ルールアサーションと、保持ルールアサーションと、を抽出する。確定ルールアサーションは、ＯＣＰ（Open Core Protocol）やＡＭＢＡ（Advanced Micro-controller Bus Architecture）等の標準的なプロトコルのハンドシェイクを伴う信号（以下、「ハンドシェイク信号」という）の確定ルール（known rule）を示す。保持ルールアサーションは、ハンドシェイク信号の保持ルール（stable rule）を示す。
【００３０】
＜図３：テーブル生成ステップ（Ｓ３０３）＞  テーブル生成部１３が、抽出ステップ（Ｓ３０２）において抽出された確定ルールアサーション及び保持ルールアサーションに基づいて、確定条件と検証対象回路の信号との関係を示すルールテーブルを生成する。このとき、テーブル生成部１３は、ベンダから提供される仕様書に言及されていない非策定ルールを考慮して、ルールテーブルを生成する。非策定ルールは、ハンドシェイクを伴うプロトコルにおいて、論理的前提に基づいて定められるルールである。換言すると、非策定ルールは、確定ルールの確定条件（「有効条件」及び「無効条件」）下のデバイス（送信デバイス及び受信デバイス）の動作に関するルールと、保持ルールの保持条件（「受領有り」及び「受領無し」）下のデバイス（送信デバイス及び受信デバイス）の動作に関するルールと、を示す。すなわち、非策定ルールでは、送信デバイスの「無効条件」下の動作と、受信デバイスの「有効条件」下の動作と、受信デバイスの「無効条件」下の動作と、送信デバイスの受領有りの動作と、受信デバイスの受領無しの動作と、受信デバイスの受領有りの動作と、が定義される。
【００３１】
図３のテーブル生成ステップ（Ｓ３０３）について説明する。
【００３２】
図５の確定ルールでは、「有効条件」の記述は“SResp != 0”であり、「無効条件」の記述は“SResp == 0”である。また、図６の保持ルールでは、「受領無し」の記述は“MRespAccept != 1”であり、「受領有り」の記述は“MRespAccept == 0”である。
【００３３】
＜図４：Ｓ４０１＞  テーブル生成部１３が、送信デバイスの「有効条件」下の動作を抽出し、抽出した動作を確定ルールテーブルに記録する。例えば、送信デバイスの「有効条件」下の動作を表す記述である“SRespLast = 0|1”が確定ルールテーブル（図５の（Ｋ１））に記録される。
【００３４】
＜図４：Ｓ４０２＞  テーブル生成部１３が、送信デバイスの「無効条件」下の動作を抽出し、抽出した動作を確定ルールテーブルに記録する。例えば、送信デバイスの「無効条件」下の動作を表す記述である“SRespLast = 0|1|x|z”が確定ルールテーブル（図５の（Ｋ２））に記録される。
【００３５】
＜図４：Ｓ４０３＞  テーブル生成部１３が、受信デバイスの「有効条件」下のサンプル動作及び「無効条件」下のサンプル動作を確定ルールテーブルに記録する。なお、受信デバイスの「有効条件」下の動作及び「無効条件」下の動作は、保持ルールに基づいて定められる。従って、Ｓ４０３では、サンプル動作が記録される。例えば、受信デバイスの「有効条件」下のサンプル動作を表す記述である“OK”と、受信デバイスの「無効条件」下のサンプル動作を表す記述である“NG”と、が確定ルールテーブル（図５の（Ｋ３），（Ｋ４））に記録される。
【００３６】
＜図４：Ｓ４０４＞  テーブル生成部１３が、送信デバイスの「受領無し」の動作を抽出し、抽出した動作を保持ルールテーブルに記録する。例えば、送信デバイスの「受領無し」の動作を表す記述である“$stable(SRespLast)”が保持ルールテーブル（図６の（Ｓ１））に記録される。
【００３７】
＜図４：Ｓ４０５＞  テーブル生成部１３が、送信デバイスの「受領有り」の動作を抽出し、抽出した動作を保持ルールテーブルに記録する。例えば、送信デバイスの「受領有り」の動作を表す記述である“0(inactive)”が保持ルールテーブル（図６の（Ｓ２））に記録される。
【００３８】
＜図４：Ｓ４０６＞  テーブル生成部１３が、受信デバイスの「受領無し」の動作を抽出し、抽出した動作を保持ルールテーブルに記録する。例えば、受信デバイスの「受領有り」の動作を表す記述である“[0:’TIMEOUT] MRespAccept = 1”が保持ルールテーブル（図６の（Ｓ３））に記録される。
【００３９】
＜図４：Ｓ４０７＞  テーブル生成部１３が、受信デバイスの「受領有り」の動作を抽出し、抽出した動作を保持ルールテーブルに記録する。例えば、受信デバイスの受領有りの動作を表す記述である“MRespAccept=0”が保持ルールテーブル（図６の（Ｓ４））に記録される。それにより、保持ルールテーブルが完成する。
【００４０】
＜図４：Ｓ４０８＞  テーブル生成部１３が、保持ルールテーブルを用いて、受信デバイスの「有効条件」下の動作を抽出し、抽出した動作を確定ルールテーブルに記録する。例えば、受信デバイスの「無効条件」下の動作を表す記述である“[0:’TIMEOUT] MRespAccept = 1”が確定ルールテーブル（図５の（Ｋ３））に記録される。
【００４１】
＜図４：Ｓ４０９＞  テーブル生成部１３が、保持ルールテーブルを用いて、受信デバイスの「無効条件」下の動作を抽出し、抽出した動作を確定ルールテーブルに記録する（図５の（Ｋ４））。例えば、受信デバイスの「無効条件」下の動作を表す記述である“[*0:’TIMEOUT] MRespAccept = 0”が確定ルールテーブルに記録される。それにより、確定ルールテーブルが完成する。
【００４２】
図４のテーブル生成ステップは、確定ルールテーブル及び保持ルールテーブルが完成した後に終了する。
【００４３】
すなわち、図４では、テーブル生成部１３は、送信デバイスの確定ルールに基づく動作を導出し、次いで送信デバイス及び受信デバイスの保持ルールに基づく動作を導出し、次いで保持ルールを用いて受信デバイスの確定ルールに基づく動作を導出する。それにより、非策定動作の確定ルール及び保持ルールが決まる。
【００４４】
＜図３：検証情報生成ステップ（Ｓ３０４）＞  検証情報生成部１４が、テーブル生成ステップ（Ｓ３０３）において生成された確定ルールテーブル及び保持ルールテーブルに基づいて、第１アサーション９２及び第１テストパタン９３に含まれていない検証対象回路の非策定動作を検証するための検証情報である第２アサーション９４を生成する。例えば、図７の確定ルールテーブルから図８の第２アサーション９４（（Ｋ２）〜（Ｋ４））が生成され、図６の保持ルールテーブルから図９の第２アサーション９４（（Ｓ２）〜（Ｓ４））が生成される。図８のＫ２〜Ｋ４は、図７のＫ２〜Ｋ４に対応する。図９のＳ２〜Ｓ４は、図６のＳ２〜Ｓ４に対応する。
【００４５】
＜図３：出力ステップ（Ｓ３０５）＞  出力部１５が、検証情報生成ステップ（Ｓ３０４）において生成された第２アサーション９４を含む検証情報をチェッカ３０に供給する。
【００４６】
図３の論理検証処理は、出力ステップ（Ｓ３０５）の後に終了する。
【００４７】
第１実施形態によれば、策定動作に関する第１アサーション９２から非策定動作に関する第２アサーション９４が生成され、第２アサーション９４に基づいて第２論理検証結果９６が生成される。第２論理検証結果９６は、第１アサーション９２に含まれていない非策定動作の論理検証結果を含む。従って、論理検証結果の漏れを低減することができる。その結果、半導体装置の設計の時間的損失及び経済的損失を低減することができる。
【００４８】
また、第１実施形態によれば、ユーザが与えるべき情報は、第１アサーション９２のみを用いて第１論理検証結果９５を生成する場合と同様である。すなわち、ユーザは、従来と同様に、ＲＴＬ記述９１と、第１アサーション９２と、第１テストパタン９３と、を入力することにより、第１論理検証結果９５及び第２論理検証結果９６の両方を得ることができる。換言すると、論理検証装置１０は、既存のシミュレータ、エミュレータ、及びプロパティチェッカ等のいかなるチェッカ３０とも組み合わせて使用することができる。
【００４９】
（第２実施形態）
本発明の第２実施形態について説明する。第２実施形態は、策定動作に関する第１アサーションから、非策定動作に関する第２テストパタンを生成する論理検証装置の例である。なお、上述の実施形態と同様の内容についての説明は省略する。
【００５０】
第２実施形態に係る論理検証装置の構成について説明する。図１０は、本発明の第２実施形態に係る論理検証装置１０を含むシステムの構成を示すブロック図である。
【００５１】
図１０のシステムは、論理検証装置１０と、入力装置２０と、チェッカ３０と、出力装置４０と、を備える。入力装置２０及び出力装置４０は、第１実施形態と同様である。
【００５２】
図１０の論理検証装置１０は、入力装置２０により受け付けられた第１テストパタン９３に基づいて第２テストパタン９７を生成するように構成される。例えば、第２テストパタン９７は、検証対象回路の非策定動作を検証するためのテストパタンである。
【００５３】
第２実施形態に係る検証情報生成部１４は、テーブル生成部１３により生成されたルールテーブルに基づいて、第１アサーション９２及び第１テストパタン９３に含まれていない検証対象回路の非策定動作を検証するための第２アサーション９４と、第１テストパタン９３において信号が無効であるときの信号の値がランダムに定められている第２テストパタン９７と、を含む検証情報を生成するように構成される。
【００５４】
第２実施形態に係る出力部１５は、検証情報生成部１４により生成された第２アサーション９４及び第２テストパタン９７を含む検証情報をチェッカ３０に供給するように構成される。
【００５５】
図１０のチェッカ３０は、入力装置２０により受け付けられた第１アサーション９２及び第１テストパタン９３に基づいて、ＲＴＬ記述９１の策定動作の論理検証を行う。それにより、第１論理検証結果９５が生成される。また、チェッカ３０は、論理検証装置１０により生成された第２テストパタン９７及び第２アサーション９４に基づいて、ＲＴＬ記述９１の非策定動作の論理検証を行う。それにより、第２論理検証結果９６が生成される。例えば、チェッカ３０は、シミュレータ、エミュレータ、及びフォーマルチェッカ等の既存ツールである。
【００５６】
第２実施形態に係る論理検証装置のオペレーションについて説明する。第２実施形態に係る論理検証処理は、図３の第１実施形態に係る論理検証処理と同様の手順により行われる。図１１は、第２実施形態に係る検証情報生成ステップ（図３のＳ３０４）の手順を示すフローチャートである。図１２は、図１１のＳ１１０２において用いられる第１アサーション９２の一例を示す概略図である。図１３は、図１２の第１アサーション９２に対応する第２テストパタン９７の一例を示す概略図である。図１４の（Ａ）は第１テストパタン９３の信号波形を示す概略図である。図１４の（Ｂ）は第２テストパタン９７の信号波形を示す概略図である。
【００５７】
第２実施形態に係る検証情報生成ステップについて説明する。
【００５８】
＜図１１：Ｓ１１０１＞  検証情報生成部１４が、テーブル生成ステップ（Ｓ３０３）において生成された確定ルールテーブル（図７を参照）から、対象信号を表す記述と「有効条件」を表す記述のペアを抽出する。対象信号は、ハンドシェイク信号である。対象信号には、確定ルール及び保持ルールが適用される。例えば、対象信号を表す記述は“SrespLast”であり（図７の（Ｋ１）を参照）、「有効条件」を表す記述は“SResp!=0”である（図７を参照）。
【００５９】
＜図１１：Ｓ１１０２＞  検証情報生成部１４が、第１テストベンチ信号を算出する。より具体的には、検証情報生成部１４は、第１アサーション９２のバインド文から、第１アサーション９２において使用される信号とＲＴＬ記述９１のインスタンスとの対応関係を求める。次いで、検証情報生成部１４は、第１アサーション９２の接続文から、ＲＴＬ記述９１のインスタンスと第１テストパタン９３において使用されるテストベンチ信号との対応関係を求める。それにより、テストベンチ信号が算出される。テストベンチ信号は、フォース対象の信号及びサンプリング対象の信号を含む（図１２を参照）。図１２では、フォース対象の信号は“SRespLast”であり、サンプリング対象の信号は“SResp”である。
【００６０】
＜図１１：Ｓ１１０３＞  検証情報生成部１４が、各対象信号について、「無効条件」下において、フォース対象の信号の値をランダム値でフォースするためのランダムコードを生成する（図１３を参照）。
【００６１】
第２実施形態に係る検証情報生成ステップは、Ｓ１１０３の後に終了する。結果として、テーブル生成ステップ（Ｓ３０３）において生成された確定ルールテーブル及び保持ルールテーブルに基づいて、第１アサーション９２及び第１テストパタン９３に含まれていない検証対象回路の非策定動作を検証するための検証情報である第２アサーション９４が生成され、テストパタン生成ステップ（Ｓ３０４）において生成されたランダムコードに対応する第２テストパタン９７が生成される。
【００６２】
従来の論理検証では、図１４の（Ａ）に示すように、第１テストパタン９３の所定の領域（図１４の（Ａ）の破線Ａ）に不活性値が現れる。従って、図１４の（Ａ）の破線Ａにより示される領域（すなわち、テストパタンに不活性値が現れる領域）については、論理検証結果を得ることはできない。
【００６３】
一方、第２実施形態では、図１４の（Ｂ）に示すように、第２テストパタン９７の所定の領域（図１４の（Ｂ）の破線Ｂ）にランダム値が現れる。その所定の領域（破線Ｂ）は、第１テストパタン９３において不活性値が現れる領域である。従って、図１４の（Ｂ）の破線Ｂにより示される領域（すなわち、テストパタンに不活性値が現れる領域）についても、論理検証結果（すなわち、第２論理検証結果９６）を得ることができる。
【００６４】
第２実施形態によれば、テストパタンに不活性値が現れる領域についてランダムコードが生成され、そのランダムコードに基づいて第２テストパタン９７が生成される。従って、従来技術により得ることのできない不活性値が現れる領域についての論理検証結果を得ることができる。すなわち、論理検証結果の漏れを低減することができる。それにより、半導体装置の設計の時間的損失及び経済的損失を低減することができる。
【００６５】
なお、第２実施形態では、第２アサーション９４の生成を省略しても良い。この場合には、第１アサーション９２及び第２テストパタン９７に基づいて、テストパタンに不活性値が現れる領域についての第２論理検証結果９６が得られる。
【００６６】
本発明の実施形態に係る論理検証装置１０の少なくとも一部は、ハードウェアで構成しても良いし、ソフトウェアで構成しても良い。ソフトウェアで構成する場合には、論理検証装置１０の少なくとも一部の機能を実現するプログラムをフレキシブルディスクやＣＤ−ＲＯＭ等の記録媒体に収納し、コンピュータに読み込ませて実行させても良い。記録媒体は、磁気ディスクや光ディスク等の着脱可能なものに限定されず、ハードディスク装置やメモリなどの固定型の記録媒体でも良い。
【００６７】
また、本発明の実施形態に係る論理検証装置１０の少なくとも一部の機能を実現するプログラムを、インターネット等の通信回線（無線通信も含む）を介して頒布しても良い。さらに、同プログラムを暗号化したり、変調をかけたり、圧縮した状態で、インターネット等の有線回線や無線回線を介して、あるいは記録媒体に収納して頒布しても良い。
【００６８】
なお、本発明は、上述した実施形態に限定されるものではなく、その要旨を逸脱しない範囲で構成要素を変形して具体化される。また、上述した実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明が形成可能である。例えば、上述した実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。
【符号の説明】
【００６９】
１０  論理検証装置
１１  入力部
１２  抽出部
１３  テーブル生成部
１４  検証情報生成部
１５  出力部
２０  入力装置
３０  チェッカ
４０  出力装置
９１  ＲＴＬ記述
９２  第１アサーション
９３  第１テストパタン
９４  第２アサーション
９５  第１論理検証結果
９６  第２論理検証結果
９７  第２テストパタン
【図１】
2011186817.tif 000003
【図２】
2011186817.tif 000004
【図３】
2011186817.tif 000005
【図４】
2011186817.tif 000006
【図５】
2011186817.tif 000007
【図６】
2011186817.tif 000008
【図７】
2011186817.tif 000009
【図８】
2011186817.tif 000010
【図９】
2011186817.tif 000011
【図１０】
2011186817.tif 000012
【図１１】
2011186817.tif 000013
【図１２】
2011186817.tif 000014
【図１３】
2011186817.tif 000015
【図１４】
2011186817.tif 000016