riscv sail2 wip.

3 files changed, 433 insertions, 8 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index b7c1c6a1..b4e36507 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -2,7 +2,7 @@ default Order dec
 
 /* type bits ('n : Int) = vector('n - 1, 'n, dec, bit) */
 type bits ('n : Int) = vector('n, dec, bit)
-
+union option ('a : Type) = {None, Some : 'a}
 infix 4 ==
 
 val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -276,8 +276,9 @@ val cast ex_int : int -> {'n, true. atom('n)}
 
 function ex_int 'n = n
 
-val ex_range : forall 'n 'm.
-  range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)}
+val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
+
+function ex_range (n as 'N) = n
 
 val coerce_int_nat : int -> nat effect {escape}
 
@@ -296,4 +297,20 @@ val print_int = "print_int" : (string, int) -> unit
 union exception = {
   Error_not_implemented : string,
   Error_misaligned_access,
-}
\ No newline at end of file
+}
+
+val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+
+infix 4 <_s
+infix 4 >=_s
+infix 4 <_u
+infix 4 >=_u
+
+function operator <_s  (x : bits('n), y : bits('n)) -> forall 'n. bool = signed(x) < signed(y)
+function operator >=_s (x : bits('n), y : bits('n)) -> forall 'n. bool = signed(x) >= signed(y)
+function operator <_u  (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigned(x) < unsigned(y)
+function operator >=_u (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigned(x) >= unsigned(y)
+
+val cast bool_to_bits : bool -> bits(1)
+function bool_to_bits x = if x then 0b1 else 0b0
\ No newline at end of file
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
new file mode 100644
index 00000000..00dbb190
--- /dev/null
+++ b/riscv/riscv.sail
@@ -0,0 +1,404 @@
+scattered union ast
+
+val decode : bits(32) -> option(ast) effect pure
+scattered function decode
+
+val execute : ast -> unit effect {escape, wreg, rreg}
+scattered function execute
+
+/* *******************************************************************/
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+function clause decode imm : bits(20) @ rd : regbits @ 0b0110111 = Some(UTYPE(imm, rd, RISCV_LUI))
+function clause decode imm : bits(20) @ rd : regbits @ 0b0010111 = Some(UTYPE(imm, rd, RISCV_AUIPC))
+
+function clause execute UTYPE(imm, rd, op) =
+    let off : bits(64) = EXTS(imm @ 0x000) in
+    let ret : regval   = match op {
+      RISCV_LUI   => off,
+      RISCV_AUIPC => PC + off
+    } in
+    wGPR(rd, ret)
+
+/* *******************************************************************/
+
+union clause ast = RISCV_JAL : (bits(21), regbits)
+
+function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_JAL(imm[19] @ imm[7..0] @ imm[8] @ imm[18..13] @ imm[12..9] @ 0b0, rd))
+
+function clause execute (RISCV_JAL(imm, rd)) = {
+    let pc : bits(64) = PC;
+    wGPR(rd, pc + 4);
+    let offset : bits(64) = EXTS(imm);
+    nextPC = pc + offset;
+}
+
+/* *******************************************************************/
+union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b1100111 =
+    Some(RISCV_JALR(imm, rs1, rd))
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+    /* write rd before anything else to prevent unintended strength */
+    wGPR(rd, PC + 4);
+    let newPC : bits(64) = rGPR(rs1) + EXTS(imm);
+    nextPC = newPC[63..1] @ 0b0;
+}
+
+/* *******************************************************************/
+union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
+
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BEQ))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BNE))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b100 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLT))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b101 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGE))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b110 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLTU))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b111 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGEU))
+
+function clause execute (BTYPE(imm, rs2, rs1, op)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let taken : bool = match op {
+    RISCV_BEQ  => rs1_val == rs2_val,
+    RISCV_BNE  => rs1_val != rs2_val,
+    RISCV_BLT  => rs1_val <_s rs2_val,
+    RISCV_BGE  => rs1_val >=_s rs2_val,
+    RISCV_BLTU => rs1_val <_u rs2_val,
+    RISCV_BGEU => rs1_val >=_u rs2_val
+  } in
+  if taken then
+    nextPC = PC + EXTS(imm)
+
+/* *******************************************************************/
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTI))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_XORI))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ORI))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ANDI))
+
+function clause execute (ITYPE (imm, rs1, rd, op)) =
+  let rs1_val = rGPR(rs1) in
+  let imm64 : bits(64) = EXTS(imm) in
+  let result : bits(64) = match op {
+    RISCV_ADDI  => rs1_val + imm64,
+    RISCV_SLTI  => EXTZ(rs1_val <_s imm64),
+    RISCV_SLTIU => EXTZ(rs1_val <_u imm64),
+    RISCV_XORI  => rs1_val ^ imm64,
+    RISCV_ORI   => rs1_val | imm64,
+    RISCV_ANDI  => rs1_val & imm64
+  } in
+  wGPR(rd, result)
+/*
+(********************************************************************)
+union ast member ((bits(6)), regbits, regbits, sop) SHIFTIOP
+
+function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b010000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))
+
+function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = 
+    let rs1_val = rGPR(rs1) in
+    let result = switch(op) {
+      case RISCV_SLLI -> rs1_val >> shamt
+      case RISCV_SRLI -> rs1_val << shamt
+      case RISCV_SRAI -> shift_right_arith64(rs1_val, shamt)
+    } in
+    wGPR(rd, result)
+
+(********************************************************************)
+union ast member (regbits, regbits, regbits, rop) RTYPE
+
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
+function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
+function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b111 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_AND))
+
+function clause execute (RTYPE(rs2, rs1, rd, op)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let (bits(64)) result = switch(op) {
+    case RISCV_ADD  -> rs1_val + rs2_val
+    case RISCV_SUB  -> rs1_val - rs2_val
+    case RISCV_SLL  -> rs1_val << (rs2_val[5..0])
+    case RISCV_SLT  -> EXTZ(rs1_val <_s rs2_val)
+    case RISCV_SLTU -> EXTZ(rs1_val <_u rs2_val)
+    case RISCV_XOR  -> rs1_val ^ rs2_val
+    case RISCV_SRL  -> rs1_val >> (rs2_val[5..0])
+    case RISCV_SRA  -> shift_right_arith64(rs1_val, rs2_val[5..0])
+    case RISCV_OR   -> rs1_val | rs2_val
+    case RISCV_AND  -> rs1_val & rs2_val
+  } in
+  wGPR(rd, result)
+
+(********************************************************************)
+union ast member ((bits(12)), regbits, regbits, bool, word_width, bool, bool) LOAD
+
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
+
+function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
+    let (bits(64)) addr = rGPR(rs1) + EXTS(imm) in
+    let (bits(64)) result = if unsigned then 
+        switch (width) {
+          case BYTE   -> EXTZ(mem_read(addr, 1, aq, rl, false))
+          case HALF   -> EXTZ(mem_read(addr, 2, aq, rl, false))
+          case WORD   -> EXTZ(mem_read(addr, 4, aq, rl, false))
+          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
+        }
+      else
+        switch (width) {
+          case BYTE   -> EXTS(mem_read(addr, 1, aq, rl, false))
+          case HALF   -> EXTS(mem_read(addr, 2, aq, rl, false))
+          case WORD   -> EXTS(mem_read(addr, 4, aq, rl, false))
+          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
+        } in
+    wGPR(rd, result)
+
+(********************************************************************)
+union ast member ((bits(12)), regbits, regbits, word_width, bool, bool) STORE
+
+function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (bits(5)) imm5 @ 0b0100011) =
+  Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false))
+function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (bits(5)) imm5 @ 0b0100011) =
+  Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false))
+function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (bits(5)) imm5 @ 0b0100011) =
+  Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false))
+function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (bits(5)) imm5 @ 0b0100011) =
+  Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))
+
+function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
+    let (bits(64)) addr = rGPR(rs1) + EXTS(imm) in {
+      switch (width) {
+        case BYTE   -> mem_write_ea(addr, 1, aq, rl, false)
+        case HALF   -> mem_write_ea(addr, 2, aq, rl, false)
+        case WORD   -> mem_write_ea(addr, 4, aq, rl, false)
+        case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false)
+      };
+      let rs2_val = rGPR(rs2) in
+      switch (width) {
+        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false)
+        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false)
+        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false)
+        case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+      }
+    }
+
+(********************************************************************)
+union ast member ((bits(12)), regbits, regbits) ADDIW
+
+function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0011011) =
+  Some(ADDIW(imm, rs1, rd))
+
+function clause execute (ADDIW(imm, rs1, rd)) =
+  let (bits(64)) imm64 = EXTS(imm) in
+  let (bits(64)) result64 = imm64 + rGPR(rs1) in
+  let (bits(64)) result32 = EXTS(result64[31..0]) in
+  wGPR(rd, result32)
+
+(********************************************************************)
+union ast member ((bits(5)), regbits, regbits, sop) SHIFTW
+
+function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b0100000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
+
+function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
+    let rs1_val = (rGPR(rs1))[31..0] in
+    let result = switch(op) {
+      case RISCV_SLLI -> rs1_val >> shamt
+      case RISCV_SRLI -> rs1_val << shamt
+      case RISCV_SRAI -> shift_right_arith32(rs1_val, shamt)
+    } in
+    wGPR(rd, EXTS(result))
+
+(********************************************************************)
+union ast member (regbits, regbits, regbits, ropw) RTYPEW
+
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
+function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
+function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
+function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))
+
+function clause execute (RTYPEW(rs2, rs1, rd, op)) =
+  let rs1_val = (rGPR(rs1))[31..0] in
+  let rs2_val = (rGPR(rs2))[31..0] in
+  let (bits(32)) result = switch(op) {
+    case RISCV_ADDW -> rs1_val + rs2_val
+    case RISCV_SUBW -> rs1_val - rs2_val
+    case RISCV_SLLW -> rs1_val << (rs2_val[4..0])
+    case RISCV_SRLW -> rs1_val >> (rs2_val[4..0])
+    case RISCV_SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
+  } in
+  wGPR(rd, EXTS(result))
+
+(********************************************************************)
+union ast member (bits(4), bits(4)) FENCE
+
+function clause decode (0b0000 @ (bits(4)) pred @ (bits(4)) succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111) = Some(FENCE (pred, succ))
+
+function clause execute (FENCE(pred, succ)) = {
+  switch(pred, succ) {
+    case (0b0011, 0b0011) -> MEM_fence_rw_rw()
+    case (0b0010, 0b0011) -> MEM_fence_r_rw()
+    case (0b0010, 0b0010) -> MEM_fence_r_r()
+    case (0b0011, 0b0001) -> MEM_fence_rw_w()
+    case (0b0001, 0b0001) -> MEM_fence_w_w()
+    case _ -> not_implemented("unsupported fence")
+  }
+}
+
+(********************************************************************)
+union ast member unit FENCEI
+function clause decode (0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111) = Some(FENCEI)
+function clause execute FENCEI = MEM_fence_i()
+
+(********************************************************************)
+union ast member unit ECALL
+function clause decode (0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(ECALL ())
+function clause execute ECALL = not_implemented("ECALL is not implemented")
+
+(********************************************************************)
+union ast member unit EBREAK
+function clause decode (0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(EBREAK ())
+function clause execute EBREAK = { exit () }
+
+(********************************************************************)
+union ast member (bool, bool, regbits, word_width, regbits) LOADRES
+
+function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
+function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
+function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
+  let (bits(64)) addr = rGPR(rs1) in
+  let (bits(64)) result =
+      switch width {
+        case WORD   -> EXTS(mem_read(addr, 4, aq, rl, true))
+        case DOUBLE -> mem_read(addr, 8, aq, rl, true)
+      } in
+  wGPR(rd, result)
+
+(********************************************************************)
+union ast member (bool, bool, regbits, regbits, word_width, regbits) STORECON
+
+function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
+
+function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
+  (*(bit)*) status = if speculate_conditional_success() then 0 else 1;
+  wGPR(rd) = (bits(64)) (EXTZ([status]));
+
+  if status == 1 then () else {
+    (bits(64)) addr = rGPR(rs1);
+    switch width {
+      case WORD   -> mem_write_ea(addr, 4, aq, rl, true)
+      case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true)
+    };
+    rs2_val = rGPR(rs2);
+    switch width {
+      case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true)
+      case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, true)
+    };
+  };
+}
+
+(********************************************************************)
+union ast member (amoop, bool, bool, regbits, regbits, word_width, regbits) AMO
+
+function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
+  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+
+function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
+  (bits(64)) addr = rGPR(rs1);
+
+  switch (width) {
+    case WORD   -> mem_write_ea(addr, 4, aq & rl, rl, true)
+    case DOUBLE -> mem_write_ea(addr, 8, aq & rl, rl, true)
+  };
+
+  (bits(64)) loaded =
+    switch (width) {
+      case WORD   -> EXTS(mem_read(addr, 4, aq, aq & rl, true))
+      case DOUBLE -> mem_read(addr, 8, aq, aq & rl, true)
+    };
+  wGPR(rd, loaded);
+
+  (bits(64)) rs2_val = rGPR(rs2);
+  (bits(64)) result =
+    switch(op) {
+      case AMOSWAP -> rs2_val
+      case AMOADD  -> rs2_val + loaded
+      case AMOXOR  -> rs2_val ^ loaded
+      case AMOAND  -> rs2_val & loaded
+      case AMOOR   -> rs2_val | loaded
+
+      case AMOMIN  -> (bits(64)) (min(signed(rs2_val),   signed(loaded)))
+      case AMOMAX  -> (bits(64)) (max(signed(rs2_val),   signed(loaded)))
+      case AMOMINU -> (bits(64)) (min(unsigned(rs2_val), unsigned(loaded)))
+      case AMOMAXU -> (bits(64)) (max(unsigned(rs2_val), unsigned(loaded)))
+    };
+
+  switch (width) {
+    case WORD   -> mem_write_value(addr, 4, result[31..0], aq & rl, rl, true)
+    case DOUBLE -> mem_write_value(addr, 8, result,        aq & rl, rl, true)
+  };
+}
+
+(********************************************************************)
+
+function clause decode _ = None
+*/
+end ast
+end decode
+end execute
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index a0120e06..a593792d 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -5,6 +5,9 @@ function not_implemented message = throw(Error_not_implemented(message))
 type regval = bits(64)
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. atom('n)}
+function regbits_to_regno n = unsigned(n)
 
 /* register x0 : regval is hard-wired zero */
 register x1 : regval
@@ -59,10 +62,13 @@ val rGPR : forall 'n, 0 <= 'n < 32. regno('n) -> regval effect {rreg}
 function rGPR 0 = 0x0000000000000000
 and rGPR (r if r > 0) = reg_deref(GPRs[r - 1])
 
-val wGPR : forall 'n, 1 <= 'n < 32. (regno('n), regval) -> unit effect {wreg}
+/*val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg}*/
+val wGPR : forall 'n . (atom('n), regval) -> unit effect {wreg, escape}
 
-function wGPR (r, v) =
+function wGPR (r, v) = {
+  assert(constraint('n >= 0 & 'n < 32));
   if (r != 0) then (*GPRs[r - 1]) = v else ()
+}
 
 function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit =
   if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else ()
@@ -158,8 +164,6 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, A
 
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
-/********************************************************************/
-
 /* Ideally these would be sail builtin */
 
 /*