(57)【特許請求の範囲】
【請求項１】
検証基準回路を利用して新規な論理回路を設計し該回路を検証対象回路とする場合におけるチェッカーとしてのアサーションを生成するアサーション自動生成装置において、
検証対象回路と前記検証基準回路それぞれにおける信号名の情報である信号情報を格納した信号情報ファイルと、
前記検証基準回路の動作パタンの内で前記検証対象回路の評価パタンに現れる信号のレベル遷移を示す情報である動作波形データを格納した波形データファイルと、
前記信号情報ファイルと前記波形データファイルとから検証対象信号とこれに対応する検証基準信号それぞれに対する信号変化情報を生成する信号変化情報自動生成部と、
前記信号変化情報を入力し、論理回路の機能仕様や設計意図を表現した記述であるアサーションを生成するアサーション生成部を有することを特徴とするアサーション自動生成装置。
【請求項２】
前記信号変化情報は、当該信号ｎの値が遷移した時刻を前記動作波形データから取り出すための第１関数Ｔn(t)の所定時間における値と、当該信号ｎの遷移時における値を前記動作波形データから取り出すための第２関数Ｎ(t)の所定時間における値とから成り、
前記アサーション生成部は、前記検証基準信号ａの前記第２関数の値Ｎa(t)と、前記検証基準信号ａ対応の検証対象信号ｂに対する前記第２関数の値Ｎb(t)と、検証基準信号ａと前記検証対象信号ｂそれぞれの前記第１関数値の相対的な差から求められる変化時間情報としての第３関数の値Ｑab(t)を変数としアサーション記述に変換するための関数Ｈにより、前記アサーションを生成することを特徴とする請求項１記載のアサーション自動生成装置。
【請求項３】
検証基準回路を利用して新規な論理回路を設計し該回路を検証対象回路とする場合におけるチェッカーとしてのアサーションを生成するアサーション自動生成方法であって、
前記検証対象回路のユーザロジック仕様における検証対象信号名と、これに対応する前記検証基準回路における検証基準信号名の情報である信号情報を検証者が用意する段階と、
ユーザロジック仕様に基づいて作成したテストパタンである評価パタンを作成する段階と、
前記検証基準回路の動作パタンを実行して、前記評価パタンおよび前記検証基準回路の回路記述に基づき、前記動作パタンの内で前記評価パタンに現れる信号のレベル遷移を示す情報である動作波形データを生成する段階と、
前記信号情報と前記動作波形データとによりアサーションを自動的に生成する段階を有することを特徴とするアサーション自動生成方法。
【請求項４】
請求項３記載のアサーション自動生成方法により生成したアサーションを用いた論理回路設計検証方法であって、
前記ユーザロジック仕様と前記検証基準回路の概要仕様に基づいて新規の仕様を把握し、これをベースに前記回路記述および生成された前記アサーションから回路変更があるか否かを判断する段階と、
回路変更があれば前記検証基準回路を変更する段階と、
前記検証基準回路をベースに前記評価パタンと前記生成されたアサーションを用いて前記検証対象回路を検証する段階と、
検証の結果がＯＫでなければ前記仕様の把握に戻って、変更後の検証基準回路を作成して検証をし直す段階を有することを特徴とする論理回路設計検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、アサーション自動生成およびアサーションをチェッカーとして組み込んだ論理回路設計検証に関する。アサーションとは、論理回路の機能仕様や設計意図を表現した記述をいう。
【背景技術】
【０００２】
論理回路の設計を検証する手段の一つとしてアサーションをチェッカーとして組み込むアサーション・ベース検証が知られている。アサーション・ベース検証では、汎用性のある回路のIP（Intellectual  Property）ないしは既存回路を利用して新規な論理回路を設計する場合、アサーションをチェッカーとして組み込むことにより、検証結果からユーザの論理回路に対する設定ミスかIP等自体の不具合かを判定することができる。
【０００３】
アサーションを作成するためには、検証対象となる回路の詳細な仕様を回路仕様書や回路記述から把握できる要素が必要であり、かつアサーション作成者および回路検証者は、検証対象となる回路の仕様を把握する必要がある。図４の模式図で示すように、原型となる基準回路Ａに機能の追加・削除など変更をかけて生成した変更回路Ａ’を検証する場合、基準回路Ａの仕様を把握し変更前のアサーションＢと異なる新規アサーションＣを作成する。
【０００４】
この場合の人為的なミスを無くすために、アサーションを自動生成できる仕組みを持つアサーション生成方法が提案されている（例えば、特許文献１参照）。この特許文献における「プロパティ」は、ここでのアサーションに相当し、プロパティの自動生成フローは図５に示すとおりである。
【０００５】
図５の自動生成装置301の入力要素は、検証対象であるプロセッサの回路仕様302とプロセッサの回路記述305である。回路仕様302は仕様解析部303で解析されて必要な情報が生成され、この情報から動作モデル生成部304によって動作モデルが生成される。一方、回路記述305は回路記述読込み部306に入力し、記述解析部307で解析される。そして、回路仕様302から得られた動作モデルと回路記述305から得られた記述解析結果がプロパティ生成部308に入力しプロパティ309が生成される。
【０００６】
【特許文献１】特開2000-268074（第６頁−第７頁、図３３）
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、上述した特許文献１記載の従来技術では、アサーションを作成するためには詳細仕様や回路記述を解析しなくてはならないから、IPのように回路記述が提供されない場合や、詳細仕様を解析できない回路に対して、アサーションを生成する事が非常に困難であるという第１の問題点がある。
【０００８】
また、仕様の解釈を間違えると、回路が正しいか判断する基準となるアサーション・チェッカーの間違いにつながるため、仕様の把握、回路記述の解析まで作業を戻して再びアサーションを生成し直さなければならず、検証実施までに多くの時間が必要となるという第２の問題点がある。
【０００９】
そこで、本発明の目的は、IPのように詳細仕様が解析できなく、また回路記述を参照不可能な回路であってもアサーションを自動生成することができるアサーション自動生成装置およびアサーション自動生成方法を提供することにある。
【００１０】
本発明の他の目的は、検証結果から正しいと判断されなかった場合であっても、検証工程の後戻りが少ない論理回路設計検証方法を提供することにある。
【課題を解決するための手段】
【００１１】
本発明のアサーション自動生成装置は、検証基準回路を利用して新規な論理回路を設計し該回路を検証対象回路とする場合におけるチェッカーとしてのアサーションを生成するアサーション自動生成装置において、検証対象回路と検証基準回路それぞれにおける信号名の情報である信号情報（図１における101）を格納した信号情報ファイルと、検証基準回路の動作パタンの内で検証対象回路の評価パタンに現れる信号のレベル遷移を示す情報である動作波形データ（図１における102）を格納した波形データファイルと、信号情報ファイルと波形データファイルとから検証対象信号とこれに対応する検証基準信号それぞれに対する信号変化情報（図１における104，105）を生成する信号変化情報自動生成部（図１における103）と、信号変化情報を入力し、論理回路の機能仕様や設計意図を表現した記述であるアサーション（図１における107）を生成するアサーション生成部（図１における106）を有することを特徴とする。
【００１２】
なお、信号変化情報は、当該信号ｎの値が遷移した時刻を動作波形データから取り出すための第１関数Ｔn(t)の所定時間における値と、当該信号ｎの遷移時における値を動作波形データから取り出すための第２関数Ｎ(t)の所定時間における値とから成り、アサーション生成部は、検証基準信号ａの第２関数の値Ｎa(t)と、検証基準信号ａ対応の検証対象信号ｂに対する第２関数の値Ｎb(t)と、検証基準信号ａと検証対象信号ｂそれぞれの第１関数値の相対的な差から求められる変化時間情報としての第３関数の値Ｑab(t)を変数としアサーション記述に変換するための関数Ｈにより、アサーションを生成することを特徴とする。
【００１３】
また、本発明のアサーション自動生成方法は、上記のアサーション自動生成装置を用いた検証基準回路に基づく論理回路設計検証方法において、検証対象回路のユーザロジック仕様（図２の201）における検証対象信号名と、これに対応する検証基準回路（図２の202）における検証基準信号名の情報である信号情報（図２の101）を検証者が用意する段階と、ユーザロジック仕様に基づいて作成したテストパタンである評価パタン（図２の206）を作成する段階と、動作パタン（図２の203）を実行して（図２のステップS1）評価パタンおよび検証基準回路の回路記述（図２の204）に基づいて、動作パタンの内で評価パタンに現れる信号のレベル遷移を示す情報である動作波形データ（図２の102）を生成する段階と、信号情報と動作波形データとによりアサーションを自動的に生成する（図２のステップS2）段階を有することを特徴とする。
【００１４】
また、本発明の論理回路設計検証方法は、アサーション自動生成方法により生成したアサーションを用いた論理回路設計検証方法であって、ユーザロジック仕様と検証基準回路の概要仕様（図２の205）に基づいて新規の仕様を把握し（図２のステップS3）、これをベースに回路記述および生成されたアサーションから回路変更があるか否かを判断する（図２のステップS4）段階と、回路変更があれば検証基準回路を変更する段階と、検証基準回路をベースに評価パタンと生成されたアサーションを用いて検証対象回路を検証する（図２のステップS5）段階と、検証の結果がＯＫでなければ（図２のステップS６）仕様の把握に戻って、変更後の検証基準回路を作成して検証をし直す段階を有することを特徴とする。
【発明の効果】
【００１５】
本発明の第１の効果は、回路の動作波形データと検証対象信号を明確にすることが可能であれば、IPなど回路の詳細仕様や回路記述の解析が行うことができない検証対象回路に対してもアサーション・ベース検証を行うことが可能なことである。その理由は、アサーション自動生成への入力要素に回路詳細仕様解析結果と、回路記述を必要としないためである。
【００１６】
本発明の第２の効果は、検証結果が正しくないと判断された場合、検証の後戻りが従来技術にくらべ少なく、IPや既存回路の一部に変更を加え再利用する場合などに、原型となる回路から自動生成したアサーションをチェッカーとして変更後の回路に組み込むことで、意図しない変更など、回路の差異をより早く発見することができることである。その理由は、検証結果判定において正しくないと判定されると、検証者は仕様の把握に戻り、検証対象回路に限った見直しとなるため検証の後戻りが少なく従来技術に比べ、再検証までの時間が短縮されるからである。
【発明を実施するための最良の形態】
【００１７】
本発明の特徴は、検証対象信号名と検証基準信号名の情報を持つ信号情報と、検証基準となる回路の動作波形データを入力とし、信号情報で指定された信号に対し、検証基準信号変化情報と検証対象信号変化情報を生成する信号変化情報自動生成部と、生成した検証基準信号変化情報および検証対象信号変化情報を入力とし、アサーションを自動生成するアサーション自動生成プログラムを有するアサーション自動生成することにある。以下、本発明の実施の形態について図面を参照して詳細に説明する。
【００１８】
図２は、本発明の論理回路設計検証方法を示すフローチャートである。この論理回路設計検証方法は、IP202を利用して新規な論理回路のユーザロジック仕様201を検証するものである。IP202は動作パタン203，回路記述204および概要仕様205から成る。IP202は検証基準回路、ユーザロジック仕様201は検証対象回路として機能する。
【００１９】
先ず、検証者は、ユーザロジック仕様201における検証対象信号名と、これに対応するIP202における検証基準信号名の情報である信号情報101を用意する。また、ユーザロジック仕様201に基づいて作成したテストパタンである評価パタンを作成する。ユーザロジック仕様201，IP202および信号情報101はファイルとして本論理回路設計検証方法を実行するためのコンピュータに接続される。
【００２０】
本論理回路設計検証方法を実行するプログラムが起動されると、動作パタン203が実行され（図２のステップS1）、評価パタン206および回路記述204に基づいて動作波形データ（以下、「波形データ」と記す）102が生成される。波形データ102とは、動作パタン203の内で評価パタン206に現れる信号のレベル遷移を示す情報である。
【００２１】
次いで、信号情報101と波形データ102とによりアサーションが自動的に生成される（図２のステップS2）。図１はアサーションの自動生成を説明するための図である。信号変化情報自動生成部103は信号情報101で指定された検証基準信号，検証対象信号に対して、波形データ102から検証基準信号変化情報104，検証対象信号変化情報105を抽出する。アサーション生成部106は検証基準信号変化情報104と検証対象信号変化情報105を比較し、アサーション107を生成する。
【００２２】
次いで、ユーザロジック仕様201と概要仕様205に基づいて新規の仕様が把握され（図２のステップS3）、これをベースに回路記述204および生成されたアサーション107から回路変更があるか否かが判断される。回路変更があればIP202を変更した変更後IP207が作成される（以上、図２のステップS4）。
【００２３】
最後に、変更後IP207またはIP208（IP202と同じ）をベースに評価パタン206とアサーション107を用いて検証対象回路を検証する（図２のステップS5）。検証の結果がＯＫであれば本論理回路設計検証は終了する。検証の結果がＯＫでなければ（以上、図２のステップS6）、検証者はIP自体のバグか、回路変更ミスか、評価パタンミスかを確認する（検証結果フィードバック工程）。そして、その後に仕様の把握（図２のステップS3）に戻って、変更後IP207を作成して検証（図２のステップS5）をし直す。
【００２４】
ここで、検証結果のフィードバックはアサーションの自動生成後の工程である仕様の把握にかかることに留意されたい。この結果、検証の結果がＯＫでなくてもアサーションを作成し直す必要はないのである。
【００２５】
図６は、図５に示した従来のプロパティ自動生成方法を用いた回路検証において、検証結果がＯＫとならず、検証結果をフィードバックする場合を想定した場合の回路設計検証のフローチャートである。図６では、アサーション作成（図６のステップT3）が仕様の把握（図６のステップT2）の後にされていることから、後戻り工程において再びアサーションを生成し直さなければならず、検証実施までに多くの時間が必要となるのである。
【００２６】
次に、波形データ102の具体例によりアサーション107の作成方法を説明する。いま、信号情報101に指定された検証基準信号ａと検証対象信号ｂが図３に示すとおりであるとする。図３を参照すると、時刻ｔ＝0〜tendの間に、検証基準信号ａは３回変化し、検証対象信号ｂは、１つ目の検証基準信号ａの立上り時からk1後、２つ目の検証基準信号ａの立上り時からk2後、３つ目の検証基準信号ａの立上り時からk3前に立ち上がっており、k3<k1<k2の関係にある。この場合に自動生成されるべきアサーションは、「信号ａの立上り時から、時間k3〜k2の間に信号ｂが変化する」である。
【００２７】
図３に示す波形デー102と、検証基準信号ａおよび検証対象信号ｂが含まれている信号情報101と図１の信号変化情報自動生成部103に入力する。信号変化情報自動生成部103は信号情報101に指定された検証基準信号ａと検証対象信号ｂに関して波形データ102から信号の変化時の値、時刻を順次に入力した検証基準信号変化情報104と検証対象信号変化情報105を生成する。ここで、信号ｎの値が変化した時刻を波形データ102から取り出す関数をＴn（ｔ）とすると、時刻ｔ＝0〜tendの信号ａの信号変化情報は式（１）、信号ｂの信号変化情報は式（２）で表される。
0004564914.tif 000002
【００２８】
0004564914.tif 000003
【００２９】
次に、検証基準信号変化情報104と検証対象信号変化情報105をアサーション生成部106に入力し、両者を比較することで信号情報101に指定した信号ａと信号ｂ間の関係が認識される。ここで、信号ｎの変化点から信号ｍの変化点までの時間を求める関数をQmn(t)とする。信号ａの変化点から信号ｂの変化するまでの時間k1は式（３）で表される。
ｋ1＝(信号ａ変化情報の一番目のデータ)―(信号ｂ変化情報の１番目のデータ)＝Qab・・式（３）
また、時刻ｔ＝0〜tendまでの信号ａに対する信号ｂの変化時間情報Qab は、式（４）で表される。
0004564914.tif 000004
【００３０】
また、信号ｎの変化時の値を波形データ102から取り出す関数をN（ｔ）とすれば、信号ａの値はA(t)、信号ｂの値はB(t)である。更に、変化時間情報Qmn(t)と変化時の値N(t)からアサーション記述に変換する関数をＨとする。
【００３１】
時刻ｔ＝０〜tendまでの信号ａと信号ｂに対するアサーションは、式（５）で表され、図３に示した波形データに対するアサーション107は、式（６）で表される。
0004564914.tif 000005
【００３２】
アサーション＝信号ｂ：ｉｆ（信号ａの立上り）then変化許容範囲[k3〜k2]（信号ｂが変化する）・・・（式６）
である。
【００３３】
また、指定信号が複数の場合のアサーションは式（７）で表される。
0004564914.tif 000006
【００３４】
なお、図１の検証基準信号と検証対象信号の信号変化が明らかで、検証基準信号変化情報104と検証対象信号変化情報105が信号変化情報自動生成部103を使用せずに生成可能である場合、図４のアサーション自動生成部208の入力は図１の検証基準信号変化情報104と検証対象信号変化情報105である。アサーション自動生成部208では、アサーション自動生成プログラム106のみが動作してアサーション107を生成する。
【図面の簡単な説明】
【００３５】
【図１】本発明のアサーションの自動生成を説明するための図
【図２】本発明による論理回路設計検証方法のフローチャート
【図３】本発明を説明するための波形データを例示する図
【図４】基準回路Ａに変更をかけた変更回路Ａ’に対する検証環境を示す模式図
【図５】従来のプロパティ自動生成方法を示す図
【図６】従来技術を組み込んだアサーション・ベース検証フローを示す図
【符号の説明】
【００３６】
101  信号情報
102  波形データ
103  信号変化情報自動生成部
104  検証基準信号変化情報
105  検証対象信号変化情報
106  アサーション生成部
107  アサーション
201  ユーザロジック仕様
202  IP
203  動作パタン
204  回路記述
205  概要仕様
206  評価パタン
207  変更後IP
208  IP
【図１】
0004564914.tif 000007
【図２】
0004564914.tif 000008
【図３】
0004564914.tif 000009
【図４】
0004564914.tif 000010
【図５】
0004564914.tif 000011
【図６】
0004564914.tif 000012