Computation of minimal unsatisfiable subformulas for SAT-based digital circuit error diagnosis

Abstract

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.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20
Fig. 21

References

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

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

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

    MathSciNet  Article  MATH  Google Scholar 

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

    Article  Google Scholar 

  5. Becker AJ (2018) Satisfiability-based methods for digital circuit design, debug, and optimization EPFL https://doi.org/10.5075/epfl-thesis-8850

    Article  Google Scholar 

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

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

  8. Bendík J, Cerna I (2018) Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets. In: LPAR. 131–142.

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

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

    Article  Google Scholar 

  11. Bryan D (1985) The ISCAS'85 benchmark circuits and netlist format. North Carolina State University pp 25

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

    Article  Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. Dave AH (2018) Application of machine learning in digital logic circuit design verification and testing. Doctoral dissertation, California State University, Fresno.

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

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

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

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

  20. Gómez LIR (2017) Machine learning support for logic diagnosis. Doctoral dissertation, University of Stuttgart.

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

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

  23. Koitz-Hristov R, Wotawa F (2018) On the superiority of conflict-driven search in MUs enumeration. In: CEUR workshop proceedings, 2289.

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

    MathSciNet  Article  Google Scholar 

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

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

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

    MathSciNet  Article  MATH  Google Scholar 

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

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

    Article  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

  32. Nadel A, Ryvchin V, Strichman O (2014) Accelerated deletion-based extraction of minimal unsatisfiable cores. J Satisfiability Boolean Modeling Comput 9: 27–51

    MathSciNet  Article  Google Scholar 

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

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  36. Ren Z, Al-Asaad H (2016) Overview of assertion-based verification and its applications. In: Int'l conf. embedded systems, cyber-physical systems, & applications

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

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

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

    Article  Google Scholar 

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

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

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

  43. da Silva PFM (2010) Max-SAT algorithms for real world instances. Master Dissertation.

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to Lamya Gaber.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Minimal unsatisfiable subsets
  • Minimal correction subsets
  • SAT solving
  • Conjunction normal form
  • GPU
  • Boolean satisfiability problem