diff options
| -rw-r--r-- | algorithm.tex | 8 | ||||
| -rw-r--r-- | introduction.tex | 9 | ||||
| -rw-r--r-- | proof.tex | 2 | ||||
| -rw-r--r-- | references.bib | 33 |
4 files changed, 13 insertions, 39 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. diff --git a/introduction.tex b/introduction.tex index b312fe0..166d092 100644 --- a/introduction.tex +++ b/introduction.tex @@ -43,12 +43,17 @@ The contributions of this paper are as follows: \begin{itemize} \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. The design of \vericert{} is described in Section~\ref{sec:design}. \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_formalise}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself. - \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve when we extend \vericert{} with such optimisations as loop pipelining and scheduling. + \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve once we have extended \vericert{} with such optimisations as loop pipelining and scheduling. \end{itemize} -\vericert{} is fully open source and available online. \JW{We'll have to blind this (and maybe even the name of the tool itself) for submission.} +\vericert{} is fully open source and available online. + \begin{center} +\ifANONYMOUS \url{https://github.com/ymherklotz/vericert} +\else + +\fi \end{center} @@ -88,7 +88,7 @@ The HTL to Verilog simulation is quite simple, as the only transformation is fro The translation from maps to case statements is done by turning each node of the tree into a case expression with the statments in each being the same. The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key in this list will be unique. In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list. The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list. The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't. In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore. In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match. -Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow. Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$. We therefore have to prove that the state value will never go over that value. This means that during the translation we have to check for each state that it can fit into an integer. Finally, as we have to assume that there are $2^{32} - 1$ states, Vericert will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct. +Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow. Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$. We therefore have to prove that the state value will never go over that value. This means that during the translation we have to check for each state that it can fit into an integer. Finally, as we have to assume that there are $2^{32} - 1$ states, \vericert{} will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct. \subsection{Deterministic Semantics} diff --git a/references.bib b/references.bib index 7df5cbe..c57bad9 100644 --- a/references.bib +++ b/references.bib @@ -335,15 +335,7 @@ year = {2008}, } -@inproceedings{loow19_formalise, - author = {Andreas L{\"{o}}{\"{o}}w and - Magnus O. Myreen}, - title = {A proof-producing translator for Verilog development in {HOL}}, - booktitle = {FormaliSE@ICSE}, - pages = {99--108}, - publisher = {{IEEE} / {ACM}}, - year = {2019} -} + @misc{slec_whitepaper, author = {Chauhan, Pankaj}, @@ -640,29 +632,6 @@ year = {2020}, pages = {7--es}, } -@inproceedings{loow19_verif_compil_verif_proces, - author = {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and - Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar - and Fox, Anthony}, - title = {Verified Compilation on a Verified Processor}, - tags = {verification}, - booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming - Language Design and Implementation}, - year = 2019, - pages = {1041--1053}, - doi = {10.1145/3314221.3314622}, - url = {https://doi.org/10.1145/3314221.3314622}, - acmid = 3314622, - address = {New York, NY, USA}, - isbn = {978-1-4503-6712-7}, - keywords = {compiler verification, hardware verification, program - verification, verified stack}, - location = {Phoenix, AZ, USA}, - numpages = 13, - publisher = {ACM}, - series = {PLDI 2019} -} - @inproceedings{loow19_proof_trans_veril_devel_hol, author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.}, title = {A Proof-producing Translator for Verilog Development in HOL}, |