Internal yosys errors when running riscv-formal tests

[albert-magyar]

While attempting to add support for a RV32IC core, I have encountered Yosys error messages while attempting to run tests.

Unfortunately, I cannot include the code to reproduce, so I was wondering if you might be able to shed some light on the meaning of the error (which is the first error with no preceding errors or warnings).

make: *** [insn_addi_ch0/PASS] Error 3
SBY [pc_bwd_ch0] smt2: ERROR: Assert `sig.size() == 1 && sig.chunks().size() == 1' failed in ./kernel/rtlil.h:1301.
SBY [pc_bwd_ch0] smt2: finished (returncode=1)
SBY [pc_bwd_ch0] smt2: job failed. ERROR.
SBY [pc_bwd_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:15 (15)
SBY [pc_bwd_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:15 (15)
SBY [pc_bwd_ch0] DONE (ERROR, rc=3)

[cliffordwolf]

Obviously that should not happen.. but without code to reproduce it there is nothing I can do about the issue. You can try narrow it down to a small example that doesn't contain any secret stuff and post that code.

[cliffordwolf]

There should be a line smt2: starting process ... in the output that tells you the command that failed. Maybe you can at least generate a stack trace for the assertion?

The input file for that command is pc_bwd_ch0/model/design.il. You can try generating a minimal test case by removing cell..endcell blocks from that file and simply re-running yosys design_smt2.ys in pc_bwd_ch0/model/. That might be simpler than trying to strip the original Verilog code to a minimal test case.

I am currently in Palo Alto. Your github profile says you are at UCB. I can take an Uber/Lyft to UCB if you'll let me troubleshoot this issue with your code on-site on your hardware..

[albert-magyar]

That is an amazing offer, but unfortunately I am using riscv-formal for an internship, so I'll just have to narrow it down to a smaller example. Thanks for the tips on directly using the .il file, I will try that.

One difference I have noticed in other wrappers is the liberal use of the keep attribute. Is this merely to simplify debugging, or is it necessary in some capacity?

[cliffordwolf]

One difference I have noticed in other wrappers is the liberal use of the keep attribute. Is this merely to simplify debugging, or is it necessary in some capacity?

It is just for debugging to make sure that those wires end up in VCD traces (i.e. are not optimized away).