{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:55:14Z","timestamp":1773194114775,"version":"3.50.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R006865\/1,EP\/P010040\/1,VeTSS"],"award-info":[{"award-number":["EP\/R006865\/1,EP\/P010040\/1,VeTSS"]}],"id":[{"id":"10.13039\/501100000266","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":[[2021,10,20]]},"abstract":"<jats:p>High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language such as Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Furthermore, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs.<\/jats:p>\n          <jats:p>To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements. An evaluation on the PolyBench\/C benchmark suite indicates that Vericert generates hardware that is around an order of magnitude slower (only around 2\u00d7 slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.<\/jats:p>","DOI":"10.1145\/3485494","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Formal verification of high-level synthesis"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2329-1029","authenticated-orcid":false,"given":"Yann","family":"Herklotz","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1404-1527","authenticated-orcid":false,"given":"James D.","family":"Pollard","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9083-8349","authenticated-orcid":false,"given":"Nadesh","family":"Ramanathan","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Handel-C language reference guide. Computing Laboratory","author":"Aubury Matthew"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2314392"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_2_2_5_1","volume-title":"Formal Verification of a Memory Model for C-Like Imperative Languages","author":"Blazy Sandrine"},{"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.1145\/1950413.1950423"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/EDAC.1992.205894"},{"key":"e_1_2_2_9_1","unstructured":"Pankaj Chauhan. 2020. Formally Ensuring Equivalence between C++ and RTL designs. https:\/\/bit.ly\/2KbT0ki  Pankaj Chauhan. 2020. Formally Ensuring Equivalence between C++ and RTL designs. https:\/\/bit.ly\/2KbT0ki"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240815"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2020.2978242"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2846654"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2110592"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837489"},{"key":"e_1_2_2_17_1","unstructured":"Stephane Gauthier and Zubair Wadood. 2020. High-Level Synthesis: Can it outperform hand-coded HDL? https:\/\/info.silexica.com\/high-level-synthesis\/1 White paper.  Stephane Gauthier and Zubair Wadood. 2020. High-Level Synthesis: Can it outperform hand-coded HDL? https:\/\/info.silexica.com\/high-level-synthesis\/1 White paper."},{"key":"e_1_2_2_18_1","volume-title":"Research Note: An Open Source Bluespec Compiler. arxiv:1905.03746.","author":"Greaves David J.","year":"2019"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2008.46"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM51124.2021.00034"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5093839"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ReConFig.2014.7032504"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.1999.761092"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2006.99495"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2005.339572"},{"key":"e_1_2_2_26_1","unstructured":"Intel. 2020. High-level Synthesis Compiler. https:\/\/intel.ly\/2UDiWr5  Intel. 2020. High-level Synthesis Compiler. https:\/\/intel.ly\/2UDiWr5"},{"key":"e_1_2_2_27_1","unstructured":"Intel. 2020. SDK for OpenCL Applications. https:\/\/intel.ly\/30sYHz0  Intel. 2020. SDK for OpenCL Applications. https:\/\/intel.ly\/30sYHz0"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2006.10"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192379"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_44"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439916"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2019.00020"},{"key":"e_1_2_2_37_1","unstructured":"Mentor. 2020. Catapult High-Level Synthesis. https:\/\/www.mentor.com\/hls-lp\/catapult-high-level-synthesis\/c-systemc-hls  Mentor. 2020. Catapult High-Level Synthesis. https:\/\/www.mentor.com\/hls-lp\/catapult-high-level-synthesis\/c-systemc-hls"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385974"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459818"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/RECONFIG.2017.8279807"},{"key":"e_1_2_2_42_1","volume-title":"Oxford Workshop on Field Programmable Logic and Applications. 15","author":"Page Ian","year":"1991"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/74382.74383"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SAMOS.2016.7818341"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.02.007"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-011-0142-y"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2013.6645550"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_49_1","unstructured":"Louis-No\u00ebl Pouchet. 2020. PolyBench\/C: the Polyhedral Benchmark suite. http:\/\/web.cse.ohio-state.edu\/~pouchet.2\/software\/polybench\/  Louis-No\u00ebl Pouchet. 2020. PolyBench\/C: the Polyhedral Benchmark suite. http:\/\/web.cse.ohio-state.edu\/~pouchet.2\/software\/polybench\/"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2435264.2435273"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386024"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428197"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASAP.2016.7760777"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397305"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428265"},{"key":"e_1_2_2_58_1","unstructured":"Xilinx. 2019. Vivado Design Suite. https:\/\/bit.ly\/2wZAmld  Xilinx. 2019. Vivado Design Suite. https:\/\/bit.ly\/2wZAmld"},{"key":"e_1_2_2_59_1","unstructured":"Xilinx. 2020. Vivado High-level Synthesis. https:\/\/bit.ly\/39ereMx  Xilinx. 2020. Vivado High-level Synthesis. https:\/\/bit.ly\/39ereMx"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2004.1283659"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203809"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/CODES-ISSS.2013.6659002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485494","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485494","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485494"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":63,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485494"],"URL":"https:\/\/doi.org\/10.1145\/3485494","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}