1 files changed, 36 insertions, 0 deletions
diff --git a/content/zettel/3c6b.md b/content/zettel/3c6b.md
new file mode 100644
index 0000000..a602a5a
--- /dev/null
+++ b/content/zettel/3c6b.md
@@ -0,0 +1,36 @@
++++
+title = "Semantics of function calls"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c6a"]
+forwardlinks = []
+zettelid = "3c6b"
++++
+
+I believe that your concern was that because we match on the value of
+the reset signal to start the function call, and that this is defined in
+the specification as well as in the implementation, that this means that
+we basically could replace it by any other value (not just 1), and the
+proof would still pass.
+
+I think that this is actually true, but similar to a different problem
+that is already present in the original version of Vericert from OOPSLA.
+In RTL, everything is started with a call to main, whereas in HTL we
+make necessary assumptions about this. The main one is a kind of calling
+convention, that says that to start the module one has to assert the
+reset signal for one clock cycle, and then set it to low until the
+module finishes execution. This is an assumption that is just in the
+semantics of Verilog and HTL directly.
+
+So for HTL from VericertFun, it's basically a similar problem and
+solution. We basically define a certain calling convention. The
+semantics then say that if a reset signal of one of the modules is now
+**low**, we will go into a call state. I think that another assumption
+that is kind of implicit to the semantics (and which will need to be
+proven during the translation to Verilog), is that the current state
+machine will indeed completely stop and relinquish control to the other
+state machine. Even though the current code does do that, it is actually
+not required to prove this until we combine the state machines into one
+large Verilog module. HTL semantics basically still have a magic jump
+where it will go from the current state machine into the new one.