Handle address translation for misaligned loads and stores better

Refactor the LOAD and STORE instruction so they split misaligned
accesses into multiple sub-accesses and perform address translation
separately. This means we should handle the case where a misaligned
access straddles a page boundary in a sensible way, even if we don't
yet cover the full range of possibilities allowed for any RISC-V
implementation.

There are options for the order in which misaligned happen, i.e. from
high-to-low or from low-to-high as well as the granularity of the splitting,
either all the way to bytes or to the largest aligned size. The splitting
can also be disabled if an implementation supports misaligned accesses in hardware.

The Zama16b extension is support with an --enable-zama16b flag on the simulator.

In addition tidy up the implementation in a few ways:

- Very long lines on the LOAD encdec were fixed by adding a helper

- Add some linebreaks in the code so it reads as less claustrophobic

- Ensure we use the same names for arguments in encdec/execute/assembly.
  Previously we used 'size' and 'width'. I opted for 'width' consistently.

Makefile

@@ -92,6 +92,7 @@ SAIL_VM_SRCS += riscv_vmem_pte.sail
 SAIL_VM_SRCS += riscv_vmem_ptw.sail
 SAIL_VM_SRCS += riscv_vmem_tlb.sail
 SAIL_VM_SRCS += riscv_vmem.sail
+SAIL_VM_SRCS += riscv_vmem_utils.sail
 
 # Non-instruction sources
 PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
@@ -194,7 +195,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
 .PHONY:
 
 all: c_emulator/riscv_sim_$(ARCH)
-.PHONY: all
+.PHONY: all check_properties
 
 # the following ensures empty sail-generated .c files don't hang around and
 # break future builds if sail exits badly
@@ -203,6 +204,9 @@ all: c_emulator/riscv_sim_$(ARCH)
 check: $(SAIL_SRCS) model/main.sail Makefile
 	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
+check_properties: $(SAIL_SRCS) Makefile
+	$(SAIL) --smt --smt-auto $(SAIL_FLAGS) $(SAIL_SRCS)
+
 interpret: $(SAIL_SRCS) model/main.sail
 	$(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 

c_emulator/riscv_platform.c

@@ -67,6 +67,26 @@ bool sys_enable_zicboz(unit u)
   return rv_enable_zicboz;
 }
 
+bool sys_enable_zama16b(unit u)
+{
+  return rv_enable_zama16b;
+}
+
+bool sys_misaligned_order_decreasing(unit u)
+{
+  return rv_misaligned_order_decreasing;
+}
+
+bool sys_misaligned_to_byte(unit u)
+{
+  return rv_misaligned_to_byte;
+}
+
+uint64_t sys_misaligned_allowed_within(unit u)
+{
+  return rv_misaligned_allowed_within;
+}
+
 uint64_t sys_pmp_count(unit u)
 {
   return rv_pmp_count;

c_emulator/riscv_platform.h

@@ -12,6 +12,11 @@ bool sys_enable_vext(unit);
 bool sys_enable_bext(unit);
 bool sys_enable_zicbom(unit);
 bool sys_enable_zicboz(unit);
+bool sys_enable_zama16b(unit);
+
+bool sys_misaligned_order_decreasing(unit);
+bool sys_misaligned_to_byte(unit);
+uint64_t sys_misaligned_allowed_within(unit);
 
 uint64_t sys_pmp_count(unit);
 uint64_t sys_pmp_grain(unit);

c_emulator/riscv_platform_impl.c

@@ -9,6 +9,11 @@ uint64_t rv_pmp_grain = 0;
 uint64_t rv_vector_vlen_exp = 0x9;
 uint64_t rv_vector_elen_exp = 0x6;
 
+/* Defaults for misaligned access behavior in the generated simulator */
+bool rv_misaligned_order_decreasing = false;
+bool rv_misaligned_to_byte = false;
+uint64_t rv_misaligned_allowed_within = 0;
+
 bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
 bool rv_enable_zfinx = false;
@@ -19,6 +24,7 @@ bool rv_enable_vext = true;
 bool rv_enable_bext = false;
 bool rv_enable_zicbom = false;
 bool rv_enable_zicboz = false;
+bool rv_enable_zama16b = false;
 
 bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;

c_emulator/riscv_platform_impl.h

@@ -14,6 +14,10 @@ extern uint64_t rv_pmp_grain;
 extern uint64_t rv_vector_vlen_exp;
 extern uint64_t rv_vector_elen_exp;
 
+extern bool rv_misaligned_order_decreasing;
+extern bool rv_misaligned_to_byte;
+extern uint64_t rv_misaligned_allowed_within;
+
 extern bool rv_enable_svinval;
 extern bool rv_enable_zcb;
 extern bool rv_enable_zfinx;
@@ -23,6 +27,7 @@ extern bool rv_enable_vext;
 extern bool rv_enable_bext;
 extern bool rv_enable_zicbom;
 extern bool rv_enable_zicboz;
+extern bool rv_enable_zama16b;
 extern bool rv_enable_writable_misa;
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;

c_emulator/riscv_sim.c

@@ -58,7 +58,11 @@ enum {
   OPT_ENABLE_ZCB,
   OPT_ENABLE_ZICBOM,
   OPT_ENABLE_ZICBOZ,
+  OPT_ENABLE_ZAMA16B,
   OPT_CACHE_BLOCK_SIZE,
+  OPT_MISALIGNED_ORDER_DEC,
+  OPT_MISALIGNED_TO_BYTE,
+  OPT_MISALIGNED_WITHIN,
 };
 
 static bool do_dump_dts = false;
@@ -133,6 +137,9 @@ static struct option options[] = {
     {"enable-misaligned",           no_argument,       0, 'm'                     },
     {"pmp-count",                   required_argument, 0, OPT_PMP_COUNT           },
     {"pmp-grain",                   required_argument, 0, OPT_PMP_GRAIN           },
+    {"misaligned-order-decreasing", no_argument,       0, OPT_MISALIGNED_ORDER_DEC},
+    {"misaligned-to-byte",          no_argument,       0, OPT_MISALIGNED_TO_BYTE  },
+    {"misaligned-allowed-within",   required_argument, 0, OPT_MISALIGNED_WITHIN   },
     {"ram-size",                    required_argument, 0, 'z'                     },
     {"disable-compressed",          no_argument,       0, 'C'                     },
     {"disable-writable-misa",       no_argument,       0, 'I'                     },
@@ -158,6 +165,7 @@ static struct option options[] = {
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
     {"enable-zicbom",               no_argument,       0, OPT_ENABLE_ZICBOM       },
     {"enable-zicboz",               no_argument,       0, OPT_ENABLE_ZICBOZ       },
+    {"enable-zama16b",              no_argument,       0, OPT_ENABLE_ZAMA16B      },
     {"cache-block-size",            required_argument, 0, OPT_CACHE_BLOCK_SIZE    },
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
@@ -334,6 +342,25 @@ static int process_args(int argc, char **argv)
       }
       rv_pmp_grain = pmp_grain;
       break;
+    case OPT_MISALIGNED_ORDER_DEC:
+      fprintf(stderr,
+              "misaligned access virtual addresses will be translated in "
+              "decreasing order.\n");
+      rv_misaligned_order_decreasing = true;
+      break;
+    case OPT_MISALIGNED_TO_BYTE:
+      fprintf(stderr,
+              "misaligned accesses will be split into individual "
+              "byte operations.\n");
+      rv_misaligned_to_byte = true;
+      break;
+    case OPT_MISALIGNED_WITHIN:
+      rv_misaligned_allowed_within = atol(optarg);
+      fprintf(stderr,
+              "misaligned accesses will be atomic when within %" PRIu64
+              " regions\n",
+              rv_misaligned_allowed_within);
+      break;
     case 'C':
       fprintf(stderr, "disabling RVC compressed instructions.\n");
       rv_enable_rvc = false;
@@ -424,6 +451,10 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling Zicbom extension.\n");
       rv_enable_zicbom = true;
       break;
+    case OPT_ENABLE_ZAMA16B:
+      fprintf(stderr, "enabling Zama16b extension.\n");
+      rv_enable_zama16b = true;
+      break;
     case OPT_ENABLE_ZICBOZ:
       fprintf(stderr, "enabling Zicboz extension.\n");
       rv_enable_zicboz = true;

model/prelude.sail

@@ -10,6 +10,7 @@ default Order dec
 
 $include <smt.sail>
 $include <option.sail>
+$include <result.sail>
 $include <arith.sail>
 $include <string.sail>
 $include <mapping.sail>

model/riscv_insts_aext.sail

@@ -81,20 +81,30 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
     * Extensions might perform additional checks on address validity.
     */
   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_Error(e)  => {
+      ext_handle_data_check_error(e);
+      RETIRE_FAIL
+    },
+
     Ext_DataAddr_OK(vaddr) => {
       /* "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(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 mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
-            MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
-            MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
-          },
+      if not(is_aligned(vaddr, width)) then {
+        handle_mem_exception(vaddr, E_Load_Addr_Align());
+        return RETIRE_FAIL
+      };
+
+      match vmem_read(vaddr, width_bytes, aq, aq & rl, true) {
+        Err(vaddr, e) => {
+          handle_mem_exception(vaddr, e);
+          RETIRE_FAIL
+        },
+
+        Ok(data) => {
+          X(rd) = sign_extend(data);
+          RETIRE_SUCCESS
+        },
       }
     }
   }
@@ -116,49 +126,51 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   // This is checked during decoding.
   assert(width_bytes <= xlen_bytes);
 
-  if speculate_conditional () == false then {
-    /* should only happen in rmem
-     * rmem: allow SC to fail very early
+  if speculate_conditional() == false then {
+    /* should only happen in RMEM
+     * RMEM: allow SC to fail very early
      */
-    X(rd) = zero_extend(0b1); RETIRE_SUCCESS
-  } else {
-    /* normal non-rmem case
-      * rmem: SC is allowed to succeed (but might fail later)
-      */
-    /* Get the address, X(rs1) (no offset).
-      * Extensions might perform additional checks on address validity.
-      */
-    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) => {
-        if not(is_aligned(vaddr, width))
-        then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
-        else {
-          match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
-                                                      * both result in a SAMO exception */
-            TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-            TR_Address(addr, _) => {
-              // Check reservation with physical address.
-              if not(match_reservation(addr)) then {
-                /* cannot happen in rmem */
-                X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
-              } else {
-                let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
-                match eares {
-                  MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-                  MemValue(_) => {
-                    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 }
-                    }
-                  }
-                }
-              }
-            }
-          }
-        }
+    X(rd) = zero_extend(0b1);
+    return RETIRE_SUCCESS
+  };
+
+  /* normal non-rmem case
+   * RMEM: SC is allowed to succeed (but might fail later)
+   */
+  /* Get the address, X(rs1) (no offset).
+   * Extensions might perform additional checks on address validity.
+   */
+  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) => {
+      if not(is_aligned(vaddr, width)) then {
+        handle_mem_exception(vaddr, E_SAMO_Addr_Align());
+        return RETIRE_FAIL
+      };
+
+      let data = X(rs2)[width_bytes * 8 - 1 .. 0];
+
+      match vmem_write(vaddr, width_bytes, data, aq & rl, rl, true) {
+        Err(vaddr, e) => {
+          handle_mem_exception(vaddr, e);
+          RETIRE_FAIL
+        },
+
+        Ok(true) => {
+          X(rd) = zero_extend(0b0);
+          cancel_reservation();
+          RETIRE_SUCCESS
+        },
+
+        Ok(false) => {
+          X(rd) = zero_extend(0b1);
+          cancel_reservation();
+          RETIRE_SUCCESS
+        },
       }
     }
   }