テスト生成
===========

処理の概要
~~~~~~~~~~~

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

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

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

#. SAT問題を解く．

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


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

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

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

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

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

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

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

.. code-block:: c++

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

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

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

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

.. code-block:: c++

   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` のみを用いてその条件を満たすテストパタンを求めることができる．
このような検出条件を求めるに以下の関数を用いる．

.. code-block:: c++

   AssignList
   BdEngine::extract_sufficient_condition();

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


正当化
~~~~~~~~

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

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


.. toctree::
   :maxdepth: 1

   structengine
   booldiffenc
   bdengine
   vidmap
   dtpgresult
   dtpgstats