(57)【要約】【課題】検証目的を達成するに十分なシミュレーション精度を達成し、かつ大規模なシステムであってもシミュレーション実行時間を許容範囲に収めることが可能であり、回路設計者と「論理回路動作モデル」設計者が異なる場合であっても短期間で的確な「論理回路動作モデル」を生成することができる論理回路動作モデル生成装置を提供する。【解決手段】本発明に係る論理回路動作モデル生成装置は、論理回路の動作をＲＴＬで記述した論理回路ＲＴＬモデルと入出力動作を記述した外部動作モデルとを統合し、論理回路の動作とそれに結合される外部装置の動作とを統合的に記述した第１の論理回路動作モデルを生成する生成部と、検証目的に応じた検証精度が記述された制約モデルを入力し、制約モデルに基づいて検証精度を保証する範囲で第１の論理回路動作モデルの規模を縮小変換し、第２の論理回路動作モデルを生成する変換部とを備えたことを特徴とする。【選択図】  図２
2007011477.tif 000002
【特許請求の範囲】
【請求項１】
論理回路の動作をレジスタ・トランスファ・レベルで記述した論理回路ＲＴＬモデルと前記論理回路ＲＴＬモデルに対する入出力動作の記述を含む外部動作モデルとを統合し、前記論理回路の動作とそれに結合される外部装置の動作とを統合的に記述した第１の論理回路動作モデルを生成する生成部と、
検証目的に応じた検証精度が記述された制約モデルを入力し、前記制約モデルに基づいて前記検証精度を保証する範囲で前記第１の論理回路動作モデルの規模を縮小変換し、第２の論理回路動作モデルを生成する変換部と、を備え、
前記生成部は、
手続を表す命令、前記命令が使用し或いは生成する値を表す変数、時刻及び分岐状態を表す変数、及びレジスタを含む記憶要素の記憶場所を表す変数を節点とし、前記命令及び前記各変数の使用関係或いは代入関係を示すように前記節点の間を結ぶ矢線を枝とするグラフを記述可能な第１の論理回路動作モデル、又は前記グラフと相互に変換可能な隣接行列若しくは辺リストで記述された第１の論理回路動作モデルを生成する、
ことを特徴とする論理回路動作モデル生成装置。
【請求項２】
前記変換部は、
前記節点において、前記制約モデルと所定の記号評価規則に従って評価記号を求め、前記節点と前記評価記号とを対応付けた評価記号表を生成する記号評価部と、
前記節点において前記評価記号表を参照し、所定の縮小変換方法毎に定められた縮小変換判定基準に基づいて縮小変換が可能か否かを判定し、縮小変換が可能と判定した場合には、縮小変換可能と判定された節点と縮小変換方法とを対応付けた縮小変換表を生成する縮小変換判定部と、
前記縮小変換表に基づいて、前記第１の論理回路動作モデルから前記第２の論理回路動作モデルに縮小変換する更新部と、
を備えたことを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項３】
前記制約モデルは、検証に必要な時刻を特定する記述を含むモデルであり、
前記変換部は、前記検証に必要な時刻の精度が、前記第１の論理回路動作モデルによって得られる時刻精度と同等の精度となるように、前記第２の論理回路動作モデルを生成することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項４】
前記制約モデルは、検証に必要な論理回路上の構成要素を特定する記述を含むモデルであり、
前記変換部は、前記検証に必要な論理回路上の構成要素の範囲を保持するように縮小変換して前記第２の論理回路動作モデルを生成することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項５】
前記制約モデルは、検証に必要な時刻を特定する記述、及び検証に必要な論理回路上の構成要素を特定する記述を含むモデルであり、
前記変換部は、前記検証に必要な時刻の精度が、前記第１の論理回路動作モデルによって得られる時刻精度と同等の精度となるように、かつ、前記検証に必要な論理回路上の構成要素の範囲を保持するように縮小変換して前記第２の論理回路動作モデルを生成することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項６】
前記記号評価部は、定数及び不定値を含めて前記評価記号として扱い、これらの組み合わせについての記号評価規則に基づいて前記評価記号を求めることを特徴とする請求項２に記載の論理回路動作モデル生成装置。
【請求項７】
前記記号評価部は、一次式、範囲式、論理式の少なくとも１つを前記評価記号として扱い、これらの組み合わせについての記号評価規則に基づいて前記評価記号をさらに求めることを特徴とする請求項６に記載の論理回路動作モデル生成装置。
【請求項８】
前記縮小変換判定部は、
読込み命令と書込み命令とがある場合において、
前記読込み命令が読み込む記憶場所と前記書込み命令が書き込む記憶場所とが同一であり、前記読込み命令が実行されたときに、前記書込み命令が直近の過去に無条件で実行されることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記読込み命令と前記書込み命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項２に記載の論理回路動作モデル生成装置。
【請求項９】
前記縮小変換判定部は、
書込み待ち命令と書込み命令とがある場合において、
前記書込み待ち命令が参照する記憶場所と前記書込み命令が書き込む記憶場所とが同一であり、前記書込み待ち命令が実行されたときに、前記書込み命令が直近の未来に無条件で実行されることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記書込み待ち命令と前記書込み命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項２に記載の論理回路動作モデル生成装置。
【請求項１０】
前記縮小変換判定部は、
値を生成する命令がある場合において、
その命令が生成する値が定数値であることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記値を生成する命令を削除することを縮小変換方法とする、
ことを特徴とする請求項２に記載の論理回路動作モデル生成装置。
【請求項１１】
前記縮小変換判定部は、
条件分岐命令がある場合において、
分岐先を決定する値が定数値であることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記条件分岐命令の直前の命令と分岐先の直後の命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項２に記載の論理回路動作モデル生成装置。
【請求項１２】
前記変換部は、縮小変換の中断を指示された場合、指示された時点が縮小変換の途中であっても、前記制約モデルを満たす既に縮小変換された範囲を第２の論理回路動作モデルとして生成することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項１３】
前記変換部は、
縮小変換が可能或いは不可能のいずれとも判定できず不明となる部位がある場合、その部位と理由を解析結果として出力することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項１４】
前記変換部は、
前記第２の論理回路動作モデルに対してさらなる縮小変換を行うとすれば、影響を受ける可能性のある範囲を示す情報をさらに出力することを特徴とする請求項１３に記載の論理回路動作モデル生成装置。
【請求項１５】
前記変換部は、
前記第２の論理回路動作モデルをさらに縮小変換するため、修正された制約モデルを入力し、縮小変換の処理を再開することを特徴とする請求項１に記載の論理回路動作モデル生成装置。
【請求項１６】
論理回路の動作をレジスタ・トランスファ・レベルで記述した論理回路ＲＴＬモデルと前記論理回路ＲＴＬモデルに対する入出力動作の記述を含む外部動作モデルとを統合し、前記論理回路の動作とそれに結合される外部装置の動作とを統合的に記述した第１の論理回路動作モデルを生成する生成ステップと、
検証目的に応じた検証精度が記述された制約モデルを入力し、前記制約モデルに基づいて前記検証精度を保証する範囲で前記第１の論理回路動作モデルの規模を縮小変換し、第２の論理回路動作モデルを生成する変換ステップと、を備え、
前記生成ステップは、
手続を表す命令、前記命令が使用し或いは生成する値を表す変数、時刻及び分岐状態を表す変数、及びレジスタを含む記憶要素の記憶場所を表す変数を節点とし、前記命令及び前記各変数の使用関係或いは代入関係を示すように前記節点の間を結ぶ矢線を枝とするグラフを記述可能な第１の論理回路動作モデル、又は前記グラフと相互に変換可能な隣接行列若しくは辺リストで記述された第１の論理回路動作モデルを生成する、
ことを特徴とする論理回路動作モデル生成方法。
【請求項１７】
前記変換ステップは、
前記節点において、前記制約モデルと所定の記号評価規則に従って評価記号を求め、前記節点と前記評価記号とを対応付けた評価記号表を生成する記号評価ステップと、
前記節点において前記評価記号表を参照し、所定の縮小変換方法毎に定められた縮小変換判定基準に基づいて縮小変換が可能か否かを判定し、縮小変換が可能と判定した場合には、縮小変換可能と判定された節点と縮小変換方法とを対応付けた縮小変換表を生成する縮小変換判定ステップと、
前記縮小変換表に基づいて、前記第１の論理回路動作モデルから前記第２の論理回路動作モデルに縮小変換する更新ステップと、
を備えたことを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項１８】
前記制約モデルは、検証に必要な時刻を特定する記述を含むモデルであり、
前記変換ステップは、前記検証に必要な時刻の精度が、前記第１の論理回路動作モデルによって得られる時刻精度と同等の精度となるように、前記第２の論理回路動作モデルを生成することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項１９】
前記制約モデルは、検証に必要な論理回路上の構成要素を特定する記述を含むモデルであり、
前記変換ステップは、前記検証に必要な論理回路上の構成要素の範囲を保持するように縮小変換して前記第２の論理回路動作モデルを生成することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項２０】
前記制約モデルは、検証に必要な時刻を特定する記述、及び検証に必要な論理回路上の構成要素を特定する記述を含むモデルであり、
前記変換ステップは、前記検証に必要な時刻の精度が、前記第１の論理回路動作モデルによって得られる時刻精度と同等の精度となるように、かつ、前記検証に必要な論理回路上の構成要素の範囲を保持するように縮小変換して前記第２の論理回路動作モデルを生成することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項２１】
前記記号評価ステップは、定数及び不定値を含めて前記評価記号として扱い、これらの組み合わせについての記号評価規則に基づいて前記評価記号を求めることを特徴とする請求項１７に記載の論理回路動作モデル生成方法。
【請求項２２】
前記記号評価ステップは、一次式、範囲式、論理式の少なくとも１つを前記評価記号として扱い、これらの組み合わせについての記号評価規則に基づいて前記評価記号をさらに求めることを特徴とする請求項２１に記載の論理回路動作モデル生成方法。
【請求項２３】
前記縮小変換判定ステップは、
読込み命令と書込み命令とがある場合において、
前記読込み命令が読み込む記憶場所と前記書込み命令が書き込む記憶場所とが同一であり、前記読込み命令が実行されたときに、前記書込み命令が直近の過去に無条件で実行されることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記読込み命令と前記書込み命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項１７に記載の論理回路動作モデル生成方法。
【請求項２４】
前記縮小変換判定ステップは、
書込み待ち命令と書込み命令とがある場合において、
前記書込み待ち命令が参照する記憶場所と前記書込み命令が書き込む記憶場所とが同一であり、前記書込み待ち命令が実行されたときに、前記書込み命令が直近の未来に無条件で実行されることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記書込み待ち命令と前記書込み命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項１７に記載の論理回路動作モデル生成方法。
【請求項２５】
前記縮小変換判定ステップは、
値を生成する命令がある場合において、
その命令が生成する値が定数値であることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記値を生成する命令を削除することを縮小変換方法とする、
ことを特徴とする請求項１７に記載の論理回路動作モデル生成方法。
【請求項２６】
前記縮小変換判定ステップは、
条件分岐命令がある場合において、
分岐先を決定する値が定数値であることを縮小変換判定基準とし、
前記縮小変換判定基準が満たされたとき、前記条件分岐命令の直前の命令と分岐先の直後の命令とを短絡することを縮小変換方法とする、
ことを特徴とする請求項１７に記載の論理回路動作モデル生成方法。
【請求項２７】
前記変換ステップは、
前記縮小変換の中断を指示された場合、指示された時点が縮小変換の途中であっても、前記制約モデルを満たす既に縮小変換された範囲を第２の論理回路動作モデルとして生成することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項２８】
前記変換ステップは、
縮小変換が可能或いは不可能のいずれとも判定できず不明となる部位がある場合、その部位と理由を解析結果として出力することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【請求項２９】
前記変換ステップは、
前記第２の論理回路動作モデルに対してさらなる縮小変換を行うとすれば、影響を受ける可能性のある範囲を示す情報をさらに出力することを特徴とする請求項２８に記載の論理回路動作モデル生成方法。
【請求項３０】
前記変換ステップは、
前記第２の論理回路動作モデルをさらに縮小変換するため、修正された制約モデルを入力し、縮小変換の処理を再開することを特徴とする請求項１６に記載の論理回路動作モデル生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理回路動作モデル生成装置及び論理回路動作モデル生成方法に係り、特に、ハードウェア記述言語等で表現された論理回路ＲＴＬモデルを変換して論理回路動作モデルを生成する論理回路動作モデル生成装置及び論理回路動作モデル生成方法に関する。
【背景技術】
【０００２】
近年、ＬＳＩ等の大規模な論理回路の設計・製造では、ＨＤＬ（Hardware  Description  Language）と呼ばれる言語でハードウェアを記述し、記述したＨＤＬからネットリストと呼ばれる回路要素の接続関係を表すデータに変換し、このネットリストから実際のＬＳＩ等のハードウェアを製造することが多い。
【０００３】
ＨＤＬからネットリストへ変換することを「論理合成」と呼び、所定の論理合成ツールを用いてＨＤＬからネットリストへ変換することができる。ネットリストは、例えば、ＡＮＤ回路、ＯＲ回路、レジスタ、カウンタ等の回路要素と相互の接続関係を表すデータであり、このネットリストを用いて従来からあるいわゆる回路図をプリントアウトすることも可能である。
【０００４】
ハードウェア記述言語（ＨＤＬ）には、種々のものがあるが、例えば、Verilog-ＨＤＬ、ＶＨＤＬ、SystemＣといったＨＤＬが今日多く用いられている。また、ＨＤＬには幾つかの記述レベルが存在し、代表的には、ビヘイビアレベルとレジスタ・トランスファ・レベル（ＲＴＬ）がある。
【０００５】
ビヘイビアレベルは、動作（ハードウェア動作に限らずソフトウェアの動作をも含む）を「クロックの概念」無しに表現したものである。詳細な設計仕様が固まっていない回路ブロックの記述や、シミュレーションを目的としたモデル、例えばＣＰＵの動作をモデル化したもの、の記述に用いられる。
【０００６】
これに対してレジスタ・トランスファ・レベル（Register  Transfer  Level：ＲＴＬ）は、回路の構成要素であるレジスタやカウンタ等と、これらの間におけるデータの転送状態（接続状態）を表現しているレベルであり、これらを動作させるための「クロックの概念」が存在するものである。
【０００７】
ＨＤＬを「論理合成」し、ネットリストを生成するためには、ＨＤＬをレジスタ・トランスファ・レベル（以下、単にＲＴＬと言う。）で記述する必要がある。ＲＴＬのレベルのＨＤＬで記述された論理回路を「論理回路ＲＴＬモデル」と呼ぶものとする。
【０００８】
他方、今日の大規模な回路では、回路自体の設計に加えて、設計した回路の検証および評価が非常に重要になってきている。設計段階において（物を作る前に）十分な検証および評価を実施することによって、結果的には開発期間が短縮され、開発コストを低減することが可能となる。
【０００９】
さらに、今日のシステムの多くは、マイクロプロセッサ等を含むハードウェア／ソフトウェア一体型のシステムが一般的になってきている。このため、ハードウェアのみならず、マイクロプロセッサ等で動作するソフトウェアをも含めて検証、評価する必要が高くなってきている。
【００１０】
ところで、今日、広く用いられている論理回路は同期式論理回路であり、「論理回路ＲＴＬモデル」では、定義されたレジスタ群への書込みは、クロック、リセット等の同期信号を用いて書き込まれるように記述されている。従って、「論理回路ＲＴＬモデル」で評価可能な時間的精度は、周期的なクロック等の同期信号が入力される毎に、レジスタの値が正しいか否かが検証できることが保証される精度である（以下、この精度をクロックサイクル精度と呼ぶものとする）。このように、「論理回路ＲＴＬモデル」を用いた検証は、クロックサイクル毎に非常に緻密な検証が可能である。
【００１１】
しかしながら、マイクロプロセッサ等を含む大規模な論理回路においては、個々の論理回路や、それらと相互に通信しマイクロプロセッサ上で動作するソフトウェアを、「論理回路ＲＴＬモデル」とマイクロプロセッサのシミュレータを接続したシミュレーション環境を用いてクロックサイクル精度で検証すると、シミュレーション時間が膨大になるという大きな問題がある。
【００１２】
一方、「論理回路ＲＴＬモデル」と通信するマイクロプロセッサ等のソフトウェアを検証する場合、クロックサイクル精度のような細かな精度で検証することは必ずしも必要ではない。また、「論理回路ＲＴＬモデル」の内部のレジスタの状態を総て検証する必要もない。
【００１３】
そこで、検証目的を達成する範囲で、シミュレーションの時間的精度（モニタ・検証する時間的な粗さ）や空間的精度（モニタ・検証するレジスタや信号の種類や量）を落とすことによって、シミュレーション時間を短縮する技術が種々開発されている。
【００１４】
例えば、特許文献１乃至３には、シミュレーション精度の粗い（抽象度の高い）シミュレーションモデルを作成し、順次そのシミュレーションモデルを詳細化していく技術が開示されている。このうち、特許文献１には、逐次処理可能なプログラミング言語のモデルを作成して、検証にかかる時間を大幅に減少させ、システムレベルの検証を容易に実現可能とする技術が開示されている。また、特許文献２には、シミュレーション精度の粗いモデルと細かいモデルとを接続するインタフェースモデルを用いて、入出力データの小数点表示やビット幅の変換を行うビット精度変換を行い、精度の粗いモデルに一部を置き換える技術が開示されている。また、特許文献３には、予め定められた動作単位毎にシミュレーション精度の粗い動作記述を準備しておき、それらを選択してモデルを作成する技術が開示されている。
【００１５】
これとは逆に、シミュレーション精度の細かい（抽象度の低い）モデルを作成し、これを要約していく技術もある。例えば、特許文献４は、１つのクロックドメインに同期して論理動作を行う回路で発生するイベントを省略して論理の検証時間を短縮する技術が開示されている。また、特許文献５には、検証目的に応じて入力やレジスタの値を一部固定して論理回路モデルの一部を削減する技術が開示されている。また、特許文献６には、同期式回路の特徴を生かして、クロックサイクルの各時刻に対してテーブルを作成し、シミュレーションを行う前にイベントスケジュールを行う技術が開示されている。
【００１６】
さらに、特許文献７には、論理回路ブロックが有する状態を動作開始状態及び動作終了状態として設定し、状態から状態へ遷移させる入出力命令のシーケンスを１クロック毎にＲＴＬモデルに与えてその動作を抽出し、時間の概念を持たないモデルを作成する技術が開示されている。
【００１７】
また、特許文献８には、論理回路の動作を特徴づける制御部に相当する回路を指定し、制御部によって動作が決定される回路を抽出してソフトウェア向けのプログラミング言語に適したモデルを作成する技術が開示されている。
【特許文献１】特開２００１−１４３５６号公報
【特許文献２】特開２００１−１０１２４７号公報
【特許文献３】特開２００３−１４１２０４号公報
【特許文献４】特開２００４−１８５２１３号公報
【特許文献５】特開２００１−２２８０８号公報
【特許文献６】米国特許第５，８６２，３６１号明細書
【特許文献７】特開２００３−１６１３４号公報
【特許文献８】特開２００４−２１８４１号公報
【発明の開示】
【発明が解決しようとする課題】
【００１８】
上記のように、シミュレーションを行うためのモデル（以下、このモデルを「論理回路動作モデル」という。）は、「論理回路ＲＴＬモデル」とは別に抽象度の高いモデルを新たに生成し、これを順次詳細化して「論理回路動作モデル」を生成する方法や、既存の「論理回路ＲＴＬモデル」（抽象度が低く細かいモデル）を用いてこれを要約することによって「論理回路動作モデル」に変換する方法によって生成されることが多い。
【００１９】
「論理回路動作モデル」の良否は、「論理回路動作モデル」の品質（第１の条件）と「論理回路動作モデル」の作成の手間（第２の条件）という２つの観点から判断する必要がある。
【００２０】
「論理回路動作モデル」の品質（第１の条件）は、検証目的を達成するに十分なシミュレーション精度（時間的精度および空間的精度）を確保すると共に、大規模なシステムであってもシミュレーション実行時間が実用上許容しうる範囲に収まることである。
【００２１】
また、「論理回路動作モデル」の作成の手間（第２の条件）は、論理回路やソフトウェアプログラムの検証開始時期までに、「論理回路動作モデル」が「論理回路ＲＴＬモデル」と整合が取れた状態で提供されることである。
【００２２】
シミュレーション精度の粗い（抽象度の高い）モデルを新たに作成し、順次モデルを詳細化していく方法（特許文献１乃至３）は、検証目的に合わせて、人手（或いは半自動）によって「論理回路動作モデル」を作成する方法である。このため、人手と時間を十分かければ「論理回路動作モデル」の品質（第１の条件）は達成される。
【００２３】
しかしながら、この方法は、「論理回路動作モデル」と「論理回路ＲＴＬモデル」の二重開発となり、２つのモデル間で整合性を保証できないという問題がある。また、過去に設計済みの論理回路を組み込む場合、「論理回路ＲＴＬモデル」は存在しても「論理回路動作モデル」は存在しない場合が多く、仕様書等から新規に「論理回路動作モデル」を開発する必要がある。このため、検証開始時期までに「論理回路動作モデル」の開発が完了しないという問題が生じる（即ち、第２の条件を満たさない）。また、特許文献３が開示するように、「論理回路動作モデル」を作成するための「部品」を予め作成しておくことで作成期間の短縮はできるものの、作成した「部品」群と「論理回路ＲＴＬモデル」との間で整合性を検査できないため、「論理回路動作モデル」と「論理回路ＲＴＬモデル」と間での整合性を保証できないという問題はより深刻となる。
【００２４】
他方、シミュレーション精度の細かい（抽象度の低い）モデルを要約する方法（特許文献４乃至８）は、設計済みの「論理回路ＲＴＬモデル」を出発点として自動的に要約して「論理回路動作モデル」を作成するため、第２の条件（開発の手間）を満足する可能性は比較的高い。
【００２５】
しかしながら、開示されている従来技術においては、第２の条件を満足する程度の開発期間では、検証目的にあった適切な時間的、空間的精度を確保し、かつ、大規模なシステムであってもシミュレーション実行時間を実用上耐えうる範囲に収めるという、第１の条件を満たす「論理回路動作モデル」を得ることは困難であると予想される。
【００２６】
例えば、特許文献４或いは特許文献５は、時間的精度としてはクロックサイクル精度を維持するものであり、システムレベルの検証としては過剰な精度であるとともに、シミュレーション実行時間が多大となり第１の条件を満たさない。
【００２７】
一方、特許文献７が開示する方法は、「論理回路ＲＴＬモデル」の内部状態を人手で設定するステップを持ち、人手で設定した内部状態を「論理回路動作モデル」への変換の出発点とするものである。このため、モデル化対象の論理回路の振る舞いを十分に分析して漏れや重複が無いように適切に内部状態を設定しないと所望の「論理回路動作モデル」を得ることができない。また、「論理回路動作モデル」を総て人手で生成する場合は、モデル化対象の論理回路の振る舞いについて仕様書等を通して分析し、漏れや重複が無いように適切に内部状態を定義する工程は、一般に、全体の約半分を占めると考えられている。このため、実際にモデルを記述する工程やモデルの整合性を確保する工程が削減されたとしても、内部状態の適切な定義の工程に多くの時間を費やし、結果的には第２の条件（開発の手間）を満足できなくなる可能性が高い。さらに、特許文献７が開示する方法は、時間の概念のある「論理回路ＲＴＬモデル」から、時間の概念の無い「論理回路動作モデル」に一気に変換する方法であるため、特定時刻を指定してモニタ・検証することができず、検証用途が限定されたものとなってしまう。
【００２８】
特許文献８の方法は、論理回路がもつ制御部を指定してそれを出発点とすることで、特許文献７の方法で用いる内部状態の設定ステップを不要としている。しかしながら、制御部が回路内に分散して複数存在する場合や、論理回路設計担当者と「論理回路動作モデル」設計担当者が異なる等の理由で「論理回路ＲＴＬモデル」について詳細な知識が無い場合等においては、適切な制御部を指定することが困難となることもあり、改良の余地がある。
【００２９】
本発明は、上記事情に鑑みてなされたもので、検証目的を達成するに十分なシミュレーション精度を達成し、かつ大規模なシステムであってもシミュレーション実行時間を許容範囲に収めることが可能であり、回路設計者と「論理回路動作モデル」設計者が異なる場合であっても短期間で的確な「論理回路動作モデル」を生成することができる論理回路動作モデル生成装置及び論理回路動作モデル生成方法を提供することを目的とする。
【課題を解決するための手段】
【００３０】
本発明に係る論理回路動作モデル生成装置は、上記課題を解決するため、請求項１に記載したように、論理回路の動作をレジスタ・トランスファ・レベルで記述した論理回路ＲＴＬモデルと前記論理回路ＲＴＬモデルに対する入出力動作の記述を含む外部動作モデルとを統合し、前記論理回路の動作とそれに結合される外部装置の動作とを統合的に記述した第１の論理回路動作モデルを生成する生成部と、検証目的に応じた検証精度が記述された制約モデルを入力し、前記制約モデルに基づいて前記検証精度を保証する範囲で前記第１の論理回路動作モデルの規模を縮小変換し、第２の論理回路動作モデルを生成する変換部とを備え、前記生成部は、手続を表す命令、前記命令が使用し或いは生成する値を表す変数、時刻及び分岐状態を表す変数、及びレジスタを含む記憶要素の記憶場所を表す変数を節点とし、前記命令及び前記各変数の使用関係或いは代入関係を示すように前記節点の間を結ぶ矢線を枝とするグラフを記述可能な第１の論理回路動作モデル、又は前記グラフと相互に変換可能な隣接行列若しくは辺リストで記述された第１の論理回路動作モデルを生成することを特徴とする。
【００３１】
また、本発明に係る論理回路動作モデル生成方法は、請求項１６に記載したように、論理回路の動作をレジスタ・トランスファ・レベルで記述した論理回路ＲＴＬモデルと前記論理回路ＲＴＬモデルに対する入出力動作の記述を含む外部動作モデルとを統合し、前記論理回路の動作とそれに結合される外部装置の動作とを統合的に記述した第１の論理回路動作モデルを生成する生成ステップと、検証目的に応じた検証精度が記述された制約モデルを入力し、前記制約モデルに基づいて前記検証精度を保証する範囲で前記第１の論理回路動作モデルの規模を縮小変換し、第２の論理回路動作モデルを生成する変換ステップとを備え、前記生成ステップは、手続を表す命令、前記命令が使用し或いは生成する値を表す変数、時刻及び分岐状態を表す変数、及びレジスタを含む記憶要素の記憶場所を表す変数を節点とし、前記命令及び前記各変数の使用関係或いは代入関係を示すように前記節点の間を結ぶ矢線を枝とするグラフを記述可能な第１の論理回路動作モデル、又は前記グラフと相互に変換可能な隣接行列若しくは辺リストで記述された第１の論理回路動作モデルを生成することを特徴とする。
【発明の効果】
【００３２】
本発明に係る論理回路動作モデル生成装置及び論理回路動作モデル生成方法によれば、検証目的を達成するに十分なシミュレーション精度を達成し、かつ大規模なシステムであってもシミュレーション実行時間を許容範囲に収めることが可能であり、回路設計者と「論理回路動作モデル」設計者が異なる場合であっても短期間で的確な「論理回路動作モデル」を生成することができる。
【発明を実施するための最良の形態】
【００３３】
本発明に係る論理回路動作モデル生成装置および論理回路動作モデル生成方法の実施形態について、添付図面を参照して説明する。
【００３４】
（１）論理回路動作モデル生成装置の位置付けと構成
図１は、本発明に係る論理回路動作モデル生成装置および論理回路動作モデル生成方法の位置付けについて概念的に説明した図である。
【００３５】
図１の左図は、対象となる大規模な論理回路のシステム構成をモデル化した図である。本モデルでは、大規模論理回路２００、論理回路２１０、およびマイクロプロセッサ２２０がバスを介して相互に接続されている。
【００３６】
このうち、大規模論理回路２００は、既に設計済みで実績のある回路、或いは詳細設計が終了しているレベルである。即ち、大規模論理回路２００は、論理合成が可能なレジスタ・トランスファ・レベル（ＲＴＬ）でのハードウェア記述言語で記述されたモデルが既に存在している。このモデルを論理回路ＲＴＬモデル１００と呼ぶ。
【００３７】
他方、論理回路２１０は、概略設計の段階であり、レジスタ・トランスファ・レベル（ＲＴＬ）でのハードウェア記述言語は存在していない。ただし、概略の機能性能や外部インタフェース（バスを介してのトランザクション）は決まっている。
【００３８】
また、マイクロプロセッサ２２０が実行するソフトウェアについても外部インタフェースは決まっているものとする。即ち、論理回路２１０や、マイクロプロセッサ２２０のソフトウェについては、バスを介してのトランザクション（読み出しや書込み）を記述することが可能なレベルであり、この外部インタフェースや概略機能を記述したモデルを外部モデル１１０と呼ぶ。
【００３９】
このような構成のシステムをシミュレーション等によって検証するためのモデルを、検証目的に応じた「粗さ」で生成することが本発明の位置付けとなる。
【００４０】
大規模論理回路２００をＲＴＬで記述した論理回路ＲＴＬモデル１００は、クロック単位のレベルでレジスタ間の信号伝送を表現可能に記述されており、正確ではあるものの非常に細かい。
【００４１】
従って、論理回路ＲＴＬモデル１００と外部動作モデル１１０とを単純に結合したモデル（これを、第１の論理回路動作モデル５０と呼ぶ）では、クロック毎に動作し、かつ内部状態もクロック毎に変化するため検証時間が膨大になってくる。
【００４２】
他方、シミュレーション等による検証は、通常何らかの検証目的をもって行われるものであり、検証目的に応じて必要となってくる検証精度は異なってくる。ここで検証精度とは、時間的な精度と、検証対象回路の範囲（空間的精度）の双方を言っている。
【００４３】
通常、ソフトウェアの検証や、概略設計段階の論理回路の検証においては、クロックレベルの時間的精度や、全レジスタを検証範囲とするような空間的精度は不要である。
【００４４】
そこで、検証目的から必要とされる検証精度を記述した制約モデルを明定し、この制約モデルの制約の下で第１の論理回路動作モデル５０を縮小変換し、第２の論理回路動作モデル６０を生成し、この第２の論理回路動作モデル６０を用いてシミュレーション等の検証を行う。これによって、短時間でかつ検証目的に応じた検証精度でシステムを評価することができる。
【００４５】
本発明に係る論理回路動作モデル生成装置および論理回路動作モデル生成方法は、論理回路ＲＴＬモデル１００と外部動作モデル１１０とから第１の論理回路動作モデル５０を自動的に生成し、さらに第２の論理回路動作モデル６０へ自動的に縮小変換するものである。
【００４６】
図２は、本発明に係る論理回路動作モデル生成装置１の実施形態の構成例を示す図である。
【００４７】
論理回路動作モデル生成装置１は、論理回路ＲＴＬモデル１００と外部動作モデル１１０とから第１の論理回路動作モデル５０を生成する生成部２と、制約モデル１２０の制約の下で生成した第１の論理回路動作モデル５０を縮小変換し、第２の論理回路動作モデル６０を生成する変換部３とを備えて構成される。
【００４８】
変換部３は、第１の論理回路動作モデル５０の内部の各節点（命令や変数を表す点）に対して制約モデル１２０の制約の下で「評価記号」を求め、評価記号表を生成する記号評価部３０と、所定の方法の縮小変換が可能か否かを評価記号表に基づいて判定し、縮小変換表を生成する縮小変換判定部３１と、縮小変換表に基づいて第１の論理回路動作モデル５０から第２の論理回路動作モデル６０へ縮小変換するとともに所定の解析結果を出力する更新部３２とを備えて構成される。
【００４９】
（２）論理回路動作モデル生成装置１の動作
図３は、論理回路動作モデル生成装置１の基本動作の流れを示すフローチャートである。
【００５０】
ステップＳＴ１では、論理回路ＲＴＬモデル１００と外部動作モデル１１０とから第１の論理回路動作モデル５０を生成する。
【００５１】
ステップＳＴ２では、第１の論理回路動作モデル５０（又は縮小変換中の第２の論理回路動作モデル６０）の記述上の各箇所（各節点）について、予め定めてある記号評価規則と制約モデル１２０とに基づいて「評価記号」を求め、評価記号表を生成する。
【００５２】
次に、ステップＳＴ３では、第１の論理回路動作モデル５０（又は縮小変換中の第２の論理回路動作モデル６０）と評価記号表を参照し、予め定めてある縮小変換判定基準に基づいて縮小変換が可能か否かを判定し、第１の論理回路動作モデル５０（又は縮小変換中の第２の論理回路動作モデル６０）の記述上の各箇所（各節点）について縮小変換の可否を記載した縮小変換表を生成する。また、本ステップで解析結果報告を生成する形態としてもよい。
【００５３】
ステップＳＴ４では、縮小変換表に縮小変換が可能な箇所があるか否かを判定する。縮小変換が可能な箇所がある場合には、ステップＳＴ５へ進む。
【００５４】
ステップＳＴ５では、縮小変換表の内容に従って第１の論理回路動作モデル５０（又は縮小変換中の第２の論理回路動作モデル６０）を縮小変換し、第２の論理回路動作モデル６０を生成する。また、縮小変換が完了した部位は縮小変換表から削除する。
【００５５】
ステップＳＴ５における縮小変換によって第２の論理回路動作モデル６０はその記述上の構造の一部が変更される。このため、再度ステップＳＴ２に戻って、変更された構造に基づいて再度各箇所の評価記号表を生成する形態としている。
【００５６】
ステップＳＴ４において、縮小変換可能な箇所が無いと判定されるまで、ステップＳＴ２からステップＳＴ５を繰り返す。
【００５７】
縮小変換可能な箇所が無くなった時点で、最終的な第２の論理回路動作モデル６０が生成される。
【００５８】
なお、縮小変換処理に時間を要するような場合には、外部からの操作によって、ステップＳＴ３が終了した時点で中断可能な形態としてもよい。
【００５９】
中断した後、解析結果報告等を設計者が分析した結果、制約モデル１２０に適宜の修正を加えることによってさらに縮小が可能であると判断される場合もある。このような場合には、制約モデル１２０に修正を加えた後、ステップＳＴ２から再開する形態としてもよい。
【００６０】
上記の各ステップについて、具体例を示しつつ以下に詳細に説明する。
【００６１】
（３）各モデルの概要
第１の論理回路動作モデル５０は、論理回路ＲＴＬモデル１００および外部動作モデル１１０を入力として生成される。そこで、まず論理回路ＲＴＬモデル１００および外部動作モデル１１０について、具体的な回路を例にとって説明する。併せて、制約モデル１２０についても説明する。
【００６２】
以下の説明では、論理回路の具体例として、非同期リセット付８ビットカウンタ回路を例として取り上げる（図１では、大規模論理回路２００に相当する部分である）。
【００６３】
図４は、非同期リセット付８ビットカウンタ回路１０１（以下、単にカウンタ回路１０１と言う。）の構成を示したものである。カウンタ回路１０１は、バスに接続されており、バス入力１０２として、ＷＲＩＯ（書込み指示）、ＲＤＩＯ（読出し指示）、ＣＳ（チップセレクト）、ＡＢ（アドレスバス）、及びＩＯＢＵＳＩ（バス入力データ）を有している。また、バス出力１０３として、ＩＯＢＵＳＯ（バス出力データ）を有している。
【００６４】
カウンタ回路１０１の内部は、論理回路Ａ、Ｂ、およびＣを有するほか、レジスタとして、ＩＯＢＵＳＯレジスタ、ＣＯＮＴＲＯＬレジスタ、ＣＯＵＮＴレジスタ等を有している。
【００６５】
カウンタ回路１０１の基本的な動作は、ＲＥＳＥＴ信号がＨ（「１」）の場合は、ＣＬＫ信号の立ち上がりで順次カウントアップし、ＲＥＳＥＴ信号がＬ（「０」）に立ち下がるとゼロリセットするという単純なものである。
【００６６】
バスを介してＲＤＩＯ（読出し指示）がカウンタ回路１０１に入力されると、その時のＡＢ（アドレスバス）の値に応じて、カウント値が格納されているＣＯＵＮＴレジスタの値か、内部状態のデータが格納されているＣＯＮＴＲＯＬレジスタの値のいずれかを出力するように構成されている。
【００６７】
図４の構成および動作が、論理回路ＲＴＬモデル１００として記述されることになる。
【００６８】
図５は、カウンタ回路１０１へ入出力される上記のバス入力１０２、バス出力１０３、およびＣＬＫ信号とＲＥＳＥＴ信号のタイミング関係を示す図である。
【００６９】
図５の最上段に示している「data」が、バスを介して外部のシステム（図１では、論理回路２１０又はマイクロプロセッサ２２０に相当する部分）と授受するデータである。
【００７０】
図５に示したタイミング関係が、後述するように外部動作モデル１１０として記述されることになる。
【００７１】
図６は、検証目的等から定めた制約を、図５と同じタイミング図上に付記したものである。第１の制約（制約１）として、時刻０においては、ＣＬＫ信号は「０」、ＲＥＳＥＴ信号は「Ｈ」、ＷＲＩＯ（書込み指示）は「Ｌ」に「確定」し、その他の信号は「不定」であることを規定している。
【００７２】
第１の制約（制約１）において、「確定」又は「不定」の区分はシステム仕様に依存するが、「確定」させることができる範囲が多いほど、第１の論理回路動作モデル５０から第２の論理回路動作モデル６０への縮小変換の規模を大きくすることが可能となり、結果的には検証時間（シミュレーション時間）が短縮される。
【００７３】
第２の制約（制約２）として、観測時刻と観測信号の対象を規定している。本例では、観測時刻としては時刻０と時刻３のみであり、観測信号の対象は、ＣＬＫ信号とＲＥＳＥＴ信号を除く総ての信号（図６に星印で示した点）であることを規定している。
【００７４】
時刻の規定は、ＣＬＫ信号の立ち上がりの直前で規定しており、時刻はＣＬＫ信号の立ち上がり毎に進んでいく。
【００７５】
検証目的に応じて観測時刻の範囲や観測信号を限定（制約）することで、検証時間（シミュレーション時間）が短縮される。ただし、検証時間（シミュレーション時間）の短縮は、ＣＬＫ信号を部分的に抽出することで実現されるものであり、各観測時刻の精度はＣＬＫ信号の精度を保持したものとなっている。図６に示した制約は、制約モデル１２０に記述されることになる。
【００７６】
なお、図６に示した例では、検証に必要な時刻の特定と論理回路上の構成要素の特定との双方を特定しているが、いずれか一方のみを特定する形態としてもよい。
【００７７】
図７は、図４に示したカウンタ回路１０１をハードウェア記述言語で記述した論理回路ＲＴＬモデル１００である。ハードウェア記述言語としては、Verilog-HDLを用いている。また記述レベルは、論理合成可能なレベル、即ちレジスタ・トランスファ・レベル（ＲＴＬ）である。
【００７８】
本例の論理回路ＲＴＬモデル１００は、大きくは５つのブロックから構成されている。ブロック０は、カウンタ回路１０１の入出力ポート（バス入力１０２、バス出力１０３）や内部レジスタの定義をしている部分である。
【００７９】
ブロック１は、内部レジスタの値をバス出力１０３（ＩＯＢＵＳＯ）へ出力する動作を記述している。ブロック２は、内部レジスタの設定・更新に関する動作を記述している。
【００８０】
ブロック３およびブロック４が実際にＣＬＫ信号の立ち上がりでカウンタをカウントアップする動作を記述している。
【００８１】
図８は、図７のうち、ブロック１の記述部分のみを抽出したものである。
【００８２】
１行目はコメント文である。２行目は、always文と呼ばれるもので、カッコ内のレジスタの値がひとつでも変化した場合には常にalways文以下の処理を実行せよ、と言う意味を持っている。
【００８３】
３行目以下は、「ＩＯＢＵＳＯ」レジスタへの代入命令と条件（内部レジスタの値による論理条件）を示している。
【００８４】
具体的には、ＣＳ＝１、ＲＤＩＯ＝１、ＷＲＩＯ＝０、ＡＢ＝８（ヘキサ）のときには、「ＣＯＮＴＲＯＬ」Ｌレジスタの内容を「ＩＯＢＵＳＯ」レジスタへ代入せよ、また、ＣＳ＝１、ＲＤＩＯ＝１、ＷＲＩＯ＝０、ＡＢ＝Ａ（ヘキサ）のときには、「ＣＯＵＮＴ」レジスタの内容を「ＩＯＢＵＳＯ」レジスタへ代入せよ、それ以外のときは、「ＩＯＢＵＳＯ」レジスタへ「Ｚ（ヘキサ）」（ハイインピーダンスを意味する）を設定せよ、と言う処理を示している。
【００８５】
図９は、図５に示した各信号のタイミング図を外部動作モデル１１０として記述したものである。外部動作モデル１１０もVerilog-HDLで記述している。
【００８６】
図９において、記号「＃」は遅延を意味しており、例えば「＃１０」は１０単位だけ時刻を遅延することを意味している。従って、７行目から２０行目にわたって、時刻単位の１０毎にＣＬＫ信号を立ち上げ（ＣＬＫ＝１）、また立ち下げ（ＣＬＫ＝０）るというクロックの動作が記述されている。この他、ＣＳやＲＤＩＯの立上がりや立下りのタイミングも図５に対応して記述されている。
【００８７】
（４）第１の論理回路動作モデル５０の生成（ステップ１）
第１の論理回路動作モデル５０を生成する第１段階として、Verilog-HDLで記述されたモデルを「グラフ」で記述したモデルに変換する。
【００８８】
なお、一般にグラフ理論等によれば、「グラフ」と隣接行列若しくは辺リストとは相互に変換可能である。従って、第１の論理回路動作モデル５０を隣接行列若しくは辺リストの態様で生成する形態としてもよい。
【００８９】
以下の説明では、第１の論理回路動作モデル５０を「グラフ」で記述したモデルに変換する場合を例として説明する。
【００９０】
図１１は、Verilog-HDLで記述されたカウンタ回路１０１のブロック１の部分（図８に相当する部分）を「グラフ」記述に変換したものである。
【００９１】
「グラフ」記述の第１の論理回路動作モデル５０（以下、単に第１の論理回路動作モデル５０という。）は、複数種の節点と、各節点を結ぶ矢印（枝）とで構成されている。
【００９２】
節点は、手続を示す命令（「wait」、「load」、「store」、「equal」、「select」等）を含む箱状の節点（符号３０１等）、命令が使用し或いは生成する値（r03等）を表す８角形の節点（符号３０３等）、時刻を示す変数（c0001等）および分岐状態を表す丸状の節点（符号３０２等）等によって構成されている。また、箱状の節点は、レジスタを含む記憶場所を表す変数（「CONTROL」、「COUNT」、「CS」、「ＡＢ」、「RDIO」等）を含んでいる。
【００９３】
図１１のグラフ記述は、図８のVerilog-HDLによる記述に一意に対応したものである。
【００９４】
例えば、符号３０１に示す手続は、「CONTROL」、「COUNT」、「CS」、「ＡＢ」、「RDIO」、「WRIO」の各レジスタの内容が変化するまで待て、というもので、図８の2行目のalways文に対応するものである。各レジスタの内容が変化した場合には、各レジスタに記憶されている値をそれぞれ読み込む（図１１のＡで示す範囲の処理）。
【００９５】
次に、「CS」、「ＡＢ」、「RDIO」、「WRIO」の各レジスタの内容から論理演算を行って、図８のif文（３行目、５行目）の条件判定を行っている（図１１のＢで示す範囲の処理）。判定した条件に応じて、符号３０６の手続によって「CONTROL」、「COUNT」、および「ｚ（ヘキサ）」の中から一つを選択する。選択された値は符号３０７の手続によって「ＩＯＢＵＳＯ」レジスタに書き込まれる。
【００９６】
符号３０１から符号３０８までの一連の処理は、各クロックごとに繰り返されることになる。この繰り返しは、符号３０９のcall文による末尾再帰の形態で行われる。
【００９７】
ブロック２乃至ブロック３の処理も同様にして、「グラフ」記述に変換される。また、Verilog-HDLで記述された外部動作モデル１１０（図９）も同様に「グラフ」記述に変換される。
【００９８】
図１２は、コールグラフと呼ばれる図であり、「グラフ」記述された論理回路ＲＴＬモデル１００のブロック１からブロック４の各ブロックと外部動作モデル１１０とを呼び出して統合させる手順を表現している。
【００９９】
コールグラフでは、ブロック間の統合を行うと共に、時間軸方向への展開を行っている。ブロック１からブロック４までのブロックは、いずれもalways文でクロック毎に繰り返し実行される形態となっている。そこで、コールグラフによるブロックの統合は、クロック毎に各ブロックを複製して、時間軸方向に順次結合して展開している。
【０１００】
時間軸方向への展開は、制約モデル１２０で記述された観測時刻の範囲まで展開する。本例では、図６で示したように、時刻０と時刻３を観測時刻と規定している。従って、時刻０から時刻３までの間にある３クロック分の範囲まで展開すれば十分である。
【０１０１】
このように各ブロックの処理を時間軸方向に展開することによって、クロック毎に変化する内部状態（レジスタ等の値の変化）を正確に一意に表現することが可能となる。
【０１０２】
他方、制約モデル１２０によって観測時刻を規定することによって、検証に必要となる最小限の範囲に時間軸方向の展開を制限することができる。
【０１０３】
図１３は、コールグラフに従って統合した最終形態の第１の論理回路動作モデル５０を示した図である。図１３では、外部動作モデル１１０と、３クロック分の範囲で時間軸方向に展開されたブロック１からブロック４の処理が「グラフ」記述されている。
【０１０４】
なお、「書込み待ち」と記されているラインは、クロック毎にレジスタにデータが書き込まれてその内容が変化することを待って次の処理を進めること（書込み待ち）に対応するものである。
【０１０５】
（５）評価記号表の生成（ステップ２）
次に、統合された最終形態の第１の論理回路動作モデル５０の各節点において、予め定められている記号評価規則と制約モデル１２０に基づいて、「評価記号」をもとめ、各節点と「評価記号」とを対応付けた評価記号表を生成する。
【０１０６】
ここで、記号評価規則とは、算術演算規則や論理演算規則等の一般的な規則や、「時刻が不明（未確定）な状態で読み込まれた値は不定とする」といった規則である。また、「評価記号」とは、定数や不定値のことをいう。
【０１０７】
図１４および図１５の例を用いて説明する。
【０１０８】
図１４の符号４０１の手続は、時刻０（c0000）においてＣＬＫ信号を読込む手続を示している。また、符号４０２および４０３は、時刻０（c0000）においてＲＥＳＥＴ信号を読込む手続を示している。
【０１０９】
制約モデル１２０（図６参照）では、時刻０においては、ＣＬＫ＝０、ＲＥＳＥＴ＝１と規定されている。従って、読込んだＣＬＫの値は０（定数）に確定している（ＣＬＫ＝０）。そこで、r01_14には、評価記号として定数「０」を割り付けて評価記号表に書き込む。
【０１１０】
同様に、r02_14は、時刻０におけるＲＥＳＥＴは１（定数）に確定しているため、評価記号として定数「１」を割り付けて評価記号表に書き込む。
【０１１１】
一方、符号４０８において読込まれるＣＬＫの値は、読み込み時刻が不明なため、（符号４０３のウェイト命令により、非同期なＲＥＳＥＴ信号が０にセットされる時刻に依存する）「時刻が不明（未確定）な状態で読み込まれた値は不定とする」の規則により、評価記号としては、「不定」となる。
【０１１２】
また、符号４０６と符号４０７では、いずれも定数同士の論理演算となり、その結果も定数として一意に定まる。図１４に示したように、即ち、r05_14には１（定数）が、またr07_14にも１（定数）がそれぞれ評価記号として割り付けられる。
【０１１３】
このようにして、統合した最終形態の第１の論理回路動作モデル５０の各節点における評価対象変数に対して評価記号を求めてゆき、図１５に例示したような評価記号表を生成することができる。
【０１１４】
なお、上述の説明では、定数や不定値を評価記号として取り扱い、これらの組み合わせを算術演算や論理演算等の記号評価規則に基づいて評価記号を求めている。
【０１１５】
この他、定数や不定値の評価記号に加えて、一次式、範囲式、および論理式の少なくとも１つを評価記号として取り扱い、これらの組合せを記号評価規則に基づいて評価記号を求める形態としてもよい。
【０１１６】
（６）第１の論理回路動作モデル５０に対する縮小変換判定（ステップＳＴ３）
ステップＳＴ３では、記号評価規則を参照しつつ、所定の縮小変換方法毎に、第１の論理回路動作モデル５０において縮小変換の可能性のある部位を検出し、さらに実際に縮小変換が可能か否かを判定していく。
【０１１７】
本実施形態では、読込み命令と書込み命令との短絡、書込み待ち命令と書込み命令との短絡、定数値の畳み込み、および確定した条件分岐命令の除去、の４種類の縮小変換を行う形態としている。
【０１１８】
図１６は、読込み命令と書込み命令との短絡についての可能性判定を示す図である。この判定の対象は、読込み命令（load命令）である。判定基準としては、対象とする読込み命令で読み込むレジスタと同一のレジスタに書き込む書込み命令が、対象とする読込み命令の無条件かつ直近の過去に存在することである。この判定基準を満たす読込み命令と書込み命令とは短絡可能と判定する。
【０１１９】
対象とするレジスタが同一であり、読込み命令の無条件かつ直近に書き込み命令がある場合は、これらを短絡したとしても観測時空間（観測時刻や観測対象ポイント）に影響を与えない。したがって、検証精度を劣化させることなく第１の論理回路動作モデル５０を縮小変換（短絡）することが可能となる。
【０１２０】
図１６の例では、判定対象となる読込み命令（load：60）は、「ＲＵＮ」レジスタの内容を読み込む命令である。読込み命令（load：60）と書込み命令（store：５１４）とは、同一のレジスタ、即ち「ＲＵＮ」レジスタを対象としており、書込み命令（store：５１４）は、読込み命令（load：60）の無条件かつ直近の過去という条件に合致する。この結果、読込み命令（load：60）と書込み命令（store：５１４）とは、短絡可能と判定する。
【０１２１】
図１７は、書込み待ち命令（wait命令）と書込み命令（store命令）との短絡についての可能性判定を示す図である。この判定の対象は、書込み待ち命令（wait命令）である。書込み待ち命令（wait命令）は1つ或いは複数の対象とするレジスタの内容をモニタし、対象レジスタの内容が変化しない限り待ちつづけ、変化したときに限り次へ（矢印の先の処理へ）進む命令である。
【０１２２】
書込み待ち命令と書込み命令との短絡可否の判定基準は、対象とするレジスタが同一であり、かつ対象とする書込み待ち命令に対して無条件かつ直近の未来に書込み命令がある場合である。この場合も、書込み待ち命令と書込み命令とを短絡しても観測時空間に影響を与えない。したがって、検証精度を劣化させることなく第１の論理回路動作モデル５０を縮小変換（短絡）することが可能となる。
【０１２３】
図１７の例では、判定対象となる書込み待ち命令（wait:129）は、「CS」、「RDIO」、「WRIO」、「AB」、「CONTROL」、および「COUNT」の各レジスタへの書込みの有無を待っている。そこで、「CS」、「RDIO」、「WRIO」、「AB」、「CONTROL」、および「COUNT」のいずれかのレジスタに対する書込み命令（store命令）を探索する。図１７の例では、store：５１８が「COUNT」レジスタに値r05_13を書き込む命令であり、store：５１６が「CONTROL」レジスタに値r04_13を書き込む命令となっている。したがってこれらの書込み命令が短絡候補ということになる。次に、これらの短絡候補となった書込み命令が、書込み待ち命令（wait:129）の無条件かつ直近の未来に位置するか否かを矢印（枝）で示されるパスを辿って判定する。無条件かつ直近の未来に位置すると判定されると、その書込み命令と書込み待ち命令は短絡可能と判定される。
【０１２４】
図１８は、定数の畳み込みについて説明する図である。
【０１２５】
ステップＳＴ２において、論理回路ＲＴＬモデル１００の各節点について評価記号を求めた。所定の領域において、総て評価記号が定数である場合には、定数同士の手続きの結果も定数となる。従って、その領域の手続きを総てまとめて１つあるいは複数の定数として代表させることが可能となる。この処理を定数の畳み込みと呼んでいる。
【０１２６】
図１８において、実線で囲まれた領域は、複数の論理演算命令やその入力、出力の変数を節点として構成されているが、制約モデル１２０の条件等から総ての変数の評価記号が定数であるとされている。
【０１２７】
この結果、実線で囲まれた領域は、最終的にはひとつの定数に畳み込むことが可能となる。この実線で囲まれた領域の定数を畳み込んだとしても観測時空間に影響を与えない。したがって、検証精度を劣化させることなく第１の論理回路動作モデル５０を縮小変換（短絡）することが可能となる。
【０１２８】
図１９は、確定した分岐条件の分岐命令（branch命令）の除去について説明する図である。分岐命令の分岐条件をしめす変数の評価記号が定数である場合は、分岐命令の分岐先は一意に確定される。従って、この場合には、分岐命令を除去し、分岐命令の直前の手続きと分岐命令の直後の手続きとを直接短絡させても観測時空間に影響を与えず、検証精度を劣化させること無く第１の論理回路動作モデル５０を縮小変換（短絡）することが可能となる。
【０１２９】
図１９の例では、分岐命令branch：８７の条件を決める変数r11_14の評価記号が定数と評価されている。この結果、分岐命令branch：８７を除去することが可能となる。
【０１３０】
（７）縮小変換の実行（ステップＳＴ５）
ステップＳＴ５では、ステップＳＴ３で縮小変換が可能と判断された部位に対して、実際に縮小変換を行う。具体的には、読込み命令と書込み命令との短絡、書込み待ち命令と書込み命令との短絡、定数値の畳み込み、および確定した条件分岐命令の除去、の４種類の縮小変換を行う。また、短絡、畳み込み等で不要となった記述を除去する。
【０１３１】
図２０は、第１の論理回路動作モデル５０（図１３に示したグラフ記述されたモデル：縮小変換前）と縮小変換後のモデル、即ち、第２の論理回路動作モデル６０を示すものである。
【０１３２】
縮小変換前の記述では、クロックサイクルの精度で記述されており、３３７の命令を含んでいる。これに対して、縮小変換後の記述は、トランザクションレベルの精度、即ち、バスを介しての外部からの読込み指示のタイミングでの精度で記述されたものとなっており、合計で１３４の命令数に縮小変換されている。
【０１３３】
縮小変換後の第２の論理回路動作モデル６０では、縮小変換前の第１の論理回路動作モデル５０に対して、６０．３％の命令が除去されている。
【０１３４】
シミュレーション等による検証は、縮小変換された第２の論理回路動作モデル６０に基づいて行われる。一般に、シミュレーション等の実行時間はモデルに含まれる命令数と強い相関関係をもつことが示されている。従って、命令数の削減によってシミュレーション等の時間を短縮することが可能となる。
【０１３５】
（８）解析結果報告
図２１は、縮小変換された第２の論理回路動作モデル６０に対する解析結果の報告例を示す図である。
【０１３６】
３つの読込み命令（load：213、load：96、load：716）に対して「短絡候補なし」と報告している。各読込み命令に対して、それぞれ「COUNT」レジスタ、「CONTROL」レジスタ、「RUN_next」レジスタに値を書き込む書込み命令が存在しなかったか、存在したとしてもそれが無条件かつ直近の過去に存在しなかったことを意味している。
【０１３７】
また、変数r03_13で示されている節点からは多数の枝が出ている。これは、変数r03_13が多数参照されており、影響範囲が広いことを示している。変数r03_13は、「RUN_next」レジスタの値を読込んだ値である。
【０１３８】
３つの読込み命令が「短絡候補なし」となり、また、変数r03_13が広い影響範囲をもって残存している理由は、「COUNT」レジスタ、「CONTROL」レジスタ、「RUN_next」レジスタに対して、外部動作モデル１１０や制約モデル１２０において、これらの各レジスタに対して具体的に規定していないため、各レジスタの値を不定値として取り扱ったことに起因している。
【０１３９】
この解析結果報告を受け取ったモデル作成者が、例えば、「RUN_next」レジスタの値が０（定数）であることが保証されることを何らかの方法で確認し、制約モデル１２０に時刻０において「RUN_next」レジスタの値が０（定数）であるとの記述を追加することで、縮小変換可能な範囲を増加させることができる。この結果、第２の論理回路動作モデル６０の規模をさらに縮小変換することが可能となる。
【０１４０】
本実施形態に係る論理回路動作モデル生成装置１および論理回路動作モデル生成方法によれば、制約モデル１２０で規定した時間的精度（観測時刻）と空間的精度（観測対象とするレジスタ等の範囲）を一貫して保持するように縮小変換している。この結果、生成した第２の論理回路動作モデル６０の精度は、クロック毎に内部レジスタの内容を記述した第１の論理回路動作モデル５０の精度を劣化させないことが保証されている。
【０１４１】
また、本実施形態に係る論理回路動作モデル生成装置１および論理回路動作モデル生成方法によれば、制約モデル１２０で規定した時間的精度、空間的精度が保証された形態で第２の論理回路動作モデル６０へ縮小変換している。カウンタ回路１０１に係る具体例では、命令数が３３７から１３４に削減されている。この結果、縮小変換されたモデルでのシミュレーション時間を大幅に短縮することが可能となる。
【０１４２】
さらに、第２の論理回路動作モデル６０の生成は、論理回路ＲＴＬモデル１００、外部動作モデル１１０、および制約モデル１２０のみから自動的に生成することができる。
【０１４３】
この結果、論理回路ＲＴＬモデル１００が既に存在する場合には、一般的に規模の大きな論理回路ＲＴＬモデル１００の詳細な構造や内部状態に関する知識をモデル作成者（第２の論理回路動作モデル６０の作成者）が知らない場合であっても、外部動作に関する知識と検証に必要な知識があれば外部動作モデル１１０と制約モデル１２０を生成することによって、自動的に第２の論理回路動作モデル６０が生成される。
【０１４４】
このため、第２の論理回路動作モデル６０の生成に係る工数を大幅に削減することができる。
【０１４５】
さらに、本実施形態に係る論理回路動作モデル生成装置１および論理回路動作モデル生成方法によれば、制約モデル１２０に記述を追加する等によって、過去に作成した論理回路動作モデルからより効率の高い論理回路動作モデルを生成することができる。このため、過去の改良結果を積み重ねて利用することも可能であり、改良に関する時間を削減することが可能である。
【０１４６】
また、解析結果報告には、影響範囲の広い箇所が明示される。そこで、影響範囲の広いものから優先的に、例えば、不定であった条件を具体的に特定できるか否かを論理回路設計者に問い合わせて確認することもできる。このように、条件特定のための調査にかかる工数も削減することができる。
【０１４７】
なお、本発明は上記の実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせても良い。
【図面の簡単な説明】
【０１４８】
【図１】本発明に係る論理回路動作モデル生成装置および論理回路動作モデル生成方法の位置付けを説明する図。
【図２】本発明に係る論理回路動作モデル生成装置の実施形態の構成例を示す図。
【図３】本発明に係る論理回路動作モデル生成方法の基本的な処理の流れを示すフローチャート。
【図４】論理回路ＲＴＬモデルを説明するための具体例としてのブロック図。
【図５】外部動作モデルを説明するための具体例としてのタイミングチャート。
【図６】制約モデルを説明する具体例を示す図。
【図７】Verilog-HDLで記述された論理回路ＲＴＬモデルの具体例を示す第１の図。
【図８】Verilog-HDLで記述された論理回路ＲＴＬモデルの具体例を示す第２の図。
【図９】Verilog-HDLで記述された外部動作モデルの具体例を示す図。
【図１０】制約モデルを記述した具体例を示す図。
【図１１】グラフで記述された論理回路ＲＴＬモデルの具体例を示す図。
【図１２】コールグラフの具体例を示す図。
【図１３】統合された第１の論理回路動作モデルの具体例を示す図。
【図１４】評価記号の生成方法の一例を示す図。
【図１５】生成される評価記号表の一例を示す図。
【図１６】読込み命令と書込み命令の短絡判定の一例を示す図。
【図１７】書込み待ち命令と書込み命令の短絡判定の一例を示す図。
【図１８】定数の畳み込み判定の一例を示す図。
【図１９】確定した条件の分岐命令削除判定の一例を示す図。
【図２０】縮小変換前の論理回路動作モデルと縮小変換後の論理回路動作モデルの一例を示す図。
【図２１】解析結果報告の一例を示す図。
【符号の説明】
【０１４９】
１  論理回路動作モデル生成装置
２  生成部
３  変換部
３０  記号評価部
３１  縮小変換判定部
３２  更新部
５０  第１の論理回路動作モデル
６０  第２の論理回路動作モデル
７０  解析結果
１００  論理回路ＲＴＬモデル
１１０  外部動作モデル
１２０  制約モデル
【図１】
2007011477.tif 000003
【図２】
2007011477.tif 000004
【図３】
2007011477.tif 000005
【図４】
2007011477.tif 000006
【図５】
2007011477.tif 000007
【図６】
2007011477.tif 000008
【図７】
2007011477.tif 000009
【図８】
2007011477.tif 000010
【図９】
2007011477.tif 000011
【図１０】
2007011477.tif 000012
【図１１】
2007011477.tif 000013
【図１２】
2007011477.tif 000014
【図１３】
2007011477.tif 000015
【図１４】
2007011477.tif 000016
【図１５】
2007011477.tif 000017
【図１６】
2007011477.tif 000018
【図１７】
2007011477.tif 000019
【図１８】
2007011477.tif 000020
【図１９】
2007011477.tif 000021
【図２０】
2007011477.tif 000022
【図２１】
2007011477.tif 000023