Add modifications

1 files changed, 27 insertions, 34 deletions

diff --git a/hls.tex b/hls.tex
index 734463c..b73b686 100644
--- a/hls.tex
+++ b/hls.tex
@@ -7,19 +7,18 @@
 
 \chapter{High-Level Synthesis}
 
-{\bf 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.
+\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
@@ -34,12 +33,10 @@ using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting t
 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.
 
-{\bf 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.
+\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
@@ -57,20 +54,17 @@ to date.
 Our position is that none of the above workarounds are necessary if the HLS tool can simply be
 trusted to work correctly.
 
-{\bf 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{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.
 
-{\bf Contributions and Outline}
-The contributions of this paper are as follows:
+\paragraph{Contributions and Outline.} The contributions of this paper are as follows:
 
 \startitemize[]
   \item We present Vericert, the first mechanically verified HLS tool that compiles C to Verilog. In
@@ -105,8 +99,7 @@ The contributions of this paper are as follows:
         correctness theorem is watertight.
 \stopitemize
 
-{\bf Companion material}
-Vericert is fully open source and available on GitHub at
+\paragraph{Companion material.} Vericert is fully open source and available on GitHub at
 
 \startalignment[center]
 \goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)].