Formalising the privileged specification

[Columbus240]

I started working on a formalisation of the privileged specification, mostly the CSRs. The CSR branch on my repo contains the current code. Some splitting and reordering of the commits in the branch is necessary, but not important right now. I’d like to describe and discuss some design decisions and problems.

• I haven’t setup automatic conversion from riscv-semantics, but I used a similar code structure. I did this because riscv-semantics doesn’t formalise many parts of the spec. For example it always assumes MXLEN=SXLEN=UXLEN and always assumes that the MXL field is implemented. And I didn’t want to configure the conversion and deal with conversion errors.
• The interface to the CSRs provided by a RiscvMachine has to have CSRField granularity, because some fields appear in multiple CSRs and are required to have the same value in all ocurrences. (riscv-semantics does the same) Also properties like WARL and WPRI are defined on this granularity in the spec.
• riscv-semantics doesn’t formalise the fields with WPRI. I chose to do so, so that an instance of RiscvMachine can implement custom extensions to the CSRs and the values get forwarded to the programs. Also, we can now capture, whether a program actually treats the WPRI fields the way it should (preserving and ignoring).
• The privileged spec describes itself as one possible specification of the privileged architecture ontop of the unprivileged ISA. Both my code and riscv-semantics don’t reflect this. It would add another layer of abstraction if we were to implement this, and because there are currently no competing privileged specifications that I know of, it would be unneccessary.
• The definition of CSRs and CSRFields were put into separate files (in my code and in riscv-semantics) so that there would be less name collisions. Because there are registers with the same name as a field, for example mscratch.
• I didn’t write down the CSRs for the debugging spec and the hypervisor stuff, because they are both still drafts.

Looking ahead

• The *XLEN of a hart may change at runtime and may differ from eachother. The current *XLEN can be determined by reading MXL, SXL and UXL. Except, if the misa register is not implemented (hardwired to zero). Then we have to use some “non-standard mechanism”.
• The Extensions field of the misa CSR may also change at runtime. This means that which instructions are valid depends on the value of this field. So changes to decoding and execution might be necessary.
• The privileged spec allows the misa CSR to be hardwired to zero. In this case MXLEN has a fixed value, but the spec says nothing about enabling or disabling extensions at runtime. To allow misa to be zero, additional operations on RiscvMachine would be necessary to get the equivalent of reading MXL and Extensions. This might create a little headache here and there, but it would represent the spec faithfully.
• How can the current privilege level be determined? riscv-semantics lets the RiscvMachine keep track of it using additional getter/setter operations. I’m not sure whether the current privilege level can be read from a CSR. I think I can solve this myself.