Fix comments in algorithm section

1 files changed, 7 insertions, 0 deletions

diff --git a/archive/algorithm.tex b/archive/algorithm.tex
index 376196a..1d66770 100644
--- a/archive/algorithm.tex
+++ b/archive/algorithm.tex
@@ -1,3 +1,10 @@
+\subsubsection{Reset signals}
+
+\YH{This section could maybe go into the proof section instead.}
+
+\JW{Yeah I agree that the rest of this paragraph describes a detail of the proof and should be in the Proof section.}
+Even though functions calls are not supported by \vericert{}, the initial function call that \compcert{} uses to enter the main function does need to be supported in the Verilog semantics, as explained further in Section~\ref{sec:verilog}.  The reset signal therefore has to be reasoned about correctly in the Semantics and in the initial function call to ensure that the initial state of the module is set correctly, as in 3AC, the entry point of the function is part of the function definition.
+
 \paragraph{Key challenge: Adding reset signals}
 In hardware, there is no notion of a stack that can be popped or pushed.  It is therefore necessary to add reset signals to the main module \JWcouldcut{that will be called} so that the proper state can be set at the start of the function.
 The main subtle change that was added to the code is the reset signal which sets the state to the starting state correctly.  In HTL, this was described directly in the semantics, where the entry point is stored in the module interface of HTL.  However, in Verilog we also want to verify that the hardware will be placed into the right state when we power it up or reset the design, and it therefore has to be encoded directly in the Verilog code.