Update on Overleaf.

1 files changed, 8 insertions, 6 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 7607e5c..32c14ba 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -300,17 +300,19 @@ A high-level overview of the architecture can be seen in Figure~\ref{fig:accumul
 \paragraph{Translating instructions}
 
 Each 3AC instruction either corresponds to a hardware construct, or does not have to be handled by the translation, such as function calls (because of inlining).
-For example, line 2 in Figure~\ref{fig:accumulator_rtl} shows a 32-bit register \texttt{x5} being initialised to 3, after which the control flow moves execution to line 3. This initialisation is also encoded in HTL at state 8 in both the control- and data-path always-blocks, shown in Figure~\ref{fig:accumulator_v}.  Simple operator instructions are translated in a similar way.
+For example, line 2 in Figure~\ref{fig:accumulator_rtl} shows a 32-bit register \texttt{x5} being initialised to 3, after which the control flow moves execution to line 3. This initialisation is also encoded in HTL at state 8 in both the control- and data-path \JW{There's an inconsistency throughout this section between `control logic' and `control-path'.} always-blocks, shown in Figure~\ref{fig:accumulator_v}.  Simple operator instructions are translated in a similar way.
 
-C and Verilog handle signedness quite differently; by default, all operators and registers in Verilog (and HTL) are unsigned, so to force an operation to handle the bits as signed, both operators have to be forced to be signed.  In addition to that, Verilog implicitly resizes expressions to the largest needed size by default, which can affect the result of the computation.  This feature is not supported by the Verilog semantics we adopted, so to match the semantics to the behaviour of the simulator and synthesis tool, braces are placed around all expressions as this inhibits implicit resizing.  Instead, explicit resizing is used in the semantics and operations can only be performed on two registers that have the same size.
+C and Verilog handle signedness quite differently. By default, all operators and registers in Verilog (and HTL) are unsigned, so to force an operation to handle the bits as signed, both operators have to be forced to be signed. Moreover, Verilog implicitly resizes expressions to the largest needed size by default, which can affect the result of the computation.  This feature is not supported by the Verilog semantics we adopted, so to match the semantics to the behaviour of the simulator and synthesis tool, braces are placed around all expressions to inhibit implicit resizing.  Instead, explicit resizing is used in the semantics, and operations can only be performed on two registers that have the same size.
 
-In addition to that, equality between \emph{unsigned} variables are actually not supported, because this requires supporting the comparison of pointers, which should only be performed between pointers with the same provenance.  In \vericert{} there is currently no way to determine the provenance of a pointer, and it therefore cannot model the semantics of unsigned comparison in \compcert{}.  As dynamic allocation is not supported either, equality comparison of pointers is rarely needed, and for the equality comparison of integers, these can be cast to signed integers during the equality check for the translation to succeed.
+In addition to that, equality between \emph{unsigned} variables is actually not supported, because this requires supporting the comparison of pointers, which should only be performed between pointers with the same provenance.  In \vericert{} there is currently no way to determine the provenance of a pointer, and it therefore cannot model the semantics of unsigned comparison in \compcert{}. \JW{Perhaps begin this sentence with `This is not a severe restriction in practice, however, because...' and then rejig the rest of the sentence accordingly? That would make the sentiment clear to the casual reader.} As dynamic allocation is not supported either, equality comparison of pointers is rarely needed, and for the equality comparison of integers, these can be cast to signed integers during the equality check for the translation to succeed.
 
-Finally, the \texttt{mulhs} and \texttt{mulhu} instructions are not translated by \vericert{} either.  These instructions fetch the upper bits of a 32-bit multiply.  However, 64-bit number representations are currently not supported in the generated hardware, so this operation cannot currently be performed.  These instructions are only generated to optimise divides by a constant number that is not a power of two, so turning off constant propagation will allow these programs to pass without error.
+Finally, the \texttt{mulhs} and \texttt{mulhu} instructions, which fetch the upper bits of a 32-bit multiplication, are not translated by \vericert{} either. 
+\JW{maybe add `because 64-bit numbers are not supported.' and then delete the next sentence?}
+However, 64-bit number representations are currently not supported in the generated hardware, so this operation cannot currently be performed.  These instructions are only generated to optimise divides \JW{divisions?} by a constant \JWcouldcut{number} that is not a power of two, so turning off constant propagation will allow these programs to pass without error.
 
 \subsubsection{RAM insertion}
-
-This pass goes from HTL back to HTL and extracts all the direct accesses to the Verilog array implementing memory and replaces them by signals which access the memory in a separate always-block.  This ensures that the synthesis tool correctly identifies the array as being a RAM, so that it is not implemented by logic directly.  The translation is performed by going through all the instructions and replacing each load and store expression one after another.  Stores can simply be replaced by the necessary wires directly, however, loads using the RAM block take two clock cycles instead of a direct load from an array which only takes one clock cycles.  This pass therefore creates a extra state which is inserted after each load.
+\JW{I thought this was going in to}
+This pass goes from HTL \JWcouldcut{back} to HTL and extracts all the direct accesses to the Verilog array implementing memory and replaces them by signals which access the memory in a separate always-block.  This ensures that the synthesis tool correctly identifies the array as being a RAM, so that it is not implemented by logic directly.  The translation is performed by going through all the instructions and replacing each load and store expression one after another.  Stores can simply be replaced by the necessary wires directly, however, loads using the RAM block take two clock cycles instead of a direct load from an array which only takes one clock cycles.  This pass therefore creates a extra state which is inserted after each load.
 
 \subsubsection{Translating HTL to Verilog}