{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,22]],"date-time":"2026-07-22T23:17:26Z","timestamp":1784762246072,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"name":"SRC JUMP 2.0 PRISM Center, NSF CAREER","award":["2238006"],"award-info":[{"award-number":["2238006"]}]},{"name":"DARPA DSSoC, Stanford Agile Hardware (AHA) Center"},{"name":"Stanford SystemX Alliance and Apple Stanford EE PhD Fellowship in Integrated Systems"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>Domain-specific languages for hardware can significantly enhance designer productivity, but sometimes at the cost of ease of verification. On the other hand, ISA specification languages are too static to be used during early stage design space exploration. We present PEak, an open-source hardware design and specification language, which aims at improving both design productivity and verification capability. PEak does this by providing a single source of truth for functional models, formal specifications, and RTL. PEak has been used in several academic projects, and PEak-generated RTL has been included in three fabricated hardware accelerators. In these projects, the formal capabilities of PEak were crucial for enabling both novel design space exploration techniques and automated compiler synthesis.<\/jats:p>","DOI":"10.1145\/3703456","type":"journal-article","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T06:02:29Z","timestamp":1731391349000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["PEak: A Single Source of Truth for Hardware Design and Verification"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9336-1267","authenticated-orcid":false,"given":"Caleb","family":"Donovick","sequence":"first","affiliation":[{"name":"Computer Science, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8232-1603","authenticated-orcid":false,"given":"Jackson","family":"Melchert","sequence":"additional","affiliation":[{"name":"Electrical Engineering, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4938-5250","authenticated-orcid":false,"given":"Ross","family":"Daly","sequence":"additional","affiliation":[{"name":"Computer Science, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7583-9730","authenticated-orcid":false,"given":"Lenny","family":"Truong","sequence":"additional","affiliation":[{"name":"Computer Science, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8834-8663","authenticated-orcid":false,"given":"Priyanka","family":"Raina","sequence":"additional","affiliation":[{"name":"Electrical Engineering, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3474-9752","authenticated-orcid":false,"given":"Pat","family":"Hanrahan","sequence":"additional","affiliation":[{"name":"Computer Science, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Computer Science, Stanford University","place":["Stanford, United States"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,3,2]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/LES.2010.2055231"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2010.21"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218553"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Clark Barrett Roberto Sebastiani Sanjit Seshia and Cesare Tinelli. 2009. Satisfiability Modulo Theories (1st ed.). Handbook of Satisfiabili IOS Press 825\u2013558. DOI:10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Gordon Bell and Allen Newell. 1970. The PMS and ISP descriptive systems for computer structures. Proceedings of the May 5-7 1970 Spring Joint Computer Conference. Association for Computing Machinery 351\u2013374. 10.1145\/1476936.1476993","DOI":"10.1145\/1476936.1476993"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/291251.289440"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSITechnologyandCir46769.2022.9830509"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.23919\/FPL.2017.8056860"},{"key":"e_1_3_2_14_2","first-page":"139","volume-title":"Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design","author":"Daly Ross","year":"2022","unstructured":"Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze Bullock, Priyanka Raina, Clark Barrett, and Pat Hanrahan. 2022. Synthesizing instruction selection rewrite rules from RTL using SMT. In Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design. 139\u2013150."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-01857-7_47"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2022.104737"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385983"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/HCS55958.2022.9895616"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.2023.3313116"},{"key":"e_1_3_2_20_2","unstructured":"Python Software Foundation. 2023. The Python Language Reference. Retrieved 19 November 2024 from https:\/\/docs.python.org\/3\/reference\/datamodel.html##basic-customization"},{"key":"e_1_3_2_21_2","volume-title":"Proceedings of the SMT Workshop 2015","author":"Gario Marco","year":"2015","unstructured":"Marco Gario and Andrea Micheli. 2015. PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In Proceedings of the SMT Workshop 2015."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2012.51"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3282307"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192379"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Kalhan Koul Jackson Melchert Kavya Sreedhar Leonard Truong Gedeon Nyengele Keyi Zhang Qiaoyi Liu Jeff Setter Po-Han Chen Yuchen Mei Maxwell Strange Ross Daly Caleb Donovick Alex Carsello Taeyoung Kong Kathleen Feng Dillon Huff Ankita Nayak Rajsekhar Setaluri James Thomas Nikhil Bhagdikar David Durst Zachary Myers Nestan Tsiskaridze Stephen Richardson Rick Bahr Kayvon Fatahalian Pat Hanrahan Clark Barrett Mark Horowitz Christopher Torng Fredrik Kjolstad and Priyanka Raina. 2023. AHA: An agile approach to the design of coarse-grained reconfigurable accelerators and compilers. ACM Trans. Embed. Comput. Syst. 22 2 (2023) 34 Pages. 10.1145\/3534933","DOI":"10.1145\/3534933"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSITechnologyandCir46783.2024.10631383"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_31_2","volume-title":"Proceedings of the 2018 Chisel Community Conference","author":"Lockhart Derek","year":"2018","unstructured":"Derek Lockhart, Stephen Twigg, Doug Hogberg, George Huang, Ravi Narayanaswami, Jeremy Coriell, Uday Dasari, Richard Ho, Doug Hogberg, George Huang, Anand Kane, Chintan Kaur, Tao Kaur, Adriana Maggiore, Kevin Townsend, and Emre Tuncer. 2018. Experiences building edge TPU with Chisel. In Proceedings of the 2018 Chisel Community Conference."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.50"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45234-8_7"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582070"},{"key":"e_1_3_2_35_2","first-page":"69","volume-title":"Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004.","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. 2004. Bluespec system verilog: Efficient, correct RTL from high level specifications. In Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. IEEE, 69\u201370."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080256"},{"key":"e_1_3_2_37_2","first-page":"161","volume-title":"Proceedings of the 2016 Formal Methods in Computer-Aided Design","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In Proceedings of the 2016 Formal Methods in Computer-Aided Design. 161\u2013168."},{"key":"e_1_3_2_38_2","first-page":"42","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-end verification of processors with ISA-Formal. In Proceedings of the International Conference on Computer Aided Verification. Springer, 42\u201358."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2010.81"},{"key":"e_1_3_2_41_2","volume-title":"Proceedings of the 3rd Summit on Advances in Programming Languages","author":"Truong Lenny","year":"2019","unstructured":"Lenny Truong and Pat Hanrahan. 2019. A golden age of hardware description languages: Applying programming language techniques to improve design productivity. In Proceedings of the 3rd Summit on Advances in Programming Languages. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_19"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530603"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T08:15:45Z","timestamp":1773389745000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,2]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3703456"],"URL":"https:\/\/doi.org\/10.1145\/3703456","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,2]]},"assertion":[{"value":"2024-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}