Fix up the fonts

5 files changed, 1139 insertions, 17 deletions

diff --git a/hls.tex b/hls.tex
index 4ea51d8..4feaa14 100644
--- a/hls.tex
+++ b/hls.tex
@@ -1 +1,108 @@
 \chapter{Formal Verification of High-Level Synthesis}
+
+\newcommand{\slowdownOrig}{27}
+\newcommand{\slowdownDiv}{2}
+\newcommand{\areaIncr}{1.1}
+
+\paragraph{Can you trust your high-level synthesis tool?}
+
+As latency, throughput, and energy efficiency become increasingly important, custom hardware
+accelerators are being designed for numerous applications.  Alas, designing these accelerators can
+be a tedious and error-prone process using a hardware description language (HDL) such as Verilog.
+An attractive alternative is \emph{high-level synthesis} (HLS), in which hardware designs are
+automatically compiled from software written in a high-level language like C.  Modern HLS tools such
+as LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel
+i++~\cite{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and
+energy-efficiency to those hand-written in an HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341},
+while offering the convenient abstractions and rich ecosystems of software development.  But
+existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to
+the software they were given, and this undermines any reasoning conducted at the software level.
+
+Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence.
+For instance, Vivado HLS has been shown to apply pipelining optimisations
+incorrectly\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or to silently generate wrong
+code should the programmer stray outside the fragment of C that it
+supports.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}} Meanwhile,
+\citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now
+Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on so
+many of their test inputs.  More recently,
+\citet{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
+using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated
+programs to the C fragment explicitly supported by all the tools, they still found that on average
+2.5\% of test-cases were compiled to designs that behaved incorrectly.
+
+\paragraph{Existing workarounds}
+
+Aware of the reliability shortcomings of HLS tools, hardware designers routinely check the generated
+hardware for functional correctness. This is commonly done by simulating the generated design
+against a large test-bench. But unless the test-bench covers all inputs exhaustively -- which is
+often infeasible -- there is a risk that bugs remain.
+
+One alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove equivalence
+between the input program and the output design. Translation validation has been successfully
+applied to several HLS
+optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.
+Nevertheless, it is an expensive task, especially for large designs, and it must be repeated every
+time the compiler is invoked.  For example, the translation validation for Catapult
+C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert
+`adjustments'~\cite[p.~3]{slec_whitepaper} to the input C program before validation succeeds. And
+even when it succeeds, translation validation does not provide watertight guarantees unless the
+validator itself has been mechanically proven
+correct~\cite[e.g.][]{tristan08_formal_verif_trans_valid}, which has not been the case in HLS tools
+to date.
+
+Our position is that none of the above workarounds are necessary if the HLS tool can simply be
+trusted to work correctly.
+
+\paragraph{Our solution}
+
+We have designed a new HLS tool in the Coq theorem prover and proved that any output design it
+produces always has the same behaviour as its input program. Our tool, called Vericert, is
+automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is
+the same as the implementation of the tool. Vericert is built by extending the CompCert verified C
+compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate
+language and a Verilog back end. It supports most C constructs, including integer operations,
+function calls (which are all inlined), local arrays, structs, unions, and general control-flow
+statements, but currently excludes support for case statements, function pointers, recursive
+function calls, non-32-bit integers, floats, and global variables.
+
+\paragraph{Contributions and Outline}
+The contributions of this paper are as follows:
+
+\begin{itemize}
+  \item We present Vericert, the first mechanically verified HLS tool that compiles C to Verilog. In
+        Section~\ref{sec:design}, we describe the design of Vericert, including certain
+        optimisations related to memory accesses and division.
+  \item We state the correctness theorem of Vericert with respect to an existing semantics for
+        Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we
+        describe how we extended this semantics to make it suitable as an HLS target.  We also
+        describe how the Verilog semantics is integrated into CompCert's language execution model
+        and its framework for performing simulation proofs. A mapping of CompCert's infinite memory
+        model onto a finite Verilog array is also described.
+  \item In Section~\ref{sec:proof}, we describe how we proved the correctness theorem. The proof
+        follows standard CompCert techniques -- forward simulations, intermediate specifications,
+        and determinism results -- but we encountered several challenges peculiar to our
+        hardware-oriented
+        setting.
+        These include handling discrepancies between the byte-addressed memory assumed by the input
+        software and the word-addressed memory that we implement in the output hardware, different
+        handling of unsigned comparisons between C and Verilog, and carefully implementing memory
+        reads and writes so that these behave properly as a RAM in hardware.
+  \item In Section~\ref{sec:evaluation}, we evaluate Vericert on the PolyBench/C benchmark
+        suite~\cite{polybench}, and compare the performance of our generated hardware against an
+        existing, unverified HLS tool called LegUp~\cite{canis11_legup}. We show that Vericert
+        generates hardware that is \slowdownOrig$\times$ slower (\slowdownDiv$\times$ slower in the
+        absence of division) and \areaIncr$\times$ larger than that generated by LegUp. This
+        performance gap can be largely attributed to Vericert's current lack of support for
+        instruction-level parallelism and the absence of an efficient, pipelined division
+        operator. We intend to close this gap in the future by introducing (and verifying) HLS
+        optimisations of our own, such as scheduling and memory analysis.  This section also reports
+        on our campaign to fuzz-test Vericert using over a hundred thousand random C programs
+        generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm that its
+        correctness theorem is watertight.
+\end{itemize}
+
+\paragraph{Companion material}
+Vericert is fully open source and available on GitHub at
+\url{https://github.com/ymherklotz/vericert}. A snapshot of the Vericert development is also
+available in a Zenodo repository~\cite{yann_herklotz_2021_5093839}.
diff --git a/introduction.tex b/introduction.tex
index 61be79c..f4ec3a1 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -1,17 +1 @@
 \chapter{Introduction}
-
-Lorem ipsum dolor sit amet, consectetur adipiscing elit. Suspendisse ante turpis, feugiat porta
-pellentesque sit amet, feugiat varius ligula. Nulla facilisi. Nam malesuada massa quis ex dignissim
-viverra. Duis feugiat elit ut consequat varius. Quisque dapibus elit lorem, sed aliquam risus
-tincidunt ac. Duis turpis est, blandit vel posuere at, facilisis at neque. Proin in lacus lobortis
-orci sagittis malesuada. In hac habitasse platea dictumst. Nunc dolor nisl, consequat nec elementum
-at, ultricies ac nulla.
-This is normal text.%
-
-Fusce accumsan mattis sapien, at ornare felis fringilla eu. Vivamus fermentum consectetur urna id egestas. Vivamus nec mi quis leo mollis rhoncus vitae non est. Integer auctor, nisi vitae egestas rhoncus, odio arcu finibus velit, nec bibendum urna dolor non neque. Curabitur sit amet arcu at velit varius varius. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Fusce pretium metus ac augue ultricies, ut euismod elit fringilla. Nunc imperdiet ligula turpis. Cras dignissim mi ac quam dapibus iaculis. Maecenas facilisis felis a leo mattis rutrum. Morbi vestibulum, velit quis convallis condimentum, odio dui tincidunt nibh, ac volutpat diam magna consectetur ligula.
-
-Aenean rhoncus tortor nec velit viverra rhoncus. Praesent in convallis massa. Proin tincidunt scelerisque risus. Pellentesque a faucibus nisl, vel imperdiet felis. Donec vel sapien placerat augue fringilla dapibus nec a dui. Fusce feugiat pellentesque nisi, vitae feugiat lacus convallis vel. Ut ullamcorper, lacus at scelerisque imperdiet, quam nulla varius velit, sed auctor lacus ante et purus. Vestibulum ante ipsum primis in faucibus orci luctus et ultrices posuere cubilia curae;
-
-Ut luctus volutpat orci sit amet tristique. Duis tincidunt neque efficitur libero vehicula dictum. Aliquam vitae rhoncus mauris, nec convallis nisi. Nulla facilisi. Fusce in nulla egestas, ultricies mauris vel, condimentum felis. Nunc vel mattis massa, at ornare enim. Mauris ornare elit non metus eleifend, quis viverra dui ultrices. Morbi ut purus ac velit ullamcorper interdum ac sit amet mauris. Aenean scelerisque, mauris quis vehicula faucibus, enim nisi malesuada quam, in facilisis sapien nisi quis purus. Ut iaculis lorem tellus, sed fermentum est elementum id. Cras sit amet eleifend quam, nec maximus mi. Donec bibendum nibh in dolor fermentum convallis. Pellentesque mollis, odio nec laoreet viverra, elit metus malesuada tellus, quis rutrum nunc est sit amet urna. Nullam ultrices augue eu lacinia molestie. Donec maximus quam ipsum, id tristique tortor molestie fermentum.
-
-Mauris egestas nisi in est commodo, ut pharetra arcu gravida. Nullam non lectus eu tellus scelerisque volutpat eget eu velit. In nec consequat magna. Mauris ultricies nunc et suscipit hendrerit. Curabitur non dapibus risus, non posuere augue. Cras faucibus elementum neque at porta. Cras nibh nunc, facilisis a posuere nec, tempus at dolor. Sed sagittis ullamcorper arcu, sit amet eleifend turpis sagittis a. Nam varius bibendum magna, quis porttitor turpis dignissim id. Mauris ac hendrerit ex. Integer tellus mauris, varius vel ullamcorper eu, rhoncus eu nisl. Vestibulum rutrum nunc pharetra sollicitudin hendrerit. Vestibulum sit amet est leo. Suspendisse at posuere diam.
diff --git a/main.pdf b/main.pdf
index 4dd0e41..b1a4ab6 100644
--- a/main.pdf
+++ b/main.pdf
diff --git a/main.tex b/main.tex
index edda3e6..9b94bd6 100644
--- a/main.tex
+++ b/main.tex
@@ -15,13 +15,24 @@
   conclusion
 }
 
+\linespread{1.3}
+
 \usepackage{graphicx}
 \usepackage{amsmath}
-\usepackage[utf8]{inputenc}
+\usepackage{amsthm}
+
+\usepackage[british]{babel}
+%\usepackage[utf8]{inputenc}
 \usepackage[sc]{mathpazo}
 \usepackage{newpxmath}
+\usepackage{newpxtext}
+\usepackage{inconsolata}
+\usepackage{microtype}
 \addtokomafont{disposition}{\rmfamily}
 
+\usepackage[natbib=true,style=alphabetic]{biblatex}
+\addbibresource{references.bib}
+
 \usepackage{epigraph}
 \setlength\epigraphwidth{1\textwidth}
 \setlength\epigraphrule{0pt} % no line between
@@ -37,6 +48,19 @@
 \newcommand{\ymhfw}{\textcolor{ymhfwcol}{FW}}
 \newcommand{\ymhwip}{\textcolor{ymhwipcol}{WIP}}
 
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}
+\newtheorem*{remark}{Remark}
+
+\hyphenation{Comp-Cert}
+\hyphenation{Veri-cert}
+\hyphenation{Poly-Bench}
+\hyphenation{Leg-Up}
+\hyphenation{straight-for-ward}
+\hyphenation{cor-re-la-tion}
+\hyphenation{gram-schmi-dt}
+\hyphenation{de-riche}
+
 \begin{document}
 
 \maketitle
@@ -52,4 +76,6 @@
 \include{schedule}
 \include{conclusion}
 
+\printbibliography{}
+
 \end{document}
diff --git a/references.bib b/references.bib
new file mode 100644
index 0000000..8e62840
--- /dev/null
+++ b/references.bib
@@ -0,0 +1,1005 @@
+@article{leroy09_formal_verif_realis_compil,
+  author =       {Leroy, Xavier},
+  title =        {Formal Verification of a Realistic Compiler},
+  journal =      {Commun. ACM},
+  volume =       52,
+  number =       7,
+  pages =        {107-115},
+  year =         2009,
+  doi =          {10.1145/1538788.1538814},
+  address =      {New York, NY, USA},
+  issn =         {0001-0782},
+  issue_date =   {July 2009},
+  month =        jul,
+  numpages =     9,
+  publisher =    {ACM},
+}
+
+@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.},
+  number    = {{OOPSLA}},
+  year      = {2020}
+ }
+
+@inproceedings{lidbury15_many_core_compil_fuzzin,
+  author          = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
+                  Alastair F.},
+  title           = {Many-Core Compiler Fuzzing},
+  booktitle       = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
+                  and Implementation},
+  year            = 2015,
+  pages           = {65-76},
+  doi             = {10.1145/2737924.2737986},
+  address         = {New York, NY, USA},
+  isbn            = 9781450334686,
+  location        = {Portland, OR, USA},
+  numpages        = 12,
+  publisher       = {ACM},
+  series          = {PLDI '15},
+}
+
+@misc{polybench,
+author = {Pouchet, Louis-No\"el},
+title = {PolyBench/C: the Polyhedral Benchmark suite},
+url = {http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/},
+year = {2020},
+}
+
+@INPROCEEDINGS{5522874,
+  author={Dan Gajski and Todd Austin and Steve Svoboda},
+  booktitle={Design Automation Conference},
+  title={What input-language is the best choice for high level synthesis (HLS)?},
+  year={2010},
+  volume={},
+  number={},
+  pages={857-858},
+  doi={10.1145/1837274.1837489}}
+
+@inproceedings{bluespec,
+  author={Nikhil, Rishiyur S. },
+  booktitle={Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.},
+  title={Bluespec System Verilog: efficient, correct RTL from high level specifications},
+  year={2004},
+  volume={},
+  number={},
+  pages={69-70},
+  doi={10.1109/MEMCOD.2004.1459818}}
+
+@inproceedings{davidthomas_asap16,
+  author    = {Thomas, David B.},
+  title     = {Synthesisable recursion for {C++} {HLS} tools},
+  booktitle = {{ASAP}},
+  pages     = {91--98},
+  publisher = {{IEEE} Computer Society},
+  year      = {2016},
+  doi = {10.1109/ASAP.2016.7760777}
+}
+
+@article{cong+11,
+  author    = {Jason Cong and
+               Bin Liu and
+               Stephen Neuendorffer and
+               Juanjo Noguera and
+               Kees A. Vissers and
+               Zhiru Zhang},
+  title     = {High-Level Synthesis for FPGAs: From Prototyping to Deployment},
+  journal   = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
+  volume    = {30},
+  number    = {4},
+  pages     = {473--491},
+  year      = {2011},
+  doi = {10.1109/TCAD.2011.2110592}
+}
+
+@inproceedings{kiwi,
+  author    = {David J. Greaves and
+               Satnam Singh},
+  title     = {Kiwi: Synthesis of {FPGA} Circuits from Parallel Programs},
+  booktitle = {{FCCM}},
+  pages     = {3--12},
+  publisher = {{IEEE} Computer Society},
+  year      = {2008},
+  doi={10.1109/FCCM.2008.46}
+}
+
+@inproceedings{spatial,
+  author    = {David Koeplinger and
+               Matthew Feldman and
+               Raghu Prabhakar and
+               Yaqi Zhang and
+               Stefan Hadjis and
+               Ruben Fiszel and
+               Tian Zhao and
+               Luigi Nardi and
+               Ardavan Pedram and
+               Christos Kozyrakis and
+               Kunle Olukotun},
+  title     = {Spatial: A Language and Compiler for Application Accelerators},
+  booktitle = {{PLDI}},
+  pages     = {296--311},
+  publisher = {{ACM}},
+  year      = {2018},
+  doi       = {https://doi.org/10.1145/3192366.3192379}
+}
+
+@misc{greaves_note,
+      title={Research Note: An Open Source Bluespec Compiler},
+      author={David J. Greaves},
+      year={2019},
+      eprint={1905.03746},
+      archivePrefix={arXiv},
+      primaryClass={cs.PL}
+}
+
+@article{takach16_high_level_synth,
+  author          = {A. {Takach}},
+  title           = {High-Level Synthesis: Status, Trends, and Future
+                  Directions},
+  journal         = {IEEE Design Test},
+  volume          = {33},
+  number          = {3},
+  pages           = {116-124},
+  year            = {2016},
+  doi             = {10.1109/MDAT.2016.2544850},
+  url             = {https://doi.org/10.1109/MDAT.2016.2544850},
+  ISSN            = {2168-2364},
+  month           = {June},
+}
+
+@inproceedings{liu16_effic_high_level_synth_desig,
+  author          = { {Dong Liu} and B. C. {Schafer}},
+  title           = {Efficient and reliable High-Level Synthesis Design Space
+                  Explorer for FPGAs},
+  booktitle       = {2016 26th International Conference on Field Programmable
+                  Logic and Applications (FPL)},
+  year            = 2016,
+  pages           = {1-8},
+  doi             = {10.1109/FPL.2016.7577370},
+  ISSN            = {1946-1488},
+  month           = {Aug},
+}
+
+@article{lahti19_are_we_there_yet,
+  author          = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and
+                  T. D. {H{\"a}m{\"a}l{\"a}inen}},
+  title           = {Are We There Yet? a Study on the State of High-Level
+                  Synthesis},
+  journal         = {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume          = {38},
+  number          = {5},
+  pages           = {898-911},
+  year            = {2019},
+  doi             = {10.1109/TCAD.2018.2834439},
+  ISSN            = {1937-4151},
+  month           = {May},
+}
+
+@misc{mentor20_catap_high_level_synth,
+  author          = {Mentor},
+  title           = {Catapult High-Level Synthesis},
+  url             = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls},
+  urldate         = {2020-06-06},
+  year            = 2020,
+}
+
+@inproceedings{gupta03_spark,
+  author          = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}},
+  title           = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
+                  transformations},
+  booktitle       = {16th International Conference on VLSI Design, 2003. Proceedings.},
+  year            = 2003,
+  pages           = {461-466},
+  doi             = {10.1109/ICVD.2003.1183177},
+  url             = {https://doi.org/10.1109/ICVD.2003.1183177},
+  ISSN            = {1063-9667},
+  month           = {Jan},
+}
+
+@article{chouksey20_verif_sched_condit_behav_high_level_synth,
+  author          = {R. {Chouksey} and C. {Karfa}},
+  title           = {Verification of Scheduling of Conditional Behaviors in
+                  High-Level Synthesis},
+  journal         = {IEEE Transactions on Very Large Scale Integration (VLSI)
+                  Systems},
+  volume          = {},
+  number          = {},
+  pages           = {1-14},
+  year            = {2020},
+  doi             = {10.1109/TVLSI.2020.2978242},
+  url             = {https://doi.org/10.1109/TVLSI.2020.2978242},
+  ISSN            = {1557-9999},
+  month           = {},
+}
+
+@inproceedings{pnueli98_trans,
+  author          = "Pnueli, A.  and Siegel, M.  and Singerman, E.",
+  title           = "Translation validation",
+  booktitle       = "Tools and Algorithms for the Construction and Analysis of Systems",
+  year            = 1998,
+  pages           = "151--166",
+  address         = "Berlin, Heidelberg",
+  editor          = "Steffen, Bernhard",
+  isbn            = "978-3-540-69753-4",
+  publisher       = "Springer",
+  doi = "10.1007/BFb0054170"
+}
+
+@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
+  author =       {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
+  title =        {Translation Validation of Code Motion Transformations
+                  Involving Loops},
+  journal =      {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume =       38,
+  number =       7,
+  pages =        {1378-1382},
+  year =         2019,
+  doi =          {10.1109/TCAD.2018.2846654},
+  ISSN =         {1937-4151},
+  month =        {July},
+}
+
+@article{banerjee14_verif_code_motion_techn_using_value_propag,
+  author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
+  title = {Verification of Code Motion Techniques Using Value
+                  Propagation},
+  journal = {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume = 33,
+  number = 8,
+  pages = {1180-1193},
+  year = 2014,
+  doi = {10.1109/TCAD.2014.2314392},
+  ISSN = {1937-4151},
+  month = {Aug}
+}
+
+@inproceedings{kim04_autom_fsmd,
+  author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
+  title = {Automated formal verification of scheduling process using
+                  finite state machines with datapath (FSMD)},
+  booktitle = {International Symposium on Signals, Circuits and
+                  Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
+  year = 2004,
+  pages = {110-115},
+  doi = {10.1109/ISQED.2004.1283659},
+  month = {March}
+}
+
+@inproceedings{karfa06_formal_verif_method_sched_high_synth,
+  author =       {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
+                  Reade, Chris},
+  title =        {A Formal Verification Method of Scheduling in High-level
+                  Synthesis},
+  booktitle =    {Proceedings of the 7th International Symposium on Quality
+                  Electronic Design},
+  year =         2006,
+  pages =        {71--78},
+  doi =          {10.1109/ISQED.2006.10},
+  acmid =        1126731,
+  address =      {Washington, DC, USA},
+  isbn =         {0-7695-2523-7},
+  numpages =     8,
+  publisher =    {IEEE Computer Society},
+  series =       {ISQED '06},
+}
+
+@inproceedings{leroy06_formal_certif_compil_back_end,
+  author = {Leroy, Xavier},
+  title = {Formal Certification of a Compiler Back-End or: Programming
+                  a Compiler with a Proof Assistant},
+  booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium
+                  on Principles of Programming Languages},
+  year = 2006,
+  pages = {42-54},
+  doi = {10.1145/1111037.1111042},
+  url = {https://doi.org/10.1145/1111037.1111042},
+  address = {New York, NY, USA},
+  isbn = 1595930272,
+  location = {Charleston, South Carolina, USA},
+  numpages = 13,
+  publisher = {ACM},
+  series = {POPL '06}
+}
+
+@book{bertot04_inter_theor_provin_progr_devel,
+  author          = {Yves Bertot and Pierre Cast{\'{e}}ran},
+  title           = {Interactive Theorem Proving and Program Development},
+  year            = 2004,
+  publisher       = {Springer Berlin Heidelberg},
+  url             = {https://doi.org/10.1007/978-3-662-07964-5},
+  doi             = {10.1007/978-3-662-07964-5},
+}
+
+@inproceedings{tristan08_formal_verif_trans_valid,
+  author = {Tristan, Jean-Baptiste and Leroy, Xavier},
+  title = {Formal Verification of Translation Validators: A Case Study on
+                  Instruction Scheduling Optimizations},
+  booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on
+                  Principles of Programming Languages},
+  year = 2008,
+  pages = {17-27},
+  doi = {10.1145/1328438.1328444},
+  address = {New York, NY, USA},
+  isbn = 9781595936899,
+  location = {San Francisco, California, USA},
+  numpages = 11,
+  publisher = {ACM},
+  series = {POPL '08}
+}
+
+@inproceedings{kundu08_valid_high_level_synth,
+  author          = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
+  title           = "Validating High-Level Synthesis",
+  booktitle       = "Computer Aided Verification",
+  year            = 2008,
+  pages           = "459--472",
+  address         = "Berlin, Heidelberg",
+  editor          = "Gupta, Aarti and Malik, Sharad",
+  isbn            = "978-3-540-70545-1",
+  publisher       = "Springer",
+  doi = "10.1007/978-3-540-70545-1_44"
+}
+
+@inproceedings{chapman92_verif_bedroc,
+  author          = {R. {Chapman} and G. {Brown} and M. {Leeser}},
+  title           = {Verified high-level synthesis in BEDROC},
+  booktitle       = {[1992] Proceedings The European Conference on Design Automation},
+  year            = 1992,
+  pages           = {59--63},
+  doi             = {10.1109/EDAC.1992.205894},
+  month           = {March},
+  publisher       = {IEEE Computer Society},
+}
+
+@article{hwang91_formal_approac_to_sched_probl,
+  author = {C. -. {Hwang} and J. -. {Lee} and Y. -. {Hsu}},
+  title = {A Formal Approach To the Scheduling Problem in High Level
+                  Synthesis},
+  journal = {IEEE Transactions on Computer-Aided Design of Integrated
+                  Circuits and Systems},
+  volume = 10,
+  number = 4,
+  pages = {464-475},
+  year = 1991,
+  doi = {10.1109/43.75629},
+  url = {https://doi.org/10.1109/43.75629},
+  month = {April}
+}
+
+@inproceedings{page91_compil_occam,
+  author = {Page, Ian and Luk, Wayne},
+  title = {Compiling Occam into field-programmable gate arrays},
+  booktitle = {FPGAs, Oxford Workshop on Field Programmable Logic and
+                  Applications},
+  year = 1991,
+  volume = 15,
+  pages = {271--283},
+}
+
+@inproceedings{grass94_high,
+  author = {W. {Grass} and M. {Mutz} and W. -. {Tiedemann}},
+  title = {High level synthesis based on formal methods},
+  booktitle = {Proceedings of Twentieth Euromicro Conference. System
+                  Architecture and Integration},
+  year = 1994,
+  pages = {83-91},
+  doi = {10.1109/EURMIC.1994.390403},
+  month = {Sep.}
+}
+
+@inproceedings{jifeng93_towar,
+  author = "Jifeng, He and Page, Ian and Bowen, Jonathan",
+  title = "Towards a provably correct hardware implementation of Occam",
+  booktitle = "Correct Hardware Design and Verification Methods",
+  year = 1993,
+  pages = "214--225",
+  address = "Berlin, Heidelberg",
+  editor = "Milne, George J.  and Pierre, Laurence",
+  isbn = "978-3-540-70655-7",
+  publisher = "Springer"
+}
+
+@article{perna12_mechan_wire_wise_verif_handel_c_synth,
+  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{perna11_correc_hardw_synth,
+  author = "Perna, Juan and Woodcock, Jim and Sampaio, Augusto and Iyoda,
+                  Juliano",
+  title = {Correct Hardware Synthesis},
+  journal = "Acta Informatica",
+  volume = 48,
+  number = 7,
+  pages = "363--396",
+  year = 2011,
+  doi = "10.1007/s00236-011-0142-y",
+  day = 01,
+  issn = "1432-0525",
+  month = "Dec"
+}
+
+@phdthesis{ellis08,
+  author = {Ellis, Martin},
+  title = {Correct synthesis and integration of compiler-generated function units},
+  school = {Newcastle University},
+  url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
+  year = {2008},
+}
+
+
+
+@misc{slec_whitepaper,
+  author = {Chauhan, Pankaj},
+  title = {Formally Ensuring Equivalence between C++ and RTL designs},
+  url = {https://bit.ly/2KbT0ki},
+  year = {2020},
+}
+
+@inproceedings{loow19_verif_compil_verif_proces,
+  author =       {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
+                  Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
+                  and Fox, Anthony},
+  title =        {Verified Compilation on a Verified Processor},
+  tags =         {verification},
+  booktitle =    {Proceedings of the 40th ACM SIGPLAN Conference on Programming
+                  Language Design and Implementation},
+  year =         2019,
+  pages =        {1041--1053},
+  doi =          {10.1145/3314221.3314622},
+  acmid =        3314622,
+  address =      {New York, NY, USA},
+  isbn =         {978-1-4503-6712-7},
+  keywords =     {compiler verification, hardware verification, program
+                  verification, verified stack},
+  location =     {Phoenix, AZ, USA},
+  numpages =     13,
+  publisher =    {ACM},
+  series =       {PLDI 2019},
+}
+
+@inproceedings{canis11_legup,
+  author          = {Andrew Canis and Jongsok Choi and Mark Aldham and Victor Zhang and Ahmed
+                  Kammoona and Jason Helge Anderson and Stephen Dean Brown and Tomasz S. Czajkowski},
+  title           = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
+  booktitle       = {{FPGA}},
+  year            = 2011,
+  pages           = {33--36},
+  publisher       = {{ACM}},
+  doi = {10.1145/1950413.1950423}
+}
+
+@INPROCEEDINGS{choi+18,
+  author={Y. {Choi} and J. {Cong}},
+  booktitle={2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
+  title={HLS-Based Optimization and Design Space Exploration for Applications with Variable Loop Bounds},
+  year={2018},
+  volume={},
+  number={},
+  pages={1-8},
+  doi={10.1145/3240765.3240815}}
+
+
+@book{micheli94_synth_optim_digit_circuit,
+  author          = {De Micheli, Giovanni},
+  title           = {Synthesis and Optimization of Digital Circuits},
+  year            = 1994,
+  publisher       = {McGraw-Hill Higher Education},
+  edition         = {1st},
+  isbn            = 0070163332,
+}
+
+@article{05_ieee_stand_veril_regis_trans_level_synth,
+  title           = {{IEEE} Standard for {Verilog} Register Transfer Level Synthesis},
+  journal         = {IEC 62142-2005 First edition 2005-06 IEEE Std 1364.1},
+  volume          = {},
+  number          = {},
+  pages           = {1-116},
+  year            = {2005},
+  doi             = {10.1109/IEEESTD.2005.339572},
+  url             = {https://doi.org/10.1109/IEEESTD.2005.339572},
+  ISSN            = {},
+  key             = {IEEE Std 1364.1},
+  keywords        = {IEC Standards;Verilog;Registers},
+  month           = {},
+  type            = {Standard},
+}
+
+@article{06_ieee_stand_veril_hardw_descr_languag,
+  author          = {},
+  title           = {{IEEE} Standard for Verilog Hardware Description Language},
+  journal         = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
+  volume          = {},
+  number          = {},
+  pages           = {1-590},
+  year            = {2006},
+  doi             = {10.1109/IEEESTD.2006.99495},
+  url             = {https://doi.org/10.1109/IEEESTD.2006.99495},
+  ISSN            = {},
+  key             = {IEEE Std 1364},
+  month           = {April},
+  type            = {Standard},
+}
+
+@misc{xilinx20_vivad_high_synth,
+  author          = {Xilinx},
+  title           = {Vivado High-level Synthesis},
+  url             = {https://bit.ly/39ereMx},
+  urldate         = {2020-07-20},
+  year            = 2020,
+}
+
+@misc{intel_hls,
+  author = {Intel},
+  title = {High-level Synthesis Compiler},
+  url = {https://intel.ly/2UDiWr5},
+  urldate = {2020-11-18},
+  year = {2020},
+  }
+
+@misc{intel20_sdk_openc_applic,
+  author          = {Intel},
+  title           = {{SDK} for {OpenCL} Applications},
+  url             = {https://intel.ly/30sYHz0},
+  urldate         = {2020-07-20},
+  year            = 2020,
+}
+
+@inproceedings{homsirikamol+14,
+  author    = {Ekawat Homsirikamol and
+               Kris Gaj},
+  title     = {Can high-level synthesis compete against a hand-written code in the
+               cryptographic domain? {A} case study},
+  booktitle = {ReConFig},
+  pages     = {1--8},
+  publisher = {{IEEE}},
+  year      = {2014},
+  doi={10.1109/ReConFig.2014.7032504}
+}
+
+@INPROCEEDINGS{7818341,
+  author={Maxime Pelcat and C\'edric Bourrasset and Luca Maggiani and François Berry},
+  booktitle={2016 International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS)},
+  title={Design productivity of a high level synthesis compiler versus HDL},
+  year={2016},
+  volume={},
+  number={},
+  pages={140-147},
+  doi={10.1109/SAMOS.2016.7818341}}
+
+@misc{silexicahlshdl,
+author = {Gauthier, Stephane and Wadood, Zubair},
+title = {High-Level Synthesis: Can it outperform hand-coded {HDL}?},
+note = {White paper},
+url = {https://info.silexica.com/high-level-synthesis/1},
+year = {2020},
+}
+
+@inproceedings{bambu_hls,
+  author    = {Christian Pilato and
+               Fabrizio Ferrandi},
+  title     = {Bambu: {A} modular framework for the high level synthesis of memory-intensive
+               applications},
+  booktitle = {{FPL}},
+  pages     = {1--4},
+  publisher = {{IEEE}},
+  year      = {2013},
+  doi       = {10.1109/FPL.2013.6645550}
+}
+
+@inproceedings{nigam20_predic_accel_desig_time_sensit_affin_types,
+  author          = {Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and
+                  Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang,
+                  Zhiru},
+  title           = {Predictable Accelerator Design with Time-Sensitive Affine Types},
+  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
+                  and Implementation},
+  year            = 2020,
+  pages           = {393-407},
+  doi             = {10.1145/3385412.3385974},
+  url             = {https://doi.org/10.1145/3385412.3385974},
+  address         = {New York, NY, USA},
+  isbn            = 9781450376136,
+  keywords        = {Affine Type Systems, High-Level Synthesis},
+  location        = {London, UK},
+  numpages        = 15,
+  publisher       = {ACM},
+  series          = {PLDI 2020},
+}
+
+@inproceedings{bourgeat20_essen_blues,
+  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},
+}
+
+@inproceedings{yang11_findin_under_bugs_c_compil,
+	author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
+	title = {Finding and Understanding Bugs in {C} Compilers},
+	booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
+                  and Implementation},
+	year = 2011,
+	pages = {283-294},
+	doi = {10.1145/1993498.1993532},
+	url = {https://doi.org/10.1145/1993498.1993532},
+	address = {New York, NY, USA},
+	isbn = 9781450306638,
+	keywords = {random program generation, random testing, automated testing, compiler testing,
+                  compiler defect},
+	location = {San Jose, California, USA},
+	numpages = 12,
+	publisher = {ACM},
+	series = {PLDI '11}
+}
+
+@inproceedings{blazy05_formal_verif_memor_model_c,
+	author = "Blazy, Sandrine and Leroy, Xavier",
+	title = "Formal Verification of a Memory Model for {C}-Like Imperative
+                  Languages",
+	tags = {verification},
+	booktitle = "Formal Methods and Software Engineering",
+	year = 2005,
+	pages = "280--299",
+	address = "Berlin, Heidelberg",
+	editor = "Lau, Kung-Kiu and Banach, Richard",
+	isbn = "978-3-540-32250-4",
+	publisher = "Springer Berlin Heidelberg",
+	doi = {0.1007/11576280_20}
+}
+
+@inproceedings{slind08_brief_overv_hol4,
+  author          = "Slind, Konrad and Norrish, Michael",
+  title           = "A Brief Overview of {HOL4}",
+  booktitle       = "Theorem Proving in Higher Order Logics",
+  year            = 2008,
+  pages           = "28--32",
+  address         = "Berlin, Heidelberg",
+  editor          = "Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne",
+  isbn            = "978-3-540-71067-7",
+  keywords        = {theorem proving;HOL},
+  publisher       = "Springer Berlin Heidelberg",
+}
+
+@inproceedings{meredith10_veril,
+	author = {P. {Meredith} and M. {Katelman} and J. {Meseguer} and
+                  G. {Ro{\c{s}}u}},
+	title = {A formal executable semantics of {Verilog}},
+	tags = {semantics},
+	booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and
+                  Models for Codesign (MEMOCODE 2010)},
+	year = 2010,
+	pages = {179-188},
+	doi = {10.1109/MEMCOD.2010.5558634},
+	url = {https://doi.org/10.1109/MEMCOD.2010.5558634},
+	month = {July}
+}
+
+@inproceedings{jourdan12_valid_lr_parser,
+	author = "Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and
+                  Leroy, Xavier",
+	title = "Validating LR(1) Parsers",
+	booktitle = "Programming Languages and Systems",
+	year = 2012,
+	pages = "397--416",
+	address = "Berlin, Heidelberg",
+	editor = "Seidl, Helmut",
+	isbn = "978-3-642-28869-2",
+	publisher = "Springer Berlin Heidelberg",
+	doi = "10.1007/978-3-642-28869-2_20"
+}
+
+@inproceedings{zhao12_formal_llvm_inter_repres_verif_progr_trans,
+  author    = {Jianzhou Zhao and
+               Santosh Nagarakatte and
+               Milo M. K. Martin and
+               Steve Zdancewic},
+  editor    = {John Field and
+               Michael Hicks},
+  title     = {Formalizing the {LLVM} intermediate representation for verified program
+               transformations},
+  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
+               of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
+               USA, January 22-28, 2012},
+  pages     = {427--440},
+  publisher = {{ACM}},
+  year      = {2012},
+  url       = {https://doi.org/10.1145/2103656.2103709},
+  doi       = {10.1145/2103656.2103709},
+  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
+  biburl    = {https://dblp.org/rec/conf/popl/ZhaoNMZ12.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
+@inproceedings{hwang99_fsmd,
+  author          = {Hwang, Enoch and Vahid, Frank and Hsu, Yu-Chin},
+  title           = {FSMD functional partitioning for low power},
+  booktitle       = {Proceedings of the conference on Design, automation and test in Europe},
+  year            = 1999,
+  pages           = {7--es},
+  doi = {10.1109/DATE.1999.761092}
+}
+
+@inproceedings{loow19_proof_trans_veril_devel_hol,
+	author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.},
+	title = {A Proof-producing Translator for Verilog Development in HOL},
+	tags = {hls, semantics},
+	booktitle = {Proceedings of the 7th International Workshop on Formal
+                  Methods in Software Engineering},
+	year = 2019,
+	pages = {99--108},
+	doi = {10.1109/FormaliSE.2019.00020},
+	url = {https://doi.org/10.1109/FormaliSE.2019.00020},
+	acmid = 3338828,
+	address = {Piscataway, NJ, USA},
+	location = {Montreal, Quebec, Canada},
+	numpages = 10,
+	publisher = {IEEE Press},
+	series = {FormaliSE '19}
+}
+
+@inproceedings{nikhil04_blues_system_veril,
+  author          = {R. {Nikhil}},
+  title           = {Bluespec System Verilog: efficient, correct RTL from high level specifications},
+  booktitle       = {Proceedings. Second ACM and IEEE International Conference on Formal Methods and
+                  Models for Co-Design, 2004. MEMOCODE '04.},
+  year            = 2004,
+  pages           = {69-70},
+  doi             = {10.1109/MEMCOD.2004.1459818},
+  url             = {https://doi.org/10.1109/MEMCOD.2004.1459818},
+}
+
+@inproceedings{schuiki20_llhd,
+  author          = {Schuiki, Fabian and Kurth, Andreas and Grosser, Tobias and Benini, Luca},
+  title           = {LLHD: A Multi-Level Intermediate Representation for Hardware Description
+                  Languages},
+  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
+                  and Implementation},
+  year            = 2020,
+  pages           = {258-271},
+  doi             = {10.1145/3385412.3386024},
+  url             = {https://doi.org/10.1145/3385412.3386024},
+  address         = {New York, NY, USA},
+  isbn            = 9781450376136,
+  location        = {London, UK},
+  numpages        = 14,
+  publisher       = {ACM},
+  series          = {PLDI 2020},
+}
+
+@InProceedings{zhu13_mechan_approac_linkin_operat_seman,
+  author          = "Zhu, Huibiao and Liu, Peng and He, Jifeng and Qin, Shengchao",
+  title           = "Mechanical Approach to Linking Operational Semantics and Algebraic Semantics
+                  for Verilog Using Maude",
+  booktitle       = "Unifying Theories of Programming",
+  year            = 2013,
+  pages           = "164--185",
+  address         = "Berlin, Heidelberg",
+  editor          = "Wolff, Burkhart and Gaudel, Marie-Claude and Feliachi, Abderrahmane",
+  isbn            = "978-3-642-35705-3",
+  publisher       = "Springer Berlin Heidelberg",
+}
+
+
+@inproceedings{poly_hls_zuo2013,
+  title={Improving polyhedral code generation for high-level synthesis},
+  author={Zuo, Wei and Li, Peng and Chen, Deming and Pouchet, Louis-No{\"e}l and Zhong, Shunan and Cong, Jason},
+  booktitle={2013 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ ISSS)},
+  pages={1--10},
+  year={2013},
+  organization={IEEE},
+  doi={https://doi.org/10.1109/CODES-ISSS.2013.6659002}
+}
+
+@INPROCEEDINGS{poly_hls_zhao2017,  author={Zhao, Jieru and Feng, Liang and Sinha, Sharad and Zhang, Wei and Liang, Yun and He, Bingsheng},  booktitle={2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},   title={COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},   year={2017},  volume={},  number={},  pages={430-437},  doi={10.1109/ICCAD.2017.8203809}}
+
+@inproceedings{poly_hls_pouchet2013polyhedral,
+  title={Polyhedral-based data reuse optimization for configurable computing},
+  author={Pouchet, Louis-Noel and Zhang, Peng and Sadayappan, Ponnuswamy and Cong, Jason},
+  booktitle={Proceedings of the ACM/SIGDA international symposium on Field programmable gate arrays},
+  pages={29--38},
+  year={2013},
+  doi={https://doi.org/10.1145/2435264.2435273}
+}
+
+@misc{quartus,
+  author          = {Intel},
+  title           = {{Intel® Quartus® Prime Software Suite}},
+  url             = {https://intel.ly/3fpUNhv},
+  urldate         = {2020-07-20},
+  year            = 2020,
+}
+
+@misc{xilinx_vivad_desig_suite,
+  author =       {Xilinx},
+  title =        {{Vivado Design Suite}},
+  url =          {https://bit.ly/2wZAmld},
+  urldate =      {2019-01-14},
+  year = 2019,
+}
+
+@inproceedings{chisel,
+  title={{Chisel: Constructing hardware in a Scala embedded language}},
+  author={Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avi{\v{z}}ienis, Rimas and Wawrzynek, John and Asanovi{\'c}, Krste},
+  booktitle={DAC Design Automation Conference 2012},
+  pages={1212--1221},
+  year={2012},
+  organization={IEEE},
+  doi={https://doi.org/10.1145/2228360.2228584},
+}
+
+@article{aubury1996handel,
+  title={Handel-C language reference guide},
+  author={Aubury, Matthew and Page, Ian and Randall, Geoff and Saul, Jonathan and Watts, Robin},
+  journal={Computing Laboratory. Oxford University, UK},
+  year={1996}
+}
+
+@inproceedings{clarke03_behav_c_veril,
+  author          = {E. {Clarke} and D. {Kroening} and K. {Yorav}},
+  title           = {Behavioral consistency of {C} and {Verilog} programs using bounded model checking},
+  booktitle       = {Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451)},
+  year            = 2003,
+  pages           = {368-371},
+  doi             = {10.1145/775832.775928},
+  url             = {https://doi.org/10.1145/775832.775928},
+}
+
+@article{besson18_compc,
+	doi = {10.1007/s10817-018-9496-y},
+	url = {https://doi.org/10.1007/s10817-018-9496-y},
+	year = {2018},
+	month = nov,
+	publisher = {Springer Science and Business Media {LLC}},
+	volume = {63},
+	number = {2},
+	pages = {369--392},
+	author = {Fr{\'{e}}d{\'{e}}ric Besson and Sandrine Blazy and Pierre Wilke},
+	title = {{CompCertS}: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics},
+	journal = {Journal of Automated Reasoning}
+}
+
+@article{sevcik13_compc,
+	author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+	title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
+	year = {2013},
+	issue_date = {June 2013},
+	publisher = {ACM},
+	address = {New York, NY, USA},
+	volume = {60},
+	number = {3},
+	issn = {0004-5411},
+	url = {https://doi.org/10.1145/2487241.2487248},
+	doi = {10.1145/2487241.2487248},
+	abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.},
+	journal = {J. ACM},
+	month = jun,
+	articleno = {22},
+	numpages = {50},
+	keywords = {semantics, Relaxed memory models, verified compilation}
+}
+
+@article{wang20_compc,
+	author = {Wang, Yuting and Xu, Xiangzhe and Wilke, Pierre and Shao, Zhong},
+	title = {CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files},
+	year = {2020},
+	issue_date = {November 2020},
+	publisher = {ACM},
+	address = {New York, NY, USA},
+	volume = {4},
+	number = {OOPSLA},
+	url = {https://doi.org/10.1145/3428265},
+	doi = {10.1145/3428265},
+	abstract = { We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files.  CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units.  We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files. },
+	journal = {Proc. ACM Program. Lang.},
+	month = nov,
+	articleno = {197},
+	numpages = {28},
+	keywords = {Generation of Object Files, Assembler Verification, Verified Separate Compilation}
+}
+
+@inproceedings{10.1145/3437992.3439916,
+author = {L\"{o}\"{o}w, Andreas},
+title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
+year = {2021},
+isbn = {9781450382991},
+publisher = {ACM},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/3437992.3439916},
+doi = {10.1145/3437992.3439916},
+abstract = {We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.},
+booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+pages = {46–60},
+numpages = {15},
+keywords = {hardware verification, hardware synthesis, compiler verification},
+location = {Virtual, Denmark},
+series = {CPP 2021}
+}
+
+@inproceedings{paulin89_sched_bindin_algor_high_level_synth,
+	author = {Paulin, P. G. and Knight, J. P.},
+	title = {Scheduling and Binding Algorithms for High-Level Synthesis},
+	booktitle = {Proceedings of the 26th ACM/IEEE Design Automation Conference},
+	year = 1989,
+	pages = {1-6},
+	doi = {10.1145/74382.74383},
+	url = {https://doi.org/10.1145/74382.74383},
+	address = {New York, NY, USA},
+	isbn = 0897913108,
+	location = {Las Vegas, Nevada, USA},
+	numpages = 6,
+	publisher = {ACM},
+	series = {DAC '89},
+}
+
+@inproceedings{venkataramani07_operat,
+	keywords = {operation chaining},
+	author = {Girish Venkataramani and Goldstein, Seth C.},
+	booktitle = {2007 IEEE/ACM International Conference on Computer-Aided Design},
+	title = {Operation chaining asynchronous pipelined circuits},
+	year = {2007},
+	volume = {},
+	number = {},
+	pages = {442-449},
+	doi = {10.1109/ICCAD.2007.4397305}
+}
+
+@inproceedings{noronha17_rapid_fpga,
+	keywords = {high-level synthesis, FPGA, inlining, compiler optimisation},
+	author = {D. H. {Noronha} and J. P. {Pinilla} and S. J. E. {Wilton}},
+	booktitle = {2017 International Conference on ReConFigurable Computing and FPGAs (ReConFig)},
+	title = {Rapid circuit-specific inlining tuning for FPGA high-level synthesis},
+	year = {2017},
+	volume = {},
+	number = {},
+	pages = {1-6},
+	doi = {10.1109/RECONFIG.2017.8279807}
+}
+
+@software{yann_herklotz_2021_5093839,
+  author       = {Yann Herklotz and
+                  James D. Pollard and
+                  Nadesh Ramanathan and
+                  John Wickerson},
+  title        = {ymherklotz/vericert: Vericert v1.2.1},
+  month        = jul,
+  year         = 2021,
+  publisher    = {Zenodo},
+  version      = {v1.2.1},
+  doi          = {10.5281/zenodo.5093839},
+  url          = {https://doi.org/10.5281/zenodo.5093839}
+}
+
+@INPROCEEDINGS{herklotz21_empir_study_reliab_high_level_synth_tools,
+	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},
+	volume = {},
+	number = {},
+	pages = {219-223},
+	doi = {10.1109/FCCM51124.2021.00034}
+}