diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | evaluation.tex | 2 | ||||
| -rw-r--r-- | proof.tex | 3 | ||||
| -rw-r--r-- | verilog.tex | 2 |
4 files changed, 8 insertions, 1 deletions
diff --git a/algorithm.tex b/algorithm.tex index 3d55d93..bf29a30 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -37,6 +37,8 @@ The main work flow of \vericert{} is shown in Figure~\ref{fig:rtlbranch}, which Existing HLS compilers usually \JW{maybe `often' is a less contentious claim} use LLVM IR as an intermediate representation when performing HLS specific \JW{HLS-specific} optimisations, as each instruction can be mapped quite well to hardware which \JW{which -> that} performs the same behaviour. CompCert's three address \JW{three-address} code (3AC)\footnote{Three address \JW{Three-address} code (3AC) is also know \JW{known} as register transfer language (RTL) in the CompCert literature, however, 3AC is used in this paper so as not to confuse it with register transfer \JW{register-transfer} level (RTL), which is another name for the final hardware target of the HLS tool.} is the intermediate language that resembles LLVM IR the most, as it also has an infinite number of pseudo-registers and each instruction maps well to hardware. However, one difference between the two is that 3AC uses operations of the target architecture and performs architecture specific optimisations as well, which is not the case in LLVM IR where all the instructions are quite abstract. This can be mitigated by making CompCert target a specific architecture such as x86\_32, where most operations translate quite well into hardware. In addition to that, many optimisations that are also useful for HLS are performed in 3AC, which means that if it is supported as the input language, the HLS algorithm benefits from the same optimisations. It is therefore a good candidate to be chosen as the input language to the HLS backend. The complete flow that Vericert takes is show in figure~\ref{fig:rtlbranch}. +\JW{I wonder if Section 2 could benefit from a `Some Key Challenges' subsection, where you highlight several interesting bits of the translation process, each with their own paragraph heading. These could be something like:\begin{enumerate}\item Discrepancy between C and Verilog w.r.t. signedness \item Deciding between byte- and word-addressable memories \item Adding reset signals \item Implementing the Oshrximm instruction correctly \end{enumerate} For the causal reader, this would immediately signal two things: (1) you can skip this subsection on your initial pass, and (2) proving the HLS tool correct was a non-trivial undertaking.} + % - Explain main differences between translating C to software and to hardware. % + This can be done by going through the simple example. diff --git a/evaluation.tex b/evaluation.tex index 8f49de1..b81d08d 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -1,6 +1,6 @@ \section{Evaluation} -Our evaluation is designed to answer the following three research questions. +Our evaluation is designed to answer the following three research questions. \JW{How about adding one more RQ at the start called `How reliable is the hardware generated by \vericert{}, and how does this compare to existing HLS tools?' Then you can answer this by saying that you couldn't break your tool using the Csmith programs generated by Du et al., which did break all the other HLS tools.} \begin{description} \item[RQ1] How fast is the hardware generated by \vericert{}, and how does this compare to existing HLS tools? \item[RQ2] How area-efficient is the hardware generated by \vericert{}, and how does this compare to existing HLS tools? @@ -15,6 +15,7 @@ However, this forward simulation might still allow for wrong behaviour of the ta \end{equation*} To prove this statement, we therefore have to prove that the Verilog semantics are deterministic and that the forward simulation between the C and the Verilog holds as well. +\JW{Hm, I'm a little confused. Which theorem is the actual `correctness' theorem? Looks like we could combine the two theorems into something like \[\forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \implies (V \Downarrow_{s} B ~\text{iff}~ C \Downarrow B)\] Is that the theorem you actually want?} \subsection{Forward Simulation} @@ -94,6 +95,8 @@ The Verilog semantics that are used are deterministic, as the order of operation \subsection{Coq Mechanisation} +\JW{Would be nice to include a few high-level metrics here. How many person-years of effort was the proof (very roughly)? How many lines of Coq? How many files, how many lemmas? How long does it take for the Coq proof to execute?} + \subsection{Proving \texttt{Oshrximm} correct} % Mention that this optimisation is not performed sometimes (clang -03). diff --git a/verilog.tex b/verilog.tex index 023a5a9..dfa378e 100644 --- a/verilog.tex +++ b/verilog.tex @@ -1,5 +1,7 @@ \section{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. Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware. Many Verilog features are only useful for simulation and do not affect the actual 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. |