diff options
Diffstat (limited to 'verilog.tex')
| -rw-r--r-- | verilog.tex | 16 |
1 files changed, 7 insertions, 9 deletions
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 |