{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:20:03Z","timestamp":1784830803575,"version":"3.55.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>In formal hardware verification, particularly for Register-Transfer Level (RTL) designs in Verilog, model checking has been the predominant technique. However, it suffers from state explosion, limited expressive power, and a large trusted computing base (TCB). Deductive verification offers greater expressive power and enables foundational verification with a minimal TCB. Nevertheless, Verilog\u2019s standard semantics, characterized by its nondeterministic and global scheduling, pose significant challenges to its application.<\/jats:p>\n                  <jats:p>To address these challenges, we propose a new Verilog semantics designed to facilitate deductive verification. Our semantics is based on least fixpoints to enable cycle-level functional evaluation and modular reasoning. For foundational verification, we prove our semantics equivalent to the standard scheduling semantics for synthesizable designs. We demonstrate the benefits of our semantics with a modular verification of a pipelined RISC-V processor\u2019s functional correctness and progress guarantees. All our results are mechanized in Rocq.<\/jats:p>","DOI":"10.1145\/3763084","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"950-977","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Revamping Verilog Semantics for Foundational Verification"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1084-881X","authenticated-orcid":false,"given":"Joonwon","family":"Choi","sequence":"first","affiliation":[{"name":"Amazon Web Services, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3800-9879","authenticated-orcid":false,"given":"Jaewoo","family":"Kim","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2115-0871","authenticated-orcid":false,"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"},{"name":"FuriosaAI, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"2020. PicoRV32 - A Size-Optimized RISC-V CPU. https:\/\/github.com\/cliffordwolf\/picorv32. [Online; accessed 2023-11-28]."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"2024. IEEE Standard for SystemVerilog\u2013Unified Hardware Design Specification and Verification Language. IEEE Std 1800-2023 (Revision of IEEE Std 1800-2017) (2024) 1\u20131354. doi:10.1109\/IEEESTD.2024.10458102","DOI":"10.1109\/IEEESTD.2024.10458102"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Mohammad-Mahdi Bidmeshki and Yiorgos Makris. 2015. Toward automatic proof generation for information flow policies in third-party hardware IP. In 2015 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). 163\u2013168. doi:10.1109\/HST.2015.7140256","DOI":"10.1109\/HST.2015.7140256"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Mohammad-Mahdi Bidmeshki and Yiorgos Makris. 2015. VeriCoq: A Verilog-to-Coq converter for proof-carrying hardware automation. In 2015 IEEE International Symposium on Circuits and Systems (ISCAS). 29\u201332. doi:10.1109\/ISCAS.2015.7168562","DOI":"10.1109\/ISCAS.2015.7168562"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607833"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622805"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_16"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Joonwon Choi Jaewoo Kim and Jeehoon Kang. 2025. Artifact for \u201cRevamping Verilog Semantics for Foundational Verification\u201d https:\/\/doi.org\/10.5281\/zenodo.16923443 10.5281\/zenodo.16923443. doi:10.5281\/zenodo.16923443","DOI":"10.5281\/zenodo.16923443"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_1_15_2","unstructured":"Clifford Cummings. 2000. Nonblocking Assignments in Verilog Synthesis Coding Styles That Kill! SNUG (Synopsys Users Group) 2000 User Papers (2000)."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_1"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Ning Dong Roberto Guanciale Mads Dam and Andreas L\u00f6\u00f6w. 2023. Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. In 2023 Formal Methods in Computer-Aided Design (FMCAD). 247\u2013256. doi:10.34727\/2023\/isbn.978-3-85448-060-0_33","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_33"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2011.113"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373811"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_2"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.003"},{"key":"e_1_3_1_25_2","unstructured":"Mike Gordon Juliano Iyoda Scott Owens and Konrad Slind. 2012. A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic. (Feb 2012)."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_3_1_27_2","volume-title":"Computer architecture: a quantitative approach","author":"Hennessy John L","year":"2011","unstructured":"John L Hennessy and David A Patterson. 2011. Computer architecture: a quantitative approach. Elsevier."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485494"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0399"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1155\/2021\/5525539"},{"key":"e_1_3_1_31_2","unstructured":"Stella Lau Thomas Bourgeat Cl\u00e9ment Pit-Claudel and Adam Chlipala. 2024. Specification and Verification of Strong Timing Isolation of Hardware Enclaves. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439916"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2011.2160627"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w. 2022. Reconciling Verified-Circuit Development and Verilog Development. In 2022 Formal Methods in Computer-Aided Design (FMCAD). 1\u201310. doi:10.34727\/2022\/isbn.978-3-85448-053-2_15","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_15"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w. 2022. A small but important concurrency problem in Verilog\u2019s semantics? (Work in progress). In 2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). 1\u20136. doi:10.1109\/MEMOCODE57689.2022.9954591","DOI":"10.1109\/MEMOCODE57689.2022.9954591"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Andreas L\u00f6\u00f6w and Magnus O. Myreen. 2019. A Proof-Producing Translator for Verilog Development in HOL. In 2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE). 99\u2013108. doi:10.1109\/FormaliSE.2019.00020","DOI":"10.1109\/FormaliSE.2019.00020"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_3_1_40_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 Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010). 179\u2013188. doi:10.1109\/MEMCOD.2010.5558634","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.214687"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3587216.3587217"},{"key":"e_1_3_1_43_2","volume-title":"A structural approach to operational semantics","author":"Plotkin Gordon D","year":"1981","unstructured":"Gordon D Plotkin. 1981. A structural approach to operational semantics. Aarhus university."},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 158\u2013174.","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0028-5"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054171"},{"key":"e_1_3_1_47_2","unstructured":"Stuart Sutherland. 2013. I\u2019m Still in Love with My X!. In Design and Verification Conference (DVCon)."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_23"},{"key":"e_1_3_1_49_2","volume-title":"The Coq Reference Manual, version 8.17.1","author":"The Coq Development Team","year":"2022","unstructured":"The Coq Development Team 2022. The Coq Reference Manual, version 8.17.1. The Coq Development Team, https:\/\/coq.inria.fr\/doc\/V8.17.1\/refman\/"},{"key":"e_1_3_1_50_2","volume-title":"The Coq Reference Manual, version 8.17.1 \u2013 Custom Entries","author":"The Coq Development Team","year":"2022","unstructured":"The Coq Development Team 2022. The Coq Reference Manual, version 8.17.1 \u2013 Custom Entries. The Coq Development Team. https:\/\/coq.inria.fr\/doc\/V8.17.1\/refman\/user-extensions\/syntax-extensions.html#custom-entries"},{"key":"e_1_3_1_51_2","volume-title":"The Coq Reference Manual, version 8.17.1 \u2013 Profiling Ltac Tactics","author":"The Coq Development Team","year":"2022","unstructured":"The Coq Development Team 2022. The Coq Reference Manual, version 8.17.1 \u2013 Profiling Ltac Tactics. The Coq Development Team. https:\/\/coq.inria.fr\/doc\/V8.17.1\/refman\/proof-engine\/ltac.html#profiling-ltac-tactics"},{"key":"e_1_3_1_52_2","unstructured":"Mike Turpin and Principal Verification Engineer. 2003. The Dangers of Living with an X (bugs hidden in your Verilog). In Synopsys Users Group Meeting."},{"key":"e_1_3_1_53_2","volume-title":"The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20191213","author":"Waterman Andrew","year":"2019","unstructured":"Andrew Waterman and Krste Asanovic. 2019. The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 20191213. Technical Report. RISC-V Foundation."},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2006.1690363"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Han Zhu Huibiao Zhu Si Liu and Jian Guo. 2011. Towards Denotational Semantics for Verilog in PVS. In 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion. 1\u20132. doi:10.1109\/SSIRI-C.2011.10","DOI":"10.1109\/SSIRI-C.2011.10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763084","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:43Z","timestamp":1784196643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":55,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763084"],"URL":"https:\/\/doi.org\/10.1145\/3763084","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}