From 13924d40f0e7e0d7abeec2febc84930324018a6f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 18 Nov 2020 11:37:40 +0000 Subject: Fix comments in algorithm section --- archive/algorithm.tex | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'archive') 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. -- cgit