\startcomponent introduction

\chapter{Introduction}

\startthesis
An optimising high-level synthesis tool can be proven correct using an interactive theorem prover
while also remaining practical.
\stopthesis

\noindent 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{\goto{bit.ly/vivado-hls-pipeline-bug}[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{\goto{bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivado-hls-pointer-bug)]}
Meanwhile, \cite{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test
Altera's (now Intel's) OpenCL compiler since it \quotation{either crashed or emitted an internal
  compiler error} on so many of their test inputs.  More recently,
\cite{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[alternative=authoryear,right={, 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[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.

\stopcomponent