基于SAT的组合电路自动测试向量生成

Automated Test Pattern Generation for Combinational Circuits Based on SAT

实现了基于可满足性(SAT)求解的方法,以解决固定型和时延故障的自动测试向量生成问题。详细讨论了如何利用电路的拓扑结构以及从ATPG到合取范式(CNF)的编码方法。CNF被输入到一个高效的SAT求解器zchaff中求解。在ISCAS85测试实例中验证了该算法的有效性。

Automated test pattern generation（ATPG） algorithms for both stuck-at and delay faults were implemented based on satisfiability（SAT） solving.Topology of the circuits was discussed in detail,as well as encoding ATPG problems into conjunctive normal forms（CNFs）,which were solved by zchaff,an efficient Boolean SAT solver.The proposed algorithms were tested using a set of ISCAS85 benchmarks to demonstrate their effectiveness.