[rvfi] rvfi_pc_wdata doesn't consider mret/dret
Nobody has claimed this yet.
- Dominant language
- SystemVerilog
- Stars
- 2.1k
- Forks
- 810
- Avg merge
- 5d 23h
- Merged PRs (30d)
- 9
Description
## 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](https://github.com/user-attachments/files/18098567/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
```bash
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:**
667fd20d2ede51caececccbcbda3652074424ce2
## 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
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;
```
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start in rtl/ibex_core.sv at the rvfi_stage_pc_wdata assignment and compare its handling of ordinary branches with mret and dret. Reproduce the issue using the commands in the report and the mret_test program. Done means rvfi_pc_wdata matches the next instruction address for both return instructions, with the simulation and relevant RISC-V Formal check passing.
Written by the indexing model from the issue text.
Assessment
- Domain
- embedded-iot, testing
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 45/100