(57)【特許請求の範囲】
【請求項１】
検証対象である論理回路に入力される複数の入力信号について予め順位付けされ、その順位は、前記論理回路の動作中に論理レベルが頻繁に変化する入力信号または論理レベルが不規則に変化する入力信号ほど高い信号名リストを用いて、コンピュータが、前記順位の高い順に、各入力端子に入力可能な全ての入力パターンを順次与え、前記各入力パターンを用いて検証を実行するステップと、
コンピュータが、検証により得られた検証結果を出力するステップとを備え、
前記論理回路の検証において入力パターンが決まっている前記入力信号について、コンピュータが、入力された前記入力パターンを正規表現に変換することを特徴とする形式的検証方法。
【請求項２】
請求項１記載の形式的検証方法において、
コンピュータが、前記入力可能な全ての入力パターンが与えられる前記入力信号を除く入力信号には、"０固定"または"１固定"のいずれかの入力パターンを与えて検証を実行することを特徴とする形式的検証方法。
【請求項３】
請求項１記載の形式的検証方法において、
コンピュータが、前記入力信号のそれぞれに対して前記入力可能な全ての入力パターンを与えて検証を実行した後、
コンピュータが、複数の前記入力信号の組み合わせのうち、前記順位の高い組み合わせから順に、前記入力可能な全ての入力パターンを与えて検証を実行することを特徴とする形式的検証方法。
【請求項４】
請求項３記載の形式的検証方法において、
コンピュータが、前記入力可能な全ての入力パターンが与えられる前記入力信号を除く入力信号には、"０固定"または"１固定"のいずれかの入力パターンを与えて検証を実行することを特徴とする形式的検証方法。
【請求項５】
請求項１記載の形式的検証方法において、
コンピュータが、メモリ不足により検証が実行できなくなったときに、検証を完了した入力パターンと検証を完了していない入力パターンとを区別して出力することを特徴とする形式的検証方法。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、論理回路の機能を検証する形式的検証方法に関する。
【０００２】
【従来の技術】
システムLSI等の半導体集積回路は、高機能になり論理規模も大きくなっている。これに伴い、半導体集積回路の論理検証は、検証規模、検証時間ともますます長大化する傾向にある。
近時、論理検証技術の１つとして、形式的検証が注目されている。形式的検証は、例えばＲＴＬ記述によりモデル化された論理回路を有限要素機械に変換し、検証すべき仕様を満たしていることを数学的に証明するものである。形式的検証は、入力パターンのみを考慮する従来のシミュレーション手法に比べて網羅性の点で優れている。そのため、シミュレーションでは見つけにくいエラーを検出できる。
【０００３】
【発明が解決しようとする課題】
しかしながら、形式的検証は、論理シミュレーションに比べ計算量が大きくなる。このため、状態数の多い回路モデルを扱うと、検証プログラムを実行するワークステーションのメモリ容量が不足し、検証不能になることがある。メモリ不足により検証不能になった場合、検証プログラムは強制終了してしまうため、検証結果は何も残らないという問題があった。すなわち、検証プログラムが強制終了した場合、どこまで検証したかを確認できないという問題があった。形式的検証の実行時間は、長い場合１週間程度かかることがある。このため、強制終了した際の時間的損失、コスト的損失は非常に大きい。
【０００４】
形式的検証で扱える回路モデルの規模は、モデルに含まれるフリップフロップの数に大きく依存する。理論的には、回路モデルの状態数は、フリップフロップの増分の２倍になり、これに対応して検証に必要なメモリ容量も２倍になる。一方で、形式的検証は、上述したように入力パターンの網羅性を特徴としているため、検証に必要なメモリ容量および検証時間を正しく見積ることは困難である。このため、ワークステーションのメモリを単に増設しただけでは、形式的検証が最後まで正しく行われるとは限らない。
【０００５】
このように、形式的検証は、論理回路の検証に非常に有用である反面、比較的起こりやすいメモリ不足による強制終了時の検討は、何もなされていない。
本発明の目的は、形式的検証が強制終了した場合に、それまでの検証結果を残すことで、検証効率を向上することにある。
【０００６】
【課題を解決するための手段】
本発明の形式的検証方法では、検証対象である論理回路に入力される入力信号について、これ等入力信号が変化したときに論理回路の動作に与える影響度の順位付けが行われる。そして、影響度の高い入力信号から順に、考えられる全ての入力パターンであるフリーパターンを与えて検証が実行される。すなわち、入力パターンは、予め設定された条件（影響度）に応じて順次生成される。したがって、検証装置のメモリ不足等により形式的検証が途中で強制終了した場合にも、上述した影響度に基づいて途中までの検証結果を残すことができる。この結果、強制終了の原因の解析が容易になり、検証効率を向上できる。検証が完了した入力パターンと、検証できなかった入力パターンとが明確になるため、全ての検証を完了するまでの時間、検証に必要な検証装置のメモリ容量を見積もることができる。
【０００７】
本発明の形式的検証方法では、入力信号のそれぞれに対してフリーパターンを与えて検証が実行された後、影響度の高い複数の入力信号から順に、フリーパターンを与えて検証が実行される。このように、徐々に複雑な入力パターンを与えることで、例えば検証装置のメモリ容量が同じ場合、より多くの入力パターンの組み合わせについて検証することができる。この結果、より多くの種類の検証履歴を残すことができる。
【０００８】
本発明の形式的検証方法では、フリーパターンを与えない入力信号には、"０固定"または"１固定"のいずれかを与えて検証が実行される。すなわち、論理回路動作に与える影響度の低い入力信号には、優先的に"０固定"または"１固定"のいずれが与えられる。予め設定された条件（影響度）と生成される入力パターンとの関係が分かりやすくなるため、強制終了の原因の解析が容易になり、検証効率を向上できる。
【０００９】
本発明の形式的検証方法では、論理回路の検証において入力パターンが決まっている入力信号について、入力パターンが正規表現で記述される。このため、順位付けされる信号の数を減らすことができ、検証時間を短縮できる。また、入力パターンを容易に生成できる。
【００１０】
【発明の実施の形態】
以下、本発明の実施形態を図面を用いて説明する。
図１〜図５は、本発明の形式的検証方法の第１の実施形態を示している。
図１は、形式的検証を行う論理回路（検証対象）の一例を示している。この論理回路は、例えば、システムLSI等の半導体集積回路内に形成されている。論理回路の仕様は、入力信号IN-A、IN-B、IN-Cを与えられたとき、出力信号OUT-1、OUT-2が同時に"１"にならないように決められている。このため、形式的検証では、出力信号OUT-1、OUT-2が同時に"１"にならないことを数学的を証明する。形式的検証は、例えば、ワークステーションの検証プログラムによって実行される。
【００１１】
図２は、入力信号IN-A、IN-B、IN-Cに対応する信号名リストを示している。信号名リストは、入力信号IN-A、IN-B、IN-Cについて、これ等入力信号が変化したときに論理回路の動作に与える影響度の順位付けしたものである。信号名リストは、検証する論理回路を熟知した設計者または検証者が作成する。
【００１２】
例えば、システムLSIの動作モード（通常動作モード、スタンバイモード、試験モード等）を設定する動作モード信号のように、論理値を固定してもよい入力信号は、順位を低くする。入力レベルを固定すると検証の意義が低くなる信号は、順位を高くする。優先順位を高くする信号として、例えば、割り込み信号がある。但し、動作モードの切り換え動作を検証の目的とするとき、動作モード信号の順位は高くなる。
【００１３】
順位付けすると検証の意味がなくなる信号は、信号名リストから除外する。例えば、通常動作モードのみの検証をする場合、リセット信号は信号名リストから除外する。同様に、割り込み信号の入力を無効として通常動作時の検証をするとき、割り込み信号は信号名リストから除外する。
【００１４】
このように、論理回路の動作のうち、着目する動作（検証する動作）において、論理レベルが頻繁に変化する入力信号あるいは論理レベルの変化が不規則な入力信号は、順位を高くする。逆に、着目する動作（検証する動作）において、論理レベルが余り変化しない入力信号、あるいは、論理回路の動作にあまり影響しない入力信号は、順位を低くする。
【００１５】
作成した信号名リストは、検証を実行するワークステーションに入力される。ワークステーションにより実行される検証プログラムは、信号名リストの順位を参照しながら入力パターンを順次生成し、検証を実行する。
図３は、検証プログラムが生成する入力パターンの組み合わせの例を示している。検証プログラムは、まず、影響度の順位の低い入力信号から、"０固定（図中の０表示）"および"１固定（図中の１表示）"を与える（（組み合わせ（１）〜（８））。
【００１６】
検証プログラムは、次に、影響度の順位の高い入力信号から順に、"フリーパターン（図中の？表示）"を与え、残りの入力信号に"０固定"および"１固定"を与える（（組み合わせ（９）〜（１２）、（１３）〜（１６）、（１７）〜（２０））。ここで、"フリーパターン"とは、網羅的に与えられる入力可能な全てのパターンである。
【００１７】
検証プログラムは、次に、影響度の順位の高い二つの入力信号から順に、"フリーパターン"を与え、残りの入力信号に"０固定"および"１固定"を与える（（組み合わせ（２１）〜（２２）、（２３）〜（２４）、（２５）〜（２６））。このように、検証プログラムは、予め信号名リストに設定された条件（影響度）に従い、"フリーパターン"が与えられる入力信号を徐々に増やしながら、入力パターンを生成する。さらに、検証プログラムは、全ての入力信号に"フリーパターン"を与える（組み合わせ（２７））。
【００１８】
入力パターンの組み合わせは、検証する入力信号の数をｎとしたとき、３のｎ乗になる。この例では、入力信号の数は"３"のため、組み合わせは、（１）〜（２７）の２７通りになる。なお、組み合わせ（１）〜（８）、組み合わせ（９）〜（１２）、組み合わせ（１３）〜（１６）、組み合わせ（１７）〜（２０）、組み合わせ（２１）〜（２２）、組み合わせ（２３）〜（２４）、組み合わせ（２５）〜（２６）からなる７つのグループにおいて、各グループ内での組み合わせの順序は、図３に限定する必要はない。例えば、組み合わせ（１３）〜（１６）のグループにおいて、検証を（１６）〜（１３）の順に実行してもよい。
【００１９】
全ての入力信号にフリーパターンを与える組み合わせ（２７）は、従来の形式的検証で使用されていた入力パターンに相当する。このように、本発明では、従来一括して実行していた論理検証を、入力信号が回路に与える影響度に応じて、複数の入力パターンの組み合わせに分割して実行する。このため、検証者・設計者は、ワークステーションのメモリ不足により、検証プログラムが強制終了した場合にも、どの組み合わせまで検証が完了したかを確認できる。
【００２０】
図４は、ワークステーション（検証プログラム）が実行する検証のフローを示している。検証は、メモリ不足が生じるまで、図３に示した組み合わせ（１）〜（２７）の順で実行される。
まず、ステップS1において、全ての入力信号IN-A、IN-B、IN-Cに順次"０固定"または"１固定"が与えられ、検証が行われる。ステップS1は、図３に示した組み合わせ（１）〜（８）に対応している。
【００２１】
次に、ステップS2において、影響度の高い順に１つの入力信号に"フリーパターン"が与えられ、残りの入力信号に"０固定"または"１固定"が与えられ、検証が行われる。ステップS2は、図３に示した組み合わせ（９）〜（２０）に対応している。
次に、ステップS3において、影響度の高い順に２つの入力信号に"フリーパターン"が与えられ、残りの入力信号に"０固定"または"１固定"が与えられ、検証が行われる。ステップS3は、図３に示した組み合わせ（２１）〜（２６）に対応している。このように、徐々に複雑な入力パターンを与えることで、より多くの入力パターンの組み合わせについて検証することができる。
【００２２】
最後に、ステップS4において、全ての入力信号IN-A、IN-B、IN-Cに"フリーパターン"が与えられ、検証が行われる。ステップS4は、図３に示した組み合わせ（２７）に対応している。
なお、入力信号の数が"３"より多いときには、ステップS3の後に、影響度の高い複数の入力信号に"フリーパターン"が順次与えられ、残りの入力信号に"０固定"または"１固定"が与えられ、検証が行われる。
【００２３】
図５は、検証時にワークステーション内で生成される入力信号IN-A、IN-B、IN-Cの波形の一部と検証結果を示している。この例では、組み合わせ（２５）の検証中にワークステーションのメモリ容量が不足し、以降の検証が実行不能になる。しかし、入力パターンの組み合わせは、予め設計者等が作成した信号名リストに基づいて決められているため、この時点で、組み合わせ（１）〜（２４）の検証が問題なく完了したことが判る。検証が完了した入力パターン（１）〜（２４）と、検証できなかった入力パターン（２５）〜（２７）とが明確になるため、全ての検証を完了するまでの時間、および検証に必要なメモリ容量が容易に見積り可能になる。
【００２４】
図６は、メモリ容量の不足により検証が中断した後に、ワークステーションから出力される検証結果の例を示している。検証結果欄の"OK"は、検証が問題なく完了したことを表している。検証結果欄の"NG"は、この入力パターン（組み合わせ（２５））で検証中にメモリ不足が発生し、検証が中断されたことを表している。検証結果欄の"−"は、このパターン（組み合わせ（２６）、（２７））での検証が実行できなかったことを表している。
【００２５】
形式的検証が途中で強制終了した場合、設計者等は、図６に示した形式的検証の実行結果に基づいて、実行できなかった組み合わせのうち、実行できた組み合わせを含まない部分を、論理シミュレーション等で検証できないかを検討する。また、検証が完了した組み合わせから、不足したメモリの容量を予測し、必要に応じて、メモリの増設を検討する。
【００２６】
以上、本実施形態では、入力パターンが、予め設定された条件（影響度）に応じて順次生成されるため、ワークステーションのメモリ不足により形式的検証が途中で強制終了した場合にも、影響度に基づいて途中までの検証結果を残すことができる。すなわち、入力信号のどのような組み合わせまで検証したかを履歴として残すことができる。この結果、検証結果が"NG"になったときに、原因の解析が容易になり、検証効率を向上できる。
【００２７】
検証が完了した入力パターン（例えば、組み合わせ（１）〜（２４））と、検証できなかった入力パターン（例えば、組み合わせ（２５）〜（２７））とが明確になるため、全ての検証を完了するまでの時間、検証に必要なメモリ容量を見積もることができる。
入力信号IN-A、IN-B、IN-Cのそれぞれに対してフリーパターンを与えて検証を実行した後、影響度の高い複数の入力信号から順に、フリーパターンを与えて検証を実行した。このように、徐々に複雑な入力パターンを与えることで、ワークステーションのメモリ容量が同じ場合、より多くの入力パターンの組み合わせについて検証することができる。この結果、より多くの種類の検証履歴を残すことができる。
【００２８】
フリーパターンを与えない入力信号、すなわち、論理回路動作に与える影響度の低い入力信号には、優先的に"０固定"または"１固定"のいずれかを与えて検証を実行した。予め設定された条件（影響度）と生成される入力パターンとの関係が分かりやすくなるため、強制終了の原因の解析が容易になり、検証効率を向上できる。
【００２９】
図７および図８は、本発明の形式的検証方法の第２の実施形態を示している。第１の実施形態で説明した要素と同一の要素については、同一の符号を付し、これ等については、詳細な説明を省略する。形式的検証を行う論理回路（検証対象）は、例えば、システムLSI等の半導体集積回路内に形成されている。
【００３０】
図７は、論理回路に入力される入力信号IN-A、IN-B、IN-C、RESET、CLK2の信号名リストを示している。すなわち、この実施形態では、第１の実施形態の信号名リストに、リセット信号RESET、クロック信号CLK2が付加されている。リセット信号RESETおよびクロック信号CLK2は、この実施形態の論理回路の検証において、入力パターンが決まっている信号である。すなわち、リセット信号RESETおよびクロック信号CLK2は、論理回路を正常に動作させるために、常に所定のタイミングの波形にする必要がある。信号名リストのうち、入力信号IN-A、IN-B、IN-Cについては、第１の実施形態と同様に、入力信号が変化したときに論理回路の動作に与える影響度の順位付けしたものである。
【００３１】
リセット信号RESETおよびクロック信号CLK2については、これ等信号の入力パターンは、正規表現で記述される。記号"［  ］"は、１サイクルにおける論理レベルを表している。記号"｛  ｝"は、繰り返し回数を表している。記号"＊"は、直前の記述が無限に続くことを表している。
【００３２】
このように、論理回路の検証において、入力パターンが常に決まっている信号については、その入力パターンを正規表現で記述する。換言すれば、ある論理レベルに変化しないと検証の意味がなくなる信号について正規表現で記述することで、順位付けされる信号の数を減らすことができ、検証時間を短縮できる。なお、信号名リストは、第１の実施形態と同様に、検証する論理回路を熟知した設計者または検証者が作成する。
【００３３】
図８は、図７の信号名リスト中で正規表現されたリセット信号RESETおよびクロック信号CLK2の実際の入力パターンを示している。リセット信号RESETおよびクロック信号CLK2の入力パターンは、設計者等が図８に示した波形をワークステーションに入力し、ワークステーションのプログラムがこれ等波形を正規表現に変換してもよく、設計者自らが正規表現で記述した入力パターンをワークステーションに入力してもよい。すなわち、入力パターンが常に決まっている信号については、その入力パターンが容易に生成される。
【００３４】
この実施形態においても、上述した第１の実施形態と同様の効果を得ることができる。さらに、この実施形態では、入力パターンが常に決まっている信号について、その入力パターンを正規表現で記述したので、順位付けされる信号の数を減らすことができ、検証時間を短縮できる。また、入力パターンを容易に生成できる。
【００３５】
なお、上述した実施形態では、検証プログラムをワークステーションで実行した例について述べた。本発明はかかる実施形態に限定されるものではない。例えば、検証プログラムをパーソナルコンピュータで実行しても良い。
以上、本発明について詳細に説明してきたが、上記の実施形態およびその変形例は発明の一例に過ぎず、本発明はこれに限定されるものではない。本発明を逸脱しない範囲で変形可能であることは明らかである。
【００３６】
【発明の効果】
本発明の形式的検証方法では、検証装置のメモリ不足等により形式的検証が途中で強制終了した場合にも、影響度に基づいて途中までの検証結果を残すことができる。この結果、強制終了の原因の解析が容易になり、検証効率を向上できる。全ての検証を完了するまでの時間、検証に必要な検証装置のメモリ容量を見積もることができる。
本発明の形式的検証方法では、より多くの入力パターンの組み合わせについて検証することができ、より多くの種類の検証履歴を残すことができる。
【００３７】
本発明の形式的検証方法では、予め設定された条件（影響度）と生成される入力パターンとの関係が分かりやすいため、強制終了の原因の解析が容易になり、検証効率を向上できる。
本発明の形式的検証方法では、順位付けされる信号の数を減らすことができ、検証時間を短縮できる。また、入力パターンを容易に生成できる。
【図面の簡単な説明】
【図１】第１の実施形態における形式的検証を行う論理回路の一例を示すブロック図である。
【図２】第１の実施形態における論理回路の動作に与える影響度の順位を示す入力信号の信号名リストである。
【図３】第１の実施形態における検証プログラムが生成する入力パターンの組み合わせ例を示す説明図である。
【図４】第１の実施形態における検証プログラムが実行する検証の手順を示すフローチャートである。
【図５】第１の実施形態におけるワークステーション内で生成される入力信号の波形の一部と検証結果を示す説明図である。
【図６】第１の実施形態におけるワークステーションから出力される検証結果の例を示す説明図である。
【図７】第２の実施形態における論理回路の動作に与える影響度の順位を示す入力信号の信号名リストである。
【図８】図７のリセット信号およびクロック信号の実際の入力パターンを示す波形図である。
【符号の説明】
CLK2  クロック信号
IN-A、IN-B、IN-C  入力信号
OUT-1、OUT-2  出力信号
RESET  リセット信号
【図１】
0004316158.tif 000002
【図２】
0004316158.tif 000003
【図３】
0004316158.tif 000004
【図４】
0004316158.tif 000005
【図５】
0004316158.tif 000006
【図６】
0004316158.tif 000007
【図７】
0004316158.tif 000008
【図８】
0004316158.tif 000009