diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index cbd3ae319..ca38b8c70 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -52,6 +52,11 @@ bool sys_enable_writable_fiom(unit u)
   return rv_enable_writable_fiom;
 }
 
+bool sys_enable_zpm(unit u)
+{
+  return rv_enable_zpm;
+}
+
 bool sys_enable_vext(unit u)
 {
   return rv_enable_vext;
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index 58792319c..859cf97b2 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -9,6 +9,7 @@ bool sys_enable_zcb(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
+bool sys_enable_zpm(unit);
 bool sys_enable_vext(unit);
 bool sys_enable_bext(unit);
 bool sys_enable_zicbom(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index a76e683d4..7b6804894 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -22,6 +22,7 @@ bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;
 bool rv_mtval_has_illegal_inst_bits = false;
 bool rv_enable_writable_fiom = true;
+bool rv_enable_zpm = false;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index d8acd3b59..67eb1ca38 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -26,6 +26,7 @@ extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 extern bool rv_mtval_has_illegal_inst_bits;
 extern bool rv_enable_writable_fiom;
+extern bool rv_enable_zpm;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 3f812c5ec..943f0fc4e 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -59,6 +59,7 @@ enum {
   OPT_ENABLE_ZICBOM,
   OPT_ENABLE_ZICBOZ,
   OPT_CACHE_BLOCK_SIZE,
+  OPT_ENABLE_ZPM,
 };
 
 static bool do_dump_dts = false;
@@ -145,6 +146,7 @@ static struct option options[] = {
     {"report-arch",                 no_argument,       0, 'a'                     },
     {"test-signature",              required_argument, 0, 'T'                     },
     {"signature-granularity",       required_argument, 0, 'g'                     },
+    {"enable-zpm",                  no_argument,       0, OPT_ENABLE_ZPM          },
 #ifdef RVFI_DII
     {"rvfi-dii",                    required_argument, 0, 'r'                     },
 #endif
@@ -344,6 +346,10 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling N extension.\n");
       rv_enable_next = true;
       break;
+    case OPT_ENABLE_ZPM:
+      fprintf(stderr, "enabling pointer masking support.\n");
+      rv_enable_zpm = true;
+      break;
     case 'I':
       fprintf(stderr, "disabling writable misa CSR.\n");
       rv_enable_writable_misa = false;
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index 245a7fe80..cf89b753c 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -169,6 +169,10 @@ val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
+val sys_enable_zpm : unit -> bool
+let sys_enable_zpm () = false
+declare ocaml target_rep function sys_enable_zpm = `Platform.enable_zpm`
+
 val sys_pmp_grain : unit -> integer
 let sys_pmp_grain () = 0
 declare ocaml target_rep function sys_pmp_grain = `Platform.sys_pmp_grain`
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v
index b17f75343..aa870af01 100644
--- a/handwritten_support/riscv_extras.v
+++ b/handwritten_support/riscv_extras.v
@@ -201,6 +201,7 @@ Axiom sys_enable_fdext : unit -> bool.
 Axiom sys_enable_next : unit -> bool.
 Axiom sys_enable_zfinx : unit -> bool.
 Axiom sys_enable_writable_fiom : unit -> bool.
+Axiom sys_enable_zpm : unit -> bool.
 
 (* The constraint solver can do this itself, but a Coq bug puts
    anonymous_subproof into the term instead of an actual subproof. *)
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
index 5ffe482cd..c716641c5 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -157,6 +157,10 @@ val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
+val sys_enable_zpm : unit -> bool
+let sys_enable_zpm () = false
+declare ocaml target_rep function sys_enable_zpm = `Platform.enable_zpm`
+
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 6478919ca..a273ebcda 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -70,6 +70,7 @@ mapping clause csr_name_map = 0x306  <-> "mcounteren"
 mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
 /* machine envcfg */
 mapping clause csr_name_map = 0x30A  <-> "menvcfg"
+mapping clause csr_name_map = 0x31A  <-> "menvcfgh"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
@@ -162,6 +163,9 @@ mapping clause csr_name_map = 0xB00  <-> "mcycle"
 mapping clause csr_name_map = 0xB02  <-> "minstret"
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
+/* machine security */
+mapping clause csr_name_map = 0x747  <-> "mseccfg"
+mapping clause csr_name_map = 0x757  <-> "mseccfgh"
 /* TODO: other hpm counters and events */
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0  <-> "tselect"
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 18c047e49..820c48b47 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -72,6 +72,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
  */
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   let width_bytes = size_bytes(width);
 
   // This is checked during decoding.
@@ -86,14 +87,15 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
       /* "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 },
+      let  vaddr_ = transform_effective_address(vaddr, pmm);
+      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 }
+            MemException(e)  => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
           },
       }
     }
@@ -111,6 +113,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   let width_bytes = size_bytes(width);
 
   // This is checked during decoding.
@@ -131,12 +134,13 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
     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 }
+        let  vaddr_ = transform_effective_address(vaddr, pmm);
+        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:
+          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_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
             TR_Address(addr, _) => {
               // Check reservation with physical address.
               if not(match_reservation(addr)) then {
@@ -145,13 +149,13 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               } else {
                 let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
                 match eares {
-                  MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                  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 }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
                     }
                   }
                 }
@@ -191,6 +195,7 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   let 'width_bytes = size_bytes(width);
 
   // This is checked during decoding.
@@ -202,18 +207,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, 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, ReadWrite(Data, Data)) {
-        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm);
+      if not(is_aligned(vaddr_, width))
+      then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr_, ReadWrite(Data, Data)) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
         TR_Address(addr, _) => {
           let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
           let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
           match eares {
-            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
             MemValue(_) => {
               match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
-                MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                MemException(e)  => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
                 MemValue(loaded) => {
                   let result : bits('width_bytes * 8) =
                     match op {
@@ -230,7 +236,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) {
                     MemValue(true)  => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS },
                     MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
-                    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+                    MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
                   }
                 }
               }
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 438fa15d0..72f57ca4c 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -320,7 +320,30 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
 function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
   not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width))
 
+function transform_VA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = {
+  sign_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0])
+}
+
+function transform_PA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = {
+  zero_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0])
+}
+
+function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = {
+ if pmm then {
+    let pmm_bits = get_pmm();
+    let mode = translationMode(cur_privilege);
+    match pmm_bits {
+      pmm_mode(Enabled7) => if mode == Sbare then transform_PA(vaddr, 7) else transform_VA(vaddr, 7),
+      pmm_mode(Enabled16) => if mode == Sbare then transform_PA(vaddr, 16) else transform_VA(vaddr, 16),
+    }
+  }
+  else {
+    vaddr
+  }
+}
+
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
+  let pmm = is_pmm_active();
   let offset : xlenbits = sign_extend(imm);
   let width_bytes = size_bytes(width);
 
@@ -332,15 +355,16 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
     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(Data)) {
-        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(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(paddr, _) =>
 
           match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
             MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
-            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
           },
       }
     },
@@ -377,6 +401,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
+  let pmm = is_pmm_active();
   let offset : xlenbits = sign_extend(imm);
   let width_bytes = size_bytes(width);
 
@@ -388,20 +413,21 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
     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(Data)) {
-        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(vaddr_, width)
+      then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr_, Write(Data)) {
+        TR_Failure(e, _)    => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
         TR_Address(paddr, _) => {
           let eares = mem_write_ea(paddr, width_bytes, aq, rl, false);
           match (eares) {
-            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
             MemValue(_) => {
               let rs2_val = X(rs2);
               match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) {
                 MemValue(true)  => RETIRE_SUCCESS,
                 MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+                MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
               }
             }
           }
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 3a5509ea4..1291c16ec 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -315,26 +315,28 @@ function process_fload16(rd, addr, value) =
   }
 
 function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
+  let pmm = is_pmm_active();
   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), size_bytes(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(Data)) {
-        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(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, _) => {
           let (aq, rl, res) = (false, false, false);
           match (width) {
             BYTE => { handle_illegal(); RETIRE_FAIL },
             HALF =>
-               process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)),
+               process_fload16(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, rl, res)),
             WORD =>
-               process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)),
+               process_fload32(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, rl, res)),
             DOUBLE if sizeof(flen) >= 64 =>
-               process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)),
+               process_fload64(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, rl, res)),
             _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"),
           }
         }
@@ -380,6 +382,7 @@ function process_fstore(vaddr, value) =
   }
 
 function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
+  let pmm = is_pmm_active();
   let offset : xlenbits = sign_extend(imm);
   let (aq, rl, con) = (false, false, false);
   /* Get the address, X(rs1) + offset.
@@ -387,10 +390,11 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
   match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(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(Data)) {
-        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(vaddr_, width)
+      then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      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 {
             BYTE   => MemValue () /* bogus placeholder for illegal size */,
@@ -399,15 +403,15 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
             DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
           };
           match (eares) {
-            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
             MemValue(_) => {
               let rs2_val = F(rs2);
               match (width) {
                 BYTE => { handle_illegal(); RETIRE_FAIL },
-                HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)),
-                WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
+                HALF => process_fstore (vaddr_, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)),
+                WORD => process_fstore (vaddr_, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
                 DOUBLE if sizeof(flen) >= 64 =>
-                  process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)),
+                  process_fstore (vaddr_, mem_write_value(addr, 8, rs2_val, aq, rl, con)),
                 _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"),
               };
             }
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index b2fcc8c57..f71810c09 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -69,6 +69,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ex
 
 val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
+  let pmm = is_pmm_active();
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
   let width_type : word_width = size_bytes(load_width_bytes);
   let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -84,14 +85,15 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-              if check_misaligned(vaddr, width_type)
-              then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-              else match translateAddr(vaddr, Read(Data)) {
-                TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+              let  vaddr_ = transform_effective_address(vaddr, pmm) in
+              if check_misaligned(vaddr_, width_type)
+              then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+              else match translateAddr(vaddr_, Read(Data)) {
+                TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                 TR_Address(paddr, _) => {
                   match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) {
                     MemValue(elem)   => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem),
-                    MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                    MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                   }
                 }
               }
@@ -135,6 +137,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(
 
 val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
+  let pmm = is_pmm_active();
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
   let width_type : word_width = size_bytes(load_width_bytes);
   let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -159,16 +162,17 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
               }
             },
             Ext_DataAddr_OK(vaddr) => {
-              if check_misaligned(vaddr, width_type) then {
-                if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
+              let  vaddr_ = transform_effective_address(vaddr, pmm) in
+              if check_misaligned(vaddr_, width_type) then {
+                if i == 0 then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
                 else {
                   vl = to_bits(sizeof(xlen), i);
                   print_reg("CSR vl <- " ^ BitStr(vl));
                   trimmed = true
                 }
-              } else match translateAddr(vaddr, Read(Data)) {
+              } else match translateAddr(vaddr_, Read(Data)) {
                 TR_Failure(e, _)     => {
-                  if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                  if i == 0 then { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                   else {
                     vl = to_bits(sizeof(xlen), i);
                     print_reg("CSR vl <- " ^ BitStr(vl));
@@ -179,7 +183,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                   match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) {
                     MemValue(elem)   => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem),
                     MemException(e)  => {
-                      if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                      if i == 0 then { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                       else {
                         vl = to_bits(sizeof(xlen), i);
                         print_reg("CSR vl <- " ^ BitStr(vl));
@@ -240,6 +244,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E
 
 val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = {
+  let pmm = is_pmm_active();
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
   let width_type : word_width = size_bytes(load_width_bytes);
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -254,21 +259,22 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Write(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Write(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
                 match (eares) {
-                  MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                  MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                   MemValue(_) => {
                     let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg));
                     let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false);
                     match (res) {
                       MemValue(true)  => (),
                       MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                      MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                     }
                   }
                 }
@@ -309,6 +315,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnab
 
 val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
 function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
+  let pmm = is_pmm_active();
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
   let width_type : word_width = size_bytes(load_width_bytes);
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -325,14 +332,15 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Read(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Read(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) {
                   MemValue(elem)   => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem),
-                  MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                  MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                 }
               }
             }
@@ -376,6 +384,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEna
 
 val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
 function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
+  let pmm = is_pmm_active();
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
   let width_type : word_width = size_bytes(load_width_bytes);
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -391,21 +400,22 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Write(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Write(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
                 match (eares) {
-                  MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                  MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                   MemValue(_) => {
                     let elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg));
                     let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem_val, false, false, false);
                     match (res) {
                       MemValue(true)  => (),
                       MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                      MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                     }
                   }
                 }
@@ -446,6 +456,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna
 
 val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
 function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
+  let pmm = is_pmm_active();
   let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
   let width_type : word_width = size_bytes(EEW_data_bytes);
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -463,14 +474,15 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Read(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Read(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) {
                   MemValue(elem)   => write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem),
-                  MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                  MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                 }
               }
             }
@@ -538,6 +550,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn
 
 val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
 function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
+  let pmm = is_pmm_active();
   let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
   let width_type : word_width = size_bytes(EEW_data_bytes);
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
@@ -554,21 +567,22 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Write(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Write(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false);
                 match (eares) {
-                  MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                  MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                   MemValue(_) => {
                     let elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, vs3 + to_bits(5, j * EMUL_data_reg));
                     let res : MemoryOpResult(bool) = mem_write_value(paddr, EEW_data_bytes, elem_val, false, false, false);
                     match (res) {
                       MemValue(true)  => (),
                       MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                      MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                     }
                   }
                 }
@@ -633,6 +647,7 @@ mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if extensionEnabled(Ext_V)
 
 val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired
 function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
+  let pmm = is_pmm_active();
   let width_type : word_width = size_bytes(load_width_bytes);
   let start_element = get_start_element();
   if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */
@@ -647,14 +662,15 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
       match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) =>
-          if check_misaligned(vaddr, width_type)
-          then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-          else match translateAddr(vaddr, Read(Data)) {
-            TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+          let  vaddr_ = transform_effective_address(vaddr, pmm) in
+          if check_misaligned(vaddr_, width_type)
+          then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+          else match translateAddr(vaddr_, Read(Data)) {
+            TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
             TR_Address(paddr, _) => {
               match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) {
                 MemValue(elem)   => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem),
-                MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
               }
             }
           }
@@ -671,14 +687,15 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
       match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) =>
-          if check_misaligned(vaddr, width_type)
-          then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-          else match translateAddr(vaddr, Read(Data)) {
-            TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+          let  vaddr_ = transform_effective_address(vaddr, pmm) in
+          if check_misaligned(vaddr_, width_type)
+          then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+          else match translateAddr(vaddr_, Read(Data)) {
+            TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
             TR_Address(paddr, _) => {
               match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) {
                 MemValue(elem)   => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j), elem),
-                MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
               }
             }
           }
@@ -715,6 +732,7 @@ mapping clause encdec = VSRETYPE(nf, rs1, vs3) if extensionEnabled(Ext_V)
 
 val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired
 function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
+  let pmm = is_pmm_active();
   let width_type : word_width = BYTE;
   let start_element = get_start_element();
   if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */
@@ -729,21 +747,22 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
       match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) =>
-          if check_misaligned(vaddr, width_type)
-          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-          else match translateAddr(vaddr, Write(Data)) {
-            TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+          let  vaddr_ = transform_effective_address(vaddr, pmm) in
+          if check_misaligned(vaddr_, width_type)
+          then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+          else match translateAddr(vaddr_, Write(Data)) {
+            TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
             TR_Address(paddr, _) => {
               let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
               match (eares) {
-                MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                 MemValue(_) => {
                   let elem : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, cur_field));
                   let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, elem, false, false, false);
                   match (res) {
                     MemValue(true)  => (),
                     MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                    MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                    MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                   }
                 }
               }
@@ -763,20 +782,21 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
       match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) =>
-          if check_misaligned(vaddr, width_type)
-          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-          else match translateAddr(vaddr, Write(Data)) {
-            TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+          let  vaddr_ = transform_effective_address(vaddr, pmm) in
+          if check_misaligned(vaddr_, width_type)
+          then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+          else match translateAddr(vaddr_, Write(Data)) {
+            TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
             TR_Address(paddr, _) => {
               let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
               match (eares) {
-                MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                 MemValue(_) => {
                   let res : MemoryOpResult(bool) = mem_write_value(paddr, load_width_bytes, vs3_val[i], false, false, false);
                   match (res) {
                     MemValue(true)  => (),
                     MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                    MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                    MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                   }
                 }
               }
@@ -820,6 +840,7 @@ mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V)
 
 val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired
 function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
+  let pmm = is_pmm_active();
   let width_type : word_width = BYTE;
   let start_element = get_start_element();
   let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3);
@@ -831,14 +852,15 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Read(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Read(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 match mem_read(Read(Data), paddr, 1, false, false, false) {
                   MemValue(elem)   => write_single_element(8, i, vd_or_vs3, elem),
-                  MemException(e)  => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                  MemException(e)  => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                 }
               }
             }
@@ -847,20 +869,21 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
         match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) {
           Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); return RETIRE_FAIL },
           Ext_DataAddr_OK(vaddr) =>
-            if check_misaligned(vaddr, width_type)
-            then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL }
-            else match translateAddr(vaddr, Write(Data)) {
-              TR_Failure(e, _)     => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+            let  vaddr_ = transform_effective_address(vaddr, pmm) in
+            if check_misaligned(vaddr_, width_type)
+            then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
+            else match translateAddr(vaddr_, Write(Data)) {
+              TR_Failure(e, _)     => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
               TR_Address(paddr, _) => {
                 let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
                 match (eares) {
-                  MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
+                  MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL },
                   MemValue(_) => {
                     let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, vd_or_vs3_val[i], false, false, false);
                     match (res) {
                       MemValue(true)  => (),
                       MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                      MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); return RETIRE_FAIL }
                     }
                   }
                 }
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index f2980fb9e..349083587 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -56,6 +56,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0x3D @ idx : bits(4),  _) => pmpReadAddrReg(unsigned(0b10 @ idx)),
     (0x3E @ idx : bits(4),  _) => pmpReadAddrReg(unsigned(0b11 @ idx)),
 
+    /* machine protection */
+    (0x747,  _) => mseccfg.bits()[sizeof(xlen) - 1 .. 0],
+    (0x757, 32) => mseccfg.bits()[63 .. 32],
+
     /* machine mode counters */
     (0xB00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
     (0xB02,  _) => minstret[(sizeof(xlen) - 1) .. 0],
@@ -146,6 +150,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x3D @ idx : bits(4),  _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
     (0x3E @ idx : bits(4),  _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
 
+    /* machine protection */
+    (0x747, 32) => { mseccfg = legalize_mseccfg(mseccfg, mseccfg.bits()[63 .. 32] @ value); Some(mseccfg.bits()[31 .. 0]) },
+    (0x747, 64) => { mseccfg = legalize_mseccfg(mseccfg, value); Some(mseccfg.bits()) },
+    (0x757, 32) => { mseccfg = legalize_mseccfg(mseccfg, value @ mseccfg.bits()[31 .. 0]); Some(mseccfg.bits()[63 .. 32]) },
+
     /* machine mode counters */
     (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
     (0xB02,  _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; Some(value) },
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index da04278b7..48c8a5fd3 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -57,6 +57,10 @@ function is_CSR_defined (csr : csreg) -> bool =
     0xB80 => sizeof(xlen) == 32, // mcycleh
     0xB82 => sizeof(xlen) == 32, // minstreth
 
+    /* machine protection */
+    0x747 => true, // mseccfg
+    0x757 => sizeof(xlen) == 32, // mseccfgh      
+
     /* disabled trigger/debug module */
     0x7a0 => true,
 
@@ -541,6 +545,7 @@ function init_sys() -> unit = {
   minstret           = zero_extend(0b0);
   minstret_increment = true;
 
+  mseccfg.bits = zero_extend(0b0);
   menvcfg.bits = zero_extend(0b0);
   senvcfg.bits = zero_extend(0b0);
   /* initialize vector csrs */
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 295a4da19..2f12c5cbd 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -95,7 +95,8 @@ val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next",
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
 val sys_enable_writable_fiom = pure {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
-
+/* whether the PME extension was enabled at boot */
+val sys_enable_zpm = pure {c: "sys_enable_zpm", ocaml: "Platform.enable_zpm", _: "sys_enable_zpm"} : unit -> bool
 /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
 val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
 /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g.
@@ -755,13 +756,55 @@ function read_seed_csr() -> xlenbits = {
 /* Writes to the seed CSR are ignored */
 function write_seed_csr () -> option(xlenbits) = None()
 
+/* Pointer Masking Different modes */
+enum PointerMaskingMode = {
+  Disabled, // Pointer Masking Disabled
+  Reserved, // Reserved Encoding for Pointer Masking
+  Enabled7, // Pointer Masking Enabled with PMM = 7
+  Enabled16, // Pointer Masking Enabled with PMM = 16
+}
+
+mapping pmm_mode : PointerMaskingMode <-> bits(2) = {
+  Disabled <-> 0b00,
+  Reserved <-> 0b01,
+  Enabled7 <-> 0b10,
+  Enabled16 <-> 0b11,
+}
+
+/*  mseccfg is a XLEN-bit read/write register that controls */
+/*  security features */
+bitfield MSeccfg : bits(64) = {
+  // Reserved WPRI bits.
+  wpri_2 : 63 .. 34,
+  // PMM bits of Pointer Masking Extension
+  PMM    : 33 .. 32,
+  // Reserved WPRI bits.
+  wpri_1 : 31 .. 10,
+  // Supervisor SEED bits
+  SSEED  : 9,
+  // User SEED bits
+  USEED  : 8,
+  // Reserved WPRI bits.
+  wpri_0 : 7 .. 3,
+  // RLB bits
+  RLB    : 2,
+  // Reserved WPRI bits.
+  MMWP   : 1,
+  // MML bits
+  MML    : 0,
+}
+
 bitfield MEnvcfg : bits(64) = {
   // Supervisor TimeCmp Extension
   STCE   : 63,
   // Page Based Memory Types Extension
   PBMTE  : 62,
   // Reserved WPRI bits.
-  wpri_1 : 61 .. 8,
+  wpri_2 : 61 .. 34,
+  // PMM bits of Pointer Masking Extension
+  PMM    : 33 .. 32,
+  // Reserved WPRI bits.
+  wpri_1 : 31 .. 8,
   // Cache Block Zero instruction Enable
   CBZE   : 7,
   // Cache Block Clean and Flush instruction Enable
@@ -774,7 +817,9 @@ bitfield MEnvcfg : bits(64) = {
   FIOM   : 0,
 }
 
-bitfield SEnvcfg : xlenbits = {
+bitfield SEnvcfg : bits(64) = {
+  // PMM bits of Pointer Masking Extension
+  PMM    : 33 .. 32,
   // Cache Block Zero instruction Enable
   CBZE   : 7,
   // Cache Block Clean and Flush instruction Enable
@@ -787,19 +832,32 @@ bitfield SEnvcfg : xlenbits = {
   FIOM   : 0,
 }
 
+register mseccfg : MSeccfg
 register menvcfg : MEnvcfg
 register senvcfg : SEnvcfg
 
+function legalize_mseccfg(o : MSeccfg, v : bits(64)) -> MSeccfg = {
+  let v = Mk_MSeccfg(v);
+  // Update PMM field only if Pointer Masking is enabled and Written value is legal
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
+  // Other extensions are not implemented yet so all other fields are read only zero.
+  o
+}
+
 function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = {
   let v = Mk_MEnvcfg(v);
   let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
+  // Update PMM field only if Pointer Masking is enabled and Written value is legal
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
 
-function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = {
+function legalize_senvcfg(o : SEnvcfg, v : bits(64)) -> SEnvcfg = {
   let v = Mk_SEnvcfg(v);
   let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
+  // Update PMM field only if Pointer Masking is enabled and Written value is legal
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
@@ -814,6 +872,7 @@ function is_fiom_active() -> bool = {
     User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
   }
 }
+
 /* vector csrs */
 register vstart : bits(16) /* use the largest possible length of vstart */
 register vxsat  : bits(1)
@@ -831,6 +890,18 @@ bitfield Vtype  : xlenbits = {
 }
 register vtype : Vtype
 
+//Returns the PMM bits value depends on the Privilege mode
+function get_pmm() -> bits(2) =
+  match cur_privilege {
+    Machine => mseccfg[PMM],
+    Supervisor => menvcfg[PMM],
+    User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM],
+  }
+
+// Return whether or not PMM is currently active, based on the current
+// privilege and the menvcfg,senvcfg and mseccfg settings.
+function is_pmm_active() -> bool = get_pmm() != zeros(2)
+
 /* the dynamic selected element width (SEW) */
 /* this returns the power of 2 for SEW */
 val get_sew_pow : unit -> {3, 4, 5, 6}
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index b9921a0c3..b407441f7 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -19,6 +19,7 @@ let config_enable_zicbom               = ref false
 let config_enable_zicboz               = ref false
 let config_pmp_count                   = ref Big_int.zero
 let config_pmp_grain                   = ref Big_int.zero
+let config_enable_zpm                  = ref false
 
 let set_config_pmp_count x = config_pmp_count := Big_int.of_int x
 let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x
@@ -106,6 +107,7 @@ let enable_svinval ()                = !config_enable_svinval
 let enable_zcb ()                    = !config_enable_zcb
 let enable_zfinx ()                  = false
 let enable_writable_fiom ()          = !config_enable_writable_fiom
+let enable_zpm ()                    = !config_enable_zpm
 let pmp_count ()                     = !config_pmp_count
 let pmp_grain ()                     = !config_pmp_grain
 
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
index 20eaef66f..f075d1724 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -50,6 +50,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-enable-next",
                            Arg.Set P.config_enable_next,
                            " enable N extension");
+                          ("-enable-zpm",
+                           Arg.Set P.config_enable_zpm,
+                           " enable zpm support");                           
                           ("-mtval-has-illegal-inst-bits",
                            Arg.Set P.config_mtval_has_illegal_inst_bits,
                            " mtval stores instruction bits on an illegal instruction exception");