{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:09:14Z","timestamp":1765544954566,"version":"build-2065373602"},"reference-count":59,"publisher":"MDPI AG","issue":"6","license":[{"start":{"date-parts":[[2024,6,9]],"date-time":"2024-06-09T00:00:00Z","timestamp":1717891200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>Digital systems are nowadays ubiquitous and often comprise an extremely high level of complexity. Guaranteeing the correct behavior of such systems has become an ever more pressing need for manufacturers. The correctness of digital systems can be addressed resorting to formal verification techniques, such as model checking. Currently, it is usually impossible to determine a priori the best algorithm to use given a verification task and, thus, portfolio approaches have become the de facto standard in model checking verification suites. This paper describes the most relevant algorithms and techniques, at the foundations of bit-level SAT-based model checking itself.<\/jats:p>","DOI":"10.3390\/a17060253","type":"journal-article","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T08:59:06Z","timestamp":1718009946000},"page":"253","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Hardware Model Checking Algorithms and Techniques"],"prefix":"10.3390","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5839-8697","authenticated-orcid":false,"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[{"name":"DAUIN, Department of Control and Computer Engineering, Politecnico di Torino, 10129 Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2476-2160","authenticated-orcid":false,"given":"Paolo Enrico","family":"Camurati","sequence":"additional","affiliation":[{"name":"DAUIN, Department of Control and Computer Engineering, Politecnico di Torino, 10129 Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0605-9014","authenticated-orcid":false,"given":"Marco","family":"Palena","sequence":"additional","affiliation":[{"name":"CNIT, National Inter-University Consortium for Telecommunications, 10129 Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6233-0994","authenticated-orcid":false,"given":"Paolo","family":"Pasini","sequence":"additional","affiliation":[{"name":"DET, Department of Electronics and Telecommunications, Politecnico di Torino, 10129 Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2024,6,9]]},"reference":[{"key":"ref_1","unstructured":"Foster, H. (2024, June 06). 2022 Wilson Research Group FPGA Functional Verification Trends. Available online: https:\/\/www.innofour.com\/static\/default\/files\/documents\/pdf\/fpga-trend-report_2022-wilson-research-verification-study_hfoster.pdf."},{"key":"ref_2","unstructured":"Rashinkar, P., Paterson, P., and Singh, L. (2013). System-on-a-Chip Verification: Methodology and Techniques, Springer."},{"key":"ref_3","first-page":"181","article-title":"Some key research problems in automated theorem proving for hardware and software verification","volume":"98","author":"Kaufmann","year":"2004","journal-title":"Math. J. Span. R. Acad. Sci."},{"key":"ref_4","unstructured":"Boyer, R.S., and Moore, J.S. (1988). A Computational Logic Handbook, Academic Press Professional, Inc.. [1st ed.]."},{"key":"ref_5","unstructured":"Harrison, J. (2008, January 7\u201314). Theorem Proving for Verification (Invited Tutorial). Proceedings of the 20th International Conference on Computer Aided Verification, CAV, Princeton, NJ, USA."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Somenzi, F., Hsu, C.J., and Bustan, D. (2016). Equivalence Checking. Electronic Design Automation for IC Implementation, Circuit Design, and Process Technology, CRC Press.","DOI":"10.1201\/b19714-6"},{"key":"ref_7","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","volume":"Volume 131","author":"Kozen","year":"1981","journal-title":"Logics of Programs"},{"key":"ref_8","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A., and Veith, H. (2018). Model Checking, MIT Press. [2nd ed.]."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-Based Algorithms for Boolean Function Manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"ref_10","unstructured":"Mishchenko, A. (2024, June 06). ABC: A System for Sequential Synthesis and Verification. Available online: http:\/\/people.eecs.berkeley.edu\/~alanmi\/abc\/."},{"key":"ref_11","unstructured":"Cabodi, G., Nocco, S., and Quer, S. (2024, June 06). PdTRAV: Politecnico di Torino Reachability Analysis & Verification. Available online: https:\/\/github.com\/polito-fmgroup\/pdtools."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/s10703-021-00369-1","article-title":"Certifying proofs for SAT-based model checking","volume":"57","author":"Griggio","year":"2021","journal-title":"Form. Methods Syst. Des."},{"key":"ref_13","unstructured":"Yu, E., Froleyks, N., Biere, A., and Heljanko, K. (2023, January 24\u201327). Towards Compositional Hardware Model Checking Certification. Proceedings of the Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA."},{"key":"ref_14","unstructured":"Biere, A., and Jussila, T. (2024, June 08). The Model Checking Competition. Available online: http:\/\/fmv.jku.at\/hwmcc."},{"key":"ref_15","unstructured":"Biere, A. (2020, January 21\u201324). Tutorial on World-Level Model Checking. Proceedings of the 2020 Formal Methods in Computer Aided Design (FMCAD), Online."},{"key":"ref_16","unstructured":"Palena, M. (2017). Exploiting Boolean Satisfiability Solvers for High Performance Bit-Level Model Checking. [Ph.D. Thesis, Politecnico di Torino]."},{"key":"ref_17","unstructured":"Pasini, P. (2017). Improving Bit-Level Model Checking Algorithms for Scalability through Circuit-Based Reasoning. [Ph.D. Thesis, Politecnico di Torino]."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R. (2018). Handbook of Model Checking, Springer. [1st ed.].","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., van Maaren, H., and Walsh, T. (2021). Handbook of Satisfiability, IOS Press. [2nd ed.]. Frontiers in Artificial Intelligence and Applications.","DOI":"10.3233\/FAIA336"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1421","DOI":"10.1109\/TCAD.2016.2633961","article-title":"Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities","volume":"36","author":"Seshia","year":"2017","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"ref_21","unstructured":"Barwise, J. (1977). Handbook of Mathematical Logic, Elsevier."},{"key":"ref_22","unstructured":"Hunter, G. (1973). Metalogic: An Introduction to the Metatheory of Standard First Order Logic, University of California Press. [1st ed.]. Macmillan Student Editions."},{"key":"ref_23","unstructured":"Hopcroft, J.E., Motwani, R., and Ullman, J.D. (2006). Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Longman Publishing Co., Inc.. [3rd ed.]."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Harrison, M.A., Banerji, R.B., and Ullman, J.D. (1971). The Complexity of Theorem-proving Procedures. Third Annual ACM Symposium on Theory of Computing, ACM.","DOI":"10.1145\/800157"},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A Machine Program for Theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"key":"ref_26","unstructured":"Marques Silva, J.P., and Sakallah, K.A. (1996, January 10\u201314). Grasp\u2014A New Search Algorithm for Satisfiability. Proceedings of the The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, San Jose, CA, USA."},{"key":"ref_27","unstructured":"Huang, J. (2007, January 6\u201312). The Effect of Restarts on the Efficiency of Clause Learning. Proceedings of the 20th International Joint Conference on Artifical Intelligence, IJCAI, Hyderabad, India."},{"key":"ref_28","unstructured":"Biere, A. (2011, January 6\u20138). Preprocessing and Inprocessing Techniques in SAT. Proceedings of the 7th International Haifa Verification Conference on Hardware and Software: Verification and Testing, HVC, Haifa, Israel."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","article-title":"Towards Understanding and Harnessing the Potential of Clause Learning","volume":"22","author":"Beame","year":"2004","journal-title":"J. Artif. Intell. Res."},{"key":"ref_30","unstructured":"Goldberg, E., and Novikov, Y. (2003, January 3\u20137). Verification of Proofs of Unsatisfiability for CNF Formulas. Proceedings of the 2003 Design, Automation and Test in Europe Conference, DATE, Munich, Germany."},{"key":"ref_31","unstructured":"Zhang, L., and Malik, S. (2003, January 3\u20137). Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. Proceedings of the 2003 Design, Automation and Test in Europe Conference, DATE, Munich, Germany."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., and Hunt, W.A. (2014, January 14\u201317). DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. Proceedings of the Theory and Applications of Satisfiability Testing\u2014SAT 2014: 17th International Conference, Vienna, Austria.","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","article-title":"A completeness theorem in modal logic","volume":"24","author":"Kripke","year":"1959","journal-title":"J. Symb. Log."},{"key":"ref_34","unstructured":"Pnueli, A. (November, January 31). The Temporal Logic of Programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, FOCS, Providence, RI, USA."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"Acm Trans. Program. Lang. Syst."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/s10009-017-0451-8","article-title":"To split or to group: From divide-and-conquer to sub-task sharing for verifying multiple properties in model checking","volume":"20","author":"Cabodi","year":"2018","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_37","unstructured":"Dureja, R., Baumgartner, J., Kanzelman, R., Williams, M., and Rozier, K.Y. (2020, January 21\u201324). Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. Proceedings of the 2020 Formal Methods in Computer Aided Design (FMCAD), Online."},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., and Zhu, Y. (1999, January 22\u201328). Symbolic Model Checking without BDDs. Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Amsterdam, The Netherlands.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., and St\u00e5lmarck, G. (2000, January 1\u20133). Checking Safety Properties Using Induction and a SAT-Solver. Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, FMCAD, Austin, TX, USA.","DOI":"10.1007\/3-540-40922-X_8"},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","article-title":"Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory","volume":"22","author":"Craig","year":"1957","journal-title":"J. Symb. Log."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Huang, G. (1995, January 24\u201326). Constructing Craig Interpolation Formulas. Proceedings of the First Annual International Conference on Computing and Combinatorics, COCOON, Xi\u2019an, China.","DOI":"10.1007\/BFb0030832"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2307\/2275541","article-title":"Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic","volume":"62","year":"1997","journal-title":"J. Symb. Log."},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","article-title":"Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations","volume":"62","year":"1997","journal-title":"J. Symb. Log."},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"McMillan, K.L. (2003, January 8\u201312). Interpolation and SAT-Based Model Checking. Proceedings of the 15th International Conference on Computer Aided Verification, CAV, Boulder, CO, USA.","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/s10703-015-0224-5","article-title":"Efficient generation of small interpolants in CNF","volume":"47","author":"Vizel","year":"2015","journal-title":"Form. Methods Syst. Des."},{"key":"ref_46","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., and Vizel, Y. (2014, January 21\u201324). DRUPing for Interpolants. Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design, FMCAD, Lausanne, Switzerland.","DOI":"10.1109\/FMCAD.2014.6987601"},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"1524","DOI":"10.1109\/TCAD.2019.2915317","article-title":"Reducing Interpolant Circuit Size Through SAT-Based Weakening","volume":"39","author":"Cabodi","year":"2020","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Bradley, A.R. (2011, January 23\u201325). SAT-Based Model Checking without Unrolling. Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Austin, TX, USA.","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s10703-017-0272-0","article-title":"SAT solver management strategies in IC3: An experimental approach","volume":"50","author":"Cabodi","year":"2017","journal-title":"Form. Methods Syst. Des."},{"key":"ref_50","unstructured":"E\u00e9n, N., Mishchenko, A., and Brayton, R. (November, January 30). Efficient Implementation of Property Directed Reachability. Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design, FMCAD, Austin, TX, USA."},{"key":"ref_51","unstructured":"Chockler, H., Ivrii, A., Matsliah, A., Moran, S., and Nevo, Z. (November, January 30). Incremental Formal Verification of Hardware. Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design, FMCAD, Austin, TX, USA."},{"key":"ref_52","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., and Manna, Z. (2007, January 11\u201314). Checking Safety by Inductive Generalization of Counterexamples to Induction. Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design, FMCAD, Austin, TX, USA.","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s10703-022-00406-7","article-title":"Interpolation with guided refinement: Revisiting incrementality in SAT-based unbounded model checking","volume":"60","author":"Cabodi","year":"2022","journal-title":"Form. Methods Syst. Des."},{"key":"ref_54","unstructured":"Mishchenko, A., and Brayton, R.K. (2005, January 7\u201311). SAT-Based Complete Don\u2019t-Care Computation for Network Optimization. Proceedings of the 2005 Design, Automation and Test in Europe Conference, DATE, Munich, Germany."},{"key":"ref_55","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Nocco, S., and Quer, S. (2011, January 14\u201318). Interpolation sequences revisited. Proceedings of the Design, Automation and Test in Europe, DATE 2011, Grenoble, France.","DOI":"10.1109\/DATE.2011.5763056"},{"key":"ref_56","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","article-title":"Benchmarking a model checker for algorithmic improvements and tuning for performance","volume":"39","author":"Cabodi","year":"2011","journal-title":"Form. Methods Syst. Des."},{"key":"ref_57","first-page":"135","article-title":"Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks","volume":"9","author":"Cabodi","year":"2016","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_58","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S. (1983). On the Complexity of Derivation in Propositional Calculus. Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, Springer.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., and Gupta, A. (2007). SAT-Based Scalable Formal Verification Solutions, Springer.","DOI":"10.1007\/978-0-387-69167-1"}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/17\/6\/253\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T14:56:10Z","timestamp":1760108170000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/17\/6\/253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,9]]},"references-count":59,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2024,6]]}},"alternative-id":["a17060253"],"URL":"https:\/\/doi.org\/10.3390\/a17060253","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2024,6,9]]}}}