\section{Introduction}

%% Motivation for why HLS might be needed

%\JW{A few high-level comments: \begin{enumerate} \item Create more tension from the start by making the reader doubt whether existing HLS tools are trustworthy. \item The intro currently draws quite a bit of motivation from Lidbury et al. 2015, but we should also now lean on our FPGA submission too. \item I wonder whether the paragraph `To mitigate the problems...' should be demoted to a `related work' discussion (perhaps as a subsection towards the end of the introduction). It outlines (and nicely dismisses) some existing attempts to tackle the problem, which is certainly useful motivation for your work, especially for readers already familiar with HLS, but I feel that it's not really on the critical path for understanding the paper.\end{enumerate}}

One current approach to writing energy-efficient and high-throughput applications is to use application-specific hardware, instead of relying on a general-purpose CPU.\@  However, custom hardware designs come at the cost of having to design and produce them, which can be a tedious and error-prone process using hardware description languages (HDL) such as Verilog.  High-level synthesis (HLS) is becoming a viable alternative, allowing designers to describe the hardware in a software programming language such as C, and inferring the hardware design from it.  Can we really trust that the generated hardware functions correctly?  It is often assumed that compilers do not change the behaviour of the original program through it's various transformations, however, as HLS tools perform complex transformations, this might not always be the case.

High-level synthesis is becoming increasingly important in the hardware design process.  HLS elevates the level of abstraction, allowing designers to describe behaviour using an untimed representation, which reduces the amount of bugs that could be introduced into the design.  The higher level of abstraction makes it easier to reason about the algorithms and therefore also facilitates maintaining them.  In addition to reducing the time it takes hardware designers to produce hardware, it also reduces the barrier of entry to hardware design for software programmers.  In both cases, correctness of the HLS tool is important, as it hinders the productivity of hardware designers by needing them to check the function correctness of the hardware, whereas software programmers may be unable to properly test the  hardware as they may be unaware of the proper tools.  In addition to that, functional verification of the design becomes much more efficient than at the HDL stage, since the entire software ecosystem can be mobilised for this task.  However, any properties that were proven about the functionality of the design may not hold for the hardware design, which may require separate checks.

%% Definition and benefits of HLS
% \NR{The abstraction of HLS helps in two ways: improving productivity of hardware designers and reducing the entry barrier of hardware design for software programmers. Both these audiences stand to benefit from the guarantees provided by verified C-to-Verilog generation.} \JW{Yes, Nadesh makes a good point here. Worth incorporating.}\YH{Added.}

%% Unreliability of HLS

Bugs in HLS tools when designing hardware are detrimental, as it may not be possible to change the hardware once it is produced.  It is therefore necessary to not only check the software version of the design correct, but also ensure that the generated hardware design works correctly, because the HLS tool can not be trusted, leading to duplicate testing and verifying of the resulting hardware design.  However, with the growing size of hardware designs, it may not be feasible to check that the hardware is correct for all possible inputs.  In addition to that, this duplicate checking discourages the use of HLS in safety-critical environments, where correctness is key.  It is therefore considered safer to manually write and verify all the hardware designs, hindering the use of higher-level constructs, faster iteration on the designs and more maintainable designs as could be achieved using HLS.\@

This is further motivated by the fact that HLS tools are often considered to be quite unreliable and fragile with respect to which language features that are supported.  Most HLS tools cannot guarantee that compilation is behaviour-preserving.  In fact, on the contrary, there is some evidence that current HLS tools are actually quite \emph{unreliable} in this regard.  For instance, an attempt by \citet{lidbury15_many_core_compil_fuzzin} to fuzz Altera's (now Intel's) OpenCL compiler had to be abandoned because the compiler ``either crashed or emitted an internal compiler error'' on a large number of their test inputs.  In addition to that, work by Du \emph{et al.}~\cite{?} fuzz tested three major commercial HLS using Csmith~\cite{yang11_findin_under_bugs_c_compil}, while restricting the C programs to the constructs explicitly supported by the synthesis tools and found that on average 2.5\% of test cases generated a design that did not match the behaviour of the input.  Meanwhile, Xilinx's 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}}.

% JW: Another candidate, probably less interesting:
% https://bit.ly/intel-hls-memory-bug

A radical solution is to write an HLS tool in a theorem prover such as Coq~\cite{bertot04_inter_theor_provin_progr_devel}, so that the translation algorithm can be proven correct in the theorem prover itself.  The algorithm can then be extracted to executable code, which exhibits the same properties as the Coq code that was proven correct in the theorem prover.  In this paper we describe a fully verified HLS tool called \vericert{}, which adds a Verilog back end to \compcert{}, an existing C compiler that has been written and formally verified in the Coq theorem prover, and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics.  The main contributions of the paper are the following:

\begin{itemize}
  \item We provide the first mechanised and formally verified HLS tool going from C to Verilog.
  \item Description of how the Verilog semantics integrate into \compcert{} and how it interacts with \compcert{}'s intermediate language.
  \item Benchmark comparisons between \vericert{} and LegUp~\cite{canis11_legup}, a well-known open source, unverified HLS tool on Polybench, a large C benchmark, and including some specific test cases from CHstone.
\end{itemize}

The first section will describe the Verilog semantics that were used and extended to fit into \compcert{}'s model.  The second section will then describe the HLS algorithm, together with its proof.

\vericert{} is open source and is hosted on GitHub\footnote{\url{https://github.com/ymherklotz/vericert}}.

% Maybe include example of C program that goes wrong.

\subsection{Background}

%% Current work in formal verification of HLS
%%\NR{This is a good paragraph, but we need to relate it more to this work and why this work is different.}
%%\NR{Focus on more high-level of "why this work is interesting"? Two key points we want to get across to the reader is that in existing works: validation is neccessary every time a new program is compiled and the verifying algorithm is not verified.}
%%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation)}
%%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.}
To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, there is a risk that bugs remain in the untested code.  To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent.  Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many 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}.  However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof.  In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially.  One example is Catapult C~\cite{mentor20_catap_high_level_synth}, which allows the use of translation validation between the C and RTL code, however, as they mention themselves~\cite{whitepaper}, this process might require quite a bit of iteration on the C code so that the equivalence checker can prove this correctly.  This can be a tedious process, as one cannot be sure about what sections in the C need to change to help the equivalence checker prove the equality.  In addition to that, the larger the design, the more infeasible using an equivalence checking tool like this would be.

A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code.  In addition to that, it would allow for the implementation of optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes.

% \NR{

\NR{I couldn't have subsections in comments so I have appended my writing to the bottom of this file.}\\ 

As latency, throughput and energy efficiency become increasingly important, custom hardware accelerators are being designed for numerous applications~\cite{??}. 
Alas, designing these accelerators come at a cost of additional engineering effort and risk, since it typically involves designing in hardware description languages (HDL), such as Verilog.
Designing at HDL level is not only arduous and time-consuming but also it limits the expressiveness and abstraction of computation. 
As such, high-level synthesis (HLS) is becoming an attractive alternative, since it offers abstraction by compiling high-level languages like C/C++ to HDL, whilst achieving comparable quality of results relative HDL designs~\cite{bdti,autoesl}.
Modern HLS tools such as LegUp~\cite{}, Vivado HLS~\cite{}, and Intel i++~\cite{} can produce designs with comparable performance and energy-efficiency to those manually coded in HDL [citation needed], while offering the convenient abstractions and rich ecosystem of software development.

\subsection{Can we trust our high-level synthesis tools?}
The common starting point for most HLS tool development is to leverage an existing software compiler framework like LLVM, such as LegUp HLS, Vivado HLS and Bambu HLS~\cite{}.
Re-using software concepts, optimisation and codebases make HLS compiliation as susceptible to bugs as any software compilers. 
These native codebases are large and they perform complex and non-trivial analyses and transformations to translate software into efficient assembly or HDL, in the case of HLS. 
Consequently, HLS tools cannot always guarantee that the generated hardware is equivalent to the input program, undermining any reasoning conducted at the software level. 
Furthermore, HDL design in itself is complex, error-prone and requires careful reasoning and formal verification to ensure behaviour, data-flow and structural correctness~\cite{}.
The added complexity of HDL design thus increases the likelihood of HLS compilation mismatches. 
% between the software program and the generated hardware. 
% There are valid reasons to doubt that HLS tools actually \emph{do} preserve equivalence, not least because they are large pieces of software that perform complex transformations.

Hence, the premise of this work is: Can we trust these compilers to translate high-level languages like C/C++ to HDL correctly? 
For instance, \citet{lidbury15_many_core_compil_fuzzin} abandoned fuzzing Altera's (now Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on a large number of their test inputs.  
Also, Du \emph{et al.}~\cite{?} fuzz tested three commercial HLS tools using Csmith~\cite{yang11_findin_under_bugs_c_compil}, while restricting the C programs to the constructs explicitly supported by the synthesis tools. 
They found that on average 2.5\% of test cases generated a design that did not match the behaviour of the input.  
Meanwhile, Xilinx's 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}}.

\subsection{Existing approach: HLS-generated hardware verification}

It is rather difficult to exhaustively test to prove the absence of bugs on these large HLS codebases, which include custom compiler directives.
Hence, most existing work on verifying HLS tools proving that the translation of a program instance to hardware is equaivalent, as known as translation valida  

To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, there is a risk that bugs remain in the untested code.  To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent.  Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many 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}.  However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof.  In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially.  One example is Catapult C~\cite{mentor20_catap_high_level_synth}, which allows the use of translation validation between the C and RTL code, however, as they mention themselves~\cite{whitepaper}, this process might require quite a bit of iteration on the C code so that the equivalence checker can prove this correctly.  This can be a tedious process, as one cannot be sure about what sections in the C need to change to help the equivalence checker prove the equality.  In addition to that, the larger the design, the more infeasible using an equivalence checking tool like this would be.

A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code.  In addition to that, it would allow for the implementation of optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes.

\subsection{Our approach}

% }


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
