@article{vericert, author = {Yann Herklotz and James D. Pollard and Nadesh Ramanathan and John Wickerson}, title = {Formal verification of high-level synthesis}, journal = {Proc. {ACM} Program. Lang.}, volume = {5}, number = {{OOPSLA}}, pages = {1--30}, year = {2021}, url = {https://doi.org/10.1145/3485494}, doi = {10.1145/3485494}, timestamp = {Sat, 08 Jan 2022 02:21:39 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/HerklotzPRW21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @misc{intel_hls, author = {{Intel}}, title = {Intel High Level Synthesis Compiler}, year = 2022, url = {https://www.intel.com/content/www/us/en/software/programmable/quartus-prime/hls-compiler.html}, } @misc{vericertfun-github, author = {Pardalos, Michalis and Herklotz, Yann and Wickerson, John}, title = {Public repository for Vericert-Fun}, year = 2022, note = {\url{https://github.com/mpardalos/Vericert-Fun} or \url{https://doi.org/10.5281/zenodo.5866708}}, } @misc{xilinx_vitis, author = {{Xilinx Inc.}}, title = {Vitis HLS}, year = 2022, url = {https://www.xilinx.com/products/design-tools/vivado/integration/esl-design.html}, } @inproceedings{Herklotz2021_empiricalstudy, author = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John}, booktitle = {2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)}, title = {An Empirical Study of the Reliability of High-Level Synthesis Tools}, year = 2021, pages = {219-223}, abstract = {High-level synthesis (HLS) is becoming an increasingly important part of the computing landscape, even in safety-critical domains where correctness is key. As such, HLS tools are increasingly relied upon. But are they trustworthy? We have subjected four widely used HLS tools - LegUp, Xilinx Vivado HLS, the Intel HLS Compiler and Bambu - to a rigorous fuzzing campaign using thousands of random, valid C programs that we generated using a modified version of the Csmith tool. For each C program, we compiled it to a hardware design using the HLS tool under test and checked whether that hardware design generates the same output as an executable generated by the GCC compiler. When discrepancies arose between GCC and the HLS tool under test, we reduced the C program to a minimal example in order to zero in on the potential bug. Our testing campaign has revealed that all four HLS tools can be made to generate wrong designs from valid C programs and one tool could be made to crash; this underlines the need for these increasingly trusted tools to be more rigorously engineered. Out of 6700 test-cases, we found 1191 programs that caused at least one tool to fail, out of which we were able to discern at least 8 unique bugs.}, doi = {10.1109/FCCM51124.2021.00034}, ISSN = {2576-2621}, month = {May}, } @inproceedings{Herklotz2021_shouldbeproven, author = {Herklotz, Yann and Wickerson, John}, title = {High-Level Synthesis Tools should be Proven Correct}, year = 2021, url = {https://yannherklotz.com/docs/drafts/formal_hls.pdf}, urldate = {2021-1-30}, } @article{compcert_Leroy2009, author = {Leroy, Xavier}, title = {Formal Verification of a Realistic Compiler}, year = 2009, issue_date = {July 2009}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 52, number = 7, issn = {0001-0782}, url = {https://doi.org/10.1145/1538788.1538814}, doi = {10.1145/1538788.1538814}, abstract = {This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.}, journal = {Commun. ACM}, month = {jul}, pages = {107–115}, numpages = 9, } @inproceedings{legup_CanisAndrew2011, author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and Kammoona, Ahmed and Anderson, Jason H. and Brown, Stephen and Czajkowski, Tomasz}, title = {LegUp: High-Level Synthesis for FPGA-Based Processor/Accelerator Systems}, year = 2011, isbn = 9781450305549, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/1950413.1950423}, doi = {10.1145/1950413.1950423}, abstract = {In this paper, we introduce a new open source high-level synthesis tool called LegUp that allows software techniques to be used for hardware design. LegUp accepts a standard C program as input and automatically compiles the program to a hybrid architecture containing an FPGA-based MIPS soft processor and custom hardware accelerators that communicate through a standard bus interface. Results show that the tool produces hardware solutions of comparable quality to a commercial high-level synthesis tool.}, booktitle = {Proceedings of the 19th ACM/SIGDA International Symposium on Field Programmable Gate Arrays}, pages = {33–36}, numpages = 4, keywords = {fpgas, high-level synthesis, hardware/software co-design, field-programmable gate arrays}, location = {Monterey, CA, USA}, series = {FPGA '11}, } @INPROCEEDINGS{faissole+19, author={Faissole, Florian and Constantinides, George A. and Thomas, David}, booktitle={2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)}, title={Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis}, year={2019}, volume={}, number={}, pages={315-315}, abstract={High-level synthesis (HLS) tools such as VivadoHLS interpret C/C++ code supplemented by proprietary optimization directives called pragmas. In order to perform loop pipelining, HLS compilers have to deal with non-trivial loop-carried data dependencies. In VivadoHLS, the dependence pragma could be used to enforce or to eliminate such dependencies, but, the behavior of this directive is only informally specified through examples. Most of the time programmers and the compiler seem to agree on what the directive means, but the accidental misuse of this pragma can lead to the silent generation of an erroneous register-transfer level (RTL) design, meaning code that previously worked may break with newer more aggressively optimised releases of the compiler. We use the Coq proof assistant to formally specify and verify the behavior of the VivadoHLS dependence pragma. We first embed the syntax and the semantics of a tiny imperative language Imp in Coq and specify a conformance relation between an Imp program and a dependence pragma based on data-flow transformations. We then implement semi-automated methods to formally verify such conformance relations for non-nested loop bodies.}, keywords={}, doi={10.1109/FCCM.2019.00056}, ISSN={2576-2621}, month={April},} @inproceedings{malecha+10, author = {J. Gregory Malecha and Greg Morrisett and Avraham Shinnar and Ryan Wisnesky}, editor = {Manuel V. Hermenegildo and Jens Palsberg}, title = {Toward a verified relational database management system}, booktitle = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23, 2010}, pages = {237--248}, publisher = {{ACM}}, year = {2010}, url = {https://doi.org/10.1145/1706299.1706329}, doi = {10.1145/1706299.1706329}, timestamp = {Tue, 22 Jun 2021 17:10:57 +0200}, biburl = {https://dblp.org/rec/conf/popl/MalechaMSW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{chlipala15, author = {Adam Chlipala}, editor = {Sriram K. Rajamani and David Walker}, title = {From Network Interface to Multithreaded Web Applications: {A} Case Study in Modular Program Verification}, booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2015, Mumbai, India, January 15-17, 2015}, pages = {609--622}, publisher = {{ACM}}, year = {2015}, url = {https://doi.org/10.1145/2676726.2677003}, doi = {10.1145/2676726.2677003}, timestamp = {Wed, 23 Jun 2021 17:06:05 +0200}, biburl = {https://dblp.org/rec/conf/popl/Chlipala15a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{gu+16, author = {Ronghui Gu and Zhong Shao and Hao Chen and Xiongnan (Newman) Wu and Jieung Kim and Vilhelm Sj{\"{o}}berg and David Costanzo}, editor = {Kimberly Keeton and Timothy Roscoe}, title = {CertiKOS: An Extensible Architecture for Building Certified Concurrent {OS} Kernels}, booktitle = {12th {USENIX} Symposium on Operating Systems Design and Implementation, {OSDI} 2016, Savannah, GA, USA, November 2-4, 2016}, pages = {653--669}, publisher = {{USENIX} Association}, year = {2016}, doi = {10.5555/3026877.3026928}, timestamp = {Tue, 02 Feb 2021 08:06:02 +0100}, biburl = {https://dblp.org/rec/conf/osdi/GuSCWKSC16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{braibant+13, author = {Thomas Braibant and Adam Chlipala}, editor = {Natasha Sharygina and Helmut Veith}, title = {Formal Verification of Hardware Synthesis}, booktitle = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8044}, pages = {213--228}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-642-39799-8\_14}, doi = {10.1007/978-3-642-39799-8\_14}, timestamp = {Tue, 14 May 2019 10:00:43 +0200}, biburl = {https://dblp.org/rec/conf/cav/BraibantC13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{bourgeat+20, author = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind}, title = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design}, booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation}, year = 2020, pages = {243-257}, doi = {10.1145/3385412.3385965}, url = {https://doi.org/10.1145/3385412.3385965}, address = {New York, NY, USA}, isbn = 9781450376136, keywords = {Hardware Description Language, Compiler Correctness, Semantics}, location = {London, UK}, numpages = 15, publisher = {ACM}, series = {PLDI 2020}, } @misc{silveroak, author = {Google}, title = {Project Silver Oak: Formal specification and verification of hardware, especially for security and privacy}, year = {2021}, publisher = {GitHub}, journal = {GitHub repository}, howpublished = {\url{https://github.com/project-oak/silveroak}} } @article{compcert, author = {Xavier Leroy}, title = {Formal verification of a realistic compiler}, journal = {Commun. {ACM}}, volume = {52}, number = {7}, pages = {107--115}, year = {2009}, url = {https://doi.org/10.1145/1538788.1538814}, doi = {10.1145/1538788.1538814}, timestamp = {Tue, 06 Nov 2018 12:51:38 +0100}, biburl = {https://dblp.org/rec/journals/cacm/Leroy09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @book{coq, author = {Yves Bertot and Pierre Cast{\'{e}}ran}, title = {Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions}, series = {Texts in Theoretical Computer Science. An {EATCS} Series}, publisher = {Springer}, year = {2004}, url = {https://doi.org/10.1007/978-3-662-07964-5}, doi = {10.1007/978-3-662-07964-5}, isbn = {978-3-642-05880-6}, timestamp = {Tue, 16 May 2017 14:24:38 +0200}, biburl = {https://dblp.org/rec/series/txtcs/BertotC04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{six+20, author = {Cyril Six and Sylvain Boulm{\'{e}} and David Monniaux}, title = {Certified and efficient instruction scheduling: application to interlocked {VLIW} processors}, journal = {Proc. {ACM} Program. Lang.}, volume = {4}, number = {{OOPSLA}}, pages = {129:1--129:29}, year = {2020}, url = {https://doi.org/10.1145/3428197}, doi = {10.1145/3428197}, timestamp = {Thu, 14 Oct 2021 08:48:52 +0200}, biburl = {https://dblp.org/rec/journals/pacmpl/SixBM20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @misc{polybench, author = {Pouchet, Louis-No\"el}, title = {PolyBench/C: the Polyhedral Benchmark suite}, url = {https://sourceforge.net/projects/polybench/}, year = {2016}, } @inproceedings{csmith, author = {Xuejun Yang and Yang Chen and Eric Eide and John Regehr}, editor = {Mary W. Hall and David A. Padua}, title = {Finding and understanding bugs in {C} compilers}, booktitle = {Proceedings of the 32nd {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2011, San Jose, CA, USA, June 4-8, 2011}, pages = {283--294}, publisher = {{ACM}}, year = {2011}, url = {https://doi.org/10.1145/1993498.1993532}, doi = {10.1145/1993498.1993532}, timestamp = {Mon, 02 Aug 2021 08:40:03 +0200}, biburl = {https://dblp.org/rec/conf/pldi/YangCER11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{sdc, author = {Andrew Canis and Stephen Dean Brown and Jason Helge Anderson}, title = {Modulo {SDC} scheduling with recurrence minimization in high-level synthesis}, booktitle = {24th International Conference on Field Programmable Logic and Applications, {FPL} 2014, Munich, Germany, 2-4 September, 2014}, pages = {1--8}, publisher = {{IEEE}}, year = {2014}, url = {https://doi.org/10.1109/FPL.2014.6927490}, doi = {10.1109/FPL.2014.6927490}, timestamp = {Wed, 16 Oct 2019 14:14:53 +0200}, biburl = {https://dblp.org/rec/conf/fpl/CanisBA14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{verismith, author = {Yann Herklotz and John Wickerson}, editor = {Stephen Neuendorffer and Lesley Shannon}, title = {Finding and Understanding Bugs in {FPGA} Synthesis Tools}, booktitle = {{FPGA} '20: The 2020 {ACM/SIGDA} International Symposium on Field-Programmable Gate Arrays, Seaside, CA, USA, February 23-25, 2020}, pages = {277--287}, publisher = {{ACM}}, year = {2020}, url = {https://doi.org/10.1145/3373087.3375310}, doi = {10.1145/3373087.3375310}, timestamp = {Sun, 25 Oct 2020 23:15:07 +0100}, biburl = {https://dblp.org/rec/conf/fpga/HerklotzW20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{perna+12, author = "Juan Perna and Jim Woodcock", title = {Mechanised Wire-Wise Verification of {Handel-C} Synthesis}, journal = "Science of Computer Programming", volume = 77, number = 4, pages = "424 - 443", year = 2012, doi = "10.1016/j.scico.2010.02.007", issn = "0167-6423", } @article{coussy+09, author = {Philippe Coussy and Daniel D. Gajski and Michael Meredith and Andr{\'{e}}s Takach}, title = {An Introduction to High-Level Synthesis}, journal = {{IEEE} Des. Test Comput.}, volume = {26}, number = {4}, pages = {8--17}, year = {2009}, url = {https://doi.org/10.1109/MDT.2009.69}, doi = {10.1109/MDT.2009.69}, timestamp = {Sun, 17 May 2020 11:44:25 +0200}, biburl = {https://dblp.org/rec/journals/dt/CoussyGMT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{pilato13_bambu, author = {C. {Pilato} and F. {Ferrandi}}, booktitle = {2013 23rd International Conference on Field programmable Logic and Applications}, title = {Bambu: A modular framework for the high level synthesis of memory-intensive applications}, year = {2013}, volume = {}, number = {}, pages = {1-4}, doi = {10.1109/FPL.2013.6645550} } @article{huang+15, author = {Qijing Huang and Ruolong Lian and Andrew Canis and Jongsok Choi and Ryan Xi and Nazanin Calagar and Stephen Dean Brown and Jason Helge Anderson}, title = {The Effect of Compiler Optimizations on High-Level Synthesis-Generated Hardware}, journal = {{ACM} Trans. Reconfigurable Technol. Syst.}, volume = {8}, number = {3}, pages = {14:1--14:26}, year = {2015}, url = {https://doi.org/10.1145/2629547}, doi = {10.1145/2629547}, timestamp = {Thu, 18 Jun 2020 15:43:43 +0200}, biburl = {https://dblp.org/rec/journals/trets/HuangLCCXCBA15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @mastersthesis{pardalos_thesis, author = {Pardalos, Michalis}, title = {Formally verified resource sharing for High Level Synthesis}, institution = {Imperial College London}, year = 2021, url = {https://mpardalos.xyz/thesis.pdf} } @INPROCEEDINGS{ferrandi2021_bambu, author={Ferrandi, Fabrizio and Castellana, Vito Giovanni and Curzel, Serena and Fezzardi, Pietro and Fiorito, Michele and Lattuada, Marco and Minutoli, Marco and Pilato, Christian and Tumeo, Antonino}, booktitle={ACM/IEEE Design Automation Conference (DAC)}, title={Bambu: an Open-Source Research Framework for the High-Level Synthesis of Complex Applications}, year={2021}, pages={1327-1330}, publisher={{IEEE}}, doi={10.1109/DAC18074.2021.9586110}, ISSN={0738-100X}, month={Dec}, }