The explanation of infeasibilities formed in Minimal Unsatisfiable Subformulas (MUSes) is a core task in the analysis of over-constrained Boolean formulas. A wide range of applications necessitate MUS detection including knowledge-based validation, software design, verification and error diagnosis in digital VLSI circuits. Consequently, various enhanced algorithms for determining MUS have been utilized for solving Maximum Satisfiability algorithms and Conjunction Normal Form (CNF) redundancies. Three enhancements are proposed in this paper. The first is a CPU-GPU algorithm for computation of Minimal Correction Subsets (MCSes) optimized for NVIDIA General Purpose Graphics Processing Unit paradigm. The proposed algorithm of generating all MCSes from the encoded CNF instance was developed using our parallel SSGPU solver and implemented using CUDA. The second enhancement is an algorithm for MUS computation based on auto-reduction of the enhanced MCSes for faster MUS detection. The third improved algorithm is for computing MUS directly without using MCSes. The two proposed algorithms outperform techniques as they could locate and explain design faults in digital VLSI circuits in earlier stages of IC design flow. The second proposed routine of MUS extraction was performed by avoiding a non-critical step in calling the SAT solver during MUS computation, leading to improving the performance of the MUS extraction algorithm. The third proposed mechanism for direct extraction of MUS was optimized by reducing the required SAT-solver calls using a classification of clauses in the input formula. Comparative analysis of the proposed algorithm against the Compute All Minimal Unsatisfiable Subsets (CAMUS) algorithm determined 1.54 × faster detection of MUS using ISCAS'85, ISCAS'89 and synthetic benchmarks. Also, the third algorithm for direct MUS computation delivers 17.05 × faster than shrinking algorithm used in MUST (minimal unsatisfiable subset) tool using ISCAS'85 and synthetic benchmarks. Moreover, it was observed that the CPU-GPU algorithm for MCSes computation based on the SSGPU solver delivered 1.92 × faster than its conventional counterpart, based on CUD@SAT equivalent on GPU using ISCAS'85, ISCAS'89 and synthetic Benchmarks.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Ali LG, Hussein AI, Ali HM (2016) Parallelization of unit propagation algorithm for SAT-based ATPG of digital circuits. In: Microelectronics (ICM) 28th international conference 184–188. Doi: 10.1109/ICCES.2017.8275337.
Ali LG, Hussein AI, Ali HM (2017) An efficient computation of minimal correction subformulas for SAT-based ATPG of digital circuits. In: Computer engineering and systems (ICCES), 12th international conference, pp 383–389. doi: 10.1109/ICCES.2017.8275337.
Alizadeh B, Behnam P, Sadeghi-Kohan S (2014) A scalable formal debugging approach with auto-correction capability based on static slicing and dynamic ranking for RTL datapath designs. IEEE Trans Comput 64(6):1564–1578 https://doi.org/10.1109/TC.2014.2329687
Asahiro Y, Iwama K, Miyano E (1996) Random generation of test instances with controlled attributes. DIMACS Ser Discrete Math Theoretical Comput Sci 26:377–394
Becker AJ (2018) Satisfiability-based methods for digital circuit design, debug, and optimization EPFL https://doi.org/10.5075/epfl-thesis-8850
Belov A, Heule M J, Marques-Silva J (2014). MUS extraction using clausal proofs. International Conference on Theory and Applications of Satisfiability Testing, 48-57. https://doi.org/10.1007/978-3-319-09284-3_5
Bendík J, Černá I , Beneš N. (2018). Recursive online enumeration of all minimal unsatisfiable subsets. In: International symposium on automated technology for verification and analysis, pp 143–159.
Bendík J, Cerna I (2018) Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets. In: LPAR. 131–142.
Bendík J, Černá I (2020) MUST: Minimal Unsatisfiable Subsets Enumeration Tool. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 135-152. https://doi.org/10.1007/978-3-030-45190-5_8
Berre Le D, Parrain A (2010) The Sat4j library, release 2.2. J Satisfiability Boolean Modeling Comput 7:59–64 https://doi.org/10.3233/SAT190075
Bryan D (1985) The ISCAS'85 benchmark circuits and netlist format. North Carolina State University pp 25
Cai S, Gallina B, Nyström D, Seceleanu C, Larsson A (2019) Tool-supported design of data aggregation processes in cloud monitoring systems. J Ambient Intell Human Comput 10:2519–2535 https://doi.org/10.1007/s12652-018-0730-6
Chen Y, Safarpour S, Marques-Silva J, Veneris A (2010) Automated design debugging with maximum satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 29(11):1804–1817 https://doi.org/10.1109/TCAD.2010.2061270
Corno F, Razzak F (2014) SAT based enforcement of domotic effects in smart environments. J Ambient Intell Human Comput 5:565–579 https://doi.org/10.1007/s12652-013-0183-x
Dave AH (2018) Application of machine learning in digital logic circuit design verification and testing. Doctoral dissertation, California State University, Fresno.
De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems, 337–340.
Fossé R, Simon L (2018) On the non-degeneracy of unsatisfiability proof graphs produced by SAT solvers. In: International conference on principles and practice of constraint programming, 128–143.
Gaber L, Hussein AI, Moness M (2019) Improved automatic correction for digital VLSI circuits. In: 2019 31st international conference on microelectronics (ICM) 18–22. 10.1109/ICM48031.2019.9021938
Guthmann O, Strichman O, Trostanetski A (2016) Minimal unsatisfiable core extraction for SMT. In: 2016 Formal methods in computer-aided design (FMCAD), 57–64. Doi: 10.5555/3077629.3077644
Gómez LIR (2017) Machine learning support for logic diagnosis. Doctoral dissertation, University of Stuttgart.
Hagihara S, Egawa N, Shimakawa M, Yonezaki N (2014). Minimal strongly unsatisfiable subsets of reactive system specifications. Proceedings of the 29th ACM/IEEE international conference on Automated software engineering 629–634.
Ignatiev A, Previti A, Liffiton M, Marques-Silva J (2015) Smallest MUS extraction with minimal hitting set dualization. In: Pesant G (ed), Principles and practice of constraint programming: 21st international conference, CP 2015 Cork, Ireland, 9255: 173–182. Springer doi: 10.1007/978–3–319–23219–5_13
Koitz-Hristov R, Wotawa F (2018) On the superiority of conflict-driven search in MUs enumeration. In: CEUR workshop proceedings, 2289.
Konnov I, Veith H, Widder J (2017) On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf Comput 252:95–109
Leo K, Tack G (2017) Debugging unsatisfiable constraint models. In: International conference on AI and OR techniques in constraint programming for combinatorial optimization problems. 77–93.
Li J, Zhu S, Zhang Y, Pu G, Vari MY (2017) Safety model checking with complementary approximations. In: Proceedings of the 36th international conference on computer-aided design. 95–100.
Liffiton MH, Previti A, Malik A, Silva JM (2016) Fast, flexible MUS enumeration Constraints 21:223–250 https://doi.org/10.1007/s10601-015-9183-0
Liffiton MH, Malik A (2013) Enumerating infeasibility: finding multiple MUSes quickly. In: International conference on AI and OR techniques in constriant programming for combinatorial optimization problems, 160–175. Doi: 10.1007/978–3–642–38171–3_11
Mandouh E, Wassal AG (2018) Application of machine learning techniques in post-silicon debugging and bug localization J. Electron. Test. 34(2) 163–181 https://doi.org/10.1007/s10836-018-5716-y
Marques-Silva J (2012) Computing minimally unsatisfiable subformulas: state of the art and future directions. J Multiple Valued Logic Soft Comput 19(1):163–183
Marques-Silva J, Janota M, Belov A (2013) . Minimal sets over monotone predicates in boolean formulae. International Conference on Computer Aided Verification, 592-607. https://doi.org/10.1007/978-3-642-39799-8_39
Nadel A, Ryvchin V, Strichman O (2014) Accelerated deletion-based extraction of minimal unsatisfiable cores. J Satisfiability Boolean Modeling Comput 9: 27–51
Narodytska N, Bjørner N, Marinescu M-C, Sagiv M (2018). Core-Guided Minimal Correction Set and Core Enumeration. In: IJCAI, 1353–1361. https://doi.org/10.24963/ijcai.2018/188
Osama M, Gaber L, Hussein AI, Mahmoud H (2018) An efficient SAT-based test generation algorithm with GPU accelerator J Electron Testing 34:511–527 https://doi.org/10.1007/s10836-018-5747-4
Palù Dal A, Dovier A, Formisano A, Pontelli E (2014) Cud@ sat: sat solving on gpus J Exp Theor Artif Intell 27:293–316 https://doi.org/10.1080/0952813X.2014.954274
Ren Z, Al-Asaad H (2016) Overview of assertion-based verification and its applications. In: Int'l conf. embedded systems, cyber-physical systems, & applications
Shi J, Fey G, Drechsler R, Glowatz A, Hapke F, Schloffel J, PASSAT (2005) Efficient SAT-based test pattern generation for industrial circuits. In: IEEE computer society annual symposium on VLSI: new frontiers in VLSI Design (ISVLSI'05), 212–217. Doi: 10.1109/ISVLSI.2005.55
Shimakawa M, Hagihara S, Yonezaki N (2018) Efficiency of the strong satisfiability checking procedure for reactive system specifications. In: AIP conference proceedings, 1955(1). Doi: 10.1063/1.5033715.
AA Sohanghpurwala MW Hassan P Athanas 2017 Hardware accelerated SAT solvers—a survey J Parallel Distributed Comput 106: 170–184 https://doi.org/10.1016/j.jpdc.2016.12.014
Zhang J, Li T, S. Li, (2015). Application and analysis of unsatisfiable cores on circuits synthesis, Seventh International Conference on Advanced Computational Intelligence (ICACI): 407–410, doi: 10.1109/ICACI.2015.7184740.
Zhendong L, Shaowei C (2018) Solving (weighted) partial MaxSAT by dynamic local search for SAT. In: Proceedings of the 27th international joint conference on artificial intelligence (IJCAI’18), AAAI Press, 1346–1352.
Zielke C, Kaufmann M (2015) A new approach to partial MUS enumeration. International Conference on Theory and Applications of Satisfiability Testing, 387-404. https://doi.org/10.1007/978-3-319-24318-4_28
da Silva PFM (2010) Max-SAT algorithms for real world instances. Master Dissertation.
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
About this article
Cite this article
Gaber, L., Hussein, A.I., Mahmoud, H. et al. Computation of minimal unsatisfiable subformulas for SAT-based digital circuit error diagnosis. J Ambient Intell Human Comput (2020). https://doi.org/10.1007/s12652-020-02247-w
- Minimal unsatisfiable subsets
- Minimal correction subsets
- SAT solving
- Conjunction normal form
- Boolean satisfiability problem