{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:55:06Z","timestamp":1773194106599,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2115587,2217064,2421734"],"award-info":[{"award-number":["2115587,2217064,2421734"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>Compared to familiar hardware-description languages like Verilog, rule-based languages like Bluespec offer opportunities to import modularity features from software programming. While Verilog modules are about connecting wires between submodules, Bluespec modules resemble objects in object-oriented programming, where interactions with a module occur only through calls to its methods. However, while software objects can typically be characterized one method at a time, the concurrent nature of hardware makes it essential to consider the repercussions of invoking multiple methods simultaneously. Prior formalizations of rule-based languages conceptualized modules by describing their semantics considering arbitrary sets of simultaneous method calls. This internalized concurrency significantly complicates correctness proofs. Rather than analyzing methods one-at-a-time, as is done when verifying software object methods, validating the correctness of rule-based modules necessitated simultaneous consideration of arbitrary subsets of method calls. The result was a number of proof cases that grew exponentially in the size of the module\u2019s API.<\/jats:p>\n          <jats:p>In this work, we side-step the exponential blowup through a set of judicious language restrictions. We introduce a new Bluespec-inspired formal language, Fjfj, that supports sequential characterization of modules, while preserving the concurrent hardware nature of the language. We evaluated Fjfj by implementing it in Coq, proving the key framework principle: the refinement theorem. We demonstrated Fjfj\u2019s expressivity via implementation and verification of three examples: a pipelined processor, a parameterized crossbar, and a network switch.<\/jats:p>","DOI":"10.1145\/3729331","type":"journal-article","created":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T16:14:56Z","timestamp":1755274496000},"page":"2007-2031","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Making Concurrent Hardware Verification Sequential"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7582-4630","authenticated-orcid":false,"given":"Jiazheng","family":"Liu","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"family":"Arvind","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.768501"},{"key":"e_1_2_2_2_1","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2026","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press. isbn:026202649X, 9780262026499"},{"key":"e_1_2_2_3_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Mike","year":"2006","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 364\u2013387. isbn:978-3-540-36750-5"},{"key":"e_1_2_2_4_1","volume-title":"Formal Methods in Computer-Aided Design","author":"Berezin Sergey","unstructured":"Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zhu. 1998. Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. In Formal Methods in Computer-Aided Design, Ganesh Gopalakrishnan and Phillip Windley (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 369\u2013386. isbn:978-3-540-49519-2"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2534169.2486011"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_2_8_1","unstructured":"B. A. Brady R. E. Bryant and S. A. Seshia. 2011. Learning conditional abstractions. In 2011 Formal Methods in Computer-Aided Design (FMCAD). 116\u2013124."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558624"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1997.628846"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_2_12_1","unstructured":"Randal E Bryant. 2018. Formal verification of pipelined Y86-64 microprocessors with UCLID5. Technical Report CMU-CS-18-122."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_2_14_1","volume-title":"Dill","author":"Burch Jerry R.","year":"1994","unstructured":"Jerry R. Burch and David L. Dill. 1994. Automatic verification of pipelined microprocessor control. In Computer Aided Verification, David L. Dill (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 68\u201380. isbn:978-3-540-48469-1"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950413.1950423"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_16"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2110592"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970511"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558626"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","unstructured":"Daniel D. Gajski. 2001. SpecC Design Environment. System Design 217\u2013235. isbn:9781461514817 https:\/\/doi.org\/10.1007\/978-1-4615-1481-7_5 10.1007\/978-1-4615-1481-7_5","DOI":"10.1007\/978-1-4615-1481-7_5"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359986.3361199"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2004.1268836"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485494"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07994-7_54"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3639051"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC56929.2023.10247894"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_2_2_31_1","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83. 9 321\u2013332."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174243.3174264"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"e_1_2_2_34_1","volume-title":"Iris: Monoids and Invariants As an Orthogonal Basis for Concurrent Reasoning. In POPL \u201915. 637\u2013650. isbn:978-1-4503-3300-9","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants As an Orthogonal Basis for Concurrent Reasoning. In POPL \u201915. 637\u2013650. isbn:978-1-4503-3300-9"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00030-1"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_2_40_1","unstructured":"Mentor. [n. d.]. ModelSim. https:\/\/www.mentor.com\/products\/fpga\/verification-simulation\/modelsim\/"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459818"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031822"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47705-8_11"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"e_1_2_2_48_1","volume-title":"Modular SMT-Based Verification of Rule-Based Hardware Designs. Ph. D. Dissertation","author":"Wright Andrew","unstructured":"Andrew Wright. 2021. Modular SMT-Based Verification of Rule-Based Hardware Designs. Ph. D. Dissertation. Massachusetts Institute of Technology, USA. https:\/\/hdl.handle.net\/1721.1\/139491"},{"key":"e_1_2_2_49_1","unstructured":"Xilinx. [n. d.]. Vivado HLS. https:\/\/www.xilinx.com\/products\/design-tools\/vivado\/integration\/esl-design.html"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3508352.3549341"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00015"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729331","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T16:14:58Z","timestamp":1755274498000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":51,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729331"],"URL":"https:\/\/doi.org\/10.1145\/3729331","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}