work on integrating risc-v model with rmem (incomplete).

23 files changed, 1069 insertions, 17 deletions

diff --git a/risc-v/Makefile b/risc-v/Makefile
new file mode 100644
index 00000000..2f6af138
--- /dev/null
+++ b/risc-v/Makefile
@@ -0,0 +1,13 @@
+
+SAIL:=../src/sail.native
+
+all: lem_ast shallow
+
+lem_ast: riscv.sail $(SAIL)
+	$(SAIL) -lem_ast $<
+
+shallow: riscv.sail $(SAIL)
+	$(SAIL) -lem_lib Riscv_extras_embed -lem $<
+
+clean:
+	rm -f riscv.lem riscv_embed*.lem
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
new file mode 100644
index 00000000..ee7cb3e1
--- /dev/null
+++ b/risc-v/hgen/ast.hgen
@@ -0,0 +1,13 @@
+| `RISCVThreadStart
+| `RISCVUTYPE of bit20 * reg * riscvUop
+| `RISCVJAL   of bit20 * reg
+| `RISCVJALR  of bit12 * reg * reg
+| `RISCVBType of bit12 * reg * reg * riscvBop
+| `RISCVIType of bit12 * reg * reg * riscvIop
+| `RISCVShiftIop of bit6 * reg * reg * riscvSop
+| `RISCVRType of reg * reg * reg * riscvRop
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth
+| `RISCVStore of bit12 * reg * reg * wordWidth
+| `RISCVADDIW of bit12 * reg * reg
+| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
+| `RISCVRTYPEW of reg * reg * reg * riscvRopw
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
new file mode 100644
index 00000000..03318805
--- /dev/null
+++ b/risc-v/hgen/fold.hgen
@@ -0,0 +1,13 @@
+| `RISCVThreadStart               -> (y_reg, y_sreg)
+| `RISCVUTYPE (_, r0, _)          -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0)               -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1)          -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVShiftIop (_, r0, r1, _)   -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRType (r0, r1, r2, _)     -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVLoad (_, r0, r1, _, _)    -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVADDIW (_, r0, r1)         -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVSHIFTW (_, r0, r1, _)     -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRTYPEW (r0, r1, r2, _)    -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 00000000..e614b714
--- /dev/null
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,122 @@
+(*| `MIPSThreadStart ->
+    SYSCALL_THREAD_START
+
+| `MIPSStopFetching ->
+    ImplementationDefinedStopFetching0
+
+(* Note different argument order, which reflects difference
+   between instruction encoding and asm format  *)
+| `MIPSRType (op, rd, rs, rt) ->
+    (translate_rtype_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_reg "rd" rd
+       )
+      
+
+(* Note different argument order similar to above *)
+| `MIPSIType (op, rt, rs, imm) ->
+    (translate_itype_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_imm16 "imm" imm
+       )
+      
+
+| `MIPSShiftI (op, rd, rt, sa) ->
+    (translate_shifti_op op)
+      (
+      translate_reg "rt" rt,
+      translate_reg "rd" rd,
+      translate_imm5 "sa" sa
+       )
+      
+
+| `MIPSShiftV (op, rd, rt, rs) ->
+    (translate_shiftv_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_reg "rd" rd
+      )
+      
+
+| `MIPSMulDiv (op, rs, rt) ->
+    (translate_muldiv_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt
+      )
+      
+
+| `MIPSMFHiLo (op, rs) ->
+    (translate_mfhilo_op op)
+      (
+      translate_reg "rs" rs
+      )
+      
+| `MIPSLUI (rt, imm) ->
+  LUI
+      (
+      translate_reg "rt" rt,
+      translate_imm16 "imm" imm
+      )
+      
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+  Load
+      (
+      translate_wordsize "width" width,
+      translate_bool "signed" signed,
+      translate_bool "linked" linked,
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSStore (width, conditional, base, rt, offset) ->
+  Store
+      (
+      translate_wordsize "width" width,
+      translate_bool "conditional" conditional,
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+  (translate_lslr_op store double left)
+      (
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSSYNC -> SYNC
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+  BEQ
+  (translate_reg "rs" rs,
+   translate_reg "rt" rt,
+   translate_imm16 "offset" offset,
+   translate_bool "ne" ne,
+   translate_bool "likely" likely
+   ) 
+
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+  BCMPZ
+  (translate_reg "rs" rs,
+   translate_imm16 "offset" offset,
+   translate_cmp "cmp" cmp,
+   translate_bool "link" link,
+   translate_bool "likely" likely
+   ) 
+| `MIPSJ (offset) ->
+  J (translate_imm26 "offset" offset) 
+| `MIPSJAL (offset) ->
+  JAL (translate_imm26 "offset" offset) 
+| `MIPSJR(rd) ->
+  JR (translate_reg "rd" rd) 
+| `MIPSJALR(rd, rs) ->
+  JALR (translate_reg "rd" rd, translate_reg "rs" rs) 
+*)
\ No newline at end of file
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 00000000..1c925e2b
--- /dev/null
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,121 @@
+let is_inc = false
+(*
+let translate_rtype_op op  = uppercase (pp_rtype_op op)
+
+let translate_rtype_op op x = match op with
+  | MIPSROpADD    -> ADD x
+  | MIPSROpADDU   -> ADDU x
+  | MIPSROpAND    -> AND x
+  | MIPSROpDADD   -> DADD x
+  | MIPSROpDADDU  -> DADDU x
+  | MIPSROpDSUB   -> DSUB x
+  | MIPSROpDSUBU  -> DSUBU x
+  | MIPSROpMOVN   -> MOVN x
+  | MIPSROpMOVZ   -> MOVZ x
+  | MIPSROpMUL    -> MUL x
+  | MIPSROpNOR    -> NOR x
+  | MIPSROpOR     -> OR x
+  | MIPSROpSLT    -> SLT x 
+  | MIPSROpSLTU   -> SLTU x
+  | MIPSROpSUB    -> SUB x
+  | MIPSROpSUBU   -> SUBU x
+  | MIPSROpXOR    -> XOR x
+
+let translate_itype_op op x = match op with
+  | MIPSIOpADDI   -> ADDI x
+  | MIPSIOpADDIU  -> ADDIU x
+  | MIPSIOpANDI   -> ANDI x
+  | MIPSIOpDADDI  -> DADDI x
+  | MIPSIOpDADDIU -> DADDIU x
+  | MIPSIOpORI    -> ORI x
+  | MIPSIOpSLTI   -> SLTI x
+  | MIPSIOpSLTIU  -> SLTIU x
+  | MIPSIOpXORI   -> XORI x
+
+let translate_shifti_op op x = match op with
+  | MIPSDSLL   -> DSLL x 
+  | MIPSDSLL32 -> DSLL32 x
+  | MIPSDSRA   -> DSRA x
+  | MIPSDSRA32 -> DSRA32 x
+  | MIPSDSRL   -> DSRL x
+  | MIPSDSRL32 -> DSRL32 x
+  | MIPSSLL    -> SLL x
+  | MIPSSRA    -> SRA x 
+  | MIPSSRL    -> SRL x 
+
+let translate_shiftv_op op x = match op with
+  | MIPSDSLLV -> DSLLV x
+  | MIPSDSRAV -> DSRAV x
+  | MIPSDSRLV -> DSRLV x
+  | MIPSSLLV  -> SLLV x 
+  | MIPSSRAV  -> SRAV x 
+  | MIPSSRLV  -> SRLV x 
+
+let translate_muldiv_op op x = match op with
+  | MIPSDDIV   -> DDIV x  
+  | MIPSDDIVU  -> DDIVU x 
+  | MIPSDIV    -> DIV x   
+  | MIPSDIVU   -> DIVU x  
+  | MIPSDMULT  -> DMULT x 
+  | MIPSDMULTU -> DMULTU x
+  | MIPSMADD   -> MADD x  
+  | MIPSMADDU  -> MADDU x 
+  | MIPSMSUB   -> MSUB x  
+  | MIPSMSUBU  -> MSUBU x 
+  | MIPSMULT   -> MULT x  
+  | MIPSMULTU  -> MULTU x 
+
+let translate_mfhilo_op op x = match op with
+  | MIPSMFHI -> MFHI x
+  | MIPSMFLO -> MFLO x
+  | MIPSMTHI -> MTHI x
+  | MIPSMTLO -> MTLO x
+
+let translate_load_op width signed linked = uppercase (pp_load_op width signed linked)
+
+let translate_store_op width conditional  = uppercase (pp_store_op width conditional)
+
+let translate_lslr_op store double left x = match (store,double,left) with
+  | (false, false, true ) -> LWL x
+  | (false, false, false) -> LWR x
+  | (false, true , true ) -> LDL x
+  | (false, true , false) -> LDR x
+  | (true , false, true ) -> SWL x
+  | (true , false, false) -> SWR x
+  | (true , true , true ) -> SDL x
+  | (true , true , false) -> SDR x
+
+let translate_beq_op ne likely            = uppercase (pp_beq_op ne likely)
+
+let translate_bcmpz_op cmp link likely    = uppercase (pp_bcmpz_op cmp link likely)
+
+
+let translate_reg name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value))
+
+let translate_imm26 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value)
+let translate_imm16 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,Nat_big_num.of_int value)
+let translate_imm5 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
+let translate_bool name = function
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
+
+let translate_wordsize _ = function
+ | MIPSByte -> Mips_embed_types.B2
+ | MIPSHalf -> Mips_embed_types.H
+ | MIPSWord -> Mips_embed_types.W
+ | MIPSDouble -> Mips_embed_types.D
+
+let translate_cmp _ = function
+  | MIPS_EQ  -> EQ'
+  | MIPS_NE  -> NE
+  | MIPS_GE  -> GE
+  | MIPS_GEU -> GEU
+  | MIPS_GT  -> GT'
+  | MIPS_LE  -> LE
+  | MIPS_LT  -> LT'
+  | MIPS_LTU -> LTU
+*)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
new file mode 100644
index 00000000..a75eef9f
--- /dev/null
+++ b/risc-v/hgen/lexer.hgen
@@ -0,0 +1,60 @@
+"lwu"   , UTYPE { op=RSICVLUI   };
+"auipc" , UTYPE { op=RSICVAUIPC };
+
+"jal",  JAL;
+"jalr", JALR;
+
+"beq",  BTYPE {op=RISCVBEQ};
+"bne",  BTYPE {op=RISCVBNE};
+"blt",  BTYPE {op=RISCVBLT};
+"bge",  BTYPE {op=RISCVBGE};
+"bltu", BTYPE {op=RISCVBLTU};
+"bgeu", BTYPE {op=RISCVBGEU};
+
+"addi",  ITYPE {op=RISCVADDI};
+"stli",  ITYPE {op=RISCVSTLI};
+"sltiu", ITYPE {op=RISCVSLTIU};
+"xori",  ITYPE {op=RISCVXORI};
+"ori",   ITYPE {op=RISCVORI};
+"andi",  ITYPE {op=RISCVANDI};
+
+"slli", SHIFTIOP{op=RISCVSLLI};
+"srli", SHIFTIOP{op=RISCVSRLI};
+"srai", SHIFTIOP{op=RISCVSRAI};
+
+"add",  RTYPE{op=RISCVADD};
+"sub",  RTYPE{op=RISCVSUB};
+"sll",  RTYPE{op=RISCVSLL};
+"slt",  RTYPE{op=RISCVSLT};
+"sltu", RTYPE{op=RISCVSLT};
+"xor",  RTYPE{op=RISCVXOR};
+"srl",  RTYPE{op=RISCVSRL};
+"sra",  RTYPE{op=RISCVSRA};
+"or",   RTYPE{op=RISCVOR};
+"and",  RTYPE{op=RISCVAND};
+
+"lb",  LOAD{unsigned=false; width=RISCBYTE};
+"lbu", LOAD{unsigned=true;  width=RISCBYTE};
+"lh",  LOAD{unsigned=false; width=RISCVHALF};
+"lhu", LOAD{unsigned=true;  width=RISCVHALF};
+"lw",  LOAD{unsigned=false; width=RISCVWORD};
+"lwu", LOAD{unsigned=true;  width=RISCVWORD};
+"ld",  LOAD{unsigned=false; width=RISCVDOUBLE};
+
+"sb", STORE{width=RISCBYTE};
+"sh", STORE{width=RISCVHALF};
+"sw", STORE{width=RISCVWORD};
+"sd", STORE{width=RISCVDOUBLE};
+
+"addiw", ADDIW;
+
+"slliw", SHIFTW{op=RISCVSLL};
+"srliw", SHIFTW{op=RISCVSRL};
+"sraiw", SHIFTW{op=RISCVSRA};
+
+"addw", RTYPEW{op=RISCVADDW};
+"subw", RTYPEW{op=RISCVSUBW};
+"sslw", RTYPEW{op=RISCVSLLW};
+"srlw", RTYPEW{op=RISCVSRLW};
+"sraw", RTYPEW{op=RISCVSRAW};
+
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
new file mode 100644
index 00000000..ff14c428
--- /dev/null
+++ b/risc-v/hgen/map.hgen
@@ -0,0 +1,12 @@
+| `RISCVUTYPE (x, r0, y)          -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0)               -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1)          -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y)      -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y)      -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `RISCVShiftIop (x, r0, r1, y)   -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
+| `RISCVRType (r0, r1, r2, y)     -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
+| `RISCVLoad (x, r0, r1, y, z)    -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z)
+| `RISCVStore (x, r0, r1, y)      -> `RISCVStore (x, map_reg r0, map_reg r1, y)
+| `RISCVADDIW (x, r0, r1)         -> `RISCVADDIW (x, map_reg r0, map_reg r1)
+| `RISCVSHIFTW (x, r0, r1, y)     -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
+| `RISCVRTYPEW (r0, r1, r2, x)    -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
new file mode 100644
index 00000000..ba4dcac7
--- /dev/null
+++ b/risc-v/hgen/parser.hgen
@@ -0,0 +1,24 @@
+| UTYPE reg COMMA NUM
+  { `RISCVUTYPE($4, $2, $1.o) }
+| JAL reg COMMA NUM
+  { `RISCVJAL($4, $2) }
+| JALR reg COMMA reg COMMA NUM
+  { `RISCVJALR($6, $4, $2) }
+| BTYPE reg COMMA reg COMMA NUM
+  { `RISCVBType($6, $4, $2, $1.op) }
+| ITYPE reg COMMA reg COMMA NUM
+  { `RISCVIType(o$6, $4, $2, $1.op) }
+| SHIFTIOP reg COMMA reg COMMA NUM
+  { `RISCVShiftIop($6, $4, $2, $1.op) }
+| RTYPE reg COMMA reg COMMA reg
+  { `RISCVRType ($6, $3, $2, $1.op) }
+| LOAD reg COMMA NUM LPAR reg RPAR
+  { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) }
+| STORE reg COMMA NUM LPAR reg RPAR
+  { `RISCVStore($4, $6, $2, $1.width) } (* reg order? *)
+| ADDIW reg COMMA reg COMMA NUM
+  { `RISCVADDIW ($6, $4, $2) }
+| SHIFTW reg COMMA reg COMMA NUM
+  { `RISCVSHIFTW ($6, $4, $2, $1.op) }
+| RTYPEW reg COMMA reg COMMA reg
+  { `RISCVRTYPEW ($6, $4, $2, $1.op) }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
new file mode 100644
index 00000000..f8cb0e30
--- /dev/null
+++ b/risc-v/hgen/pretty.hgen
@@ -0,0 +1,12 @@
+| `RISCVUTYPE(imm, rd, op)        -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm
+| `RISCVJAL(imm, rd)              -> sprintf "jal  %s, %d" (pp_reg rd) imm
+| `RISCVJALR(imm, rs, rd)         -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVBType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVIType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRType (rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs)
+| `RISCVStore(imm, rs, rd, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rd) imm (pp_reg rs)
+| `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
diff --git a/risc-v/hgen/regs_out_in.hgen b/risc-v/hgen/regs_out_in.hgen
new file mode 100644
index 00000000..8e1fd093
--- /dev/null
+++ b/risc-v/hgen/regs_out_in.hgen
@@ -0,0 +1,5 @@
+(* for each instruction instance, identify the role of the registers
+   and possible branching: (outputs, inputs, voidstars, branch) *)
+
+| `MIPSAdd ->
+      ([], [], [], [Next])
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
new file mode 100644
index 00000000..8064aa19
--- /dev/null
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -0,0 +1,12 @@
+| ("UTYPE", [imm; rd; op])        -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg  rd)
+| ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ("ITYPE", [imm; rs1; rd; op])   -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPE", [rs2; rs1; rd; op])   -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| ("LOAD", [imm; rs; rd; unsigned; width]) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| ("ADDIW", [imm; rs; rd])        -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("SHIFTW", [imm; rs; rd; op])   -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPEW", [rs2; rs1; rd; op])  -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 00000000..9473d011
--- /dev/null
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,99 @@
+(*| SYSCALL_THREAD_START -> `MIPSThreadStart
+| (ADD    (rs, rt, rd)) -> `MIPSRType (MIPSROpADD   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (ADDU   (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (AND    (rs, rt, rd)) -> `MIPSRType (MIPSROpAND   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADD   (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADDU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUB   (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUBU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVN   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVZ   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MUL    (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (NOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (OR     (rs, rt, rd)) -> `MIPSRType (MIPSROpOR    , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLT    (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLTU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUB    (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUBU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (XOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+
+| (ADDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ADDIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ANDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (DADDI  (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ORI    (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI   ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (SLTI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (SLTIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (XORI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+
+| (DSLL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSLL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SLL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRA     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+
+| DSLLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRAV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SLLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRAV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+
+| DDIV   (rs, rt) -> `MIPSMulDiv (MIPSDDIV   , (translate_out_ireg rs), (translate_out_ireg rt))
+| DDIVU  (rs, rt) -> `MIPSMulDiv (MIPSDDIVU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIV    (rs, rt) -> `MIPSMulDiv (MIPSDIV    , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIVU   (rs, rt) -> `MIPSMulDiv (MIPSDIVU   , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULT  (rs, rt) -> `MIPSMulDiv (MIPSDMULT  , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADD   (rs, rt) -> `MIPSMulDiv (MIPSMADD   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADDU  (rs, rt) -> `MIPSMulDiv (MIPSMADDU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUB   (rs, rt) -> `MIPSMulDiv (MIPSMSUB   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUBU  (rs, rt) -> `MIPSMulDiv (MIPSMSUBU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULT   (rs, rt) -> `MIPSMulDiv (MIPSMULT   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULTU  (rs, rt) -> `MIPSMulDiv (MIPSMULTU  , (translate_out_ireg rs), (translate_out_ireg rt))
+
+| MFHI  (rs)  -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs))
+| MFLO  (rs)  -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs))
+| MTHI  (rs)  -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs))
+| MTLO  (rs)  -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs))
+
+| LUI  (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm))
+| Load (width, signed, linked, base, rt, offset) ->
+  `MIPSLoad (
+     (translate_out_wordWidth width), 
+     (translate_out_bool signed),
+     (translate_out_bool linked),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16 offset)
+   )
+| Store (width, conditional, base, rt, offset) ->
+  `MIPSStore (
+     (translate_out_wordWidth width), 
+     (translate_out_bool conditional),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16  offset)
+   )
+| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SYNC -> `MIPSSYNC
+| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely))
+| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+| J (offset) -> `MIPSJ (translate_out_imm26 offset)
+| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset)
+| JR (rd) -> `MIPSJR (translate_out_ireg rd)
+| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
+
+*)
\ No newline at end of file
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 00000000..2c2efd8e
--- /dev/null
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,40 @@
+(*let translate_out_big_bit = Sail_values.unsigned
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_imm26 imm = translate_out_int imm
+
+let translate_out_imm16 imm = translate_out_int imm
+let translate_out_simm16 imm = translate_out_signed_int imm 16
+
+let translate_out_imm5 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | Sail_values.B1  -> true
+  | Sail_values.B0 -> false
+  | _ -> failwith "translate_out_bool Undef"
+
+
+let translate_out_wordWidth = function
+    | Mips_embed_types.B2 -> MIPSByte
+    | Mips_embed_types.H -> MIPSHalf
+    | Mips_embed_types.W -> MIPSWord
+    | Mips_embed_types.D -> MIPSDouble
+
+let translate_out_cmp = function
+    | Mips_embed_types.EQ' -> MIPS_EQ  (* equal *)
+    | Mips_embed_types.NE -> MIPS_NE  (* not equal *)
+    | Mips_embed_types.GE -> MIPS_GE  (* signed greater than or equal *)
+    | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) 
+    | Mips_embed_types.GT' -> MIPS_GT  (* signed strictly greater than *) 
+    | Mips_embed_types.LE -> MIPS_LE  (* signed less than or equal *) 
+    | Mips_embed_types.LT' -> MIPS_LT  (* signed strictly less than *) 
+    | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) 
+*)
\ No newline at end of file
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
new file mode 100644
index 00000000..cc993ae3
--- /dev/null
+++ b/risc-v/hgen/token_types.hgen
@@ -0,0 +1,12 @@
+type token_UTYPE    = {op : riscvUop }
+type token_JAL      = unit
+type token_JALR     = unit
+type token_BType    = {op : riscvBop }
+type token_IType    = {op : riscvIop }
+type token_ShiftIop = {op : riscvSop }
+type token_RTYPE    = {op : riscvRop }
+type token_Load     = {unsigned: bool; width : wordWidth }
+type token_Store    = {width : wordWidth }
+type token_ADDIW    = unit
+type token_SHIFTW   = {op : riscvSop }
+type token_RTYPEW   = {op : riscvRopw }
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
new file mode 100644
index 00000000..0a874b81
--- /dev/null
+++ b/risc-v/hgen/tokens.hgen
@@ -0,0 +1,13 @@
+%token <RISCVHGenBase.token_UTYPE>    UTYPE   
+%token <RISCVHGenBase.token_JAL>      JAL     
+%token <RISCVHGenBase.token_JALR>     JALR    
+%token <RISCVHGenBase.token_BType>    BTYPE   
+%token <RISCVHGenBase.token_IType>    ITYPE   
+%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
+%token <RISCVHGenBase.token_RTYPE>    RTYPE   
+%token <RISCVHGenBase.token_Load>     LOAD    
+%token <RISCVHGenBase.token_Store>    STORE   
+%token <RISCVHGenBase.token_ADDIW>    ADDIW   
+%token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
+%token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
+
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
new file mode 100644
index 00000000..3b825af2
--- /dev/null
+++ b/risc-v/hgen/trans_sail.hgen
@@ -0,0 +1,105 @@
+| `RISCVUTYPE(imm, rd, op) -> 
+    ("UTYPE",
+      [
+      translate_imm20 "imm" imm;
+      translate_reg "rd" rd;
+      translate_uop "op" op;
+       ],
+      [])
+| `RISCVJAL(imm, rd) -> 
+   ("JAL",
+    [
+      translate_imm20 "imm" imm;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVJALR(imm, rs, rd) -> 
+   ("JALR",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rd;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVBType(imm, rs2, rs1, op)  -> 
+   ("BTYPE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_bop "op" op;
+    ],
+    [])
+| `RISCVIType(imm, rs1, rd, op)  -> 
+   ("ITYPE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_iop "op" op;
+    ],
+    [])
+| `RISCVShiftIop(imm, rs, rd, op) -> 
+   ("SHIFTIOP",
+    [
+      translate_imm6 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRType (rs2, rs1, rd, op)  -> 
+   ("RTYPE",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_rop "op" op;
+    ],
+    [])
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> 
+   ("LOAD",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_bool "unsigned" unsigned;
+      translate_width "width" width;
+    ],
+    [])
+| `RISCVStore(imm, rs, rd, width) -> 
+   ("LOAD",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_width "width" width;
+    ],
+    [])
+| `RISCVADDIW(imm, rs, rd)        -> 
+   ("ADDIW",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVSHIFTW(imm, rs, rd, op)   -> 
+   ("SHIFTW",
+    [
+      translate_imm5 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> 
+   ("RTYPEW",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_ropw "op" op;
+    ],
+    [])
+
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
new file mode 100644
index 00000000..e31b11f8
--- /dev/null
+++ b/risc-v/hgen/types.hgen
@@ -0,0 +1,116 @@
+type bit20 = int
+type bit12 = int
+type bit6  = int
+type bit5  = int
+
+type riscvUop =  (* upper immediate ops *)
+| RISCVLUI
+| RISCVAUIPC
+
+let pp_riscv_uop = function
+| RISCVLUI   -> "lui"
+| RISCVAUIPC -> "auipc"
+
+
+type riscvBop =  (* branch ops *)
+| RISCVBEQ 
+| RISCVBNE
+| RISCVBLT
+| RISCVBGE
+| RISCVBLTU
+| RISCVBGEU
+
+let pp_riscv_bop = function
+| RISCVBEQ  -> "beq"
+| RISCVBNE  -> "bne"
+| RISCVBLT  -> "blt"
+| RISCVBGE  -> "bge"
+| RISCVBLTU -> "bltu"
+| RISCVBGEU -> "bgeu"
+
+type riscvIop = (* immediate ops *)
+| RISCVADDI
+| RISCVSLTI
+| RISCVSLTIU
+| RISCVXORI
+| RISCVORI
+| RISCVANDI
+
+let pp_riscv_iop = function
+| RISCVADDI  -> "addi"
+| RISCVSLTI  -> "slti"
+| RISCVSLTIU -> "sltiu"
+| RISCVXORI  -> "xori"
+| RISCVORI   -> "ori"
+| RISCVANDI  -> "andi"
+
+type riscvSop = (* shift ops *)
+| RISCVSLLI
+| RISCVSRLI
+| RISCVSRAI
+
+let pp_riscv_sop = function
+| RISCVSLLI -> "slli"
+| RISCVSRLI -> "srli"
+| RISCVSRAI -> "srai"
+
+type riscvRop = (* reg-reg ops *)
+| RISCVADD
+| RISCVSUB
+| RISCVSLL
+| RISCVSLT 
+| RISCVSLTU
+| RISCVXOR
+| RISCVSRL
+| RISCVSRA
+| RISCVOR
+| RISCVAND
+
+let pp_riscv_rop = function
+| RISCVADD  -> "add"
+| RISCVSUB  -> "sub"
+| RISCVSLL  -> "sll"
+| RISCVSLT  -> "slt"
+| RISCVSLTU -> "sltu"
+| RISCVXOR  -> "xor"
+| RISCVSRL  -> "srl"
+| RISCVSRA  -> "sra"
+| RISCVOR   -> "or"
+| RISCVAND  -> "and"
+
+type riscvRopw = (* reg-reg 32-bit ops *)
+| RISCVADDW
+| RISCVSUBW
+| RISCVSLLW
+| RISCVSRLW
+| RISCVSRAW
+
+let pp_riscv_ropw = function
+| RISCVADDW -> "addw"
+| RISCVSUBW -> "subw"
+| RISCVSLLW -> "sllw"
+| RISCVSRLW -> "srlw"
+| RISCVSRAW -> "sraw"
+
+type wordWidth = 
+  | RISCVBYTE
+  | RISCVHALF
+  | RISCVWORD
+  | RISCVDOUBLE
+
+let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with
+  | (false, RISCVBYTE)    -> "lb"
+  | (true,  RISCVBYTE)    -> "lbu"
+  | (false, RISCVHALF)    -> "lh"
+  | (true,  RISCVHALF)    -> "lhu"
+  | (false, RISCVWORD)    -> "lw"
+  | (true,  RISCVWORD)    -> "lwu"
+  | (_, RISCVDOUBLE)      -> "ld"
+  | _                          -> failwith "unexpected load op"
+
+let pp_riscv_store_op width = match width with
+| RISCVBYTE -> "sb"
+| RISCVHALF -> "sh"
+| RISCVWORD -> "sw"
+| RISCVDOUBLE -> "sd"
+| _ -> failwith "unexpected store op"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
new file mode 100644
index 00000000..99d3d375
--- /dev/null
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -0,0 +1,78 @@
+let translate_out_big_bit = function
+  | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits
+  | _ -> assert false
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm12 imm = translate_out_signed_int imm 12
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | (name, Bit, [Bitc_one])  -> true
+  | (name, Bit, [Bitc_zero]) -> false
+  | _ -> assert false
+
+let translate_out_enum (name,_,bits) =
+    Nat_big_num.to_int (IInt.integer_of_bit_list bits)
+
+let translate_out_wordWidth w = 
+    match translate_out_enum w with
+    | 0 -> RISCVBYTE
+    | 1 -> RISCVHALF
+    | 2 -> RISCVWORD
+    | 3 -> RISCVDOUBLE
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_uop op = match translate_out_enum op with
+    | 0 -> RISCVLUI
+    | 1 -> RISCVAUIPC
+    | _ -> failwith "Unknown uop in sail translate out"
+
+let translate_out_bop op = match translate_out_enum op with
+| 0 -> RISCVBEQ 
+| 1 -> RISCVBNE 
+| 2 -> RISCVBLT 
+| 3 -> RISCVBGE 
+| 4 -> RISCVBLTU
+| 5 -> RISCVBGEU
+
+let translate_out_iop op = match translate_out_enum op with
+| 0 -> RISCVADDI 
+| 1 -> RISCVSLTI 
+| 2 -> RISCVSLTIU
+| 3 -> RISCVXORI 
+| 4 -> RISCVORI  
+| 5 -> RISCVANDI 
+
+let translate_out_sop op = match translate_out_enum op with 
+| 0 -> RISCVSLLI
+| 1 -> RISCVSRLI
+| 2 -> RISCVSRAI
+
+let translate_out_rop op = match translate_out_enum op with
+| 0 -> RISCVADD 
+| 1 -> RISCVSUB 
+| 2 -> RISCVSLL 
+| 3 -> RISCVSLT 
+| 4 -> RISCVSLTU
+| 5 -> RISCVXOR 
+| 6 -> RISCVSRL 
+| 7 -> RISCVSRA 
+| 8 -> RISCVOR  
+| 9 -> RISCVAND 
+
+let translate_out_ropw op = match translate_out_enum op with
+| 0 -> RISCVADDW
+| 1 -> RISCVSUBW
+| 2 -> RISCVSLLW
+| 3 -> RISCVSRLW
+| 4 -> RISCVSRAW
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
new file mode 100644
index 00000000..9dd36d5e
--- /dev/null
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -0,0 +1,33 @@
+let translate_enum enum_values name value =
+  let rec bit_count n =
+    if n = 0 then 0
+    else 1 + (bit_count (n lsr 1)) in
+  let rec find_index element = function
+    | h::tail -> if h = element then 0 else 1 + (find_index element tail)
+    | _ -> failwith "translate_enum could not find value"
+    in
+  let size = bit_count (List.length enum_values) in
+  let index = find_index value enum_values in
+  (name, Range0 (Some size),  IInt.bit_list_of_integer size (Nat_big_num.of_int index))
+
+let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
+let translate_reg name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+let translate_imm20 name value = 
+    (name, Bvector (Some 26), bit_list_of_integer 26 (Nat_big_num.of_int value))
+let translate_imm16 name value = 
+    (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+let translate_imm12 name value = 
+    (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
+let translate_imm6 name value = 
+    (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+let translate_imm5 name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+let translate_bool name value =
+  (name, Bit, [if value then Bitc_one else Bitc_zero])
diff --git a/risc-v/risc-v.sail b/risc-v/riscv.sail
index 4b90e792..c91a0104 100644
--- a/risc-v/risc-v.sail
+++ b/risc-v/riscv.sail
@@ -72,6 +72,8 @@ 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 word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
+
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -192,31 +194,52 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, bool, [|8|]) LOAD
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 1))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 2))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 4))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 8))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  1))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  2))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  4))
+union ast member ((bit[12]), regno, regno, bool, word_width) LOAD
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD))
 function clause execute(LOAD(imm, rs1, rd, unsigned, width)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
     let (bit[64]) result = if unsigned then 
-        EXTZ(MEMr(addr, width))
+        switch (width) {
+          case BYTE   -> EXTZ(MEMr(addr, 1))
+          case WORD   -> EXTZ(MEMr(addr, 2))
+          case HALF   -> EXTZ(MEMr(addr, 4))
+          case DOUBLE -> MEMr(addr, 8)
+        }
       else
-        EXTS(MEMr(addr, width)) in
+        switch (width) {
+          case BYTE   -> EXTS(MEMr(addr, 1))
+          case WORD   -> EXTS(MEMr(addr, 2))
+          case HALF   -> EXTS(MEMr(addr, 4))
+          case DOUBLE -> MEMr(addr, 8)
+        } in
     wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, [|8|]) STORE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 1))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 2))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 4))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 8))
+union ast member ((bit[12]), regno, regno, word_width) STORE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE))
 function clause execute (STORE(imm, rs2, rs1, width)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
-      MEMea(addr, width);
-      MEMval(addr, width, rGPR(rs2));
+      switch (width) {
+        case BYTE   -> MEMea(addr, 1)
+        case WORD   -> MEMea(addr, 2)
+        case HALF   -> MEMea(addr, 4)
+        case DOUBLE -> MEMea(addr, 8)
+      };
+      let rs2_val = rGPR(rs2) in
+      switch (width) {
+        case BYTE   -> MEMval(addr, 1, rs2_val)
+        case WORD   -> MEMval(addr, 2, rs2_val)
+        case HALF   -> MEMval(addr, 4, rs2_val)
+        case DOUBLE -> MEMval(addr, 8, rs2_val)
+      }
     }
 
 union ast member ((bit[12]), regno, regno) ADDIW
@@ -258,6 +281,8 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, EXTS(result))
 
+function clause decode _ = None
+
 end ast
 end decode
 end execute
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
new file mode 100644
index 00000000..c09c85c2
--- /dev/null
+++ b/risc-v/riscv_extras.lem
@@ -0,0 +1,58 @@
+open import Pervasives
+open import Interp_ast
+open import Interp_interface
+open import Sail_impl_base
+open import Interp_inter_imp
+import Set_extra
+
+let memory_parameter_transformer mode v =
+  match v with
+  | Interp_ast.V_tuple [location;length] ->
+    let (v,loc_regs) = extern_with_track mode extern_vector_value location in
+
+    match length with
+    | Interp_ast.V_lit (L_aux (L_num len) _) ->
+      (v,(natFromInteger len),loc_regs)
+    | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs ->
+      match loc_regs with
+      | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+      | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+      end
+    | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'"
+    end
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
+
+let memory_parameter_transformer_option_address _mode v =
+  match v with
+  | Interp_ast.V_tuple [location;_] ->
+     Just (extern_vector_value location)
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
+
+
+let read_memory_functions : memory_reads =
+  [ ("MEMr",             (MR Read_plain              memory_parameter_transformer));
+    ("MEMr_reserve",     (MR Read_reserve            memory_parameter_transformer));
+  ]
+
+let memory_writes : memory_writes =
+  []
+
+let memory_eas : memory_write_eas =
+  [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
+    ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
+  ]
+
+let memory_vals : memory_write_vals =
+  [ ("MEMval",      (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional", (MV memory_parameter_transformer_option_address
+                           (Just 
+                           (fun (IState interp context) b -> 
+                             let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
+                             (IState (Interp.add_answer_to_stack interp bit) context)))));
+  ]
+
+let barrier_functions = [
+  ("MEM_sync", Barrier_MIPS_SYNC);
+  ]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
new file mode 100644
index 00000000..cbc8bd0d
--- /dev/null
+++ b/risc-v/riscv_extras_embed.lem
@@ -0,0 +1,32 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import Prompt
+
+val MEMr             : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+val MEMea                 : (vector bitU * integer) -> M unit
+val MEMea_conditional     : (vector bitU * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
+
+let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+
+val MEM_sync  : unit -> M unit
+
+let MEM_sync () = barrier Barrier_Isync
+
+let duplicate (bit,len) =
+  let bits = repeat [bit] len in
+  let start = len - 1 in
+  Vector bits start false
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
new file mode 100644
index 00000000..7fb62161
--- /dev/null
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -0,0 +1,34 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import State
+
+val MEMr             : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+val MEMea                 : (vector bitU * integer) -> M unit
+val MEMea_conditional     : (vector bitU * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
+
+let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+
+val MEM_sync  : unit -> M unit
+
+let MEM_sync () = barrier Barrier_MIPS_SYNC
+
+
+let duplicate (bit,len) =
+  let bits = repeat [bit] len in
+  let start = len - 1 in
+  Vector bits start false