Conversation
tperami
force-pushed
the
feature/immediates
branch
from
6a2f552 to
1be1da8
Compare
tperami
force-pushed
the
feature/32bit
branch
2 times, most recently
from
e97c73a to
bb8b12d
Compare
|
I change the LDR/STR part to not do 4-way case splitting, you can have a look at it |
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
I did a pass of the LDR/STR code, but the rest still needs a deduplication pass. Feel free to comment my changes on the LDR/STR part
instrs-user.sail
Outdated
| if sf == bitone then { | ||
| /* 64-bit */ | ||
| let res : bits(64) = match op { | ||
| MoveReg(m) => X(m), | ||
| MoveImm(data) => match data.hw { | ||
| 0b00 => sail_zero_extend(data.imm, 64), /* imm at bits [15:0] */ | ||
| 0b01 => sail_zero_extend(data.imm, 48) @ 0x0000, /* imm at bits [31:16] */ | ||
| 0b10 => sail_zero_extend(data.imm, 32) @ 0x00000000, /* imm at bits [47:32] */ | ||
| 0b11 => data.imm @ 0x000000000000 /* imm at bits [63:48] */ | ||
| } | ||
| }; | ||
| X(d) = res; | ||
| } else { | ||
| /* 32-bit - zero-extended on write */ | ||
| let res : bits(32) = match op { | ||
| MoveReg(m) => W(m), | ||
| MoveImm(data) => match data.hw { | ||
| 0b00 => sail_zero_extend(data.imm, 32), /* imm at bits [15:0] */ | ||
| 0b01 => data.imm @ 0x0000, /* imm at bits [31:16] */ | ||
| _ => sail_zeros(32) /* unreachable: validated in decode */ | ||
| } | ||
| }; | ||
| W(d) = res; | ||
| } |
There was a problem hiding this comment.
Can we deduplicate that logic by create the immediate with hw only once and then, only in the 32 bit case, extracting the lower 32 bits?
Also isn't the logic like:
sail_shiftleft(sail_zero_extend(data.imm, 64), 16 * unsigned(hw))
This would avoid an unecessary match
instrs-user.sail
Outdated
|
|
||
| if is_imm == bitzero then { | ||
| /* For 32-bit (sf=0), imm6[5] must be 0 in register form */ | ||
| if sf == bitzero & is_imm == bitzero & imm6[5] == bitone then None () |
There was a problem hiding this comment.
Can you put that check in the is_imm == bitzero case just below, it would be easier to read
| /* Ask for the value of the program counter register and record it | ||
| * in the local variable base */ |
There was a problem hiding this comment.
Any particular reason you delete those comments?
interface.sail
Outdated
| /* See tiny-arm for descriptions, interface for definitions */ | ||
| val iFetch : (bits(addr_size), AccessDescriptor) -> bits(32) | ||
| val rMem : (bits(addr_size), AccessDescriptor) -> bits(64) | ||
| val rMem : forall 'N, 'N > 0. (int('N), bits(addr_size), AccessDescriptor) -> bits('N * 8) |
There was a problem hiding this comment.
For dependently type backend like Rocq or Lean, it would be better to do bits(8 * 'N) as that what we tend to use there
instrs-user.sail
Outdated
| if sf == bitone then { | ||
| /* 64-bit */ | ||
| let operand1 = X(n); | ||
| let operand2 = X(m); | ||
| X(d) = operand1 ^ operand2; | ||
| } else { | ||
| /* 32-bit */ | ||
| let operand1 = W(n); | ||
| let operand2 = W(m); | ||
| W(d) = operand1 ^ operand2; | ||
| } |
There was a problem hiding this comment.
Could we just have a sized version of X (both read and write) and then just write:
| if sf == bitone then { | |
| /* 64-bit */ | |
| let operand1 = X(n); | |
| let operand2 = X(m); | |
| X(d) = operand1 ^ operand2; | |
| } else { | |
| /* 32-bit */ | |
| let operand1 = W(n); | |
| let operand2 = W(m); | |
| W(d) = operand1 ^ operand2; | |
| } | |
| let size = if sf == bitzero then 32 else 64; | |
| let operand1 = X(n, size); | |
| let operand2 = X(m, size); | |
| X(d, size) = operand1 ^ operand2; |
This would avoid the duplication (also for the other instructions). Then I think we wouldn't even need the W functions
febyeji
force-pushed
the
feature/32bit
branch
from
bb8b12d to
ad070a6
Compare
2 participants
No description provided.