针对传统的自动测试图形向量生成采用逐个求解单一故障模型导致生成测试向量数据量巨大的缺点,提出一种基于布尔满足性(boolean satisfiability,SAT)的多目标故障测试向量动态压缩方法,同时论证多目标故障测试生成问题为布尔满足性问题.该方法将具有鲁棒性的SAT算法嵌入经典的动态压缩流程中,首先利用经典动态压缩算法求解最小测试向量检测大部分失效故障,然后采用SAT求解器对未测出的多故障电路进行同一求解和附加约束求解方式,最终得到故障覆盖率高的测试向量和同一测试最大故障列表.实验数据表明,在相同电路模型情况下,此方法求得的测试向量相比经典动态压缩减少高达70％.%The traditional ATPG generating test pattern data by single faults model leads to huge test pattern quantities.Aiming for this problem,this paper proposed a dynamic compaction of multiple target test patterns based on SAT and demonstrated how the multiple target test generation problems could be formulated as a SAT problem.This method integrated robust SAT algorithm into the classical dynamic compaction flow.Classical dynamic compaction flow pruned a large number of faults which were easy to detect with only a few test patterns,and then the SAT solver to get the one synchronous solution in multiple target faulty and additional constraint.Finally,it obtained the high faulty coverage test pattern data and the maximum faulty list for one synchronous test.Experimental results on same large industrial circuits show that generated data of multiple target test generation compared with them of classical dynamic compression is able to reduce data count as much as 70％.
展开▼
