Update on Overleaf.

1 files changed, 1 insertions, 1 deletions

diff --git a/algorithm.tex b/algorithm.tex
index f61368d..302494f 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -4,7 +4,7 @@
 This section covers \JP{describes} the main architecture of the HLS tool, and the way in which the Verilog back end \JP{back-end? backend?} 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 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}.  \JP{I think this could be reworded: ``C was chosen as the source language as it remains the most common source language amongst production-quality HLS tools~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because it is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}, lending practicality. The availability of \compcert{} [cite], also provides a solid basis for formally verified C compilation.''}
+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}.  \JP{I think this could be reworded: ``C was chosen as the source language as it remains the most common source language amongst production-quality HLS tools~\cite{canis11_legup, xilinx20_vivad_high_synth, intel_hls, bambu_hls}. This, in turn, may be because it is ``[t]he starting point for the vast majority of algorithms to be implemented in hardware''~\cite{5522874}, lending a degree of practicality. The availability of \compcert{} [cite] also provides a solid basis for formally verified C compilation.''}
 %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.