blob: a602a5a08d1a21cb1349ff355a16b994069aa14a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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.
|
