(57)【要約】【課題】テストパタンの準備を行うことなく論理検証を実行できる論理回路設計検証装置及び論理回路設計検証方法を提供すること【解決手段】検証モデル生成部１１０は検証基準回路ＲＴＬ２１０と、検証対象回路ＲＴＬ２２０と、に基づいて検証基準回路と検証対象回路に同一信号を入力し、かつ各々の回路から異なる出力信号を出力する検証モデル１４０を生成する。アサーション生成部１２０は、検証基準回路と前記検証対象回路との等価性検証に用いる条件を含む情報が記述された設計ファイルに基づいて、検証基準回路からの出力信号と、検証対象回路からの出力信号と、が一致することを検証するためのアサーションを生成する。プロパティ検証部１３０は検証モデル１４０と、アサーション１５０と、を用いて検証対象回路が検証基準回路と論理的に等価であるか否かを検証する。【選択図】図１
2011180870.tif 000002
【特許請求の範囲】
【請求項１】
検証基準回路の回路動作記述と、検証対象回路の回路動作記述と、に基づいて前記検証基準回路と前記検証対象回路に同一信号を入力し、かつ各々の回路から異なる出力信号を出力する検証モデルを生成する検証モデル生成部と、
前記検証基準回路と前記検証対象回路との等価性検証に用いる条件を含む情報が記述された設計ファイルに基づいて、前記検証基準回路からの出力信号と、前記検証対象回路からの出力信号と、が一致することを検証するためのアサーションを生成するアサーション生成部と、
前記検証モデルと、前記アサーションと、を用いて前記検証対象回路が前記検証基準回路と論理的に等価であるか否かを数学的に検証するプロパティ検証を実行する検証部と、を備える論理回路検証装置。
【請求項２】
前記設定ファイルには、前記検証対象回路に前記検証基準回路と比べて新たに追加された追加機能に関する情報が含まれ、
前記アサーション生成部は、前記検証対象回路の前記追加機能を前記プロパティ検証の検証対象から除外した前記アサーションを生成することを特徴とする請求項１に記載の論理回路検証装置。
【請求項３】
前記設定ファイルには、
前記検証基準回路と前記検証対象回路の信号の対応関係の情報、前記検証基準回路と前記検証対象回路とからの出力信号の出力タイミングの情報、前記検証基準回路と前記検証対象回路とからの出力信号が一致するためのタイミングの情報、及び前記検証基準回路と前記検証対象回路とに入力される入力信号の制約の情報、のうち少なくとも１つに関する情報が含まれることを特徴とする請求項１または請求項２に記載の論理回路検証装置。
【請求項４】
検証基準回路の回路動作記述と、検証対象回路の回路動作記述と、に基づいて前記検証基準回路と前記検証対象回路に同一信号を入力し、かつ各々の回路から異なる出力信号を出力する検証モデルを生成する検証モデル生成ステップと、
前記検証基準回路と前記検証対象回路との等価性検証に用いる条件を含む情報が記述された設計ファイルに基づいて、前記検証基準回路からの出力信号と、前記検証対象回路からの出力信号と、が一致することを検証するためのアサーションを生成するアサーション生成ステップと、
前記検証モデルと、前記アサーションと、を用いて前記検証対象回路が前記検証基準回路と論理的に等価であるか否かを数学的に検証するプロパティ検証を実行する検証ステップと、を備える論理回路検証方法。
【請求項５】
前記設定ファイルには、前記検証対象回路に前記検証基準回路と比べて新たに追加された追加機能に関する情報が含まれ、
前記アサーションステップでは、前記検証対象回路の前記追加機能を前記プロパティ検証の検証対象から除外した前記アサーションを生成することを特徴とする請求項４に記載の論理回路検証方法。
【請求項６】
前記設定ファイルには、
前記検証基準回路と前記検証対象回路の信号の対応関係の情報、前記検証基準回路と前記検証対象回路とからの出力信号の出力タイミングの情報、前記検証基準回路と前記検証対象回路とからの出力信号が一致するためのタイミングの情報、及び前記検証基準回路と前記検証対象回路とに入力される入力信号の制約の情報、のうち少なくとも１つに関する情報が含まれることを特徴とする請求項４または請求項５に記載の論理回路検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は論理回路設計検証装置及び論理回路設計検証方法、より詳細にはアサーションを用いて論理回路の検証を行う論理回路設計検証装置及び論理回路設計検証方法に関する。
【背景技術】
【０００２】
論理回路の設計は、ＨＤＬ（Hardware Description Language）と呼ばれるプログラミング言語を用いて行われることが多い。新しい論理回路を設計する場合、一般的に既存の論理回路を流用して新たな論理回路を設計することが行われる。これにより、設計の効率化を図っている。
【０００３】
しかし、既存の論理回路の機能拡張、ＬＳＩ（Large Scale Integration）プロセスの変更等により、既存回路をそのまま流用できることは少ない。すなわち、既存回路の設計を修正することにより新しい論理回路を設計する。この設計の修正により、新たに設計した論理回路に論理バグが混入する恐れがある。論理バグを検出するために、新たに設計した論理回路に対して、変更を行わなかった部分を含めた論理検証を行う必要がある。
【０００４】
ここで、既存の論理回路と新たに設計した論理回路との等価性を検証するために等価性検証技術が用いられる。一般に、論理回路の等価性を検証するためには、回路の一致性を検証する形式検証が用いられる。しかし形式検証では、２つの回路が論理的に等価であるが回路構造的に異なっている場合に、正しい等価性の検証が出来ない。
【０００５】
特許文献１には、アサーションを自動生成する論理回路設計方法に関する技術が開示されている。特許文献１に開示されているアサーション自動生成装置のブロック図を図４に示す。
【０００６】
当該アサーション自動生成装置は、検証基準回路ＲＴＬに対してテストパタンである動作パタンを用いたシミュレーションを行い、信号波形ファイルを生成する。当該信号波形ファイルを基に等価性検証に用いるアサーションを生成する。当該アサーション自動生成装置は、生成したアサーションを用いて検証対象回路を検証する。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開２００７−１１５００１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、特許文献１に記載のアサーション自動生成装置によっては、以下の問題がある。前述のように当該アサーション自動生成装置では、所望のテストを行うために用いるテストパタンを予め用意する必要がある。しかしながら、テストパタンの用意が不十分である場合、十分なテストが行われない恐れがある。すなわち、当該アサーション自動生成装置によっては、網羅的な論理検証の実行が行われない恐れがある。
【０００９】
本発明はこのような問題を解決するためになされたものであり、テストパタンの準備を行うことなく論理検証を実行できる論理回路設計検証装置及び論理回路設計検証方法を提供することを主たる目的とする。
【課題を解決するための手段】
【００１０】
本発明にかかる論理回路設計検証装置の一態様は、
検証基準回路の回路動作記述と、検証対象回路の回路動作記述と、に基づいて前記検証基準回路と前記検証対象回路に同一信号を入力し、かつ各々の回路から異なる出力信号を出力する検証モデルを生成する検証モデル生成部と、
前記検証基準回路と前記検証対象回路との等価性検証に用いる条件を含む情報が記述された設計ファイルに基づいて、前記検証基準回路からの出力信号と、前記検証対象回路からの出力信号と、が一致することを検証するためのアサーションを生成するアサーション生成部と、
前記検証モデルと、前記アサーションと、を用いて前記検証対象回路が前記検証基準回路と論理的に等価であるか否かを数学的に検証するプロパティ検証を実行する検証部と、を備えるものである。
【００１１】
本発明にかかる論理回路設計検証方法の一態様は、
検証基準回路の回路動作記述と、検証対象回路の回路動作記述と、に基づいて前記検証基準回路と前記検証対象回路に同一信号を入力し、かつ各々の回路から異なる出力信号を出力する検証モデルを生成する検証モデル生成ステップと、
前記検証基準回路と前記検証対象回路との等価性検証に用いる条件を含む情報が記述された設計ファイルに基づいて、前記検証基準回路からの出力信号と、前記検証対象回路からの出力信号と、が一致することを検証するためのアサーションを生成するアサーション生成ステップと、
前記検証モデルと、前記アサーションと、を用いて前記検証対象回路が前記検証基準回路と論理的に等価であるか否かを数学的に検証するプロパティ検証を実行する検証ステップと、を備えるものである。
【発明の効果】
【００１２】
本発明によれば、テストパタンの準備を行うことなく論理検証を実行できる論理回路設計検証装置及び論理回路設計検証方法を提供することができる。
【図面の簡単な説明】
【００１３】
【図１】実施の形態１にかかる論理回路設計検証装置の全体構成を示すブロック図である。
【図２】実施の形態１にかかる検証モデル（検証基準回路と検証対象回路が論理的に等価である場合）の例を示す図である。
【図３】実施の形態１にかかる検証モデル（検証基準回路と検証対象回路が論理的に等価ではない場合）の例を示す図である。
【図４】特許文献１に記載のアサーション自動生成装置の全体構成を示すブロック図である。
【発明を実施するための形態】
【００１４】
実施の形態１
以下、図面を参照して本発明の実施の形態について説明する。図１は、本実施の形態にかかる論理回路設計検証装置の構成を示すブロック図である。
【００１５】
論理回路設計検証装置１０は、検証モデル生成部１１０と、アサーション生成部１２０と、プロパティ検証部１３０と、を備える。論理回路設計検証装置１０には、検証基準回路ＲＴＬ（Register Transfer Level, レジスタ転送レベル）２１０と、検証対象回路ＲＴＬ２２０と、設定ファイル２３０と、が入力される。論理回路設計検証装置１０は、検証モデル３００を出力する。
【００１６】
検証基準回路ＲＴＬ２１０は、既存の回路（検証基準回路）の構成を示すＲＴＬファイルである。ユーザは予め設計した論理回路のＲＴＬファイルを準備しているものとする。ここで検証基準回路とは、従来のシステムに用いられている論理回路であり、検証の基準となる論理回路である。
【００１７】
検証対象回路ＲＴＬ２２０は、新たに設計した論理回路（検証対象回路）に対応するＲＴＬファイルである。検証対象回路は、検証基準回路ＲＴＬ２１０に対応する検証基準回路の設計を一部変更した回路である。
【００１８】
設定ファイル２３０は、検証基準回路と、検証対象回路との等価性検証に用いる条件を含む情報が格納されているファイルである。具体的には、設定ファイル２３０には、検証基準回路と検証対象回路の信号の対応関係の情報、検証基準回路と検証対象回路とからの出力信号の出力タイミングの情報、検証基準回路と検証対象回路とからの出力信号が一致するためのタイミングの情報、検証基準回路と検証対象回路とに入力される入力信号の制約の情報等が含まれうる。また、設定ファイル２３０には、検証対象回路に検証基準回路と比べて新たに追加された追加機能に関する情報が含まれうる。さらにまた、設定ファイル２３０には検証対象回路及び検証基準回路の内部レジスタの初期値等の情報も設定される。
【００１９】
例えば、検証基準回路が加算器であり、かつ加算結果を出力するために２クロックを要していたとする。また、検証対象回路が加算結果を出力するために３クロックを要するとする。この場合に設定ファイル２３０には、検証基準回路に入力してから２クロック後の出力と、検証対象回路に入力してから３クロック後の出力と、が対応するという情報が記述される。また、入力信号の制約としてどのような範囲の数値が入力されるか、どのタイミングにより入力信号が入力されるか等も記述される。さらにまた、後述のプロパティ検証部１３０によるプロパティ検証は、有効ビットが点灯している場合に行うこと等も記述されうる。
【００２０】
なお、設定ファイル２３０は、適宜書き換えることが可能である。たとえば、検証対象回路の設計が変更により信号名が変わった場合、当該信号名を設計ファイル２３０に記述することが出来る。
【００２１】
検証モデル生成部１１０は、検証基準回路と、検証対象回路の等価性を検証するために用いる検証モデル１４０を生成する処理部である。検証モデル生成部１１０には、外部から検証基準回路ＲＴＬ２１０と、検証対象回路ＲＴＬ２２０と、が入力される。検証モデル生成部１１０が生成する検証モデル１４０の例を図２及び図３に示す。
【００２２】
図２は、検証基準回路と、検証対象回路と、が論理的に等価である場合の検証モデル１４０を示す図である。検証モデル１４０は、検証基準回路に等価な回路である検証基準回路モデル１４０１と、検証対象回路に等価な回路である検証対象回路モデル１４０２と、を含む構成である。検証基準回路モデル１４０１と、検証対象回路モデル１４０２には同一の入力信号１４０３が入力される。また、検証基準回路モデル１４０１から出力される出力信号１４０４と、検証対象回路モデル１４０２から出力される出力信号１４０５と、は別信号となる。
【００２３】
図３は、検証対象回路に検証基準回路と比べて新たに追加された追加機能がある場合の検証モデル１４０を示す図である。図２に示した構成と異なり、検証対象回路モデル１４０２は、等価相当機能回路モデル１４０２１と、追加機能回路モデル１４０２２と、を備える構成である。
【００２４】
等価相当機能回路モデル１４０２１は、検証基準回路と論理的に等価な処理を行う回路である。追加機能回路モデル１４０２２は、検証基準回路に新たに追加された機能に関する回路である。設定ファイル２３０には、検証対象回路内のどの回路が検証基準回路と等価な回路であるかが記述される。すなわち、設定ファイル２３０には、検証対象回路内のどの箇所が等価相当機能回路モデル１４０２１に該当するかが記述される。この設定ファイル２３０の記述を参照し、後述のアサーション生成部１２０は追加機能回路モデル１４０２２に入力信号１４２０３を入力しないような検証を行うアサーション１５０を生成する。
【００２５】
アサーション生成部１２０は、入力された設定ファイル２３０の内容を解析し、解析内容に基づいてアサーション１５０を生成する処理部である。アサーション１５０は、検証基準回路と検証対象回路の等価性を検証するために用いられる。より具体的には、アサーション１５０の記述において、出力信号１４０４と、出力信号１４０５と、が一致することが記述される。また、アサーション１５０には、設定ファイル２３０内に記述された入力信号の制約等が反映された検証内容が記述される。アサーション生成部１２０は、生成したアサーション１５０をプロパティ検証部１３０に入力する。
【００２６】
例えば、設定ファイル２３０内に、「検証基準回路に入力信号を入力してから２クロック後の出力と、検証対象回路に入力信号を入力してから３クロック後の出力と、が対応する」という情報が記述されていたとする。この場合アサーション生成部１２０は、入力信号１４０３の入力から２クロック後の出力信号１４０４と、入力信号１４０３の入力から３クロック後の出力信号１４０５と、が一致することを検証することが記述されたアサーション１５０を生成する。
【００２７】
また、アサーション生成部１２０は、検証対象回路に検証基準回路と比べて新たに追加された追加機能に関する情報が記述されている場合、図３に示すように追加機能回路モデル１４０２２をプロパティ検証対象から除外するようなアサーション１５０を生成する。これにより、追加機能を除外したうえで検証基準回路と検証対象回路との等価検証を実行することが出来る。
【００２８】
プロパティ検証部１３０は、入力された検証モデル１４０と、アサーション１５０と、を用いてプロパティ検証を行う処理部である。プロパティ検証部１３０は、当該プロパティ検証によって、検証基準回路と検証対象回路が等価であるか否かを検証する。より具体的には、プロパティ検証部１３０はアサーション１５０の記述を基に検証モデル１４０に対して入力信号１４０３を入力する。そして、プロパティ検証部１３０は出力信号１４０４と、出力信号１４０５と、が一致するか否かを判定する。プロパティ検証部１３０は当該判定結果を用いて検証基準回路と検証対象回路が等価であるか否かを検証する。プロパティ検証部１３０は、検証結果を検証結果ファイル３００として出力する。
【００２９】
なおプロパティ検証とは、論理回路をはじめとする設計情報を数学的に解析するフォーマルベリフィケーション（形式的論理検証）の一つである。プロパティ検証では、設計した論理回路の機能記述言語（たとえばＨＤＬ）による機能記述が満たすべき条件（プロパティ）を満たしているか否かを数学的に証明する。
【００３０】
検証結果ファイル３００は、プロパティ検証部１３０によるプロパティ検証の結果が記述されたファイルである。すなわち、検証結果ファイル３００には、検証基準回路と検証対象回路が等価であるか否かの情報が記述される。ユーザは検証結果ファイル３００を参照することにより、検証基準回路と、検証対象回路と、が等価であるか否かを判断することが出来る。
【００３１】
続いて、本実施の形態にかかる論理回路設計検証装置の効果について説明する。上述のように検証基準回路の回路動作記述（本例では検証基準回路ＲＴＬ２１０）と検証対象回路の回路動作記述（本例では検証対象回路ＲＴＬ２２０）とから検証モデル１４０を生成する。また、検証基準回路と検証対象回路との関連性等を記載した設定ファイル２３０の内容からアサーション１５０を生成する。ここで、設定ファイル２３０には、等価性検証に用いる条件を含む情報が記述されている。プロパティ検証部１３０は検証モデル１４０と、アサーション１５０と、を用いることにより検証基準回路と検証対象回路との等価性を検証することが出来る。
【００３２】
また、上述のプロパティ検証部１３０によるプロパティ検証は、検証基準回路と検証対象回路の等価性を数学的に証明することが出来る。これにより、等価性の検証の網羅性を把握でき、当該網羅性を向上させる対応を行うことが可能になる。プロパティ検証による数学的な証明により論理回路設計の品質の向上も可能となる。
【００３３】
上述の論理回路設計検証装置において、ユーザが行うべき作業は検証基準回路と、検証対象回路と、に関する情報を設定ファイル２３０に記述することのみである。ここで、設定ファイル２３０は、一般のユーザに理解しやすい任意の記述形式により記述することが可能である。そのため、ユーザは新たにアサーション言語等を用いた記述を行う必要が無い。これにより、アサーション言語等に不慣れなユーザであっても正確に論理回路設計の検証を行うことが出来る。
【００３４】
また上述の構成では、ユーザがテストパタンを生成する必要がない。そのため、検証にかかる準備時間が削減される。検証準備時間の削減により、両回路の等価性の検証にかかる時間が削減される。
【００３５】
さらにまた、設定ファイル２３０には、検証対象回路に検証基準回路と比べて新たに追加された追加機能に関する情報を記載可能である。そして、上述のようにアサーション生成部１２０は追加機能を等価性検証の対象から除外することが可能である。これにより、追加機能がある場合であっても、等価な箇所に関する等価性検証を実行することが出来る。なお、追加機能に関する機能の検証は別途実行することにより、論理バグの排除された論理回路を得ることができる。
【００３６】
なお、本発明は上記実施の形態に限られたものではなく、趣旨を逸脱しない範囲で適宜変更することが可能である。
【符号の説明】
【００３７】
１０        論理回路設計検証装置
１１０      検証モデル生成部
１２０      アサーション生成部
１３０      プロパティ検証部
１４０      検証モデル
１４０１    検証基準回路モデル
１４０２    検証対象回路モデル
１４０２１  等価相当機能回路モデル
１４０２２  追加機能回路モデル
１４０３    入力信号
１４０４    出力信号
１４０５    出力信号
１５０      アサーション
２１０      検証基準回路ＲＴＬ
２２０      検証対象回路ＲＴＬ
２３０      設定ファイル
３００      検証結果ファイル
【図１】
2011180870.tif 000003
【図２】
2011180870.tif 000004
【図３】
2011180870.tif 000005
【図４】
2011180870.tif 000006