Update the F/D and vector loads/stores to use the vmem_utils helpers.

For writes, this involves appropriate wrappers to access source registers
of different types (i.e. reg, freg, vreg).

Add some comments on the API available from `vmem_utils`.

Update Makefile.old for SMT properties.

Author: pmundkur

Makefile.old

@@ -92,6 +92,7 @@ SAIL_SYS_SRCS += riscv_zicntr_control.sail
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 SAIL_SYS_SRCS += riscv_smcntrpmf.sail
+SAIL_SYS_SRCS += riscv_inst_retire.sail
 
 SAIL_VM_SRCS += riscv_vmem_pte.sail
 SAIL_VM_SRCS += riscv_vmem_ptw.sail
@@ -115,7 +116,6 @@ SAIL_ARCH_SRCS += riscv_sstc.sail
 SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
 SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_extensions.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail riscv_inst_retire.sail
 SAIL_ARCH_SRCS += riscv_types_kext.sail riscv_zvk_utils.sail   # Shared/common code for the cryptography extension.
-SAIL_ARCH_SRCS += riscv_inst_retire.sail
 
 SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
 RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail

doc/ReadingGuide.md

@@ -80,9 +80,15 @@ such as the platform memory map.
   appropriate access fault. This file also contains definitions that
   are used in the weak memory concurrency model.
 
-- The `riscv_vmem_*.sail` files describe the S-mode address
-  translation. See the [Virtual Memory Notes](./notes_Virtual_Memory.adoc)
-  for details.
+- The `riscv_vmem_{types,pte,ptw,tlb}.sail` and `riscv_vmem.sail`
+  files describe the S-mode address translation.
+  See the [Virtual Memory Notes](./notes_Virtual_Memory.adoc) for
+  details.
+
+- The `riscv_vmem_utils.sail` file provides a higher level interface
+  to virtual memory for load/store style instructions that handles
+  address translation and accesses to misaligned addresses taking
+  platform configuration options into account.
 
 - The `riscv_addr_checks_common.sail` and `riscv_addr_checks.sail`
   contain extension hooks to support the checking and transformation

model/riscv_insts_fext.sail

@@ -295,24 +295,9 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
   assert(width_bytes <= flen_bytes);
 
   let offset : xlenbits = sign_extend(imm);
-  /* Get the address, X(rs1) + offset.
-     Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
-    Ext_DataAddr_OK(vaddr) => {
-      if   check_misaligned(vaddr, width)
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
-      else match translateAddr(vaddr, Read(Data)) {
-        TR_Failure(e, _)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
-        TR_Address(addr, _) => {
-          let (aq, rl, res) = (false, false, false);
-          match mem_read(Read(Data), addr, width_bytes, aq, rl, res) {
-            Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
-            Err(e)     => RETIRE_FAIL(Memory_Exception(vaddr, e)),
-          }
-        },
-      }
-    }
+  match vmem_read(rs1, offset, width_bytes, false, false, false) {
+    Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
+    Err(e)     => { RETIRE_FAIL(e) }
   }
 }
 
@@ -355,31 +340,10 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
   assert(width_bytes <= flen_bytes);
 
   let offset : xlenbits = sign_extend(imm);
-  let (aq, rl, con) = (false, false, false);
-  /* Get the address, X(rs1) + offset.
-     Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
-    Ext_DataAddr_Error(e)  => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
-    Ext_DataAddr_OK(vaddr) => {
-      if   check_misaligned(vaddr, width)
-      then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
-      else match translateAddr(vaddr, Write(Data)) {
-        TR_Failure(e, _)    => RETIRE_FAIL(Memory_Exception(vaddr, e)),
-        TR_Address(addr, _) => {
-          match mem_write_ea(addr, width_bytes, aq, rl, false) {
-            Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
-            Ok(_)  => {
-              let rs2_val = F(rs2);
-              match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, con) {
-                Ok(true)  => RETIRE_SUCCESS,
-                Ok(false) => { internal_error(__FILE__, __LINE__, "store got false from mem_write_value") },
-                Err(e)    => RETIRE_FAIL(Memory_Exception(vaddr, e))
-              }
-            },
-          }
-        }
-      }
-    }
+  match vmem_write(rs1, offset, width_bytes, rs2) {
+    Ok(true)  => RETIRE_SUCCESS,
+    Ok(false) => internal_error(__FILE__, __LINE__, "store got false from vmem_write"),
+    Err(e)    => RETIRE_FAIL(e),
   }
 }