Even if reading and altering VCD files was in scope for nMigen (which I don't think it is), the pyvcd library we are using does not support reading VCD files. I believe that the appropriate solution for this is altering SymbiYosys such that it would support symbolic mappings, one way or another.

Do the symbolic names carry over from Python to the IL that Symbiyosys uses?

Right now that only happens for the nmigen.decoding attribute, which is set on switch cases. But it would be quite easy to add a way to serialize a dict of every possible decoder value into an attribute on a signal. The reason it's not done right now is that e.g. a 16-bit signal would result in a very large dict, and a 32-bit signal would result in unparsable RTLIL. Whereas in case of a switch case it always results in reasonably sized RTLIL, which is not much larger than the one before the attribute is added.

A proper solution for this issue is quite challenging. Your suggestion of post-processing VCD files is actually not that bad, but there is the very real problem that we can't easily implement it.

I've looked closer at what SymbiYosys is doing. I believe there is a solution that is fairly elegant, would benefit everyone in FOSS FPGA community, and would solve 90% of the problem here. That is:

• Yosys should support SystemVerilog enumerations, probably by storing the name-to-value map in an attribute applied to every reg or wire of the enum type.
• yosys-smtbmc should use this attribute when writing VCD files. (Or better, write FST files, which natively support enums.)
• nMigen should emit this attribute.

Would you be interested in tackling this? I could provide guidance and/or review of Yosys patches.

I could try. But I wouldn't even start unless I knew such a feature would be accepted into yosys.

I'm confident it would. SystemVerilog features in general are something Yosys is sorely lacking.

It seems like this has been tried several times already: YosysHQ/yosys#248 so I'm hesitant to spend a lot of time on it.

@RobertBaruch You could try a Yosys plugin?

FYI -- Google also recently released https://github.com/google/verible which is a SystemVerilog parser, linter and code formatter. It does a pretty good job at https://github.com/SymbiFlow/sv-tests but would still need quite a bit of work to hook into Yosys for synthesis. @hzeller is currently looking at what is needed to make that happen.

@RobertBaruch Looks like we can skip doing anything about SystemVerilog then, and only add an attribute. What do you think?

Perhaps a good starting place would be kernel/rtlil.h. Add a struct to hold the value<->string map (is RTLIL::IdString useful?) for an enum, and make that a top-level entity, or a module-level entity. Add nullable pointers to RTLIL::Wire and then make sure this can be written from and read to text.

I've asked Clifford what would be the best approach here, your suggestion vs an attribute.

@RobertBaruch As I expected Clifford thinks this should be done using just attributes.

@RobertBaruch Friendly ping--have you looked into implementing this?

I have some time next week that I can devote to working on this.

Excellent, thanks!

I did find where the traces for cover mode are written (backends/smt2/smtio.py), and where the actual value is written (bv2bin), but that value appears to come from another process, No clue where that is, or whether those values are always assumed to be integers. Thoughts?

(and really, considering Clifford wrote yosys, wouldn't he be in the best position to just solve this in, like, a few minutes?)

I've written up a proposal at YosysHQ/yosys#1594. Hopefully this will start a discussion about the feature, and whether it's even feasible in yosys.

Thanks.