(57)【要約】【課題】ステートマシンのデッドロックを検出し、回路の品質を向上させることができる回路設計の検証方法および検証プログラムの提供を図る。【解決手段】検証対象の回路記述から相互に依存関係がある複数のステートマシンを取り出し(OPA)、該取り出した複数のステートマシンの遷移を合成して１つの遷移図を生成し(OPB)、該生成した遷移図の各ステートがアイドル状態に遷移できるかどうかを検証する第１検証プロパティを生成し(OPC)、該生成した第１検証プロパティを前記取り出した複数のステートマシンに挿入して形式的検証を行い(OPD, OPE)、前記第１検証プロパティを前記取り出した複数のステートマシンに挿入して行う前記形式的検証の結果、前記第１検証プロパティに違反が見られれば、当該第１検証プロパティから、実際の回路においてデッドロックが発生するかどうかを検証する第２検証プロパティを生成する(OPF)ように構成する。【選択図】図２
2011134242.tif 000002
【特許請求の範囲】
【請求項１】
検証対象の回路記述から相互に依存関係がある複数のステートマシンを取り出し、
該取り出した複数のステートマシンの遷移を合成して１つの遷移図を生成し、
該生成した遷移図の各ステートがアイドル状態に遷移できるかどうかを検証する第１検証プロパティを生成し、
該生成した第１検証プロパティを前記取り出した複数のステートマシンに挿入して形式的検証を行い、
前記第１検証プロパティを前記取り出した複数のステートマシンに挿入して行う前記形式的検証の結果、前記第１検証プロパティに違反が見られれば、当該第１検証プロパティから、実際の回路においてデッドロックが発生するかどうかを検証する第２検証プロパティを生成することを特徴とする回路設計の検証方法。
【請求項２】
請求項１に記載の検証方法において、
前記第１検証プロパティを前記取り出した複数のステートマシンに挿入して行う前記形式的検証の結果、前記第１検証プロパティに違反が見られなければ、前記取り出した複数のステートマシンは、デッドロックを発生しないと判断することを特徴とする回路設計の検証方法。
【請求項３】
請求項１または２に記載の検証方法において、さらに、
前記生成した第２検証プロパティを前記検証対象の回路記述に挿入して形式的検証またはシミュレーションを行うことを特徴とする回路設計の検証方法。
【請求項４】
請求項３に記載の検証方法において、さらに、
前記第２検証プロパティを前記検証対象の回路記述に挿入して行う前記形式的検証またはシミュレーションの結果、前記第２検証プロパティに違反が見られれば、前記取り出した複数のステートマシンはデッドロックを発生すると判断し、前記第２検証プロパティに違反が見られなければ、前記取り出した複数のステートマシンはデッドロックを発生しないと判断することを特徴とする回路設計の検証方法。
【請求項５】
コンピュータに、
検証対象の回路記述から相互に依存関係がある複数のステートマシンを取り出す手順と、
該取り出した複数のステートマシンの遷移を合成して１つの遷移図を生成する手順と、
該生成した遷移図の各ステートがアイドル状態に遷移できるかどうかを検証する第１検証プロパティを生成する手順と、
該生成した第１検証プロパティを前記取り出した複数のステートマシンに挿入して形式的検証を行う手順と、
前記第１検証プロパティを前記取り出した複数のステートマシンに挿入して行う前記形式的検証の結果、前記第１検証プロパティに違反が見られれば、当該第１検証プロパティから、実際の回路においてデッドロックが発生するかどうかを検証する第２検証プロパティを生成する手順と、を実行させることを特徴とする回路設計の検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路設計の検証方法および検証プログラムに関する。
【背景技術】
【０００２】
近年、半導体集積回路の製造技術の進歩に伴って、半導体基板における回路の集積度が向上し、また、同一の半導体チップに対して様々な回路が搭載されるようになってきている。
【０００３】
従来、論理回路設計の検証方法は、例えば、検証項目を抽出した後、人手でチェッカを作成し、そのチェッカを用いてシミュレーション検証または形式的検証を行うものであった。
【０００４】
ところで、従来、プロパティ検証に要する時間を短縮することのできるＬＳＩ設計検証装置、並びに、モジュール毎のプロパティを検証してモジュール間インタフェース仕様の最適化を行うＬＳＩ設計検証方法が提案されている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００８−１８１２１０号公報
【特許文献２】特開２００３−１９６３４２号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
上述したように、従来、論理回路設計の検証方法は、例えば、検証項目を抽出した後、人手でチェッカを作成し、そのチェッカを用いてシミュレーション検証または形式的検証を行っていた。
【０００７】
しかしながら、そのような検証方法だと、ステートマシンのデッドロックを検出するためのチェッカを作成することが難しく、また、検証項目を抽出する時点で検証項目の漏れが生じてステートマシンの検証が行われない虞れもあった。その結果、従来、ステートマシンのデッドロックを検出することは困難となっていた。
【課題を解決するための手段】
【０００８】
一実施形態の回路設計の検証方法によれば、検証対象の回路記述から相互に依存関係がある複数のステートマシンを取り出し、該取り出した複数のステートマシンの遷移を合成して１つの遷移図を生成する。
【０００９】
さらに、該生成した遷移図の各ステートがアイドル状態に遷移できるかどうかを検証する第１検証プロパティを生成し、該生成した第１検証プロパティを前記取り出した複数のステートマシンに挿入して形式的検証を行う。
【００１０】
そして、前記形式的検証の結果、前記第１検証プロパティに違反が見られれば、当該第１検証プロパティから、実際の回路においてデッドロックが発生するかどうかを検証する第２検証プロパティを生成する。
【発明の効果】
【００１１】
開示の回路設計の検証方法および検証プログラムは、ステートマシンのデッドロックを検出し、回路の品質を向上させることができるという効果を奏する。
【図面の簡単な説明】
【００１２】
【図１】一実施例の回路設計の検証を行うシステムの一例を示すブロック図である。
【図２】図１の回路設計検証システムにおける動作の一例を説明するための図である。
【図３】図１の回路設計検証システムのハード構成の一例を示すブロック図である。
【図４】ステートマシンの回路記述を取り出す処理の一例を説明するための図である。
【図５】第１検証プロパティの生成処理の一例を説明するための図である。
【図６】第２検証プロパティの生成処理の一例を説明するための図である。
【図７】第２検証プロパティを挿入して行う検証処理の一例を説明するための図である。
【図８】相互に依存関係があるステートマシンを抽出した場合の一実施例を説明するための図である。
【図９】図８に示す２つのステートマシンの遷移を合成して生成した遷移図の一例を示す図である。
【発明を実施するための形態】
【００１３】
以下、添付図面を参照して、回路設計の検証方法および検証プログラムの実施例を詳述する。
【００１４】
図１は一実施例の回路設計の検証を行うシステムの一例を示すブロック図であり、また、図２は図１の回路設計検証システムにおける動作の一例を説明するための図である。
【００１５】
図１において、参照符号１００は回路記述，１０１はステートマシン抽出回路，１０２はステートマシンデータベース，１０３は合成遷移図生成装置，１０４は合成ステートマシン遷移図データベース，および，１０５は第１検証プロパティ生成装置を示している。
【００１６】
ここで、回路記述１００としては、例えば、ＲＴＬ（Register Transfer Level）等によるプロラムレベルの回路記述でもよく、また、ゲートレベルの回路記述でもよい。
【００１７】
さらに、参照符号１０６は第１検証プロパティデータベース，１０７は形式的検証装置，１０８は第２検証プロパティ生成装置，１０９は第２検証プロパティデータベース，および，１１０は検証装置を示している。
【００１８】
図２に示されるように、処理動作が開始すると、オペレーションＯＰＡにおいて、ステートマシン抽出回路１０１により検証対象の論理回路（回路記述１００）から相互に依存関係があるステートマシンを取り出（抽出）し、オペレーションＯＰＢに進む。なお、取り出したステートマシンは、ステートマシンデータベース１０２に格納される。
【００１９】
ここで、相互に依存関係があるステートマシンとは、例えば、各ステートマシン同士が遷移条件である信号を直接、或いは、組み合わせ回路の論理を通って入出力している関係のものを表している。
【００２０】
次に、オペレーションＯＰＢにおいて、合成遷移図生成装置１０３により取り出したステートマシンの遷移を合成して遷移図を生成する。この生成された合成ステートマシン遷移図は、合成ステートマシン遷移図データベース１０４に格納される。
【００２１】
さらに、オペレーションＯＰＣに進んで、第１検証プロパティ生成装置１０５により遷移図の各ステートからアイドル状態（IDLEのステート）に戻ることができるかどうかのプロパティ（第１検証プロパティ：property A）を生成してオペレーションＯＰＤに進む。なお、生成された第１検証プロパティは、第１検証プロパティデータベース１０６に格納される。
【００２２】
オペレーションＯＰＤでは、形式的検証装置１０７により、第１検証プロパティ（property A）を、取り出した複数のステートマシンに挿入して形式的検証（第１検証プロパティが組み込まれた合成ステートマシンの形式的検証）を行う。
【００２３】
さらに、オペレーションＯＰＥに進んで、第１検証プロパティが組み込まれた合成ステートマシンの形式的検証により第１検証プロパティ（property A）に違反（Error）が見られるかどうかを判定する。
【００２４】
オペレーションＯＰＥにおいて、第１検証プロパティが組み込まれた合成ステートマシンの形式的検証により第１検証プロパティに違反が見られると判定されると、オペレーションＯＰＦに進み、違反が見られないと判定されると、処理を終了する。
【００２５】
オペレーションＯＰＦでは、第２検証プロパティ生成装置１０８により、違反が見られると判定された第１検証プロパティから、実際の回路においてデッドロックが発生するかどうかを検証するための第２検証プロパティを生成オペレーションＯＰＧに進む。なお、生成された第２検証プロパティは、第２検証プロパティデータベース１０９に格納される。
【００２６】
オペレーションＯＰＧでは、検証装置１１０により、第２検証プロパティ（property B）を、検証対象の回路記述に挿入して検証を行う。ここで、検証装置１１０により行う検証は、形式的検証またはシミュレーションである。
【００２７】
そして、オペレーションＯＰＧにおいて、第２検証プロパティを検証対象の回路記述に挿入して行う検証の結果、第２検証プロパティに違反が見られなければ、取り出した複数のステートマシンはデッドロックを発生しないと判断して処理を終了する。
【００２８】
図３は図１の回路設計検証システムのハード構成の一例を示すブロック図である。図３において、参照符号２００はバス，２０１はＣＰＵ，２０２はメモリユニット，２０３は表示ユニット，および，２０４は出力ユニットを示している。
【００２９】
また、参照符号２０５は入力ユニット，２０６は通信ユニット，２０７は記憶装置，２０８はドライバ，および，２０９は記憶媒体を示している。
【００３０】
このように、回路設計検証システムは、汎用的なコンピュータにより実現することができ、回路設計の検証プログラムは、このようなコンピュータにより実行される。
【００３１】
なお、回路設計の検証プログラムは、例えば、ＣＤ−ＲＯＭやＤＶＤ等の光ディスクまたは磁気ディスクや磁気テープといった記憶媒体（可搬型記録媒体）２０９によりドライバ２０８を介して提供される。
【００３２】
或いは、通信ユニット２０６によりインターネット等に接続して、回路設計の検証プログラムを、バス２００を介して記憶装置２０７に格納し、その格納されたプログラムを実行することになる。
【００３３】
図４はステートマシンの回路記述を取り出す処理の一例を説明するための図であり、図１中のステートマシン抽出装置１０１により行われる図２中のオペレーションＯＰＡの一例を詳述するものである。
【００３４】
図４に示されるように、ステートマシンの回路記述を取り出す処理が開始すると、オペレーションＯＰＨにおいて、対象となる回路記述におけるステートマシンをすべて抽出して、オペレーションＯＰＩに進む。
【００３５】
さらに、オペレーションＯＰＩでは、各ステートマシンの遷移条件信号を抽出してオペレーションＯＰＪに進む。
【００３６】
オペレーションＯＰＪでは、抽出したステートマシン、並びに、抽出した各ステートマシンの遷移条件信号において、相互に依存関係があるステートマシンのみを抽出する。
【００３７】
このようにして抽出されたステートマシンは、上述したように、図１中のステートマシンデータベース１０２に格納されることになる。
【００３８】
図５は第１検証プロパティの生成処理の一例を説明するための図であり、図１中の第１検証プロパティ生成装置１０５により行われる図２中のオペレーションＯＰＣの一例を詳述するものである。
【００３９】
すなわち、合成遷移図生成装置１０３により複数のステートマシンの遷移を合成した１つの遷移図を生成し、その合成遷移図からすべてのステートがアイドル状態（IDLEステート）に遷移することができるかどうかを検証する第１検証プロパティを生成する。
【００４０】
図５に示されるように、第１検証プロパティの生成処理が開始すると、オペレーションＯＰＫにおいて、各ステートの中からIDLEステートを指定して、オペレーションＯＰＬに進む。
【００４１】
オペレーションＯＰＬでは、IDLEステート以外のすべてのステートを列挙し、さらに、オペレーションＯＰＭに進んで、always（IDLEステート→列挙された各ステート→IDLEステート）となるプロパティ（第１検証プロパティ：property A）を作成する。
【００４２】
このようにして生成された第１検証プロパティは、上述したように、図１中の第１検証プロパティデータベース１０６に格納されることになる。
【００４３】
図６は第２検証プロパティの生成処理の一例を説明するための図であり、図１中の第２検証プロパティ生成装置１０８により行われる図２中のオペレーションＯＰＦの一例を詳述するものである。
【００４４】
すなわち、第１検証プロパティ（property A）は、図４中のオペレーションＯＰＪにより抽出された相互に依存関係があるステートマシンに組み込まれ、図１中の形式的検証装置１０７により形式的検証が行われる。
【００４５】
この形式的検証装置１０７による形式的検証の結果、いずれかの第１検証プロパティに違反が見られれば、この違反の第１検証プロパティから実際の論理回路でデッドロックが発生するかどうかを検証するための第２検証プロパティ（property B）を生成する。
【００４６】
ここで、実際の論理回路でデッドロックが発生するかどうかの検証は、違反が見られた第１検証プロパティのステートに遷移するかどうかの検証に相当する。
【００４７】
図６に示されるように、第２検証プロパティの生成処理が開始すると、オペレーションＯＰＮにおいて、違反があった第１検証プロパティを抽出して、オペレーションＯＰＯに進む。
【００４８】
オペレーションＯＰＯでは、always（IDLEステート→列挙された各ステート→IDLEステート）となっているプロパティ（第１検証プロパティ：property A）の中で "列挙されたステート" の部分を抽出する。
【００４９】
さらに、オペレーションＯＰＰに進んで、never（"列挙された各ステート"）となる第２検証プロパティ（property B）を作成して処理を終了する。
【００５０】
このようにして生成された第２検証プロパティは、上述したように、図１中の第２検証プロパティデータベース１０９に格納されることになる。
【００５１】
そして、第２検証プロパティデータベース１０９に格納された第２検証プロパティ（property B）は、検証対象の回路記述に組み込まれ、図１中の検証装置１１０による検証が行われる。
【００５２】
図７は第２検証プロパティを挿入して行う検証処理の一例を説明するための図であり、図１中の検証装置１１０により行われる図２中のオペレーションＯＰＧの一例を詳述するものである。
【００５３】
図７に示されるように、第２検証プロパティを挿入して行う検証処理が開始すると、オペレーションＯＰＱにおいて、生成されたプロパティを検証環境に組み込んでオペレーションＯＰＲに進む。
【００５４】
オペレーションＯＰＲでは、検証装置１１０により、全体の回路に対する検証を行って処理を終了する。
【００５５】
ここで、検証装置１１０による検証は、例えば、形式的検証或いはシミュレーションである。これを対象回路全体に対して組み込み形式的検証またはシミュレーション検証を行うことでデッドロックを検出する。
【００５６】
以上において、各オペレーションは、フローチャートにおける各ステップであってもよい。
【００５７】
図８は相互に依存関係があるステートマシンを抽出した場合の一実施例を説明するための図であり、図８（ａ）は "A State machine" を示し、また、図８（ｂ）は "B State machine" を示している。
【００５８】
ここで、図８（ａ）および図８（ｂ）において、参照符号 "I" はIDLEステート（アイドル状態）を表し、"W" はWRITEステート（書き込み状態）を表し、そして、"R" はREADYステート（レディ状態）を表す。
【００５９】
すなわち、図８（ａ）は、IDLEステート "I" およびWRITEステート "W" 間で遷移する "A State machine" を示し、また、図８（ｂ）は、IDLEステート "I"，WRITEステート "W" およびREADYステート "R" 間で遷移する "B State machine" を示している。
【００６０】
なお、図８（ｂ）に示す "B State machine" において、e ＝ A State ＝＝ I & a、および、b ＝ B State ＝＝ W & 〜 f & 〜 h が成立している。
【００６１】
図９は図８に示す２つのステートマシンの遷移（図８（ａ）および図８（ｂ））を合成して生成した遷移図の一例を示す図である。なお、図９において、図８（ａ）および図８（ｂ）の各ステートマシンのIDLEステートの組み合わせが "AI & BI" であるため、"AI & BI" がIDLEステートを表している。
【００６２】
図９からすべてのステートを抽出し、１つのステートからIDLEステートに戻ることができるかどうかを検証するプロパティを生成する。
【００６３】
property１：assert always(｛(AI & BI)；〜(AI & BI)[*]；(AW & BW)｝|=>
｛〜(AI & BI)[*]；(AI & BI)｝)；
property２：assert always(｛(AI & BI)；〜(AI & BI)[*]；(AW & BR)｝|=>
｛〜(AI & BI)[*]；(AI & BI)｝)；
property３：assert always(｛(AI & BI)；〜(AI & BI)[*]；(AI & BW)｝|=>
｛〜(AI & BI)[*]；(AI & BI)｝)；
property４：assert always(｛(AI & BI)；〜(AI & BI)[*]；(AW & BI)｝|=>
｛〜(AI & BI)[*]；(AI & BI)｝)；
【００６４】
property１〜４は、第１検証プロパティ（property A）に対応し、それぞれ抽出した相互に依存関係があるステートマシン（取り出した複数のステートマシン）に挿入されて形式的検証を行うことになる。
【００６５】
このとき、例えば、property４を組み込んで行った形式的検証が Errorとなった場合、すなわち、property４を組み込んで行った形式的検証の結果、第１検証プロパティ（property A）に違反が見られた場合を考える。
【００６６】
ここで、ステートマシンは、各ステートの遷移条件である信号の動作条件に制限がないため、実際の回路では、遷移しないステートに遷移している可能性がある。そのため、実際の回路でデッドロックするかどうかの検証を行う。
【００６７】
すなわち、property４から、次のような、実際の回路（検証対象の回路記述）でデッドロックが発生するかどうか（Errorとなったプロパティのステートに遷移するかどうか）を検証するproperty５（第２検証プロパティ（property B））を生成する。
property５：assert never｛(AW & BI)｝；
【００６８】
そして、検証対象の回路記述に対して、property５を組み込んだ形式的検証またはシミュレーション検証を行えば、ステートマシンの遷移がデッドロックしてしまう回路を検出することが可能になる。
【００６９】
すなわち、ステートマシンのデッドロックを検出することにより、回路の品質を向上させることができる。
【００７０】
なお、図８および図９を参照した説明は単なる例であり、様々な相互に依存関係がある複数のステートマシンを抽出した場合に対しても本実施例を適用することができるのはいうまでもない。
【００７１】
また、上述した回路設計の検証方法は、前述した図３に示すようなハード構成（コンピュータ）により実行されるプログラムとして提供することもできる。
【符号の説明】
【００７２】
１００    回路記述
１０１    ステートマシン抽出回路
１０２    ステートマシンデータベース
１０３    合成遷移図生成装置
１０４    合成ステートマシン遷移図データベース
１０５    第１検証プロパティ生成装置
１０６    第１検証プロパティデータベース
１０７    形式的検証装置
１０８    第２検証プロパティ生成装置
１０９    第２検証プロパティデータベース
１１０    検証装置
２００    バス
２０１    ＣＰＵ
２０２    メモリユニット
２０３    表示ユニット
２０４    出力ユニット
２０５    入力ユニット
２０６    通信ユニット
２０７    記憶装置
２０８    ドライバ
２０９    記憶媒体
【図１】
2011134242.tif 000003
【図２】
2011134242.tif 000004
【図３】
2011134242.tif 000005
【図４】
2011134242.tif 000006
【図５】
2011134242.tif 000007
【図６】
2011134242.tif 000008
【図７】
2011134242.tif 000009
【図８】
2011134242.tif 000010
【図９】
2011134242.tif 000011