(57)【特許請求の範囲】
【請求項１】
同期式順序回路の動作を表す有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑのある部分集合ｐにおいて、ｐ内のある状態から出発し永遠にｑから外に出ない状態遷移のパスが存在するか否かを判定する論理検証装置であって、
前記有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ａ［ｉ］が入力された場合に、Ｍにおけるａ［ｉ］の像計算及びその結果とｑとの集合積演算によって集合ａ［ｉ＋１］を求める計算手段と、
前記集合ｐの部分集合あるいはｐ全体をａ［０］として、前記計算手段を繰り返し適用することでａ［１］、ａ［２］、ａ［３］、・・・を求め、空でない集合ａ［ｋ］がその後のｎ個の集合ａ［ｋ＋１］、ａ［ｋ＋２］、・・・ａ［ｋ＋ｎ］の和集合に対して部分集合になっているような自然数ｋが存在するか否かを判定する判定手段と、
前記判定手段を満足する前記集合ｐがある場合は、永遠にｑから外に出ない状態遷移のパスが存在する旨を出力する出力手段と、
を備えていることを特徴とする論理検証装置。
【請求項２】
前記判定手段は、状態集合ｐから開始して、状態集合分割と前記計算手段の繰り返し適用を深さ優先で再帰的に行うことを特徴とする請求項１記載の論理検証装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、有限状態機械で機能仕様が与えられた論理装置のモデルが、機能仕様を満たしているか否かを検証する論理検証装置に関する。
【０００２】
有限状態機械は、同期式順序機械やプロトコルの数学的モデルとして広く利用されており、同期式順序回路やプロトコルの検証方法にも関連する。論理装置の機能設計が仕様を正しく実現しているか否かの検証手法として、モデル検査手法が知られている（参考文献２、５参照）。これは有限状態機械が時相論理で表現された仕様を満足する／しないことを数学的に証明するものである。
【０００３】
前記モデル検査手法による論理装置の検証作業は、抽象的な仕様に関する検証作業から現実の回路の動作に関する検証作業まで、様々な段階から構成されている。これらの段階の内、機能仕様の検証は論理装置の最も早い段階における誤り検出が期待できるため、迅速、かつ確実な検証処理を行うことが要望されていた。また、前記検証処理を行う際、一般の方法ではメモリ容量が限界に達するような複雑な論理装置に対しても、検証が実行できるようにすることが要望されていた。
【０００４】
【従来の技術】
以下、従来の技術について説明する。
§１：従来技術の説明（その１）
前記有限状態機械とは、出力を持つ有限オートマトンとして定義される。有限状態機械の一般形式は次の式（１）  で与えられる。
【０００５】
Ｍ＝（Ｑ，Σ，Φ，δ，λ，Ｉ）・・・式（１）
前記各記号の意味は次の通りである。
Ｑ：状態の集合（有限）
Σ：入力アルファベット（有限）
Φ：出力アルファベット（有限）
δ：遷移関係式
λ：出力関係式
Ｉ：初期状態集合
前記遷移関係式δは、次の状態を決める関数であるが、非決定的な遷移を表現するために、現状態、次状態、入力が与えられたときに、現状態でその入力が与えられたときに次状態に遷移する場合があれば、値として１、なければ０を取るような関数である。なお、遷移が決定的である場合には、現状態、入力から次状態を求める関数として状態遷移を表すことが可能になる。前記出力関係式λも同様に出力が非決定的な場合に対応する。
【０００６】
原則的に、全ての同期式順序回路は有限状態機械でモデル化できる。このため、論理装置を設計する際に、仕様として有限状態機械を用いる方法が広く用いられている。例えば、論理合成においては、装置の仕様を設計記述言語で書いた後、合成システムでその記述を有限状態機械に変換し、状態をフリップフロップ回路やレジスタで、遷移関係式δや出力関係式λを組み合わせ回路で実現する方法が一般的である。
【０００７】
なお、前記有限状態機械の基礎理論に関しては、参考文献６の第２章で詳しく論じられている。有限状態機械を仕様とする装置の検証とは、装置が有限状態機械の状態遷移を正しく実現しているかどうかを調べることである。この目的で用いられる技術としては、論理シミュレーションと形式的検証を挙げることができる。
【０００８】
前記論理シミュレーションとは、装置のモデル（設計記述言語による記述、ゲートレベルの回路図など）に対して、適当な入力を加えて動作を模擬する処理である。この際に得られる出力が元の有限状態機械から得られる値と一致することを確認する。
【０００９】
前記形式的検証とは、元の有限状態機械が満たしている性質（プロパティ）を装置のモデルが満たしているかどうかを数学的に証明するアプローチである。代表的な例として、記号モデル検査、記号シミュレーションなどが知られている。形式的検証に関しては、参考文献５、参考文献３、参考文献１１、参考文献１３、参考文献８に詳しく述べられている。
【００１０】
前記形式的検証（形式的検証手法）は、現在研究段階から実用段階に向かいつつある技術であり、プロセッサの設計検証に利用した事例が報告されている。中でも制御論理の検証で記号モデル検査手法（参考文献２を参照）が最も実用に近いと考えられている。
【００１１】
§２：従来技術の説明（その２）・・・図１１参照
図１１は従来技術の説明図１であり、有限状態機械の例を示す。前記形式的検証手法の内、記号モデル検査手法は、Ｋｒｉｐｋｅ構造の論理装置モデルを論理関数を用いて表現し、計算木論理（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ  ：ＣＴＬ  ）で表された仕様を満足する空でない状態集合が存在するか否かを検査することにより、論理装置のモデルが仕様を満足するか否かを検証する手法である。
【００１２】
ここで、Ｋｒｉｐｋｅ構造とは、状態の有限集合Ｓと、状態の遷移関係Ｒと、初期状態点の集合Ｓ０  と、各状態で真となる原始命題の集合Ｌとを用いて、次の式（２）  のように表される非決定的有限オートマトンの一種である。
【００１３】
Ｋ＝（Ｓ，Ｒ，Ｓ０  ，Ｌ）・・・式（２）
また、計算木論理は、時相論理の一種であり、通常の論理演算子に加えて、全称を表す演算子Ａ、存在を表す演算子Ｅとともに、「いつか」を表す時相演算子Ｆ、「いつも」を表す時相演算子Ｇ、「次に」を表す時相演算子Ｘ、及び「まで」を表す時相演算子Ｕを用いて表される。
【００１４】
例えば、時相演算子ＡＧａは、初期状態から到達可能な状態集合の全てにおいて論理式ａが成立する旨を示している。この場合は、論理装置のモデルにおいて、初期状態から遷移可能な全ての道筋を辿っていき、その道筋の全てが論理式ａが成立している状態に辿り着くか否かを調べれば良い。
【００１５】
すなわち、記号モデル検査手法における検証作業は、Ｋｒｉｐｋｅ構造の状態遷移を辿り、各状態において、仕様を表す計算木論理式が成立するかを確認する作業であり、この作業は、計算木論理の式を用いたモデル上の最小不動点、或いは最大不動点を求める集合演算に帰着される。
【００１６】
このような集合演算は、或る状態集合｛ｑ｝から１回の遷移で到達可能な状態集合を求める像計算Ｉｍａｇｅ  （｛ｑ｝）と、或る状態集合｛ｑ｝に１回の状態遷移で到達可能な状態集合を求める逆像計算Ｉｍａｇｅ  −１（｛ｑ｝）とを組み合わせることによって実現される。
【００１７】
例えば、図１１に示すように、９つの状態ｑ０  〜ｑ８  間の状態遷移で表される有限状態機械の例において、像計算および逆像計算を行った結果の例を、次の式（３）  〜式（６）  に示す。
【００１８】
Ｉｍａｇｅ  （｛ｑ０  ｝）＝｛ｑ０  ，ｑ１  ，ｑ２  ，ｑ３  ｝・・・式（３）
Ｉｍａｇｅ  （｛ｑ３  ，ｑ８  ｝）＝｛ｑ２  ，ｑ３  ，ｑ５  ，ｑ６  ，ｑ８  ｝・・・式（４）
Ｉｍａｇｅ  −１（｛ｑ０  ｝）＝｛ｑ０  ，ｑ１  ｝・・・式（５）
Ｉｍａｇｅ  −１（｛ｑ５  ｝）＝｛ｑ１  ，ｑ２  ，ｑ３  ，ｑ４  ｝・・・式（６）
図１１に示した有限状態機械において、例えば、状態ｑ７  を示す論理式ｐを用いた時相論理ＡＦｐを検証する際には、初期状態ｑ０  から順次に像計算を繰り返し、初期状態から遷移可能な全ての道筋が状態ｑ７  に到達するか否かを調べれば良い。一方、時相論理ＥＦｐを検証する場合には、状態ｑ７  から逆像計算を繰り返して、初期状態ｑ０  に到達する道筋があるか否かを調べれば良い。
【００１９】
ところで、実際の記号モデル検査法においては、集合演算を論理関数処理に置き換える手法が一般的であり（参考文献５を参照）、また、論理関数を二分決定グラフで表現することにより、論理関数処理の効率化が計られている（参考文献１を参照）。
【００２０】
§３：従来技術の説明（その３）・・・図１２〜図１４参照
図１２は従来技術の説明図２、図１３は従来技術の説明図３、図１４は従来技術の説明図４である。前記記号モデル検査手法において、メモリ規模の縮小と処理時間の短縮とを両立可能にしたプロパティ検証装置（特願平８−２２０００５号参照）が既に提案されている。以下、この従来技術について、図１２〜図１４を参照しながら説明する。
【００２１】
図１２において、プロパティ検証装置は、論理式入力手段としての入力受付部２１１を介して受け付けた計算木論理式を単一パス表現変換部２１２によって単一パス表現に変換し、更に、手続き列変換部２１３によって後述する手続き列に変換した後に集合演算部２１４の処理に供し、得られた状態集合が空であるか否かを判定処理部２１５によって判定することにより、入力されたプロパティを検証する構成となっている。
【００２２】
前記入力受付部２１１において、演算子判別部２２１は、受け取った計算木論理式の先頭の演算子に応じて、この計算木論理式を直接或いは否定処理部２２２を介して初期状態付加部２２３に送出する。ここで、演算子判別部２２１は、先頭の演算子が全称を示す演算子Ａである場合に、計算木論理式全体を否定処理部２２２に送出し、一方、存在を示す演算子Ｅである場合には、そのまま初期状態付加部２２３に送出すれば良い。
【００２３】
また、否定処理部２２２は、演算子判別部２２１から受け取った計算木論理式全体を否定し、更に、論理演算規則に従って必要な式の変形を行って計算木論理式を整理し、得られた計算木論理式を初期状態付加部２２３に送出する。この初期状態付加部２２３は、受け取った計算木論理式の先頭に初期状態に対応する命題論理式を付加することにより、検証作業の開始状態として、この計算木論理式を単一パス表現変換部２１２に送出する。
【００２４】
そして、単一パス表現変換部２１２において、式変形処理部２２４は上述した入力受付部２１１から計算木論理式を受け取り、変換規則格納部２２５に保持されている変換規則に従ってこの計算木論理式を変形し、単一パス表現に変換する。ここで、変換規則格納部２２５には、計算木論理式を単一パス表現に変換する手続きとして、状態集合を示す命題論理式ｐ、ｑ及び上述した計算木論理式の部分式ｆを用いて、次の式（７）  〜式（１０）に示す変換規則を格納しておけば良い。
【００２５】
Ｒ（ｐ∧ＥＸ  ｆ）＝ｐＲ（ｆ）・・・式（７）
Ｒ（ｐ∧ＥＦ  ｆ）＝｛Ｒ（ｐ∧ｆ），ｐＴｒｕｅ＊  Ｒ（ｆ）｝・・・式（８）
Ｒ（ｐ∧ＥＧ  ｑ）＝（ｐ∧ｆ）ｑω・・・式（９）
Ｒ（ｐ∧Ｅ（ｑ∪ｆ）＝｛Ｒ（ｐ∧ｆ），ｐｑ＊  Ｒ（ｆ）｝・・・式（１０）
前記式（７）  から式（１０）においては、命題論理式ｐの有限回及び無限回の繰り返しを指数符号「＊  」及び指数符号「ω」で示し、また、場合分けを｛｝で括って示してある。また、式変形処理部２２４は、受け取った計算木論理式から上述した変換規則に適合する箇所を検出し、該当する変換規則をそれぞれ適用することにより、単一パス表現への変換処理を行えば良い。
【００２６】
ここで、単一パス表現とは、枝分かれのない一本の状態集合列、或いは枝分かれのない一本の状態集合列に無限ループとなる状態集合列が連結した状態集合列であり、任意の状態集合を表す命題論理式の集合Ｐを用いて、単一パス表現ｓの集合Ｓを次のように定義する。
【００２７】
▲１▼：ｐ∈Ｐである状態集合は単一パス表現である。
▲２▼：ｐ∈Ｐである状態集合ｐとｓ∈Ｓである状態集合列ｓとの連接ｐｓは単一パス表現である。
【００２８】
▲３▼：ｐ∈Ｐである状態集合ｐの無限回の繰り返しｐωは単一パス表現である。
▲４▼：ｐ∈Ｐである状態集合ｐの状態集合ｐの有限回の繰り返しｐ＊  とｓ∈Ｓである状態集合列ｓとの連接ｐ＊  は単一パス表現である。
【００２９】
従って、式変形処理部２２４は、上述した変換規則に従って式を変形していき、前記定義した単一パス表現で表される状態集合列を求めれば良い。例えば、入力受付部２１１を介して検証すべきプロパティを示す計算木論理式「ＡＧ（ｐ→ＡＦｑ）」が入力した場合は、先頭の演算子が全称を示す演算子Ａであるので、演算子判別部２２１からの指示に応じて否定処理部２２２が動作し、図１３の（ａ）に示すように、入力された計算木論理式を一旦否定した後に整理することで、演算子Ａを含まない計算木論理式が得られる。
【００３０】
更に、初期状態付加部２２３により、この計算木論理式の先頭には初期状態に対応する命題論理式ｐｉが付加され、得られた計算木論理式が式変形処理部２２４の処理に供される。この計算木論理式の入力に応じて、式変形処理部２２４が動作し、図１３の（ｂ）において、それぞれ下線を付して示す部分式に、上述した式（８）  及び式（９）  を順次に適用して整理することにより、図１３の（ｂ）に示す単一パス表現が得られる。
【００３１】
前記手続き列変換部２１３において、式変形処理部２２６は、変換規則格納部２２７に保持された変換規則に従って、単一パス表現を以下に述べる検証手続き列に変換する構成となっている。ここで基本的な検証手続き列は、像計算によってのみ構成されており、命題論理式ｐ、ｑと像計算を示す演算子Ｉｍａｇｅ  及び最大不動点と最小不動点をそれぞれ表す演算子ｇｆｐ  １ｆｐ  を用いて、次の式（１１）から式（１３）のように表される。
【００３２】
ＦｉｎｄＴｒａｎｓ（ｐ）＝Ｉｍｇ（ｐ）・・・（１１）
ＦｉｎｄＴｒａｉｌ（ｐ，ｑ）＝１ｆｐ  Ｚ．［ｐ  ∨Ｉｍｇ（Ｚ）］・・・（１１）
ＦｉｎｄＬｏｏｐ（ｐ）  ＝ｇｆｐ  Ｚ．  Ｚ．ｐ  ∧Ｉｍｇ（Ｚ）］・・・（１３）
前記式（１１）に示した検証手続きＦｉｎｄＴｒａｎｓ（ｐ）は、まさに像計算そのものであり、図１４の（ａ）に示したように、命題論理式ｐで表された状態集合から一回の状態遷移で到達可能な状態集合を返す手続きである。前記式（１２）に示した検証手続きＦｉｎｄＴｒａｉｌ（ｐ，ｑ）は、図１４の（ｂ）に示したように、命題論理式ｐで表された状態集合から、命題論理式ｑが成り立つ状態集合を経由して到達可能な状態集合｛図１４の（ｂ）図において斜線を付して示す｝を返す手続きである。
【００３３】
前記式（１３）に示した検証手続き  ＦｉｎｄＬｏｏｐ（ｐ）  は、図１４の（ｃ）に示すように、命題論理式ｐで表された状態集合に含まれており、かつ、命題論理式ｐが成り立つループを構成する部分集合と、そのループから到達可能な部分集合の和集合｛図１４の（ｃ）において斜線を付して示す｝を返す手続きである。また、変換規則格納部２２７は、単一パス表現ｓ及び命題論理式ｐを用いて、次の式（１４）から式（１８）のように表される変換規則Ｓを格納している。
【００３４】
Ｓ（ｐ）＝ｐ・・・（１４）
Ｓ（ｓｐ）＝ＦｉｎｄＴｒａｎｓ（Ｓ（ｓ））  ∧ｐ・・・（１５）
Ｓ（ｓｐ＊  ）＝ＦｉｎｄＴｒａｉｌ（ＦｉｎｄＴｒａｎｓ（Ｓ（ｓ），ｐ）  ）・・・（１６）
Ｓ（ｓｐω）＝ＦｉｎｄＬｏｏｐ（ＦｉｎｄＴｒａｉｌ（（Ｓ（ｓ），ｐ）  ∧  ｐ）  ）・・・（１７）
Ｓ（｛ｓ∧ｐ，ｓｐ＊  ｝）＝ＦｉｎｄＴｒａｉｌ（Ｓ（ｓ），ｐ）  ・・・（１８）
従って、式変形処理部２２６は、受け取った単一パス表現からこれらの変換規則に適合する部分を検出し、該当する変換規則を順次に適用することにより、単一パス表現を検証手続き列に変換すれば良い。例えば、図１３の（ｂ）に示した単一パス表現の入力に応じて、式変形処理部２２６が前記式（１７）及び式（１８）を順次適用し、更に、式を整理することにより、図１３の（ｃ）に示したようにして、手続き列に変換することができる。
【００３５】
このようにして得られた手続き列の入力に応じて、集合演算部２１４は、上述した式（１１）から式（１３）に示した像計算及び不動点計算を実行し、単一パス表現で表される状態集合を求め、判定処理部２１５に入力し、状態集合が空集合であるか否かを判定すれば良い。
【００３６】
上述したように、これらの手続き列は像計算のみを用いて実行可能であるから、状態遷移関係を関数で表して、二分木決定グラフの規模を縮小した場合においても、現実的な計算機システムの処理能力を用いて集合演算処理を実行し、論理装置のモデルが、単一パス表現で表すことが可能なプロパティを実現しているか否かを検証することが出来る。
【００３７】
これにより、単一パス表現可能なプロパティに関しては、記号モデル検査手法を適用する際に問題となる、メモリ量の抑制と処理時間の短縮とを両立することができるので、記号モデル検査手法を現実的な規則を持つ論理装置のプロパティ検証に適用することが可能になる。
【００３８】
§４：参考文献
（参考文献１）：Ｒ  ．Ｅ  ．Ｂｒｙａｎｔ．  Ｇｒａｐｈ  ｂａｓｅｄ  ａｌｇｏｒｉｔｈｍ  ｆｏｒ  ｂｏｏｌｅａｎ  ｆｕｎｃｔｉｏｎ  ｍａｎｉｐｕｌａｔｉｏｎ．  ＩＥＥＥ  Ｔｒａｎｓ．  Ｃｏｍｐｕｔ  ．，  Ｃ−３５（８）：６７７−６９１，  １９８６．
（参考文献２）：Ｅ．Ｍ．Ｃｌａｒｋｅ，  Ｅ．Ａ．  Ｅｍｅｒｓｏｎ，  ａｎｄ  Ａ．Ｐ．Ｓｉｓｔｌａ．  Ａｕｔｏｍａｔｉｃ  ｖｅｒｉｆｉｃａｔｉｏｎ  ｏｆ  ｆｉｎｉｔｅ−ｓｔａｔｅ  ｃｏｎｃｕｒｒｅｎｔ  ｓｙｓｔｅｍｓ  ｕｓｉｎｇ  ｔｅｍｐｏｒａｌ  ｌｏｇｉｃ  ｓｐｅｃｉｆｉｃａｔｉｏｎｓ．  ＡＣＭ  Ｔｒａｎｓ．  Ｐｒｏｇ．  Ｌａｎｇ．  Ｓｙｓｔ。，  ８（２）：２４４−２６３，  １９８６．
（参考文献３）：藤田，陳，山崎．形式的検証手法の実設計への適用例．情報処理，３５（８）：７１９−７２５，１９９４．
（参考文献４）：藤田，Ｅ．Ｍ．Ｃｌａｒｋｅ．      ＢＤＤのＣＡＤへの応用．情報処理，３４（５）：６０９−６１６，１９９３．
（参考文献５）：平石、浜口、論理関数処理に基づく形式的検証手法．情報処理，３５（８）：７１０−７１８，１９９４．
（参考文献６）：Ｊ．Ｅ．Ｈｏｐｃｒｏｆｔ  ａｎｄ  Ｊ．Ｄ．Ｕ１１ｍａｎ．  Ｉｎｔｒｏｄｕｃｔｉｏｎ  ｔｏ  Ａｕｔｏｍａｔａ  Ｔｈｅｏｒｙ，  Ｌａｎｇｕａｇｅｓ，  ａｎｄ  Ｃｏｍｐｕｔａｔｉｏｎ．  Ａｄｄｉｓｏｎ−Ｗｅｓｌｅｙ  Ｐｕｂｌｉｓｈｉｎｇ  Ｃｏｍｐａｎｙ，  １９７９．
（参考文献７）：湊．計算機上でのＢＤＤの処理技法．情報処理，３４（５）：５９３−５９９，１９９３．
（参考文献８）：谷口，北道．代数的手法による仕様記述と設計及び検証．情報処理，３５（８）：７４２−７５０，１９９４．
（参考文献９）：石浦．ＢＤＤとは．情報処理，３４（５）：５８５−５９２，１９９３．
（参考文献１０）：Ｈ．Ｉｗａｓｈｉｔａ，  Ｓ．Ｋｏｗａｔａｒｉ，  Ｔ．Ｎａｋａｔａ，  ａｎｄ  Ｆ．Ｈｉｒｏｓｅ．  Ａｕｔｏｍａｔｉｃ  ｔｅｓｔ  ｐｒｏｇｒａｍ  ｇｅｎｅｒａｔｉｏｎ  ｆｏｒ  ｐｉｐｅｌｉｎｅｄ  ｐｒｏｃｅｓｓｏｒｓ．  Ｉｎ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｃｏｎｆｅｒｅｎｃｅ  ｏｎ  Ｃｏｍｐｕｔｅｒ−Ａｉｄｅｄ  Ｄｅｓｉｇｎ，  ｐｐ．５８０−５８３，１９９４．
（参考文献１１）：木村．形式的タイミング検証について．情報処理，３５（８）：７２６−７３５，１９９４．
（参考文献１２）：Ｋ．  Ｒａｖｉ  ａｎｄ  Ｆ．  Ｓｏｍｅｎｚｉ．  Ｈｉｇｈ−ｄｅｎｓｉｔｙ  ｒｅａｃｈａｂｉｌｉｔｙ  ａｎａｌｙｓｉｓ．  Ｉｎ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｃｏｎｆｅｒｅｎｃｅ  ｏｎ  Ｃｏｍｐｕｔｅｒ−Ａｉｄｅｄ  Ｄｅｓｉｇｎ，  ｐｐ．１５４−１５８，  １９９５．
（参考文献１３）：高原．プロセス代数を用いた形式的検証．情報処理，３５（８）：７３６−７４１，１９９４．
（参考文献１４）：渡部，久木元．ＢＤＤの応用．情報処理，３４（５）：６００−６０８，１９９３．
【００３９】
【発明が解決しようとする課題】
前記のような従来のものにおいては、次のような課題があった。
（１）  ：記号モデル検査手法では、有限状態機械の動作を論理式で表し、検証手続きを論理関数処理で実現している。その際に、論理関数の表現形式として二分木決定グラフ（ＢＤＤ）を用いている。設計検証で扱われる有限状態機械の状態数は１０２０を越えることも珍しくなく、論理関数を用いた非明示的な表現手法と、ＢＤＤを用いた効率的な論理関数処理が不可欠である。
【００４０】
ところが、状態数が多く、状態遷移が複雑な装置では、有限状態機械の遷移関係を表すＢＤＤの規模や、論理関数処理の途中で生成されるＢＤＤの規模が膨大になるという問題がある。ＢＤＤの規模はＢＤＤのノード数で計ることができるが、最悪の場合、変数に対して指数オーダで増大する可能性がある。
【００４１】
（２）  ：前記（１）  の問題は、前記提案されているプロパティ検証装置（特願平８−２２０００５号参照）によって軽減されるが、更に装置が複雑になれば、この方法でもＢＤＤの規模が限界に達することは避けられない。一部のプロパティに関しては、検証手続きの途中で状態集合を分割することでＢＤＤの規模を抑える手法（参考文献１０、参考文献１２を参照）が知られている。これは、初期状態からの像計算の繰り返しによる状態数え上げの処理（参考文献５を参照）を制限された記憶容量内で実行するものである。
【００４２】
一般の記号モデル検査は、逆像計算をベースとするため（参考文献５を参照）、この方法の応用範囲は限られる。これに対して前記プロパティ検証装置（特願平８−２２０００５号参照）では、像計算をベースとしているため、より広い応用が可能である。前記プロパティ検証装置（特願平８−２２０００５号参照）によれば、ＦｉｎｄＴｒａｉｌ（）  の手続きは、状態数え上げに基づくものであり、状態集合を分割して計算することができる。
【００４３】
また、ＦｉｎｄＴｒａｎｓ（）  も状態集合を分割して計算することは容易である。しかしながら、ＦｉｎｄＬｏｏｐ（）は、状態数え上げとは全く異なる手続きであり、状態集合を分割して処理することはできなかった。従って、多くの場合、状態集合分割の手法は、記号モデル検査手法の記憶容量削減には寄与しなかった。
【００４４】
本発明は、このような従来の課題を解決し、記号モデル検査手法において、状態集合分割手法を用いることができるようにして、記憶容量削減を可能とし、複雑な論理装置の検証もできるようにすることを目的とする。
【００４５】
【課題を解決するための手段】
本発明は前記の目的を達成するため次のように構成した。
(1) ：同期式順序回路の動作を表す有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑのある部分集合ｐにおいて、ｐ内のある状態から出発し永遠にｑから外に出ない状態遷移のパスが存在するか否かを判定する論理検証装置であって、前記有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ａ［ｉ］が入力された場合に、Ｍにおけるａ［ｉ］の像計算及びその結果とｑとの集合積演算によって集合ａ［ｉ＋１］を求める計算手段と、前記集合ｐの部分集合あるいはｐ全体をａ［０］として、前記計算手段を繰り返し適用することでａ［１］、ａ［２］、ａ［３］、・・・を求め、空でない集合ａ［ｋ］がその後のｎ個の集合ａ［ｋ＋１］、ａ［ｋ＋２］、・・・ａ［ｋ＋ｎ］の和集合に対して部分集合になっているような自然数ｋが存在するか否かを判定する判定手段と、前記判定手段を満足する前記集合ｐがある場合は、永遠にｑから外に出ない状態遷移のパスが存在する旨を出力する出力手段とを備えていることを特徴とする。
【００４６】
(2) ：前記(1) の論理検証装置であって、前記判定手段は、状態集合ｐから開始して、状態集合分割と前記計算手段の繰り返し適用を深さ優先で再帰的に行うことを特徴とする。
【００５１】
（作用）
前記構成に基づく本発明の作用を図１〜図４を参照しながら説明する。なお、Ｓ１〜Ｓ３８は各処理ステップを示す。
【００５２】
(a) ：作用１・・・図１参照
論理装置の検証装置において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ（状態集合ｑ）、及びｑの部分集合ｐが入力すると（Ｓ１）、有限状態機械Ｍ上の像計算を行い（Ｓ２）、ｑとの集合積の計算を行う（Ｓ３）。そして、前記Ｓ２、Ｓ３の処理を繰り返して行いながら、その計算過程の状態集合の関係を状態集合比較により調べることで（Ｓ４）、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するか否かを判定する。
【００５３】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、状態集合を分割して計算することを可能にする基本的なアルゴリズムを与える。そして、記号モデル検査の多くの場合に、状態集合分割の手法を用いることができるようになる。従って、記憶容量削減を可能とし、複雑な論理装置の検証も可能になる。
【００５４】
(b) ：作用２・・・図２参照
論理装置の検証装置において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ（状態集合ｐ）が入力すると（Ｓ１１）、状態集合ｐから開始して、状態集合分割（Ｓ１２）、Ｍ上の像計算（Ｓ１３）、およびｑとの集合積の計算（Ｓ１４）、状態集合比較（Ｓ１５）を繰り返して行う。すなわち、状態集合ｐから開始して、状態集合分割、Ｍ上の像計算、およびｑとの集合積の計算を深さ優先で再帰的に繰り返し、その計算過程を状態集合比較により調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ないパスが存在するかどうかを判定する。
【００５５】
その結果、前記パスが１つでも見つかればその時点で処理を終了する。しかし、前記パスが存在しない場合はバックトラック判定を行い（Ｓ１６）、処理終了条件を満たしていない場合は、分割して残った状態集合について再び前記Ｓ１３の処理から実行する。
【００５６】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、繰り返し計算の度に状態集合を分割するアルゴリズムを与える。従って、前記状態集合を分割した分、記憶容量の削減が可能になる。
【００５７】
(c) ：作用３・・・図３参照
論理装置の検証装置において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ１，ｐ２，・・・，ｐｎ（既に分割されている部分集合）が入力すると（Ｓ２１）、前記部分集合ｐ１，ｐ２，・・・，ｐｎをそれぞれｐ（状態集合）とおいて、開始状態集合の設定（Ｓ２２）を行う。そして、状態集合ｐから開始して、Ｍ上の像計算（Ｓ２３）、およびｑとの集合積の計算（Ｓ２４）、状態集合比較（Ｓ２５）を繰り返して行う。
【００５８】
このように、前記設定された開始状態集合に対して、有限状態機械Ｍ上の像計算を行い、ｑとの集合積の計算を行う。そして、前記Ｓ２３、Ｓ２４の処理を繰り返して行いながら、その計算過程の状態集合の関係を比較して調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するか否かを判定する。
【００５９】
その結果、前記パスが１つでも見つかればその時点で処理を終了する。しかし、前記パスが存在しない場合は、開始状態集合の更新の判定を行い（Ｓ２６）、更新を必要とする場合は、前記Ｓ２２の処理から繰り返して行う。すなわち、前記状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内の或る状態から出発し、ずっとｑから外に出ない状態遷移のパスが存在するかどうかを判定する。
【００６０】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、既にｐがｐ１，ｐ２，・・・，ｐｎに分割されている場合、それをひとまとめにすることなく、別々に計算するアルゴリズムを与える。従って、この場合にも、前記状態集合を分割した分、記憶容量の削減が可能になる。
【００６１】
(d) ：作用４・・・図４参照
論理装置の検証装置において、有限状態機械Ｍ、Ｍの状態集合ｑ、ｑの部分集合ｐ１，ｐ２，・・・，ｐｎ（既に分割されている部分集合）が入力すると（Ｓ３１）、開始状態集合の設定を行い（Ｓ３２）、前記ｐ１，ｐ２，・・・，ｐｎをそれぞれｐとおく。そして、状態集合ｐから開始して、状態集合分割（Ｓ３３）、Ｍ上の像計算（Ｓ３４）、及びｑとの集合積の計算（Ｓ３５）を深さ優先で再帰的に繰り返し、その計算過程を状態集合比較（Ｓ３６）により調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内のある状態から出発し、永遠にｑから外に出ないパスが存在するかどうかを判定する。
【００６２】
その結果、前記パスが１つでも見つかればその時点で処理を終了する。しかし、前記パスが存在しない場合はバックトラック判定を行い（Ｓ３７）、処理終了条件を満たしていない場合は、分割して残った状態集合について再び前記Ｓ３４の処理から実行する。そして、前記パスが１つでも見つかればその時点で処理を終了するが、見つからなかった場合は、前記処理終了条件を満たした時点で、開始状態集合更新の判定を行って（Ｓ３８）、開始状態集合更新の必要がなくなるまで、前記Ｓ３２から処理を繰り返して行う。但し、１つでも前記パスが見つかれば、その時点で処理を終了する。
【００６３】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、既にｐがｐ１，ｐ２，・・・，ｐｎに分割されている場合、それをひとまとめにすることなく、計算するアルゴリズムを与える。また、前記計算途中で更に状態集合の分割が行われるため、その分、記憶容量の削減が可能になる。
【００６４】
(e) ：作用５
前記論理検証装置において、有限状態機械Ｍ、及びＭに関するプロパティの入力があると、前記入力部ではその入力データを受け取り、予め入力データの分割が必要であれば分割した後、そのデータを制御部へ転送する。しかし、予め分割の必要がなければそのまま前記制御部へ転送する。
【００６５】
その後、制御部では前記入力データを受け取ると状態集合を分割しながら、前記各演算部を呼び出し、検証処理を行って検証結果を検証結果出力部へ出力する。この場合、状態遷移判定演算部が呼び出されると状態集合ｐの要素から一回の状態遷移で到達可能な状態集合を求める演算を行い、演算結果を前記制御部へ返す。
【００６６】
また、到達可能性判定演算部が呼び出されると、状態集合ｐの要素から状態集合ｑの要素を経由して到達可能な状態集合を求める演算を行い、演算結果を前記制御部へ返す。更に、ループ判定演算部が呼び出されると、ｐ内のある状態から出発し、永遠にｑの外に出ない状態遷移のパスが存在するか否かの演算を行い、演算結果を前記制御部へ返す。
【００６７】
このようにすれば、記号モデル検査手法において状態集合分割手法を用いることが可能となる。従って、記憶容量削減を可能とし、複雑な論理装置の検証もできるようになる。
【００７０】
(f) ：その他
以上のようにしたので次のような特徴がある。すなわち、論理装置の検証装置において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが入力すると、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するかを判定する。
【００７１】
従って、記号モデル検査の多くの場合に、状態集合分割の手法を用いることができるようになる。状態集合分割の手法を用いれば、一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。前記記憶容量の問題は記号モデル検査の実用性にかかる重大な問題であり、本発明の寄与するところは大きい。
【００７２】
更に、分割計算の初期段階において、プロパティ反例若しくは実例を発見できる場合があるため、例えば、設計誤りの多く存在する論理検証の初期段階において、分割を行わない場合よりも高速に設計誤りを発見できる。
【００７３】
【発明の実施の形態】
以下、発明の実施の形態を図面に基づいて詳細に説明する。
§１：論理装置の検証を行うための装置の説明・・・図５参照
図５は検証装置の説明図である。この装置は、同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証装置（単に「検証装置」とも記す）の例である。
【００７４】
この検証装置には、有限状態機械Ｍ、及びＭに関するプロパティの入力を行う有限状態機械、プロパティ入力部１と、検証結果の出力を行う検証結果出力部３と、状態集合ｐの要素から一回の状態遷移で到達可能な状態集合を求める状態遷移判定演算部４と、状態集合ｐの要素から状態集合ｑの要素を経由して到達可能な状態集合を求める到達可能性判定演算部６と、ｐ内の或る状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するかどうかを判定するループ判定演算部５と、状態集合を分割しながら前記各演算部を呼び出して、プロパティに対応する状態遷移のパスを求める状態集合分割および演算部呼び出し制御部２を備えている。また、前記有限状態機械、プロパティ入力部１には、入力データを予め分割するための分割処理部７が設けてある。
【００７５】
有限状態機械Ｍ及びＭに関するプロパティの入力があると、前記入力部１では、その入力データを受け取り、予め入力データの分割が必要であれば、分割処理部７により分割した後、そのデータを、状態集合分割及び演算部呼び出し制御部２へ転送する。なお、予め分割の必要がなければ、そのまま前記制御部２へ転送する。
【００７６】
その後、状態集合分割及び演算部呼び出し制御部２では、前記入力データを受け取ると、状態集合を分割しながら、前記各演算部４、５、６を呼び出し、検証処理を行って、検証結果を検証結果出力部３へ出力する。この場合、状態遷移判定演算部４（参考文献１２を参照）が呼び出されると、状態集合ｐの要素から一回の状態遷移で到達可能な状態集合を求める演算を行い、演算結果を前記制御部２へ返す。
【００７７】
また、到達可能性判定演算部６（参考文献１２を参照）が呼び出されると、状態集合ｐの要素から状態集合ｑの要素を経由して到達可能な状態集合を求める演算を行い、演算結果を前記制御部２へ返す。更に、ループ判定演算部５が呼び出されると、ｐ内のある状態から出発し、永遠にｑの外に出ない状態遷移のパスが存在するか否かの演算を行い、演算結果を前記制御部２へ返す。
【００７８】
なお、前記入力部１、制御部２、検証結果出力部３、状態遷移判定演算部４、ループ判定演算部５、到達可能性判定演算部６は、全てプログラムの実行により前記処理を行うものであり、特に、前記状態遷移判定演算部４、ループ判定演算部５、到達可能性判定演算部６は、例えば、サブルーチンにより構成する。すなわち、前記制御部２（メインルーチン）が前記各サブルーチンを必要に応じて呼び出すことで、前記検証処理を行う。
【００７９】
なお、前記状態遷移判定演算部４の状態遷移判定手続き、及び前記到達可能性判定演算部６の到達可能性判定手続きとして、前記従来例で説明したプロパティ検証装置（特願平８−２２０００５号参照）の処理において使用している、ＦｉｎｄＴｒａｎｓ（）  、及びＦｉｎｄＴｒａｉｌ（）  の手続きをそれぞれ使用する。また、ループ判定演算部５のループ判定手続きとしては、Ｆｉｎｄｌｏｏｐ（）の返す値が空であるかどうかで判定する代わりに、以下に説明する実施の形態３、または４における手続きを用いる。
【００８０】
更に、以下に説明する実施の形態３、または４における状態集合ｐ１，ｐ２，・・・，ｐｎは、前もって全てが与えられている必要はない。ＦｉｎｄＴｒａｎｓ（）  、及びＦｉｎｄＴｒａｉｌ（）  の計算中に、返り値の部分集合が得られた時点で、実施の形態３、又は４の手続きを先行して実行することができる。それによって検証対象の状態遷移のパスが見つかれば、検証手続きを早期に打ち切ることも可能である。
【００８１】
§２：具体例による検証装置の説明・・・図６参照
図６は検証装置の具体例である。図６に示した検証装置は、図５に示した検証装置を具体化した装置例であり、以下に説明する各実施の形態ではこの検証装置を使用して検証処理を行う。
【００８２】
図５に示した検証装置は、エンジニアリングワークステーション、或いはパーソナルコンピュータ等の各種コンピュータにより実現される装置であり、コンピュータ本体１１と、前記コンピュータ本体１１に接続された表示装置１２、入力装置１３、出力装置１４、ハードディスク装置（ＨＤＤ）１５等により構成される。そして、前記コンピュータ本体１１内には入出力制御部１６、ＣＰＵ１７、メモリ１８等が設けてある。
【００８３】
また、前記ハードディスク装置１５の記憶媒体には、論理装置の検証を行うためのプログラム（図５に示した各部を実現するためのプログラム）やその他のプログラム、検証対象データやその他の各種データ等が格納されている。そして、論理装置の検証を行う際には、ＣＰＵ１７の制御によりハードディスク装置１５の記憶媒体に格納されている前記プログラムやデータを読み出してコンピュータ本体１１内に取り込み、ＣＰＵ１７が前記プログラムを実行することにより必要な処理を行う。
【００８４】
なお、メモリ１８はＣＰＵ１７がワーク用として使用するものである。また、ハードディスク装置１５の記憶媒体に格納したプログラムやデータは、例えば、次のようにして格納する。
【００８５】
（１）  ：フレキシブルディスク（フロッピィディスク）に格納されているデータ（他の装置で作成したデータ）を、前記コンピュータ本体１１に設けたドライブ装置により読み取り、ハードディスク装置１５の記憶媒体（記録媒体）に格納する。
【００８６】
（２）  ：光磁気ディスク、或いはＣＤ−ＲＯＭ等の記憶媒体に格納されているデータを、前記コンピュータ本体１１に設けたドライブ装置により読み取り、ハードディスク装置１５の記憶媒体（記録媒体）に格納する。
【００８７】
（３）  ：ＬＡＮ等の通信回線を介して他の装置から伝送されたデータを前記コンピュータ本体１１で受信し、そのデータをハードディスク装置１５の記憶媒体（記録媒体）に格納する。
【００８８】
§３：実施の形態１の処理説明・・・図７参照
図７は実施の形態１の処理フローチャートである。以下、図７に基づいて実施の形態１の処理を説明する。なお、この処理は図５、図６に示した検証装置で行う処理であり、Ｓ５１〜Ｓ５８は各処理ステップを示す。また、Ｉｍａｇｅ（ａ）は有限状態機械Ｍにおける状態集合ａの像計算を行う関数であり、ｉは任意のパラメータである。
【００８９】
この処理は、同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証処理において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ（状態集合ｐ）が与えられたとき、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するか否かを判定する処理である。
【００９０】
前記処理では、ａ［ｉ  ］←Ｉｍａｇｅ（ａ［ｉ−１  ］）  ∩ｑの演算の繰り返しにより、ａ［ｉ  ］が空集合になった場合には、ｐ内の状態から出発するといつか必ずｑの外に出ることが分かる。そして、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在する場合には、ａ［ｋ  ］がどの要素から時刻を逆に辿ってもｑの要素だけを通りａ［ｋ  ］の要素のどれかに到達するパスが存在することを示している。
【００９１】
すなわち、ａ［ｋ  ］の要素を通るループがｑの外に存在することを示しており、ｐ内のある状態から出発してａ［ｋ  ］内の状態を通り、永遠にｑの外に出ない状態遷移のパスが存在することが分かる。以下、検証処理について説明する。
【００９２】
有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが入力すると（Ｓ５１）、先ず、初期化処理として、ａ［０］←ｐ，ｉ←０とする（Ｓ５２）。そして、ｉをインクリメント（ｉ←ｉ＋１）し（Ｓ５３）、Ｍ上の像計算、及びｑとの集合積の演算、すなわち、ａ［ｉ  ］←Ｉｍａｇｅ（ａ［ｉ−１  ］）  ∩ｑの演算を行う（Ｓ５４）。
【００９３】
その後、ａ［ｉ  ］が空集合か否かを判断し（Ｓ５５）、空集合でなければ、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋ（０≦ｋ≦ｉ−１）が存在するか否かを判断する（Ｓ５６）。その結果、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在しなければ、前記Ｓ５３の処理から繰り返して行う。
【００９４】
このようにして、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在することが分かったので、この検証処理を終了する（Ｓ５７）。しかし、前記Ｓ５５の処理で、ａ［ｉ  ］が空集合であると判断した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在しないことが分かったので、検証処理を終了する（Ｓ５８）。
【００９５】
前記処理により、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するかどうかを判定する処理において、状態集合を分割して計算することを可能にする基本的アルゴリズムを与えることができる。
【００９６】
§４：実施の形態２の処理説明・・・図８参照
図８は実施の形態２の処理フローチャートである。以下、図８に基づいて実施の形態２の処理を説明する。なお、この処理は図５、図６に示した検証装置で行う処理であり、Ｓ６１〜Ｓ７４は各処理ステップを示す。また、Ｉｍａｇｅ（ａ）は、有限状態機械Ｍにおける状態集合ａの像計算を行う関数であり、ｉはパラメータである。
【００９７】
この処理は、同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証処理において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが与えられたとき、状態集合ｐから開始して、状態集合分割、Ｍ上の像計算、およびｑとの集合積の計算を深さ優先で再帰的に繰り返し、その計算過程を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ないパスが存在するか否かを判定する処理である。
【００９８】
この処理では、ａ［ｉ  ］＝ｔとおいて該ｔを２分割し、その一方を新たなａ［ｉ  ］とし、他方をｔのままスタックに保存しておき、前記分割後の新たなａ［ｉ  ］を対象として検証処理を行う。そして、前記新たなａ［ｉ  ］について、更に分割を繰り返しながら検証処理を行い、前記パスが存在するか否かを判定する。
【００９９】
このようにして前記新たなａ［ｉ  ］に対し、１つでも前記パスが見つかれば、処理を終了するが、最後まで前記パスが見つからなかった場合は、前記スタックしておいた他方のｔを取り出し、このｔを新たなａ［ｉ  ］として前記と同様な検証処理を行い、前記パスが存在するか否かを判断する。具体的には次の通りである。
【０１００】
有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが入力したら（Ｓ６１）、先ず、初期化処理として、ａ［０］←ｐ，ｉ←０とする（Ｓ６２）。そして、ｔ←ａ［ｉ  ］として（Ｓ６３）、ｔを２分割し、ａ［ｉ  ］をｔに代入（但し、ａ［ｉ  ］≠φ）する（Ｓ６４）。すなわち、ａ［ｉ  ］をｔとおいて、そのｔを２分割し、そのいずれか一方のｔをａ［ｉ  ］とする。このため前記２分割したｔが、新たなａ［ｉ  ］と残りのｔとに分けられる。
【０１０１】
そして、前記ｔが空集合か否かを判断し（Ｓ６５）、ｔが空集合でなければ、現在の変数値をスタックに保存する（Ｓ６６）が、ｔが空集合であれば何もしない。このように、前記２分割して新たにａ［ｉ  ］となった方を対象として、次の処理を行うが、他方のｔについては、空集合でなければスタックに保存しておき、必要があれば、前記新たにａ［ｉ  ］の処理終了後に取り出して処理を行う。
【０１０２】
前記新たにａ［ｉ  ］に対して処理を行う場合、ｉをインクリメント（ｉ←ｉ＋１）し（Ｓ６７）、Ｍ上の像計算、及びｑとの集合積の演算、すなわち、ａ［ｉ  ］←Ｉｍａｇｅ（ａ［ｉ−１  ］）  ∩ｑの演算を行う（Ｓ６８）。
【０１０３】
その後、ａ［ｉ  ］が空集合か否かを判断し（Ｓ６９）、空集合でなければ、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋ（０≦ｋ≦ｉ−１）が存在するか否かを判断する（Ｓ７０）。その結果、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在しなければ、前記Ｓ６３の処理から繰り返して行う。
【０１０４】
このようにして、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在することが分かったので、この検証処理を終了する（Ｓ７１）。しかし、前記Ｓ６９の処理で、ａ［ｉ  ］が空集合であると判断した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在しないことが分かったので、前記新たなａ［ｉ  ］についての検証処理を終了し、その後、スタックが空か否かを判断する（Ｓ７２）。
【０１０５】
その結果、スタックが空でなければ、スタックから変数値を復帰させ（Ｓ７２）、前記Ｓ６７の処理から繰り返して行う。しかし、前記Ｓ７２の処理でスタックが空であれば、前記パスが無いとして検証処理を終了する（Ｓ７４）。
【０１０６】
§５：実施の形態３の処理説明・・・図９参照
図９は実施の形態３の処理フローチャートである。以下、図９に基づいて実施の形態３の処理を説明する。なお、この処理は図５、図６に示した検証装置で行う処理であり、Ｓ８１〜Ｓ９１は各処理ステップを示す。また、Ｉｍａｇｅ（ａ）は、有限状態機械Ｍにおける状態集合ａの像計算を行う関数であり、ｉ、ｊは任意のパラメータである。
【０１０７】
この処理は、同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証処理において、有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ［１］，ｐ［２］，・・・，ｐ［ｎ］（以下、ｑの部分集合を、ｐ１，ｐ２，・・・，ｐｎと記す）が与えられたとき、前記部分集合ｐ１，ｐ２，・・・，ｐｎをそれぞれｑとおいて、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内のある状態から出発し、ずっとｑから外に出ない状態遷移のパスが存在するかを判定する処理である。具体的には次の通りである。
【０１０８】
有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが入力すると（Ｓ８１）、先ず、初期化処理として任意のパラメータｊに１を代入（ｊ←１）し（Ｓ８２）、ａ［０］←ｐ［ｊ］、ｉ←０とする（Ｓ８３）。そして、ｉをインクリメント（ｉ←ｉ＋１）し（Ｓ８４）、Ｍ上の像計算、及びｑとの集合積の演算、すなわち、ａ［ｉ  ］←Ｉｍａｇｅ（ａ［ｉ−１  ］）  ∩ｑの演算を行う（Ｓ８５）。
【０１０９】
その後、ａ［ｉ  ］が空集合か否かを判断し（Ｓ８６）、空集合でなければ、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋ（０≦ｋ≦ｉ−１）が存在するか否かを判断する（Ｓ８７）。その結果、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在しなければ、前記Ｓ８４の処理から繰り返して行う。
【０１１０】
このようにして、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在することが分かったので、この検証処理を終了する（Ｓ８８）。しかし、前記Ｓ８６の処理で、ａ［ｉ  ］が空集合であると判断した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在しないことが分かったので、ｊをインクリメント（ｊ←ｊ＋１）し（Ｓ８９）、ｊ≦ｎの条件を満たしているか否かを判断する（Ｓ９０）。
【０１１１】
その結果、ｊ≦ｎの条件を満たしていた場合には、前記Ｓ８３の処理から繰り返して行うが、ｊ≦ｎの条件を満たしていない場合、すなわち、ｊ＞ｎとなった場合には前記パスが無いと判断し、検証処理を終了する（Ｓ９１）。
【０１１２】
§６：実施の形態４の処理説明・・・図１０参照
図１０は実施の形態４の処理フローチャートである。以下、図１０に基づいて実施の形態４の処理を説明する。なお、この処理は図５、図６に示した検証装置で行う処理であり、Ｓ１０１〜Ｓ１１７は各処理ステップを示す。
【０１１３】
この処理は、同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証処理において、有限状態機械Ｍ、Ｍの状態集合ｑ、ｑの部分集合ｐ［１］，ｐ［２］，・・・，ｐ［ｎ］（以下、ｑの部分集合を、ｐ１，ｐ２，・・・，ｐｎと記す）が与えられたとき、前記ｐ１，ｐ２，・・・，ｐｎをそれぞれｐとおいて、状態ｐから開始して、状態集合分割、Ｍ上の像計算、およびｑとの集合積の計算を深さ優先で再帰的に繰り返し、その計算過程を調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内のある状態から出発し、永遠にｑから外に出ないパスが存在するかどうかを判定する処理である。具体的には次の通りである。
【０１１４】
有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ１，ｐ２，・・・，ｐｎが入力すると（Ｓ１０１）、先ず、初期化処理として任意のパラメータｊに１を代入（ｊ←１）し（Ｓ１０２）、ａ［０］←ｐ［ｊ］、ｉ←０とする（Ｓ１０３）。そして、ｔ←ａ［ｉ  ］として（Ｓ１０４）、ｔを２分割し、ａ［ｉ  ］をｔに代入（但し、ａ［ｉ  ］≠φ）する（Ｓ１０５）。すなわち、ａ［ｉ  ］をｔとおいて、そのｔを２分割し、そのいずれか一方のｔをａ［ｉ  ］とする。このため２分割したｔが、新たなａ［ｉ  ］と残りのｔとに分けられる。
【０１１５】
そして、前記ｔが空集合か否かを判断し（Ｓ１０６）、ｔが空集合でなければ、現在の変数値をスタックに保存する（Ｓ１０７）が、ｔが空集合であれば何もしない。このように、前記２分割して新たにａ［ｉ  ］となった方を対象として、次の処理を行うが、他方のｔについては、空集合でなければスタックに保存しておき、必要があれば、前記新たにａ［ｉ  ］の処理終了後に取り出して処理を行う。
【０１１６】
前記新たにａ［ｉ  ］に対して処理を行う場合、ｉをインクリメント（ｉ←ｉ＋１）し（Ｓ１０８）、Ｍ上の像計算、及びｑとの集合積の演算、すなわち、ａ［ｉ  ］←Ｉｍａｇｅ（ａ［ｉ−１  ］）  ∩ｑの演算を行う（Ｓ１０９）。その後、ａ［ｉ  ］が空集合か否かを判断し（Ｓ１１０）、空集合でなければ、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋ（０≦ｋ≦ｉ−１）が存在するか否かを判断する（Ｓ１１１）。その結果、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在しなければ、前記Ｓ１０４の処理から繰り返して行う。
【０１１７】
このようにして、ａ［ｋ  ］⊆（ａ［ｋ＋１  ］∪ａ［ｋ＋２  ］∪・・・∪ａ［ｉ  ］）となるｋが存在した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在することが分かったので、この検証処理を終了する（Ｓ１１２）。しかし、前記Ｓ１１０の処理で、ａ［ｉ  ］が空集合であると判断した場合には、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在しないことが分かったので、前記新たなａ［ｉ  ］についての検証処理を終了し、その後、スタックが空か否かを判断する（Ｓ１１３）。
【０１１８】
その結果、スタックが空でなければ、スタックから変数値を復帰させ（Ｓ１１４）、前記Ｓ１０８の処理から繰り返して行う。しかし、前記Ｓ１１３の処理でスタックが空であれば、ｊをインクリメント（ｊ←ｊ＋１）し（Ｓ１１５）、ｊ≦ｎの条件を満たしているか否かを判断する（Ｓ１１６）。その結果、ｊ≦ｎの条件を満たしていれば、前記Ｓ１０３の処理から繰り返して行う。しかし、ｊ≦ｎの条件を満たしていない場合、すなわち、ｊ＞ｎの場合には、パスがないと判断し、検証処理を終了する（Ｓ１１７）。
【０１１９】
（他の実施の形態）
以上実施の形態について説明したが、本発明は次のようにしても実施可能である。
【０１２０】
（１）  ：前記論理装置の検証処理において、状態集合の分割を行う場合、或る集合ｒ内の状態から出発すると、いつか必ずｑの外に出ると判定された場合、ｒ内には状態遷移のループが存在しないことが分かる。従って、その後の計算では、ｑの代わりに、
【０１２１】
【数１】
0003600420.tif 000002
【０１２２】
を使っても良い。
【０１２３】
【発明の効果】
以上説明したように、本発明によれば次のような効果がある。
（１）  ：有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが与えられたとき、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するかを判定する検証方法を適用したので、記号モデル検査の多くの場合に、状態集合分割の手法を用いることができるようになる。
【０１２４】
（２）  ：状態集合分割の手法を用いることができるので、従来の一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。前記記憶容量の問題は記号モデル検査の実用性にかかる重大な問題であり、本発明の寄与するところは大きい。
【０１２５】
（３）  ：前記分割計算の初期段階において、プロパティ反例、若しくは実例を発見できる場合があるため、例えば、設計誤りの多く存在する論理検証の初期段階において、分割を行わない場合よりも高速に設計誤りを発見できる。
【０１２６】
(4) ：有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが与えられたとき、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するかを判定する。
【０１２７】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、状態集合を分割して計算することを可能にする基本的なアルゴリズムを与える。その結果、記号モデル検査の多くの場合に、状態集合分割の手法を用いることができるようになる。
【０１２８】
状態集合分割の手法を用いれば、一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。前記記憶容量の問題は記号モデル検査の実用性にかかる重大な問題であり、本発明の寄与するところは大きい。
【０１２９】
更に、分割計算の初期段階において、プロパティ反例、若しくは実例を発見できる場合があるため、例えば、設計誤りの多く存在する論理検証の初期段階において、分割を行わない場合よりも高速に設計誤りを発見できる。
【０１３０】
(5) ：有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐが与えられたとき、状態ｐから開始して、状態集合分割、Ｍ上の像計算、およびｑとの集合積の計算を深さ優先で再帰的に繰り返し、その計算過程を調べることで、ｐ内のある状態から出発し、永遠にｑから外に出ないパスが存在するかどうかを判定する。
【０１３１】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、繰り返し計算の度に状態集合を分割するアルゴリズムを与える。従って、状態集合を分割した分だけ、メモリ容量の削減が可能になり、従来の一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。
【０１３２】
(6) ：有限状態機械Ｍ、Ｍの状態の部分集合ｑ、及びｑの部分集合ｐ１，ｐ２，・・・，ｐｎが与えられたとき、前記部分集合ｐ１，ｐ２，・・・，ｐｎをそれぞれｑとおいて、状態集合ｐから開始して、Ｍ上の像計算およびｑとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内のある状態から出発し、ずっとｑから外に出ない状態遷移のパスが存在するかを判定する。
【０１３３】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、既にｐがｐ１，ｐ２，・・・，ｐｎに分割されている場合、それをひとまとめにすることなく、計算するアルゴリズムを与える。従って、従来の一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。
【０１３４】
(7) ：有限状態機械Ｍ、Ｍの状態集合ｑ、ｑの部分集合ｐ１，ｐ２，・・・，ｐｎが与えられたとき、前記ｐ１，ｐ２，・・・，ｐｎをそれぞれｐとおいて、状態ｐから開始して、状態集合分割、Ｍ上の像計算、およびｑとの集合積の計算を深さ優先で再帰的に繰り返し、その計算過程を調べることで、ｐ１∪ｐ２∪ｐ３・・・∪ｐｎ内のある状態から出発し、永遠にｑから外に出ないパスが存在するかどうかを判定する。
【０１３５】
このようにすれば、ｐ内の或る状態から出発し永遠にｑの外に出ない状態遷移のパスが存在するか否かを判定する処理において、既にｐがｐ１，ｐ２，・・・，ｐｎに分割されている場合、それをひとまとめにすることなく、計算するアルゴリズムを与える。従って、従来の一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。
【０１３６】
(8) ：有限状態機械Ｍ、及びＭに関するプロパティの入力部と、検証結果の出力部と、状態集合ｐの要素から一回の状態遷移で到達可能な状態集合を求める状態遷移判定演算部と、状態集合ｐの要素から状態集合ｑの要素を経由して到達可能な状態集合を求める到達可能性判定演算部と、ｐ内の或る状態から出発し、永遠にｑから外に出ない状態遷移のパスが存在するかどうかを判定するループ判定演算部と、状態集合を分割しながら前記各演算部を呼び出して、プロパティに対応する状態遷移のパスを求める制御部とを備えている。
【０１３７】
このようにすれば、状態集合を分割しながら各演算部を呼び出し、プロパティに対応する状態遷移のパスを求めることができる。このように、状態集合分割の手法を用いることができるので、従来の一般の方法ではメモリの記憶容量が限界に達する複雑な論理装置に対しても検証を実行することが可能になる。
【図面の簡単な説明】
【図１】本発明の原理説明図１である。
【図２】本発明の原理説明図２である。
【図３】本発明の原理説明図３である。
【図４】本発明の原理説明図４である。
【図５】実施の形態における検証装置の説明図である。
【図６】実施の形態における検証装置の具体例である。
【図７】実施の形態１の処理フローチャートである。
【図８】実施の形態２の処理フローチャートである。
【図９】実施の形態３の処理フローチャートである。
【図１０】実施の形態４の処理フローチャートである。
【図１１】従来技術の説明図１である。
【図１２】従来技術の説明図２である。
【図１３】従来技術の説明図３である。
【図１４】従来技術の説明図４である。
【符号の説明】
１  有限状態機械、プロパティ入力部
２  状態集合分割及び演算部呼び出し制御部
３  検証結果出力部
４  状態遷移判定演算部
５  ループ判定演算部
６  到達可能性判定演算部
７  分割処理部
１１  コンピュータ本体
１２  表示装置
１３  入力装置
１４  出力装置
１５  ハードディスク装置
１６  入出力制御部
１７  ＣＰＵ（中央演算処理装置）
１８  メモリ
【図１】
0003600420.tif 000003
【図２】
0003600420.tif 000004
【図３】
0003600420.tif 000005
【図４】
0003600420.tif 000006
【図５】
0003600420.tif 000007
【図６】
0003600420.tif 000008
【図７】
0003600420.tif 000009
【図８】
0003600420.tif 000010
【図９】
0003600420.tif 000011
【図１０】
0003600420.tif 000012
【図１１】
0003600420.tif 000013
【図１２】
0003600420.tif 000014
【図１３】
0003600420.tif 000015
【図１４】
0003600420.tif 000016