Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2

2 files changed, 1519 insertions, 0 deletions

diff --git a/mips/mips.sail b/mips/mips.sail
new file mode 100644
index 00000000..fc639d65
--- /dev/null
+++ b/mips/mips.sail
@@ -0,0 +1,1517 @@
+(* bit vectors have indices decreasing from left i.e. msb is highest index *)
+default Order dec
+
+(* external functions *)
+val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
+val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
+
+register (bit[64]) PC
+
+(* CP0 Registers *)
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+register (CauseReg) CP0Cause
+register (bit[64]) CP0EPC
+
+typedef StatusReg = register bits [31:0] {
+  31 .. 28        : CU;  (* co-processor enable bits *)
+  (* RP/FR/RE/MX/PX not implemented *)
+  22              : BEV; (* use boot exception vectors XXX initialise to one *)
+  (* TS/SR/NMI not implemented *)
+  15 .. 8         : IM;  (* Interrupt mask *)
+  (* KX/SX/UX not implemented (XXX initialise to one) *)
+  4 .. 3          : KSU; (* Processor mode *)
+  2               : ERL; (* error level XXX initialise to one *)
+  1               : EXL; (* exception level *)
+  0               : IE;  (* interrupt enable *)
+}
+register (StatusReg) CP0Status
+
+(* Implementation registers -- not ISA defined *)
+register (bit[1])  branchPending
+register (bit[1])  inBranchDelay
+register (bit[1])  exceptionSignalled
+register (bit[64]) delayedPC
+
+(* General purpose registers *)
+
+register (bit[64]) GPR0 (* should never be read or written *)
+register (bit[64]) GPR1
+register (bit[64]) GPR2
+register (bit[64]) GPR3
+register (bit[64]) GPR4
+register (bit[64]) GPR5
+register (bit[64]) GPR6
+register (bit[64]) GPR7
+register (bit[64]) GPR8
+register (bit[64]) GPR9
+register (bit[64]) GPR10
+register (bit[64]) GPR11
+register (bit[64]) GPR12
+register (bit[64]) GPR13
+register (bit[64]) GPR14
+register (bit[64]) GPR15
+register (bit[64]) GPR16
+register (bit[64]) GPR17
+register (bit[64]) GPR18
+register (bit[64]) GPR19
+register (bit[64]) GPR20
+register (bit[64]) GPR21
+register (bit[64]) GPR22
+register (bit[64]) GPR23
+register (bit[64]) GPR24
+register (bit[64]) GPR25
+register (bit[64]) GPR26
+register (bit[64]) GPR27
+register (bit[64]) GPR28
+register (bit[64]) GPR29
+register (bit[64]) GPR30
+register (bit[64]) GPR31
+
+(* Special registers For MUL/DIV *)
+register (bit[64]) HI
+register (bit[64]) LO
+
+let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
+  [ GPR0, GPR1, GPR2, GPR3, GPR4, GPR5, GPR6, GPR7, GPR8, GPR9, GPR10,
+  GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
+  GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
+  ]
+
+(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
+val bit[64] -> bool effect pure isWordVal
+function bool NotWordVal (word) = 
+    (word[31] ^^ 32) != word[63..32]
+
+val bit[5] -> bit[64] effect {rreg} rGPR
+function bit[64] rGPR idx = {
+         if idx == 0 then 0 else GPR[idx]
+}
+
+val (bit[5], bit[64]) -> unit effect {wreg} wGPR
+function unit wGPR (idx, v) = {
+         if idx == 0 then () else GPR[idx] := v
+}
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmem } MEMw_conditional
+val extern unit -> unit effect { barr } MEM_sync
+
+typedef Exception = enumerate
+{
+   Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E;
+   XTLBRefillL; XTLBRefillS
+}
+
+(* Return the ISA defined code for an exception condition *)
+function (bit[5]) ExceptionCode ((Exception) ex) =
+   switch (ex)
+   {
+      case Int         -> mask(0x00) (* Interrupt *)
+      case Mod         -> mask(0x01) (* TLB modification exception *)
+      case TLBL        -> mask(0x02) (* TLB exception (load or fetch) *)
+      case TLBS        -> mask(0x03) (* TLB exception (store) *)
+      case AdEL        -> mask(0x04) (* Address error (load or fetch) *)
+      case AdES        -> mask(0x05) (* Address error (store) *)
+      case Sys         -> mask(0x08) (* Syscall *)
+      case Bp          -> mask(0x09) (* Breakpoint *)
+      case ResI        -> mask(0x0a) (* Reserved instruction *)
+      case CpU         -> mask(0x0b) (* Coprocessor Unusable *)
+      case Ov          -> mask(0x0c) (* Arithmetic overflow *)
+      case Tr          -> mask(0x0d) (* Trap *)
+      case C2E         -> mask(0x12) (* C2E coprocessor 2 exception *)
+      case XTLBRefillL -> mask(0x02)
+      case XTLBRefillS -> mask(0x03)
+   }
+
+
+function unit SignalException ((Exception) ex) = 
+  {
+    CP0Cause.ExcCode := ExceptionCode(ex);
+    CP0Status.EXL         := 1;
+    exceptionSignalled    := 1;
+    (* Only update EPC and BD if not already in EXL mode *)
+    if (~ (CP0Status.EXL)) then 
+      {
+        if (inBranchDelay) then
+          {
+            CP0EPC := PC - 4;
+            CP0Cause.BD := 1;
+          }
+        else
+          {
+            CP0EPC := PC;
+            CP0Cause.BD := 0;
+          }
+      };
+
+      (* choose an exception vector to branch to *)
+      vectorOffset := if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) & ~ (CP0Status.EXL) then
+                     0x080
+                  else
+                     0x180;
+      (bit[64]) vectorBase  := if CP0Status.BEV then
+                   0xFFFFFFFFBFC00200
+                else
+                   0xFFFFFFFF80000000;
+      PC := vectorBase + EXTS(vectorOffset);
+  }
+
+typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
+function (bool, bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
+  {
+    (false, vAddr)
+  }
+
+typedef regno = bit[5]                      (* a register number *)
+typedef imm16 = bit[16]                     (* 16-bit immediate *)
+typedef regregreg   = (regno, regno, regno) (* a commonly used instruction format with three register operands *)
+typedef regregimm16 = (regno, regno, imm16) (* a commonly used instruction format with two register operands and 16-bit immediate *)
+typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction; internal_error }
+(* Used by branch and trap instructions *)
+typedef Comparison = enumerate { 
+  EQ; (* equal *)
+  NE; (* not equal *)
+  GE; (* signed greater than or equal *)
+  GEU;(* unsigned greater than or equal *) 
+  GT; (* signed strictly greater than *) 
+  LE; (* signed less than or equal *) 
+  LT; (* signed strictly less than *) 
+  LTU;(* unsigned less than or qual *) 
+}
+function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) =
+  switch(cmp) {
+    case EQ  -> valA ==   valB
+    case NE  -> valA !=   valB
+    case GE  -> valA >=_s valB
+    case GEU -> valA >=   valB
+    case GT  -> valA >    valB
+    case LE  -> valA <=_s valB
+    case LT  -> valA <_s  valB
+    case LTU -> valA <    valB
+  }
+typedef WordType = enumerate { B; H; W; D}
+function nat wordWidthBytes((WordType) w) =
+  switch(w) {
+    case B -> 1
+    case H -> 2
+    case W -> 4
+    case D -> 8
+  }
+function nat logWordWidth((WordType) w) =
+  switch(w) {
+    case B -> 0
+    case H -> 1
+    case W -> 2
+    case D -> 3
+  }
+scattered function unit execute
+scattered typedef ast = const union
+
+val bit[32] -> ast effect pure decode
+scattered function ast decode
+
+(**************************************************************************************)
+(* [D]ADD[I][U] various forms of ADD                                                  *)
+(**************************************************************************************)
+
+(* DADDIU Doubleword Add Immediate Unsigned -- 
+   the simplest possible instruction, no undefined behaviour or exceptions 
+   reg, reg, immediate *)
+
+union ast member regregimm16 DADDIU
+
+function clause decode (0b011001 : (regno) rs : (regno) rt : (imm16) imm) = 
+  DADDIU(rs, rt, imm)
+
+function clause execute (DADDIU (rs, rt, imm)) =
+  {
+    wGPR(rt) := rGPR(rs) + EXTS(imm)
+  }
+
+(* DADDU Doubleword Add Unsigned -- another very simple instruction,
+   reg, reg, reg *)
+
+union ast member regregreg DADDU
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101101) = 
+  DADDU(rs, rt, rd)
+
+function clause execute (DADDU (rs, rt, rd)) =
+  {
+    wGPR(rd) := rGPR(rs) + rGPR(rt)
+  }
+
+(* DADDI Doubleword Add Immediate
+   reg, reg, imm with possible exception *)
+
+union ast member regregimm16 DADDI
+
+function clause decode (0b011000 : (regno) rs : (regno) rt : (imm16) imm) = 
+  DADDI(rs, rt, imm)
+
+function clause execute (DADDI (rs, rt, imm)) =
+  {
+    let (temp, overflow, _) = (rGPR(rs) +_s EXTS(imm)) in (* XXX is this the same definition of overflow as in spec? *)
+    {
+      if overflow then
+        SignalException(Ov)
+      else
+        wGPR(rt) := temp
+    }
+  }
+
+(* DADD Doubleword Add
+   reg, reg, reg with possible exception *)
+
+union ast member regregreg DADD
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = 
+  DADD(rs, rt, rd)
+
+function clause execute (DADD (rs, rt, rd)) =
+  {
+    let (temp, overflow, _) = (rGPR(rs) +_s rGPR(rt)) in
+    {
+      if overflow then
+        SignalException(Ov)
+      else
+        wGPR(rd) := temp
+    }
+  }
+
+(* ADD   32-bit add           -- reg, reg, reg with possible undefined behaviour or exception *)
+
+union ast member regregreg ADD
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100000) =
+  ADD(rs, rt, rd)
+
+function clause execute (ADD(rs, rt, rd)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    (bit[64]) opB := rGPR(rt);
+    if NotWordVal(opA) | NotWordVal(opB) then
+      wGPR(rd) := undefined (* XXX could exit instead *)
+    else
+      let ((bit[32]) temp, overflow, _) = ((opA[31 .. 0]) +_s (opB[31 .. 0])) in
+        if overflow then
+          SignalException(Ov)
+        else
+          wGPR(rd) := EXTS(temp)
+  }
+
+(* ADDI  32-bit add immediate -- reg, reg, imm with possible undefined behaviour or exception *)
+
+union ast member regregimm16 ADDI
+
+function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) =
+  ADDI(rs, rt, imm)
+
+function clause execute (ADDI(rs, rt, imm)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    if NotWordVal(opA) then
+      wGPR(rt) := undefined (* XXX could exit instead *)
+    else
+      let ((bit[32]) temp, overflow, _) = ((opA[31 .. 0]) +_s EXTS(imm)) in
+        if overflow then
+          SignalException(Ov)
+        else
+          wGPR(rt) := EXTS(temp)
+  }
+
+(* ADDU  32-bit add immediate -- reg, reg, reg with possible undefined behaviour *)
+
+union ast member regregreg ADDU
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100001) =
+  ADDU(rs, rt, rd)
+
+function clause execute (ADDU(rs, rt, rd)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    (bit[64]) opB := rGPR(rt);
+    if NotWordVal(opA) | NotWordVal(opB) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := EXTS(opA[31..0] + opB[31..0])
+  }
+
+
+(* ADDIU 32-bit add immediate -- reg, reg, imm with possible undefined behaviour *)
+
+union ast member regregimm16 ADDIU
+
+function clause decode (0b001000 : (regno) rs : (regno) rt : (imm16) imm) =
+  ADDIU(rs, rt, imm)
+
+function clause execute (ADDIU(rs, rt, imm)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    if NotWordVal(opA) then
+      wGPR(rt) := undefined (* XXX could exit instead *)
+    else
+      let ((bit[32]) temp, overflow, _) = ((opA[31 .. 0]) +_s EXTS(imm)) in
+        if overflow then
+          SignalException(Ov)
+        else
+          wGPR(rt) := EXTS(temp)
+  }
+
+(**************************************************************************************)
+(* [D]SUB[U] various forms of SUB                                                     *)
+(**************************************************************************************)
+
+(* DSUBU doubleword subtract 'unsigned' reg, reg, reg *)
+
+union ast member regregreg DSUBU
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = 
+  DSUBU(rs, rt, rd)
+
+function clause execute (DSUBU (rs, rt, rd)) =
+  {
+    wGPR(rd) := rGPR(rs) - rGPR(rt)
+  }
+
+(* DSUB reg, reg, reg with possible exception *)
+
+union ast member regregreg DSUB
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101110) = 
+  DSUB(rs, rt, rd)
+
+function clause execute (DSUB (rs, rt, rd)) =
+  {
+    let (temp, overflow, _) = (rGPR(rs) -_s rGPR(rt)) in
+    {
+      if overflow then
+        SignalException(Ov)
+      else
+        wGPR(rd) := temp
+    }
+  }
+
+(* SUB   32-bit sub           -- reg, reg, reg with possible undefined behaviour or exception *)
+
+union ast member regregreg SUB
+
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100010) =
+  SUB(rs, rt, rd)
+
+function clause execute (SUB(rs, rt, rd)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    (bit[64]) opB := rGPR(rt);
+    if NotWordVal(opA) | NotWordVal(opB) then
+      wGPR(rd) := undefined (* XXX could exit instead *)
+    else
+      let ((bit[32]) temp, overflow, _) = ((opA[31 .. 0]) -_s (opB[31 .. 0])) in
+        if overflow then
+          SignalException(Ov)
+        else
+          wGPR(rd) := EXTS(temp)
+  }
+
+(* SUBU  32-bit 'unsigned' sub -- reg, reg, reg with possible undefined behaviour *)
+
+union ast member regregreg SUBU
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100011) =
+  SUBU(rs, rt, rd)
+function clause execute (SUBU(rs, rt, rd)) = 
+  {
+    (bit[64]) opA := rGPR(rs);
+    (bit[64]) opB := rGPR(rt);
+    if NotWordVal(opA) | NotWordVal(opB) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := EXTS(opA[31..0] - opB[31..0])
+  }
+
+(**************************************************************************************)
+(* Logical bitwise operations                                                         *)
+(**************************************************************************************)
+
+(* AND reg, reg, reg *)
+
+union ast member regregreg AND
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100100) = 
+  AND(rs, rt, rd)
+function clause execute (AND (rs, rt, rd)) =
+  {
+    wGPR(rd) := (rGPR(rs) & rGPR(rt))
+  }
+
+(* ANDI reg, reg, imm *)
+
+union ast member regregimm16 ANDI
+function clause decode (0b001100 : (regno) rs : (regno) rt : (imm16) imm) = 
+  ANDI(rs, rt, imm)
+function clause execute (ANDI (rs, rt, imm)) =
+  {
+    wGPR(rt) := (rGPR(rs) & EXTZ(imm))
+  }
+
+(* OR reg, reg, reg *)
+
+union ast member regregreg OR
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100101) = 
+  OR(rs, rt, rd)
+function clause execute (OR (rs, rt, rd)) =
+  {
+    wGPR(rd) := (rGPR(rs) | rGPR(rt))
+  }
+
+(* ORI reg, reg, imm *)
+
+union ast member regregimm16 ORI
+function clause decode (0b001101 : (regno) rs : (regno) rt : (imm16) imm) = 
+  ORI(rs, rt, imm)
+function clause execute (ORI (rs, rt, imm)) =
+  {
+    wGPR(rt) := (rGPR(rs) | EXTZ(imm))
+  }
+
+(* NOR reg, reg, reg *)
+
+union ast member regregreg NOR
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100111) = 
+  NOR(rs, rt, rd)
+function clause execute (NOR (rs, rt, rd)) =
+  {
+    wGPR(rd) := ~(rGPR(rs) | rGPR(rt))
+  }
+
+(* XOR reg, reg, reg *)
+
+union ast member regregreg XOR
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b100110) = 
+  XOR(rs, rt, rd)
+function clause execute (XOR (rs, rt, rd)) =
+  {
+    wGPR(rd) := (rGPR(rs) ^ rGPR(rt))
+  }
+
+(* XORI reg, reg, imm *)
+union ast member regregimm16 XORI
+function clause decode (0b001110 : (regno) rs : (regno) rt : (imm16) imm) = 
+  XORI(rs, rt, imm)
+function clause execute (XORI (rs, rt, imm)) =
+  {
+    wGPR(rt) := (rGPR(rs) ^ EXTZ(imm))
+  }
+
+(* LUI reg, imm 32-bit load immediate into upper 16 bits *)
+union ast member (regno, imm16) LUI 
+function clause decode (0b001111 : 0b00000 : (regno) rt : (imm16) imm) = 
+  LUI(rt, imm)
+function clause execute (LUI (rt, imm)) =
+  {
+    wGPR(rt) := EXTS(imm : 0x0000)
+  }
+
+(**************************************************************************************)
+(* 64-bit  shift operations                                                           *)
+(**************************************************************************************)
+
+(* DSLL reg, reg, imm5 *)
+
+union ast member regregreg DSLL
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111000) = 
+  DSLL(rt, rd, sa)
+function clause execute (DSLL (rt, rd, sa)) =
+  {
+    
+    wGPR(rd) := (rGPR(rt) << sa) (* make tuareg mode less blue >> *)
+  }
+
+(* DSLL32 reg, reg, imm5 *)
+
+union ast member regregreg DSLL32
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111100) = 
+  DSLL32(rt, rd, sa)
+function clause execute (DSLL32 (rt, rd, sa)) =
+  {
+    wGPR(rd) := (rGPR(rt) << (1 : sa)) (* make tuareg mode less blue >> *)
+  }
+
+(* DSLLV reg, reg, reg *)
+
+union ast member regregreg DSLLV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101100) = 
+  DSLLV(rs, rt, rd)
+function clause execute (DSLLV (rs, rt, rd)) =
+  {
+    wGPR(rd) := (rGPR(rs) << ((rGPR(rt))[5:0])) (* make tuareg mode less blue >> *)
+  }
+
+(* DSRA arithmetic shift duplicating sign bit - reg, reg, imm5 *)
+
+union ast member regregreg DSRA
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111011) = 
+  DSRA(rt, rd, sa)
+function clause execute (DSRA (rt, rd, sa)) =
+  {
+    temp     := rGPR(rt);
+    wGPR(rd) := ((temp[63] ^^ sa) : (temp[63 .. sa]))
+  }
+
+(* DSRA32 reg, reg, imm5 *)
+
+union ast member regregreg DSRA32
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111111) = 
+  DSRA32(rt, rd, sa)
+function clause execute (DSRA32 (rt, rd, sa)) =
+  {
+    temp     := rGPR(rt);
+    sa32     := (0b1 : sa); (* sa+32 *)
+    wGPR(rd) := ((temp[63] ^^ sa32) : (temp[63 .. sa32]))
+  }
+
+(* DSRAV reg, reg, reg *)
+union ast member regregreg DSRAV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101111) = 
+  DSRAV(rs, rt, rd)
+function clause execute (DSRAV (rs, rt, rd)) =
+  {
+    temp     := rGPR(rt);
+    sa       := (rGPR(rs)) [5..0];
+    wGPR(rd) := ((temp[63] ^^ sa) : temp[63 .. sa])
+  }
+
+(* DSRL shift right logical - reg, reg, imm5 *)
+
+union ast member regregreg DSRL
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111010) = 
+  DSRL(rt, rd, sa)
+function clause execute (DSRL (rt, rd, sa)) =
+  {
+    temp     := rGPR(rt);
+    wGPR(rd) := ((bitzero ^^ sa) : (temp[63 .. sa]))
+  }
+
+(* DSRL32 reg, reg, imm5 *)
+
+union ast member regregreg DSRL32
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (bit[5]) sa : 0b111110) = 
+  DSRA32(rt, rd, sa)
+function clause execute (DSRL32 (rt, rd, sa)) =
+  {
+    temp     := rGPR(rt);
+    sa32     := (0b1 : sa); (* sa+32 *)
+    wGPR(rd) := ((bitzero ^^ sa32) : (temp[63 .. sa32]))
+  }
+
+(* DSRLV reg, reg, reg *)
+
+union ast member regregreg DSRLV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b010110) = 
+  DSRLV(rs, rt, rd)
+function clause execute (DSRLV (rs, rt, rd)) =
+  {
+    temp     := rGPR(rt);
+    sa       := (rGPR(rs)) [5..0];
+    wGPR(rd) := ((bitone ^^ sa) : temp[63 .. sa])
+  }
+
+(**************************************************************************************)
+(* 32-bit  shift operations                                                           *)
+(**************************************************************************************)
+
+(* SLL 32-bit shift left *)
+
+union ast member regregreg SLL
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000000) = 
+  SLL(rt, rd, sa)
+function clause execute (SLL(rt, rd, sa)) =
+  {
+    wGPR(rd) := EXTS((rGPR(rt)) [(31-sa)..0] : (bitzero ^^ sa))
+  }
+
+(* SLLV 32-bit shift left variable *)
+
+union ast member regregreg SLLV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000100) = 
+  SLLV(rs, rt, rd)
+function clause execute (SLLV(rs, rt, rd)) =
+  {
+    sa       := (rGPR(rs))[4..0];
+    wGPR(rd) := EXTS((rGPR(rt)) [(31-sa)..0] : (bitzero ^^ sa))
+  }
+
+(* SRA 32-bit arithmetic shift right *)
+
+union ast member regregreg SRA
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000011) = 
+  SRA(rt, rd, sa)
+function clause execute (SRA(rt, rd, sa)) =
+  {
+    temp := rGPR(rt);
+    if (NotWordVal(temp)) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := (temp[31] ^^ (sa+32)) : temp [31..sa]
+  }
+
+(* SRAV 32-bit arithmetic shift right variable *)
+
+union ast member regregreg SRAV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000111) = 
+  SRAV(rs, rt, rd)
+function clause execute (SRAV(rs, rt, rd)) =
+  {
+    temp := rGPR(rt);
+    sa   := (rGPR(rs))[4..0];
+    if (NotWordVal(temp)) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := (temp[31] ^^ (sa+32)) : temp [31..sa]
+  }
+
+(* SRL 32-bit shift right *)
+
+union ast member regregreg SRL
+function clause decode (0b000000 : 0b00000 : (regno) rt : (regno) rd : (regno) sa : 0b000010) = 
+  SRL(rt, rd, sa)
+function clause execute (SRL(rt, rd, sa)) =
+  {
+    temp := rGPR(rt);
+    if (NotWordVal(temp)) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+  }
+
+(* SRLV 32-bit shift right variable *)
+
+union ast member regregreg SRLV
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000110) = 
+  SRLV(rs, rt, rd)
+function clause execute (SRLV(rs, rt, rd)) =
+  {
+    temp := rGPR(rt);
+    sa   := (rGPR(rs))[4..0];
+    if (NotWordVal(temp)) then
+      wGPR(rd) := undefined
+    else
+      wGPR(rd) := EXTS((bitzero ^^ sa) : (temp [31..sa]))
+  }
+
+(**************************************************************************************)
+(* set less than / conditional move                                                    *)
+(**************************************************************************************)
+
+(* SLT set if less than (signed) *)
+
+union ast member regregreg SLT
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101010) = 
+  SLT(rs, rt, rd)
+function clause execute (SLT(rs, rt, rd)) =
+  {
+    wGPR(rd) := if (rGPR(rs) <_s rGPR(rt)) then 1 else 0
+  }
+
+(* SLT set if less than immediate (signed) *)
+
+union ast member regregimm16 SLTI
+function clause decode (0b001010 : (regno) rs : (regno) rt : (imm16) imm) = 
+  SLTI(rs, rt, imm)
+function clause execute (SLTI(rs, rt, imm)) =
+  {
+    wGPR(rt) := if (rGPR(rs) <_s EXTS(imm)) then 1 else 0
+  }
+
+(* SLTU set if less than unsigned *)
+
+union ast member regregreg SLTU
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b101011) = 
+  SLT(rs, rt, rd)
+function clause execute (SLTU(rs, rt, rd)) =
+  {
+    wGPR(rd) := if (rGPR(rs) < rGPR(rt)) then 1 else 0
+  }
+
+(* SLTIU set if less than immediate unsigned *)
+
+union ast member regregimm16 SLTIU
+function clause decode (0b001011 : (regno) rs : (regno) rt : (imm16) imm) = 
+  SLTIU(rs, rt, imm)
+function clause execute (SLTIU(rs, rt, imm)) =
+  {
+    wGPR(rt) := if (rGPR(rs) < EXTS(imm)) then 1 else 0
+  }
+
+(* MOVN move if non-zero *)
+
+union ast member regregreg MOVN
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001011) = 
+  MOVN(rs, rt, rd)
+function clause execute (MOVN(rs, rt, rd)) =
+  {
+    if (rGPR(rt) != 0) then 
+      wGPR(rd) := rGPR(rs)
+  }
+
+(* MOVZ move if zero *)
+
+union ast member regregreg MOVZ
+function clause decode (0b000000 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b001010) = 
+  MOVZ(rs, rt, rd)
+function clause execute (MOVZ(rs, rt, rd)) =
+  {
+    if (rGPR(rt) == 0) then 
+      wGPR(rd) := rGPR(rs)
+  }
+
+(******************************************************************************)
+(* MUL/DIV instructions                                                       *)
+(******************************************************************************)
+
+(* MFHI move from HI register *)
+union ast member regno MFHI
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010000) = 
+  MFHI(rd)
+function clause execute (MFHI(rd)) =
+  {
+    wGPR(rd) := HI
+  }
+
+(* MFLO move from LO register *)
+union ast member regno MFLO
+function clause decode (0b000000 : 0b0000000000 : (regno) rd : 0b00000 : 0b010010) = 
+  MFLO(rd)
+function clause execute (MFLO(rd)) =
+  {
+    wGPR(rd) := LO
+  }
+
+(* MTHI move to HI register *)
+union ast member regno MTHI
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010001) = 
+  MTHI(rs)
+function clause execute (MTHI(rs)) =
+  {
+    HI := rGPR(rs)
+  }
+
+(* MTLO move to LO register *)
+union ast member regno MTLO
+function clause decode (0b000000 : (regno) rs : 0b000000000000000 : 0b010011) = 
+  MTLO(rs)
+function clause execute (MTLO(rs)) =
+  {
+    LO := rGPR(rs)
+  }
+
+(* MUL 32-bit multiply into GPR *)
+union ast member regregreg MUL
+function clause decode (0b011100 : (regno) rs : (regno) rt : (regno) rd : 0b00000 : 0b000010) =
+  MUL(rs, rt, rd)
+function clause execute (MUL(rs, rt, rd)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) result := (rsVal[31..0]) *_s (rtVal[31..0]);
+    wGPR(rd) := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        EXTS(result[31..0]);
+    (* HI and LO are always undefined after MUL *)
+    HI := undefined;
+    LO := undefined;
+  }
+
+(* MULT 32-bit multiply into HI/LO *)
+union ast member (regno, regno) MULT
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011000) =
+  MULT(rs, rt)
+function clause execute (MULT(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        (rsVal[31..0]) *_s (rtVal[31..0]);
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* MULTU 32-bit unsignedm rultiply into HI/LO *)
+union ast member (regno, regno) MULTU
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011001) =
+  MULTU(rs, rt)
+function clause execute (MULTU(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        (rsVal[31..0]) * (rtVal[31..0]);
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* DMULT 64-bit multiply into HI/LO *)
+union ast member (regno, regno) DMULT
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011100) =
+  DMULT(rs, rt)
+function clause execute (DMULT(rs, rt)) =
+  {
+    (bit[128]) result := (rGPR(rs)) *_s (rGPR(rt));
+    HI := (result[127..64]);
+    LO := (result[63..0]);
+  }
+
+(* DMULTU 64-bit unsigned multiply into HI/LO *)
+union ast member (regno, regno) DMULTU
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011101) =
+  DMULTU(rs, rt)
+function clause execute (DMULTU(rs, rt)) =
+  {
+    (bit[128]) result := (rGPR(rs)) * (rGPR(rt));
+    HI := (result[127..64]);
+    LO := (result[63..0]);
+  }
+
+(* MADD 32-bit signed multiply and add into HI/LO *)
+union ast member (regno, regno) MADD
+function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000000) =
+  MADD(rs, rt)
+function clause execute (MADD(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        ((rsVal[31..0]) *_s (rtVal[31..0]));
+    (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]);
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* MADDU 32-bit unsigned multiply and add into HI/LO *)
+union ast member (regno, regno) MADDU
+function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000001) =
+  MADDU(rs, rt)
+function clause execute (MADDU(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        ((rsVal[31..0]) * (rtVal[31..0]));
+    (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]);
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* MSUB 32-bit signed multiply and sub from HI/LO *)
+union ast member (regno, regno) MSUB
+function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000100) =
+  MSUB(rs, rt)
+function clause execute (MSUB(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        ((rsVal[31..0]) *_s (rtVal[31..0]));
+    (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result;
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* MSUBU 32-bit unsigned multiply and sub from HI/LO *)
+union ast member (regno, regno) MSUBU
+function clause decode (0b011100 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b000101) =
+  MSUBU(rs, rt)
+function clause execute (MSUBU(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        undefined
+      else
+        ((rsVal[31..0]) * (rtVal[31..0]));
+    (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result;
+    HI := EXTS(result[63..32]);
+    LO := EXTS(result[31..0]);
+  }
+
+(* DIV 32-bit divide into HI/LO *)
+union ast member (regno, regno) DIV
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011010) =
+  DIV(rs, rt)
+function clause execute (DIV(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    let ((bit[32]) q, (bit[32])r) = (if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        (undefined, undefined)
+      else
+        ((rsVal[31..0]) quot_s (rtVal[31..0]), (rsVal[31..0]) mod (rtVal[31..0])))
+    in
+    {
+      HI := EXTS(r);
+      LO := EXTS(q);
+    }
+  }
+
+(* DIVU 32-bit unsigned divide into HI/LO *)
+union ast member (regno, regno) DIVU
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011011) =
+  DIVU(rs, rt)
+function clause execute (DIVU(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    let ((bit[32]) q, (bit[32])r) = (if (NotWordVal(rsVal) | NotWordVal(rtVal)) then
+        (undefined, undefined)
+      else
+        ((rsVal[31..0]) quot (rtVal[31..0]), (rsVal[31..0]) mod (rtVal[31..0])))
+    in
+    {
+      HI := EXTS(r);
+      LO := EXTS(q);
+    }
+  }
+
+(* DDIV 64-bit divide into HI/LO *)
+union ast member (regno, regno) DDIV
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011110) =
+  DDIV(rs, rt)
+function clause execute (DDIV(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    LO    := rsVal quot_s rtVal;
+    HI    := rsVal mod rtVal; (* signed? *)
+  }
+
+(* DDIV 64-bit divide into HI/LO *)
+union ast member (regno, regno) DDIVU
+function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : 0b011111) =
+  DDIVU(rs, rt)
+function clause execute (DDIVU(rs, rt)) =
+  {
+    rsVal := rGPR(rs);
+    rtVal := rGPR(rt);
+    LO    := rsVal quot rtVal;
+    HI    := rsVal mod rtVal;
+  }
+
+(**************************************************************************************)
+(* Jump instructions -- unconditional branches                                        *)
+(**************************************************************************************)
+
+(* J    - jump, the simplest control flow instruction, with branch delay slot *)
+union ast member (bit[26]) J
+function clause decode (0b000010 : (bit[26]) offset) =
+  J(offset)
+function clause execute (J(offset)) = 
+  {
+    delayedPC     := PC[63..28] : offset : 0b00;
+    branchPending := 1
+  }
+
+(* JAL    - jump and link *)
+union ast member (bit[26]) JAL
+function clause decode (0b000011 : (bit[26]) offset) =
+  JAL(offset)
+function clause execute (JAL(offset)) = 
+  {
+    delayedPC     := PC[63..28] : offset : 0b00;
+    branchPending := 1;
+    wGPR(31)      := PC + 8;
+  }
+
+(* JR -- jump via register *)
+union ast member regno JR
+function clause decode (0b000000 : (regno) rs : 0b00000 : 0b00000 : (regno) hint : 0b001000) =
+  JR(rs) (* hint is ignored *)
+function clause execute (JR(rs)) =
+  {
+    delayedPC     := rGPR(rs);
+    branchPending := 1;
+  }
+
+(* JALR -- jump via register with link *)
+union ast member (regno, regno) JALR
+function clause decode (0b000000 : (regno) rs : 0b00000 : (regno) rd : (regno) hint : 0b001001) =
+  JALR(rs, rd) (* hint is ignored *)
+function clause execute (JALR(rs, rd)) =
+  {
+    delayedPC     := rGPR(rs);
+    branchPending := 1;
+    wGPR(rd)      := PC + 8;
+  }
+
+(**************************************************************************************)
+(* B[N]EQ[L]  - branch on (not) equal (likely)                                        *)
+(* Conditional branch instructions with two register operands                         *)
+(**************************************************************************************)
+
+union ast member (regno, regno, imm16, bool, bool) BEQ
+function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) =  BEQ(rs, rt, imm, false, false)  (* BEQ  *)
+function clause decode (0b000100 : (regno) rs : (regno) rt : (imm16) imm) =  BEQ(rs, rt, imm, false, true)   (* BEQL *)
+function clause decode (0b000101 : (regno) rs : (regno) rt : (imm16) imm) =  BEQ(rs, rt, imm, true , false)  (* BNE  *)
+function clause decode (0b010101 : (regno) rs : (regno) rt : (imm16) imm) =  BEQ(rs, rt, imm, true , true)   (* BNEL *)
+function clause execute (BEQ(rs, rd, imm, ne, likely)) =
+  {
+    if ((rGPR(rs) == rGPR(rd)) ^ ne) then
+      {
+        delayedPC     := PC + EXTS(imm : 0b00);
+        branchPending := 1;
+      }
+    else
+      {
+        if (likely) then
+          PC := PC + 4; (* skip branch delay *)
+      }
+  }
+
+(* 
+   
+   Branches comparing with zero (single register operand, possible link in r31)
+*)
+
+(**************************************************************************************)
+(* BGEZ[AL][L] - branch on comparison with zero (possibly  link, likely)              *)
+(* Conditional branch instructions with single register operand                       *)
+(**************************************************************************************)
+
+union ast member (regno, imm16, Comparison, bool, bool) BCMPZ
+function clause decode (0b000001 : (regno) rs : 0b00000 : (imm16) imm) = BCMPZ(rs, imm, LT, false, false) (* BLTZ *)
+function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = BCMPZ(rs, imm, LT, true, false)  (* BLTZAL *)
+function clause decode (0b000001 : (regno) rs : 0b00010 : (imm16) imm) = BCMPZ(rs, imm, LT, false, true)  (* BLTZL *)
+function clause decode (0b000001 : (regno) rs : 0b10010 : (imm16) imm) = BCMPZ(rs, imm, LT, true, true)   (* BLTZALL *)
+
+function clause decode (0b000001 : (regno) rs : 0b00001 : (imm16) imm) = BCMPZ(rs, imm, GE, false, false) (* BGEZ *)
+function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = BCMPZ(rs, imm, GE, true, false)  (* BGEZAL *)
+function clause decode (0b000001 : (regno) rs : 0b00011 : (imm16) imm) = BCMPZ(rs, imm, GE, false, true)  (* BGEZL *)
+function clause decode (0b000001 : (regno) rs : 0b10011 : (imm16) imm) = BCMPZ(rs, imm, GE, true, true)   (* BGEZALL *)
+
+function clause decode (0b000111 : (regno) rs : 0b00000 : (imm16) imm) = BCMPZ(rs, imm, GT, false, false) (* BGTZ *)
+function clause decode (0b010111 : (regno) rs : 0b00000 : (imm16) imm) = BCMPZ(rs, imm, GT, false, true)  (* BGTZL *)
+
+function clause decode (0b000110 : (regno) rs : 0b00000 : (imm16) imm) = BCMPZ(rs, imm, LE, false, false) (* BLEZ *)
+function clause decode (0b010110 : (regno) rs : 0b00000 : (imm16) imm) = BCMPZ(rs, imm, LE, false, true)  (* BLEZL *)
+
+function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
+  {
+    (bit[64]) linkVal := PC + 8;
+    regVal := rGPR(rs);
+    condition := compare(cmp, regVal, 0);
+    if (condition) then
+      {
+        delayedPC := PC + EXTS(imm : 0b00);
+        branchPending := 1;
+      }
+    else if (likely) then
+      {
+        PC := PC + 4  (* skip branch delay *)
+      };
+    if (link) then
+      wGPR(31) := linkVal
+  }
+
+(**************************************************************************************)
+(* SYSCALL/BREAK/WAIT/Trap                                                            *)
+(**************************************************************************************)
+
+union ast member unit SYSCALL
+function clause decode (0b000000 : (bit[20]) code : 0b001100) =
+  SYSCALL (* code is ignored *)
+function clause execute (SYSCALL) =
+  {
+    SignalException(Sys)
+  }
+
+(* BREAK is identical to SYSCALL exception for the exception raised *)
+union ast member unit BREAK
+function clause decode (0b000000 : (bit[20]) code : 0b001101) =
+  BREAK (* code is ignored *)
+function clause execute (BREAK) =
+  {
+    SignalException(Bp)
+  }
+
+(* Accept WAIT as a NOP *)
+union ast member unit WAIT
+function clause decode (0b010000 : 0x80000 : 0b100000) =
+  WAIT (* we only accept code == 0 *)
+function clause execute (WAIT) = ()
+
+(* Trap instructions with two register operands *)
+union ast member (regno, regno, Comparison) TRAPREG
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110000) = TRAPREG(rs, rt, GE) (* TGE *)
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110001) = TRAPREG(rs, rt, GEU) (* TGEU *)
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110010) = TRAPREG(rs, rt, LT) (* TLT *)
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110011) = TRAPREG(rs, rt, LTU) (* TLTU *)
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110100) = TRAPREG(rs, rt, EQ) (* TEQ *)
+function clause decode (0b000000 : (regno) rs : (regno) rt : (bit[10]) code : 0b110110) = TRAPREG(rs, rt, NE) (* TNE *)
+function clause execute (TRAPREG(rs, rt, cmp)) =
+  {
+    rs_val := rGPR(rs);
+    rt_val := rGPR(rt);
+    condition := compare(cmp, rs_val, rt_val);
+    if (condition) then
+      SignalException(Tr)
+  }
+
+
+(* Trap instructions with one register and one immediate operand *)
+union ast member (regno, imm16, Comparison) TRAPIMM
+function clause decode (0b000001 : (regno) rs : 0b01100 : (imm16) imm) = TRAPIMM(rs, imm, EQ) (* TEQI *)
+function clause decode (0b000001 : (regno) rs : 0b01110 : (imm16) imm) = TRAPIMM(rs, imm, NE) (* TNEI *)
+function clause decode (0b000001 : (regno) rs : 0b10000 : (imm16) imm) = TRAPIMM(rs, imm, GE) (* TGEI *)
+function clause decode (0b000001 : (regno) rs : 0b10001 : (imm16) imm) = TRAPIMM(rs, imm, GEU) (* TGEIU *)
+function clause decode (0b000001 : (regno) rs : 0b01010 : (imm16) imm) = TRAPIMM(rs, imm, LT)  (* TLTI *)
+function clause decode (0b000001 : (regno) rs : 0b01011 : (imm16) imm) = TRAPIMM(rs, imm, LTU)  (* TLTIU *)
+function clause execute (TRAPIMM(rs, imm, cmp)) =
+  {
+    rs_val := rGPR(rs);
+    imm_val := EXTS(imm);
+    condition := compare(cmp, rs_val, imm_val);
+    if (condition) then
+      SignalException(Tr)
+  }
+
+(**************************************************************************************)
+(* Load instructions -- various width/signs                                           *)
+(**************************************************************************************)
+
+union ast member (WordType, bool, bool, regno, regno, imm16) Load
+function clause decode (0b100000 : (regno) base : (regno) rt : (imm16) offset) = Load(B, true,  false, base, rt, offset) (* LB *)
+function clause decode (0b100100 : (regno) base : (regno) rt : (imm16) offset) = Load(B, false, false, base, rt, offset) (* LBU *)
+function clause decode (0b100001 : (regno) base : (regno) rt : (imm16) offset) = Load(H, true,  false, base, rt, offset) (* LH *)
+function clause decode (0b100101 : (regno) base : (regno) rt : (imm16) offset) = Load(H, false, false, base, rt, offset) (* LHU *)
+function clause decode (0b100011 : (regno) base : (regno) rt : (imm16) offset) = Load(W, true,  false, base, rt, offset) (* LW *)
+function clause decode (0b100111 : (regno) base : (regno) rt : (imm16) offset) = Load(W, false, false, base, rt, offset) (* LWU *)
+function clause decode (0b110111 : (regno) base : (regno) rt : (imm16) offset) = Load(D, false, false, base, rt, offset) (* LD *)
+function clause decode (0b110000 : (regno) base : (regno) rt : (imm16) offset) = Load(W, false, true, base, rt, offset)  (* LL *)
+function clause decode (0b110100 : (regno) base : (regno) rt : (imm16) offset) = Load(D, false, true, base, rt, offset)  (* LLD *)
+function clause execute (Load(width, signed, linked, base, rt, offset)) =
+  {
+    (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+    if (vAddr[logWordWidth(width) .. 0] != 0) then
+      SignalException(AdEL) (* unaligned access *)
+    else
+      let (ex, pAddr) = (TranslateAddress(vAddr, LoadData)) in
+      {
+        if ~ (ex) then
+          {
+            memResult := if (linked) then
+                MEMr_reserve(pAddr, wordWidthBytes(width))
+              else
+                MEMr(pAddr, wordWidthBytes(width));
+            if (signed) then
+              wGPR(rt) := EXTS(memResult)
+            else
+              wGPR(rt) := EXTZ(memResult)
+          }
+      }
+  }
+
+(**************************************************************************************)
+(* Store instructions -- various widths                                               *)
+(**************************************************************************************)
+
+union ast member (WordType, bool, regno, regno, imm16) Store
+function clause decode (0b101000 : (regno) base : (regno) rt : (imm16) offset) = Store(B, false, base, rt, offset) (* SB *)
+function clause decode (0b101001 : (regno) base : (regno) rt : (imm16) offset) = Store(H, false, base, rt, offset) (* SH *)
+function clause decode (0b101011 : (regno) base : (regno) rt : (imm16) offset) = Store(W, false, base, rt, offset) (* SW *)
+function clause decode (0b111111 : (regno) base : (regno) rt : (imm16) offset) = Store(D, false, base, rt, offset) (* SD *)
+function clause decode (0b111000 : (regno) base : (regno) rt : (imm16) offset) = Store(W, true, base, rt, offset)  (* SC *)
+function clause decode (0b111100 : (regno) base : (regno) rt : (imm16) offset) = Store(D, true, base, rt, offset)  (* SCD *)
+function clause execute (Store(width, conditional, base, rt, offset)) =
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        if (vAddr[logWordWidth(width)..0] != 0) then
+          SignalException(AdES) (* unaligned access *)
+        else
+          let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+          {
+            if ~ (ex) then
+              {
+                if (conditional) then
+                  {
+                    success  := (MEMw_conditional(vAddr, wordWidthBytes(width), rGPR(rt)));
+                    wGPR(rt) := EXTZ([success])
+                  }
+                else
+                  MEMw(vAddr, wordWidthBytes(width)) := rGPR(rt)
+              }
+          }
+      }
+
+(* LWL   - Load word left (big-endian only) *)
+
+union ast member regregimm16 LWL
+function clause decode(0b100010 : (regno) base : (regno) rt : (imm16) offset) =
+      LWL(base, rt, offset)
+function clause execute(LWL(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, LoadData)) in
+        if ~ (ex) then
+          {
+            mem_val   := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *)
+            reg_val   := rGPR(rt);
+            wGPR(rt)  := EXTS(switch(vAddr[1..0])
+              {
+                case 0b00 -> mem_val
+                case 0b01 -> mem_val[23..0] : reg_val[07..0]
+                case 0b10 -> mem_val[15..0] : reg_val[15..0]
+                case 0b11 -> mem_val[07..0] : reg_val[23..0]
+              });
+          }
+      }
+union ast member regregimm16 LWR
+function clause decode(0b100110 : (regno) base : (regno) rt : (imm16) offset) =
+      LWR(base, rt, offset)
+function clause execute(LWR(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, LoadData)) in
+        if ~ (ex) then
+          {
+            mem_val   := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *)
+            reg_val   := rGPR(rt);
+            wGPR(rt)  := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
+              {
+                case 0b00 -> reg_val[31..8]  : mem_val[7..0]
+                case 0b01 -> reg_val[31..16] : mem_val[15..0]
+                case 0b10 -> reg_val[31..24] : mem_val[23..0]
+                case 0b11 -> mem_val
+              });
+          }
+      }
+
+(* SWL   - Store word left *)
+union ast member regregimm16 SWL
+function clause decode(0b101010 : (regno) base : (regno) rt : (imm16) offset) =
+      SWL(base, rt, offset)
+function clause execute(SWL(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+        if ~ (ex) then
+          {
+            reg_val   := rGPR(rt);
+            switch (vAddr[1..0])
+            {
+              case 0b00 -> (MEMw(pAddr, 4) := reg_val[31..0])
+              case 0b01 -> (MEMw(pAddr, 3) := reg_val[31..8])
+              case 0b10 -> (MEMw(pAddr, 2) := reg_val[31..16])
+              case 0b11 -> (MEMw(pAddr, 1) := reg_val[31..24])
+            }
+          }
+      }
+
+union ast member regregimm16 SWR
+function clause decode(0b101110 : (regno) base : (regno) rt : (imm16) offset) =
+      SWR(base, rt, offset)
+function clause execute(SWR(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+        if ~ (ex) then
+          {
+            wordAddr := pAddr[63..2] : 0b00;
+            reg_val   := rGPR(rt);
+            switch (vAddr[1..0])
+              {
+                case 0b00 -> (MEMw(wordAddr, 1) := reg_val[7..0])
+                case 0b01 -> (MEMw(wordAddr, 2) := reg_val[15..0])
+                case 0b10 -> (MEMw(wordAddr, 3) := reg_val[23..0])
+                case 0b11 -> (MEMw(wordAddr, 4) := reg_val[31..0])
+              }
+          }
+      }
+
+(* Load double-word left *)
+union ast member regregimm16 LDL
+function clause decode(0b011010 : (regno) base : (regno) rt : (imm16) offset) =
+  LDL(base, rt, offset)
+function clause execute(LDL(base, rt, offset)) = 
+  {
+    (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+    let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+    if ~ (ex) then
+      {
+        mem_val   := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *)
+        reg_val   := rGPR(rt);
+        wGPR(rt)  := switch(vAddr[2..0])
+              {
+                case 0b000 -> mem_val
+                case 0b001 -> mem_val[55..0] : reg_val[7..0]
+                case 0b010 -> mem_val[47..0] : reg_val[15..0]
+                case 0b011 -> mem_val[39..0] : reg_val[23..0]
+                case 0b100 -> mem_val[31..0] : reg_val[31..0]
+                case 0b101 -> mem_val[23..0] : reg_val[39..0]
+                case 0b110 -> mem_val[15..0] : reg_val[47..0]
+                case 0b111 -> mem_val[07..0] : reg_val[55..0]
+              };
+      }
+  }
+
+(* Load double-word right *)
+union ast member regregimm16 LDR
+function clause decode(0b011011 : (regno) base : (regno) rt : (imm16) offset) =
+  LDR(base, rt, offset)
+function clause execute(LDR(base, rt, offset)) = 
+  {
+    (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+    let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+    if ~ (ex) then
+      {
+        mem_val   := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *)
+        reg_val   := rGPR(rt);
+        wGPR(rt)  := switch(vAddr[2..0])
+              {
+                case 0b000 -> reg_val[55..0] : mem_val[07..0]
+                case 0b001 -> reg_val[47..0] : mem_val[15..0]
+                case 0b010 -> reg_val[39..0] : mem_val[23..0]
+                case 0b011 -> reg_val[31..0] : mem_val[31..0]
+                case 0b100 -> reg_val[23..0] : mem_val[39..0]
+                case 0b101 -> reg_val[15..0] : mem_val[47..0]
+                case 0b110 -> reg_val[07..0] : mem_val[55..0]
+                case 0b111 -> mem_val
+              };
+      }
+  }
+
+(* SDL   - Store double-word left *)
+union ast member regregimm16 SDL
+function clause decode(0b101100 : (regno) base : (regno) rt : (imm16) offset) =
+      SDL(base, rt, offset)
+function clause execute(SDL(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+        if ~ (ex) then
+          {
+            reg_val := rGPR(rt);
+            switch (vAddr[2..0])
+            {
+              case 0b000 -> (MEMw(pAddr, 8) := reg_val[63..00])
+              case 0b001 -> (MEMw(pAddr, 7) := reg_val[63..08])
+              case 0b010 -> (MEMw(pAddr, 6) := reg_val[63..16])
+              case 0b011 -> (MEMw(pAddr, 5) := reg_val[63..24])
+              case 0b100 -> (MEMw(pAddr, 4) := reg_val[63..32])
+              case 0b101 -> (MEMw(pAddr, 3) := reg_val[63..40])
+              case 0b110 -> (MEMw(pAddr, 2) := reg_val[63..48])
+              case 0b111 -> (MEMw(pAddr, 1) := reg_val[63..56])
+            }
+          }
+      }
+
+
+(* SDR   - Store double-word right *)
+union ast member regregimm16 SDR
+function clause decode(0b101101 : (regno) base : (regno) rt : (imm16) offset) =
+      SDR(base, rt, offset)
+function clause execute(SDR(base, rt, offset)) = 
+      {
+        (bit[64]) vAddr := EXTS(offset) + rGPR(base);
+        let (ex, pAddr) = (TranslateAddress(vAddr, StoreData)) in
+        if ~ (ex) then
+          {
+            reg_val := rGPR(rt);
+            wordAddr := pAddr[63..3] : 0b000;
+            switch (vAddr[2..0])
+            {
+              case 0b000 -> (MEMw(wordAddr, 1) := reg_val[07..0])
+              case 0b001 -> (MEMw(wordAddr, 2) := reg_val[15..0])
+              case 0b010 -> (MEMw(wordAddr, 3) := reg_val[23..0])
+              case 0b011 -> (MEMw(wordAddr, 4) := reg_val[31..0])
+              case 0b100 -> (MEMw(wordAddr, 5) := reg_val[39..0])
+              case 0b101 -> (MEMw(wordAddr, 6) := reg_val[47..0])
+              case 0b110 -> (MEMw(wordAddr, 7) := reg_val[55..0])
+              case 0b111 -> (MEMw(wordAddr, 8) := reg_val[63..0])
+            }
+          }
+      }
+
+(* CACHE - manipulate (non-existent) caches *)
+
+union ast member regregimm16 CACHE
+function clause decode (0b101111 : (regno) base : (regno) op : (imm16) imm) =
+  CACHE(base, op, imm)
+function clause execute (CACHE(base, op, imm)) =
+  () (* XXX NOP *)
+
+(* PREF - prefetching into (non-existent) caches *)
+
+union ast member regregimm16 PREF
+function clause decode (0b110011 : (regno) base : (regno) op : (imm16) imm) =
+  PREF(base, op, imm)
+function clause execute (PREF(base, op, imm)) =
+  () (* XXX NOP *)
+
+
+(* SYNC  - Memory barrier *)
+union ast member unit SYNC
+function clause decode (0b000000 : 0b00000 : 0b00000 : 0b00000 : (regno) stype : 0b001111) = 
+  SYNC() (* stype is currently ignored *)
+function clause execute(SYNC) =
+  MEM_sync()
+
+function clause decode _ = exit no_matching_pattern
+
+end decode
+end execute
+end ast
+
+(* fetch decode execute *)
+function unit fde() =
+{
+  let (ex, pAddr) = (TranslateAddress (PC, Instruction)) in
+  if (~ (ex)) then
+    {
+      opcode := MEMr(pAddr, 4);
+      instr  := decode(opcode);
+      execute(instr);
+    };
+  (* Compute the next PC to execute *)
+  if exceptionSignalled then
+    {
+      (* new PC computed in SignalException based on exception type *)
+      inBranchDelay := 1;
+      branchPending := 1;
+      exceptionSignalled := 1;
+    }
+  else if inBranchDelay then
+    {
+      PC := delayedPC;
+      inBranchDelay := 1;
+      branchPending := 1;
+    }
+  else 
+    {
+      PC := PC + 4;
+      if branchPending then
+          inBranchDelay := 1
+    };
+}
diff --git a/src/Makefile b/src/Makefile
index 4016a07b..3888d0c6 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -46,6 +46,8 @@ get_elf:
 	rm -rf src_elf/gnu_extensions/*.ml*
 	$(MAKE) -C $(ELFDIR)/src clean
 	$(MAKE) -C $(ELFDIR)/src lem-all-ocaml
+	mkdir -p src_elf/{abis,adaptors,gnu_extensions}
+	mkdir -p src_elf/abis/{aarch64,amd64,power64,x86}
 	cp -a $(ELFDIR)/src/*.ml src_elf
 	cp -a $(ELFDIR)/src/abis/*.ml src_elf/abis
 	cp -a $(ELFDIR)/src/abis/amd64/*.ml src_elf/abis/amd64