Add first paragraph

1 files changed, 7 insertions, 2 deletions

diff --git a/main.tex b/main.tex
index 4e2dfb9..bd15da2 100644
--- a/main.tex
+++ b/main.tex
@@ -190,9 +190,12 @@
 %% environment and commands, and keywords command.
 \maketitle
 
-
 \section{Introduction}
 
+The current approach to writing energy-efficient and high-throughput applications is to use custom hardware which has been specialised for that application, instead of relying on and optimising for a CPU.\@  This comes at the cost of having to design the customised hardware, which, if using hardware description languages such as Verilog can be tedious and quite error prone.  Especially with the size 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 can be quite inefficient.  Furthermore, the algorithms that are being accelerated in hardware often already have a software implemention, meaning they have to be reimplemented efficiently in a hardware description language which can be time consuming.
+
+
+
 \section{Background}
 
 \subsection{Verilog}
@@ -277,11 +280,13 @@ based on what they evaluate to. For case I think that would end up being a three
 
 \begin{equation}
   \label{eq:9}
-  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
+  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
 \end{equation}
 
 \section{Proof}
 
+\section{Coq mechanisation}
+
 \section{Conclusion}
 
 %% Acknowledgments