(57)【要約】【課題】簡単な、非計算的な構成性の定義（Constructivity-SAT）と、新しい定式化に基づく、任意の有限型の変数に対して実装が簡単な記号アルゴリズムとによって、回路定義を改善する。【解決手段】簡単な変換によって、値⊥（「ボトム」と読む）で拡張された変数型に関する、定義から導出された方程式集合の充足可能性として、構成性を再定式化することができることが示される。この定式化は、非計算的であり、任意の有限型の変数に容易に拡張可能である。また、この定式化は、同様にして、添字つき変数の定義も扱う。この構成性チェックはＣＯＳＰＡＮで実装された。ＣＯＳＰＡＮは、市販のFormalCheck検証ツールのための検証エンジンである。この実装は簡単であり、経験によれば、通常、無視しうるオーバーヘッドしか受けない。【選択図】図１
2006209787.tif 000002
【特許請求の範囲】
【請求項１】
巡回動作用の回路を評価する方法であって、該回路がこの回路中のゲートを指定する定義の集合の言葉で指定されており、該定義が１つもしくは複数個の変数により特徴づけられているような方法において、
該定義の集合内の複数の変数のうちの少なくとも一部の変数を、⊥値を含む変数型に変換することにより、該定義の集合を通る単一のパス中に修正された定義の集合を形成するステップと、
該修正された定義の集合の解が、値が⊥の変数を含むかどうかを確認するステップと、
該確認するステップの結果に基づいて、評価中の回路が構成的な回路であるかどうかについての指示を出力するステップと、
を有することを特徴とする方法。
【請求項２】
前記確認するステップは、前記修正された定義の集合によって表される連立方程式集合を解くことによって実行されることを特徴とする請求項１に記載の方法。
【請求項３】
前記変数のうちの少なくとも１つが値⊥を有することが前記解から明らかになったときに、巡回性条件を報告するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項４】
前記少なくとも一部の変数は、内部変数に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項５】
前記少なくとも一部の変数は、外部変数以外に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項６】
前記外部変数は、入力変数およびクロックされる遅延要素に対応することを特徴とする請求項５に記載の方法。
【請求項７】
回路の使用から前記定義の集合を生成するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項８】
ｘを内部変数とし、Ａを別の内部変数とし、ｚを添字つき変数として、型の定義（ｚ［ｘ］＝Ａ）が、
【数１】
2006209787.tif 000003
に変換されることを特徴とする請求項１に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータ支援回路設計に関する。
【背景技術】
【０００２】
回路は、定義の集合として記述されることが可能である。各定義は、回路のゲートを指定する。ほとんどの回路では、このような定義集合の誘導従属性グラフは非巡回的である。すなわち、回路は、システムがとらなければならない状態における不確定性を引き起こす可能性のある、あるいは、実際には、回路がいかなる安定状態にも定まらなくなる可能性のある、（クロックされる遅延素子のない）フィードバックループを含まない。全体として回路を定義する定義集合を調べる際には、個々の定義、あるいは、（通常は）定義の集まりは、意味論的に巡回的であること、または、構文論的に巡回的であることがある。定義が統語論的に巡回的(syntactically cyclic)であるとは、変数ｐがそれ自身により、または、実質的にｐで表される少なくとも１つの他の変数ｑにより、表される場合をいう。意味論的に巡回的(semantically cyclic)な定義とは、少なくとも１つの評価(valuation)に対して（例えば、回路の１つ以上の外部変数の特定の評価について）、統語論的に非巡回的な条件が存在しないものをいう。
【０００３】
統語論的に巡回的な定義は、ディジタル設計の多くの状況で起こる。S. Malik, ”Analysis of cyclic combinational circuits”, IEEE Transactions on Computer-Aided Design, 1994、には、ルーティング機構を通じて巡回的に機能ユニットを接続することによりそれらの機能ユニットを再利用することがしばしば好ましいことが指摘されている。また、L. Stok, ”False loops through resource sharing”, in International Conference on Computer-Aided Design, 1992、には、このような定義は、合成プログラムの出力においてしばしば生じることが指摘されている。これらの場合、意図されているのは、外部の「自由」入力および（クロックされるラッチのような）クロックされる遅延要素の各評価ごとに、「意味論的に」巡回的なパスを分解するように、ルーティング機構は外部入力を通じて制御可能であるということである。
【０００４】
意味論的に巡回的な定義は、例えば、いくつかのミーリー機械(Mealy machine)から構成されるシステムにおいて、組合せ入力と出力の間のフィードバック接続から偶然に生じることがある。
【０００５】
意味論的に巡回的な定義を受け入れる検証システムは、巡回条件に関連する許容できない挙動を有するシステムを証明するという危険を明らかに冒す。他方、統語論的に巡回的な定義を禁止する検証システムは、形式検証によれば巡回条件がないものと証明される可能性のある回路定義を拒絶する。現在のほとんどの設計および検証システムは、すべての統語論的に巡回的な定義を禁止するか、または、受け入れ可能な一部の意味論的に非巡回的な定義のみを受け入れる。
【０００６】
エステレルコンパイラ(Esterel compiler)は、Berryにより提案された「構成性」(constructivity)の概念を用いて、意味論的巡回性のある定義を解析する、従来唯一知られているシステムであると思われる。このシステムは、回路について、あらゆる外部入力に対して、回路の定義に関する一連の推論により、各内部配線ごとに一意的な値が導出可能である場合に限り、回路を意味論的に非巡回的であるとみなす（詳細な説明は後述）。T. Shiple, ”Formal Analysis of Synchronous Circuits”, PhD dissertation, University of California, Berkeley, 1996、によれば、構成的定義とは、J. A. Brzozowski and C-J. H. Seger, ”Asynchronous Circuits”, Springer Verlag, 1994、で定義された上に有界でない慣性遅延モデルにおいて、任意の遅延値の割当てに対して、電気的に正しく動作するものにほかならない。
【発明の開示】
【発明が解決しようとする課題】
【０００７】
本発明にもっとも関連の深い研究は、前掲のBerryの論文と、前掲のShipleの論文に記載されている。Berryは、Malikの前掲論文による研究に基づいて、構成性のオリジナルな操作的定式化（Constructivity）および計算的定式化（Constructivity-FIX）を提案した。これらの定義は、計算プロセスに基づいている（「意味論的非巡回性」の概念の非計算的定義のほうが好ましいかもしれないが）。T. Shiple, G. Berry and H. Touati, ”Constructive analysis of cyclic circuits”, in European Design and Test Conference, 1996、も参照。ここまでに掲げた文献では、構成性をチェックするために、記号的な、固定点によるアルゴリズムを使用する。これらのアルゴリズムは、実装が困難であり、非ブール型の変数に対してはやや非効率的である。
【０００８】
すべての可能な外部評価を列挙することによって構成性をチェックするのは非効率的である。構成性をチェックするための記号アルゴリズムは、入力評価をＢＤＤで表して、集合を操作する。
・R. Bryant, ”Graph based algorithms for boolean function manipulation”, IEEE Transactions on Computers, 1986
・G. Berry, ”The Constructive Semantics of Esterel”, 1995（ftp://ftp-sop.inria.fr/meije/esterel/papers/constructiveness.ps.gzで入手可能）
・前掲のT. Shiple, G. Berry and H. Touatiの文献
・前掲のShipleのPhD dissertation
を参照。この操作は、回路定義と変数の型から導出される連立固定点方程式に基づく。型がｋ個の値をとる変数の場合、これらのアルゴリズムは、各変数ごとにｋ個の評価集合を必要とする。さらに、算術演算の場合、固定点方程式は、型のすべての数の分割（＋の場合）または因数分解（＊の場合）から構成される。したがって、これらのアルゴリズムは、非ブール型の変数に対して実装するのはやや非効率的であり困難である。
【課題を解決するための手段】
【０００９】
本発明による定式化は、簡単な、非計算的な構成性の定義（Constructivity-SAT）と、新しい定式化に基づく、任意の有限型の変数に対して実装が簡単な記号アルゴリズムとを提示することによって、従来技術の限界を克服する。簡単な変換によって、値⊥（「ボトム」と読む）で拡張された変数型に関する、定義から導出された方程式集合の充足可能性として、構成性を再定式化することができることが示される。この定式化は、非計算的であり、任意の有限型の変数に容易に拡張可能である。また、この定式化は、同様にして、添字つき変数の定義も扱う。この構成性チェックはＣＯＳＰＡＮで実装された。ＣＯＳＰＡＮは、市販のFormalCheck検証ツールのための検証エンジンである。この実装は簡単であり、経験によれば、通常、無視しうるオーバーヘッドしか受けない。
【発明を実施するための最良の形態】
【００１０】
巡回的定義
記法：記法は一般に、E. W. Dijkstra and C. S. Scholten, ”Predicate Calculus and Program Semantics”, Springer Verlag, 1990、で使用されたスタイルに従う。関数適用は「．」で表し、右結合性である。例えば、ｆ．ｇ．ａはｆ．（ｇ．ａ）と解釈される。量化式および結合演算子を含む式は、（Ｑｘ：ｒ．ｘ：ｇ．ｘ）というフォーマットで書かれる。ただし、Ｑは量化記号（例えば、∀、∃）または結合演算子（例えば、＋、＊、ｍｉｎ、ｍａｘ、ｌｕｐ、ｇｌｂ）であり、ｘはダミー変数であり、ｒ．ｘはｘの変域であり、ｇ．ｘは式である。例えば、（∀ｘ  ｒ（ｘ）⇒ｇ（ｘ））は、（∀ｘ：ｒ．ｘ：ｇ．ｘ）と表され、（∃ｘ  ｒ（ｘ）∧ｇ（ｘ））は、（∃ｘ：ｒ．ｘ：ｇ．ｘ）と表され、Σi-0nｘｉは、（＋ｉ：ｉ∈［０，ｎ］：ｘ．ｉ）と表される。変域ｒが真であるか、または、文脈からわかるときには、それを落として（Ｑｘ：：ｇ．ｘ）と書く。証明は、同値または含意の連鎖として提示し、連鎖の各リンクに示唆を付す。
【００１１】
簡単のため、すべての変数が、単一の有限型Ｔ上で定義されているとみなす。演算子記号の語彙は有限集合Ｆで与えられる。Ｆ内の各記号は、自然数である対応するarityを有する。arity ｎの記号ｆは、関数ｆ＊：Ｔｎ→Ｔに対応し、arity ０の記号はＴの値に対応する。Ｆおよび変数Ｘの集合上の項は以下のように構成される。Ｘ内の変数は項であり、項ｔ．ｉ（ｉ∈［０，ｎ］）およびarity ｎの関数記号ｆに対して、ｆ．（ｔ．０，...，ｔ．（ｎ−１））は項である。
【００１２】
定義０（同時定義）。同時定義は、３項組（Ｅ，Ｘ，Ｙ）で指定される。ただし、ＸおよびＹは互いに素の（重複のない）変数の有限集合であり、Ｅは、ｙ：：＝ｔの形の式の集合である。ここで、ｙ∈Ｙであり、ｔはＸ∪Ｙ内の項であり、Ｙ内の各変数ごとにＥ内のただ１つの式があるようなものである。
【００１３】
定義の集合としての回路の初期の非公式的な記述では、Ｘは「外部」変数（自由入力およびラッチ）の集合であり、Ｙは「内部」変数（内部ゲート出力）の集合であるが、同時定義は、内部変数のみの定義を含むことに注意すべきである。同時定義は、Ｙ内の変数間に依存関係を引き起こす。それぞれの式ｙ：：＝ｔに対して、ｙは、ｔに現れる各変数に「依存する」。同時定義は、この依存関係がサイクルを含む場合に限り、統語論的に巡回的である。以下の例で、意味論的非巡回性の正確な概念を定式化する際のいくつかの微妙な点を例示する。
【００１４】
例０：統語論的非巡回性
外部変数集合は｛ｘ，ｙ｝であり、内部変数集合は｛ｐ，ｑ｝である。
ｐ：：＝ｘ∧¬ｙ
ｑ：：＝ｘ∨ｙ
ただし、∧は交わり（ＡＮＤ）演算を表し、∨は結び（ＯＲ）演算を表し、¬ｙはｙの否定を表す。これは統語論的に非巡回的である。従って、ｘおよびｙのあらゆる評価に対して、ｐおよびｑは一意的に定義された値を有する。
【００１５】
例１：統語論的巡回性、意味論的非巡回性
外部変数集合は｛ｘ，ｙ｝であり、内部変数集合は｛ｐ，ｑ｝である。
ｐ：：＝ｉｆ  ｘ  ｔｈｅｎ  ｙ  ｅｌｓｅ  ｑ
ｑ：：＝ｉｆ  ｘ  ｔｈｅｎ  ｐ  ｅｌｓｅ  ｘ
これは、統語論的に巡回的である（少し注意して解析すれば、ｐ：：＝ｑ  ｑ：：＝ｐという条件が生じうることがわかるから）。しかし、さらに注意深く解析すれば、ｘがｔｒｕｅ（真）である場合、この定義は次の非巡回的定義に簡単化されることがわかる。
ｐ：：＝ｙ
ｑ：：＝ｐ
同様に、ｘがｆａｌｓｅ（偽）のときも、簡単化された定義は非巡回的である。従って、外部変数ｘのそれぞれの設定は、統語論的巡回性を破る。
【００１６】
例２：意味論的巡回性
外部変数集合は｛ｘ，ｙ｝であり、内部変数集合は｛ｐ，ｑ｝である。
ｐ：：＝ｑ∧ｘ
ｑ：：＝ｐ
これは統語論的に巡回的である。ｘがｆａｌｓｅである場合、簡単化された定義は非巡回的であるが、ｘがｔｒｕｅのときは、次のように意味論的サイクルを表すものに簡単化される。
ｐ：：＝ｑ
ｑ：：＝ｐ
【００１７】
同時定義のもっともらしい意味論は、各式ｙ：：＝ｔを方程式ｙ＝ｔとして解釈し、この同時（連立）方程式の集合が、外部変数のそれぞれの評価に対して解を有する場合に、この定義が意味論的に非巡回的であると宣言することである。この意味論では、例０および１は意味論的に非巡回的であるが、例２も非巡回的になる。各入力評価に対して一意的な解が存在することを要求することによって、この状況を修正すればよいと思うかもしれないが、以下の例は、これもまた正しくないことを例示する。
【００１８】
例３：「一意解」判断基準の誤り
外部変数集合は｛ｘ，ｙ｝であり、内部変数集合は｛ｐ，ｑ｝である。
ｐ：：＝ｑ∧ｘ
ｑ：：＝ｉｆ  ｐ  ｔｈｅｎ  ¬ｑ  ｅｌｓｅ  ｆａｌｓｅ
これは、一意的な解ｐ＝ｆａｌｓｅ，ｑ＝ｆａｌｓｅを有する。従って、この定義は、ｘの各評価に対して一意的な解を有するのである。このように、「一意解」判断基準では、ｐ：：＝ｐ，ｑ：：＝¬ｑというサイクルが検出されないままとなる。
【００１９】
これらの例は、連立方程式に対する解による直接的な定式化は存在しないかもしれないことを示唆する。Berryは、Malikの定式化を拡張して、構成性(Constructivity)という条件を提案した。構成性は、上記の例で非公式的に実行された簡単化プロセスに基づいている。外部変数のそれぞれの評価に対して、定義の右辺を簡単化しようと試みる。定義ｙ：：＝ｔ内の項ｔが定数ａに簡単化される場合、現在の評価はｙ＝ａで拡張され、定義ｙ：：＝ｔは除去される。この簡単化は、現在未定義の変数の値とは無関係に現在の評価によって結果が定義される場合に制限される。例えば、現在の評価が｛ｘ＝ｆａｌｓｅ｝である場合、「ｉｆ  ｘ  ｔｈｅｎ  ｙ  ｅｌｓｅ  ｚ」はｚに簡単化され、ｘ∧ｙはｆａｌｓｅに簡単化されるが、ｙ∨¬ｙはｔｒｕｅには簡単化されない。Berryは、このプロセスが、簡単化ステップが適用される順序とは独立に一意的な結果を生成することを示している。構成性の適切さは、Shipleの論文(PhD dissertation)に示されている。そこでは、構成的定義が、上に有界な慣性遅延モデル（J. A. Brzozowski and C-J. H. Seger, ”Asynchronous Circuits”, Springer Verlag, 1994、を参照）において、任意の遅延値の割当てに対して、まさに電気的に正しく動作するものであることが示されている。Malikは、意味論的巡回性を検出する問題はＮＰ完全であることを示している。
【００２０】
定義１（Constructivity）。同時定義は、外部変数のそれぞれの評価に対して、簡単化プロセスが定義の空集合を導く場合に限り、意味論的に非巡回的である。
【００２１】
充足可能性としての構成性
われわれの新しい定式化を導く簡単化プロセスの別の見方がある。簡単化は、外部変数のもとの評価の「極大」（この評価では定義集合をさらに簡単化することができないという意味で極大）拡張を計算する固定点プロセスとみなされる。MalikおよびShipleによって用いされた構成性をチェックするアルゴリズムは、この固定点定式化を使用する。後述の定理１によれば、この固定点定式化を充足可能性の問題に書き直すことが可能である。この観察から、非ブール型に拡張される構成性の簡単なアルゴリズムを開発することに導かれる。
【００２２】
固定点プロセスとして簡単化を定式化するため、Scottの完全半順序（ＣＰＯ：Complete Partial Order）の理論からのいくつかの周知の概念を必要とする（D. S. Scott, ”A type-theoretical alternative to CUCH, ISWIN, OWHY”, Unpublished notes, Oxford, 1969, published in Theoretical Computer Science, 1993、を参照）。型Ｔは、新しい要素⊥（ボトムと読む）で拡張されて、型Ｔ⊥を形成する。Ｔ⊥は、半順序◇を備える。この半順序は、ａ＝ｂまたはａ＝⊥である場合に限りａ◇ｂ、によって定義される。注意すべき点であるが、◇はＣＰＯである（◇に関して単調増大であるあらゆる要素列は最小上界（ｌｕｂ：least upper bound）を有する）。２つの要素ａ、ｂの最大下界（ｇｌｂ：greatest lower bound）は、
ｇｌｂ．（ａ，ｂ）＝ｉｆ  ａ≠ｂ  ｔｈｅｎ  ⊥  ｅｌｓｅ  ａ
として定義される。｜ｕ｜＝｜ｖ｜∧（∀ｉ：：ｕ．ｉ◇ｖ．ｉ）である場合に限りｕ⊆ｖ（「ｕはｖより小さい」と読む）、によって、順序◇は、Ｔ⊥上のベクトルに各点ごとに拡張される。この順序は、Ｔ⊥上のベクトルの集合に関してＣＰＯである。最大下界もまた、同じ長さのベクトルに関して各点ごとに定義される。すなわち、あらゆるｉに対して、ｗ．ｉ＝ｇｌｂ．（ｕ．ｉ，ｖ．ｉ）である場合、ｇｌｂ．（ｕ，ｖ）＝ｗである。
【００２３】
Ｆ内の各関数記号ｆに対して、ｆ⊥は、ＴではなくＴ⊥への適用を示す同じarityの記号である。Ｔ⊥上のｆ⊥の解釈ｆ⊥*は、ｆ*を拡張した関数であるはずであり、順序⊆に関して単調である。すなわち、ｆ⊥のarityの長さのベクトルｕ、ｖに対して、ｕ⊆ｖはｆ⊥*．ｕ⊆ｆ⊥*．ｖを含意する。順序⊆および単調性条件は、⊥の非公式の記述を「未定義」値としてエンコードする。すなわち、ｖがｕ「よりも定義されている」場合、ｆ⊥*．ｖはｆ⊥*．ｕ「よりも定義されている」はずである。項ｔの拡張はｔ⊥によって表され、項の構造に基づいて再帰的に定義される。すなわち、（ｘ）⊥＝ｘであり、（ｆ．（ｔ．０，...，ｔ．（ｎ−１）））⊥＝ｆ⊥．（ｔ⊥．０，...，ｔ⊥．（ｎ−１））である。拡張された項の解釈もまた⊆に関して単調であることを示すことは簡単である。ＣＰＯ上のあらゆる単調関数は最小固定点を有する。
【００２４】
ここで、簡単化プロセス中に構成される部分評価は、Ｘ∪ＹからＴ⊥への全関数として表すことができる。ただし、現在未定義の変数には値⊥が与えられる。初期評価Ｖは、ＸをＴの中に写像し、Ｙを｛⊥｝に写像する関数である。各ステップで、ある非決定論的に選択される関数ｙ：：＝ｔに対して、現在の評価ＶはＶ．［ｙ←ｔ⊥＊．Ｖ］に更新される。文献
・H. Bekic, ”Definable operations in general algebra, and the theory of automata and flowcharts”, Technical Report, IBM, 1969, reprinted in ”Programming Languages and Their Definitions”, LNCS 177, 1984 
・P. Cousot, ”Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice (rapport de recherche r.r. 88), Technical report, Laboratoire IMAG, Universite scientifique et medicale de Grenoble, 1978
により提示された議論によって、単調性に基づいて、この非決定論的プロセスは、導出された方程式の集合の同時最小固定点である評価｛ｙ＝ｔ⊥*｜（ｙ：：＝ｔ）∈Ｅ｝で終了する。同時定義Ｃ＝（Ｅ，Ｘ，Ｙ）に対して、この最小固定点(least fixpoint)を（ｌｆｐ  Ｙ：Ｅ*．（Ｘ，Ｙ））で表す。この固定点は、Ｘの各評価に依存し、各評価ごとに定義される。ここで、構成性定義を次のようにあらためて述べることができる。
【００２５】
定義２（Constructivity-FIX）。同時定義（Ｅ，Ｘ，Ｙ）は、各初期評価Ｖに対してベクトル（ｌｆｐ  Ｙ：Ｅ＊．（Ｖ，Ｙ））が⊥成分を有しない場合に限り、意味論的に非巡回的である。
【００２６】
Ｔ⊥上のベクトルｖに対して、述語∀ｉ：：ｖ．ｉ≠⊥を⊥ｆｒｅｅ．ｖで表す。構成性条件は、ちょうど（∀ｖ：⊥ｆｒｅｅ．ｖ：⊥ｆｒｅｅ．（ｌｆｐ  Ｙ：Ｅ＊．（ｖ，Ｙ）））である。Malikは、内部変数の集合Ｙが「出力」変数の部分集合Ｗを有するような、より弱い条件をチェックしている。述語（∀ｉ：ｉ∈Ｗ：ｖ．ｉ≠⊥）をｏｕｔｐｕｔ⊥ｆｒｅｅ．ｖで表す。Malikの条件は、（∀ｖ：⊥ｆｒｅｅ．ｖ：ｏｕｔｐｕｔ∀ｆｒｅｅ．（ｌｆｐ  Ｙ：Ｅ＊．（ｖ，Ｙ）））と表すことができる。
【００２７】
Constructivity-FIX条件を、各初期評価ごとに独立にチェックすることは非効率的である。Malik、Berry、TouatiおよびShipleは、外部評価の集合に作用する導出された方式を用いている。型Ｔがｋ個の要素を有する場合、この方式は、Ｙ内の各変数ｙにｋ個の部分集合を関連づける。集合ｙ．ｉ（ｉ∈［０，ｋ］）は、変数ｙがｉと評価される外部評価を含む。これらの部分集合は、基本演算の意味論から導出される集合演算によって更新される。例えば、定義「ｘ：：＝ｙ∧ｚ」に対して、更新は、ｘ．ｆａｌｓｅ＝ｙ．ｆａｌｓｅ∪ｚ．ｆａｌｓｅ、およびｘ．ｔｒｕｅ＝ｙ．ｔｒｕｅ∩ｚ．ｔｒｕｅによって与えられる。
【００２８】
この方式は、非ブール型の場合に生じる２つの制限を有する。（ｉ）アルゴリズムは、各変数ごとにｋ個の集合を維持しなければならない。（ｉｉ）必要な集合演算は、基本演算が（有界な）算術を含むときにはきわめて複雑になる可能性がある。例えば、定義ｘ：：＝ｙ＋ｚに対して、ｘ．ｋは、ｋをｌ＋ｍとするさまざまな分割に対するｙ．ｌ＋ｚ．ｍとして定義されることになる。同様に、ｘ：：＝ｙ*ｚに対して、ｘ．ｋは、ｋをｌ＊ｍとするさまざまな因数分解に対するｙ．ｌ＊ｚ．ｍとして定義されることになる。われわれの新しい定式化Constructivity-SATは、Constructivity-FIXを充足可能性問題に変え、これらの問題点を回避する。
【００２９】
この新しい定式化は、Constructivity-FIXの定義を強化して、Ｅ＊のあらゆる固定点が⊥ｆｒｅｅであることを要求する。２つの定式化の同値性は定理１で示される。
【００３０】
定義３（Constructivity-SAT）。同時定義（Ｅ，Ｘ，Ｙ）は、（∀ｖ，ｕ：⊥ｆｒｅｅ．ｖ∧ｕ＝Ｅ*．（ｕ，ｖ）：⊥ｆｒｅｅ．ｕ）である場合に限り、意味論的に非巡回的である。
【００３１】
補題０。あるＣＰＯ⊆上の単調属性Ｐおよび単調関数ｆに対して、（∀ｕ：ｕ＝ｆ．ｕ：Ｐ．ｕ）である場合に限り、Ｐ．（ｌｆｐ  Ｘ：ｆ．Ｘ）である。
【００３２】
証明。
Ｐ．（ｌｆｐ  Ｘ：ｆ．Ｘ）⇔（∀ｕ：ｕ＝ｆ．ｕ：Ｐ．ｕ）
の右から左への含意は自明に真である。（ｌｆｐ  Ｘ：ｆ．Ｘ）は、条件ｕ＝ｆ．ｕを満たすからである。逆向きについて、ｆの固定点は、⊆による半順序を有し、最小固定点は他のいかなる固定点より小さいことに注意する。Ｐの単調性より、Ｐが最小固定点に対して成立すれば、Ｐはあらゆる固定点に対して成立する。
【００３３】
定理１。Constructivity-FIXとConstructivity-SATは同値である。
【００３４】
証明。任意の同時定義Ｃ＝（Ｅ，Ｘ，Ｙ）に対して、
ＣがConstructivity-FIXを満たす
≡  （∀ｖ：⊥ｆｒｅｅ．ｖ：⊥ｆｒｅｅ．（ｌｆｐ  Ｙ：Ｅ＊．（ｖ，Ｙ）））  （定義より）
≡  （∀ｖ：⊥ｆｒｅｅ．ｖ：（∀ｕ：ｕ＝Ｅ＊．（ｖ，ｕ）：⊥ｆｒｅｅ．ｕ））  （⊥ｆｒｅｅは⊆に関して単調；補題０）
≡  （∀ｖ，ｕ：⊥ｆｒｅｅ．ｖ∧ｕ＝Ｅ＊．（ｖ，ｕ）：⊥ｆｒｅｅ．ｕ）  （書き換え）
≡  ＣがConstructivity-SATを満たす  （定義より）
【００３５】
関数ｆのＴnからＴn⊥への拡張は、一般に次のように定義することができる。ベクトルｖにおけるこの拡張の値は、順序においてｖより大きい⊥ｆｒｅｅベクトルにおける関数値の最大下界である。形式的には、
ｆ＊⊥．ｖ＝（ｇｌｂ  ｗ：⊥ｆｒｅｅ．ｗ∧ｖ⊆ｗ：ｆ＊．ｗ）
である。これがｆの単調な拡張であることを示すのは簡単である。基本算術関数およびブール関数の拡張は、この公式によって容易に決定される。例えば、∧の拡張は次のように与えられる。
ｕ∧⊥ｖ＝
ｆａｌｓｅ    ｕ＝ｆａｌｓｅまたはｖ＝ｆａｌｓｅの場合
⊥            上記以外で、ｕ＝⊥またはｖ＝⊥の場合
ｕ∧ｖ        上記以外の場合
【００３６】
この一般的定式化を例証するために、次のチェックをする。
ｕ∧⊥ｆａｌｓｅ
＝  （ｇｌｂ  ｘ，ｙ：ｘ≠⊥∧ｙ≠⊥∧ｕ◇ｘ∧ｆａｌｓｅ◇ｙ：ｘ∧ｙ）  （一般的定式化より）
＝  （ｇｌｂ  ｘ：ｘ≠⊥∧ｕ◇ｘ：ｘ∧ｆａｌｓｅ）  （◇の定義より）
＝  （ｇｌｂ  ｘ：ｘ≠⊥∧ｕ◇ｘ：ｆａｌｓｅ）  （∧の定義より）
＝  ｆａｌｓｅ  （ｇｌｂの定義より）
【００３７】
＊の拡張は、ｆａｌｓｅの代わりに０とすれば、∧の拡張と同様である。＋の拡張は次のように与えられる。
ｕ＋⊥ｖ＝
⊥        ｕ＝⊥またはｖ＝⊥の場合
ｕ＋ｖ    上記以外の場合
他の基本演算子の拡張も同様に容易に定義することができ、本明細書の末尾の付録に示すとおりである。このように、この新しい定式化によれば、従来の定式化のいずれの制限をも克服する。この拡張は定義および計算が容易であり、各変数ごとに評価の集合を維持する必要がない。必要な変更は、変数の型および基本演算子の定義の両方を拡張することだけである。
【００３８】
ＣＯＳＰＡＮシステムのＳ／Ｒ言語を含む多くの入力言語においては、変数の配列を宣言することが可能である。ｚがこのような配列変数である場合、ｚ［ｃ］：：＝ｔ（ただし、ｃは定数）の形の定義は、ｚ［ｃ］を通常の変数として扱うことによって、上記の方法で処理することができる。しかし、ｚ［ｅ］：：＝ｔ（ただし、ｅは非定数項）の形の定義は、上記の方法では処理することができない。これは、定義の集合｛ｚ［ｃ］：：＝ｉｆ  （ｅ＝ｃ）  ｔｈｅｎ  ｔ｜ｃ∈ｉｎｄｉｃｅｓ（ｚ）｝に対応するからである。注意すべき点であるが、項
ｉｆ  （ｅ＝ｃ）  ｔｈｅｎ  ｔ
は部分関数である。代表的な例として、以下の定義を考える。ただし、ｚは｛０，１｝を添字とする配列であり、ｘおよびｙは変数である。
ｚ［ｘ］：：＝ａ
ｚ［ｙ］：：＝ｂ
Ｓ／Ｒの意味論は、ｘおよびｙの評価が別個であることを要求する。ｚ［０］に対する定義項は、部分関数
ｉｆ  ｘ＝０  ｔｈｅｎ  ａ  ｅｌｓｅ  ｉｆ  ｙ＝０  ｔｈｅｎ  ｂ
である。この項は、これ自体、ｘ＝０かつｙ＝０に対してのみ定義されるＴ⊥上の部分関数とみなすことが可能である。この解釈では、これは◇に関して単調である。（部分関数ｆが半順序◇に関して単調であるのは、ｘ◇ｙのとき、ｆがｘで定義され、ｆがｙで定義され、ｆ．ｘ◇ｆ．ｙである場合であり、この場合に限る。）ｚ［０］およびｚ［１］に対する項を再び組み合わせると、ｚ［ｘ］およびｚ［ｙ］に対するもとの定義の、（Ｔ⊥に対する）次の修正が得られる。
ｚ［ｘ］：：＝ｉｆ  ｘ≠⊥  ｔｈｅｎ  ａ
ｚ［ｙ］：：＝ｉｆ  ｙ≠⊥  ｔｈｅｎ  ｂ
これらの定義は、以下のようにして、引き起こされた「方程式」に寄与する。
ｘ≠⊥⇒（ｚ［ｘ］＝ａ）
ｙ≠⊥⇒（ｚ［ｙ］＝ｂ）
【００３９】
実装
われわれは、ＣＯＳＰＡＮ／FormalCheck検証システムにおいてこの新たな定式化を実装した。ＣＯＳＰＡＮシステムに対する入力言語は、K. Katzenelson and R. P. Kurshan, ”S/R: A language for specifying protocols and other coodinating processes”, Proc. IEEE Conf. Comput. Comm., pp.286-292, 1986、に記載されているＳ／Ｒ(”selection/resolution”)である。Ｓ／Ｒプログラムは、Rabin/Streett型の受容条件を有するミーリー機械とみなすことが可能ないくつかのプロセスからなる。各プロセスの変数は、状態変数または選択変数のいずれかである。さらに、選択変数は、システムの次状態関係を決定するために用いられる自由（非制約）入力または組合せ変数のいずれかである。上で用いた用語において、状態変数は、自由変数とともに、「外部」変数を形成する。入力および状態変数は、選択サイクルの期間中に値を変えないからである。他の選択変数は「内部変数」を形成する。
【００４０】
Ｓ／Ｒには、選択変数間の依存関係に対する制限はない。あるプロセス内で宣言された選択変数は、相互に依存することが可能であり、また、他のプロセスへの入力として使用可能であるため、潜在的に、プロセス境界にまたがる統語論的サイクルを導入する可能性がある。さらに、意味論的サイクルの存在は、状態変数の評価に依存する可能性がある。例えば、意味論的サイクルは、それが引き起こされる特定の状態が到達不能である場合、「到達不能」である可能性がある。そこで、問題は、ある自由入力評価に対して、意味論的サイクルが、プログラムの到達可能状態に存在するかどうかを識別することである（この問題は、Shipleの論文(PhD dissertation)ではＰＳＰＡＣＥ完全であることが示されている）。
【００４１】
Ｓ／Ｒコンパイラは、プログラムをパースし、内部変数間の統語論的依存関係を解析する。統語論的サイクルがある場合、消去により各統語論的サイクルが切れることになる内部変数の集合を識別する。このような集合を一般に「フィードバック頂点集合」(feedback vertex set)という。パーサは、それらの変数をフィードバック頂点集合に保持し、他の変数をマクロ展開して、フィードバック頂点集合内の変数がそれらの変数自身および入力変数で定義され、それらの定義項が、解析されるべき同時定義を形成するようにする。これらの内部変数を「関連」(relevant)変数ということにする。
【００４２】
われわれの実装は、単一のＭＴＢＤＤ終端を用いて⊥を表現する。乗算に対するＭＴＢＤＤのビット数は指数関数的であるが、他のほとんどの演算を効率的に表現するため、ＣＯＳＰＡＮで使用される。関連変数の型は、⊥終端を含むように拡張される。入力および状態変数の型は拡張されない。この実装は、本明細書で定義されるような拡張された基本演算子のライブラリを含む。これは、ブール演算子、＋、*、ｄｉｖ、ｅｘｐ、ｍｏｄのような算術演算子、および、ｉｆ−ｔｈｅｎ−ｅｌｓｅのような条件演算子を含む、Ｓ／Ｒの基本演算子を拡張する。
【００４３】
添字なしの関連変数の各定義ｘ：：＝ｔは、方程式ｘ＝ｔ＊⊥に変換され、添字つき変数の定義ｚ［ｅ］：：＝ｔは、上記のように、（ｅ＊⊥≠⊥）⇒（ｚ［ｅ＊⊥］＝ｔ＊⊥）に変換される。さらに説明すると、回路定義ｘ：：＝Ａ∧Ｂは、ｘ：：＝Ａ⊥∧⊥Ｂ⊥に変換され、回路定義ｚ［ｊ］＝Ａ（ただし、ｊは単なるダミー変数）は、ｚ［ｊ］＝Ａ⊥に変換されるが、回路定義ｚ［ｘ］＝Ａ（ただし、ｘは変数）は、（ｘ⊥≠⊥）⇒（ｚ［ｘ⊥］＝Ａ⊥）に変換される。これらの公式の連結が、同時固定点項Ｙ＝Ｅ＊．（Ｓ，Ｘ，Ｙ）を形成する。ただし、Ｓは状態変数の集合であり、Ｘは自由入力変数の集合であり、Ｙは関連変数の集合である。Constructivity-SAT公式は、状態変数に関する次の述語を（否定により）決定する。
Ｃｙｃｌｉｃ．Ｓ＝（∃Ｘ，Ｙ：：Ｙ＝Ｅ＊．（Ｓ，Ｘ，Ｙ）∧¬⊥ｆｒｅｅ．Ｙ）
【００４４】
述語¬Ｃｙｃｌｉｃは、到達可能性解析中に不変性がチェックされる。これが失敗した場合、システムは自動的に、初期状態から、Ｃｙｃｌｉｃ．ｓが真であるような状態ｓ間でのエラートラックを生成する。（Ｙ＝Ｅ*．（ｓ，ｋ，Ｙ）∧¬⊥ｆｒｅｅ．Ｙ）に対するＢＤＤを調べることによって、状態ｓにおける特定の入力ｋに対する意味論的サイクルに関係する変数の集合を回復することは困難ではない。１−ノードへのあらゆるパスは、値⊥を有する変数を含む。これらの変数は意味論的サイクルに関係する。
【００４５】
図１は、本発明の方法の流れ図である。ブロック１０で、巡回性をテストすべき与えられた回路を表現する方程式の集合を得る。ブロック２０で、この集合の方程式内の変数のうち、（外部ソースから、または、クロックされる遅延要素から入力される信号に対応する変数ではなく）回路の内部変数に対応する各変数を、⊥を含むように型が拡張された変数で置き換える。ブロック３０で、連立方程式の集合を有効に解く通常の方程式ソルバに、得られた方程式の集合を入力する。しかし、実際の解が得られる必要はない。むしろ、解において、いずれかの変数が値⊥をとることになるかどうかの結論が得られなければならない。いずれかの変数が値⊥をとる場合、回路は統語論的巡回性を含むと結論される。ブロック３０の方程式ソルバは、公知の市販のソルバとすることが可能である。われわれは、ＣＯＳＰＡＮにおけるＢＤＤ(Binary Decision Diagram) Satisfaction Checkerを使用したが、カーネギー・メロンにより提供されているＢＤＤパッケージや、コロラド大学により提供されているＢＤＤパッケージのような他のパッケージも存在する。なお、ソルバパッケージによっては、２値変数用にのみ設計されているものもあるかもしれない。しかし、このようなパッケージは、単に各変数を２個の変数で置き換えることにより、型定義に値⊥を含める追加自由度を得ることによって、図１の方法とともに使用可能である。
【００４６】
付録
この付録は、Ｓ／Ｒの拡張された基本演算子の定義を含む。
【００４７】
ブール演算子：
ｕ∧⊥ｖ＝
ｆａｌｓｅ    ｕ＝ｆａｌｓｅまたはｖ＝ｆａｌｓｅの場合
⊥            上記以外で、ｕ＝⊥またはｖ＝⊥の場合
ｕ∧ｖ        上記以外の場合
ｕ∨⊥ｖ＝
ｔｒｕｅ    ｕ＝ｔｒｕｅまたはｖ＝ｔｒｕｅの場合
⊥          上記以外で、ｕ＝⊥またはｖ＝⊥の場合
ｕ∨ｖ      上記以外の場合
¬⊥ｕ＝
⊥      ｕ＝⊥の場合
¬ｕ    上記以外の場合
【００４８】
算術演算子：
ｕ＋⊥ｖ＝
⊥        ｕ＝⊥またはｖ＝⊥の場合
ｕ＋ｖ    上記以外の場合
ｕ＊⊥ｖ＝
０        ｕ＝０またはｖ＝０の場合
⊥        上記以外で、ｕ＝⊥またはｖ＝⊥の場合
ｕ＊ｖ    上記以外の場合
ｕ  ｄｉｖ⊥  ｖ＝
０                ｕ＝０の場合
⊥                上記以外で、（ｕ＝⊥かつｖ≠０）またはｖ＝⊥の場合
ｕ  ｄｉｖ  ｖ    上記以外の場合
ｕ  ｍｏｄ⊥  ｖ＝
０                ｕ＝０またはｖ＝１の場合
⊥                上記以外で、（ｕ＝⊥かつｖ≠０）またはｖ＝⊥の場合
ｕ  ｍｏｄ  ｖ    上記以外の場合
ｕ  ｅｘｐ⊥  ｖ＝
０                ｕ＝０の場合
１                上記以外で、ｕ＝１またはｖ＝０の場合
⊥                上記以外で、ｕ＝⊥またはｖ＝⊥の場合
ｕ  ｅｘｐ  ｖ    上記以外の場合
【００４９】
比較演算子：
ｕ＜⊥ｖ＝
⊥        ｕ＝⊥またはｖ＝⊥の場合
ｕ＜ｖ    上記以外の場合
ｕ≦⊥ｖ＝
⊥        ｕ＝⊥またはｖ＝⊥の場合
ｕ≦ｖ    上記以外の場合
ｕ＝⊥ｖ＝
⊥        ｕ＝⊥またはｖ＝⊥の場合
ｕ＝ｖ    上記以外の場合
【００５０】
条件演算子：
（ｉｆ  ｃ  ｔｈｅｎ  ｕ  ｅｌｓｅ  ｖ）⊥＝
ｕ    ｃ＝ｔｒｕｅの場合
ｖ    上記以外で、ｃ＝ｆａｌｓｅの場合
ｕ    上記以外で、ｃ＝⊥かつｕ＝ｖの場合
⊥    上記以外で、ｃ＝⊥かつｕ≠ｖの場合
（ｉｆ  ｃ  ｔｈｅｎ  ｕ）⊥＝
ｕ    ｃ＝ｔｒｕｅの場合
【００５１】
［発明の効果］
以上述べたごとく、本発明によれば、簡単な、非計算的な構成性の定義（Constructivity-SAT）と、新しい定式化に基づく、任意の有限型の変数に対して実装が簡単な記号アルゴリズムとによって、回路定義における従来技術の限界が克服される。
【図面の簡単な説明】
【００５２】
【図１】本発明の方法の流れ図である。
【図１】
2006209787.tif 000004
【手続補正書】
【提出日】平成18年5月11日(2006.5.11)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
巡回動作用の回路を評価するための、コンピュータにより処理される方法であって、該回路がこの回路中のゲートを指定する定義の集合の言葉で指定されており、該定義が１つもしくは複数個の変数により特徴づけられているような方法において、
該定義の集合内の複数の変数のうちの少なくとも一部の変数を、コンピュータ内の演算手段によって⊥値を含む変数型に変換することにより、該定義の集合を通る単一のパス中に修正された定義の集合を形成するステップと、
該修正された定義の集合の解が、値が⊥の変数を含むかどうかを該コンピュータ内の判定手段によって確認するステップと、
該確認するステップの結果に基づいて、評価中の回路が構成的な回路であるかどうかについての指示を該コンピュータ内の出力手段によって出力するステップと、
を有することを特徴とする方法。
【請求項２】
前記確認するステップは、前記修正された定義の集合によって表される連立方程式集合を解くことによって実行されることを特徴とする請求項１に記載の方法。
【請求項３】
前記変数のうちの少なくとも１つが値⊥を有することが前記解から明らかになったときに、巡回性条件を報告するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項４】
前記少なくとも一部の変数は、内部変数に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項５】
前記少なくとも一部の変数は、外部変数以外に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項６】
前記外部変数は、入力変数およびクロックされる遅延要素に対応することを特徴とする請求項５に記載の方法。
【請求項７】
回路の使用から前記定義の集合を生成するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項８】
ｘを内部変数とし、Ａを別の内部変数とし、ｚを添字つき変数として、型の定義（ｚ［ｘ］＝Ａ）が、
【数１】
2006209787.tif 000005
に変換されることを特徴とする請求項１に記載の方法。
【手続補正書】
【提出日】平成18年5月18日(2006.5.18)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
巡回動作用の回路を評価するための、コンピュータにより処理される方法であって、該回路がこの回路中のゲートを指定する定義の集合の言葉で指定されており、該定義が１つもしくは複数個の変数により特徴づけられているような方法において、
該定義の集合内の複数の変数のうちの少なくとも一部の変数を、コンピュータ内の演算手段によって⊥値を含む変数型に変換することにより、該定義の集合を通る単一のパス中に修正された定義の集合を形成するステップと、
該修正された定義の集合の解が、値が⊥の変数を含むかどうかを該コンピュータ内の判定手段によって確認するステップと、
該確認するステップの結果に基づいて、評価中の回路が構成的な回路であるかどうかについての指示を該コンピュータ内の出力手段によって出力するステップと、
を有することを特徴とする方法。
【請求項２】
巡回動作用の回路を評価する方法に関するプログラムを記録したコンピュータ読み取り可能な記録媒体であって、該回路がこの回路中のゲートを指定する定義の集合の言葉で指定されており、該定義が１つもしくは複数個の変数により特徴づけられているような記録媒体において、
コンピュータに、
該定義の集合内の複数の変数のうちの少なくとも一部の変数を、コンピュータ内の演算手段によって⊥値を含む変数型に変換することにより、該定義の集合を通る単一のパス中に修正された定義の集合を形成するステップと、
該修正された定義の集合の解が、値が⊥の変数を含むかどうかを該コンピュータ内の判定手段によって確認するステップと、
を実行させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項３】
該確認するステップの結果に基づいて、評価中の回路が構成的な回路であるかどうかについての指示を該コンピュータ内の出力手段によって出力するステップと、
前記確認するステップは、前記修正された定義の集合によって表される連立方程式集合を解くことによって実行されることを特徴とする請求項１に記載の方法。
【請求項４】
前記変数のうちの少なくとも１つが値⊥を有することが前記解から明らかになったときに、巡回性条件を報告するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項５】
前記少なくとも一部の変数は、内部変数に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項６】
前記少なくとも一部の変数は、外部変数以外に対応する前記変数の部分集合を形成することを特徴とする請求項１に記載の方法。
【請求項７】
前記外部変数は、入力変数およびクロックされる遅延要素に対応することを特徴とする請求項５に記載の方法。
【請求項８】
回路の使用から前記定義の集合を生成するステップをさらに有することを特徴とする請求項１に記載の方法。
【請求項９】
ｘを内部変数とし、Ａを別の内部変数とし、ｚを添字つき変数として、型の定義（ｚ［ｘ］＝Ａ）が、
【数１】
2006209787.tif 000006
に変換されることを特徴とする請求項１に記載の方法。