面向动态特性的自动测试向量生成系统优化方法

严大鹏; 何其润; 郭京; 王泊宁; 蔡志匡

doi:10.11999/JEIT260025

面向动态特性的自动测试向量生成系统优化方法

doi: 10.11999/JEIT260025 cstr: 32379.14.JEIT260025

严大鹏¹,
何其润¹,
郭京¹,
王泊宁¹,
蔡志匡^{1, 2, ,}

1.
南京邮电大学集成电路科学与工程学院南京 210023
2.
射频集成与微组装技术国家地方联合工程实验室南京 210023

详细信息

作者简介:
严大鹏：男，讲师，研究方向为智能化测试与芯粒测试

何其润：男，硕士生，研究方向为智能化ATPG

郭京：女，硕士生，研究方向为智能化ATPG

王泊宁：男，博士生，研究方向为测试向量优化大模型

蔡志匡：男，教授，研究方向为芯粒测试与智能化测试

通讯作者:
蔡志匡　whczk@njupt.edu.cn

中图分类号: XXXXX
计量
- 文章访问数: 15
- HTML全文浏览量: 5
- PDF下载量: 0
- 被引次数: 0
出版历程
- 收稿日期: 2026-01-08
- 修回日期: 2026-03-11
- 录用日期: 2026-03-24
- 网络出版日期: 2026-04-19

Optimizing SAT-Based ATPG Systems: Unified Fault Set Construction, Modeling, and Solving

1.
School of Integrated Circuit Science and Engineering, Nanjing University of Posts and Telecommunications, Nanjing 210023, China
2.
National and Local Joint Engineering Laboratory for RF Integration and Micro-Assembly Technology, Nanjing 210023, China

摘要

摘要: 基于布尔可满足性的自动测试向量生成系统作为芯片故障检测的关键环节，系统效率受故障压缩策略、布尔可满足性建模策略及求解器传播能力共同制约，随着集成电路复杂度持续提升，其性能面临严峻挑战。该文提出一种面向自动测试向量生成系统的统一优化框架。构建检测点驱动的动态故障集，在保持可测故障覆盖完备性的前提下压缩待测故障规模。提出基于新型故障敏化约束的布尔可满足建模方法，通过显式敏化条件替代故障电路复制并约束于故障扇出锥内，减少合取范式变量与子句规模。引入面向扇出-重汇聚结构的动态蕴含学习，将结构相关性转化为增量蕴含以加强传播并提升冲突剪枝效率。实验结果表明，该方法能平均压缩故障集规模57.99%，子句和变量数开销平均降低11.44%和3.50%，平均将求解时间缩短22.43%，性能优于已有的测试向量生成系统。
- 自动测试向量生成 /
- 布尔可满足性 /
- 故障压缩 /
- 故障敏化约束 /
- 动态蕴含学习
Abstract: Objective SAT-Based automatic test pattern generation is widely used to produce tests for hard-to-detect single stuck-at faults and to prove fault untestability in combinational logic. When SAT-ATPG is scaled to large netlists with dense fanout and reconvergence, its runtime and memory consumption are frequently dominated by three interacting issues. Representative fault lists produced by conventional dominance or equivalence collapsing can remain large, increasing the number of SAT calls and enlarging the incremental context that must be maintained across faults. Meanwhile, SAT modeling may introduce redundant CNF overhead, especially when a faulty-circuit copy is explicitly constructed or when propagation constraints are encoded in a global form without locality control. In addition, fanout-reconvergence amplifies assignment correlations along sensitized paths; such correlations are often revealed only after repeated decisions and backtracks if only standard unit propagation is relied upon. A unified optimization objective is to reduce the overall CNF size and solving cost while preserving completeness, so that a practical SAT-ATPG system can remain efficient and stable across circuits of different scales. Methods A three-part framework is developed and implemented in an incremental SAT-ATPG flow, and the overall workflow is illustrated. (Fig.1) A checkpoint-driven dynamic fault-set construction method is introduced, where checkpoints are collected during netlist-to-DAG conversion, including all primary inputs and all fanout branches, and XOR or XNOR outputs are additionally recorded as supplementary checkpoints to prevent over-collapsing of XOR-related fault behavior. Representative faults are initialized on checkpoints with compact rules that combine dominance-oriented collapsing and equivalence-aware refinement, and solver-guided repair is performed when an untestable representative indicates potential masking under structural constraints. The procedure is summarized. (Algorithm 1) A fault-sensitization-constraint-based SAT modeling method is then employed to avoid explicit faulty-circuit duplication. Fault activation, propagation, and observability are captured by additional sensitization constraints over the original circuit variables, and auxiliary variables are introduced only when local bookkeeping is required. Constraint localization is enforced within the fault fanout cone, and cone boundary and internal vertices are identified by a graph traversal procedure. (Fig.2) A fanout-reconvergence-oriented dynamic implication learning mechanism is further integrated into the incremental solving loop. Reconvergence pairs inside the fault fanout cone are monitored under partial assignments, and structure-induced implications are injected as implied assignments when a reconvergent output becomes functionally determined, or as short conflict clauses when a branch-value combination becomes inconsistent with sensitization constraints. The dynamic implication procedure is summarized. (Algorithm 2) Results and Discussions The unified system is evaluated on ISCAS’85 and ISCAS’89 benchmark circuits, with TG-PRO used as the baseline implementation under the same SAT solver and termination settings. The checkpoint-driven dynamic fault-set construction substantially reduces the representative fault space entering ATPG. With respect to the uncollapsed fault space, the average representative-fault ratio decreases from 51.38% to 42.01%, corresponding to an average fault-space reduction of 57.99%, and the best-case ratio reaches 33.19% on large reconvergence-heavy circuits, which indicates that checkpoint-centered representative allocation effectively suppresses redundancy without expanding the untestable set. (Table 1) The reduced fault set size is reflected in preprocessing efficiency, and the total runtime for fault-set construction is consistently lowered; an average reduction of 8.37% is observed across the evaluated circuits. (Fig. 3) For SAT model construction, the sensitization-constraint encoding reduces CNF overhead compared with the baseline model construction. Over the benchmark set in total, the number of CNF clauses is reduced by 11.44% and the number of CNF variables is reduced by 3.50%, demonstrating that avoiding explicit faulty-circuit duplication and localizing auxiliary constraints to the fanout cone effectively lowers memory demand. (Table 2) The reduced CNF size and the strengthened locality of constraints are reflected in end-to-end runtime, and the total runtime of SAT modeling and solving is reduced across the evaluated benchmarks. (Fig. 4) Dynamic implication learning further improves solving efficiency on reconvergence-heavy structures. Compared with static implication integration, CNF construction time is increased by 3.0% on average because of additional monitoring and injection operations, yet the overall runtime is reduced by 4.25% on average, indicating a positive cost-benefit trade-off. The overhead attributed to implication learning accounts for 2.51% of total runtime in aggregate across circuits, which confirms that the injected implications and pruning clauses provide measurable solving benefits with limited extra cost. (Table 3) Conclusions A unified optimization framework for SAT-Based ATPG is developed by combining checkpoint-driven dynamic fault-set construction, localized fault-sensitization constraints for CNF modeling, and fanout-reconvergence-oriented implication learning. Representative faults are compressed with solver-guided repair of dominance and equivalence relations to prevent masking, CNF growth is constrained through duplication-free modeling localized to the fault fanout cone, and reconvergence correlations are exploited through incremental implication injection to strengthen propagation and early conflict pruning. Experimental results on standard benchmark circuits show consistent reductions in representative fault scale, CNF size, and total runtime, providing a practical approach for scaling SAT-ATPG to larger designs with complex fanout and reconvergence.
- Automatic test pattern generation /
- Boolean satisfiability /
- Fault collapsing /
- Fault sensitization constraints /
- Dynamic implication learning

HTML全文

图 1 优化的SAT-Based ATPG系统框架

下载: 全尺寸图片幻灯片

图 2 故障扇出锥信息识别

下载: 全尺寸图片幻灯片

图 3 不同故障集构建方法运行时间对比

下载: 全尺寸图片幻灯片

图 4 不同SAT模型构建方法运行时间

下载: 全尺寸图片幻灯片

1 Dynamic Fault-Set construction based on checkpoints

输入：L_check, L_xor
1. F ← $ \varnothing $;
2. for each l in L_check do
3. 　if is PI(l) and \|D(l) \| > 1 then
4. 　　F ← F $ \cup $ {stem(l, s-a-0), stem(l, s-a-1)}; continue;
5. 　for each v_d in D(l ) do
6. 　　if Type(v_d) in {XOR, XNOR, INV, BUF} then
7. 　　　F ← F $ \cup $ { fault(l → v_d, s-a-0), fault(l → v_d, s-a-1)}; 　　　　　continue;
8. 　　F ← F $ \cup $ { fault(l → v_d, dom) };
9. 　　if AllFaninInCheckpoints(v_d) and IsMinPin(l, v_d) then
10. 　　 F ← F $ \cup $ {fault(l → v_d, eq)};
11. for each l in L_xor do
12. if \|D(l) \| > 1 then
13. 　F ← F $ \cup $ {stem(l, s-a-0), stem(l, s-a-1)}; continue;
14. d ← UniqueDest(l );
15. F ← F $ \cup $ { fault(l → d,s-a-0), fault(l → d,s-a-1) };
16. for each f reported as U during ATPG do
17. if Type(f) == stem then continue;
18. 　f ← EqShift(f);
19. 　if NeedCompensate(VertexOf(f)) then
20. 　g ← DomFaultAtOutput(VertexOf(f));
21. 　g ← EqShift(g);
22. 　F ← F $ \cup $ {g};
输出： F

下载: 导出CSV

2. Dynamic implication method based on fanout-reconvergence pairs

输入：G={V, L}, CNF
1. CNF' ← CNF; F-Rpairs ← $ \varnothing $; maxcolor[ ] ← 1;
2. for each PI $ \in $ PIs do assign PI.color[0] ← maxcolor[0]++;
3. 　if \|V_d(PI)\| > 1 then CandidateFanouts[PI.color[0]] ← PI;
4. push all outputs of PIs into Ldyeing;
5. while Ldyeing not empty do l ← pop(Ldyeing); v_d ← V_d(l);
6. 　if v_d == $ \varnothing $ then continue; LD ← LogicDepth(l);
7. 　if maxcolor[LD] == 0 then maxcolor[LD] ← 1;
8. 　PropagateColor(l, v_d, maxcolor); push(v_d.output) into 　　　Ldyeing;
9. 　if \|v_d.inputs\| > 1 and AllInputsColored(v_d) then
10. 　　c ← MergeColor(v_d.inputs); f ← CandidateFanouts[c];
11. 　　if f ≠ $ \varnothing $ then add (f, v_d) to F-Rpairs;
12. 　　CandidateFanouts[c] ← UpdateFanout(c, v_d.output);
13. for each (f, r) ∈ F-Rpairs do InitPairType(f, r);
14. during CDCL solving, when a literal in cone(f, r) is assigned do
15. $ \Delta $ ← ImplyByPair(f, r);
16. 　if $ \Delta $ == CONFLICT then LearnClause(); return UNSAT;
17. 　if $ \Delta $ ≠ $ \varnothing $ then CNF' ← CNF' ∧ Encode($ \Delta $); Enqueue($ \Delta $);
输出：CNF′

下载: 导出CSV

表 1 不同故障集构建方法故障数目对比

基准电路	#F_uc	TG-PRO系统				本文方法
基准电路	#F_uc	#F_t	#F_d	#F_ud	#F_t/#F_uc	#F_t	#F_d	#F_ud	#F_t/#F_uc
C432	864	524	520	4	60.65%	458	454	4	53.01%
C3540	7080	3428	3291	137	48.42%	2905	2768	137	41.03%
C5315	10630	5350	5291	59	50.33%	4528	4469	59	42.60%
C7552	15104	7550	7419	131	49.99%	6148	6017	131	40.70%
S349	698	350	348	2	50.14%	275	273	2	39.40%
S400	800	424	418	6	53.00%	388	374	14	43.69%
S526	1052	555	554	1	52.76%	474	473	1	45.06%
S832	1664	870	856	14	52.28%	719	705	14	43.21%
S1238	2476	1355	1286	69	54.73%	1040	971	69	42.00%
S1423	2846	1515	1501	14	53.23%	1213	1199	14	42.62%
S1494	2988	1506	1496	12	50.40%	1123	1111	12	37.58%
S38417	76834	31180	31015	165	40.58%	25502	25337	165	33.19%

下载: 导出CSV

表 2 不同SAT模型构建方法所需的CNF子句、变量数目开销

基准电路	TG-PRO系统		本文方法
基准电路	#Ave (Clauses)	#Ave (Variables)	#Ave (Clauses)	#Ave (Variables)
C432	2013.830	523.181	1370.430	382.111
C1908	4592.400	1618.990	3802.680	1343.480
C3540	6681.410	2537.880	6099.210	2269.700
C5315	3159.040	3386.380	2973.550	3262.150
C7552	4446.020	4507.700	4270.750	4376.600
S349	377.590	259.269	343.145	228.284
S400	395.008	289.958	346.834	261.849
S526	474.880	386.776	439.203	356.188
S832	541.756	599.791	517.921	565.063
S1238	1604.910	809.356	1447.820	721.873
S1423	1772.140	993.290	1428.690	861.201
S1494	844.5180	941.913	832.800	897.744
S38417	1873.810	25358.300	1612.890	25207.300

下载: 导出CSV

表 3 不同蕴含学习方法对运行时间的影响(ms)

基准电路	静态蕴含			动态蕴含
基准电路	T_CNF	T_solve	T_t	T_CNF	T_solve	T_t	T_impl
C432	258	106	367	272	77	351	14
C3540	8036	2723	10766	8065	1738	9810	29
C5315	8975	2077	11062	9215	1542	10766	240
C7552	17894	4608	22516	18372	2563	20935	478
S349	49	11	61	50	7	57	1
S400	59	13	73	60	11	72	0
S526	97	22	121	97	18	116	0
S832	204	39	246	207	36	246	3
S1238	733	183	919	741	123	865	7
S1423	932	207	1142	1066	135	1126	134
S1494	445	121	569	447	85	539	2
S38417	56256	30365	86679	58570	25060	83690	2314

下载: 导出CSV

参考文献(30)

[1]	HUANG Junhua, ZHEN Huiling, WANG Naixing, et al. Accelerate SAT-based ATPG via preprocessing and new conflict management heuristics[C]. 2022 27th Asia and South Pacific Design Automation Conference (ASP-DAC), Taipei, China, 2022: 365–370. doi: 10.1109/ASP-DAC52403.2022.9712573.
[2]	ROTH J P. Diagnosis of automata failures: A calculus and a method[J]. IBM Journal of Research and Development, 1966, 10(4): 278–291. doi: 10.1147/rd.104.0278.
[3]	GOEL. An implicit enumeration algorithm to generate tests for combinational logic circuits[J]. IEEE Transactions on Computers, 1981, C-30(3): 215–222. doi: 10.1109/TC.1981.1675757.
[4]	FUJIWARA and SHIMONO. On the acceleration of test generation algorithms[J]. IEEE Transactions on Computers, 1983, C-32(12): 1137–1144. doi: 10.1109/TC.1983.1676174.
[5]	LARRABEE T. Test pattern generation using Boolean satisfiability[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992, 11(1): 4–15. doi: 10.1109/43.108614.
[6]	SHI Junhao, FEY G, DRECHSLER R, et al. PASSAT: Efficient SAT-based test pattern generation for industrial circuits[C]. Proceedings of the IEEE Computer Society Annual Symposium on VLSI: New Frontiers in VLSI Design (ISVLSI’05), Tampa, USA, 2005: 212–217. doi: 10.1109/ISVLSI.2005.55.
[7]	DRECHSLER R, DIEPENBECK M, EGGERSGLÜß S, et al. PASSAT 2.0: A multi-functional SAT-based testing framework[C]. Proceedings of the 2013 14th Latin American Test Workshop - LATW, Cordoba, Argentina, 2013: 1. doi: 1 0.1109/LATW.2013.6562675.
[8]	CZUTRO A, POLIAN I, LEWIS M, et al. TIGUAN: Thread-parallel integrated test pattern generator utilizing satisfiability ANalysis[C]. Proceedings of the 22nd International Conference on VLSI Design, New Delhi, India, 2009: 227–232. doi: 10.1109/VLSI.Design.2009.20.
[9]	SILVA J O M and SAKALLAH K A. Robust search algorithms for test pattern generation[C]. Proceedings of the 27th International Symposium on Fault Tolerant Computing, Seattle, USA, 1997: 152–161. doi: 10.1109/FTCS.1997.614088.
[10]	CHEN Huan and MARQUES-SILVA J. TG-PRO: A new model for SAT-based ATPG[C]. 2009 IEEE International High Level Design Validation and Test Workshop, San Francisco, USA, 2009: 76–81. doi: 10.1109/HLDVT.2009.5340173.
[11]	DAO A Q, LIN M P H, and MISHCHENKO A. SAT-based fault equivalence checking in functional safety verification[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, 37(12): 3198–3205. doi: 10.1109/TCAD.2018.2791465.
[12]	POMERANZ I and REDDY S M. Equivalence, dominance, and similarity relations between fault pairs and a fault pair collapsing process for fault diagnosis[J]. IEEE Transactions on Computers, 2010, 59(2): 150–158. doi: 10.1109/TC.2009.112.
[13]	GRIGORYAN T, MALKHASYAN H, MUSHYAN G, et al. Fault collapsing for digital circuits based on relations between stuck-at faults[C]. 2015 Computer Science and Information Technologies (CSIT), Yerevan, Armenia, 2015: 15–18. doi: 10.1109/CSITechnol.2015.7358242.
[14]	秦蔚蓉, 崔晓通, 程克非. 面向输出混淆度最优化的逻辑加密线性规划方法[J]. 电子与信息学报, 2025, 47(9): 3167–3177. doi: 10.11999/JEIT250527. QIN Weirong, CUI Xiaotong, and CHENG Kefei. Optimizing output obfuscation of logic locking with linear programming[J]. Journal of Electronics & Information Technology, 2025, 47(9): 3167–3177. doi: 10.11999/JEIT250527.
[15]	SCHULZ M H and AUTH E. Advanced automatic test pattern generation and redundancy identification techniques[C]. Proceedings of the Eighteenth International Symposium on Fault-Tolerant Computing. Digest of Papers, Tokyo, Japan, 1988: 30–35. doi: 10.1109/FTCS.1988.5293.
[16]	KUNZ W and PRADHAN D K. Recursive learning: An attractive alternative to the decision tree for test generation in digital circuits[C]. Proceedings International Test Conference 1992, Baltimore, USA, 1992: 816–825. doi: 10.1109/TEST.1992.527905.
[17]	ARORA R and HSIAO M S. Enhancing SAT-based equivalence checking with static logic implications[C]. Proceedings of the Eighth IEEE International High-Level Design Validation and Test Workshop, San Francisco, USA, 2003: 63–68. doi: 10.1109/HLDVT.2003.1252476.
[18]	LIU Hongduo, XU Peng, PU Yuan, et al. NeuroSelect: Learning to select clauses in SAT solvers[C]. Proceedings of the 61st ACM/IEEE Design Automation Conference, San Francisco, USA, 2024: 131. doi: 10.1145/3649329.3656250.
[19]	YAN Zhiyuan, LI Min, SHI Zhengyuan, et al. AsymSAT: Accelerating SAT solving with asymmetric graph-based model prediction[C]. Proceedings of 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), Valencia, Spain, 2024: 1–2. doi: 10.23919/DATE58400.2024.10546648.
[20]	储著飞, 马铖昱, 闫鸣, 等. 基于半张量积的逻辑综合研究进展[J]. 电子与信息学报, 2024, 46(9): 3490–3502. doi: 10.11999/JEIT231457. CHU Zhufei, MA Chengyu, YAN Ming, et al. Research progress in logic synthesis based on semi-tensor product[J]. Journal of Electronics & Information Technology, 2024, 46(9): 3490–3502. doi: 10.11999/JEIT231457.
[21]	SHI Zhengyuan, TANG Tiebing, ZHU Jiaying, et al. Logic optimization meets SAT: A novel framework for circuit-SAT solving[C]. 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2025: 1–7. doi: 10.1109/DAC63849.2025.11133310.
[22]	CHAO Zhiteng, ZHANG Xindi, HUANG Junying, et al. A fast test compaction method using dedicated Pure MaxSAT solver embedded in DFT flow[J]. Integration, 2025, 100: 102265. doi: 10.1016/j.vlsi.2024.102265.
[23]	CHAO Zhiteng, WANG Senlin, TIAN Pengyu, et al. A distributed ATPG system combining test compaction based on pure MaxSAT[C]. Proceedings of the 2023 IEEE 32nd Asian Test Symposium (ATS), Beijing, China, 2023: 1–6. doi: 10.1109/ATS59501.2023.10317948.
[24]	易茂祥, 张佳桐, 鲁迎春, 等. 一种基于BRAM分段同步查表的测试向量编解码方案[J]. 电子与信息学报, 2025, 47(9): 3374–3384. doi: 10.11999/JEIT250053. YI Maoxiang, ZHANG Jiatong, LU Yingchun, et al. A test vector CODEC scheme based on BRAM-segmented synchronous table lookup[J]. Journal of Electronics & Information Technology, 2025, 47(9): 3374–3384. doi: 10.11999/JEIT250053.
[25]	CHAO Zhiteng, ZHANG Xindi, ZHANG Xinyu, et al. PastATPG: A hybrid ATPG framework for better test compaction with partial assignment SAT[C]. Proceedings of the 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2025: 1–7. doi: 10.1109/DAC63849.2025.11132425.
[26]	FAZEKAS K, NIEMETZ A, PREINER M, et al. Satisfiability modulo user propagators[J]. Journal of Artificial Intelligence Research, 2024, 81: 989–1017. doi: 10.1613/jair.1.16163.
[27]	QIAN Yuhang, CHEN Zhihan, ZHANG Xindi, et al. X-SAT: An efficient circuit-based SAT solver[C]. 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2025: 1–7. doi: 10.1109/DAC63849.2025.11132604.
[28]	ZHANG Yu, ZHEN Huiling, YUAN Mingxuan, et al. DiffSAT: Differential MaxSAT layer for SAT solving[C]. Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design, Newark, USA, 2024: 114. doi: 10.1145/3676536.3676748.
[29]	SHI Zhengyuan, JIANG Wentao, ZHANG Xindi, et al. DynamicSAT: Dynamic configuration tuning for SAT solving[C]. Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming (CP), Glasgow, Scotland, 2025: 34. doi: 10.4230/LIPIcs.CP.2025.34.
[30]	ZHOU Shuai, ZHANG Weikang, ZHANG Xindi, et al. Parallel dynamic partitioning for datapath combinational equivalence checking[C]. Proceedings of the 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2025: 1–7. doi: 10.1109/DAC63849.2025.11132837.