Skip to content

Commit

Permalink
Merge pull request #477 from Timmmm/user/timh/silly_switch
Browse files Browse the repository at this point in the history 
Remove unnecessary matches for loads/stores
  • Loading branch information
@billmcspadden-riscv
billmcspadden-riscv committed Jun 4, 2024
2 parents b15c0d3 + a6b656d commit 7ff6d94
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 7ff6d94

Please sign in to comment.