{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:58Z","timestamp":1774984078733,"version":"3.50.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,8,29]]},"abstract":"<jats:p>It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning for hardware designs expressed in the style of the Bluespec language. We can specify, implement, and verify realistic designs entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in FPGAs. Our methodology, using labeled transition systems, has been evaluated in a case study verifying an infinite family of multicore systems, with cache-coherent shared memory and pipelined cores implementing (the base integer subset of) the RISC-V instruction set.<\/jats:p>","DOI":"10.1145\/3110268","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":82,"title":["Kami: a platform for high-level parametric hardware specification and its modular verification"],"prefix":"10.1145","volume":"1","author":[{"given":"Joonwon","family":"Choi","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Muralidaran","family":"Vijayaraghavan","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Benjamin","family":"Sherman","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"family":"Arvind","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382681"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_25"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Ritwik\n       \n      Bhattacharya Steven M.\n       \n      German and \n      \n      \n      Ganesh\n       \n      Gopalakrishnan\n    . 2006.\n      \n  \n   \n  Exploiting symmetry and transactions for partial order reduction of rule based specifications. In Antti Valmari editor SPIN volume \n  3925\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer 252\u2013270.  Ritwik Bhattacharya Steven M. German and Ganesh Gopalakrishnan. 2006. Exploiting symmetry and transactions for partial order reduction of rule based specifications. In Antti Valmari editor SPIN volume 3925 of Lecture Notes in Computer Science. Springer 252\u2013270.","DOI":"10.1007\/11691617_15"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289440"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958089"},{"key":"e_1_2_2_6_1","volume-title":"Computer Aided Verification","author":"Burch Jerry R"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0092-y"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371249"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487887"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_8"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1992.276232"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"e_1_2_2_15_1","first-page":"647","article-title":"System and method for scheduling TRS rules. (Jan. 12 2010)","volume":"7","author":"Esposito Thomas M","year":"2010","journal-title":"US Patent"},{"key":"e_1_2_2_16_1","volume-title":"TYPES 2015","author":"Pizani Flor Joao Paulo","year":"2015"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190269"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.018"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926425"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034805"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2000.896524"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1992.0024"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.1995.486381"},{"key":"e_1_2_2_25_1","unstructured":"Chung-Wah Norris Ip David L. Dill and John C. Mitchell. 1996. State Reduction Methods For Automatic Formal Verification. (1996).  Chung-Wah Norris Ip David L. Dill and John C. Mitchell. 1996. State Reduction Methods For Automatic Formal Verification. (1996)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_40"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022969405325"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSCC.2016.7418021"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_32"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2014.6961840"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_33_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/HOTCHIPS.2013.7478320"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2007.79"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886667"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_17"},{"key":"e_1_2_2_39_1","volume-title":"Proceedings of the International Symposium on Shared Memory Multiprocessing. 111\u2013134","author":"McMillan K.L.","year":"1992"},{"key":"e_1_2_2_40_1","volume-title":"Computer Aided Verification","author":"McMillan Kenneth L"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_17"},{"key":"e_1_2_2_42_1","series-title":"LNCS","volume-title":"Proc. CAV\u201998","author":"Moore J Strother"},{"key":"e_1_2_2_43_1","volume-title":"CreateSpace","author":"Nikhil Rishiyur S","year":"2010"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/237502.237573"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ESSCIRC.2016.7598255"},{"key":"e_1_2_2_46_1","doi-asserted-by":"crossref","unstructured":"Alastair Reid. 2016. Trustworthy Specifications of ARMR v8-A and v8-M System Level Architecture. In Formal Methods in Computer-Aided Design FMCAD.  Alastair Reid. 2016. Trustworthy Specifications of ARMR v8-A and v8-M System Level Architecture. In Formal Methods in Computer-Aided Design FMCAD.","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996583"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35409-5_20"},{"key":"e_1_2_2_50_1"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"e_1_2_2_52_1","unstructured":"Muralidaran Vijayaraghavan. 2016. Modular Verification of Hardware Systems. Ph.D. Dissertation. http:\/\/hdl.handle.net\/ 1721.1\/106096  Muralidaran Vijayaraghavan. 2016. Modular Verification of Hardware Systems. Ph.D. Dissertation. http:\/\/hdl.handle.net\/ 1721.1\/106096"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"e_1_2_2_54_1","volume-title":"11th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, MEMCODE 2013","author":"Vijayaraghavan Muralidaran","year":"2013"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.368009"},{"key":"e_1_2_2_57_1","volume-title":"4th RISC-V Workshop. https:\/\/riscv.org\/wp- content\/ uploads\/2016\/07\/Wed830_Riscy_Processors_V1.pdf","author":"Wright Andy","year":"2016"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835949"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2010.11"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110268","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":58,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110268"],"URL":"https:\/\/doi.org\/10.1145\/3110268","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}