Mismatch between documentation and checks

[acw1251]

I have been playing with riscv-formal for checking one of our small processors, and I came across a few issues where the documentation does not appear to match what the checks are actually doing. Our small processor supports a bit less than the bare minimum of RV32I (It's actually a bare minimal RV32E processor that I temporarily increased the number of registers to 32 registers just for testing with riscv-formal - as a result, its basically just an RV32I processor without counters). It supports interrupts and exceptions, but for the purposes of these tests, I have hardwired the interrupt inputs to 0. I'm currently running the same checks as picorv except I changed the isa to rv32i and I'm skipping liveness for now.

1. rvfi_intr - According to rvfi.md: "rvfi_intr must be set for the first instruction that is part of a trap handler, i.e. an instruction that has a rvfi_pc_rdata that does not match the rvfi_pc_wdata of the previous instruction.". Looking at the checks, it seems like rvfi_intr is ignored. My implementation sets rvfi_pc_wdata to the start of the trap handler for each instruction that causes a fault and it passes all the checks that are done for picorv (except liveness - I'm skipping it for now).

2. rvfi_rs1_addr and rvfi_rs2_addr - According to rvfi.md: "For an instruction that reads no rs1/rs2 register, this output can have an arbitrary value." Our processor always assumes rs1 is insn[19:15] and rs2 is insn[24:20]. I tried keeping those values for rvfi_rs1_addr and rvfi_rs2_addr, but I failed checks for addi, lui, and other similar instructions that don't use rs1 and/or rs2. I ended up changing rvfi_rsX_addr and rvfi_rsX_rdata to 0 if the instruction doesn't use rsX, and with that change I passed all the tests. This is consistent with what I saw when looking at the instruction check system verilog.

Anyways, I'm really enjoying using with riscv-formal. Thanks!

[cliffordwolf]

Looking at the checks, it seems like rvfi_intr is ignored.

Yeah, that's because rocket doesn't really set it yet either and PicoRV32 is only verified in non-interrupt mode (because it's using a non-standard interrupt mechanism that pre-dates the priv spec).

This should be added to rvfi_pc_fwd_check and rvfi_pc_bwd_check. (Both checks could need some love in general.) I will fix this soon-ish.

My implementation sets rvfi_pc_wdata to the start of the trap handler for each instruction that causes a fault

That also works.

I tried keeping those values for rvfi_rs1_addr and rvfi_rs2_addr, but I failed checks for addi, lui, and other similar instructions

That's a bug in rvfi_insn_check.sv. What you are doing should work (as long as the value on rvfi_rs1_rdata/rvfi_rs2_rdata correctly represents the machine state). I will fix this some time this week.

[acw1251]

Thanks for the quick reply. As I said, I have all the checks passing without any changes to riscv-formal, so it's not urgent.

[cliffordwolf]

The rs1/rs2 issue should be fixed now. (The intr issue is still open.)

[Wren6991]

I have also encountered this, with the pc_fwd check. I update pc_wdata for instructions which retire as an interrupt is asserted, as suggested above. The solver immediately finds a loophole in this: it asserts an interrupt in a pipeline bubble between two instructions, which it creates by starving instruction fetch briefly.

The earlier instruction has already retired, so its pc_wdata points to the sequentially-next instruction. However, the next instruction to actually retire is the first instruction of the interrupt handler, which is nonsequential with the previous instruction. This fails the check.

I am trying to come up with a workaround for this, but all I can think of at the moment is "retiring" a dummy nop in the interrupted bubble to link up the pre-interrupt pc_wdata with the in-interrupt pc_rdata, which is a bit of a hack.

I am also playing with hacking my local copy of pc_fwd_ch0 to not check pc_rdata on cycles where rvfi_intr is asserted, but then I need additional properties to check that e.g. rvfi_intr is not just tied high.

As an aside, moving to the latest version of riscv-formal (I was around 40 commits behind) has found a lot of nasty bugs in my processor, so thank you for all the hard work there :)

[jerralph]

Had posted a message here about rs2_addr error getting flagged for ADDI but was wrong. I thought it was complaining about ADDI rs2_addr but it was actually rs1_addr. Nothing to see here :)