Use better types for virtual memory translation code

Change the VM code from using `bits(64)` everywhere to using more accurate types. This also enables Sv57 support.

Makefile

@@ -83,14 +83,13 @@ SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 # SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
 # SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
 
-# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail
+# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_tlb.sail
 # ifeq ($(ARCH),RV32)
 # SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS)
 # else
 # SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
 # endif
 
-SAIL_VM_SRCS += riscv_vmem_common.sail
 SAIL_VM_SRCS += riscv_vmem_pte.sail
 SAIL_VM_SRCS += riscv_vmem_ptw.sail
 SAIL_VM_SRCS += riscv_vmem_tlb.sail

doc/ReadingGuide.md

@@ -77,8 +77,7 @@ such as the platform memory map.
   are used in the weak memory concurrency model.
 
 - The `riscv_vmem_*.sail` files describe the S-mode address
-  translation.  `riscv_vmem_types` and `riscv_vmem_common.sail`
-  contain the definitions and processing of the page-table entries and
+  translation.  `riscv_vmem_types` contains the definitions and processing of the page-table entries and
   their various permission and status bits.  `riscv_types_ext`,
   `riscv_vmem_sv32.sail`, `riscv_vmem_sv39.sail`, and
   `riscv_vmem_sv48.sail` contain the specifications for the

doc/notes_Virtual_Memory.adoc

@@ -15,15 +15,11 @@ vmem specification code is in file:
 
 Additional files:
 
-    model/riscv_vmem_common.sail
     model/riscv_vmem_pte.sail
     model/riscv_vmem_ptw.sail
     model/riscv_vmem_tlb.sail
     model/riscv_vmem_types.sail
 
-`riscv_vmem_common.sail` contains the parameterization for Sv32, Sv39,
-Sv48 and Sv57.
-
 `riscv_vmem_pte.sail` describes Page Table Entries, checks for
 permission bits, etc.
 

model/riscv_insts_base.sail

@@ -710,8 +710,11 @@ mapping clause encdec = SFENCE_VMA(rs1, rs2)
   <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SFENCE_VMA(rs1, rs2) = {
-  let addr : option(xlenbits) = if rs1 == 0b00000 then None() else Some(X(rs1));
-  let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2));
+  let addr = if rs1 != zreg then Some(X(rs1)) else None();
+  // Note, the Sail model does not currently support Sv32 & SXLEN=32 on RV64.
+  // In that case this asidlen would be incorrect because the maximum asidlen
+  // is 9 but we always set it to 16 for RV64.
+  let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None();
   match cur_privilege {
     User       => { handle_illegal(); RETIRE_FAIL },
     Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) {

model/riscv_step.sail

@@ -127,7 +127,6 @@ function loop () : unit -> unit = {
 function init_model () -> unit = {
   init_platform (); /* devices */
   init_sys ();      /* processor */
-  init_vmem ();     /* virtual memory */
 
   /* initialize extensions last */
   ext_init ();

model/riscv_sys_regs.sail

@@ -848,24 +848,31 @@ bitfield Satp64 : bits(64) = {
   PPN  : 43 .. 0
 }
 
-function legalize_satp64(a : Architecture, o : bits(64), v : bits(64)) -> bits(64) = {
-  let s = Mk_Satp64(v);
-  match satp64Mode_of_bits(a, s[Mode]) {
-    None()     => o,
-    Some(Sv32) => o,  /* Sv32 is unsupported for now */
-    Some(_)    => s.bits
-  }
-}
-
 bitfield Satp32 : bits(32) = {
   Mode : 31,
   Asid : 30 .. 22,
   PPN  : 21 .. 0
 }
 
-function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(32) = {
-  /* all 32-bit satp modes are valid */
-  v
+// TODO: This currently assumes all ASID bits are implemented
+// and does not legalize the asid field if asidlen is not the maximum.
+function legalize_satp(
+  a : Architecture,
+  o : xlenbits,
+  v : xlenbits,
+) -> xlenbits = {
+  if xlen == 32 then {
+    /* all 32-bit satp modes are valid */
+    v
+  } else if xlen == 64 then {
+    let s = Mk_Satp64(v);
+    match satpMode_of_bits(a, s[Mode]) {
+      None()     => o,
+      Some(_)    => s.bits
+    }
+  } else {
+    internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen))
+  }
 }
 
 /* disabled trigger/debug module */

model/riscv_types.sail

@@ -31,6 +31,9 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1)
 type half = bits(16)
 type word = bits(32)
 
+type pagesize_bits : Int = 12
+let  pagesize_bits = sizeof(pagesize_bits)
+
 /* register identifiers */
 
 type regidx  = bits(5)
@@ -295,14 +298,15 @@ function extStatus_of_bits(e) =
 /* supervisor-level address translation modes */
 
 type satp_mode = bits(4)
-enum SATPMode = {Sbare, Sv32, Sv39, Sv48}
+enum SATPMode = {Bare, Sv32, Sv39, Sv48, Sv57}
 
-function satp64Mode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) =
+function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) =
   match (a, m) {
-    (_,    0x0) => Some(Sbare),
+    (_,    0x0) => Some(Bare),
     (RV32, 0x1) => Some(Sv32),
     (RV64, 0x8) => Some(Sv39),
     (RV64, 0x9) => Some(Sv48),
+    (RV64, 0xA) => Some(Sv57),
     (_, _)      => None()
   }