riscv · ved-rivos · Jan 20, 2024
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
@@ -92,6 +92,16 @@ bool plat_mtval_has_illegal_inst_bits(unit u)
   return rv_mtval_has_illegal_inst_bits;
 }
 
+bool sys_enable_svnapot(unit u)
+{
+  return rv_enable_svnapot;
+}
+
+bool sys_enable_svpbmt(unit u)
+{
+  return rv_enable_svpbmt;
+}
+
 mach_bits plat_ram_base(unit u)
 {
   return rv_ram_base;

diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
@@ -11,6 +11,8 @@ bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
 bool sys_enable_vext(unit);
 bool sys_enable_bext(unit);
+bool sys_enable_svnapot(unit);
+bool sys_enable_svpbmt(unit);
 
 uint64_t sys_pmp_count(unit);
 uint64_t sys_pmp_grain(unit);

diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
@@ -20,6 +20,8 @@ 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_svnapot = false;
+bool rv_enable_svpbmt = 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
@@ -24,6 +24,8 @@ 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_svnapot;
+extern bool rv_enable_svpbmt;
 
 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
@@ -56,6 +56,8 @@ enum {
   OPT_PMP_GRAIN,
   OPT_ENABLE_SVINVAL,
   OPT_ENABLE_ZCB,
+  OPT_ENABLE_SVNAPOT,
+  OPT_ENABLE_SVPBMT,
 };
 
 static bool do_dump_dts = false;
@@ -154,6 +156,8 @@ static struct option options[] = {
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
+    {"enable-svnapot",              no_argument,       0, OPT_ENABLE_SVNAPOT      },
+    {"enable-svpbmt",               no_argument,       0, OPT_ENABLE_SVPBMT       },
     {0,                             0,                 0, 0                       }
 };
 
@@ -415,6 +419,14 @@ static int process_args(int argc, char **argv)
       trace_log_path = optarg;
       fprintf(stderr, "using %s for trace output.\n", trace_log_path);
       break;
+    case OPT_ENABLE_SVNAPOT:
+      fprintf(stderr, "enabling Svnapot extension.\n");
+      rv_enable_svnapot = true;
+      break;
+    case OPT_ENABLE_SVPBMT:
+      fprintf(stderr, "enabling Svpbmt extension.\n");
+      rv_enable_svpbmt = true;
+      break;
     case '?':
       print_usage(argv[0], 1);
       break;

diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
@@ -23,7 +23,7 @@ function fetch() -> FetchResult =
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),
-        TR_Address(ppclo, _) => {
+        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.
@@ -41,7 +41,7 @@ function fetch() -> FetchResult =
                   Ext_FetchAddr_OK(use_pc_hi) => {
                     match translateAddr(use_pc_hi, Execute()) {
                       TR_Failure(e, _)     => F_Error(e, PC_hi),
-                      TR_Address(ppchi, _) => {
+                      TR_Address(ppchi, _, _) => {
                         match mem_read(Execute(), ppchi, 2, false, false, false) {
                           MemException(e) => F_Error(e, PC_hi),
                           MemValue(ihi)   => F_Base(append(ihi, ilo))

diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
@@ -21,7 +21,7 @@ function fetch() -> FetchResult = {
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),
-        TR_Address(_, _) => {
+        TR_Address(_, _, _) => {
           let i = rvfi_instruction[rvfi_insn];
           rvfi_inst_data->rvfi_insn()   = zero_extend(i);
           if   (i[1 .. 0] != 0b11)
@@ -34,7 +34,7 @@ function fetch() -> FetchResult = {
               Ext_FetchAddr_OK(use_pc_hi) =>
                 match translateAddr(use_pc_hi, Execute()) {
                   TR_Failure(e, _) => F_Error(e, PC),
-                  TR_Address(_, _) => F_Base(i)
+                  TR_Address(_, _, _) => F_Base(i)
               }
             }
           }

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
@@ -84,11 +84,11 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
       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, _) =>
+        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 }
-          },
+        }
       }
     }
   }
@@ -131,7 +131,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
           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, _) => {
+            TR_Address(addr, _, _) => {
               // Check reservation with physical address.
               if not(match_reservation(addr)) then {
                 /* cannot happen in rmem */
@@ -197,7 +197,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
       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, _) => {
+        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 {

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -331,14 +331,13 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
       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, _) =>
-
+        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 },
-          },
+        }
       }
-    },
+    }
   }
 }
 
@@ -387,7 +386,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
       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, _) => {
+        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 },

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -322,7 +322,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, 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, _) => {
+        TR_Address(addr, _, _) => {
           let (aq, rl, res) = (false, false, false);
           match (width) {
             BYTE => { handle_illegal(); RETIRE_FAIL },
@@ -388,7 +388,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, 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, _) => {
+        TR_Address(addr, _, _) => {
           let eares : MemoryOpResult(unit) = match width {
             BYTE   => MemValue () /* bogus placeholder for illegal size */,
             HALF   => mem_write_ea(addr, 2, aq, rl, false),

diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
@@ -88,7 +88,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
               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, _) => {
+                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 }
@@ -175,7 +175,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                     trimmed = true
                   }
                 },
-                TR_Address(paddr, _) => {
+                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)  => {
@@ -258,7 +258,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
             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, _) => {
+              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 },
@@ -329,7 +329,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
             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, _) => {
+              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 }
@@ -395,7 +395,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
             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, _) => {
+              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 },
@@ -467,7 +467,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
             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, _) => {
+              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 }
@@ -558,7 +558,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
             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, _) => {
+              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 },
@@ -651,7 +651,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
           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, _) => {
+            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 }
@@ -675,7 +675,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
           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, _) => {
+            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 }
@@ -733,7 +733,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
           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, _) => {
+            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 },
@@ -767,7 +767,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
           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, _) => {
+            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 },
@@ -835,7 +835,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
             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, _) => {
+              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 }
@@ -851,7 +851,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
             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, _) => {
+              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 },

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
@@ -108,6 +108,12 @@ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "
 /* whether misa.b was enabled at boot */
 val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool
 
+/* whether svnapot was enabled at boot */
+val sys_enable_svnapot = {c: "sys_enable_svnapot", ocaml: "Platform.enable_svnapot", _: "sys_enable_svnapot"} : unit -> bool
+
+/* whether svpbmt was enabled at boot */
+val sys_enable_svpbmt = {c: "sys_enable_svpbmt", ocaml: "Platform.enable_svpbmt", _: "sys_enable_svpbmt"} : unit -> bool
+
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
    unsetting C. If it returns true the write will have no effect. */
@@ -175,6 +181,12 @@ function haveZicond() -> bool = true
 /* Zabha extension support */
 function haveZabha() -> bool = true
 
+/* Svpbmt extension support */
+function haveSvpbmt() -> bool = sys_enable_svpbmt()
+
+/* Svnapot extension support */
+function haveSvnapot() -> bool = sys_enable_svnapot()
+
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.
@@ -843,7 +855,10 @@ register senvcfg : SEnvcfg
 
 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];
+  let o = [o with
+            FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0,
+            PBMTE = if haveSvpbmt() then v[PBMTE] else 0b0
+          ];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }