(57)【特許請求の範囲】
【請求項１】
回路の論理検証装置であって、
素子の種類毎に、入出力端子間の論理反転経路と、出力端子が固定出力となる入力端子の条件である発振停止条件とが記憶された論理反転経路発振停止条件記憶手段と、
検証対象とする回路に含まれるループ回路を探知するループ検出手段と、
前記探知されたループ回路のループ経路に含まれる素子毎に、前記論理反転経路発振停止条件記憶手段を参照し、ループ経路における当該素子の入力端子と出力端子の接続が前記論理反転経路に該当するか否かを検出し、ループ経路に含まれる論理反転経路の数を計数し、前記ループ回路が正帰還ループであるか負帰還ループであるかを判定する正・負帰還チェック手段と、
前記正・負帰還チェック手段が負帰還ループであると判定した場合に、前記ループ回路のループ経路に含まれる素子毎に、前記論理反転経路発振停止条件記憶手段を参照し、当該素子の入力端子のうちループ経路に含まれない入力端子が前記発振停止条件を満たす場合にはそのループ回路について問題なしと判定し、入力端子の条件によっては前記発振停止条件を満たす場合はその条件を明示するループ外入力チェック手段と、を備え、
前記回路の構成が発振ループ構成となっているかどうかの判定結果、及び発振状態を回避するための条件を明示するようにしたことを特徴とする論理検証装置。
【請求項２】
前記ループ回路のループ経路に含まれる素子に排他的論理和または排他的否定論理和が存在するか否かを検出し、検出された場合には、当該素子のループ経路に含まれない入力端子の入力値を前段に遡ってトレースし、その入力端子の入力がクランプされておりそのクランプされている入力値によって、その排他的論理和または排他的否定論理和をインバータまたはノンインバータに縮退できる場合には縮退する排他論理処理手段をさらに備え、
前記排他論理処理手段が前記縮退を行った場合には、縮退したループ回路について、
前記正・負帰還チェック手段、ループ外入力チェック手段による判定を行うことを特徴とする請求項１記載の論理検証装置。
【請求項３】
前記排他論理処理手段が、排他的論理和または排他的否定論理和について、当該素子のループ経路に含まれない入力端子の入力値をトレースした結果、その入力端子の入力が不確定な場合は、前記正・負帰還チェック手段による判定を行わず、前記ループ外入力チェック手段により、前記排他的論理和または排他的否定論理和以外の素子について判定を行うことを特徴とする請求項２記載の論理検証装置。
【請求項４】
前記排他論理処理手段による入力端子の入力値トレースは、当該入力端子が別の小ループに含まれる場合に、入力値トレースを中止し、入力値を不確定として処理する入力値トレースであることを特徴とする請求項３記載の論理検証装置。
【請求項５】
前記ループ外入力チェック手段が、前記ループ経路に含まれない入力端子の入力値を前段に遡ってトレースし、そのトレースされた入力値によって、前記発振停止条件を満たすか否か判定をすることを特徴とする請求項１乃至３いずれか１項記載の論理検証装置。
【請求項６】
前記ループ外入力チェック手段による入力端子の入力値トレースは、当該入力端子が別の小ループに含まれる場合に、入力値トレースを中止し、入力値を不確定として処理する入力値トレースであることを特徴とする請求項５記載の論理検証装置。
【請求項７】
前記ループ外入力チェック手段による入力端子の入力値トレースは、前段に遡ってトレースした結果、順序回路、入出力回路の折返し、アダー、パリティジェネレータの全端子接続と、ラッチとマルチプレクサとデコーダとのイネーブル部分の端子接続の出力論理に接続されている場合は、入力値を不確定として扱うことを特徴とする請求項５または６記載の論理検証装置。
【請求項８】
前記ループ外入力チェック手段による入力端子の入力値トレースは、任意の指定した段数遡っても値の確定または不確定が決まらない場合は、前記入力値を不確定として扱うことを特徴とする請求項５乃至７いずれか１項記載の論理検証装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明はループ回路における発振構成箇所の検出方法に係わり、特に半導体装置の中でも特定用途向けＩＣであるＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  ＩＣ）または複合ＩＣであるＳＯＣ（Ｓｙｓｔｅｍ  Ｏｎ  Ｃｈｉｐ）などでは、ある特定の目的のために種々の回路を構成する場合が多いため、論理ゲートによる負帰還ループを作り込む危険性が高い。そのため、負帰還ループがチップに作り込まれる前に予め検出するように改善したループ回路における発振構成箇所の検出方法に関する。
【０００２】
【従来の技術】
近年、半導体素子の微細化技術の進展に伴い、その半導体素子で構成するＬＳＩも大規模化し、半導体メモリ、マイクロコンピュータ、あるいはこれらのＬＳＩを１チップに搭載した複合ＬＳＩであるＳＯＣも大容量化してきている。この大容量化とともにその回路機能も複雑化し、設計段階における回路検証の精度向上が重要な課題の一つである。
【０００３】
これらのＬＳＩの内部回路において論理ゲートによるループ回路として正帰還ループまたは負帰還ループが存在するが、特に負帰還ループが存在すると実機では論理回路が発振→中間電圧となり、リーク電流が発生する原因となる。
【０００４】
そうした不具合の原因となる負帰還ループは、例えば外販ＡＳＩＣのように、小規模（ゲート数にして１００Ｋ以下）設計が主流で、かつ回路設計に人手が入ることが多いＬＳＩでは、意図的に作り込まれない限り内部回路内に作り込まれることはなかった。
【０００５】
しかし、近年設計が大規模化しており、回路設計でも論理合成ツール等を用いた自動設計手法を用いることが多くなったことにより、意識せずに作り込まれてしまうといった例が発生する様になってきた。
【０００６】
回路規模は今後も更に増えていく傾向にあり、今後ますますこうしたこと例は増えていくと考えられる。
【０００７】
【発明が解決しようとする課題】
上述したような従来の例えばＡＳＩＣやＳＯＣでは、そうした設計環境の変化にあっても、発振ループ個所を特に検出する仕組みは、今のところまだ開発されていないが、例えば、論理推移から発振か否かの判定を論理シミュレーションを用いて検証する方法の一例が特願平１−１９３６６８号公報に記載されている。
【０００８】
同公報記載の検証方法を参照すると、特定時刻ｔ〜ｔ＋Δｔにおける論理推移から発振か否かを判定しているが、回路構成によっては、ループ内に初期値を入れることが出来ず、論理シミュレーション上では時刻ｔにおいてもその少し後のｔ＋Δｔにおいても内部論理は不定〜不定で、論理推移を見ることが出来なくなり判定が出来ない。
【０００９】
例えば、上述した従来の検証方法の説明用回路例を示した図１２を参照すると、この回路は、ＮＡＮＤ１２ａ→ＡＮＤ１２ｂ→ＮＡＮＤ１２ａのループを一つ有し、入力端子ＢはＨＩＧＨ＿ＣＬＡＭＰ（“１”でクランプ）１２ｃにより論理レベルの“１”にクランプされているので、論理シミュレーション上ではＮＡＮＤ１２ａの出力は最初から不確定であり、これは時刻がいくら進んでも不確定の反転は不確定である。
【００１０】
したがって、シミュレーション結果の波形図を示した図１３の様に、時刻ｔ＝０における入力ＡがＸのため、それ以降の出力Ｙ→入力Ａ間はＸが周回し続けることになり、最初（時刻ｔ＝０）から最後まで不確定Ｘが流れるような形になっていまい、発振しているのかどうかがわからない。
【００１１】
しかし、実機上でのＮＡＮＤ１２ａの入出力波形を示した図１４を参照すると、論理レベルのＨＩＧＨ（＝１）／ＬＯＷ（＝０）の値を繰り返しつつ次第に中間電圧付近に安定していくので、貫通電流が流れる原因となってしまう。
【００１２】
また、論理シミュレータを用いる方法では、検出の可否はＶＥＣＴＯＲの質に大きく左右されてしまうが、回路規模が大きい程、内部ノード全てをトグルさせるＶＥＣＴＯＲの作成は困難であり、実際には対応が難しくなってきているのが現状である。
【００１３】
本発明の目的は、上述した従来の欠点に鑑みなされたものであり、論理ゲート一つ一つに対する特定ルールに基づいた情報を備えたライブラリを用意することで、回路そのものに対して発振ループ回路の検出、検証を行う検証方法を提供することにある。
【００１４】
【課題を解決するための手段】
本発明の論理検証装置は、回路の論理検証装置であって、素子の種類毎に、入出力端子間の論理反転経路と、出力端子が固定出力となる入力端子の条件である発振停止条件とが記憶された論理反転経路発振停止条件記憶手段と、検証対象とする回路に含まれるループ回路を探知するループ検出手段と、前記探知されたループ回路のループ経路に含まれる素子毎に、前記論理反転経路発振停止条件記憶手段を参照し、ループ経路における当該素子の入力端子と出力端子の接続が前記論理反転経路に該当するか否かを検出し、ループ経路に含まれる論理反転経路の数を計数し、前記ループ回路が正帰還ループであるか負帰還ループであるかを判定する正・負帰還チェック手段と、前記正・負帰還チェック手段が負帰還ループであると判定した場合に、前記ループ回路のループ経路に含まれる素子毎に、前記論理反転経路発振停止条件記憶手段を参照し、当該素子の入力端子のうちループ経路に含まれない入力端子が前記発振停止条件を満たす場合にはそのループ回路について問題なしと判定し、入力端子の条件によっては前記発振停止条件を満たす場合はその条件を明示するループ外入力チェック手段と、を備え、前記回路の構成が発振ループ構成となっているかどうかの判定結果、及び発振状態を回避するための条件を明示するようにしたことを特徴とする。
【００１５】
また、本発明の論理検証装置は、前記ループ回路のループ経路に含まれる素子に排他的論理和または排他的否定論理和が存在するか否かを検出し、検出された場合には、当該素子のループ経路に含まれない入力端子の入力値を前段に遡ってトレースし、その入力端子の入力がクランプされておりそのクランプされている入力値によって、その排他的論理和または排他的否定論理和をインバータまたはノンインバータに縮退できる場合には縮退する排他論理処理手段をさらに備え、前記排他論理処理手段が前記縮退を行った場合には、縮退したループ回路について、前記正・負帰還チェック手段、ループ外入力チェック手段による判定を行うことができる。
【００１６】
さらに、本発明の論理検証装置は、前記排他論理処理手段が、排他的論理和または排他的否定論理和について、当該素子のループ経路に含まれない入力端子の入力値をトレースした結果、その入力端子の入力が不確定な場合は、前記正・負帰還チェック手段による判定を行わず、前記ループ外入力チェック手段により、前記排他的論理和または排他的否定論理和以外の素子について判定を行うこともできる。
【００１７】
さらにまた、本発明の論理検証装置は、前記排他論理処理手段による入力端子の入力値トレースは、当該入力端子が別の小ループに含まれる場合に、入力値トレースを中止し、入力値を不確定として処理する入力値トレースであることもできる。
【００１８】
また、本発明の論理検証装置は、前記ループ外入力チェック手段が、前記ループ経路に含まれない入力端子の入力値を前段に遡ってトレースし、そのトレースされた入力値によって、前記発振停止条件を満たすか否か判定をすることもできる。
【００１９】
さらに、本発明の論理検証装置は、前記ループ外入力チェック手段による入力端子の入力値トレースは、当該入力端子が別の小ループに含まれる場合に、入力値トレースを中止し、入力値を不確定として処理する入力値トレースであることもできる。
【００２０】
さらにまた、本発明の論理検証装置は、前記ループ外入力チェック手段による入力端子の入力値トレースは、前段に遡ってトレースした結果、順序回路、入出力回路の折返し、アダー、パリティジェネレータの全端子接続と、ラッチとマルチプレクサとデコーダとのイネーブル部分の端子接続の出力論理に接続されている場合は、入力値を不確定として扱うこともできる。
【００２１】
また、本発明の論理検証装置は、前記ループ外入力チェック手段による入力端子の入力値トレースは、任意の指定した段数遡っても値の確定または不確定が決まらない場合は、前記入力値を不確定として扱うこともできる。
【００２８】
【発明の実施の形態】
本発明は、論理ゲートによる負帰還のループを特に検出する方法として、禁止情報のデータベース化と、回路ルールチェックの検証システムを構築（論理トレース）することで、リーク電流による不良を無くし、品質の高いチップを供給できるというものである。
【００２９】
まず、本発明の第１の実施形態を図面を参照しながら詳細に説明する。
【００３０】
本発明の第１の実施形態によるループ回路における発振構成箇所の検出方法をフローチャートで示した図１を参照すると、この方法は、論理検証装置（図示せず）に適用され、プログラム制御により動作するループ検出処理Ｓ１と、排他的論理和または排他的否定論理和の処理Ｓ２（後述の図２）と、正・負帰還チェック処理Ｓ３（後述の図３）と、ループ外入力チェック処理Ｓ４（後述の図４）と、回路箇所を明示して問題点を表示するためのディスプレイ処理や印刷処理などの出力処理Ｓ５と、処理Ｓ１と処理Ｓ４からサブルーチンとして起動される“入力段トレース”処理を示す図５の処理が含まれる。さらに、処理Ｓ２および処理Ｓ４の制御に必要な真理値情報１１および専用のライブラリ１２（後述の図６）からなる記憶媒体も含んで構成される。
【００３１】
ループ検出処理Ｓ１は、既にある公知技術を流用してループ個所を探す処理である。すなわち、全ての素子を始点として出力段をトレースしていき、これまでに訪れた素子に戻った場合、その素子をループとして検出する。
【００３２】
探索においては、目的が論理ゲートのみの構成によるループを見つけることであること、また、経験則よりこれらの素子が含まれていた場合発振に至ることは無いことから、特定の素子（下記に記載）への接続は検索対象から外して、他の経路の探索を行う。つまり、その経路はループになっていないと判断する。
【００３３】
検証対象外となるループで接続される特定素子：
順序回路、ＬＡＴＣＨとＭＵＬＴＩＰＬＥＸＥＲとＤＥＣＯＤＥＲとのＥＮＡＢＬＥ部分、Ｉ／Ｏ折返し、ＡＤＤＥＲへの接続。
【００３４】
検証対象となるループで接続される素子：
ＩＮＶＥＲＴＥＲ、ＮＯＮ−ＩＮＶＥＲＴＥＲ、ＯＲ、ＮＯＲ、ＡＮＤ、ＮＡＮＤ、ＸＯＲ、ＸＮＯＲ、複合ゲート、ＬＡＴＣＨとＭＵＬＴＩＰＬＥＸＥＲとＤＥＣＯＤＥＲのデータ部分。
【００３５】
処理３および処理４の実行に必要なライブラリ（図６）内では予め個々の素子に関して、▲１▼論理反転経路▲２▼発振停止条件、の２つの情報が定義されている。論理反転経路は、文字どおり、ループ内での接続経路において、“入出力端子間で論理レベルが極性反転する経路がどこか”を定義したものである。
【００３６】
また、発振停止条件は、“ループ外である他方の入力端子からの入力値がどの値で固定されていれば発振しないか”の情報が定義されている。
【００３７】
処理Ｓ２においては、ＸＯＲ／ＸＮＯＲがある場合の処理を行う。ＸＯＲ／ＸＮＯＲはループ外である他方の入力端子からの入力値によって、その入出力端子間で信号レベルが極性反転するかしないかが変わるため、例外的にループ外である他方の入力端子からの入力を最初にトレースして、ループ外からの入力値が固定されているかどうかを検証する。
【００３８】
そして、ループ外からの入力値の固定が可能なら、これらＸＯＲ／ＸＮＯＲを真理値情報１１に基づいてＩＮＶＥＲＴＥＲもしくはＮＯＮ−ＩＮＶＥＲＴＥＲに置き換える。置き換えられない場合、そのループは正帰還・負帰還の判定（処理３）が出来ないため、他のブロックのループ外入力チェック（処理４）からのみ判定する。
【００３９】
処理Ｓ３においては、ループ内の各素子に対してライブラリ内に貯えられた論理反転経路との照らし合わせを行い、ループ全体で反転経路がいくつ存在するかを計算する。その結果を元にループの正・負帰還を判定する。
【００４０】
判定結果が奇数の場合は負帰還ループ、“０”か偶数の場合は正帰還ループと判定する。正帰還ループの場合は回路的に発振することは無いため、そのループに関しては問題無しと判定する。前述の様に、ＩＮＶＥＲＴＥＲもしくはＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えの出来ないＸＯＲもしくはＸＮＯＲが存在した場合、この処理は行われない。
【００４１】
処理Ｓ４においては、ループ内の各素子がループ外である他方の入力端子からの入力値によって、出力論理が固定される可能性について検証を行う。方法としては、それら素子の前段にあたる素子を検証する。
【００４２】
前段の素子が論理ゲート等であり、クランプまたは外部端子に接続されている時に特定の値で確定すると判定するが、順序回路等、下記に示す素子が前段であった場合は経験則よりその前段素子の出力が固定されることはないため、その接続で値が固定することは無いと判定する。また、それ以外の素子の場合は、さらに前段の素子を検証する。
【００４３】
論理レベルは固定され無いと判定して、それ以上の前段トレースを行わない接続素子：
順序回路、Ｉ／Ｏ折返し、アダー、パリティジェネレータの全接続、ラッチとマルチプレクサとデコーダーのイネーブル部分の接続。
【００４４】
前段トレースの結果、ループ内の素子に対しその素子のループ外である他方の入力端子からの入力値が固定される場合は、ライブラリ内に貯えられた発振停止条件との照らし合わせを行い、そのループ内の素子の出力論理レベルが固定されるかどうかを判定する。外部端子の使用条件によっては固定される、といった場合はその条件も明示する。
【００４５】
厳密にいえば、上述した素子／接続でも前段トレース自体は可能なため、任意に検証をする、しないを選択出来る様にしてもいい。
【００４６】
また、前段トレースにおける段数についても、原則的には確定する、しないが明らかになるまで検証を行うことになっているが、任意にその段数を指定して、その段数以内で値の確定、不確定が決まらない場合は不確定扱いにする仕組みでもよい。
【００４７】
また、入力トレースを終了するもう一つの条件として、既に訪れたことのある素子が出てきた場合がある。こうした場合は構成的に２重ループになっており、そのままでは永遠に廻り続けるため、そのループについてはカットする。
【００４８】
出力処理Ｓ５において問題無しと判定するに足る十分な確証が得られなかった場合に、どの素子がループ構成になっているかの情報を外部の表示手段に明示して、このループに関する検証を終了する。
【００４９】
明示にあたっては、個々の素子に対して回路データ内で与えられるユニークな名前を用いて、どの接続が実機上で発振する可能性のあるループになっているかを具体的に示す。
【００５０】
最後に処理Ｓ６で、ループ検出処理Ｓ１で検出したループ全てを検出したかどうかを確認する。
【００５１】
次に、上述した個々処理に関する詳しい説明、条件、実施理由と、本発明の検証方法の全体のフロチャートを示した図１と、それぞれの処理の詳細なフロチャートを示した図２〜図５とを併せて参照しながら実施形態を具体的に説明する。
【００５２】
まず、図１内の処理について説明する。処理Ｓ１の“ループ構成を見つける”では、ループ個所を探す。処理Ｓ１が終わったら処理Ｓ２に移る。ループを見つけるアルゴリズムや、その条件については前述した内容の通りである。
【００５３】
処理Ｓ２“ＸＯＲ／ＸＮＯＲの処理”においては、処理Ｓ１で検出されたループ内にＸＯＲ／ＸＮＯＲがある場合ＩＮＶＥＲＴＥＲ／ＮＯＮ−ＩＮＶＥＲＴＥＲに置き換える試みを行う。ＸＯＲ／ＸＮＯＲがあり、かつ置き換えが出来なかった場合、処理Ｓ３は行われず処理Ｓ４に移る。それ以外は処理Ｓ３に移る。
【００５４】
処理Ｓ３“正・負帰還チェック”では処理Ｓ１で発見され、場合によっては処理Ｓ２でＸＯＲ／ＸＮＯＲが他のブロックに置き換えられたループが正帰還ループか負帰還ループかを判定する。
【００５５】
正帰還ループの場合、そのループの検証は終了して処理Ｓ６へ移る。負帰還ループの場合は処理Ｓ４に移る。その判定には“専用ライブラリ”に記述されている“論理反転経路”がループ内の接続にいくつ用いられているかを検証することで行われる。
【００５６】
処理Ｓ４“ループ外入力チェック”は、処理Ｓ３で負帰還ループと判定された場合か、処理Ｓ２でＸＯＲ／ＸＮＯＲ全てを置き換え出来なかった場合に行われる処理である。
【００５７】
処理Ｓ１で検出されたループ、あるいは処理Ｓ２でＸＯＲ／ＸＮＯＲが他の素子に置き換えられたループ内の各素子（ＸＯＲ／ＸＮＯＲは除く）に対してループ外である他方の入力端子からの入力値によって出力が固定されるかどうかを判定する。
【００５８】
その結果、ループ外の入力がクランプで固定されており、“専用ライブラリ”内で定義されている“発振停止条件”と照らし合わせた時に普遍的に発振することが無い場合は、このループの検証は終了して処理Ｓ６へ移る。それ以外の場合、つまり、条件付きＯＫ，あるいは問題有りの場合は処理Ｓ５へ移る。
【００５９】
処理Ｓ５“回路個所を明示して問題点を表示”は処理Ｓ４の結果として、普遍的に発振しないという確証が得られなかった場合に行われる。具体的には、処理Ｓ４で検証されたループがループ外である他方の入力端子からの入力値によって、発振停止される確証が得られない場合と、外部端子の使い方によっては発振停止される場合を含む。後者の場合は外部端子の使い方条件についてもここで表示する。この処理が終わると処理Ｓ６に移る。
【００６０】
処理Ｓ６“他のループがあるか？”では、回路内に検証すべき他のループがあるかを確認する。ある場合は再び処理Ｓ２へ移り、一連の検証が行われる。無い場合はそのまま終了する。
【００６１】
次に、処理Ｓ１でのループ発見後に必ず行われるフロー、すなわち、図１内における処理Ｓ２“ＸＯＲ／ＸＮＯＲの処理”の詳細な検証方法を示した図２の処理について説明をする。なお、図１内の処理Ｓ１およびび処理Ｓ６については公知技術なので特にここでの詳細な動作説明は省略する。
【００６２】
処理Ｓ２ａ“ＸＯＲ／ＸＮＯＲの有無”は、処理Ｓ１で発見されたループ内にＸＯＲ／ＸＮＯＲが含まれるかをチェックする。一つでも含まれる場合は処理Ｓ２ｂへ、そうでない場合は即図１でいうところの処理Ｓ３へ移る。
【００６３】
処理Ｓ２ｂ“入力段トレース”は、処理Ｓ２ａで発見されたＸＯＲ／ＸＮＯＲでまだ検証のされていないものを一つ選択して、その素子に対するループ外である他方の入力端子からの入力値が固定されているかどうかを検証する。
【００６４】
この“入力段トレース”部分の動作については、さらに詳細な検証方法を示した図５があり、この処理については後述する。図５に示す処理を実行の結果、返り値を得たら処理Ｓ２ｃへ移る。
【００６５】
処理Ｓ２ｃ“（ＮＯＮ−）ＩＮＶＥＲＴＥＲに置き換え可？”は、処理Ｓ２ｂで前段トレースを行ったＸＯＲ／ＸＮＯＲをＩＮＶＥＲＴＥＲ／ＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えることが可能かどうかを判定する。
【００６６】
具体的には、処理Ｓ２ｂで検証したＸＯＲ／ＸＮＯＲに入力される、ループ外である他方の入力端子からの入力値が“１”ならＩＮＶＥＲＴＥＲに置き換えが可能、“０”ならＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えが可能、と判断して処理Ｓ２ｄへ移る。
【００６７】
それ以外（不定）の場合は、置き換え不可と判断して、図１でいう所の処理Ｓ４へ一気に移動する。これは複数のＸＯＲ／ＸＮＯＲがある場合に一つでも置き換え不可のものがあれば図１でいう所の処理４へ移動するものである。
【００６８】
処理Ｓ２ｄ“置き換えを実行”は、処理Ｓ２ｃの判定結果を受けて、処理Ｓ２ｃで判定をおこなったＸＯＲ／ＸＮＯＲをＩＮＶＥＲＴＥＲ／ＮＯＮ−ＩＮＶＥＲＴＥＲに置き換える。
【００６９】
この後、処理Ｓ２ｅへ移る。処理Ｓ２ｅ“他にもＸＯＲ／ＸＮＯＲはあるか？”では、処理Ｓ２ａで発見されたＸＯＲ／ＸＮＯＲが他にある場合は、それを対象に再び処理Ｓ２ｂから処理を行う。無ければ図１に示す処理Ｓ３に移動する。
【００７０】
次に、図１における処理Ｓ３について、その詳細な検証方法を記載した図３を参照しながら説明する。この処理は、処理Ｓ２でのＸＯＲ／ＸＮＯＲ検証の結果、処理Ｓ１で検出したループ内にＸＯＲ／ＸＮＯＲが存在しない場合、もしくは、ＸＯＲ／ＸＮＯＲが存在するが全てＩＮＶＥＲＴＥＲ／ＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えが可能だった場合に行われ、内容としてはそのループが正帰還ループか、負帰還ループかの判定を行う。
【００７１】
処理Ｓ３ａ“始点を決める”では、処理Ｓ１で発見して、場合によっては処理２で一部変換されたループ内の任意の素子を検証素子として選択する。最終的にはＳすべての素子を同じ条件で検証することになるので、この選択方法は任意で問題無い。選択したら処理Ｓ３ｂへ移る。
【００７２】
処理Ｓ３ｂ“反転経路通る？”では、現在検証している素子のループ内における入出力端子間において、入力および出力信号の極性が反転するかどうかを検証する。
【００７３】
現在検証している素子は処理Ｓ３ａで最初に選択された素子か、後述する処理Ｓ３ｄで新たに検証素子として選択された素子が対象となる。検証の方法はライブラリ（図６）内で定義されている“論理反転経路”の接続がループ内にあれば、反転経路を通っているとして、処理Ｓ３ｃに移動する。そうでない場合は処理Ｓ３ｄに移動する。
【００７４】
処理Ｓ３ｃ“反転数＋１”は、処理Ｓ３ｂの検証の結果、検証している素子のループ内における入出力端子間において、入力および出力信号の極性が反転する場合に行われる。
【００７５】
内部的に反転数を１増加する。内部記憶は処理Ｓ３を終了した時にクリアされるが、それまでは保持される。この処理終了後は処理Ｓ３ｄへ移る。
【００７６】
処理Ｓ３ｄ“次段へ”では、検証している素子を他の素子に移す。具体的には後段の素子を新たに検証する素子として選択する。この処理の次の処理Ｓ３ｅへ移る。
【００７７】
処理Ｓ３ｅ“始点に戻ったか？”では、処理Ｓ３ｄの実行結果、検証する素子として選択された素子が処理Ｓ３ａで選択されたものと同じかどうかを判定する。
【００７８】
選択された素子が同一の場合は、ループ内の全ての素子に対して検証したことになるので、処理Ｓ３ｆへ移る。同一でなければ、処理Ｓ３ｂに戻り同様の検証を行う。
【００７９】
処理Ｓ３ｆ“判定”では、処理Ｓ３ｂ〜Ｓ３ｅまでの結果として内部的に記憶された反転数が偶数か奇数かで行う。偶数の場合は正帰還ループと判断して、次の移り先としては図１の中でいう所の処理Ｓ５となる。
【００８０】
反対に奇数の場合は図１の中でいう処理Ｓ４になる。どちらに移動するとしても、内部記憶として保持されていた反転数はここで一度クリアされることとなる。
【００８１】
次に、図１における処理Ｓ４について、その詳細な検証方法のフローチャートを示した図４を参照しながら説明する。
【００８２】
この処理は、処理Ｓ３ｃで検証した正・負帰還チェックの結果、負帰還ループと検証された場合、および処理Ｓ２ｂのＸＯＲ／ＸＮＯＲ検証の結果、処理Ｓ１で検出したループ内のＸＯＲ／ＸＮＯＲ全てを他の素子に置き換えることが出来なかった場合に行われる。
【００８３】
内容としては、処理Ｓ１で検出され、場合によっては処理Ｓ２でＸＯＲ／ＸＮＯＲが他の素子に置き換えられたループ内の全ての素子に対して、ループ外である他方の入力端子からの入力信号により出力値が固定されるかどうかを検証する。
【００８４】
処理Ｓ４ａ“始点決める”では、処理Ｓ１で検出され、場合によっては処理Ｓ２でＸＯＲ／ＸＮＯＲが他の素子に置き換えられたループ内の全ての素子を検証するにあたって、任意の素子を最初に検証する素子として選択する。
【００８５】
最終的には全ての素子を検証することとなるため、この素子の選択は任意で問題無い。この処理の後、処理Ｓ４ｂへ移る。
【００８６】
処理Ｓ４ｂ“ＸＯＲ／ＸＮＯＲ？”では、現在検証している素子がＸＯＲ／ＸＮＯＲかどうかを判定する。現在検証している素子とは、処理Ｓ４ａで最初に選択されたか、後述する処理Ｓ４ｉで新たに検証素子として選択された素子が対象となる。
【００８７】
現在検証している素子がＸＯＲ／ＸＮＯＲの場合、ループ外である他方の入力端子からの入力値が固定されるかどうかはここに至るまでの間にすでに処理Ｓ２ｂで行われている。したがって、これ以上のこの素子に関する検証は不要のため、一気に処理４ｉまで移る。それ以外の場合は通常通りの検証を行うため、処理Ｓ４ｃへ移る。
【００８８】
処理Ｓ４ｃ“発振停止条件有り？”では、現在検証している素子が専用ライブラリ（図６）内で定義されている“発振停止条件”を持つかどうかを確認する。
【００８９】
現在検証している素子とは、処理Ｓ４ａで最初に選択されたか、後述する処理Ｓ４ｉで新たに検証素子として選択された素子が対象となる。例えば、ＩＮＶＥＲＴＥＲの様に、入力端子が一個所しかなく、ループ外から発振を停めることが出来ない素子等は、その“発振停止条件”を持たない。
【００９０】
“発振停止条件”が無い場合、ループ外である他方の入力端子からの入力値で出力値が固定されることは無いとして、これ以上この素子に関する検証は不要のため、処理Ｓ４ｉへ移る。“発振停止条件”がある場合は処理Ｓ４ｄへ移る。
【００９１】
処理Ｓ４ｄ“入力段トレース”は、現在検証している素子のループ外からの入力値が固定されているかどうかを検証する。現在検証している素子とは、処理Ｓ４ａで最初に選択されたか、後述する処理Ｓ４ｉで新たに検証素子として選択された素子が対象となる。
【００９２】
処理Ｓ４ｃにおいて、現在検証している素子が専用ライブラリ（図６）内で定義されている“発振停止条件”を持つ時に行われる。この部分の動作については、さらに詳細な検証方法を示す図５があり、この図５については後述する。図５に示す処理の結果、返り値を得たら処理Ｓ４ｅへ移る。
【００９３】
処理Ｓ４ｅ“発振停止条件と比較”は、処理Ｓ４ｄで得られた現在検証している素子のループ外である他方の入力端子からの入力値と、専用ライブラリ（図６）内で“発振停止条件”として定義されている条件を満たすかどうかの比較を行う。
【００９４】
処理Ｓ４ｄで得られたループ外からの入力値が不定（Ｘ）の場合は、専用ライブラリ内（図６）の“発振停止条件”として提示されている条件に関わらず満たさないということになる。この後は処理Ｓ４ｆへ移る。
【００９５】
処理Ｓ４ｆ“発振止まる？”では、処理Ｓ４ｅで行った判定の結果により次の移り先が変化する。具体的には処理Ｓ４ｅで得られた判定結果が、専用ライブラリ内（図６）の“発振停止条件”として提示されている条件を満たす、といった内容であれば、このループで発振することは無いとして処理Ｓ４ｇへ移る。
【００９６】
これには、“満たすが、外部端子が○○の場合のみ”といった条件付きの場合も含まれる。満たさない場合は他の素子を検証すべく処理Ｓ４ｉへ移る。
【００９７】
処理Ｓ４ｇ“条件有り？”は、処理Ｓ４ｆで、現在検証している素子はループ外である他方の入力端子からの入力値により発振の停止が可能な場合に行われる処理である。現在検証している素子とは、処理Ｓ４ａで最初に選択されたか、後述する処理Ｓ４ｉで新たに検証素子として選択された素子が対象となる。
【００９８】
処理Ｓ４ｄにおいて、ループ外からの入力をトレースして、そのループ外からである他方の入力端子の入力値が固定すると判定された際に、クランプで普遍的に値が固定されるのか、外部端子の使用条件によって固定されることがあるのかによって次の移り先が分岐する。
【００９９】
クランプで普遍的に固定される場合は、現在検証している処理Ｓ１で発見されたループはこの時点で発振しないと判定できるため、このループの検証は終了して、図１内でいう所の処理Ｓ６へ移る。外部端子の使用条件によって発振が停止するかどうかが変化する場合は処理Ｓ４ｈへ移る。
【０１００】
処理Ｓ４ｈ“条件明示”は、上述した処理Ｓ４ｇで発振停止に条件がある場合にその条件を示すものである。この処理の後は処理Ｓ４ｉへ移る。
【０１０１】
処理Ｓ４ｉ“次段へ”の処理は、現在検証している素子からはループ外である他方の入力端子からの入力値で発振停止出来るという確証が得られない場合、および、発振停止出来るが条件付きであり、普遍的でない場合に行われる。
【０１０２】
ループ内の他の素子に関しての検証を行うため、現在検証している素子の後段の素子を新たな現在検証している素子として選択する。処理後は処理Ｓ４ｊへ移動する。
【０１０３】
処理Ｓ４ｊ“始点に戻ったか？”では、処理Ｓ４ｇの結果、検証する素子として選択された素子が処理Ｓ４ａで選択されたものと同じかどうかを判定する。
【０１０４】
同一の場合は、ループ内の全ての素子に対して検証したことになるので、処理Ｓ４全体の検証結果として、“条件付きＯＫ、あるいは問題有り”という形で、図１でいう所の処理Ｓ５へ移る。同一でなければ、処理Ｓ４ｂに戻り同様の検証を行う。
【０１０５】
最後に、図２に処理Ｓ２ｂおよび図４の処理Ｓ４ｄにおいてサブルーチンとして起動されている“入力段トレース”の詳細なフローチャートを示した図５を参照しながら説明する。
【０１０６】
処理ＳＲａ“前段見る”では、現在検証している素子の一つ前段の素子を新たに現在検証する素子として選択する。最初にここに訪れた時は、処理Ｓ２ｂ、処理Ｓ４ｄから起動された時に検証していた素子のループ外である他方の入力端子から１つ前段の素子を現在検証する素子として選択する。複数ある場合は全て選択する形となる。その（それらの）素子に関する判定は次の処理ＳＲｂで行う。
【０１０７】
処理ＳＲｂ“前に訪れたか？”は、処理ＳＲａで選択した素子（群）が前に訪れた所である場合、その経路をトレースしつづけると無限ループに陥ってしまうため、カットする必要がある。そうした部分がある場合は処理ＳＲｃへ移る。なければ処理ＳＲｄに直接移る。
【０１０８】
処理ＳＲｃ“小ループをカット。値はＸとする”は、処理ＳＲｂで現在検証している素子（群）がこれまでに訪れたことのある素子であった場合は、その経路は検証対象外として、その経路からの値は確定しない（Ｘ）とする。その後、処理ＳＲｄへと進む。
【０１０９】
処理ＳＲｄ“０・１・Ｘいずれかに確定？”は、現在検証している素子（群）がクランプである場合、その種類、接続により、そこが“０”“１”に確定すると判定する。
【０１１０】
外部端子である場合は“０”“１”の任意の値に確定できるとする（その場合は後からその確定する任意の値を条件として処理Ｓ５で表示することとなる）。順序回路などの場合は確定しない（Ｘ）と判定する。それ以外の素子の場合は、判定は保留とする。
【０１１１】
個々の詳細な判定条件については前述した通りである。ここに至るまでに得られたこれらの値が確定する個所／しない個所／判定保留の個所より、処理Ｓ２ｂ／処理Ｓ４ｄから起動された時に検証していた素子に対するループ外からの入力値が“０”／“１”／“Ｘ”いずれかに確定するかを判定する。
【０１１２】
“０”／“１”／“Ｘ”いずれにも確定しない場合は再び処理ＳＲａに戻り、そうでない場合は、確定する値を返り値として処理Ｓ２ｃまたはＳ４ｅに戻る。
【０１１３】
次に、具体的な検証対象の回路例を示した図７を参照しながら上述した検証方法を適用する第１の実施例を説明する。
【０１１４】
処理Ｓ１（図１）：ループ構成を見つける（この処理は公知技術の応用）
一例として、図７に示すＩＮＶＥＲＴＥＲ付きＡＮＤ７ａ→ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂ→２入力ＯＲ７ｃ→ＡＮＤ７ａのループが一つだけ発見されたと仮定する。
【０１１５】
処理Ｓ２（図１）：ＸＯＲ／ＸＮＯＲ処理は、処理Ｓ１で見つけたループ内にＸＯＲ／ＸＮＯＲがある場合の処理を行う。
【０１１６】
処理Ｓ２ａ（図２）→“ループ内にＸＯＲ／ＸＮＯＲはあるか？”→無いため、“検証継続”で処理Ｓ３へ移る。
【０１１７】
処理Ｓ３（図１）：正・負帰還チェックは、処理Ｓ１で見つけたループが正帰還ループか負帰還ループかを検証する。
【０１１８】
処理Ｓ３ａ（図３）：検証するにあたっての始点を処理Ｓ１で見つけたループ内で１つ決める。ここでは、仮にＡＮＤ（図７の７ａ）とする。
【０１１９】
処理Ｓ３ｂ（図３）：ＡＮＤ（図７の７ａ）のループ内における入出力経路（入力Ａ→出力Ｙ）が論理反転かどうかを検証する。専用ライブラリ図６の“論理反転経路”と照らし合わせ、論理反転経路を通過しているかを判定する。
【０１２０】
図７のＡＮＤ（７ａ）の場合、ライブラリよりを参照すると、入力Ａ→出力Ｙの経路は論理反転経路に当るため、“通る”ことになり、処理Ｓ３ｃへ移る。
【０１２１】
処理Ｓ３ｃ（図３）：内部記憶として、反転数を＋１し、処理Ｓ３ｄへ移る。
【０１２２】
処理Ｓ３ｄ（図３）：ＡＮＤ７ａの検証は終わったため、別の素子の検証に移る。
【０１２３】
後段ブロックであるＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂへ移動する。処理Ｓ３ｅへ移る。
【０１２４】
処理Ｓ３ｅ（図３）：全ての素子を検証したかどうかを確認する。処理Ｓ３ａで選択した始点はＡＮＤ７ａで、ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂでは無いため、“ＮＯ”へ移動する。フロチャート上では処理Ｓ３ｂ（２回目）にあたる。
【０１２５】
処理Ｓ３ｂ（図３）−２：ＩＮＶＥＲＴＥＲ（図７の７ｂ）におけるループ内の入出力経路（入力Ａ→出力Ｙ）が論理反転かどうかを検証する。専用ライブラリ図６の“論理反転経路”列と照らし合わせ、反転経路を通過しているかを判定する。図７のＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂの場合、ライブラリより反転経路は存在しないため、“通らない”へ進み、次の処理Ｓ３ｄへ移る。
【０１２６】
処理Ｓ３ｄ（図３）−２：ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂの検証が終わったたため、別の素子の検証に移る。ここでは、後段ブロックであるＯＲ７ｃへ移動し、次の処理Ｓ３ｅへ移る。
【０１２７】
処理Ｓ３ｅ（図３）−２：全ての素子を検証したかどうかを確認する。処理Ｓ３ａで選択した始点はＮＡＮＤ７ａであり、ＯＲ７ｃでは無いので“ＮＯ”へ移動する。フロチャート上では処理Ｓ３ｂ（３回目）にあたる。
【０１２８】
処理Ｓ３ｂ（図３）−３：ＯＲ（図７の７ｃ）におけるループ内の入出力経路が論理反転かどうかを検証する。専用ライブラリ図６の“論理反転経路”と照らし合わせ、反転経路を通過しているかを判定する。図７のＯＲ７ｃの場合、ライブラリを参照して反転経路が存在しないので、“通らない”へ進み、次の処理Ｓ３ｄへ移る。
【０１２９】
処理Ｓ３ｄ（図３）−３：ＯＲ７ｃの検証が終わったため、別の素子の検証に移る。ここでは、後段ブロックであるＡＮＤ７ａへ移動し、次の処理Ｓ３ｅへ移る。
【０１３０】
処理Ｓ３ｅ（図３）−３：全ての素子を検証したかどうかを確認する。処理Ｓ３ａで選択した始点はＡＮＤ７ａであり、始点に戻っているため、一連の検証を終了して“ＮＯ”へ進み、次の処理Ｓ３ｆに移動する。
【０１３１】
処理Ｓ３ｆ（図３）：判定する。内部記憶されている総反転数は１で奇数（処理Ｓ３ｃで定義）である。“反転数＝奇数”へ進み、処理Ｓ３としては“負帰還”を結果として返す。
【０１３２】
再び図１の処理Ｓ３に戻った時に“負帰還”であれば処理Ｓ４へ移動することとなる。なお、この処理Ｓ１で発見したループの検証を終えた時点で内部記憶の反転数は一度クリアされる。（０に戻る）
処理Ｓ４（図１）：ループ外である他方の入力端子（Ｂ）からの入力で発振を止められるかの検証を行う。
【０１３３】
処理Ｓ４ａ（図４）：処理Ｓ１で見つけたループ内で、検証の始点とする素子を一つ任意に選択する。仮にＡＮＤ（図７の７ａ）とする。
【０１３４】
処理Ｓ４ｂ（図４）：ＡＮＤ７ａがＸＯＲ／ＸＮＯＲでないか確認（処理Ｓ２にて別方法でトレース済みのため）。ＡＮＤ７ａはＸＯＲ／ＸＮＯＲで無いため、“ＮＯ”へ進み、次の処理Ｓ４ｃへ移動する。
【０１３５】
処理Ｓ４ｃ（図４）：ＡＮＤ７ａは発振停止条件を持つかどうかを確認する。ＡＮＤ７ａの場合は、図６のライブラリ参照して入力Ｂ＝０で固定されていれば、発振を止めることが出来るため“ＹＥＳ”へ進み、次の処理Ｓ４ｄへ移る。
【０１３６】
処理Ｓ４ｄ（図４）：ＡＮＤ７ａへのループ外である他方の入力端子からの入力段をトレース（サブルーチン）する。
【０１３７】
処理ＳＲａ（図５）：ＡＮＤ７ａの１つ前段をトレースする。ＡＮＤ７ａの入力Ｂは外部端子“ＩＮ１”から来ている。
【０１３８】
処理ＳＲｂ（図５）：処理ＳＲａで見つけたＡＮＤ７ａの一つ前段の素子は前に訪れたかどうかを確認。まだ訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃへ移る。
【０１３９】
処理ＳＲｃ（図５）：処理ＳＲａで見つけたＡＮＤ７ａの前段入力により値が“０”／“１”／“Ｘ”（不定）いずれかに確定するかを判定する。ＡＮＤ７ａの入力Ｂは外部端子からの接続で、確定させることは可能である。したがって“ＹＥＳ”へ進み、図４の処理Ｓ４ｅへ移る。
【０１４０】
処理Ｓ４ｅ（図４）：処理Ｓ５を通しての帰り値と、発振停止条件と比較する。
【０１４１】
処理Ｓ４ｃで得た発振停止条件より、処理ＳＲｃで得られた外部端子が“０”で固定される限り発振を停めることが可能である。したがって、処理Ｓ４ｆへ移る。
【０１４２】
処理Ｓ４ｆ（図４）：処理Ｓ４ｅの結果より、発振は止まるかどうかを判定。判定の結果、止まるので“ＹＥＳ”へ進み、次の処理Ｓ４ｇへ移る。
【０１４３】
処理Ｓ４ｇ（図４）：処理Ｓ４ｅの結果より、発振停止にあたっての条件があるかどうか判定する。処理Ｓ４ｅより、外部端子“ＩＮ１”が“０”で固定という条件が存在するため“ＹＥＳ”へ進み、次の処理Ｓ４ｈへ移る。
【０１４４】
処理Ｓ４ｈ（図４）：処理Ｓ４ｇで確認された条件を明示する。例えば、この例の場合は“外部端子「ＩＮ１」が０で固定なら問題無し”。
【０１４５】
処理Ｓ４ｉ（図４）：ＡＮＤ７ａの検証が終わったため、別の素子の検証にうつる。後段ブロックであるＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂを新たに検証する素子として選択し、処理Ｓ４ｊへ移る。
【０１４６】
処理Ｓ４ｊ（図４）：現在検証している素子であるＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂで、処理Ｓ１で発見された現在検証しているループ内の始点に戻ったかを確認する。始点はＡＮＤ７ａで、現在検証している素子はＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂのため、“ＮＯ”へ進み、次の処理Ｓ４ｂ（２回目）へ移る。
【０１４７】
処理Ｓ４ｂ（図４）−２：ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂがＸＯＲ／ＸＮＯＲでないか確認（処理Ｓ２にて別方法でトレース済みのため）。ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂはＸＯＲ／ＸＮＯＲでは無いため“ＮＯ”へ進み、次の処理Ｓ４ｃ−２へ移動する。
【０１４８】
処理Ｓ４ｃ（図４）−２：ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂが発振停止条件を持つかどうかを確認する。図６のライブラリを参照すると発振停止条件を持たないことから“ＮＯ”へ進み、処理Ｓ４ｉ−２へ移る。
【０１４９】
処理Ｓ４ｉ（図４）−２：ＮＯＮ−ＩＮＶＥＲＴＥＲ７ｂの検証が終わったので、別の素子の検証に移る。
【０１５０】
後段ブロックであるＯＲ７ｃを新たに検証する素子として選択し、処理Ｓ４ｊ−２へ移る。
【０１５１】
処理Ｓ４ｊ（図４）−２：現在検証している素子であるＯＲ７ｃで、処理Ｓ１で発見された、現在検証しているループ内の始点に戻ったかを確認する。始点はＡＮＤ７ａで、現在検証している素子はＯＲ７ｃのため“ＮＯ”へ進み、処理Ｓ４ｂ（３回目）へ移る。
【０１５２】
処理Ｓ４ｂ（図４）−３：ＯＲ７ｃがＸＯＲ／ＸＮＯＲでないか確認（処理Ｓ２にて別方法でトレース済みのため）。ＯＲ７ｃはＸＯＲ／ＸＮＯＲで無いため“ＮＯ”へ進み、処理Ｓ４ｃ−３へ移る。
【０１５３】
処理Ｓ４ｃ（図４）−３：ＯＲ７ｃが発振停止条件を持つかどうかを確認する。
【０１５４】
図６のライブラリを参照すると入力Ｂ＝１で固定されていれば、発振を停めることが出来るため“ＹＥＳ”へ進み、次の処理Ｓ４ｄ−３へ移る。
【０１５５】
処理Ｓ４ｄ（図４）−３：ＯＲ７ｃへのループ外である入力端子Ｂからの入力段をトレースする（サブルーチン）。次の処理ＳＲａ−３へ移る。
【０１５６】
処理ＳＲａ（図５）−３：ＯＲ７ｃのループ外である他方の入力端子Ｂからの１つ前段の素子をトレースする。ＯＲ７ｃの入力Ｂは“０”（ＬＯＷ）でクランプされている。次の処理ＳＲｂ−３へ移る。
【０１５７】
処理ＳＲｂ（図５）−３：処理ＳＲａで見つけたＯＲ７ｃの一つ前段の素子は前に訪れたかどうかを確認する。まだ訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃ−３へ移る。
【０１５８】
処理ＳＲｃ（図５）−３：処理ＳＲａで見つけたＯＲ７ｃの前段入力により、値が“０”／“１”／“Ｘ”（不定）いずれかに確定するかを判定する。この場合“０”でクランプされているため、“０”で固定されるので“ＹＥＳ”へ進み、処理Ｓ４ｅ−３へ移る。
【０１５９】
処理Ｓ４ｅ（図４）−３：処理ＳＲｃ−３で得られたＯＲ７ｃへのループ外である他方の入力端子Ｂからの入力値“０”と発振停止条件を比較する。処理Ｓ４ｃ−３で得た発振停止条件より、“０”でクランプされていても発振停止とはならない。次の処理Ｓ４ｆ−３へ移る。
【０１６０】
処理Ｓ４ｆ（図４）−３：処理Ｓ４ｅ−３の結果、発振が停まるか判定した結果、発振は止まらないので“ＮＯ”へ進み、処理Ｓ４ｉ−３へ移る。
【０１６１】
処理Ｓ４ｉ（図４）−３：ＯＲ７ｃの検証が終わったため、別の素子の検証にうつる。後段ブロックであるＡＮＤ７ａを新たに検証する素子として選択して処理Ｓ４ｊ−３へ移る。
【０１６２】
処理Ｓ４ｊ（図４）−３：現在検証している素子であるＡＮＤ７ａで、処理Ｓ１で発見された、現在検証しているループ内の始点に戻ったかを確認する。始点はＡＮＤ７ａで、現在検証している素子もＡＮＤ７ａのため“ＹＥＳ”へ進み、処理Ｓ５へ移る。
【０１６３】
処理Ｓ５（図１）：処理Ｓ１で発見されたループ回路個所を明示して、問題点を表示する。この例ではＡＮＤ７ａ，ＮＯＮ−ＩＮＶＥＲＴＥＲ７ａ，ＯＲ７ｃを回路データ内でブロック毎に与えられたユニークな名前を用いて明示しつつ、実機上で発振する可能性があること、また、外部端子ＩＮ１＝０固定で使う限りにおいては問題無い旨明示する。
【０１６４】
処理Ｓ６（図１）：処理Ｓ１で発見された他のループは有るか？→無いので“無”へ進む。（処理おわり）
上述したように本発明は、問題のある回路構成を検出したり、実機上で発振状態を回避するための条件等を予め明示することで、より良い品質の製品を供給することが出来る。また、通常開発そのものの数倍〜数十倍かかる、不良発生時の解析、発見、リカバリのＴＡＴを完全にカットできる。
【０１６５】
さらに、一つ一つの素子に対して、入出力端子間で信号極性が反転する経路、および他の入力値に関係無く出力値を確定させるために必要な入力条件の情報をライブラリ化することで、回路構成に依存すること無く、発振ループ構成になっているかどうかの判定を行うことが出来る。
【０１６６】
さらにまた、そのライブラリそのものは、真理値情報１１を基に容易に作成、更新することが出来る。
【０１６７】
次に、具体的な検証対象の回路例を示した図８を参照しながら前述した検証方法を適用する第２の実施例を説明する。ここではループ部分にＸＯＲが含まれている場合の例である。
【０１６８】
上述した第１の実施例と異なる点は、ＸＯＲ／ＸＮＯＲが含まれている場合、ループ外である他方の入力端子からの入力値によって、信号極性の反転、非反転が変化するため、ループ内が正帰還ループか負帰還ループかの判定が通常の手段では行えない点にある。
【０１６９】
本発明では、ループ外の入力がクランプにより論理が確定している場合に関して、ＩＮＶＥＲＴＥＲ／ＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えることで反転、非反転の検証を可能にしている。また、置き換えられない場合でも他のブロックのループ外入力チェックも行い、疑似エラーとなる可能性を探っている。
【０１７０】
処理Ｓ１（図１）：ループ構成を見つける（前述したように公知技術の応用）。
【０１７１】
処理Ｓ２へ進む。例として、図８に示した様なＩＮＶＥＲＴＥＲ付きＡＮＤ８ａ→ＮＯＮ−ＩＮＶＥＲＴＥＲ８ｂ→２入力ＸＯＲ８ｃ→ＩＮＶＥＲＴＥＲ付きＡＮＤ８ａによるループが一つだけ発見されたと仮定する。
【０１７２】
処理Ｓ２（図１）：ＸＯＲ／ＸＮＯＲ処理。すなわち処理２ａへ移る。
【０１７３】
処理Ｓ２ａ（図２）：処理Ｓ１で発見されたループ内にＸＯＲ／ＸＮＯＲはあるか？→ＸＯＲ８ｃが存在するので“有り”へ進み、次の処理Ｓ２ｂへ移る。
【０１７４】
処理Ｓ２ｂ（図２）：処理Ｓ２ａで発見されたＸＯＲ８ｃのループ外である他方の入力端子Ｂからの入力段をトレースする。
【０１７５】
処理ＳＲａ（図５）：ＸＯＲ８ｃのループ外からの入力がどこからきているか、一つ前段を見る。ＸＯＲ８ｃのループ外である他方の入力端子Ｂからの入力はＬＯＷでクランプ（８ｅ）されており、論理レベルの“０”で固定されている。次の処理ＳＲｂへ移る。
【０１７６】
処理ＳＲｂ（図５）：クランプ（８ｅ）は前に訪れたことがあるか？→訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃへ移る。
【０１７７】
処理ＳＲｃ（図５）：ここまでで、ＸＯＲ８ｃのループ外からの入力が“０”“１”“Ｘ”のいずれかになるか確定するか？→ＸＯＲ８ｃのループ外からの入力はＬＯＷクランプ（８ｅ）なので、“０”に確定するため“ＹＥＳ”へ進み、処理Ｓ２ｃへ移る。
【０１７８】
処理Ｓ２ｃ（図２）：処理Ｓ１で発見されたループ内における、ＸＯＲ８ｃはＩＮＶＥＲＴＥＲなどに置き換えが可能か？→処理ＳＲｃの結果から、ループ外がＬＯＷ固定のため、真理値情報１１よりＮＯＮ−ＩＮＶＥＲＴＥＲに置き換えが可能となり、次の処理Ｓ２ｄへ移る。
【０１７９】
処理Ｓ２ｄ（図２）：処理Ｓ１で発見されたループ内における、ＸＯＲ８ｃをＮＯＮ−ＩＮＶＥＲＴＥＲに置き換える。以後、内部的に置き換えられた図９に示す回路に対して解析を行い、次の処理Ｓ２ｅへ移る。
【０１８０】
処理Ｓ２ｅ（図２）：他にも処理Ｓ１で発見されたループ内において、ＸＯＲ／ＸＮＯＲがあるか？→無いため“検証継続”し、処理Ｓ３へ移る。
【０１８１】
処理Ｓ３（図１）：処理Ｓ１で発見されたループが正帰還ループか、負帰還ループかを判定し、処理Ｓ３ａへ移る。
【０１８２】
処理Ｓ３ａ（図３）：各素子を検証するにあたって、どの素子から検証を始めるかを任意に決める。仮にＡＮＤ（図９の９ａ）とする。
【０１８３】
これ以降の、処理Ｓ３内で検証する素子がＮＯＮ−ＩＮＶＥＲＴＥＲ９ｃに移動するまでは上述した第１の実施例と同様であるからここでの説明は省略する。
【０１８４】
処理Ｓ３ｄ（図３）−２：現在検証している素子の検証が終わったため、次段の素子を新たに検証する素子として選択する。後段ブロックであるＮＯＮ−ＩＮＶＥＲＴＥＲ（元はＸＯＲ８ｃ）９ｃへ移動し、次の処理Ｓ３ｅ−２へ移る。
【０１８５】
処理Ｓ３ｅ（図３）−２：現在検証している素子が処理Ｓ１で発見されたループ上を一回りして、始点に戻ったかどうかを確認する？→始点は９ａで、９ｃでは無いため“ＮＯ”へ進み、処理Ｓ３ｂ−２へ移る。
【０１８６】
処理Ｓ３ｂ（図３）−３：現在検証している素子がループ内で接続されている経路は専用ライブラリ（図６）内で定義されている“論理反転経路”に含まれているかを判定する。図９におけるＮＯＮ−ＩＮＶＥＲＴＥＲ９ｃの場合、ライブラリを参照すると論理反転経路は存在しないため、“通らない”へ進む。
【０１８７】
これ以降の動作は上述した第１の実施例と同様であり、ここでの説明は省略する。
【０１８８】
次に、具体的な検証対象の回路例を示した図１０を参照しながら前述した検証方法を適用する第３の実施例を説明する。この例はＸＯＲ／ＸＮＯＲが上述した第２の実施例の様に縮退出来ないケースについて説明する。
【０１８９】
ここでの縮退とは、冗長な個所、構成を、より簡略化されたものに置き換えることが可能である場合に、それに置き換えることを意味し、この例では、ＸＯＲ／ＸＮＯＲを回路構成よりＢＵＦＦＥＲ／ＩＮＶＥＲＴＥＲに置き換えることである。
【０１９０】
縮退が出来ない場合は、ループの反転・非反転検証は行わず、他ブロックのループ外入力チェックのみを行うものとなる。
【０１９１】
処理Ｓ１（図１）：ループ構成を見つける（公知技術の応用）例として、図１０に示す様なＩＮＶＥＲＴＥＲ付きＡＮＤ１０ａ→ＮＯＮ−ＩＮＶＥＲＴＥＲ１０ｂ→２入力ＸＯＲ１０ｃ→ＩＮＶＥＲＴＥＲ付きＡＮＤ１０ａによるループが一つだけ発見されたと仮定する。
【０１９２】
処理Ｓ２（図１）：処理Ｓ１で発見されたループ内におけるＸＯＲ／ＸＮＯＲ処理を行う。処理Ｓ２ａへ移る。
【０１９３】
処理Ｓ２ａ（図２）：処理Ｓ１で発見されたループ内にＸＯＲ／ＸＮＯＲはあるか？→有り→処理Ｓ２ｂへ移る。
【０１９４】
処理Ｓ２ｂ（図２）：処理Ｓ２ａで発見されたＸＯＲ／ＸＮＯＲのループ外である他方の入力端子Ｂの入力段トレースを行う。すなわち、処理ＳＲａへ移る。
【０１９５】
処理ＳＲａ（図５）：処理Ｓ２ａで発見されたＸＯＲ／ＸＮＯＲのループ外の前段ブロックからの入力を見る。ＸＯＲ１０ｃのループ外からの入力値は順序回路１０ｅから来ており、その値が固定することは考え難い。次の処理ＳＲｂへ移る。
【０１９６】
処理ＳＲｂ（図５）：順序回路１０ｅは前に訪れたか？→訪れていないため、“ＮＯ”へ進み、次の処理ＳＲｃへ移る。
【０１９７】
処理ＳＲｃ（図５）：順序回路１０ｅの出力は“０”“１”“Ｘ”いずれかに確定するか？→Ｘに確定する“ＹＥＳ”へ進む。処理Ｓ２ｃへ戻る。
【０１９８】
処理Ｓ２ｃ（図２）：処理Ｓ２ａで発見されたＸＯＲ／ＸＮＯＲをＩＮＶＥＲＴＥＲなどに置き換え出来るか？→ループ外からの入力が何に固定されるか不確定のため、置き換えも出来ない。
【０１９９】
これ以降の動作は、処理Ｓ４内で検証する素子が１０ｃに移動するまで前述した第１の実施例と同様であるから、ここでの説明は省略する。
【０２００】
処理Ｓ４ｂ（図４）：ループ外である他方の入力端子からの入力値をトレースするが、ＸＯＲ／ＸＮＯＲに関しては既に検証済みのため、現在選択されている検証対象の素子がＸＯＲ／ＸＮＯＲでないか確認する（処理Ｓ２にて別方法でトレース済みのため）。ＸＯＲのため“ＹＥＳ”へ進む。すなわち、入力段検証をスキップし処理Ｓ４ｉへ移る。
【０２０１】
処理Ｓ４ｉ（図４）：現在検証している素子の一つ次段の素子を新たに検証素子として選択する。こここではＡＮＤ１０ａを選択する。処理Ｓ４ｊへ移る。
【０２０２】
処理Ｓ４ｊ（図４）：処理Ｓ４ｉで選択した素子で、始点に戻ったか？→始点はＡＮＤ１０ａで“ＹＥＳ”へ進む。
【０２０３】
これ以降の動作は前述した第１の実施例と同様であるからここでの説明は省略する。
【０２０４】
次に、具体的な検証対象の回路例を示した図１１を参照しながら前述した検証方法を適用する第４の実施例を説明する。ここでは２重ループ構成の場合の例について説明する。
【０２０５】
発見したループの中にさらに小さい例えば負帰還ループが存在する場合は、入力段トレース時にトレースが終了しなくなってしまう。小さいループは別検証にても可能であること、また、小さいループ内で値が確定している場合は、ループカット後引き続きトレースを続けることで発見が可能であるから、そうしたケースにおいては、その部分におけるループ外入力値は不確定（Ｘ）として一旦ループをカットすることでトレースを継続する。
【０２０６】
処理Ｓ１（図１）：ループ構成を見つける（この処理は公知技術の応用）例として、図１１に示す様なＮＡＮＤ１１ａ→ＩＮＶＥＲＴＥＲ１１ｂ→ＮＡＮＤ１１ｃ→ＡＮＤ１１ｄ→ＮＡＮＤ１１ａによるループが、数あるループの中一つとして発見されたと仮定する。
【０２０７】
これ以降の動作は処理Ｓ４内で検証素子がＮＡＮＤ１１ｃに移動するまで前述した第１の実施例と同様であるからここでの説明は省略する。
【０２０８】
処理Ｓ４ｂ（図４）：ループ外である他方の入力端子からの入力値をトレースするにあたって、現在検証している素子がＸＯＲ／ＸＮＯＲでないか確認する。上述したように、現在検証している素子はＮＡＮＤ１１ｃであり、ＸＯＲでは無いため“ＮＯ”へ進み、次の処理Ｓ４ｃへ移る。
【０２０９】
処理Ｓ４ｃ（図４）：現在検証している素子であるＮＡＮＤ１１ｃは発振停止条件を持つか？→図６のライブラリを参照すると入力Ａ＝０で固定されていれば、発振を止めることが出来るため“ＹＥＳ”へ進み、次の処理Ｓ４ｄへ移る。
【０２１０】
処理Ｓ４ｄ（図４）：素子ＮＡＮＤ１１ｃのループ外である他方の入力端子Ａからの入力値をトレースする。
【０２１１】
処理ＳＲａ（図５）：現在検証する素子はＮＡＮＤ１１ｃだが、ループ外からの１つ前段の素子であるＡＮＤ１１ｄを新たに現在検証する素子として選択し、次の処理ＳＲｂへ移る。
【０２１２】
処理ＳＲｂ（図５）：この素子ＡＮＤ１１ｄは前に訪れたことがあるか？→訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃへ移る。
【０２１３】
処理ＳＲｃ（図５）：この素子ＡＮＤ１１ｄの出力値が“０”／“１”／“Ｘ”（不確定）のいずれに確定するかを判定するが、この情報のみでは確定させることは不可能であるから“ＮＯ”へ進み、次の処理ＳＲａ（２回目）へ移る。
【０２１４】
処理ＳＲａ（図５）−２：現在検証する素子はＡＮＤ１１ｄだが、さらに１つ前段の素子であるＮＡＮＤ１１ｃ（入力Ａから）と、ＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅ（入力Ｂから）から来ている。その二つを新たに検証している素子として選択し、次の処理ＳＲｂ−２へ移る。
【０２１５】
処理ＳＲｂ（図５）−２：これらの素子は前に訪れたことがあるかを確認すると、ＡＮＤ１１ｃは前に訪れているので“ＹＥＳ”へ進み、次の処理ＳＲｄ−２へ移る。
【０２１６】
処理ＳＲｄ（図５）−２：ＮＡＮＤ１１ｃ→ＡＮＤ１１ｄ→ＮＡＮＤ１１ｃとループになっているため、この経路はカットする。ＮＡＮＤ１１ｃの入力Ａは不確定（Ｘ）と判定し、次の処理ＳＲｃ−２へ移る。
【０２１７】
処理ＳＲｃ（図５）−２：処理ＳＲｄ−２より、ＮＡＮＤ１１ｃの入力Ａは不確定（Ｘ）と判定し、処理Ｓ４ｅへ戻る。
【０２１８】
処理Ｓ４ｅ（図４）：最後にループ内で検証していた素子であるＮＡＮＤ１１ｃに戻って、発振停止条件と比較する。処理Ｓ４ｃで得た発振停止条件は満たしていない。次の処理Ｓ４ｆへ移る。
【０２１９】
処理Ｓ４ｆ（図４）：処理Ｓ４ｅからの入力値で発振は停止するとはいいきれないため“ＮＯ”へ進み、処理Ｓ４ｉへ移る。
【０２２０】
処理Ｓ４ｉ（図４）：現在検証している素子として、新たに次段であるＡＮＤ１１ｄを選択し、処理Ｓ４ｊへ移る。
【０２２１】
処理４Ｓ４ｊ（図４）：処理Ｓ４ｉで選択された素子は、初めて処理Ｓ４に入った時に、始点として選択された素子か？→始点はＡＮＤ１１ａなので“ＮＯ”へ進み、処理Ｓ４ｂ（２回目）へ移る。
【０２２２】
処理Ｓ４ｂ（図４）−２：処理Ｓ４ｉで選択されたＡＮＤ１１ｄはＸＯＲ／ＸＮＯＲでないか確認？→“ＮＯ”へ進み、次の処理Ｓ４ｃ−２へ移る。
【０２２３】
処理Ｓ４ｃ（図４）−２：処理Ｓ４ｉで選択されたＡＮＤ１１ｄは専用ライブラリ（図６）内で、発振停止条件を持つか？→入力Ｂが“０”で固定されていれば発振停止するため“ＹＥＳ”へ進み、次の処理Ｓ４ｄ−２へ移る。
【０２２４】
処理Ｓ４ｄ（図４）−２：処理Ｓ４ｉで選択されたＡＮＤ１１ｄのループ外からの入力をトレースするため、サブルーチンの処理ＳＲａ−３へ移る。
【０２２５】
処理ＳＲａ（図５）−３：ＡＮＤ１１ｄのループ外からの１つ前段の素子を確認する。ＡＮＤ１１ｄの入力Ｂは、ＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅから来ている。次の処理ＳＲｂ−３へ移る。
【０２２６】
処理ＳＲｂ（図５）−３：処理ＳＲａ−３で選択されたＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅが前に訪れた素子か確認する。→訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃ−３へ移る。
【０２２７】
処理ＳＲｃ（図５）−３：処理ＳＲａ−３で選択された素子からの出力値が、“０”／“１”／“Ｘ”（不確定）のいずれに確定するかを判定する。ＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅの出力からきており、この情報のみからでは確定しているかわからない。処理ＳＲａ−４へ戻る。
【０２２８】
処理ＳＲａ（図５）−４：ＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅのさらに１つ前段をトレースする。ＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅの入力ＡはＬＯＷ＿ＣＬＡＭＰ（ＬＯＷでクランプ）１１ｇから来ている。次の処理ＳＲｂ−４へ移る。
【０２２９】
処理ＳＲｂ（図５）−４：処理ＳＲａ−４で選択された素子は前に訪れたことがあるか？→訪れていないため“ＮＯ”へ進み、次の処理ＳＲｃ−４へ移る。
【０２３０】
処理ＳＲｃ（図５）−４：処理ＳＲａ−４で選択された素子の出力値が“０”／“１”／“Ｘ”（不確定）いずれかに確定するかを判定する。処理ＳＲａ−４で発見されたＬＯＷ＿ＣＬＡＭＰ１１ｇはＮＯＮ−ＩＮＶＥＲＴＥＲ１１ｅを経由して、ＡＮＤ１１ｄの入力端子Ｂに接続されてる。結果、ＡＮＤ１１ｄからは“０”しか出ない。
【０２３１】
これ以降の動作は前述した第１の実施例と同様であるからここでの説明は省略する。
【０２３２】
【発明の効果】
上述したように、本発明のループ回路における発振構成箇所の検出方法は、内部回路における正帰還および負帰還によるループ回路のうち禁止されている負帰還ループを論理検証段階で検出するループ検出手段として、内部回路を構成する素子それぞれの少なくとも一方の入力端子と出力端子間で信号極性が反転する経路と、他方の入力端子の入力値に関係無く出力値を確定させるために必要な入力条件の情報とを、あらかじめ定める真理値情報に基き作成および更新して論理検証装置の記憶手段にライブラリ化するとともに、ライブラリを引用しながら、内部回路の構成が発振ループ構成になっているかどうかの判定を行ない、その判定結果を外部の表示手段に表示するので、問題のある回路構成を検出したり、実機上で発振状態を回避する為の条件等を予め明示することができ、より良い品質の製品を供給することが出来る。
【０２３３】
また、通常、開発そのものの数倍〜数十倍かかる、不良発生時の解析、発見、リカバリのＴＡＴを完全にカットできる。
【０２３４】
さらに、一つ一つの素子に対して、入出力間で反転する経路、および、他の入力値に関係無く出力を確定させるために必要な入力条件の情報をライブラリ化することで、回路構成に依存すること無く、発振ループ構成になっているかどうかの判定を容易に行うことが出来る。
【０２３５】
さらにまた、そのライブラリそのものは、真理値情報を基に容易に作成、更新することが出来る。
【図面の簡単な説明】
【図１】本発明の実施形態によるループ回路における発振構成箇所の検出方法を示す全体のフローチャートである。
【図２】処理Ｓ２の詳細なフローチャートである。
【図３】処理Ｓ３の詳細なフローチャートである。
【図４】処理Ｓ４の詳細なフローチャートである。
【図５】処理Ｓ２ｂおよびＳ４ｄの詳細なフローチャートである。
【図６】ライブラリの例を示す図である。
【図７】本発明の検証方法を適用する第１の実施例の回路例を示した図である。
【図８】本発明の検証方法を適用する第２の実施例の回路例を示した図である。
【図９】図８におけるＸＯＲ８ｃをＮＯＮ−ＩＮＶＥＲＴＥＲ９ｃに置き換えた図である。
【図１０】本発明の検証方法を適用する第３の実施例の回路例を示した図である。
【図１１】本発明の検証方法を適用する第４の実施例の回路例を示した図である。
【図１２】従来の検証方法の説明用回路例を示す図である。
【図１３】シミュレーション結果の波形図を示した図である。
【図１４】実機上でのＮＡＮＤの入出力波形を示した図である。
【符号の説明】
１１    真理値情報
１２    ライブラリ
７ａ，８ａ，９ａ，１０ａ    ＩＮＶＥＲＴＥＲ付きＡＮＤ
７ｂ，８ｂ，９ｃ，１０ｂ，１１ｅ，１２ｂ    ＮＯＮ−ＩＮＶＥＲＴＥＲ
７ｃ    ＯＲ
８ｃ，１０ｃ    ＸＯＲ
１０ｅ    順序回路
１１ａ，１１ｃ，１２ａ    ＮＡＮＤ
１１ｂ    ＩＮＶＥＲＴＥＲ
１１ｄ    ＡＮＤ
１１ｇ    ＬＯＷ＿ＣＬＡＭＰ
１２ｃ    ＨＩＧＨ＿ＣＬＡＭＰ
【図１】
0003703390.tif 000002
【図２】
0003703390.tif 000003
【図３】
0003703390.tif 000004
【図４】
0003703390.tif 000005
【図５】
0003703390.tif 000006
【図６】
0003703390.tif 000007
【図７】
0003703390.tif 000008
【図８】
0003703390.tif 000009
【図９】
0003703390.tif 000010
【図１０】
0003703390.tif 000011
【図１１】
0003703390.tif 000012
【図１２】
0003703390.tif 000013
【図１３】
0003703390.tif 000014
【図１４】
0003703390.tif 000015