(57)【特許請求の範囲】
【請求項１】
明示されない状態遷移元からの状態遷移が記述可能であり、且つ前記明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証装置であって、
前記有限状態機械のすべての状態遷移先を抽出する状態遷移先抽出手段と、
前記有限状態機械のすべての値が明示された状態遷移元を抽出する状態遷移元抽出手段と、
前記抽出された状態遷移先に含まれるが、前記抽出された状態遷移元に含まれない状態遷移先を、前記有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出する状態遷移先差分抽出手段と
を備えることを特徴とする設計検証装置。
【請求項２】
前記設計仕様は、レジスタ転送レベル言語を用いて記述されたことを特徴とする請求項１に記載の設計検証装置。
【請求項３】
前記レジスタ転送レベル言語は、Ｖｅｒｉｌｏｇ（登録商標）又はＩＥＥＥ（Institute of Electrical and Electronics Engineers）１０７６で規定されたＶＨＤＬであり、
状態遷移先抽出手段は、前記設計仕様中のｃａｓｅ文におけるステート信号の代入文から状態遷移先を抽出し、
状態遷移元抽出手段は、前記設計仕様中のｃａｓｅ文における値が明示された分岐条件から状態遷移元を抽出する
ことを特徴とする請求項２に記載の設計検証装置。
【請求項４】
前記明示されない状態遷移元からの状態遷移は、ｄｅｆａｕｌｔ文又はｏｔｈｅｒｓ文として記述されることを特徴とする請求項３に記載の設計検証装置。
【請求項５】
明示されない状態遷移元からの状態遷移が記述可能であり、且つ前記明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証装置において、
前記有限状態機械のすべての状態遷移先を抽出し、
前記有限状態機械のすべての値が明示された状態遷移元を抽出し、
前記抽出された状態遷移先に含まれるが、前記抽出された状態遷移元に含まれない状態遷移先を、前記有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出する
ことを特徴とする設計検証方法。
【請求項６】
明示されない状態遷移元からの状態遷移が記述可能であり、且つ前記明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証プログラムであって、
前記有限状態機械のすべての状態遷移先を抽出する状態遷移先抽出処理と、
前記有限状態機械のすべての値が明示された状態遷移元を抽出する状態遷移元抽出処理と、
前記抽出された状態遷移先に含まれるが、前記抽出された状態遷移元に含まれない状態遷移先を、前記有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出する状態遷移先差分抽出処理と
をコンピュータに実行させることを特徴とする設計検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、有限状態機械の設計仕様の検証時に、有限状態機械のデッドロックを検出する設計検証装置、設計検証方法、及び設計検証プログラムに関する。
【背景技術】
【０００２】
近年、ＬＳＩ（Large Scale Integration、ＳＯＣ（System-On-a-Chip、ＦＰＧＡ（Field Programmable Gate Array）等の開発において、ディジタル回路はレジスタ転送レベル（ＲＴＬ：Register Transfer Level）の手法を用いて設計されることが多い。ＲＴＬによる設計では、ディジタル回路の動作は、レジスタ間の信号の流れと、信号の流れに対する論理演算の組み合わせにより記述される。ＲＴＬでは、ディジタル回路は、Ｖｅｒｉｌｏｇ（登録商標）、ＩＥＥＥ（Institute of Electrical and Electronics Engineers）１０７６において規定されたＶＨＤＬ等の、ＲＴＬ用のハードウェア記述言語（以下、「ＲＴＬ言語」という。）を用いて記述される。
【０００３】
ＲＴＬ言語によるディジタル回路の記述は、有限状態機械（ＦＳＭ：Finite State Machine）を含むことがある。有限状態機械とは、有限個の状態と状態遷移の組み合わせにより記述される動作モデルである。ディジタル回路の有限状態機械に相当する部分は「デッドロック」（Deadlock）を起こさない設計になっていることが必要である。「デッドロック」とは、プロセス等の複数の処理単位が互いの処理の終了を待つ結果、どの処理単位も先の処理を実行することができなくなることである。
【０００４】
ディジタル回路の設計作業を支援するための、ＥＤＡ（Electronic Design Automation）ツールの多くは、ＦＳＭ回路の検出を行うことができる。特に、ＥＤＡツールの一種である形式的検証（Formal Verification）ツールは、静的にＦＳＭ回路のデッドロックを検出することができる。形式的検証とは、ディジタル回路の形式仕様記述に基づいて、ディジタル回路が正しいこと又は正しくないことを証明することである。形式的検証ツールを用いることにより、設計者は、ディジタル回路が意図しない状態に陥り、ディジタル回路が正常に動作しないという問題の多くを回避することができる。
【０００５】
形式的検証では、テストパターンを必要とすることなく、設計仕様の検証が可能である。そのため、形式的検証による検証精度は、設計検証者のスキルに対する依存性が低い。
【０００６】
有限状態機械の設計仕様を検証する際に、有限状態機械のデッドロックを検出する技術の一例が、特許文献１に開示されている。
【０００７】
特許文献１のデッドロック検証装置は、入力手段、変換手段、検証手段、及び出力手段を含む。入力手段は、検証対象であるシステムにおける各プロセス間の関連及び各プロセスの状態遷移を図形として入力する。変換手段は、入力手段からの入力に基づいて、各プロセスに関連するイベントの情報、各プロセスの各状態においてイベントが生じた場合の状態の遷移及び当該状態が正常終了状態であるか否かの情報、「拒否集合」の情報を生成し、出力する。「拒否集合」とは、各プロセスの各状態において生じる可能性のないイベントの情報である。検証手段は、出力された情報に基づいて、各プロセスの各遷移状態において、デッドロックが生じるか否かを順次判定する。出力手段は、検証結果を出力する。
【０００８】
特許文献１のデッドロック検証装置は、以下のように動作する。検証手段は、
ａ）各プロセスが特定状態の時に、特定状態において生じる可能性のあるイベントがあるか否かを演算し、ｂ）生じる可能性のあるイベントがなく、且つ特定状態が正常終了状態でない場合には、デッドロックが生じると判断し、生じる可能性のあるイベントがある場合には、一つのイベントを順次選択し、ｃ）選択されたイベントが生じた場合の各プロセスの遷移状態を演算し、当該遷移状態を特定状態としてａ）以下の処理を繰り返す。
なお、検証手段は、発生可能イベントを、各プロセスに関連するイベントの和集合から、各プロセスの現在の状態における拒否集合の和集合を減算して算出する。
【０００９】
上記動作の結果、特許文献１のデッドロック検証装置は、検証対象であるシステムにおいて、デッドロックが生じるか否かを判定する。
【００１０】
さて、ＦＳＭの状態遷移条件がＲＴＬ言語で記述される場合には、「ｃａｓｅ文」が使用されることが多い。「ｃａｓｅ文」は、多分岐の条件分岐を表現するコードである。ｃａｓｅ文では、分岐条件を規定する値が明示された条件分岐、及びその他の分岐条件が明示されない条件分岐が記述可能である。「ｄｅｆａｕｌｔ文」はＶＨＤＬのｃａｓｅ文における、分岐条件が明示されない条件分岐を記述するためのコードである。同様に、「ｏｔｈｅｒｓ文」はＶｅｒｉｌｏｇのｃａｓｅ文における、分岐条件が明示されない条件分岐を記述するためのコードである。ｃａｓｅ文は、ディジタル回路のＦＳＭ回路部分以外の部分の設計仕様における、一般的な条件分岐の記述にも利用される。
【００１１】
形式的検証ツールは、ｃａｓｅ文を検証した結果、実現されない条件分岐が存在する場合に、その条件分岐を「デッドコード」として検出することがある。「デッドコード」とは、実際に機能することがない設計仕様の部分である。
【００１２】
ｃａｓｅ文の条件分岐の記述において、全ての分岐条件が明示的に記述されている場合には、形式的検証ツールは、例えば、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文をデッドコードとして検出する。一方、設計者がｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文に分岐することを意図して、一部の分岐条件のみが明示的に記述される場合には、形式的検証ツールは、「ｏｔｈｅｒｓ文」や「ｄｅｆａｕｌｔ文」をデッドコードとして検出しない。
【００１３】
さて、検証された設計仕様からディジタル回路が合成される際には、論理合成ツールが、設計仕様をゲートレベルのネットリストに変換する。この際、利用者が特別な指示を行わなければ、論理合成ツールは、ＦＳＭ回路の状態遷移条件を記述したｃａｓｅ文中のｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文を合成の対象にしない。すなわち、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文により記述された状態遷移は、ディジタル回路として合成されない。その理由は、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文により記述された機能を合成の対象にすると、合成されるディジタル回路の回路規模が非常に大きくなるからである。
【００１４】
ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文により記述された機能を合成の対象に指定するためには、利用者は、仕様記述中に論理合成ツールに依存する特別な指示を挿入するか、論理合成ツールに対する特別な指示を有効にする必要がある。ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文により記述された機能を合成の対象に指定するための特別な指示は、例えば、「ａｔｔｒｉｂｕｔｅ記述」（ＶＨＤＬの場合）や「ｄｉｒｅｃｔｉｖｅ記述」（Ｖｅｒｉｌｏｇの場合）である。
【００１５】
ユーザが特別な指示を怠ると、論理合成ツールは、ＦＳＭ回路の状態遷移条件が記述されたｃａｓｅ文中の、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文により記述された状態遷移が含まれないＦＳＭ回路を合成する可能性がある。つまり、合成されたＦＳＭ回路は、合成されなかった状態遷移を実行しないために、デッドロックに陥る可能性を有する。
【００１６】
そのため、ＦＳＭ回路の状態遷移条件が記述されたｃａｓｅ文は、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文に分岐するｃａｓｅ文であるべきではない。すなわち、ＦＳＭ回路の状態遷移条件が記述されたｃａｓｅ文では、ｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文がデッドコードであるべきである。もしＦＳＭ回路の設計仕様が上記制約を満たさない場合には、設計仕様から合成されるＦＳＭ回路は、デッドロックに陥る可能性を有する。
【先行技術文献】
【特許文献】
【００１７】
【特許文献１】特開平６−２１４８１２
【発明の概要】
【発明が解決しようとする課題】
【００１８】
ところが、既存の形式的検証ツールは、論理合成ツールにより、ＦＳＭ回路の設計仕様中のｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文に対応する状態遷移がディジタル回路として合成されないことに起因する、ＦＳＭ回路のデッドロックが発生する可能性を検出しない。つまり、形式的検証ツールによりデッドロックが検出されない設計仕様であっても、設計仕様から合成されるＦＳＭ回路がデッドロックに陥る可能性がある。
【００１９】
そのため、設計段階では、ＲＴＬのコーディングスタイルをマニュアル化する等の手法により、デッドロックを回避することが行われることがある。しかしながら、この方法では、設計者のスキルに依存して、仕様記述の品質にばらつきが生じるという問題がある。あるいは、合成されたディジタル回路の試験等により、ＦＳＭ回路にデッドロックが無いことを確認することが行われることがある。しかしながら、この方法では、開発期間や開発費用が増加するという問題がある。
【００２０】
以上説明したように、形式的検証ツールは、ＦＳＭ回路の設計仕様を記述したｃａｓｅ文において、全ての分岐条件が明示的に記述されていないことをエラーとして検出しない。一方、論理合成ツールは、ＦＳＭ回路の設計仕様を記述したｃａｓｅ文において、分岐条件が明示的に記述されない分岐条件に対応する状態遷移をディジタル回路の合成対象にしないことがある。そのため、論理合成ツールにより合成対象にされない状態遷移の存在に起因して、論理合成ツールにより合成されるディジタル回路に、デッドロックが発生する可能性がある。従って、形式的検証ツールには、明示されない状態遷移元からの状態遷移が設計仕様に記述可能であり、且つ設計仕様に基づく回路の合成時に明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様を検証する際に、有限状態機械におけるデッドロックが検出されない可能性があるという問題がある。
（発明の目的）
本発明の主たる目的は、明示されない状態遷移元からの状態遷移が設計仕様に記述可能であり、且つ設計仕様に基づく回路の合成時に明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様を検証する際に、有限状態機械におけるデッドロック検出の可能性を向上させることができる有限状態機械の設計検証装置、設計検証方法、及び設計検証プログラムを提供することにある。
【課題を解決するための手段】
【００２１】
本発明の設計検証装置は、明示されない状態遷移元からの状態遷移が記述可能であり、且つ明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証装置であって、有限状態機械のすべての状態遷移先を抽出する状態遷移先抽出手段と、有限状態機械のすべての値が明示された状態遷移元を抽出する状態遷移元抽出手段と、抽出された状態遷移先に含まれるが、抽出された状態遷移元に含まれない状態遷移先を、有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出する状態遷移先差分抽出手段とを備えることを特徴とする。
【００２２】
本発明の設計検証方法は、明示されない状態遷移元からの状態遷移が記述可能であり、且つ明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証装置において、有限状態機械のすべての状態遷移先を抽出し、有限状態機械のすべての値が明示された状態遷移元を抽出し、抽出された状態遷移先に含まれるが、抽出された状態遷移元に含まれない状態遷移先を、有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出することを特徴とする。
【００２３】
本発明の設計検証プログラムは、明示されない状態遷移元からの状態遷移が記述可能であり、且つ明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様の検証を行う設計検証装置において、有限状態機械のすべての状態遷移先を抽出する状態遷移先抽出処理と、有限状態機械のすべての値が明示された状態遷移元を抽出する状態遷移元抽出処理と、抽出された状態遷移先に含まれるが、抽出された状態遷移元に含まれない状態遷移先を、有限状態機械のデッドロックを発生させる可能性がある状態遷移先として抽出する状態遷移先差分抽出処理とをコンピュータに実行させることを特徴とする。
【発明の効果】
【００２４】
本発明によれば、明示されない状態遷移元からの状態遷移が設計仕様に記述可能であり、且つ設計仕様に基づく回路の合成時に明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様を検証する際に、有限状態機械におけるデッドロック検出の可能性を向上させることができるという効果がある。
【図面の簡単な説明】
【００２５】
【図１】本発明の第１の実施形態における設計検証装置１００の構成の一例を示すブロック図である。
【図２】本発明の第１の実施形態における設計検証装置１００の動作を示すフローチャートである。
【図３】本発明の第１の実施形態における設計検証装置１００の動作の具体例を説明するための図である。
【図４】本発明の第２の実施形態における設計検証装置１１０の構成の一例を示すブロック図である。
【図５】本発明の第２の実施形態における設計検証装置１１０の動作を示すフローチャートである。
【図６】本発明の第２の実施形態における設計仕様２１０の具体例を示す図である。
【図７】本発明の第２の実施形態における設計仕様２１０に対応するタイミングチャートを示す図である。
【図８】本発明の第２の実施形態における設計検証装置１１０の状態遷移先抽出手段１１１の動作の具体例を説明するための図である。
【図９】本発明の第２の実施形態における設計検証装置１１０の状態遷移元抽出手段１１２及び状態遷移先差分抽出手段１１３の動作の具体例を説明するための図である。
【発明を実施するための形態】
【００２６】
以下、本発明の実施形態について、図面を参照して詳細に説明する。なお、すべての図面において、同等の構成要素には同じ符号を付し、適宜説明を省略する。
（第１の実施形態）
本実施形態における構成について説明する。
【００２７】
図１は、本発明の第１の実施形態における設計検証装置１００の構成の一例を示すブロック図である。
【００２８】
設計検証装置１００は、ＦＳＭ回路を含むディジタル回路の設計仕様２００を入力して、状態遷移先差分３００を抽出する。状態遷移先差分３００は、ＦＳＭ回路の設計仕様において明示されない状態遷移元への、状態遷移に起因する、ＦＳＭ回路のデッドロックを引き起こす可能性のある状態に関する情報である。設計検証装置１００は、状態遷移先抽出手段１０１、状態遷移元抽出手段１０２、及び状態遷移先差分抽出手段１０３を有する。
【００２９】
状態遷移先抽出手段１０１は、設計仕様２００から、ＦＳＭ回路の設計仕様において明示された状態遷移先を抽出する。
【００３０】
状態遷移元抽出手段１０２は、設計仕様２００から、ＦＳＭ回路の設計仕様において明示された状態遷移元を抽出する。
【００３１】
状態遷移先差分抽出手段１０３は、抽出された状態遷移先から、抽出された状態遷移元を除いた差分である、状態遷移先差分３００を抽出する。
【００３２】
次に、本実施形態における動作について説明する。
【００３３】
図２は、本発明の第１の実施形態における設計検証装置１００の動作を示すフローチャートである。なお、図２に示すフローチャート及び以下の説明は一例であり、適宜求める処理に応じて、処理順等を入れ替えたり、処理を戻したり、又は処理を繰り返したりしてもよい。
【００３４】
状態遷移先抽出手段１０１は、設計仕様２００から、ＦＳＭ回路の設計仕様において明示された状態遷移先を抽出する（ステップＳ１０１）。
【００３５】
状態遷移元抽出手段１０２は、設計仕様２００から、ＦＳＭ回路の設計仕様において明示された状態遷移元を抽出する（ステップＳ１０２）。
【００３６】
状態遷移先差分抽出手段１０３は、抽出された状態遷移先から、抽出された状態遷移元を除いた差分である、状態遷移先差分３００を抽出する（ステップＳ１０３）。
【００３７】
次に、本発明の第１の実施形態の処理の具体例について説明する。
【００３８】
図３は、本発明の第１の実施形態における設計検証装置１００の動作の具体例を説明するための図である。
【００３９】
図３（ａ）は、設計仕様２００に含まれる、ＦＳＭ回路の設計仕様の一部である状態遷移条件を示す。１番目の状態遷移条件“条件１”では、明示された状態遷移元“状態０”から、明示された状態遷移先“状態１”への状態遷移が記述されている。２番目の状態遷移条件“条件２”では、明示された状態遷移元“状態１”から、明示された状態遷移先“状態１”及び“状態２”への状態遷移が記述されている。３番目の状態遷移条件“条件３”では、明示されない状態遷移元“その他”から、明示された状態遷移先“状態０”への状態遷移が記述されている。
【００４０】
図３（ｂ）は、設計検証装置１００の各手段が抽出する情報を示す。図３（ｂ）の第１列は、状態遷移元抽出手段１０２により抽出される状態遷移元を示す。図３（ｂ）の第２列は、状態遷移先抽出手段１０１により抽出される状態遷移先を示す。図３（ｂ）の第３列は、状態遷移先差分抽出手段１０３により抽出される状態遷移先差分３００を示す。
【００４１】
状態遷移先抽出手段１０１は、１番目の状態遷移条件“条件１”から、明示された状態遷移先“状態１”を抽出する。状態遷移先抽出手段１０１は、２番目の状態遷移条件“条件２”から、明示された状態遷移先“状態１”及び“状態２”を抽出する。状態遷移先抽出手段１０１は、３番目の状態遷移条件“条件３”から、明示された状態遷移先“状態０”を抽出する。つまり、状態遷移先抽出手段１０１は、全ての状態遷移条件から、明示された状態遷移先“状態０”、“状態１”及び“状態２”を抽出する（ステップＳ１０１）。
【００４２】
状態遷移元抽出手段１０２は、１番目の状態遷移条件“条件１”から、明示された状態遷移元“状態０”を抽出する。状態遷移元抽出手段１０２は、２番目の状態遷移条件“条件２”から、明示された状態遷移元“状態１”を抽出する。状態遷移元抽出手段１０２は、３番目の状態遷移条件“条件３”は、状態遷移元は“その他”であり、明示された状態遷移元を含まないので、いずれの状態も抽出しない。つまり、状態遷移元抽出手段１０２は、全ての状態遷移条件から、明示された状態遷移元“状態０”及び“状態１”を抽出する（ステップＳ１０２）。
【００４３】
状態遷移先差分抽出手段１０３は、抽出された状態遷移先“状態０”、“状態１”及び“状態２”から、抽出された状態遷移元“状態０”及び“状態１”を除いた差分である状態“状態２”を、状態遷移先差分３００として抽出する（ステップＳ１０３）。
【００４４】
さて、設計仕様からディジタル回路が合成される際には、論理合成ツールが、設計仕様をゲートレベルのネットリストに変換する。この際、利用者が特別な指示を行わなければ、論理合成ツールは、ＦＳＭ回路の、状態遷移元が明示されない状態遷移を合成の対象にしない。すなわち、本具体例においては、状態遷移条件“条件３”により記述された状態遷移は、ディジタル回路として合成されない。その結果、合成されたＦＳＭ回路は、一旦、状態“状態２”へ状態遷移すると、他の状態へ状態遷移しない。つまり、合成されたＦＳＭ回路は、状態“状態２”において、デッドロックに陥る。
【００４５】
設計検証者は、設計検証装置１００により抽出された状態遷移先差分３００を参照することにより、設計仕様２００から合成されるＦＳＭ回路が、状態“状態２”においてデッドロックに陥る可能性があることを知ることができる。
【００４６】
以上説明したように、論理合成ツールは、ＦＳＭ回路の設計仕様において、状態遷移元が明示されない状態遷移を合成の対象にしないことがある。つまり、論理合成ツールにより合成されるＦＳＭ回路は、状態遷移元が明示されない状態遷移が合成されないことに起因して、デッドロックを有する可能性がある。一方、本実施形態の設計検証装置１００は、ＦＳＭ回路の設計仕様において、明示されない状態遷移元を抽出する。設計検証者は、設計検証装置により抽出された明示されない状態遷移元を参照することにより、設計仕様から合成されるＦＳＭ回路が、特定の状態においてデッドロックに陥る可能性があることを知ることができる。従って、本実施形態の設計検証装置１００は、明示されない状態遷移元からの状態遷移が設計仕様に記述可能であり、且つ設計仕様に基づく回路の合成時に明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様を検証する際に、有限状態機械のデッドロック検出の可能性を向上させることができる。
（第２の実施形態）
次に、上述した第１の実施形態において、特定のＲＴＬ言語を用いて記述された設計仕様を検証して、論理合成ツールにより合成されるＦＳＭ回路がデッドロックに陥る可能性があるか否かの診断メッセージを表示する、本発明の第２の実施形態について説明する。特定のＲＴＬ言語とは、ＶＨＤＬ又はＶｅｒｉｌｏｇである。以下の説明において、第１の実施形態と同等の構成要素には同じ符号を付し、適宜説明を省略する。
【００４７】
まず、以下の説明における前提について説明する。  次に、本実施形態における構成について説明する。
【００４８】
図４は、本発明の第２の実施形態における設計検証装置１１０の構成の一例を示すブロック図である。
【００４９】
設計検証装置１１０は、ＶＨＤＬ又はＶｅｒｉｌｏｇを用いて記述された、ＦＳＭ回路を含むディジタル回路の設計仕様２１０を入力して、診断メッセージ３１０を表示する。診断メッセージ３１０は、ＦＳＭ回路の設計仕様において明示されない、つまり、ｏｔｈｅｒｓ文又はｄｅｆａｕｌｔ文に対応する状態遷移元への、状態遷移に起因する、ＦＳＭ回路のデッドロックの可能性の有無に関する情報である。設計検証装置１１０は、状態遷移先抽出手段１１１、状態遷移元抽出手段１１２、状態遷移先差分抽出手段１１３、及び表示手段１１４を有する。
【００５０】
状態遷移先抽出手段１１１は、設計仕様２１０から、ＦＳＭ回路の設計仕様において明示された状態遷移先を抽出する。
【００５１】
状態遷移元抽出手段１１２は、設計仕様２１０から、ＦＳＭ回路の設計仕様において明示された、つまり、ｏｔｈｅｒｓ文又はｄｅｆａｕｌｔ文に対応しない状態遷移元を抽出する。
【００５２】
状態遷移先差分抽出手段１１３は、抽出された状態遷移先から、抽出された状態遷移元を除いた差分である、状態遷移先差分の情報を抽出する。
【００５３】
表示手段１１４は、状態遷移先差分の情報に基づいて、診断メッセージ３１０を表示する。
【００５４】
次に、本実施形態における動作について説明する。
【００５５】
図５は、本発明の第２の実施形態における設計検証装置１１０の動作を示すフローチャートである。なお、図５に示すフローチャート及び以下の説明は一例であり、適宜求める処理に応じて、処理順等を入れ替えたり、処理を戻したり、又は処理を繰り返したりしてもよい。
【００５６】
状態遷移先抽出手段１１１は、設計仕様２１０から、ＦＳＭ回路の設計仕様を記述するｃａｓｅ文を抽出する（ステップＳ２０１）。
【００５７】
状態遷移先抽出手段１１１は、抽出したｃａｓｅ文から、明示された状態遷移先を含む、ステート信号の代入文を抽出する（ステップＳ２０２）。
【００５８】
状態遷移先抽出手段１１１は、抽出した代入文から、右辺において明示された全ての状態遷移先を抽出し、ソートし、同一の状態遷移先が複数ある場合には、１つを残して削除する（ステップＳ２０３）。
【００５９】
状態遷移元抽出手段１１２は、抽出されたｃａｓｅ文から、ＦＳＭ回路の設計仕様において明示された状態遷移元を抽出する（ステップＳ２０４）。
【００６０】
状態遷移先差分抽出手段１１３は、抽出された状態遷移先から、抽出された状態遷移元を除いた差分の有無を判定する（ステップＳ２０５）。
【００６１】
差分があれば（ステップＳ２０５：Ｙｅｓ）、表示手段１１４は、設計仕様から合成されるＦＳＭ回路がデッドロックに落ちる可能性がある旨の、診断メッセージ３１０を表示する（ステップＳ２０６）。
【００６２】
差分がなければ（ステップＳ２０５：Ｎｏ）、表示手段１１４は、設計仕様から合成されるＦＳＭ回路がデッドロックに落ちる可能性がない旨の、診断メッセージ３１０を表示する（ステップＳ２０７）。
【００６３】
次に、本発明の第２の実施形態の処理の具体例について説明する。
【００６４】
図６は、本発明の第２の実施形態における設計仕様２１０の具体例を示す図である。図６の設計仕様はＶＨＤＬを用いて記述される。なお、説明のために、設計仕様の各行の行頭に行番号を示す。
【００６５】
図６の行３６から行８１のｃａｓｅ文は、ＦＳＭ回路の設計仕様の一部である状態遷移条件を示す。キーワード“ｗｈｅｎ”に続いて記述された値が状態遷移元を、変数“NEXT_STAGE”に代入される値が状態遷移先を示す。行３７から行３９の状態遷移条件では、明示された状態遷移元“０００”から、明示された状態遷移先“００１”への状態遷移が記述される。行４０から行５０の状態遷移条件では、明示された状態遷移元“００１”から、明示された状態遷移先“０１０”、“１００”、又は“００１”への状態遷移が記述される。行５１から行６１の状態遷移条件では、明示された状態遷移元“０１０”から、明示された状態遷移先“０１１”、“０００”、又は“０１０”への状態遷移が記述される。行６２から行６９の状態遷移条件では、明示された状態遷移元“０１１”から、明示された状態遷移先“００１”、又は“０１１”への状態遷移が記述される。行７０から行７７の状態遷移条件では、明示された状態遷移元“１００”から、明示された状態遷移先“１０１”、又は“１００”への状態遷移が記述される。行７８から行８０の状態遷移条件では、明示されない状態遷移元から、明示された状態遷移先“０００”への状態遷移が記述される。
【００６６】
設計仕様に明示された状態遷移元“０００”、“００１”、“０１０”、“０１１”、“１００”のそれぞれは、状態遷移元以外の状態に遷移可能である。更に、設計仕様に明示さない状態遷移元“１０１”は、状態遷移元以外の状態“０００”に遷移可能である。従って、設計仕様の論理上は、デッドロックは発生しない。つまり、一般的な形式的検証ツールは、図６の設計仕様に対して、ＦＳＭ回路のデッドロックを検出しない。
【００６７】
図７は、本発明の第２の実施形態における設計仕様２１０に対応するタイミングチャートを示す。図７は、ＦＳＭ回路の設計者が意図するＦＳＭ回路の信号出力のタイミングチャートである。
【００６８】
図７を用いて、形式的検証ツールがＦＳＭ回路の設計仕様を検証する際の、形式的検証ツールから見たＦＳＭ回路の詳細な動作を説明する。図６の行２６から行３２の“RESETB”信号及び“CLK”信号に対する動作記述に対応して、リセット期間中（“RESETB”信号が“０”）には、図６の行２８の通り、“CURRENT_STATE”信号は状態“０００”へ遷移する。そして、リセット状態が解除された（“RESETB”信号が“１”）次のクロックエッジのタイミングで、図６の行３０、行３８の通り、“CURRENT_STATE”信号は状態“００１”へ遷移する。次のクロックエッジで、図６の行４１と行４４の条件式から行４５の動作に対応して、“CURRENT_STATE”信号は状態“１００”へ遷移する。更に、次のクロックエッジで、図６の行７１の条件式から行７２の動作に対応して、“CURRENT_STATE”信号は状態“１０１”へ遷移する。そして、その次のクロックエッジのタイミングで、図６の行７９の動作に対応して、“CURRENT_STATE”信号は状態“０００”へ遷移する。最後の状態“０００”へ遷移は、図６のｃａｓｅ文に状態“１０１”が遷移元である場合の動作が明示されていないため、図６の行７８の“ｏｔｈｅｒｓ”条件に分岐するために発生する。形式的検証ツールによるＦＳＭ回路の設計仕様の検証において、上述のように“CURRENT_STATE”信号が遷移するため、ＦＳＭ回路のデッドロックは検出されない。
【００６９】
一方、図６の設計仕様からＦＳＭ回路を合成する場合、論理合成ツールは、設計仕様をゲートレベルのネットリストに変換する。このとき、論理合成ツールは、利用者が特別な指示を行わなければ、ＦＳＭ回路の設計仕様中のｏｔｈｅｒｓ文やｄｅｆａｕｌｔ文に対応するディジタル回路を合成しない。つまり、論理合成ツールは、ＦＳＭ回路の設計仕様を記述したｃａｓｅ文において、分岐条件が明示的に記述されない分岐条件に対応する状態遷移、すなわち、状態遷移元“１０１”から状態遷移先“０００”への状態遷移をディジタル回路として合成しない。その結果、合成されたＦＳＭ回路は、状態遷移元“１０１”から他の状態へ状態遷移できない。従って、論理合成ツールにより合成されるＦＳＭ回路には、デッドロックが発生する可能性がある。
【００７０】
図８は、本発明の第２の実施形態における設計検証装置１１０の状態遷移先抽出手段１１１の動作の具体例を説明するための図である。図８（ａ）は、ＦＳＭの設計仕様から抽出された、ＦＳＭ回路の状態遷移先の記述である。図８（ｂ）は、状態遷移先の記述から抽出された状態遷移先である。図８（ｃ）は、抽出された状態遷移先をソートした結果である。図８（ｄ）は、ソートされた状態遷移先から、同一の状態遷移先を１つ残して削除した結果である。なお、図８（ａ）、（ｂ）、（ｃ）では、説明のために、各行の行頭に設計仕様における行番号を示す。
【００７１】
図９は、本発明の第２の実施形態における設計検証装置１１０の状態遷移元抽出手段１１２及び状態遷移先差分抽出手段１１３の動作の具体例を説明するための図である。図９（ａ）は、ＦＳＭの設計仕様から抽出された、ＦＳＭ回路の状態遷移元の記述である。図９（ｂ）は、状態遷移元の記述から抽出された状態遷移元のリストである。図９（ｃ）は、図８（ｄ）に示した、状態遷移先のリストである。図９（ｄ）は、状態遷移先のリストから状態遷移元のリストを除いた状態遷移先の差分のリストである。なお、図９（ａ）では、説明のために、各行の行頭に設計仕様における行番号を示す。
【００７２】
図８及び図９を用いて、設計検証装置１１０の動作の具体例を説明する。
【００７３】
状態遷移先抽出手段１１１は、設計仕様２１０から、ＦＳＭ回路の設計仕様を記述するｃａｓｅ文を抽出し（ステップＳ２０１）、抽出したｃａｓｅ文から、明示された状態遷移先を含むステート信号の代入文を抽出する（ステップＳ２０２、図８（ａ））。
【００７４】
状態遷移先抽出手段１１１は、抽出した代入文から、右辺において明示された全ての状態遷移先を抽出し（図８（ｂ））、ソートし（図８（ｃ））、同一の状態遷移先が複数ある場合には、１つを残して削除する（ユニーク化を行う）（ステップＳ２０３、図８（ｄ））。
【００７５】
状態遷移元抽出手段１１２は、抽出されたｃａｓｅ文から、ＦＳＭ回路の設計仕様において明示された状態遷移元を抽出する（ステップＳ２０４）。
【００７６】
状態遷移先差分抽出手段１１３は、抽出された状態遷移先から、抽出された状態遷移元を除いた差分の有無を判定する（ステップＳ２０５）。
【００７７】
差分があれば（ステップＳ２０５：Ｙｅｓ）、表示手段１１４は、設計仕様中の明示されない状態遷移元からの状態遷移が合成されないことに起因して、ＦＳＭ回路がデッドロックに陥る可能性がある旨の、診断メッセージ３１０を表示する（ステップＳ２０６）。
【００７８】
差分がなければ（ステップＳ２０５：Ｎｏ）、表示手段１１４は、設計仕様中の明示されない状態遷移元からの状態遷移が合成されないことに起因して、ＦＳＭ回路がデッドロックに陥る可能性がない旨の、診断メッセージ３１０を表示する（ステップＳ２０７）。  表示手段１１４は、例えば、状態遷移元“１０１”において、ＦＳＭ回路がデッドロックに陥る可能性がある旨の診断メッセージと、その他の状態遷移元においては、ＦＳＭ回路がデッドロックに陥る可能性がない旨の診断メッセージを表示する。
【００７９】
以上説明したように、論理合成ツールは、ＦＳＭ回路の設計仕様において、状態遷移元が明示されない状態遷移を合成の対象にしないことがある。つまり、論理合成ツールにより合成されるＦＳＭ回路は、状態遷移元が明示されない状態遷移が合成されないことに起因して、デッドロックを有する可能性がある。一方、本実施形態の設計検証装置１１０は、ＦＳＭ回路の設計仕様において、設計仕様から合成されるＦＳＭ回路が、特定の状態においてデッドロックに陥る可能性がある旨を示す診断メッセージを表示する。従って、本実施形態の設計検証装置１１０は、明示されない状態遷移元からの状態遷移が設計仕様に記述可能であり、且つ設計仕様に基づく回路の合成時に明示されない状態遷移元からの状態遷移が回路として合成されないことがある、有限状態機械の設計仕様を検証する際に、有限状態機械のデッドロック検出の可能性を向上させることができる。
【００８０】
なお、明示されない状態遷移元からの状態遷移が合成されないことによるＦＳＭ回路のデッドロックは、論理合成ツールにより合成されたディジタル回路の評価段階又はゲートシミュレーション段階で見つける必要があった。本実施形態の設計検証装置１１０は、明示されない状態遷移元からの状態遷移が合成されないことによるＦＳＭ回路のデッドロックを、設計段階において、しかもＲＴＬシミュレーション以前に検出することができる。従って、本実施形態の設計検証装置１１０は、後工程におけるデバッグに要する時間を大幅に短縮し、前工程における品質を改善することができる。
【００８１】
なお、設計仕様がＶｅｒｉｌｏｇを用いて記述された場合の設計検証装置１１０の動作は、明示されない分岐条件を示すキーワードが、ｏｔｈｅｒｓ文ではなく、ｄｅｆａｕｌｔ文であることを除いて、設計仕様がＶＨＤＬを用いて記述された場合と同様である。
【００８２】
なお、上述した各実施形態における設計検証装置は、専用の装置によって実現してもよいが、コンピュータ（情報処理装置）によっても実現可能である。この場合、係るコンピュータは、メモリ（不図示）に格納されたソフトウェア・プログラムをＣＰＵ（Ｃｅｎｔｒａｌ＿Ｐｒｏｃｅｓｓｉｎｇ＿Ｕｎｉｔ、不図示）に読み出し、読み出したソフトウェア・プログラムをＣＰＵにおいて実行することにより、実行結果を、例えば、ユーザ・インタフェースに出力する。上述した各実施形態及び変形例の場合、係るソフトウェア・プログラムには、上述したところの、図１に示した設計検証装置１００の各手段、図４に示した設計検証装置１１０の各手段の機能を実現可能な記述がなされていればよい。但し、設計検証装置１１０の表示手段１１４は、適宜ハードウェアを含むことも想定される。そして、このような場合、係るソフトウェア・プログラム（コンピュータ・プログラム）は、本発明を構成すると捉えることができる。更に、係るソフトウェア・プログラムを格納した、コンピュータ読み取り可能な記憶媒体も、本発明を構成すると捉えることができる。
【００８３】
以上、本発明を、上述した各実施形態およびその変形例によって例示的に説明した。しかしながら、本発明の技術的範囲は、上述した各実施形態およびその変形例に記載した範囲には限定されない。当業者には、係る実施形態に対して多様な変更又は改良を加えることが可能であることは明らかである。そのような場合、係る変更又は改良を加えた新たな実施形態も、本発明の技術的範囲に含まれ得る。そしてこのことは、特許請求の範囲に記載した事項から明らかである。
【産業上の利用可能性】
【００８４】
本発明は、ＲＴＬを用いた半導体デバイスの開発において、有限状態機械の設計仕様を検証する用途に利用できる。
【符号の説明】
【００８５】
１００  設計検証装置
１０１  状態遷移先抽出手段
１０２  状態遷移元抽出手段
１０３  状態遷移先差分抽出手段
２００  設計仕様
３００  状態遷移先差分
１１０  設計検証装置
１１１  状態遷移先抽出手段
１１２  状態遷移元抽出手段
１１３  状態遷移先差分抽出手段
１１４  表示手段
２１０  設計仕様
３１０  診断メッセージ
【図１】
0006394278.tif 000002
【図２】
0006394278.tif 000003
【図３】
0006394278.tif 000004
【図４】
0006394278.tif 000005
【図５】
0006394278.tif 000006
【図６】
0006394278.tif 000007
【図７】
0006394278.tif 000008
【図８】
0006394278.tif 000009
【図９】
0006394278.tif 000010