(57)【要約】【課題】検証の時間を短縮すること。【解決手段】記憶部１ａは、論理回路の定義情報２を記憶する。演算部１ｂは、定義情報２を参照して、共通のモジュール定義からインスタンス化される論理ブロック２ａ，２ｂを特定する。演算部１ｂは、論理ブロック２ａ，２ｂの対応関係、論理ブロック２ａ，２ｂで用いられる変数ｘ１，ｘ２の対応関係および変数ｙ１，ｙ２の対応関係を示す情報を生成する。演算部１ｂは、定義情報２に関する和積形の論理式３を用いた充足可能性問題の検証中に、論理式３に含まれる変数ｘ１，ｙ１の組に対する学習節５を取得すると、対応関係に基づいて、変数ｘ１，ｙ１を含む論理ブロック２ａに対応する論理ブロック２ｂを特定する。演算部１ｂは、論理ブロック２ｂに含まれる変数の中から変数ｘ１，ｙ１に対応する変数ｘ２，ｙ２を検索する。演算部１ｂは、変数ｘ２，ｙ２に対して、学習節５に応じた学習節６を生成する。【選択図】図１
2015172873.tif 000002
【特許請求の範囲】
【請求項１】
論理回路の定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、前記複数の論理ブロックの対応関係および前記複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、
前記複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、前記論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、前記対応情報に基づいて、前記第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、前記第２の論理ブロックに含まれる変数の中から前記第１の変数の組に対応する第２の変数の組を検索し、
前記第２の変数の組に対して前記第１の学習節に応じた第２の学習節を生成する、
処理をコンピュータに実行させる検証プログラム。
【請求項２】
前記対応情報の生成では、論理ブロック内で各変数が定義される順序と、当該論理ブロックおよび当該論理ブロックを包含する他の論理ブロックの階層関係とを示すインデックスを各変数に付与することで前記対応情報を生成し、
前記検索では、前記第１の変数の組に対応するインデックスの組に基づいて前記第２の変数の組を検索する、請求項１記載の検証プログラム。
【請求項３】
前記論理回路は、順序回路を時間展開した組合せ回路である、請求項１または２記載の検証プログラム。
【請求項４】
コンピュータが、
論理回路の定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、前記複数の論理ブロックの対応関係および前記複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、
前記複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、前記論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、前記対応情報に基づいて、前記第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、前記第２の論理ブロックに含まれる変数の中から前記第１の変数の組に対応する第２の変数の組を検索し、
前記第２の変数の組に対して前記第１の学習節に応じた第２の学習節を生成する、
検証方法。
【請求項５】
論理回路の定義情報を記憶する記憶部と、
前記定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、前記複数の論理ブロックの対応関係および前記複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、
前記複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、前記論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、前記対応情報に基づいて、前記第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、前記第２の論理ブロックに含まれる変数の中から前記第１の変数の組に対応する第２の変数の組を検索し、
前記第２の変数の組に対して前記第１の学習節に応じた第２の学習節を生成する、演算部と、
を有する検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は検証プログラム、検証方法および検証装置に関する。
【背景技術】
【０００２】
現在、論理回路の設計では、論理回路が期待する動作を行うかをコンピュータを用いて検証することで、設計工程の品質向上が図られている。このような検証に形式的検証と呼ばれる方法を用いることがある。形式的検証では、設計仕様と設計した論理回路とを数学的に解析することで設計した論理回路が適正であることを検証する。
【０００３】
ここで、論理回路の形式的検証に利用される技術として、ＳＡＴ（SATisfiability、充足可能性問題）ソルバが知られている。ＳＡＴソルバは、和積形（ＣＮＦ：Conjunctive Normal Form）で表された論理式（ＣＮＦ論理式やＣＮＦ式などと呼ばれることもある）が全体として真になる論理変数の真偽値の組合せが存在するか否かを検証する。
【０００４】
ＳＡＴでは、ＣＮＦ論理式に含まれる各論理変数（以下、単に変数という）の真偽値を順次設定しながら探索木を構築することで、ＣＮＦ論理式を真にする全変数の真偽値の組合せが存在するか否かを検証する。検証中に、ＣＮＦ論理式を真にできない（充足不可能な）変数の真偽値の組合せを特定すると、探索木を後戻り（バックトラック）して、特定した組に属する変数の真偽値の組合せを変更し、探索を継続する。このとき、特定した変数の真偽値の組合せ（バックトラックの原因）に対して、その組では充足可能な解が存在しないという情報（学習節と呼ばれる）をＣＮＦ論理式に追加し得る。
【０００５】
なお、回路ベースとＣＮＦベースの充足可能性アルゴリズムを結合したハイブリッド方式でブール充足可能性問題を検証する方法が考えられている。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００４−５６７４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
所定のハードウェア記述言語で表された論理回路の内部変数をＣＮＦ論理式の変数に対応させ、ＳＡＴソルバを用いて論理回路の形式的検証を行うことがある。ハードウェア記述言語では、論理回路内で用いられる共通のモジュールを１つの定義（モジュール定義）で記述し、同じモジュール定義を複数回呼出すことで、論理回路内に同一構造のモジュールのインスタンス（論理ブロック）を複数定義し得る。このとき、ＳＡＴソルバは、各論理ブロックがもつ各変数を、ＣＮＦ論理式の異なる変数に対応付けることになる。しかし、各変数を別個に扱ってＳＡＴによる検証を行うと、真偽値の探索対象となる変数の数が増大して、ＳＡＴソルバの処理時間が長引くおそれがある。
【０００８】
１つの側面では、本発明は、検証の時間を短縮する検証プログラム、検証方法および検証装置を提供することを目的とする。
【課題を解決するための手段】
【０００９】
１つの態様では、コンピュータによって実行される検証プログラムが提供される。この検証プログラムでは、論理回路の定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、複数の論理ブロックの対応関係および複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、対応情報に基づいて、第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、第２の論理ブロックに含まれる変数の中から第１の変数の組に対応する第２の変数の組を検索し、第２の変数の組に対して第１の学習節に応じた第２の学習節を生成する、処理をコンピュータに実行させる。
【００１０】
また、１つの態様では、検証方法が提供される。この検証方法では、コンピュータが、論理回路の定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、複数の論理ブロックの対応関係および複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、対応情報に基づいて、第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、第２の論理ブロックに含まれる変数の中から第１の変数の組に対応する第２の変数の組を検索し、第２の変数の組に対して第１の学習節に応じた第２の学習節を生成する。
【００１１】
また、１つの態様では、検証装置が提供される。この検証装置は、記憶部と演算部とを有する。記憶部は、論理回路の定義情報を記憶する。演算部は、定義情報を参照して、共通のモジュール定義を呼出し元とする複数の論理ブロックを特定し、複数の論理ブロックの対応関係および複数の論理ブロックで用いられる複数の変数の対応関係を示す対応情報を生成し、複数の変数に関する和積形の論理式を示す情報を用いた充足可能性問題の検証処理の実行中に、論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、対応情報に基づいて、第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定し、第２の論理ブロックに含まれる変数の中から第１の変数の組に対応する第２の変数の組を検索し、第２の変数の組に対して第１の学習節に応じた第２の学習節を生成する。
【発明の効果】
【００１２】
１つの側面では、検証の時間を短縮できる。
【図面の簡単な説明】
【００１３】
【図１】第１の実施の形態の検証装置を示す図である。
【図２】第２の実施の形態の検証対象の論理回路の例を示す図である。
【図３】バックトラックの例（その１）を示す図である。
【図４】バックトラックの例（その２）を示す図である。
【図５】第２の実施の形態の検証装置のハードウェア例を示す図である。
【図６】検証装置のソフトウェア例を示す図である。
【図７】検証対象回路データの例を示す図である。
【図８】組合せ回路データの例を示す図である。
【図９】時間展開後の検証対象回路の例を示す図である。
【図１０】オフセット管理に用いるリスト要素の構造体の例を示す図である。
【図１１】オフセットテーブルの例を示す図である。
【図１２】インデックスの計算例を示す図である。
【図１３】ＣＮＦ論理式データの例を示す図である。
【図１４】検証処理の例を示すフローチャートである。
【図１５】学習節の複製の例を示す図である。
【発明を実施するための形態】
【００１４】
以下、本実施の形態を図面を参照して説明する。
［第１の実施の形態］
図１は、第１の実施の形態の検証装置を示す図である。検証装置１は、ＳＡＴソルバを用いて論理回路の検証を行う。検証装置１は、記憶部１ａおよび演算部１ｂを有する。
【００１５】
記憶部１ａは、ＲＡＭ（Random Access Memory）などの揮発性記憶装置でもよいし、ＨＤＤ（Hard Disk Drive）やフラッシュメモリなどの不揮発性記憶装置でもよい。記憶部１ａは、所定のハードウェア記述言語による論理回路の定義情報２を記憶する。
【００１６】
定義情報２は、検証対象の論理回路を定義した情報である。定義情報２では、予め用意されたモジュール定義（モジュールの定義内容）を呼出すための記述により、同じ構造をもつ複数の論理ブロック（モジュールのインスタンス）を定義可能である。モジュール定義は、所定のライブラリに登録された情報でもよい。
【００１７】
定義情報２は、論理ブロック２ａ，２ｂを含む。論理ブロック２ａ，２ｂは、共通のモジュール定義からインスタンス化される論理ブロックである。論理ブロック２ａは、変数ｘ１，ｙ１を含む。論理ブロック２ｂは、変数ｘ２，ｙ２を含む。変数ｘ１，ｙ１および変数ｘ２，ｙ２は、信号の状態などを示す論理変数（真または偽の値をとる）である。論理ブロック２ａ，２ｂは、その他の論理変数を含んでもよい。また、定義情報２は、論理ブロック２ａ，２ｂ以外の他の論理ブロックを含んでもよい。なお、以下の説明では真偽値のうち、真（ｔｒｕｅ）を“１”と表す。偽（ｆａｌｓｅ）を“０”と表す。
【００１８】
演算部１ｂは、ＣＰＵ（Central Processing Unit）、ＤＳＰ（Digital Signal Processor）、ＡＳＩＣ（Application Specific Integrated Circuit）、ＦＰＧＡ（Field Programmable Gate Array）などを含み得る。演算部１ｂはプログラムを実行するプロセッサであってもよい。ここでいう「プロセッサ」には、複数のプロセッサの集合（マルチプロセッサ）も含まれ得る。
【００１９】
演算部１ｂは、記憶部１ａに記憶された定義情報２を参照して、共通のモジュール定義からインスタンス化される（呼び出される）複数の論理ブロックを特定する。演算部１ｂは、特定した複数の論理ブロックおよび複数の論理ブロックで用いられる複数の変数の間の対応関係を示す情報を生成する。
【００２０】
例えば、演算部１ｂは、定義情報２を参照して、共通のモジュール定義からインスタンス化される論理ブロック２ａ，２ｂを特定する。演算部１ｂは、論理ブロック２ａと論理ブロック２ｂとの対応関係（共通のモジュール定義からインスタンス化されるという対応関係）を示す情報を生成する。演算部１ｂは、論理ブロック２ａで用いられる変数ｘ１，ｙ１と論理ブロック２ｂで用いられる変数ｘ２，ｙ２との間の対応関係を示す情報を生成する。
【００２１】
具体的には、演算部１ｂは、呼出し元のモジュール定義に記述されている変数の順序で論理ブロック２ａ，２ｂ内の各変数を対応付けることができる。モジュール定義で変数ｘ，ｙ，・・・が定義され、それに応じて、論理ブロック２ａの変数ｘ１，ｙ１，・・・および論理ブロック２ｂの変数ｘ２，ｙ２，・・・が見出されるのであれば、変数ｘ１，ｘ２を対応付け、変数ｙ１，ｙ２を対応付けることができる。演算部１ｂは、生成した対応関係の情報を記憶部１ａに格納する。
【００２２】
演算部１ｂは、定義情報２に含まれる複数の変数に関する和積形の論理式（ＣＮＦ論理式）を示す情報を用いた充足可能性（ＳＡＴ）問題の検証処理を実行する。例えば、演算部１ｂは、定義情報２を所定のルールに従ってＣＮＦ論理式３を示す情報に変換する。演算部１ｂは、ＣＮＦ論理式３を示す情報を記憶部１ａに格納する。定義情報２に含まれる各論理ブロックの各変数は、ＣＮＦ論理式３の変数に相当する。ＣＮＦ論理式３は、検証したいプロパティに応じた所定の条件を含んでもよい。ＣＮＦ論理式３は、定義情報２から生成されたＣＮＦ論理式の例である。図１で示されるようにＣＮＦ論理式３は次の記述で表せる。
【００２３】
φ＝（ｘ１＋ｘ３）（ｘ１’＋ｘ４＋ｘ５）・・・（ｙ１＋ｙ３＋ｙ５）
演算部１ｂは、φが真（“１”）になるような変数ｘ１，ｘ２，・・・の真偽値の組合せが存在するかを検証する。ここで、ｘ１’の表記は、ｘ１の否定（¬ｘ１）を示す。各変数に対する真偽値のあてはめの順序は任意に決定できる。例えば、ＣＮＦ論理式３に現れる個数が多い変数から優先的に真偽値を探索することが考えられる。
【００２４】
演算部１ｂは、充足可能性問題の検証中に、和積形の論理式に含まれる第１の変数の組に対する第１の学習節を取得すると、生成した対応関係の情報に基づいて、第１の変数の組を含む第１の論理ブロックに対応する第２の論理ブロックを特定する。演算部１ｂは、第２の論理ブロックに含まれる変数の中から第１の変数の組に対応する第２の変数の組を検索する。
【００２５】
例えば、演算部１ｂは、ＣＮＦ論理式３の変数ｘ１，ｙ１の組（第１の変数の組）について、ｘ１＝ｙ１＝１（ｘ１＝１かつｙ１＝１）のときに、φが偽（“０”）になる（充足不可能である）ことを検出する。なお、「ｘ１＝ｙ１＝１のときに充足不可能である」ことを、「ｘ１＝ｙ１＝１のときに矛盾が発生する」というように表すこともある。このとき、演算部１ｂは学習節５（第１の学習節）を生成し、ＣＮＦ論理式３に追加する。学習節５は、ｘ１＝ｙ１＝１の否定を示す項“（ｘ１’＋ｙ１’）”である。
【００２６】
更に、演算部１ｂは、記憶部１ａに記憶された対応関係の情報に基づいて、ｘ１，ｙ１を含む論理ブロック２ａを特定し、論理ブロック２ａに対応する論理ブロック２ｂを特定する。更に、演算部１ｂは、対応関係の情報に基づいて、論理ブロック２ｂの変数のうち、変数ｘ１，ｙ１に対応する変数ｘ２，ｙ２（第２の変数の組）を検索する。
【００２７】
演算部１ｂは、検索した第２の変数の組に対して、第１の学習節に応じた第２の学習節を生成する。例えば、演算部１ｂは、変数ｘ２，ｙ２に対して、学習節５に応じた学習節６（第２の学習節）を生成する。上記の例では、ｘ１＝ｙ１＝１のとき充足不可能であるため、ｘ２＝ｙ２＝１のときも同様に充足不可能であると判断できる。よって、学習節６は、ｘ２＝ｙ２＝１の否定を示す項“（ｘ２’＋ｙ２’）”である。演算部１ｂは、学習節６をＣＮＦ論理式３に追加する。ＣＮＦ論理式４は、ＣＮＦ論理式３に学習節５，６を追加した結果である。
【００２８】
検証装置１によれば、演算部１ｂにより、定義情報２が参照されて、共通のモジュール定義からインスタンス化される論理ブロック２ａ，２ｂが特定される。演算部１ｂにより、論理ブロック２ａ，２ｂの対応関係、論理ブロック２ａ，２ｂで用いられる変数ｘ１，ｘ２の対応関係、変数ｙ１，ｙ２の対応関係を示す情報が生成される。演算部１ｂにより、定義情報２に含まれる複数の変数に関するＣＮＦ論理式３を示す情報を用いた充足可能性問題の検証処理の実行中に、ＣＮＦ論理式３に含まれる変数ｘ１，ｙ１に対する学習節５が取得される。すると、演算部１ｂにより、生成した対応関係に基づいて、変数ｘ１，ｙ１を含む論理ブロック２ａに対応する論理ブロック２ｂが特定される。演算部１ｂにより、論理ブロック２ｂに含まれる変数の中から変数ｘ１，ｙ１に対応する変数ｘ２，ｙ２が検索される。演算部１ｂにより、変数ｘ２，ｙ２に対して、学習節５に応じた学習節６が生成される。
【００２９】
これにより、検証の時間を短縮できる。具体的には、上記のように、論理ブロック２ａで見出された学習節５は、共通の構造をもつ（呼出し元のモジュール定義が共通する）論理ブロック２ｂに対しても適用できると考えられる。すなわち、論理ブロック２ｂの各変数に対して真偽値の決定を行っていけば、変数ｘ２，ｙ２に対しても同様に学習節６が見出されると考えられる。そこで、学習節５を取得したタイミングで、論理ブロック２ｂの変数ｘ２，ｙ２に対する学習節６を生成することで、変数ｘ２，ｙ２に対する学習節６を先取りする。すると、学習節５を取得したタイミングで変数ｘ２，ｙ２に対する制約が追加されることになり、変数ｘ２，ｙ２に関する余計なバックトラック（変数ｘ１，ｙ１について発生したバックトラックに対して冗長的に発生するバックトラック）の発生を抑えられる。その結果、論理回路の検証の時間を短縮できる。
【００３０】
検証装置１による検証は、順序回路を時間展開することで得られた組合せ回路の定義情報を用いる場合に特に有効である。順序回路を時間展開することで得られた組合せ回路は、順序回路の所定の論理ブロックの複製を複数個含む論理回路として表せるからである。
【００３１】
［第２の実施の形態］
図２は、第２の実施の形態の検証対象の論理回路の例を示す図である。第２の実施の形態では、検証対象として順序回路Ｚを想定する。順序回路Ｚは、外部からの入力と順序回路Ｚの内部状態の両方により出力が定まる論理回路である。順序回路Ｚは、クロックのタイミングに合わせて動作する。順序回路Ｚは、論理ブロックＣ０およびフリップフロップＦＦを有する。論理ブロックＣ０は組合せ回路である。フリップフロップＦＦは、論理ブロックＣ０の出力を記憶する。論理ブロックＣ０は、外部からの入力信号とフリップフロップＦＦに記憶された内部状態とに応じた信号を出力する。
【００３２】
第２の実施の形態では、順序回路Ｚを時間展開して、順序回路Ｚ全体を組合せ回路化し、所定のプロパティについてＳＡＴソルバによる形式的検証を行う。ＳＡＴは、充足可能性問題や充足可能性判定問題などと呼ばれることがある。
【００３３】
例えば、クロックの１周期を単位時間として、順序回路Ｚをｎ（ｎは２以上の整数）時間分の組合せ回路に展開できる。時刻ｔ＝１の論理ブロックを論理ブロックＣ１とする。時刻ｔ＝２の論理ブロックを論理ブロックＣ２とする。時刻ｔ＝ｎの論理ブロックを論理ブロックＣｎとする。すると、順序回路Ｚは、論理ブロックＣ１，Ｃ２，・・・，Ｃｎを直列に接続した組合せ回路Ｚ１として表せる。
【００３４】
順序回路Ｚは、所定のハードウェア記述言語（例えば、Ｖｅｒｉｌｏｇ  ＨＤＬ（Hardware Description Language）やＶＨＤＬなど）を用いて記述される（具体例については後述する）。この場合、論理ブロックＣ１，Ｃ２，・・・，Ｃｎは、論理ブロックＣの定義内容（モジュール定義）を複数回呼出すことで定義される。すると、論理ブロックＣ１，Ｃ２，・・・，Ｃｎを表す複数の変数が定められる。
【００３５】
組合せ回路Ｚ１は、論理ブロックＣ１，Ｃ２，・・・，Ｃｎの複数の変数に関するＣＮＦ論理式で表せる。図２では、組合せ回路Ｚ１に対応するＣＮＦ論理式φ１も例示されている。ここで、ＳＡＴソルバによる真偽値の探索ではバックトラックが発生し得る。
【００３６】
図３は、バックトラックの例（その１）を示す図である。図３では、ＣＮＦ論理式に含まれる変数として変数ａ，ｂ，ｃ，ｄ，ｅ，ｆ，ｇを想定する。変数ａ，ｂ，ｃ，ｄ，ｅ，ｆ，ｇは、１つの論理ブロックに対して定められる変数である。例えば、ＳＡＴソルバは、予め定められた順序で各変数の真偽値を決定する。図３の例では、変数ａ，ｂ，ｃ，ｄ，ｅ，ｆ，ｇの順に“１”（すなわち、ｔｒｕｅ）とする。変数ａから変数ｇまでの真偽値を“１”としたときに矛盾が発生したとする。すると、ＳＡＴソルバは、所定の矛盾解析機能により矛盾が発生した原因を解析し、学習節を求める。例えば、ａ＝ｄ＝ｇ＝１が矛盾の原因であったとすると、（ａ’＋ｄ’＋ｇ’）を学習する。学習節（ａ’＋ｄ’＋ｇ’）は、ａ’＝１かｄ’＝１かｇ’＝１（言い換えれば、ａ，ｄ，ｇの少なくとも何れかが０）でなければならないことを意味する。
【００３７】
そして、学習節の真偽値を決定する変数が１つになるポイントに戻る。図３の例では、変数ｄを“１”に決定した時点に後戻りする（バックトラック）。ａ＝ｄ＝１のとき、学習節（ａ’＋ｄ’＋ｇ’）＝ｇ’より、次にｇ＝０（すなわち、ｇ’＝１）を設定して、探索を継続する。具体的には、既に決めた変数ａ＝ｂ＝ｃ＝ｄ＝１に対して、変数ｇ＝０（前回とは逆の値）を代入して、変数ｅ＝１、変数ｆ＝１と順次設定していく。
【００３８】
図４は、バックトラックの例（その２）を示す図である。図４では、図３で例示した探索木を２単位時間分表している。時刻ｔ＝１に相当する論理ブロックの変数をａ１，ｂ１，ｃ１，ｄ１，ｅ１，ｆ１，ｇ１と表す。時刻ｔ＝２に相当する論理ブロックの変数をａ２，ｂ２，ｃ２，ｄ２，ｅ２，ｆ２，ｇ２と表す。また、図３と同様の手順で探索を行うことを想定する。このとき、バックトラックが重複して発生する。
【００３９】
例えば、時刻ｔ＝１に相当する変数ａ１，ｂ１，ｃ１，・・・に、順番に“１”を設定する。そして、図３の例と同様にａ１＝ｄ１＝ｇ１＝１で矛盾が発生したとする。すると、ＳＡＴソルバは（ａ１’＋ｄ１’＋ｇ１’）を学習する。また、変数ｄ１を“１”に設定した時点に後戻りする（バックトラック）。以降は、図３と同様に、変数ｇ１＝０、ｅ１＝１、ｆ１＝１と順次設定していく。
【００４０】
続いて、時刻ｔ＝２に相当する変数ａ２，ｂ２，ｃ２，・・・に、順番に“１”を設定する。時刻ｔ＝２の論理は、時刻ｔ＝１の論理と同じである。このため、時刻ｔ＝１の部分の探索で検出された矛盾と同条件（ａ２＝ｄ２＝ｇ２＝１）の矛盾が時刻ｔ＝２に相当する論理ブロックでも発生し、バックトラックが生じることになる。
【００４１】
このように時間展開された論理回路に対応するＣＮＦ論理式を全体で１つの式とみなして充足可能性の検証を行うと、各時刻に対応する部分で同様のバックトラックが引き起こされることになり、処理時間が増大し得る。一方、同じ論理構造をもつ複数のインスタンスで同様のバックトラックが何度も発生するのは余計である。そこで、第２の実施の形態では、組合せ回路における、ある変数の組に対して取得された学習節に応じて、別の変数の組に対する学習節を生成する装置を提供する。
【００４２】
図５は、第２の実施の形態の検証装置のハードウェア例を示す図である。検証装置１００は、プロセッサ１０１、ＲＡＭ１０２、ＨＤＤ１０３、画像信号処理部１０４、入力信号処理部１０５、読み取り装置１０６、通信インタフェース１０７を有する。各ユニットが検証装置１００のバスに接続されている。
【００４３】
プロセッサ１０１は、検証装置１００全体を制御する。プロセッサ１０１は、マルチプロセッサであってもよい。プロセッサ１０１は、例えばＣＰＵ、ＤＳＰ、ＡＳＩＣまたはＦＰＧＡなどである。プロセッサ１０１は、ＣＰＵ、ＤＳＰ、ＡＳＩＣ、ＦＰＧＡなどのうちの２以上の要素の組合せであってもよい。
【００４４】
ＲＡＭ１０２は、検証装置１００の主記憶装置である。ＲＡＭ１０２は、プロセッサ１０１に実行させるＯＳ（Operating System）のプログラムやアプリケーションプログラムの少なくとも一部を一時的に記憶する。また、ＲＡＭ１０２は、プロセッサ１０１による処理に用いる各種データを記憶する。
【００４５】
ＨＤＤ１０３は、検証装置１００の補助記憶装置である。ＨＤＤ１０３は、内蔵した磁気ディスクに対して、磁気的にデータの書き込みおよび読み出しを行う。ＨＤＤ１０３には、ＯＳのプログラム、アプリケーションプログラム、および各種データが格納される。検証装置１００は、フラッシュメモリやＳＳＤ（Solid State Drive）などの他の種類の補助記憶装置を備えてもよく、複数の補助記憶装置を備えてもよい。
【００４６】
画像信号処理部１０４は、プロセッサ１０１からの命令に従って、検証装置１００に接続されたディスプレイ１１に画像を出力する。ディスプレイ１１としては、ＣＲＴ（Cathode Ray Tube）ディスプレイ、液晶ディスプレイ（ＬＣＤ：Liquid Crystal Display）、有機ＥＬ（Electro-Luminescence）ディスプレイなど各種のディスプレイを用いることができる。
【００４７】
入力信号処理部１０５は、検証装置１００に接続された入力デバイス１２から入力信号を取得し、プロセッサ１０１に出力する。入力デバイス１２としては、マウスやタッチパネルなどのポインティングデバイス、キーボード、ボタンスイッチなど各種の入力デバイスを用いることができる。また、検証装置１００には複数の種類の入力デバイスが接続されてもよい。
【００４８】
読み取り装置１０６は、記録媒体１３に記録されたプログラムやデータを読み取る装置である。記録媒体１３として、例えば、フレキシブルディスク（ＦＤ：Flexible Disk）やＨＤＤなどの磁気ディスク、ＣＤ（Compact Disc）やＤＶＤ（Digital Versatile Disc）などの光ディスク、光磁気ディスク（ＭＯ：Magneto-Optical disk）を使用できる。また、記録媒体１３として、例えば、フラッシュメモリカードなどの不揮発性の半導体メモリを使用することもできる。読み取り装置１０６は、例えば、プロセッサ１０１からの命令に従って、記録媒体１３から読み取ったプログラムやデータをＲＡＭ１０２またはＨＤＤ１０３に格納する。
【００４９】
通信インタフェース１０７は、ネットワーク１０を介して他の装置（サーバコンピュータなど）と通信を行う。
図６は、検証装置のソフトウェア例を示す図である。検証装置１００は、記憶部１１０、時間展開部１２０、ＣＮＦ変換部１３０およびＳＡＴ処理部１４０を有する。記憶部１１０は、ＲＡＭ１０２やＨＤＤ１０３の記憶領域を用いて実現できる。時間展開部１２０、ＣＮＦ変換部１３０およびＳＡＴ処理部１４０は、プロセッサ１０１によりプログラムが実行されることで実現できる。
【００５０】
記憶部１１０は、検証対象回路データ１１１、組合せ回路データ１１２、オフセットテーブル１１３およびＣＮＦ論理式データ１１４を記憶する。また、記憶部１１０は、検証したいプロパティに応じた所定の条件を記憶する。
【００５１】
検証対象回路データ１１１は、検証対象である順序回路Ｚを所定のハードウェア記述言語で記述した情報である。組合せ回路データ１１２は、順序回路Ｚを時間展開した組合せ回路を当該ハードウェア記述言語で記述した情報である。
【００５２】
オフセットテーブル１１３は、組合せ回路データ１１２で定められる論理ブロックおよび変数に対するオフセット値を定めた情報である。オフセット値は、ＣＮＦ論理式の各変数に対するインデックスの決定に用いられる。ＣＮＦ論理式データ１１４は、組合せ回路データ１１２の各変数に関するＣＮＦ論理式を示す情報である。
【００５３】
時間展開部１２０は、記憶部１１０に記憶された検証対象回路データ１１１を時間展開して、組合せ回路データ１１２を生成する。すなわち、時間展開部１２０は、検証対象回路データ１１１における順序回路Ｚの記述を時間展開して組合せ回路化し、組合せ回路Ｚ１の情報を生成する。時間展開部１２０は、生成した組合せ回路データ１１２を記憶部１１０に格納する。
【００５４】
ＣＮＦ変換部１３０は、組合せ回路データ１１２の構文を解析することで、オフセットテーブル１１３を生成し、記憶部１１０に格納する。具体的には、ＣＮＦ変換部１３０は、組合せ回路データ１１２における論理ブロックの入れ子構造を検出し、論理ブロックの階層および同一階層における論理ブロックの複製状況を表すオフセット値を決定し、オフセットテーブル１１３に登録する。ＣＮＦ変換部１３０は、各論理ブロックに含まれる変数に対してもオフセット値を決定し、オフセットテーブル１１３に登録する。
【００５５】
ＣＮＦ変換部１３０は、組合せ回路データ１１２を、ＣＮＦ論理式データ１１４に変換する。例えば、基本的な演算の論理ゲートに対するＣＮＦ論理式の情報を、ライブラリとして記憶部１１０に予め格納しておくことが考えられる。ＣＮＦ変換部１３０は、組合せ回路データ１１２に含まれる論理ゲートに応じて、記憶部１１０に記憶された各論理ゲートに対するＣＮＦ論理式を組合せることで、ＣＮＦ論理式データ１１４を生成し得る。
【００５６】
ＳＡＴ処理部１４０は、ＣＮＦ論理式データ１１４を用いて、順序回路Ｚに関する所定のプロパティを検証するＳＡＴソルバである。例えば、ＣＮＦ論理式φ１において、デッドロックなどのエラー発生時の状態がφ１＝１で表されるなら、充足可能である場合に設計に誤りがあることになる。ＳＡＴ処理部１４０は、反例パターン（φ１＝１を充足させる変数値の組合せなど）を出力する。一方、充足不可能である場合（φ１＝１を充足させる変数値の組合せが存在しない場合）に、設計は正しいということになる。
【００５７】
ＳＡＴ処理部１４０は、検証中に、ＣＮＦ論理式データ１１４の一部の変数の組（第１の変数の組）に対して学習節（第１の学習節）を取得すると、オフセットテーブル１１３を参照して、第１の変数の組を含む論理ブロックの複製状況を確認する。ＳＡＴ処理部１４０は、第１の変数の組を含む論理ブロックに対応する他の論理ブロックがある場合、オフセットテーブル１１３を参照して、他の論理ブロックの変数のうち、第１の変数の組に対応する第２の変数の組を検索する。ＳＡＴ処理部１４０は、第２の変数の組に対して、第１の学習節に応じた第２の学習節を生成し、ＣＮＦ論理式データ１１４に第１，第２の学習節を追加する。他の論理ブロックが複数ある場合、ＳＡＴ処理部１４０は、第２の学習節も複数生成し、ＣＮＦ論理式データ１１４に追加する。
【００５８】
図７は、検証対象回路データの例を示す図である。検証対象回路データ１１１は、Ｖｅｒｉｌｏｇ  ＨＤＬと呼ばれるハードウェア記述言語を用いた、順序回路Ｚの記述を例示している。検証対象回路データ１１１の左側に付された番号は行番号である。以下、検証対象回路データ１１１の説明において、行番号により各行の記述を指し示す。
【００５９】
順序回路Ｚは、モジュールの階層構造で定義される。具体的には、最上位の階層のモジュール（テスト対象のモジュール）は、モジュール名“ＤＵＴ”（Design Under Test）のモジュールである。このモジュールは順序回路Ｚに相当する。ここで、例えば、モジュール名“Ｍ”のモジュールを指す場合に、モジュール“Ｍ”のように表記する（後述するインスタンスについても同様）。
【００６０】
モジュール“ＤＵＴ”は、モジュール“Ｃ”のインスタンス“Ｃ０”（インスタンス名“Ｃ０”のインスタンス）を含んでいる。モジュール“ＤＵＴ”はモジュール“Ｃ”よりも上位の階層である。モジュール“ＤＵＴ”（上位モジュール）がモジュール“Ｃ”（下位モジュール）を呼び出しているともいえる。なお、インスタンス“Ｃ０”は、論理ブロックＣ０に相当する。モジュール“ＤＵＴ”の定義は１行目〜５行目の記述が該当する。
【００６１】
モジュール“Ｃ”は、モジュール“Ｂ”のインスタンス“Ｂ０”、“Ｂ１”を含んでいる。モジュール“Ｃ”は、モジュール“Ｂ”よりも上位の階層である。モジュール“Ｃ”（上位モジュール）がモジュール“Ｂ”（下位モジュール）を呼び出しているともいえる。モジュール“Ｃ”の定義は６行目〜１０行目の記述が該当する。
【００６２】
モジュール“Ｂ”は、モジュール“Ａ”のインスタンス“Ａ０”、“Ａ１”を含んでいる。モジュール“Ｂ”は、モジュール“Ａ”よりも上位の階層である。モジュール“Ｂ”（上位モジュール）がモジュール“Ａ”（下位モジュール）を呼び出しているともいえる。モジュール“Ｂ”の定義は１１行目〜１５行目の記述が該当する。
【００６３】
モジュール“Ａ”は、最下位の階層のモジュールである。モジュール“Ａ”は、変数ｖ１，ｖ２，ｖ３，ｏ０，ｏ１を含む。モジュール“Ａ”の定義は１６行目〜２３行目の記述が該当する。
【００６４】
図８は、組合せ回路データの例を示す図である。組合せ回路データ１１２は、検証対象回路データ１１１に応じて時間展開部１２０により生成され、記憶部１１０に格納される。組合せ回路データ１１２の左側に付された番号は行番号である。
【００６５】
具体的には、モジュール“ＤＵＴ＿ｕｎｒｏｌｌ”により組合せ回路が定義されている。モジュール“ＤＵＴ＿ｕｎｒｏｌｌ”は、組合せ回路Ｚ１に相当する。モジュール“ＤＵＴ＿ｕｎｒｏｌｌ”は、モジュール“Ｃ”のインスタンス“Ｃ１”、“Ｃ２”、・・・、“Ｃｎ”を含む。インスタンス“Ｃ１”、“Ｃ２”、・・・、“Ｃｎ”は、論理ブロックＣ１，Ｃ２，・・・，Ｃｎに相当する。ここで、モジュール“Ａ”、“Ｂ”、“Ｃ”の具体的な定義内容は、図７で例示した同名のモジュールの定義内容と同一である（図８では図示を省略している）。
【００６６】
図９は、時間展開後の検証対象回路の例を示す図である。図９では、組合せ回路データ１１２で表される組合せ回路Ｚ１を例示している。このように、組合せ回路データ１１２により、モジュール“Ｃ”のインスタンス“Ｃ１”、“Ｃ２”、・・・、“Ｃｎ”（すなわち、論理ブロックＣ１，Ｃ２，・・・，Ｃｎ）の入出力の関係が表される。論理ブロックＣ１，Ｃ２，・・・，Ｃｎそれぞれに含まれるモジュール“Ｂ”のインスタンス“Ｂ０”、“Ｂ１”の入出力の関係およびモジュール“Ａ”のインスタンス“Ａ０”、“Ａ１”の入出力の関係についても同様である。
【００６７】
図１０は、オフセット管理に用いるリスト要素の構造体の例を示す図である。構造体Ｐは、各インスタンス（論理ブロック）および各変数に対するオフセットの管理に用いられる。このため、各インスタンスおよび各変数に対して１つのリスト要素が対応付けられることになる。リスト要素の階層構造では、モジュールおよび変数の階層構造が考慮される。すなわち、最上層のリスト要素はモジュールに対応することになる。最下層のリスト要素は変数に対応することになる。
【００６８】
ＣＮＦ変換部１３０は、構造体Ｐを用いてオフセットテーブル１１３を生成する。構造体Ｐの左側に付された番号は行番号である。構造体Ｐは、モジュール名、インスタンス名、オフセットおよび下位インスタンスリストの項目を含む。
【００６９】
モジュール名の項目には、モジュール名を示す文字列型のデータが設定される。ただし、最下層のリスト要素は値をもたない。モジュール名の項目に変数名が設定される。インスタンス名の項目には、モジュールに対するインスタンス名を示す文字列型のデータが設定される。ただし、最上層および最下層のリスト要素は、インスタンス名の設定値をもたない（値なし）。
【００７０】
オフセットの項目には、オフセットの値（オフセット値）を示す整数型のデータが設定される。下位インスタンスリストの項目には、１つ下位の階層のリスト要素へのポインタを示す配列型のデータが設定される。ただし、最下層のリスト要素は、下位インスタンスリストの設定値をもたない（値なし）。
【００７１】
図１１は、オフセットテーブルの例を示す図である。オフセットテーブル１１３は、組合せ回路データ１１２および構造体Ｐに基づいてＣＮＦ変換部１３０により生成され、記憶部１１０に格納される。ただし、オフセットテーブル１１３では、モジュール“Ｃ”のインスタンスについて、ｎ＝３までのインスタンスを図示し、ｎ≧４のインスタンスの図示を省略している。
【００７２】
例えば、最上層のリスト要素Ｐ１は、モジュール“ＤＵＴ＿ｕｎｒｏｌｌ”を示す。モジュール“ＤＵＴ＿ｕｎｒｏｌｌ”は最上層なので、リスト要素Ｐ１はインスタンス名の設定値をもたない。リスト要素Ｐ１には、オフセット値として“０”、下位インスタンスリストとしてリスト要素Ｐ１１，Ｐ１２，Ｐ１３へのポインタが設定されている。
【００７３】
リスト要素Ｐ１１，Ｐ１２，Ｐ１３は、それぞれモジュール“Ｃ”のインスタンス“Ｃ１”、“Ｃ２”、“Ｃ３”（論理ブロックＣ１，Ｃ２，Ｃ３）を示す。リスト要素Ｐ１１には、オフセット値として“０”、下位インスタンスリストとしてリスト要素Ｐ２１，Ｐ２２へのポインタが設定されている。リスト要素Ｐ１２には、オフセットとして値“１０００”、下位インスタンスリストとしてリスト要素Ｐ２１，Ｐ２２へのポインタが設定されている。リスト要素Ｐ１３には、オフセット値として“２０００”、下位インスタンスリストとしてリスト要素Ｐ２１，Ｐ２２へのポインタが設定されている。
【００７４】
リスト要素Ｐ２１，Ｐ２２は、それぞれモジュール“Ｂ”のインスタンス“Ｂ０”、“Ｂ１”を示す。リスト要素Ｐ２１には、オフセット値として“１００”、下位インスタンスリストとしてリスト要素Ｐ３１，Ｐ３２へのポインタが設定されている。リスト要素Ｐ２２には、オフセット値として“３００”、下位インスタンスリストとしてリスト要素Ｐ３１，Ｐ３２へのポインタが設定されている。
【００７５】
リスト要素Ｐ３１，Ｐ３２は、それぞれモジュール“Ａ”のインスタンス“Ａ０”、“Ａ１”を示す。リスト要素Ｐ３１には、オフセット値として“０”、下位インスタンスリストとしてリスト要素Ｐ４１，Ｐ４２，Ｐ４３へのポインタが設定されている。リスト要素Ｐ３２には、オフセット値として“１００”、下位インスタンスリストとしてリスト要素Ｐ４１，Ｐ４２，Ｐ４３へのポインタが設定されている。
【００７６】
リスト要素Ｐ４１，Ｐ４２，Ｐ４３は、それぞれ変数“ｖ１”、“ｖ２”、“ｖ３”を示す。リスト要素Ｐ４１，Ｐ４２，Ｐ４３は、最下層のリスト要素なのでインスタンス名および下位インスタンスリストの設定値をもたない。リスト要素Ｐ４１には、オフセット値“０”が設定されている。リスト要素Ｐ４２には、オフセット値“１”が設定されている。リスト要素Ｐ４３には、オフセット値“２”が設定されている。
【００７７】
ＣＮＦ変換部１３０は、図７，８で例示した階層構造をもつ組合せ回路Ｚ１に対して、次のようにオフセットテーブル１１３を生成し得る。（１）最下層のモジュール“Ａ”内で変数が定義される順番（例えば、ｖ１，ｖ２，ｖ３，・・・）を予め決定しておき、その順番にオフセット値を与える。具体的には、モジュール“Ａ”内のｍ（ここではｍ≦１００）個の変数ｖ（ｊ）（ｊ＝０，・・・，ｍ−１）に対し、オフセット値ｊを与える。（２）インスタンス“Ａ（ｉ）”（ｉ＝０，１）のベース値（インスタンスに対するオフセット値）を１００×ｉとする。モジュール“Ａ”のインスタンスを２つ包含するインスタンス“Ｂ（ｉ）”（ｉ＝０，１）のベース値を１００×（２×ｉ＋１）とする。モジュール“Ｂ”のインスタンスを２つ包含するインスタンス“Ｃ（ｉ）”（ｉ＝１，・・・，ｎ）のベース値を１０００×ｉとする。
【００７８】
図１２は、インデックスの計算例を示す図である。図１２では、モジュール“Ｃ”に対する論理ブロックＣ１，Ｃ２が例示されている。論理ブロックＣ１は、モジュール“Ｃ”のインスタンスなので、モジュール“Ｂ”のインスタンス“Ｂ０”、“Ｂ１”を含む。論理ブロックＣ２も同様にモジュール“Ｂ”のインスタンス“Ｂ０”、“Ｂ１”を含む。インスタンス“Ｂ０”は、モジュール“Ａ”のインスタンス“Ａ０”、“Ａ１”を含む。インスタンス“Ｂ１”も同様にモジュール“Ａ”のインスタンス“Ａ０”、“Ａ１”を含む。
【００７９】
ここで、論理ブロックＣ１に含まれるインスタンス“Ｂ０”、“Ｂ１”およびインスタンス“Ａ０”、“Ａ１”それぞれも、所定のモジュール定義を呼出して表された論理ブロックということができる。すなわち、組合せ回路Ｚ１は論理ブロックの階層構造により表されているといえる。以下の説明において、例えば、論理ブロックＣ１の配下のインスタンス“Ｂ０”を指して論理ブロックＣ１／Ｂ０と表記することがある。論理ブロックＣ１の配下のインスタンス“Ｂ１”を指して論理ブロックＣ１／Ｂ１と表記することがある。あるいは、論理ブロックＣ１／Ｂ０の配下のインスタンス“Ａ０”を指して論理ブロックＣ１／Ｂ０／Ａ０と表記することがある。このように、インスタンス名の列挙により、階層構造をもつ各論理ブロックを区別する。この表記は、変数においても同様である。例えば、論理ブロックＣ１／Ｂ０／Ａ０の配下の変数“ｖ１”であれば、変数Ｃ１／Ｂ０／Ａ０／ｖ１のように表せる。
【００８０】
図１２では、オフセットテーブル１１３で定義される各論理ブロックのオフセット値を「ｏｆｆ＝０」（“ｏｆｆ”は“ｏｆｆｓｅｔ”の先頭の３文字）のように示している。各論理ブロックおよび各変数のオフセット値は次の通りである。
【００８１】
論理ブロックＣ１のオフセット値は“０”である。論理ブロックＣ２のオフセット値は“１０００”である。論理ブロックＣ１／Ｂ０のオフセット値は“１００”である。論理ブロックＣ１／Ｂ１のオフセット値は“３００”である。論理ブロックＣ２／Ｂ０のオフセット値は“１００”である。論理ブロックＣ２／Ｂ１のオフセット値は“３００”である。
【００８２】
論理ブロックＣ１／Ｂ０／Ａ０のオフセット値は“０”である。変数Ｃ１／Ｂ０／Ａ０／ｖ１のオフセット値は“０”である。変数Ｃ１／Ｂ０／Ａ０／ｖ２のオフセット値は“１”である。変数Ｃ１／Ｂ０／Ａ０／ｖ３のオフセット値は“２”である。
【００８３】
論理ブロックＣ１／Ｂ０／Ａ１のオフセット値は“１００”である。変数Ｃ１／Ｂ０／Ａ１／ｖ１のオフセット値は“０”である。変数Ｃ１／Ｂ０／Ａ１／ｖ２のオフセット値は“１”である。変数Ｃ１／Ｂ０／Ａ１／ｖ３のオフセット値は“２”である。
【００８４】
論理ブロックＣ１／Ｂ１／Ａ０のオフセット値は“０”である。変数Ｃ１／Ｂ１／Ａ０／ｖ１のオフセット値は“０”である。変数Ｃ１／Ｂ１／Ａ０／ｖ２のオフセット値は“１”である。変数Ｃ１／Ｂ１／Ａ０／ｖ３のオフセット値は“２”である。
【００８５】
論理ブロックＣ１／Ｂ１／Ａ１のオフセット値は“１００”である。変数Ｃ１／Ｂ１／Ａ１／ｖ１のオフセット値は“０”である。変数Ｃ１／Ｂ１／Ａ１／ｖ２のオフセット値は“１”である。変数Ｃ１／Ｂ１／Ａ１／ｖ３のオフセット値は“２”である。
【００８６】
他の論理ブロックおよび他の変数も同様にしてオフセット値が定められる。これらのオフセット値を用いて各変数のインデックスを求めることができる。例えば、変数Ｃ１／Ｂ１／Ａ１／ｖ２のインデックスは、変数Ｃ１／Ｂ１／Ａ１／ｖ２のオフセット値“１”、論理ブロックＣ１／Ｂ１／Ａ１のオフセット値“１００”、論理ブロックＣ１／Ｂ１のオフセット値“３００”および論理ブロックＣ１のオフセット値“０”の合計である。よって、変数Ｃ１／Ｂ１／Ａ１／ｖ２のインデックスは、１＋１００＋３００＋０＝４０１となる。
【００８７】
他の例を挙げれば、変数Ｃ１／Ｂ０／Ａ０／ｖ３のインデックスは、変数Ｃ１／Ｂ０／Ａ０／ｖ３のオフセット値“２”、論理ブロックＣ１／Ｂ０／Ａ０のオフセット値“０”、論理ブロックＣ１／Ｂ０のオフセット値“１００”および論理ブロックＣ１のオフセット値“０”の合計である。よって、変数Ｃ１／Ｂ０／Ａ０／ｖ３のインデックスは、２＋０＋１００＋０＝１０２となる。
【００８８】
図１３は、ＣＮＦ論理式データの例を示す図である。ＣＮＦ論理式データ１１４は、学習節が追加される前のＣＮＦ論理式φ１のデータ例を示している。ここで、ＣＮＦ論理式データ１１４では、変数をｘ１’，ｘ２などのように表記している。これらの変数は、各論理ブロックにおける前述の各変数（変数Ｃ１／Ｂ０／Ａ０／ｖ１など）に対応している。すなわち、変数ｘ１’，ｘ２なども一意のインデックスが対応付けられる。
【００８９】
例えば、ＣＮＦ論理式データ１１４では、論理和をとる１つの項（変数の組）を配列で表し、各配列へのポインタのリストにより各項の論理積をとることを表す。ＣＮＦ論理式データ１１４によれば、φ１＝（ｘ１’＋ｘ２）（ｘ１’＋ｘ３＋ｘ９）（ｘ２’＋ｘ３’＋ｘ４）・・・（ｘ７’＋ｘ８’＋ｘ１１’）である。これは、図２で例示したＣＮＦ論理式φ１に相当する。
【００９０】
ＣＮＦ論理式データ１１４ａは、ＳＡＴ処理部１４０により、ＣＮＦ論理式φ１に所定の学習節が追加された例を示している。追加された学習節は、（ｘ４＋ｘ７）および（ｘ３＋ｘ６＋ｘ９）である。これらの項がＣＮＦ論理式φ１に追加されることで、φ１＝１（真）になるために、（ｘ４＋ｘ７）＝１、かつ、（ｘ３＋ｘ６＋ｘ９）＝１が必要であることを表せる。
【００９１】
図１４は、検証処理の例を示すフローチャートである。以下、図１４に示す処理をステップ番号に沿って説明する。
（Ｓ１１）時間展開部１２０は、検証対象の順序回路Ｚを、組合せ回路Ｚ１へ時間展開する。具体的には、時間展開部１２０は、検証対象回路データ１１１を参照して、１つのモジュールをｎ時間分複製し、組合せ回路データ１１２を生成し、記憶部１１０に格納する。ここで、ｎの値は検証したい内容に応じて予め与えられる。
【００９２】
（Ｓ１２）ＣＮＦ変換部１３０は、組合せ回路データ１１２を参照して、オフセットテーブル１１３を生成する。各論理ブロックおよび各変数に対するオフセット値の付与ルールは、図１１で例示したように予め与えられる。
【００９３】
（Ｓ１３）ＣＮＦ変換部１３０は、組合せ回路データ１１２を参照して、ＣＮＦ論理式データ１１４を生成し、記憶部１１０に格納する（組合せ回路データ１１２をＣＮＦ論理式データ１１４に変換）。例えば、前述のように基本的な演算の論理ゲートに対するＣＮＦ論理式の情報を、ライブラリとして記憶部１１０に予め格納しておく。ＣＮＦ変換部１３０は、組合せ回路データ１１２に含まれる論理ゲートに応じて、記憶部１１０に記憶された各論理ゲートに対するＣＮＦ論理式を組合せることで、ＣＮＦ論理式データ１１４を生成し得る。ＣＮＦ論理式データ１１４に含まれる各変数は、オフセットテーブル１１３から計算されるインデックスに一意に対応付けられる。
【００９４】
（Ｓ１４）ＳＡＴ処理部１４０は、ＣＮＦ論理式データ１１４を用いて組合せ回路Ｚ１が検証する所定のプロパティ（例えば、デッドロックなど）に対応する内部状態を取り得るか否かについて、ＳＡＴの手法による検証を開始する。ＳＡＴ処理部１４０は、各変数に対する真偽値の探索の順序を任意に決定できる。例えば、ＣＮＦ論理式データ１１４の各配列内に現れる個数が多い変数から優先的に真偽値を探索することが考えられる。
【００９５】
（Ｓ１５）ＳＡＴ処理部１４０は、何れかの変数の組を決定したところで矛盾が発生したか否かを判定する。矛盾が発生した場合、処理をステップＳ１６に進める。矛盾が発生していない場合、処理をステップＳ１９に進める。
【００９６】
（Ｓ１６）ＳＡＴ処理部１４０は、所定の矛盾解析機能により、矛盾の原因を求め、当該原因に応じた学習節を生成する。例えば、ＣＮＦ論理式が（ｘ１＋ｘ７’＋ｘ９）および（ｘ１＋ｘ７’＋ｘ９’）のような２つの項を含むとき、ｘ１＝０かつｘ７＝１で矛盾が発生する。この場合、矛盾の原因はｘ１＝０かつｘ７＝１ということになる。この場合、ｘ１＝１かｘ７＝０でなければならない旨を示す学習節（ｘ１＋ｘ７’）をＣＮＦ論理式に追加する。ＳＡＴ処理部１４０は、生成した学習節をＣＮＦ論理式データ１１４に登録する。
【００９７】
（Ｓ１７）ＳＡＴ処理部１４０は、学習節に含まれる変数の組のインデックスとオフセットテーブル１１３とに基づいて、学習節の変数の組を含むモジュールのインスタンス化の状況を確認する。オフセットテーブル１１３の例でいえば、インデックスの１００〜１９９の変数は論理ブロックＣ１／Ｂ０／Ａ０に包含される。同様に、インデックスの２００〜２９９の変数は論理ブロックＣ１／Ｂ０／Ａ１に包含される。インデックスの３００〜３９９の変数は論理ブロックＣ１／Ｂ１／Ａ０に包含される。インデックスの４００〜４９９の変数は論理ブロックＣ１／Ｂ１／Ａ１に包含される。すなわち、下２桁が００〜９９のインデックスはモジュールＡの１つのインスタンスに包含される。したがって、例えば、学習節に含まれる各変数のインデックスが３００〜３９９の範囲に全て含まれていれば（例えば、インデックスの組が“３００，３０２”）、ＳＡＴ処理部１４０は、モジュールＡのインスタンス化の状況を確認する。本例の場合、モジュールＣのインスタンス１つ当たり、モジュールＡのインスタンスは４個含まれている。組合せ回路データ１１２に含まれるモジュールＣのインスタンスの数がｎなら、組合せ回路データ１１２に含まれるモジュールＡのインスタンスの数は４ｎである。
【００９８】
（Ｓ１８）ＳＡＴ処理部１４０は、ステップＳ１７で確認したインスタンスに含まれる変数のうち、これらの変数のインデックスに基づいて、ステップＳ１６で生成した学習節に含まれる変数の組に対応する変数の組を特定する。ステップＳ１７の例のように、学習節に含まれる変数のインデックスの組が“３００，３０２”であれば、インデックスの組“１００，１０２”、“２００，２０２”、“４００，４０２”、“１１００，１１０２”、“１２００，１２０２”・・・などに対応する変数の組を特定する。ＳＡＴ処理部１４０は、特定した変数の各組について、ステップＳ１６で生成した学習節と同様の学習節を生成する。例えば、インデックス“３００，３０２”の変数の組（ｘ１，ｙ１）について、学習節（ｘ１＋ｙ１）を生成したなら、インデックス“１００，１０２”の変数の組（ｘ２，ｙ２）について、学習節（ｘ２＋ｙ２）を生成する。インデックス“２００，２０２”、“４００，４０２”、“１１００，１１０２”などに対応する変数の組に対しても同様である。この場合、モジュールＡに含まれるある変数の組に対して学習節を生成したなら、他の変数の４ｎ−１個の組に対して学習節が生成されることになる。そして、処理をステップＳ１５に進める。
【００９９】
（Ｓ１９）ＳＡＴ処理部１４０は、ＣＮＦ論理式データ１１４を用いた検証を完了したか否かを判定する。完了した場合、処理をステップＳ２０に進める。完了していない場合、処理をステップＳ１５に進める（検証を継続する）。
【０１００】
（Ｓ２０）ＳＡＴ処理部１４０は、充足可否の検証結果を出力する。例えば、ＣＮＦ論理式φ１において、デッドロックなどのエラー発生時の状態がφ１＝１で表されるなら、充足可能である場合に設計に誤りがあることになる。その場合、ＳＡＴ処理部１４０は、反例パターン（φ１＝１を充足させる変数値の組合せなど）を出力する。一方、充足不可能である場合（φ１＝１を充足させる変数値の組合せが存在しない場合）に、設計は正しいということになるので、その旨を出力する。
【０１０１】
図１５は、学習節の複製の例を示す図である。例えば、検証装置１００は、ステップＳ１７，Ｓ１８で例示したように、インデックスの組“３００，３０２”に対応する変数Ｃ１／Ｂ１／Ａ０／ｖ１（変数ｘ１）および変数Ｃ１／Ｂ１／Ａ０／ｖ３（変数ｘ２）について学習節Ｌを取得する。ここで、図１５では、学習節Ｌを組合せ回路データ１１２内の定義およびインデックスを用いて“Ｌ＝（ｖ１＋ｖ３）＝（３００＋３０２）”と表記している。
【０１０２】
検証装置１００は、学習節Ｌの変数の組に対応する他の変数の組について学習節を複製する。具体的には、インデックスの組“１００，１０２”、“２００，２０２”、“４００，４０２”、“１１００，１１０２”、“１２００，１２０２”・・・などに対応する変数の組に対して、学習節Ｌと同様の学習節を生成する。そして、検証装置１００は、生成した複数の学習節の論理積を新たな学習節とする。図１５では、この学習節を変数のインデックスを用いて“｛（１００＋１０２）∧（２００＋２０２）∧（３００＋３０２）∧（４００＋４０２）・・・｝”と表している。
【０１０３】
ここで、モジュールＡに包含される変数の組について学習節が取得された場合を例示したが、モジュールＢやモジュールＣに包含される変数の組について学習節が取得された場合も同様にして学習節を複製できる。
【０１０４】
例えば、検証装置１００は、インデックスの組“１０１，２０１”に対応する変数の組に対する学習節を取得することもある。インデックスの組“１０１，２０１”に対応する変数の組を包含するモジュールはモジュールＢである。したがって、検証装置１００は、モジュールＢの複製状況を確認する。本例では、モジュールＣはモジュールＢを２つ含む。したがって、組合せ回路データ１１２に含まれるモジュールＢのインスタンスの数は２ｎである。このため、検証装置１００は、インデックスの組“１０１，２０１”に対応する変数の組の学習節に対して、２ｎ−１個の他の学習節を生成する。例えば、インデックスの組“３０１，４０１”に対応する変数の組などについて他の学習節を生成する。
【０１０５】
また、例えば、検証装置１００は、インデックスの組“２０２，３０１”に対応する変数の組に対する学習節を取得することもある。インデックスの組“２０２，３０１”に対応する変数の組を包含するモジュールはモジュールＣである。したがって、検証装置１００は、モジュールＣの複製状況を確認する。本例では、組合せ回路Ｚ１はモジュールＣのインスタンスをｎ個含む。このため、検証装置１００は、インデックスの組“２０２，３０１”に対応する変数の組の学習節に対して、ｎ−１個の他の学習節を生成する。例えば、インデックスの組“１２０２，１３０１”に対応する変数の組などについて他の学習節を生成する。
【０１０６】
このように、学習節に含まれる複数の変数が、モジュールＢの複数のインスタンスやモジュールＣの複数のインスタンスに跨る場合であっても、学習節の複製を行える。すなわち、モジュールの階層構造に依らずに、学習節を複製できる。
【０１０７】
以上のように、検証装置１００によれば検証の時間を短縮できる。具体的には、上記のように、ある論理ブロックで見出された学習節は、共通の構造をもつ（呼出し元のモジュール定義が共通する）他の論理ブロックに対しても適用できると考えられる。すなわち、呼出し元のモジュール定義が共通する他の論理ブロックの各変数に対して真偽値の決定を行っていけば、先に取得された学習節の変数の組に対応する変数に対して、同様の学習節が見出されると考えられる。
【０１０８】
そこで、１つの学習節を取得したタイミングで、別の論理ブロックの変数の組に対する学習節を生成することで、別の論理ブロックの変数の組に対する学習節を先取りする。すると、１つの学習節を取得したタイミングで他の変数の組に対する制約が追加されることになる。また、その後、他の変数の組に対して余計な真偽値の探索が行われることを抑制でき、余計なバックトラックの発生を抑えられる。その結果、論理回路の検証の時間を短縮できる。
【０１０９】
検証装置１００による検証は、順序回路を時間展開することで得られた組合せ回路の定義情報を用いる場合に特に有効である。順序回路を時間展開することで得られた組合せ回路は、順序回路の所定の論理ブロックの複製を複数個含む論理回路として表せるからである。
【０１１０】
また、第２の実施の形態では、モジュール“Ｃ”内に他のモジュールが含まれる例（モジュールが階層構造をもつ例）を示した。一方、モジュール“Ｃ”の直下に変数が定義されている場合（モジュール“Ｃ”が階層構造をもたない場合）にも、次のように簡便にインスタンスのオフセット値（ベース値）および変数のオフセット値を決定できる。具体的には、次のとおりである。
【０１１１】
（１）モジュール“Ｃ”内で変数が定義される順番を予め決定しておき、その順番にオフセット値を与える。具体的には、モジュール“Ｃ”内のｍ（ｍは正の整数）個の変数ｖ（ｊ）（ｊ＝０，・・・，ｍ−１）に対し、オフセット値ｊを与える。
【０１１２】
（２）インスタンス“Ｃ（ｉ）”（ｉ＝１，・・・，ｎ）のベース値を（ｍ×（ｉ−１））とする。
（３）ＳＡＴによる検証中に、モジュール“Ｃ”の何れかのインスタンスにおいて学習節Ｌ（ｉ）を見つけた場合、学習節Ｌ（ｉ）に含まれる変数ｓ（ｊ）（ｊ＝０，・・・，ｍ−１）のインデックスからベース値Ｂ（ｉ）とオフセット値Ｆ（ｊ）を求める。ベース値Ｂ（ｉ）を０，・・・，（ｍ×（ｎ−１））とすることで、Ｌ（１），・・・，Ｌ（ｎ）を求める。そして、｛∧i=1nＬ（ｉ）｝＝｛Ｌ（１）∧・・・∧Ｌ（ｎ）｝を学習節とする。このようにして、論理回路の検証の時間を短縮できる。
【０１１３】
なお、第１の実施の形態の情報処理は、演算部１ｂにプログラムを実行させることで実現できる。また、第２の実施の形態の情報処理は、プロセッサ１０１にプログラムを実行させることで実現できる。プログラムは、コンピュータ読み取り可能な記録媒体１３（例えば、光ディスク、メモリ装置およびメモリカードなど）に記録できる。
【０１１４】
例えば、プログラムを記録した記録媒体１３を配布することで、プログラムを流通させることができる。また、プログラムを他のコンピュータに格納しておき、ネットワーク経由でプログラムを配布してもよい。コンピュータは、例えば、記録媒体１３に記録されたプログラムまたは他のコンピュータから受信したプログラムを、ＲＡＭ１０２やＨＤＤ１０３などの記憶装置に格納し（インストールし）、当該記憶装置からプログラムを読み込んで実行してもよい。
【符号の説明】
【０１１５】
１  検証装置
１ａ  記憶部
１ｂ  演算部
２  論理回路の定義情報
２ａ，２ｂ  論理ブロック
３，４  論理式
５，６  学習節
【図１】
2015172873.tif 000003
【図２】
2015172873.tif 000004
【図３】
2015172873.tif 000005
【図４】
2015172873.tif 000006
【図５】
2015172873.tif 000007
【図６】
2015172873.tif 000008
【図７】
2015172873.tif 000009
【図８】
2015172873.tif 000010
【図９】
2015172873.tif 000011
【図１０】
2015172873.tif 000012
【図１１】
2015172873.tif 000013
【図１２】
2015172873.tif 000014
【図１３】
2015172873.tif 000015
【図１４】
2015172873.tif 000016
【図１５】
2015172873.tif 000017