(57)【要約】【課題】回路動作の検証を行うにあたって、回路ブロック毎に、出力信号を入力信号に基づく論理式で表せれば、論理固定値を後段に伝播することが可能となる。前段の回路ブロックから後段の回路ブロックへ、論理固定値を順次伝播することによって、回路の検証に必要な工程数や処理時間を短縮出来る。しかし、論理情報が無いブラックボックス状態の回路ブロックについては、論理固定値を後段に伝播することが不可能だった。【解決手段】論理情報が無いブラックボックス状態の回路ブロックであっても、タイミング情報を考慮することによって、論理固定値を後段の回路に伝播することが可能となる。【選択図】図２
2010140104.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータによって実行される回路検証方法であって、
（ａ）検証対象回路の設計に係るデザインデータと、前記検証対象回路の動作に係るライブラリとを入力するステップと、前記ライブラリは、前記検証対象回路の論理情報と、前記検証対象回路のタイミング情報とを含み、
（ｂ）前記検証対象回路における所定のノードに対して、初期値となる論理固定値を設定するステップと、
（ｃ）論理固定値が設定されたノードから、前記デザインデータをトレースして、前記論理固定値の伝播先となる次段の回路ブロックを選択するステップと、
（ｄ）前記ステップ（ｃ）で選択された回路ブロックにおいて、入力部から出力部へ論理固定値を伝播するステップと、
（ｅ）実行可能な論理固定値の伝播が全ての回路ブロックで完了したかどうかを判定し、前記伝播が完了するまで前記ステップ（ｃ）およびステップ（ｄ）を繰り返すステップと、
（ｆ）実行可能な論理固定値の伝播が全ての回路ブロックで完了していた場合に、前記論理情報伝播部および前記タイミング情報伝播部による前記論理固定値の伝播結果を用いて前記検証対象回路全体の検証を実行するステップと
を具備し、
前記ステップ（ｄ）は、
（ｄ−１）前記ステップ（ｃ）で選択された回路ブロックのライブラリについて、前記ライブラリ中に論理情報が定義されているかどうかを判定するステップと、
（ｄ−２）前記ライブラリ中に前記論理情報が定義されている場合に、前記論理情報に基づいて、前記回路ブロックの入力部から出力部へ論理固定値を伝播するステップと、
（ｄ−３）前記ライブラリ中に前記論理情報が定義されていない場合に、タイミング情報に基づいて、前記回路ブロックの入力部から出力部へ論理固定値を伝播するステップと
を具備する
回路検証方法。
【請求項２】
請求項１に記載の回路検証方法において、
前記ステップ（ｄ−３）は、
（ｄ−３−１）前記ステップ（ｃ）で選択された回路ブロックにおけるタイミング情報が、入力信号と出力信号との関係を定義するタイミングアークの数を１つだけ具備する場合に、前記タイミングアークに基づいて前記出力信号の論理固定値を求めて伝播するステップ
を具備する
回路検証方法。
【請求項３】
請求項１または２に記載の回路検証方法において、
前記ステップ（ｄ−３）は、
（ｄ−３−２）前記ステップ（ｃ）で選択された回路ブロックが複数の入力部を具備し、かつ、前記選択された回路ブロックにおけるタイミング情報が、前記複数の入力部と、前記選択された回路ブロックの出力部とに係る複数のタイミングアークを具備する場合、前記複数のタイミングアークのそれぞれにおいて、活性化条件が満たされているタイミングアークについては前記出力信号における複数の論理値を求め、前記活性化条件が満たされていないタイミングアークについては無視するステップと、
（ｄ−３−３）前記ステップ（ｄ−３−２）で得られた前記複数の論理値のそれぞれについて、確定値「０」または「１」に固定される場合は前記確定値に固定し、確定値に固定されない場合は未確定値として取り扱うステップと、
（ｄ−３−４）前記ステップ（ｄ−３−３）で得られた前記複数の論理値の全てが、任意の確定値に一致した場合に、前記選択された回路ブロックの出力信号として前記任意の確定値を伝播するステップと、
（ｄ−３−５）前記ステップ（ｄ−３−３）で得られた前記複数の論理値のうち、一部が未確定となり、残りの全てが任意の確定値に一致した場合に、前記選択された回路ブロックの出力信号として前記任意の確定値を伝播するステップと、
（ｄ−３−６）前記ステップ（ｄ−３−３）で得られた前記複数の論理値が、前記ステップ（ｄ−３−４）の条件も前記ステップ（ｄ−３−５）の条件も満たさない場合に、前記選択された回路ブロックの出力信号として未確定値を伝播するステップと、
（ｄ−３−７）前記ステップ（ｃ）で選択された回路ブロックにおける入力信号に未確定値が含まれていた場合に、前記未確定値が確定値「０」であった場合と、前記未確定値が確定値「１」であった場合との全ての組み合わせについて、前記ステップ（ｄ−３−４）〜（ｄ−３−６）を実行した場合に前記選択された回路ブロックの出力信号として伝搬される論理値を求めるステップと、
（ｄ−３−８）前記ステップ（ｄ−３−７）で得られた論理値の全てが、任意の確定値に一致した場合に、前記選択された回路ブロックの出力信号として前記任意の確定値を伝播するステップと、
（ｄ−３−９）前記ステップ（ｄ−３−７）で得られた論理値が一致しなかった場合は、前記選択された回路ブロックの出力信号として未確定値を伝播するステップと
を具備する
回路検証方法。
【請求項４】
請求項１〜３のいずれかに記載の回路検証方法において、
前記ステップ（ｄ−３）は、
（ｄ−３−１０）前記ステップ（ｃ）で選択された回路ブロックが有するタイミングアークにハイインピーダンス状態が含まれる場合において、前記ハイインピーダンス状態を含むタイミングアークの入力信号を、トライステートバッファのイネーブル信号として捉えるステップと、
（ｄ−３−１１）前記ステップ（ｄ−３−１０）における前記入力信号の論理値が、ハイインピーダンス状態から確定値へ遷移する側に固定されている場合、前記トライステートバッファのイネーブル信号がＯｎ状態であるとして、他のタイミングアークによる固定値伝播を行うステップと、
（ｄ−３−１２）前記ステップ（ｄ−３−１０）における前記入力信号の論理値が、確定値からハイインピーダンス状態へ遷移する側に固定されている場合、前記トライステートバッファのイネーブル信号がＯｆｆ状態であるとして、前記タイミングアークの出力信号をハイインピーダンス状態とするステップと、
（ｄ−３−１３）前記ステップ（ｄ−３−１０）における前記入力信号の論理値が、前記ステップ（ｄ−３−１１）と、前記ステップ（ｄ−３−１２）との、いずれの場合でも適用範囲外であった場合、出力信号を未確定状態として伝播するステップと
を具備する
回路検証方法。
【請求項５】
請求項１〜４のいずれかに記載の回路検証方法において、
前記ステップ（ｄ−３）は、
（ｄ−３−１４）前記ステップ（ｃ）で選択された回路ブロックが有するタイミングアークの全てが、クロック属性を持つ入力信号に係る場合に、前記回路ブロックの出力信号として不確定値を伝播するステップと、
（ｄ−３−１５）前記ステップ（ｃ）で選択された回路ブロックが有するタイミングアークに、クロック属性を持つ入力信号に係るタイミングアークと、非同期セット／リセットに係るタイミングアークとが含まれる場合に、前記回路ブロックの出力信号として、前記非同期セット／リセットに係るタイミングアークにしたがって得られる固定値を伝播するステップと、
（ｄ−３−１６）前記ステップ（ｃ）で選択された回路ブロックが有するタイミングアークに、クロック属性を持つ入力信号に係るタイミングアークと、非同期セット／リセット以外の入力信号に係るタイミングアークとが含まれ、かつ、前記クロック属性を持つ入力信号の値が、クロックにより遷移が起こる方向に固定されている場合に、前記非同期セット／リセット以外の入力信号に係るタイミングアークにしたがって得られる固定値を、前記回路ブロックの出力信号として伝播するステップと
を具備する
回路検証方法。
【請求項６】
検証対象回路の設計に係るデザインデータと、前記検証対象回路の動作に係るライブラリとを入力する入力部と、
前記デザインデータを記憶するためのデザイン記憶部と、
前記ライブラリに含まれる前記検証対象回路の論理情報を記憶するための論理情報記憶部と、
前記ライブラリに含まれる前記検証対象回路のタイミング情報を記憶するためのタイミング情報記憶部と、
前記検証対象回路における所定のノードに対して、初期値となる論理固定値を設定する論理固定値設定部と、
論理固定値が設定されたノードから、前記デザインデータをトレースして、前記論理固定値の伝播先となる次段の回路ブロックを選択する次段回路ブロック選択部と、
前記次段回路ブロック選択部が選択した回路ブロックのライブラリについて、前記ライブラリ中に論理情報が定義されているかどうかを判定するライブラリ判定部と、
前記ライブラリ中に前記論理情報が定義されている場合に、前記論理情報に基づいて、前記回路ブロックの入力部から出力部へ論理固定値を伝播する論理情報伝播部と、
前記ライブラリ中に前記論理情報が定義されていない場合に、タイミング情報に基づいて、前記回路ブロックの入力部から出力部へ論理固定値を伝播するタイミング情報伝播部と、
実行可能な論理固定値の伝播が全ての回路ブロックで完了したかどうか判定する伝播完了判定部と、
実行可能な論理固定値の伝播が全ての回路ブロックで完了していた場合に、前記論理情報伝播部および前記タイミング情報伝播部による前記論理固定値の伝播結果を用いて前記検証対象回路全体の検証を実行する検証実行部と
を具備する
回路検証装置。
【請求項７】
請求項６に記載の回路検証装置において、
回路検証プログラムを記憶するためのプログラム記憶部と、
前記検証実行部が実行した検証の結果を出力するための出力部と
をさらに具備する
回路検証装置。
【請求項８】
請求項１〜５のいずれかに記載の回路検証方法において、
前記ステップのそれぞれを、計算機で実行可能に具備する
回路検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路の動作を検証する回路検証方法と、この回路検証方法を用いるための回路検証装置と、この回路検証装置でこの回路検証方法を実施するための回路検証プログラムとに係る。
【背景技術】
【０００２】
情報機器の高機能化にしたがい、１つの半導体装置に搭載される集積回路の規模が増大を続けている。特に高集積化されたシステムＬＳＩ（Ｌａｒｇｅ  Ｓｃａｌｅ  Ｉｎｔｅｇｒａｔｉｏｎ）やＳｏＣ（Ｓｙｓｔｅｍ  Ｏｎ  ａ  Ｃｈｉｐ）では、半導体集積回路のデザインをＨＤＬ（Ｈａｒｄｗａｒｅ  Ｄｅｓｃｒｉｐｔｉｏｎ  Ｌａｎｇｕａｇｅ）で記述することが多い。この場合、ＨＤＬによるデザインでは、回路の具体的な内容の全てを設計者が把握する必要は無いため、いわゆるブラックボックスとして取り扱われる回路ブロックが存在する。
【０００３】
ブラックボックス状態の回路ブロックは、その実際の運用においては、どの入力信号に対してどの出力信号が得られるかだけを把握できれば十分である。しかし、設計段階において、ブラックボックス状態の回路ブロックを含む集積回路全体が所望の動作を達成できるかどうか、シミュレーションしておく必要がある。このとき、集積回路全体のデザインに関わるデータと、集積回路を構成する各回路ブロックの論理情報を定義するライブラリとが用いられる。ただし、ブラックボックス状態の回路ブロックについては、その論理情報が不明であるため、そのままではライブラリの中で定義することが出来ない。
【０００４】
図１は、従来技術における回路検証方法について説明するためのフローチャートである。このフローチャートは、デザインおよびライブラリの入力を行うステップＳ１０１と、論理固定値の設定を行うステップＳ１０２と、論理固定値の次段への伝播を行うステップＳ１０３と、ライブラリセルの論理情報を用いた固定値伝播の実行を行うステップＳ１０４と、回路中の固定値伝播が完了したかどうかを判定するステップＳ１０５と、固定値伝播結果を用いた検証の実行を行うステップＳ１０６とを具備する。
【０００５】
図１のフローチャートでは、最初に、ステップＳ１０１が実行される。ステップＳ１０１の次には、ステップＳ１０２が実行される。ステップＳ１０２の次には、ステップＳ１０３が実行される。ステップＳ１０３の次には、Ｓ１０４が実行される。ステップＳ１０４の次には、ステップＳ１０５が実行される。ステップＳ１０５の判定結果が「ｎｏ」であった場合には、その次にステップＳ１０３〜ステップＳ１０５が再度実行される。ステップＳ１０５の判定結果が「ｙｅｓ」であった場合には、その次にステップＳ１０６が実行される。ステップＳ１０６が実行されると、図１のフローチャートは終了する。
【０００６】
図１のフローチャートの各ステップについて詳細に説明する。
【０００７】
ステップＳ１０１では、検証対象回路の設計に係るデザインデータと、動作に係るライブラリとを入力する。
【０００８】
ステップＳ１０２では、検証対象回路のスタートポイントに対して初期値としての論理固定値を設定する。検証対象回路のスタートポイントとは、検証対象回路の任意のノードであり、例えば、検証対象回路全体における外部入力端子が含まれる。
【０００９】
ステップＳ１０３では、設定されたスタートポイントから、デザインデータをトレースして、論理固定値を伝播する次段の回路ブロックを選択する。
【００１０】
ステップＳ１０４では、選択された回路ブロックにおいて、ライブラリに定義された論理情報に基づいて、入力信号の論理固定値から出力信号への論理固定値の伝播を行う。なお、論理固定値の伝播を行った後、選択された回路ブロックの後段の出力信号を入力する回路ブロック、すなわち後段の回路ブロックを、新しく選択する。
【００１１】
ステップＳ１０５では、検証対象回路全体で、可能な論理固定値の伝播が全ての回路ブロックで行われたかどうか判定する。
【００１２】
ステップＳ１０６では、伝播させた論理固定値を利用して、検証対象回路における各種の検証を行う。
【００１３】
上記に関連して、特許文献１（特開２００７−１４０８７７号公報）には、論理等価性検証システムに係る記載が開示されている。特許文献１に記載の論理等価性検証システムは、ＲＴＬ（Ｒｅｇｉｓｔｅｒ  Ｔｒａｎｓｆｅｒ  Ｌｅｖｅｌ）／ゲートレベル回路記述と、ライブラリと、論理等価性検証部とを具備することを特徴とする。ここで、ＲＴＬ／ゲートレベル回路記述は、ＲＴＬ回路記述情報及びゲートレベル記述情報を有する。ライブラリは、論理等価性検証実行用情報を有する。論理等価性検証部は、コンパイラと、検証回路データベースと、論理等価性検証処理部と、ブラックボックスセル更新手段とを有する。さらにここで、コンパイラは、前記ＲＴＬ／ゲートレベル回路記述情報及び前記ライブラリ情報から、回路データベースを作成する。検証回路データベースは、前記コンパイラから出力される情報から参照回路情報を作成する参照回路データベースと、前記コンパイラから出力される情報から検証回路情報を作成する。論理等価性検証処理部は、前記参照回路データベース及び前記検証回路データベースから出力される情報から検証処理を実行する。ブラックボックスセル更新手段は、ブラックボックスセルに任意の論理を与えてファンクションセルに更新する。
【００１４】
【特許文献１】特開２００７−１４０８７７号公報
【発明の開示】
【発明が解決しようとする課題】
【００１５】
以上に説明したように、回路の検証を行うにあたって、回路ブロック毎に、出力信号を入力信号に基づく論理式で表せれば、論理固定値を後段に伝播することが可能となる。前段の回路ブロックから後段の回路ブロックへ、論理固定値を順次伝播することによって、回路の検証に必要な工程数や処理時間を短縮出来る。しかし、論理情報が無いブラックボックス状態の回路ブロックについては、論理固定値を後段に伝播することが不可能だった。
【課題を解決するための手段】
【００１６】
以下に、（発明を実施するための最良の形態）で使用される番号を用いて、課題を解決するための手段を説明する。これらの番号は、（特許請求の範囲）の記載と（発明を実施するための最良の形態）との対応関係を明らかにするために付加されたものである。ただし、それらの番号を、（特許請求の範囲）に記載されている発明の技術的範囲の解釈に用いてはならない。
【００１７】
本発明による回路検証方法は、（ａ）検証対象回路の設計に係るデザインデータと、検証対象回路の動作に係るライブラリとを入力するステップと、ライブラリは、検証対象回路の論理情報と、検証対象回路のタイミング情報とを含み、（ｂ）検証対象回路における所定のノードに対して、初期値となる論理固定値を設定するステップと、（ｃ）論理固定値が設定されたノードから、デザインデータをトレースして、論理固定値の伝播先となる次段の回路ブロックを選択するステップと、（ｄ）ステップ（ｃ）で選択された回路ブロックにおいて、入力部から出力部へ論理固定値を伝播するステップと、（ｅ）実行可能な論理固定値の伝播が全ての回路ブロックで完了したかどうかを判定し、伝播が完了するまでステップ（ｃ）およびステップ（ｄ）を繰り返すステップと、（ｆ）実行可能な論理固定値の伝播が全ての回路ブロックで完了していた場合に、論理情報伝播部およびタイミング情報伝播部による論理固定値の伝播結果を用いて検証対象回路全体の検証を実行するステップとを具備する。ステップ（ｄ）は、（ｄ−１）ステップ（ｃ）で選択された回路ブロックのライブラリについて、ライブラリ中に論理情報が定義されているかどうかを判定するステップと、（ｄ−２）ライブラリ中に論理情報が定義されている場合に、論理情報に基づいて、回路ブロックの入力部から出力部へ論理固定値を伝播するステップと、（ｄ−３）ライブラリ中に論理情報が定義されていない場合に、タイミング情報に基づいて、回路ブロックの入力部から出力部へ論理固定値を伝播するステップとを具備する。
【００１８】
本発明による回路検証装置は、入力部と、デザイン記憶部と、論理情報記憶部と、タイミング情報記憶部と、論理固定値設定部と、次段回路ブロック選択部と、ライブラリ判定部と、論理情報伝播部と、タイミング情報伝播部と、伝播完了判定部と、検証実行部とを具備する。ここで、入力部は、検証対象回路の設計に係るデザインデータと、検証対象回路の動作に係るライブラリとを入力するものである。デザイン記憶部は、デザインデータを記憶するためのものである。論理情報記憶部は、ライブラリに含まれる検証対象回路の論理情報を記憶するためのものである。タイミング情報記憶部は、ライブラリに含まれる検証対象回路のタイミング情報を記憶するためのものである。論理固定値設定部は、検証対象回路における所定のノードに対して、初期値となる論理固定値を設定するものである。次段回路ブロック選択部は、論理固定値が設定されたノードから、デザインデータをトレースして、論理固定値の伝播先となる次段の回路ブロックを選択するものである。ライブラリ判定部は、次段回路ブロック選択部が選択した回路ブロックのライブラリについて、ライブラリ中に論理情報が定義されているかどうかを判定するものである。論理情報伝播部は、ライブラリ中に論理情報が定義されている場合に、論理情報に基づいて、回路ブロックの入力部から出力部へ論理固定値を伝播するものである。タイミング情報伝播部は、ライブラリ中に論理情報が定義されていない場合に、タイミング情報に基づいて、回路ブロックの入力部から出力部へ論理固定値を伝播するものである。伝播完了判定部は、実行可能な論理固定値の伝播が全ての回路ブロックで完了したかどうか判定するものである。検証実行部は、実行可能な論理固定値の伝播が全ての回路ブロックで完了していた場合に、論理情報伝播部およびタイミング情報伝播部による論理固定値の伝播結果を用いて検証対象回路全体の検証を実行するものである。
【発明の効果】
【００１９】
本発明の回路検証方法と、回路検証装置と、回路検証プログラムとによれば、論理情報が無いブラックボックス状態の回路ブロックであっても、タイミング情報を考慮することによって、論理固定値を後段の回路に伝播することが可能となる。
【発明を実施するための最良の形態】
【００２０】
添付図面を参照して、本発明による回路検証方法と、回路検証装置と、回路検証プログラムとを実施するための最良の形態を以下に説明する。
【００２１】
図１１は、本発明の実施形態における回路検証装置の構成を説明するためのブロック図である。この回路検証装置は、例えば、入力部１１１と、演算部１１２と、記憶部１１３と、出力部１１４とを具備する計算機を用いて構成しても良い。ここで、記憶部１１３は、プログラム記憶部１１３１と、デザイン記憶部１１３２と、ライブラリセル１１３３とを具備する。ライブラリセル１１３３は、論理情報記憶部１１３４と、タイミング情報記憶部１１３５とを具備する。
【００２２】
入力部１１１は、演算部１１２に接続されている。演算部１１２は、記憶部１１３と、出力部１１４とに接続されている。
【００２３】
記憶部１１３は、プログラム、デザイン、論理情報、タイミング情報などを記憶するためのものである。
【００２４】
プログラム記憶部１１３１は、本発明による回路検証プログラムを記憶するためのものである。
【００２５】
デザイン記憶部１１３２は、検証対象回路の設計に係るデザインのデータを記憶するためのものである。検証対象回路のデザインは、検証対象回路を構成する回路ブロックや、これらの回路ブロック同士の接続関係などの情報を含む。
【００２６】
ライブラリセル１１３３は、検証対象回路の動作に係るライブラリ情報を記憶するためのものである。ライブラリ情報は、論理情報と、タイミング情報とを含む。
【００２７】
論理情報記憶部は、ライブラリ情報のうち、論理情報を記憶するためのものである。論理情報は、それぞれの回路ブロックにおいて、出力信号を入力信号に基づく論理式で表現したものである。なお、全ての回路ブロックにおいて論理情報が存在するとは限らない。特に、内部がブラックボックス状態であれば、その回路ブロックの論理情報は用意し得ない。
【００２８】
タイミング情報は、ライブラリ情報のうち、タイミング情報を記憶するためのものである。タイミング情報は、それぞれの回路ブロックにおいて、入力信号と出力信号との遅延量、論理値の可能な組み合わせ、限定条件、などの情報を含む。これらのタイミング情報は、１つの入力信号と、１つの出力信号との関係を表すタイミングアークの集合として捉えることが可能である。
【００２９】
入力部１１１は、回路検証プログラム、検証対象回路のデザイン、検証対象回路のライブラリ情報、論理情報、タイミング情報などを外部から入力するためのものである。ただし、これらの情報の一部または全てが、予め記憶部１１３に記憶されている場合は、さらに入力する必要は無い。
【００３０】
演算部１１２は、検証対象回路のデザイン、論理情報、タイミング情報などを用いて、回路検証プログラムを実行するためのものである。
【００３１】
出力部１１４は、演算部１１２の演算結果を外部に出力するためのものである。ただし、演算部１１２の演算結果を記憶部１１３に記憶しても良い。
【００３２】
なお、ここで説明した回路検証装置は、あくまでも一例であって、必ずしもこの構成に限定されない。同じ機能を実施可能であれば、他の構成であっても構わない。
【００３３】
図２は、本発明の実施形態における回路検証方法について説明するためのフローチャートである。このフローチャートは、デザインおよびライブラリの入力を行うステップＳ２０１と、論理固定値の設定を行うステップＳ２０２と、論理固定値の次段への伝播を行うステップＳ２０３と、論理固定値の伝播先のライブラリセルに論理情報が存在するかどうかを判定するステップＳ２０４と、ライブラリセルの論理情報を用いた固定値伝播の実行を行うステップＳ２０５−１と、ライブラリセルのタイミング情報を用いた固定値伝播の実行を行うステップＳ２０５−２と、回路中の固定値伝播が完了したかどうかを判定するステップＳ２０６と、固定値伝播結果を用いた検証の実行を行うステップＳ２０７とを具備する。
【００３４】
図２のフローチャートでは、最初に、ステップＳ２０１が実行される。ステップＳ２０１の次には、ステップＳ２０２が実行される。ステップＳ２０２の次には、ステップＳ２０３が実行される。ステップＳ２０３の次には、ステップＳ２０４が実行される。ステップＳ２０４における判定結果が「ｙｅｓ」であった場合には、その次にステップＳ２０５−１が実行される。ステップＳ２０４における判定結果が「ｎｏ」であった場合には、その次にステップＳ２０５−２が実行される。ステップＳ２０５−１またはステップＳ２０５−２の次には、ステップＳ２０６が実行される。ステップＳ２０６の判定結果が「ｎｏ」であった場合には、その次にステップＳ２０３〜ステップＳ２０６が再度実行される。ステップＳ２０６の判定結果が「ｙｅｓ」であった場合には、その次にステップＳ２０７が実行される。ステップＳ２０７が実行されると、図２のフローチャートは終了する。
【００３５】
図２のフローチャートの各ステップについて詳細に説明する。
【００３６】
ステップＳ２０１では、検証対象回路のデザインとライブラリとを入力する。
【００３７】
ステップＳ２０２では、検証対象回路のスタートポイントに対して論理固定値を設定する。回路の検証は、後述するように、回路ブロック単位で、前段から後段に向かって行う。そこで、最も前段の回路ブロックの入力部から検証を開始することが好ましい。検証対象回路のスタートポイントとは、検証に用いる初期値を設定するための、検証対象回路に含まれる任意のノードであり、例えば、検証対象回路全体における外部入力端子が含まれる。
【００３８】
ステップＳ２０３では、設定されたスタートポイントから、デザインをトレースして、論理固定値を伝播する次段の回路ブロックを選択する。
【００３９】
ステップＳ２０４では、ステップＳ２０３で選択された回路ブロックのライブラリを参照する。ここで、ライブラリ中に論理情報が定義されていれば、ステップＳ２０５−１に進む。ここで、ライブラリ中に論理情報が定義されていなければ、ステップＳ２０５−２に進む。
【００４０】
ステップＳ２０５−１では、選択された回路ブロックにおいて、ライブラリに定義された論理情報に基づいて、入力信号の論理固定値から出力信号への論理固定値の伝播を行う。なお、論理固定値の伝播を行った後、選択された回路ブロックの後段の出力信号を入力する回路ブロック、すなわち後段の回路ブロックを、新しく選択する。
【００４１】
ステップＳ２０５−２では、選択された回路ブロックにおいて、ライブラリに定義されたタイミング情報に基づいて、入力信号の論理固定値を出力信号に伝播させる。この具体的な方法については、後で詳細に説明する。なお、論理固定値の伝播を行えた場合は、選択された回路ブロックの後段の出力信号を入力する回路ブロック、すなわち後段の回路ブロックを、新しく選択する。
【００４２】
ステップＳ２０６では、検証対象回路全体で、可能な論理固定値の伝播が全ての回路ブロックで行われたかどうか判定する。
【００４３】
ステップＳ２０７では、伝播させた論理固定値を利用して、検証対象回路における各種の検証を行う。
【００４４】
図１２は、本発明による回路検証装置の構成を機能ブロックで説明するためのブロック図である。図１１における演算部および記憶部を利用して、図２における各ステップをそれぞれに実行可能な機能ブロックを構成していることを説明する。なお、図１１と図１２で共通する構成要素については、同じ番号を用いて説明する。
【００４５】
本発明による回路検証装置は、機能ブロックとして、入力部１１１と、記憶演算部１２と、出力部１１４とを具備する。記憶演算部１２は、デザイン記憶部１１３２と、ライブラリセル１１３３と、論理固定値設定部１２１と、次段回路ブロック選択部１２２と、ライブラリ判定部１２３と、論理情報伝達部１２４と、タイミング情報伝達部１２５と、伝播完了判定部１２６と、検証実行部１２７とを具備する。ライブラリセル１１３３は、論理情報記憶部１１３４と、タイミング情報記憶部１１３５とを具備する。
【００４６】
記憶演算部１２は、入力部１１１と、出力部１１４とに接続されている。記憶演算部１２に含まれる各機能ブロックは、実質的には演算部１１２と記憶部１１３であって、相互に接続されていると捉えることも出来るので、その接続関係にかかわる説明を省略する。
【００４７】
入力部１１１は、ステップＳ２０１を実行するための機能ブロックである。なお、ステップＳ２０１で入力したデザインおよびライブラリは、それぞれ、デザイン記憶部１１３２およびライブラリセル１１３３に記憶される。さらには、ステップＳ２０１で入力したライブラリのうち、論理情報およびタイミング情報は、それぞれ、論理情報記憶部１１３４およびタイミング情報記憶部１１３５に記憶される。
【００４８】
論理固定値設定部１２１は、ステップＳ２０２を実行するための機能ブロックである。
【００４９】
次段回路ブロック選択部１２２は、ステップＳ２０３を実行するための機能ブロックである。
【００５０】
ライブラリ判定部１２３は、ステップＳ２０４を実行するための機能ブロックである。
【００５１】
論理情報伝達部１２４は、ステップＳ２０５−１を実行するための機能ブロックである。
【００５２】
タイミング情報伝達部１２５は、ステップＳ２０５−２を実行するための機能ブロックである。
【００５３】
伝播完了判定部１２６は、ステップＳ２０６を実行するための機能ブロックである。
【００５４】
検証実行部１２７は、ステップＳ２０７を実行するための機能ブロックである。なお、ステップＳ２０７で得られた結果は、出力部１１４から外部に出力される。
【００５５】
上記に説明したステップＳ２０１〜Ｓ２０３、Ｓ２０５−１、Ｓ２０６およびＳ２０７は、図１のフローチャートで従来技術として説明したステップＳ１０１〜Ｓ１０３、Ｓ１０４、Ｓ１０５およびＳ１０６と同じである。すなわち、本発明による回路検証方法は、図１で説明した従来技術に、論理情報が無いブラックボックス状の回路ブロックを選び出すステップＳ２０４と、ブラックボックス状の回路ブロックにおいてタイミング情報だけで論理固定値の伝播を試みるステップＳ２０５−２とを追加したものであると捉えることが出来る。
【００５６】
また、本発明による回路検証方法において重要なのは、論理固定値を伝播することであって、ステップＳ２０７における検証については従来技術のものを用いればよいので、その詳細な説明を省略する。
【００５７】
ここで、ステップＳ２０５−２の詳細について説明する。ここでは、検証対象となるブラックボックス回路の種類によって、固定論理伝播の動作が異なるので、それぞれの場合を実施例として説明する。
【００５８】
（第１の実施例）
検証対象となるブラックボックス回路の第１の種類として、出力信号に１つの入力信号からのタイミングアークしか存在しない場合について説明する。
【００５９】
【表１】
2010140104.tif 000003
【００６０】
表１は、入力遷移および出力遷移の組み合わせと、固定論理伝播動作との対応関係を説明するための表である。ここで、「Ｒｉｓｅ」は０から１への遷移を意味し、「Ｆａｌｌ」は１から０への遷移を意味する。
【００６１】
例えば、１行目の「Ｒｉｓｅ−Ｒｉｓｅ」は、入力信号が０から１へ遷移する時に、出力信号も０から１へ遷移することを意味する。同じく「Ｆａｌｌ−Ｆａｌｌ」は、入力信号が１から０へ遷移する時に、出力信号も１から０へ遷移することを意味する。すなわち、１行目に対応する固定論理伝播動作は、入力信号の値をそのまま出力信号として伝播することに他ならない。
【００６２】
また、２行目の「Ｒｉｓｅ−Ｆａｌｌ」は、入力信号が１から０へ遷移する時に、出力信号は反対に０から１へ遷移することを意味する。同じく「Ｆａｌｌ−Ｒｉｓｅ」は、入力信号が１から０へ遷移する時に、出力信号は反対に０から１へ遷移することを意味する。すなわち、２行目に対応する固定論理伝播動作は、荷や羽力信号の値を反転して出力信号として伝播することに他ならない。
【００６３】
図３は、１入力１出力のブラックボックス回路３について説明するための概略図である。このブラックボックス回路３は、入力部３１と、出力部３２とを具備する。
【００６４】
このブラックボックス回路３は、入力部３１に供給される入力信号Ａの値に基づいて、出力部３２から出力信号Ｙを出力する。
【００６５】
このブラックボックス回路３のタイミングアークが、表１の１行目と同じ組み合わせであった場合、入力信号Ａの値が「０」に固定されると、出力信号Ｙの値は「０」に固定される。同様に、入力信号Ａの値が「１」に固定されると、出力信号Ｙの値は「１」に固定される。
【００６６】
（第２の実施例）
次に、検証対象となるブラックボックス回路の第２の種類として、出力信号に複数の入力信号からのタイミングアークが存在する場合について説明する。
【００６７】
複数の入力信号からのタイミングアークが存在する場合、個々のタイミングアークについては固定値伝播の値を確定できても、これらの値が一致しない場合がある。これでは、最終的な値が確定されない。そこで、１入力１出力の場合における処理に、次のような条件判断動作を追加する。すなわち、複数のタイミングアークのそれぞれについて、個々のタイミングアークが有効となる条件を考慮した上で固定値の伝播を行う。この条件を、以下、「活性化条件」と呼ぶ。
【００６８】
固定値伝播は、次の５つのルールに従って行う。第１のルールでは、複数のタイミングアークのそれぞれを個別に処理して、出力信号Ｙの値を確定する。ただし、出力信号Ｙの値が０または１に確定されない場合は、未確定値「Ｘ」として扱う。
【００６９】
第２のルールでは、第１のルールを適用した結果、複数のタイミングアークの全てにおいて、出力信号Ｙの値が一致し、かつ、この値が「０」または「１」であるなら、その値を出力信号Ｙとして伝播する。
【００７０】
第３のルールでは、第１のルールを適用した結果、出力信号Ｙの値が未確定となった場合は、活性化条件が有効なタイミングアークのみに着目し、そのタイミングアークの全てにおいて、出力信号Ｙの値が「０」または「１」のどちらかに一致した場合は、その値を出力信号Ｙとして伝播する。
【００７１】
第４のルールでは、第１のルールを適用した結果、上記以外の状態が得られた場合は、出力信号Ｙの値は未確定値とする。
【００７２】
第５のルールでは、第１のルールが適用不可能である場合、すなわち、入力信号の値に未確定値「Ｘ」が含まれていた場合には、その入力信号が「０」であった場合と、「１」であった場合との全ての組み合わせについて、ルール２〜４を適用する。その結果、いずれの場合でも出力信号Ｙが「０」または「１」のどちらかに一致した場合は、その値を出力信号Ｙとして伝播する。反対に、出力信号Ｙの値が一致しなかった場合は、未確定値「Ｘ」を出力信号Ｙとして伝播する。
【００７３】
図４は、２入力１出力のブラックボックス回路４について説明するための概略図である。このブラックボックス４は、第１の入力部４１と、第２の入力部４２と、出力部４３とを具備する。
【００７４】
このブラックボックス回路４は、第１の入力部４１から供給される第１の入力信号Ａと、第２の入力部４２から供給される第２の入力信号Ｂとに基づいて、出力信号Ｙを出力部４３から出力する。
【００７５】
例として、次のような場合について説明する。第１の入力信号Ａと、出力信号Ｙとに係る第１のタイミングアークは、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌと、活性化条件「Ｂ＝１」との組み合わせである。第２の入力信号Ｂと、出力信号Ｙとに係る第２のタイミングアークは、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌと、活性化条件「Ａ＝１」との組み合わせである。
【００７６】
活性化条件の詳細について説明する。上記における第１のタイミングアークの場合、活性化条件「Ｂ＝１」とは、第２の入力信号Ｂ＝１の時に、Ｒｉｓｅ−ＲｉｓｅおよびＦａｌｌ−Ｆａｌｌが有効になることを意味する。反対に、第２の入力信号Ｂ＝０の時は、第１の入力信号Ａと出力信号Ｙとに係る関係は、Ｒｉｓｅ−ＲｉｓｅもＦａｌｌ−Ｆａｌｌも無効化される。
【００７７】
ここで、第１の入力信号Ａと、第２の入力信号Ｂとに具体的な値を当てはめて、それぞれのケースについて説明する。
【００７８】
第１のケースとして、第１の入力信号Ａ＝０、第２の入力信号Ｂ＝０の場合について説明する。第１のルールを適用すると、第１のタイミングアークでも、第２のタイミングアークでも、出力信号Ｙ＝０が得られる。ここで、第２のルールを適用して、出力信号Ｙとして「０」を伝播する。
【００７９】
第２のケースとして、第１の入力信号Ａ＝０、第２の入力信号Ｂ＝１の場合について説明する。第１のルールを適用すると、第１のタイミングアークでは出力信号Ｙ＝０となり、第２のタイミングアークでは出力信号Ｙ＝１となる。第２のルールは適用できないので、第３のルールを適用すると、第１のタイミングアークでは活性化条件が有効であり、第２のタイミングアークでは活性化条件が無効である。したがって、出力信号Ｙの値として、第１のタイミングアークで得られた「０」を伝播する。
【００８０】
第３のケースとして、第１の入力信号Ａ＝未確定値「Ｘ」、第２の入力信号Ｂ＝０の場合について説明する。第１のルールが適用不可能なので、第５のルールを適用する。第１の入力信号Ａ＝０と仮定すると、第２のルールによって出力信号Ｙ＝０が得られる。第１の入力信号Ｂ＝１と仮定すると、第３のルールによって出力信号Ｙ＝０が得られる。第１の入力信号Ａの値が「１」であっても「０」であっても、出力信号Ｙの値は「０」が得られるので、第５のルールによって出力信号Ｙの値として「０」が伝播される。
【００８１】
（第３の実施例）
次に、検証対象となるブラックボックス回路の第３の種類として、タイミングアークにＨｉＺ（ハイインピーダンス）状態への遷移を含む場合について説明する。
【００８２】
検証対象となっているブラックボックス回路のタイミングアークに、Ｈｉｚ状態への遷移が含まれている場合を考える。この場合、このタイミングアークの入力信号を、トライステートバッファのイネーブル信号として捉え、以下のルールに従って処理を行う。
【００８３】
第１のルールとして、入力信号がＨｉＺ状態から確定値へ遷移する側に固定されている場合、トライステートバッファのイネーブル信号がＯｎ状態であるとして、他のタイミングアークによる固定値伝播を行う。
【００８４】
第２のルールとして、入力信号が確定値からＨｉＺ状態へ遷移する側に固定されている場合、トライステートバッファのイネーブル信号がＯｆｆ状態であるとして、出力信号をＨｉＺ状態とする。
【００８５】
第３のルールとして、第１のルールでも第２のルールでも適用範囲外の場合、固定値伝播処理を行わず、出力信号を未確定状態「Ｘ」とする。これは、トライステートバッファのイネーブル信号がＯｆｆ状態となる可能性があるためである。
【００８６】
図５は、ＨｉＺ状態への遷移を含むタイミングアークを有するブラックボックス回路５について説明するための概略図である。このブラックボックス回路５は、第１の信号入力部５１と、第２の信号入力部５２と、信号出力部５３とを具備する。
【００８７】
このブラックボックス回路５は、第１の信号入力部５１から供給される第１の入力信号Ａと、第２の信号入力部５２から供給される第２の入力信号ＥＮとに基づいて、出力信号Ｙを信号出力部５３から出力する。
【００８８】
例として、次のような場合について説明する。第１の入力信号Ａと、出力信号Ｙとに係る第１のタイミングアークは、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌとの組み合わせである。第２の入力信号ＥＮと、出力信号Ｙとに係る第２のタイミングアークは、Ｒｉｓｅ−ＺＨと、Ｒｉｓｅ−ＺＬと、Ｆａｌｌ−Ｈｚと、Ｆａｌｌ−ＬＺとの組み合わせである。ここで、ＺＨと、ＺＬと、ＨＺと、ＬＺとはそれぞれ、ＨｉＺ状態から確定値「１」への遷移と、ＨｉＺ状態から確定値「０」への遷移と、確定値「１」からＨｉＺ状態への遷移と、確定値「０」からＨｉＺ状態への遷移とに対応している。
【００８９】
ここで、この第２の入力信号ＥＮに係る第２のタイミングアークがＨｉＺ状態への遷移を含む場合について、第２の入力信号ＥＮに具体的な固定値を設定しながらそれぞれのケースを考える。
【００９０】
第１のケースとして、第２の入力信号ＥＮ＝０の場合について説明する。第２の入力信号ＥＮは、０に固定されている。これは、第２の入力信号ＥＮにおけるＦａｌｌ動作が完了した状態である。第２のタイミングアークによれば、第２の入力信号ＥＮがＦａｌｌ動作を完了した時、出力信号Ｙは確定値「１」または確定値「０」からＨｉＺ状態へ遷移する動作を完了しなければならない。いずれにしても、第２の入力信号ＥＮは、出力信号ＹがＨｉＺ状態へ遷移する側に固定されている。そこで、第２のルールを適用して、出力信号ＹをＨｉＺ状態に設定する。
【００９１】
第２のケースとして、第２の入力信号ＥＮ＝１の場合について説明する。第２の入力信号ＥＮは、１に固定されている。これは、第２の入力信号ＥＮにおけるＲｉｓｅ動作が完了した状態である。第２のタイミングアークによれば、第２の入力信号ＥＮがＲｉｓｅ動作を完了した時、出力信号ＹはＨｉＺ状態から確定値「０」または確定値「１」へ遷移する動作を完了しなければならない。いずれにしても、第２の入力信号ＥＮは、出力信号ＹがＨｉＺ状態から遷移する側に固定されている。そこで、第１のルールを適用して、他のタイミングアークによる固定値伝播を行う。すなわち、第１のタイミングアークで決定される出力信号Ｙの値を伝播する。
【００９２】
（第４の実施例）
次に、検証対象となるブラックボックス回路の第４の種類として、入力信号がクロック属性を持つ場合について説明する。
【００９３】
【表２】
2010140104.tif 000004
【００９４】
表２は、入力信号がクロック属性を持つ場合に、他のタイミングアークの状況に応じて行う処理を説明するためのものである。
【００９５】
表２に記載のとおり、入力信号がクロック属性を持つ場合には、以下の３つのルールを適用して固定論理伝播動作を行う。
【００９６】
第１のルールとして、クロック属性を持つ入力信号に係るタイミングアーク以外に他のタイミングアークが存在しない場合は、固定値の論理伝播を行わない。このとき、出力信号は不確定値「Ｘ」となる。
【００９７】
第２のルールとして、クロック属性を持つ入力信号に係るタイミングアーク以外に、非同期セット／リセットに係るタイミングアークが存在する場合には、この非同期セット／リセットに係るタイミングアークにしたがって固定値の論理伝播を行う。
【００９８】
第３のルールとして、クロック属性を持つ入力信号に係るタイミングアーク以外に、非同期セット／リセットに係らないタイミングアークが存在し、かつ、前者のタイミングアークにかかわる入力信号の値がクロックにより遷移が起こる方向に固定されている場合、後者のタイミングアークにしたがって固定値の論理伝播を行う。
【００９９】
図６は、クロック属性端子を含むブラックボックス回路６について説明するための概略図である。このブラックボックス回路６は、第１の入力部６１と、第２の入力部６２と、出力部６３とを具備する。
【０１００】
このブラックボックス回路６は、第１の入力部６１に供給される第１の入力信号Ａの値と、第２の入力部６２に供給される第２の入力信号Ｃの値とに基づいて、出力部６３から出力信号Ｙを出力する。
【０１０１】
このブラックボックス回路６において、第２の入力部６２から供給される第２の入力信号Ｃにクロック属性が付加されている場合について説明する。
【０１０２】
第１のケースとして、このブラックボックス回路６が次のようなタイミングアークを有する場合を考える。第１のタイミングアークは、第２の入力信号Ｃと、出力信号Ｙとに係り、その具体的な内容としては、Ｒｉｓｅ−Ｒｉｓｅと、Ｒｉｓｅ−Ｆａｌｌとの組み合わせである。第１の入力信号Ａと、出力信号Ｙとに係るタイミングアークは存在しない。
【０１０３】
このケースでは、クロック属性に係るタイミングアーク以外のタイミングアークが存在しないので、第１のルールが適用される。その結果、固定値伝版処理を行わない。言い換えれば、第２の入力信号Ｃが固定されているとこのブラックボックス回路６が動作しないと考えられる。
【０１０４】
第２のケースとして、このブラックボックス回路６が次のようなタイミングアークを有する場合を考える。第１のタイミングアークは、第１の入力信号Ａと、出力信号Ｙとに係り、その具体的な内容は、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌとの組み合わせである。第２のタイミングアークは、第２の入力信号Ｃと、出力信号Ｙとに係り、その具体的な内容は、Ｒｉｓｅ−Ｒｉｓｅと、Ｒｉｓｅ−Ｆａｌｌとの組み合わせである。
【０１０５】
このケースでは、クロック属性を持つ入力信号に係る第２のタイミングアーク以外に、非同期セット／リセットに係らない第１のタイミングアークが存在する。また、第２のタイミングアークに係る第２の入力信号Ｃの値は１に固定されている。すなわち、第２の入力信号Ｃの値は、クロックにより遷移が起こる方向に固定されている。その結果、第３のルールが適用されて、第１のタイミングアークによる固定値伝播処理を行う。
【０１０６】
（第５の実施例）
ここまで、本発明の第１〜４の実施例について説明した。そのために用いた第１〜４の種類のブラックボックス回路３〜６は、固定論理伝播の動作における概念を示すための、各機能に特化した単純なモデルであった。しかし、実際に論理モデルを記述できないようなブラックボックス回路は、これらのように単純化できるものではない。このように複雑な論理を持つブラックボックス回路に対する本発明の適用を、以下に説明する。
【０１０７】
例として、差動入力バッファについて説明する。図７は、差動入力バッファ７について説明するための概略図である。この差動入力バッファ７は、第１の入力部７１と、第２の入力部７２と、出力部７３とを具備する。
【０１０８】
この差動入力バッファ７は、第１の入力部７１から供給される第１の入力信号Ａの値と、第２の入力部７２から供給される第２の入力信号Ｂの値とに基づいて、出力部７３から出力信号Ｙを出力する。
【０１０９】
差動入力バッファでは、第１の入力信号Ａと、第２の入力信号Ｂとに、常にお互いに反転した信号が与えられることが正常動作の前提条件となっている。
【０１１０】
【表３】
2010140104.tif 000005
【０１１１】
表３は、差動バッファの正常動作の前提条件を表現した真理値表である。部分的に見れば、Ｙ＝Ａとも、Ｙ＝Ｎｏｔ（Ｂ）とも表現出来そうであるが、Ａ＝Ｂの場合にはＹの値が未確定値「Ｘ」となっている。
【０１１２】
この真理値表には、出力信号Ｙが不確定値「Ｘ」となる状態が含まれている。そのため、例えばＹ＝Ａ×Ｂのような、単純な論理式で表現することが出来ない。一部のライブラリでは、その論理モデルを表現するにあたって、単純な論理式しか用いることが出来ない。したがって、このようなライブラリでは、論理を正確に記述することが出来ない。この問題を回避するために、論理モデルをブラックボックスとして表現することによってライブラリ化を実現する。
【０１１３】
したがって、図７の例のように複雑な論理を持つブロックに対して、入力信号ＡおよびＢの論理を固定する設定を行っても、ライブラリ中に論理式が記述され得ない。つまり、ライブラリ中に出力信号Ｙの論理式を固定することが出来ない。
【０１１４】
図８は、複雑な論理を持つ回路ブロック８の出力信号Ｙに固定値を伝播できないことを説明するための概念図である。
【０１１５】
図７の例における、差動入力バッファのタイミングアークについて説明する。第１のタイミングアークは、第１の入力信号Ａと、出力信号Ｙとに係り、Ｒｉｓｅ−Ｒｉｓｅ（ただし活性化条件は「Ｂ＝０」）と、Ｆａｌｌ−Ｆａｌｌ（ただし活性化条件は「Ｂ＝１」）との組み合わせである。第２のタイミングアークは、第２の入力信号Ｂと、出力信号Ｙとに係り、Ｒｉｓｅ−Ｆａｌｌ（ただし活性化条件は「Ａ＝０」）と、Ｆａｌｌ−Ｒｉｓｅ（ただし活性化条件は「Ａ＝１」）との組み合わせである。
【０１１６】
ここで、第１の入力信号Ａの論理値と、第２の入力信号Ｂの論理値とを、それぞれ固定したケースについて考える。
【０１１７】
第１のケースとして、第１の入力信号Ａ＝０、第２の入力信号Ｂ＝１で論理が固定された場合について説明する。この場合は、次のような処理を行う。
【０１１８】
第１の工程として、表１を参照すると、第１のタイミングアークが、第１の竜力信号Ａをそのまま出力信号Ｙとするバッファ動作であることが判定される。ここで、第１の入力信号Ａ＝０で論理が固定されているので、出力信号Ｙ＝０と推定される。
【０１１９】
第２の工程として、第１の工程と同様に表１を参照すると、第２のタイミングアークが、第２の出力信号Ｂを反転して出力信号Ｙとするインバータ動作であることが判定される。ここで、第２の入力信号Ｂ＝１と固定されているので、出力信号Ｙ＝０と推定される。
【０１２０】
第３の工程として、第１の工程の結果と、第２の工程の結果とのいずれの場合でも出力信号Ｙ＝０と推定されているので、出力信号Ｙ＝０で論理を固定する。
【０１２１】
第２のケースとして、第１の入力信号Ａ＝１、第２の入力信号Ｂ＝１で論理が固定された場合について説明する。この場合は、次のような処理を行う。
【０１２２】
第１の工程として、表１を参照すると、第１のタイミングアークが、第１の竜力信号Ａをそのまま出力信号Ｙとするバッファ動作であることが判定される。ここで、第１の入力信号Ａ＝１で論理が固定されているので、出力信号Ｙ＝１と推定される。
【０１２３】
第２の工程として、第１の工程と同様に表１を参照すると、第２のタイミングアークが、第２の出力信号Ｂを反転して出力信号Ｙとするインバータ動作であることが判定される。ここで、第２の入力信号Ｂ＝１と固定されているので、出力信号Ｙ＝０と推定される。
【０１２４】
第３の工程として、第１の工程の結果と、第２の工程の結果とで出力信号Ｙの推定値が食い違っているので、両タイミングアークの活性化条件を確認する。
【０１２５】
第１のタイミングアークにおいて、第１の入力信号Ａ＝１に論理が固定されているので、これはＲｉｓｅ−Ｒｉｓｅの状態に対応する。Ｒｉｓｅ−Ｒｉｓｅの活性化条件は「第２の入力信号Ｂ＝０」だが、このケースでは第２の入力信号Ｂ＝１で論理が固定されているので、活性化条件が満たされていない。
【０１２６】
第２のタイミングアークにおいて、第２の入力信号Ｂ＝１に論理が固定されているので、これはＲｉｓｅ−Ｆａｌｌの状態に対応する。Ｒｉｓｅ−Ｆａｌｌの活性化条件は「第１の入力信号Ａ＝０」だが、このケースでは第１の入力信号Ａ＝１で論理が固定されているので、活性化条件が満たされていない。
【０１２７】
このケースでは、両タイミングアークにおける活性化条件がどちらとも満たされていない。したがって、第１の工程の推定結果も、第２の工程の推定結果も、どちらとも有効ではないと判定される。結果的に、出力信号Ｙの論理は固定されない。
【０１２８】
その他のケースについても同様であるので、詳細な説明を省略する。各ケースについて出力信号Ｙの論理値をまとめると、次のような表が得られる。
【０１２９】
【表４】
2010140104.tif 000006
【０１３０】
表４は、図７の論理ブロックについて本発明の回路検証方法を行った結果得られた出力信号Ｙの論理をまとめた表である。表４において、実際の真理値表である表３と同じ内容が得られていることが確認出来る。
【０１３１】
（第６の実施例）
一般的に、回路の論理シミュレーションを行う場合、使用する論理モデルをライブラリで記述する際、かなり自由な記述が出来る。このため、ほとんど全ての論理回路ブロックについて正確な論理を記述することが可能であり、また、これらの正確な記述に基づいたシミュレーションを行うことが可能である。
【０１３２】
これに対して、論理等価性検証やＳＴＡ（Ｓｔａｔｉｃ  Ｔｉｍｉｎｇ  Ａｎａｌｙｓｉｓ：静的タイミング解析）のような、静的な検証ツールや論理合成で使用する論理モデルについては、論理回路ブロックの動作仕様によっては、その正確な論理を表現できない場合が多く存在する。これは、ツールの機能上、または使用するライブラリの仕様上、単純な論理式による表現しか扱うことが出来ないためである。
【０１３３】
このように、論理を正確に表現できない論理回路ブロックについては、その論理を不正確に記述をしてしまうと、論理合成や各種検証が正しく行えなくなる。そこで、このような論理回路ブロックは、論理情報を一切記述しないブラックボックスとしてライブラリ化が行われる。
【０１３４】
図９は、本発明の第６の実施例による回路検証方法について説明するために用いる回路の論理モデル９の概略図である。図９の論理モデル９は、ＩＯバッファを示している。
【０１３５】
このＩＯバッファの論理モデル９は、第１の論理回路９１と、第２の論理回路９２と、第１の入力部９１１（Ａ）と、第２の入力部９１２（ＯＥＮ）と、第３の入力部９２２（ＣＴＬ）と、第４の入力部９３（ＵＤＣ０）と、第５の入力部９４（ＵＤＣ１）と、第６の入力部９５（Ｃ０）と、第７の入力部９６（Ｃ１）と、第１の出力部９７（Ｙ０）と、第２の出力部９２３（Ｙ１）と、第３の出力部９８（ＣＴＲＳＴＢＹＢ）とを具備する。
【０１３６】
第１の入力部９１１は、第１の論理回路９１１における第１の入力部に接続されている。第２の入力部９１２は、第１の論理回路９１１における第１の入力部に接続されている。第１の出力部９７は、第１の論理回路９１１における出力部９９に接続されている。
【０１３７】
第１の論理回路９１における接続部９９は、第２の論理回路９２における第１の入力部９２１に接続されている。第３の入力部９２２は、第２の論理回路９２における第２の入力部に接続されている。第２の出力部９２３は、第２の論理回路９２における出力部に接続されている。
【０１３８】
このＩＯバッファ９の場合、破線で囲まれた部分、すなわち、第１の論理回路９１と、第２の論理回路９２とに係る部分のみを考えれば、正確な論理を記述することが可能である。しかし、このＩＯバッファ９における破線の外の部分には他の入出力部があり、これらの動作については単純な論理式を定義出来ない。
【０１３９】
例えば、第４の入力部９３（ＵＤＣ０）と、第５の入力部９４（ＵＤＣ１）とは、ＩＯバッファ９においてＰＵ（Ｐｕｌｌ  Ｕｐ）抵抗とＰＤ（Ｐｕｌｌ  Ｄｏｗｎ）抵抗とを切り替えるための端子として動作する。
【０１４０】
【表５】
2010140104.tif 000007
【０１４１】
表５は、第４の入力部９３（ＵＤＣ０）と、第５の入力部９４（ＵＤＣ１）とに係る真理値表である。
【０１４２】
ここで、論理シミュレータ用のライブラリであれば、表５の真理値表を正確に記述することが可能である。しかし、論理合成、ＳＴＡおよび論理等価性検証で使用するライブラリでは、Ｐｕｌｌ  ＵｐおよびＰｕｌｌ  Ｄｏｗｎを表現する方法が無いため、正確な論理を記述出来ない。
【０１４３】
このため、図９のようなＩＯバッファ９については、ライブラリ上で論理を定義せずに、ブラックボックスのライブラリが提供される。
次に、図９のＩＯバッファ９が別の回路の中で使用された場合について説明する。
【０１４４】
図１０は、本発明の第６の実施例による回路検証方法について説明するために用いる回路の論理モデル９およびＭＵＸ回路１０の概略図である。図１０の回路は、図９のＩＯバッファ９を、ＭＵＸ回路１０に接続したものに等しい。
【０１４５】
ＭＵＸ回路１０は、第１の入力部１０１（ＭＯＤＥ１）と、第２の入力部１０２（ＭＯＤＥ２）と、第３の入力部９２３と、出力部１０３（ＭＵＸＯＵＴ）とを具備する。
【０１４６】
ＩＯバッファ回路９における第２の出力部９２３（Ｙ１）が、ＭＵＸ回路１０の第３の入力部９２３に接続されている。
【０１４７】
図１０の回路におけるその他の構成要素および接続関係は、図９と同じであるので、詳細な説明を省略する。
【０１４８】
図１０の回路では、ＩＯバッファ９の出力信号Ｙ１によってＭＵＸ回路１０を制御する。ＭＵＸ回路１０は、出力信号Ｙ１に制御されて、第１の入力信号ＭＯＤＥ１、または、第２の入力信号ＭＯＤＥ２のいずれかの値を、出力信号ＭＵＸＯＵＴに伝播する。
【０１４９】
図１０の回路において、第１の出力部９７に信号Ｙ０として「０」を外部から供給した場合、信号ＭＯＤＥ１の値が信号ＭＵＸＯＵＴまで伝播することである。しかし、ＩＯバッファ９がブラックボックスであった場合は、信号Ｙ０が信号Ｙ１に伝播することは無い。したがって、信号ＭＵＸＯＵＴに信号ＭＯＤＥ１が伝播したとしても、このことを図１０の回路は認識出来ない。
【０１５０】
このことにより、例えば、信号ＭＯＤＥ２は本来使用されないのに、この信号ＭＯＤＥ２に対する不要な検証や論理検証が行われる結果、擬似エラーの発生要因となる。
【０１５１】
この対策として、ＩＯバッファ回路９の出力部９２３の信号Ｙ１として設計者が期待する値（この場合は「０」）を設定する方法がよく行われている。しかし、信号ＣＴＬや信号ＯＥＮが誤った値に固定されていた場合や、信号Ｙ０の値を変更した場合には、実際とは異なる状態をＩＯバッファ回路９内に設定していることになる。このため、設計者の意図しない検証が行われてしまう、という問題がある。
【０１５２】
ここで、本発明を用いれば、論理情報が無くても、タイミングアークさえあれば、第２の出力端子９２３の信号Ｙ１へ固定値を論理伝播することが可能となる。
【０１５３】
ＩＯバッファ回路９は、以下の４つのタイミングアークを具備する。第１のタイミングアークは、入力信号Ｙ０と、出力信号Ｙ１とに係り、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌと、活性化条件「ＣＴＬ＝１」との組み合わせである。第２のタイミングアークは、入力信号ＣＴＬと、出力信号Ｙ１とに係り、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌと、活性化条件「Ｙ０＝１」との組み合わせである。第３のタイミングアークは、入力信号Ａと出力信号Ｙ０とに係り、Ｒｉｓｅ−Ｒｉｓｅと、Ｆａｌｌ−Ｆａｌｌとの組み合わせである。第４のタイミングアークは、入力信号ＯＥＮと、出力信号Ｙ０とに係り、Ｒｉｓｅ−ＺＨと、Ｒｉｓｅ−ＺＬと、Ｆａｌｌ−ＨＺと、Ｆａｌｌ−ＬＺとの組み合わせである。
【０１５４】
ＩＯバッファ回路９は、以下の３つの制約条件をさらに具備する。第１の制約条件は、「Ｙ０＝０」である。第２の制約条件は、「ＯＥＮ＝０」である。第３の制約条件は、「ＣＴＬ＝１」である。
【０１５５】
論理伝播の第１〜第４のステップについて説明する。第１のステップとして、第４のタイミングアークから、ＯＥＮ＝０のとき、トライステート部のイネーブルがＯｆｆになると判定されて、トライステート部の出力にＨｉＺが設定される。この詳細については、第３の実施例で説明したとおりであるので、更なる説明は省略する。
【０１５６】
第２のステップとして、Ｙ０（＝０）と、トライステート部の出力（＝ＨｉＺ）のｗｉｒｄ演算を行う。この処理は、本発明とは関係無く、従来技術と同様の、通常のツールの演算処理である。ｗｉｒｄ部の論理として０が得られる。
【０１５７】
第３のステップとして、第１のタイミングアークと、第２のタイミングアークとに基づいて、Ｙ１への固定値伝播を以下のように処理する。
【０１５８】
第３のステップにおける第１のサブステップとして、第１のタイミングアークと、第３の制約条件と、第１の制約条件とから、Ｙ１の値は０に固定される。
【０１５９】
第３のステップにおける第２のサブステップとして、第２のタイミングアークと、第３の制約条件とから、Ｙ１の値は１に固定される。
【０１６０】
第３のステップにおける第３のサブステップとして、第１のサブステップによる結果と、第２のサブステップによる結果とが異なるため、活性化条件をチェックする。ここで、第１の制約条件「Ｙ０＝０」が、第２のタイミングアークの活性化条件「Ｙ０＝１」を満たさないため、第２のタイミングアークは活性化されない。反対に、第３の制約条件「ＣＴＬ＝１」が、第１のタイミングアークの活性化条件「ＣＴＬ＝１」を満たすため、第１のタイミングアークは活性化される。したがって、出力信号Ｙ１には第３のステップにおける第１のサブステップによる結果である「０」が伝播される。この処理方法については第２の実施例で詳細に説明したので、更なる説明を省略する。
【０１６１】
第４のステップとして、Ｙ１＝０としてＭＵＸ回路１０のセレクタ信号として「０」が伝播される。
【０１６２】
以上に説明したように、本発明の回路検証方法では、ブラックボックスについて、論理情報だけではなく、タイミング情報も考慮して固定値を伝播させるため、以下の効果が得られる。まず、回路中に必要な固定値を伝播できるので、不要な検証を行わなくなり、擬似エラーの防止や実行ＴＡＴが短縮される。また、ブラックボックスの入力側の制約を変更しても、その変更を考慮した固定値伝播が行えるため、設計者の手作業による誤りを未然に防止し、後戻りの工数などを削減できる。
【０１６３】
本発明による回路検証プログラムは、これまで説明した回路検証方法の各ステップを、計算機上で実行可能に構成したものである。
【図面の簡単な説明】
【０１６４】
【図１】図１は、従来技術における回路検証方法について説明するためのフローチャートである。
【図２】図２は、本発明の実施形態における回路検証方法について説明するためのフローチャートである。
【図３】図３は、１入力１出力のブラックボックス回路について説明するための概略図である。
【図４】図４は、２入力１出力のブラックボックス回路について説明するための概略図である。
【図５】図５は、ＨｉＺ状態への遷移を含むタイミングアークを有するブラックボックス回路について説明するための概略図である。
【図６】図６は、クロック属性端子を含むブラックボックス回路について説明するための概略図である。
【図７】図７は、差動入力バッファ回路について説明するための概略図である。
【図８】図８は、複雑な論理を持つ回路ブロックの出力信号Ｙに固定値を伝播できないことを説明するための概念図である。
【図９】図９は、本発明の第６の実施例による回路検証方法について説明するために用いる回路の論理モデルの概略図である。
【図１０】図１０は、本発明の第６の実施例による回路検証方法について説明するために用いる回路の論理モデルおよびＭＵＸ回路の概略図である。
【図１１】図１１は、本発明による回路検証装置の構成を説明するためのブロック図である。
【図１２】図１２は、本発明による回路検証装置の構成を機能ブロックで説明するためのブロック図である。
【符号の説明】
【０１６５】
３  １入力１出力のブラックボックス回路
３１  入力部
３２  出力部
４  ２入力１出力のブラックボックス回路
４１  第１の入力部
４２  第２の入力部
４３  出力部
５  ＨｉＺ状態への遷移を含むタイミングアークを有するブラックボックス回路
５１  第１の入力部
５２  第２の入力部
５３  出力部
６  クロック属性端子を含むブラックボックス回路
６１  第１の入力部
６２  第２の入力部
６３  出力部
７  差動入力バッファ回路
７１  第１の入力部
７２  第２の入力部
７３  出力部
８  複雑な論理を持つ回路ブロック
８１  第１の入力部
８２  第２の入力部
８３  出力部
９  ＩＯバッファ回路
９１  第１の論理回路
９１１  第１の入力部
９１２  第２の入力部
９２  第２の論理回路
９２１  第２の論理回路における第１の入力部
９２２  第３の入力部
９２３  第２の出力部
９３  第４の入力部
９４  第５の入力部
９５  第６の入力部
９６  第７の入力部
９７  第１の出力部
９８  第３の出力部
９９  接続部
１０  ＭＵＸ回路
１０１  ＭＵＸ回路の第１の入力部
１０２  ＭＵＸ回路の第２の入力部
１０３  ＭＵＸ回路の出力部
１１  回路検証装置
１１１  入力部
１１２  演算部
１１３  記憶部
１１３１  プログラム記憶部
１１３２  デザイン記憶部
１１３３  ライブラリセル
１１３４  論理情報記憶部
１１３５  タイミング情報記憶部
１１４  出力部
１２  記憶演算部
１２１  論理固定値設定部
１２２  次段回路ブロック選択部
１２３  ライブラリ判定部
１２４  論理情報伝達部
１２５  タイミング情報伝達部
１２６  伝播完了判定部
１２７  検証実行部
【図１】
2010140104.tif 000008
【図２】
2010140104.tif 000009
【図３】
2010140104.tif 000010
【図４】
2010140104.tif 000011
【図５】
2010140104.tif 000012
【図６】
2010140104.tif 000013
【図７】
2010140104.tif 000014
【図８】
2010140104.tif 000015
【図９】
2010140104.tif 000016
【図１０】
2010140104.tif 000017
【図１１】
2010140104.tif 000018
【図１２】
2010140104.tif 000019