\section{Related Work}

\begin{figure}
  \centering
  \begin{tikzpicture}[xscale=1.7]
    \def\opacity{0.2}
    \definecolor{colorusabletool}{HTML}{1b9e77}
    \definecolor{colorhighlevel}{HTML}{d95f02}
    \definecolor{colorproof}{HTML}{7570b3}
    \definecolor{colormechanised}{HTML}{e7298a}

    \tikzset{myellipse/.style={draw=none, fill opacity=0.2}}
    \tikzset{myoutline/.style={draw=white, thick}}

    \draw[myellipse, fill=colorusabletool] (-1.1,1.6) ellipse (3.1 and 2.3);
    \draw[myellipse, fill=colorhighlevel] (1.1,1.8) ellipse (2.9 and 2.1);
    \draw[myellipse, fill=colorproof] (0,0.3) ellipse (3.7 and 1.9);
    \draw[myellipse, fill=colormechanised] (0,0) ellipse (3 and 1.0);

    \draw[myoutline] (-1.1,1.6) ellipse (3.1 and 2.3);
    \draw[myoutline] (1.1,1.8) ellipse (2.9 and 2.1);
    \draw[myoutline] (0,0.3) ellipse (3.7 and 1.9);
    \draw[myoutline] (0,0) ellipse (3 and 1.0);

    \node[align=center] at (0,2.8) {Standard HLS tools \\ \footnotesize\cite{canis11_legup,intel20_sdk_openc_applic} \\ \footnotesize\cite{nigam20_predic_accel_desig_time_sensit_affin_types,xilinx20_vivad_high_synth}};
    \node[align=center] at (0.15,1.5) {Translation validation approaches \\ \footnotesize\cite{mentor20_catap_high_level_synth,kundu08_valid_high_level_synth,clarke03_behav_c_veril}};
    \node at (0,0.5) {\bf \vericert{}};
    \node[align=left] at (-1.8,0.0) {\footnotesize K\^oika \cite{bourgeat20_essen_blues}};
    \node[align=left] at (-1.8,0.32) { \footnotesize\citet{10.1145/3437992.3439916}};

    \node at (2.2,0.2) {\footnotesize\citet{ellis08}};
    \node at (-1.3,-0.32) { {\footnotesize\citet{perna12_mechan_wire_wise_verif_handel_c_synth}}};
    \node at (0,-1.3) {\footnotesize BEDROC \cite{chapman92_verif_bedroc}};

    \node[align=left] at (-2.9,-1.7) {\color{colorproof}Correctness \\ \color{colorproof}proof};
    \draw[myoutline] (1.2,-0.9) to (2.6,-1.7);
    \node[align=right] at (2.6,-1.7) {\color{colormechanised}Mechanised \\ \color{colormechanised}correctness proof};
    \node at (-2.8,4.1) {\color{colorusabletool}\strut Usable tool};
    \node at (2.1,4.1) {\color{colorhighlevel}\strut High-level software input};
  \end{tikzpicture}
  \Description{A Venn diagram containing the related works.}
  \caption{Summary of related work}\label{fig:related_euler}
\end{figure}

A summary of the related works can be found in Fig.~\ref{fig:related_euler}, which is represented as an Euler diagram.  The categories chosen for the Euler diagram are: whether the tool is usable, whether it takes a high-level software language as input, whether it has a correctness proof, and finally whether that proof is mechanised.  The goal of \vericert{} is to cover all of these categories.

Most practical HLS tools~\citep{canis11_legup,xilinx20_vivad_high_synth,intel20_sdk_openc_applic,nigam20_predic_accel_desig_time_sensit_affin_types} fit into the category of usable tools that take high-level inputs.  On the other end of the spectrum, there are tools such as BEDROC~\citep{chapman92_verif_bedroc} for which there is no practical tool, and even though it is described as high-level synthesis, it more closely resembles today's logic synthesis tools.

Ongoing work in translation validation~\citep{pnueli98_trans} seeks to prove equivalence between the hardware generated by an HLS tool and the original behavioural description in C.  An example of a tool that implements this is Mentor's Catapult~\citep{mentor20_catap_high_level_synth}, which tries to match the states in the hardware description to states in the original C code after an unverified translation.  Using translation validation is quite effective for verifying complex optimisations such as scheduling~\citep{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\citep{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}, but the validation has to be run every time the HLS is performed.  In addition to that, the proofs are often not mechanised or directly related to the actual implementation, meaning the verifying algorithm might be wrong and hence could give false positives or false negatives.

Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translator from a core fragment of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, so is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a proof-producing translator from HOL4 code describing state transitions into Verilog to design a verified processor, which is described further by \citet{loow19_verif_compil_verif_proces}. \citet{10.1145/3437992.3439916} has also worked on formally verifying a logic synthesis tool that can transform hardware descriptions into low-level netlists.  This synthesis back end can seamlessly integrate with the proof-producing HOL4 to Verilog translator as it is based on the same Verilog semantics, and therefore creates verified translation from HOL4 circuit descriptions to synthesised Verilog netlists.
Perna et al. designed a formally verified translator from a deep embedding of Handel-C~\citep{aubury1996handel} into a deep embedding of a circuit~\cite{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth}.
Finally, \citet{ellis08} used Isabelle to implement and reason about intermediate languages for software/hardware compilation, where parts could be implemented in hardware and the correctness could still be shown.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End: