Cava1 semantics was a Moore machine, but Cava2 is Mealy?

[fshaked]

Here are two circuits, test1 written in cava1, and test2 written in cava2, which I thought should behave the same, but simulate gives different traces (included in the file).

[blaxill]

FWIW this is the intended semantics for cava2, using moore machines for control logic would be difficult.

[fshaked]

Ok, I didn't know this was intentional. Any point for leaving this issue open?

[jadephilipoom]

I'm not sure I understand why the semantics are different, and I don't remember discussing a change. @blaxill , would you mind elaborating a bit?

[samuelgruetter]

Also, is it the case that every Cava1 circuit has an equivalent Cava2 circuit? For instance, is it possible to implement a cava1-style Loop combinator using existing cava2 operators? (When I tried to do that, the only solution I found duplicates the state)

[blaxill]

They are equivalent but the recent version doesn't require a binder for "output" to already be present. Technically cava1 is also a mealy machine as its output is dependent on the current state and current input (same cycle).

The reason for the observed difference is the first version stores input to the register before responding where as the second stores it to a register but also uses the value immediately. To be specific they both have a mealy state transition function T and output function G, T is equivalent in both but G is not. This is because the second formulation G is somewhat pushed outside the loop.

Sam is right that this can cause state to be duplicated, but in these cases since the duplicated state is not used as a register but just to output a value, it should be possible to trim this register (e.g. downstream tools should definitely see it as only used same cycle and never as a true register).

[blaxill]

I'm happy to change this (how "G" is represented), the choice is mostly syntactical- apart from the false state duplication.

[jadephilipoom]

This is clearer to me now, thanks! I don't see a strong reason to change the setup to match cava1, personally, if it hasn't been a problem so far.

[samuelgruetter]

it should be possible to trim this register (e.g. downstream tools should definitely see it as only used same cycle and never as a true register).

But what about Coq itself? Shouldn't it also be able to trim or deduplicate or not even duplicate it in the first place? For instance, in order to prove that a Cava device implements a state machine (against which we proved bedrock2 functions), with Cava1 we need to give a relation of type state_machine_state -> circuit_state cava_device -> Prop, and I think proofs would become quite cumbersome if all the Cava state was duplicated.

if it hasn't been a problem so far.

It already was a problem when @fshaked tried to translate the IncrementWait example from Cava1 to Cava2...

[blaxill]

if all the Cava state was duplicated.

I didn't need to duplicate any state for the more realistic SHA256, which includes serialisation, padding, etc., so I don't expect to need to duplicate large amounts of state. Any false-duplicated state will also be equivalent to last cycle + this cycle values which are not the same and can be thought of a different way of keeping the values around in scope.

It already was a problem when @fshaked tried to translate the IncrementWait example from Cava1 to Cava2...

Can you show me the more specific issue in IncrementWait? The example in this issue could be just written with a delay rather than loop.

[samuelgruetter]

The example in this issue could be just written with a delay rather than loop.

Aah true, yes this example is so simple that it doesn't need a loop.

I don't have any intuition on how common false-duplicated state will be, so I trust the judgment of those who have more experience with hardware than me here :)

[fshaked]

Can you show me the more specific issue in IncrementWait? The example in this issue could be just written with a delay rather than loop.

cava1
cava2
Each of those has an example sample_trace a few lines below the definition. In the third cycle we check the status of the device, in cava1 the busy bit is high, in cava2 the done bit is high.