[rvfi] rvfi_pc_wdata doesn't consider mret/dret

[georgerennie]

Observed Behavior

The RISC-V formal interface specifies rvfi_pc_wdata to contain the address of the next instruction. RISC-V Formal's pc_fwd check verifies that for an arbitrary instruction the next instruction's address stored in rvfi_pc_rdata is the same (unless a trap occurs). This fails for ibex when an mret or dret instruction is encountered as the rvfi_pc_wdata logic currently does not consider pc changes due to them.

The screenshot and fst below show the execution of an mret instruction (shown as an unknown instruction as the surfer waveform decoder doesn't yet support them). You can see that for the mret rvfi_pc_wdata is 0x001003CA, even though the next instruction is at address 0x00000000 (as seen in rvfi_pc_rdata). This behaviour also occurs with dret.

sim.tar.gz

Expected Behavior

This should instead have a value consistent with the address of the next instruction (that comes from mepc), as shown below

Steps to reproduce the issue

https://github.com/georgerennie/ibex/tree/george/mret_pc_wdata contains a sample test program that just runs an mret instruction in main. The waveform from above can be reproduced with

fusesoc --cores-root=. run --target=sim --setup --build lowrisc:ibex:ibex_simple_system $(util/ibex_config.py small fusesoc_opts) --RVFI
make -C examples/sw/simple_system/mret_test
./build/lowrisc_ibex_ibex_simple_system_0/sim-verilator/Vibex_simple_system --meminit=ram,examples/sw/simple_system/mret_test/mret_test.elf -t

I was able to reproduce this behaviour with all of the supported configurations (and didn't check any others).

My Environment

I found this whilst trying to get the risc-v formal environment working again, but reproduced it with simulation

EDA tool and version:
Verilator 5.030 2024-10-27

Operating system:
Manjaro 6.6.63-1-MANJARO

Version of the Ibex source code:
667fd20

Potential patch

This patch potentially misses cases that should be considered, but with it applied I no longer see this issue testing the above setup in basic simulation for all the supported configurations and with risc-v formal for the small configuration although without debug input (I don't yet have other configs running in risc-v formal).

diff --git a/rtl/ibex_core.sv b/rtl/ibex_core.sv
index 807e3151..b2a7376a 100644
--- a/rtl/ibex_core.sv
+++ b/rtl/ibex_core.sv
@@ -1597,7 +1597,10 @@ module ibex_core import ibex_pkg::*; #(
             rvfi_stage_rs2_addr[i]             <= rvfi_rs2_addr_d;
             rvfi_stage_rs3_addr[i]             <= rvfi_rs3_addr_d;
             rvfi_stage_pc_rdata[i]             <= pc_id;
-            rvfi_stage_pc_wdata[i]             <= pc_set ? branch_target_ex : pc_if;
+            rvfi_stage_pc_wdata[i]             <= id_stage_i.mret_insn_dec ? csr_mepc :
+                                                  id_stage_i.dret_insn_dec ? csr_depc :
+                                                  pc_set                   ? {branch_target_ex, 1'b0} :
+                                                                             pc_if;
             rvfi_stage_mem_rmask[i]            <= rvfi_mem_mask_int;
             rvfi_stage_mem_wmask[i]            <= data_we_o ? rvfi_mem_mask_int : 4'b0000;
             rvfi_stage_rs1_rdata[i]            <= rvfi_rs1_data_d;