split RISC-V to two Sail files to make it more readable

3 files changed, 277 insertions, 201 deletions

diff --git a/risc-v/Makefile b/risc-v/Makefile
index 856a48eb..d027556e 100644
--- a/risc-v/Makefile
+++ b/risc-v/Makefile
@@ -1,6 +1,6 @@
 
 SAIL:=../src/sail.native
-SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail
+SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail
 all: lem_ast shallow
 
 lem_ast: $(SOURCES) $(SAIL)
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index ea885d90..8658ae96 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -1,177 +1,11 @@
-default Order dec
-
-typedef regval = bit[64]
-typedef regno = bit[5]
-
-register (regval) x0
-register (regval) x1
-register (regval) x2
-register (regval) x3
-register (regval) x4
-register (regval) x5
-register (regval) x6
-register (regval) x7
-register (regval) x8
-register (regval) x9
-register (regval) x10
-register (regval) x11
-register (regval) x12
-register (regval) x13
-register (regval) x14
-register (regval) x15
-register (regval) x16
-register (regval) x17
-register (regval) x18
-register (regval) x19
-register (regval) x20
-register (regval) x21
-register (regval) x22
-register (regval) x23
-register (regval) x24
-register (regval) x25
-register (regval) x26
-register (regval) x27
-register (regval) x28
-register (regval) x29
-register (regval) x30
-register (regval) x31
-
-register (bit[64]) PC
-register (bit[64]) nextPC
-
-let (vector <0, 32, inc, (register<(regval)>)>) GPRs =
-  [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14,
-    x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27,
-    x28, x29, x30, x31
-  ]
-
-function (regval) rGPR ((regno) r) = 
-    if (r == 0) then 
-        0
-    else 
-        GPRs[r]
-
-function unit wGPR((regno) r, (regval) v) =
-    if (r != 0) then
-        GPRs[r] := v
-
-function forall 'a. 'a effect { escape } not_implemented((string) message) =
-{
-  exit message;
-}
-
-function unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) =
-{
-  if (unsigned(addr) mod width != 0) then
-    exit "misaligned memory access";
-}
-
-
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire
-function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) =
-{
-  if (aq | res) then
-    check_alignment(addr, width);
-
-  switch (aq, rl, res) {
-    case (false, false, false) -> MEMr(addr, width)
-    case (true,  false, false) -> MEMr_acquire(addr, width)
-    case (false, false, true)  -> MEMr_reserved(addr, width)
-    case (true,  false, true)  -> MEMr_reserved_acquire(addr, width)
-    case (false, true,  false) -> not_implemented("load.rl is not implemented")
-    case (true,  true,  false) -> MEMr_strong_acquire(addr, width)
-    case (false, true,  true)  -> not_implemented("lr.rl is not implemented")
-    case (true,  true,  true)  -> MEMr_reserved_strong_acquire(addr, width)
-  }
-}
-
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release
-function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) =
-{
-  if (rl | con) then
-    check_alignment(addr, width);
-
-  switch (aq, rl, con) {
-    case (false, false, false) -> MEMea(addr, width)
-    case (false, true,  false) -> MEMea_release(addr, width)
-    case (false, false, true)  -> MEMea_conditional(addr, width)
-    case (false, true , true)  -> MEMea_conditional_release(addr, width)
-    case (true,  false, false) -> not_implemented("store.aq is not implemented")
-    case (true,  true,  false) -> MEMea_strong_release(addr, width)
-    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
-    case (true,  true , true)  -> MEMea_conditional_strong_release(addr, width)
-  }
-}
-
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release
-function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) =
-{
-  if (rl | con) then
-    check_alignment(addr, width);
-
-  switch (aq, rl, con) {
-    case (false, false, false) -> MEMval(addr, width, value)
-    case (false, true,  false) -> MEMval_release(addr, width, value)
-    case (false, false, true)  -> MEMval_conditional(addr, width, value)
-    case (false, true,  true)  -> MEMval_conditional_release(addr, width, value)
-    case (true,  false, false) -> not_implemented("store.aq is not implemented")
-    case (true,  true,  false) -> MEMval_strong_release(addr, width, value)
-    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
-    case (true,  true,  true)  -> MEMval_conditional_strong_release(addr, width, value)
-  }
-}
-
-val extern unit -> bool effect {exmem} speculate_conditional_success
-
-val extern unit -> unit effect { barr } MEM_fence_rw_rw
-val extern unit -> unit effect { barr } MEM_fence_r_rw
-val extern unit -> unit effect { barr } MEM_fence_rw_w
-val extern unit -> unit effect { barr } MEM_fence_w_w
-val extern unit -> unit effect { barr } MEM_fence_i
-
-(* Ideally these would be sail builtin *)
-function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
-    let (bit[128]) v128 = EXTS(v) in
-    (v128 >> shift)[63..0]
-
-function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) =
-    let (bit[64]) v64 = EXTS(v) in
-    (v64 >> shift)[31..0]
-
-typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
-typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
-typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
-typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
-typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
-typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
-typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR;
-    AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *)
-
-
-typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
-
-scattered function unit execute
 scattered typedef ast = const union
 
 val bit[32] -> option<ast> effect pure decode
-
 scattered function option<ast> decode
 
+scattered function unit execute
+
+(********************************************************************)
 union ast member ((bit[20]), regno, uop) UTYPE
 
 function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI))
@@ -185,30 +19,44 @@ function clause execute (UTYPE(imm, rd, op)) =
     } in
     wGPR(rd, ret)
 
+(********************************************************************)
 union ast member ((bit[21]), regno) JAL
+
 function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
+
 function clause execute (JAL(imm, rd)) =
     let (bit[64]) offset = EXTS(imm) in {
       nextPC :=  PC + offset;
       wGPR(rd, PC + 4);
     }
 
+(********************************************************************)
 union ast member((bit[12]), regno, regno) JALR
+
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) =
     Some(JALR(imm, rs1, rd))
+
 function clause execute (JALR(imm, rs1, rd)) =
     let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in {
       nextPC := newPC[63..1] : 0b0;
       wGPR(rd, PC + 4);
     }
 
+(********************************************************************)
 union ast member ((bit[13]), regno, regno, bop) BTYPE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
+
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) =
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
 
 function clause execute (BTYPE(imm, rs2, rs1, op)) =
   let rs1_val = rGPR(rs1) in
@@ -224,13 +72,16 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
   if (taken) then
       nextPC := PC + EXTS(imm)
 
+(********************************************************************)
 union ast member ((bit[12]), regno, regno, iop) ITYPE
+
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI))
+
 function clause execute (ITYPE (imm, rs1, rd, op)) =
   let rs1_val = rGPR(rs1) in
   let imm64 = (bit[64]) (EXTS(imm)) in
@@ -244,10 +95,13 @@ function clause execute (ITYPE (imm, rs1, rd, op)) =
   } in
   wGPR(rd, result)
 
+(********************************************************************)
 union ast member ((bit[6]), regno, regno, sop) SHIFTIOP
+
 function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI))
 function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI))
 function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI))
+
 function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = 
     let rs1_val = rGPR(rs1) in
     let result = switch(op) {
@@ -257,7 +111,9 @@ function clause execute (SHIFTIOP(shamt, rs1, rd, op)) =
     } in
     wGPR(rd, result)
 
+(********************************************************************)
 union ast member (regno, regno, regno, rop) RTYPE
+
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD))
 function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB))
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL))
@@ -268,6 +124,7 @@ function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno)
 function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA))
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR))
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND))
+
 function clause execute (RTYPE(rs2, rs1, rd, op)) =
   let rs1_val = rGPR(rs1) in
   let rs2_val = rGPR(rs2) in
@@ -285,7 +142,9 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, result)
 
+(********************************************************************)
 union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD
+
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
@@ -293,6 +152,7 @@ function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b000
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
+
 function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
     let (bit[64]) result = if unsigned then 
@@ -311,11 +171,18 @@ function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
         } in
     wGPR(rd, result)
 
+(********************************************************************)
 union ast member ((bit[12]), regno, regno, word_width, bool, bool) STORE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false))
+
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) =
+  Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) =
+  Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) =
+  Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) =
+  Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false))
+
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
       switch (width) {
@@ -333,18 +200,25 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
       }
     }
 
+(********************************************************************)
 union ast member ((bit[12]), regno, regno) ADDIW
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd))
+
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) =
+  Some(ADDIW(imm, rs1, rd))
+
 function clause execute (ADDIW(imm, rs1, rd)) =
   let (bit[64]) imm64 = EXTS(imm) in
   let (bit[64]) result64 = imm64 + rGPR(rs1) in
   let (bit[64]) result32 = EXTS(result64[31..0]) in
   wGPR(rd, result32)
 
+(********************************************************************)
 union ast member ((bit[5]), regno, regno, sop) SHIFTW
+
 function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI))
 function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI))
 function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI))
+
 function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
     let rs1_val = (rGPR(rs1))[31..0] in
     let result = switch(op) {
@@ -354,12 +228,15 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) =
     } in
     wGPR(rd, EXTS(result))
 
+(********************************************************************)
 union ast member (regno, regno, regno, ropw) RTYPEW
+
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW))
 function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW))
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW))
 function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW))
 function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, 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
@@ -372,8 +249,11 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, EXTS(result))
 
+(********************************************************************)
 union ast member (bit[4], bit[4]) FENCE
+
 function clause decode (0b0000 : (bit[4]) pred : (bit[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()
@@ -384,19 +264,24 @@ function clause execute (FENCE(pred, succ)) = {
   }
 }
 
+(********************************************************************)
 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, regno, word_width, regno) LOADRES
+
 function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
 function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
@@ -408,9 +293,14 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
       } in
   wGPR(rd, result)
 
+(********************************************************************)
 union ast member (bool, bool, regno, regno, word_width, regno) STORECON
-function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
-function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
+
+function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
+function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) 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) := (bit[64]) (EXTZ([status]));
@@ -429,26 +319,45 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   };
 }
 
+(********************************************************************)
 union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO
 
-function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) =
+  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
 
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   (bit[64]) addr := rGPR(rs1);
@@ -486,6 +395,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   };
 }
 
+(********************************************************************)
+
 function clause decode _ = None
 
 end ast
diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail
new file mode 100644
index 00000000..a11d5561
--- /dev/null
+++ b/risc-v/riscv_types.sail
@@ -0,0 +1,165 @@
+default Order dec
+
+function forall 'a. 'a effect { escape } not_implemented((string) message) =
+  exit message
+
+typedef regval = bit[64]
+typedef regno = bit[5]
+
+(* register (regval) x0 is hard-wired zero *)
+register (regval) x1
+register (regval) x2
+register (regval) x3
+register (regval) x4
+register (regval) x5
+register (regval) x6
+register (regval) x7
+register (regval) x8
+register (regval) x9
+register (regval) x10
+register (regval) x11
+register (regval) x12
+register (regval) x13
+register (regval) x14
+register (regval) x15
+register (regval) x16
+register (regval) x17
+register (regval) x18
+register (regval) x19
+register (regval) x20
+register (regval) x21
+register (regval) x22
+register (regval) x23
+register (regval) x24
+register (regval) x25
+register (regval) x26
+register (regval) x27
+register (regval) x28
+register (regval) x29
+register (regval) x30
+register (regval) x31
+
+register (bit[64]) PC
+register (bit[64]) nextPC
+
+let (vector <1, 31, inc, (register<(regval)>)>) GPRs =
+  [ (* x0, *) x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14,
+    x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27,
+    x28, x29, x30, x31
+  ]
+
+function (regval) rGPR ((regno) r) =
+    if (r == 0) then
+        0
+    else
+        GPRs[r]
+
+function unit wGPR((regno) r, (regval) v) =
+    if (r != 0) then
+        GPRs[r] := v
+
+function unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) =
+  if (unsigned(addr) mod width != 0) then
+    exit "misaligned memory access"
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire
+
+function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) =
+{
+  if (aq | res) then
+    check_alignment(addr, width);
+
+  switch (aq, rl, res) {
+    case (false, false, false) -> MEMr(addr, width)
+    case (true,  false, false) -> MEMr_acquire(addr, width)
+    case (false, false, true)  -> MEMr_reserved(addr, width)
+    case (true,  false, true)  -> MEMr_reserved_acquire(addr, width)
+    case (false, true,  false) -> not_implemented("load.rl is not implemented")
+    case (true,  true,  false) -> MEMr_strong_acquire(addr, width)
+    case (false, true,  true)  -> not_implemented("lr.rl is not implemented")
+    case (true,  true,  true)  -> MEMr_reserved_strong_acquire(addr, width)
+  }
+}
+
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release
+
+function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) =
+{
+  if (rl | con) then
+    check_alignment(addr, width);
+
+  switch (aq, rl, con) {
+    case (false, false, false) -> MEMea(addr, width)
+    case (false, true,  false) -> MEMea_release(addr, width)
+    case (false, false, true)  -> MEMea_conditional(addr, width)
+    case (false, true , true)  -> MEMea_conditional_release(addr, width)
+    case (true,  false, false) -> not_implemented("store.aq is not implemented")
+    case (true,  true,  false) -> MEMea_strong_release(addr, width)
+    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
+    case (true,  true , true)  -> MEMea_conditional_strong_release(addr, width)
+  }
+}
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release
+
+function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) =
+{
+  if (rl | con) then
+    check_alignment(addr, width);
+
+  switch (aq, rl, con) {
+    case (false, false, false) -> MEMval(addr, width, value)
+    case (false, true,  false) -> MEMval_release(addr, width, value)
+    case (false, false, true)  -> MEMval_conditional(addr, width, value)
+    case (false, true,  true)  -> MEMval_conditional_release(addr, width, value)
+    case (true,  false, false) -> not_implemented("store.aq is not implemented")
+    case (true,  true,  false) -> MEMval_strong_release(addr, width, value)
+    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
+    case (true,  true,  true)  -> MEMval_conditional_strong_release(addr, width, value)
+  }
+}
+
+val extern unit -> bool effect {exmem} speculate_conditional_success
+
+val extern unit -> unit effect { barr } MEM_fence_rw_rw
+val extern unit -> unit effect { barr } MEM_fence_r_rw
+val extern unit -> unit effect { barr } MEM_fence_rw_w
+val extern unit -> unit effect { barr } MEM_fence_w_w
+val extern unit -> unit effect { barr } MEM_fence_i
+
+typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
+typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
+typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
+typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
+typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
+typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
+typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR;
+    AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *)
+
+typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
+
+(********************************************************************)
+
+(* Ideally these would be sail builtin *)
+function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
+    let (bit[128]) v128 = EXTS(v) in
+    (v128 >> shift)[63..0]
+
+function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) =
+    let (bit[64]) v64 = EXTS(v) in
+    (v64 >> shift)[31..0]