(57)【特許請求の範囲】
【請求項１】
複数の論理回路の等価性を形式的に検証する形式検証装置において、
前記論理回路を記述する回路記述と、前記論理回路に与えられる入力信号に関する情報とから、前記論理回路に対応した定常化有限状態機械を生成する定常化有限状態機械生成部と、
前記複数の回路記述から前記定常化有限状態機械生成部によって個別に生成された複数の定常化有限状態機械の論理的等価性を検証する等価性検証部と、
前記等価性検証部の検証結果を出力する出力部とを備え、
前記定常化有限状態機械生成部は、
前記回路記述で表された回路の複数の入力信号のうち、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械を生成する有限状態機械生成部と、
前記有限状態機械生成部によって生成した有限状態機械を、過渡的な状態への遷移を持たない定常化有限状態機械に変換する有限状態機械への変換部と、
を備えることを特徴とする論理回路の形式検証装置。
【請求項２】
前記定常化有限状態機械生成部は、前記論理回路を記述する回路記述に基づいて予備的な有限状態機械を生成する予備的な有限状態機械生成部を備え、一意的に定義された状態遷移を行う有限状態機械を生成する有限状態機械生成部は、前記予備的な有限状態機械生成部によって生成された予備的な有限状態機械に基づいて、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械を生成するものであることを特徴とする請求項１に記載の論理回路の形式検証装置。
【請求項３】
前記有限状態機械生成部が、クロック信号と他の信号の値が同時に変化するタイミングに対して、一義的に定義された状態遷移を行う有限状態機械を生成することを特徴とする請求項１または請求項２に記載の論理回路の形式検証装置。
【請求項４】
前記出力部が、定常化有限状態機械生成部において見いだした情報をも出力するものである請求項１記載の論理回路の形式検証装置。
【請求項５】
複数の論理回路の等価性を形式的に検証する形式検証方法において、
入出力装置を備えたコンピュータとそれを制御するプログラムによって実現される定常化有限状態機械生成部、等価性検証部、前記定常化有限状態機械生成部に具備された有限状態機械生成部と定常化有限状態機械変換部を使用し、
前記入出力装置から入力された各論理回路を記述する回路記述と各前記論理回路に与えられる入力信号に関する情報に基づいて、
前記有限状態機械生成部により、各論理回路について、前記回路記述で表された回路の複数の入力信号のうち、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械をそれぞれ生成する有限状態機械生成処理と、
前記定常化有限状態機械変換部により、前記有限状態機械生成処理によって生成した各論理回路に対応する有限状態機械を、各論理回路に対応する過渡的な状態への遷移を持たない定常化有限状態機械に変換する有限状態機械への変換処理と、
前記等価性検証部により、複数の回路記述から前記定常化有限状態機械生成部によって個別に生成された複数の定常化有限状態機械の論理的等価性を検証する等価性検証処理とを備えていることを特徴とする論理回路の検証方法。
【請求項６】
前記定常化有限状態機械生成部が予備的な有限状態機械生成部を備え、
この予備的な有限状態機械生成部により、前記論理回路を記述する回路記述に基づいて予備的な有限状態機械を生成する予備的な有限状態機械生成処理と、
前記有限状態機械生成部により、前記予備的な有限状態機械生成部によって生成された予備的な有限状態機械に基づいて、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械を生成するしょりを備えていることを特徴とする請求項５に記載の論理回路の形式検証方法。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、有限状態機械を利用した順序回路の形式検証方法及びその装置に関する。
【０００２】
【従来の技術】
近年のコンピューターを構成する回路などの論理回路の規模の増大に伴い、回路の設計期間やテスト期間を短縮するための技術、すなわち、論理合成技術、シミュレーション技術、形式検証技術などが年々重要視されてきている。これらの技術では、順序回路を扱う場合、通常、順序回路を有限状態機械を用いて数学的にモデル化し、この有限状態機械に対して、状態数の短縮、等価性の判定などの処理が行われる。近年では、有限状態機械の要素となる遷移関数や出力関数を二分決定ダイアグラムを用いてコンパクトに表現する技術が発達したことにより、上記の処理をより大規模な有限状態機械に適用することが可能となった。
【０００３】
上記技術の中で、形式検証技術は、等価性判定技術とモデルチェッキング技術に分けられる。前者は、二つの回路の論理的等価性を判定する技術であり、後者は、対象となる回路がユーザーの指定した論理的性質を満たすか否かを判定する技術である。
【０００４】
論理回路、特に、順序回路を対象としたこれらの形式検証技術では、与えられた回路を記述する回路記述から、これをモデル化する有限状態機械を構成するために、通常、図２５に示すような処理が行われる。まず、与えられた回路記述Ａ，Ｂに含まれる全ての入力信号の任意の値の組み合わせを入力アルファベットとする有限状態機械Ｍ0 Ａ，Ｍ0 Ｂを作る（ステップ３１）。そして、この回路に対する入力のうち、クロック信号に対応するものを、自動的、または、ユーザーによる情報を利用して検出する。更に、クロック信号がどのような値を取るときに、クロック信号以外の入力信号や出力信号の値が変化するかというようなタイミングに関する情報をユーザーから得る（ステップ３２）。そして、これを元に、前記有限状態機械Ｍ0 Ａ，Ｍ0 Ｂから、クロック信号以外の入力信号の任意の値の組み合わせを入力アルファベットとする有限状態機械（同期機械Ｍ1 Ａ，Ｍ1 Ｂ）を構成する（ステップ３３）。同期機械における状態遷移は、同期機械自身が内部に持っているクロックによって、処与のタイミングで起きると考える。そして、順序回路の等価性の検証技術では、二つの順序回路からこのようにして作った二つの同期機械Ｍ1 Ａ，Ｍ1 Ｂの間の論理的等価性を証明することにより、元の順序回路の間の等価性を検証し（ステップ３４）、その結果を出力する（ステップ３５）。
【０００５】
【発明が解決しようとする課題】
ところが、上記の等価性判定技術、すなわち、等価性を判定したい二つの順序回路の回路記述からそれぞれの同期機械を構成し、これらの論理的等価性を判明するという技術には次のような問題点がある。
【０００６】
近年では、通常の同期回路に比べ、より消費電力の少ない回路を作ることなどが重要視されてきているため、ゲート付クロックなどを用いて回路を実現することや、論理回路の一部を、フリップフロップやラッチなどの論理素子を用いず、トランジスタを組み合わせて実現することが必要となってきている。このような場合には、設計された回路の状態遷移や入出力信号の値の変化がユーザーの期待するクロック信号やその他の信号の変化のタイミングに応じて正しく起こるか否か自体が必ずしも保証されない。
【０００７】
このため、このような回路の間の等価性を、回路記述から同期機械を作ることによって行うと、もしも、回路記述中に誤って設計者の意図しないタイミングで状態遷移や入出力信号の値の変化が起こるようなことがあっても、これを検出できない場合が生ずる。
【０００８】
例えば、図１０（ａ）（ｂ）には、それぞれ、マスタスレーブ型ＪＫ−フリップフロップと、エッジトリガー型ＪＫ−フリップフロップをＮＡＮＤゲートなどを用いて実現する回路を示した。これら二つの回路は、クロック信号ｃｌｋの値が０である間のみに、その他の入力信号ｊ，ｋの値が変化し、状態遷移はクロック信号の立ち下がり時、すなわち、ｃｌｋ＝１からｃｌｋ＝０になる瞬間にのみ起きると仮定すると、全く等価な入出力の関係を示す。しかし、もし、クロック信号の値が１である間に入力信号の値が変化することがあるならば、これらの回路は異なる振る舞いを示す場合が存在する。
【０００９】
また、図１１は、ＪＫ−フリップフロップの動作をＶＨＤＬ言語による記述したものであるが、この記述は、同期機械を構成することによる形式検証を用いた場合には、図１０のどちらのＪＫ−フリップフロップ回路とも等価になるにもかかわらず、上述の理由と同じく実際には（ａ）の回路とは等価ではなく、（ｂ）の回路のみと等価である。
【００１０】
設計者が設計の始めの段階で、ある回路を実現するために、内部で図１０（ｂ）のエッジトリガー型ＪＫ−フリップフロップを用いており、これを同図（ａ）のマスタスレーブ型ＪＫ−フリップフロップに変更したとする。従来の検証技術では、検証を行うために、クロック信号の値が０である間のみに、入力信号ｊ，ｋの値が変化し、状態遷移はクロック信号の立ち下がり時に生じることのみを設計者が指定する。そのため、もしも、クロック信号の値が１である間にｊ，ｋの値が変化するような場合があっても、変更前後の違いを検出することができない。従って、設計者は、個別にモデルチェッキングによる検証などを用いて、クロック信号の値が１である間にｊ，ｋの値が変化しないことを検証しなくてはならない。しかし、設計者が必ずこの確認をするとは限らず、相違に気付かないまま、変更前後の回路を等価であると考えてしまうという問題がある。
【００１１】
【課題を解決するための手段】
上記問題点を解決するために、請求項１の発明は、複数の論理回路の等価性を形式的に検証する形式検証装置において、前記論理回路を記述する回路記述と、前記論理回路に与えられる入力信号に関する情報とから、前記論理回路に対応した定常化有限状態機械を生成する定常化有限状態機械生成部と、前記複数の回路記述から前記定常化有限状態機械生成部によって個別に生成された複数の定常化有限状態機械の論理的等価性を検証する等価性検証部と、前記等価性検証部の検証結果を出力する出力部とを備え、前記定常化有限状態機械生成部は、前記回路記述で表された回路の複数の入力信号のうち、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械を生成する有限状態機械生成部と、前記有限状態機械生成部によって生成した有限状態機械を、過渡的な状態への遷移を持たない定常化有限状態機械に変換する有限状態機械への変換部と、を備えることを特徴とする。
【００１２】
また、請求項５の発明は、前記請求項１の発明を方法の観点から把握したものであって、複数の論理回路の等価性を形式的に検証する形式検証方法において、入出力装置を備えたコンピュータとそれを制御するプログラムによって実現される定常化有限状態機械生成部、等価性検証部、前記定常化有限状態機械生成部に具備された有限状態機械生成部と定常化有限状態機械変換部を使用し、前記入出力装置から入力された各論理回路を記述する回路記述と各前記論理回路に与えられる入力信号に関する情報に基づいて、前記有限状態機械生成部により、各論理回路について、前記回路記述で表された回路の複数の入力信号のうち、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械をそれぞれ生成する有限状態機械生成処理と、前記定常化有限状態機械変換部により、前記有限状態機械生成処理によって生成した各論理回路に対応する有限状態機械を、各論理回路に対応する過渡的な状態への遷移を持たない定常化有限状態機械に変換する有限状態機械への変換処理と、前記等価性検証部により、複数の回路記述から前記定常化有限状態機械生成部によって個別に生成された複数の定常化有限状態機械の論理的等価性を検証する等価性検証処理とを備えていることを特徴とする。
【００１３】
このような構成を有する請求項１または請求項５の発明によれば、等価性を検証する二つの論理回路の記述に対して、入力信号のうちいずれの信号が他の入力信号と全く同時に変化することがないかということなどを指定した情報を元にして、定常化有限状態機械生成部によって、それぞれ個別に、定常化有限状態機械を生成する。この情報は、従来技術のように入出力信号値の変化する時のクロックの値などの多くの情報をユーザーが指定するものとは異なり、入力信号のうちいずれがクロック信号であるかを指定する程度の非常に少ない情報だけでよい。定常化有限状態機械生成部によって作られた定常化有限状態機械は、任意の入力信号の値の変化のタイミングに対し、一意的に定義された状態遷移を行い、かつ、過渡的な状態への遷移を持たないという特徴を有する。従って、本発明を用いれば、与えられた二つの論理回路の記述から生成した二つの定常化有限状態機械の論理的等価性を等価性検証部において形式検証することにより、複数の入出力信号の値の変化のタイミングを考慮した順序回路の形式検証を行うことが可能となる。
【００１４】
更に、このような構成の請求項１または請求項５に記載の発明によれば、例えば、通常の順序回路と、これをゲート付きクロックを用いて実現した回路の間の検証や、一つの回路の中にクロックの立ち上がりで遷移する部分と立ち下がりで遷移する部分を共に含むような回路の間の等価性の検証が可能である。特に、同期機械を用いて検証を行う場合、設計した回路の中に、誤りにより設計者の意図しないクロックのタイミングで入力信号が変化する場合や、設計者の意図しないクロックのタイミングで状態遷移を起こしてしまう場合がある。このような場合が含まれるとき、この誤りを同期機械の構成の際に打ち消してしまうことがある。本発明では、同期機械を構成することなく、等価性の検証を行うことにより、このような問題点を解決する。
【００１５】
請求項２の発明は、前記請求項１の発明において、前記定常化有限状態機械生成部は、前記論理回路を記述する回路記述に基づいて予備的な有限状態機械を生成する予備的な有限状態機械生成部を備え、一意的に定義された状態遷移を行う有限状態機械を生成する有限状態機械生成部は、前記予備的な有限状態機械生成部によって生成された予備的な有限状態機械に基づいて、所定の入力信号とその他の入力信号の変化のタイミングに対し、一意的に定義された状態遷移を行う有限状態機械を生成するものであることを特徴とする。また、請求項６の発明は、前記の請求項２の発明を方法の観点から把握したものである。
【００１６】
前記のような請求項２および請求項６の発明によれば、前記論理回路を記述する回路記述と、前記論理回路に与えられる入力信号に関する情報とから、予備的な有限状態機械、一意的に定義された状態遷移を行う有限状態機械、過渡的な状態への遷移を持たない定常化有限状態機械と言うように順次性質の異なる有限状態機械を生成することで、論理回路の持つクロック、その他の入力信号値の変化に対する状態遷移、及び出力の関係を、クロック信号値の変化に対するタイミングを含めて正しく表現することが容易となり、等価性検証部において回路の詳細に立ちいることなく等価性の検証を行うことが可能となる。
【００１７】
請求項３の発明は、前記有限状態機械生成部が、クロック信号と他の信号の値が同時に変化するタイミングに対して、一義的に定義された状態遷移を行う有限状態機械を生成することを特徴とする。この請求項３の発明によれば、クロック信号と他の入出力信号の値の変化のタイミングの関係まで考慮した有限状態機械を生成することができ、論理回路のより正確な検証が実施できる。
【００１８】
請求項４の発明は、前記出力部が、定常化有限状態機械生成部において見いだした情報をも出力するものである。この請求項４の発明によれば、前記出力部は検証結果を出力するのみならず、例えば定常化有限状態機械の生成時に発見された状態の不安定性なども出力することができ、定常化有限状態機械の変換を効率良く実施できる。
【００１９】
【発明の実施の形態】
以下、図面を参照しながら本発明の一実施形態について説明する。
なお、後述する実施形態はコンピュータ上に実現され、実施形態の各機能は、所定の手順（プログラム）がこのコンピュータを制御することで実現される。例えば、入力部は、入力するプログラムやデータの態様によって種々のものを採用することができ、キーボードやマウスなどの入出力装置、ネットワーク接続装置、データ読み取り装置などを使用できる。また、各記憶部は、外部から入力したデータを蓄えるためのものであり、磁気や光ディスク装置、半導体メモリ等の所望の装置を用いることができる。さらに、他の部分は、コンピュータのソフトウェアによって構成されることが典型的である。
【００２０】
本明細書における各「部」は、実施形態の各機能に対応する概念的なもので、必ずしも特定のハードウェアやソフトウェア・ルーチンに１対１には対応しない。同一のハードウェア要素が、場合によって異なった部を構成する。例えば、コンピュータは、ある命令を実行するときにある部となり、別の命令を実行するときは別の部となりうる。また、一つの部が、わずか１命令によって実現される場合もあれば、多数の命令によって実現される場合もある。したがって、本明細書では、以下、実施形態の各機能を有する仮想的回路ブロック（部）を想定して実施形態を説明する。また、本実施形態における各手順の各ステップは、その性質に反しない限り、実行順序を変更し、複数同時に実行し、また、実行ごとに異なった順序で実行してもよい。
【００２１】
また、本発明をコンピュータのソフトウェアとして実現した場合には、そのソフトウェアを磁気あるいは光などを利用した記録媒体に記録しておき、これを個々の設計者が読み出して自己のコンピュータによって実行することも、本発明の実施形態の一つである。
【００２２】
［Ａ．第１実施形態］
［１．有限状態機械と定常化有限状態機械］
［１−１．有限状態機械の定義］
本発明の入力となる有限状態機械の定義を行う。
有限状態機械Ｍとは、図４に示すとおり、有限個の要素よりなる入力記号の集合（以下入力アルファベットという）Ｉ、有限個の要素よりなる出力記号の集合（以下出力アルファベットという）Ｏ、有限個の要素よりなる状態の集合Σ、遷移関数δ、出力関数ω、初期状態Ｓinitの６つの組を指定したものである。これを、有限状態機械Ｍ＝（Ｉ，Ｏ，Σ，δ，ω，Ｓinit）と表記する。ここで、遷移関数δは、Σ×ＩからΣへの関数であり、出力関数ωは、Σ×ＩからＯへの関数であり、初期状態Ｓinitは、Σのある一つの要素、即ち、Ｓinit∈Σである。入力ｉ∈Ｉが与えられたときの、状態δ∈Σの、遷移関数δによる遷移先をδ（ｓ，ｉ）と表記し、出力関数ωによる出力をω（ｓ，ｉ）と表記する。以下では、特に混乱を招かない限り、δ，ωと、δ（ｓ，ｉ），ω（ｓ，ｉ）を区別しない。
【００２３】
［１−２．有限状態機械の具体例］
図５（ａ）は、有限状態機械の一具体例であり、入力アルファベットをＩ＝｛０，１｝、出力アルファベットをＯ＝｛０，１｝、そして、状態の集合をΣ＝｛Ａ，Ｂ｝としている。状態は２００のように、状態名を丸で囲むことによって表す。各状態から出る矢印２０１に添えられた数字の組２０２と２０３は、矢印２０１の始点となる状態において、入力値２０２が与えられると、矢印の終点となる状態に遷移し、この遷移に伴う出力値が２０３となることを意味している。図５（ａ）の例では、状態Ａにおいて入力０が与えられたとき、遷移先の状態はＡであり、これに伴い１を出力する。状態Ａにおいて入力１が与えられたとき、遷移先の状態はＢであり、これに伴い１を出力する。状態Ｂにおいて入力０が与えられたとき、遷移先の状態はＢであり、これに伴い１を出力する。状態Ｂにおいて入力１が与えられたとき、遷移先の状態はＡであり、これに伴い０を出力する。２０４は状態名を二重丸で囲んだもので、これにより、Ｂが初期状態であることを表現している。
【００２４】
なお、本明細書における有限状態機械の表現は、この図５に限らず、図１２などに示すように、状態名と出力値をＡ／０のように丸で囲み、入力値を０――のように遷移先を示す矢印に添えて記載する表現も使用する。
【００２５】
大部分の順序回路は、電源を入れた直後の内部状態が一意的に定まらない。このため、その順序回路を有限状態機械でモデル化するとき、初期状態が指定できない場合がある。図５（ｂ）は、このような場合の有限状態機械を表しており、初期状態を明示していない。初期状態を指定しない有限状態機械を以後有限状態機械をＭ＝（Ｉ，Ｏ，Σ，δ，ω）と表記する。本発明では、このように初期状態が明示されない有限状態機械と、初期状態が明示された有限状態機械とを、ほとんどの場合に全く同様に扱うことが可能である。即ち、本発明の対象とする有限状態機械は、通常の有限状態機械とは異なり、必ずしもΣの一要素である初期状態を持つことを必要としないため、電源を入れた直後の内部状態が一意的に定まらないような順序回路をも扱うことが可能である。
【００２６】
［１−３．定常状態集合、安定状態、不安定状態、過渡的状態、過渡的遷移］
有限状態機械Ｍ＝（Ｉ，Ｏ，Σ，δ，ω）において、ある入力ｉ∈Ｉが与えられ続けたとき、要素数ｔ≧１個のΣの部分集合Ｓ＝｛ｓ0 ，ｓ1 ，…，ｓt-1 ｝⊆Σに含まれる任意の状態が、常にＳに含まれる状態にのみ遷移し、かつ、Ｓに含まれる全ての状態に遷移しうるとき、Ｓを有限状態機械Ｍの入力ｉ∈Ｉに対する定常状態集合と呼ぶ。また、特に、要素数が１の定常状態集合に含まれる状態を、有限状態機械Ｍの入力ｉ∈Ｉに対する安定状態と呼ぶ。逆に、要素数が２以上の定常状態集合に含まれる状態を、有限状態機械Ｍの入力ｉ∈Ｉに対する不安定状態と呼ぶ。
【００２７】
有限状態機械Ｍ＝（Ｉ，Ｏ，Σ，δ，ω）において、有限状態機械Ｍの入力ｉ∈Ｉに対する定常状態集合に含まれない状態を、有限状態機械Ｍの入力ｉ∈Ｉに対する過渡的状態と呼ぶ。また、過渡的状態からの遷移を過渡的遷移と呼ぶ。これらの各集合の関係については、図６に示すとおりである。
【００２８】
［１−４．状態の安定性］
図８は、有限状態機械の一例である。この有限状態機械は、入力アルファベットをＩ＝｛０，１｝、出力アルファベットをＯ＝｛０，１｝、そして、状態の集合をΣ＝｛Ａ，Ｂ，Ｃ，Ｄ，Ｅ，Ｆ，Ｇ，Ｈ｝としており、初期状態を指定していない。例えば、状態Ｅから出発して、入力１が与えられ続けると、過渡的状態Ａを経由して、最終的に状態Ｂに遷移し、これより後、入力１が与えられ続けても常に状態Ｂに留まっている。この性質を状態Ｂは「入力１に対する安定状態」にあるという。また、例えば、状態Ａから出発して、入力０が与えられ続けると、過渡的状態Ｅと過渡的状態Ｆを経由して、状態Ｇに遷移し、これより先、入力０が与えられ続けると、状態Ｂ、状態Ｃ、状態Ｇの順に、これら三つの状態を周期的に遷移し続ける。この性質を状態の集合｛Ｂ，Ｃ，Ｇ｝は「入力０に対する定常状態集合」にあるという。
【００２９】
図９の有限状態機械Ｍでは、入力０に対しては、安定状態はなく、定常状態集合は、｛Ｂ，Ｃ，Ｇ｝と｛Ｄ，Ｈ｝であり、過渡的状態は、ＡとＥとＦであり、不安定状態は、ＢとＣとＧとＤとＨである。入力１に対しては、安定状態はＢのみであり、定常状態集合は、｛Ｂ｝と｛Ｃ，Ｆ，Ｇ，Ｈ｝であり、過渡的状態は、ＡとＤとＥであり、不安定状態は、ＣとＦとＧとＨである。
【００３０】
［１−５．定常化有限状態機械］
以下に、定常化有限状態機械の定義を行う。
入力として与えられた有限状態機械から過渡的状態への遷移を消去して、対応する定常化有限状態機械を生成することが、本発明における定常化有限状態機械への変換部の目的である。
【００３１】
有限状態機械Ｍ＝（Ｉ，Ｏ，Σ，δ，ω）に対応する定常化有限状態機械 newＭ＝（Ｉ，Ｏ，Σ， newδ， newω）とは、有限状態機械Ｍと同じ入力アルファベット、出力アルファベット、及び同じ状態の集合を持つ。なお、初期状態の指定された有限状態機械Ｍ＝（Ｉ，Ｏ，Σ，δ，ω，ｓinit）に対しては、 newＭも同じ初期状態を持つ。
【００３２】
定常化有限状態機械の遷移関数 newδは、以下の性質を持つ。
(1) 有限状態機械Ｍの入力ｉ∈Ｉに対する定常状態集合は、 newＭにおいても、同じ入力ｉに対する定常状態集合となり、かつ、この集合に含まれる状態は、入力ｉによって有限状態機械Ｍの遷移先と同じ状態に遷移する。なお、この条件は、有限状態機械Ｍと newＭは、任意の入力ｉに対して同じ安定状態を持つことも意味している。
【００３３】
(2) もしも、有限状態機械Ｍの入力ｉ∈Ｉに対する過渡的状態ｓが、入力ｉを与えられ続けたとき、定常状態集合Ｓに含まれる状態に遷移するならば、 newＭにおいて、この状態ｓは、入力ｉを与えられたとき、一回の遷移でＳに含まれる状態に遷移する。
【００３４】
(3) そして、出力関数 newωは、以下の性質を持つ。有限状態機械Ｍの入力ｉ∈Ｉに対する安定状態からの、入力ｉによる遷移に伴う出力は newＭにおいても等しい。
【００３５】
(4) もしも、有限状態機械Ｍの入力ｉ∈Ｉに対する過渡的状態ｓが、入力ｉを与えられ続けたとき、安定状態に遷移するならば、 newＭにおいて、この状態ｓの入力ｉを与えられたときの遷移に伴う出力は、安定状態における出力に等しい。
なお、上の定義では、不安定状態からの遷移に伴う出力や、不安定状態への過渡的遷移に伴う出力は、特に定めていない。
【００３６】
このように定義された定常化有限状態機械と、定常化されていない有限状態機械とを、ある状態において入力ｉが１回与えられた場合にどのような状態に遷移するかを比較する。その結果は、図７に示すとおりである。この図７から明らかなように、定常化有限状態機械と定常化されていない有限状態機械とでは、図中（Ｃ）のように、１回の入力ｉに対する過渡的状態への遷移があるか否かによる違いがある。従って、本発明における定常化有限状態機械への変換部の目的は、過渡状態への遷移（図中（Ｃ）に示すような遷移）がない有限状態機械を得ることにある。
【００３７】
［１−６．定常化有限状態機械の具体例］
図９に示した有限状態機械 newＭは、図８の有限状態機械Ｍに対応する定常化有限状態機械であり、上記の性質を全て満たしている。例えば、有限状態機械Ｍの入力０に対する定常状態集合｛Ｄ，Ｈ｝は、 newＭにおいても、入力０に対する定常状態集合となっている。更に、この定常状態集合｛Ｄ，Ｈ｝に含まれる状態Ｄは、入力０が与えられたとき有限状態機械Ｍにおいても、 newＭにおいても、状態Ｈに遷移し、状態Ｈは、入力０が与えられたとき有限状態機械Ｍにおいても、 newＭにおいても、状態Ｄに遷移する。また。有限状態機械Ｍの入力０に対する過渡的状態Ａは、入力０が与えられ続けたとき、過渡的状態Ｅ，Ｆを経由して、定常状態集合｛Ｂ，Ｃ，Ｇ｝に含まれる状態Ｇに到達し、その後、｛Ｂ，Ｃ，Ｇ｝の中をサイクリックに遷移し続けるのに対し、 newＭでは、入力０に対する過渡的状態Ａは、入力０が一度与えられたとき、過渡的状態を経由することなく、直ちに、定常状態集合｛Ｂ，Ｃ，Ｇ｝に含まれる状態Ｂに到達し、その後、入力０が与えられ続けたとき、｛Ｂ，Ｃ，Ｇ｝の中をサイクリックに遷移し続ける。また、有限状態機械Ｍの入力１に対する安定状態Ｂは、 newＭにおいても、入力１に対する安定状態であり、この状態Ｂにおいて、入力１が与えられ続ける限り。有限状態機械Ｍ、 newＭ共に安定な出力値を出力し続ける。そして、入力１でＢに遷移する過渡的状態ＡとＥは、どちらも、この遷移に伴って、安定な出力値０を出力する。
【００３８】
［２．本実施形態の論理回路の形式検証装置］
［２−１．全体の構成］
本発明の論理回路の形式検証装置の一実施形態の概要を、図１により説明する。図１に記載の有限状態機械変換装置は、コンピュータ上に実現される。このコンピュータは、中央演算装置（ＣＰＵ）１、キーボードやマウスなどの入力装置２、ＣＲＴディスプレイやプリンタなどの出力装置３、及びメモリやハードディスクなどの記憶装置４を備えている。これらの各装置は、バス５によって接続され、相互に情報が交換される。
【００３９】
本実施形態の変換装置は、このようなコンピュータ上において実行される次のような各部分を持つプログラムとして構成されている。
【００４０】
(1) 検証対象となる回路記述の入力部１０。
【００４１】
(2) 回路中の入力信号のうち、いずれの信号がクロック信号であるかを示す記述を入力とする補助信号入力部１１。
【００４２】
(3) 前記の回路記述及び補助情報に基づいて、過渡的状態への遷移がない定常化有限状態機械 newＭを生成する定常化有限状態機械生成部１２。
【００４３】
(4) 前記定常化有限状態機械生成部１２に設けられ、クロック信号の変化のタイミングによる解釈の任意性を含んでいる予備的な有限状態機械Ｍ0 を生成する第１の有限状態機械の生成部１３。
【００４４】
(5) 前記定常化有限状態機械生成部１２に設けられ、前記予備的な有限状態機械Ｍ0 と補助情報に基づいて、クロック信号を特定してその変化のタイミングによる解釈の任意性を排除した有限状態機械Ｍを生成する第２の有限状態機械生成部１４。
【００４５】
(6) 前記定常化有限状態機械生成部１２に設けられ、前記有限状態機械生成部１４で生成された有限状態機械Ｍを、過渡的状態への遷移を除去した定常化有限状態機械 newＭへ変換するための変換部１５。
【００４６】
(7) 前記の変換部１５によって得られた定常化有限状態機械 newＭの複数個を比較して、その等価性を検証する等価性検証部１６。
【００４７】
(8) 前記等価性検証部１６で得られた検証結果や、前記定常化有限状態機械生成部１２で得られた回路の不安定性などを出力する結果出力部１７。
【００４８】
［２−２．全体の作用］
図２は、前記図１の検証装置において、２つの回路の等価性を検証する際の作用を説明する図である。図３は、本実施形態の検証装置の動作順序を示すフローチャートである。図２において、回路記述１００Ａと回路記述１００Ｂは、等価性の検証を行う二つの論理回路の記述、補助情報２００は、回路記述Ａと回路記述Ｂに記述された回路中の入力信号のうち、いずれの信号がクロック信号であるかなどを示す記述である。即ち、これらの記述は、回路記述入力部１０や補助情報入力部１１から本装置に入力されるもので、例えばＶＨＤＬ言語のようなハードウェア記述言語による回路の動作記述や、論理素子間のネットリストによる回路記述、トランジスタネットリストによる回路記述などである。
【００４９】
本実施形態では、まず、回路記述入力部１０より定常化有限状態機械生成部１２に回路記述１００Ａと回路記述１００Ｂがそれぞれ個別に入力として渡される（ステップ３０１）。定常化有限状態機械生成部１２の第１の有限状態機械生成部１３では、この回路記述１００Ａと回路記述１００Ｂに基づいて、これら回路記述に対応する予備的な有限状態機械Ｍ0 ＡとＭ0 Ｂ生成する（ステップ３０２）。補助情報入力部１１からは、前記各回路記述１００Ａ，Ｂと対になった補助情報２００が定常化有限状態機械生成部１２に渡される（ステップ３０３）。定常化有限状態機械生成部１２の第２の生成部１４では、この補助情報２００に基づいてクロック信号を特定し、その変化のタイミングを考慮して遷移先を特定することによって、前記の予備的な有限状態機械Ｍ0 から解釈の任意性を除去した有限状態機械ＭＡ，ＭＢを生成する（ステップ３０４）。
【００５０】
定常化有限状態機械への変換部１５では、前記のようにして得られた有限状態機械ＭＡ，ＭＢを、過渡的状態への遷移を消去した定常化有限状態機械 newＭＡ， newＭＢとに変換する（３０５）。この変換部１５によって得られる定常化有限状態機械 newＭＡ， newＭＢは、変換前の有限状態機械ＭＡ，ＭＢと同じ安定状態を持ち、かつ、安定状態においては有限状態機械ＭＡ，ＭＢと同じ出力をする一方、任意の過渡的状態からの遷移に関しては有限状態機械ＭＡ，ＭＢと異なり、直ちに安定状態に遷移するという性質を持つ。これによって、有限状態機械ＭＡ，ＭＢの瞬時的かつ、本質的でない振舞いが除去される。
【００５１】
そして、等価性検証部１６によって、定常化有限状態機械 newＭＡ， newＭＢの間の等価性を形式的に検証し（ステップ３０６）、この結果を出力部１７において出力する（ステップ３０７）。また、出力部１７では、定常化有限状態機械生成部１２において見い出された各回路の不安定性などの情報を出力する。
【００５２】
［２−３．予備的な有限状態機械生成部１３］
次に、定常化有限状態機械生成部１２に設けられた予備的な有限状態機械生成部１３の働きを例を用いて説明する。例えば、図１０（ａ）に示したマスタスレーブ型ＪＫ−フリップフロップを実現する回路から有限状態機械Ｍを作る場合、以下の手順により、回路記述１００の情報のみを用いてまず予備的な有限状態機械Ｍ0 を作り、続いて、補助情報２００を用いて、予備的な有限状態機械Ｍ0 から求める有限状態機械Ｍを作る。
【００５３】
予備的な有限状態機械Ｍ0 を作るには、例えば、回路記述１００が図１０のような論理素子間のネットリスト記述の場合、まず、回路記述１００の信号の流れからフィードバックループを見い出し、これから状態ビットを見い出す。ただし、このとき、クロック信号は他の入力信号と同様に一つの入力信号として扱い、特別には扱わない。回路記述全体から見い出された各状態ビットは、０または１の値を取り得るとし、これらの値の任意の組合わせが、有限状態機械Ｍ0 の状態集合の要素となる一つの状態を構成する。そして、入力信号、及び、状態ビットの値と出力信号、及び、状態ビットの値との関係から、有限状態機械Ｍ0 の出力関数と遷移関数を決定する。このようにして、図１０（ａ）の回路からは、例えば、図１２に示した有限状態機械Ｍ0 が作られる。なお、この図の有限状態機械では、初期状態を指定していない。また、図１２においては、状態名と出力値をＡ／０のように丸で囲み、入力アルファベット［ｃｌｋ，ｊ，ｉ］を０――のように遷移先を示す矢印に添えて表現する。
【００５４】
また、回路記述１００にトランジスタネットリストで記述された回路が与えられた場合には、例えば、下記の(1) から(3) に述べられている手法などを用いて、この回路に対応する有限状態機械Ｍ0 を構成する。
【００５５】
(1) T.Kam and P.A.Subrahmanyam, “State Machine Abstraction from Circuit Layouts using BDD′s: Applications in Verification and  Synthesis", in Proc. European Design  Automation Conf.,1992, pp. 92-97
（２）  Ｊ．Ｍｏｏｎｄａｎｏｓ，  Ｊ．Ａ．Ｗｅｈｂｅｎ，  Ｊ．Ａ．Ａｂｒａｈａｍ  ａｎｄ  Ｄ．Ｇ．Ｓａａｂ，“VERTEX: VERification of Transistor-level circuits based on model EXtracation", in Proc. The European Conf. on Design Automation with the European Event in ASIC Design,1993,pp.111-115
（３）  Ｍ．Ｐａｎｄｅｙ，  Ａ．Ｊａｉｎ，  Ｒ．Ｅ．Ｂｒｙａｎｔ，  ｅｔ  ａｌ．，  “Extraction of Finite State Machines from Transistor Netlists by Symbolic Simulation", in Proc. of International Conference on Computer Design′95, pp.596-601
［２−４．解釈の任意性を含まない有限状態機械の生成部１４］
［２−４−１．予備的な有限状態機械Ｍ0 から作成した同期機械の問題点］
前記のようにして予備的な有限状態機械Ｍ0 を生成した後は、(d) のような公知の技術では、これに続いて同期機械を作成する。
【００５６】
(4) J.Bormann, J.Lohse, M.Payer and G.Venzl,“Model Checking in Industrial Hardware Design" ,in 32th ACM/IEEE Design Automation Conference,1995, pp.298-303
例えば、前記(4) の技術では、ここで作った有限状態機械Ｍ0 から、「クロック信号のいかなるタイミングで入出力信号値の変化が生じるか。」といった情報をユーザーから得ることにより、クロック信号を陽に含まない有限状態機械（同期機械）Ｍ1 を生成する。このユーザーから得る情報は、例えば、クロック信号の値が０である間にのみ、その他の入力信号の値が変化し、クロック信号の値が１の間はその他の入力信号の値は変化せず、クロック信号の値が１から０になる瞬間（クロック信号の立ち下がり時）に出力信号値が変化すると言うものである。
【００５７】
図１３は、図１２から、クロック信号の値が０である間にのみ、入力信号ｊ，ｋの値が変化し、クロック信号の立ち下がり時に状態遷移が起こるという情報を用いて生成した同期機械の例である。しかし、この手法には、設計された回路中に、誤りによって設計者の意図しないタイミングで入力信号が変化するような状況などが含まれる場合に、これを正しく検出することができないという問題点がある。実際、この手法を用いた場合、図１０（ａ）（ｂ）からは、共に、図１３の同期機械が作られ、二つの回路の間の非等価性を検出できなくなってしまう。
【００５８】
［２−４−２．有限状態機械Ｍ0 におけるの解釈の任意性］
そこで、本発明では、出力信号値の変化のタイミングとクロック信号を含む任意の入力信号値の変化のタイミングとの関係を保つために、有限状態機械Ｍ0 から同期機械を構成することを行わず、クロック信号を陽に入力信号として含む有限状態機械を形式検証の対象とする。
【００５９】
ただし、回路記述１００のみから先に述べた手法で構成した有限状態機械Ｍ0 には、クロック信号と全く同時にその他の入力信号が変化したときに、この変化がクロック信号の変化の直前、または、直後のいずれで生じたと解釈するかによる任意性がある。この任意性により、本発明で等価性を検証する二つの回路記述が、実際には等価な回路の記述であったも、それらから構成した有限状態機械は、論理的に非等価となってしまうことがあり得る。
【００６０】
例えば、図１４（ａ）（ｂ）に示した二つの有限状態機械は、どちらもクロック信号ｃｌｋとその他の信号ａの二つの入力信号よりなる入力アルファベットと、１ビットの出力信号よりなる出力アルファベットを持ち、それぞれ、状態Ａ、及び、状態Ｄを初期状態に持つ。これらの初期状態は、いずれもｃｌｋ＝１，ａ＝０のときに０を出力し続ける安定状態である。これらの有限状態機械において、ｃｌｋの値が０になる直前に入力信号ａの値が０から１に変化すると、図１５（ａ）（ｂ）に示したように、どちらの有限状態機械も出力信号の値がｃｌｋの立ち下がりと同時に０から１に変化する。また、入力信号ａの値の変化が、ｃｌｋの値が０になった直後である場合には、図１６（ａ）（ｂ）に示したように、どちらの有限状態機械の出力信号の値も０に留まっている。従って、これらの状況だけを考えるならば、二つの有限状態は等価に振舞う。しかし、ｃｌｋの値が１から０になる変化と全く同時にａの値が０から１に変化する場合には、図１７（ａ）（ｂ）に示したように、前者は出力信号の値が０から１に変化し、後者は出力信号の値が０に留まる。
【００６１】
従って、図１４（ａ）（ｂ）の有限状態機械は、クロック信号とその他の入力信号ａの値が全く同時に変化する場合の解釈の任意性、すなわち、前者の有限状態機械は、クロック信号とその他の入力信号ａの値が全く同時に変化する場合、クロック信号の方が一瞬遅れて変化すると解釈され、一方、後者の有限状態機械は、逆にクロック信号の方が一瞬早く変化すると解釈されることが原因となり、両者が非等価となってしまう。しかし、実際の回路では、このような状況は有り得ないので、解釈の任意性が存在することは望ましくない。
【００６２】
［２−４−３．解釈の任意性を含まない有限状態機械Ｍの生成］
本発明では、前記のような予備的な有限状態機械Ｍ0 における解釈の任意性によって発生する問題を解決する。そのために、第２の有限状態機械生成部１４において、予備的な有限状態機械Ｍ0 から解釈の任意性を含まない新たな有限状態機械Ｍを次のようにして構成する。そして、次に、この解釈の任意性を含まない有限状態機械Ｍを、さらに過渡的遷移を含まない定常化有限状態機械 newＭに変換して、等価性を検証する。
【００６３】
第２の有限状態機械生成部１４において、有限状態機械Ｍ0 から有限状態機械Ｍを構成するには、次のようにする。例えば、回路記述１００が一つのクロック信号によって動作が制御される場合、まず、補助情報入力部１１を介して得られた補助情報２００によってクロック信号ｃｌｋを特定し、クロック信号の直前の値を保持する状態ビットｃを導入する。そして、図１８に示すように、ｃの値が０であるか１であるかに応じて、有限状態機械Ｍ0 に含まれている各状態ｓをそれぞれ二つの状態ｓ0 ，ｓ1 に分け、これらを有限状態機械Ｍの状態とする。今、有限状態機械Ｍ0 においてｃｌｋ＝０その他の入力値がｉのときの状態ｓの遷移先をｓ′（ｉ，０）とし、ｃｌｋ＝１その他の入力値がｉのときの状態ｓの遷移先をｓ′（ｉ，１）とする。
【００６４】
このとき、図１９に示すように、有限状態機械Ｍにおいては、Ｓ0 の遷移先を、ｃｌｋ＝０その他の入力値がｉのとき、ｓ′0 （ｉ，０）、ｃｌｋ＝１その他の入力値がｉのときｓ′1 （ｉ，０）となるように定め、ｓ1 の遷移先を、ｃｌｋ＝０その他の入力値がｉのときｓ′0 （ｉ，１）、ｃｌｋ＝１その他の入力値がｉのときｓ′1 （ｉ，１）となるように定める。
【００６５】
このようにして、有限状態機械Ｍの遷移関数δを、
【数１】
ｓ′c ＝δ（ｓc ，ｉ，clk ）＝（δ0 （ｓ，ｉ，c ））clk 
によって決定する。ここで、ｃはクロック信号の直前の値を保持する状態ビット、ｉはクロック以外の入力信号、ｓは予備的な有限状態機械Ｍ0 の状態、δ0 （ｓc ，ｉ，clk ）は予備的な有限状態機械Ｍ0 の遷移関数である。同様に、有限状態機械Ｍの出力関数ωを
【数２】
ｏ＝ω（ｓc ，ｉ，clk ）＝ω0 （ｓ，ｉ，c ）
によって決定する。ここで、ω0 は、予備的な有限状態機械Ｍ0 の出力関数である。
【００６６】
［２−４−４．解釈の任意性を含まない有限状態機械Ｍの例］
以上の方法を用いて、図１４（ａ）（ｂ）に示した有限状態機械から作った有限状態機械の例を、それぞれ、図２０（ａ）（ｂ）に示す。なお、この図の例、及び、図１４、図２１の例では、説明の便宜上、初期状態を定めた有限状態機械を例としたが、後に述べる等価性検証部において用いるアルゴリズムによっては、初期状態の指定は必要ではないことがある。そのような場合には、予備的な有限状態機械Ｍ0 から、有限状態機械Ｍを構成する際、初期状態を定める方法は特に指定する必要がない。一方、等価性検証部において用いるアルゴリズムが初期状態を必要とする場合には、補助情報２００を元に、予備的な有限状態機械Ｍ0 の初期状態ｓinitを見い出し、次に、有限状態機械Ｍにおいて、ｓinitの状態を二つに分けたｓinit 0，ｓinit 1のいずれが初期状態となるかを決定する必要がある。
【００６７】
以上の例では、定常化有限状態機械生成部に入力として与えられる回路記述として、それのみではクロック信号を特定できない場合を説明した。一方、図１１に示したような、ＶＨＤＬ言語のレジスター転送レベルによる回路記述などが定常化有限状態機械生成部に与えられた時には、通常は、「’ＥＶＥＮＴ」や「’ＬＡＳＴ＿ＶＡＬＵＥ」のような属性の付けられた信号をクロック信号と解釈できることが多い。そして、このような場合には、自然に、直前のクロック信号の値を状態ビットとして定めることができる。しかし、ゲート付クロックを含むような回路記述などには、クロック信号に上のような属性が付けられていないこともあり得る。このため、一般に、クロック信号を一つ持つ回路に対する回路記述では常に補助情報によって、外部からクロック信号を指定し、これによって指定されたクロック信号の直前の値を状態ビットと定める方が、適切に有限状態機械Ｍ0 を構成することができる。
【００６８】
［２−５．定常化有限状態機械への変換部１５］
上のようにして作った有限状態機械Ｍは、元の有限状態機械Ｍ0 と異なり、ある状態において、ある入力が与えられたとき、安定状態に遷移するためにいくつかの過渡的状態を経由することがある。例えば、図１４（ａ）の有限状態機械を有限状態機械Ｍ0 とすると、状態Ａは、ｃｌｋ＝１，ａ＝１の入力が与えられ続けたとき、状態Ａに留まっているので安定状態という。また、このとき値０を出力し続けている。続いて、ｃｌｋ＝０と変化すると状態Ｃに遷移し、この後状態Ｃに留まって１を出力し続ける。従って、状態Ｃも安定状態である。これに対し、有限状態機械Ｍ0 から構成した図２０（ａ）の有限状態機械Ｍでは、ｃｌｋ＝１，ａ＝１で０を出力し続ける安定状態Ａ1 においてｃｌｋ＝０となると、状態Ａ0 に遷移した後、直ちに状態Ｃ0 に遷移し、その後、安定状態Ｃ0 に留まって１を出力し続ける。ここで見られる状態Ａ0 のような状態を過渡的状態と呼び、この例のように、元の有限状態機械Ｍ0 に過渡的状態への遷移が含まれていなくても、これから構成した有限状態機械Ｍには含まれることがある。
【００６９】
本発明では、有限状態機械Ｍに含まれる過渡的状態への遷移を取り除くために、定常化有限状態機械への変換部１５を用いて、有限状態機械Ｍを過渡的状態への遷移を行わないことを特徴とする定常化有限状態機械 newＭに変換する。この変換を効率的に行うための技術としては、例えば、前記(1) (3) が知られている。また、公知技術ではないが、本発明者の開発にかかる反復二乗法を使用した変換方法を用いることもできる。
【００７０】
図２０（ａ）（ｂ）に示した有限状態機械Ｍを有限状態機械変換部１２において上記技術を用いて変換した定常化有限状態機械 newＭの例を、それぞれ図２１（ａ）（ｂ）に示す。例えば、図２０（ａ）の有限状態機械Ｍでは、ｃｌｋ＝１，ａ＝１で０を出力し続ける安定状態Ａ1 において、ｃｌｋ＝０となると、０を出力する過渡的状態Ａ0 を経由して、その後、１を出力し続ける安定状態Ｃ0 に遷移するのに対し、図２１（ａ）の定常化有限状態機械 newＭでは、同じ安定状態Ａ1 において、ｃｌｋ＝０となると、どの過渡的状態へも遷移することなく、有限状態機械Ｍの場合の遷移先と同じ安定状態Ｃ0 に遷移する。更に、図２２（ａ）（ｂ）、図２３（ａ）（ｂ）及び図２４（ａ）（ｂ）に示したように、図２１（ａ）（ｂ）の定常化有限状態機械 newＭは、クロック信号ｃｌｋとその他の入力信号ａとが全く同時に変化する場合も含めて、入出力の関係が等価となる。
【００７１】
このようにして、本発明における定常化有限状態機械生成部１２は、与えられた回路記述と補助情報とから、予備的な有限状態機械の生成部と解釈の任意性を排除した有限状態機械の生成部と、さらに定常化有限状態機械への変換部とを用いることにより、定常化有限状態機械 newＭを生成し、この定常化有限状態機械 newＭは、クロック信号の値の変化と全く同時にその他の入力信号の値が変化するような実際の回路ではあり得ない状況に対しては、解釈の任意性なく、常にクロック信号の値の変化がその他の入力信号の値の変化よりも遅れて変化すると一意的に解釈することのできる有限状態機械となる。
【００７２】
［２−６．等価性検証部１６］
次に、図１に示した本実施形態における等価性検証部１６の働きを説明する。等価性検証部１６では、回路記述１００Ａ，１００Ｂから定常化有限状態機械生成部１２を用いて作られた二つの定常化有限状態機械 newＭＡ， newＭＢの間の論理的等価性を検証し、この結果を出力部１７に出力する。これら二つの定常化有限状態機械 newＭＡ， newＭＢは、これまでに述べたように、クロック、及び、その他の入力信号値の変化に対する状態遷移、及び、出力の関係を、クロック信号値の変化に対するタイミングを含めて正しく表現しているので、等価性検証部１６では、回路の詳細に立ちいることなく等価性の検証を行うことが可能となる。
【００７３】
これを効率良く行うためのアルゴリズムには、例えば、次に示されているものなどを用いることができる。
【００７４】
(5) O. Coudert, C. Berthet and J. C. Madre, “Verification of Sequential Machines Using Boolean Functional Vectors" ,in Formal VLSI Correctness Verification 1989, pp.179-196;USP 5,491,639 T.Filkorn,1996
これらのアルゴリズムでは、定常化有限状態機械 newＭＡ， newＭＢとの間の等価性を検証するために、それぞれの初期状態を指定する必要がある。一方、もしも、定常化有限状態機械生成部１２において有限状態機械Ｍを定常化有限状態機械 newＭに変換するに当たって、反復二乗法による変換方法などのように有限状態機械のリセット可能性や、二つの有限状態機械間の整列可能性が、変換前後において保存される方法を採用すれば、検証のアルゴリズムとして、(6) に示されているものを用いることができる。
【００７５】
(6) USP 5,331,568 C.Pixley,1994
このアルゴリズムを用いるならば、検証する二つの有限状態機械の初期状態は指定する必要がない。即ち、初期の有限状態機械Ｍ0 から有限状態機械Ｍを作成する際に、クロックを指定する情報だけでは初期状態を決定することができず、また、ハードウェアのスイッチが入れられた直後の初期状態は一般に不定であるので、この等価性の検証は、Pixleyのアルゴリズムが適している。
【００７６】
Pixleyのアルゴリズムでは、検証する有限状態機械の初期状態は指定する必要がない。そして、比較する２つの定常化有限状態機械 newＭＡ， newＭＢの状態ＳＡ，ＳＢは、任意の入力シーケンスに対して常に同じ出力シーケンスを与えるとき等価であると定義する。このとき、２つの定常化有限状態機械 newＭＡ， newＭＢの等価性は、有限状態機械ＭＰ＝ newＭＡ× newＭＢの任意の状態｛ｓＡ，ｓＢ｝∈ΣＰを、２つの等価な状態よりなる組｛ＳＡ，ＳＢ｝∈ΣＰへ遷移させることのできる入力シーケンスが存在するか否かで決定される。このような手法を用いることにより、本発明の検証システムでは、クロック立ち上がり時に状態遷移するべく仕様記述されているにもかかわらず、クロックの立ち下がりで状態遷移するように設計された回路の誤りなどを見出すことができる。
【００７７】
【発明の効果】
以上のとおり、本発明にかかる論理回路の形式検証装置によれば、与えられた二つの論理回路の記述から生成した二つの定常化有限状態機械の論理的等価性を等価性検証部において形式検証することにより、入出力信号の値の変化のタイミングとクロック信号の値の変化のタイミングの関係までを考慮した順序回路の形式検証を行うことが可能となる。
【００７８】
特に、本発明では、従来の有限状態機械の入力信号からクロックを取り除く手法とは逆に、クロック信号を入力信号として残し、さらに、状態を構成するビットにもクロック直前の値を持たせる。これによって、設計者の予期したクロックのタイミング以外で入力信号が変化することなどによる、回路動作の相違のような誤りを検出することが可能になる。これは、トランジスタネットリストによるハードウェア記述や、素子にループを持たせて状態を構成した順序回路のような、記述の抽象度の低い回路の等価性の検証にきわめて有利である。
【図面の簡単な説明】
【図１】本発明による論理回路の検証装置の一実施形態の構成を示す機能ブロック図。
【図２】二つの論理記述を有限状態機械に変換して比較する手法を示す機能ブロック図。
【図３】図１の検証装置の動作を示すフロー図。
【図４】有限状態機械の定義を説明する図。
【図５】有限状態機械の一具体例を示す図。
【図６】有限状態機械がとる各状態の関係を示す図。
【図７】定常化有限状態機械と定常化されていない有限状態機械の特徴を比較する図。
【図８】過渡的な状態への遷移を含む有限状態機械の一具体例を示す図。
【図９】図６の有限状態機械を変換して得られた定常化有限状態機械を示す図。
【図１０】ＪＫ−フリップフロップを実現する回路を示す図。
【図１１】ＶＨＤＬ言語によるＪＫ−フリップフロップの動作記述の一例を示す図。
【図１２】図１０（ａ）のＪＫ−フリップフロップを実現する回路から作った有限状態機械を示す図。
【図１３】図１２の有限状態機械から作った同期機械を示す図。
【図１４】有限状態機械の解釈の任意性を説明するために、二つの有限状態機械（ａ）（ｂ）の状態遷移を比較する図。
【図１５】図１４の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、ｃｌｋの値が０になる直前に入力信号ａの値が０から１に変化する場合を示す。
【図１６】図１４の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、入力信号ａの値の変化がｃｌｋの値が０になる直後の場合を示す。
【図１７】図１４の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、ｃｌｋの値が１から０になる変化と同時にａの値が０から１に変化する場合を示す。
【図１８】予備的な有限状態機械に直前のクロック値を保持するビット値を導入する手法を示す図。
【図１９】図１８の手法により解釈の任意性を含まない有限状態機械の遷移関数を決定する手法を示す図。
【図２０】図１４に示した二つの予備的な有限状態機械（ａ）（ｂ）の直前のクロック値を新たな状態ビットとして作った解釈の任意性を含まない有限状態機械（ａ）（ｂ）を示す図。
【図２１】図２０の有限状態機械から変換した二つの定常化有限状態機械（ａ）（ｂ）を示す図。
【図２２】図２１の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、ｃｌｋの値が０になる直前に入力信号ａの値が０から１に変化する場合を示す。
【図２３】図２１の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、入力信号ａの値の変化がｃｌｋの値が０になる直後の場合を示す。
【図２４】図２１の二つの有限状態機械（ａ）（ｂ）の入力、出力及び遷移を比較するタイムチャートで、ｃｌｋの値が１から０になる変化と同時にａの値が０から１に変化する場合を示す。
【図２５】従来の同期機械による検証装置の動作を示すフロー図。
【符号の説明】
１００…回路記述Ａ，Ｂ
２００…補助情報
１０…回路記述入力部
１１…補助情報入力部
１２…定常化有限状態機械生成部
１３…予備的な有限状態機械の生成部
１４…任意性を含まない有限状態機械の生成部
１５…定常化有限状態機械 newＭへの変換部
１６…等価性検証部
１７…出力部
【図１】
0003660097.tif 000002
【図２】
0003660097.tif 000003
【図３】
0003660097.tif 000004
【図４】
0003660097.tif 000005
【図５】
0003660097.tif 000006
【図６】
0003660097.tif 000007
【図７】
0003660097.tif 000008
【図８】
0003660097.tif 000009
【図９】
0003660097.tif 000010
【図１０】
0003660097.tif 000011
【図１１】
0003660097.tif 000012
【図１２】
0003660097.tif 000013
【図１３】
0003660097.tif 000014
【図１４】
0003660097.tif 000015
【図１５】
0003660097.tif 000016
【図１６】
0003660097.tif 000017
【図１７】
0003660097.tif 000018
【図１８】
0003660097.tif 000019
【図１９】
0003660097.tif 000020
【図２０】
0003660097.tif 000021
【図２１】
0003660097.tif 000022
【図２２】
0003660097.tif 000023
【図２３】
0003660097.tif 000024
【図２４】
0003660097.tif 000025
【図２５】
0003660097.tif 000026