Fix algorithm section

2 files changed, 20 insertions, 17 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 6c02326..4ea9f98 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -220,6 +220,11 @@ An HTL program thus consists of two maps: a control map that describes how to ca
   \caption{The FSMD for the example shown in Figure~\ref{fig:accumulator_c_rtl}, split into a data path and control logic for the next state calculation.  The Update block takes the current state, current values of all registers and at most one value stored in the array, and calculates a new value that can either be stored back in the array or in a register.}\label{fig:accumulator_diagram}
 \end{figure*}
 
+The translation from 3AC to HTL is straightforward, as each 3AC instruction either matches up quite well to a hardware construct, or does not have to be handled by the translation, such as function calls.
+%At each instruction, the control flow is separated from the data computation and is then added to the control logic and data-flow map respectively.
+%\JW{I suspect that you could safely chop that sentence.}
+For example, in state 15 in figure~\ref{fig:accumulator_rtl}, the register \texttt{x8} is initialised to 1, after which the control flow moves to state 14.  This is encoded in HTL by initialising a 32-bit register \texttt{reg\_8} to 1 in the data-flow section, and also adding a transition to the state 15 in the control logic section.  Simple operator instructions are translated in a similar way.  For example, in state 5, the value in the array is added to the current value of the accumulated sum, which is simply translated to an addition of the equivalent registers in the HTL code.
+
 \paragraph{Translating memory}
 Hardware does not have the same memory model as C, so the memory model needs to be translated, as follows.  Global variables are not translated in \vericert{} at the moment. The stack of the main function becomes a block of RAM, \JW{check this -- maybe change to 2D array of registers?} as seen in Figure~\ref{fig:accumulator_diagram}. Program variables that have their address taken are stored in this RAM, as are any arrays or structs defined in the function. Variables that do not have their address taken are kept in registers.
 
@@ -227,15 +232,8 @@ Hardware does not have the same memory model as C, so the memory model needs to
 Each 3AC instruction either corresponds to a hardware construct, or does not have to be handled by the translation, such as function calls.
 For example, in state 15 in figure~\ref{fig:accumulator_rtl}, the register \texttt{x8} is initialised to 1, after which the control flow moves to state 14.  This is encoded in HTL by initialising a 32-bit register \texttt{reg\_8} to 1 in the data-flow section, and also adding a transition to the state 14 in the control logic section.  Simple operator instructions are translated in a similar way.  For example, in state 5, the value in the array is added to the current value of the accumulated sum, which is simply translated to an addition of the equivalent registers in the HTL code.
 
-\paragraph{Key challenge: signedness} Note that the comparison in state 3 is signed. This is because 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 resizes expressions to the largest needed size by default, which can affect the result of the computation.  This feature is also not supported by the Verilog semantics we adopted, and there would therefore be a mismatch between the Verilog semantics and the actual behaviour of Verilog according to the standard.  To bypass this issue, braces are used to stop the Verilog simulator or synthesis tool from resizing anything inside the braces.  Instead, explicit resizing is used in the semantics and operations can only be performed on two registers that have the same size.
-
-\subsection{Translating HTL to Verilog}
-
-Finally, we have to translate the HTL code into proper Verilog. % and prove that it behaves the same as the 3AC according to the Verilog semantics.
-Whereas HTL is a language that is specifically designed to represent the FSMDs we are interested in, Verilog is a general-purpose HDL.\@  So the challenge here is to translate our FSMD representation into a Verilog AST.  However, as all the instructions are already expressed in Verilog, only the maps need to be translated to valid Verilog, and correct declarations for all the variables in the program need to be added as well.
-
-This translation seems quite straightforward, but proving it correct is not that simple, as all the implicit assumptions that were made in HTL need to be translated explicitly to Verilog statements and it needs to be shown that these explicit behaviours are equivalent to the assumptions made in the HTL semantics.
-Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated for our worked example.  In general, the structure is similar to that of the HTL code, but the control and datapath maps become Verilog case-statements.  The other main addition to the code is the initialisation of all the variables in the code to the correct bitwidths and the declaration of the inputs and outputs to the module, so that the module can be used inside a larger hardware design.
+\paragraph{Key challenge: signedness} Note that the comparison in state 3 is signed. This is because 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 resizes expressions to the largest needed size by default, which can affect the result of the computation.  This feature is also not supported by the Verilog semantics we adopted, and there would therefore be a mismatch between the Verilog semantics and the actual behaviour of Verilog according to the standard.  To bypass this issue, braces are used to stop the Verilog simulator or synthesis tool from resizing anything inside the braces.  Instead, explicit resizing is used in the semantics and operations can only be performed on two registers that
+have the same size.
 
 \begin{figure}
   \centering
@@ -309,17 +307,13 @@ endmodule
   \caption{Verilog output for our running example, as generated by \vericert{}. The left column contains the datapath and the right column contains the control logic.}\label{fig:accumulator_v}
 \end{figure}
 
-The translation from 3AC to HTL is straightforward, as each 3AC instruction either matches up quite well to a hardware construct, or does not have to be handled by the translation, such as function calls.
-%At each instruction, the control flow is separated from the data computation and is then added to the control logic and data-flow map respectively.
-%\JW{I suspect that you could safely chop that sentence.}
-For example, in state 15 in figure~\ref{fig:accumulator_rtl}, the register \texttt{x8} is initialised to 1, after which the control flow moves to state 14.  This is encoded in HTL by initialising a 32-bit register \texttt{reg\_8} to 1 in the data-flow section, and also adding a transition to the state 15 in the control logic section.  Simple operator instructions are translated in a similar way.  For example, in state 5, the value in the array is added to the current value of the accumulated sum, which is simply translated to an addition of the equivalent registers in the HTL code.
-
 \subsection{Translating HTL to Verilog}
 
-Finally, we have to translate the HTL code into proper Verilog and prove that it behaves the same as the 3AC according to the Verilog semantics.  Whereas HTL is a language that is specifically designed to represent the FSMDs we are interested in, Verilog is a general-purpose HDL.\@  So the challenge here is to translate our FSMD representation into a Verilog AST.  However, as all the instructions are already expressed in Verilog, only the maps need to be translated to valid Verilog, and correct declarations for all the variables in the program need to be added as well.
+Finally, we have to translate the HTL code into proper Verilog. % and prove that it behaves the same as the 3AC according to the Verilog semantics.
+Whereas HTL is a language that is specifically designed to represent the FSMDs we are interested in, Verilog is a general-purpose HDL.\@  So the challenge here is to translate our FSMD representation into a Verilog AST.  However, as all the instructions are already expressed in Verilog, only the maps need to be translated to valid Verilog, and correct declarations for all the variables in the program need to be added as well.
 
-This translation seems quite straightforward, however, proving that it is correct is not that simple, as all the implicit assumptions that were made in HTL need to be translated explicitly to Verilog statements and needs it needs to be shown that these explicit behaviours are equivalent to the assumptions made in the HTL semantics.
-Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated.  In general, the structure is similar to that of the HTL code, however, the control and datapath maps have been translated to case statements.  The other main addition to the code is the initialisation of all the variables in the code to the correct bitwidths and the declaration of the inputs and outputs to the module, so that the module can be used inside a larger hardware design.
+This translation seems quite straightforward, but proving it correct is not that simple, as all the implicit assumptions that were made in HTL need to be translated explicitly to Verilog statements and it needs to be shown that these explicit behaviours are equivalent to the assumptions made in the HTL semantics.
+Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated for our worked example.  In general, the structure is similar to that of the HTL code, but the control and datapath maps become Verilog case-statements.  The other main addition to the code is the initialisation of all the variables in the code to the correct bitwidths and the declaration of the inputs and outputs to the module, so that the module can be used inside a larger hardware design.
 
 \subsection{Optimisations}
 
diff --git a/archive/algorithm.tex b/archive/algorithm.tex
index 1d66770..bd85e4b 100644
--- a/archive/algorithm.tex
+++ b/archive/algorithm.tex
@@ -1,3 +1,12 @@
+\subsection{Translating HTL to Verilog}
+
+Finally, we have to translate the HTL code into proper Verilog and prove that it behaves the same as the 3AC according to the Verilog semantics.  Whereas HTL is a language that is specifically designed to represent the FSMDs we are interested in, Verilog is a general-purpose HDL.\@  So the challenge here is to translate our FSMD representation into a Verilog AST.  However, as all the instructions are already expressed in Verilog, only the maps need to be translated to valid Verilog, and correct declarations for all the variables in the program need to be added as well.
+
+This translation seems quite straightforward, however, proving that it is correct is not that simple, as all the implicit assumptions that were made in HTL need to be translated explicitly to Verilog statements and needs it needs to be shown that these explicit behaviours are equivalent to the assumptions made in the HTL semantics.
+Figure~\ref{fig:accumulator_v} shows the final Verilog output that is generated.  In general, the structure is similar to that of the HTL code, however, the control and datapath maps have been translated to case statements.  The other main addition to the code is the initialisation of all the variables in the code to the correct bitwidths and the declaration of the inputs and outputs to the module, so that the module can be used inside a larger hardware design.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsubsection{Reset signals}
 
 \YH{This section could maybe go into the proof section instead.}