Add modifications to Verilog syntax adn implement more notes

1 files changed, 7 insertions, 9 deletions

diff --git a/introduction.tex b/introduction.tex
index cbf4780..1476d33 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -2,20 +2,18 @@
 
 %% Motivation for why HLS might be needed
 
-The current approach to writing energy-efficient and high-throughput applications is to use application-specific hardware, instead of relying on a general purpose \JW{general-purpose} CPU.\@  However, custom hardware designs come at the cost of having to design and produce it \JW{them?}, which can be a tedious and error-prone process using hardware description languages (HDL) such as Verilog.  Especially with the size of hardware designs grow \JW{growing} over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of hardware description languages \JW{HDLs} can be quite inefficient.  Furthermore, the algorithms that are being accelerated in hardware often already have a software implementation, meaning they have to be reimplemented efficiently in a hardware description language which can be time consuming \JW{time-consuming}.
+The 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.  Especially with the size of hardware designs growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of HDLs can be quite inefficient.  Furthermore, the algorithms that are being accelerated in hardware often already have a software implementation, meaning they have to be reimplemented efficiently in a hardware description language which can be time-consuming.
 
 %% Definition and benefits of HLS
-One possible solution to \JW{the} tedious design process of custom hardware is to use high-level synthesis (HLS), which is the process of generating custom hardware, represented in a hardware description language \JW{HDL}, based on a behavioural description, often \JW{in} a subset of C.  This elevates the level of abstraction, because the description of the algorithm in C is inherently untimed, meaning actions don't have to be scheduled into clock cycles.  The higher level of abstraction makes it easier to reason about the algorithms and therefore also makes them easier to maintain.  This already reduces the time taken to design the hardware, especially if a software description of the algorithm already exists, because it won't \JW{doesn't} have to be designed again at a lower level and directly in hardware.  However, another benefit of using HLS to design the hardware, \JW{no comma here} is that functional verification of the design is much simpler and more efficient than if it was \JW{were} done at the HDL stage, as the whole software ecosystem can be used to do that.  Instead of having to run simulations of the hardware, the C code can just be compiled and executed natively, as the hardware design after HLS should have the same behaviour.
-\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.}
+One possible solution to the tedious design process of custom hardware is to use high-level synthesis (HLS), which is the process of generating custom hardware, represented in a HDL, based on a behavioural description, often in a subset of C.  This elevates the level of abstraction, because the description of the algorithm in C is inherently untimed, meaning actions don't have to be scheduled into clock cycles.  The higher level of abstraction makes it easier to reason about the algorithms and therefore also makes them easier to maintain.  This already reduces the time taken to design the hardware, especially if a software description of the algorithm already exists, because it doesn't have to be designed again at a lower level and directly in hardware.  However, another benefit of using HLS to design the hardware is that functional verification of the design is much simpler and more efficient than if it were done at the HDL stage, as the whole software ecosystem can be used to do that.  Instead of having to run simulations of the hardware, the C code can just be compiled and executed natively, as the hardware design after HLS should have the same behaviour.  Moreover, the abstraction that HLS provides helps to improve the productivity of hardware designers, as well as reduces the barrier of entry to hardware design for software programmers.  For hardware designers, checking that the created hardware does indeed behave properly may reduce productivity, whereas for software programmers it may be unfeasible to properly test the hardware as they are unaware of the standard tools used.  Both these audiences therefore stand to benefit from the guarantees provided by verified C-to-Verilog generation.
+% \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
 
-However, the fact that the behaviour is preserved after HLS cannot be guaranteed most existing tools,\YH{Mentor's catapult C can in some cases} meaning behavioural simulation of the hardware design still has to be performed. HLS tools are also known to be quite unreliable, for example, Intel's (formerly Altera's) OpenCL SDK compiler contained too many bugs to even be considered for random testing, as more than 25\% of the testcases failed~\cite{lidbury15_many_core_compil_fuzzin}. In addition to that, designers often feel like HLS tools are quite unreliable and fragile with respect to which language features that are supported.\YH{Need citation}
-\JW{Here's some text that could be helpful in this paragraph... However, 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 so many of their test inputs. 
-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}}.}
+However, the fact that the behaviour is preserved after HLS cannot be guaranteed most existing tools,\YH{Mentor's catapult C can in some cases} meaning behavioural simulation of the hardware design still has to be performed. HLS tools are also known to be quite unreliable, for example, Intel's (formerly Altera's) OpenCL SDK compiler contained too many bugs to even be considered for random testing, as more than 25\% of the test cases failed~\cite{lidbury15_many_core_compil_fuzzin}. In addition to that, designers often feel like HLS tools are quite unreliable and fragile with respect to which language features that are supported.  However, 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 so many of their test inputs.  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}}.  As HLS tools are extremely complex and can therefore incorrectly change the behaviour of the design, it is not possible to guarantee that all the properties of the code that were proven in software will also hold for the generated hardware.
+
 % JW: Another candidate, probably less interesting:
 % https://bit.ly/intel-hls-memory-bug
-As HLS tools are extremely complex and can therefore incorrectly change the behaviour of the design, it is not possible to guarantee that all the properties of the code that were proven in software will also hold for the generated hardware.
 
 %% 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.}
@@ -28,7 +26,7 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b
 
 %% Contributions of paper
 
-In this paper we describe a fully verified high-level synthesis \JW{HLS} tool called CoqUp, which adds a Verilog backend to CompCert 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:
+In this paper we describe a fully verified high-level synthesis \JW{HLS} tool called CoqUp, which adds a Verilog back end to CompCert 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 First mechanised and formally verified HLS flow from C to Verilog.
@@ -45,7 +43,7 @@ CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherkl
 \NR{Other comments:}
 \NR{Is both the translator and verifier written in Coq?}\YH{Currently there is no verifier, the algorithms themselves are proven directly in Coq.}
 %%\NR{A tool-flow diagram here will be useful. I thought you had one previously?}
-\NR{Do you think we have a very simple example of a program where wrong Verilog is generated in VHLS or LegUp, but not in CoqUp?}\YH{The legup example actually with the shift might be a good one.}
+\NR{Do you think we have a very simple example of a program where wrong Verilog is generated in VHLS or LegUp, but not in CoqUp?}\YH{The LegUp example actually with the shift might be a good one.}
 
 %%% Local Variables:
 %%% mode: latex