Hello — first, thanks for Ibex. We've been using it as the real-core reference for some RVFI tooling precisely because it's clean, well documented, and easy to build, and it executed every test program we threw at it exactly right. This is a reporting issue rather than an execution one.
Summary
On any retirement whose instruction performs no memory access, Ibex reports rvfi_mem_rmask = 4'b1111, alongside an rvfi_mem_addr that is not a memory address and an rvfi_mem_rdata held over from an earlier load. The trace therefore makes a positive claim that four bytes were read from a given address, for instructions that issued no memory request.
Where it comes from
All line numbers against master as of 2026-08-20.
-
rtl/ibex_core.sv:1653 drives the read mask from the store flag alone:
rvfi_stage_mem_rmask[i] <= data_we_o ? 4'b0000 : rvfi_mem_mask_int;
Nothing here is conditioned on whether the instruction actually issued a memory request, so every non-store takes the rvfi_mem_mask_int branch.
-
rtl/ibex_core.sv:1792-1799 derives that mask from lsu_type alone:
unique case (lsu_type)
2'b00: rvfi_mem_mask_int = 4'b1111;
2'b01: rvfi_mem_mask_int = 4'b0011;
2'b10: rvfi_mem_mask_int = 4'b0001;
default: rvfi_mem_mask_int = 4'b0000;
endcase
-
rtl/ibex_decoder.sv:227 sets data_type_o = 2'b00 as the unconditional default in the decoder's default-assignment block, and only the load/store cases override it. So for every non-memory instruction, lsu_type is the word encoding and the mask is 4'b1111.
The two companion fields are stale rather than zeroed, which is what turns this from a cosmetic issue into a checkable one:
rtl/ibex_core.sv:1761-1769 sets rvfi_mem_addr_d = alu_adder_result_ex on the first ID cycle of every instruction, so on an addi the reported address is the ALU result.rtl/ibex_core.sv:1771-1778 holds rvfi_mem_rdata_d at its previous value unless lsu_resp_valid, so the reported data is whatever the last load returned.
Stores are correct — data_we_o gates rmask to zero and the write mask carries the real size.
Why this is a spec deviation
docs/source/rvfi.rst in riscv-formal:
For memory operations (rvfi_mem_rmask and/or rvfi_mem_wmask are non-zero), rvfi_mem_addr holds the accessed memory location.
rvfi_mem_rmask is a bitmask that specifies which bytes in rvfi_mem_rdata contain valid read data from rvfi_mem_addr.
A non-zero mask is what identifies a retirement as a memory operation, and it asserts that the named bytes of rvfi_mem_rdata are valid data from rvfi_mem_addr. On a non-memory instruction none of those three fields carries meaning, so the claim can't hold.
I want to be fair about the counter-argument, because there is one. checks/rvfi_insn_check.sv only asserts one direction — if (spec_mem_rmask[i]) assert(mem_rmask[i]); — and never the converse, and the CSR section of the spec explicitly permits activating more rmask bits than an instruction requires. So a superset mask is tolerated in general. The condition attached to that allowance is "as long as the reported bits correctly reflect the machine state," and that's the part that fails here: the address isn't a memory address and the data was never read from it.
It's reachable by riscv-formal's own check
checks/rvfi_dmem_check.sv picks an address and asserts, for any retirement reporting that address:
if (enable && rvfi_mem_rmask[channel_idx*`RISCV_FORMAL_XLEN/8 + i] && dmem_written[i])
assert(dmem_shadow[i*8 +: 8] == rvfi_mem_rdata[i*8 +: 8]);Since dmem_addr is rand_const, the solver is free to choose an address that a non-memory instruction's stale rvfi_mem_addr happens to alias. With rmask asserted and rvfi_mem_rdata holding an unrelated earlier value, that assertion has a counterexample. I haven't run the proof myself, so I'd treat that as a strong expectation rather than a result — but it does mean this is inside the scope of the existing checks rather than a matter of interpretation.
I'd note in the same breath that doc/03_reference/rvfi.rst already says Ibex "is not yet formally verified," and as far as I can tell dv/uvm only wires the RVFI signals into core_ibex_rvfi_if while the Spike co-simulation compares architectural state rather than RVFI reporting. So this looks like a gap that nothing currently exercises, not a regression.
Observed
Verilator 5.050, ibex_top at 3250d99482f1963891ef1cf19356eeaeeaa71d30, upstream small config plus +define+RVFI, running a 26-instruction RV32I program (arithmetic, word/byte/halfword load-store pairs, a taken forward beq, a backward bne loop, a trapping ecall). 20 of the 26 retirements report a non-zero rvfi_mem_rmask with no memory access; the 6 genuine accesses all report correctly. The RTL is unmodified and the testbench tie-offs are copied from examples/simple_system/.
Happy to share the program listing, the build recipe or the captured waveform if any of that is useful — just say which.
Possible fix
Deliberately vague on the sampling point, since you'll know better than I do where it belongs — but the shape seems to be qualifying the masks with the LSU request rather than with data_we_o alone. lsu_req is already in scope in ibex_core.sv:
rvfi_stage_mem_rmask[i] <= (lsu_req && !data_we_o) ? rvfi_mem_mask_int : 4'b0000;
rvfi_stage_mem_wmask[i] <= (lsu_req && data_we_o) ? rvfi_mem_mask_int : 4'b0000;
though it may be cleaner to capture the qualifier at instr_first_cycle_id alongside rvfi_mem_addr_d, so all three fields are sampled consistently. Zeroing rvfi_mem_addr and rvfi_mem_rdata when there's no access would also make traces easier to read, but that's taste rather than spec.
Found with the RVFI Commit Inspector in WaveCrux, which flags RVFI traces against the specification. Everything above is checkable from the RTL and the riscv-formal sources without it.
Hello — first, thanks for Ibex. We've been using it as the real-core reference for some RVFI tooling precisely because it's clean, well documented, and easy to build, and it executed every test program we threw at it exactly right. This is a reporting issue rather than an execution one.
Summary
On any retirement whose instruction performs no memory access, Ibex reports
rvfi_mem_rmask = 4'b1111, alongside anrvfi_mem_addrthat is not a memory address and anrvfi_mem_rdataheld over from an earlier load. The trace therefore makes a positive claim that four bytes were read from a given address, for instructions that issued no memory request.Where it comes from
All line numbers against
masteras of 2026-08-20.rtl/ibex_core.sv:1653drives the read mask from the store flag alone:Nothing here is conditioned on whether the instruction actually issued a memory request, so every non-store takes the
rvfi_mem_mask_intbranch.rtl/ibex_core.sv:1792-1799derives that mask fromlsu_typealone:rtl/ibex_decoder.sv:227setsdata_type_o = 2'b00as the unconditional default in the decoder's default-assignment block, and only the load/store cases override it. So for every non-memory instruction,lsu_typeis the word encoding and the mask is4'b1111.The two companion fields are stale rather than zeroed, which is what turns this from a cosmetic issue into a checkable one:
rtl/ibex_core.sv:1761-1769setsrvfi_mem_addr_d = alu_adder_result_exon the first ID cycle of every instruction, so on anaddithe reported address is the ALU result.rtl/ibex_core.sv:1771-1778holdsrvfi_mem_rdata_dat its previous value unlesslsu_resp_valid, so the reported data is whatever the last load returned.Stores are correct —
data_we_ogatesrmaskto zero and the write mask carries the real size.Why this is a spec deviation
docs/source/rvfi.rstin riscv-formal:A non-zero mask is what identifies a retirement as a memory operation, and it asserts that the named bytes of
rvfi_mem_rdataare valid data fromrvfi_mem_addr. On a non-memory instruction none of those three fields carries meaning, so the claim can't hold.I want to be fair about the counter-argument, because there is one.
checks/rvfi_insn_check.svonly asserts one direction —if (spec_mem_rmask[i]) assert(mem_rmask[i]);— and never the converse, and the CSR section of the spec explicitly permits activating morermaskbits than an instruction requires. So a superset mask is tolerated in general. The condition attached to that allowance is "as long as the reported bits correctly reflect the machine state," and that's the part that fails here: the address isn't a memory address and the data was never read from it.It's reachable by riscv-formal's own check
checks/rvfi_dmem_check.svpicks an address and asserts, for any retirement reporting that address:Since
dmem_addrisrand_const, the solver is free to choose an address that a non-memory instruction's stalervfi_mem_addrhappens to alias. Withrmaskasserted andrvfi_mem_rdataholding an unrelated earlier value, that assertion has a counterexample. I haven't run the proof myself, so I'd treat that as a strong expectation rather than a result — but it does mean this is inside the scope of the existing checks rather than a matter of interpretation.I'd note in the same breath that
doc/03_reference/rvfi.rstalready says Ibex "is not yet formally verified," and as far as I can telldv/uvmonly wires the RVFI signals intocore_ibex_rvfi_ifwhile the Spike co-simulation compares architectural state rather than RVFI reporting. So this looks like a gap that nothing currently exercises, not a regression.Observed
Verilator 5.050,
ibex_topat3250d99482f1963891ef1cf19356eeaeeaa71d30, upstreamsmallconfig plus+define+RVFI, running a 26-instruction RV32I program (arithmetic, word/byte/halfword load-store pairs, a taken forwardbeq, a backwardbneloop, a trappingecall). 20 of the 26 retirements report a non-zerorvfi_mem_rmaskwith no memory access; the 6 genuine accesses all report correctly. The RTL is unmodified and the testbench tie-offs are copied fromexamples/simple_system/.Happy to share the program listing, the build recipe or the captured waveform if any of that is useful — just say which.
Possible fix
Deliberately vague on the sampling point, since you'll know better than I do where it belongs — but the shape seems to be qualifying the masks with the LSU request rather than with
data_we_oalone.lsu_reqis already in scope inibex_core.sv:though it may be cleaner to capture the qualifier at
instr_first_cycle_idalongsidervfi_mem_addr_d, so all three fields are sampled consistently. Zeroingrvfi_mem_addrandrvfi_mem_rdatawhen there's no access would also make traces easier to read, but that's taste rather than spec.Found with the RVFI Commit Inspector in WaveCrux, which flags RVFI traces against the specification. Everything above is checkable from the RTL and the riscv-formal sources without it.