(57)【要約】【課題】  システムレベル設計言語による回路記述とハードウェア記述言語による回路記述との等価性を、シミュレーション結果を用いて容易に検証する。【解決手段】  回路記述１０、２０を用いたシミュレーションにより、信号値遷移の発生毎に、信号名情報、発生時刻情報、第１信号値情報および第２信号値情報が対応づけられたシミュレーション結果１２、２２が取得される（Ｓ１、Ｓ２）。そして、シミュレーション結果１２の各情報に基づいて、シミュレーション結果１２における検証対象信号の信号値遷移の発生時刻が、信号値遷移の波及順序が維持される限り、シミュレーション結果２２における発生時刻に順次変更される（Ｓ３）。この後、検証対象信号における信号値遷移の発生時刻の全てがシミュレーション結果１２、２２で一致する場合、回路記述１０、２０は等価であると判定される（Ｓ４）。【選択図】    図1
2005316595.tif 000002
【特許請求の範囲】
【請求項１】
第１設計言語で記述された上位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報と、信号値遷移を発生させる信号の信号値を示す第２信号値情報とが対応づけられた上位シミュレーション結果を取得し、
前記上位回路記述から変換されて第２設計言語で記述された下位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報とが対応づけられた下位シミュレーション結果を取得し、
前記上位シミュレーション結果における前記信号名情報、前記発生時刻情報、前記第１信号値情報および前記第２信号値情報に基づいて、前記上位シミュレーション結果における検証対象信号の信号値遷移の発生時刻を、前記上位シミュレーション結果における信号値遷移の波及順序が維持される限り、前記下位シミュレーション結果における前記検証対象信号の信号値遷移の発生時刻に順次変更する発生時刻変更処理を実施し、
前記検証対象信号における信号値遷移の発生時刻の全てが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致する場合、前記上位回路記述と前記下位回路記述とは等価であると判定することを特徴とする回路記述間の等価性検証方法。
【請求項２】
請求項１記載の回路記述間の等価性検証方法において、
前記下位シミュレーション結果は、信号値遷移を発生させる信号の信号値を示す第２信号値情報が更に対応づけられており、
前記検証対象信号における信号値遷移の発生時刻の少なくとも一つが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致しない場合、発生時刻が一致しない前記検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との前記下位シミュレーション結果における因果関係を示す因果関係情報を生成して提示することを特徴とする回路記述間の等価性検証方法。
【請求項３】
請求項２記載の回路記述間の等価性検証方法において、
前記下位シミュレーション結果を用いて、前記下位回路記述で定義された各信号の信号波形を生成して表示装置に表示するとともに、発生時刻が一致しない前記検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための波及経路情報を前記因果関係情報として生成して前記信号波形に重ねて前記表示装置に表示することを特徴とする回路記述間の等価性検証方法。
【請求項４】
第１設計言語で記述された上位回路記述と、前記上位回路記述から変換されて第２設計言語で記述された下位回路記述との等価性を検証するコンピュータに、
前記上位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報と、信号値遷移を発生させる信号の信号値を示す第２信号値情報とが対応づけられた上位シミュレーション結果を取得する第１ステップと、
前記下位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報とが対応づけられた下位シミュレーション結果を取得する第２ステップと、
前記上位シミュレーション結果における前記信号名情報、前記発生時刻情報、前記第１信号値情報および前記第２信号値情報に基づいて、前記上位シミュレーション結果における検証対象信号の信号値遷移の発生時刻を、前記上位シミュレーション結果における信号値遷移の波及順序が維持される限り、前記下位シミュレーション結果における前記検証対象信号の信号値遷移の発生時刻に順次変更する発生時刻変更処理を実施する第３ステップと、
前記検証対象信号における信号値遷移の発生時刻の全てが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致する場合、前記上位回路記述と前記下位回路記述とは等価であると判定する第４ステップとを実行させることを特徴とする回路記述間の等価性検証プログラム。
【請求項５】
請求項４記載の回路記述間の等価性検証プログラムにおいて、
前記下位シミュレーション結果は、信号値遷移を発生させる信号の信号値を示す第２信号値情報が更に対応づけられており、
前記第４ステップで、前記検証対象信号における信号値遷移の発生時刻の少なくとも一つが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致しない場合、発生時刻が一致しない前記検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との前記下位シミュレーション結果における因果関係を示す因果関係情報を生成して提示する第５ステップを前記コンピュータに更に実行させることを特徴とする回路記述間の等価性検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムレベル設計言語で記述された動作レベルの回路記述とハードウェア記述言語で記述されたＲＴＬ（Resister Transfer Level）の回路記述との等価性を検証する技術に関する。
【背景技術】
【０００２】
近時、システムＬＳＩ設計においては、Ｖｅｒｉｌｏｇ−ＨＤＬやＶＨＤＬ等のハードウェア記述言語（ＨＤＬ：Hardware Description Language）によりＲＴＬの回路記述を作成する手法に代えて、Ｃ（Ｃ＋＋）言語をベースとしたＳｙｓｔｅｍＣやＳｐｅｃＣ等のシステムレベル設計言語により動作レベルの回路記述を作成する手法の導入が進められている。システムレベル設計言語は抽象度の高い記述が可能であるため、システムレベル設計言語による回路記述の作成手法を導入することで、回路記述の記述量、すなわち回路記述の作成時間を低減でき、設計効率を向上させることができる。システムレベル設計言語による回路記述の作成手法を導入したシステムＬＳＩ設計では、システムレベル設計言語による回路記述（上位回路記述）を、ハードウェア記述言語による論理合成可能な回路記述（下位回路記述）に変換する高位合成が実施される。そして、上位回路記述と下位回路記述との等価性を検証する形式的検証が実施される。
【０００３】
また、特許文献１には、メモリ回路の異なる２つの回路記述の各々にクロック信号を付加してシミュレーションを実施することで、アドレスとデータとのレーシングを抑えて正確な検証を実施する技術が開示されている。特許文献２には、半導体集積回路の論理検証時に、テストベクタを供給するためのハードウェア記述言語で記述されたテストベンチの変換方法において、検証対象回路の各端子への信号の印可に相当する動作の記述方法を、遅延時間を用いた記述方法から、クロックに同期した記述方法に変換する技術が開示されている。
【特許文献１】特開平６−３０１７４０号公報
【特許文献２】特開平１０−３１９０９０号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかしながら、現状の高位合成ツールおよび形式的検証ツールでは、大規模な回路に対応できない、あるいは適用可能な記述に制限がある等の問題がある。このため、上位回路記述および下位回路記述をそれぞれ用いたシミュレーションを実施し、上位回路記述と下位回路記述との等価性をシミュレーション結果から人手で判定しているのが実状である。ところが、ハードウェア記述言語にはクロックの概念が存在するのに対して、システムレベル設計言語にはクロックの概念は存在しないため、上位回路記述および下位回路記述をそれぞれ用いたシミュレーションのシミュレーション結果（入力信号および出力信号の信号値遷移タイミング）同士が一致することはほとんどない。このため、上位回路記述と下位回路記述との等価性をシミュレーション結果から判定することは容易ではなく、回路記述間の等価性検証に多大な時間を要する。この結果、設計効率が著しく低下し、システムレベル設計言語による回路記述の作成手法の導入に伴う設計効率向上の効果を十分に享受できない。
【０００５】
本発明は、このような従来の問題点に鑑みてなされたものであり、システムレベル設計言語による回路記述とハードウェア記述言語による回路記述との等価性を、シミュレーション結果を用いて容易に検証することを目的とする。また、本発明の別の目的は、システムレベル設計言語による回路記述とハードウェア記述言語による回路記述との不等価の原因解析の効率を向上させることにある。
【課題を解決するための手段】
【０００６】
本発明の一形態では、第１設計言語で記述された上位回路記述と、上位回路記述から変換されて第２設計言語で記述された下位回路記述との等価性を検証するコンピュータにより、以下に示す処理が実施される。まず、上位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号名情報、発生時刻情報、第１信号値情報および第２信号値情報が対応づけられた上位シミュレーション結果が取得される。ここで、信号名情報は、信号値遷移が発生した信号の信号名を示す。発生時刻情報は、信号値遷移の発生時刻を示す。第１信号値情報は、信号値遷移が発生した信号の信号値遷移後の信号値を示す。第２信号値情報は、信号値遷移が発生した信号に信号値遷移を発生させる信号の信号値を示す。また、下位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号名情報、発生時刻情報および第１信号値情報が対応づけられた下位シミュレーション結果が取得される。
【０００７】
この後、上位シミュレーション結果に対して発生時刻変更処理が実施される。発生時刻変更処理では、上位シミュレーション結果における信号名情報、発生時刻情報、第１信号値情報および第２信号値情報に基づいて、上位シミュレーション結果における検証対象信号の信号値遷移の発生時刻が、上位シミュレーション結果における信号値遷移の波及順序が維持される限り、下位シミュレーション結果における検証対象信号の信号値遷移の発生時刻に順次変更される。
【０００８】
そして、検証対象信号における信号値遷移の発生時刻の全てが発生時刻変更処理後の上位シミュレーション結果と下位シミュレーション結果とで一致する場合、上位回路記述と下位回路記述とは等価であると判定される。すなわち、検証対象信号における信号値遷移の発生時刻の少なくとも一つが発生時刻変更処理後の上位シミュレーション結果と下位シミュレーション結果とで一致しない場合、上位回路記述と下位回路記述とは不等価であると判定される。
【０００９】
これにより、上位回路記述および下位回路記述をそれぞれ用いたシミュレーションの実施後に、検証対象信号における信号値遷移の発生時刻のいずれかが上位シミュレーション結果と下位シミュレーション結果とで一致しない場合でも、上位回路記述と下位回路記述との等価性を、シミュレーション結果を用いて容易に検証できる。このため、回路記述間の等価性検証に要する時間を大幅に削減でき、設計効率を向上させることができる。
【００１０】
本発明の前記一形態の好ましい例では、下位シミュレーション結果は、第２信号値情報が更に対応づけられている。また、検証対象信号における信号値遷移の発生時刻の少なくとも一つが発生時刻変更処理後の上位シミュレーション結果と下位シミュレーション結果とで一致しない場合、因果関係情報が提示される。ここで、因果関係情報は、発生時刻変更処理後の上位シミュレーション結果と下位シミュレーション結果とで発生時刻が一致しない検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との下位シミュレーション結果における因果関係を示す。このため、上位回路記述と下位回路記述とは不等価であると判定された場合に因果関係情報を利用することで、上位回路記述と下位回路記述との不等価の原因解析の効率を向上させることができる。上位回路記述と下位回路記述との不等価の原因解析に要する時間を短縮できるため、設計効率の向上に寄与できる。
【００１１】
本発明の前記一形態の好ましい例では、下位シミュレーション結果を用いて、下位回路記述で定義された各信号の信号波形が生成され表示装置に表示されるとともに、波及経路情報が生成され信号波形に重なって表示装置に表示される。ここで、波及経路情報は、発生時刻変更処理後の上位シミュレーション結果と下位シミュレーション結果とで発生時刻が一致しない検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための情報である。このため、設計者は、上位回路記述と下位回路記述との不等価の原因を、信号波形および波及経路情報の表示から視覚的に認識できる。
【発明の効果】
【００１２】
本発明では、第１設計言語による上位回路記述と第２設計言語による下位回路記述との等価性を、シミュレーション結果を用いて容易に検証でき、設計効率を向上させることができる。また、上位回路記述と下位回路記述との不等価の原因解析の効率を向上させることができ、設計効率の向上に寄与できる。
【発明を実施するための最良の形態】
【００１３】
以下、図面を用いて本発明の実施形態を説明する。
図１は、本発明の基本原理を示している。第１設計言語で記述された上位回路記述１０と、上位回路記述１０から変換されて第２設計言語で記述された下位回路記述２０との等価性を検証するコンピュータにより、以下に示す処理が実施される。まず、上位回路記述１０を用いたシミュレーションにより、信号値遷移の発生毎に、信号名情報、発生時刻情報、第１信号値情報および第２信号値情報が対応づけられた上位シミュレーション結果（上位Ｓｉｍ結果）１２が取得される（ステップＳ１）。ここで、信号名情報は、信号値遷移が発生した信号の信号名を示す。発生時刻情報は、信号値遷移の発生時刻を示す。第１信号値情報は、信号値遷移が発生した信号の信号値遷移後の信号値を示す。第２信号値情報は、信号値遷移が発生した信号に信号値遷移を発生させる信号の信号値を示す。また、下位回路記述２０を用いたシミュレーションにより、信号値遷移の発生毎に、信号名情報、発生時刻情報、第１信号値情報および第２信号値情報が対応づけられた下位シミュレーション結果２２が取得される（ステップＳ２）。
【００１４】
この後、上位シミュレーション結果１２に対して発生時刻変更処理が実施される（ステップＳ３）。発生時刻変更処理では、上位シミュレーション結果１２における信号名情報、発生時刻情報、第１信号値情報および第２信号値情報に基づいて、上位シミュレーション結果１２における検証対象信号の信号値遷移の発生時刻が、上位シミュレーション結果１２における信号値遷移の波及順序が維持される限り、下位シミュレーション結果２２における検証対象信号の信号値遷移の発生時刻に順次変更される。
【００１５】
そして、検証対象信号における信号値遷移の発生時刻の全てが発生時刻変更処理後の上位シミュレーション結果１２と下位シミュレーション結果２２とで一致する場合、上位回路記述１０と下位回路記述２０とは等価であると判定される（ステップＳ４）。すなわち、検証対象信号における信号値遷移の発生時刻の少なくとも一つが発生時刻変更処理後の上位シミュレーション結果１２と下位シミュレーション結果２２とで一致しない場合、上位回路記述と下位回路記述とは不等価であると判定される。
【００１６】
検証対象信号における信号値遷移の発生時刻の少なくとも一つが発生時刻変更処理後の上位シミュレーション結果１２と下位シミュレーション結果２２とで一致しない場合、すなわち上位回路記述１０と下位回路記述２０とは不等価であると判定された場合、因果関係情報が提示される（ステップＳ５）。ここで、因果関係情報は、発生時刻変更処理後の上位シミュレーション結果１２と下位シミュレーション結果２２とで発生時刻が一致しない検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との因果関係を示す。例えば、下位シミュレーション結果２２を用いて、下位回路記述２０で定義された各信号の信号波形が生成され表示装置に表示されるとともに、波及経路情報が生成され信号波形に重なって表示装置に表示される。ここで、波及経路情報は、発生時刻変更処理後の上位シミュレーション結果１２と下位シミュレーション結果２２とで発生時刻が一致しない検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための情報である。
【００１７】
図２は、本発明を実現するためのシステム構成例を示している。本発明を実現するためのシステムは、例えば、ワークステーション１等の計算機と、等価性検証プログラムを記録したＣＤ−ＲＯＭ８またはフレキシブルディスク９等の記録媒体とから構成されている。ワークステーション１は、画面表示を行うディスプレイ２と、キーの押下により指示を入力するキーボード３と、ＣＰＵ４、ハードディスク５および記録媒体ドライブ装置６が内蔵された制御装置７とを有している。記録媒体ドライブ装置６には、ＣＤ−ＲＯＭ８またはフレキシブルディスク９が装着可能である。ワークステーション１は、ＣＤ−ＲＯＭ８またはフレキシブルディスク９の記録媒体ドライブ装置６への装着後、キーボード３を介して入力される指示に応答して、ＣＤ−ＲＯＭ８またはフレキシブルディスク９に記録された等価性検証プログラムをハードディスク５にダウンロードする。ワークステーション１は、ＣＰＵ４が等価性検証プログラムを実行することにより、回路記述間の等価性検証処理が可能になる。
【００１８】
図３は、本発明の一実施形態を示している。図４は、図３のＳｙｓｔｅｍＣによる回路記述１００およびテストベンチ１０１の一例を示している。図５は、図４の回路記述１００およびテストベンチ１０１を用いたシミュレーションのシミュレーション結果を示している。
図３において、まず、ワークステーション１は、図４に示すようなＳｙｓｔｅｍＣ（第１設計言語）で記述された動作レベルの回路記述１００（上位回路記述）とテストベンチ１０１とを用いてＳｙｓｔｅｍＣシミュレータによりシミュレーションを実施し、図５に示すようなシミュレーション結果１０２（上位シミュレーション結果）を取得してハードディスク５に格納する（ステップＳ１０）。シミュレーション結果１０２では、信号値遷移の発生毎に、信号名情報（図５の信号名の列）と、発生時刻情報（図５の発生時刻の列）と、第１信号値情報（図５の信号値の列）と、第２信号値情報（図５の発生要因の列）とが対応づけられている。ここで、信号名情報は、信号値遷移が発生した信号の信号名を示す。発生時刻情報は、信号値遷移の発生時刻を示す。第１信号値情報は、信号値遷移が発生した信号の信号値遷移後の信号値を示す。第２信号値情報は、信号値遷移が発生した信号に信号値遷移を発生させる信号の信号値を示す。例えば、図５のシミュレーション結果１０２において、※印が付加された行は、信号ｐの信号値ｐ［２］への信号値遷移が時刻Ｔ２に発生し、信号ｐに信号値遷移を発生させる信号ａ、ｂの信号値はそれぞれａ［２］、ｂ［２］であることを示している。なお、信号ａ、ｂの信号値遷移は、テストベンチ１０１により発生するものであるため、信号ａ、ｂに対応する第２信号値情報は、第１信号値情報と同一にしてある。
【００１９】
また、ワークステーション１は、ＶＨＤＬ（第２設計言語）で記述されたＲＴＬの回路記述２００（下位回路記述）とテストベンチ２０１とを用いてＶＨＤＬシミュレータによりシミュレーションを実施し、シミュレーション結果２０２（下位シミュレーション結果）を取得してハードディスク５に格納する（ステップＳ２０）。ここで、ＶＨＤＬによる回路記述２００は、ＳｙｓｔｅｍＣによる回路記述１００を高位合成して生成された回路記述である。また、図示を省略するが、シミュレーション結果２０２では、シミュレーション結果１０２と同様に、信号値遷移の発生毎に、信号名情報と、発生時刻情報と、第１信号値情報と、第２信号値情報とが対応づけられている。
【００２０】
この後、ワークステーション１は、シミュレーション結果１０２に対して発生時刻変更処理を実施する（ステップＳ３０）。発生時刻変更処理では、シミュレーション結果１０２における信号名情報、発生時刻情報、第１信号値情報および第２信号値情報に基づいて、シミュレーション結果１０２における検証対象信号ａ、ｂ、ｃの信号値遷移の発生時刻が、シミュレーション結果１０２における信号値遷移の波及順序が維持される限り、シミュレーション結果２０２における検証対象信号ａ、ｂ、ｃの信号値遷移の発生時刻に順次変更される。ここで、シミュレーション結果１０２における信号値遷移の波及順序は、ある信号の信号値遷移と、その信号値遷移に起因して発生する別の信号の信号値遷移との発生順序を示す。シミュレーション結果１０２における検証対象信号ａ、ｂ、ｃの信号値遷移の発生時刻が順次変更された後、検証対象信号ａ、ｂ、ｃにおける信号値遷移の発生時刻の全てがシミュレーション結果１０２とシミュレーション結果２０２とで一致する場合、発生時刻変更処理の成功が通知される。また、検証対象信号ａ、ｂ、ｃにおける信号値遷移の発生時刻の少なくとも一つがシミュレーション結果１０２とシミュレーション結果２０２とで一致しない場合、発生時刻変更処理の不成功が通知される。なお、発生時刻変更処理の詳細については、図６〜図８で説明する。
【００２１】
そして、ワークステーション１は、発生時刻変更処理の成否に応じて、回路記述１００と回路記述２００との等価性を判定する（ステップＳ４０）。具体的には、ワークステーション１は、発生時刻変更処理の成功が通知された場合、回路記述１００と回路記述２００とは等価であると判定する。また、ワークステーション１は、発生時刻変更処理の不成功が通知された場合、回路記述１００と回路記述２００とは不等価であると判定する。
【００２２】
さらに、ワークステーション１は、回路記述１００と回路記述２００とは不等価であると判定した場合、シミュレーション結果２０２を用いて、回路記述２００で定義された各信号の信号波形に波及経路情報を重ねてディスプレイ２（表示装置）に表示する（ステップＳ５０）。ここで、波及経路情報は、発生時刻変更処理後のシミュレーション結果１０２とシミュレーション結果２０２とで発生時刻が一致しない検証対象信号ａ、ｂ、ｃの信号値遷移を発生させる信号値遷移の波及経路を明示するための情報である。換言すれば、ワークステーション１は、発生時刻変更処理後のシミュレーション結果１０２とシミュレーション結果２０２とで発生時刻が一致しない検証対象信号ａ、ｂ、ｃの信号値遷移とその信号値遷移の発生に関与する信号値遷移との因果関係を示す因果関係情報を生成して提示する。
【００２３】
図６は、図３の発生時刻変更処理の詳細を示している。
ワークステーション１は、ハードディスク５に格納したシミュレーション結果１０２、２０２の信号名情報、発生時刻情報、第１信号値情報および第２信号値情報を探索しながら以下に示す処理を実施する。
ステップＳ３０１において、ワークステーション１は、検証対象信号ａ、ｂ、ｃのいずれかを指定する。この後、処理はステップＳ３０２に移行する。
【００２４】
ステップＳ３０２において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号における信号値遷移のいずれかを指定する。例えば、ワークステーション１は、ステップＳ３０１で検証対象信号ａを指定した場合、検証対象信号ａにおける信号値遷移（信号値ａ［１］への信号値遷移、信号値ａ［２］への信号値遷移、信号値ａ［３］への信号値遷移）のいずれかを指定する。この後、処理はステップＳ３０３に移行する。
【００２５】
ステップＳ３０３において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号におけるステップＳ３０２で指定した信号値遷移について、シミュレーション結果１０２における発生時刻とシミュレーション結果２０２における発生時刻とが一致するか否かを判定する。双方の発生時刻が一致しない場合、処理はステップＳ３０４に移行する。双方の発生時刻が一致する場合、処理はステップＳ３０８に移行する。
【００２６】
ステップＳ３０４において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号におけるステップＳ３０２で指定した信号値遷移について、シミュレーション結果１０２における発生時刻がシミュレーション結果２０２における発生時刻より前であるか否かを判定する。シミュレーション結果１０２における発生時刻がシミュレーション結果２０２における発生時刻より前である場合、処理はステップＳ３０５に移行する。シミュレーション結果１０２における発生時刻がシミュレーション結果２における発生時刻より前ではない場合、処理はステップＳ３０６に移行する。
【００２７】
ステップＳ３０５において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号におけるステップＳ３０２で指定した信号値遷移を変更対象として前方変更処理を実施する。前方変更処理の詳細については、図７で説明する。この後、処理はステップＳ３０７に移行する。
ステップＳ３０６において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号におけるステップＳ３０２で指定した信号値遷移を変更対象として後方変更処理を実施する。後方変更処理の詳細については、図８で説明する。この後、処理はステップＳ３０７に移行する。
【００２８】
ステップＳ３０７において、ワークステーション１は、ステップＳ３０５で実施した後方変更処理またはステップＳ３０６で実施した前方変更処理の成功が通知されたか否かを判定する。成功が通知された場合、処理はステップＳ３０８に移行する。成功が通知されなかった場合、すなわち不成功が通知された場合、処理はステップＳ３１１に移行する。
ステップＳ３０８において、ワークステーション１は、ステップＳ３０１で指定した検証対象信号における全ての信号値遷移について処理が実施されたか否かを判定する。全ての信号値遷移について処理が実施されていない場合、処理はステップＳ３０２に移行し、ワークステーション１は、ステップＳ３０１で指定した検証対象信号における次の信号値遷移を指定し、ステップＳ３０３以降の処理を適宜実施する。全ての信号値遷移について処理が実施されている場合、処理はステップＳ３０９に移行する。
【００２９】
ステップＳ３０９において、ワークステーション１は、全ての検証対象信号について処理が実施されたか否かを判定する。全ての検証対象信号について処理が実施されていない場合、処理はステップＳ３０１に移行し、ワークステーション１は、次の検証対象信号を指定し、ステップＳ３０２以降の処理を適宜実施する。全ての検証対象信号について処理が実施されている場合、処理はステップＳ３１０に移行する。
【００３０】
ステップＳ３１０において、ワークステーション１は、発生時刻変更処理の成功を通知し、発生時刻変更処理を完了する。
ステップＳ３１１において、ワークステーション１は、発生時刻変更処理の不成功を通知し、発生時刻変更処理を完了する。
図７は、図６の前方変更処理の詳細を示している。
【００３１】
ステップＳ７０１において、ワークステーション１は、変更対象の信号値遷移のシミュレーション結果１０２における発生時刻を、図６のステップＳ３０１で指定された検証対象信号におけるステップＳ３０２で指定された信号値遷移のシミュレーション結果２０２における発生時刻に変更した場合、シミュレーション結果１０２における信号値遷移の波及順序を維持できるか否かを判定する。シミュレーション結果１０２における信号値遷移の波及順序を維持できない場合、処理はステップＳ７０２に移行する。シミュレーション結果１０２における信号値遷移の波及順序を維持できる場合、処理はステップＳ７０７に移行する。
【００３２】
ステップＳ７０２において、ワークステーション１は、変更対象の信号値遷移を発生させる信号における信号値遷移のいずれかを指定する。この後、処理はステップＳ７０３に移行する。
ステップＳ７０３において、ワークステーション１は、ステップＳ７０２で指定した信号値遷移の発生時刻を変更できるか否かを判定する。発生時刻を変更できる場合、処理はステップＳ７０４に移行する。発生時刻を変更できない場合、処理はステップ７０９に移行する。
【００３３】
ステップＳ７０４において、ワークステーション１は、ステップＳ７０２で指定した信号値遷移を変更対象として前方変更処理を再帰的に実施する。この後、処理はステップＳ７０５に移行する。
ステップＳ７０５において、ワークステーション１は、ステップＳ７０４で実施した前方変更処理の成功が通知されたか否かを判定する。成功が通知された場合、処理はステップＳ７０６に移行する。成功が通知されなかった場合、すなわち不成功が通知された場合、処理はステップＳ７０９に移行する。
【００３４】
ステップＳ７０６において、ワークステーション１は、変更対象の信号値遷移を発生させる信号における全ての信号値遷移について処理が実施されたか否かを判定する。全ての信号値遷移について処理が実施されていない場合、処理はステップＳ７０２に移行し、ワークステーション１は、変更対象の信号値遷移を発生させる信号における次の信号値遷移を指定し、ステップＳ７０３以降の処理を適宜実施する。全ての信号値遷移について処理が実施されている場合、処理はステップＳ７０７に移行する。
【００３５】
ステップＳ７０７において、ワークステーション１は、変更対象の信号値遷移のシミュレーション結果１０２における発生時刻を、図６のステップＳ３０１で指定された検証対象信号におけるステップＳ３０２で指定された信号値遷移のシミュレーション結果２０２における発生時刻に変更する。この後、処理はステップＳ７０８に移行する。
ステップＳ７０８において、ワークステーション１は、前方変更処理の成功を通知し、前方変更処理を完了する。
【００３６】
ステップＳ７０９において、ワークステーション１は、前方変更処理の不成功を通知し、前方変更処理を完了する。
図８は、図６の後方変更処理の詳細を示している。
ステップＳ８０１において、ワークステーション１は、変更対象の信号値遷移のシミュレーション結果１０２における発生時刻を、図６のステップＳ３０１で指定された検証対象信号におけるステップＳ３０２で指定された信号値遷移のシミュレーション結果２０２における発生時刻に変更した場合、シミュレーション結果１０２における信号値遷移の波及順序を維持できるか否かを判定する。シミュレーション結果１０２における信号値遷移の波及順序を維持できない場合、処理はステップＳ８０２に移行する。シミュレーション結果１０２における信号値遷移の波及順序を維持できる場合、処理はステップＳ８０７に移行する。
【００３７】
ステップＳ８０２において、ワークステーション１は、変更対象の信号値遷移に起因して発生する信号値遷移のいずれかを指定する。この後、処理はステップＳ８０３に移行する。
ステップＳ８０３において、ワークステーション１は、ステップＳ８０２で指定した信号値遷移の発生時刻を変更できるか否かを判定する。発生時刻を変更できる場合、処理はステップＳ８０４に移行する。発生時刻を変更できない場合、処理はステップ８０９に移行する。
【００３８】
ステップＳ８０４において、ワークステーション１は、ステップＳ８０２で指定した信号値遷移を変更対象として後方変更処理を再帰的に実施する。この後、処理はステップＳ８０５に移行する。
ステップＳ８０５において、ワークステーション１は、ステップＳ８０４で実施した後方変更処理の成功が通知されたか否かを判定する。成功が通知された場合、処理はステップＳ８０６に移行する。成功が通知されなかった場合、すなわち不成功が通知された場合、処理はステップＳ８０９に移行する。
【００３９】
ステップＳ８０６において、ワークステーション１は、変更対象の信号値遷移に起因して発生する全ての信号値遷移について処理が実施されたか否かを判定する。全ての信号値遷移について処理が実施されていない場合、処理はステップＳ８０２に移行し、ワークステーション１は、変更対象の信号値遷移に起因して発生する次の信号値遷移を指定し、ステップＳ８０３以降の処理を適宜実施する。全ての信号値遷移について処理が実施されている場合、処理はステップＳ８０７に移行する。
【００４０】
ステップＳ８０７において、ワークステーション１は、変更対象の信号値遷移のシミュレーション結果１０２における発生時刻を、図６のステップＳ３０１で指定された検証対象信号におけるステップＳ３０２で指定された信号値遷移のシミュレーション結果２０２における発生時刻に変更する。この後、処理はステップＳ８０８に移行する。
ステップＳ８０８において、ワークステーション１は、後方変更処理の成功を通知し、後方変更処理を完了する。
【００４１】
ステップＳ８０９において、ワークステーション１は、後方変更処理の不成功を通知し、後方変更処理を完了する。
ここで、以上のような発生時刻変更処理を具体的に説明する。図９は、発生時刻変更処理前のシミュレーション結果１０２、２０２を示している。図１０は、発生時刻変更処理中のシミュレーション結果１０２、２０２を示している。図１１は、発生時刻変更処理後のシミュレーション結果１０２、２０２を示している。なお、この例では、シミュレーション結果１０２における時刻Ｔ１、Ｔ２、Ｔ３を、シミュレーション結果２０２における時刻Ｔ１’、Ｔ４’、Ｔ７’として扱っている。
【００４２】
まず、ワークステーション１は、検証対象信号ａ、ｂ、ｃの中から検証対象信号ａを指定する（図６のステップＳ３０１）。そして、ワークステーション１は、検証対象信号ａの信号値ａ［１］への信号値遷移を指定する（図６のステップＳ３０２）。検証対象信号ａの信号値ａ［１］への信号値遷移の発生時刻は、シミュレーション結果１０２（時刻Ｔ１’）とシミュレーション結果２０２（時刻Ｔ１’）とで一致するため、ワークステーション１は、検証対象信号ａの信号値ａ［１］への信号値遷移を変更対象とした前方変更処理または後方変更処理のいずれも実施しない。
【００４３】
次に、ワークステーション１は、検証対象信号ａの信号値ａ［２］への信号値遷移を指定する（図６のステップＳ３０２）。検証対象信号ａの信号値ａ［２］への信号値遷移の発生時刻は、シミュレーション結果１０２（時刻Ｔ４’）とシミュレーション結果２０２（時刻Ｔ２’）とで一致せず、シミュレーション結果１０２における発生時刻Ｔ４’がシミュレーション結果２０２における発生時刻Ｔ２’より前ではないため、ワークステーション１は、検証対象信号ａの信号値ａ［２］への信号値遷移を変更対象として前方変更処理を実施する（図６のステップＳ３０６）。検証対象信号ａは入力信号であるため、シミュレーション結果１０２における検証対象信号ａの信号値ａ［２］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ａの信号値ａ［２］への信号値遷移の発生時刻Ｔ２’に変更しても、シミュレーション結果１０２における信号値遷移の波及順序を維持できる。従って、図１０（ａ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ａの信号値ａ［２］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ａの信号値ａ［２］への信号値遷移の発生時刻Ｔ２’に変更する（図７のステップＳ７０７）。
【００４４】
次に、ワークステーション１は、検証対象信号ａの信号値ａ［３］への信号値遷移を指定する（図６のステップＳ３０２）。そして、検証対象信号ａの信号値ａ［２］への信号値遷移を指定した場合と同様に、ワークステーション１は、検証対象信号ａの信号値ａ［３］への信号値遷移を変更対象として前方変更処理を実施する（図６のステップＳ３０６）。従って、図１０（ｂ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ａの信号値ａ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ａの信号値ａ［３］への信号値遷移の発生時刻Ｔ３’に変更する（図７のステップＳ７０７）。
【００４５】
次に、ワークステーション１は、検証対象信号ｂを指定する（図６のステップＳ３０１）。そして、検証対象信号ａを指定した場合と同様に、ワークステーション１は、検証対象信号ｂの信号値ｂ［１］への信号値遷移を変更対象とした前方変更処理または後方変更処理のいずれも実施せず、検証対象信号ｂの信号値ｂ［２］、ｂ［３］への信号値遷移を変更対象として前方変更処理をそれぞれ実施する。すなわち、図１０（ｃ）、（ｄ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ｂの信号値ｂ［２］、ｂ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｂの信号値ｂ［２］、ｂ［３］への信号値遷移の発生時刻Ｔ２’、Ｔ３’に順次変更する。
【００４６】
次に、ワークステーション１は、検証対象信号ｃを指定する（図６のステップＳ３０１）。そして、ワークステーション１は、検証対象信号ｃの信号値ｃ［１］への信号値遷移を指定する（図６のステップＳ３０２）。検証対象信号ｃの信号値ｃ［１］への信号値遷移の発生時刻は、シミュレーション結果１０２（時刻Ｔ１’）とシミュレーション結果２０２（時刻Ｔ４’）とで一致せず、シミュレーション結果１０２における発生時刻Ｔ１’がシミュレーション結果２０２における発生時刻Ｔ４’より前であるため、ワークステーション１は、検証対象信号ｃの信号値ｃ［１］への信号値遷移を変更対象として後方変更処理を実施する（図６のステップＳ３０５）。検証対象信号ｃは出力信号であるため、シミュレーション結果１０２における検証対象信号ｃの信号値ｃ［１］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［１］への信号値遷移の発生時刻Ｔ４’に変更しても、シミュレーション結果１０２における信号値遷移の波及順序を維持できる。従って、図１０（ｅ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ｃの信号値ｃ［１］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［１］への信号値遷移の発生時刻Ｔ４’に変更する（図８のステップＳ８０７）。
【００４７】
次に、ワークステーション１は、検証対象信号ｃの信号値ｃ［２］への信号値遷移を指定する（図６のステップＳ３０２）。そして、検証対象信号ｃの信号値ｃ［１］への信号値遷移を指定した場合と同様に、ワークステーション１は、検証対象信号ｃの信号値ｃ［２］への信号値遷移を変更対象として後方変更処理を実施する（図６のステップＳ３０５）。従って、図１０（ｆ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ｃの信号値ｃ［２］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［２］への信号値遷移の発生時刻Ｔ５’に変更する（図８のステップＳ８０７）。
【００４８】
次に、ワークステーション１は、検証対象信号ｃの信号値ｃ［３］への信号値遷移を指定する（図６のステップＳ３０２）。検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻は、シミュレーション結果１０２（時刻Ｔ７’）とシミュレーション結果２０２（時刻Ｔ６’）とで一致せず、シミュレーション結果１０２における発生時刻Ｔ７’がシミュレーション結果２０２における発生時刻Ｔ６’より前ではないため、ワークステーション１は、検証対象信号ｃの信号値ｃ［３］への信号値遷移を変更対象として前方変更処理を実施する（図６のステップＳ３０６）。検証対象信号ｃの信号値ｃ［３］への信号値遷移は、信号ｓの信号値ｓ［３］への信号値遷移に起因して発生する。このため、シミュレーション結果１０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更すると、検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻が信号ｓの信号値ｓ［３］への信号値遷移の発生時刻Ｔ７’より前になり、シミュレーション結果１０２における信号値遷移の波及順序を維持できない。
【００４９】
従って、ワークステーション１は、信号ｓの信号値ｓ［３］への信号値遷移の発生時刻を変更するために、信号ｓの信号値ｓ［３］への信号値遷移を指定する（図７のステップＳ７０２）。信号ｓの信号値ｓ［３］への信号値遷移は発生時刻を変更可能であるため、ワークステーション１は、信号ｓの信号値ｓ［３］への信号値遷移を変更対象として前方変更処理を再帰的に実施する（図７のステップＳ７０４）。信号ｓの信号値ｓ［３］への信号値遷移は、信号ｐの信号値ｐ［３］への信号値遷移と信号ｑの信号値ｑ［３］への信号値遷移とに起因して発生する。このため、シミュレーション結果１０２における検証対象信号ｓの信号値ｓ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更すると、検証対象信号ｓの信号値ｓ［３］への信号値遷移の発生時刻が信号ｐの信号値ｐ［３］への信号値遷移の発生時刻Ｔ７’および信号ｑの信号値ｑ［３］への信号値遷移の発生時刻Ｔ７’より前になり、シミュレーション結果１０２における信号値遷移の波及順序を維持できない。
【００５０】
従って、ワークステーション１は、まず、信号ｐの信号値ｐ［３］への信号値遷移の発生時刻を変更するために、信号ｐの信号値ｐ［３］への信号値遷移を指定する（図７のステップＳ７０２）。信号ｐの信号値ｐ［３］への信号値遷移は発生時刻を変更可能であるため、ワークステーション１は、信号ｐの信号値ｐ［３］への信号値遷移を変更対象として前方変更処理を再帰的に実施する（図７のステップＳ７０４）。信号ｐの信号値ｐ［３］への信号値遷移は、信号ａの信号値ａ［３］への信号値遷移と信号ｂの信号値ｂ［３］への信号値遷移とに起因して発生する。ところが、シミュレーション結果１０２における検証対象信号ｐの信号値ｐ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更しても、シミュレーション結果１０２における信号値遷移の波及順序を維持できる。従って、図１１（ｇ）に示すように、ワークステーション１は、シミュレーション結果１０２における検証対象信号ｐの信号値ｐ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更する（図７のステップＳ７０７）。
【００５１】
次に、ワークステーション１は、信号ｑの信号値ｑ［３］への信号値遷移の発生時刻を変更するために、信号ｑの信号値ｑ［３］への信号値遷移を指定する（図７のステップＳ７０２）。そして、信号ｐの信号値ｐ［３］への信号値遷移を指定した場合と同様に、ワークステーション１は、信号ｑの信号値ｑ［３］への信号値遷移を変更対象として前方変更処理を再帰的に実施する（図７のステップＳ７０４）。従って、図１１（ｈ）に示すように、ワークステーション１は、シミュレーション結果１０２における信号ｑの信号値ｑ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更する（図７のステップＳ７０７）。
【００５２】
この後、ワークステーション１は、信号ｐの信号値ｐ［３］への信号値遷移および信号ｑの信号値ｑ［３］への信号値遷移を変更対象とした前方変更処理の成功を認識すると、図１１（ｉ）に示すように、シミュレーション結果１０２における信号ｓの信号値ｓ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更する（図７のステップＳ７０７）。
【００５３】
そして、ワークステーション１は、信号ｓの信号値ｓ［３］への信号値遷移を変更対象とした前方変更処理の成功を認識すると、図１１（ｊ）に示すように、シミュレーション結果１０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻を、シミュレーション結果２０２における検証対象信号ｃの信号値ｃ［３］への信号値遷移の発生時刻Ｔ６’に変更する（図７のステップＳ７０７）。これにより、全ての検証対象信号ａ、ｂ、ｃついての処理が完了し、ワークステーション１は、発生時刻変更処理の成功を通知して、発生時刻変更処理を完了する。
【００５４】
図１２は、図３の回路記述１００、２００間の不等価判定に伴う信号波形および信号値遷移の波及経路の表示例を示している。この例は、検証対象信号ｃの信号値ｃ［２］への信号値遷移が指定されているときに、発生時刻変更処理の不成功が通知された場合を示している。
ワークステーション１は、発生時刻変更処理の不成功通知により回路記述１００と回路記述２００とは不等価であると判定した場合、シミュレーション結果２０２を用いて、回路記述２００で定義された信号ａ、ｂ、ｃ、ｘ、ｙ、ｚの信号波形に、検証対象信号ｃの信号値ｃ［２］への信号値遷移を発生させる信号値遷移の波及経路を明示するための矢印（波及経路情報）を重ねてディスプレイ２に表示する。なお、信号ｘ、ｙ、ｚは、回路記述１００の高位合成に伴って、回路記述２００で新たに定義された信号である。
【００５５】
回路記述２００とテストベンチ２０１とを用いたシミュレーションでは、信号ａの信号値ａ［３］への信号値遷移および信号ｂの信号値ｂ［２］への信号値遷移に起因して、信号ｘの信号値ｘ［２］への信号値遷移が発生する。信号ａの信号値ａ［２］への信号値遷移および信号ｂの信号値ｂ［２］への信号値遷移に起因して、信号ｙの信号値ｙ［２］への信号値遷移が発生する。信号ｘの信号値ｘ［２］への信号値遷移および信号ｙの信号値ｙ［２］への信号値遷移に起因して、信号ｚの信号値ｚ［２］への信号値遷移が発生する。信号ｚの信号値ｚ［２］への信号値遷移に起因して、信号ｃの信号値ｃ［２］への信号値遷移が発生する。従って、検証対象信号ｃの信号値ｃ［２］への信号値遷移を発生させる信号値遷移の波及経路としては、以下に示す信号値遷移の波及経路（１）〜（４）が存在する。
（１）ａ［３］−＞ｘ［２］−＞ｚ［２］−＞ｃ［２］
（２）ｂ［２］−＞ｘ［２］−＞ｚ［２］−＞ｃ［２］
（３）ａ［２］−＞ｙ［２］−＞ｚ［２］−＞ｃ［２］
（４）ｂ［２］−＞ｙ［２］−＞ｚ［２］−＞ｃ［２］
検証対象信号ｃの信号値ｃ［２］への信号値遷移の発生に関与する信号値遷移間の因果関係を矢印で表示することで、検証対象信号ｃの信号値ｃ［２］への信号値遷移を発生させる信号値遷移の波及経路（１）〜（４）が明示されるため、検証対象信号ｃの信号値ｃ［２］への信号値遷移を発生させる信号値遷移の波及経路に、本来含まれてはならない信号ａの信号値ａ［３］への信号値遷移が含まれていることを容易に認識できる。この結果、回路記述１００と回路記述２００との不等価の原因解析の効率が向上する。
【００５６】
以上、本実施形態では、回路記述１００および回路記述２００をそれぞれ用いたシミュレーションの実施後に、検証対象信号における信号値遷移の発生時刻のいずれかがシミュレーション結果１０２とシミュレーション結果２０２とで一致しない場合でも、回路記述１００と回路記述２００との等価性を、シミュレーション結果１０２、２０２を用いて容易に検証できる。このため、回路記述１００、２００間の等価性検証に要する時間を大幅に削減でき、設計効率を向上させることができる。
【００５７】
また、回路記述１００と回路記述２００とは不等価であると判定された場合、回路記述２００で定義された各信号の信号波形に、発生時刻変更処理後のシミュレーション結果１０２とシミュレーション結果２０２とで発生時刻が一致しない検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための矢印が重なってディスプレイ２に表示されるため、回路記述１００と回路記述２００との不等価の原因を視覚的に認識でき、不等価の原因解析の効率を向上させることができる。回路記述１００と回路記述２００との不等価の原因解析に要する時間を短縮できるため、設計効率の向上に寄与できる。
【００５８】
なお、前述の実施形態では、ＳｙｓｔｅｍＣによる回路記述１００とＶＨＤＬによる回路記述２００との等価性検証に本発明を適用した例について述べた。しかしながら、本発明は、かかる実施形態に限定されるものではない。例えば、回路記述１００がその他のシステムレベル設計言語（例えば、ＳｐｅｃＣ）により記述された場合、あるいは回路記述２００がその他のハードウェア記述言語（例えば、Ｖｅｒｉｌｏｇ−ＨＤＬ）により記述された場合にも本発明を同様に適用できる。
【００５９】
前述の実施形態では、回路記述１００と回路記述２００とは不等価であると判定された場合、回路記述２００で定義された各信号の信号波形に、発生時刻変更処理後のシミュレーション結果１０２とシミュレーション結果２０２とで発生時刻が一致しない検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための矢印が重なってディスプレイ２に表示される例について述べた。しかしながら、本発明は、かかる実施形態に限定されるものではない。例えば、発生時刻が一致しない検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するテキストメッセージをディスプレイ２に表示させてもよい。
【００６０】
以上の実施形態において説明した発明を整理して、付記として開示する。
（付記１）
第１設計言語で記述された上位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報と、信号値遷移を発生させる信号の信号値を示す第２信号値情報とが対応づけられた上位シミュレーション結果を取得し、
前記上位回路記述から変換されて第２設計言語で記述された下位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報とが対応づけられた下位シミュレーション結果を取得し、
前記上位シミュレーション結果における前記信号名情報、前記発生時刻情報、前記第１信号値情報および前記第２信号値情報に基づいて、前記上位シミュレーション結果における検証対象信号の信号値遷移の発生時刻を、前記上位シミュレーション結果における信号値遷移の波及順序が維持される限り、前記下位シミュレーション結果における前記検証対象信号の信号値遷移の発生時刻に順次変更する発生時刻変更処理を実施し、
前記検証対象信号における信号値遷移の発生時刻の全てが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致する場合、前記上位回路記述と前記下位回路記述とは等価であると判定することを特徴とする回路記述間の等価性検証方法。
（付記２）
付記１記載の回路記述間の等価性検証方法において、
前記下位シミュレーション結果は、信号値遷移を発生させる信号の信号値を示す第２信号値情報が更に対応づけられており、
前記検証対象信号における信号値遷移の発生時刻の少なくとも一つが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致しない場合、発生時刻が一致しない前記検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との前記下位シミュレーション結果における因果関係を示す因果関係情報を生成して提示することを特徴とする回路記述間の等価性検証方法。
（付記３）
付記２記載の回路記述間の等価性検証方法において、
前記下位シミュレーション結果を用いて、前記下位回路記述で定義された各信号の信号波形を生成して表示装置に表示するとともに、発生時刻が一致しない前記検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための波及経路情報を前記因果関係情報として生成して前記信号波形に重ねて前記表示装置に表示することを特徴とする回路記述間の等価性検証方法。
（付記４）
第１設計言語で記述された上位回路記述と、前記上位回路記述から変換されて第２設計言語で記述された下位回路記述との等価性を検証するコンピュータに、
前記上位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報と、信号値遷移を発生させる信号の信号値を示す第２信号値情報とが対応づけられた上位シミュレーション結果を取得する第１ステップと、
前記下位回路記述を用いたシミュレーションにより、信号値遷移の発生毎に、信号値遷移が発生した信号の信号名を示す信号名情報と、信号値遷移の発生時刻を示す発生時刻情報と、信号値遷移後の信号値を示す第１信号値情報とが対応づけられた下位シミュレーション結果を取得する第２ステップと、
前記上位シミュレーション結果における前記信号名情報、前記発生時刻情報、前記第１信号値情報および前記第２信号値情報に基づいて、前記上位シミュレーション結果における検証対象信号の信号値遷移の発生時刻を、前記上位シミュレーション結果における信号値遷移の波及順序が維持される限り、前記下位シミュレーション結果における前記検証対象信号の信号値遷移の発生時刻に順次変更する発生時刻変更処理を実施する第３ステップと、
前記検証対象信号における信号値遷移の発生時刻の全てが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致する場合、前記上位回路記述と前記下位回路記述とは等価であると判定する第４ステップとを実行させることを特徴とする回路記述間の等価性検証プログラム。
（付記５）
付記４記載の回路記述間の等価性検証プログラムにおいて、
前記下位シミュレーション結果は、信号値遷移を発生させる信号の信号値を示す第２信号値情報が更に対応づけられており、
前記第４ステップで、前記検証対象信号における信号値遷移の発生時刻の少なくとも一つが前記発生時刻変更処理後の上位シミュレーション結果と前記下位シミュレーション結果とで一致しない場合、発生時刻が一致しない前記検証対象信号の信号値遷移とその信号値遷移の発生に関与する信号値遷移との前記下位シミュレーション結果における因果関係を示す因果関係情報を生成して提示する第５ステップを前記コンピュータに更に実行させることを特徴とする回路記述間の等価性検証プログラム。
（付記６）
付記５記載の回路記述間の等価性検証方法において、
前記第５ステップは、前記下位シミュレーション結果を用いて、前記下位回路記述で定義された各信号の信号波形を生成して表示装置に表示するとともに、発生時刻が一致しない前記検証対象信号の信号値遷移を発生させる信号値遷移の波及経路を明示するための波及経路情報を前記因果関係情報として生成して前記信号波形に重ねて前記表示装置に表示するステップであることを特徴とする回路記述間の等価性検証プログラム。
【００６１】
以上、本発明について詳細に説明してきたが、前述の実施形態およびその変形例は発明の一例に過ぎず、本発明はこれらに限定されるものではない。本発明を逸脱しない範囲で変形可能であることは明らかである。
【図面の簡単な説明】
【００６２】
【図１】本発明の基本原理を示す説明図である。
【図２】本発明を実現するためのシステム構成例を示す説明図である。
【図３】本発明の一実施形態を示す説明図である。
【図４】図３のＳｙｓｔｅｍＣによる回路記述およびテストベンチの一例を示す説明図である。
【図５】図４の回路記述およびテストベンチを用いたシミュレーションのシミュレーション結果を示す説明図である。
【図６】図３の発生時刻変更処理の詳細を示すフローチャートである。
【図７】図６の前方変更処理の詳細を示すフローチャートである。
【図８】図６の後方変更処理の詳細を示すフローチャートである。
【図９】発生時刻変更処理前のシミュレーション結果を示すタイミングチャートである。
【図１０】発生時刻変更処理中のシミュレーション結果を示すタイミングチャートである。
【図１１】発生時刻変更処理後のシミュレーション結果を示すタイミングチャートである。
【図１２】図３の回路記述間の不等価判定に伴う信号波形および信号値遷移の波及経路の表示例を示す説明図である。
【符号の説明】
【００６３】
１  ワークステーション
２  ディスプレイ
３  キーボード
４  ＣＰＵ
５  ハードディスク
６  記録媒体ドライブ装置
７  制御装置
８  ＣＤ−ＲＯＭ
９  フレキシブルディスク
１０  上位回路記述
１２  上位シミュレーション結果
２０  下位回路記述
２２  下位シミュレーション結果
１００、２００  回路記述
１０１、２０１  テストベンチ
１０２、２０２  シミュレーション結果
【図１】
2005316595.tif 000003
【図２】
2005316595.tif 000004
【図３】
2005316595.tif 000005
【図４】
2005316595.tif 000006
【図５】
2005316595.tif 000007
【図６】
2005316595.tif 000008
【図７】
2005316595.tif 000009
【図８】
2005316595.tif 000010
【図９】
2005316595.tif 000011
【図１０】
2005316595.tif 000012
【図１１】
2005316595.tif 000013
【図１２】
2005316595.tif 000014