Efficient Static Compaction of Test Patterns Using Partial Maximum Satisfiability

In this section, we state some basic properties of the PMS problem.

Given a set of Boolean variables $\{x_1,x_2,\mathrm{\dots },x_n\}$ , a literal is defined as a variable $x_i$ or its negation form $-x_i$ . A clause $C_i$ is defined as a disjunction of literals (i.e., $C_i=l_{i_1}\vee l_{i_2}\vee \mathrm{\dots }\vee l_{i_j}$ ). A CNF $F$ is defined as a conjunction of clauses that is composed of a set of clauses (i.e., $F=C_1\Lambda C_2\Lambda \mathrm{\dots }\Lambda C_c$ ).

The PMS problem is defined as finding an assignment in the CNF formula, in which clauses are composed of hard clauses and soft clauses, so that all hard clauses are satisfied and the number of satisfied soft clauses is maximized. The weighted PMS, where each soft clause is associated with a positive weight, aims to satisfy all hard clauses and maximize the total weight of the satisfied soft clauses. The assignment $\alpha$ of Weighted PMS (WPMS) instance $F$ is feasible if the assignment satisfies all hard clauses in $F$ . The cost of a feasible assignment $\alpha$ is defined as the number of falsified soft clauses under $\alpha$ for PMS. For convenience, the cost of any infeasible assignment is defined to be + $\mathrm{\infty }$ . Typically, $F$ is written to Weighted CNF (WCNF) file and as input to Weight SAT (WSAT) solver.

We introduce the translation process from the relationship between tests and faults into a PMS problem in Procedure 1. According to R-Matric, faults are translated in the Step (2) and tests are translated in the Step (3).

For Step (2) in Procedure 1, the translation of faults is illustrated in Fig. 1 . Note that the black arrow between the test ${\text{𝒕}}_p$ and fault ${\text{𝒇}}_q$ indicates that ${\mathit{t}}_p$ is in the TSet ( ${\text{𝒇}}_q)$ , and the white arrow from fault ${\text{𝒇}}_q$ indicates that ${\text{𝒇}}_q$ can be translated into the $C_q$ . For example, ${\text{𝒇}}_4$ can be detected by ${\text{𝒕}}_2$ , ${\text{𝒕}}_5$ , and ${\text{𝒕}}_6$ ; thus, TSet ( ${\text{𝒇}}_4)=\{{\mathit{t}}_2$ , ${\text{𝒕}}_5,{\text{𝒕}}_6\}$ . Consequently, clause ${\text{𝒇}}_4$ is $2\vee 5\vee 6$ . In the same way, clause ${\text{𝒇}}_{14}$ is $1\vee 2\vee 7$ . At the end of the second iteration, all the faults were mapped into hard clauses, and all the tests were mapped into soft clauses, which would be passed to a PMS solver to find the satisfying assignments; this would indicate which tests can be reduced.

10.26599/TST.2019.9010046.F1 Fig. 1Translation of faults.

Since some translation procedures in Fig. 1 are left out, in Table 2 , considering the relationship between tests and faults, we show all the clauses, which include 14 hard clauses and 7 soft clauses. For hard clauses on the left of Table 2 , the weight is set to the number of soft clauses plus 1. Different from this, the weight of soft clauses is set to 1 on the right of Table 2 . All clauses end of in a 0 and are solved in a PMS solver. The $j$ -th line in hard clauses represents tests related to $j$ -th faults. For example, ${\text{𝒇}}_1$ can be detected by ${\text{𝒕}}_1$ and ${\text{𝒕}}_3$ ; Thus, $\text{TSet}({\mathit{f}}_{i1})=\{{\mathit{t}}_1,{\mathit{t}}_3\}$ ; consequently, the clauses for ${\mathit{f}}_1$ is 1, 3, 0 in WCNF file. This example illustrates that ${\mathit{f}}_1$ can be detected only if ${\mathit{t}}_1$ or ${\mathit{t}}_3$ exists. In soft clauses, all literals are negative and all clauses are unit fault.

After constructing the relationship between tests and faults with the WCNF, each fault is transformed into a hard clause denoted by ${𝝋}_F$ , which means that the fault must be detected. Each test in the hard clause is treated as a Boolean variable, which represents the state of redundancy, while each test is transformed into a unit soft clause denoted by ${𝝋}_T$ , and the unit fault is converted to a unit hard clause. Therefore, the complete CNF ${𝝋}_{\text{compaction}}$ for static test compaction is formulated as follows,

(2) $${𝝋}_{\text{compaction}}={𝝋}_F\cdot {𝝋}_T$$

The CNF ${𝝋}_{\text{compaction}}$ can be solved by a PMS solver. If the solver returns a solution in which no soft clauses is satisfiable, no test pattern can be reduced. Otherwise, the satisfied soft clauses indicate the reduced test patterns.

Converting the test set reduction problem into a PMS problem can ensure the effective reduction of the number of test sets, and the change will not reduce the fault coverage. The compaction procedure is described in Procedure 2.

In Procedure 2, note that our static test compaction process can be used for both sequential and combinational circuits and we operate differently aiming at different types of circuits in Step (1). When TetraMAX is used to generate test sets, the fault model used is SAFs in Step (2). There are many reasons for choosing SAFs. First, it is easy to generate a fault list, and the total number of faults increases linearly with the number of logic gates in the circuit. Second, the test set that can cover all the SAFs also has a high coverage rate for other types of faults in the chip.

Last, the SAFs aims at a single fault in the chip, while existing experiments have shown that the test set that can cover all single faults also has a high coverage rate when multiple faults are being detected^{[ 22 ]}. For the generated PMS formulas, SATLike, which is a famous incomplete partial MaxSAT solver based on the dynamic local search^{[ 23 ]} approach, is selected in Step (6). In terms of the new set of test patterns, Step (7) confirms that the fault coverage will not decrease.