changes to support get_model for ppcmem.

18 files changed, 856 insertions, 96 deletions

diff --git a/mips/hgen/ast.hgen b/mips/hgen/ast.hgen
new file mode 100644
index 00000000..c9a39bbf
--- /dev/null
+++ b/mips/hgen/ast.hgen
@@ -0,0 +1,13 @@
+| `MIPSRType of mipsRTypeOp * reg * reg * reg
+| `MIPSIType of mipsITypeOp * reg * reg * bit16
+| `MIPSShiftI of mipsShiftIOp * reg * reg * bit5
+| `MIPSShiftV of mipsShiftVOp * reg * reg * reg
+| `MIPSMulDiv of mipsMulDivOp * reg * reg
+| `MIPSMFHiLo of mipsMFHiLoOp * reg
+| `MIPSLUI of reg * bit16
+| `MIPSLoad of mipsWordWidth * bool * bool * reg * reg * bit16 (* width, signed, linked, base, rt, offset *)
+| `MIPSStore of mipsWordWidth * bool * reg * reg * bit16       (* width, conditional, base, rt, offset *)
+| `MIPSLSLR of bool * bool * bool  * reg * reg * bit16         (* store, double, left, base, rt, offset *)
+| `MIPSSYNC
+| `MIPSBEQ of reg * reg * bit16 * bool * bool                  (* rs, rt, offset, not equal, likely *)
+| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool                  (* rs, offset, cmp, link, likely *)
diff --git a/mips/hgen/fold.hgen b/mips/hgen/fold.hgen
new file mode 100644
index 00000000..08b6cc16
--- /dev/null
+++ b/mips/hgen/fold.hgen
@@ -0,0 +1,13 @@
+| `MIPSRType  (op, rd, rs, rt)  -> fold_reg rt (fold_reg rs (fold_reg rd (y_reg, y_sreg)))
+| `MIPSIType  (op, rs, rt, imm) -> fold_reg rs (fold_reg rt (y_reg, y_sreg))
+| `MIPSShiftI (op, rd, rt, imm) -> fold_reg rt (fold_reg rd (y_reg, y_sreg))
+| `MIPSShiftV (op, rd, rt, rs)  -> fold_reg rs (fold_reg rt (fold_reg rd (y_reg, y_sreg)))
+| `MIPSMulDiv (op, rs, rt)      -> fold_reg rs (fold_reg rt  (y_reg, y_sreg))
+| `MIPSMFHiLo (op, rs)          -> fold_reg rs (y_reg, y_sreg)
+| `MIPSLUI (rt, imm)            -> fold_reg rt (y_reg, y_sreg)
+| `MIPSLoad (width, signed, linked, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSStore (width, conditional, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSLSLR (store, double, left, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSSYNC -> (y_reg, y_sreg)
+| `MIPSBEQ (rs, rt, offset, ne, likely) -> fold_reg rs (fold_reg rt (y_reg, y_sreg))
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> fold_reg rs (y_reg, y_sreg)
diff --git a/mips/hgen/lexer.hgen b/mips/hgen/lexer.hgen
new file mode 100644
index 00000000..17e72450
--- /dev/null
+++ b/mips/hgen/lexer.hgen
@@ -0,0 +1,112 @@
+"add"   , RTYPE {txt="ADD"   ; op=MIPSROpADD    };
+"addu"  , RTYPE {txt="ADDU"  ; op=MIPSROpADDU   };
+"and"   , RTYPE {txt="AND"   ; op=MIPSROpAND    };
+"dadd"  , RTYPE {txt="DADD"  ; op=MIPSROpDADD   };
+"daddu" , RTYPE {txt="DADDU" ; op=MIPSROpDADDU  };
+"dsub"  , RTYPE {txt="DSUB"  ; op=MIPSROpDSUB   };
+"dsubu" , RTYPE {txt="DSUBU" ; op=MIPSROpDSUBU  };
+"movn"  , RTYPE {txt="MOVN"  ; op=MIPSROpMOVN   };
+"movz"  , RTYPE {txt="MOVZ"  ; op=MIPSROpMOVZ   };
+"mul"   , RTYPE {txt="MUL"   ; op=MIPSROpMUL    };
+"nor"   , RTYPE {txt="NOR"   ; op=MIPSROpNOR    };
+"or"    , RTYPE {txt="OR"    ; op=MIPSROpOR     };
+"slt"   , RTYPE {txt="SLT"   ; op=MIPSROpSLT    };
+"sltu"  , RTYPE {txt="SLTU"  ; op=MIPSROpSLTU   };
+"sub"   , RTYPE {txt="SUB"   ; op=MIPSROpSUB    };
+"subu"  , RTYPE {txt="SUBU"  ; op=MIPSROpSUBU   };
+"xor"   , RTYPE {txt="XOR"   ; op=MIPSROpXOR    };
+
+"addi"  , ITYPE {txt="ADDI"  ; op=MIPSIOpADDI   };
+"addiu" , ITYPE {txt="ADDIU" ; op=MIPSIOpADDIU  };
+"andi"  , ITYPE {txt="ANDI"  ; op=MIPSIOpANDI   };
+"daddi" , ITYPE {txt="DADDI" ; op=MIPSIOpDADDI  };
+"daddiu", ITYPE {txt="DADDIU"; op=MIPSIOpDADDIU };
+"ori"   , ITYPE {txt="ORI"   ; op=MIPSIOpORI    };
+"slti"  , ITYPE {txt="SLTI"  ; op=MIPSIOpSLTI   };
+"sltiu" , ITYPE {txt="SLTIU" ; op=MIPSIOpSLTIU  };
+"xori"  , ITYPE {txt="XORI"  ; op=MIPSIOpXORI   };
+
+"dsll"   , SHIFTI {txt="DSLL"   ; op=MIPSDSLL   };
+"dsll32" , SHIFTI {txt="DSLL32" ; op=MIPSDSLL32 };
+"dsra"   , SHIFTI {txt="DSRA"   ; op=MIPSDSRA   };
+"dsra32" , SHIFTI {txt="DSRA32" ; op=MIPSDSRA32 };
+"dsrl"   , SHIFTI {txt="DSRL"   ; op=MIPSDSRL   };
+"dsrl32" , SHIFTI {txt="DSRL32" ; op=MIPSDSRL32 };
+"sll"    , SHIFTI {txt="SLL"    ; op=MIPSSLL    };
+"sra"    , SHIFTI {txt="SRA"    ; op=MIPSSRA    };
+"srl"    , SHIFTI {txt="SRL"    ; op=MIPSSRL    };
+
+"dsllv", SHIFTV {txt="DSLLV" ; op=MIPSDSLLV };
+"dsrav", SHIFTV {txt="DSRAV" ; op=MIPSDSRAV };
+"dsrlv", SHIFTV {txt="DSRLV" ; op=MIPSDSRLV };
+"sllv" , SHIFTV {txt="SLLV"  ; op=MIPSSLLV  };
+"srav" , SHIFTV {txt="SRAV"  ; op=MIPSSRAV  };
+"srlv" , SHIFTV {txt="SRLV"  ; op=MIPSSRLV  };
+
+"ddiv"  , MULDIV {txt="DDIV"  ; op=MIPSDDIV   };
+"ddivu" , MULDIV {txt="DDIVU" ; op=MIPSDDIVU  };
+"div"   , MULDIV {txt="DIV"   ; op=MIPSDIV    };
+"divu"  , MULDIV {txt="DIVU"  ; op=MIPSDIVU   };
+"dmult" , MULDIV {txt="DMULT" ; op=MIPSDMULT  };
+"dmultu", MULDIV {txt="DMULTU"; op=MIPSDMULTU };
+"madd"  , MULDIV {txt="MADD"  ; op=MIPSMADD   };
+"maddu" , MULDIV {txt="MADDU" ; op=MIPSMADDU  };
+"msub"  , MULDIV {txt="MSUB"  ; op=MIPSMSUB   };
+"msubu" , MULDIV {txt="MSUBU" ; op=MIPSMSUBU  };
+"mult"  , MULDIV {txt="MULT"  ; op=MIPSMULT   };
+"multu" , MULDIV {txt="MULTU" ; op=MIPSMULTU  };
+
+"mfhi" , MFHILO {txt="MFHI" ; op=MIPSMFHI };
+"mflo" , MFHILO {txt="MFLO" ; op=MIPSMFLO };
+"mthi" , MFHILO {txt="MTHI" ; op=MIPSMTHI };
+"mtlo" , MFHILO {txt="MTLO" ; op=MIPSMTLO };
+
+"lui" , LUI {txt="LUI" };
+
+"lb"  , LOAD {txt="LB"  ; width=MIPSByte   ; signed=true;  linked=false };
+"lbu" , LOAD {txt="LBU" ; width=MIPSByte   ; signed=false; linked=false };
+"lh"  , LOAD {txt="LH"  ; width=MIPSHalf   ; signed=true;  linked=false };
+"lhu" , LOAD {txt="LHU" ; width=MIPSHalf   ; signed=false; linked=false };
+"lw"  , LOAD {txt="LW"  ; width=MIPSWord   ; signed=true;  linked=false };
+"lwu" , LOAD {txt="LWU" ; width=MIPSWord   ; signed=false; linked=false };
+"ld"  , LOAD {txt="LD"  ; width=MIPSDouble ; signed=false; linked=false };
+"ll"  , LOAD {txt="LL"  ; width=MIPSWord   ; signed=true;  linked=true  };
+"lld" , LOAD {txt="LLD" ; width=MIPSDouble ; signed=false; linked=true  };
+
+"sb"  , STORE {txt="SB"  ; width=MIPSByte   ; conditional=false };
+"sh"  , STORE {txt="SH"  ; width=MIPSHalf   ; conditional=false };
+"sw"  , STORE {txt="SW"  ; width=MIPSWord   ; conditional=false };
+"sd"  , STORE {txt="SD"  ; width=MIPSDouble ; conditional=false };
+"sc"  , STORE {txt="SC"  ; width=MIPSWord   ; conditional=true  };
+"scd" , STORE {txt="SCD" ; width=MIPSDouble ; conditional=true  };
+
+"lwl" , LSLR {txt="LWL" ; store=false; double=false; left=true };
+"lwr" , LSLR {txt="LWR" ; store=false; double=false; left=false};
+"ldl" , LSLR {txt="LDL" ; store=false; double=true ; left=true };
+"ldr" , LSLR {txt="LDR" ; store=false; double=true ; left=false};
+"swl" , LSLR {txt="SWL" ; store=true ; double=false; left=true };
+"swr" , LSLR {txt="SWR" ; store=true ; double=false; left=false};
+"sdl" , LSLR {txt="SDL" ; store=true ; double=true ; left=true };
+"sdr" , LSLR {txt="SDR" ; store=true ; double=true ; left=false};
+"sync", SYNC {txt="SYNC"};
+
+"beq",  BEQ {txt="BEQ"; ne=false; likely=false };
+"beql", BEQ {txt="BEQ"; ne=false; likely=true  };
+"bne",  BEQ {txt="BEQ"; ne=true ; likely=false };
+"bnel", BEQ {txt="BEQ"; ne=true ; likely=true  };
+
+"bltz",   BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=false };
+"bltzal", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=true  };
+"bltzl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true;  link=false };
+"bltzall",BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true;  link=true  };
+
+"bgez",   BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=false };
+"bgezal", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=true  };
+"bgezl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true;  link=false };
+"bgezall",BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true;  link=true  };
+
+"bgtz",   BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=false; link=false };
+"bgtzl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=true;  link=false };
+
+"blez",   BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=false; link=false };
+"blezl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=true;  link=false };
diff --git a/mips/hgen/map.hgen b/mips/hgen/map.hgen
new file mode 100644
index 00000000..68c9e46a
--- /dev/null
+++ b/mips/hgen/map.hgen
@@ -0,0 +1,14 @@
+| `MIPSRType  (op, rd, rs, rt)  -> `MIPSRType (op, map_reg rd, map_reg rs, map_reg rt)
+| `MIPSIType  (op, rs, rt, imm) -> `MIPSIType  (op, map_reg rs, map_reg rt, imm)
+| `MIPSShiftI (op, rd, rt, imm) -> `MIPSShiftI (op, map_reg rd, map_reg rt, imm)
+| `MIPSShiftV (op, rd, rt, rs)  -> `MIPSShiftV (op, map_reg rd, map_reg rt, map_reg rs)
+| `MIPSMulDiv (op, rs, rt)      -> `MIPSMulDiv (op, map_reg rs, map_reg rt)
+| `MIPSMFHiLo (op, rs)          -> `MIPSMFHiLo (op, map_reg rs)
+| `MIPSLUI (rt, imm)            -> `MIPSLUI (map_reg rt, imm)
+| `MIPSLoad (width, signed, linked, base, rt, offset) -> `MIPSLoad (width, signed, linked, map_reg base, map_reg rt, offset)
+| `MIPSStore (width, conditional, base, rt, offset) -> `MIPSStore (width, conditional, map_reg base, map_reg rt, offset)
+| `MIPSLSLR (store, double, left, base, rt, offset) -> `MIPSLSLR (store, double, left, map_reg base, map_reg rt, offset)
+| `MIPSSYNC -> `MIPSSYNC
+| `MIPSBEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ (map_reg rs, map_reg rt, offset, ne, likely)
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ (map_reg rs, offset, cmp, link, likely)
+
diff --git a/mips/hgen/parser.hgen b/mips/hgen/parser.hgen
new file mode 100644
index 00000000..bf15ab1e
--- /dev/null
+++ b/mips/hgen/parser.hgen
@@ -0,0 +1,26 @@
+| RTYPE ARCH_REG COMMA ARCH_REG COMMA ARCH_REG
+    { `MIPSRType ($1.op, $2, $4, $6) }
+| ITYPE ARCH_REG COMMA ARCH_REG COMMA NUM
+    { `MIPSIType ($1.op, $2, $4, $6) }
+| SHIFTI ARCH_REG COMMA ARCH_REG COMMA NUM
+    { `MIPSShiftI ($1.op, $2, $4, $6) }
+| SHIFTV ARCH_REG COMMA ARCH_REG COMMA ARCH_REG
+    { `MIPSShiftV ($1.op, $2, $4, $6) }
+| MULDIV ARCH_REG COMMA ARCH_REG
+    { `MIPSMulDiv ($1.op, $2, $4) }
+| MFHILO ARCH_REG
+    { `MIPSMFHiLo ($1.op, $2) }
+| LUI ARCH_REG COMMA NUM
+    { `MIPSLUI ($2, $4) }
+| LOAD ARCH_REG COMMA NUM LPAR ARCH_REG RPAR
+    { `MIPSLoad ($1.width, $1.signed, $1.linked, $6, $2, $4) }
+| STORE ARCH_REG COMMA NUM LPAR ARCH_REG RPAR
+    { `MIPSStore ($1.width, $1.conditional, $6, $2, $4) }
+| LSLR  ARCH_REG COMMA NUM LPAR ARCH_REG RPAR
+    { `MIPSLSLR ($1.store, $1.double, $1.left, $6, $2, $4) }
+| SYNC
+    { `MIPSSYNC }
+| BEQ ARCH_REG COMMA ARCH_REG COMMA NUM
+    { `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) }
+| BCMPZ ARCH_REG COMMA NUM
+    { `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) }
diff --git a/mips/hgen/pretty.hgen b/mips/hgen/pretty.hgen
new file mode 100644
index 00000000..43c41bb8
--- /dev/null
+++ b/mips/hgen/pretty.hgen
@@ -0,0 +1,27 @@
+| `MIPSThreadStart -> "START" (* TODO *)
+| `MIPSStopFetching -> "STOP" (* TODO *)
+| `MIPSRType (op, rd,rs,rt) ->
+      sprintf "%s %s,%s,%s" (pp_rtype_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt)
+| `MIPSIType (op,rd,rs,imm) ->
+      sprintf "%s %s,%s,%d" (pp_itype_op op) (pp_reg rd) (pp_reg rs) imm
+| `MIPSShiftI (op, rs, rt, imm) ->
+      sprintf "%s %s,%s,%d" (pp_shifti_op op) (pp_reg rs) (pp_reg rt) imm
+| `MIPSShiftV (op, rd,rs,rt) ->
+      sprintf "%s %s,%s,%s" (pp_shiftv_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt)
+| `MIPSMulDiv (op, rs, rt) ->
+      sprintf "%s %s,%s" (pp_muldiv_op op) (pp_reg rs) (pp_reg rt)
+| `MIPSMFHiLo (op, rs) ->
+      sprintf "%s %s" (pp_mfhilo_op op) (pp_reg rs)
+| `MIPSLUI (rt, imm) ->
+      sprintf "LUI %s,%d" (pp_reg rt) imm
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_load_op width signed linked) (pp_reg rt) offset (pp_reg base)
+| `MIPSStore (width, conditional, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_store_op width conditional) (pp_reg rt) offset (pp_reg base)
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_lslr_op store double left) (pp_reg rt) offset (pp_reg base)
+| `MIPSSYNC -> "SYNC"
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+      sprintf "%s, %s, %s, .%+d" (pp_beq_op ne likely) (pp_reg rs) (pp_reg rt) offset
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+      sprintf "%s, %s, .%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset
diff --git a/mips/hgen/regs_out_in.hgen b/mips/hgen/regs_out_in.hgen
new file mode 100644
index 00000000..8e1fd093
--- /dev/null
+++ b/mips/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/mips/hgen/sail_trans_out.hgen b/mips/hgen/sail_trans_out.hgen
new file mode 100644
index 00000000..5ecad705
--- /dev/null
+++ b/mips/hgen/sail_trans_out.hgen
@@ -0,0 +1,93 @@
+| ("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_imm16 imm))
+| ("ADDIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16 imm))
+| ("DADDIU", [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16 imm))
+| ("SLTIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 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_imm16  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_imm16  offset)
+   )
+| "LWL", [base; rt; offset] -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "LWR", [base; rt; offset] -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "LDL", [base; rt; offset] -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "LDR", [base; rt; offset] -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "SWL", [base; rt; offset] -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "SWR", [base; rt; offset] -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "SDL", [base; rt; offset] -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "SDR", [base; rt; offset] -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_imm16 offset))
+| "SYNC", [] -> `MIPSSYNC
+| "BEQ", [rs; rt; offset; ne; likely] -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_imm16 offset), (translate_out_bool ne), (translate_out_bool likely))
+| "BCMPZ", [rs; offset; cmp; link; likely] -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_imm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+
diff --git a/mips/hgen/token_types.hgen b/mips/hgen/token_types.hgen
new file mode 100644
index 00000000..2c2df1a6
--- /dev/null
+++ b/mips/hgen/token_types.hgen
@@ -0,0 +1,42 @@
+type token_RTYPE = {txt : string; op : mipsRTypeOp }
+type token_ITYPE = {txt : string; op : mipsITypeOp }
+type token_ShiftI = {txt : string; op : mipsShiftIOp }
+type token_ShiftV = {txt : string; op : mipsShiftVOp }
+type token_MulDiv = {txt : string; op : mipsMulDivOp }
+type token_MFHiLo = {txt : string; op : mipsMFHiLoOp }
+type token_LUI    = {txt : string }
+type token_Load   = {txt : string; width: mipsWordWidth; signed : bool; linked : bool}
+type token_Store  = {txt : string; width: mipsWordWidth; conditional : bool}
+type token_LSLR   = {txt : string; store : bool; double : bool; left: bool } (* Load/Store Left/Right *)
+type token_SYNC   = {txt : string}
+type token_BEQ    = {txt : string; ne : bool; likely : bool }
+type token_BCMPZ  = {txt : string; cmp : mipsCmp; likely : bool; link : bool }
+
+(*
+(bit[26]) J
+(bit[26]) JAL
+(regno, imm16, Comparison) TRAPIMM
+(regno, imm16, Comparison, bool, bool) BCMPZ
+
+(regno, regno) JALR
+
+(regno, regno) RDHWR
+(regno, regno, Comparison) TRAPREG
+(regno, regno, bit[3], bool) MFC0
+(regno, regno, bit[3], bool) MTC0
+(regno, regno, imm16, bool, bool) BEQ
+TLBP
+TLBR
+TLBWI
+TLBWR
+regno JR
+
+regregimm16 CACHE
+regregimm16 PREF
+
+unit BREAK
+unit ERET
+unit HCF
+unit SYSCALL
+unit WAIT
+*)
\ No newline at end of file
diff --git a/mips/hgen/tokens.hgen b/mips/hgen/tokens.hgen
new file mode 100644
index 00000000..00b99e8e
--- /dev/null
+++ b/mips/hgen/tokens.hgen
@@ -0,0 +1,13 @@
+%token <MIPSHGenBase.token_RTYPE> RTYPE
+%token <MIPSHGenBase.token_ITYPE> ITYPE
+%token <MIPSHGenBase.token_ShiftI> SHIFTI
+%token <MIPSHGenBase.token_ShiftV> SHIFTV
+%token <MIPSHGenBase.token_MulDiv> MULDIV
+%token <MIPSHGenBase.token_MFHiLo> MFHILO
+%token <MIPSHGenBase.token_LUI> LUI
+%token <MIPSHGenBase.token_Load> LOAD
+%token <MIPSHGenBase.token_Store> STORE
+%token <MIPSHGenBase.token_LSLR> LSLR
+%token <MIPSHGenBase.token_SYNC> SYNC
+%token <MIPSHGenBase.token_BEQ> BEQ
+%token <MIPSHGenBase.token_BCMPZ> BCMPZ
diff --git a/mips/hgen/trans_sail.hgen b/mips/hgen/trans_sail.hgen
new file mode 100644
index 00000000..5dcecfd2
--- /dev/null
+++ b/mips/hgen/trans_sail.hgen
@@ -0,0 +1,112 @@
+| `MIPSStopFetching ->
+    ("ImplementationDefinedStopFetching",
+      [],
+      [])
+
+(* Note different argument order, which reflects difference
+   between instruction encoding and asm format  *)
+| `MIPSRType (op, rd, rs, rt) ->
+    (pp_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) ->
+    (pp_itype_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      translate_imm16 "imm" imm;
+       ],
+      [])
+
+| `MIPSShiftI (op, rd, rt, sa) ->
+    (pp_shifti_op op,
+      [
+      translate_reg "rt" rt;
+      translate_reg "rd" rd;
+      translate_imm5 "sa" sa;
+       ],
+      [])
+
+| `MIPSShiftV (op, rd, rt, rs) ->
+    (pp_shiftv_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      translate_reg "rd" rd;
+      ],
+      [])
+
+| `MIPSMulDiv (op, rs, rt) ->
+    (pp_muldiv_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      ],
+      [])
+
+| `MIPSMFHiLo (op, rs) ->
+    (pp_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) ->
+  (pp_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;
+   ], [])
diff --git a/mips/hgen/types.hgen b/mips/hgen/types.hgen
new file mode 100644
index 00000000..ba576e06
--- /dev/null
+++ b/mips/hgen/types.hgen
@@ -0,0 +1,208 @@
+type mipsRTypeOp = 
+| MIPSROpADD
+| MIPSROpADDU
+| MIPSROpAND
+| MIPSROpDADD
+| MIPSROpDADDU
+| MIPSROpDSUB
+| MIPSROpDSUBU
+| MIPSROpMOVN
+| MIPSROpMOVZ
+| MIPSROpMUL
+| MIPSROpNOR
+| MIPSROpOR
+| MIPSROpSLT
+| MIPSROpSLTU
+| MIPSROpSUB
+| MIPSROpSUBU
+| MIPSROpXOR
+
+let pp_rtype_op = function
+| MIPSROpADD    -> "ADD"
+| MIPSROpADDU   -> "ADDU"
+| MIPSROpAND    -> "AND"
+| MIPSROpDADD   -> "DADD"
+| MIPSROpDADDU  -> "DADDU"
+| MIPSROpDSUB   -> "DSUB"
+| MIPSROpDSUBU  -> "DSUBU"
+| MIPSROpMOVN   -> "MOVN"
+| MIPSROpMOVZ   -> "MOVZ"
+| MIPSROpMUL    -> "MUL"
+| MIPSROpNOR    -> "NOR"
+| MIPSROpOR     -> "OR"
+| MIPSROpSLT    -> "SLT"
+| MIPSROpSLTU   -> "SLTU"
+| MIPSROpSUB    -> "SUB"
+| MIPSROpSUBU   -> "SUBU"
+| MIPSROpXOR    -> "XOR"
+
+type bit16 = int
+type bit5  = int
+
+type mipsITypeOp = 
+| MIPSIOpADDI
+| MIPSIOpADDIU
+| MIPSIOpANDI
+| MIPSIOpDADDI
+| MIPSIOpDADDIU
+| MIPSIOpORI
+| MIPSIOpSLTI
+| MIPSIOpSLTIU
+| MIPSIOpXORI
+
+let pp_itype_op = function
+| MIPSIOpADDI   -> "ADDI"
+| MIPSIOpADDIU  -> "ADDIU"
+| MIPSIOpANDI   -> "ANDI"
+| MIPSIOpDADDI  -> "DADDI"
+| MIPSIOpDADDIU -> "DADDIU"
+| MIPSIOpORI    -> "ORI"
+| MIPSIOpSLTI   -> "SLTI"
+| MIPSIOpSLTIU  -> "SLTIU"
+| MIPSIOpXORI   -> "XORI"
+
+type mipsShiftIOp = 
+| MIPSDSLL
+| MIPSDSLL32
+| MIPSDSRA
+| MIPSDSRA32
+| MIPSDSRL
+| MIPSDSRL32
+| MIPSSLL
+| MIPSSRA
+| MIPSSRL
+
+let pp_shifti_op = function
+| MIPSDSLL   -> "DSLL" 
+| MIPSDSLL32 -> "DSLL32"
+| MIPSDSRA   -> "DSRA"  
+| MIPSDSRA32 -> "DSRA32"
+| MIPSDSRL   -> "DSRL"  
+| MIPSDSRL32 -> "DSRL32"
+| MIPSSLL    -> "SLL"   
+| MIPSSRA    -> "SRA"   
+| MIPSSRL    -> "SRL"   
+
+type mipsShiftVOp = 
+| MIPSDSLLV
+| MIPSDSRAV
+| MIPSDSRLV
+| MIPSSLLV
+| MIPSSRAV
+| MIPSSRLV
+
+let pp_shiftv_op = function
+| MIPSDSLLV -> "DSLLV"
+| MIPSDSRAV -> "DSRAV"
+| MIPSDSRLV -> "DSRLV"
+| MIPSSLLV  -> "SLLV" 
+| MIPSSRAV  -> "SRAV" 
+| MIPSSRLV  -> "SRLV" 
+
+type mipsMulDivOp =
+| MIPSDDIV
+| MIPSDDIVU
+| MIPSDIV
+| MIPSDIVU
+| MIPSDMULT
+| MIPSDMULTU
+| MIPSMADD
+| MIPSMADDU
+| MIPSMSUB
+| MIPSMSUBU
+| MIPSMULT
+| MIPSMULTU
+
+let pp_muldiv_op = function
+| MIPSDDIV   -> "DDIV"  
+| MIPSDDIVU  -> "DDIVU" 
+| MIPSDIV    -> "DIV"   
+| MIPSDIVU   -> "DIVU"  
+| MIPSDMULT  -> "DMULT" 
+| MIPSDMULTU -> "DMULTU"
+| MIPSMADD   -> "MADD"  
+| MIPSMADDU  -> "MADDU" 
+| MIPSMSUB   -> "MSUB"  
+| MIPSMSUBU  -> "MSUBU" 
+| MIPSMULT   -> "MULT"  
+| MIPSMULTU  -> "MULTU" 
+
+type mipsMFHiLoOp =
+| MIPSMFHI
+| MIPSMFLO
+| MIPSMTHI
+| MIPSMTLO
+
+let pp_mfhilo_op = function
+| MIPSMFHI -> "MFHI"
+| MIPSMFLO -> "MFLO"
+| MIPSMTHI -> "MTHI"
+| MIPSMTLO -> "MTLO"
+
+type mipsWordWidth = 
+| MIPSByte
+| MIPSHalf
+| MIPSWord
+| MIPSDouble
+
+type mipsCmp =
+| MIPS_EQ  (* equal *)
+| MIPS_NE  (* not equal *)
+| MIPS_GE  (* signed greater than or equal *)
+| MIPS_GEU (* unsigned greater than or equal *) 
+| MIPS_GT  (* signed strictly greater than *) 
+| MIPS_LE  (* signed less than or equal *) 
+| MIPS_LT  (* signed strictly less than *) 
+| MIPS_LTU (* unsigned less than or qual *) 
+
+let pp_load_op width signed linked = match (width, signed, linked) with
+  | (MIPSByte, true, false)    -> "LB"
+  | (MIPSByte, false, false)   -> "LBU"
+  | (MIPSHalf, true, false)    -> "LH"
+  | (MIPSHalf, false, false)   -> "LHU"
+  | (MIPSWord, true, false)    -> "LW"
+  | (MIPSWord, false, false)   -> "LWU"
+  | (MIPSDouble, false, false) -> "LD"
+  | (MIPSWord, true, true)     -> "LL"
+  | (MIPSDouble, false, true)  -> "LLD"
+  | _                          -> failwith "unexpected load op"
+
+let pp_store_op width conditional = match (width, conditional) with
+  | (MIPSByte,   false) -> "SB"
+  | (MIPSHalf,   false) -> "SH"
+  | (MIPSWord,   false) -> "SW"
+  | (MIPSDouble, false) -> "SD"
+  | (MIPSWord,   true)  -> "SC"
+  | (MIPSDouble, true)  -> "SCD"
+  | _                   -> failwith "unexpected store op"
+
+let pp_lslr_op store double left = match (store, double, left) with
+  | (false, false, true ) -> "LWL"
+  | (false, false, false) -> "LWR"
+  | (false, true , true ) -> "LDL"
+  | (false, true , false) -> "LDR"
+  | (true , false, true ) -> "SWL"
+  | (true , false, false) -> "SWR"
+  | (true , true , true ) -> "SDL"
+  | (true , true , false) -> "SDR"
+
+let pp_beq_op ne likely = match (ne, likely) with
+  | (false, false) -> "BEQ"
+  | (false, true)  -> "BEQL"
+  | (true , false) -> "BNE"
+  | (true , true)  -> "BNEL"
+
+let pp_bcmpz_op cmp link likely = match (cmp, likely, link) with
+| (MIPS_LT, false , false ) -> "bltz"
+| (MIPS_LT, false , true  ) -> "bltzal"
+| (MIPS_LT, true  , false ) -> "bltzl"
+| (MIPS_LT, true  , true  ) -> "bltzall"
+| (MIPS_GE, false , false ) -> "bgez"
+| (MIPS_GE, false , true  ) -> "bgezal"
+| (MIPS_GE, true  , false ) -> "bgezl"
+| (MIPS_GE, true  , true  ) -> "bgezall"
+| (MIPS_GT, false , false ) -> "bgtz"
+| (MIPS_GT, true  , false ) -> "bgtzl"
+| (MIPS_LE, false , false ) -> "blez"
+| (MIPS_LE, true  , false ) -> "blezl"
+| _ -> failwith "unknown bcmpz instruction"
diff --git a/mips/hgen/types_sail_trans_out.hgen b/mips/hgen/types_sail_trans_out.hgen
new file mode 100644
index 00000000..c48c4b6f
--- /dev/null
+++ b/mips/hgen/types_sail_trans_out.hgen
@@ -0,0 +1,39 @@
+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_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_imm16 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 inst = 
+    match translate_out_enum inst with
+    | 0 -> MIPSByte
+    | 1 -> MIPSHalf
+    | 2 -> MIPSWord
+    | 3 -> MIPSDouble
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_cmp inst = 
+    match translate_out_enum inst with
+    | 0 -> MIPS_EQ  (* equal *)
+    | 1 -> MIPS_NE  (* not equal *)
+    | 2 -> MIPS_GE  (* signed greater than or equal *)
+    | 3 -> MIPS_GEU (* unsigned greater than or equal *) 
+    | 4 -> MIPS_GT  (* signed strictly greater than *) 
+    | 5 -> MIPS_LE  (* signed less than or equal *) 
+    | 6 -> MIPS_LT  (* signed strictly less than *) 
+    | 7 -> MIPS_LTU (* unsigned less than or qual *) 
+    | _ -> failwith "Unknown mipsCmp in sail translate out"
diff --git a/mips/hgen/types_trans_sail.hgen b/mips/hgen/types_trans_sail.hgen
new file mode 100644
index 00000000..111cc3fd
--- /dev/null
+++ b/mips/hgen/types_trans_sail.hgen
@@ -0,0 +1,30 @@
+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_imm16 name value = 
+    (name, Bvector (Some 16), bit_list_of_integer 16 (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])
+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_wordsize = translate_enum [MIPSByte; MIPSHalf; MIPSWord; MIPSDouble]
+let translate_cmp = translate_enum [
+MIPS_EQ  ;(* equal *)
+MIPS_NE  ;(* not equal *)
+MIPS_GE  ;(* signed greater than or equal *)
+MIPS_GEU ;(* unsigned greater than or equal *) 
+MIPS_GT  ;(* signed strictly greater than *) 
+MIPS_LE  ;(* signed less than or equal *) 
+MIPS_LT  ;(* signed strictly less than *) 
+MIPS_LTU ;(* unsigned less than or qual *) 
+]
\ No newline at end of file
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index b282764d..80350af1 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -499,100 +499,6 @@ function unit incrementCP0Count() = {
     SignalException(Int);
 }
 
-function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = 
-      let entryValid = entry.valid in
-      let entryR     = entry.r in
-      let entryMask  = entry.pagemask in
-      let entryVPN   = entry.vpn2 in
-      let entryASID  = entry.asid in
-      let entryG     = entry.g in
-      (entryValid &
-       (r == entryR) & 
-       ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
-       ((asid == (entryASID)) | (entryG)))
-
-function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
-  let r    = (VAddr[63..62]) in
-  let vpn2 = (VAddr[39..13]) in
-  let asid = TLBEntryHi.ASID in {
-    foreach (idx from 0 to 63) {
-      if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then
-        return (Some ((TLBIndexT) idx))
-    };
-    None
-  }
-
-function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
-  let idx = tlbSearch(vAddr) in
-  switch(idx) {
-    case (Some(idx)) -> 
-    let entry = (TLBEntries[idx]) in
-    let entryMask = entry.pagemask in
-    
-    let evenOddBit = switch(entryMask) {
-      case 0x0000 -> 12
-      case 0x0003 -> 14
-      case 0x000f -> 16
-      case 0x003f -> 18
-      case 0x00ff -> 20
-      case 0x03ff -> 22
-      case 0x0fff -> 24
-      case 0x3fff -> 26
-      case 0xffff -> 28
-      case _      -> undefined
-    } in
-    let isOdd = (vAddr[evenOddBit]) in
-    let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then
-        (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1)
-      else
-        (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
-    if (~(v)) then 
-      (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
-    else if ((accessType == StoreData) & ~(d)) then
-      (SignalExceptionTLB(TLBMod, vAddr))
-    else
-      (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), 
-       if (accessType == StoreData) then caps else capl)
-    case None ->  (SignalExceptionTLB(
-      if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
-  }
-}
-
-function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = 
-  {
-    let currentAccessLevel = getAccessLevel() in
-    let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
-    let (requiredLevel, addr) = switch(vAddr[63..62]) {
-      case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *)
-        case (true, 0b11) -> (Kernel, None)               (* kseg3 mapped 32-bit compat *)
-        case (true, 0b10) -> (Supervisor, None)           (* sseg  mapped 32-bit compat *)
-        case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
-        case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
-        case (_, _) -> (Kernel, None) (* xkseg mapped *)
-      }
-      case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0])))       (* xkphys bits 61-59 are cache mode (ignored) *)
-      case 0b01 -> (Supervisor, None)                       (* xsseg - supervisor mapped *)
-      case 0b00 -> (User, None) (* xuseg - user mapped *)
-    } in
-    if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
-      (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
-    else 
-      let (pa, c) = switch(addr) {
-      case (Some(a)) -> (a, false)
-      case None      -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
-          (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
-        else
-          TLBTranslate2(vAddr, accessType)
-      }
-      in if (unsigned(pa) > MAX_PA) then
-          (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
-        else
-          (pa, c)
-  }
-
-function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
-      let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
-
 typedef regno = bit[5]                      (* a register number *)
 typedef imm16 = bit[16]                     (* 16-bit immediate *)
 (* a commonly used instruction format with three register operands *)
diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail
new file mode 100644
index 00000000..e2549dd6
--- /dev/null
+++ b/mips/mips_tlb.sail
@@ -0,0 +1,94 @@
+
+function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = 
+      let entryValid = entry.valid in
+      let entryR     = entry.r in
+      let entryMask  = entry.pagemask in
+      let entryVPN   = entry.vpn2 in
+      let entryASID  = entry.asid in
+      let entryG     = entry.g in
+      (entryValid &
+       (r == entryR) & 
+       ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
+       ((asid == (entryASID)) | (entryG)))
+
+function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
+  let r    = (VAddr[63..62]) in
+  let vpn2 = (VAddr[39..13]) in
+  let asid = TLBEntryHi.ASID in {
+    foreach (idx from 0 to 63) {
+      if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then
+        return (Some ((TLBIndexT) idx))
+    };
+    None
+  }
+
+function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
+  let idx = tlbSearch(vAddr) in
+  switch(idx) {
+    case (Some(idx)) -> 
+    let entry = (TLBEntries[idx]) in
+    let entryMask = entry.pagemask in
+    
+    let evenOddBit = switch(entryMask) {
+      case 0x0000 -> 12
+      case 0x0003 -> 14
+      case 0x000f -> 16
+      case 0x003f -> 18
+      case 0x00ff -> 20
+      case 0x03ff -> 22
+      case 0x0fff -> 24
+      case 0x3fff -> 26
+      case 0xffff -> 28
+      case _      -> undefined
+    } in
+    let isOdd = (vAddr[evenOddBit]) in
+    let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then
+        (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1)
+      else
+        (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
+    if (~(v)) then 
+      (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
+    else if ((accessType == StoreData) & ~(d)) then
+      (SignalExceptionTLB(TLBMod, vAddr))
+    else
+      (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), 
+       if (accessType == StoreData) then caps else capl)
+    case None ->  (SignalExceptionTLB(
+      if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
+  }
+}
+
+function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = 
+  {
+    let currentAccessLevel = getAccessLevel() in
+    let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
+    let (requiredLevel, addr) = switch(vAddr[63..62]) {
+      case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *)
+        case (true, 0b11) -> (Kernel, None)               (* kseg3 mapped 32-bit compat *)
+        case (true, 0b10) -> (Supervisor, None)           (* sseg  mapped 32-bit compat *)
+        case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
+        case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
+        case (_, _) -> (Kernel, None) (* xkseg mapped *)
+      }
+      case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0])))       (* xkphys bits 61-59 are cache mode (ignored) *)
+      case 0b01 -> (Supervisor, None)                       (* xsseg - supervisor mapped *)
+      case 0b00 -> (User, None) (* xuseg - user mapped *)
+    } in
+    if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
+      (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+    else 
+      let (pa, c) = switch(addr) {
+      case (Some(a)) -> (a, false)
+      case None      -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
+          (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+        else
+          TLBTranslate2(vAddr, accessType)
+      }
+      in if (unsigned(pa) > MAX_PA) then
+          (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+        else
+          (pa, c)
+  }
+
+function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
+      let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail
new file mode 100644
index 00000000..b2ddfca8
--- /dev/null
+++ b/mips/mips_tlb_stub.sail
@@ -0,0 +1,4 @@
+function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = None
+
+function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
+      vAddr
diff --git a/src/Makefile b/src/Makefile
index 937c76c9..7849e666 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,9 +25,10 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
 ELFDIR= $(BITBUCKET_ROOT)/linksem
 
 MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
-CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 elf:
 	make -C $(ELFDIR)
@@ -48,6 +49,11 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o mips $(MIPS_SAILS)
 
+_build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
+	mkdir -p _build
+	cd _build ; \
+	../sail.native -lem_ast -o mips_notlb $(MIPS_NOTLB_SAILS)
+
 _build/cheri.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
@@ -74,6 +80,9 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
+mips_notlb: _build/mips_notlb.ml  _build/mips_extras.ml
+	true
+
 mips: elf run_mips.native
 
 cheri: elf run_cheri.native