Renamed pmm with zpm

c_emulator/riscv_platform.c

@@ -47,9 +47,9 @@ bool sys_enable_writable_fiom(unit u)
   return rv_enable_writable_fiom;
 }
 
-bool sys_enable_pmm(unit u)
+bool sys_enable_zpm(unit u)
 {
-  return rv_enable_pmm;
+  return rv_enable_zpm;
 }
 
 bool sys_enable_vext(unit u)

c_emulator/riscv_platform.h

@@ -8,7 +8,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_pmm(unit);
+bool sys_enable_zpm(unit);
 bool sys_enable_vext(unit);
 
 uint64_t sys_pmp_count(unit);

c_emulator/riscv_platform_impl.c

@@ -18,7 +18,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_pmm = false;
+bool rv_enable_zpm = false;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);

c_emulator/riscv_platform_impl.h

@@ -22,7 +22,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_pmm;
+extern bool rv_enable_zpm;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;

c_emulator/riscv_sim.c

@@ -136,7 +136,7 @@ static struct option options[] = {
     {"report-arch",                 no_argument,       0, 'a'                     },
     {"test-signature",              required_argument, 0, 'T'                     },
     {"signature-granularity",       required_argument, 0, 'g'                     },
-    {"enable-pmm",                  no_argument,       0, 'Y'                     },
+    {"enable-zpm",                  no_argument,       0, 'Y'                     },
 #ifdef RVFI_DII
     {"rvfi-dii",                    required_argument, 0, 'r'                     },
 #endif
@@ -318,7 +318,7 @@ static int process_args(int argc, char **argv)
       break;
     case 'Y':
       fprintf(stderr, "enabling pointer masking support.\n");
-      rv_enable_pmm = true;
+      rv_enable_zpm = true;
       break;      
     case 'I':
       fprintf(stderr, "disabling writable misa CSR.\n");

handwritten_support/riscv_extras.lem

@@ -169,9 +169,9 @@ 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_pmm : unit -> bool
-let sys_enable_pmm () = false
-declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`
+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 : unit -> bitvector
 let plat_ram_base () = []

handwritten_support/riscv_extras.v

@@ -201,7 +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_pmm : 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. *)

handwritten_support/riscv_extras_sequential.lem

@@ -157,9 +157,9 @@ 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_pmm : unit -> bool
-let sys_enable_pmm () = false
-declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`
+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

model/riscv_insts_base.sail

@@ -327,19 +327,19 @@ function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
   let XLEN = sizeof(xlen);
   let i = XLEN -(PMLEN +1);
   let effective_bit = effective_address[i..i];
-  let NVBITS = replicate_bits(effective_bit, PMLEN);
-  let VBITS = effective_address[i..0];
-  NVBITS @ VBITS
+  let masked_bits = replicate_bits(effective_bit, PMLEN);
+  let unmasked_bits = effective_address[i..0];
+  masked_bits @ unmasked_bits
 }
 
 function transform_PA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
   assert(PMLEN >= 0, "PMLEN out of range");
   assert(PMLEN <= 63, "PMLEN out of range");
   let XLEN = sizeof(xlen);
   let i = XLEN -(PMLEN + 1);
-  let NVBITS = replicate_bits(0b0, PMLEN);
-  let VBITS = effective_address[i..0];
-  NVBITS @ VBITS
+  let masked_bits = replicate_bits(0b0, PMLEN);
+  let unmasked_bits = effective_address[i..0];
+  masked_bits @ unmasked_bits
 }
 
 function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = {
@@ -353,6 +353,12 @@ function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits =
           (0b11) => transform_PA (vaddr,16),
         }
       },
+      (Sv39) => {
+        match (pmm_bits){
+          (0b10) => transform_VA (vaddr,7),
+          (0b11) => transform_VA (vaddr,16),          
+        }
+      },      
       (Sv48) => {
         match (pmm_bits){
           (0b10) => transform_VA (vaddr,7),

model/riscv_sys_regs.sail

@@ -94,7 +94,7 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
    supervisor mode is implemented and non-bare addressing modes are supported. */
 val sys_enable_writable_fiom = {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_pmm = {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool
+val sys_enable_zpm = {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 = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
@@ -841,7 +841,7 @@ register senvcfg : SEnvcfg
 function legalize_mseccfg(o : MSeccfg, v : xlenbits) -> 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_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
@@ -850,7 +850,7 @@ 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_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
@@ -859,7 +859,7 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> 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_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];  
+  let o = [o with PMM  = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM()];  
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
@@ -907,7 +907,7 @@ function get_pmm() -> bits(2) = {
   match cur_privilege {
     Machine => mseccfg.PMM(),
     Supervisor => menvcfg.PMM(),
-    User => senvcfg.PMM(),
+    User => if haveSupMode() then senvcfg.PMM() else menvcfg.PMM(),
   }
 } 
 

ocaml_emulator/platform.ml

@@ -15,7 +15,7 @@ let config_enable_writable_fiom        = ref true
 let config_enable_vext                 = ref true
 let config_pmp_count                   = ref Big_int.zero
 let config_pmp_grain                   = ref Big_int.zero
-let config_enable_pmm                  = ref false
+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
@@ -93,7 +93,7 @@ let mtval_has_illegal_inst_bits ()   = !config_mtval_has_illegal_inst_bits
 let enable_zcb ()                    = !config_enable_zcb
 let enable_zfinx ()                  = false
 let enable_writable_fiom ()          = !config_enable_writable_fiom
-let enable_pmm ()                    = !config_enable_pmm
+let enable_zpm ()                    = !config_enable_zpm
 let pmp_count ()                     = !config_pmp_count
 let pmp_grain ()                     = !config_pmp_grain
 

ocaml_emulator/riscv_ocaml_sim.ml

@@ -50,9 +50,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-enable-next",
                            Arg.Set P.config_enable_next,
                            " enable N extension");
-                          ("-enable-pmm",
-                           Arg.Set P.config_enable_pmm,
-                           " enable PMM support");                           
+                          ("-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");