Check misalignment of AMOs before address translation

This is optional according to the spec - you can check afterwards. However

1. it seems extremely unlikely that any real designs will do that for atomics, which (ignoring Zam which the model doesn't support yet), always have to be aligned, and
2. the LR and SC instructions already check before address translation, so this wasn't even consistent.

Ideally in future this would be configurable.

This also includes a minor refactor to reuse the existing alignment checking code.

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)) {

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);