Resolved Some Conflicts For PMM

riscv · Jul 28, 2024 · 77f8f2b · 77f8f2b
1 parent 5157ee2
commit 77f8f2b
Show file tree

Hide file tree

Showing 6 changed files with 118 additions and 217 deletions.
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
@@ -56,6 +56,7 @@ enum {
   OPT_PMP_GRAIN,
   OPT_ENABLE_SVINVAL,
   OPT_ENABLE_ZCB,
+  OPT_ENABLE_ZJPM,
 };
 
 static bool do_dump_dts = false;
@@ -128,7 +129,7 @@ static struct option options[] = {
     {"pmp-count",                   required_argument, 0, OPT_PMP_COUNT           },
     {"pmp-grain",                   required_argument, 0, OPT_PMP_GRAIN           },
     {"enable-next",                 no_argument,       0, 'N'                     },
-    {"ram-size",                    required_argument, 0, 'z'                     },
+    {"ram-size",                    required_argument, 0, 'z'                     }, 
     {"disable-compressed",          no_argument,       0, 'C'                     },
     {"disable-writable-misa",       no_argument,       0, 'I'                     },
     {"disable-fdext",               no_argument,       0, 'F'                     },
@@ -139,7 +140,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, 'Y'                     },
+    {"enable-zpm",                  no_argument,       0, OPT_ENABLE_ZJPM          }, 
 #ifdef RVFI_DII
     {"rvfi-dii",                    required_argument, 0, 'r'                     },
 #endif
@@ -151,8 +152,8 @@ static struct option options[] = {
     {"enable-zfinx",                no_argument,       0, 'x'                     },
     {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
     {"enable-svinval",              no_argument,       0, OPT_ENABLE_SVINVAL      },
-    {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},    
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
+
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
@@ -269,8 +270,7 @@ static int process_args(int argc, char **argv)
                     "t:"
                     "T:"
                     "g:"
-                    "h"
-                    "Y"                    
+                    "h"                    
 #ifdef RVFI_DII
                     "r:"
 #endif
@@ -326,7 +326,7 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling N extension.\n");
       rv_enable_next = true;
       break;
-    case 'Y':
+    case OPT_ENABLE_ZJPM:
       fprintf(stderr, "enabling pointer masking support.\n");
       rv_enable_zpm = true;
       break;      

diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
@@ -169,22 +169,17 @@ 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`
 
-<<<<<<< HEAD
+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`
 
 val sys_pmp_count : unit -> integer
 let sys_pmp_count () = 0
 declare ocaml target_rep function sys_pmp_count = `Platform.sys_pmp_count`
-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`
->>>>>>> 717cb55 (Renamed pmm with zpm)
 
 val plat_ram_base : unit -> bitvector
 let plat_ram_base () = []
@@ -260,4 +255,4 @@ val print_bits : string -> bitvector -> unit
 let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs)))
 
 val print_dbg : string -> unit
-let print_dbg msg = ()
+let print_dbg msg = ()
diff --git 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"
@@ -164,6 +165,7 @@ 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"