Add some detail about how call/return works in HTL

1 files changed, 1 insertions, 1 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 5860a00..c47cf66 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -410,7 +410,7 @@ registers present in \lstinline{externctrl} to the name of the register they tar
 The CompCert correctness theorem~\cite{compcert} expresses that every behaviour that can be exhibited by the compiled program is also a behaviour of the source program. \vericert{}~\cite{Herklotz2020} adapted this theorem for HLS by replacing `compiled program' with `generated Verilog design'. In both cases, a formal semantics is required for the source and target languages. \vericertfun{} targets the same fragment of the Verilog language as \citeauthor{Herklotz2020} already mechanised in Coq, so no changes are required there. 
 
 Where changes \emph{are} required is in the semantics of the intermediate language HTL, which sits between CompCert's 3AC and the final Verilog.
-When \citeauthor{Herklotz2020} designed HTL, they did not include a semantics for function calls because they assumed all function calls would already have been inlined. We have extended HTL so that its semantics is additionally parameterised by an environment that maps function names to state machines. We have added a semantics for function calls that looks up the named function in this environment, activates the corresponding state machine, and creates a new frame on the stack. We have also added a semantics for return statements that pops the current frame off the stack and reactivates the caller's state machine. \MP{TODO: Consider saying something here about how the effect of a function call is to put the state machine into a particular `callstate'. My concern is that this requires introducing a different notion of `state', distinct from the states of the state machine, and that this will probably confuse readers.}
+When \citeauthor{Herklotz2020} designed HTL, they did not include a semantics for function calls because they assumed all function calls would already have been inlined. We have extended HTL so that its semantics is additionally parameterised by an environment that maps function names to state machines. We have added a semantics for function calls that looks up the named function in this environment, activates the corresponding state machine, and creates a new frame on the stack. We have also added a semantics for return statements that pops the current frame off the stack and reactivates the caller's state machine. Calls are initiated by triggering the reset signal of the called module (using the externctrl mechanism described earlier). Similarly, a function enters its returning state by setting its own ``finished'' register. \emph{There are no call or return instructions in HTL}. \MP{One aspect of this I didn't mention: This introduces non-determinism. When you set the reset of a module, the next state can be either a call or a normal executing state, ignoring the reset. This non-determinism does not affect the RTL-to-HTL proof, but could affect the HTL-to-Verilog one.}
 
 At the point of writing, the correctness of \vericertfun{} from C to HTL has been mostly proven,
 meaning basic instructions, as well as the function calls themselves and their interaction with the