Value of rs1 during CSR*I instructions

[olofk]

I'm a bit confused whether this is an issue with riscv-formal or if I'm just holding it wrong. The issue I see is that the reg test fails because of a mismatch for rvfi_rs1_rdata. I think the problem is that the rs1 data is read from the wrong register. It's an optimization, which is fine because we never care about the data in rs1 dugin CSR*I instruction. But it seems like riscv-formal needs to have correct rs1 data here. Is that the intention, or can we relax the requirement in this case?

[towoe]

From my understanding the register data must reflect the actual content only if the register address is non-zero. So if the register is not used maybe there is a way to use some status to discover that and use this when forwarding the registers?

[olofk]

@towoe Good idea. It seems like setting rvfi_rs1_addr to zero in these cases work. Still fails though, so keeping open for a bit more until I got it figured out