nmigen
nmigen copied to clipboard
m-labs
Find solution to translate values to strings for Symbiyosys vcd files
When dumping the result of covers and counterexamples, Symbiyosys writes .vcd files. However, any signals that were enums or FSM states are no longer strings, but just plain old binary.
In gtkwave, it's possible to select a signal and then Edit > Data Format > Translate Filter File. You can then select a filter file, which is just a map of original value to string value:
00 ZERO
01 FIRST
02 TOOOO
The configuration can also be saved in a .gtkw file. However, this only affects displayed signals. If you delete the signal and display it again, it is not translated. This is horrible.
Proposal:
Better might be to just go into the vcd file and edit the values. Although it would require an extra step, I wouldn't object to something like this:
python3 <toplevel.py> stringify <input_vcd> -o <output_vcd>
This would parse the input vcd file, replace numeric values with string values for enum and fsm states, and output the result.
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: https://github.com/YosysHQ/yosys/issues/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.
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 https://github.com/YosysHQ/yosys/issues/1594. Hopefully this will start a discussion about the feature, and whether it's even feasible in yosys.