Register checks do not seem to be checking anything

[JobNoorman]

While trying to figure out why bugs deliberately added to the register file or bypass logic of my CPU where not caught by the register checks, I noticed that the register checks don't seem to be checking anything.

More specifically, I tried the following (on picorv32):

• Forcing rvfi_rsx_rdata to fixed values;
• Forcing rvfi_rd_wdata to a fixed value;
• Adding assert(0) on line 40 of rvfi_reg_check.sv.

In all cases, the register checks would pass just fine.

The assert(0) was added inside the if (check) test and when added instead in the else branch of that test, the check did fail. It seems therefore that the check input never becomes true which causes all checks to be disabled.

[cliffordwolf]

Wow. Thanks for bringing this to my attention. We've optimized the depths of checks for performance and for reg_check we apparently made it one cycle shorter than we should have. a4b1484 now makes sure the fail happens in the cycle we expect it to.

[JobNoorman]

Thanks for the quick fix!

I noticed that the register checks take a very long time to complete now (about one hour for picorv32). Is this expected?

[cliffordwolf]

Thanks for the quick fix!

Thanks for reporting the issue. We'll set up CI, with falsification via test bugs, for the public parts of riscv-formal to avoid issues like this in the future.

about one hour for picorv32

You have a fast machine. :) For me it's almost 4 hours on the could instance I usually run riscv-formal on.

I'll reduce the default bounds of the checks to speed it up a little. After all, the PicoRV32 core is meant as an example that's easy to run and play with. So I guess quick runtime is far more valuable here than deep bounds.