テスト生成

処理の概要

SATソルバを用いたテスト生成の処理の概要を以下に記す．

1. 正常回路の論理関係を表すCNFを作る．

2. 故障回路の論理関係を表すCNFを作る．

3. SAT問題を解く．

4. SAT問題の解からテストパタンを求める．

実際には効率的な処理を行うために以下の工夫を行う．

• 正常回路において故障の推移的ファンアウトと無関係な部分を削除する． より厳密には故障の推移的ファンアウトの推移的ファンインのみを対象とする．

• 故障回路において故障の推移的ファンアウト以外を削除する．

• 故障箇所から FFR の根のノードの出力までの故障伝搬条件は別途考えるこ とにして FFR の根のノードの出力から外部出力までの故障伝搬条件のみを CNFとして生成する．

特に最後の項目が重要で，FFR 内の故障伝搬は FFR の構造的な性質から故障 伝搬経路はつねに単一経路となり， 故障伝搬条件も一意に定まる． さらにその条件もすべての side input の値割り当ての論理積の形で表される のでCNFにする必要がない． すると同一のFFR内の故障に対するテスト生成問題は全て同一のCNFを用いる ことができる．

テスト生成問題を表す CNF の生成

正常回路の論理関係を表すCNFを生成するために StructEngine を用いる．

StructEngine(
  const TpgNetwork& network,
  const JsonValue& option
);

option で指定できる値は以下の通り．

キーワード	タイプ	説明	デフォルト値
sat_param	JsonValue	SATソルバの初期化パラメータ
justifier	string	Jusitifer の初期化パラメータ

故障回路の論理関係を表すCNFを生成するために BoolDiffEnc を用いる． ただし， BoolDiffEnc は StructEngine と組み合わせて使うので BoolDiffEnc を組み込んだ BdEngine を用いたほうが簡単である．

BdEngine(
  const TpgNetwork& network,
  const TpgNode& node,
  const JsonValue& option
);

BdEngine は StructEngine の派生クラスなので network と StructEngine と同様である． node は故障伝搬の起点となるノードを指定する． option は StructEngine のオプションに加えて以下の値が指定できる．

キーワード	タイプ	説明	デフォルト値
extractor	string	検出条件の抽出方法

BdEngine を生成した時点で node を起点とした故障伝搬条件を求めるた めに必要な情報は全て設定されている． あとは BdEngine::solve() を呼び出すことで設定した条件を満たす 解を求めることができる．

SAT問題から値を取り出す．

SAT問題の解は SatModel の形で取り出すことができる． SatModel からは個々の SatLiteral に対する真偽値を得ることができるが， 個々の SatLiteral が元の回路のどのような値に対応しているかが わからなければテスト生成問題の解を求めることはできない．

そこで， StructEngine および BoolDiffEnc ( BdEngine ) はもとのネットワークのノード( TpgNode )と SatLiteral の対応関係を持っている． TpgNode と SatLiteral の対応関係は VidMap が持つ．

StructEngine は2つの VidMap を持つ． 1つは gvar_map で現時刻におけるノードの値を持つ SatLiteral との対応関係を表す． もう1つは hvar_map で1時刻前のノードの値を持つ SatLiteral との対応関係を表す．

BoolDiffEnc も2つの VidMap を持つ． 1つは fvar_map で現時刻における故障値を表す SatLiteral との対応関係を表す． もう1つは dvar_map で故障伝搬条件を表す SatLiteral との対応関係を表す． ただ， dvar_map は内部で用いられる．

故障の検出条件の抽出

SATの解からテストパタンを求めるだけなら上記の gvar_map から外部入力 ノードの値を取り出せばよいが， 複数の故障を同時に検出できる質のよいテストパタンを求めるなどのより高度 な処理を行うためには，故障の検出条件を抽出する必要がある．

もちろん， SatModel に含まれる全ての値割り当ての集合も完全な故障の検 出条件である． ただ，値割り当てのなかには故障を検出するために必ずしも必要でないものが含まれる． そこで，故障の検出条件を満たす(可能であれば)極小の値割り当てを求めたい． さらに， gvar_map と hvar_map に含まれる変数のみからなる割り当て を検出条件として用いれば， StructEnc のみを用いてその条件を満たすテストパタンを求めることができる． このような検出条件を求めるに以下の関数を用いる．

AssignList
BdEngine::extract_sufficient_condition();

この関数を呼ぶ前にSAT問題の解が求められている必要がある． この検出条件の抽出方法は唯一ではない． そこで， BdEngine のオプションの extractor の値 としてアルゴリズムを指定する文字列を指定する． 現時点では可能な文字列は "simple" のみである．

正当化

故障の検出条件として回路内部のノードの値割り当てが与えられた時， そのままではテストパタンにはならない． ただし，その検出条件は充足可能であることがわかっているので 充足解が与えられればテストパタン(外部入力における値割り当て)を 求めることができる． この操作を「正当化(Justification)」と呼ぶ．

正当化の結果は唯一ではない． 例えば2入力ANDゲートの出力を0にするためにはどちらか一方の入力の値を0にすればよい． そこでいくつかのヒューリスティックが考えられる． 正当化の手法に関しては StructEngine のオプション justifier の値と して指定する． 現在，有効な値は "simple" , "just1" , "just2" となっている．

• StructEngine
• BoolDiffEnc
• BdEngine
• VidMap
• DtpgResult
• DtpgStats