CSR semantics ============= 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. M-mode CSRs ----------- Machine Information Registers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ mvendorid, marchid, mimpid, mhartid, mconfigptr ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ These CSRs are mandatory and expected to be constant, but may be all 0. Machine Trap Setup ~~~~~~~~~~~~~~~~~~ mstatus ^^^^^^^ 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. misa ^^^^ Can be read-only 0, but existence is mandatory. Reserved bits must be 0 regardless of writes. medeleg, mideleg ^^^^^^^^^^^^^^^^ Only exist if S mode is supported. mie, mtvec ^^^^^^^^^^ Mandatory. mcounteren ^^^^^^^^^^ 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. Machine Trap Handling ~~~~~~~~~~~~~~~~~~~~~ mscratch ^^^^^^^^ Nothing special for this CSR. mepc ^^^^ 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. mcause, mtval, mip ^^^^^^^^^^^^^^^^^^ Nothing special for these CSRs. Machine Protection and Translation ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TBD Machine Counter/Timers ~~~~~~~~~~~~~~~~~~~~~~ mcycle, minstret ^^^^^^^^^^^^^^^^ 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``. mhpmcounter, mhpmevent ^^^^^^^^^^^^^^^^^^^^^^ Machine performance-monitoring counters are currently not supported by riscv-formal. CSR 0xFFF ~~~~~~~~~ This address is used as a catch-all to mean no address and thus is not able to be tested normally. Debug-Mode CSRs --------------- TBD U-Mode CSRs ----------- TBD S-Mode CSRs ----------- TBD