{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:34Z","timestamp":1784793814889,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>SystemVerilog remains one of the most widely used languages for designing and verifying digital circuits. Despite its importance, the SystemVerilog standard suffers from ambiguities, which can lead to inconsistent implementations and portability challenges. Formal methods can provide precise semantics to address these issues.<\/jats:p>\n                  <jats:p>\n                    We focus on SystemVerilog\u2019s mechanism for determining the bit-width of each expression that appears in a design. This is surprisingly subtle because an expression\u2019s bit-width can depend on both its children\n                    <jats:italic>and<\/jats:italic>\n                    its parents. First, we develop a Rocq formalization of the existing IEEE standard for SystemVerilog. We then construct a bidirectional type system that captures the context-dependent nature of SystemVerilog expressions and prove it equivalent to our formalization of the standard using Rocq. We provide a reference implementation that determines bit-widths in linear time and prove its correspondence to our system, also in Rocq. Based on these results, we propose revisions to the text of the standard that reduce redundancy and improve precision.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_22","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:39Z","timestamp":1784791119000},"page":"426-445","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Mechanised, Bidirectional Type System for Bit-Width Determination in SystemVerilog"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5185-2887","authenticated-orcid":false,"given":"Gabriel","family":"Desfrene","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4218-3987","authenticated-orcid":false,"given":"Quentin","family":"Corradi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4179-291X","authenticated-orcid":false,"given":"Michalis","family":"Pardalos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Bierman, G.M., Meijer, E., Torgersen, M.: Lost in translation: formalizing proposed extensions to C#. In: Gabriel, R.P., Bacon, D.F., Lopes, C.V., Steele\u00a0Jr., G.L. (eds.) Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, 21\u201325 October 2007, Montreal, Quebec, Canada, pp. 479\u2013498. ACM (2007). https:\/\/doi.org\/10.1145\/1297027.1297063","DOI":"10.1145\/1297027.1297063"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Chen, Q., et al.: The essence of verilog: a tractable and tested operational semantics for verilog. Proc. ACM Program. Lang. 7(OOPSLA2) (2023). https:\/\/doi.org\/10.1145\/3622805","DOI":"10.1145\/3622805"},{"key":"22_CR3","unstructured":"ChipsAlliance: SV-tests: test suite designed to check compliance with the SystemVerilog standard. GitHub repository. https:\/\/github.com\/chipsalliance\/sv-tests"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Choi, J., Kim, J., Kang, J.: Revamping Verilog semantics for foundational verification. Proc. ACM Program. Lang. 9(OOPSLA2) (2025). https:\/\/doi.org\/10.1145\/3763084","DOI":"10.1145\/3763084"},{"issue":"1","key":"22_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0167-6423(95)00021-6","volume":"26","author":"T Coquand","year":"1996","unstructured":"Coquand, T.: An algorithm for type-checking dependent types. Sci. Comput. Program. 26(1), 167\u2013177 (1996). https:\/\/doi.org\/10.1016\/0167-6423(95)00021-6","journal-title":"Sci. Comput. Program."},{"key":"22_CR6","unstructured":"Desfrene, G., Corradi, Q., Pardalos, M., Wickerson, J.: Rocq formalization of SystemVerilog expression bit-width determination (2026)"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surv. 54(5) (2021). https:\/\/doi.org\/10.1145\/3450952","DOI":"10.1145\/3450952"},{"issue":"9","key":"22_CR8","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1145\/2544174.2500582","volume":"48","author":"J Dunfield","year":"2013","unstructured":"Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. SIGPLAN Not. 48(9), 429\u2013442 (2013). https:\/\/doi.org\/10.1145\/2544174.2500582","journal-title":"SIGPLAN Not."},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Flake, P., Moorby, P., Golson, S., Salz, A., Davidmann, S.: Verilog HDL and its ancestors and descendants. Proc. ACM Program. Lang. 4(HOPL) (2020). https:\/\/doi.org\/10.1145\/3386337","DOI":"10.1145\/3386337"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Gillenwater, J., et al.: Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability. In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2008, pp. 41\u201350. Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1328408.1328416","DOI":"10.1145\/1328408.1328416"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"IEEE: Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2023 (2024). https:\/\/doi.org\/10.1109\/IEEESTD.2024.10458102","DOI":"10.1109\/IEEESTD.2024.10458102"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"L\u00f6\u00f6w, A.: Lutsig: a verified Verilog compiler for verified circuit development. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pp. 46\u201360. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3437992.3439916","DOI":"10.1145\/3437992.3439916"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"L\u00f6\u00f6w, A.: The simulation semantics of synthesisable Verilog. Proc. ACM Program. Lang. 9(OOPSLA1) (2025). https:\/\/doi.org\/10.1145\/3720484","DOI":"10.1145\/3720484"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Meredith, P., Katelman, M., Meseguer, J., Rosu, G.: A formal executable semantics of Verilog. In: Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp. 179\u2013188 (2010). https:\/\/doi.org\/10.1109\/MEMCOD.2010.5558634","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"22_CR15","unstructured":"nebuchadnezzar_II: Lint tool is throwing an error about bit width when adding two 10-bit unsigned numbers and assigning to a 11-bit net. Electrical Engineering Stack Exchange (2023). https:\/\/electronics.stackexchange.com\/q\/665616"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Odersky, M., Zenger, C., Zenger, M.: Colored local type inference. In: Hankin, C., Schmidt, D. (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, 17\u201319 January 2001, pp. 41\u201353. ACM (2001). https:\/\/doi.org\/10.1145\/360204.360207","DOI":"10.1145\/360204.360207"},{"key":"22_CR17","unstructured":"Pardalos, M., Pozzi, L., Wickerson, J.: Towards mechanized verification of Verilog equivalence checking. In: Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE) (2025). https:\/\/capra.cs.cornell.edu\/latte25\/paper\/9.pdf"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/345099.345100","volume":"22","author":"BC Pierce","year":"2000","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1\u201344 (2000). https:\/\/doi.org\/10.1145\/345099.345100","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR19","unstructured":"r\/Verilog: Tutorial is wrong about truncation rules? (2026). https:\/\/www.reddit.com\/r\/Verilog\/comments\/1t0nb27\/tutorial_is_wrong_about_truncation_rules\/"},{"key":"22_CR20","unstructured":"The Rocq Development Team: The Rocq Prover (2025). https:\/\/rocq-prover.org\/, version 9.0.0"},{"key":"22_CR21","unstructured":"Williams, S.: Icarus Verilog quirks: unsized expressions as arguments to concatenation (2024). https:\/\/steveicarus.github.io\/iverilog\/usage\/icarus_verilog_quirks.html#unsized-expressions-as-arguments-to-concatenation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:42Z","timestamp":1784791122000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}