Optimizing SATisfiability-Based Automatic Test Pattern Generation 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 > 2025 >

YAN Dapeng, HE Qirun, GUO Jing, WANG Boning, CAI Zhikuang. Optimizing SATisfiability-Based Automatic Test Pattern Generation 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 SATisfiability-Based Automatic Test Pattern Generation 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 SATisfiability-Based Automatic Test Pattern Generation Systems: Unified Fault Set Construction,Modeling, and Solving[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT260025

PDF( 2002 KB)

Optimizing SATisfiability-Based Automatic Test Pattern Generation 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-18

Available Online: 2026-04-19

Abstract

Abstract

Objective Boolean SATisfiability-Based Automatic Test Pattern Generation (SAT-Based ATPG) is widely used to generate tests for hard-to-detect single stuck-at faults and to prove fault untestability in combinational logic. When SAT-Based ATPG is applied to large netlists with dense fanout and reconvergence, its runtime and memory consumption are often dominated by three interacting issues. Representative fault lists produced by conventional dominance- or equivalence-based fault 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 Conjunctive Normal Form (CNF) overhead, especially when an explicit faulty-circuit copy is constructed or when propagation constraints are encoded globally without locality control. In addition, fanout-reconvergence structures amplify assignment correlations along sensitized paths, and such correlations are often exposed only after repeated decisions and backtracking when only standard unit propagation is used. The unified optimization objective is therefore to reduce overall CNF size and solving cost while preserving completeness, so that a practical SAT-Based ATPG system remains efficient and stable across circuits of different scales. Methods A three-part framework is developed and implemented in an incremental SAT-Based ATPG flow, and the overall workflow is illustrated (Fig. 1). First, a checkpoint-driven dynamic fault-set construction method is proposed. Checkpoints are collected during netlist-to-directed-acyclic-graph conversion, including all primary inputs and all fanout branches, and XOR/XNOR outputs are additionally recorded as supplementary checkpoints to avoid over-collapsing XOR-related fault behavior. Representative faults are initialized on checkpoints by compact rules that combine dominance-oriented fault collapsing with equivalence-aware refinement, and solver-guided repair is performed when an untestable representative fault indicates potential masking under structural constraints. The procedure is summarized in Algorithm 1. Second, a SAT modeling method based on fault sensitization constraints is adopted to avoid explicit faulty-circuit duplication. Fault activation, propagation, and observability are represented by additional fault sensitization constraints over the original circuit variables, and auxiliary variables are introduced only when local bookkeeping is required. Constraint localization is restricted to the fault fanout cone, and cone-boundary and internal vertices are identified through a graph-traversal procedure (Fig. 2). Third, a dynamic implication learning mechanism oriented to fanout-reconvergence pairs is integrated into the incremental solving loop. Reconvergence pairs within the fault fanout cone are monitored under partial assignments, and structure-induced implications are injected either as implied assignments when a reconvergent output becomes functionally determined or as short conflict clauses when a branch-value combination becomes inconsistent with the fault sensitization constraints. The dynamic implication learning procedure is summarized in 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 method substantially reduces the representative fault space entering ATPG. Relative 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%. The best-case ratio reaches 33.19% on large circuits with heavy reconvergence, which indicates that checkpoint-centered representative-fault allocation effectively suppresses redundancy without enlarging the untestable fault set (Table 1). The reduced fault-set size is reflected in preprocessing efficiency, and the total runtime for fault-set construction is consistently reduced, with an average reduction of 8.37% across the evaluated circuits (Fig. 3). For SAT model construction, the fault-sensitization-constraint encoding reduces CNF overhead relative to the baseline model construction. Across the benchmark set, the numbers of CNF clauses and CNF variables are reduced by 11.44% and 3.50%, respectively, which shows that avoiding explicit faulty-circuit duplication and localizing auxiliary constraints to the fault fanout cone effectively lowers memory demand (Table 2). The reduced CNF size and strengthened locality of constraints are further 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 in reconvergence-heavy structures. Compared with static implication learning, CNF construction time increases by 3.0% on average because of the additional monitoring and injection operations, yet the overall runtime decreases by 4.42% on average, which indicates a favorable cost-benefit trade-off. The overhead attributed to dynamic implication learning accounts for 2.51% of the total runtime aggregated across circuits, which confirms that the injected implications and pruning clauses provide measurable solving benefits at 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 dynamic implication learning. Representative faults are compressed through solver-guided repair of dominance and equivalence relations to avoid masking, CNF growth is controlled through duplication-free modeling localized to the fault fanout cone, and reconvergence correlations are exploited through incremental implication injection to strengthen propagation and enable 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-Based 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 P. 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 H and SHIMONO T. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. 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]. The 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, USA, 2025: 1–7. doi: 10.1109/DAC63849.2025.11132837.