For the most part the CSR values output via RVFI match exactly the CSR values observable via the ISA. But there are a few minor differences that are outlined here.
Most importantly, for RV64 processors in RV32 mode, the values output via
RVFI are still following RV64 CSR encondings, including some of the information
that is not available through the RV32 ISA, such as SXL and UXL in mstatus.
Counters are always output as singe 64-bit wide CSRs even on RV32 targets.
These CSRs are mandatory and expected to be constant, but may be all 0.
Mandatory. (Reminder: RV64 processors in RV32 mode are expected to output the RV64 format.) May be all 0, reserved bits must be 0 regardless of writes.
Can be read-only 0, but existence is mandatory. Reserved bits must be 0 regardless of writes.
Only exist if S mode is supported.
Mandatory.
Currently only the IR and CY bits of mcounteren are supported by
riscv-formal. The other bits are ignored.
mcounteren must only exist if U mode is supported.
Nothing special for this CSR.
The version of mepc observable through the ISA masks mepc[1] on CSR reads
when the processor is in a mode that does not supprt 16-bit instruction
alignment. However, writes to that bit shall still modify the underlying
architectural state.
In riscv-formal semantics the mepc value output via RVFI must be the actual
architectural state with mepc[1] not masked.
Nothing special for these CSRs.
TBD
Always 64-bit wide, even on pure RV32 processors (no mcycleh/minstreth).
Incrementing those counters should happen "between instructions", this means
for example that an instruction that isn't a CSR write to mcycle should
always have rvfi_csr_mcycle_rdata == rvfi_csr_mcycle_wdata.
Machine performance-monitoring counters are currently not supported by riscv-formal.
This address is used as a catch-all to mean no address and thus is not able to be tested normally.
TBD
TBD
TBD