Update on Overleaf.

1 files changed, 28 insertions, 9 deletions

diff --git a/introduction.tex b/introduction.tex
index a5421e4..7abed31 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -6,15 +6,6 @@
 
 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.
 
-\NR{
-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 compiles high-level languages like C/C++ to HDL. 
-HLS compilation is generally realised by leveraging existing software compiler frameworks like LLVM, introducing the possibility of bugs during the translation from C to Verilog.  
-Hence, the premise of this work is: Can we trust these compilers to translate high-level languages like C/C++ to HDL correctly? 
-}
-
 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
@@ -54,6 +45,34 @@ To mitigate the problems about the unreliability of synthesis tool, it is often
 
 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 usual starting point for most HLS tool development is to leverage an existing software compiler framework like LLVM. 
+Re-using software concepts, optimisation and codebases make HLS compiliation as susceptible to bugs as any software compilers for the same reasons. 
+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? 
+
+\subsection{Evidence of unreliability and previous works}
+
+\subsection{Our approach}
+
+% }
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"