diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | verilog.tex | 16 |
2 files changed, 8 insertions, 10 deletions
diff --git a/algorithm.tex b/algorithm.tex index 332ca92..2c4f577 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -10,7 +10,7 @@ This section covers the main architecture of the HLS tool, and the way in which First of all, the choice of C for the input language of \vericert{} is because it is the most widely supported language for HLS, and most major HLS tools also use it as an input. As a lot of existing code is also written in C for HLS, supporting C as an input language compared to a custom domain-specific language means that \vericert{} is more practical. \JW{Can we mention one or two alternatives that we considered?} \paragraph{Choice of target language} -Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. \JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?} +Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language, which can be synthesised into logic gates which can be placed onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC). Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. \JW{Can we mention one or two alternatives that we considered? Bluespec or Chisel or one of Adam Chlipala's languages, perhaps?} \paragraph{Choice of implementation language} The framework that was chosen for the frontend was \compcert{}, as it is a mature framework for simulation proofs about intermediate languages, in addition to already providing a validated parser~\cite{jourdan12_valid_lr_parser} from C into the internal representation of Clight. Other frameworks were also considered, such as Vellvm~\cite{zhao12_formal_llvm_inter_repres_verif_progr_trans}, as LLVM IR in particular is often used by HLS tools anyways, however, these would require more work to support a higher level language such as C as input, or even providing a parser for LLVM IR.\@ diff --git a/verilog.tex b/verilog.tex index 9b67118..3380209 100644 --- a/verilog.tex +++ b/verilog.tex @@ -1,7 +1,5 @@ \section{Verilog}\label{sec:verilog} -%\JW{I'm not sure the Verilog syntax figure adds enough value to be worthy of inclusion in the body -- perhaps it could be demoted to an appendix. Instead, I think it would be interesting to see a bit more about how the semantics works. Not the whole gamut of inference rules or anything, but a little bit about how the rules work and what the appropriate notion of state is.} - This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target. The Verilog standard is quite large, and not all Verilog features are needed to be able to describe hardware. Many Features are only useful for simulation and do not affect the hardware itself. We can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard. @@ -57,11 +55,11 @@ In addition to adding support for two-dimensional arrays, support for receiving \centering \begin{minipage}{1.0\linewidth} \begin{gather*} - \inferrule[Module]{\Gamma_{r} ! s_{t} = \yhconstant{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1}) ! s_{t} = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1})\ (\Gamma_{a}^{1}\ //\ \Delta_{a}^{1})}\\ + \inferrule[Module]{\Gamma_{r} ! s_{t} = \yhconstant{Some } v \\ (m, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{m} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1}) ! s_{t} = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1}\ //\ \Delta_{r}^{1})\ (\Gamma_{a}^{1}\ //\ \Delta_{a}^{1})}\\ % \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \yhconstant{Some } 1 \\ \Gamma_{r}!\textit{ret} = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\ % - \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf}\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf}\ m\ n\ (\yhfunction{init\_params}\ \vec{r}\ a\ //\ \{s_{t} \rightarrow n\})}\\ + \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf }\ m\ n\ (\yhfunction{init\_params}\ \vec{r}\ a\ //\ \{s_{t} \rightarrow n\})}\\ % \inferrule[Return]{ }{\yhconstant{Returnstate } (\yhconstant{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \yhconstant{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r}\ //\ \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon} \end{gather*} @@ -73,9 +71,9 @@ In addition to adding support for two-dimensional arrays, support for receiving \compcert{} defines a specific model of computation which all semantics have to follow in order to prove properties about them. \compcert{} has three main states that need to be defined: \begin{description} - \item[\texttt{State}] The main state when executing a function. - \item[\texttt{Callstate}] The state that is reached when a function is called. - \item[\texttt{Returnstate}] The state that is reached when a function returns back to the caller. + \item[\texttt{State} \textit{sf} $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame \textit{sf}, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$. + \item[\texttt{Callstate} \textit{sf} $m$ $\vec{r}$] The state that is reached when a function is called, with the current stack frame \textit{sf}, current module $m$ and arguments $\vec{r}$. + \item[\texttt{Returnstate} \textit{sf} $r$] The state that is reached when a function returns back to the caller, with stack frame \textit{sf} and return value $r$. \end{description} However, as Verilog behaves quite differently to software programming languages, this model does not match the Verilog semantics. Instead, the module definition in Verilog needs to be enriched to support this model of computation, by adding required signals to the inputs and outputs of modules. @@ -87,9 +85,9 @@ However, as Verilog behaves quite differently to software programming languages, \item[stack] The function stack can be modelled as a RAM using a two-dimensional array in the module, denoted as \textit{stk}. \end{description} -Figure~\ref{fig:inferrence_module} shows the inferrence rules that convert from one state to another. The first thing to note is that there is no step from \texttt{State} +Figure~\ref{fig:inferrence_module} shows the inferrence rules that convert from one state to another. The first rule is the normal rule of execution -%~\NR{Isn't the 'main' addition that the PL community may not have seen the always blocks? It can be counter-intuitive to them. Also have you intentionally avoided assign statements? Finally, what is $\epsilon$ in the syntax?}\YH{Yes, I will probably have to explain always blocks some more, I'll try and add a paragraph about them. Yes, assign statements are quite complex to model and many semantics do not model them. They are also not needed for translation. The $\epsilon$ is an empty skip statement, which is just a semicolon.} +The first thing to note is that there is no step from \texttt{State} to \texttt{Callstate}, as function calls are not supported, and it is therefore impossible in our semantics to ever reach a \texttt{Callstate} except for the initial call to main. %%% Local Variables: %%% mode: latex |