diff options
| -rw-r--r-- | algorithm.tex | 5 | ||||
| -rw-r--r-- | archive/algorithm.tex | 5 | ||||
| -rw-r--r-- | verilog.tex | 19 |
3 files changed, 13 insertions, 16 deletions
diff --git a/algorithm.tex b/algorithm.tex index 3a27591..4a31df0 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -220,11 +220,6 @@ An HTL program thus consists of two maps: a control map that describes how to ca \caption{The FSMD for the example shown in Figure~\ref{fig:accumulator_c_rtl}, split into a data path and control logic for the next state calculation. The Update block takes the current state, current values of all registers and at most one value stored in the array, and calculates a new value that can either be stored back in the array or in a register.}\label{fig:accumulator_diagram} \end{figure*} -The translation from 3AC to HTL is straightforward, as each 3AC instruction either matches up quite well to a hardware construct, or does not have to be handled by the translation, such as function calls. -%At each instruction, the control flow is separated from the data computation and is then added to the control logic and data-flow map respectively. -%\JW{I suspect that you could safely chop that sentence.} -For example, in state 15 in figure~\ref{fig:accumulator_rtl}, the register \texttt{x8} is initialised to 1, after which the control flow moves to state 14. This is encoded in HTL by initialising a 32-bit register \texttt{reg\_8} to 1 in the data-flow section, and also adding a transition to the state 15 in the control logic section. Simple operator instructions are translated in a similar way. For example, in state 5, the value in the array is added to the current value of the accumulated sum, which is simply translated to an addition of the equivalent registers in the HTL code. - \paragraph{Translating memory} Hardware does not have the same memory model as C, so the memory model needs to be translated, as follows. Global variables are not translated in \vericert{} at the moment. The stack of the main function becomes a block of RAM, \JW{check this -- maybe change to 2D array of registers?} as seen in Figure~\ref{fig:accumulator_diagram}. Program variables that have their address taken are stored in this RAM, as are any arrays or structs defined in the function. Variables that do not have their address taken are kept in registers. diff --git a/archive/algorithm.tex b/archive/algorithm.tex index bd85e4b..d04b5e0 100644 --- a/archive/algorithm.tex +++ b/archive/algorithm.tex @@ -1,3 +1,8 @@ +The translation from 3AC to HTL is straightforward, as each 3AC instruction either matches up quite well to a hardware construct, or does not have to be handled by the translation, such as function calls. +%At each instruction, the control flow is separated from the data computation and is then added to the control logic and data-flow map respectively. +%\JW{I suspect that you could safely chop that sentence.} +For example, in state 15 in figure~\ref{fig:accumulator_rtl}, the register \texttt{x8} is initialised to 1, after which the control flow moves to state 14. This is encoded in HTL by initialising a 32-bit register \texttt{reg\_8} to 1 in the data-flow section, and also adding a transition to the state 15 in the control logic section. Simple operator instructions are translated in a similar way. For example, in state 5, the value in the array is added to the current value of the accumulated sum, which is simply translated to an addition of the equivalent registers in the HTL code. + \subsection{Translating HTL to Verilog} Finally, we have to translate the HTL code into proper Verilog and prove that it behaves the same as the 3AC according to the Verilog semantics. Whereas HTL is a language that is specifically designed to represent the FSMDs we are interested in, Verilog is a general-purpose HDL.\@ So the challenge here is to translate our FSMD representation into a Verilog AST. However, as all the instructions are already expressed in Verilog, only the maps need to be translated to valid Verilog, and correct declarations for all the variables in the program need to be added as well. diff --git a/verilog.tex b/verilog.tex index e6a9a2d..690f7e5 100644 --- a/verilog.tex +++ b/verilog.tex @@ -78,28 +78,25 @@ which modifies one array element using blocking assignment and then a second usi \label{fig:inferrence_module} \end{figure*} -The \compcert{} model defines a set of computational states. -The \compcert{} computation model requires our Verilog semantics to be enriched. In order to support the three CompCert states, our module definitions require five additional Verilog registers. - -\compcert{} defines a specific model of computation that all semantics have to follow in order to prove properties about them. In this section, we first describe three of \compcert{}'s original computational states. Then, we describe the five registers and semantic rules we add to Verilog semantics to integrate it to the \compcert{} model. \compcert{} has three main states that need to be defined: +The \compcert{} computation model defines a set of states through which execution passes. In this subsection, we explain how we extend our Verilog semantics with five special-purpose registers in order to integrate it into \compcert{}. +\compcert{} executions pass through three main states: \begin{description} \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} $v$] The state that is reached when a function returns back to the caller, with stack frame \textit{sf} and return value $v$. \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. -\NR{I understand this better. Maybe a concise way of saying this is: "The CompCert computation model require our Verilog semantics to be enriched. In order to support the three CompCert states, our module definitions require five additional Verilog registers."} +To support this computational model, we extend the Verilog module we generate with the following five registers and a RAM block: \begin{description} - \item[program counter] First of all, the program counter needs to be modelled, which can be done using a register which keeps track of state, denoted as $\sigma$. - \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed, which can be modelled using a reset signal that sets the state accordingly, denoted as $rst$. - \item[return value] The return value can be modelled by setting a finished flag to one when the result is ready, and putting the result into a 32-bit output register, denoted as \textit{fin} and \textit{rtrn} respectively. - \item[stack] The function stack can be modelled as a RAM using a two-di\-men\-sion\-al array in the module, denoted as \textit{stk}. + \item[program counter] The program counter can be modelled using a register that keeps track of the state, denoted as $\sigma$. + \item[function entry point] When a function is called, the entry point denotes the first instruction that will be executed. This can be modelled using a reset signal that sets the state accordingly, denoted as \textit{rst}. + \item[return value] The return value can be modelled by setting a finished flag to 1 when the result is ready, and putting the result into a 32-bit output register. These are denoted as \textit{fin} and \textit{rtrn} respectively. + \item[stack] The function stack can be modelled as a RAM block, which is implemented using an array in the module, and denoted as \textit{stk}. \end{description} -Figure~\ref{fig:inferrence_module} shows the inference rules that convert from one state to another. The first rule \textsc{Step} is the normal rule of execution. Assuming that the module is not being reset, and that the finish state has not been reached yet and that the current and next state are $v$ and $v'$, and finally that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Step} rule, we can then define one step in the \texttt{State}. The \textsc{Finish} rule is the rule that returns the final value of running the module and is applied when the \textit{fin} register is set. The return value is then taken from the \textit{ret} register. +Figure~\ref{fig:inferrence_module} shows the inference rules for moving between the computational states. The first, \textsc{Step}, is the normal rule of execution. It defines one step in the \texttt{State} state, assuming that the module is not being reset, that the finish state has not been reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state $\Gamma$ to $\Gamma'$ using the \textsc{Step} rule. The \textsc{Finish} rule returns the final value of running the module and is applied when the \textit{fin} register is set; the return value is then taken from the \textit{ret} register. The first thing to note about the \textsc{Call} rule 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. The same can be said about the \textsc{Return} state rule, which will only be matched for the final return value from the main function, as there is no rule that allocates another stack frame \textit{sf} except for the initial call to main. Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module}, an initial state and final state need to be defined. |