(57)【要約】【課題】アサーション記述が不完全な場合であっても、設計者の負担を軽減する。【解決手段】論理回路設計検証装置は、回路記述及びアサーション記述を入力する入力部１４と、入力部１４によって入力された回路記述から信号名を抽出する抽出部と、抽出部によって抽出された信号名のうち、入力部１４によって入力されたアサーション記述の前提条件及び検証要件に含まれていない信号名を検出する漏れ検出部と、漏れ検出部によって検出された信号名を出力する出力部１６と、を備えている。【選択図】図１
2010113395.tif 000002
【特許請求の範囲】
【請求項１】
回路記述及びアサーション記述を入力する入力部と、
前記入力部によって入力された回路記述から信号名を抽出する抽出部と、
前記抽出部によって抽出された信号名のうち、前記入力部によって入力されたアサーション記述の前提条件及び検証要件に含まれていない信号名を検出する漏れ検出部と、
前記漏れ検出部によって検出された信号名を出力する出力部と、を備えることを特徴とする論理回路設計検証装置。
【請求項２】
前記漏れ検出部は、前記入力部によって入力されたアサーション記述に並列条件が含まれている場合には、前記入力部によって入力されたアサーション記述の前提条件及び検証要件に前記並列条件の数だけ含まれていない信号名を検出する請求項１に記載の論理回路設計検証装置。
【請求項３】
前記抽出部は、さらに、前記入力部によって入力された回路記述から中間変数を抽出し、
前記漏れ検出部は、さらに、前記抽出部によって抽出された中間変数のうち、前記入力部によって入力されたアサーション記述の前提条件及び検証要件に含まれる信号名に関連する中間変数の到達度を算出し、
前記出力部は、さらに、前記漏れ検出部によって算出された到達度を出力する請求項１又は２に記載の論理回路設計検証装置。
【請求項４】
前記漏れ検出部は、前記中間変数のビット数の総和に対する前記入力部によって入力されたアサーション記述の前提条件及び検証要件に含まれる中間変数の数の割合を前記到達度の単位値とする請求項３に記載の論理回路設計検証装置。
【請求項５】
前記出力部は、前記漏れ検出部によって算出された到達度が所定の基準値に満たない場合に警告を出力する請求項３又は４に記載の論理回路設計検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理回路設計検証装置に関し、特に、半導体装置の論理回路設計検証の上流工程においてアサーションベース検証を行うときに使用される論理回路設計検証装置に関する。
【背景技術】
【０００２】
半導体装置の論理回路設計検証の上流工程において行われる検証手法として、実現したい仕様に対して論理回路を記述した回路記述と、論理回路とは別に前提条件及び検証要件を記述したアサーション記述と、を比較し、両者が一致しているか否かについて検証するアサーションベース検証が知られている。
【０００３】
アサーションベース検証を実現する技術として、回路記述と仕様記述とを比較し、両者が一致しているか否かを検証し、アサーション記述に含まれる各アサーションについて、回路記述の信号名と一致する信号名の割合を表示する技術が知られている（特許文献１を参照）。
【０００４】
従来、設計者は、このような技術を用いて、アサーション記述と回路記述との間で一致しない信号名を特定し、全てのアサーションについて回路記述の信号名とアサーションの信号名とが一致するまで回路記述を修正して、アサーションベース検証を終了していた。
【０００５】
しかしながら、特許文献１に開示された技術は、アサーション記述が完全であることを前提として行われるので、ヒューマンエラーなどによってアサーション記述が不完全となる場合（例えば、設計者が、一部の信号名を記述し忘れてアサーション記述を作成してしまった場合）には、正確なアサーションベース検証を行うことはできない。その結果、回路記述が完全であったとしても、設計者は、回路記述が不完全であることを前提に作業を行うので、アサーションベース検証以降の工程において手戻りをしなければならず、設計者の負担が増加してしまう。
【０００６】
即ち、従来の技術では、アサーション記述が不完全な場合には、設計者の負担が増加するという問題があった。
【特許文献１】特開２００７−９４８９１号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
本発明の目的は、アサーション記述が不完全な場合であっても、設計者の負担を軽減する論理回路設計検証装置を提供することである。
【課題を解決するための手段】
【０００８】
本発明の態様によれば、回路記述及びアサーション記述を入力する入力部と、前記入力部によって入力された回路記述から信号名を抽出する抽出部と、前記抽出部によって抽出された信号名のうち、前記入力部によって入力されたアサーション記述の前提条件及び検証要件に含まれていない信号名を検出する漏れ検出部と、前記漏れ検出部によって検出された信号名を出力する出力部と、を備えることを特徴とする論理回路設計検証装置が提供される。
【発明の効果】
【０００９】
本発明によれば、アサーション記述が不完全な場合であっても、設計者の負担を軽減することができる。
【発明を実施するための最良の形態】
【００１０】
以下、本発明の実施形態について図面を参照して説明する。なお、以下の実施形態は、本発明の実施の一態様であって、本発明の範囲を限定するものではない。
【００１１】
（第１実施形態）
まず、本発明の第１実施形態について説明する。本発明の第１実施形態は、アサーション記述から漏れている信号名を出力する論理回路設計検証装置の例である。
【００１２】
本発明の第１実施形態に係る論理回路設計検証装置の構成について、図１及び図２を参照して説明する。図１は、本発明の第１実施形態に係る論理回路設計検証装置の構成を示すブロック図である。図２は、図１に示すプロセッサ１０の機能構成を示す機能ブロック図である。
【００１３】
図１に示すように、論理回路設計検証装置は、様々な処理を実行するプロセッサ１０と、様々なデータを記憶するメモリ１２と、所定の命令の入力を受け付ける入力部１４（例えば、キーボード）と、所定の情報を出力する出力部１６（例えば、ディスプレイ）と、を備えている。
【００１４】
図１に示すように、プロセッサ１０は、メモリ１２、入力部１４、及び出力部１６に接続されている。また、プロセッサ１０は、メモリ１２に記憶された論理回路設計検証プログラム１２ａを起動することによって、図２に示すように、抽出部１０２及び漏れ検出部１０４として動作する。
【００１５】
本発明の第１実施形態に係る論理回路設計検証装置の処理について、図３乃至図６を参照して説明する。図３は、本発明の第１実施形態に係る論理回路設計検証処理の処理手順を示すフローチャートである。図４は、本発明の第１実施形態に係るレジスタ情報の概略を示す概略図である。図５は、図３に示す漏れ検出処理（Ｓ３０３）の処理手順を示すフローチャートである。図６は、図３に示す漏れ検出処理（Ｓ３０３）の処理結果を示す概略図である。
【００１６】
本発明の第１実施形態に係る論理回路設計検証処理では、図３に示すように、入力工程（Ｓ３０１）が行われる。入力工程（Ｓ３０１）では、入力部１４が、信号名及びクロック・リセット情報を含む回路記述（例えば、ＲＴＬ（Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌ）記述）と、ＳＶＡ（Ｓｙｓｔｅｍ  Ｖｅｒｉｌｏｇ  Ａｓｓｅｒｔｉｏｎ）に従って記述された前提条件及び検証要件を含むアサーション記述（式１．１乃至式１．３）と、を入力する。ここで、回路記述及びアサーション記述の入力は、ユーザによって行われる。
【００１７】
〔式１．１〕  REQ && ACK |=> DOUT ==0;
〔式１．２〕  
REQ && ACK && (DIN==0 || DIN==1)
|=>
##9 (DOUT == $past(DIN) + $past(DIN,2) || (DOUT == $past(DIN));
〔式１．３〕  
DOUT[0] || DOUT[1] || DOUT[2] || DOUT[3] || DOUT[4] || DOUT[5] || DOUT[6] || DOUT[7] |-> $past(ACK, 3);
次に、図３に示すように、抽出工程（Ｓ３０２）が行われる。抽出工程（Ｓ３０２）では、抽出部１０２が、入力工程（Ｓ３０１）において入力された回路記述からレジスタの信号名及び種別を抽出して、レジスタ情報（図４）を作成する。
【００１８】
次に、図３に示すように、漏れ検出処理（Ｓ３０３）が行われる。
【００１９】
漏れ検出処理（Ｓ３０３）では、図５に示すように、漏れ検出部１０４が、抽出工程（Ｓ３０２）において抽出された信号名と入力工程（Ｓ３０１）において入力されたアサーション記述とを比較する（Ｓ５０１）。
【００２０】
次に、図５に示すように、並列条件（ＯＲ）を含んでいないアサーション記述（式１．１）が比較対象となる場合には（Ｓ５０２−ＮＯ）、抽出工程（Ｓ３０２）において作成されたレジスタ情報（図４）に対して、アサーション記述（式１．１）の前提条件及び検証要件に含まれていない信号名にフラグをセットする（Ｓ５０３）。
【００２１】
一方、図５に示すように、並列条件（ＯＲ）を含んでいるアサーション記述（式１．２及び式１．３）が比較対象となる場合には（Ｓ５０２−ＹＥＳ）、抽出工程（Ｓ３０２）において作成されたレジスタ情報（図４）に対して、アサーション記述（式１．２及び式１．３）の前提条件及び検証要件に並列条件（ＯＲ）の数だけ含まれていない信号名にフラグをセットする（Ｓ５０４）。
【００２２】
ここで、図６は、入力信号ＤＩＮ及び出力信号ＤＯＵＴがアサーション記述の前提条件から漏れており、出力信号ＡＣＫがアサーション記述の検証要件から漏れており、入力信号ＣＬＫ，ＲＳＴ＿Ｘがアサーション記述の前提条件及び検証要件の比較対象から除外されており、入力信号ＲＥＱ，ＤＩＮがアサーション記述の検証要件の比較対象から除外されていることを示している。
【００２３】
図５に示すように、図３に示す漏れ検出処理（Ｓ３０３）は、Ｓ５０３又はＳ５０４の後に終了する。
【００２４】
次に、図３に示すように、出力工程（Ｓ３０４）が行われる。出力工程（Ｓ３０４）では、出力部１６が、漏れ検出処理（Ｓ３０３）において検出された信号名（即ち、レジスタ情報（図６）のうち、フラグがセットされている信号名である入力信号ＤＩＮ及び出力信号ＡＣＫ，ＤＯＵＴ）を出力する。
【００２５】
図３に示すように、本発明の第１実施形態に係る論理回路設計検証処理は、出力工程（Ｓ３０４）の後に終了する。
【００２６】
なお、本発明の第１実施形態では、入力信号ＣＬＫ，ＲＳＴ＿Ｘ，ＲＥＱ，ＤＩＮは、アサーション記述の検証要件に出現する可能性が低いために比較対象から除外されているが、比較対象としても良い。
【００２７】
本発明の第１実施形態によれば、アサーション記述が不完全な場合に、アサーション記述から漏れている信号名が出力される。その結果、設計者がアサーション記述から漏れている信号名を容易に把握することができるので、設計者の負担が軽減される。
【００２８】
（第２実施形態）
本発明の第２実施形態について説明する。本発明の第１実施形態は、アサーション記述から漏れている信号名を出力する論理回路設計検証装置の例であったが、本発明の第２実施形態は、回路記述に対するアサーション記述の到達度を出力する論理回路設計検証装置の例である。なお、本発明の第２実施形態に係る論理回路検証装置の構成は、本発明の第１実施形態に係る論理回路検証装置と同様である。
【００２９】
本発明の第２実施形態に係る論理回路検証装置の処理について、図７乃至図１１を参照して説明する。図７は、本発明の第２実施形態に係る論理回路設計検証処理の処理手順を示すフローチャートである。図８は、図７に示す中間変数抽出処理（Ｓ７０３）の処理手順を示すフローチャートである。図９は、本発明の第２実施形態に係るレジスタ接続情報の概略を示す概略図である。図１０は、図７に示す到達度算出処理（Ｓ７０５）の処理手順を示すフローチャートである。図１１は、本発明の第２実施形態に係るレジスタ情報の概略を示す概略図である。
【００３０】
本発明の第２実施形態に係る論理回路設計検証処理では、図７に示すように、入力工程（Ｓ７０１）が行われる。入力工程（Ｓ７０１）では、入力部１４が、信号名及びクロック・リセット情報を含む回路記述（例えば、ＲＴＬ記述）と、ＳＶＡに従って記述された前提条件及び検証要件を含むアサーション記述（式２．１）と、を入力する。ここで、回路記述及びアサーション記述の入力は、ユーザによって行われる。
【００３１】
〔式２．１〕  REQ && ACK |=> DOUT == 7’h00;
〔式２．２〕  REQ |-> ##[0:10] ACK;
次に、図７に示すように、抽出工程（Ｓ７０２）が行われる。抽出工程（Ｓ７０２）では、抽出工程（Ｓ３０２）では、抽出部１０２が、入力工程（Ｓ７０１）において入力された回路記述からレジスタの信号名及び種別を抽出して、レジスタ情報（図４）を作成する。
【００３２】
次に、図７に示すように、中間変数抽出処理（Ｓ７０３）が行われる。
【００３３】
中間変数抽出処理（Ｓ７０３）では、図８に示すように、抽出部１０２が、入力工程（Ｓ７０１）において入力された回路記述からレジスタの接続関係を特定する（Ｓ８０１）。
【００３４】
次に、図８に示すように、特定されたレジスタの接続関係に対して、アサーション記述（式２．１）に含まれている信号名を特定する（Ｓ８０２）。
【００３５】
次に、図８に示すように、特定された信号名に関連する中間変数を抽出して、レジスタ接続情報（図９）を作成する（Ｓ８０３）。ここで、図９は、レジスタ情報（図４）及びアサーション記述（式２．１）から、入力信号ＲＥＱ及び出力信号ＡＣＫ，ＤＯＵＴが、アサーション記述（式２．１）に含まれている信号名として特定され、特定された信号名に挟まれた変数ｓｔａｔｅ，ｃｎｔが、関連する中間変数として抽出されたことを示している。
【００３６】
図８に示すように、図７に示す中間変数抽出処理（Ｓ７０３）は、Ｓ８０３の後に終了する。
【００３７】
次に、図７に示すように、漏れ検出処理（Ｓ７０４）が行われる。
【００３８】
漏れ検出処理（Ｓ７０４）では、図１０に示すように、漏れ検出部１０４が、入力工程（Ｓ７０１）において入力されたクロック・リセット情報に基づいて、到達度の単位値を算出する（Ｓ１００１）。ここで、漏れ検出部１０４は、“１／（並列条件（ＯＲ）の数）”を入力信号及び出力信号の単位値とし、“１／（中間変数のビット数の総和）”を中間変数の単位値とする。
【００３９】
次に、図１０に示すように、漏れ検出部１０４が、抽出工程（Ｓ７０２）において抽出された信号名と入力工程（Ｓ７０１）において入力されたアサーション記述とを比較する（Ｓ１００２）。
【００４０】
次に、図１０に示すように、漏れ検出部１０４が、抽出工程（Ｓ７０２）において作成されたレジスタ情報（図４）に対して、アサーション記述の前提条件又は検証要件に含まれている信号名の到達度に単位値を加算する（Ｓ１００３）。ここで、Ｓ１００３は、アサーション記述毎に行われ、到達度が１に達した信号名に対しては省略される。
【００４１】
次に、図１０に示すように、漏れ検出部１０４が、アサーション記述の前提条件又は検証要件に含まれている信号名に関連する中間変数の到達度に単位値を加算する（Ｓ１００４）。ここで、Ｓ１００４は、アサーション記述毎に行われ、到達度が１に達した中間変数に対しては省略される。
【００４２】
図１０に示すように、Ｓ１００１乃至Ｓ１００４は、全てのアサーション記述について完了するまで繰り返され（Ｓ１００５−ＮＯ）、図７に示す漏れ検出処理（Ｓ７０４）は、全てのアサーション記述について完了した後に終了する（Ｓ１００５−ＹＥＳ）。
【００４３】
ここで、図１１は、入力信号ＲＥＱ及び出力信号ＡＣＫがアサーション記述の前提条件に含まれており、出力信号ＤＯＵＴがアサーション記述の検出要件に含まれており、中間変数ｓｔａｔｅ，ｃｎｔの到達度が０．０８３３３であることを示している。
【００４４】
次に、図７に示すように、出力工程（Ｓ７０５）が行われる。出力工程（Ｓ７０５）では、出力部１６が、漏れ検出処理（Ｓ７０４）において検出された信号名（即ち、レジスタ情報（図１１）のうち、到達度が０の信号名である入力信号ＤＩＮ及び出力信号ＡＣＫ，ＤＯＵＴ）、並びに中間変数ｄｉｎ＿ｐａｓｔを出力する。ここで、出力部１６は、到達度が所定の基準値に満たない信号名又は中間変数が存在する場合には、警告を出力する。
【００４５】
図７に示すように、本発明の第２実施形態に係る論理回路設計検証処理は、出力工程（Ｓ７０５）の後に終了する。
【００４６】
なお、本発明の第２実施形態は、本発明の第１実施形態と組み合わせて実施されても良い。
【００４７】
また、本発明の第２実施形態では、漏れ検出部１０４は、 “１／（中間変数のビット数の総和）”に代えて、“１／（中間変数の始点と終点とを結ぶ経路の数）”を中間変数の単位値としても良い。この場合には、漏れ検出部１０４は、経路上に存在する信号名に関連するレジスタの到達度に単位値を加算する。
【００４８】
本発明の第２実施形態によれば、アサーション記述が不完全な場合に、アサーション記述から漏れている信号名だけでなく、アサーション記述の到達度が出力される。その結果、設計者は、アサーション記述の完成度を把握することができるので、作業効率が向上する。
【００４９】
また、本発明の第２実施形態によれば、到達度の単位値がアサーション記述あたり１未満の値である。その結果、アサーション記述に関連するレジスタの数が多い場合であっても、より正確な到達度の数値が得られる。
【００５０】
また、本発明の第２実施形態によれば、到達度が基準値に満たない場合に警告が行われる。その結果、設計者は、アサーション記述の不備を容易に把握することができる。
【図面の簡単な説明】
【００５１】
【図１】本発明の第１実施形態に係る論理回路設計検証装置の構成を示すブロック図である。
【図２】図１に示すプロセッサ１０の機能構成を示す機能ブロック図である。
【図３】本発明の第１実施形態に係る論理回路設計検証処理の処理手順を示すフローチャートである。
【図４】本発明の第１実施形態に係るレジスタ情報の概略を示す概略図である。
【図５】図３に示す漏れ検出処理（Ｓ３０３）の処理手順を示すフローチャートである。
【図６】図３に示す漏れ検出処理（Ｓ３０３）の処理結果を示す概略図である。
【図７】本発明の第２実施形態に係る論理回路設計検証処理の処理手順を示すフローチャートである。
【図８】図７に示す中間変数抽出処理（Ｓ７０３）の処理手順を示すフローチャートである。
【図９】本発明の第２実施形態に係るレジスタ接続情報の概略を示す概略図である。
【図１０】図７に示す到達度算出処理（Ｓ７０５）の処理手順を示すフローチャートである。
【図１１】本発明の第２実施形態に係るレジスタ情報の概略を示す概略図である。
【符号の説明】
【００５２】
１０  プロセッサ
１０２  抽出部
１０４  漏れ検出部
１２  メモリ
１２ａ  論理回路設計検証プログラム
１４  入力部
１６  出力部
【図１】
2010113395.tif 000003
【図２】
2010113395.tif 000004
【図３】
2010113395.tif 000005
【図４】
2010113395.tif 000006
【図５】
2010113395.tif 000007
【図６】
2010113395.tif 000008
【図７】
2010113395.tif 000009
【図８】
2010113395.tif 000010
【図９】
2010113395.tif 000011
【図１０】
2010113395.tif 000012
【図１１】
2010113395.tif 000013