Update on Overleaf.

1 files changed, 151 insertions, 0 deletions

diff --git a/references.bib b/references.bib
new file mode 100644
index 0000000..ed9e2bb
--- /dev/null
+++ b/references.bib
@@ -0,0 +1,151 @@
+@unpublished{Herklotz2020,
+  author          = {Herklotz, Yann and Pollard, James and Ramanathan, Nadesh
+                  and Wickerson, John},
+  title           = {Formal Verification of High-Level Synthesis},
+  year            = 2020,
+  url             = {https://yannherklotz.com/docs/drafts/formal_hls.pdf},
+  urldate         = {2021-1-30},
+  abstract        = {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 de-
+                  signs of comparable performance and energy efficiency to those
+                  coded by hand in a hardware description language like 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. Worse, there is
+                  mounting evidence that existing HLS tools are quite
+                  unreliable, sometimes generating wrong hard- ware or crashing
+                  when given valid inputs. To address this problem, we present
+                  the first HLS tool that is mechanically verified to preserve
+                  the behaviour of its in- put software. Our tool, called
+                  Vericert, extends the Comp- Cert verified C compiler with a
+                  new hardware-oriented in- termediate language and a Verilog
+                  back end, and has been proven correct in Coq. Vericert
+                  supports all C constructs ex- cept for case statements,
+                  function pointers, recursive func- tion calls, integers larger
+                  than 32 bits, floats, and global vari- ables. An evaluation on
+                  the PolyBench/C benchmark suite indicates that Vericert
+                  generates hardware that is around an order of magnitude slower
+                  and larger than hardware gener- ated by an existing,
+                  optimising (but unverified) HLS tool.},
+  tags            = {Vericert,HLS,Verified},
+}
+
+@misc{intel_hls,
+  publisher       = {Intel},
+  title           = {Intel High Level Synthesis Compiler},
+  year            = 2021,
+  url             = {https://www.intel.com/content/www/us/en/software/programmable/quartus-prime/hls-compiler.html},
+}
+
+@misc{xilinx_vitis,
+  publisher       = {Xilinx Inc.},
+  title           = {Vitis HLS},
+  year            = 2021,
+  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},
+}