{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T00:01:30Z","timestamp":1755993690995,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,24]]},"DOI":"10.1145\/3671016.3671376","type":"proceedings-article","created":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T20:19:32Z","timestamp":1721247572000},"page":"209-218","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Murphi2Chisel: A Protocol Compiler from Murphi to Chisel"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-3602-1941","authenticated-orcid":false,"given":"Zhenghai","family":"Cai","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2817-063X","authenticated-orcid":false,"given":"Yongjian","family":"Li","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9561-7403","authenticated-orcid":false,"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,24]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The rocket chip generator. EECS Department","author":"Asanovic Krste","year":"2016","unstructured":"Krste Asanovic, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, 2016. The rocket chip generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17 4 (2016), 6\u20132."},{"key":"e_1_3_2_1_2_1","unstructured":"Krste Asanovi\u0107 and Avizienis. 2016. The Rocket Chip Generator. Technical Report UCB\/EECS-2016-17. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/EECS-2016-17.html"},{"volume-title":"Satisfiability modulo theories","author":"Barrett Clark","key":"e_1_3_2_1_3_1","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Springer."},{"key":"e_1_3_2_1_4_1","unstructured":"ABC Berkeley. 2009. A system for sequential synthesis and verification."},{"key":"e_1_3_2_1_5_1","unstructured":"BOSC. [n. d.]. XiangShan-doc. https:\/\/github.com\/OpenXiangShan\/XiangShan"},{"key":"e_1_3_2_1_6_1","unstructured":"Zhenghai Cai. [n. d.]. Murphi2Chisel. https:\/\/github.com\/murphi2chisel\/Multi-verify-Engines-for-Cache-Coherence-Protocols-Murphi2Chisel"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exz023"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_44"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2007.346210"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_2_1_11_1","volume-title":"1st Workshop on Computer Architecture Research with RISC-V. 23","author":"Cook Henry","year":"2017","unstructured":"Henry Cook, Wesley Terpstra, and Yunsup Lee. 2017. Diplomatic design patterns: A TileLink case study. In 1st Workshop on Computer Architecture Research with RISC-V. 23."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Shirley Dewasurendra Pabudi Abeyrathne and Dhammika Elkaduwe. 2015. Strategy to Design Formally Verified hardware\/software implementation of Network Protocols on Reconfigurable Hardware. https:\/\/doi.org\/10.1109\/ICIINFS.2015.7398980","DOI":"10.1109\/ICIINFS.2015.7398980"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_86"},{"key":"e_1_3_2_1_14_1","unstructured":"Jielin Dong. 2005. Network Protocol Handbook. (2005)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0104-3"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2019.8702538"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_23"},{"volume-title":"Handbook of Model Checking","author":"Holzmann J","key":"e_1_3_2_1_18_1","unstructured":"Gerard\u00a0J Holzmann. 2018. Explicit-state model checking. In Handbook of Model Checking. Springer, 153\u2013171."},{"key":"e_1_3_2_1_19_1","unstructured":"Alan\u00a0J. Hu. 1997. Ever verifier."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISOCC53507.2021.9614007"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/IECON48115.2021.9589614"},{"key":"e_1_3_2_1_23_1","volume-title":"An agile approach to building RISC-V microprocessors. ieee Micro 36, 2","author":"Lee Yunsup","year":"2016","unstructured":"Yunsup Lee, Andrew Waterman, Henry Cook, Brian Zimmer, Ben Keller, Alberto Puggelli, Jaehwa Kwak, Ruzica Jevtic, Stevo Bailey, Milovan Blagojevic, 2016. An agile approach to building RISC-V microprocessors. ieee Micro 36, 2 (2016), 8\u201320."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_15"},{"volume-title":"Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking","author":"McMillan L.","key":"e_1_3_2_1_25_1","unstructured":"K.\u00a0L. McMillan. 2001. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. In Correct Hardware Design and Verification Methods, Tiziana Margaria and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 179\u2013195."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/237502.237573"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1186\/s13673-019-0165-x"},{"key":"e_1_3_2_1_28_1","volume-title":"Proc. 7th RISC-V Workshop.","author":"Terpstra W","year":"2017","unstructured":"W Terpstra. 2017. TileLink: A Free And Open Source, High Performance Scalable Cache Coherent Fabric Designed for RISC-V. In Proc. 7th RISC-V Workshop."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICFCC.2009.31"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"e_1_3_2_1_31_1","unstructured":"Clifford Wolf. 2016. Yosys open synthesis suite."},{"key":"e_1_3_2_1_32_1","volume-title":"Fourth Workshop on Computer Architecture Research with RISC-V, Vol.\u00a05. 1\u20137.","author":"Zhao Jerry","year":"2020","unstructured":"Jerry Zhao, Ben Korpan, Abraham Gonzalez, and Krste Asanovic. 2020. Sonicboom: The 3rd generation berkeley out-of-order machine. In Fourth Workshop on Computer Architecture Research with RISC-V, Vol.\u00a05. 1\u20137."}],"event":{"name":"Internetware 2024: 15th Asia-Pacific Symposium on Internetware","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Macau China","acronym":"Internetware 2024"},"container-title":["Proceedings of the 15th Asia-Pacific Symposium on Internetware"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3671016.3671376","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3671016.3671376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:37:01Z","timestamp":1755909421000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3671016.3671376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,24]]},"references-count":32,"alternative-id":["10.1145\/3671016.3671376","10.1145\/3671016"],"URL":"https:\/\/doi.org\/10.1145\/3671016.3671376","relation":{},"subject":[],"published":{"date-parts":[[2024,7,24]]},"assertion":[{"value":"2024-07-24","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}