Move riscv memory definitions into a separate file.

3 files changed, 106 insertions, 107 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 5ac7597f..6c58a421 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,4 +1,4 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv.sail
+SAIL_SRCS = prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv.sail
 SAIL_DIR ?= $(realpath ..)
 
 export SAIL_DIR
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
new file mode 100644
index 00000000..5ec665e8
--- /dev/null
+++ b/riscv/riscv_mem.sail
@@ -0,0 +1,105 @@
+/* memory */
+
+function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit =
+  if unsigned(addr) % width != 0 then throw Error_misaligned_access() else ()
+
+val MEMr                         : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_strong_acquire          : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+
+function MEMr                         (addr, width) = __RISCV_read(addr, width)
+function MEMr_acquire                 (addr, width) = __RISCV_read(addr, width)
+function MEMr_strong_acquire          (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved                (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_acquire        (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width)
+
+val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape}
+
+function mem_read (addr, width, aq, rl, res) = {
+  if aq | res then check_alignment(addr, width);
+
+  match (aq, rl, res) {
+    (false, false, false) => MEMr(addr, width),
+    (true,  false, false) => MEMr_acquire(addr, width),
+    (false, false, true)  => MEMr_reserved(addr, width),
+    (true,  false, true)  => MEMr_reserved_acquire(addr, width),
+    (false, true,  false) => throw(Error_not_implemented("load.rl")),
+    (true,  true,  false) => MEMr_strong_acquire(addr, width),
+    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
+    (true,  true,  true)  => MEMr_reserved_strong_acquire(addr, width)
+  }
+}
+
+val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
+  (xlenbits, atom('n)) -> unit effect {eamem}
+
+val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> unit effect {eamem, escape}
+
+function mem_write_ea (addr, width, aq, rl, con) = {
+  if rl | con then check_alignment(addr, width);
+
+  match (aq, rl, con) {
+    (false, false, false) => MEMea(addr, width),
+    (false, true,  false) => MEMea_release(addr, width),
+    (false, false, true)  => MEMea_conditional(addr, width),
+    (false, true , true)  => MEMea_conditional_release(addr, width),
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  true,  false) => MEMea_strong_release(addr, width),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (true,  true , true)  => MEMea_conditional_strong_release(addr, width)
+  }
+}
+
+val MEMval                            : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_release                    : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_strong_release             : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional                : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_release        : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+
+function MEMval                            (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_release                    (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_strong_release             (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional                (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_release        (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
+
+val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape}
+
+function mem_write_value (addr, width, value, aq, rl, con) = {
+  if rl | con then check_alignment(addr, width);
+
+  match (aq, rl, con) {
+    (false, false, false) => MEMval(addr, width, value),
+    (false, true,  false) => MEMval_release(addr, width, value),
+    (false, false, true)  => MEMval_conditional(addr, width, value),
+    (false, true,  true)  => MEMval_conditional_release(addr, width, value),
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  true,  false) => MEMval_strong_release(addr, width, value),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (true,  true,  true)  => MEMval_conditional_strong_release(addr, width, value)
+  }
+}
+
+val "speculate_conditional_success" : unit -> bool effect {exmem}
+
+val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr}
+val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit effect {barr}
+val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
+val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
+val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
+val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index f64eb5a9..818132c4 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -221,112 +221,6 @@ function extStatus_of_bits(e) = {
 type satp_mode = bits(4)
 enum SATPMode = {Sbare, Sv32, Sv39}
 
-
-/* memory */
-
-function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit =
-  if unsigned(addr) % width != 0 then throw Error_misaligned_access() else ()
-
-val MEMr                         : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_strong_acquire          : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-
-function MEMr                         (addr, width) = __RISCV_read(addr, width)
-function MEMr_acquire                 (addr, width) = __RISCV_read(addr, width)
-function MEMr_strong_acquire          (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved                (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved_acquire        (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width)
-
-val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape}
-
-function mem_read (addr, width, aq, rl, res) = {
-  if aq | res then check_alignment(addr, width);
-
-  match (aq, rl, res) {
-    (false, false, false) => MEMr(addr, width),
-    (true,  false, false) => MEMr_acquire(addr, width),
-    (false, false, true)  => MEMr_reserved(addr, width),
-    (true,  false, true)  => MEMr_reserved_acquire(addr, width),
-    (false, true,  false) => throw(Error_not_implemented("load.rl")),
-    (true,  true,  false) => MEMr_strong_acquire(addr, width),
-    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (true,  true,  true)  => MEMr_reserved_strong_acquire(addr, width)
-  }
-}
-
-val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-
-val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> unit effect {eamem, escape}
-
-function mem_write_ea (addr, width, aq, rl, con) = {
-  if rl | con then check_alignment(addr, width);
-
-  match (aq, rl, con) {
-    (false, false, false) => MEMea(addr, width),
-    (false, true,  false) => MEMea_release(addr, width),
-    (false, false, true)  => MEMea_conditional(addr, width),
-    (false, true , true)  => MEMea_conditional_release(addr, width),
-    (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MEMea_strong_release(addr, width),
-    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true , true)  => MEMea_conditional_strong_release(addr, width)
-  }
-}
-
-val MEMval                            : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_release                    : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_strong_release             : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional                : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional_release        : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-
-function MEMval                            (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_release                    (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_strong_release             (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional                (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional_release        (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
-
-val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape}
-
-function mem_write_value (addr, width, value, aq, rl, con) = {
-  if rl | con then check_alignment(addr, width);
-
-  match (aq, rl, con) {
-    (false, false, false) => MEMval(addr, width, value),
-    (false, true,  false) => MEMval_release(addr, width, value),
-    (false, false, true)  => MEMval_conditional(addr, width, value),
-    (false, true,  true)  => MEMval_conditional_release(addr, width, value),
-    (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MEMval_strong_release(addr, width, value),
-    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true,  true)  => MEMval_conditional_strong_release(addr, width, value)
-  }
-}
-
-val "speculate_conditional_success" : unit -> bool effect {exmem}
-
-val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr}
-val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit effect {barr}
-val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
-val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
-val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
-val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
 /* CSR access control bits (from CSR addresses) */
 type csrRW = bits(2)  /* read/write */