{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:40:48Z","timestamp":1740123648532,"version":"3.37.3"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,6,26]],"date-time":"2021-06-26T00:00:00Z","timestamp":1624665600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,26]],"date-time":"2021-06-26T00:00:00Z","timestamp":1624665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10836-021-05956-y","type":"journal-article","created":{"date-parts":[[2021,6,26]],"date-time":"2021-06-26T09:02:31Z","timestamp":1624698151000},"page":"561-567","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits"],"prefix":"10.1007","volume":"37","author":[{"given":"Mishal Fatima","family":"Minhas","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2562-2669","authenticated-orcid":false,"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,6,26]]},"reference":[{"key":"5956_CR1","doi-asserted-by":"crossref","unstructured":"Hasan O, Tahar S (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition. IGI Global, pp. 7162\u20137170","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"issue":"2","key":"5956_CR2","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1109\/TCAD.2017.2705049","volume":"37","author":"S Shiraz","year":"2018","unstructured":"Shiraz S, Hasan O (2018) A HOL library for hardware verification using theorem proving. IEEE Trans Comput Aided Des Integr Circuits Syst 37(2):512\u2013516","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"issue":"12","key":"5956_CR3","doi-asserted-by":"publisher","first-page":"2131","DOI":"10.1109\/TCAD.2016.2547898","volume":"35","author":"C Yu","year":"2016","unstructured":"Yu C, Brown W, Liu D, Rossi A, Ciesielski M (2016) Formal verification of arithmetic circuits by function extraction. IEEE Trans Comput Aided Des Integr Circuits Syst 35(12):2131\u20132142","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"5956_CR4","doi-asserted-by":"crossref","unstructured":"Chandrasekharan A, Soeken M, Gro\u00dfe D, Drechsler R (2016) Precise error determination of approximated components in sequential circuits with model checking. In Design Automation Conference, ACM, p. 129","DOI":"10.1145\/2897937.2898069"},{"issue":"1","key":"5956_CR5","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.microrel.2014.09.025","volume":"55","author":"GB Hamad","year":"2015","unstructured":"Hamad GB, Hasan SR, Mohamed OA, Savaria Y (2015) Characterizing, modeling, and analyzing soft error propagation in asynchronous and synchronous digital circuits. Microelectron Reliab 55(1):238\u2013250","journal-title":"Microelectron Reliab"},{"issue":"3","key":"5956_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s10817-016-9363-7","volume":"56","author":"G Klein","year":"2016","unstructured":"Klein G, Gamboa R (2016) Interactive theorem proving. J Autom Reason 56(3):201\u2013203","journal-title":"J Autom Reason"},{"key":"5956_CR7","doi-asserted-by":"crossref","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking, vol. 10. Springer","DOI":"10.1007\/978-3-319-10575-8"},{"key":"5956_CR8","doi-asserted-by":"crossref","unstructured":"Guo X, Dutta RG, Mishra P, Jin Y (2016) Scalable SoC trust verification using integrated theorem proving and model checking. In Hardware Oriented Security and Trust, pp. 124\u2013129","DOI":"10.1109\/HST.2016.7495569"},{"key":"5956_CR9","doi-asserted-by":"crossref","unstructured":"Seidel PM (2014) A case for multi-level combination of theorem proving and model checking tools. In Microprocessor Test and Verification, pp. 90\u201397","DOI":"10.1109\/MTV.2014.29"},{"key":"5956_CR10","doi-asserted-by":"crossref","unstructured":"Chau C, Hunt WA, Roncken M, Sutherland I (201) A framework for asynchronous circuit modeling and verification in ACL2. In Haifa Verification Conference, Springer, pp. 3\u201318","DOI":"10.1007\/978-3-319-70389-3_1"},{"key":"5956_CR11","doi-asserted-by":"crossref","unstructured":"Russinoff DM (2019) Formal verification of floating-point hardware design: A mathematical approach. Springer","DOI":"10.1007\/978-3-319-95513-1"},{"key":"5956_CR12","unstructured":"Bozzano M, Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2019) nuXmv 2.0.0 User Manual"},{"key":"5956_CR13","doi-asserted-by":"crossref","unstructured":"Irfan A, Cimatti A, Griggio A, Roveri M, Sebastiani R (2016) Verilog2SMV: A tool for word-level verification. In Design, Automation & Test in Europe, pp. 1156\u20131159","DOI":"10.3850\/9783981537079_0765"},{"key":"5956_CR14","doi-asserted-by":"crossref","unstructured":"Minhas M, Hasan O, Saghar K (2018) Ver2Smv - A tool for verilog to SMV translation for verifying digital circuits. In Engineering and Emerging Technologies, pp. 1\u20135","DOI":"10.1109\/ICEET1.2018.8338617"},{"key":"5956_CR15","doi-asserted-by":"crossref","unstructured":"Vasudevan S, Liu L, Hertz S (2019) A comparative study of assertion mining algorithms in GoldMine. In Machine Learning in VLSI Computer-Aided Design. Springer, pp. 609\u2013645","DOI":"10.1007\/978-3-030-04666-8_20"},{"key":"5956_CR16","doi-asserted-by":"crossref","unstructured":"Zhang T, Saab D, Abraham JA (2017) Automatic assertion generation for simulation, formal verification and emulation. In VLSI, pp. 471\u2013476","DOI":"10.1109\/ISVLSI.2017.88"},{"key":"5956_CR17","doi-asserted-by":"crossref","unstructured":"Mehta AB (2018) SystemVerilog Assertions (SVA). In ASIC\/SoC Functional Design Verification. Springer, pp. 75\u2013128","DOI":"10.1007\/978-3-319-59418-7_6"},{"key":"5956_CR18","unstructured":"Wolf C, Glaser J, Kepler J (2013) Yosys - A free Verilog synthesis suite. In 21st Austrian Workshop on Microelectronics (Austrochip)"},{"key":"5956_CR19","unstructured":"Opencores.\u00a0https:\/\/www.opencores.org"},{"key":"5956_CR20","unstructured":"Verilog counterexample guided abstraction and refinement (VCEGAR). https:\/\/www.cs.cmu.edu\/modelcheck\/vcegar\/"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-021-05956-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10836-021-05956-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-021-05956-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T05:06:31Z","timestamp":1636693591000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10836-021-05956-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,26]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["5956"],"URL":"https:\/\/doi.org\/10.1007\/s10836-021-05956-y","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"type":"print","value":"0923-8174"},{"type":"electronic","value":"1573-0727"}],"subject":[],"published":{"date-parts":[[2021,6,26]]},"assertion":[{"value":"25 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 June 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}