{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T16:39:29Z","timestamp":1772642369603,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"The Natural Science Foundation of China","award":["62025202,62002157,61932021"],"award-info":[{"award-number":["62025202,62002157,61932021"]}]},{"name":"Jiangsu Natural Science Foundation","award":["BK20202001"],"award-info":[{"award-number":["BK20202001"]}]},{"name":"The Fundamental Research Funds for the Central Universities of China","award":["020214380102, 020214912220"],"award-info":[{"award-number":["020214380102, 020214912220"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>\n            With the increasing need to apply modern software techniques to hardware design, Verilog, the most popular Hardware Description Language (HDL), plays an infrastructure role. However, Verilog has several semantic pitfalls that often confuse software and hardware developers. Although prior research on formal semantics for Verilog exists, it is not comprehensive and has not fully addressed these issues. In this work, we present a novel scheme inspired by previous work on defining core languages for software languages like JavaScript and Python. Specifically, we define the formal semantics of Verilog using a core language called \u03bb\n            <jats:sub>\n              <jats:italic>V<\/jats:italic>\n            <\/jats:sub>\n            , which captures the essence of Verilog using as few language structures as possible. \u03bb\n            <jats:sub>\n              <jats:italic>V<\/jats:italic>\n            <\/jats:sub>\n            not only covers the most complete set of language features to date, but also addresses the aforementioned pitfalls. We implemented \u03bb\n            <jats:sub>\n              <jats:italic>V<\/jats:italic>\n            <\/jats:sub>\n            with about 27,000 lines of Java code, and comprehensively tested its totality and conformance with Verilog. As a reliable reference semantics, \u03bb\n            <jats:sub>\n              <jats:italic>V<\/jats:italic>\n            <\/jats:sub>\n            can detect semantic bugs in real-world Verilog simulators and expose ambiguities in Verilog\u2019s standard specification. Moreover, as a useful core language, \u03bb\n            <jats:sub>\n              <jats:italic>V<\/jats:italic>\n            <\/jats:sub>\n            has the potential to facilitate the development of tools such as a state-space explorer and a concolic execution tool for Verilog.\n          <\/jats:p>","DOI":"10.1145\/3622805","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"234-263","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5498-5927","authenticated-orcid":false,"given":"Qinlin","family":"Chen","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3737-8768","authenticated-orcid":false,"given":"Nairen","family":"Zhang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9099-4262","authenticated-orcid":false,"given":"Jinpeng","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3792-1237","authenticated-orcid":false,"given":"Tian","family":"Tan","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6299-4704","authenticated-orcid":false,"given":"Chang","family":"Xu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7970-1384","authenticated-orcid":false,"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1285-2298","authenticated-orcid":false,"given":"Yue","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2006.99495"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342260"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872414"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218632"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8320642"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8321324"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2001.991473"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80282-8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_12_1","volume-title":"Language wars in the 21st century: verilog versus vhdl\u2013revisited","author":"Golson Steve","unstructured":"Steve Golson and Leah Clark . 2016. Language wars in the 21st century: verilog versus vhdl\u2013revisited . Synopsys Users Group (SNUG) . Steve Golson and Leah Clark. 2016. Language wars in the 21st century: verilog versus vhdl\u2013revisited. Synopsys Users Group (SNUG)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523251"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/45.1.27"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.3390\/electronics7060081"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000","author":"He Jifeng","year":"2000","unstructured":"Jifeng He and Qiwen Xu . 2000 . An Operational Semantics of a Simulator Algorithm . In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000 , June 24-29, 2000, Las Vegas, Nevada, USA, Hamid R. Arabnia (Ed.). CSREA Press. Jifeng He and Qiwen Xu. 2000. An Operational Semantics of a Simulator Algorithm. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000, June 24-29, 2000, Las Vegas, Nevada, USA, Hamid R. Arabnia (Ed.). CSREA Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECS.2000.911568"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485494"},{"key":"e_1_2_1_20_1","volume-title":"Published in the proceedings of the ICS2000","author":"Huibiao Zhu","year":"2000","unstructured":"Zhu Huibiao and He Jifeng . 2000 . A DC-based Semantics for Verilog . In Published in the proceedings of the ICS2000 , Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing. 421\u2013432. Zhu Huibiao and He Jifeng. 2000. A DC-based Semantics for Verilog. In Published in the proceedings of the ICS2000, Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing. 421\u2013432."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203780"},{"key":"e_1_2_1_22_1","volume-title":"Computer-aided reasoning: ACL2 case studies. 4","author":"Kaufmann Matt","unstructured":"Matt Kaufmann , Panagiotis Manolios , and J Strother Moore . 2013. Computer-aided reasoning: ACL2 case studies. 4 , Springer Science & Business Media . Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. 2013. Computer-aided reasoning: ACL2 case studies. 4, Springer Science & Business Media."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2678015.2678016"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2019.9"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE57689.2022.9954591"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2019.00020"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3066560"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"e_1_2_1_30_1","unstructured":"Terence Parr. 2013. The definitive ANTLR 4 reference. The Definitive ANTLR 4 Reference 1\u2013326. \t\t\t\t  Terence Parr. 2013. The definitive ANTLR 4 reference. The Definitive ANTLR 4 Reference 1\u2013326."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384577.2384579"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509536"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386024"},{"key":"e_1_2_1_34_1","unstructured":"Wilson Snyder. 2023. Verilator. https:\/\/veripool.org\/verilator\/documentation\/ \t\t\t\t  Wilson Snyder. 2023. Verilator. https:\/\/veripool.org\/verilator\/documentation\/"},{"key":"e_1_2_1_35_1","unstructured":"Wilson Snyder. 2023. vppreproc. https:\/\/metacpan.org\/dist\/Verilog-Perl\/view\/vppreproc \t\t\t\t  Wilson Snyder. 2023. vppreproc. https:\/\/metacpan.org\/dist\/Verilog-Perl\/view\/vppreproc"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2019.7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_1_38_1","unstructured":"Stephen Williams. 2023. Icarus Verilog. https:\/\/steveicarus.github.io\/iverilog\/ \t\t\t\t  Stephen Williams. 2023. Icarus Verilog. https:\/\/steveicarus.github.io\/iverilog\/"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510578"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0069-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622805","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622805"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":40,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622805"],"URL":"https:\/\/doi.org\/10.1145\/3622805","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}