Fix algorithm

1 files changed, 3 insertions, 2 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 4ea9f98..cbdd0f0 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -294,7 +294,8 @@ module main(reset, clk, finish, return_val);
         32'd5: state <= 32'd4;
         32'd4: state <= 32'd3;
         32'd3: state <=
-          ({$signed(reg_1) < $signed(32'd3)}
+          ({$signed(reg_1)
+            < $signed(32'd3)}
              ? 32'd7 : 32'd2);
         32'd2: state <= 32'd1;
         32'd1: ;
@@ -322,7 +323,7 @@ Although we would not claim that \vericert{} is a proper `optimising' HLS compil
 \subsubsection{Byte- and word-addressable memories}
 
 One big difference between C and Verilog is how memory is represented.  In hardware, efficient RAMs are not as available as in software, and need to be explicitly implemented by declaring two-dimensional arrays with specific properties.  A major limitation is that RAMs often only allow one read and one write per clock cycle. So, to make loads and stores as efficient as possible, the RAM needs to be word-addressable, which means that an entire integer can be loaded or stored in one clock cycle.
-However, the memory model that \compcert{} uses for its intermediate languages is byte-addressable~\cite{blazy05_formal_verif_memor_model_c}.  It therefore has to be proven that the byte-addressable memory behaves in the same way as the word-addressable memory in hardware.  Any modifications of the bytes in the \compcert{} memory model also have to be shown to modify the word-addressable memory in the same way.  Since only integer loads and stores are currently supported in \vericert{}, it follows that the addresses given to the loads and stores should be multiples of four.  If that is the case, then the translation from byte-addressed memory to word-addressed memory can be done by dividing the address by four.
+However, the memory model that \compcert{} uses for its intermediate languages is byte-addre\-ssa\-ble~\cite{blazy05_formal_verif_memor_model_c}.  It therefore has to be proven that the byte-addressable memory behaves in the same way as the word-addressable memory in hardware.  Any modifications of the bytes in the \compcert{} memory model also have to be shown to modify the word-addressable memory in the same way.  Since only integer loads and stores are currently supported in \vericert{}, it follows that the addresses given to the loads and stores should be multiples of four.  If that is the case, then the translation from byte-addressed memory to word-addressed memory can be done by dividing the address by four.
 
 \subsubsection{Implementing the \texttt{Oshrximm} instruction}