Vectors and name collisions about koika HOT 2 CLOSED

Thanks a lot for the report. I will expand on the following when I have time (probably next week, if that's OK).

• On DerivingShow: It could/should be made smarter to avoid collisions; in the meantime it's the user's job to provide custom names or avoid collisions in naming. Using $ would lead to less readable names in C++, so I'm not too sure about that.

• On vectors: The way reg_t works makes the semantics a lot simpler (no need to reason about finite sets of strings). Kôika lets you define family of vectors, and in your example they indeed don't all have the same size.

• On verilog names: we should do proper encoding of names like it's done in C++ (where we need tricks to avoid __, for example).

from koika.

As promised, some details:

In practice, this problem is easy to deal with and in fact the solution is always some register renamings away.

I think that's key. I'd rather not invest too much in generating complicated names, since renaming makes the generated nicer too. We could try to issue a warning in case of name collisions, though. And we should definitely check for too-long verilog names.

The context of this question is that I am looking for a way to generate Verilog through Kôika in such a way as to get BRAM blocks to be used through inference when using vectors past a certain size.

That's a nice goal, though I think it's a bit hard with the current Kôika set-up. The issue is basically that in Kôika right now everything needs to be reversible, and writing to a BRAM isn't really, so you need to make sure that you write to the corresponding array only from a rule that cannot fail. Without doing guard lifting or similar tricks, you find yourself playing the game that the memory bus rule plays in the RV core. The general solution would be to have a clean notion of modules with a request/response interface, and @threonorm is working on that.

This does not correspond to a vector in the traditional sense and it would in particular not be suitable for BRAM storage. Is this behavior desired or just a natural consequence of the way registers are managed?

It's desired; for a bram-style device, you'd probably want to use array_t instead — but for reasons of trust we actually compile arrays away when lowering to Verilog (it wasn't always like that; we used to produce arrays in the generated Verilog, but we removed them after a while). Reintroducing types at the RTL level could be a good way to start tackling this problem; it would also make it possible to introduce a bram type. But it would be quite a bit of work.

am I missing situations where a full blown inductive type is useful?

You get very nice compositionality properties from using an inductive; in particular, you can nicely isolate the type of each submodules without having to deal with strings (that is precisely the kind of aliasing problems that pop up when using show), and you can trivially define environments based on FiniteType instances.

from koika.