5 files changed, 185 insertions, 2 deletions
diff --git a/test/smt/assembly_mapping.sat.sail b/test/smt/assembly_mapping.sat.sail
new file mode 100644
index 00000000..a7b0bec5
--- /dev/null
+++ b/test/smt/assembly_mapping.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(assembly(UTYPE(0x00000, 0b00000, RISCV_LUI)) == x)
+}
diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
new file mode 100644
index 00000000..d34f3629
--- /dev/null
+++ b/test/smt/encdec.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(utype_mnemonic(RISCV_LUI) == x)
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index c9cadec3..f59bdba9 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+                step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
                 if re.match('.+\.sat\.sail$', filename):
                     step('grep -q ^sat$ {}.out'.format(basename))
                 else:
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-$counterexample
+$property
 function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
diff --git a/test/smt/store_load.sat.sail b/test/smt/store_load.sat.sail
new file mode 100644
index 00000000..810bbfbb
--- /dev/null
+++ b/test/smt/store_load.sat.sail
@@ -0,0 +1,55 @@
+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))
+}
+
+/* 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)
+}