rvfi_reg_check is possibly broken (picorv32 also fails the assertion)

[silabs-robin]

It seems the checker is wrong as both picorv32 and cv32e40x get failing assertions and the traces look weird.
Otherwise, I might be wrong and have misunderstood something here.
If anyone else currently see reg_check working fine then please let me know.

Brief:
Register checks should execute (at least) 2 instructions, then check that the last one reads correctly that which the first one wrote.
What I observe is that the register read is arbitrary (undriven) and does not match the register read.
Example: Write rd_wdata='hABCD to rd_addr=1, and then CEX because a read from rs1_addr=2 (note: different than rd) does not have matching data rs1_rdata != 'hABCD.

Evidence 1

picorv32 see failure when running the reg check.

Fresh build/install of yosys/symbiyosys/boolector from:
https://symbiyosys.readthedocs.io/en/latest/install.html
Followed the README in cores/picorv32 to wget the source and launch checks.
Failure reported in "reg" checks.
NB! It was not able to parse by default, so I changed the const rand reg macro to just reg. (this was not changed for cv32e40x using a different formal tool).

"logfile.txt" line 63:

SBY 15:21:37 [reg_ch0] engine_0: ##   0:00:13  Assert failed in rvfi_testbench: rvfi_testbench.sv:39.17-57.3|rvfi_reg_check.sv:43.71-44.59

"src/rvfi_reg_check.sv" line 44:

                                        assert(register_shadow == rvfi_rs2_rdata[`RISCV_FORMAL_CHANNEL_IDX*`RISCV_FORMAL_XLEN +: `RISCV_FORMAL_XLEN]);

The rs2 check fails.

This might also be a bug in picorv32, or it might be a bug in my methodology.

Evidence 2

cv32e40x see failure when running the reg check, and the checker seems to do an arbitrary comparison.

A similar problem is observed here. There is a CEX because the register_shadow was set for a different register than the one being read later (rs1).

It is also possible to get a trace where only 1 instruction retires, but that seems counter to the purpose of the test. I would think assumes should be in place to not permit this.

Thoughts

I don't fully understand the code,
but it seems that nothing is driving register_index and that it should maybe be stored similar to how register_shadow is stored.

Extra info - Possibly a similar bug in the PC checks

There is a similar issue in pc_fwd and pc_bwd where the expected PC can be stored once, then one or more instructions may follow, and finally the check happens but the expected PC was not updated by the intermediate instructions so the comparison is done against an outdated expectation and gets an error

[dvc94ch]

It was not able to parse by default, so I changed the const rand reg macro to just reg.

Checks passed for me today. I changed const rand reg to rand const reg.

[silabs-robin]

It was not able to parse by default, so I changed the const rand reg macro to just reg.

Checks passed for me today. I changed const rand reg to rand const reg.

Hi @dvc94ch. Thanks for doing a test of those proofs. I am quite busy at the moment but I will certainly try out the same change as you show here and continue my debugging from there.

[silabs-robin]

Hi. I am back again.

Checks passed for me today. I changed const rand reg to rand const reg.

Indeed this works. I just tried it on picorv32 myself. That seems to resolve the part about picorv32.
However, from the LRM I can't really see that "rand" is allowed in this context at all (the formal tool I use agrees). Is it then a bug to use "rand" here, or even a bug of yosys to accept "rand", or did I overlook something?
(btw, does it usually take >2h to run the reg test on picorv32? Other tests are much faster.)

But to the main question about whether the "reg" check is ok or not.
I think I found the problem.
In the traces above, you can see insn_order and register_index changing values.
AFAICT, the checker intends these signals to be random constants?
I have fixed this locally with assumes, but I also created this PR #54 to solve it in riscv_formal as well.