Handle address translation for misaligned loads and stores better

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
+        },
       }
     }
   }