diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 14 |
1 files changed, 13 insertions, 1 deletions
@@ -153,7 +153,7 @@ %% Note: \begin{abstract}...\end{abstract} environment must come %% before \maketitle command \begin{abstract} - We propose a formally verified HLS flow based on CompCert~\cite{leroy09_formal_verif_realis_compil}, by adding a Verilog backend which is a language used to describe hardware. + High-level synthesis (HLS) is the process of converting an algorithmic description, often written in C, to specialised hardware with the same behaviour, expressed in a hardware description language. HLS is becoming increasingly popular, as it allows for faster prototyping as well as simpler behavioural verification, as all the software tools can be used. The HLS process has to be trusted though to be sure that . C constructs are also often not supported in various combinations, which make existing tools quite brittle. Our work focuses on formally verifying the high-level synthesis process from C to Verilog by proving that the behaviour remains the same according to the C and Verilog semantics. \end{abstract} @@ -193,6 +193,14 @@ \section{Introduction} +\section{Background} + +\subsection{Verilog} + +\subsection{CompCert / Coq / Proof by simulation} + +\subsection{HLS} + \section{Verilog Semantics} Definition of state. @@ -262,6 +270,10 @@ based on what they evaluate to. For case I think that would end up being a three \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})} \end{equation} +\section{Proof} + +\section{Conclusion} + %% Acknowledgments \begin{acks} %% acks environment is optional %% contents suppressed with 'anonymous' |