Pipe standard PTE attributes along with the result

riscv · Mar 18, 2024 · 563c819 · 563c819
1 parent 22a9eac
commit 563c819
Show file tree

Hide file tree

Showing 13 changed files with 51 additions and 61 deletions.
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
@@ -87,16 +87,6 @@ bool sys_enable_svpbmt(unit u)
   return rv_enable_svpbmt;
 }
 
-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/model/riscv_fetch.sail b/model/riscv_fetch.sail
@@ -86,7 +86,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.
@@ -104,7 +104,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
@@ -83,7 +83,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)
@@ -96,7 +96,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
@@ -147,7 +147,7 @@ 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 (width, sizeof(xlen)) {
                    (BYTE, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
                    (HALF, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
@@ -211,7 +211,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, _, _) => {
                   let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
                     (BYTE, _)    => mem_write_ea(addr, 1, aq & rl, rl, true),
                     (HALF, _)    => mem_write_ea(addr, 2, aq & rl, rl, true),
@@ -283,7 +283,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
       Ext_DataAddr_OK(vaddr) => {
         match translateAddr(vaddr, ReadWrite(Data, Data)) {
           TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-          TR_Address(addr, _) => {
+          TR_Address(addr, _, _) => {
             let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
               (BYTE, _)    => mem_write_ea(addr, 1, aq & rl, rl, true),
               (HALF, _)    => mem_write_ea(addr, 2, aq & rl, rl, true),

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -395,7 +395,7 @@ 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 (width) {
             BYTE =>
               process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
@@ -451,7 +451,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 : MemoryOpResult(unit) = match width {
             BYTE   => mem_write_ea(paddr, 1, aq, rl, false),
             HALF   => mem_write_ea(paddr, 2, aq, rl, false),

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -384,7 +384,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 },
@@ -450,7 +450,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
@@ -125,7 +125,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 }
@@ -212,7 +212,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)  => {
@@ -295,7 +295,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 },
@@ -366,7 +366,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 }
@@ -432,7 +432,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 },
@@ -504,7 +504,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 }
@@ -595,7 +595,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 },
@@ -688,7 +688,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 }
@@ -712,7 +712,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 }
@@ -770,7 +770,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 },
@@ -804,7 +804,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 },
@@ -872,7 +872,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 }
@@ -888,7 +888,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_vmem_common.sail b/model/riscv_vmem_common.sail
@@ -223,7 +223,7 @@ union PTW_Result('paddr : Type, 'pte : Type) = {
 
 /* Result of address translation */
 
-union TR_Result('paddr : Type, 'failure : Type) = {
-  TR_Address : ('paddr, ext_ptw),
+union TR_Result('paddr : Type, 'std_ext_bits : Type, 'failure : Type) = {
+  TR_Address : ('paddr, 'std_ext_bits, ext_ptw),
   TR_Failure : ('failure, ext_ptw)
 }
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
@@ -96,7 +96,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
+val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType)
 function translateAddr_priv(vAddr, ac, effPriv) = {
   let mxr    : bool   = mstatus[MXR] == 0b1;
   let do_sum : bool   = mstatus[SUM] == 0b1;
@@ -109,16 +109,16 @@ function translateAddr_priv(vAddr, ac, effPriv) = {
   let ext_ptw : ext_ptw = init_ext_ptw;
 
   match mode {
-    Sbare => TR_Address(vAddr, ext_ptw),
+    Sbare => TR_Address(vAddr, zeros(), ext_ptw),
     Sv32  => match translate32(asid, ptb, vAddr, ac, effPriv, mxr, do_sum, SV32_LEVELS - 1, ext_ptw) {
-               TR_Address(pa, ext_ptw) => TR_Address(to_phys_addr(pa), ext_ptw),
+               TR_Address(pa, std_ext, ext_ptw) => TR_Address(to_phys_addr(pa), std_ext, ext_ptw),
                TR_Failure(f, ext_ptw)  => TR_Failure(translationException(ac, f), ext_ptw)
              },
     _     => internal_error(__FILE__, __LINE__, "unsupported address translation scheme")
   }
 }
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType)
 function translateAddr(vAddr, ac) =
   translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))
 

diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
@@ -117,7 +117,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
+val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType)
 function translateAddr_priv(vAddr, ac, effPriv) = {
   let mxr    : bool   = mstatus[MXR] == 0b1;
   let do_sum : bool   = mstatus[SUM] == 0b1;
@@ -130,17 +130,17 @@ function translateAddr_priv(vAddr, ac, effPriv) = {
   let ext_ptw : ext_ptw = init_ext_ptw;
 
   match mode {
-    Sbare => TR_Address(vAddr, ext_ptw),
+    Sbare => TR_Address(vAddr, zeros(), ext_ptw),
     Sv39  => { if   isValidSv39Addr(vAddr)
                then match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1, ext_ptw) {
-                      TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw),
+                      TR_Address(pa, std_ext, ext_ptw) => TR_Address(zero_extend(pa), std_ext, ext_ptw),
                       TR_Failure(f, ext_ptw)  => TR_Failure(translationException(ac, f), ext_ptw)
                     }
                else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw)
              },
     Sv48  => { if   isValidSv48Addr(vAddr)
                then match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1, ext_ptw) {
-                      TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw),
+                      TR_Address(pa, std_ext, ext_ptw) => TR_Address(zero_extend(pa), std_ext, ext_ptw),
                       TR_Failure(f, ext_ptw)  => TR_Failure(translationException(ac, f), ext_ptw)
                     }
                else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw)
@@ -149,7 +149,7 @@ function translateAddr_priv(vAddr, ac, effPriv) = {
   }
 }
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType)
 function translateAddr(vAddr, ac) =
   translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))