Allow extensions to types of memory access, and factor out PTE and PTW definitions.

14 files changed, 176 insertions, 166 deletions

diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 06e20f9..318d2a2 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -46,7 +46,7 @@ type ext_data_addr_error = unit
 
 /* Default data addr is just base register + immediate offset (may be zero).
    Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, width : word_width)
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
          -> Ext_DataAddr_Check(ext_data_addr_error) =
   let addr = X(base) + offset in
   Ext_DataAddr_OK(addr)
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index ae8748c..d615691 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -14,14 +14,14 @@ function fetch() -> FetchResult =
     Ext_FetchAddr_OK(use_pc) => {
       if   (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
       then F_Error(E_Fetch_Addr_Align, PC)
-      else match translateAddr(use_pc, Execute) {
+      else match translateAddr(use_pc, Execute()) {
         TR_Failure(e)     => F_Error(e, PC),
         TR_Address(ppclo) => {
           /* split instruction fetch into 16-bit granules to handle RVC, as
            * well as to generate precise fault addresses in any fetch
            * exceptions.
            */
-          match mem_read(Execute, ppclo, 2, false, false, false) {
+          match mem_read(Execute(), ppclo, 2, false, false, false) {
             MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
             MemValue(ilo)   => {
               if   isRVC(ilo)
@@ -32,10 +32,10 @@ function fetch() -> FetchResult =
                 match ext_fetch_check_pc(PC, PC_hi) {
                   Ext_FetchAddr_Error(e)      => F_Ext_Error(e),
                   Ext_FetchAddr_OK(use_pc_hi) => {
-                    match translateAddr(use_pc_hi, Execute) {
+                    match translateAddr(use_pc_hi, Execute()) {
                       TR_Failure(e)     => F_Error(e, PC_hi),
                       TR_Address(ppchi) => {
-                        match mem_read(Execute, ppchi, 2, false, false, false) {
+                        match mem_read(Execute(), 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 cd2f069..a9d6be7 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -44,7 +44,7 @@ function clause execute(LOADRES(aq, rl, 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(), Read, width) {
+    match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
         let aligned : bool =
@@ -62,12 +62,12 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
          */
         if (~ (aligned))
         then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
-        else match translateAddr(vaddr, Read) {
+        else match translateAddr(vaddr, Read(Data)) {
                TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                TR_Address(addr) =>
                  match (width, sizeof(xlen)) {
-                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(Read, addr, 4, aq, rl, true), false),
-                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read, addr, 8, aq, rl, true), false),
+                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, true), false),
+                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, true), false),
                    _            => internal_error("LOADRES expected WORD or DOUBLE")
                  }
              }
@@ -103,7 +103,7 @@ 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, width) {
+      match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) => {
           let aligned : bool =
@@ -123,8 +123,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               /* cannot happen in rmem */
               X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
             } else {
-              match translateAddr(vaddr, Write) {  /* Write and ReadWrite are equivalent here:
-                                                    * both result in a SAMO exception */
+              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) => {
                   let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -189,10 +189,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     /* Get the address, X(rs1) (no offset).
      * Some extensions perform additional checks on address validity.
      */
-    match ext_data_get_addr(rs1, zeros(), ReadWrite, width) {
+    match ext_data_get_addr(rs1, zeros(), ReadWrite(Data), width) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
-        match translateAddr(vaddr, ReadWrite) {
+        match translateAddr(vaddr, ReadWrite(Data)) {
           TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
           TR_Address(addr) => {
             let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -205,8 +205,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(ReadWrite, addr, 4, aq, aq & rl, true)),
-                  (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite, addr, 8, aq, aq & rl, true)),
+                  (WORD, _)    => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(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 14a626e..0df5ce8 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -318,23 +318,23 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   let offset : xlenbits = EXTS(imm);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Read, width) {
+  match ext_data_get_addr(rs1, offset, Read(Data), width) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     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) {
+      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_load(rd, vaddr, mem_read(Read, addr, 1, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 1, aq, rl, false), is_unsigned),
             (HALF, _)   =>
-               process_load(rd, vaddr, mem_read(Read, addr, 2, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, false), is_unsigned),
             (WORD, _)   =>
-               process_load(rd, vaddr, mem_read(Read, addr, 4, aq, rl, false), is_unsigned),
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, false), is_unsigned),
             (DOUBLE, 64) =>
-               process_load(rd, vaddr, mem_read(Read, addr, 8, aq, rl, false), is_unsigned)
+               process_load(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, false), is_unsigned)
           }
       }
   }
@@ -373,12 +373,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   let offset : xlenbits = EXTS(imm);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Write, width) {
+  match ext_data_get_addr(rs1, offset, Write(Data), width) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
       then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
-      else match translateAddr(vaddr, Write) {
+      else match translateAddr(vaddr, Write(Data)) {
         TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr) => {
           let eares : MemoryOpResult(unit) = match width {
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 9f417c0..b62caf8 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -20,7 +20,7 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool
   unsigned(addr) % width == 0
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
+function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
   let result = (match (aq, rl, res) {
     (false, false, false) => Some(read_ram(Read_plain, addr, width)),
     (true, false, false)  => Some(read_ram(Read_RISCV_acquire, addr, width)),
@@ -32,17 +32,17 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, ad
     (false, true, true)   => None()
   }) : option(bits(8 * 'n));
   match (t, result) {
-    (Execute, None()) => MemException(E_Fetch_Access_Fault),
-    (Read,    None()) => MemException(E_Load_Access_Fault),
-    (_,       None()) => MemException(E_SAMO_Access_Fault),
-    (_,      Some(v)) => { if   get_config_print_mem()
-                           then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
-                           MemValue(v) }
+    (Execute(),  None()) => MemException(E_Fetch_Access_Fault),
+    (Read(Data), None()) => MemException(E_Load_Access_Fault),
+    (_,          None()) => MemException(E_SAMO_Access_Fault),
+    (_,         Some(v)) => { if   get_config_print_mem()
+                              then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+                              MemValue(v) }
   }
 }
 
 /* dispatches to MMIO regions or physical memory regions depending on physical memory map */
-function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
   if   within_mmio_readable(addr, width)
   then mmio_read(addr, width)
   else if within_phys_mem(addr, width)
@@ -50,7 +50,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType,
   else MemException(E_Load_Access_Fault)
 
 /* PMP checks if enabled */
-function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
   if   (~ (plat_enable_pmp ()))
   then checked_mem_read(t, addr, width, aq, rl, res)
   else {
@@ -81,9 +81,9 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
 $else
-val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
 $endif
 
 function mem_read (typ, addr, width, aq, rl, res) = {
@@ -148,10 +148,10 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
   else MemException(E_SAMO_Access_Fault)
 
 /* PMP checks if enabled */
-function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
+function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) =
   if   (~ (plat_enable_pmp ()))
   then checked_mem_write(wk, addr, width, data, meta)
-  else match pmpCheck(addr, width, Write, effectivePrivilege(mstatus, cur_privilege)) {
+  else match pmpCheck(addr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) {
          None()  => checked_mem_write(wk, addr, width, data, meta),
          Some(e) => MemException(e)
   }
@@ -163,18 +163,18 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, ad
  * data.
  * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
  */
-val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (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) = {
+val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = {
   rvfi_write(addr, width, value);
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_SAMO_Addr_Align)
   else match (aq, rl, con) {
-    (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, meta),
-    (false, true,  false) => pmp_mem_write(Write_RISCV_release, addr, width, value, meta),
-    (false, false, true)  => pmp_mem_write(Write_RISCV_conditional, addr, width, value, meta),
-    (false, true , true)  => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, meta),
-    (true,  true,  false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, meta),
-    (true,  true , true)  => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, meta),
+    (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, ext_acc, meta),
+    (false, true,  false) => pmp_mem_write(Write_RISCV_release, addr, width, value, ext_acc, meta),
+    (false, false, true)  => pmp_mem_write(Write_RISCV_conditional, addr, width, value, ext_acc, meta),
+    (false, true , true)  => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, ext_acc, meta),
+    (true,  true,  false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, ext_acc, meta),
+    (true,  true , true)  => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, ext_acc, meta),
     // throw an illegal instruction here?
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq"))
@@ -184,4 +184,4 @@ function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
 /* Memory write with a default metadata value. */
 val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
 function mem_write_value (addr, width, value, aq, rl, con) =
-  mem_write_value_meta(addr, width, value, default_meta, aq, rl, con)
+  mem_write_value_meta(addr, width, value, default_write_acc, default_meta, aq, rl, con)
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 4c65f7d..c1de35c 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -26,18 +26,18 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
 
 /* permission checks */
 
-val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> bool
+val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool
 function pmpCheckRWX(ent, acc) = {
   match acc {
-    Read      => ent.R() == true,
-    Write     => ent.W() == true,
-    ReadWrite => ent.R() == true & ent.W() == true,
-    Execute   => ent.X() == true
+    Read(Data)       => ent.R() == true,
+    Write(Data)      => ent.W() == true,
+    ReadWrite(Data)  => ent.R() == true & ent.W() == true,
+    Execute()        => ent.X() == true
   }
 }
 
 // this needs to be called with the effective current privilege.
-val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> bool
+val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
 function pmpCheckPerms(ent, acc, priv) = {
   match priv {
     Machine => if   ent.L() == true
@@ -68,7 +68,7 @@ function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> p
 
 enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail}
 
-function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privilege,
+function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege,
                        ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = {
   let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr);
   match pmpMatchAddr(addr, width, rng) {
@@ -82,7 +82,7 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: P
 
 /* priority checks */
 
-function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType, priv: Privilege)
+function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
                   -> option(ExceptionType) = {
   let width : xlenbits = to_bits(sizeof(xlen), width);
   let check : bool =
@@ -158,10 +158,10 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
   if   check
   then None()
   else match acc {
-    Read      => Some(E_Load_Access_Fault),
-    Write     => Some(E_SAMO_Access_Fault),
-    ReadWrite => Some(E_SAMO_Access_Fault),
-    Execute   => Some(E_Fetch_Access_Fault)
+    Read(Data)      => Some(E_Load_Access_Fault),
+    Write(Data)     => Some(E_SAMO_Access_Fault),
+    ReadWrite(Data) => Some(E_SAMO_Access_Fault),
+    Execute()       => Some(E_Fetch_Access_Fault)
   }
 }
 
diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
new file mode 100644
index 0000000..34266cc
--- /dev/null
+++ b/model/riscv_pte.sail
@@ -0,0 +1,50 @@
+/* PTE attributes, permission checks and updates */
+
+type pteAttribs = bits(8)
+
+bitfield PTE_Bits : pteAttribs = {
+  D : 7,
+  A : 6,
+  G : 5,
+  U : 4,
+  X : 3,
+  W : 2,
+  R : 1,
+  V : 0
+}
+
+function isPTEPtr(p : pteAttribs) -> bool = {
+  let a = Mk_PTE_Bits(p);
+  a.R() == false & a.W() == false & a.X() == false
+}
+
+function isInvalidPTE(p : pteAttribs) -> bool = {
+  let a = Mk_PTE_Bits(p);
+  a.V() == false | (a.W() == true & a.R() == false)
+}
+
+function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
+  match (ac, priv) {
+    (Read(Data),      User)       => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
+    (Write(Data),     User)       => p.U() == true & p.W() == true,
+    (ReadWrite(Data), User)       => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
+    (Execute(),       User)       => p.U() == true & p.X() == true,
+
+    (Read(Data),      Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
+    (Write(Data),     Supervisor) => (p.U() == false | do_sum) & p.W() == true,
+    (ReadWrite(Data), Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
+    (Execute(),       Supervisor) => p.U() == false & p.X() == true,
+
+    (_,               Machine)    => internal_error("m-mode mem perm check")
+  }
+}
+
+function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type)) -> option(PTE_Bits) = {
+  let update_d = (a == Write(Data) | a == ReadWrite(Data)) & p.D() == false; // dirty-bit
+  let update_a = p.A() == false;                                             // accessed-bit
+  if update_d | update_a then {
+    let np = update_A(p, true);
+    let np = if update_d then update_D(np, true) else np;
+    Some(np)
+  } else None()
+}
diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail
new file mode 100644
index 0000000..e2056b4
--- /dev/null
+++ b/model/riscv_ptw.sail
@@ -0,0 +1,37 @@
+/* failure modes for address-translation/page-table-walks */
+enum PTW_Error = {
+  PTW_Access,       /* physical memory access error for a PTE */
+  PTW_Invalid_PTE,
+  PTW_No_Permission,
+  PTW_Misaligned,   /* misaligned superpage */
+  PTW_PTE_Update    /* PTE update needed but not enabled */
+}
+val ptw_error_to_str : PTW_Error -> string
+function ptw_error_to_str(e) =
+  match (e) {
+    PTW_Access        => "mem-access-error",
+    PTW_Invalid_PTE   => "invalid-pte",
+    PTW_No_Permission => "no-permission",
+    PTW_Misaligned    => "misaligned-superpage",
+    PTW_PTE_Update    => "pte-update-needed"
+  }
+
+overload to_str = {ptw_error_to_str}
+
+/* conversion of these translation/PTW failures into architectural exceptions */
+function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = {
+  let e : ExceptionType =
+  match (a, f) {
+    (ReadWrite(Data), PTW_Access) => E_SAMO_Access_Fault,
+    (ReadWrite(Data), _)          => E_SAMO_Page_Fault,
+    (Read(Data), PTW_Access)      => E_Load_Access_Fault,
+    (Read(Data), _)               => E_Load_Page_Fault,
+    (Write(Data), PTW_Access)     => E_SAMO_Access_Fault,
+    (Write(Data), _)              => E_SAMO_Page_Fault,
+    (Execute(), PTW_Access)       => E_Fetch_Access_Fault,
+    (Execute(), _)                => E_Fetch_Page_Fault
+  } in {
+/*  print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
+    e
+  }
+}
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index a47afc3..e0a1f45 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -97,18 +97,12 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
 
 /* memory access types */
 
-enum AccessType = {Read, Write, ReadWrite, Execute}
-
-val accessType_to_str : AccessType -> string
-function accessType_to_str (a) =
-  match (a) {
-    Read      => "R",
-    Write     => "W",
-    ReadWrite => "RW",
-    Execute   => "X"
-  }
-
-overload to_str = {accessType_to_str}
+union AccessType ('a : Type) = {
+  Read      : 'a,
+  Write     : 'a,
+  ReadWrite : 'a,
+  Execute   : unit
+}
 
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c8808f7..f77366b 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -8,95 +8,6 @@
 
 let PAGESIZE_BITS = 12
 
-/* PTE attributes, permission checks and updates */
-
-type pteAttribs = bits(8)
-
-bitfield PTE_Bits : pteAttribs = {
-  D : 7,
-  A : 6,
-  G : 5,
-  U : 4,
-  X : 3,
-  W : 2,
-  R : 1,
-  V : 0
-}
-
-function isPTEPtr(p : pteAttribs) -> bool = {
-  let a = Mk_PTE_Bits(p);
-  a.R() == false & a.W() == false & a.X() == false
-}
-
-function isInvalidPTE(p : pteAttribs) -> bool = {
-  let a = Mk_PTE_Bits(p);
-  a.V() == false | (a.W() == true & a.R() == false)
-}
-
-function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
-  match (ac, priv) {
-    (Read,      User)       => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Write,     User)       => p.U() == true & p.W() == true,
-    (ReadWrite, User)       => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute,   User)       => p.U() == true & p.X() == true,
-
-    (Read,      Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
-    (Write,     Supervisor) => (p.U() == false | do_sum) & p.W() == true,
-    (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute,   Supervisor) => p.U() == false & p.X() == true,
-
-    (_,         Machine)    => internal_error("m-mode mem perm check")
-  }
-}
-
-function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = {
-  let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit
-  let update_a = p.A() == false;                                 // accessed-bit
-  if update_d | update_a then {
-    let np = update_A(p, true);
-    let np = if update_d then update_D(np, true) else np;
-    Some(np)
-  } else None()
-}
-
-/* failure modes for address-translation/page-table-walks */
-enum PTW_Error = {
-  PTW_Access,       /* physical memory access error for a PTE */
-  PTW_Invalid_PTE,
-  PTW_No_Permission,
-  PTW_Misaligned,   /* misaligned superpage */
-  PTW_PTE_Update    /* PTE update needed but not enabled */
-}
-val ptw_error_to_str : PTW_Error -> string
-function ptw_error_to_str(e) =
-  match (e) {
-    PTW_Access        => "mem-access-error",
-    PTW_Invalid_PTE   => "invalid-pte",
-    PTW_No_Permission => "no-permission",
-    PTW_Misaligned    => "misaligned-superpage",
-    PTW_PTE_Update    => "pte-update-needed"
-  }
-
-overload to_str = {ptw_error_to_str}
-
-/* conversion of these translation/PTW failures into architectural exceptions */
-function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = {
-  let e : ExceptionType =
-  match (a, f) {
-    (ReadWrite, PTW_Access) => E_SAMO_Access_Fault,
-    (ReadWrite, _)          => E_SAMO_Page_Fault,
-    (Read, PTW_Access)      => E_Load_Access_Fault,
-    (Read, _)               => E_Load_Page_Fault,
-    (Write, PTW_Access)     => E_SAMO_Access_Fault,
-    (Write, _)              => E_SAMO_Page_Fault,
-    (Fetch, PTW_Access)     => E_Fetch_Access_Fault,
-    (Fetch, _)              => E_Fetch_Page_Fault
-  } in {
-/*  print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
-    e
-  }
-}
-
 /*
  * Definitions for RV32, which has a single address translation mode: Sv32.
  */
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index e3cca0b..467ac5f 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -33,11 +33,11 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr : (xlenbits, AccessType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
 function translateAddr(vAddr, ac) = {
   let effPriv : Privilege = match ac {
-    Execute => cur_privilege,
-    _       => effectivePrivilege(mstatus, cur_privilege)
+    Execute() => cur_privilege,
+    _         => effectivePrivilege(mstatus, cur_privilege)
   };
   let mxr    : bool   = mstatus.MXR() == true;
   let do_sum : bool   = mstatus.SUM() == true;
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a575a07..c31a9bb 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -1,6 +1,6 @@
 /* Sv39 address translation for RV64. */
 
-val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
+val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rreg, escape}
 function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
   let va = Mk_SV39_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -105,7 +105,7 @@ function flush_TLB39(asid, addr) =
 
 /* address translation */
 
-val translate39 : (asid64, paddr64, vaddr39, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
 function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
   match lookup_TLB39(asid, vAddr) {
     Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index a898ac7..664807c 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -1,6 +1,6 @@
 /* Sv48 address translation for RV64. */
 
-val walk48 : (vaddr48, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
+val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rreg, escape}
 function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
   let va = Mk_SV48_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
@@ -105,7 +105,7 @@ function flush_TLB48(asid, addr) =
 
 /* address translation */
 
-val translate48 : (asid64, paddr64, vaddr48, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem}
 function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
   match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false) {
     PTW_Failure(f) => TR_Failure(f),
diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail
new file mode 100644
index 0000000..577de37
--- /dev/null
+++ b/model/riscv_vmem_types.sail
@@ -0,0 +1,18 @@
+// Specialize the accesstype for memory
+
+type ext_access_type = unit
+
+let Data  : ext_access_type = ()
+
+let default_write_acc : ext_access_type = Data
+
+val accessType_to_str : AccessType(ext_access_type) -> string
+function accessType_to_str (a) =
+  match (a) {
+    Read(Data)      => "R",
+    Write(Data)     => "W",
+    ReadWrite(Data) => "RW",
+    Execute()       => "X"
+  }
+
+overload to_str = {accessType_to_str}