{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:23:08Z","timestamp":1787592188003,"version":"build-2736575974"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Despite numerous previous formalisation projects targeting Verilog, the semantics of Verilog defined by the Verilog standard \u2013 Verilog\u2019s simulation semantics \u2013 has thus far eluded definitive mathematical formalisation. Previous projects on formalising the semantics have made good progress but no previous project provides a formalisation that can be used to execute or formally reason about real-world hardware designs. In this paper, we show that the reason for this is that the Verilog standard is inconsistent both with Verilog practice and itself. We pinpoint a series of problems in the Verilog standard that we have identified in how the standard defines the semantics of the subset of Verilog used to describe hardware designs, that is, the synthesisable subset of Verilog. We show how the most complete Verilog formalisation to date inherits these problems and how, after we repair these problems in an executable implementation of the formalisation, the repaired implementation can be used to execute real-world hardware designs. The existing formalisation together with the repairs hence constitute the first formalisation of Verilog\u2019s simulation semantics compatible with real-world hardware designs. Additionally, to make the results of this paper accessible to a wider (nonmathematical) audience, we provide a visual formalisation of Verilog\u2019s simulation semantics.<\/jats:p>","DOI":"10.1145\/3720484","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1295-1320","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The Simulation Semantics of Synthesisable Verilog"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9564-4663","authenticated-orcid":false,"given":"Andreas","family":"L\u00f6\u00f6w","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"[n. d.]. cocotb website. https:\/\/cocotb.org."},{"key":"e_1_3_1_3_2","unstructured":"[n. d.]. Icarus Verilog website. http:\/\/iverilog.icarus.com."},{"key":"e_1_3_1_4_2","unstructured":"[n. d.]. Ohm website. https:\/\/ohmjs.org."},{"key":"e_1_3_1_5_2","unstructured":"[n. d.]. React website. https:\/\/react.dev."},{"key":"e_1_3_1_6_2","unstructured":"[n. d.]. ReScript website. https:\/\/rescript-lang.org."},{"key":"e_1_3_1_7_2","unstructured":"[n. d.]. Verilator website. https:\/\/veripool.org\/verilator."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"1996. IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Std 1364-1995 (1996). doi:10.1109\/IEEESTD.1996.81542","DOI":"10.1109\/IEEESTD.1996.81542"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"2005. Verilog Register Transfer Level Synthesis. IEEE Std 62142-2005 (2005). doi:10.1109\/IEEESTD.2005.339572","DOI":"10.1109\/IEEESTD.2005.339572"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"2006. IEEE Standard for Verilog Hardware Description Language. IEEE Std 1364-2005 (2006). doi:10.1109\/IEEESTD.2006.99495","DOI":"10.1109\/IEEESTD.2006.99495"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"2024. IEEE Standard for SystemVerilog-Unified Hardware Design Specification and Verification Language. IEEE Std 1800-2023 (2024). doi:10.1109\/IEEESTD.2024.10458102","DOI":"10.1109\/IEEESTD.2024.10458102"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Martin Bodin Arthur Chargueraud Daniele Filaretti Philippa Gardner Sergio Maffeis Daiva Naudziuniene Alan Schmitt and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. In Symposium on Principles of Programming Languages. doi:10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Jonathan P. Bowen He Jifeng and Xu Qiwen. 2000. An animatable operational semantics of the Verilog hardware description language. In International Conference on Formal Engineering Methods. doi:10.1109\/ICFEM.2000.873820","DOI":"10.1109\/ICFEM.2000.873820"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622805"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Qinlin Chen Nairen Zhang Jinpeng Wang Tian Tan Chang Xu Xiaoxing Ma and Yue Li. 2023. The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog (Artifact). doi:10.5281\/zenodo.10020331","DOI":"10.5281\/zenodo.10020331"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Frank DeRemer and Hans Kron. 1975. Programming-in-the Large versus Programming-in-the-Small. In Proceedings of the International Conference on Reliable Software. doi:10.1145\/800027.808431","DOI":"10.1145\/800027.808431"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3386337"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Michael Gordon. 1995. The Semantic Challenge of Verilog HDL. In Symposium on Logic in Computer Science. doi:10.1109\/LICS.1995.523251","DOI":"10.1109\/LICS.1995.523251"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"He Jifeng and Zhu Huibiao. 2000. Formalising Verilog. In International Conference on Electronics Circuits and Systems. doi:10.1109\/ICECS.2000.911568","DOI":"10.1109\/ICECS.2000.911568"},{"key":"e_1_3_1_20_2","volume-title":"An Operational Semantics of a Simulator Algorithm","author":"Jifeng He","year":"2000","unstructured":"He Jifeng and Xu Qiwen. 2000. An Operational Semantics of a Simulator Algorithm. Technical Report 204. International Institute for Software Technology, United Nations University."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w. 2022. A small but important concurrency problem in Verilog\u2019s semantics?. In Conference on Formal Methods and Models for System Design. doi:10.1109\/MEMOCODE57689.2022.9954591","DOI":"10.1109\/MEMOCODE57689.2022.9954591"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w. 2025. The Simulation Semantics of Synthesisable Verilog (Artefact). doi:10.5281\/zenodo.14708857","DOI":"10.5281\/zenodo.14708857"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w. 2025. The Simulation Semantics of Synthesisable Verilog (Extended Version). (2025). doi:10.48550\/arXiv.2502.19348","DOI":"10.48550\/arXiv.2502.19348"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Marek Materzok. 2019. DigitalJS: A Visual Verilog Simulator for Teaching. In Computer Science Education Research Conference. doi:10.1145\/3375258.3375272","DOI":"10.1145\/3375258.3375272"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Kayvan Memarian Justus Matthiesen James Lingard Kyndylan Nienhuis David Chisnall Robert N. M. Watson and Peter Sewell. 2016. Into the Depths of C: Elaborating the de Facto Standards. In Conference on Programming Language Design and Implementation. doi:10.1145\/2908080.2908081","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Patrick Meredith Michael Katelman Jos\u00e9 Meseguer and Grigore Ro\u015fu. 2010. A Formal Executable Semantics of Verilog. In International Conference on Formal Methods and Models for Codesign. doi:10.1109\/MEMCOD.2010.5558634","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_3_1_28_2","unstructured":"Don Mills. 2012. Yet Another Latch and Gotchas Paper. In Synopsys Users Group Conference (SNUG)."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/TE.2008.919650"},{"key":"e_1_3_1_30_2","volume-title":"Hardware Design Based on Verilog HDL","author":"Pace Gordon J.","year":"1998","unstructured":"Gordon J. Pace. 1998. Hardware Design Based on Verilog HDL. Ph. D. Dissertation. Oxford University."},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_1_32_2","volume-title":"Towards an Operational Semantics of Verilog","author":"Schneider Gerardo","year":"1998","unstructured":"Gerardo Schneider and Xu Qiwen. 1998. Towards an Operational Semantics of Verilog. Technical Report 147. International Institute for Software Technology, United Nations University."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Gerardo Schneider and Qiwen Xu. 1998. Towards a Formal Semantics of Verilog Using Duration Calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems. doi:10.1007\/BFb0055355","DOI":"10.1007\/BFb0055355"},{"key":"e_1_3_1_34_2","volume-title":"A Uniform Semantics for Verilog and VHDL Suitable for Both Simulation and Verification","author":"Stewart Daryl","year":"2002","unstructured":"Daryl Stewart. 2002. A Uniform Semantics for Verilog and VHDL Suitable for Both Simulation and Verification. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-71715-9"},{"key":"e_1_3_1_36_2","unstructured":"Claire Wolf. [n. d.]. Yosys Open SYnthesis Suite. https:\/\/yosyshq.net\/yosys."},{"key":"e_1_3_1_37_2","unstructured":"Xilinx 2022. Vivado Design Suite User Guide: Getting Started (UG910 v2022.2). Xilinx."},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Huibiao Zhu Jonathan P. Bowen and He Jifeng. 2001. Deriving operational semantics from denotational semantics for Verilog. In Asia-Pacific Software Engineering Conference. doi:10.1109\/APSEC.2001.991475","DOI":"10.1109\/APSEC.2001.991475"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Huibiao Zhu Jifeng He and Jonathan P. Bowen. 2001. From Operational Semantics to Denotational Semantics for Verilog. In Correct Hardware Design and Verification Methods. doi:10.1007\/3-540-44798-9_34","DOI":"10.1007\/3-540-44798-9_34"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"Huibiao Zhu Jifeng He and Jonathan P. Bowen. 2006. From algebraic semantics to denotational semantics for Verilog. In International Conference on Engineering of Complex Computer Systems. doi:10.1109\/ICECCS.2006.1690363","DOI":"10.1109\/ICECCS.2006.1690363"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720484","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720484","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:25Z","timestamp":1787588965000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720484"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":39,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720484"],"URL":"https:\/\/doi.org\/10.1145\/3720484","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}