Merge branch 'master' into experiments

18 files changed, 678 insertions, 153 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 8983b5ae..b1968173 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -5,9 +5,13 @@
 | `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
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool
+| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool
 | `RISCVADDIW of bit12 * reg * reg
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
 | `RISCVFENCE of bit4 * bit4
+| `RISCVFENCEI
+| `RISCVLoadRes of bool * bool * reg * wordWidth * reg
+| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
+| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
index 03318805..4c51e114 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -1,13 +1,16 @@
-| `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)))
+| `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)))
+| `RISCVLoadRes (_, _, rs1, _, rd)       -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg))
+| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
+| `RISCVAMO (_, _, _, rs2, rs1, _, rd)   -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (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
index 50026612..07c1d082 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -3,10 +3,10 @@
       translate_imm20 "imm" imm,
       translate_reg "rd" rd,
       translate_uop op)
-| `RISCVJAL(imm, rd) -> JAL0(
+| `RISCVJAL(imm, rd) -> RISCV_JAL(
       translate_imm21 "imm" imm,
       translate_reg "rd" rd)
-| `RISCVJALR(imm, rs, rd) -> JALR0(
+| `RISCVJALR(imm, rs, rd) -> RISCV_JALR(
       translate_imm12 "imm" imm,
       translate_reg "rs" rd,
       translate_reg "rd" rd)
@@ -30,17 +30,21 @@
       translate_reg "rs1" rs1,
       translate_reg "rd" rd,
       translate_rop op)
-| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD(
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD(
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
       translate_reg "rd" rd,
       translate_bool "unsigned" unsigned,
-      translate_wordWidth width)
-| `RISCVStore(imm, rs, rd, width) -> STORE (
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE (
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
       translate_reg "rd" rd,
-      translate_wordWidth width)
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
 | `RISCVADDIW(imm, rs, rd) -> ADDIW(
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
@@ -56,5 +60,27 @@
       translate_reg "rd" rd,
       translate_ropw op)
 | `RISCVFENCE(pred, succ) -> FENCE(
-  translate_imm4 "pred" pred,
-  translate_imm4 "succ" succ)
+      translate_imm4 "pred" pred,
+      translate_imm4 "succ" succ)
+| `RISCVFENCEI -> FENCEI
+| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO(
+      translate_amoop op,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index 4d8bd87a..e6edd24d 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -4,48 +4,59 @@ 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_uop op = match op with
-  | RISCVLUI   -> LUI0
-  | RISCVAUIPC -> AUIPC
+  | RISCVLUI   -> RISCV_LUI
+  | RISCVAUIPC -> RISCV_AUIPC
 
 let translate_bop op = match op with
-  | RISCVBEQ  -> BEQ0
-  | RISCVBNE  -> BNE
-  | RISCVBLT  -> BLT
-  | RISCVBGE  -> BGE
-  | RISCVBLTU -> BLTU
-  | RISCVBGEU -> BGEU
+  | RISCVBEQ  -> RISCV_BEQ
+  | RISCVBNE  -> RISCV_BNE
+  | RISCVBLT  -> RISCV_BLT
+  | RISCVBGE  -> RISCV_BGE
+  | RISCVBLTU -> RISCV_BLTU
+  | RISCVBGEU -> RISCV_BGEU
 
 let translate_iop op = match op with
-  | RISCVADDI  -> ADDI0 
-  | RISCVSLTI  -> SLTI0
-  | RISCVSLTIU -> SLTIU0
-  | RISCVXORI  -> XORI0
-  | RISCVORI   -> ORI0
-  | RISCVANDI  -> ANDI0
+  | RISCVADDI  -> RISCV_ADDI
+  | RISCVSLTI  -> RISCV_SLTI
+  | RISCVSLTIU -> RISCV_SLTIU
+  | RISCVXORI  -> RISCV_XORI
+  | RISCVORI   -> RISCV_ORI
+  | RISCVANDI  -> RISCV_ANDI
 
 let translate_sop op = match op with
-  | RISCVSLLI -> SLLI
-  | RISCVSRLI -> SRLI
-  | RISCVSRAI -> SRAI
+  | RISCVSLLI -> RISCV_SLLI
+  | RISCVSRLI -> RISCV_SRLI
+  | RISCVSRAI -> RISCV_SRAI
 
 let translate_rop op = match op with
-  | RISCVADD  -> ADD0 
-  | RISCVSUB  -> SUB0 
-  | RISCVSLL  -> SLL0 
-  | RISCVSLT  -> SLT0 
-  | RISCVSLTU -> SLTU0
-  | RISCVXOR  -> XOR0 
-  | RISCVSRL  -> SRL0 
-  | RISCVSRA  -> SRA0 
-  | RISCVOR   -> OR0  
-  | RISCVAND  -> AND0 
+  | RISCVADD  -> RISCV_ADD
+  | RISCVSUB  -> RISCV_SUB
+  | RISCVSLL  -> RISCV_SLL
+  | RISCVSLT  -> RISCV_SLT
+  | RISCVSLTU -> RISCV_SLTU
+  | RISCVXOR  -> RISCV_XOR
+  | RISCVSRL  -> RISCV_SRL
+  | RISCVSRA  -> RISCV_SRA
+  | RISCVOR   -> RISCV_OR
+  | RISCVAND  -> RISCV_AND
 
 let translate_ropw op = match op with
-  | RISCVADDW -> ADDW 
-  | RISCVSUBW -> SUBW 
-  | RISCVSLLW -> SLLW 
-  | RISCVSRLW -> SRLW 
-  | RISCVSRAW -> SRAW 
+  | RISCVADDW -> RISCV_ADDW
+  | RISCVSUBW -> RISCV_SUBW
+  | RISCVSLLW -> RISCV_SLLW
+  | RISCVSRLW -> RISCV_SRLW
+  | RISCVSRAW -> RISCV_SRAW
+
+let translate_amoop op = match op with
+  | RISCVAMOSWAP -> AMOSWAP
+  | RISCVAMOADD  -> AMOADD
+  | RISCVAMOXOR  -> AMOXOR
+  | RISCVAMOAND  -> AMOAND
+  | RISCVAMOOR   -> AMOOR
+  | RISCVAMOMIN  -> AMOMIN
+  | RISCVAMOMAX  -> AMOMAX
+  | RISCVAMOMINU -> AMOMINU
+  | RISCVAMOMAXU -> AMOMAXU
 
 let translate_wordWidth op = match op with
   | RISCVBYTE   -> BYTE  
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index 5f2c8326..e42b8a62 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -33,18 +33,44 @@
 "or",   RTYPE{op=RISCVOR};
 "and",  RTYPE{op=RISCVAND};
 
-"lb",  LOAD{unsigned=false; width=RISCVBYTE};
-"lbu", LOAD{unsigned=true;  width=RISCVBYTE};
-"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=RISCVBYTE};
-"sh", STORE{width=RISCVHALF};
-"sw", STORE{width=RISCVWORD};
-"sd", STORE{width=RISCVDOUBLE};
+"lb",  LOAD{unsigned=false; width=RISCVBYTE;   aq=false; rl=false};
+"lbu", LOAD{unsigned=true;  width=RISCVBYTE;   aq=false; rl=false};
+"lh",  LOAD{unsigned=false; width=RISCVHALF;   aq=false; rl=false};
+"lhu", LOAD{unsigned=true;  width=RISCVHALF;   aq=false; rl=false};
+"lw",  LOAD{unsigned=false; width=RISCVWORD;   aq=false; rl=false};
+"lwu", LOAD{unsigned=true;  width=RISCVWORD;   aq=false; rl=false};
+"ld",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false};
+
+"lb.aq",  LOAD{unsigned=false; width=RISCVBYTE;   aq=true; rl=false};
+"lbu.aq", LOAD{unsigned=true;  width=RISCVBYTE;   aq=true; rl=false};
+"lh.aq",  LOAD{unsigned=false; width=RISCVHALF;   aq=true; rl=false};
+"lhu.aq", LOAD{unsigned=true;  width=RISCVHALF;   aq=true; rl=false};
+"lw.aq",  LOAD{unsigned=false; width=RISCVWORD;   aq=true; rl=false};
+"lwu.aq", LOAD{unsigned=true;  width=RISCVWORD;   aq=true; rl=false};
+"ld.aq",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false};
+
+"lb.aq.rl",  LOAD{unsigned=false; width=RISCVBYTE;   aq=true; rl=true};
+"lbu.aq.rl", LOAD{unsigned=true;  width=RISCVBYTE;   aq=true; rl=true};
+"lh.aq.rl",  LOAD{unsigned=false; width=RISCVHALF;   aq=true; rl=true};
+"lhu.aq.rl", LOAD{unsigned=true;  width=RISCVHALF;   aq=true; rl=true};
+"lw.aq.rl",  LOAD{unsigned=false; width=RISCVWORD;   aq=true; rl=true};
+"lwu.aq.rl", LOAD{unsigned=true;  width=RISCVWORD;   aq=true; rl=true};
+"ld.aq.rl",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true};
+
+"sb", STORE{width=RISCVBYTE;   aq=false; rl=false};
+"sh", STORE{width=RISCVHALF;   aq=false; rl=false};
+"sw", STORE{width=RISCVWORD;   aq=false; rl=false};
+"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false};
+
+"sb.rl", STORE{width=RISCVBYTE;   aq=false; rl=true};
+"sh.rl", STORE{width=RISCVHALF;   aq=false; rl=true};
+"sw.rl", STORE{width=RISCVWORD;   aq=false; rl=true};
+"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true};
+
+"sb.aq.rl", STORE{width=RISCVBYTE;   aq=true; rl=true};
+"sh.aq.rl", STORE{width=RISCVHALF;   aq=true; rl=true};
+"sw.aq.rl", STORE{width=RISCVWORD;   aq=true; rl=true};
+"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true};
 
 "addiw", ADDIW ();
 
@@ -62,3 +88,103 @@
 "r",  FENCEOPTION Fence_R;
 "w",  FENCEOPTION Fence_W;
 "rw", FENCEOPTION Fence_RW;
+
+"fence.i", FENCEI ();
+
+"lr.w",       LOADRES {width=RISCVWORD;   aq=false; rl=false};
+"lr.w.aq",    LOADRES {width=RISCVWORD;   aq=true;  rl=false};
+"lr.w.aq.rl", LOADRES {width=RISCVWORD;   aq=true;  rl=true};
+"lr.d",       LOADRES {width=RISCVDOUBLE; aq=false; rl=false};
+"lr.d.aq",    LOADRES {width=RISCVDOUBLE; aq=true;  rl=false};
+"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true;  rl=true};
+
+"sc.w",       STORECON {width=RISCVWORD;   aq=false; rl=false};
+"sc.w.rl",    STORECON {width=RISCVWORD;   aq=false; rl=true};
+"sc.w.aq.rl", STORECON {width=RISCVWORD;   aq=true;  rl=true};
+"sc.d",       STORECON {width=RISCVDOUBLE; aq=false; rl=false};
+"sc.d.rl",    STORECON {width=RISCVDOUBLE; aq=false; rl=true};
+"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true;  rl=true};
+
+"amoswap.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP};
+"amoadd.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD};
+"amoand.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOAND};
+"amoor.w",    AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOOR};
+"amoxor.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOXOR};
+"amomax.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAX};
+"amomin.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMIN};
+"amomaxu.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAXU};
+"amominu.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMINU};
+
+"amoswap.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOSWAP};
+"amoadd.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOADD};
+"amoand.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOAND};
+"amoor.d",    AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOOR};
+"amoxor.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOXOR};
+"amomax.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAX};
+"amomin.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMIN};
+"amomaxu.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAXU};
+"amominu.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMINU};
+
+"amoswap.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOSWAP};
+"amoadd.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOADD};
+"amoand.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOAND};
+"amoor.w.aq",    AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOOR};
+"amoxor.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOXOR};
+"amomax.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAX};
+"amomin.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMIN};
+"amomaxu.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAXU};
+"amominu.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMINU};
+
+"amoswap.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOSWAP};
+"amoadd.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOADD};
+"amoand.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOAND};
+"amoor.d.aq",    AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOOR};
+"amoxor.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOXOR};
+"amomax.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAX};
+"amomin.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMIN};
+"amomaxu.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAXU};
+"amominu.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMINU};
+
+"amoswap.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOSWAP};
+"amoadd.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOADD};
+"amoand.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOAND};
+"amoor.w.rl",    AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOOR};
+"amoxor.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOXOR};
+"amomax.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAX};
+"amomin.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMIN};
+"amomaxu.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAXU};
+"amominu.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMINU};
+
+"amoswap.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOSWAP};
+"amoadd.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOADD};
+"amoand.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOAND};
+"amoor.d.rl",    AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOOR};
+"amoxor.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOXOR};
+"amomax.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAX};
+"amomin.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMIN};
+"amomaxu.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAXU};
+"amominu.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMINU};
+
+"amoswap.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOSWAP};
+"amoadd.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOADD};
+"amoand.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOAND};
+"amoor.w.aq.rl",    AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOOR};
+"amoxor.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOXOR};
+"amomax.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAX};
+"amomin.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMIN};
+"amomaxu.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAXU};
+"amominu.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMINU};
+
+"amoswap.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOSWAP};
+"amoadd.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOADD};
+"amoand.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOAND};
+"amoor.d.aq.rl",    AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOOR};
+"amoxor.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOXOR};
+"amomax.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAX};
+"amomin.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMIN};
+"amomaxu.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAXU};
+"amominu.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMINU};
+
+(** pseudo instructions *********************************************)
+
+"li", LI ()
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index ff14c428..bab5ced8 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -1,12 +1,15 @@
-| `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)
+| `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, a, b)       -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b)
+| `RISCVStore (x, r0, r1, y, z, a)         -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a)
+| `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)
+| `RISCVLoadRes (aq, rl, rs1, w, rd)       -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd)
+| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd)  -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 37fd8d8d..210e38fb 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -1,36 +1,74 @@
 | UTYPE reg COMMA NUM
-  { `RISCVUTYPE($4, $2, $1.op) }
+  { (* it's not clear if NUM here should be before or after filling the
+      lowest 12 bits with zeros, or if it should be signed or unsigned;
+      currently assuming: NUM does not include the 12 zeros, and is unsigned *)
+    if not (iskbituimm 20 $4) then failwith "immediate is not 20bit"
+    else `RISCVUTYPE ($4, $2, $1.op) }
 | JAL reg COMMA NUM
-  { `RISCVJAL($4, $2) }
+  { if not ($4 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit"
+    else `RISCVJAL ($4, $2) }
 | JALR reg COMMA reg COMMA NUM
-  { `RISCVJALR($6, $4, $2) }
+  { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit"
+    else `RISCVJALR ($6, $4, $2) }
 | BTYPE reg COMMA reg COMMA NUM
-  { `RISCVBType($6, $4, $2, $1.op) }
+  { if not ($6 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit"
+    else `RISCVBType ($6, $4, $2, $1.op) }
 | ITYPE reg COMMA reg COMMA NUM
-  { `RISCVIType($6, $4, $2, $1.op) }
+  { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit"
+    else `RISCVIType ($6, $4, $2, $1.op) }
+| ADDIW reg COMMA reg COMMA NUM
+  { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else `RISCVADDIW ($6, $4, $2) }
 | SHIFTIOP reg COMMA reg COMMA NUM
-  { `RISCVShiftIop($6, $4, $2, $1.op) }
+  { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit"
+    else `RISCVShiftIop ($6, $4, $2, $1.op) }
+| SHIFTW reg COMMA reg COMMA NUM
+  { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit"
+    else `RISCVSHIFTW ($6, $4, $2, $1.op) }
 | RTYPE reg COMMA reg COMMA reg
   { `RISCVRType ($6, $4, $2, $1.op) }
 | LOAD reg COMMA NUM LPAR reg RPAR
-  { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) }
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) }
 | STORE reg COMMA NUM LPAR reg RPAR
-  { `RISCVStore($4, $2, $6, $1.width) }
-| ADDIW reg COMMA reg COMMA NUM
-  { `RISCVADDIW ($6, $4, $2) }
-| SHIFTW reg COMMA reg COMMA NUM
-  { `RISCVSHIFTW ($6, $4, $2, $1.op) }
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) }
 | RTYPEW reg COMMA reg COMMA reg
   { `RISCVRTYPEW ($6, $4, $2, $1.op) }
 | FENCE FENCEOPTION COMMA FENCEOPTION
   { match ($2, $4) with
     | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
     | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+    | (Fence_R,  Fence_R)  -> `RISCVFENCE (0b0010, 0b0010)
     | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 0b0001)
+    | (Fence_W,  Fence_W)  -> `RISCVFENCE (0b0001, 0b0001)
     | (Fence_RW, Fence_R)  -> failwith "'fence rw,r' is not supported"
-    | (Fence_R,  Fence_R)  -> failwith "'fence r,r' is not supported"
     | (Fence_R,  Fence_W)  -> failwith "'fence r,w' is not supported"
     | (Fence_W,  Fence_RW) -> failwith "'fence w,rw' is not supported"
     | (Fence_W,  Fence_R)  -> failwith "'fence w,r' is not supported"
-    | (Fence_W,  Fence_W)  -> failwith "'fence w,w' is not supported"
   }
+| FENCEI
+  { `RISCVFENCEI }
+| LOADRES reg COMMA LPAR reg RPAR
+  { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) }
+| LOADRES reg COMMA NUM LPAR reg RPAR
+  { if $4 <> 0 then failwith "'lr' offset must be 0" else
+    `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) }
+| STORECON reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) }
+| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'sc' offset must be 0" else
+    `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) }
+| AMO reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
+| AMO reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else
+    `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) }
+
+/* pseudo-ops */
+| LI reg COMMA NUM
+  { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)"
+    else `RISCVIType ($4, IReg R0, $2, RISCVORI) }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 1da3ef11..fc1c0000 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -7,9 +7,24 @@
 | `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, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1)
+
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs)
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (pp_reg rs2) imm (pp_reg rs1)
+
 | `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)
 | `RISCVFENCE(pred, succ)         -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
+| `RISCVFENCEI                    -> sprintf "fence.i"
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1)
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
diff --git a/risc-v/hgen/pretty_xml.hgen b/risc-v/hgen/pretty_xml.hgen
new file mode 100644
index 00000000..b0306161
--- /dev/null
+++ b/risc-v/hgen/pretty_xml.hgen
@@ -0,0 +1,137 @@
+| `RISCVThreadStart -> ("op_thread_start", [])
+
+| `RISCVStopFetching -> ("op_stop_fetching", [])
+
+| `RISCVUTYPE(imm, rd, op) ->
+    ("op_U_type",
+      [ ("op",   pp_riscv_uop op);
+        ("uimm", sprintf "%d" imm);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVJAL(imm, rd) ->
+    ("op_jal",
+      [ ("offset", sprintf "%d" imm);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVJALR(imm, rs1, rd) ->
+    ("op_jalr",
+      [ ("offset", sprintf "%d" imm);
+        ("base",   pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVBType(imm, rs2, rs1, op) ->
+    ("op_branch",
+      [ ("op",     pp_riscv_bop op);
+        ("offset", sprintf "%d" imm);
+        ("src2",   pp_reg rs2);
+        ("src1",   pp_reg rs1);
+      ])
+
+| `RISCVIType(imm, rs1, rd, op) ->
+    ("op_I_type",
+      [ ("op",   pp_riscv_iop op);
+        ("iimm", sprintf "%d" imm);
+        ("src",  pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVShiftIop(imm, rs1, rd, op) ->
+    ("op_IS_type",
+      [ ("op",     pp_riscv_sop op);
+        ("shamt",  sprintf "%d" imm);
+        ("src",    pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVSHIFTW(imm, rs1, rd, op) ->
+    ("op_ISW_type",
+      [ ("op",    pp_riscv_sop op);
+        ("shamt", sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRType (rs2, rs1, rd, op) ->
+    ("op_R_type",
+      [ ("op",   pp_riscv_rop op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) ->
+    ("op_load",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("unsigned", if unsigned then "true" else "false");
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+        ("dest",     pp_reg rd);
+      ])
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    ("op_store",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("src",      pp_reg rs2);
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+      ])
+
+| `RISCVADDIW(imm, rs1, rd) ->
+    ("op_addiw",
+      [ ("iimm",  sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRTYPEW(rs2, rs1, rd, op) ->
+    ("op_RW_type",
+      [ ("op",   pp_riscv_ropw op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVFENCE(pred, succ) ->
+    ("op_fence",
+      [ ("pred", pp_riscv_fence_option pred);
+        ("succ", pp_riscv_fence_option succ);
+      ])
+
+| `RISCVFENCEI -> ("op_fence_i", [])
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    ("op_lr",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    ("op_sc",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("src",   pp_reg rs2);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    ("op_amo",
+      [ ("op",    pp_riscv_amo_op_part op);
+        ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("src",   pp_reg rs2);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index dca5bea1..2f9a80f1 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -6,9 +6,18 @@
 | ("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)
+| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl])
+                                  -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ("STORE", [imm; rs; rd; width; aq; rl])
+                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
 | ("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)
 | ("FENCE", [pred; succ])         -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| ("FENCEI", [])                  -> `RISCVFENCEI
+| ("LOADRES", [aq; rl; rs1; width; rd])
+                                  -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("STORECON", [aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("AMO", [op; aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 6158ebd7..3025992e 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -1,14 +1,23 @@
 | EBREAK                      -> `RISCVStopFetching
 | UTYPE( imm, rd, op)         -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
-| JAL0( imm, rd)              -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
-| JALR0( imm, rs, rd)         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| RISCV_JAL( imm, rd)         -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
+| RISCV_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_simm13 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)
+| LOAD( imm, rs, rd, unsigned, width, aq, rl)
+                              -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| STORE( imm, rs, rd, width, aq, rl)
+                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
 | 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)
 | FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| FENCEI                      -> `RISCVFENCEI
+| LOADRES( aq, rl, rs1, width, rd)
+                              -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| STORECON( aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| AMO( op, aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index a891d7d0..6b3b7f51 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -10,48 +10,59 @@ let translate_out_signed_int inst bits =
 let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
 
 let translate_out_uop op = match op with
-  | LUI0  -> RISCVLUI  
-  | AUIPC -> RISCVAUIPC
+  | RISCV_LUI   -> RISCVLUI
+  | RISCV_AUIPC -> RISCVAUIPC
 
 let translate_out_bop op = match op with
-  | BEQ0 -> RISCVBEQ 
-  | BNE  -> RISCVBNE 
-  | BLT  -> RISCVBLT 
-  | BGE  -> RISCVBGE 
-  | BLTU -> RISCVBLTU
-  | BGEU -> RISCVBGEU
+  | RISCV_BEQ  -> RISCVBEQ
+  | RISCV_BNE  -> RISCVBNE
+  | RISCV_BLT  -> RISCVBLT
+  | RISCV_BGE  -> RISCVBGE
+  | RISCV_BLTU -> RISCVBLTU
+  | RISCV_BGEU -> RISCVBGEU
 
 let translate_out_iop op = match op with
-  | ADDI0  -> RISCVADDI 
-  | SLTI0  -> RISCVSLTI 
-  | SLTIU0 -> RISCVSLTIU
-  | XORI0  -> RISCVXORI 
-  | ORI0   -> RISCVORI  
-  | ANDI0  -> RISCVANDI 
+  | RISCV_ADDI   -> RISCVADDI
+  | RISCV_SLTI   -> RISCVSLTI
+  | RISCV_SLTIU  -> RISCVSLTIU
+  | RISCV_XORI   -> RISCVXORI
+  | RISCV_ORI    -> RISCVORI
+  | RISCV_ANDI   -> RISCVANDI
 
 let translate_out_sop op = match op with
-  | SLLI -> RISCVSLLI
-  | SRLI -> RISCVSRLI
-  | SRAI -> RISCVSRAI
+  | RISCV_SLLI -> RISCVSLLI
+  | RISCV_SRLI -> RISCVSRLI
+  | RISCV_SRAI -> RISCVSRAI
 
 let translate_out_rop op = match op with
-  | ADD0  -> RISCVADD 
-  | SUB0  -> RISCVSUB 
-  | SLL0  -> RISCVSLL 
-  | SLT0  -> RISCVSLT 
-  | SLTU0 -> RISCVSLTU
-  | XOR0  -> RISCVXOR 
-  | SRL0  -> RISCVSRL 
-  | SRA0  -> RISCVSRA 
-  | OR0   -> RISCVOR  
-  | AND0  -> RISCVAND 
+  | RISCV_ADD   -> RISCVADD
+  | RISCV_SUB   -> RISCVSUB
+  | RISCV_SLL   -> RISCVSLL
+  | RISCV_SLT   -> RISCVSLT
+  | RISCV_SLTU  -> RISCVSLTU
+  | RISCV_XOR   -> RISCVXOR
+  | RISCV_SRL   -> RISCVSRL
+  | RISCV_SRA   -> RISCVSRA
+  | RISCV_OR    -> RISCVOR
+  | RISCV_AND   -> RISCVAND
 
 let translate_out_ropw op = match op with
-  | ADDW  -> RISCVADDW
-  | SUBW  -> RISCVSUBW
-  | SLLW  -> RISCVSLLW
-  | SRLW  -> RISCVSRLW
-  | SRAW  -> RISCVSRAW
+  | RISCV_ADDW  -> RISCVADDW
+  | RISCV_SUBW  -> RISCVSUBW
+  | RISCV_SLLW  -> RISCVSLLW
+  | RISCV_SRLW  -> RISCVSRLW
+  | RISCV_SRAW  -> RISCVSRAW
+
+let translate_out_amoop op = match op with
+  | AMOSWAP -> RISCVAMOSWAP
+  | AMOADD  -> RISCVAMOADD
+  | AMOXOR  -> RISCVAMOXOR
+  | AMOAND  -> RISCVAMOAND
+  | AMOOR   -> RISCVAMOOR
+  | AMOMIN  -> RISCVAMOMIN
+  | AMOMAX  -> RISCVAMOMAX
+  | AMOMINU -> RISCVAMOMINU
+  | AMOMAXU -> RISCVAMOMAXU
 
 let translate_out_wordWidth op = match op with
   | BYTE   -> RISCVBYTE  
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index 2980b985..f29e318d 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -5,11 +5,19 @@ 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_Load     = {unsigned: bool; width : wordWidth; aq: bool; rl: bool }
+type token_Store    = {width : wordWidth; aq: bool; rl: bool }
 type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
 type token_FENCE    = unit
+type token_FENCEI   = unit
+type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
+type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
+type token_AMO      = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop }
 
 type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
+
+(* pseudo-ops *)
+
+type token_LI = unit
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index f952cf77..f812adbd 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -12,3 +12,8 @@
 %token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
 %token <RISCVHGenBase.token_FENCE>    FENCE
 %token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
+%token <RISCVHGenBase.token_FENCEI>   FENCEI
+%token <RISCVHGenBase.token_LoadRes>  LOADRES
+%token <RISCVHGenBase.token_StoreCon> STORECON
+%token <RISCVHGenBase.token_AMO>      AMO
+%token <RISCVHGenBase.token_LI>       LI
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index df22d9dc..8b7cbe11 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -58,7 +58,7 @@
       translate_rop "op" op;
     ],
     [])
-| `RISCVLoad(imm, rs, rd, unsigned, width) -> 
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
    ("LOAD",
     [
       translate_imm12 "imm" imm;
@@ -66,15 +66,19 @@
       translate_reg "rd" rd;
       translate_bool "unsigned" unsigned;
       translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
     ],
     [])
-| `RISCVStore(imm, rs2, rs1, width) -> 
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
    ("STORE",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs2" rs2;
       translate_reg "rs1" rs1;
       translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
     ],
     [])
 | `RISCVADDIW(imm, rs, rd)        -> 
@@ -110,3 +114,40 @@
      translate_imm4 "succ" succ;
   ], 
   [])
+| `RISCVFENCEI ->
+  ("FENCEI",
+  [],
+  [])
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+   ("LOADRES",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+   ("STORECON",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+   ("AMO",
+    [
+      translate_amoop "op" op;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index 87fc9b95..a0b75606 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -99,22 +99,71 @@ type wordWidth =
   | 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"
+let pp_word_width width : string =
+  begin match width with
+  | RISCVBYTE   -> "b"
+  | RISCVHALF   -> "h"
+  | RISCVWORD   -> "w"
+  | RISCVDOUBLE -> "d"
+  end
+
+let pp_riscv_load_op (unsigned, width, aq, rl) =
+  "l" ^
+  (pp_word_width width) ^
+  (if unsigned then "u" else "") ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_op (width, aq, rl) =
+  "s" ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_load_reserved_op (aq, rl, width) =
+  "lr." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_conditional_op (aq, rl, width) =
+  "sc." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+type riscvAmoop =
+  | RISCVAMOSWAP
+  | RISCVAMOADD
+  | RISCVAMOXOR
+  | RISCVAMOAND
+  | RISCVAMOOR
+  | RISCVAMOMIN
+  | RISCVAMOMAX
+  | RISCVAMOMINU
+  | RISCVAMOMAXU
+
+let pp_riscv_amo_op_part = function
+  | RISCVAMOSWAP -> "swap"
+  | RISCVAMOADD  -> "add"
+  | RISCVAMOXOR  -> "xor"
+  | RISCVAMOAND  -> "and"
+  | RISCVAMOOR   -> "or"
+  | RISCVAMOMIN  -> "min"
+  | RISCVAMOMAX  -> "max"
+  | RISCVAMOMINU -> "minu"
+  | RISCVAMOMAXU -> "maxu"
+
+let pp_riscv_amo_op (op, aq, rl, width) =
+  "amo" ^
+  pp_riscv_amo_op_part op ^
+  begin match width with
+  | RISCVWORD   -> ".w"
+  | RISCVDOUBLE -> ".d"
+  | _ -> assert false
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
 
 let pp_riscv_fence_option = function
   | 0b0011 -> "rw"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index e22110d0..66a2020c 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -84,3 +84,15 @@ let translate_out_ropw op = match translate_out_enum op with
 | 3 -> RISCVSRLW
 | 4 -> RISCVSRAW
 | _ -> failwith "Unknown ropw in sail translate out"
+
+let translate_out_amoop op = match translate_out_enum op with
+| 0 -> RISCVAMOSWAP
+| 1 -> RISCVAMOADD
+| 2 -> RISCVAMOXOR
+| 3 -> RISCVAMOAND
+| 4 -> RISCVAMOOR
+| 5 -> RISCVAMOMIN
+| 6 -> RISCVAMOMAX
+| 7 -> RISCVAMOMINU
+| 8 -> RISCVAMOMAXU
+| _ -> failwith "Unknown amoop in sail translate out"
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
index 1bf174fa..238c7e5b 100644
--- a/risc-v/hgen/types_trans_sail.hgen
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -11,29 +11,47 @@ let translate_enum enum_values name value =
   (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_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU]
+
 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_imm21 name value = 
     (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
+
 let translate_imm20 name value = 
     (name, Bvector (Some 20), bit_list_of_integer 20 (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_imm13 name value = 
     (name, Bvector (Some 13), bit_list_of_integer 13 (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_imm4 name value = 
     (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+
 let translate_bool name value =
   (name, Bit, [if value then Bitc_one else Bitc_zero])