Remove unnecessary matches for loads/stores

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.

2 files changed, 72 insertions, 155 deletions

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 4264997..7a7e492 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -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 }
+          },
+      }
     }
   }
 }
@@ -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
@@ -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 {
@@ -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 }
@@ -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 }
                   }
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index c119ce9..26915f2 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] == 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 },
+          },
       }
+    },
   }
 }
 
@@ -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 }