Dynamic pipeline NoC

[sertel]

Restructure and design the routers in order to be able to construct a NoC that is dynamic in the horizontal dimension but not in the vertical dimension.
For sake of simplicity, please start with a stateful NoC where each channel is represented by a single register.

Steps:

• Create a static pipeline.
• Integrate MetaCoq via Nix as a new input to the flake.
• Use MetaCoq to create the inductive data types for the registers.
• Create functions for the routers that still need the reg_t type as an input. Use a Module Type to get this done.
• Do the composition of a NoC dynamically.

[garvitchhabra-7]

The pipeline composition is completely dynamic now.

[garvitchhabra-7]

MetaCoq runs into some issues using Parameter when we try to generate Coq code from syntax, I'm checking if I can find a way to fix this.

Not Supported raised at unquote_list

[sertel]

So you mean the Parameter command?

[garvitchhabra-7]

Yes if I define nocsize using Parameter, the MetaCoq commands (both the command which is used to build inductive types and the command that is used to build definitions) error out, they work fine when using Definition.

[sertel]

Ah, I see.
Thanks for clarifying!
I'm looking forward to your ideas.