sail-riscv
sail-riscv copied to clipboard
riscv
Support for RV32E / RV64E
This model currently assumes there are 32 X registers i.e. the "embedded" ISA variants with only 16 registers are not supported.
The CHERIoT fork of this repo includes a bit of a hack to work around this. It raises a Sail exception for the invalid registers in the register access functions then catches it and raises a RISC-V reserved instruction in the instruction fetch loop. This almost works but has a major disadvantage that any side effects of instruction execution that happen before the illegal register access will still take effect! For example if rd of a csrrw is greater than 15 this won't be noticed until the CSR has already been written but it will then a reserved instruction exception!
We could fix this in the decode mapping, for example by adding a guard such as if validXReg(rd) && validXReg(rs1) && validXReg(rs2) on every mapping where validXReg would account for the embedded variants, however this would be very intrusive. I'm posting this to canvas opinion and see if anyone has any better ideas.
In the existing model, there are two types used to index into registers:
https://github.com/riscv/sail-riscv/blob/05b845c91d1c1db7b361fc8d06e815b54ca0b07a/model/riscv_types.sail#L36 https://github.com/riscv/sail-riscv/blob/05b845c91d1c1db7b361fc8d06e815b54ca0b07a/model/riscv_types.sail#L42
These are just bit vectors. The instruction AST just uses these directly
https://github.com/riscv/sail-riscv/blob/05b845c91d1c1db7b361fc8d06e815b54ca0b07a/model/riscv_insts_base.sail#L19
and the machine instruction codec mapping function just slice these directly out of the bits:
https://github.com/riscv/sail-riscv/blob/05b845c91d1c1db7b361fc8d06e815b54ca0b07a/model/riscv_insts_base.sail#L26-L27
By contrast, in some other architectural modeling that I've done with sail, I ended up defining an algebraic type for register selectors, gave that a dedicated encoding mapping function, made the instruction AST use the algebraic type, and had the codec mapping appeal to the register selector mapping function. We could rework the RISC-V sail model to use that approach, and if we did it right, models of RV-E could provide a different type and different codecs than models of RV-I.
This is probably more intrusive than the if validXReg(rd) approach in terms of LoC changed, but it's a type directed chore and sail will tell model authors if they're trying to slice out the bits rather than map to a valid register, which the if validXreg(rd) approach will not.
Hi Robert. I'm glad someone else has looked at this.
Some months back, I was looking at what needs to be done to support the E extension. It was a cursory inspection, and I didn't consider the CSR write action.
You are entirely correct. And this condition needs to be correctly handled. And yes, it will be intrusive. Nevertheless, it will need to be supported.
Thanks for pointing this out.
Bill Mc.
On Thu, Aug 15, 2024 at 9:15 AM Robert Norton @.***> wrote:
This model currently assumes there are 32 X registers i.e. the "embedded" ISA variants with only 16 registers are not supported. The CHERIoT fork of this repo includes a bit of a hack https://github.com/CHERIoT-Platform/sail-riscv/commit/4d04efaaefdf28191b821382baa73afe75d3664e to work around this. It raises a Sail exception for the invalid registers in the register access functions then catches it and raises a RISC-V reserved instruction in the instruction fetch loop. This almost works but has a major disadvantage that any side effects of instruction execution that happen before the illegal register access will still take effect! For example if rd of a csrrw is greater than 15 this won't be noticed until the CSR has already been written but it will then a reserved instruction exception!
We could fix this in the decode mapping, for example by adding a guard such as if validXReg(rd) && validXReg(rs1) && validXReg(rs2) on every mapping where validXReg would account for the embedded variants, however this would be very intrusive. I'm posting this to canvas opinion and see if anyone has any better ideas.
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/523, or unsubscribe https://github.com/notifications/unsubscribe-auth/AXROLOEO23TVUEBWTZKE3ATZRSZWJAVCNFSM6AAAAABMSJC432VHI2DSMVQWIX3LMV43ASLTON2WKOZSGQ3DQMJTGUZTENY . You are receiving this because you are subscribed to this thread.Message ID: @.***>
-- Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309
Join me at RISC-V Summit North America http://www.riscvsummit.com/ in October!
Following on from @nwf-msr's comment, if you wanted to make the spec truely parametric in whether the E extension exists or not you could do something like:
type E : Bool
struct regidx = {
idx : bits(if E then 4 else 5)
}
mapping xreg : bits(5) <-> regidx = {
forwards bv if constraint(E) && bv[4] == 0 => struct { idx = bv[3..0] },
forwards bv if not(constraint(E)) => struct { idx = bv },
backwards reg => zero_extend(reg.idx),
}
Then the decode clauses would look like e.g.
union clause ast = UTYPE : (bits(20), regidx, uop)
mapping clause encdec = UTYPE(imm, rd, op)
<-> imm @ xreg(rd) @ encdec_uop(op)
Currently this requires the --abstract-types option for Sail which is quite experimental, and might explode. I've been slowly working on tying this together with the Sail module system, so you can write extensions as Sail optional modules and have types that vary depending whether that extension is present, and you avoid the problem of ifdefs where certain combinations are not statically checked to work.
This is probably more intrusive than the if validXReg(rd) approach in terms of LoC changed, but it's a type directed chore and sail will tell model authors if they're trying to slice out the bits rather than map to a valid register, which the if validXreg(rd) approach will not.
I think the fact that it can be checked would make this approach much better than just having a validXreg guard. I'm not even sure it would be that much more of a chore.
Following on from @nwf-msr's comment, if you wanted to make the spec truely parametric in whether the E extension exists
Oh, that's very cute. I hadn't imagined something so elaborate and had just imagined swapping out between model/riscv-regs-i.sail and riscv-regs-e.sail.
That's probably the simplest way to handle it right now, but I've been trying to add features to handle some of the RISC-V configurability in a more generic way, but it's not 100% in place yet.
have types that vary depending whether that extension is present
Would that require recompiling the Sail code to switch between E and not-E, because you have to include/exclude the E code? I think it would be better (if possible) if we could always compile the E code but make it a "configure time" option (i.e. a parameter to model_init() or similar).
Also why does regidx need to be a struct and not just a type alias?
type regidx = bits(if E then 4 else 5)
Also why does
regidxneed to be a struct and not just a type alias?
To strongly encourage, if not quite force, the use of the partial xreg mapping (as in https://github.com/riscv/sail-riscv/issues/523#issuecomment-2291570640) in the instruction codec mapping-s, rather than just slicing the register bits out of the instruction bits.
A type alias to the type you suggest seems like it would make slicing somewhat challenging. I think you'd need to replace @ rd @ with @ pad_rd @ rd @ with pad_rd : bits(if E then 1 else 0) and ensure that it was zero. That is, I think the struct type is also more ergonomic despite the additional layer of struct-ure.
Would that require recompiling the Sail code to switch between E and not-E, because you have to include/exclude the E code? I think it would be better (if possible) if we could always compile the E code but make it a "configure time" option (i.e. a parameter to model_init() or similar).
In theory no, but it would require some enhancements to the Sail->C backend to handle a type like bits(if ... then len else other_len) at runtime (which just means representing it as a variable-width bitvector that can handle both lengths, which we already have). Some Sail backends can't handle that so you'd have to instantiate the abstract types with concrete types at compile time.
I’m on my phone right so I can’t check: is misa.E defined to indicate an RV32/64E? and, if so, is it required to be readonly? If it does and is not required to be readonly, we should “clarify” the spec to make it so to spare the complications .
On Thursday, August 15, 2024, Alasdair Armstrong @.***> wrote:
Would that require recompiling the Sail code to switch between E and not-E, because you have to include/exclude the E code? I think it would be better (if possible) if we could always compile the E code but make it a "configure time" option (i.e. a parameter to model_init() or similar).
In theory no, but it would require some enhancements to the Sail->C backend to handle a type like bits(if ... then len else other_len) at runtime (which just means representing it as a variable-width bitvector that can handle both lengths, which we already have). Some Sail backends can't handle that so you'd have to instantiate the abstract types with concrete types at compile time.
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/523#issuecomment-2291601052, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJSBV33VALZKJLPA7HDZRTGDJAVCNFSM6AAAAABMSJC432VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEOJRGYYDCMBVGI . You are receiving this because you are subscribed to this thread.Message ID: @.***>
It's read-only:
The "I" bit will be set for RV32I, RV64I, and RV128I base ISAs, and the "E" bit will be set for RV32E and RV64E. The Extensions field is a WARL field that can contain writable bits where the implementation allows the supported ISA to be modified. At reset, the Extensions field shall contain the maximal set of supported extensions, and "I" shall be selected over "E" if both are available.
The "E" bit is read-only. Unless misa is all read-only zero, the "E" bit always reads as the complement of the "I" bit. If an execution environment supports both RV32E and RV32I, software can select RV32E by clearing the "I" bit.
Would it be a mistake to not support runtime switching of E, even though the spec does support it (the model already has that limitations for XLEN)?
It obviously makes the code way nicer if it's a compile time option (or "constraint time") and runtime switching of E seems like it would be an extremely niche design.
Ah, so the I bit can be RW, but E must always be the complement, regardless of what the write data is. My preference is that the I bit be readonly; there is no reason I can think of to switch it. Programs written for E will still run (because selecting X16..X31 has undefined consequences so it won't even trap always. It will make ACTs slightly more complicated, in that we will need to run additional tests (and different boot code) if the bit is RW vs readonly.
On Sun, Aug 25, 2024 at 11:32 PM Tim Hutt @.***> wrote:
It's read-only:
The "I" bit will be set for RV32I, RV64I, and RV128I base ISAs, and the "E" bit will be set for RV32E and RV64E. The Extensions field is a WARL field that can contain writable bits where the implementation allows the supported ISA to be modified. At reset, the Extensions field shall contain the maximal set of supported extensions, and "I" shall be selected over "E" if both are available.
The "E" bit is read-only. Unless misa is all read-only zero, the "E" bit always reads as the complement of the "I" bit. If an execution environment supports both RV32E and RV32I, software can select RV32E by clearing the "I" bit.
Would it be a mistake to not support runtime switching of E, even though the spec does support it (the model already has that limitations for XLEN)?
It obviously makes the code way nicer if it's a compile time option (or "constraint time") and runtime switching of E seems like it would be an extremely niche design.
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/523#issuecomment-2309432677, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJWWS4GLWQCMBRJUDQTZTLDXXAVCNFSM6AAAAABMSJC432VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMBZGQZTENRXG4 . You are receiving this because you commented.Message ID: @.***>
My preference is that the I bit be readonly; there is no reason I can think of to switch it.
I agree. Do you think you could convince them to specify that?
Wel, I can try....
On Fri, Aug 30, 2024 at 12:05 AM Tim Hutt @.***> wrote:
My preference is that the I bit be readonly; there is no reason I can think of to switch it.
I agree. Do you think you could convince them to specify that?
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/523#issuecomment-2320282244, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJQA7OR6UYOOVGDYQS3ZUAKTLAVCNFSM6AAAAABMSJC432VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMRQGI4DEMRUGQ . You are receiving this because you commented.Message ID: @.***>
I tried. There is an obscure use case for this (allowing custom ops using X16-31 in E mode). Andrew just doesn't see the need to prohibit this - though setting misa.I to be read_only in the Sail model is likely pretty safe, and we can use the ACT waiver system to deal with the consequences of when a test succeeds in changing misa.I.
On Fri, Aug 30, 2024 at 4:44 PM Allen Baum @.***> wrote:
Wel, I can try....
On Fri, Aug 30, 2024 at 12:05 AM Tim Hutt @.***> wrote:
My preference is that the I bit be readonly; there is no reason I can think of to switch it.
I agree. Do you think you could convince them to specify that?
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/523#issuecomment-2320282244, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJQA7OR6UYOOVGDYQS3ZUAKTLAVCNFSM6AAAAABMSJC432VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMRQGI4DEMRUGQ . You are receiving this because you commented.Message ID: @.***>