Update on Overleaf.

1 files changed, 2 insertions, 0 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.