path: root/references.bib

@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},
}