express device_implements_state_machine using only run1, without runUntilResp (on top of #959)
#960
Conversation
verilator simulation functional test
not compatible any more with newer OpenTitan version
without using runUntilResp, so that each condition talks only about one cycle, which should be closer to Cava specs
|
I haven't really looked at this PR yet but I noticed yesterday that Also, I'm redoing CavaIncrementDevice.v anyway so don't worry about breaking it. |
| a_valid h2d = true -> | ||
| a_opcode h2d = Get -> | ||
| a_size h2d = N.of_nat log2_nbytes -> | ||
| a_address h2d = word_to_N (state_machine.reg_addr r) -> | ||
| d_ready h2d = true -> | ||
| device.run1 sL h2d = (sL', d2h) -> | ||
| if d_valid d2h then | ||
| exists sH', | ||
| device_state_related sH' sL' /\ | ||
| state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data d2h)) sH' | ||
| else | ||
| device_state_related sH sL' /\ | ||
| (device.maxRespDelay sL' h2d < device.maxRespDelay sL h2d)%nat; |
There was a problem hiding this comment.
This is incorrect in general (the original code also has the same issue).
TLDR: you never check a_ready d2h=1, and you might be sending multiple valid Get requests, instead of just one.
The process of reading from a register is broken down to two sub-tasks:
- Host sends a 'Get' command on channel A (h2d packet); and
- the device reply with an ack, that includes the value of the register, on channel D (d2h packet).
When you send an h2d packet on channel A you have to check that a_ready from the previous d2h packet is set to 1, only then you can send your h2d packet with a_valid=1, and you must send it only once (otherwise the other side might consider it as multiple messages).
After you sent the h2d packet on channel A you need to wait (i.e. send h2d packets with a_valid=0 and d_ready=1) until you get back a d2h packet with d_valid=1.
| we will get an ack response and the device will end up in a state corresponding to a | ||
| high-level state reached after a high-level write, but not necessarily in the state | ||
| we used to show that sH accepts writes *) | ||
| state_machine_write_to_device_write_or_later: forall log2_nbytes r v sH sL sL' h2d d2h, |
There was a problem hiding this comment.
Similar issue as with state_machine_read_to_device_read_or_later.
| @@ -186,7 +187,11 @@ Section WithParameters. | |||
| device.run1 s i := Semantics.step incr s (i, tt); | |||
| device.addr_range_start := INCR_BASE_ADDR; | |||
| device.addr_range_pastend := INCR_END_ADDR; | |||
| device.maxRespDelay := 1; | |||
| device.maxRespDelay '((istate, (val, tl_d2h)), tlul_state) h2d := | |||
| (* if the value register was requested, and we're in state Busy1, it will take one | |||
There was a problem hiding this comment.
I'm not sure if this is relevant, but the SW semantics allows reading the value register only when in the DONE state.
|
I added one more file, |
I'm trying to work top-down from
device_implements_state_machinetowards Cava Hmac, and the first too-high-level item that I encountered was that the read/write steps indevice_implements_state_machinetalk about several device steps at once (because they're usingrunUntilResp).I wrote an alternative
device_implements_state_machinethat only usesrun1, but notrunUntilResp.That should bring the interface closer to the structure of Cava proofs, hopefully.
Unfortunately, the proofs for
CavaIncrementDevice.vbreak badly, and I haven't fixed them yet, so this is still a draft, but I'm posting it here because I'd be interested to know what @fshaked thinks about the changes I made inMMIOToCava.v, and whether they could simplify what you're working on?