(57)【特許請求の範囲】
【請求項１】
任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンにおける有界モデル検査方法であって、下記要件を備える。
Fはイベンチュアリィ演算子、Gはグローバリー演算子、Uはアンティル演算子、Xはネクスト−タイム演算子を表す時相演算子F(p)、G(p)、U(p, q)、X(p)に関連付けられた特性を、ブール充足可能性検査のための変換スキーマに変換し、
特性全体を、F(p)、G(p)、U(p, q)、X(p)の各演算子に関する前記変換スキーマの繰り返し実行によって検査し、
前記F(p)の変換スキーマは、下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  現在のパスのi番目の状態におけるpの充足可能性を検査する。
c)  充足可能な場合は、探索を成功として終了する。
d)  充足不能な場合は、pはi番目の状態においては常に偽であることを学習し、この学習した知識を制約データベースに追加する。
e)  iを所定の上限まで増大させながらステップb〜dを繰り返し実行することによって探索を継続する。
f)  所定の上限に到達すると、探索を不確定のまま終了する。
前記G(p)の変換スキーマは下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  pが現在のパスのi番目の状態において充足されることを保証するための制約をデータベースに追加し、充足可能性を検査する。
c)  充足不能な場合は、探索を失敗として終了する。
d)  充足可能な場合は、開始状態からi番目の状態までの間でj番目の状態が各々ループバック状態かどうか検査し、ループバック状態が検出されたら探索を成功として終了する。
e)  開始状態より前のj番目の状態が各々ループバック状態かどうか検査し、ループバック状態が検出されたら探索を成功として終了する。
f)  iを所定の上限まで増大させながらステップa〜eを繰り返し実行することによって探索を継続する。
g)  所定の上限に到達すると、探索を不確定のまま終了する。
【請求項２】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、次に検査する演算子に関して選択肢が存在する場合には、ブール充足可能性検査における探索の難度により決定される優先順位に従って選択を行うと共に、前記探索の難度は、X演算子、F演算子、U演算子、G演算子の順によって高くする。
【請求項３】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、変換スキーマが、対応するブール充足可能性問題をサイズの小さい複数のブール充足可能性下位問題に分割するために、対応する有界モデル検査問題のk番目のSATインスタンスに対して分割を実行する。
【請求項４】
請求項３に記載の任意線形時間論理時相特性の有界モデル検査方法であって、前記分割を演算子間にまたがって実行し、各演算子に対しては時間フレーム間と時間フレーム内の両方で実行する。
【請求項５】
請求項４に記載の任意線形時間論理時相特性の有界モデル検査方法であって、前記分割は可能な場合は常に、漸増的に関連付けられるブール充足可能性下位問題に到達するように方向付けする。
【請求項６】
請求項４に記載の任意線形時間論理時相特性の有界モデル検査方法であって、複数のブール充足可能性下位問題にまたがる学習を使用する。
【請求項７】
請求項４に記載の任意線形時間論理時相特性の有界モデル検査方法であって、複数の関連する下位問題にまたがる学習を行うために、ブール充足可能性アルゴリズムの漸増的な公式化を使用する。
【請求項８】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、定数の伝搬に基づく回路単純化を使用する。
【請求項９】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、構造同形の検出に基づく回路の単純化を使用する。
【請求項１０】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ブール充足可能性検査問題を、回路ベースとCNFベースの充足可能性アルゴリズムを結合したハイブリッドSATソルバーを使用して解決する。
【請求項１１】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ステップd〜e間の完全性を検査するステップをさらに備える。
【請求項１２】
請求項１１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、完全性を検査するステップはさらに下記ステップを備える。
(i)  i番目の状態を起点とする遷移がパス内の検査済みの状態を訪れないようにするための制約を追加し、制約データベースの充足可能性を検査する。
(ii)  充足不能な場合は、探索を失敗として終了する。
(iii)  充足不能でない場合は、探索を継続する。
(iv)  以前の状態がすべて検査されるまでステップ(i)〜(iii)を繰り返す。
【請求項１３】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ステップdは以下によって実行される。
(di)  i番目の状態からj番目の状態までの遷移の充足可能性を検査する。
(dii)  ステップdiの遷移が充足可能な場合は、探索を成功として終了する。
(diii)  ステップdiの遷移が充足不能な場合は、このような遷移が存在しないことを学習し、この知識を制約データベースに追加する。
(div)  開始状態からi番目の状態までのすべての状態が検査されるまで(di)〜(diii)を繰り返すことによって探索を継続する。
【請求項１４】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ステップeは以下によって実行される。
(ei)  j番目の状態から開始状態までの各状態のＰの充足可能性を検査する。
(eii)  ステップeiで充足不能な場合は、ステップeを中止してステップfに進む。
(eiii)  ステップeiで充足可能な場合は、i番目の状態からj番目の状態までの遷移の充足可能性を検査する。
(eiv)  ステップeiiiの遷移が充足可能な場合は、探索を成功として終了する。
(ev)  ステップeiiiの遷移が充足不能な場合は、初期状態(i=0)から開始状態までのすべての状態が検査されるまでステップei〜eivを繰り返すことによって探索を継続する。
【請求項１５】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ステップe〜f間の完全性を検査するステップをさらに備える。
【請求項１６】
請求項１５に記載の任意線形時間論理時相特性の有界モデル検査方法であって、完全性を検査するステップはさらに下記ステップを備える。
(i)  i番目の状態を起点とする遷移がパス内の検査済みの状態を訪れないようにするための制約を追加し、制約データベースの充足可能性を検査する。
(ii)  ステップiで充足不能な場合は、探索を失敗として終了する。
(iii)  ステップiで充足可能な場合は、探索を継続する。
(iv)  以前の状態がすべて検査されるまでステップ(i)〜(iii)を繰り返す。
【請求項１７】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、U(p, q) の変換スキーマは下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  現在のパスのi番目の状態におけるqの充足可能性を検査する。
c)  充足可能な場合は、探索を成功として終了する。
d)  充足不能な場合は、qはi番目の状態においては常に偽であることを学習し、この学習した知識を制約データベースに追加する。
e)  pがi番目の状態において充足されることを保証するための制約をデータベースに追加し、充足可能性を検査する。
f)  ステップeで充足不能な場合は、探索を失敗として終了する。
g)  ステップeで充足可能な場合は、探索を継続する。
h)  iを所定の上限まで増大させながらステップb〜gを繰り返し実行することによって探索を継続する。
i)  所定の上限に到達すると、探索を不確定のまま終了する。
【請求項１８】
請求項１７に記載の任意線形時間論理時相特性の有界モデル検査方法であって、ステップg〜h間の完全性を検査するステップをさらに備える。
【請求項１９】
請求項１８に記載の任意線形時間論理時相特性の有界モデル検査方法であって、完全性を検査するステップはさらに下記ステップを備える。
(i)  i番目の状態を起点とする遷移がパス内の検査済みの状態を訪れないようにするための制約を追加し、制約データベースの充足可能性を検査する。
(ii)  ステップiで充足不能な場合は、探索を失敗として終了する。
(iii)  ステップiで充足可能な場合は、探索を継続する。
(iv)  以前の状態がすべて検査されるまでステップ(i)〜(iii)を繰り返す。
【請求項２０】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、X(p)の変換スキーマは下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  さらにもう1つの時間フレームに遷移関係を展開し、時間フレームi+1においてpが真であるかどうかを検査する。
c)  pが時間フレームi+1において真であることが確認された場合は、成功として終了する。
d)  pが時間フレームi+1において偽であることが確認された場合は、失敗として終了する。
e)  pの検査が時間フレームi+1において不確定の場合は、不確定として終了する。
【請求項２１】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、充足可能性検査のサブセットが単一の充足可能性検査として結合される。
【請求項２２】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、充足可能性検査のサブセットが単一の充足可能性検査として結合される。
【請求項２３】
請求項１７に記載の任意線形時間論理時相特性の有界モデル検査方法であって、充足可能性検査のサブセットが単一の充足可能性検査として結合される。
【請求項２４】
請求項２０に記載の任意線形時間論理時相特性の有界モデル検査方法であって、充足可能性検査のサブセットが単一の充足可能性検査として結合される。
【請求項２５】
線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンにおける帰納証明の方法であって、下記ステップを備える。
SATインスタンスの基本ケースを、与えられた特性の否定に関して検査するステップ、SATインスタンスの帰納ステップを、与えられた特性に対応するモニター述語に関して検査するステップ、k=0から開始し、任意に指定された上限までそれを漸増させるステップを備え、前記基本ケースの検査はさらに下記ステップを備える。
否定された特性を、Fがイベンチュアリィ演算子、Xがネクスト−タイム演算子を表す時相演算子F(p)およびX(p)と関連づけられたブール充足可能性検査から成る変換スキーマに変換するステップと、初期状態を起点として、F(p)、X(p)演算子に関する変換スキーマの繰り返し実行により、否定された特性の証拠を探索するステップ。
証拠が検出されないことが証明された場合は、証明全体を成功として終了する。
k時間フレーム内に証拠が検出された場合は、証明全体を失敗として終了する。
結果が不確定の場合は、帰納ステップの検査を継続する。
この帰納ステップの検査は、以下の変換スキーマから成る。
モニター述語が任意状態からk時間フレームにわたって有効で、かつk+1番目の時間フレーム内では有効ではない状況を保証するための制約を追加する。
充足不能な場合は、証明全体を成功として終了する。
充足不能でない場合は、探索を継続する。
前記探索を、kを所定の上限まで漸増させながら基本ケースと帰納ステップを繰り返し実行することで継続する。
kが指定された上限に到達した場合は、証明は不確定となる。
前記F(p)の変換スキーマは下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  現在のパスのi番目の状態におけるpの充足可能性を検査する。
c)  充足可能な場合は、探索を成功として終了する。
d)  充足不能な場合は、pはi番目の状態においては常に偽であることを学習し、この学習した知識を制約データベースに追加する。
e)  iを所定の上限まで増大させながらステップb〜dを繰り返し実行することによって探索を継続する。
f)  所定の上限に到達すると、探索を不確定のまま終了する。
前記X(p)の変換スキーマは下記ステップを備える。
a)  時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始し、ここでi=0は初期状態に対応する。
b)  さらにもう1つの時間フレームに遷移関係を展開し、時間フレームi+1においてpが真であるかどうかを検査する。
c)  pが時間フレームi+1において真であることが確認された場合は、成功として終了する。
d)  pが時間フレームi+1において偽であることが確認された場合は、失敗として終了する。
e)  pの検査が時間フレームi+1において不確定の場合は、不確定として終了する。
【請求項２６】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、k時間フレーム内の状態が一意であることを保証するための制約を追加し、それにより完全な証明プロシージャーを提供する。
【請求項２７】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、次に検査する演算子に関して選択肢が存在する場合には、探索の難度により決定される優先順位に従って選択を行うと共に、前記探索の難度を、X演算子、F演算子の順に高める。
【請求項２８】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、変換スキーマが、対応するブール充足可能性問題をサイズの小さい複数のブール充足可能性下位問題に分割するために、帰納下位問題のk番目のSATインスタンスに対して分割を実行する。
【請求項２９】
請求項２８に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、前記分割を演算子間にまたがって実行し、各演算子に対しては時間フレーム間と時間フレーム内の両方で実行する。
【請求項３０】
請求項２９に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、この分割は可能な場合は常に、漸増的に関連付けられるブール充足可能性問題に到達するように方向付けする。
【請求項３１】
請求項２９に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、複数のブール充足可能性問題にまたがる学習を使用する。
【請求項３２】
請求項２９に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、複数の関連する下位問題にまたがる学習を行うために、ブール充足可能性アルゴリズムの漸増的な公式化を使用する。
【請求項３３】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、定数の伝搬に基づく回路単純化を使用する。
【請求項３４】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、構造同形の検出に基づく回路の単純化を使用する。
【請求項３５】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、ブール充足可能性検査問題を、回路ベースとCNFベースの充足可能性アルゴリズムを結合したハイブリッドSATソルバーを使用して解決する。
【請求項３６】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、ステップd〜e間の完全性を検査するステップをさらに備える。
【請求項３７】
請求項３６に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、完全性を検査するステップはさらに下記ステップを備える。
(i)  i番目の状態を起点とする遷移がパス内の検査済みの状態を訪れないようにするための制約を追加し、制約データベースの充足可能性を検査する。
(ii)  ステップiで充足不能な場合は、探索を失敗として終了する。
(iii)  ステップiiで充足不能な場合は、探索を継続する。および
(iv)  以前の状態がすべて検査されるまでステップ(i)〜(iii)を繰り返す。
【請求項３８】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、充足可能性検査のサブセットは単一の充足可能性検査として結合できる。
【請求項３９】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、充足可能性検査のサブセットは単一の充足可能性検査として結合できる。
【請求項４０】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、真であることが既知の追加の制約を帰納不変式として使用する。
【請求項４１】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、帰納不変式として使用される過剰近似到達可能状態集合を得るために、近似到達可能性分析を使用する。
【請求項４２】
請求項４１に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、帰納不変式として使用される過剰近似到達可能状態集合を得るために、近似到達可能性分析をベースとする二分決定グラフを使用する。
【請求項４３】
請求項２５に記載の線形時間時相論理で表現された安全性特性の帰納証明の方法であって、展開されたモデル内で回路信号間の等価が発見され、帰納不変式として使用される。
【請求項４４】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、改変の下に埋め込まれた有界数のEX演算子を有する特性を含めるために、充足可能性検査を使用してEXの解を列挙し、その後減少させることによって、変換スキーマが線形時間時相論理を超えて拡張される。
【請求項４５】
請求項４４に記載の任意線形時間論理時相特性の有界モデル検査方法であって、改変の下に埋め込まれたFモダリティを近似的な方法で処理するために、有界数のX演算子を使用してFをモデリングすることにより、変換スキーマが線形時間時相論理を超えて拡張される。
【請求項４６】
請求項１に記載の任意線形時間論理時相特性の有界モデル検査方法であって、特性二分決定図ベース分析を使用して、有界モデル検査方式が計算木論理特性に拡張される。
【請求項４７】
任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、前記エンジンは下記要件を備える。
Fはイベンチュアリィ演算子、Gはグローバリー演算子、Uはアンティル演算子、Xはネクスト−タイム演算子を表す時相演算子F(p)、G(p)、U(p, q)、X(p)に関連付けられた特性を、ブール充足可能性検査から成る変換スキーマに変換するように適応された特性トランスレーター、および、
特性全体を、F(p)、G(p)、U(p, q)、X(p)の各演算子に関する変換スキーマの繰り返し実行で構成されるカスタマイズされた方法で検査するように適応された特性チェッカー。
【請求項４８】
請求項４７に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、次に検査する演算子に関して選択肢が存在する場合には、当該エンジンが、探索の難度により決定される優先順位に従って選択を行うように適応され、前記探索の難度は、X演算子、F演算子、U演算子、G演算子の順に高まる。
【請求項４９】
請求項４７に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、変換スキーマに関して、対応するブール充足可能性問題をサイズの小さい複数のブール充足可能性下位問題に分割するために、対応する有界モデル検査問題のk番目のSATインスタンスに対して分割を実行するように適応される。
【請求項５０】
請求項４９に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、分割を演算子間にまたがって実行し、また各演算子に対しては時間フレーム間と時間フレーム内の両方で実行するように適応される。
【請求項５１】
請求項５０に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、分割を可能な場合は常に、漸増的に関連付けられるブール充足可能性下位問題に到達するように方向付けするように適応される。
【請求項５２】
請求項５０に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、複数のブール充足可能性下位問題にまたがって学習するように適応される。
【請求項５３】
請求項５０に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、複数の関連する下位問題にまたがる学習を行うために、ブール充足可能性アルゴリズムの漸増的な公式化を実行するように適応される。
【請求項５４】
請求項４７に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、定数の伝搬に基づく回路の単純化を実行するように適応される。
【請求項５５】
請求項４７に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、構造同形の検出に基づく回路の単純化を実行するように適応される。
【請求項５６】
請求項４７に記載の任意線形時間論理時相特性の有界モデル検査の機能を有する回路検証用の検証エンジンであって、当該エンジンは、ブール充足可能性検査問題を解決するためのハイブリッドSATソルバーをさらに備え、当該ハイブリッドSATソルバーは回路ベースおよびCNFベースの充足可能性アルゴリズムの使用を組み合わせる。
【請求項５７】
線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、前記エンジンは下記要件を備える。
与えられた特性が否定された場合に、SATインスタンスの基本ケースを検査するように適応された基本ケース・チェッカー、
与えられた特性に対応するモニター述語においてSATインスタンスの帰納ステップを検査するように適応された帰納ステップ・チェッカー、
否定された特性を特性に変換するように適応された特性トランスレーター、
Fはイベンチュアリィ演算子、Xはネクスト−タイム演算子を表す時相演算子F(p)、X(p)に関連付けられたブール充足可能性検査から成る検査スキーマ、および
否定された特性の証拠を探索するように適応されたサーチャー。
【請求項５８】
請求項５７に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、次に検査する演算子に関して選択肢が存在する場合には、当該エンジンが、探索の難度により決定される優先順位に従って選択を行うように適応され、当該難度がX演算子、F演算子の順に高まると想定するように適応される。
【請求項５９】
請求項５７に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、変換スキーマに関して、対応するブール充足可能性問題をサイズの小さい複数のブール充足可能性下位問題に分割するために、対応する有界モデル検査問題のk番目のSATインスタンスに対して分割を実行するように適応される。
【請求項６０】
請求項５９に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、分割を演算子間にまたがって実行し、また各演算子に対しては時間フレーム間と時間フレーム内の両方で実行するように適応される。
【請求項６１】
請求項６０に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、分割を可能な場合は常に、漸増的に関連付けられるブール充足可能性下位問題に到達するように方向付けするように適応される。
【請求項６２】
請求項６０に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、複数のブール充足可能性下位問題にまたがって学習するように適応される。
【請求項６３】
請求項６０に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、複数の関連する下位問題にまたがる学習を行うために、ブール充足可能性アルゴリズムの漸増的な公式化を実行するように適応される。
【請求項６４】
請求項５７に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、定数の伝搬に基づく回路の単純化を実行するように適応される。
【請求項６５】
請求項５７に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、構造同形の検出に基づく回路の単純化を実行するように適応される。
【請求項６６】
請求項５７に記載の線形時間論理時相特性のうち安全性特性を証明する機能を有する回路用帰納証明エンジンであって、当該エンジンは、ブール充足可能性検査問題を解決するためのハイブリッドSATソルバーをさらに備え、当該ハイブリッドSATソルバーは回路ベースおよびCNFベースの充足可能性アルゴリズムの使用を組み合わせる。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明では、デジタル回路の形式的検証における技術に関し、特に、ブール充足可能性(Boolean Satisfiability)と二分決定グラフ(Binary Decision Diagrams)に基づく新規な分割、順次学習、および帰納証明を使用して、デジタル回路の時相特性に関する有界モデル検査(bounded model checking)を行うためのソフトウェア、システム、方法が提供される。
【０００２】
【従来の技術】
１．  参考文献
以下の各論文は有益な背景情報を提供するものであり、本明細書の以降の部分では各々に付される括弧で囲んだ文献番号により適宜言及される。
【０００３】
【非特許文献１】
E. M. Clarke, 0. Grumberg, and D. Peled, Model Checking (モデル検査): MIT Press, 1999.
【非特許文献２】
K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem (状態爆発問題): Kluwer Academic Publishers, 1993.
【非特許文献３】
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs (BDDSを使用しない記号的モデル検査), " in Proceedings of Workshop on Tools and Algorithms for Analysis and Construction of Systems (TACAS), vol. 1579, LNCS, 1999.
【非特許文献４】
R. E. Bryant, "Graph-based algorithms for Boolean function manipulation (ブール関数操作のためのグラフ・ベース・アルゴリズム)," IEEE Transactions on Computers, vol. C-35(8), pp. 677-691, 1986.
【非特許文献５】
M. Sheeran, S. Singh, and G. Stalmarck, "Checking Safety Properties using Induction and a SAT Solver (帰納およびSATソルバーを使用した安全特性の検査)," in Proceedings of Conference on Formal Methods in Computer-Aided Design, 2000.
【非特許文献６】
P. Ashar, M. Ganai, A. Gupta, Z. Yang, A. Mukaiyama, and K. Wakabayashi, "Formal Verification in an Industrial Setting: DiVer Verification Platform White Paper (産業環境における形式的検証: DiVer検証プラットフォーム白書)," NEC USA, CCRL 2001-C004-4-5509-1N, Dec 2001 2001.
【非特許文献７】
P. Ashar, P. Chauhan, M. Ganai, A. Gupta, Z. Yang, and L. Zhang, "DiVer Document: User Manual Verification Platform for Digital Systems (DiVerドキュメント: デジタル・システムのためのユーザー・マニュアル検証プラットフォーム)," NEC USA, CCRL 2001-C005-4-5509-2N, Dec 2001 2001.
【非特許文献８】
P. Ashar, P. Chauhan, M. Ganai, A. Gupta, Z. Yang, and L. Zhang, "DiVer Document: Tutorial - NEC production design case studies (DiVerドキュメント: チュートリアル−NEC生産設計事例研究)," NEC USA, CCRL 2001-C083-4-5509-5, Dec 2001 2001.
【非特許文献９】
H. Zhang, "SATO: An efficient propositional prover (SATO: 効率的な命題プルーバー)," in Proceedings of International Conference on Automated Deduction, vol. 1249, LNAI, 1997, pp. 272-275.
【非特許文献１０】
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver (Chaff: 効率的なSATソルバーの設計)in Proceedings of Design Automation Conference, 2001.
【非特許文献１１】
P. Bjesse and K. Claessen, "SAT-based verification without state space traversal (状態空間トラバースを伴わないSATベース検証)," in Proceedings of Conference on Formal Methods in Computer-Aided Design, 2000.
【非特許文献１２】
M. Ganai and A. Aziz, "Improved SAT-based Bounded Reachability Analysis (改良型SATベース有界到達可能性分析)," in Proceedings of VLSI Design Conference, 2002.
【非特許文献１３】
O. Shtrichman, "Tuning SAT Checkers for Bounded Model Checking (有界モデル検査用SATチェッカーのチューニング)," in Proceedings of International Conference on Computer-Aided Verification, 2000.
【非特許文献１４】
O. Shtrichman, "Pruning Techniques for the SAT-based bounded model checking (SATベース有界モデル検査のための枝取り)," in Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2001.
【非特許文献１５】
M. Ganai, L. Zhang, P. Ashar, and A. Gupta, "Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver (高性能SATソルバーを得るための回路ベースおよびCNFベース・アルゴリズムの強みの結合)," NEC USA, CCRL 2001-C079-4-5502-2, December 2001.
【非特許文献１６】
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, "Symbolic model checking using SAT procedures instead of BDDs (BDDの代わりにSATプロシージャーを使用した記号的モデル検査)," in Proceedings of the Design Automation Conference, 1999, pp. 317-320.
【非特許文献１７】
A. Gupta, Z. Yang, P. Ashar, and A. Gupta, "SAT-based Image Computation with Application in Reachability Analysis (到達可能性分析での応用例を持つSATベースのイメージ計算)," in Proceedings of Conference on Formal Methods in Computer-Aided Design, 2000, pp. 354-371.
【非特許文献１８】
A. Gupta, A. E. Casavant, P. Ashar, X. G. Liu, A. Mukaiyama, and K. Wakabayashi, "Property-specific testbench generation for guided simulation (誘導シミュレーションのための特性別テストベンチの生成)," in Proceedings of VLSI Design Conference, 2002.
【非特許文献１９】
J. Kim, J. Whittemore, J. P. M. Silva, and K. Sakallah, "Incremental Boolean Satisfiability and its application to delay fault testing (増分ブール充足可能性とその遅延故障テストへの応用)," in Proceedings of International Workshop on Logic Synthesis, 1999.
【非特許文献２０】
A. Kuehlmann and F. Krohm, "Equivalence Checking using Cuts and Heaps (カットとヒープを使用した等価検査)," in Proceedings of Design Automation Conference, 1997.
【非特許文献２１】
M. Ganai and A. Kuehlmann, "On-the-fly compression of logical circuits (論理回路のオンザフライ圧縮)," in Proceedings of International Workshop on Logic Synthesis, 2000.
【非特許文献２２】
A. Kuehlmann, M. Ganai, and V. Paruthi, "Circuit-based Boolean Reasoning (回路ベースのブール推論)," in Proceedings of Design Automation Conference, 2001.
【非特許文献２３】
P. Goel, "An implicit enumeration algorithm to generate tests for Combinational circuits (組み合わせ回路用テストを生成するための暗黙エニュメレーション・アルゴリズム)" IEEE Transactions on Computers, vol. C-30, pp. 215-222, 1981.
【非特許文献２４】
H. Fujiwara and T. Shimono, "On the Acceleration of Test Generation Algorithms (テスト生成アルゴリズムの加速)," IEEE Transactions on Computers, vol. C-32, pp. 265-272, 1983.
【非特許文献２５】
M. Schulz, E. Trischler, and T. Sarfert, "SOCRATES: A highly efficient ATPG System (SOCRATES: 高効率ATPGシステム)," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 7, pp. 126-137, 1988.
【非特許文献２６】
M. N. Velev, "Benchmark Suites. (ベンチマーク・スイート、http ://www.ece.cmu.edu/~mvelev)," October 2000.
【非特許文献２７】
A. Gupta, A. Gupta, Z. Yang, and P. Ashar, "Dynamic detection and removal of inactive clauses in SAT with application in image computation (イメージ計算に応用事例を持つ、SATにおける非活動文節の動的検出および除去)," in Proceedings of Design Automation Conference, 2001.
【非特許文献２８】
H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi, "Algorithms for approximate FSM traversal based on state space decomposition, 状態空間分割に基づく近似FSMトラバーサルのためのアルゴリズム"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15(12), pp. 1465-1478, 1996.
【非特許文献２９】
I.-H. Moon, J.-Y. Jang, G. D. Hachtel, F. Somenzi, C. Pixley, and J. Yuan, "Approximate reachability don't-cares for CTL model checking (CTLモデル検査のための近似到達可能性のドントケア)," in Proceedings of the International Conference on Computer-Aided Design. San Jose, 1998.
【非特許文献３０】
K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi, "Approximation and decomposition of Decision Diagrams (決定図の近似と分解)," in Proceedings of the Design Automation Conference. San Francisco, 1998, pp. 445-450.
【０００４】
２．  序文
ａ）  モデル検査
ハードウェア設計がますます複雑化するにつれ、コスト増大の原因となるエラーを回避できる効果的な検証方法へのニーズが高まっている。記号的モデル検査（非特許文献１、２参照）のような形式的検証手法の登場により、しらみ潰しの検査が可能になり、シミュレーションなどの従来手法に比較して、見つかりにくいバグも容易に検出できるようになった。しかし、これらの手法は、状態爆発問題が原因で実用使用においてはうまくスケーリングできないという難点があった。最近発表された代替手法では、有界モデル検査 (BMC: Bounded Model Checking)(非特許文献３参照)が使用されている。主に二分決定グラフ(BDD: Binary Decision Diagrams)(非特許文献４参照)の使用をベースとする記号的モデル検査とは異なり、BMCはブール充足可能性 (SAT: Satisfiability) 決定手順の使用をベースとする。そのためBMCでは、実用レベルではるかに大規模な設計を扱うことができ、特にバグが存在する場合に、その検出において高い効果を期待できる。
【０００５】
モデル検査では、ハードウェア設計は有限状態機械として表され、その仕様は時相論理で表現された特性で構成される。この仕様が充足されるかどうかを検査するため、設計の状態空間がしらみ潰しに探索される。仕様が充足されない場合は、典型的には、正当性特性の違反を実証する反証が検出される。有界モデル検査では、有界長kの反証(バグ)の検出に焦点が当てられる。これにより、無限パスと不動点演算の処理を回避できるほか、考慮の対象が有界長kのパスのみに絞り込まれるという利点が生まれる。具体的には、この問題は、長さkの反証が存在している場合にのみ真となる命題式に変換される。実用使用では、境界kを漸増させて最も短い反証を検出することができる。ただし、一定の境界まで反証が検出されないときの完全性を保証するため、これとは別に推論を行う必要がある（非特許文献３、５参照）。
【０００６】
【発明が解決しようとする課題】
３．  技術と関連研究の背景
この項では、関連研究の様々な態様を、背景とBMCの従来技術を踏まえて論じる。
【０００７】
仕様はLTL (Linear Temporal Logic: 線形時相論理) で表現される。LTLには、next time演算子X、eventuality演算子F、globally演算子G、until演算子Uの各時相演算子が含まれる。解説を簡素化するため、ここではタイプE fの式について考察する。ここで、Eは存在パス修飾子、fはパス修飾子を持たない時間式である。設計は、状態の有限集合S、初期状態の集合I、状態T間の遷移関係、原子命題を有する状態のラベリングLで構成される、標準Kripke構造M =(S, I, T, L)として記述される。Kripke構造M、LTL式f、境界kが与えられたとすると、BMCにおける変換タスクとは、すなわち、構造M内の式fに関して長さｋの証拠が存在するときにのみ充足可能な命題式<M, f>kを構築することとなる。
【０００８】
この状態集合は有限なので、状態はブール変数sの記号エンコードを使用して表され、長さkの有限シーケンスはシーケンスs0 ... skとして表される。
【０００９】
さらに、このシーケンスがM内で有効なパスであることを保証するために、第1の制約集合<M>kが使用される。
【数１】
0004000567.tif 000002
【００１０】
この式の最初の部分は「シーケンスにおける第1の状態は初期状態Iでなくてはならない」という制約を課し、この式の2番目の部分は「連続する状態の各ペアは遷移関係Tに準じた関係になければならない」という制約を課す。ここでは、この2番目の部分は順次設計のkステップにわたる展開に対応し、kの増大に伴ってSAT問題のサイズが増大することに注意する必要がある。
【００１１】
その次の制約集合では、M内のこの有効パスがLTL式fを充足することが保証される。また、図2(非特許文献３より)に示されるように、このパスが(k, l)ループかどうかによって、ケース分割が必要となることもある。状態kから状態lへのループのケースは、lLk =T(sk,sl)に変換できる。ループがないケースは、¬Lkに変換できる。ここで、
【数２】
0004000567.tif 000003
である。  [ｆ]0ｋはループなしケースにおける式fの変換を表し、ｌ[ｆ]0ｋは(k, l)ループのケース(詳細な定義については非特許文献３を参照)におけるfの変換を表す。最後に、問題全体の一括変換は以下によって得られる。
【数３】
0004000567.tif 000004
【００１２】
ここで、1番目の項は有効パスの要件を示し、2番目の項は、そのパスがケース分割された仕様式を充足することを示す。本論文の解説においては、この変換がモノリシックである(すなわち、与えられたkに対して式全体が生成される)ことに留意することが重要である。この式は、SATO(非特許文献９参照)、Chaff(非特許文献１０参照)などの標準的なSATソルバーによる充足可能性検査に付される。
【００１３】
実用使用では、長い証拠の探索は境界kを漸増させて実行される。これは、証拠が存在する場合にはきわめて有効である。しかし、証拠が存在しない場合には、その特性が偽であることを確定するために別の証明手法が必要となる。この場合は、有限状態機械の直径までのすべてのkを検査するので十分である(非特許文献３参照)。また、同様の状況において安全特性を証明するための方法として、ループなしパス、最短パスなどその他の制約の使用も提唱されている（非特許文献５、１１参照）。
【００１４】
BMCエンジンは、有界長の反証を検出することに加えて、帰納証明の実行にも使用できる(非特許文献１６参照)。深度kを増大させて実行される帰納と、ループなしパスに対する制限を組み合わせると、安全特性の完全な証明手法が得られる（非特許文献５、１１参照）。深度kの帰納は、以下の2ステップから成る。
【００１５】
(a)  基本ケース:その特性が、初期状態から始まる長さkの各パス上で有効であることを証明する。
【００１６】
(b)  帰納ステップ:その特性が、任意の状態から始まる長さkのパス上で有効であり、さらには、長さ(k+1)のパスの拡張上でも有効であることを証明する。
【００１７】
ループなしパスに限定することにより、「パス内に同一の状態がない」という追加の制約が課される。ここで、基本ケースでは初期状態制約が使用されるが、帰納ステップではこの制約は使用されないことに注意する必要がある。したがって、帰納ステップには到達不能な状態も含まれる可能性がある。実用使用では、追加の制約 (すなわち、特性自体よりも強力な帰納不変式)を使わずに帰納証明を完了することは不可能なこともある。この場合は、到達可能性の制約など、設計者に既知の回路制約を使用して帰納不変式を強化することができる。
【００１８】
上記の手法は、ゲートとフリップフロップが多数存在する回路上では演算能力が低下する。これらの手法は回路のサイズが大きくなるに従って急激に低速となり、メモリ消費量も増大する。
【００１９】
本発明は、従来技術に関連する短所を克服し、上記問題のいくつかを解決することを目指すものであり、線形時間論理で表された任意の時相特性を対象とした有界モデル検査の方法を提供することを目的とする。
【００２０】
【課題を解決するための手段】
本発明による有界モデル検査の方法は、Fはeventuality演算子、Gはglobally演算子、Uはuntil演算子、Xはnext-time演算子を表す時相演算子F(p)、G(p)、U(p, q)、X(p)に関連付けられた特性を、ブール充足可能性検査から成る特性検査スキーマに変換するステップから成る。特性全体は、F(p)、G(p)、U(p, q)、X(p)の各演算子に関する特性検査スキーマの反復呼び出しと、原子命題およびブール演算子の標準的な処理で構成されるカスタマイズされた方法で検査される。
【００２１】
ある特定の機能拡張では、次に検査する演算子に関して選択肢が存在する場合には、探索の難度により決定される優先順位に従って選択が行われる。
【００２２】
さらに具体的には、この探索の難度は、原子命題、X演算子、F演算子、U演算子、G演算子の順に高まると想定される。
【００２３】
他の特定の機能拡張では、特性検査スキーマのサブセットが、対応するブール充足可能性問題をサイズの小さい複数のブール充足可能性下位問題に分割するために、対応する有界モデル検査問題のk番目のインスタンスに対して分割を実行する。
【００２４】
さらに具体的には、この分割は演算子間にまたがって実行され、各演算子に対しては時間フレーム間と時間フレーム内の両方で実行される。
【００２５】
さらに具体的には、この分割は可能な場合は常に、漸増的に関連付けられるブール充足可能性下位問題に到達するように方向付けされる。
【００２６】
さらに具体的には、複数のブール充足可能性下位問題にまたがる学習が使用される。
【００２７】
さらに具体的には、複数の関連する下位問題にまたがる学習を行うために、ブール充足可能性アルゴリズムの漸増的な公式化が使用される。
【００２８】
他の特定の機能拡張では、定数の伝搬に基づく回路の単純化が使用される。
【００２９】
他の特定の機能拡張では、構造同形の検出に基づく回路の単純化が使用される。
【００３０】
他の特定の機能拡張では、ブール充足可能性検査問題が、回路ベースとCNFベースの充足可能性アルゴリズムの使用を結合したハイブリッドSATソルバーを使用して解決される。
【００３１】
他の特定の機能拡張では、F(p)の特性検査スキーマは、時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始するステップを備え、ここでi=0は初期状態に対応する。現在のパスのi番目の状態におけるpの充足可能性が検査される。充足可能な場合、探索は成功として終了される。充足不能な場合、pはi番目の状態においては常に偽であることが学習され、この学習された知識が制約データベースに追加される。探索は、iを所定の上限まで増大させながらそれまでのステップを繰り返し実行することで継続される。所定の上限に到達すると、探索は不確定のまま終了される。
【００３２】
他の特定の機能拡張では、完全性が検査される。
【００３３】
さらに具体的には、この完全性の検査は、i番目の状態を起点とする遷移がパス内の検査済みの状態を訪れないようにするための制約を追加するステップと、制約データベースの充足可能性を検査するステップとを備える。充足不能な場合、探索は失敗として終了される。充足不能でない場合、探索は継続される。これらのステップは、以前の状態がすべて検査されるまで繰り返される。
【００３４】
他の特定の機能拡張では、G(p)の特性検査スキーマは、時間フレームiにおいて所定の制約データベースを使用して所定の開始状態から探索を開始するステップを備え、ここでi=0は初期状態に対応する。pが現在のパスのi番目の状態において充足されることを保証するための制約がデータベースに追加され、充足可能性が検査される。充足不能な場合、探索は失敗として終了される。充足可能な場合、開始状態からi番目の状態までの間でj番目の状態が各々ループバック状態かどうか検査され、ループバック状態が検出されたら探索は成功として終了される。開始状態より前のj番目の状態が各々ループバック状態かどうか検査され、ループバック状態が検出されたら探索は成功として終了される。探索は、iを所定の上限まで増大させながら、これらのステップを繰り返し実行することで継続される。所定の上限に到達した時点で、探索は不確定のまま終了される。
【００３５】
前述の方法の機能拡張には上記に加えてさらに数種類があることは、請求項と発明の詳細な説明から明らかとなるであろう。
【００３６】
本明細書における発明の他の態様は、線形時間時相論理で表現された安全性特性の帰納証明の方法であって、kインスタンスの基本ケースを、与えられた特性の否定に関して検査するステップ、kインスタンスの帰納ステップを、与えられた特性に対応するモニター述語に関して検査するステップ、k=0から開始し、任意に指定された上限までそれを漸増させるステップを備え、基本ケースの検査はさらに、否定された特性を、Fがeventuality演算子、Xがnext-time演算子を表す時相演算子F(p)およびX(p)と関連づけられたブール充足可能性検査から成る特性検査スキーマに変換するステップを備える。否定された特性の証拠を検出するために、F(p)、X(p)に関する特性検査スキーマの反復呼び出しと、原子命題およびブール演算子の標準的な処理で構成される探索が初期状態を起点として実行される。証拠が検出されないことが証明された場合は、証明全体が成功として終了される。k時間フレーム内に証拠が検出された場合は、証明全体が失敗として終了され、結果が不確定の場合は、以下の特性検査スキーマから成る帰納ステップの検査が継続される。すなわち、モニター述語が任意状態からk時間フレームにわたって有効で、かつk+1番目の時間フレーム内では有効ではない状況を保証するための制約が追加される。充足不能な場合、探索は成功として終了される。充足不能でない場合、探索は継続される。この探索は、kを所定の上限まで漸増させながら基本ケースと帰納ステップを繰り返し実行することで継続される。kが指定された上限に到達した場合は、証明は不確定となる。
【００３７】
本明細書における発明の他の態様は、回路を検証するための検証エンジンであって、このエンジンは線形時間論理で表された任意の時相特性の有界モデル検査を実行する機能を有する。このエンジンは、特性トランスレーターと特性チェッカーを備える。特性トランスレーターは、Fはeventuality演算子、Gはglobally演算子、Uはuntil演算子、Xはnext-time演算子を表す時相演算子F(p)、G(p)、U(p, q)、X(p)に関連付けられた特性を、ブール充足可能性検査から成る特性検査スキーマに変換するように適応される。特性チェッカーは、特性全体が、F(p)、G(p)、U(p, q)、X(p)の各演算子に関する特性検査スキーマの反復呼び出しと、原子命題およびブール演算子の標準的な処理で構成されるカスタマイズされた方法で検査されるように適応される。
【００３８】
本明細書における発明の他の態様は、回路のための帰納証明エンジンであって、このエンジンは線形時間論理の時相特性における安全性特性を証明する機能を有する。このエンジンは、与えられた特性が否定された場合に、kインスタンスの基本ケースを検査するように適応された基本ケース・チェッカーを備える。与えられた特性に対応するモニター述語においてkインスタンスの帰納ステップを検査するように適応された、帰納ステップ・チェッカーが提供される。否定された特性を、Fがeventuality演算子、Xがnext-time演算子を表す時相演算子F(p)およびX(p)と関連づけられたブール充足可能性検査から成る特性検査スキーマに変換するように適応された特性トランスレーターが提供され、さらに、否定された特性の証拠を探索するように適応されたサーチャーが提供される。
【００３９】
本明細書における発明のさらに他の態様は、回路のための帰納証明エンジンであって、このエンジンは線形時間論理の時相特性における安全性特性を証明する機能を有する。このエンジンは、与えられた特性が否定された場合に、kインスタンスの基本ケースを検査するように適応された基本ケース・チェッカーを備える。与えられた特性に対応するモニター述語においてkインスタンスの帰納ステップを検査するように適応された、帰納ステップ・チェッカーが提供される。否定された特性を、Fがeventuality演算子、Xがnext-time演算子を表す時相演算子F(p)およびX(p)と関連づけられたブール充足可能性検査から成る特性検査スキーマに変換するように適応された、特性トランスレーターが提供される。否定された特性の証拠を探索するように適応された、サーチャーが提供される。
【００４０】
上記の様々な特定の機能拡張に関してさらに具体的な機能拡張が提供されることは、請求項と詳細な説明から明らかとなるであろう。
【００４１】
【発明の実施の形態】
（カスタマイズ特性変換）
この節では、本発明の一部を成すカスタマイズ変換について説明する。この変換スキーマは、モノリシックSAT式を生成するのではなく、可能な場合は早期に終了することを前提に、有界な論理積/論理和に対して遅延指標付けを行うことにより、式を漸増的に構築するものと考えることができる。学習と分割を使用して複数の単純なSAT下位問題を生成するステップを採用した、漸増的な公式化は、広く使用されている。
【００４２】
場合によっては、ループなしパスのスケルトン(パス上のすべての状態が特異な対を成す)にのみ焦点を当てることを目的として、追加の制約が使用されることもある。これらの制約は、安全特性を対象とする場合には、証明の完全性を保証するために使用されていた（非特許文献５、１１参照）。変換スキーマでは、これらの制約は、ループを有する証拠を必要とする活性特性を対象に使用される。一例として、特性G(p)について考察する。各状態においてpが真であり、パス上の最後の状態を除くすべての状態が特異な場合には、ループなしパスのスケルトンに焦点が当てられる。最後の状態は、「ループバック状態」と呼ばれるパス上のl番目の状態と同一であり、これによって(k,l)ループを形成する。
【００４３】
G(p)の証拠はすべて、境界kを増大させることによってシステマティックに検出される、ループなしスケルトンを持つことは明白である。kが与えられた場合、ループバック状態の探索は初期状態かk番目の状態のどちらからでも開始できる。ループバック状態が検出された場合、特性は真である。一方、すべてのループなしスケルトンを検査してもループバック状態が検出されなかった場合には、特性は偽である。G(p)特性の一括変換もまた、kを増大させて(k,l)ループを考慮することはすでに述べた。ただし、この変換では、「パス・スケルトンがループなしでなければならない」という制約は課せられない。ループなしパスのスケルトンには、設計の順次直径ほどに厳格な境界はないが、SATソルバーの範囲内での証明機能が提供される。これに対し、順次直径に関する推論には、QBF(Quantified Boolean Logic: 定量化ブール論理)ソルバーが必要とされる。
【００４４】
詳細を説明する前に、本発明の変換スキーマにより生成されるSAT下位問題を定義する数種類の制約を分類しておくと有益である。これらの制約とは、以下のとおりである。
−    回路制約
−    特性副次式による制約
−    充足不能なSATインスタンスから学習された制約
−    ループなしパスのスケルトンのみを考慮するためのループ検査制約
【００４５】
一括変換では、最初の2種類の制約 (すなわち、回路制約と特性制約)しか使用されないことに注意する必要がある。学習された制約(非特許文献１２参照)とループ検査制約(非特許文献５参照)の使用は、各々従来から知られていたが、単純な安全特性を検証する状況での使用に限られている。また、典型的にはSATソルバーそのものによって生成される、他の1種類の制約(矛盾する文節から生じる制約)があることにも注意する必要がある。本発明の変換スキームでは、漸増的な公式化を使用することにより、こうした制約も容易に共有することができる。
【００４６】
本発明のカスタマイズ特性変換における分割、学習、およびインクリメンタル(漸増的)の各態様への注目を促すため、一般的なLTL特性を処理するための擬似コードの非限定的な例をここに示す。ここで、pおよびqは、命題式とX演算子との任意のブール結合を示し、各々は回路のグラフ表現における1つのノードと関連付けられる。is_sat(C)は、SATソルバーへの呼び出しを示し、SATソルバーは、ブール式Cが充足可能である場合にのみ真を返す。L_ijは、i番目からj番目までの時間フレームの間にループ遷移がある(すなわち、L_ij=T(si,sj))ことを示す。Nは、ユーザーの制御下にある展開の最大深度を示す。説明を簡素化するため、これらの変換では、SAT下位問題に常に追加される回路制約は示していない。
【００４７】
一例として、F(p)の変換について考慮する。指標iにおける外側forループ(第13行)は、BMCの境界kをユーザー指定の上限Nまで漸増することに相当する。このループは、特性データベースCを構築する(第8行)。このデータベースは、初期には真である。各iについて、(C & p_i)の充足可能性(すなわち、現在の時間フレームにおいてpが真である間に、現在の文節データベースが充足可能かどうか)が検査される(第14行)。充足可能な場合、F(p)の証拠が検出され、真が返される。充足可能でない場合は、「時間フレームiにおいてpは常に偽である」という事実が学習され、文節データベースC(第15行)に追加される。指標jにおける内側forループ(第16〜21行)は任意であり、証明を実行する際に選択的に使用される。このループは、パス上の現在の状態siから任意の以前の状態sjまでの間にループがないことを保証するために、対を成す制約をCに追加する。続いて、C上でSAT検査が実行される(第21行)。Cが充足不能な場合は、どの時間フレームにおいても、すべてのループなしパスを検査した結果pが真であることが検出されなかったことを意味するので、その特性は偽であると結論付けることができる。これにより、F(p)に関する完全性の引数が得られる。一方、Cが充足可能な場合は、現在のパスをループなしに保ちながら拡張する方法があるので、ループ指標iを漸増させながらさらに繰り返しが実行される。さらなる最適化の方策として、第19行のコメント行に示されるように、対を成すループ制約が漸増的に追加される。これにより、すべての制約を追加することなく早期に終了できる可能性が生まれる。
【００４８】
ループ付きの証拠を必要とする特性G(p)に関して、ループ制約がどのように処理されるかを知ることも有益である。ここでも、iにおける外側forループは、BMCの境界kを漸増させることに相当する。このプロシージャーは、(C & p_i)の充足可能性を検査することから開始される。充足不能な場合は、現在の時間フレームiにおいてpを充足する方法はないので、特性G(p)は偽である。充足可能な場合は、このパス上の現在の状態siから以前の状態sjまでの間にループ遷移があるかどうか検査するための制約が追加される。これは漸増的に検査されるので(第35行)、該当する最初のループが検出された時点でプロシージャーを終了できる。該当するループが検出されない場合は、この事実が学習され、文節データベースCに追加される(第36行)。すべてのループ制約が追加されたら、完全性検査が実行され(第38行)、これによって、特性が偽であると結論付けるか、あるいは次の繰り返しのためにループなしパスのスケルトンを拡張することが可能になる。以下に、一般的なLTL特性に関する疑似コードを示す。
【００４９】
1 /* N = Max depth
2  f_i = property node at ith time-frame
3  L_ij = Loop constraint between the ith
4         and jth time frames
5  &(l) = cnf conjunction(disjunction) */
6
7  F(p){
8   F(1,p,0)
9  }
10
11  F(IC,p,start){
12   C = IC ;
13   for( i = start ; i < N ; i++){
14    if( is_sat(C & p_i)) return true ;
15    C = C & !p_i ;
16    for( j = i ; j >= start ; j--){ //optional 16-21
17     C = C & !L_ij ;
18     // optional 19
19     // if( !is_sat(C)) return false;
20    }
21    if ( !is_sat(C)) return false;
22   }
23  }
24
25  G(p){
30    C = 1;
31    for ( i = 0 ; i < N ; i++){
32     C = C & p_i ;
33     if ( !is_sat(C)) return false ;
34     for ( j = i ; j >= 0 ; j-- ) {
35     if ( is_sat( C & L_ij )) return true ;
36     C = C & !L_ij ;
37    }
38    if ( !is_sat(C)) return false ;
39   }
40  }
41
42  G( IC,p,start){
43    C = IC ; t = 0 ; C'' = 1 ;
44    for ( i = start ; i < N ; i++){
45     C = C & p_i ;
46     if ( !is_sat(C)) return false ;
47     for ( j = i ; j >= start ; j-- ) {
48     if ( is_sat( C & L_ij )) return true ;
49     C = C & !L_ij ;
50    }
51    C' = C & C'' ;
52    for ( j = start -1 ; j >= t ; j--)
53     if ( !is_sat( C' & p_j )) {
54      t = j + 1 ; C'' = C'' & !p_j ; break ; }
55     C' = C' & p_j ;
56     if ( is_sat( C' & L_ij ) return true
57     C' = C' & !L_ij ;
58    }
59    for ( l = start -1 ; l >= t ; l--)
60     C = C & !L_il ;
61     if ( !is_sat(C)) return false ;
62    }
63  }
64
65  F( p or F(q) ) {
66    C = 1 ;
67    for ( i = 0 ; i < N ; i++){
68     if ( is_sat( C & p_i ) return true ;
69     C = C & !p_i ;
70
71     if ( F(C,q,i)) return true ;
72
73     for ( j = i ; j >= 0 ; j--) {
74      C = C & !L_ij ;
75     // if ( !is_sat(C)) return false ;
76     }
77    // reached the bound
78    if ( !is_sat(C)) return false ;
79    }
80  }
81
82  F( p or F(q) ) {
83    C = 1 ;
84    for ( i = 0 ; i < N ; i++){
85     if ( !is_sat( C & p_i ) {
86      C = C & !p_i ;
87     } else {
88     if ( F(C & q,i,q,i )) return true ;
89     }
90     for ( j = i ; j >= 0 ; j--) {
91      C = C & !L_ij ;
92     // if ( !is_sat(C)) return false ;
93     }
94    // reached the bound
95    if ( !is_sat(C)) return false ;
96   }
97  }
98
99  F( p or G(q) ) {
100   C = 1 ;
101   for ( i = 0 ; i < N ; i++){
102    if ( is_sat( C & p_i ) return false ;
103     C = C & !p_i ;
104
105    if ( G(C,q,i )) return true ;
106
107    for ( j = i ; j >= 0 ; j--) {
108     C = C & !L_ij ;
109    // if ( !is_sat(C)) return false ;
110    }
111   // reached the bound
112   if ( !is_sat(C)) return false ;
113  }
114 }
115
116  F( p or G(q) ) {
117    C = 1 ;
118    for ( i = 0 ; i < N ; i++){
119     if ( !is_sat( C & p_i ) {
120      C = C & !p_i ;
121     } else {
122     if ( G(C & p_i,q,i )) return true ;
123     }
124     for ( j = i ; j >= 0 ; j--) {
125      C = C & !L_ij ;
126     // if ( !is_sat(C)) return false ;
127     }
128    // reached the bound
129    if ( !is_sat(C)) return false ;
130   }
131  }
132
133  U( IC,q,r,start ) {
134    C = IC ;
135    for ( i = start ; i < N ; i++){
136     if ( is_sat( C & r_i )) return true ;
137     C = C & !r_i & q ;
138     if ( !is_sat(C)) return false ;
139     for ( j = i ; j >= 0 ; j--) {
140      C = C & !L_ij ;
141     // if ( !is_sat(C)) return false ;
142     }
143    // reached the bound
144    if ( !is_sat(C)) return false ;
145   }
146  }
147
148  F( p or U(q,r) ) {
149   C = 1 ;
150   for ( i = 0 ; i < N ; i++){
151     if ( !is_sat( C & p_i ) {
152     C = C & !p_i ;
153    } else {
154     if ( U(C & p_i,q,r,i )) return true ;
155    }
156    for ( j = i ; j >= 0 ; j--) {
157     C = C & !L_ij ;
158     // if ( !is_sat(C)) return false ;
159    }
160     // reached the bound
161     if ( !is_sat(C)) return false ;
162    }
163  }
165  F( p or U(q,r) ) {
166   C = 1 ;
167   for ( i = 0 ; i < N ; i++){
168     if ( is_sat( C & p_i )) return true ;
169     C = C & !p_i ;
170     if ( U(C & q,r,i )) return true ;
171    for ( j = i ; j >= 0 ; j--) {
172     C = C & !L_ij ;
173     // if ( !is_sat(C)) return false ;
174    }
175    // reached the bound
176    if ( !is_sat(C)) return false ;
177   }
178  }
【００５０】
F(p and G(q))のように特性をネストすると、構成要素のF副次式とG副次式に分割することができ、そのパーティション全体にまたがる学習が可能になる。ここではF(p and G(q))を対象に、非限定アルゴリズムの例を示す。iにおける外側ループ(第118行)は、BMCの境界kを漸増させる。第1のSAT下位問題は、(C & p_i)を検査する。偽の場合は、then !p_iが学習され、Cに追加される(第120行)。このとき、現在のパスをループなしのまま拡張できなければ(第124〜128行)、特性が偽であることが証明される。一方、(C & p_i)が真であれば、アルゴリズムは時間フレームiからG(q)の検査を継続する。
【００５１】
この検査は、関数呼び出しG(C & p_i, q, i)によって実行される。G(C & p_i、q、i)は、siを起点としてパスの探索を行い、各状態でqが真であることが確認されると、パスが以前の状態にループバックする。ここで、G(C & p_i, q, i)は、時間フレームiよりも短い時間フレームjにおいてもループバック状態を検査する(第52〜58行)ことに注意する必要がある。この場合、G(C & p_i, q, i)はさらにsiまで、各状態においてqが真であることを追加して証明しなければならない。任意の時間フレームjにおいて充足不能なことが判明した場合は、!q_jが学習される(第54行)。ここで、この特性を分析する過程で多数のSAT呼び出しが行われるという事実と、データベース(C, C', C")が連続する呼び出しの間でどのように漸増されるかについて注目する必要がある。SAT呼び出しで充足不能であることが判明するごとに、新たな制約を学習する機会が得られる。こうした特性の分析は、一括変換を使用するよりも、本発明の手法を使用した方がはるかに高速になる。
【００５２】
擬似コードに示される残りの特性と、有益とみなされるその他のLTL特性は、同様の方法で処理される。この手法の特徴は、可能な場合は常に、分割、学習、および漸増的SAT検査が実行されることにある。また、証明の完全性を確保するため、ループ検査の制約を任意に追加することもできる。
【００５３】
１．  正当性特性の拡張範囲
候補となるすべての正当性特性がLTLで表現できるわけではない。例えば、生産設計の1つにおいて、仕様AG(p ->EX q)を使用して、任意の状態を起点とする1つの遷移の実現可能性を検査する必要が生じたことが報告されている。これはLTL特性として表現することはできないが、SATベースのBMCフレームワーク内でそれを処理することは可能である。
【００５４】
以下に、有界数のEX演算子(「EX:n」として示す)を使用した、さらに一般的なケースを疑似コードで示す。非限定的な例として、第1の変換について考慮する(第2の変換は、第1の変換と同様である)。第1の変換は、否定された特性EF(p & !(EX q))の証拠を探索するので、前述の特性の反証を得るために使用できる。ここで注目すべきは、!(EX q)がEX !qと同一となる可能性のあるLTLセマンティクスはここでは使用されないことである。その代わりに、!(EX q)= AX !qであるCTLセマンティクスが使用される。順次設計をさらにnステップにわたって前方に展開し、X:n qに対応する回路ノードを作成することにより(「q_{n+1}」として示される)、n個のX演算子を処理することは容易である。以下に、一般的な非LTL特性に関する疑似コードを示す。
【００５５】
1 EF(p and ! EX:n q) {
2  C = 1; C' = 0;
3  for (i=0;i<N;i++) {
4   if (!is_sat(C & p_i)) {
5     C = C & !p_i;
6   } else {
7    if (!is_sat(C & p_i & q_{n+i}))
8      return true;
9    else {
10     // exclude states with p & q_{n+i}
11     while(1) {
12      C' = C'|get_sat_state_cube(i);
13      if (!is_sat(C & !C' & p_i))
14        break; // no more p_i states
15      if (!is_sat(C & !C' & p_i & q_{n+i}))
16        return true; // found witness
17     } // end of while loop
18    }
19   }
20   for (j=i;j>=0;j--) {
21     C=C & !L_ij;
22     // if (!is_sat(C)) return false;
23   }
24   if (!is_sat(C)) return false;
25  }
26 }
27
28 ef(p or !EX:n q){
29  C=1;
30  for (i=0;i<N;i++){
31   if (is_sat(C & p_i)) return true;
32   else {
33     C=C & !p_i;
34     if (!is_sat(C & q_{n+i})) return else;
35      else {
36      // excluse states with q_{n+i}
37     while(1) {
38      C'=C'|get_sat_state_cube(i);
39      if (!is_sat(C & !C')
40        break; // no more states
41      if (!is_sat(C & !C' & q_{n+i}))
42        return true; // found witness
43     } // end of while loop
44    }
45   }
46   for (j=i;j>=0;j--) {
47     C=C & !L_ij;
48     // if (!is_sat(C)) return false;
49   }
50   if (!is_sat(C)) return false;
51  }
52 }
【００５６】
このプロシージャーは、p_iが充足可能かどうか検査する(第4行)。充足可能でない場合は、!p_i(第5行)が学習され、iが漸増される。充足可能な場合、当該プロシージャーは、当該状態がq_{n+i}も充足するかどうか検査する(第7行)。q_{n+i}も同時に充足する方法がない場合は、証拠が検出されたとみなされる(第8行)。充足可能な場合は、p_iとq_{n+i}の両方を充足する状態が考慮対象から除外される。これはwhileループによって行われる(第11〜17行)。除外集合C'(初期化により空にされる)は、ループの各反復において、充足する状態キューブ(すなわち、p_iとq_{n+i}の両方を充足する状態)を追加することによって更新される(第16行)。次に、C'以外にp_iを充足する状態があるかどうかが検査される(第13行)。該当する状態が存在しない場合には、当該プロシージャーはwhileループから分離し、iを漸増させながらさらに長い証拠を探索しなければならない(第14行)。一方、このような状態が存在する場合は、その状態がq_{n+i}も併せて充足するかどうかが検査される(第15行)。充足しない場合は、証拠が検出されたとみなされる。充足する場合は、whileループが実行され、これらの状態が除外される。完全性については、当該プロシージャーをループなしのスケルトンのみに絞り込んで実行するかどうかを選択できる(第20〜24行)。
【００５７】
ここで、除外集合内の(p_i & q_{n+i})の解を漸増的に列挙するために、SATソルバーが使用されていることに注目する必要がある。SATとBDDの組み合わせは、イメージ集合の計算にも使用できる(非特許文献１７参照)ほか、SATベースのBMCフレームワーク内では制約として使用することができる。
【００５８】
我々が遭遇したもう1つの有用なCTL特性は、AG(p ->EF q)である。これはリセット可能性、デッドロックの不在などの検査に使用できる。SATベースのBMCフレームワーク内では、改変が行われることと、ネストされたEF演算子が不動点の性質を有することを理由として、この特性を検査することは不可能である。ただし、実用使用では、qが真の場合において対象となる状態の最終的な到達可能性を検査する際には、設計者は常に境界を意識しているものである。このようなケースでは、nが漸増されるEX:n演算子は、EF演算子の有界近似としての役割を果たす。
【００５９】
実用使用では、正当性特性の範囲を拡張して、CTLのすべてのモダリティを含めることができる。ここで注意を要するのは、改変にいかに対処するかという問題と、(証拠パスではなく)証拠グラフをいかにして継続的に追跡するかという問題である。概してこれには、QBFソルバーか、SATとBDDとの組み合わせを使用することが必要とされる。
【００６０】
２．  漸増的SAT手法
上述したように、BMCには、境界kを漸増させながら、問題に対応する一連のSATインスタンスを解決する作業が伴う。複数のSATインスタンスが各々の文節集合の間に空でない交差部分を有する場合には、これらのインスタンスの間で対立文節を共有でき、この共有によりSATの解決時間が全体的に短縮できることが、数人の研究者（非特許文献１３、１９参照）によって観察されている。特に、BMC問題のkインスタンスとk+1インスタンスは遷移関係のk回の展開を共有するため、回路制約の重複が多く発生する。問題のkインスタンスの検査中に演繹された制約を再使用する制約共有手法（非特許文献１３、１４参照）は、この事実を利用したものであり、これにより全体的な検証時間が短縮されるという効果が得られている。
【００６１】
本発明で考察する実施例のBMC実装では、共有は、遷移関係の展開に伴って回路制約の間で発生するだけでなく、特性の変換から生じる制約の間でも発生する。さらに、制約を漸増的に追加する本発明の変換スキーマでは、境界kを漸増させたときに複数のSAT問題が生成され、分割が使用されたときには単一のkインスタンス内でさえも複数のSAT問題が生成される(カスタマイズ特性変換の記載を参照)。複数のSATインスタンス間で制約を共有することに重点を置くことにより、漸増的SAT手法によって全体的な検証時間が短縮される可能性が生まれる。
【００６２】
SATソルバーの基本的な制約共有手法は、以下のように実行される(非特許文献１４参照)。2つのSATインスタンスをS_1およびS_2とすると、共通する文節の集合Y_0のみから演繹された対立文節(すなわち、S_1とS_2の両方に存在する文節)が識別される。識別は、Y_0文節の最初のマーキングに基づいて行われる。続いて、コンフリクト分析によって生成された各々の対立文節を対象にマーキングを実行する。1つの対立文節において、対立につながるすべての文節がマーキングされた場合は、その対立文節もマーキングされる。
【００６３】
本実施例の実装では、各文節は「gflag」と呼ばれるビット・ベクトル・フィールドを有する。gflagの各ビットは、その文節がそのビット位置に対応するグループに属するかどうかを示す。さらに、各文節は、「制約文節」、「回路文節」、「対立文節」という3つのタイプに分類される。1つの制約文節は、最大1つのグループに属する。回路文節は、どのグループにも属さない。コンフリクト分析時に追加された対立文節は、1つのグループに属し、かつ対立につながる文節が存在する場合に、そのグループのメンバーとなる。回路文節のみから演繹された対立文節(初期状態制約を含む)は、必ずしも複製できるとは限らないが、再使用は常に可能である。
【００６４】
ここで、EF(p)特性の証明に漸増的SAT手法を使用した簡単な例を示す。i番目の時間フレームにおいて、制約文節(p_i=1)が新規グループgidに追加される。(前述したように、p_iは、i番目の時間フレームにおける特性ノードpである)。結果がUNSATになると、この文節グループgidは、以降の時間フレームで再使用されないので削除される。この削除に伴って、グループgidのすべての対立文節と制約文節が除去される。ただし、回路文節のみから演繹された対立文節はそのまま保持される。これらの回路文節は、時間フレーム間で共有することができる。さらに、結果がUNSATとなったため、グローバル学習を使用して、その文節(p_i=0)を文節グループroot_gidに追加する。グローバル学習されたこれらの文節から演繹された対立文節もまた、以降の時間フレームで再使用できる。以下に示すのは、漸増的SAT手法の使用法を示す疑似コードである。
【００６５】
0004000567.tif 000005
【００６６】
他の特性の変換においても、対立文節と学習された制約文節に対して漸増的SAT手法を使用するために、同様の変更が行われる。
【００６７】
３．  回路の単純化
本発明で考察するBMC実装の実施例においては、前処理段階と、設計の遷移関係を展開する際の特性検査の段階で、回路単純化手法が使用される。これは、生成されるSAT問題を単純化して、全体的な検証時間を短縮することを目的とする。さらに、回路単純化手法は、CNFベースのSAT決定プロシージャー内に定数を伝搬する方法に比較して、定数の処理を効率的に行えることが確認されている。こうした定数は、フリップフロップ上の定数値を伴う初期状態制約と環境的制約、および特性検査時に追加された学習済み定数制約が原因で発生する。
【００６８】
回路の単純化は、非標準形の2入力AND/INVERTERグラフ表現(非特許文献２０参照)を使用し、この種のグラフ表現に対してオンザフライ式のリダクション・アルゴリズム（非特許文献２１、２２参照）を実行することによって実現される。このグラフは、設計と、複数の時間フレームにまたがる記号的計算において算出されるブール関数の両方を表現するために使用される。この方法の不利な点は、標準形のBDDとは異なり、AND/INVERTERグラフは非標準形であることである。この方法の有利な点は、このグラフはBDDに比較して、サイズが特定の関数や変数の順序の影響をはるかに受けにくく、簡潔なことである。
【００６９】
オンザフライ式リダクション・アルゴリズムは、AND/INVERTERグラフを表現するための効率的な関数ハッシング・スキームをベースとする。ハッシュ・テーブルは、BDDと同様に、構築時に構造的な冗長性を除去するために使用される。さらに、ローカルの4入力副構造をすべて標準形の表現に変換する構造的な２階層ルックアップ・スキームが適用され、ローカルの冗長性が効果的に除去される。ローカルの２階層ルックアップが適用されない場合は、単純書き換え方式によって、回路グラフがさらに縮小される(詳細については非特許文献２２を参照)。具体的には、これは、多数の同形の副構造を識別し、これらの副構造を同一のサブグラフにマッピングすることによって、グラフを大幅に圧縮する方式である。直感的に表現するならば、この単純化グラフによりSATソルバーの探索空間が縮小され、ひいてはブール推論の効率が高まる。有界到達可能性分析への応用(非特許文献１２参照)からも明らかなように、こうした単純化によりSATにもたらされる計算上の優位性はきわめて顕著である。
【００７０】
４．  ハイブリッドSATソルバー
本発明におけるBMCエンジンの実施例では、ハイブリッドSATソルバーが使用されている。このハイブリッドSATソルバーは、元来の回路形式の論理式と、CNFにおける学習された対立文節とをそれぞれ処理する一方で、決定変数の選択、BCP、およびバックトラッキングにおいて革新的な最新鋭機能を採用している。ここでは特に、回路ベースの方式とCNFベースの方式の主要ステップにおける重要な違いと、ハイブリッド方式とすることで両方式からどのような利点が実現されるかについて説明する。
【００７１】
ａ）  回路ベースBCPの最新技術の現状
SATソルバーの一部を成すBCPは、多数のインスタンスにおいて総実行時間の約80%を占めるとされる。これは、BCPをどんな形であれ改良できれば、SATソルバーの全体的なパフォーマンスが大幅に向上することを意味する。
【００７２】
従来の回路をベースとするブール推論実装（非特許文献２２から２５参照）は、INVERTERを別個の頂点またはゲート入力上の属性として備えた、ANDおよびORのゲート頂点をベースとする表現を使用する。ANDおよびORゲートにまたがって定数を伝搬する方法はよく知られているが、速度は実装によって大きく異なる傾向がある。一例として非特許文献２２を取り上げると、この技術は含意の伝搬を高速化する手段としてルックアップ・テーブルを使用している。このルックアップ・テーブルは、頂点の入力と出力の現在値に基づいて、暗黙値をカプセル化するゲートの次の「状態」と、その頂点に対して採るべき次の処置を決定する。図3に示す非特許文献２２の総称頂点タイプ用のアルゴリズムimplyは、回路グラフ上で繰り返し実行される。
【００７３】
このアルゴリズムは、各頂点について、新しい暗黙値と以降の処理の方向を決定する。例として、図4(出典は非特許文献２２)に、2入力ANDゲートの含意ルックアップ・テーブルに含まれるいくつかのケースを示す。ブール論理の場合、justification_queueにおいて新たなケース分割をスケジュールする必要があるのは、1つのケース(AND頂点の出力における論理0)だけである。他のケースはすべて、対立を発生させるか(この場合、アルゴリズムはバックトラッキングのために戻る)、さらなる含意を発生させるか、justification_queueの次の要素を処理するための戻りを発生させるかのいずれかである。この含意アルゴリズムは、オーバーヘッドが少ないため非常に効率的である。目安として示すと、256 MBのメモリを搭載した750 MHzのIntel PIIIでは、毎秒100万含意以上を実行できる。
【００７４】
１．  CNFベースBCPとの比較
Chaff(非特許文献１０参照)に示されるCNFベースBCPでは、2リテラル監視と遅延更新によって効率化が図られている。この方式は、サイズの大きい文節が不必要に走査される状況を回避できるため、文節が大きい場合に際だって有利である。また、この方式では、オーバーヘッドの削減を狙って、充足された文節の追跡は行われない。ただし、充足された文節を訪れることにより必然的に生じるコストまでは解消されない。具体的には、文節が監視対象ではないリテラルに割り当てられたことにより充足された場合でも、監視対象のリテラルへのポインターは更新される。これに加えて、ゲートを文節に変換するプロセスに組み込まれる固有のオーバーヘッドもある。回路ベースの方式では1つのゲートはモノリシックなエンティティであるのに対し、CNFベースの方式では、1つの2入力ゲートが3個の文節に変換される。そのため、回路方式では、1ゲートに存在する1含意について図4のテーブルを1回探索するだけでよいが、CNF方式では、複数の文節を処理する必要がある。
【００７５】
回路ゲートから生じる文節は概して短く、これらの文節に関しては、上記の相違点がBCP時間にかなり大きな違いをもたらす。次項に示すように、ゲート表現を対象とするBCPは、Chaffのような最新鋭のCNFベース・ソルバーのBCPに比較して、一貫してはるかに高速である。
【００７６】
ｂ）  対立ベースの学習の効果を活用するハイブリッド方式
一方、対立ベースの学習済み文節のようにサイズの大きい文節の場合は、回路ベースのBCPにゲート・ツリーとして付加すると、学習済み構造の規模を過剰に増大させる恐れがある。学習済み構造のサイズを過剰に増大させるゲート・ツリーを付加することは、回路サイズの大幅な増大につながる。これはさらに、含意数を増大させ、ひいては回路構造にBCPを実行したことによる利得を相殺する結果となる。サイズの大きい文節の場合は、これらをモノリシックな文節として維持し、CNFベースの2リテラル監視と遅延更新の利点を活用して処理した方が効率的である。
【００７７】
次に、上記の観察を踏まえて、ハイブリッド方式について考察する。このハイブリッド方式とは、均質ゲートのデータ構造を使用して回路ベースの論理表現を維持する一方で、状況に応じて、学習された文節をCNFとして維持し、別個に処理する方式である。
【００７８】
ｃ）  BCPの結果
表1(図5)に示す時間は、256 MBのメモリを搭載した750 MHzのIntel PIII上で100万含意の処理に要した秒単位のBCP時間である。サンプルとしては、大規模な工業用回路にBMCを適用して導出したサイズの大きい論理式を使用した。「ハイブリッド」と「Chaff」の欄に示した時間は、ハイブリッド方式とCNF方式を完全に同一の論理式を対象に実行した結果である。BCP時間には、SATプロセス中に付加された学習済み文節のBCPに要した時間と、最初のゲート文節のBCPに要した時間が含まれる。1次入力とゲートの数で表した式のサイズは、「1次入力」と「ゲート」の欄に示されている。「CH」の欄は、CNFのBCP時間とハイブリッドのBCP時間との対比を比率として示したものである。この表から、サイズの大きい式においては、ハイブリッド方式はChaffのCNFベース方式に比較して、一貫して高速である。
【００７９】
学習済み文節のBCPで達成されるオーバーヘッドの削減を実証するため、100万含意当たりのBCP時間を、同じ式に含まれるゲート文節のみを対象とした回路ベース方式との対比として示した。これは、「構造」欄に示している。「CS(HS)」欄は、「Chaff(ハイブリッド)」の時間と「構造」の時間との対比を比率として示したものである。これらの欄(「CS」および「HS」)により、ゲート文節のみを対象とした場合のBCP時間と、ゲート文節と学習済み文節を対象とした場合のBCP時間とを比較することが可能になる。この比較から、サイズの大きい学習済み文節がBCP時間のオーバーヘッドを大幅に増加させているのは明らかである。
【００８０】
ｄ）  ハイブリッドSATソルバーの総合的な利点
これまでBCPが高速であることを実証してきたが、これだけではハイブリッドSATソルバーの利点を語り尽くしたとは言えない。そのためには、ハイブリッド方式によってSATプロセス全体が高速になることを実証する必要がある。ハイブリッド方式を使用すると、純粋なCNF方式では使用できない多数の新たな回路ベース・ヒューリスティックと利点を活用する道が開かれる。この項では、ハイブリッド方式によりもたらされる利点について考察する。この比較のため、表2(図6)にSAT実行時間を示す。ここに示す時間は、256 MBのメモリを搭載した750 MHzのIntel PIII上での実行時間である。論理式は、3個の大規模な工業用回路(バス、アービター、コントローラー)と、非特許文献２６に掲載されるいくつかのパブリック・ドメインのベンチマークに対してBMCを適用して導出したものである。結果を適正なものに保つため、ハイブリッド方式を70以上の論理式に対して実行し、その中から40秒を上回るCPU時間を要した論理式の結果だけを報告する。これらの論理式を、充足不能なインスタンスと充足可能なインスタンスに分配した。論理式の式サイズは、1次入力とゲートの数を示す「1次入力」欄と「ゲート」欄から判断できる。
【００８１】
ｅ）  同一のヒューリスティックにおけるChaffとハイブリッドの比較
第1の比較では、ハイブリッド・ソルバーとChaffを完全に同一のヒューリスティックに適用した。すなわち、この2つは、BCPの相違を除いてまったく同一のアルゴリズムを使用して、含意の処理、対立ベースの学習、バックトラッキング、決定変数の選択の順に実行された。ヒューリスティックは同一とはいえ、複数のノードが対立した際の対立ノードの選択は制御されなかったので、多少の相違が存在することは否めない。充足不能なインスタンスについては、常に探索空間全体を走査する必要があるので上記の相違による影響はほとんどないが、充足可能インスタンスについては、2つのソルバーのうち1つが偶然に早期に解決されるインスタンスに遭遇する状況が発生するため、顕著な影響が出る可能性がある。この事実を考慮すると、この制御された実験おいては、充足不能なインスタンスのみを妥当なデータとみなすべきであろう。「Chaff」欄と「H」欄は、表2(図6)のChaffソルバーとハイブリッド・ソルバーの時間を示す。ハイブリッド・ソルバーの全体的なパフォーマンスは、Chaffのそれよりもはるかに良好であることは明らかである。ハイブリッドの時間に対するChaffの時間の典型的な比率は1.3以上であり、最大のケースでは3.75にも達する。充足不能な全インスタンスにおいてハイブリッド・ソルバーが費やした総時間に対するChaffが費やした総時間の比率は、1.48である。表2(図6)に示す充足可能なインスタンスについては、ハイブリッドに対するChaffの比率(Chaff/H)は1.0を中心として均等に分布しているが、標準偏差は大きいという、予想通りの結果となっている。
【００８２】
５．  回路ベースのSATヒューリスティック
この項では、ハイブリッド・ソルバーの機能強化に使用される回路ベース・ヒューリスティックの詳細を示す。ここでは、表3(図7)を参照する。表3(図6)で使用するサンプルは、表2(図6)と同じである。「H1」欄は、前項で説明したChaffと同じヒューリスティックを使用した場合のハイブリッド・ソルバーの実行時間を示す。
【００８３】
ａ）  含意を追跡する順序
Chaffでは、含意はFIFOメカニズムを使用して追跡される。すなわち、基本的には、含意は生成された順序で処理される。ハイブリッド方式では、ゲートのファンアウトと方向性の情報に基づき、回路パスに沿って含意を追跡することができる。学習済み文節から生成された含意をパスに沿って追跡する一方で、ゲートから生成された含意はFIFO方式で追跡する方法が非常に効果的であることが判明した。「H2」欄は、このヒューリスティックを使用した場合の総実行時間を示す。この欄の結果から、このヒューリスティックでは、ほぼすべてのサンプルにおいて(18中14)、H1を上回る速度が達成されることは明らかである。「H2」の右側にあるすべての欄では、このヒューリスティックが使用されている。
【００８４】
ｂ）  分岐変数決定戦略
決定戦略では、分岐点となる未割り当ての変数と値が選択される。これまで数種類の戦略が提唱されているが、決定的な勝者はまだ出現していない。最も大きな成功を収めた戦略はいずれも、何らかの形式の動的リテラル・カウントをベースとしている。次に、回路情報を使ってこの基本メカニズムの機能を強化する方法について考察する。
【００８５】
CNFベース・ソルバーは、最多の文節を充足するリテラルを選択するために、文節に含まれる正と負のリテラル数をカウントする。ここで重要なのは、どうしたら各ゲートの入力と出力において無矛盾値を取得できるかという問題である。図8に示すように、文節に含まれるリテラルをカウントするだけではこの問題に対処することはできない。図8(a)を参照すると、ORゲートoは入力aおよびbを有し、ファンアウト・ゲートはx、y、およびzを有している。図8(b)は、生成された文節を示す。この図から、変数が入力であるとき、文節内のその正と負のリテラル数は互いに相殺されることが分かる。また、変数がゲートの出力のときには、正のリテラル数が負のリテラル数よりも常に1多くなる。図8(b)の対応するスコアは、それぞれ5と4である。端的に言うと、リテラル数からは、ゲートから生成された文節に関する有益な情報は得られない。一方、ゲートのファンアウト情報からは、意思決定に必要とされるゲートの正と負のファンアウト数を正確に決定できる。これは、「ファンアウト・ヒューリスティック」と呼ばれる。「H2-fs」欄は、このヒューリスティックでのSAT時間を示す。このヒューリスティックが決定的な勝者というわけではないが、過半数を少し上回るサンプル(26/45)において、原型ハイブリッド方式(H2)よりも良好な結果をもたらすことは特筆に値する。
【００８６】
式の充足性を決定しない文節は、「非アクティブな文節」と呼ばれる(非特許文献２７参照)。非アクティブな文節は、観察不能になったゲートから生じる。これらの文節とそれに含まれる変数の決定を処理することは、基本的には無駄な努力である。これらの文節を動的に検出して除去するためには、文節にマーキングとアンマーキングを繰り返し行う必要がある。これらの実行時間演算を行うと枝取りされた探索空間が得られるが、マーキングとアンマーキングを繰り返し実行することで全体的なパフォーマンスに損失が生じる。このパフォーマンス向上は、到達可能性分析にのみ見られることに注意する必要がある。回路に対して演算を行う伝搬-位置調整型のブール推論メカニズム(非特許文献２４参照)では、観察不能なゲートと非アクティブ領域の動的検出は自動的に開始される。位置調整を必要とする変数は、「フロンティア変数」と呼ばれる。この戦略は、変数決定の対象を動的に変動するフロンティア上の未割り当てゲートに絞り込むことによって適用される。これは、「フロンティア・ヒューリスティック」と呼ばれる。このヒューリスティックにはさらに、充足する割り当てが存在するときには、より迅速にそれに到達できるという利点もある。「H2-ft」欄は、このヒューリスティックでのSAT時間を示す。サンプルの80%において原型ハイブリッド方式(H2)よりも良好な結果が得られた。
【００８７】
「H2-ft-fs」欄は、フロンティア・ヒューリスティックとファンアウト・ヒューリスティックの両方を使用した場合の実行時間を示す。ここでも、サンプルの約73%においてH2を上回る速度が観察された。
【００８８】
ｃ）  XOR／XNORゲートの学習
多数のXORおよびXNORゲートを有する回路では、SATソルバーのパフォーマンスが低下することが知られている。均質なゲートを有する回路表現を与えられた場合は、回路内のXORおよびXNORゲートを抽出することは可能であり、かなりの効率も期待できる。ハイブリッド表現では、これらのXOR/XNORゲートの文節が学習され、CNF文節データベースに加えられる。「H2-ft-fs-six」欄は、この学習をフロンティアおよびファンアウト・ヒューリスティックと共に適用した場合の実行時間を示す。これら3つのヒューリスティックをすべて採り入れた場合、サンプルの62%以上で基本的なハイブリッド方式(H2)を上回る速度が観察された。
【００８９】
ｄ）  ハイブリッド・ソルバーでの最良の結果
「H-best」欄に、ハイブリッド・ソルバーで得られた最良の結果を示す。すべてのサンプルにおいてハイブリッド・ソルバーがChaffよりも高速なことは明らかである。「Chaff/H-best」欄に、最良のハイブリッド・ソルバー時間に対するChaff時間の比率を示す。すべてのサンプルで50%以上の速度向上が見られ、サンプルの69%で2を上回った。表3(図6)のヒューリスティックは明らかに未成熟であり、さらなる研究を要する。とはいえ、H2-ftヒューリスティックはきわめて良好に動作するので、デフォルトとして使用できるのは明らかである。
【００９０】
ｅ）  有界モデル検査における含意
SATはBMCのようなアプリケーションにおいてコア・エンジンとなる。事実、50〜100時間フレームにわたる回路分析を必要とする典型的なBMC処理では、SATソルバーが1回の実行で数千回も呼び出されることが予想される。SATソルバーは1回の呼び出しにつき数分間程度を消費するため、長いBMC実行の場合は完了までに数日間を要することになる。そのため、コア・エンジンで2倍の速度向上が実現できることは、絶対的な実行時間が大幅に短縮されることであり、その影響はきわめて大きいものとなる。本研究のもう1つのテーマは、回路SAT手法は有力な候補であり、CNFベースの手法に勝ることを明確に実証することである。実用使用における効果としては、SATのために回路全体をCNFデータ構造にコピーしなくてもよいため、それに伴うオーバーヘッドを見込む必要がないことが挙げられる。これは、これらのアプリケーションのメモリ所要量がほぼ半減されるため、より大規模な回路にスケーリングすることが可能になり、BMCの場合はスケーリングできる時間フレーム数も増大する、という利点をもたらす。
【００９１】
６．  生産設計に関する実験結果
生産設計を検証するため、BMCエンジンの実装をDiVer内で適用した。各検証タスクでは、対象となる特性の証拠(または反証)を探索した。これらの特性は、安全性と活性とした。結果を表4(図9)にまとめる。ほとんどの実験は、256 MBのメモリを搭載した750 MHzのIntel PIII上で実施した。表内に「(S)」を付記して示した一部の実験は、Sun UltraSparc 440 MHz、1GBのワークステーション上で実施した。
【００９２】
各設計を対象に、第4欄に示す5つのオプション・セットに関して実験を行った。最初の4つのオプション・セットは、カスタマイズ変換の4種類の組み合わせ(「+/- T」として示す)と、構造的同形を使用した回路単純化(「+/- C」として示す)に関連する。(定数の伝搬により実現された回路単純化を、常にデフォルトとして使用する。)第1のオプション・セットop1はこのいずれも使用せず、第2のオプション・セットop2は回路単純化のみを使用し、第3のオプション・セットop3はカスタマイズ変換のみを使用し、第4のオプション・セットはこの両方を使用する。この4つのオプション・セットはすべて、第6項で説明した漸増的SAT手法を実行する能力を有するChaff SATソルバー(非特許文献１０参照)の修正版を使用する。最後に、第5のオプション・セットop5も、カスタマイズ変換と回路単純化の両方を使用する。これは、第8および9項で説明したハイブリッドSATソルバー(「+H」として示す)を使用することを除いて、第4のオプション・セットと同じである。
【００９３】
漸増的SAT手法の使用により実現可能なパフォーマンスの利得はどの程度かを調べることも興味深い。そのため全5オプション・セットについて、SATソルバーで漸増的SAT手法を使用する場合と使用しない場合の実験も行った。カスタマイズ変換は、SATソルバーで漸増的SAT手法の使用の有無にかかわらず、常に漸増的な公式化を使用することに留意されたい。
【００９４】
表4(図9)に、いくつかの設計および特性に関する全5オプション・セット(1〜5を付番)の結果を示す。2番目と3番目の欄はそれぞれ、各特性に関する影響の静的コーン(全オプション・セット間で同一)内に存在するフリップフロップ数とゲート数を示す。5番目の欄は、証拠/反証を検出するために展開された時間フレーム数(すなわち、BMCのパラメータk)を示し、6番目の欄は、そのkにおいて証拠が検出されたかどうかを示す。次の2欄は、漸増的SAT手法を使用した場合と使用しなかった場合(それぞれ、「+Inc」および「-Inc」として示す)にかかった時間(単位: 秒)を示す。最後の欄は、漸増的 SAT手法を使用した検証を実行するために必要とされたメモリ量(単位: メガバイト)を示す。(ほとんどのサンプルでは、漸増的SATを使用しない検証で消費されたメモリ量も同程度であった。)
【００９５】
オプション・セット2〜5では基本BMC(オプション・セット1)に比較して一貫してパフォーマンスが向上したことから、本発明の機能拡張の効果は明らかである。サイズが大きいサンプルは、同じ境界kに関して最大2オーダーのパフォーマンス向上を示した。基本BMCは、割り当てられた時間(10,000秒)内に、機能拡張を行ったBMCよりも少ない数の時間フレームしか完了できないケースが多数あったことは注目に値する。特に、バスのサンプルでは、基本BMCはこの時間内ではついに証拠を検出できなかった。
【００９６】
ほとんどのサンプルにおいて、カスタマイズ変換のみを使用した機能拡張(op3)は、回路単純化のみを使用した機能拡張(op2)よりも良好なパフォーマンスを示した。また、この両方を組み合わせた機能拡張(op4)は、いずれか一方のみを使用した機能拡張に比較して常に良好な結果を示した。さらに、ハイブリッドSATソルバーを使用した機能拡張(op5)は、ほとんどのサンプルにおいてこれよりもさらに高いパフォーマンスを示した。
【００９７】
漸増的SAT手法の使用については、BMCの異なるkインスタンス間で回路制約だけが共有される基本BMC(op1)において、漸増的SAT手法の使用による利得が最も少ないことに注目する必要がある。漸増的SATの真の利点は、上記に加えてBMCの各kインスタンス内で制約を共有することも可能な本発明のカスタマイズ変換に見ることができる。カスタマイズ変換を使用する場合(op3、op4、op5)の改善率は、使用しない場合(op1、op2)よりも概して高い。これは、SAT解決時間が大きな影響を及ぼす比較的大きなサンプル(Bus3、Dma2、およびD1-P5)の結果から明白である。さらに、SATソルバーで漸増的SAT手法を使用することによる利得は、カスタマイズ変換を使用する場合よりも少ない。これは、SATソルバーが制約の共有を行わない場合でさえも、分割戦略として漸増的な公式化を採ることに大きな利点があることを示している。
【００９８】
７．  帰納による安全性特性の証明
BMCエンジンは、有界長の反証を検出することに加えて、帰納証明の実行にも使用できる(非特許文献１６参照)。深度kを増大させて実行される帰納と、ループなしパスに対する制限を組み合わせると、安全特性の完全な証明手法が得られる（非特許文献５、１１参照）。深度kの帰納は、以下の2ステップから成る。
【００９９】
基本ケース：その特性が、初期状態から始まる長さkの各パス上で有効であることを証明する。
帰納ステップ：その特性が、任意の状態から始まる長さkのパス上で有効であり、さらには、長さ(k+1)のパスの拡張上でも有効であることを証明する。
【０１００】
ループなしパスに限定することにより、「パス内に同一の状態がない」という追加の制約が課される。ここで、基本ケースでは初期状態制約が使用されるが、帰納ステップではこの制約は使用されないことに注意する必要がある。したがって、帰納ステップには到達不能な状態も含まれる可能性がある。実用使用では、追加の制約(すなわち、特性自体よりも強力な帰納不変式)を使わずに帰納証明を完了することは不可能なこともある。この場合は、到達可能性の制約など、設計者に既知の回路制約を使用して帰納不変式を強化することができる。
【０１０１】
ａ）    帰納証明のためのBMCプロシージャー
この項では、BMCエンジンで使用される帰納プロシージャーについて解説する。以下に擬似コードを例として示す。
【０１０２】
0004000567.tif 000006
【０１０３】
ここで、pは、真であることを証明すべき安全性特性に対応するモニター述語である。すなわち、正当性特性はG(p)である。LTLで表現された任意の安全性特性を与えられると、質問票作成手法(非特許文献１参照)を使用して、「安全性特性はモニター述語がすべての到達可能な状態において真である場合にのみ真である」というモニター述語を得ることができる。ここに示した擬似コードでは、cは真であることが既知の回路制約、Iは初期状態制約、Pは到達可能性制約をそれぞれ示す。本書で解説する証明プロシージャーのサンプルは、cとＲは有効であることを前提とする。すなわち、c_iはすべての時間フレームにおいて真でなければならず、Ｒは到達可能状態の過剰近似でなければならない。(これが得られない場合は、各々が擬似コード内で「真」であるとみなすことができる。)
【０１０４】
擬似コードでは、BCは基本ケースの検査を実行するための文節データベース、ICは帰納ステップ検査を実行するための文節データベースである。このプロシージャーは、初期化によって開始される(第3、4行)。第1のSAT検査(第5行)は、cとRを充足する状態が!pも同時に充足するかどうかを確認するために実行される。このような状態が存在しない場合、特性pは明らかに真である。これは、帰納証明がまだ開始されない段階の早期終了ケースとされる。i上のループ(第7〜18行)は、深度をユーザー定義の限界値Nまで増大させて帰納証明を実行する。最初に、基本ケースが検査される。これは、制約c_iを追加し、i番目の時間フレームにおける!p_iの充足可能性をチェックすることにより行われる。充足可能な場合は、初期状態から始まる反証が検出されたことを意味するため、特性は偽である(第10、11行)。一方、充足可能でない場合は、p_iが学習され、BCデータベースに追加される(第12行)。次に、(i+1)番目の時間フレームにおける帰納ステップが検査される。ここでは、帰納的仮説によりp_iは真であると想定され(第13行)、制約c_i+1が追加され(第14行)、さらには、長さ(i+1)のパスはループなしという制限のもとで!p_i+1の充足可能性が検査される(第16行)。これが充足可能でない場合は、帰納証明が成功したのであり、特性はまさしく真である。一方、充足可能な場合は、帰納証明は深度iで失敗したのであり、引き続きiを漸増させてループを再試行する。そのまま限界値Nに到達すると、結果は不確定となる。
【０１０５】
このプロシージャーは、基本ケースと深度iにおける帰納ステップについてそれぞれモノリシックSAT式を生成するのではなく、充足不能なSATインスタンスから学習しながらSAT下位問題を漸増的に構築する。数個の工業用設計で得られた実験結果により実証されたように、上記の機能拡張で強化した本発明のBMCエンジンは、実用使用においてこうした証明を効果的に実行することができる。これらの結果は、440 MHz、1 GBのSun UltraSparcワークステーション上で実施した実験の結果をまとめた表5(図10)に示されている。
【０１０６】
BMCエンジンが反証を検出できなかった設計(第1欄)と安全特性(第2欄)に対しては、帰納証明を実行した。これらの証明では設計者から提供された回路制約を使用したが、到達可能性制約は使用しなかった。第3欄は、特性に関する影響のコーン内に存在するフリップフロップ数（＃FF）とゲート数（＃G）を示す。第4欄は、検証状況を示す。ここで、「T」は特性が真であることを証明されたことを示し、「-」は帰納証明が不確定に終わったことを示す。BMCエンジンが真であることを証明できたのは、33特性のうち23特性であった。第5欄は、帰納証明が実施された最大深度を示す。成功裡に終わった証明の深度は、すべて2未満であった。一方、不確定性の証明は、多数の特性において深度25まで成功しなかった。最後に、第6欄と第7欄は、証明の実行で必要とされた時間(単位: 秒)とメモリ量(単位: メガバイト)を示す。時間とメモリの所要量は、深度25の場合でも非常に少ないこと注目されたい。
【０１０７】
次の項では、効果的な到達可能性の不変式を発見するために行った試みと、帰納証明でこれらの不変式を使用した結果について解説する。
【０１０８】
８．  BMCとBDDの結合
この項では、BDDとSATベースのBMCを結合するための新規なフレームワークについて説明する。その基本概念はいたって大まかで、「BDDとして計算された状態集合に関する外部情報を利用してBMCの探索を制約する」というものである。BDDの操作は(時間とメモリの両方において)資源集約的な傾向があり、これが実用使用では問題となる。そのため、BDDは回路またはCNFの形式に変換される。これにより、BMCエンジンはBDDを回路/CNF制約として処理できるようになる。
【０１０９】
このフレームワークを使用して帰納証明を行う方法は、以下のとおりである。最初のタスクは、到達可能状態の集合の過剰近似を得ることである。これは様々な方法で行うことができる。例えば、設計の「存在」抽象化は、一部のラッチを疑似1次入力として抽出して取り除く方法で行うことができる。こうした抽象化の有力な候補となるのは、順次コアに寄与しない周辺のラッチや、特性信号の依存性閉包の深部に存在するラッチなどである。本質的には、抽象設計は、実設計に存在するパスのスーパーセットを含まなければならない。この要件は、BDDベースの記号的走査を使用して、到達可能状態の過剰近似集合を得ることによって満たすことができる。また、抽象設計に細密走査を行う代わりに、近似走査手法を使用することもできる（非特許文献２８、２９参照）。これに加えて、BDD用の過剰近似手法を使用して、最終BDDのサイズをさらに縮小することも可能である(非特許文献３０参照)。
【０１１０】
BDD(または、一連のBDD)として到達可能状態の過剰近似集合が得られたら、それをBMCエンジンに適した形式に変換することが次のタスクとなる。このとき、BDDは回路/CNF形式に変換される。この形式の各内部BDDノードは、BDD変数(この場合は、「状態」変数)によって制御されるマルチププレクサーとみなされる。この派生された回路/CNFを到達可能性制約としてBMCエンジンに追加し、本発明で解説した疑似コード形式の帰納証明プロシージャーとして使用する。
【０１１１】
実用使用では、BDDベースの到達可能性制約の使用によって帰納証明の完了が可能になり、一方、この制約を使わない証明は不成功に終わったという事例が報告されている。表6(図11)に実験結果を示す。この実験も、440 MHz、1 GBのSun UltraSparcワークステーション上で実施した。この表で、第3〜6欄は抽象設計に対するBDDベースの到達可能性分析の結果を示し、第7〜11欄はフル設計に対するBMCベースの帰納証明の結果を示す。実験に使用した抽象設計は、制約なし設計から、特性信号の依存性閉包の深部に存在するラッチを抽象化して除去することによって自動的に取得した。どのケースでも、これに要した時間は1分間未満であった。第3欄は、抽象設計内に存在するフリップフロップ数（＃FF）とゲート数（＃G）を示す。これらの数値は、フル設計の対応する数値(第7欄)に比較してはるかに小さいことに注目されたい。第4欄は、回路形式への変換を含む、抽象設計の記号的走査に要した時間(単位: 秒)を示す。第5欄には記号的走査に要した反復回数、第6欄にはBDDの最終的なサイズ(一部のケースでは、さらに過剰近似を行った後のサイズ)を示す。BMC帰納証明については、第8欄と第9欄に帰納の検証状況と深度をそれぞれ示す。いずれのケースにおいても証明はきわめて容易に完了できたことに留意されたい。最後に、第10欄と第11欄に、BMCエンジンが費やした時間とメモリ量を示す。
【０１１２】
これらの結果のうち特に注目されるのは、必要とされるBDDの時間とサイズをできるだけ抑えるため、BDDベース分析では大まかな近似しか行わなかったにもかかわらず、得られた到達可能性制約はBMCの帰納証明を完遂するのに十分な強度を持ち得ていたことである。BDD、BMCエンジンのいずれもこれらの安全特性を個別では証明できないが、本発明のフレームワークと組み合わせることにより、証明が20秒未満で完了するという驚くべき成果が得られた。
【０１１３】
組み合わせフレームワークを使用した主な動機は、SATベースBMCエンジンの本来の機能はパス・ベースで、一方、BDDベース記号的分析は集合ベースであるという事実に発する。これにより、純粋なBMCエンジンの機能を可能な限りBDDで補完するという利用法が可能になる。このフレームワークはさらに、任意CTL特性の反証/証拠を検出する用途にも利用できる。与えられた設計から得た抽象設計にBDDベースの近似モデル検査を実行することにより、「証拠グラフ」のBDD表現を得ることができる(非特許文献１８参照)。これらの状態は、BMCエンジンの反証探索に制約を付加するか、優先順位を付けるために使用できる。
【０１１４】
前述の明細書の説明から、当該技術に精通した当業者には本発明には他の変更および異型が可能なことが明らかであろう。したがって、本書では本発明のごく一部の実施例のみが特に説明されているが、本発明の精神および範囲から逸脱することなく無数の変更が可能であることは明らかである。
【０１１５】
【発明の効果】
以上説明したように本発明の有界モデル検査方法によれば、アプリケーションのメモリ所要量がほぼ半減されるため、より大規模な回路にスケーリングすることが可能になり、BMCの場合はスケーリングできる時間フレーム数も増大する。
【図面の簡単な説明】
【図１】  BMCシステムに含まれる機能を図示する検証プラットフォームの概略図を示す図である。
【図２】  (a)ループなしの有界パスのケース分割を示す。(b) (k-l)ループにおける有界パスのケース分割を示す図である。
【図３】  回路ベースのBCPプロシージャーの実装に関する疑似コードを示す図である。
【図４】  高速含意伝搬のための2入力ANDルックアップ・テーブルを示す図である。
【図５】  100万含意当たりのブール制約伝搬 (BCP: Boolean Constraint Propagation)時間を記載した表1を示す図である。
【図６】  比較におけるSAT実行時間を記載した表2を示す。
【図７】  ハイブリッド・ソルバーのヒューリスティックによって向上したSAT実行時間を記載した表3を示す図である。
【図８】  文節内のリテラル計数の例を示す図である。
【図９】  BMC検証の結果を記載した表4を示す図である。
【図１０】  到達可能性の制約のない帰納例による証明の結果を記載した表5を示す図である。
【図１１】  到達可能性の制約のある帰納例による証明の結果を記載した表6を示す図である。
【図１】
0004000567.tif 000007
【図２】
0004000567.tif 000008
【図３】
0004000567.tif 000009
【図４】
0004000567.tif 000010
【図５】
0004000567.tif 000011
【図６】
0004000567.tif 000012
【図７】
0004000567.tif 000013
【図８】
0004000567.tif 000014
【図９】
0004000567.tif 000015
【図１０】
0004000567.tif 000016
【図１１】
0004000567.tif 000017