(57)【要約】【課題】状態数が多く、状態遷移が複雑な回路に対しても、形式的論理検証可能な回路を提供し、効率良くかつ高精度の論理検証可能な回路設計を行う。【解決手段】ステートマシン回路２０の状態遷移を引き起こす信号ｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４が、ステートマシン回路２０の入力信号として定義されている。これによって、この入力信号を少ない値に設定することにより、この信号ｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４と比較を行なうカウンタの状態数を減らして形式的論理検証を行なう。【選択図】図３
2008304960.tif 000002
【特許請求の範囲】
【請求項１】
設計仕様書に基づいてハードウェア記述言語による論理回路設計を行ない、その回路の形式的論理検証を行なって、その検証結果を回路設計に反映させる論理回路設計装置において、
設計仕様書に基づいてハードウェア記述言語による論理回路の設計を行なう論理回路設計部と、
設計仕様書に基づいてプロパティの生成を行なうプロパティ生成部と、
設計された論理回路についてプロパティデータを使用して形式的論理検証を行なう形式的論理検証部と、
検証結果を分析して問題が有る場合に論理設計に反映させるための検証結果分析部と、
を備え、
前記論理回路設計部は、形式的論理検証対象となる論理回路の状態遷移値が該論理回路の入力信号として定義することを特徴とする論理回路設計装置。
【請求項２】
入力信号と定義される状態遷移値を、検証に支障が出ない範囲で小さく設定することを特徴とする請求項１記載の論理回路設計装置。
【請求項３】
設計仕様書に基づいてハードウェア記述言語による論理回路設計を行ない、その回路の形式的論理検証を行なって、その検証結果を回路設計に反映させる論理回路設計方法おいて、
設計仕様書に基づいてハードウェア記述言語による論理回路の設計を行なう論理回路設計ステップと、
設計仕様書に基づいてプロパティの生成を行なうプロパティ生成ステップと、
設計された論理回路についてプロパティデータを使用して形式的論理検証を行なう形式的論理検証ステップと、
検証結果を分析して問題が有る場合に論理設計に反映させるための検証結果分析ステップと、
を備え、
前記論理回路設計ステップでは、形式的論理検証対象となる論理回路の状態遷移値が該論理回路の入力信号として定義することを特徴とする論理回路設計方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウェア記述言語にて作成した半導体集積回路の検証を、形式的論理検証で行うことに関し、この形式的論理検証を有効活用し、効率良くかつ高精度の論理検証可能な論理回路設計装置及び論理回路設計方法に関する。
【背景技術】
【０００２】
一般に、半導体集積回路の検証方法には、論理シミュレーションによる検証と、形式的論理検証がある。論理シミュレーションによる検証では、入力パターン（テストベクタ）を検証の対象回路に与えて動作をシミュレーションし、結果を期待値と比較して、機能が正しく実現されていることを確認する。
【０００３】
しかし、近年システムＬＳＩ等の半導体集積回路は、大規模化、複雑化が進み、テストベクタを使用する論理シミュレーションは、膨大な検証時間と、検証するためのテストベクタ作成に多大な工数が必要となっている。さらに、テストベクタ作成については、所望の回路を活性化させて機能を確認するための適切なテストベクタを作成するスキルが要求され、不適切なテストベクタは検証漏れによる設計ミスの原因となる。
【０００４】
一方、形式的論理検証は、回路の論理を数学的な手法により解析し、検証する方法である。さらに、形式的論理検証には、２つの回路の論理的な等価性を比較検証する等価性検証と、設計者が望む設計仕様を満たす回路記述となっているかを検証するプロパティ検証がある。前述のプロパティ検証は、数学的な手法であるため、検証すべき設計仕様（プロパティ）が正しく定義されていれば、正当性を保証することができる。従って、形式的論理検証は、入力パターンのみを考慮する論理シミュレーションによる検証に比べて、網羅性に優れている。そのため、論理シミュレーションによる検証では見つけにくいコーナーケースのバグなどを検出できる。
【０００５】
以降、形式的論理検証とは、プロパティ検証を示すものとする。他方、後述する特許文献１で述べられているように、形式的論理検証では、対象回路の動作を時刻を追って表示することが困難であり、対象回路に不具合があって、その原因を解析したりする場合には、論理シミュレーションによる検証を用いた方が便利な場合もある。
【０００６】
このように、形式的論理検証は前述したように論理シミュレーションによる検証に対する利点があるものの、一般的には両者による検証を用いている。従って、半導体集積回路は、形式的論理検証及び論理シミュレーションによる検証の長所・短所を見極めたうえで、効率良くかつ高精度の論理検証が行われている。
【特許文献１】特開２０００−３０５９７７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
ここで、図５のステートマシン回路の検証方法について考察する。図５は、従来のステートマシン回路の構成の一例を示すブロック図である。図６は、このステートマシンの各ステートにおける移行条件を示す表であり、図７は、このステートマシンの各ステートにおけるリセットとカウントアップの条件を示す表であり、図８は、このステートマシンの各ステートにおける出力データを示す表である。
図５、図６、図７、図８に示すように、ステートマシン回路１００は、４つのＳＴＡＴＥと、４つのカウンタを内部に持つ回路である。
【０００８】
次に、ステートマシン回路１００の動作を説明する。
ステートマシン回路１００は、リセット直後にＳＴＡＴＥ０となり、第１のカウンタの出力値ｃｏｕｎｔ１がリセットされ、リセット解除後に第１のカウンタがカウントアップ開始する。入力データｉｎｄａｔａ＝“００１”かつｃｏｕｎｔ１＝ｃｎｔ＿ｖａｌ１となった時に、ＳＴＡＴＥ１へ状態遷移し、第２のカウンタの出力値ｃｏｕｎｔ２がリセットされる。その後、ｃｏｕｎｔ２がカウントアップされ、入力データｉｎｄａｔａ＝“０１０”かつｃｏｕｎｔ２＝ｃｎｔ＿ｖａｌ２となった時に、ＳＴＡＴＥ２へ状態遷移し、第３のカウンタの出力値ｃｏｕｎｔ３がリセットされる。その後、ｃｏｕｎｔ３がカウントアップされ、入力データｉｎｄａｔａ＝“１００”かつｃｏｕｎｔ３＝ｃｎｔ＿ｖａｌ３となった時に、ＳＴＡＴＥ３へ状態遷移し、第４のカウンタの出力値ｃｏｕｎｔ４がリセットされる。その後、ｃｏｕｎｔ４がカウントアップされ、入力データｉｎｄａｔａ＝“１０１”かつｃｏｕｎｔ４＝ｃｎｔ＿ｖａｌ４となった時に、ＳＴＡＴＥ０へ状態遷移し、元の状態へ戻る。出力データｏｕｔｄａｔａは、現在の状態（ｃｕｒｒｅｎｔ＿ｓｔａｔｅ）に従って、ＳＴＡＴＥ０の時は、“００”、ＳＴＡＴＥ１の時は、“０１”、ＳＴＡＴＥ２の時は、“１０”、ＳＴＡＴＥ３の時は、“１１”を出力する。
【０００９】
このステートマシン回路１００に関して、ステートマシンのデットロックを形式的論理検証で検証する場合を考えると、４つのカウンタのビット幅がそれぞれ１６ビットであるため、数学的に全状態を網羅するには、状態数が多くなり検証プログラムの実行に非常に時間がかかってしまう。この場合、ステートマシンのデットロックに関して、検証に多大な時間を要する。また、ステートマシンのデットロックを論理シミュレーションを用いて検証する場合を考えた場合も、デッドロックを検証するためのテストベクタ作成に多大な工数が必要となる。
【００１０】
また、形式的論理検証は、状態数が多く、状態遷移が複雑な回路を扱うと、検証プログラムを実行するのに多大な時間を要するとともに、ワークステーションのメモリ容量が不足し、検証不能になることがある。この場合、検証プログラムは強制終了してしまうため、検証結果は何も残らないという問題もあった。
【００１１】
形式的論理検証で扱える回路の規模は、回路に含まれるフリップフロップの数に大きく依存する。従って、形式的論理検証は、論理回路の検証に非常に有用である反面、状態数増大時には、検証できないという問題がある。
【００１２】
本発明は、このような状況に鑑みてなされたものであり、状態数が多く、状態遷移が複雑な回路に対しても、形式的論理検証可能な回路を提供し、効率良くかつ高精度の論理検証可能な回路設計を行う論理回路設計装置及び論理回路設計方法を提供することを目的とする。
【課題を解決するための手段】
【００１３】
本発明は、設計仕様書に基づいてハードウェア記述言語による論理回路設計を行ない、その回路の形式的論理検証を行なって、その検証結果を回路設計に反映させる論理回路設計装置において、
設計仕様書に基づいてハードウェア記述言語による論理回路の設計を行なう論理回路設計部と、設計仕様書に基づいてプロパティの生成を行なうプロパティ生成部と、設計された論理回路についてプロパティデータを使用して形式的論理検証を行なう形式的論理検証部と、検証結果を分析して問題が有る場合に論理設計に反映させるための検証結果分析部と、を備え、
前記論理回路設計部は、形式的論理検証対象となる論理回路の状態遷移値が該論理回路の入力信号として定義することを特徴とする。
【００１４】
入力信号と定義される状態遷移値を、検証に支障が出ない範囲で小さく設定することを特徴とする。
【００１５】
また、本発明は、設計仕様書に基づいてハードウェア記述言語による論理回路設計を行ない、その回路の形式的論理検証を行なって、その検証結果を回路設計に反映させる論理回路設計方法おいて、
設計仕様書に基づいてハードウェア記述言語による論理回路の設計を行なう論理回路設計ステップと、設計仕様書に基づいてプロパティの生成を行なうプロパティ生成ステップと、設計された論理回路についてプロパティデータを使用して形式的論理検証を行なう形式的論理検証ステップと、検証結果を分析して問題が有る場合に論理設計に反映させるための検証結果分析ステップと、を備え、
前記論理回路設計ステップでは、形式的論理検証対象となる論理回路の状態遷移値が該論理回路の入力信号として定義することを特徴とする。
【発明の効果】
【００１６】
本発明によれば、形式的論理検証対象となる論理回路の状態遷移値を該論理回路の入力信号として定義することにより、入力信号に制約を与えることができ、状態数を減らすことが可能となるため、形式的論理検証による検証を効率良くかつ高精度に行うことが可能になり、設計ミスの少ない論理回路を作成できる。
【発明を実施するための最良の形態】
【００１７】
以下、本発明に係る回路を添付図面を参照して説明する。また、同一の符号を付した部分は同一物を表す。
【００１８】
図１は本発明に係る論理回路設計装置の一例を示すブロック図である。
この論理回路設計装置１０は、ハード記述言語で記述された仕様データを記憶する仕様記憶部１１、仕様データに基づいて論理回路を設計する論理回路設計部１２、仕様データに基づいてプロパティを生成するプロパティ生成部１３、論理回路データを記憶する論理回路データ記憶部１４、プロパティデータを記憶するプロパティデータ記憶部１５、論理回路データとプロパティデータから形式的論理検証を行なう形式的論理検証部１６、検証結果を分析して問題が有る場合に論理設計に反映させるための検証結果分析部１７とから構成される。
【００１９】
図２は、この論理回路設計装置の動作を示すフローチャートである。図３は設計された論理回路の概念を示すブロック図であり、図４は具体的論理回路を示す回路図である。
【００２０】
論理回路設計部１２では、設計仕様書８に基づいて、ハードウェア記述言語（HDL:Hardware Description Language）で論理回路を設計する（ステップＳ２）。この設計された論理回路データは、論理回路データ記憶部１４に記憶される。また、同時にプロパティ生成部１３は、設計仕様書８に基づいてプロパティを作成する（ステップＳ３）。プロパティは、プロパティ記述言語（例えば、ＰＳＬ、ＳＶＡ）を用いて記述される。作成されたプロパティデータは、プロパティデータ記憶部１５に記憶される。
【００２１】
形式的論理検証部１６は、論理回路データ記憶部１４とプロパティデータ記憶部１５に記憶されている論理回路データとプロパティデータに基づいて形式的論理検証を行なう（ステップＳ４）。検証結果分析部１７は、検証結果を分析して、まず検証結果が得られたか否かを確認する（ステップＳ５）。ワークステーションのメモリ容量が足りない等が原因で検証結果が得られない場合は、設計検証環境の見直しの旨を通知して（ステップＳ６）、処理を終了する。この場合、形式的論理検証の検証プログラムを実行するワークステーションのハードウェアの限界（論理回路データが形式的論理検証に最適な回路になっていないケース）と、論理回路の状態数増大に起因する論理回路の最適化不足の２種類が考えられる。最初のケースでは、設計検証環境自体のバグとなり、全体を見直す必要がある。２番目のケースでは、ステップＳ２で論理回路を再設計する必要がある。
従って、論理回路設計装置１０は、見直しが必要な点を利用者に通知して（例えば、ワークステーションのディスプレイにログを表示する）処理を終了する。
【００２２】
ステップＳ５において、形式的論理検証部１６による検証結果を受けた検証結果分析部１７が、検証結果がＯＫか否かを確認する（ステップＳ７）。そして、回路とプロパティのどちらのバグかを確認する（ステップＳ８）。回路バグの場合、その点を修正するように、論理回路設計部１２に指示を出して、ステップＳ２に戻り、再設計をさせる。
プロパティバグの場合は、プロパティ生成部１３に指示を出して、ステップＳ３に戻り、プロパティの再生成をさせる。
【００２３】
論理回路設計部１２では、論理回路の状態数を出来るだけ少なくして、形式的論理検証を行なう検証プログラムの処理時間を短縮するとともに、検証プログラムで必要となるメモリ容量も少なくて済むように論理回路の再設計をする。その概念図が図３であり、具体的回路が図４である。
【００２４】
図３に示すように、設計対象となる回路は、ステートマシン回路２０である。このステートマシン回路２０は、動作は図５に示したステートマシン回路１００と同じである。異なる点は、各カウンタの比較値であるｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４信号が、入力ポートとして定義されているところが異なる。
【００２５】
ステートマシン回路２０とステートマシン回路１００とは、デットロックを形式的論理検証で検証を行う場合の実行しやすさに、大きな違いがある。前述したように図５の回路では、状態数が多いため、検証プログラムの実行に多大な時間を要する。
【００２６】
一方、図３のステートマシン回路２０のように、各カウンタの比較値を入力ポートとして定義することで、設計仕様としてプロパティによる制約を与えることが可能になる。この制約では、ｃｎｔ＿ｖａｌ１＝“０００Ｆ”のようにカウンタとの比較値を小さい値とすることで、状態数の増大を減らすことが可能になる。このように設計仕様のプロパティによる制約を活用することで、形式的論理検証による検証を効率良くかつ高精度に行うことが可能になる。
【００２７】
次に図４の回路に関して説明する。状態遷移回路３０への入力信号は、状態遷移信号（ｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４信号）とカウンタ出力とを比較器によって出力したものである。
【００２８】
状態遷移回路３０への入力信号形成回路は、フリップフロップからなるカウンタ２１，２３，２５，２７と、比較器２２，２４，２６，２８とからなる。カウンタ２１，２３，２５，２７がカウントしたカウント値ｃｏｕｎｔ１，２，３，４が比較器２２，２４，２６，２８に入力され、比較値ｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４と比較される。カウント値が比較値より小さい場合には、カウンタにフィードバックされカウントが続けられる。そして、カウント値が比較値と同じになると、入力信号として状態遷移回路３０に入力される。
【００２９】
ステートマシン回路２０全体の動作としては、リセット直後にＳＴＡＴＥ０となり、カウンタ２１の出力値ｃｏｕｎｔ１がリセットされ、リセット解除後にカウンタ２１がカウントアップ開始する。入力データｉｎｄａｔａ＝“００１”かつｃｏｕｎｔ１＝ｃｎｔ＿ｖａｌ１となった時に、ＳＴＡＴＥ１へ状態遷移し、カウンタ２３の出力値ｃｏｕｎｔ２がリセットされる。その後、ｃｏｕｎｔ２がカウントアップされ、入力データｉｎｄａｔａ＝“０１０”かつｃｏｕｎｔ２＝ｃｎｔ＿ｖａｌ２となった時に、ＳＴＡＴＥ２へ状態遷移し、カウンタ２５の出力値ｃｏｕｎｔ３がリセットされる。その後、ｃｏｕｎｔ３がカウントアップされ、入力データｉｎｄａｔａ＝“１００”かつｃｏｕｎｔ３＝ｃｎｔ＿ｖａｌ３となった時に、ＳＴＡＴＥ３へ状態遷移し、カウンタ２７の出力値ｃｏｕｎｔ４がリセットされる。その後、ｃｏｕｎｔ４がカウントアップされ、入力データｉｎｄａｔａ＝“１０１”かつｃｏｕｎｔ４＝ｃｎｔ＿ｖａｌ４となった時に、ＳＴＡＴＥ０へ状態遷移し、元の状態へ戻る。出力データｏｕｔｄａｔａは、現在の状態（ｃｕｒｒｅｎｔ＿ｓｔａｔｅ）に従って、ＳＴＡＴＥ０の時は、“００”、ＳＴＡＴＥ１の時は、“０１”、ＳＴＡＴＥ２の時は、“１０”、ＳＴＡＴＥ３の時は、“１１”を出力する。
【００３０】
ステートマシン回路２０内のカウンタ２１，２３，２５，２７は、単純に、状態遷移値であるｃｎｔ＿ｖａｌ１、ｃｎｔ＿ｖａｌ２、ｃｎｔ＿ｖａｌ３、ｃｎｔ＿ｖａｌ４までカウントする動作のため、状態遷移値は、カウンタ２１，２３，２５，２７の最大値に設定する必要はなく、状態遷移が支障なく可能な範囲で小さい値に設定すればよい。こうすることで、状態数を減らすことができ、形式的論理検証による検証を効率良くかつ高精度に行うことが可能になる。そして、この検証結果を踏まえて、再設計も可能となり、設計ミスの少ない論理回路を作成できる。
【図面の簡単な説明】
【００３１】
【図１】本発明に係る論理回路設計装置の一例を示すブロック図である。
【図２】論理回路設計装置の動作を示すフローチャートである。
【図３】設計された論理回路の概念を示すブロック図である。
【図４】設計された論理回路の具体的回路を示す回路図である。
【図５】従来のステートマシン回路の構成の一例を示すブロック図である。
【図６】従来のステートマシン回路の各ステートにおける移行条件を示す表である。
【図７】従来のステートマシン回路の各ステートにおけるリセットとカウントアップの条件を示す表である。
【図８】従来のステートマシン回路の各ステートにおける出力データを示す表である。
【符号の説明】
【００３２】
８    設計仕様書
１０  論理回路設計装置
１２  論理回路設計部
１３  プロパティ生成部
１４  論理回路データ記憶部
１５  プロパティデータ記憶部
１６  形式的論理検証部
１７  検証結果分析部
２０  ステートマシン回路
２１，２３，２５，２７  カウンタ
２２，２４，２６，２８  比較器
３０  状態遷移回路
１００  ステートマシン回路
【図１】
2008304960.tif 000003
【図２】
2008304960.tif 000004
【図３】
2008304960.tif 000005
【図４】
2008304960.tif 000006
【図５】
2008304960.tif 000007
【図６】
2008304960.tif 000008
【図７】
2008304960.tif 000009
【図８】
2008304960.tif 000010