More refactoring for RV32

- split out memory access definitions in prelude that depend on xlen
- make riscv_xlen now part of the prelude set, so that riscv_duopod can use the definition
- update xlen use in riscv_duopod so that it can now support rv32

8 files changed, 97 insertions, 90 deletions

diff --git a/Makefile b/Makefile
index 051dfc8..d3806fa 100644
--- a/Makefile
+++ b/Makefile
@@ -8,8 +8,8 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 SAIL_SYS_SRCS = riscv_csr_map.sail riscv_sys_regs.sail riscv_next_regs.sail riscv_next_control.sail riscv_sys_control.sail
 
 # non-instruction sources
-PRELUDE = prelude.sail prelude_mapping.sail
-SAIL_OTHER_SRCS = $(PRELUDE) riscv_xlen.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+PRELUDE = prelude.sail prelude_mapping.sail riscv_xlen.sail prelude_mem.sail
+SAIL_OTHER_SRCS = $(PRELUDE) riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 SAIL_OTHER_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_xlen.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 
 PRELUDE_SRCS   = $(addprefix model/,$(PRELUDE))
diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index f1eb1ab..1946a9e 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -9,9 +9,12 @@ The model contains the following Sail modules in the `model` directory:
 
 - `prelude.sail` contains useful Sail library functions.  This file
   should be referred to as needed.  The lowest level memory access
-  primitives are defined in this file, and are implemented
+  primitives are defined in `prelude_mem.sail`, and are implemented
   by the various Sail backends.
 
+- `riscv_xlen.sail` contains the `XLEN` definition for the model.  It
+  can be set for either RV32 or RV64.
+
 - `riscv_types.sail` contains some basic RISC-V definitions.  This
   file should be read first, since it provides basic definitions that
   are used throughout the specification, such as privilege
diff --git a/model/prelude.sail b/model/prelude.sail
index 6ed8554..33638aa 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -268,73 +268,6 @@ overload min = {min_nat, min_int}
 
 overload max = {max_nat, max_int}
 
-val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
-function __RISCV_write (addr, width, data, aq, rl, con) =
-  match (aq, rl, con) {
-    (false, false, false) => __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, true,  false) => __WriteRAM_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, false, true)  => __WriteRAM_conditional(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, true,  true)  => __WriteRAM_conditional_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (true,  true,  false) => __WriteRAM_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (true,  true,  true)  => __WriteRAM_conditional_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (true,  false, false) => false,
-    (true,  false, true)  => false
-  }
-
-val __TraceMemoryWrite : forall 'n 'm.
-  (atom('n), bits('m), bits(8 * 'n)) -> unit
-
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
-function __RISCV_read (addr, width, aq, rl, res) =
-  match (aq, rl, res) {
-    (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, false, true)  => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, true,  false) => None(),
-    (false, true,  true)  => None()
-  }
-
-val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
-
 val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
 
 val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
new file mode 100644
index 0000000..532d0fd
--- /dev/null
+++ b/model/prelude_mem.sail
@@ -0,0 +1,70 @@
+/* These functions define the primitives for physical memory access.
+ * They depend on the XLEN of the architecture.
+ */
+
+val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+
+val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
+function __RISCV_write (addr, width, data, aq, rl, con) =
+  match (aq, rl, con) {
+    (false, false, false) => __WriteRAM(xlen_val, width, EXTZ(0x0), addr, data),
+    (false, true,  false) => __WriteRAM_release(xlen_val, width, EXTZ(0x0), addr, data),
+    (false, false, true)  => __WriteRAM_conditional(xlen_val, width, EXTZ(0x0), addr, data),
+    (false, true,  true)  => __WriteRAM_conditional_release(xlen_val, width, EXTZ(0x0), addr, data),
+    (true,  true,  false) => __WriteRAM_strong_release(xlen_val, width, EXTZ(0x0), addr, data),
+    (true,  true,  true)  => __WriteRAM_conditional_strong_release(xlen_val, width, EXTZ(0x0), addr, data),
+    (true,  false, false) => false,
+    (true,  false, true)  => false
+  }
+
+val __TraceMemoryWrite : forall 'n 'm.
+  (atom('n), bits('m), bits(8 * 'n)) -> unit
+
+val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
+function __RISCV_read (addr, width, aq, rl, res) =
+  match (aq, rl, res) {
+    (false, false, false) => Some(__ReadRAM(xlen_val, width, EXTZ(0x0), addr)),
+    (true,  false, false) => Some(__ReadRAM_acquire(xlen_val, width, EXTZ(0x0), addr)),
+    (true,  true,  false) => Some(__ReadRAM_strong_acquire(xlen_val, width, EXTZ(0x0), addr)),
+    (false, false, true)  => Some(__ReadRAM_reserved(xlen_val, width, EXTZ(0x0), addr)),
+    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(xlen_val, width, EXTZ(0x0), addr)),
+    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(xlen_val, width, EXTZ(0x0), addr)),
+    (false, true,  false) => None(),
+    (false, true,  true)  => None()
+  }
+
+val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index f7a7712..c68a5a5 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -1,6 +1,4 @@
-
-type xlen = atom(64)
-type xlen_t = bits(64)
+// This file depends on the xlen definitions in riscv_xlen.sail.
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
@@ -13,18 +11,18 @@ function regbits_to_regno b = let r as atom(_) = unsigned(b) in r
 
 /* Architectural state */
 
-register PC : xlen_t
-register nextPC : xlen_t
+register PC : xlenbits
+register nextPC : xlenbits
 
-register Xs : vector(32, dec, xlen_t)
+register Xs : vector(32, dec, xlenbits)
 
 /* Getters and setters for X registers (special case for zeros register, x0) */
-val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlen_t effect {rreg}
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
 
-function rX 0 = 0x0000000000000000
+function rX 0 = EXTZ(0x0)
 and rX (r if r > 0) = Xs[r]
 
-val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlen_t) -> unit effect {wreg}
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
 
 function wX (r, v) =
   if r != 0 then {
@@ -35,7 +33,7 @@ overload X = {rX, wX}
 
 /* Accessors for memory */
 
-val MEMr : forall 'n, 'n >= 0. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr : forall 'n, 'n >= 0. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
 function MEMr (addr, width) =
   match __RISCV_read(addr, width, false, false, false) {
     Some(v) => v,
@@ -61,7 +59,7 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0
 
 function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
   let rs1_val = X(rs1) in
-  let imm_ext : xlen_t = EXTS(imm) in
+  let imm_ext : xlenbits = EXTS(imm) in
   let result = rs1_val + imm_ext in
   X(rd) = result
 
@@ -74,8 +72,8 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0
   = Some(LOAD(imm, rs1, rd))
 
 function clause execute(LOAD(imm, rs1, rd)) =
-    let addr : xlen_t = X(rs1) + EXTS(imm) in
-    let result : xlen_t = MEMr(addr, 8) in
+    let addr : xlenbits = X(rs1) + EXTS(imm) in
+    let result : xlenbits = MEMr(addr, xlen_val_bytes) in
     X(rd) = result
 
 /* ****************************************************************** */
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 524b0d0..94ca69b 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -1,7 +1,5 @@
 /* Basic type and function definitions used pervasively in the model. */
 
-type xlenbits = bits(xlen)
-
 let xlen_max_unsigned = 2 ^ xlen_val - 1
 let xlen_max_signed = 2 ^ (xlen_val - 1) - 1
 let xlen_min_signed = 0 - 2 ^ (xlen_val - 1)
@@ -79,7 +77,7 @@ val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
 /*function rX 0 = 0x0000000000000000
 and rX (r if r > 0) = Xs[r]*/
 function rX r = match r {
-  0 => 0x0000000000000000,
+  0 => EXTZ(0x0),
   1 => x1,
   2 => x2,
   3 => x3,
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index 5c404ba..78030e6 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -146,7 +146,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
   /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */
-  match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+  match (phys_mem_read(Data, EXTZ(pte_addr), xlen_val_bytes, false, false, false)) {
     MemException(_) => {
 /*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
@@ -313,7 +313,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
               n_ent.pte = update_BITS(ent.pte, pbits.bits());
               writeTLB39(idx, n_ent);
               /* update page table */
-              match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits(), false, false, false) {
+              match checked_mem_write(EXTZ(ent.pteAddr), xlen_val_bytes, ent.pte.bits(), false, false, false) {
                 MemValue(_) => (),
                 MemException(e) => internal_error("invalid physical address in TLB")
               };
@@ -339,7 +339,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
                 TR39_Failure(PTW_PTE_Update)
               } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
-                match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
+                match checked_mem_write(EXTZ(pteAddr), xlen_val_bytes, w_pte.bits(), false, false, false) {
                   MemValue(_) => {
                     addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                     TR39_Address(pAddr)
diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail
index afce058..801aca8 100644
--- a/model/riscv_xlen.sail
+++ b/model/riscv_xlen.sail
@@ -1,4 +1,9 @@
 /* Define the XLEN value for the architecture. */
 
+// type-level definitions
 type xlen : Int = 64
-let xlen_val = 64
+type xlenbits   = bits(xlen)
+
+// value-level definitions
+let xlen_val       = 64
+let xlen_val_bytes = 8      // byte-width of xlen bits