diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0f4da8372..192cb2dff 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -68,20 +68,10 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Read(Data), 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 }, @@ -129,17 +119,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Write(Data), 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 { @@ -219,7 +199,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - match translateAddr(vaddr, ReadWrite(Data, Data)) { + if not(is_aligned(vaddr, width)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + else 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)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b33..5122dcde8 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -313,14 +313,17 @@ function process_load(rd, vaddr, value, is_unsigned) = MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } +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 misaligned accesses are not supported. 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);