diff options
Diffstat (limited to 'algorithm.tex')
| -rw-r--r-- | algorithm.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/algorithm.tex b/algorithm.tex index 757857d..bf98b6c 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -31,7 +31,7 @@ The framework that was chosen for the frontend was \compcert{}, as it is a matur \node[language] at (4.7,-2) (dfgstmd) {HTL}; \node[language] at (6.7,-2) (verilog) {Verilog}; \node at (0,1) {\compcert{}}; - \node at (0,-2) {Vericert}; + \node at (0,-2) {\vericert{}}; \draw[->] (clight) -- (conta); \draw[->] (conta) -- (cminor); \draw[->] (cminor) -- (rtl); @@ -97,7 +97,7 @@ main() { \subsection{Translating C to Verilog, by example} -Using the simple accumulator program shown in Figure~\ref{fig:accumulator_c} as a worked example, this section describes the main translation that is performed in Vericert to go from the behavioural description in C into a hardware design in Verilog. +Using the simple accumulator program shown in Figure~\ref{fig:accumulator_c} as a worked example, this section describes the main translation that is performed in \vericert{} to go from the behavioural description in C into a hardware design in Verilog. \subsubsection{Translating C to 3AC} @@ -111,7 +111,7 @@ The first step of the translation is to use \compcert{} to transform the input C % + TODO Explain how memory is mapped -The first translation performed in Vericert is from 3AC to a new hardware translation language (HTL), which is one step towards being completely translated to hardware described in Verilog. The main translation that is performed is going from a CFG representation of the computation to a finite state machine with datapath (FSMD)~\cite{hwang99_fsmd}\JW{I feel like this could use some sort of citation, but I'm not sure what. I guess this is all from "Hardware Design 101", right?}\YH{I think I found a good one actually, which goes over the basics.} representation in HTL.\@ The core idea of the FSMD representation is that it separates the control flow from the operations on the memory and registers, so that the state transitions can be translated into a simple finite state machine (FSM) and each state then contains data operations that update the memory and registers. Figure~\ref{fig:accumulator_diagram} shows the resulting architecture of the FSMD. \JW{I think it would be worth having a sentence to explain how the C model of memory is translated to a hardware-centric model of memory. For instance, in C we have global variables/arrays, stack-allocated variables/arrays, and heap-allocated variables/arrays (anything else?). In Verilog we have registers and RAM blocks. So what's the correspondence between the two worlds? Globals and heap-allocated are not handled, stack-allocated variables become registers, and stack-allocated arrays become RAM blocks? Am I close?}\YH{Stack allocated variables become RAM as well, so that we can deal with addresses easily and take addresses of any variable.} \JW{I see, thanks. So, in short, the only registers in your hardware designs are those that store things like the current state, etc. You generate a fixed number of registers every time you synthesis -- you don't generate extra registers to store any of the program variables. Right?} Hardware does not have the same memory model as C, the memory model therefore needs to be translated in the following way. Global variables are not translated in Vericert at the moment, however, the stack of the main function will become the RAM seen in Figure~\ref{fig:accumulator_diagram}. Variables that have their address is taken will therefore be stored in the RAM, as well as any arrays or structs defined in the function. Variables that did not have their address taken will be kept in registers. +The first translation performed in \vericert{} is from 3AC to a new hardware translation language (HTL), which is one step towards being completely translated to hardware described in Verilog. The main translation that is performed is going from a CFG representation of the computation to a finite state machine with datapath (FSMD)~\cite{hwang99_fsmd}\JW{I feel like this could use some sort of citation, but I'm not sure what. I guess this is all from "Hardware Design 101", right?}\YH{I think I found a good one actually, which goes over the basics.} representation in HTL.\@ The core idea of the FSMD representation is that it separates the control flow from the operations on the memory and registers, so that the state transitions can be translated into a simple finite state machine (FSM) and each state then contains data operations that update the memory and registers. Figure~\ref{fig:accumulator_diagram} shows the resulting architecture of the FSMD. \JW{I think it would be worth having a sentence to explain how the C model of memory is translated to a hardware-centric model of memory. For instance, in C we have global variables/arrays, stack-allocated variables/arrays, and heap-allocated variables/arrays (anything else?). In Verilog we have registers and RAM blocks. So what's the correspondence between the two worlds? Globals and heap-allocated are not handled, stack-allocated variables become registers, and stack-allocated arrays become RAM blocks? Am I close?}\YH{Stack allocated variables become RAM as well, so that we can deal with addresses easily and take addresses of any variable.} \JW{I see, thanks. So, in short, the only registers in your hardware designs are those that store things like the current state, etc. You generate a fixed number of registers every time you synthesis -- you don't generate extra registers to store any of the program variables. Right?} Hardware does not have the same memory model as C, the memory model therefore needs to be translated in the following way. Global variables are not translated in \vericert{} at the moment, however, the stack of the main function will become the RAM seen in Figure~\ref{fig:accumulator_diagram}. Variables that have their address is taken will therefore be stored in the RAM, as well as any arrays or structs defined in the function. Variables that did not have their address taken will be kept in registers. \begin{figure*} \centering @@ -217,7 +217,7 @@ However, the memory model that \compcert{} uses for its intermediate languages~\ % Mention that this optimisation is not performed sometimes (clang -03). -Vericert performs some optimisations at the level of the instructions that are generated, so that the hardware performs the instructions as quickly as possible and so that the maximum frequency at which the hardware can run is increased. One of the main constructs that cripple performance of the generated hardware is the instantiation of divider circuits in the hardware. In the case of Vericert, it requires the result of the divide operation to be ready in the same clock cycle, meaning the divide circuit needs to be implemented fully combinationally. This is inefficient in terms of hardware size, but also in terms of latency, because it means that the maximum frequency of the hardware needs to be reduced dramatically so that the divide circuit has enough time to finish. +\vericert{} performs some optimisations at the level of the instructions that are generated, so that the hardware performs the instructions as quickly as possible and so that the maximum frequency at which the hardware can run is increased. One of the main constructs that cripple performance of the generated hardware is the instantiation of divider circuits in the hardware. In the case of \vericert{}, it requires the result of the divide operation to be ready in the same clock cycle, meaning the divide circuit needs to be implemented fully combinationally. This is inefficient in terms of hardware size, but also in terms of latency, because it means that the maximum frequency of the hardware needs to be reduced dramatically so that the divide circuit has enough time to finish. These small optimisations were found to be the most error prone, and guaranteeing that the new representation is equivalent to representation used in the \compcert{} semantics is difficult without proving this for all possible inputs. |