(57)【特許請求の範囲】
【請求項１】
動作レベルの記述に対するレジスタ転送レベルの記述の等価性を検証する動作レベル記述とレジスタ転送レベル記述間の等価性検証方法であって、
動作合成手段が、第１の記憶装置から動作レベルの記述を読み出し、前記動作レベルの記述から１つ又は複数の工程を経てレジスタ転送レベルの記述を生成し、前記各工程後の中間レベルの記述を生成し、前記各工程前後の記述の対応関係を生成し、前記レジスタ転送レベルの記述と前記中間レベルの記述と前記対応関係とを第２の記憶装置に記憶するステップと、
モデル抽出手段が、前記第１および第２の記憶装置から前記動作レベルの記述と前記レジスタ転送レベルの記述と前記中間レベルの記述とを読み出し、有限状態機械をベースとする制御構造と信号の更新を表現可能なモデルを抽出し、第３の記憶装置に記録するステップと、
信号値抽出手段が、前記第３の記憶装置から前記モデルを読み込み、当該モデル上でシンボリックシミュレーションを行い、信号値の更新関数を抽出し、第４の記憶装置に記録するステップと、
関数等価性比較手段が、前記第２および第４の記憶装置から前記更新関数と前記対応関係を読み出し、前記対応関係に基づき対応する信号の更新関数を比較するステップとを含む
動作レベル記述とレジスタ転送レベル記述間の等価性検証方法。
【請求項２】
前記シンボリックシミュレーションにおいては、入力端子からの値の入力及び出力端子への値の出力を関数で表現する請求項１記載の動作レベル記述とレジスタ転送レベル記述間の等価性検証方法。
【請求項３】
動作レベルの記述に対するレジスタ転送レベルの記述の等価性を検証する動作レベル記述とレジスタ転送レベル記述間の等価性検証装置であって、
第１の記憶装置から動作レベルの記述を読み出し、前記動作レベルの記述から１つ又は複数の工程を経てレジスタ転送レベルの記述を生成し、前記各工程後の中間レベルの記述を生成し、前記各工程前後の記述の対応関係を生成し、前記レジスタ転送レベルの記述と前記中間レベルの記述と前記対応関係とを第２の記憶装置に記憶する動作合成手段と、
前記第１および第２の記憶装置から前記動作レベルの記述と前記レジスタ転送レベルの記述と前記中間レベルの記述とを読み出し、有限状態機械をベースとする制御構造と信号の更新を表現可能なモデルを抽出し、第３の記憶装置に記録するモデル抽出手段と、
前記第３の記憶装置から前記モデルを読み込み、当該モデル上でシンボリックシミュレーションを行い、信号値の更新関数を抽出し、第４の記憶装置に記録する信号値抽出手段と、
前記第２および第４の記憶装置から前記更新関数と前記対応関係を読み出し、前記対応関係に基づき対応する信号の更新関数を比較する関数等価性比較手段と
を含む動作レベル記述とレジスタ転送レベル記述間の等価性検証装置。
【請求項４】
前記シンボリックシミュレーションにおいては、入力端子からの値の入力及び出力端子への値の出力を関数で表現する請求項３記載の動作レベル記述とレジスタ転送レベル記述間の等価性検証装置。
【請求項５】
コンピュータを、
第１の記憶装置から動作レベルの記述を読み出し、前記動作レベルの記述から１つ又は複数の工程を経てレジスタ転送レベルの記述を生成し、前記各工程後の中間レベルの記述を生成し、前記各工程前後の記述の対応関係を生成し、前記レジスタ転送レベルの記述と前記中間レベルの記述と前記対応関係とを第２の記憶装置に記憶する動作合成手段と、
前記第１および第２の記憶装置から前記動作レベルの記述と前記レジスタ転送レベルの記述と前記中間レベルの記述とを読み出し、有限状態機械をベースとする制御構造と信号の更新を表現可能なモデルを抽出し、第３の記憶装置に記録するモデル抽出手段と、
前記第３の記憶装置から前記モデルを読み込み、当該モデル上でシンボリックシミュレーションを行い、信号値の更新関数を抽出し、第４の記憶装置に記録する信号値抽出手段と、
前記第２および第４の記憶装置から前記更新関数と前記対応関係を読み出し、前記対応関係に基づき対応する信号の更新関数を比較する関数等価性比較手段と
して機能させるプログラム。
【請求項６】
前記シンボリックシミュレーションにおいては、入力端子からの値の入力及び出力端子への値の出力を関数で表現する請求項５項に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、複数の論理回路が論理的に等価であるかどうかを検証する論理回路等価検証装置に関し、特に動作合成システムの入力となる動作レベル記述と出力となるレジスタ転送レベル回路が等価であるかどうかを検証するものに関する。
【背景技術】
【０００２】
一般に、LSI もしくはVLSIの設計にあたっては、設計を自動的に行う、もしくは支援するLSI 設計自動化・支援技術が採用されている。この、LSI 設計自動化・支援技術を採用したVLSI設計のうち、代表的なものとしては、各種EDA(electronic design automation) ツールを利用したトップダウン設計があげられる。この種のトップダウン設計は、その上流工程から、機能設計、論理設計、レイアウト設計と大別することができる。このうち、とくに機能設計の自動化は動作合成（高位合成、機能合成とも呼ばれる）と呼ばれ、論理設計の自動化は論理合成と呼ばれる。
【０００３】
詳しくは、前述のトップダウン設計においては、まず、システムの仕様作成として、LSI 全体をシステムと捉え、その動作を記述することが行われる。このようにして作成された記述は、動作レベル記述（behavioral description）と呼ばれる。この動作レベル記述の作成は、たとえば、Ｃ言語ライクな言語を用いてなされる。
【０００４】
次に、動作合成フェーズにおいて、作成された動作レベル記述がRTL(register transfer level)記述に自動変換される。なお、従来、このフェーズに関しては、人手により置き換えられ、 HDL(hardware description language) を用いて、直接、RTL 記述を作成される場合が多かった。
【０００５】
次いで、論理合成フェーズにおいて、RTL 記述が、ゲートレベルの記述（ゲートレベル論理回路：ネットリスト) に自動変換される。このようにして生成されたネットリストをもとに、レイアウト設計が行われ、ついで、チップ設計が行われる。
【０００６】
これら上述した各段階（フェーズ）において合成を行うためのツールの実態は、一般に、ソフトウェアで構成される。しかしながら、それらはソフトウェアである以上必ずしもバグがないとはいえず、各合成段階においては、適切な合成がなされたか否かの検証をする必要がある。
【０００７】
ここで、上述したフェーズの内、論理合成に関しては、比較的、以前から活発に行われていたため、その正当性を確立すべく、論理合成の検証（論理検証）も活発に行われていた。これに対して、動作合成については、上記のように人手により置き換えられることが多いため、その検証についても、論理検証ほどは、検討されていなかった。
【０００８】
【非特許文献１】2000年、フォーマルメソッド・イン・システムデザイン、第16号、59-91頁(Formal Methods in System Design, No. 16, pp.59-91, 2000)
【非特許文献２】1999年、インターナショナルカンファレンスオンコンピュータデザイン、458-466頁（International Conference on Computer Design, pp. 458 -466, 1999）
【発明の開示】
【発明が解決しようとする課題】
【０００９】
しかしながら、近年のLSI の高集積化・大規模化に伴い、LSI を構成するゲート数は、数百万になることも珍しくなくなってきており、これに起因して、動作合成に対する要求も高まってきている。また、これに関連して、動作合成フェーズの正当性の検証も非常に重要な研究課題となってきている。
【００１０】
ここで、従来最も一般的に行われていた動作合成フェーズにおける正当性の検証は、所定のテストパターンを用いて行われるシミュレーションであったが、このシミュレーションは以下のような問題を含んでいた。
【００１１】
すなわち、テストパターンを用いて行われるシミュレーションを実行するためには、当然ながら、テストパターンの生成を行わなければならず、そのために時間およびコストがかかるといった問題があった。しかも、そのシミュレーションを実行することにより検証できる合成の内容は、テストパターンに依存しており、使用したテストパターンにて考慮されていないエラーを検証することはできない。従って、従来のシミュレーションによる検証では、満足する結果を得られない恐れもあった。
【００１２】
また、動作合成において動作レベル記述から生成されたRTL 記述の正当性を検証する他の手法としては、たとえば動作レベル記述との等価性検証によってRTL 記述の正当性を検証するものも研究されている。
【００１３】
たとえば、動作合成の検証装置の一例が、非特許文献１に記載されている。非特許文献１に記載された動作合成の検証装置は、動作レベル記述およびRTL 記述、そして動作合成の副産物である対応関係から、PVS という定理証明システムのための、1)形式仕様 記述、2)等価性条件(correctness lemmas), 3)検証スクリプトを出力する。等価性条件とは、動作レベル記述およびRTL 記述の分岐・合流構造を含まない基本ブロック(basic block) 毎に実行パス（状態の系列）を抽出し、実行パスの対応関係と信号の対応関係が与えられたときに、各対応するパス毎に対応する信号値の変化が同じであることを表す論理式のことである。PVS は検証スクリプトにしたがって、各パスを実行したときの各信号値の変化を表す関数を項書換えを用いて生成する。そして、対応するパスにおける対応する信号ペアに対して、その変化を表す関数が等価であることを調べる。全ての対応するパスのペア、全ての対応する信号値のペアに対して、その変化を表す関数が等価であることをしめすことにより、動作レベル記述とRTL 記述が等価であることを検査する。
【００１４】
また、動作合成の検証装置の別の一例が、非特許文献２に記載されている。非特許文献２に記載された動作合成の検証装置は、実行パスを抽出し、実行パスの対応関係と信号の対応関係が与えられたときに、各パスを実行したときの各信号値の変化を表す関数を生成して、対応するパスの対応する信号に対してこの関数が等価であることを調べるのは非特許文献１と同じであるが、抽出する実行パスが基本ブロックに制限されない。もとの動作レベル記述の繰り返し構造（ループ構造）に対して、RTL 記述に対応する実行パスが見つかるまでループを展開しながら実行パスを抽出する。また、信号値の変化を表す関数の生成は、項書換えではなく、シンボルシミュレーションという技術を用いる。
【００１５】
しかしながら、非特許文献１及び２に記載の従来の検証装置では、次のような問題がある。
【００１６】
第１の問題点は、動作レベル記述とRTL 記述との完全な等価性検証を扱っていないということである。その理由は、動作合成で行なわれる工程をいわゆるスケジューリングやバインディングのみに限っているためである。一般に、動作合成では、かかる工程のみならず、動作レベル記述を受けて後の工程に適した形に変換する前処理工程やバインディングを終えた記述を論理合成可能なRTL 記述に変換する後処理工程がおこなわれる。しかし、動作レベル記述とRTL 記述の間では抽象度の乖離が非常に大きく、これらの工程を含む動作レベル記述とRTL 記述との完全な等価性検証を一度に行うことは困難である。
【００１７】
第２の問題点は、検証に時間がかかるということである。その理由は、非特許文献１、２では記述に制御構造があったときは、合流のないパス（実行系列）を抽出し、それぞれのパスに対して信号値の変化を抽出し比較している。実行系列の数は分岐合流構造の個数に対して指数的に増大するため、制御構造が複雑になると抽出されるパスの数が増大し、シンボルシミュレーションや関数値の比較の回数が増大するため、結果として検証に時間がかかるためである。
【００１８】
［発明の目的］
本発明の目的は、動作合成における合成の検証に関し、時間及びコストの経済化を図り、且つ、満足の行く結果を自動的に得ることのできる検証ツールを提供することを目的とする。
【課題を解決するための手段】
【００１９】
本発明の発明者は、上記課題を解決するにあたり、動作合成の内部で行われる処理について検討した。
【００２０】
一般に、動作合成装置は、動作レベル記述からRTL 記述の導出を、細かい工程による記述の変形を積み重ねて行う。詳しくは、まず前処理として、動作レベル記述を受けて関数呼び出しの解消などといった後の工程に適した形への変形、不要コードの削除による変形、言語レベル最適化による変形などを行う。次に、これらの前処理された記述を受けて、どのステップ（もしくはステート）でどの動作・演算を実行すべきかを決めるスケジューリング工程を行う。さらに、スケジュールされた記述を受けて、値を保持するためのレジスタを生成し、コストが最小となるように共有化し、このレジスタを変数に割り当て、置き換えるレジスタバインディング工程、演算器の数を最適となるように記述中の演算子に演算器を割り当て、置き換える演算器マッピング（演算器バインディングとも言う）工程、さらに、バインディングを終えた記述を論理合成可能なRTL 記述に変換する後処理工程を行う。そして、これらの工程終了時にはそれぞれ中間レベル記述が得られる。
【００２１】
本発明は、動作合成装置と密接な連携を取り、各工程終了後の中間レベル記述を出力させ、工程ごとにそれぞれその前後の中間レベル記述間の等価性を検証することを特徴としている。中間レベル記述間の抽象度の乖離は、動作合成装置の入力と出力である動作レベル記述とRTL 記述間の抽象度の乖離よりも小さく、その間で行われる工程が明確にわかっているために等価性検証を容易に行うことができる。動作合成のすべての工程について中間レベル間の等価性検証を行うことにより、動作レベル記述とRTL 記述との完全な等価性検証が可能となる。
【００２２】
さらに、動作合成装置に中間レベル記述間の対応関係を出力させる。動作合成の各工程では記述の変形が行われているが、動作レベル記述とRTL 記述を直接比較する場合には、どの記述がどの記述に置き換えられたのか、どの変数がどのレジスタに置き換えられたのか、といった対応関係を自動的に認識することができないため、その等価性検証には設計者による対話的な操作を必要とする半自動的なものになってしまっている。しかし、これらの情報を動作合成システムが出力することにより、等価性検証を自動で行うことができる。
【００２３】
また、本発明では、各工程の前後の記述の等価性の検証は、それぞれの記述から「有限状態機械をベースとする制御構造と信号の更新を表現可能なモデル」を抽出し、このモデル上でシンボリックシミュレーションを行うことで信号値の更新を関数で表し、対応する信号の更新関数が等価であることを検証することで行う。そして、モデルの抽出に際しては合流状態に入射する遷移が必ず２つであるようにモデルに変換し、シンボリックシミュレーションにおいては合流状態に到達したときにif-then-elseによる表現式をもちいて合流後の信号値の更新を関数で表すようにすることにより、記述の制御構造における分岐合流構造をシンボルシミュレーションで扱うことを容易にし、且つ、このモデルのもとで合流構造にも適用可能なシンボルシミュレーションの手順を実現している。このため、制御構造が複雑であっても、実行パスをすべて抽出する必要がなくなり、これにより検証時間の短縮を可能とする。
【発明の効果】
【００２４】
本発明においては、次のような効果を奏する。
【００２５】
第１の効果は、動作レベル記述とRTL 記述との完全な等価性検証を扱うことができることにある。その理由は、前述のように動作合成装置が出力する各工程後の中間レベル記述により、動作レベル記述とRTL 記述の等価性検証を、各工程前後の等価性検証という、より容易な問題に帰着しているためである。
【００２６】
第２の効果は、検証に必要となる時間を短縮することができることにある。その理由は、シンボリックシミュレーションを行う上で都合のよいモデルを考案し、その上で、合流構造を扱えるシンボリックシミュレーションの手順を考案したためである。
【発明を実施するための最良の形態】
【００２７】
次に、本発明の実施の形態について図面を参照して詳細に説明する。
【００２８】
図１を参照すると、本発明の第一の実施の形態は、動作レベル記述を記憶する記憶装置１と、動作合成装置２と、ＲＴＬ記述を記憶する記憶装置３と、動作合成の中間レベル記述及び対応関係を記憶する記憶装置４と、モデル抽出装置５と、モデルと対応関係を記憶する記憶装置６と、信号値関数を抽出する装置７と、信号値関数を記憶する装置８と、信号値関数の等価性を比較する装置９とを含んで構成されている。このような装置はパーソナルコンピュータやワークステーション等のコンピュータと等価性検証プログラムとで実現することができる。等価性検証プログラムは磁気ディスク等のコンピュータ可読記録媒体に記録されて提供され、コンピュータに読み込まれることにより、そのコンピュータの動作を制御し、そのコンピュータ上にモデル抽出装置５、信号値関数抽出装置７、関数等価性比較装置９に相当する機能手段を実現する。
【００２９】
図２を参照すると、動作レベル記述が例示されている。この動作レベル記述の作成は、たとえば、Ｃ言語ライクな言語を用いてなされる。記憶装置１は動作レベル記述をあらかじめ記憶しておく。
【００３０】
動作合成装置２は、動作レベル記述を入力とし、処理の過程で中間レベル記述及び対応関係を出力しながら、最終的にＲＴＬ記述を出力とする装置である。ＲＴＬ記述は動作合成装置２から出力された後、記憶装置３に記憶される。中間レベル記述は、動作合成装置２の各工程終了後に出力される合成中途の記述である。中間レベル記述は動作合成装置２より出力され、記憶装置４に記憶される。中間レベル記述の出力は、例えばＣ言語ライクな言語を用いてなされる。図３、図４を参照すると中間レベル記述が例示されている。図３は、前処理工程後の中間記述の例である。図４は、スケジューリング・バインディング工程後の中間記述の例である。図３、図４において、“input”と宣言される信号は入力信号を表している。“output”と宣言される信号は出力信号を表している。“variable”と宣言される信号はそれぞれ通常の信号を表している。“terminal”と宣言される信号は通常の配線信号を表している。“register”と宣言される信号はそれぞれレジスタとなる信号を表している。その他はＣ言語の記述法にのっとっている。対応関係は、動作合成装置２の内部工程において行われる記述変換操作について、その前後の記述間の対応情報である。対応関係は、動作合成装置２によって出力され、記憶装置４に記憶される。
【００３１】
モデル抽出装置５は、動作レベル記述、中間レベル記述、ＲＴＬ記述から、それぞれ有限状態機械をベースとする制御構造と信号の更新を表現可能なモデルを抽出する装置である。有限状態機械をベースとする制御構造と信号の更新を表現可能なモデルには、たとえば拡張有限状態機械モデル（EFSMモデル, Extended Finite State Machine）が使用される。EFSMモデルは、状態の集合S 、p 次元の入力値の集合I = I1 × I2 × I3× ... ×Ip 、q 次元の出力値の集合O = O1 × O2 ×O3 × ... × Oq 、n 次元の信号値の集合D = D1 × D2 ×D3 ×... × Dn 、遷移条件関数の集合F = ｛ f1, f2, ... ｝、信号値更新関数の集合U = ｛ u1, u2, ... ｝、遷移関係の集合Ｔから構成される順序機械の表現形式である。
【００３２】
遷移条件関数fiは信号値の集合D と入力値の集合I から真偽値への関数である（D × I ->｛0,1 ｝）。
【００３３】
信号値更新関数uiは、信号値の集合D と入力値の集合I から信号値の集合D と出力値の集合O への関数である（D× I -> D × O）。
【００３４】
遷移関係は状態の集合S と遷移条件関数の集合F から状態の集合S と信号値更新関数の集合U への関数である(S × F -> S × U)。
【００３５】
EFSMモデルは有向グラフを用いて表現する。グラフの頂点が状態に対応し、グラフの枝が遷移に対応する。遷移にはその遷移の遷移条件と動作内容がラベル f/uとして付記される。
【００３６】
EFSMモデルの入力、出力、信号値はそれぞれ固有の名前を持ち、名前でその値を参照可能である。この名前はそれぞれ、動作レベル記述、RTL 記述および中間レベル記述の、同名の入力ポート名、出力ポート名、信号名（変数やレジスタ）に対応する。
【００３７】
EFSMの状態はいくつかのグループに分割される。このグループをブロックと呼ぶ。ひとつのブロックに属する状態は遷移で連結されている。ブロック中のどの状態からも遷移が入射しない状態をブロック開始状態と呼ぶ。ブロック外の状態への遷移が出射する状態をブロック終了状態と呼ぶ。
【００３８】
図５および図６を参照するとEFSMモデルが例示されている。この図５のEFSMモデルは図３に例示されている中間記述から変換したものである。この図６のEFSMモデルは図４に例示されている中間記述から変換したものである。状態および遷移がそれぞれグラフで表現される。グラフの頂点は状態を表し、状態の名前が付記されている。グラフの枝が遷移を表し、遷移条件と信号値更新関数が付記されている。ブロックは破線四角で表現される。
【００３９】
本発明で扱うEFSMの状態には、分岐状態、合流状態、通常状態がある。これらはすべて排他である。分岐状態は２本の遷移が出射する状態である。合流状態は２つの遷移が入射する状態である。通常状態は入射する遷移も出射する遷移も一つの状態である。
【００４０】
本発明で扱うEFSMの遷移には、通常遷移、分岐遷移、合流遷移がある。これらはすべて排他である。分岐遷移とは分岐状態から出射する遷移である。合流遷移とは合流状態に入射する遷移である。分岐遷移、合流遷移は信号値を変更しないし、何も出力しない。
【００４１】
本発明で扱うEFSMには、ブロック分割についていくつかの制限が設けられている。まず第一に、各ブロックの内部には繰り返し構造を含んでいてはならない。これは、繰り返し構造を持つ記述を対象にしないということではない。繰り返し構造がある記述に対しては、繰り返しの開始部分までのブロック、繰り返しの本体部分のブロック、繰り返し終了後のブロックというブロックに分割すれば、各ブロックは繰り返し構造を持たない。
【００４２】
次に、任意の状態において出射する遷移は高々２本であり、ブロック開始状態以外の状態において入射する遷移は高々２本でなければならない。もとの記述において３個所以上からの合流がある場合には、新たに生成された合流状態および合流遷移によって分解される。この制約によって、後述するシンボリックシミュレーションにおいて合流のある制御構造を扱うことを可能としている。
【００４３】
最後に、各ブロックのブロック開始状態はただ一つでなければならない。また、任意の二つのブロックにおいてそのブロック間遷移はただ一つでなければならない。
【００４４】
信号値関数抽出装置７は、モデルから信号値関数を抽出する装置である。信号値関数は、信号値の変化を表した関数であり、任意の変数及び任意の演算により表現される。信号値関数は記憶装置８に記憶される。
【００４５】
関数等価性比較装置９は、入力された二つの関数を比較し等価な関数であることを判定する装置である。
【００４６】
次に、図を参照して本実施の形態の動作について詳細に説明する。
【００４７】
動作合成装置２では入力である動作レベル記述がRTL 記述に自動変換される。動作合成に関しては、例えば文献「2000年、アイ・イー・イー・イー・トランザクションズ・オン・コンピュー タ・エイディッド・デザイン・オブ・インテグレイティッド・サーキット・アンド・システムズ、第19巻、第11号、1507-1522 頁（IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, Vol.19, No.11, pp.1507-1522, 2000）」に示されている既知の方法を用いる。
【００４８】
動作合成の内部では細かい工程が記述の変形を順に行っており、各工程終了時にはそれぞれ中間レベル記述が得られる。
図１に例示される動作合成装置２は、「前処理工程」「スケジューリング・レジスタバインディング工程」「演算器バインディング工程」「後処理工程」の工程毎に中間レベル記述を出力する。
動作合成装置は、各工程における処理によって、工程前の中間記述におけるどの信号が、工程後の中間記述におけるどの信号に変換されたかという情報を持っている。また、工程前の中間記述におけるどの記述群が、工程後の中間記述におけるどの記述群に変換されたかという情報ももっている。動作合成装置は、これらの情報を対応関係として出力する。図７を参照すると対応関係が例示されている。図７に例示される対応関係においては、図３に例示される中間記述におけるラベルＬ０１，Ｌ０２から始まる記述群それぞれに対して、図４に例示される中間記述におけるラベルＬ１１，Ｌ１２から始まる記述群が対応することを表している。また、それぞれの記述群の開始時点における信号の対応関係が示されている。たとえば、ラベルＬ０１の時点における信号i1は、ラベルＬ１１における信号in0に対応していることが指定されている。その他の信号についても同様である。
【００４９】
論理等価性検証装置は、図８に示される処理フロー中のステップ１の繰り返しによって、各工程における、その前後の中間レベル記述が等価であることを調べる。ただし、最初の工程では前の記述は動作合成装置２の入力である動作レベル記述であり、最後の工程では後の記述は動作合成装置２の出力であるRTL 記述であるが、以下の説明では統一的に中間レベル記述と呼ぶ。以下の説明では、検証の対象として注目する工程の前の中間レベル記述を中間レベル記述H とよび、この工程の後の中間レベル記述を中間レベル記述L とよぶ。
【００５０】
図９を参照するとステップ１の詳細が示されている。
【００５１】
ステップ１１で、中間レベル記述H および中間レベル記述L からそれぞれEFSMモデルを抽出する。ステップ１１の詳細な手順を以下に示す。
【００５２】
中間レベル記述中の全ての文は、信号への代入を定義する「代入文」、条件分岐による制御構造を表現する「条件分岐文」(if 文) 、非条件分岐による制御構造を表現する「非条件分岐文」（goto文およびlabel 文）に帰着して表現されているものとする。ただし、他の構文はすべてこれらに読み替えることができるため一般性を失わない。
【００５３】
記述の実行順序である上から下に順に、文の種類に従って以下のようにEFSMに変換する。
【００５４】
「代入文」に対して、通常遷移を生成する。代入文の内容から通常遷移の信号値更新関数を定義する。この定義は、代入文の代入定義式をそのまま用いる。
【００５５】
図１０を参照すると代入文のEFSMへの変換の処理が例示されている。この例では、代入文「e=a+b+d 」の前の文まで変換処理が終わっている。このときの状態がS7である。これに続き、これからこの代入文の処理が行われる。代入文に対しては通常遷移が生成され、遷移条件がTRUEに、信号値更新関数が「e=a+b+d 」となり、遷移後の状態がS8である。これ以後は、この代入文につづく文が続いて変換される。
【００５６】
「条件分岐文」に対して、分岐状態、合流状態と、分岐遷移、合流遷移を生成する。分岐内部の文に対する処理は再帰的に行う。ただし、if文以下の文に制御が移ることがない場合には合流状態および合流遷移は生成しない。合流状態が生成される時は、分岐状態と合流状態の間に相互リンクを張っておき、対応する分岐状態や合流状態がわかるようにしてもよい。これは、分岐状態から合流状態までの遷移系列により決定される。たとえば、分岐状態から合流状態までの遷移系列に、相互リンクのない合流状態がない、などである。先に述べたように、分岐遷移、合流遷移では信号値は更新されない。すなわち、各信号値は保存されるように信号値更新関数が定義される。
【００５７】
図１１を参照すると条件分岐文のEFSMへの変換の処理が例示されている。この例では、条件分岐文「if(a<b) ｛... ｝else｛... ｝」の前の文までの変換処理が終わっており、このときの状態がS1である。これからこの条件分岐文の処理が行われる。この条件分岐文に対しては分岐状態と分岐遷移が生成される、条件成立側の分岐遷移の遷移条件は「a<b 」となる。信号値は更新されない。条件非成立側の分岐遷移の遷移条件は「!(a<b)」となる。これも信号値は更新されない。分岐遷移後の状態はそれぞれS2, S14 となる。条件成立側、非成立側の分岐の内部の処理はそれぞれ再帰的に行われる。変換後の状態はそれぞれS13, S15となっている。その後合流遷移が生成される。合流遷移の遷移条件は共にTRUE, 信号値は更新されない。合流後の状態はS16 となっている。その後、条件分岐文に続く文の変換を続けて行う。
【００５８】
「非条件分岐文」に対して、合流状態と合流遷移を生成する。このとき、その合流方法が飛び先のラベルに合流する他の遷移に依存して２種類ある。
【００５９】
飛び先のラベルに合流する他の遷移の中に、もっとも最近の分岐（合流状態と相互リンクが張られているものを除く）が同じものどうしのペアが存在する場合は、このペアに対して合流状態および合流遷移を生成する。さらに、このとき、分岐状態と合流状態の相互リンクを張る。
【００６０】
このようなペアがつくれないときは、分岐の履歴が似ているものどうしでペアをつくり合流状態を生成する。分岐の履歴が似ているとは、履歴のはじめの部分系列が同じであることのことである。このときは、分岐状態が特定できないので分岐状態と合流状態の間に相互リンクはつくらない。
【００６１】
以上を繰り返して、ひとつのラベルに遷移する複数のgoto文に対して合流状態に入射する遷移がつねに２本であることを保証しながら合流する。
【００６２】
「条件分岐文」と同様に、分岐遷移、合流遷移では信号値は更新されない（各信号値は保存されるように信号値更新関数が定義される）。
【００６３】
図１２を参照すると非条件分岐文のEFSMへの変換の処理が例示されている。この例には３つの分岐先が同じ非条件分岐文「goto STXX 」が含まれている。それぞれ、非条件分岐文の前までの変換処理が終了しており、状態がそれぞれSa, Sb, Sdである。この３つの非条件分岐文のうち、非条件分岐文(1) および(2) が最も最近の分岐が同じであるためにペアとなる。そこで、これらに対し合流遷移を生成する。合流遷移の遷移条件は共にTRUE, 信号値は更新されない。合流後の状態はScとなっている。さらに、最も最近の分岐と相互リンクが張られる。つぎに、これ以上最も最近の分岐が同じであるペアが作れないので、合流後のScと非条件分岐文(3) とのペアを作る。これらに対して合流遷移を生成する。合流遷移の遷移条件は共にTRUE, 信号値は更新されない。合流後の状態はSeとなっている。分岐状態が特定できないので分岐状態との相互リンクは作らない。
【００６４】
RTLに近いレベルでは、複数の連続する複数の文を同時に実行することが指定されている場合がある。このような場合、レジスタと内部端子の別が明示されたり、信号値の更新のタイミングを明示的に指定したり（クロックバウンダリに対応する）、更新の依存関係が上から下へとなっていない場合がある。このようなときには、一つの状態における信号（レジスタ値）の更新関係を項書換え手法を用いて抽出し、これから得られた信号値更新関数により通常遷移を生成する。
【００６５】
かかる手順で得られたEFSMモデルをEHおよびELと呼ぶこととする。EHは中間レベル記述H に対応するEFSMモデル、ELは中間レベル記述L に対応するEFSMモデルである。
【００６６】
先に述べたように動作合成装置２は、対応関係により中間レベル記述における記述群を指定している。この記述群の情報を元にEFSM EH,ELのブロック分割の情報とする。ただし、記述群それぞれに対応してブロックを分割する必要はなく、先に述べたEFSMモデルの制限を満たす限り幾つかの処理単位を集めて一つのブロックとすることが可能である。これら情報により、EFSM EH,ELのそれぞれについてブロック開始状態、ブロック終了状態が指定される。
【００６７】
ブロック開始状態、ブロック終了状態が指定されると、記憶装置４に格納された対応関係からブロック開始状態、終了状態の対応関係がさらに指定される。得られた対応関係は記憶装置６に記憶される。
【００６８】
図３に例示されている中間記述から変換されたEFSMを例示した図５を参照すると、EFSMが二つのブロックL01 とL02 に分割されている様子が例示されている。同様に、図４に例示されている中間記述から変換されたEFSMを例示した図６を参照すると、EFSMが二つのブロックL １１とL １２に分割されている様子が例示されている。
【００６９】
さらに動作合成装置２によって出力されている記述群の対応関係により、EHのブロック開始状態SsとELのブロック開始状態Ss'の組（対応関係）及び、EHのブロック終了状態SeとELのブロック終了状態の組（対応関係）が指定される。
【００７０】
また、信号の対応関係からEHの信号r とELの信号r'の組（対応関係）が指定される。ここで、 EFSM EHのすべての信号に対して対応関係が与えられているわけではない。対応関係が与えられていない信号は、後に述べる信号関数比較において、比較対象信号とはしない。
【００７１】
図１８を参照すると、対応関係が例示されている。ブロックの対応関係からＥＦＳＭ２のブロックＬ１における状態Ｓ０，状態Ｓ１６がそれぞれＥＦＳＭ３のブロックＬ１１における状態Ｓ０，状態１８に対応することが示されている。また、このブロックにおいて、i1とin0が、i2とin1が、oとout0がそれぞれ対応していることなどが示されている。
【００７２】
ステップ１２では、両方のEFSMモデルEH、ELから、各ブロックの開始状態Ss、終了状態Se、信号r のペアごとに、信号値更新関数V(Ss,Se)(x) 及び遷移条件関数C(Ss,Se)(x) を生成する。信号値更新関数とはブロックの開始状態Ssから終了状態Seまで実行したときの信号値の変化を、開始状態Ssにおける信号値のベクトルx で表す関数である。遷移条件関数とはブロックの開始状態Ssから終了状態Seまで実行するための条件をブロック開始状態Ssにおける信号値のベクトルx で表す関数である。
【００７３】
図１３は、ステップ１２の詳細な手順である。かかる手順では、EFSMの各状態に対して、ブロック開始状態Ssから状態s まで実行したときの信号値の変化を状態Ssにおける信号値のベクトルx で表す信号値更新関数V(Ss,s)(x)とブロック開始状態Ssから状態s まで到達する条件である遷移条件関数C(Ss,s)(x)を順に求める。
【００７４】
ステップ１２１では、EFSMから未処理のブロックをひとつ選択する。
【００７５】
ステップ１２２では、ブロックの開始状態Ssに対して信号値更新関数および遷移条件関数を以下のように設定する。
V(Ss,Ss)(x)  = x
C(Ss,Ss) = TRUE
さらに、Ssから一遷移で到達可能な状態を処理候補集合に追加する。
【００７６】
ステップ１２３では、処理候補集合から状態s をひとつ取り出し、これに信号値更新関数および遷移条件関数を設定する。これの関数は、処理対象の状態s に入射する遷移の種類によって以下の（ａ）、（ｂ）、（ｃ）、（ｄ）のように決定される。
【００７７】
（ａ）入射する遷移Tが通常遷移である場合。
遷移Tの出射元の状態をs1とする。状態s1から遷移して状態sに到達するとき各信号値は遷移Tの信号値更新関数U(t)(x)に依って更新される。したがって、ブロックの開始状態から状態sまで到達したときの信号値更新関数は、状態s1までの信号値更新関数と遷移Tの信号値更新関数の合成関数となる。
ただし、信号値更新関数U(t)(x)において入力信号の値を読み出すことが指定されている場合には代入される信号の値だけでなく、入力信号の値も、値が読み出されたことをあらわすために、関数による表現を用いて更新する。具体的には、入力信号iの値がexpであるとき、更新後の値は入力を読み出すことを表す関数inp()を用いてinp(exp)とあらわす。
【００７８】
また、遷移T は状態s1から無条件に実行されるので（遷移T の遷移条件がTRUEである）、遷移条件関数は状態s1のそれが保存される。
V(Ss,s)(x) = ( U(t) 〇 V(Ss,s1))(x)
C(Ss,s)(x) = C(Ss,s1)(x)
【００７９】
図１４には、通常遷移に対するシンボルシミュレーションが例示されている。この例では、図５に例示されているEFSM２のブロックL01 が選択されている。このブロックの開始状態S0に対して、V(S0,S0)(x), C(S0,S0)(x)がそれぞれ割り当てられている。S0からS1への通常遷移では、a, bに入力信号i, jの値がそれぞれ読み込まれ、その他の信号は1 で初期化される。従って、遷移後にa, bの値がそれぞれi, jとなり、b, c, d の値がそれぞれ1 となる。入力信号i, jからは値が読み込まれたので、それぞれinp(i), inp(j)に更新される。
【００８０】
（ｂ）入射する遷移T が分岐遷移である場合。
遷移Tの出射元の状態をs1とする。EFSMへの制約により遷移Tにおいて信号値は更新されない。したがって、ブロックの開始状態から状態sまで到達したときの信号値更新関数は、状態s1までの信号値更新関数が保存される。また、遷移Tは状態s1において遷移条件C(t)(x)が成り立つときに実行される。したがって、状態sに到達するための遷移条件関数は状態s1での遷移条件関数と遷移Tの遷移条件の論理積となる。
V(Ss,s)(x)=V(Ss,s1)(x)
C(Ss,s)(x)=C(Ss,s1)(ｘ)∧C(t)(V(Ss,s1)(x))
【００８１】
図１５には、分岐遷移に対するシンボルシミュレーションが例示されている。S1からS2への分岐遷移の遷移条件は(a<b) である。したがって、状態S2への遷移条件は、この遷移の遷移条件を状態S1での書く信号の値で読み替えた論理式と、状態S1までの遷移条件の論理積(i<j) となる。
【００８２】
（ｃ）状態sが合流状態であり、入射する遷移T1,T2が合流遷移であるとき、かつ、合流状態sから分岐状態sdに相互リンクが張られているとき。
遷移T1,T2の出射元の状態をそれぞれs1,s2とする。EFSMへの制約により遷移T1、T2において信号値は更新されない。
【００８３】
しかし、どちらの遷移を経由して状態s に到達したかに依ってブロックの開始状態から状態s まで到達したときの信号値は異なる。これは、分岐状態sd から出射する遷移の遷移条件に依存する。
【００８４】
ここで、分岐状態sdから出射する遷移Td1, Td2の遷移条件がそれぞれh, ¬ hであり、遷移T1, T2はそれぞれ遷移Td1, Td2を経由してs に到達しているものとする。このとき、ブロックの開始状態から状態s まで到達したときの信号r の信号値更新関数はite(if-then-else) に基づく表現式を用いて、下記のように表される。(ite c a b) の値は、c が真であるときa, cが偽であるときb である。また、(ite c, a, b) のa とb が同じであるとき、a と表現される。また、状態s に到達するための遷移条件関数は合流元の状態s1, s2での遷移条件関数の論理和になる。
V(Ss,s)(x) = (ite h(V(Ss,sd)(x)), V(Ss,s1)(x), V(Ss,s2)(x))
C(Ss,s)(x) = C(Ss,s1)(x) ∨ C(Ss,s2)(x)
【００８５】
図１６には、分岐状態と相互リンクが張られている合流状態への合流遷移に対するシンボルシミュレーションが例示されている。合流状態S7と相互リンクを張られている分岐状態はS ２であり、この状態から出射する分岐状態の遷移条件はそれぞれ(a>0), !(a>0) である。したがって、状態S7での信号値更新関数は(a>0) を条件とするite の表現式で表されている。
【００８６】
（ｄ）状態sが合流状態であり、入射する遷移T1,t2が合流遷移であるときかつ、合流状態sから分岐状態sdに相互リンクが張られていないとき。
遷移T1,t2の出射元の状態をそれぞれs1,s2とする。EFSMへの制約により遷移T1、t2において信号値は更新されない。
【００８７】
しかし、どちらの遷移を経由して状態s に到達したかに依ってブロックの開始状態から状態s まで到達したときの信号値は異なる。これは、合流元の状態 s1, s2 での遷移条件関数に依存する。
【００８８】
ブロックの開始状態から状態s まで到達したときの信号r の信号値更新関数はite(if-then-else) に基づく表現式と、不定値を表す変数dcを用いて以下のように表される。また、状態s に到達するための遷移条件関数は合流元の状態s1, s2での遷移条件関数の論理和になる。
V(Ss,s)(x) = (ite C(Ss,s1)(x), V(Ss,s1)(x), (ite C(Ss,s2)(x), V(Ss,s2)(x), dc))
C(Ss,s)(x) = C(Ss,s1)(x) ∨ C(Ss,s2)(x)
【００８９】
ブロックの最終状態に到達したときは、ブロックの開始状態Ss、ブロックの終了状態Se、信号r 、信号値更新関数V(Ss,Se)(x) の組と遷移条件関数C(Ss,Se)(x) を記憶装置に記憶する（ステップ１２４）。
【００９０】
ステップ１３では、対応する開始状態、対応する終了状態、対応する信号の組に対して、信号値更新関数が等価であることを関数等価性比較装置により調べる。
【００９１】
図１７は、ステップ１３の詳細な手順である。ステップ１３１では、EFSM  ＥＨのブロック開始状態Ss, ブロック終了状態Se, 対応関係が与えられている信号の名から信号r をひとつ選ぶ。これにより組(Ss, Se, r) が指定され、これに対応付けられた信号値関数と遷移条件関数が、記憶装置８から選ばれる。
【００９２】
ステップ１３２では、動作合成装置２により出力された対応関係から、(Ss, Se, r) に対応する、ブロック開始状態、ブロック終了状態、信号の組(Ss', Se', r')を選択し、これに対応付けられた信号値関数と遷移条件関数が、記憶装置８から選ばれる。
【００９３】
ステップ１３３では、取り出した信号値関数、遷移条件関数がそれぞれ等価であることを検査する。この検査にはたとえば文献「1995年、プロシーディングス・オブ・インターナショナル・ カンファレンス・オン・コンピュータ・エイディッド・デザイン、２-6頁(Proceedings of International Conference on Computer Aided Design, pp.2-6, 1995)」に記された既知の技術を使用する。
【００９４】
すべてのEFSM EH のブロック開始状態Ss, ブロック終了状態Se、信号r の組に対して比較を行うまで、かかる手順を繰り返す。
【００９５】
次に、本実施の形態の効果について説明する。
【００９６】
本実施の形態では、動作合成装置から出力される中間レベル記述を利用して、動作レベル記述とRTL記述との比較を、いくつかの中間レベル記述間の比較に帰着し、さらに、動作合成による記述変換の過程の情報である対応関係を検証のために使用することにより、動作レベル記述とRTL記述との完全な等価性の比較を行うことができる。
【００９７】
さらに、EFSMモデル変換手順において合流状態に入射する遷移が必ず２つであるようにEFSMモデルに変換し、シンボルシミュレーション手順において合流状態に到達したときにiteによる表現式をもちいて合流後の信号値の更新を関数であらわすことにより、制御構造に分岐合流構造があってもすべての実行パスを抽出することなく信号値の変化を関数であらわすことが可能となる。実行パスを抽出しなくてもよいことにより、シンボルシミュレーションを行う回数や、信号値更新関数を比較する回数を減らすことができ、検証のために必要となる実行時間を削減することができる。
【００９８】
次に、本発明の第二の実施の形態について詳細に説明する。
【００９９】
本発明の第二の実施の形態では、動作合成装置が対応関係において処理単位の対応関係、信号の対応関係に加えて、分岐構造の対応関係を与え、論理検証装置がこの対応情報を利用することが異なる。
【０１００】
動作合成装置は、２つの注目する中間レベル記述に対して、分岐条件が等価である分岐のペア(b, b') を出力する。
【０１０１】
論理検証装置は、シンボルシミュレーションにおいてこの分岐のペア(b, b') に対して仮想的な信号(B, B') を用意しこれについても他の信号と同様にシミュレーションを行う。
【０１０２】
シンボルシミュレーションの手順は第一の実施の形態と同じであるが、ステップ１２３の処理対象が分岐遷移であるときおよび相互リンクが存在する合流状態に入射する合流遷移であるときのみ異なる。
【０１０３】
分岐遷移の場合は、信号値更新関数および遷移条件関数が以下のように更新される。
V(Ss,s)(x) = V(Ss,s1)(x)           ：  信号B 以外の信号に対応する要素
= C(t)(V(Ss,s1)(x))     ：  信号B に対応する要素
C(Ss,s)(x) = C(Ss,s1)(ｘ) ∧ V(Ss,s1)(ｘ)(B)
ここで、V(Ss,s1)( ｘ)(B)はV(Ss,s1)( ｘ) の信号B の要素である関数をあらわす。
【０１０４】
相互リンクが存在する合流状態に入射する合流遷移に対しては、信号値更新関数が以下のように更新される。
V(Ss,s)(x) = (ite   V(Ss,sd)(ｘ)(B), V(Ss,s1)(x), V(Ss,s2)(x))
【０１０５】
そして、最後にステップ１３においては、分岐のペアに対して生成された仮想的な信号についても信号値関数の比較処理の対象とする。
【０１０６】
次に、本実施の形態の効果について説明する。
【０１０７】
本実施の形態では、動作合成装置が等価であると考えられる中間端子のペアを指定し、論理検証装置がこれらの中間端子のペアが確かに等価であることを確かめ、さらに、信号値更新関数や遷移条件関数を中間端子を用いて簡単化する。一般に関数の等価性比較は関数が複雑になれば、比較に必要とする時間が増大する。したがって、中間端子をもちいて比較すべき関数を簡単化することにより検証に要する時間を削減することができる。
【図面の簡単な説明】
【０１０８】
【図１】本発明の実施の形態において例示されるシステムの構成を説明するために用いられる図である。
【図２】本発明の実施の形態において例示される動作レベル記述を説明するために用いられる図である。
【図３】本発明の実施の形態において例示される中間レベル記述を説明するために用いられる図である。
【図４】本発明の実施の形態において例示される中間レベル記述を説明するために用いられる図である。
【図５】本発明の実施の形態において例示されるEFSMモデルを説明するために用いられる図である。
【図６】本発明の実施の形態において例示されるEFSMモデルを説明するために用いられる図である。
【図７】本発明の実施の形態において例示される対応関係を説明するために用いられる図である。
【図８】本発明の実施の形態において例示されるシステムの処理の流れを説明するために用いられる図である。
【図９】図４に示されるステップ１を説明するために用いられる図である。
【図１０】本発明の実施の形態において例示される代入文の処理を説明するために用いられる図である。
【図１１】本発明の実施の形態において例示される条件分岐文の処理を説明するために用いられる図である。
【図１２】本発明の実施の形態において例示される非条件分岐文の処理を説明するために用いられる図である。
【図１３】図５に示されるステップ１２を説明するために用いられる図である。
【図１４】本発明の実施の形態において例示される通常遷移に対するシンボルシミュレーションの処理を説明するために用いられる図である。
【図１５】本発明の実施の形態において例示される分岐遷移に対するシンボルシミュレーションの処理を説明するために用いられる図である。
【図１６】本発明の実施の形態において例示される分岐状態と相互リンクが張られている合流状態へ入射する合流遷移に対するシンボルシミュレーションの処理を説明するために用いられる図である。
【図１７】図５に示されるステップ１３を説明するために用いられる図である。
【図１８】本発明の実施の形態において例示される対応関係を説明するために用いられる図である。
【符号の説明】
【０１０９】
１…記憶装置
２…動作合成装置
３…記憶装置
４…記憶装置
５…モデル抽出装置
６…記憶装置
７…信号値関数抽出装置
８…記憶装置
９…関数等価性比較装置
【図１】
0004702357.tif 000002
【図２】
0004702357.tif 000003
【図３】
0004702357.tif 000004
【図４】
0004702357.tif 000005
【図５】
0004702357.tif 000006
【図６】
0004702357.tif 000007
【図７】
0004702357.tif 000008
【図８】
0004702357.tif 000009
【図９】
0004702357.tif 000010
【図１０】
0004702357.tif 000011
【図１１】
0004702357.tif 000012
【図１２】
0004702357.tif 000013
【図１３】
0004702357.tif 000014
【図１４】
0004702357.tif 000015
【図１５】
0004702357.tif 000016
【図１６】
0004702357.tif 000017
【図１７】
0004702357.tif 000018
【図１８】
0004702357.tif 000019