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 f8bc8ae..e630cbe 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -1,10 +1,10 @@ \section{Designing a verified HLS tool} \label{sec:design} -This section covers the main architecture of the HLS tool, and the way in which the back end was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. +This section covers the main architecture of the HLS tool, and the way in which the Verilog back end was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. \paragraph{Choice of source language} -First of all, the choice of C for the input language of \vericert{} is simply because it is what most major HLS tools use~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because C is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}. +First of all, the choice of C as the input language of \vericert{} is simply because it is what most major HLS tools use~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because C is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}. %Since a lot of existing code for HLS is written in C, supporting C as an input language, rather than a custom domain-specific language, means that \vericert{} is more practical. %An alternative was to support LLVM IR as an input language, however, to get a full work flow from a higher level language to hardware, a front end for that language to LLVM IR would also have to be verified. \JW{Maybe save LLVM for the `Choice of implementation language'?} We considered Bluespec~\cite{nikhil04_blues_system_veril}, but decided that although it ``can be classed as a high-level language''~\cite{greaves_note}, it is too hardware-oriented to be used for traditional HLS. @@ -216,7 +216,7 @@ An HTL program thus consists of two maps: a control map that describes how to ca \end{figure*} \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, 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. +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. \paragraph{Translating instructions} Each 3AC instruction either corresponds to a hardware construct, or does not have to be handled by the translation, such as function calls. @@ -301,7 +301,7 @@ endmodule \end{minted} %\caption{Verilog always block describing the control logic of the module.}\label{fig:accumulator_v_2} %\end{subfigure} - \caption{Accumulator example using \vericert{} to translate the 3AC to a state machine expressed in Verilog. \JW{If space permits, it would probably be preferable to have this code in a single column, as splitting a single module across two subfigures is a bit jarring.}\YH{I actually don't mind it for some reason, because it separates control flow and data path, but it's true it is weird. The only problem is it's very long if I don't do that.}}\label{fig:accumulator_v} + \caption{Verilog output for our running example, as generated by \vericert{}. The left column contains the datapath and the right column contains the control logic.}\label{fig:accumulator_v} \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. |