1 files changed, 155 insertions, 0 deletions
diff --git a/test/smt/rv_add_1.sat.sail b/test/smt/rv_add_1.sat.sail
new file mode 100644
index 00000000..b2a562c4
--- /dev/null
+++ b/test/smt/rv_add_1.sat.sail
@@ -0,0 +1,155 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen       : Int  = 32
+type xlen_bytes : Int  = 4
+type xlenbits   : Type = bits(xlen)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = unsigned(b)
+
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI}
+
+/* Architectural state */
+register R1 : xlenbits
+register R2 : xlenbits
+register R3 : xlenbits
+register R4 : xlenbits
+register R5 : xlenbits
+register R6 : xlenbits
+register R7 : xlenbits
+register R8 : xlenbits
+register R9 : xlenbits
+register R10 : xlenbits
+register R11 : xlenbits
+register R12 : xlenbits
+register R13 : xlenbits
+register R14 : xlenbits
+register R15 : xlenbits
+register R16 : xlenbits
+register R17 : xlenbits
+register R18 : xlenbits
+register R19 : xlenbits
+register R20 : xlenbits
+register R21 : xlenbits
+register R22 : xlenbits
+register R23 : xlenbits
+register R24 : xlenbits
+register R25 : xlenbits
+register R26 : xlenbits
+register R27 : xlenbits
+register R28 : xlenbits
+register R29 : xlenbits
+register R30 : xlenbits
+register R31 : xlenbits
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+
+function rX(r) = {
+  if r == 0 then sail_zero_extend(0x0, sizeof(xlen))
+  else if r == 1 then R1
+  else if r == 2 then R2
+  else if r == 3 then R3
+  else if r == 4 then R4
+  else if r == 5 then R5
+  else if r == 6 then R6
+  else if r == 7 then R7
+  else if r == 8 then R8
+  else if r == 9 then R9
+  else if r == 10 then R10
+  else if r == 11 then R11
+  else if r == 12 then R12
+  else if r == 13 then R13
+  else if r == 14 then R14
+  else if r == 15 then R15
+  else if r == 16 then R16
+  else if r == 17 then R17
+  else if r == 18 then R18
+  else if r == 19 then R19
+  else if r == 20 then R20
+  else if r == 21 then R21
+  else if r == 22 then R22
+  else if r == 23 then R23
+  else if r == 24 then R24
+  else if r == 25 then R25
+  else if r == 26 then R26
+  else if r == 27 then R27
+  else if r == 28 then R28
+  else if r == 29 then R29
+  else if r == 30 then R30
+  else R31
+}
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+
+function wX(r, v) = {
+  if r == 0 then ()
+  else if r == 1 then R1 = v
+  else if r == 2 then R2 = v
+  else if r == 3 then R3 = v
+  else if r == 4 then R4 = v
+  else if r == 5 then R5 = v
+  else if r == 6 then R6 = v
+  else if r == 7 then R7 = v
+  else if r == 8 then R8 = v
+  else if r == 9 then R9 = v
+  else if r == 10 then R10 = v
+  else if r == 11 then R11 = v
+  else if r == 12 then R12 = v
+  else if r == 13 then R13 = v
+  else if r == 14 then R14 = v
+  else if r == 15 then R15 = v
+  else if r == 16 then R16 = v
+  else if r == 17 then R17 = v
+  else if r == 18 then R18 = v
+  else if r == 19 then R19 = v
+  else if r == 20 then R20 = v
+  else if r == 21 then R21 = v
+  else if r == 22 then R22 = v
+  else if r == 23 then R23 = v
+  else if r == 24 then R24 = v
+  else if r == 25 then R25 = v
+  else if r == 26 then R26 = v
+  else if r == 27 then R27 = v
+  else if r == 28 then R28 = v
+  else if r == 29 then R29 = v
+  else if r == 30 then R30 = v
+  else R31 = v
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+val decode : bits(32) -> option(ast) effect pure
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlenbits = sail_sign_extend(imm, sizeof(xlen)) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+function clause decode _ = None()
+
+function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+  let v = X(rs1);
+  match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
+    Some(instr) => {
+      execute(instr);
+      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)))
+    },
+    _ => true
+  }
+}