Evaluation for arrow netlist layer

[jadephilipoom]

Based on previous conversation with @blaxill, we need something like the monad combinational for the arrow-based pipeline. This doesn't have to be performant because it doesn't need to ever get evaluated. It just has to exist so that we can prove that build_netlist is correct, since "correctness" for `build_netlist" means "evaluating in the arrow representation = evaluating in the netlist representation", and we need some way to express the right-hand-side. Importantly, it will be part of the trusted code base (unless/until we do #142 and make another layer below it), so it needs to be as simple and obvious as possible.

[blaxill]

The result of build_netlist can be run through makeNetlist to get a CavaState (which is shared with the Monads modules). Currently there is no simulation for CavaState, but I think writing that is what is needed. If we had a function to for combinational execution for CavaState, if the state came from arrows built with build_netlist it should be possible to prove that the execution was equal to combinational. Is that along the lines you were thinking?

[jadephilipoom]

I'm a bit confused about what CavaState is exactly -- your use of the words "simulate" and "execution" suggests that it's a representation of a circuit, full stop, not a temporary state?

Running with that assumption, this would mean that essentially, the last translation pass is build_netlist and then makeNetlist, and the lowest-level representation that we connect to the proofs is CavaState?

[blaxill]

Yeah CavaState is our lowest level representation which we generate (in Haskell) systemverilog files from, defined here:

https://github.com/project-oak/oak-hardware/blob/d01c528db13be08411e5513f76a1112eb4ba86b6/cava/cava/Cava/Netlist.v#L175-L185

For arrows, this is created through a state monad in CircuitLowering.v but the final step is in Netlist.v which executes the state monad and I think does some house keeping such as wiring up input/output labels. The representation is a list of Instances which are referred to by a N index.

[blaxill]

To clarify

we need something like the monad combinational for the arrow-based pipeline.

I see the correspondence as, monad CavaBool/combinational is to monad CavaNet, as arrow combinational_evaluation is to arrow build_netlist. That is, both monad combinational and arrow combinational_evaluation evaluate a combinational circuit in Coq. Both monad CavaNet and arrow build_netlist return a state CavaState.

The CavaState type that is constructed via state CavaState is what is used to generate a systemverilog file. The CavaState captures a netlist of components and could be simulated, but currently there is no functionality to do that. The systemverilog generation is also split across some Coq components and some Haskell components.

[jadephilipoom]

Ah, okay, I think I had misunderstood the structure here a little bit. In that case, we should be all good.