Mealy vs other approaches to sequential logic?

[christiaanb]

I see that you're modeling sequential logic using Mealy machines so far. Is that because that's easier to implement as far as Lean => Verilog conversion goes? Or is that because it's easier to write proofs over Mealy machines vs e.g. guarded atomic transactions as you have them in BlueSpec?

[christiaanb]

ps Happy to jump on a call to discuss things, my email address can be found in my github profile.