{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:55:18Z","timestamp":1773194118882,"version":"3.50.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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,VeTSS"],"award-info":[{"award-number":["EP\/R006865\/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":[[2024,6,20]]},"abstract":"<jats:p>\n            High-level synthesis (HLS) is the automatic compilation of software programs into custom hardware designs. With programmable hardware devices (such as FPGAs) now widespread, HLS is increasingly relied upon, but existing HLS tools are too unreliable for safety- and security-critical applications. Herklotz et al. partially addressed this concern by building\n            <jats:italic toggle=\"yes\">Vericert<\/jats:italic>\n            , a prototype HLS tool that is proven correct in Coq (\u00e0 la CompCert), but it cannot compete performance-wise with unverified tools. This paper reports on our efforts to close this performance gap, thus obtaining the first\n            <jats:italic toggle=\"yes\">practical<\/jats:italic>\n            verified HLS tool. We achieve this by implementing a flexible operation scheduler based on\n            <jats:italic toggle=\"yes\">hyperblocks<\/jats:italic>\n            (basic blocks of predicated instructions) that supports\n            <jats:italic toggle=\"yes\">operation chaining<\/jats:italic>\n            (packing dependent operations into a single clock cycle). Correctness is proven via translation validation: each schedule is checked using a Coq-verified validator that uses a SAT solver to reason about predicates. Avoiding exponential blow-up in this validation process is a key challenge, which we address by using\n            <jats:italic toggle=\"yes\">final-state predicates<\/jats:italic>\n            and\n            <jats:italic toggle=\"yes\">value summaries<\/jats:italic>\n            . Experiments on the PolyBench\/C suite indicate that scheduling makes Vericert-generated hardware\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mn>2.1\u00d7<\/mml:mn>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            faster, thus bringing Vericert into competition with a state-of-the-art open-source HLS tool when a similar set of optimisations is enabled.\n          <\/jats:p>","DOI":"10.1145\/3656455","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1929-1953","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Hyperblock Scheduling for Verified High-Level Synthesis"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2329-1029","authenticated-orcid":false,"given":"Yann","family":"Herklotz","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"AbsInt. 2019. CompCert release 19.10. https:\/\/www.absint.com\/releasenotes\/compcert\/19.10\/."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567085"},{"key":"e_1_3_1_4_2","unstructured":"AMD. 2023. Vitis Forums. https:\/\/bit.ly\/vitisifc (accessed 2023-06-02). Relevant quote from AMD: \u201cIf-Conversion aims to convert a sequence of blocks into a single block for better optimization result.\u201d."},{"key":"e_1_3_1_5_2","unstructured":"AMD. 2023. Vitis High-level Synthesis. https:\/\/bit.ly\/41R0204 (accessed 2023-05-21)."},{"key":"e_1_3_1_6_2","author":"Baker Kenneth R.","year":"2019","unstructured":"Kenneth R. Baker and Dan Trietsch. 2019. Principles of sequencing and scheduling (second edition. ed.). Wiley, Hoboken, NJ, USA.","journal-title":"Principles of sequencing and scheduling"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155119"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"e_1_3_1_9_2","unstructured":"Michel Berkelaar. 2010. lp_solve v5.5. https:\/\/lpsolve.sourceforge.net\/5.5\/."},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46117-5_88"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055252"},{"key":"e_1_3_1_12_2","author":"Canis Andrew","year":"2015","unstructured":"Andrew Canis. 2015. LegUp: open-source high-level synthesis research framework. phdthesis. University of Toronto.","journal-title":"phdthesis"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1950413.1950423"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380211204"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2020.2978242"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Jason Cong and Zhiru Zhang. 2006. An efficient and versatile scheduling algorithm based on SDC formulation. In 2006 43rd ACM\/IEEE Design Automation Conference. 433\u2013438. https:\/\/doi.org\/10.1145\/1146909.1147025 10.1145\/1146909.1147025","DOI":"10.1145\/1146909.1147025"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179503"},{"key":"e_1_3_1_18_2","author":"Ellis John R","year":"1985","unstructured":"John R Ellis. 1985. Bulldog: A compiler for VLIW architectures. Ph. D. Dissertation. Yale.","journal-title":"Ph. D. Dissertation"},{"key":"e_1_3_1_19_2","unstructured":"Fabrizio Ferrandi. 2014. PandA-Bambu release notes. https:\/\/github.com\/ferrandi\/PandA-bambu\/blob\/04123a3edb37040db52c44f6591006391cf4a90b\/src\/frontend_analysis\/IR_manipulation\/predicate_statements.cpp#L35 (accessed 2023-11-16)."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586110"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1981.1675827"},{"key":"e_1_3_1_22_2","unstructured":"Google. 2023. XLS: Accelerated HW Synthesis. https:\/\/github.com\/google\/xls\/blob\/dde7095ff1050b09c37cb44d1977bff1af8de050\/xls\/scheduling\/mutual_exclusion_pass.h#L112 (accessed 2023-11-14). The XLS scheduler refers to using an SMT solver to merge mutually exclusive nodes."},{"key":"e_1_3_1_23_2","unstructured":"Google. 2024. Google XLS. https:\/\/google.github.io\/xls\/ (accessed 2024-03-21)."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575681"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Yann Herklotz Zewei Du Nadesh Ramanathan and John Wickerson. 2021. An Empirical Study of the Reliability of High-Level Synthesis Tools. In 2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 219\u2013223. https:\/\/doi.org\/10.1109\/FCCM51124.2021.00034 10.1109\/FCCM51124.2021.00034","DOI":"10.1109\/FCCM51124.2021.00034"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485494"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Yann Herklotz and John Wickerson. 2024. Artefact: Hyperblock Scheduling for Verified High- Level Synthesis. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10808233 10.5281\/zenodo.10808233","DOI":"10.5281\/zenodo.10808233"},{"key":"e_1_3_1_28_2","author":"Hopwood Gregory Littell","year":"1978","unstructured":"Gregory Littell Hopwood. 1978. Decompilation. Ph. D. Dissertation. University of California, Irvine. AAI7811860.","journal-title":"Ph. D. Dissertation"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3200-2_7"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"IEEE. 2024. IEEE Standard for SystemVerilog\u2013Unified Hardware Design Specification and Verification Language. (2024) 1\u20131354. https:\/\/doi.org\/10.1109\/IEEESTD.2024.10458102 10.1109\/IEEESTD.2024.10458102","DOI":"10.1109\/IEEESTD.2024.10458102"},{"key":"e_1_3_1_31_2","unstructured":"Intel. 2023. High-level Synthesis Compiler. https:\/\/intel.ly\/2UDiWr5 (accessed 2023-06-23)."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3174243.3174264"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISQED.2006.10"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/144965.144998"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.1987.1270350"},{"key":"e_1_3_1_37_2","unstructured":"Louis-No\u00ebl Pouchet. 2020. PolyBench\/C: the Polyhedral Benchmark suite. http:\/\/web.cse.ohio-state.edu\/pouchet.2\/software\/polybench\/."},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Carmine Rizzi Andrea Guerrieri and Lana Josipovi\u0107. 2023. An Iterative Method for Mapping-Aware Frequency Regulation in Dataflow Circuits. In 2023 60th ACM\/IEEE Design Automation Conference (DAC). 1\u20136. https:\/\/doi.org\/10.1109\/DAC56929.2023.10247686 10.1109\/DAC56929.2023.10247686","DOI":"10.1109\/DAC56929.2023.10247686"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_3_1_40_2","unstructured":"Siemens. 2021. Catapult High-Level Synthesis. https:\/\/eda.sw.siemens.com\/en-US\/ic\/catapult-high-level-synthesis\/hls\/c-cplus\/ (accessed 2023-11-14)."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503679"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/2684746.2689063"},{"key":"e_1_3_1_43_2","unstructured":"Andreas Tiemeyer Tom Melham Daniel Kroening and John O\u2019Leary. 2019. CREST: Hardware Formal Verification with ANSI-C Reference Specifications. abs\/1908.01324 (2019)."},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415657"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Hanyu Wang Carmine Rizzi and Lana Josipovi\u0107. 2023. MapBuf: Simultaneous Technology Mapping and Buffer Insertion for HLS Performance Optimization. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD). 1\u20139. https:\/\/doi.org\/10.1109\/ICCAD57390.2023.10323639 10.1109\/ICCAD57390.2023.10323639","DOI":"10.1109\/ICCAD57390.2023.10323639"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Youngsik Kim S. Kopuri and N. Mansouri. 2004. Automated formal verification of scheduling process using finite state machines with datapath (FSMD). In International Symposium on Signals Circuits and Systems. Proceedings SCS 2003. (Cat. No.03EX720). 110\u2013115. https:\/\/doi.org\/10.1109\/ISQED.2004.1283659 10.1109\/ISQED.2004.1283659","DOI":"10.1109\/ISQED.2004.1283659"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Zhiru Zhang and Bin Liu. 2013. SDC-based modulo scheduling for pipeline synthesis. In 2013 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). 211\u2013218. https:\/\/doi.org\/10.1109\/ICCAD.2013.6691121 10.1109\/ICCAD.2013.6691121","DOI":"10.1109\/ICCAD.2013.6691121"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2554688.2554775"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656455","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656455","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:25Z","timestamp":1751661745000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656455"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656455"],"URL":"https:\/\/doi.org\/10.1145\/3656455","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}