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

YAN Dapeng; HE Qirun; GUO Jing; WANG Boning; CAI Zhikuang

doi:10.11999/JEIT260025

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2026 >

YAN Dapeng, HE Qirun, GUO Jing, WANG Boning, CAI Zhikuang. Optimizing SAT-Based ATPG Systems: Unified Fault Set Construction, Modeling, and Solving[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260025

Citation:

YAN Dapeng, HE Qirun, GUO Jing, WANG Boning, CAI Zhikuang. Optimizing SAT-Based ATPG Systems: Unified Fault Set Construction, Modeling, and Solving[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260025

Citation:

PDF( 2039 KB)

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

doi: 10.11999/JEIT260025 cstr: 32379.14.JEIT260025

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

Received Date: 2026-01-08
Accepted Date: 2026-03-24
Rev Recd Date: 2026-03-11

Available Online: 2026-04-19

Abstract

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

FullText(HTML)

References(30)

References

[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.