Narrow the external interface to riscv_mem to mem_{read,write,write_ea}.

7 files changed, 26 insertions, 23 deletions

diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 2cc9ea2..b076b95 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -21,7 +21,7 @@ function fetch() -> FetchResult =
            * well as to generate precise fault addresses in any fetch
            * exceptions.
            */
-          match checked_mem_read(Instruction, ppclo, 2, false, false, false) {
+          match mem_read(Instruction, ppclo, 2, false, false, false) {
             MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
             MemValue(ilo)   => {
               if   isRVC(ilo)
@@ -35,7 +35,7 @@ function fetch() -> FetchResult =
                     match translateAddr(use_pc_hi, Execute, Instruction) {
                       TR_Failure(e)     => F_Error(e, PC_hi),
                       TR_Address(ppchi) => {
-                        match checked_mem_read(Instruction, ppchi, 2, false, false, false) {
+                        match mem_read(Instruction, ppchi, 2, false, false, false) {
                           MemException(e) => F_Error(E_Fetch_Access_Fault, PC_hi),
                           MemValue(ihi)   => F_Base(append(ihi, ilo))
                         }
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 1ba280d..91346ee 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -66,8 +66,8 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
                TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                TR_Address(addr) =>
                  match (width, sizeof(xlen)) {
-                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
-                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
+                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(Data, addr, 4, aq, rl, true), false),
+                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Data, addr, 8, aq, rl, true), false),
                    _            => internal_error("LOADRES expected WORD or DOUBLE")
                  }
              }
@@ -204,8 +204,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
               MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
               MemValue(_) => {
                 let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
-                  (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
-                  (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+                  (WORD, _)    => extend_value(false, mem_read(Data, addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(false, mem_read(Data, addr, 8, aq, aq & rl, true)),
                   _            => internal_error ("AMO expected WORD or DOUBLE")
                 };
                 match (rval) {
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index ae4c885..acfd1db 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -328,13 +328,13 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
         TR_Address(addr) =>
           match (width, sizeof(xlen)) {
             (BYTE, _)   =>
-               process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Data, addr, 1, aq, rl, false), is_unsigned),
             (HALF, _)   =>
-               process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Data, addr, 2, aq, rl, false), is_unsigned),
             (WORD, _)   =>
-               process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Data, addr, 4, aq, rl, false), is_unsigned),
             (DOUBLE, 64) =>
-               process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned)
+               process_load(rd, vaddr, mem_read(Data, addr, 8, aq, rl, false), is_unsigned)
           }
       }
   }
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 4d28458..5fa9a3c 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -56,19 +56,19 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (ReadType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
 $else
-val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (ReadType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
 $endif
 
-function mem_read (addr, width, aq, rl, res) = {
+function mem_read (typ, addr, width, aq, rl, res) = {
  let result : MemoryOpResult(bits(8 * 'n)) =
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_Load_Addr_Align)
   else match (aq, rl, res) {
     (false, true,  false) => throw(Error_not_implemented("load.rl")),
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => checked_mem_read(Data, addr, width, aq, rl, res)
+    (_, _, _)             => checked_mem_read(typ, addr, width, aq, rl, res)
   };
  rvfi_read(addr, width, result);
  result
@@ -145,7 +145,10 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
-/* Memory write with an explicit metadata value */
+/* Memory write with an explicit metadata value.  Metadata writes are
+ * currently assumed to have the same alignment constraints as their
+ * data.
+ */
 /* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
 val mem_write_value_meta : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
 function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index a765422..21fa68a 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -12,7 +12,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
   let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
                                 PTE32_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
-  match (checked_mem_read(Data, to_phys_addr(pte_addr), 4, false, false, false)) {
+  match (mem_read(Data, to_phys_addr(pte_addr), 4, false, false, false)) {
     MemException(_) => {
 /*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
@@ -135,7 +135,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
               n_ent.pte = n_pte.bits();
               write_TLB32(idx, n_ent);
               /* update page table */
-              match checked_mem_write(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), default_meta, false, false, false) {
+              match mem_write_value(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), false, false, false) {
                 MemValue(_)     => (),
                 MemException(e) => internal_error("invalid physical address in TLB")
               };
@@ -161,7 +161,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
                 TR_Failure(PTW_PTE_Update)
               } else {
                 w_pte : SV32_PTE = update_BITS(pte, pbits.bits());
-                match checked_mem_write(to_phys_addr(pteAddr), 4, w_pte.bits(), default_meta, false, false, false) {
+                match mem_write_value(to_phys_addr(pteAddr), 4, w_pte.bits(), false, false, false) {
                   MemValue(_) => {
                     add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                     TR_Address(pAddr)
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index 68626f1..d68190f 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -6,7 +6,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
-  match (checked_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+  match (mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
     MemException(_) => {
 /*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
@@ -129,7 +129,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
               n_ent.pte = n_pte.bits();
               write_TLB39(idx, n_ent);
               /* update page table */
-              match checked_mem_write(EXTZ(ent.pteAddr), 8, n_pte.bits(), default_meta, false, false, false) {
+              match mem_write_value(EXTZ(ent.pteAddr), 8, n_pte.bits(), false, false, false) {
                 MemValue(_)     => (),
                 MemException(e) => internal_error("invalid physical address in TLB")
               };
@@ -155,7 +155,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
                 TR_Failure(PTW_PTE_Update)
               } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
-                match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), default_meta, false, false, false) {
+                match mem_write_value(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
                   MemValue(_) => {
                     add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                     TR_Address(pAddr)
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 9d90bdc..162097d 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -6,7 +6,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
                                 PTE48_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
-  match (checked_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+  match (mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
     MemException(_) => {
 /*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
@@ -122,7 +122,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
             TR_Failure(PTW_PTE_Update)
           } else {
             w_pte : SV48_PTE = update_BITS(pte, pbits.bits());
-            match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), default_meta, false, false, false) {
+            match mem_write_value(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
               MemValue(_) => {
                 add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                 TR_Address(pAddr)