Update references

1 files changed, 13 insertions, 34 deletions

diff --git a/references.bib b/references.bib
index 28aff54..cec647e 100644
--- a/references.bib
+++ b/references.bib
@@ -1,37 +1,16 @@
-@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},
+@article{Herklotz2020,
+	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 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. 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\texttimes{} slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.},
+	author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
+	location = {New York, NY, USA},
+	publisher = {Association for Computing Machinery},
+	url = {https://doi.org/10.1145/3485494},
+	date = {2021-10},
+	doi = {10.1145/3485494},
+	journaltitle = {Proc. ACM Program. Lang.},
+	keywords = {high-level synthesis,Coq,Verilog,CompCert,C},
+	number = {OOPSLA},
+	title = {Formal Verification of High-Level Synthesis},
+	volume = {5}
 }
 
 @misc{intel_hls,