diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0e0a52b32..eaa49ae60 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -53,14 +53,12 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size) * 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)); + if haveAtomics() then { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. @@ -68,32 +66,19 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) { 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, 1, aq, aq & rl, true) { + MemValue(result) => { load_reservation(addr); X(rd) = zero_extend(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + }, + } } } } else { @@ -113,6 +98,11 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid( /* 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 @@ -129,17 +119,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) { 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 { @@ -150,25 +130,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 } @@ -212,47 +179,36 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(s /* 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)); + if haveAtomics() then { /* 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 eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); 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 rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; + let rs2_val = extend_value(is_unsigned, rs2_val); 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 loaded = extend_value(is_unsigned, loaded); let result : xlenbits = match op { AMOSWAP => rs2_val, @@ -269,20 +225,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(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) { + let rval : xlenbits = sign_extend(loaded[width_bytes * 8 - 1 .. 0]); + let wval = mem_write_value(addr, width_bytes, result[width_bytes * 8 - 1 .. 0], aq & rl, rl, true); + match wval { MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index d28f51d7b..40e4efea8 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -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] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 } +// 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 }, + }, } + }, } } @@ -380,9 +373,14 @@ 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) @@ -390,25 +388,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { 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 } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 664495450..32008d798 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -282,59 +282,27 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt() /* Execution semantics ================================ */ -val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) - -> Retired -function process_fload64(rd, addr, value) = - if sizeof(flen) == 64 - then match value { - MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - else { - /* should not get here */ - RETIRE_FAIL - } +function clause execute(LOAD_FP(imm, rs1, rd, width)) = { + let width_bytes = size_bytes(width); -val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) - -> Retired -function process_fload32(rd, addr, value) = - match value { - MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); -val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16))) - -> Retired -function process_fload16(rd, addr, value) = - match value { - MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - -function clause execute(LOAD_FP(imm, rs1, rd, width)) = { let offset : xlenbits = sign_extend(imm); /* 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) => 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(addr, _) => { - let (aq, rl, res) = (false, false, false); - match (width) { - BYTE => { handle_illegal(); RETIRE_FAIL }, - HALF => - process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)), - WORD => - process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), - DOUBLE if sizeof(flen) >= 64 => - process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), - _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), - } - } + TR_Address(addr, _) => + match mem_read(Read(Data), addr, 2, false, false, false) { + MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + }, } } } @@ -368,20 +336,16 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) /* Execution semantics ================================ */ -val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired -function process_fstore(vaddr, value) = - match value { - 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 } - } - function clause execute (STORE_FP(imm, rs2, rs1, width)) = { + let width_bytes = size_bytes(width); + + // This is checked during decoding. + assert(width_bytes <= sizeof(xlen_bytes)); // TODO: Should this actually be flen? + let offset : xlenbits = sign_extend(imm); - let (aq, rl, con) = (false, false, false); /* 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) @@ -389,24 +353,16 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match width { - BYTE => MemValue () /* bogus placeholder for illegal size */, - HALF => mem_write_ea(addr, 2, aq, rl, false), - WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) - }; + let eares = mem_write_ea(addr, width_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = F(rs2); - match (width) { - BYTE => { handle_illegal(); RETIRE_FAIL }, - HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), - WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), - DOUBLE if sizeof(flen) >= 64 => - process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), - _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), - }; + match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], false, false, 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 } + } } } }