3 files changed, 75 insertions, 46 deletions
diff --git a/test/smt/store_load.sat.sail b/test/smt/store_load.sat.sail
index 810bbfbb..8010979f 100644
--- a/test/smt/store_load.sat.sail
+++ b/test/smt/store_load.sat.sail
@@ -1,55 +1,12 @@
 default Order dec
 
 $include <prelude.sail>
-$include <regfp.sail>
-
-register x0 : bits(32)
-register x1 : bits(32)
-register x2 : bits(32)
-register x3 : bits(32)
-
-function wX(r: bits(2), v: bits(32)) -> unit = {
-  match r {
-    0b00 => x0 = v,
-    0b01 => x1 = v,
-    0b10 => x2 = v,
-    0b11 => x3 = v
-  }
-}
-
-function rX(r: bits(2)) -> bits(32) = {
-  match r {
-    0b00 => x0,
-    0b01 => x1,
-    0b10 => x2,
-    0b11 => x3
-  }
-}
-
-overload X = {rX, wX}
-
-scattered union ast
-
-val execute : ast -> bool
-
-union clause ast = LOAD : (bits(2), bits(2))
-
-function clause execute(LOAD(rd, rs)) = {
-  X(rd) = __read_mem(Read_plain, 32, X(rs), 4);
-  true
-}
-
-union clause ast = STORE : (bits(2), bits(2))
-
-function clause execute(STORE(rd, rs)) = {
-  let addr = X(rd);
-  __write_mem(Write_plain, 32, addr, 4, X(rs))
-}
+$include "test/arch.sail"
 
 /* Default memory model is as weak as possible, so this is not true */
 $counterexample
 function prop() -> bool = {
-  let _ = execute(STORE(0b01, 0b10));
-  let _ = execute(LOAD(0b00, 0b01));
+  let _ = arch_store(0b01, 0b10);
+  let _ = arch_load(0b00, 0b01);
   X(0b00) == X(0b10)
 }
diff --git a/test/smt/store_load_scattered.sat.sail b/test/smt/store_load_scattered.sat.sail
new file mode 100644
index 00000000..d556295f
--- /dev/null
+++ b/test/smt/store_load_scattered.sat.sail
@@ -0,0 +1,31 @@
+default Order dec
+
+$include <prelude.sail>
+$include <regfp.sail>
+$include "test/arch.sail"
+
+scattered union ast
+
+val execute : ast -> bool
+
+union clause ast = LOAD : (bits(2), bits(2))
+
+function clause execute(LOAD(rd, rs)) = {
+  X(rd) = __read_mem(Read_plain, 32, X(rs), 4);
+  true
+}
+
+union clause ast = STORE : (bits(2), bits(2))
+
+function clause execute(STORE(rd, rs)) = {
+  let addr = X(rd);
+  __write_mem(Write_plain, 32, addr, 4, X(rs))
+}
+
+/* Default memory model is as weak as possible, so this is not true */
+$counterexample
+function prop() -> bool = {
+  let _ = execute(STORE(0b01, 0b10));
+  let _ = execute(LOAD(0b00, 0b01));
+  X(0b00) == X(0b10)
+}
diff --git a/test/smt/test/arch.sail b/test/smt/test/arch.sail
new file mode 100644
index 00000000..a2d61a1b
--- /dev/null
+++ b/test/smt/test/arch.sail
@@ -0,0 +1,41 @@
+$ifndef _SMT_TEST_ARCH
+$define _SMT_TEST_ARCH
+
+$include <regfp.sail>
+
+register x0 : bits(32)
+register x1 : bits(32)
+register x2 : bits(32)
+register x3 : bits(32)
+
+function wX(r: bits(2), v: bits(32)) -> unit = {
+  match r {
+    0b00 => x0 = v,
+    0b01 => x1 = v,
+    0b10 => x2 = v,
+    0b11 => x3 = v
+  }
+}
+
+function rX(r: bits(2)) -> bits(32) = {
+  match r {
+    0b00 => x0,
+    0b01 => x1,
+    0b10 => x2,
+    0b11 => x3
+  }
+}
+
+overload X = {rX, wX}
+
+function arch_load(rd: bits(2), rs: bits(2)) -> bool = {
+  X(rd) = __read_mem(Read_plain, 32, X(rs), 4);
+  true
+}
+
+function arch_store(rd: bits(2), rs: bits(2)) -> bool = {
+  let addr = X(rd);
+  __write_mem(Write_plain, 32, addr, 4, X(rs))
+}
+
+$endif