Backend to back end

2 files changed, 2 insertions, 2 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 06cf110..5fee4db 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -81,7 +81,7 @@ The main work flow of \vericert{} is given in Figure~\ref{fig:rtlbranch}, which
 We select CompCert's three-address code (3AC)\footnote{This is known as register transfer language (RTL) in the \compcert{} literature. `3AC' is used in this paper instead to avoid confusion with register-transfer level (RTL), which is another name for the final hardware target of the HLS tool.} as the starting point. Branching off \emph{before} this point (at CminorSel or earlier) denies \compcert{} the opportunity to perform optimisations such as constant propagation and dead code elimination, which, despite being designed for software compilers, have been found useful in HLS tools as well~\cite{cong+11}. And if we branch off \emph{after} this point (at LTL or later) then \compcert{} has already performed register allocation to reduce the number of registers and spill some variables to the stack; this transformation is not required in HLS because there are many more registers available, and these should be used instead of RAM whenever possible. %\JP{``\compcert{} performs register allocation during the translation to LTL, with some registers spilled onto the stack: this is unnecessary in HLS since as many registers as are required may be described in the output RTL.''} \JP{Maybe something about FPGAs being register-dense (so rarely a need to worry about the number of flops)?}
 
 3AC is also attractive because it is the closest intermediate language to LLVM IR, which is used by several existing HLS compilers. %\JP{We already ruled out LLVM as a starting point, so this seems like it needs further qualification.}\YH{Well not because it's not a good starting point, but the ecosystem in Coq isn't as good.  I think it's still OK here to say that being similar to LLVM IR is an advantage?} 
-It has an unlimited number of pseudo-registers, and is represented as a control flow graph (CFG) where each instruction is a node with links to the instructions that can follow it. One difference between LLVM IR and 3AC is that 3AC includes operations that are specific to the chosen target architecture; we chose to target the x86\_32 backend because it generally produces relatively dense 3AC thanks to the availability of complex addressing modes.% reducing cycle counts in the absence of an effective scheduling approach.
+It has an unlimited number of pseudo-registers, and is represented as a control flow graph (CFG) where each instruction is a node with links to the instructions that can follow it. One difference between LLVM IR and 3AC is that 3AC includes operations that are specific to the chosen target architecture; we chose to target the x86\_32 back end because it generally produces relatively dense 3AC thanks to the availability of complex addressing modes.% reducing cycle counts in the absence of an effective scheduling approach.
 
 \subsection{An introduction to Verilog}
 
diff --git a/related.tex b/related.tex
index a93dbf0..ee8e6b4 100644
--- a/related.tex
+++ b/related.tex
@@ -48,7 +48,7 @@ Most practical HLS tools~\citep{canis11_legup,xilinx20_vivad_high_synth,intel20_
 
 Ongoing work in translation validation~\citep{pnueli98_trans} seeks to prove equivalence between the hardware generated by an HLS tool and the original behavioural description in C.  An example of a tool that implements this is Mentor's Catapult~\citep{mentor20_catap_high_level_synth}, which tries to match the states in the 3AC description to states in the original C code after an unverified translation.  Using translation validation is quite effective for verifying complex optimisations such as scheduling~\citep{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\citep{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}, but the validation has to be run every time the HLS is performed.  In addition to that, the proofs are often not mechanised or directly related to the actual implementation, meaning the verifying algorithm might be wrong and hence could give false positives or false negatives.
 
-Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translator from a core fragment of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, so is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a proof-producing translator from HOL4 code describing state transitions into Verilog to design a verified processor, which is described further by \citet{loow19_verif_compil_verif_proces}. \citet{10.1145/3437992.3439916} has also worked on formally verifying a logic synthesis tool that can transform hardware descriptions into low-level netlists.  This synthesis backend can seamlessly integrate with the proof-producing HOL4 to Verilog translator as it is based on the same Verilog semantics, and therefore creates verified translation from HOL4 circuit descriptions to synthesised Verilog netlists.
+Finally, there are a few relevant mechanically verified tools.  First, K\^{o}ika is a formally verified translator from a core fragment of BlueSpec into a circuit representation which can then be printed as a Verilog design.  This is a translation from a high-level hardware description language into an equivalent circuit representation, so is a different approach to HLS.  \citet{loow19_proof_trans_veril_devel_hol} used a proof-producing translator from HOL4 code describing state transitions into Verilog to design a verified processor, which is described further by \citet{loow19_verif_compil_verif_proces}. \citet{10.1145/3437992.3439916} has also worked on formally verifying a logic synthesis tool that can transform hardware descriptions into low-level netlists.  This synthesis back end can seamlessly integrate with the proof-producing HOL4 to Verilog translator as it is based on the same Verilog semantics, and therefore creates verified translation from HOL4 circuit descriptions to synthesised Verilog netlists.
 Perna et al. designed a formally verified translator from a deep embedding of Handel-C~\citep{aubury1996handel} into a deep embedding of a circuit~\cite{perna12_mechan_wire_wise_verif_handel_c_synth,perna11_correc_hardw_synth}.
 Finally, \citet{ellis08} used Isabelle to implement and reason about intermediate languages for software/hardware compilation, where parts could be implemented in hardware and the correctness could still be shown.