Skip to content

Commit

Permalink
Remove unnecessary matches for loads/stores
Browse files Browse the repository at this point in the history 
Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size.

This also simplifies the AMO operation by not extending and truncating the values so many times, and removing the use of to_bits.
  • Loading branch information
@Timmmm
Timmmm committed Jun 3, 2024
1 parent b15c0d3 commit a6b656d
Show file tree
Hide file tree
Showing 2 changed files with 72 additions and 155 deletions.
148 changes: 40 additions & 108 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,46 +53,31 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
* call to load_reservation in LR and cancel_reservation in SC.
*/

val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
function process_loadres(rd, addr, value, is_unsigned) =
match extend_value(is_unsigned, value) {
MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}

function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) {
match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
/* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
* to treat them as valid here; otherwise we'd need to throw an internal_error.
*/
match width {
BYTE => true,
HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
/* "LR faults like a normal load, even though it's in the AMO major opcode space."
* - Andrew Waterman, isa-dev, 10 Jul 2018.
*/
if not(aligned)
if not(is_aligned(vaddr, width))
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) =>
match (width, sizeof(xlen)) {
(BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
(HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
(WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false),
(DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
}
}
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) =>
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
},
}
}
}
}
Expand All @@ -108,6 +93,11 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

if speculate_conditional () == false then {
/* should only happen in rmem
* rmem: allow SC to fail very early
Expand All @@ -120,20 +110,10 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) {
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
/* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
* to treat them as valid here; otherwise we'd need to throw an internal_error.
*/
match width {
BYTE => true,
HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
if not(aligned)
if not(is_aligned(vaddr, width))
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else {
if match_reservation(vaddr) == false then {
Expand All @@ -144,25 +124,12 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
* both result in a SAMO exception */
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
(WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true),
(DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
};
let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
rs2_val = X(rs2);
let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true),
(HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true),
(WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true),
(DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
};
match (res) {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
Expand Down Expand Up @@ -202,77 +169,42 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
let 'width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
(WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true),
(DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
let is_unsigned : bool = match op {
AMOMINU => true,
AMOMAXU => true,
_ => false
};
let rs2_val : xlenbits = match width {
BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]),
HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]),
WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]),
DOUBLE => X(rs2)
};
let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
(BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)),
(HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)),
(WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)),
(DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
match (mval) {
match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(loaded) => {
let result : xlenbits =
let result : bits('width_bytes * 8) =
match op {
AMOSWAP => rs2_val,
AMOADD => rs2_val + loaded,
AMOXOR => rs2_val ^ loaded,
AMOAND => rs2_val & loaded,
AMOOR => rs2_val | loaded,

/* These operations convert bitvectors to integer values using [un]signed,
* and back using to_bits().
*/
AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))),
AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))),
AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
AMOMIN => if rs2_val <_s loaded then rs2_val else loaded,
AMOMAX => if rs2_val >_s loaded then rs2_val else loaded,
AMOMINU => if rs2_val <_u loaded then rs2_val else loaded,
AMOMAXU => if rs2_val >_u loaded then rs2_val else loaded,
};
let rval : xlenbits = match width {
BYTE => sign_extend(loaded[7..0]),
HALF => sign_extend(loaded[15..0]),
WORD => sign_extend(loaded[31..0]),
DOUBLE => loaded
};
let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true),
(HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true),
(WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
(DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
match (wval) {
MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS },
match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) {
MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS },
MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
Expand Down
79 changes: 32 additions & 47 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -300,52 +300,45 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
<-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))

val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
function extend_value(is_unsigned, value) = match (value) {
MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits),
MemException(e) => MemException(e)
}

val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
function process_load(rd, vaddr, value, is_unsigned) =
match extend_value(is_unsigned, value) {
MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
val extend_value : forall 'n, 0 < 'n <= xlen. (bool, bits('n)) -> xlenbits
function extend_value(is_unsigned, value) = if is_unsigned then zero_extend(value) else sign_extend(value)

function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
match width {
BYTE => true,
HALF => vaddr[0..0] == zeros(),
WORD => vaddr[1..0] == zeros(),
DOUBLE => vaddr[2..0] == zeros(),
}

// Return true if the address is misaligned and we don't support misaligned access.
function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
if plat_enable_misaligned_access() then false
else match width {
BYTE => false,
HALF => vaddr[0] == bitone,
WORD => vaddr[0] == bitone | vaddr[1] == bitone,
DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
}
not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width))

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) {
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(paddr, _) =>
match (width) {
BYTE =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
HALF =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
WORD =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
DOUBLE if sizeof(xlen) >= 64 =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
_ => report_invalid_width(__FILE__, __LINE__, width, "load")
}

match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
},
}
},
}
}

Expand Down Expand Up @@ -380,35 +373,27 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
This may need revisiting. */
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) {
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(paddr, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => mem_write_ea(paddr, 1, aq, rl, false),
HALF => mem_write_ea(paddr, 2, aq, rl, false),
WORD => mem_write_ea(paddr, 4, aq, rl, false),
DOUBLE => mem_write_ea(paddr, 8, aq, rl, false)
};
let eares = mem_write_ea(paddr, width_bytes, aq, rl, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let rs2_val = X(rs2);
let res : MemoryOpResult(bool) = match (width) {
BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false),
HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false),
WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false),
DOUBLE if sizeof(xlen) >= 64
=> mem_write_value(paddr, 8, rs2_val, aq, rl, false),
_ => report_invalid_width(__FILE__, __LINE__, width, "store"),
};
match (res) {
match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) {
MemValue(true) => RETIRE_SUCCESS,
MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
Expand Down

0 comments on commit a6b656d

Please sign in to comment.