Addition of the Zcmp Compressed Extension #525
Conversation
There was a problem hiding this comment.
"Pull requests should be a single set of related changes with a clean commit history free from merge commits." - https://github.com/riscv/sail-riscv/blob/master/CONTRIBUTING.md
Also from that document:
"It is desirable in a pull request to explain how the code presented has been verified and how the verification has been made reproducible. Ideally the pull request is accompanied by some form of automated verification that is presented in a way that the reviewers of the pull request can run. It is desirable that the pull request explains how it relates to the existing RISC-V architectural tests."
| enum clause extension = Ext_Zcmp | ||
| function clause extensionEnabled(Ext_Zcmp) = extensionEnabled(Ext_Zca) & not(extensionEnabled(Ext_Zcd)) | ||
|
|
||
| mapping RLIST_MAPPING : bits(4) <-> string = { |
There was a problem hiding this comment.
We don't use UPPER_SNAKE_CASE for mappings
| 0xc <-> "{ra, s0-s7}", | ||
| 0xd <-> "{ra, s0-s8}", | ||
| 0xe <-> "{ra, s0-s9}", | ||
| 0xf <-> "{ra, s0-11}", |
There was a problem hiding this comment.
This should probably be split up into tokens ('{', ra, sep, s0, '-', range end) and 0x6 through 0xf should be deduplicable
| } | ||
|
|
||
| mapping CM_PUSH_MAPPING_32 : (bits(4), bits(2)) <-> string = { | ||
| (0x4, 0b00) <-> "{ra}, -16", |
There was a problem hiding this comment.
Hm, I feel like there must be a better way to do this reusing the rlist mapping, duplicating it all seems rather sad. Ideally the stack adjustment would also be calculated in a general manner rather than every case enumerated individually.
There was a problem hiding this comment.
Yes. Exactly. This can be done relatively straightforwardly. I think something like this might work
type Zcmp_constants = {1, 4, 7}
enum zcmp_variants with as_nat -> Zcmp_constants = {
RV32E_Zcmp => 1,
RV32I_Zcmp => 4,
RV64_Zcmp => 7
}
type RList = bits(4)
type Spimm = bits(2)
function stack_adj_base(variant : zcmp_variants, rlist : RList) -> nat = {
match (variant, unsigned(rlist)) {
(RV32E_Zcmp, _) => 16,
(RV32I_Zcmp, i) if 4 <= i & i < 8 => 16,
(RV32I_Zcmp, i) if 8 <= i & i < 12 => 32,
(RV32I_Zcmp, i) if 12 <= i & i < 15 => 48,
(RV32I_Zcmp, 15) => 64,
(RV64_Zcmp, i) if 4 <= i & i < 6 => 16,
(RV64_Zcmp, i) if 6 <= i & i < 8 => 32,
(RV64_Zcmp, i) if 8 <= i & i < 10 => 48,
(RV64_Zcmp, i) if 10 <= i & i < 12 => 64,
(RV64_Zcmp, i) if 12 <= i & i < 14 => 80,
(RV64_Zcmp, 14) => 96,
(RV64_Zcmp, 15) => 112,
(_, _) => internal_error(__FILE__, __LINE__, "Using reserved bits ")
function stack_adj(variant : zcmp_variants, rlist : RList, spimm : Spimm) -> nat = {
stack_adj_base(variant, rlist) + unsigned(spimm) * 16
}
(You can probably replace the use of nat with something more constrained, using Sail's liquid types, but I don't have time at the moment to work out the details.)
| (0xf, 0b11) <-> "{ra, s0-s11}, -160", | ||
| } | ||
|
|
||
| mapping CM_POP_MAPPING_32 : (bits(4), bits(2)) <-> string = { |
There was a problem hiding this comment.
Push and pop would ideally be the same mapping, just with the adjustment negated, not duplicated
| union clause ast = CM_PUSH : (bits(4), bits(2)) | ||
|
|
||
| mapping clause encdec_compressed = CM_PUSH(rlist, sp54) if extensionEnabled(Ext_Zcmp) | ||
| <-> 0b101 @ 0b11000 @ rlist : bits(4) @ sp54 : bits(2) @ 0b10 if extensionEnabled(Ext_Zcmp) |
|
|
||
| if (sizeof(xlen) == 32) then { | ||
| match rlist { | ||
| 0x4 => {stack_adj_base = zero_extend(0x10);}, |
| var addr : bits(xlen) = X(sp) - zero_extend(bytes); | ||
|
|
||
| foreach (i from 0 to 12) { | ||
| //if register i is in xreg_list |
There was a problem hiding this comment.
Pointless comment (that's also poorly formatted)
| foreach (i from 0 to 12) { | ||
| //if register i is in xreg_list | ||
| if (reg_list[i] != 0b00000) then { | ||
| if (bytes == 0x4) then { |
| if (bytes == 0x4) then { | ||
| let rs1 = reg_list[i]; | ||
| let imm : bits(xlen) = stack_adj - zero_extend(bytes); | ||
| let _ = execute(STORE(imm[11..0], rs1, sp, WORD, false, false)) |
There was a problem hiding this comment.
And if one of these doesn't retire successfully you just steamroll ahead ignoring the error entirely...
| "cm.popret" ^ spc() ^ CM_POP_MAPPING_32(rlist, sp54) if (sizeof(xlen) == 32) | ||
|
|
||
| mapping clause assembly = CM_POPRET(rlist, sp54) if (sizeof(xlen) == 64) <-> | ||
| "cm.popret" ^ spc() ^ CM_POP_MAPPING_64(rlist, sp54) if (sizeof(xlen) == 64) |
There was a problem hiding this comment.
"All files should end with a newline character"
|
Cc @tariqkurd-repo who surely takes an interest in the existence and quality of this implementation |
|
|
||
| reg_list : vector (13, dec, bits(5)) = [0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000, 0b00000]; | ||
|
|
||
| match rlist { |
There was a problem hiding this comment.
This rlist seems duplicated between functions. If so, I think it should be factored into a helper function. I think it also needs some kind of comment, i.e. why do we jump straight from 0b00001 to 0b01000?
There was a problem hiding this comment.
(Note that this is more of a rhetorical question, as I know it's because x8 is the first saved register and x1 is the return address).
|
Please rebase your commits properly before opening pull requests. Stuff like this 38d7ad4 just shouldn't be here. |
|
The whole bit with a big table-like thing for setting the reglist, why not do something like: |
I think it needs reversing, but yes that's what I meant (and the list should be defined outside one function since it's needed by multiple instructions). |
Added four instructions related to Zcmp: cm.push, cm.pop, cm.popretz, and cm.popret.