implement RV64I based on version 2.0 user spec.

1 files changed, 235 insertions, 1938 deletions

diff --git a/risc-v/risc-v.sail b/risc-v/risc-v.sail
index 92e8da51..edf95c62 100644
--- a/risc-v/risc-v.sail
+++ b/risc-v/risc-v.sail
@@ -1,1966 +1,263 @@
 default Order dec
 
-register (bit[64]) x0
-register (bit[64]) x1
-register (bit[64]) x2
-register (bit[64]) x3
-register (bit[64]) x4
-register (bit[64]) x5
-register (bit[64]) x6
-register (bit[64]) x7
-register (bit[64]) x8
-register (bit[64]) x9
-register (bit[64]) x10
-register (bit[64]) x11
-register (bit[64]) x12
-register (bit[64]) x13
-register (bit[64]) x14
-register (bit[64]) x15
-register (bit[64]) x16
-register (bit[64]) x17
-register (bit[64]) x18
-register (bit[64]) x19
-register (bit[64]) x20
-register (bit[64]) x21
-register (bit[64]) x22
-register (bit[64]) x23
-register (bit[64]) x24
-register (bit[64]) x25
-register (bit[64]) x26
-register (bit[64]) x27
-register (bit[64]) x28
-register (bit[64]) x29
-register (bit[64]) x30
-register (bit[64]) x31
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) x =
+typedef regval = bit[64]
+typedef regno = bit[5]
+
+register (regval) x0
+register (regval) x1
+register (regval) x2
+register (regval) x3
+register (regval) x4
+register (regval) x5
+register (regval) x6
+register (regval) x7
+register (regval) x8
+register (regval) x9
+register (regval) x10
+register (regval) x11
+register (regval) x12
+register (regval) x13
+register (regval) x14
+register (regval) x15
+register (regval) x16
+register (regval) x17
+register (regval) x18
+register (regval) x19
+register (regval) x20
+register (regval) x21
+register (regval) x22
+register (regval) x23
+register (regval) x24
+register (regval) x25
+register (regval) x26
+register (regval) x27
+register (regval) x28
+register (regval) x29
+register (regval) x30
+register (regval) x31
+
+register (bit[64]) PC
+register (bit[64]) nextPC
+
+let (vector <0, 32, inc, (register<(regval)>)>) GPRs =
   [x0, x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31]
 
-typedef arithr = enumerate { ADD; SLL; SLT; SLTU; XOR; SRL; OR; AND }
-
-
-scattered function unit execute
-scattered typedef ast = const union
-
-val bit[32] -> ast effect pure decode
-
-scattered function ast decode
-
-union ast member (bit[5], bit[5], arithr, bit[5]) Arithr1
-
-function clause decode (0b0000000 :
-(bit[5]) src2 :
-(bit[5]) src1 :
-(bit[3]) arithr_op :
-(bit[5]) dest :
-0b0110011 ) =
-Arithr1(src2,src1, (([|7|]) arithr_op), dest)
-  
-
-function clause execute (Arithr1(src2,src1, arithr_op, dest)) =
-  {
-   switch arithr_op {
-     case ADD -> x[dest] := x[src1] + x[src2]
-(*     case SLL ->
-     case SLT ->
-     case SLTU ->
-     case XOR ->
-     case SRL ->
-     case OR ->
-     case AND -> *)
-   }
-}
-
-end ast
-end decode
-end execute 
-
-(*val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS
-
-(* XXX binary coded decimal *)
-function forall Type 'a . 'a DEC_TO_BCD ( x ) = x
-function forall Type 'a . 'a BCD_TO_DEC ( x ) = x
-(* XXX carry out *)
-function forall Nat 'a . bit carry_out ( (bit['a]) _,carry ) = carry
-(* XXX Storage control *)
-function forall Type 'a . 'a real_addr ( x ) = x
-(* XXX For stvxl and lvxl - what does that do? *)
-function forall Type 'a . unit mark_as_not_likely_to_be_needed_again_anytime_soon ( x ) = ()
-
-(* XXX *)
-val extern forall Nat 'k, Nat 'r,
-  0 <= 'k, 'k <= 64, 'r + 'k = 64.
-  (bit[64], [|'k|]) -> [|0:'r|] effect pure countLeadingZeroes
-
-function forall Nat 'n, Nat 'm .
-  bit['m] EXTS_EXPLICIT((bit['n]) v, ([|'m|]) m) =
-  (v[0] ^^ (m - length(v))) : v
-
-val forall Nat 'n, Nat 'm, 0 <= 'n, 'n <= 'm, 'm <= 63 .
-  ([|'n|],[|'m|]) -> bit[64]
-  effect pure
-  MASK
-
-function (bit[64]) MASK(start, stop) = {
-  (bit[64]) mask_temp := 0;
-  if(start > stop) then {
-    mask_temp[start .. 63] := bitone ^^ (64 - start);
-    mask_temp[0 .. stop] := bitone ^^ (stop + 1);
-  } else {
-    mask_temp[start .. stop ] := bitone ^^ (stop - start + 1);
-  };
-  mask_temp;
-}
-
-val forall Nat 'n, 0 <= 'n, 'n <= 63 .
-  (bit[64], [|'n|]) -> bit[64] effect pure ROTL
-
-function (bit[64]) ROTL(v, n) = v[n .. 63] : v[0 .. (n-1)]
-
-(* Branch facility registers *)
-
-typedef cr = register bits [ 32 : 63 ] {
-  32 .. 35 : CR0;
-    32 : LT; 33 : GT; 34 : EQ; 35 : SO;
-  36 .. 39 : CR1;
-    36 : FX; 37 : FEX; 38 : VX; 39 : OX;
-  40 .. 43 : CR2;
-  44 .. 47 : CR3;
-  48 .. 51 : CR4;
-  52 .. 55 : CR5;
-  56 .. 59 : CR6;
-    (* name clashing - do we need hierarchical naming for fields, or do
-    we just don't care? LT, GT, etc. are not used in the code anyway.
-    56 : LT; 57 : GT; 58 : EQ; 59 : SO;
-    *)
-  60 .. 63 : CR7;
-}
-register (cr) CR
-
-register (bit[64]) CTR
-register (bit[64]) LR
-
-typedef xer = register bits [ 0 : 63 ] {
-  32 : SO;
-  33 : OV;
-  34 : CA;
-}
-register (xer) XER
-
-register alias CA = XER.CA
-
-(* Fixed-point registers *)
-
-register (bit[64]) GPR0
-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
-
-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
-  ]
-
-register (bit[32:63]) VRSAVE
-
-register (bit[64]) SPRG4
-register (bit[64]) SPRG5
-register (bit[64]) SPRG6
-register (bit[64]) SPRG7
-
-(* XXX bogus, length should be 1024 with many more values - cf. mfspr
-  definition - eg. SPRG4 to SPRG7 are at offsets 260 to 263, VRSAVE is 256,
-  etc. *)
-let (vector <0, 10, inc, (register<(bit[64])>) >) SPR =
-  [ undefined, XER, undefined, undefined,
-    undefined, undefined, undefined, undefined,
-    LR, CTR
-  ]
-
-(* XXX DCR is implementation-dependent; also, some DCR are only 32 bits
- instead of 64, and mtdcrux/mfdcrux do special tricks in that case, not
- shown in pseudo-code. We just define two dummy DCR here, using sparse
- vector definition. *)
-register (vector <0, 64, inc, bit>) DCR0
-register (vector <0, 64, inc, bit>) DCR1
-let (vector <0, 2** 64, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR =
-  [ 0=DCR0, 1=DCR1 ]
-
-(* Floating-point registers *)
-
-register (bit[64]) FPR0
-register (bit[64]) FPR1
-register (bit[64]) FPR2
-register (bit[64]) FPR3
-register (bit[64]) FPR4
-register (bit[64]) FPR5
-register (bit[64]) FPR6
-register (bit[64]) FPR7
-register (bit[64]) FPR8
-register (bit[64]) FPR9
-register (bit[64]) FPR10
-register (bit[64]) FPR11
-register (bit[64]) FPR12
-register (bit[64]) FPR13
-register (bit[64]) FPR14
-register (bit[64]) FPR15
-register (bit[64]) FPR16
-register (bit[64]) FPR17
-register (bit[64]) FPR18
-register (bit[64]) FPR19
-register (bit[64]) FPR20
-register (bit[64]) FPR21
-register (bit[64]) FPR22
-register (bit[64]) FPR23
-register (bit[64]) FPR24
-register (bit[64]) FPR25
-register (bit[64]) FPR26
-register (bit[64]) FPR27
-register (bit[64]) FPR28
-register (bit[64]) FPR29
-register (bit[64]) FPR30
-register (bit[64]) FPR31
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) FPR =
-  [ FPR0, FPR1, FPR2, FPR3, FPR4, FPR5, FPR6, FPR7, FPR8, FPR9, FPR10,
-  FPR11, FPR12, FPR13, FPR14, FPR15, FPR16, FPR17, FPR18, FPR19, FPR20,
-  FPR21, FPR22, FPR23, FPR24, FPR25, FPR26, FPR27, FPR28, FPR29, FPR30, FPR31
-  ]
-
-typedef fpscr = register bits [ 0 : 63 ] {
-  32 : FX;
-  33 : FEX;
-  34 : VX;
-  35 : OX;
-  36 : UX;
-  37 : ZX;
-  38 : XX;
-  39 : VXSNAN;
-  40 : VXISI;
-  41 : VXIDI;
-  42 : VXZDZ;
-  43 : VXIMZ;
-  44 : VXVC;
-  45 : FR;
-  46 : FI;
-  47 .. 51 : FPRF;
-  47 : C;
-  48 .. 51 : FPCC;
-    48 : FL; 49 : FG; 50 : FE; 51 : FU;
-  53 : VXSOFT;
-  54 : VXSQRT;
-  55 : VXCVI;
-  56 : VE;
-  57 : OE;
-  58 : UE;
-  59 : ZE;
-  60 : XE;
-  61 : NI;
-  62 .. 63 : RN;
-}
-register (fpscr) FPSCR
+function (regval) rGPR ((regno) r) = 
+    if (r == 0) then 
+        0
+    else 
+        GPRs[r]
 
-(* Pair-wise access to FPR registers *)
+function unit wGPR((regno) r, (regval) v) =
+    if (r != 0) then
+        GPRs[r] := v
 
-register alias FPRp0 = FPR0 : FPR1
-register alias FPRp2 = FPR2 : FPR3
-register alias FPRp4 = FPR4 : FPR5
-register alias FPRp6 = FPR6 : FPR7
-register alias FPRp8 = FPR8 : FPR9
-register alias FPRp10 = FPR10 : FPR11
-register alias FPRp12 = FPR12 : FPR13
-register alias FPRp14 = FPR14 : FPR15
-register alias FPRp16 = FPR16 : FPR17
-register alias FPRp18 = FPR18 : FPR19
-register alias FPRp20 = FPR20 : FPR21
-register alias FPRp22 = FPR22 : FPR23
-register alias FPRp24 = FPR24 : FPR25
-register alias FPRp26 = FPR26 : FPR27
-register alias FPRp28 = FPR28 : FPR29
-register alias FPRp30 = FPR30 : FPR31
-
-let (vector <0, 32, inc, (register<(bit[128])>)>) FPRp =
-  [ 0 = FPRp0, 2 = FPRp2, 4 = FPRp4, 6 = FPRp6, 8 = FPRp8, 10 = FPRp10,
-  12 = FPRp12, 14 = FPRp14, 16 = FPRp16, 18 = FPRp18, 20 = FPRp20, 22 =
-  FPRp22, 24 = FPRp24, 26 = FPRp26, 28 = FPRp28, 30 = FPRp30 ]
-
-
-(* XXX *)
-val bit[32] -> bit[64] effect pure DOUBLE
-val bit[64] -> bit[32] effect { undef } SINGLE
-
-function  bit[64] DOUBLE word = {
-  (bit[64]) temp := 0;
-  if word[1..8] > 0 & word[1..8] < 255
-  then {
-    temp[0..1] := word[0..1];
-    temp[2] := ~(word[1]);
-    temp[3] := ~(word[1]);
-    temp[4] := ~(word[1]);
-    temp[5..63] := word[2..31] : 0b00000000000000000000000000000;
-  } else if word[1..8] == 0 & word[9..31] != 0 
-  then {
-    sign := word[0];
-    exp := 0-126;
-    (bit[53]) frac := 0b0 : word[9..31] : 0b00000000000000000000000000000;
-    foreach (i from 0 to 52) {
-      if frac[0] == 0 
-      then { frac[0..52] := frac[1..52] : 0b0;
-             exp := exp -1; }
-      else ()
-     };
-     temp[0] := sign;
-     temp[1..11] := (bit[10]) exp + 1023;
-     temp[12..63] := frac[1..52];
-   } else {
-     temp[0..1] := word[0..1];
-     temp[2] := word[1];
-     temp[3] := word[1];
-     temp[4] := word[1];
-     temp[5..63] := word[2..31] : 0b00000000000000000000000000000;
-   };
-   temp
-}
-
-function bit[32] SINGLE ((bit[64]) frs) = {
-  (bit[32]) word := 0;
-  if (frs[1..11] > 896) | (frs[1..63] == 0) 
-  then { word[0..1] := frs[0..1];
-         word[2..31] := frs[5..34]; }
-  else if (874 <= frs[1..11]) & (frs[1..11] <= 896)
-  then { 
-   sign := frs[0];
-   (bit[10]) exp := frs[1..11] - 1023;
-   (bit[53]) frac := 0b1 : frs[12..63];
-   foreach (i from 0 to 53) {
-     if exp < (0-126) 
-     then { frac[0..52] := 0b0 : frac[0..51];
-            exp := exp + 1; }
-     else ()};
-   } else word := undefined;
-   word   
-}
-
-(* Vector registers *)
-
-register (bit[128]) VR0
-register (bit[128]) VR1
-register (bit[128]) VR2
-register (bit[128]) VR3
-register (bit[128]) VR4
-register (bit[128]) VR5
-register (bit[128]) VR6
-register (bit[128]) VR7
-register (bit[128]) VR8
-register (bit[128]) VR9
-register (bit[128]) VR10
-register (bit[128]) VR11
-register (bit[128]) VR12
-register (bit[128]) VR13
-register (bit[128]) VR14
-register (bit[128]) VR15
-register (bit[128]) VR16
-register (bit[128]) VR17
-register (bit[128]) VR18
-register (bit[128]) VR19
-register (bit[128]) VR20
-register (bit[128]) VR21
-register (bit[128]) VR22
-register (bit[128]) VR23
-register (bit[128]) VR24
-register (bit[128]) VR25
-register (bit[128]) VR26
-register (bit[128]) VR27
-register (bit[128]) VR28
-register (bit[128]) VR29
-register (bit[128]) VR30
-register (bit[128]) VR31
-
-let (vector <0, 32, inc, (register<(bit[128])>) >) VR =
-  [ VR0, VR1, VR2, VR3, VR4, VR5, VR6, VR7, VR8, VR9, VR10,
-  VR11, VR12, VR13, VR14, VR15, VR16, VR17, VR18, VR19, VR20,
-  VR21, VR22, VR23, VR24, VR25, VR26, VR27, VR28, VR29, VR30, VR31
-  ]
-
-typedef vscr = register bits [ 96 : 127 ] {
-  111 : NJ;
-  127 : SAT;
-}
-register (vscr) VSCR
-
-(* XXX extend with zeroes -- the resulting size in completely unknown and depends of context *)
-val extern forall Nat 'n, Nat 'm. bit['n] -> bit['m] effect pure EXTZ
-
-(* Chop has a very weird definition where the resulting size depends of
-   context, but in practice it is used with the following definition everywhere,
-   except in vaddcuw which probably needs to be patched accordingly. *)
-val forall Nat 'n, Nat 'm, 'm <= 'n. (bit['n], [|'m|]) -> bit['m] effect pure Chop
-function forall Nat 'm. (bit['m]) Chop(x, y) = x[0..y]
-
-val forall Nat 'n, Nat 'm, Nat 'k, 'n <= 0, 0 <= 'm.
-  (implicit<'k>, int, [|'n|], [|'m|]) -> bit['k] effect { wreg } Clamp
-
-function forall Nat 'n, Nat 'm, Nat 'k, 'n <= 0, 0 <= 'm. (bit['k])
-Clamp((int) x, ([|'n|]) y, ([|'m|]) z) = {
-  ([|'n:'m|]) result := 0;
-  if (x<y) then {
-    result := y;
-    VSCR.SAT := 1;
-  } else if (x > z) then {
-    result := z;
-    VSCR.SAT := 1;
-  } else {
-    result := x;
-  };
-  (bit['k]) result;
-}
-
-(* XXX *)
-val extern bit[32] -> bit[32] effect pure RoundToSPIntCeil
-val extern bit[32] -> bit[32] effect pure RoundToSPIntFloor
-val extern bit[32] -> bit[32] effect pure RoundToSPIntNear
-val extern bit[32] -> bit[32] effect pure RoundToSPIntTrunc
-val extern bit[32] -> bit[32] effect pure RoundToNearSP
-val extern bit[32] -> bit[32] effect pure ReciprocalEstimateSP
-val extern bit[32] -> bit[32] effect pure ReciprocalSquareRootEstimateSP
-val extern bit[32] -> bit[32] effect pure LogBase2EstimateSP
-val extern bit[32] -> bit[32] effect pure Power2EstimateSP
-val extern (bit[32], bit[5]) -> bit[32] effect pure ConvertSPtoSXWsaturate
-val extern (bit[32], bit[5]) -> bit[32] effect pure ConvertSPtoUXWsaturate
-
-
-register (bit[64]) NIA (* next instruction address *)
-register (bit[64]) CIA (* current instruction address *)
-
-
-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 forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
 
-val extern unit -> unit effect { barr } I_Sync
-val extern unit -> unit effect { barr } H_Sync (*corresponds to Sync in barrier kinds*)
-val extern unit -> unit effect { barr } LW_Sync
-val extern unit -> unit effect { barr } EIEIO_Sync
+(* Ideally these would be sail builtin *)
+function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
+    let (bit[128]) v128 = EXTS(v) in
+    (v128 >> shift)[63..0]
 
-val forall Nat 'n, Nat 'm, 'n *8 = 'm. (implicit<'m>,(bit['m])) -> (bit['m]) effect pure byte_reverse
-function forall Nat 'n, Nat 'm, 'n*8 = 'm. (bit['m]) effect pure byte_reverse((bit['m]) input) = {
-  (bit['m]) output := 0;
-  j := length(input);
-  foreach (i from 0 to (length(input)) by 8) {
-   output[i..i+7] := input[j-7 ..j];
-   j := j-8; };
-  output
-}  
+function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) =
+    let (bit[64]) v64 = EXTS(v) in
+    (v64 >> shift)[31..0]
 
-(* XXX effect for trap? *)
-val extern unit -> unit effect pure trap
-
-register (bit[1]) mode64bit
-register (bit[1]) bigendianmode
-
-val (bit[64],bit) -> unit effect {rreg,wreg} set_overflow_cr0 
-function (unit) set_overflow_cr0(target_register,new_xer_so) = {
-  (if mode64bit
-   then m := 0
-   else m := 32);
-  (bit[64]) zero := 0;
-  (if target_register[m..63] <_s zero[m..63]
-  then c := 0b100
-  else if target_register[m..63] >_s zero[m..63] 
-  then c := 0b010
-  else c := 0b001);
-  CR.CR0 := c:[new_xer_so]
-}
-
-function (unit) set_SO_OV(overflow) =  {
-  XER.OV := overflow;
-  XER.SO := (XER.SO | overflow);
-}
+typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
+typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
+typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
+typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
+typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
+typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
 
 scattered function unit execute
 scattered typedef ast = const union
 
-val bit[32] -> ast effect pure decode
-
-scattered function ast decode
-
-union ast member (bit[24], bit, bit) B
-
-function clause decode (0b010010 :
-(bit[24]) LI :
-[AA] :
-[LK] as instr) =
-  B (LI,AA,LK)
-
-function clause execute (B (LI, AA, LK)) =
-  {
-    if AA then NIA := EXTS (LI : 0b00) else NIA := CIA + EXTS (LI : 0b00);
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[14], bit, bit) Bc
-
-function clause decode (0b010000 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[14]) BD :
-[AA] :
-[LK] as instr) =
-  Bc (BO,BI,BD,AA,LK)
-
-function clause execute (Bc (BO, BI, BD, AA, LK)) =
-  {
-    if mode64bit then M := 0 else M := 32;
-    ctr_temp := CTR;
-    if ~ (BO[2])
-    then {
-      ctr_temp := ctr_temp - 1;
-      CTR := ctr_temp
-    }
-    else ();
-    ctr_ok := (BO[2] | ~ (ctr_temp[M .. 63] == 0) ^ BO[3]);
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~ (BO[1]));
-    if ctr_ok & cond_ok
-    then if AA then NIA := EXTS (BD : 0b00) else NIA := CIA + EXTS (BD : 0b00)
-    else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[2], bit) Bclr
-
-function clause decode (0b010011 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[3]) _ :
-(bit[2]) BH :
-0b0000010000 :
-[LK] as instr) =
-  Bclr (BO,BI,BH,LK)
-
-function clause execute (Bclr (BO, BI, BH, LK)) =
-  {
-    if mode64bit then M := 0 else M := 32;
-    ctr_temp := CTR;
-    if ~ (BO[2])
-    then {
-      ctr_temp := ctr_temp - 1;
-      CTR := ctr_temp
-    }
-    else ();
-    ctr_ok := (BO[2] | ~ (ctr_temp[M .. 63] == 0) ^ BO[3]);
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~ (BO[1]));
-    if ctr_ok & cond_ok then NIA := LR[0 .. 61] : 0b00 else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[2], bit) Bcctr
-
-function clause decode (0b010011 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[3]) _ :
-(bit[2]) BH :
-0b1000010000 :
-[LK] as instr) =
-  Bcctr (BO,BI,BH,LK)
-
-function clause execute (Bcctr (BO, BI, BH, LK)) =
-  {
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~ (BO[1]));
-    if cond_ok then NIA := CTR[0 .. 61] : 0b00 else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[7]) Sc
-
-function clause decode (0b010001 :
-(bit[5]) _ :
-(bit[5]) _ :
-(bit[4]) _ :
-(bit[7]) LEV :
-(bit[3]) _ :
-0b1 :
-(bit[1]) _ as instr) =
-  Sc (LEV)
-
-function clause execute (Sc (LEV)) = ()
-
-union ast member (bit[5], bit[5], bit[16]) Lbzu
-
-function clause decode (0b100011 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lbzu (RT,RA,D)
-
-function clause execute (Lbzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    GPR[RT] :=
-      0b00000000000000000000000000000000000000000000000000000000 : MEMr (EA,1);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lbzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001110111 :
-(bit[1]) _ as instr) =
-  Lbzux (RT,RA,RB)
-
-function clause execute (Lbzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] :=
-      0b00000000000000000000000000000000000000000000000000000000 : MEMr (EA,1);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lhzu
-
-function clause decode (0b101001 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lhzu (RT,RA,D)
-
-function clause execute (Lhzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr (EA,2);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100110111 :
-(bit[1]) _ as instr) =
-  Lhzux (RT,RA,RB)
-
-function clause execute (Lhzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr (EA,2);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lhau
-
-function clause decode (0b101011 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lhau (RT,RA,D)
-
-function clause execute (Lhau (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    GPR[RT] := EXTS (MEMr (EA,2));
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhaux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101110111 :
-(bit[1]) _ as instr) =
-  Lhaux (RT,RA,RB)
-
-function clause execute (Lhaux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] := EXTS (MEMr (EA,2));
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lwz
-
-function clause decode (0b100000 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lwz (RT,RA,D)
-
-function clause execute (Lwz (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (D);
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr (EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lwzu
-
-function clause decode (0b100001 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lwzu (RT,RA,D)
-
-function clause execute (Lwzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr (EA,4);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110111 :
-(bit[1]) _ as instr) =
-  Lwzux (RT,RA,RB)
-
-function clause execute (Lwzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr (EA,4);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwaux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101110101 :
-(bit[1]) _ as instr) =
-  Lwaux (RT,RA,RB)
-
-function clause execute (Lwaux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] := EXTS (MEMr (EA,4));
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Ld
-
-function clause decode (0b111010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[14]) DS :
-0b00 as instr) =
-  Ld (RT,RA,DS)
-
-function clause execute (Ld (RT, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (DS : 0b00);
-    GPR[RT] := MEMr (EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Ldu
-
-function clause decode (0b111010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[14]) DS :
-0b01 as instr) =
-  Ldu (RT,RA,DS)
-
-function clause execute (Ldu (RT, RA, DS)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (DS : 0b00);
-    GPR[RT] := MEMr (EA,8);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Ldux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110101 :
-(bit[1]) _ as instr) =
-  Ldux (RT,RA,RB)
-
-function clause execute (Ldux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RT] := MEMr (EA,8);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stbu
-
-function clause decode (0b100111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stbu (RS,RA,D)
-
-function clause execute (Stbu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    MEMw(EA,1) := (GPR[RS])[56 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stbux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011110111 :
-(bit[1]) _ as instr) =
-  Stbux (RS,RA,RB)
-
-function clause execute (Stbux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,1) := (GPR[RS])[56 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Sthu
-
-function clause decode (0b101101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Sthu (RS,RA,D)
-
-function clause execute (Sthu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    MEMw(EA,2) := (GPR[RS])[48 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Sthux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110110111 :
-(bit[1]) _ as instr) =
-  Sthux (RS,RA,RB)
-
-function clause execute (Sthux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,2) := (GPR[RS])[48 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stw
-
-function clause decode (0b100100 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stw (RS,RA,D)
-
-function clause execute (Stw (RS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (D);
-    MEMw(EA,4) := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stwu
-
-function clause decode (0b100101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stwu (RS,RA,D)
-
-function clause execute (Stwu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    MEMw(EA,4) := (GPR[RS])[32 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stwux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010110111 :
-(bit[1]) _ as instr) =
-  Stwux (RS,RA,RB)
-
-function clause execute (Stwux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,4) := (GPR[RS])[32 .. 63];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Std
-
-function clause decode (0b111110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[14]) DS :
-0b00 as instr) =
-  Std (RS,RA,DS)
-
-function clause execute (Std (RS, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (DS : 0b00);
-    MEMw(EA,8) := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Stdu
-
-function clause decode (0b111110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[14]) DS :
-0b01 as instr) =
-  Stdu (RS,RA,DS)
-
-function clause execute (Stdu (RS, RA, DS)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (DS : 0b00);
-    MEMw(EA,8) := GPR[RS];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stdux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010110101 :
-(bit[1]) _ as instr) =
-  Stdux (RS,RA,RB)
-
-function clause execute (Stdux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,8) := GPR[RS];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[12], bit[4]) Lq
+val bit[32] -> option<ast> effect pure decode
 
-function clause decode (0b111000 :
-(bit[5]) RTp :
-(bit[5]) RA :
-(bit[12]) DQ :
-(bit[4]) PT as instr) =
-  Lq (RTp,RA,DQ,PT)
+scattered function option<ast> decode
 
-function clause execute (Lq (RTp, RA, DQ, PT)) =
-  {
-    (bit[64]) EA := 0;
-    (bit[64]) b := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (DQ : 0b0000);
-    (bit[128]) mem := MEMr (EA,16);
-    if bigendianmode
-    then {
-      GPR[RTp] := mem[0 .. 63];
-      GPR[RTp + 1] := mem[64 .. 127]
-    }
-    else {
-      (bit[128]) bytereverse := byte_reverse (mem);
-      GPR[RTp] := bytereverse[0 .. 63];
-      GPR[RTp + 1] := bytereverse[64 .. 127]
-    }
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Stq
-
-function clause decode (0b111110 :
-(bit[5]) RSp :
-(bit[5]) RA :
-(bit[14]) DS :
-0b10 as instr) =
-  Stq (RSp,RA,DS)
-
-function clause execute (Stq (RSp, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    {
-      (bit[64]) EA := 0;
-      (bit[64]) b := 0;
-      if RA == 0 then b := 0 else b := GPR[RA];
-      EA := b + EXTS (DS : 0b00);
-      (bit[128]) mem := 0;
-      mem[0..63] := GPR[RSp];
-      mem[64..127] := GPR[RSp + 1];
-      if ~ (bigendianmode) then mem := byte_reverse (mem) else ();
-      MEMw(EA,16) := mem
-    };
-    EA := b + EXTS (DS : 0b00);
-    MEMw(EA,8) := RSp
-  }
+union ast member ((bit[20]), regno, uop) UTYPE
 
-union ast member (bit[5], bit[5], bit[16]) Lmw
+function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI))
+function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC))
 
-function clause decode (0b101110 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lmw (RT,RA,D)
+function clause execute (UTYPE(imm, rd, op)) =
+    let (bit[64]) off = EXTS(imm : 0x000) in
+    let ret = switch (op) {
+      case LUI   -> off
+      case AUIPC -> PC + off
+    } in
+    wGPR(rd, ret)
 
-function clause execute (Lmw (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (D);
-    size := ([|32|]) (32 - RT) * 4;
-    buffer := MEMr (EA,size);
-    i := 0;
-    foreach (r from RT to 31 by 1 in inc)
-    {
-      GPR[r] := 0b00000000000000000000000000000000 : buffer[i .. i + 31];
-      i := i + 32
+union ast member ((bit[20]), regno) JAL
+function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd))
+function clause execute (JAL(imm, rd)) =
+    let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in {
+      nextPC :=  PC + offset;
+      wGPR(rd, PC + 4);
     }
-  }
 
-union ast member (bit[5], bit[5], bit[5]) Lswi
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) NB :
-0b1001010101 :
-(bit[1]) _ as instr) =
-  Lswi (RT,RA,NB)
-
-function clause execute (Lswi (RT, RA, NB)) =
-  {
-    (bit[64]) EA := 0;
-    if RA == 0 then EA := 0 else EA := GPR[RA];
-    ([|32|]) r := 0;
-    r := RT - 1;
-    ([|32|]) size := if NB == 0 then 32 else NB;
-    (bit[256]) membuffer := MEMr (EA,size);
-    j := 0;
-    i := 32;
-    foreach (n from (if NB == 0 then 32 else NB) to 1 by 1 in dec)
-    {
-      if i == 32
-      then {
-        r := ([|32|]) (r + 1) mod 32;
-        GPR[r] := 0
-      }
-      else ();
-      (GPR[r])[i..i + 7] := membuffer[j .. j + 7];
-      j := j + 8;
-      i := i + 8;
-      if i == 64 then i := 32 else ();
-      EA := EA + 1
+union ast member((bit[12]), regno, regno) JALR
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) =
+    Some(JALR(imm, rs1, rd))
+function clause execute (JALR(imm, rs1, rd)) =
+    let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in {
+      nextPC := newPC[63..1] : 0b0;
+      wGPR(rd, PC + 4);
     }
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Addi
-
-function clause decode (0b001110 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Addi (RT,RA,SI)
-
-function clause execute (Addi (RT, RA, SI)) =
-  if RA == 0 then GPR[RT] := EXTS (SI) else GPR[RT] := GPR[RA] + EXTS (SI)
-
-union ast member (bit[5], bit[5], bit[16]) Addis
-
-function clause decode (0b001111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Addis (RT,RA,SI)
-
-function clause execute (Addis (RT, RA, SI)) =
-  if RA == 0
-  then GPR[RT] := EXTS (SI : 0b0000000000000000)
-  else GPR[RT] := GPR[RA] + EXTS (SI : 0b0000000000000000)
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Add
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b100001010 :
-[Rc] as instr) =
-  Add (RT,RA,RB,OE,Rc)
-
-function clause execute (Add (RT, RA, RB, OE, Rc)) =
-  let (temp, overflow, _) = (GPR[RA] +_s GPR[RB]) in
-    {
-      GPR[RT] := temp;
-      if Rc
-      then {
-        xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0 (temp,xer_so)
-      }
-      else ();
-      if OE then set_SO_OV (overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Subf
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000101000 :
-[Rc] as instr) =
-  Subf (RT,RA,RB,OE,Rc)
 
-function clause execute (Subf (RT, RA, RB, OE, Rc)) =
-  let (t, overflow, _) = (~ (GPR[RA]) +_s GPR[RB]) in
-    {
-      (bit[64]) temp := t + 1;
-      GPR[RT] := temp;
-      if Rc
-      then {
-        xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0 (temp,xer_so)
-      }
-      else ();
-      if OE then set_SO_OV (overflow) else ()
+union ast member ((bit[12]), regno, regno, bop) BTYPE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU))
+
+function clause execute (BTYPE(imm, rs2, rs1, op)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let taken   = switch(op) {
+    case BEQ  -> rs1_val == rs2_val
+    case BNE  -> rs1_val != rs2_val
+    case BLT  -> rs1_val <_s rs2_val
+    case BGE  -> rs1_val >=_s rs2_val
+    case BLTU -> rs1_val <_u rs2_val
+    case BGEU -> rs1_val >= rs2_val (* XXX is this signed or unsigned? *)
+  } in
+  if (taken) then
+      nextPC := PC + EXTS(imm : 0b0)
+
+union ast member ((bit[12]), regno, regno, iop) ITYPE
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI))
+function clause execute (ITYPE (imm, rs1, rd, op)) =
+  let rs1_val = rGPR(rs1) in
+  let imm64 = (bit[64]) (EXTS(imm)) in
+  let (bit[64]) result = switch(op) {
+    case ADDI  -> rs1_val + imm64
+    case SLTI  -> EXTZ(rs1_val <_s imm64)
+    case SLTIU -> EXTZ(rs1_val <_u imm64)
+    case XORI  -> rs1_val ^ imm64
+    case ORI   -> rs1_val | imm64
+    case ANDI  -> rs1_val & imm64
+  } in
+  wGPR(rd, result)
+
+union ast member ((bit[6]), regno, regno, sop) SHIFTIOP
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI))
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI))
+function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI))
+function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = 
+    let rs1_val = rGPR(rs1) in
+    let result = switch(op) {
+      case SLLI -> rs1_val >> shamt
+      case SRLI -> rs1_val << shamt
+      case SRAI -> shift_right_arith64(rs1_val, shamt)
+    } in
+    wGPR(rd, result)
+
+union ast member (regno, regno, regno, rop) RTYPE
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND))
+function clause execute (RTYPE(rs2, rs1, rd, op)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let (bit[64]) result = switch(op) {
+    case ADD  -> rs1_val + rs2_val
+    case SUB  -> rs1_val - rs2_val
+    case SLL  -> rs1_val << (rs2_val[5..0])
+    case SLT  -> EXTZ(rs1_val <_s rs2_val)
+    case SLTU -> EXTZ(rs1_val <_u rs2_val)
+    case XOR  -> rs1_val ^ rs2_val
+    case SRL  -> rs1_val >> (rs2_val[5..0])
+    case SRA  -> shift_right_arith64(rs1_val, rs2_val[5..0])
+    case OR   -> rs1_val | rs2_val
+    case AND  -> rs1_val & rs2_val
+  } in
+  wGPR(rd, result)
+
+union ast member ((bit[12]), regno, regno, bool, [|8|]) LOAD
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 1))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 2))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 4))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 8))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  1))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  2))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  4))
+function clause execute(LOAD(imm, rs1, rd, unsigned, width)) =
+    let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
+    let (bit[64]) result = if unsigned then 
+        EXTZ(MEMr(addr, width))
+      else
+        EXTS(MEMr(addr, width)) in
+    wGPR(rd, result)
+
+union ast member ((bit[12]), regno, regno, [|8|]) STORE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 1))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 2))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 4))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 8))
+function clause execute (STORE(imm, rs2, rs1, width)) =
+    let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
+      MEMea(addr, width);
+      MEMval(addr, width, rGPR(rs2));
     }
 
-union ast member (bit[5], bit[5], bit[16]) Addic
-
-function clause decode (0b001100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Addic (RT,RA,SI)
-
-function clause execute (Addic (RT, RA, SI)) =
-  let (temp, _, carry) = (GPR[RA] +_s EXTS (SI)) in
-    {
-      GPR[RT] := temp;
-      CA := carry
-    }
-
-union ast member (bit[5], bit[5], bit[16]) AddicDot
-
-function clause decode (0b001101 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  AddicDot (RT,RA,SI)
-
-function clause execute (AddicDot (RT, RA, SI)) =
-  let (temp, overflow, carry) = (GPR[RA] +_s EXTS (SI)) in
-    {
-      GPR[RT] := temp;
-      CA := carry;
-      set_overflow_cr0 (temp,overflow)
-    }
-
-union ast member (bit[5], bit[5], bit, bit) Neg
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b001101000 :
-[Rc] as instr) =
-  Neg (RT,RA,OE,Rc)
-
-function clause execute (Neg (RT, RA, OE, Rc)) =
-  let (temp, overflow, _) = (~ (GPR[RA]) +_s (bit) 1) in
-    {
-      GPR[RT] := temp;
-      if Rc then set_overflow_cr0 (temp,XER.SO) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Mullw
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011101011 :
-[Rc] as instr) =
-  Mullw (RT,RA,RB,OE,Rc)
-
-function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
-  let (prod, overflow, _) = ((GPR[RA])[32 .. 63] *_s (GPR[RB])[32 .. 63]) in
-    {
-      GPR[RT] := prod;
-      if Rc
-      then {
-        xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0 (prod,xer_so)
-      }
-      else ();
-      if OE then set_SO_OV (overflow) else ()
-    }
-
-union ast member (bit[3], bit, bit[5], bit[16]) Cmpi
-
-function clause decode (0b001011 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Cmpi (BF,L,RA,SI)
-
-function clause execute (Cmpi (BF, L, RA, SI)) =
-  {
-    (bit[64]) a := 0;
-    if L == 0 then a := EXTS ((GPR[RA])[32 .. 63]) else a := GPR[RA];
-    if a < EXTS (SI)
-    then c := 0b100
-    else if a > EXTS (SI) then c := 0b010 else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[3], bit, bit[5], bit[5]) Cmp
-
-function clause decode (0b011111 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000000000 :
-(bit[1]) _ as instr) =
-  Cmp (BF,L,RA,RB)
-
-function clause execute (Cmp (BF, L, RA, RB)) =
-  {
-    (bit[64]) a := 0;
-    (bit[64]) b := 0;
-    if L == 0
-    then {
-      a := EXTS ((GPR[RA])[32 .. 63]);
-      b := EXTS ((GPR[RB])[32 .. 63])
-    }
-    else {
-      a := GPR[RA];
-      b := GPR[RB]
-    };
-    if a < b then c := 0b100 else if a > b then c := 0b010 else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Ori
-
-function clause decode (0b011000 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Ori (RS,RA,UI)
-
-function clause execute (Ori (RS, RA, UI)) =
-  GPR[RA] := (GPR[RS] | 0b000000000000000000000000000000000000000000000000 : UI)
-
-union ast member (bit[5], bit[5], bit[16]) Oris
-
-function clause decode (0b011001 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Oris (RS,RA,UI)
-
-function clause execute (Oris (RS, RA, UI)) =
-  GPR[RA] :=
-    (GPR[RS] | 0b00000000000000000000000000000000 : UI : 0b0000000000000000)
-
-union ast member (bit[5], bit[5], bit[16]) Xori
-
-function clause decode (0b011010 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Xori (RS,RA,UI)
-
-function clause execute (Xori (RS, RA, UI)) =
-  GPR[RA] := GPR[RS] ^ 0b000000000000000000000000000000000000000000000000 : UI
-
-union ast member (bit[5], bit[5], bit[5], bit) Or
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110111100 :
-[Rc] as instr) =
-  Or (RS,RA,RB,Rc)
-
-function clause execute (Or (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := (GPR[RS] | GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0 (temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit) Extsw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b1111011010 :
-[Rc] as instr) =
-  Extsw (RS,RA,Rc)
-
-function clause execute (Extsw (RS, RA, Rc)) =
-  {
-    s := (GPR[RS])[32];
-    (bit[64]) temp := 0;
-    temp := (GPR[RS])[32 .. 63];
-    temp := s ^^ 32;
-    if Rc then set_overflow_cr0 (temp,XER.SO) else ();
-    GPR[RA] := temp
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicr
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-(bit[6]) me :
-0b001 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Rldicr (RS,RA,instr[16 .. 20] : instr[30 .. 30],me,Rc)
-
-function clause execute (Rldicr (RS, RA, sh, me, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL (GPR[RS],n);
-    e := [me[5]] : me[0 .. 4];
-    m := MASK (0,e);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0 (temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[10]) Mtspr
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[10]) spr :
-0b0111010011 :
-(bit[1]) _ as instr) =
-  Mtspr (RS,spr)
-
-function clause execute (Mtspr (RS, spr)) =
-  {
-    n := spr[5 .. 9] : spr[0 .. 4];
-    if n == 13
-    then trap ()
-    else if length (SPR[n]) == 64
-    then SPR[n] := GPR[RS]
-    else SPR[n] := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[10]) Mfspr
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[10]) spr :
-0b0101010011 :
-(bit[1]) _ as instr) =
-  Mfspr (RT,spr)
-
-function clause execute (Mfspr (RT, spr)) =
-  {
-    n := spr[5 .. 9] : spr[0 .. 4];
-    if length (SPR[n]) == 64
-    then GPR[RT] := SPR[n]
-    else GPR[RT] := 0b00000000000000000000000000000000 : SPR[n]
-  }
-
-union ast member (bit[5], bit[8]) Mtcrf
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-0b0 :
-(bit[8]) FXM :
-(bit[1]) _ :
-0b0010010000 :
-(bit[1]) _ as instr) =
-  Mtcrf (RS,FXM)
-
-function clause execute (Mtcrf (RS, FXM)) =
-  {
-    mask :=
-      (FXM[0] ^^ 4) :
-        (FXM[1] ^^ 4) :
-          (FXM[2] ^^ 4) :
-            (FXM[3] ^^ 4) :
-              (FXM[4] ^^ 4) : (FXM[5] ^^ 4) : (FXM[6] ^^ 4) : (FXM[7] ^^ 4);
-    CR :=
-      ((bit[32]) ((GPR[RS])[32 .. 63] & mask) |
-        (bit[32]) (CR & ~ ((bit[32]) mask)))
-  }
-
-union ast member (bit[5]) Mfcr
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-0b0 :
-(bit[9]) _ :
-0b0000010011 :
-(bit[1]) _ as instr) =
-  Mfcr (RT)
-
-function clause execute (Mfcr (RT)) =
-  GPR[RT] := 0b00000000000000000000000000000000 : CR
-
-union ast member (bit[5], bit[5], bit[16]) Lfsu
-
-function clause decode (0b110001 :
-(bit[5]) FRT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lfsu (FRT,RA,D)
-
-function clause execute (Lfsu (FRT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    FPR[FRT] := DOUBLE (MEMr (EA,4));
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lfsux
-
-function clause decode (0b011111 :
-(bit[5]) FRT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000110111 :
-(bit[1]) _ as instr) =
-  Lfsux (FRT,RA,RB)
-
-function clause execute (Lfsux (FRT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    FPR[FRT] := DOUBLE (MEMr (EA,4));
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lfd
-
-function clause decode (0b110010 :
-(bit[5]) FRT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lfd (FRT,RA,D)
-
-function clause execute (Lfd (FRT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (D);
-    FPR[FRT] := MEMr (EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lfdu
-
-function clause decode (0b110011 :
-(bit[5]) FRT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Lfdu (FRT,RA,D)
-
-function clause execute (Lfdu (FRT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    FPR[FRT] := MEMr (EA,8);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lfdux
-
-function clause decode (0b011111 :
-(bit[5]) FRT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1001110111 :
-(bit[1]) _ as instr) =
-  Lfdux (FRT,RA,RB)
-
-function clause execute (Lfdux (FRT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    FPR[FRT] := MEMr (EA,8);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stfsu
-
-function clause decode (0b110101 :
-(bit[5]) FRS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stfsu (FRS,RA,D)
-
-function clause execute (Stfsu (FRS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    MEMw(EA,4) := SINGLE (FPR[FRS]);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stfsux
-
-function clause decode (0b011111 :
-(bit[5]) FRS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1010110111 :
-(bit[1]) _ as instr) =
-  Stfsux (FRS,RA,RB)
-
-function clause execute (Stfsux (FRS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,4) := SINGLE (FPR[FRS]);
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stfd
-
-function clause decode (0b110110 :
-(bit[5]) FRS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stfd (FRS,RA,D)
-
-function clause execute (Stfd (FRS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (D);
-    MEMw(EA,8) := FPR[FRS]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stfdu
-
-function clause decode (0b110111 :
-(bit[5]) FRS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Stfdu (FRS,RA,D)
-
-function clause execute (Stfdu (FRS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS (D);
-    MEMw(EA,8) := FPR[FRS];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stfdux
-
-function clause decode (0b011111 :
-(bit[5]) FRS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1011110111 :
-(bit[1]) _ as instr) =
-  Stfdux (FRS,RA,RB)
-
-function clause execute (Stfdux (FRS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw(EA,8) := FPR[FRS];
-    GPR[RA] := EA
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Lfdp
-
-function clause decode (0b111001 :
-(bit[5]) FRTp :
-(bit[5]) RA :
-(bit[14]) DS :
-0b0 :
-0b0 as instr) =
-  Lfdp (FRTp,RA,DS)
-
-function clause execute (Lfdp (FRTp, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (DS : 0b00);
-    FPRp[FRTp] := MEMr (EA,16)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lfdpx
-
-function clause decode (0b011111 :
-(bit[5]) FRTp :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1100010111 :
-(bit[1]) _ as instr) =
-  Lfdpx (FRTp,RA,RB)
-
-function clause execute (Lfdpx (FRTp, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    FPRp[FRTp] := MEMr (EA,16)
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Stfdp
-
-function clause decode (0b111101 :
-(bit[5]) FRSp :
-(bit[5]) RA :
-(bit[14]) DS :
-0b0 :
-0b0 as instr) =
-  Stfdp (FRSp,RA,DS)
-
-function clause execute (Stfdp (FRSp, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS (DS : 0b00);
-    MEMw(EA,16) := FPRp[FRSp]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stfdpx
-
-function clause decode (0b011111 :
-(bit[5]) FRSp :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1110010111 :
-(bit[1]) _ as instr) =
-  Stfdpx (FRSp,RA,RB)
-
-function clause execute (Stfdpx (FRSp, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw(EA,16) := FPRp[FRSp]
-  }
-
-union ast member (bit[5], bit) Mffs
-
-function clause decode (0b111111 :
-(bit[5]) FRT :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1001000111 :
-[Rc] as instr) =
-  Mffs (FRT,Rc)
-
-function clause execute (Mffs (FRT, Rc)) = ()
-
-union ast member (bit[3], bit[3]) Mcrfs
-
-function clause decode (0b111111 :
-(bit[3]) BF :
-(bit[2]) _ :
-(bit[3]) BFA :
-(bit[2]) _ :
-(bit[5]) _ :
-0b0001000000 :
-(bit[1]) _ as instr) =
-  Mcrfs (BF,BFA)
-
-function clause execute (Mcrfs (BF, BFA)) = ()
-
-union ast member (bit[5], bit[5], bit[5]) Lvx
-
-function clause decode (0b011111 :
-(bit[5]) VRT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001100111 :
-(bit[1]) _ as instr) =
-  Lvx (VRT,RA,RB)
-
-function clause execute (Lvx (VRT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    VR[VRT] :=
-      MEMr
-        (EA & 0b1111111111111111111111111111111111111111111111111111111111110000,16)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stvx
-
-function clause decode (0b011111 :
-(bit[5]) VRS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011100111 :
-(bit[1]) _ as instr) =
-  Stvx (VRS,RA,RB)
-
-function clause execute (Stvx (VRS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw(EA & 0b1111111111111111111111111111111111111111111111111111111111110000,16) :=
-      VR[VRS]
-  }
-
-union ast member (bit[5]) Mtvscr
-
-function clause decode (0b000100 :
-(bit[10]) _ :
-(bit[5]) VRB :
-0b11001000100 as instr) =
-  Mtvscr (VRB)
-
-function clause execute (Mtvscr (VRB)) = VSCR := (VR[VRB])[96 .. 127]
-
-union ast member (bit[5]) Mfvscr
-
-function clause decode (0b000100 :
-(bit[5]) VRT :
-(bit[10]) _ :
-0b11000000100 as instr) =
-  Mfvscr (VRT)
-
-function clause execute (Mfvscr (VRT)) =
-  VR[VRT] :=
-    0b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 :
-      VSCR
-
-union ast member (bit[2]) Sync
-
-function clause decode (0b011111 :
-(bit[3]) _ :
-(bit[2]) L :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1001010110 :
-(bit[1]) _ as instr) =
-  Sync (L)
-
-function clause execute (Sync (L)) =
-  switch L { case 0b00 -> { H_Sync (()) } case 0b01 -> { LW_Sync (()) } }
-
-union ast member (bit[5]) Mbar
-
-function clause decode (0b011111 :
-(bit[5]) MO :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1101010110 :
-(bit[1]) _ as instr) =
-  Mbar (MO)
-
-function clause execute (Mbar (MO)) = ()
-
-
-typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction } 
-
-function clause decode _ = exit no_matching_pattern
+union ast member ((bit[12]), regno, regno) ADDIW
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd))
+function clause execute (ADDIW(imm, rs1, rd)) =
+  let (bit[64]) imm64 = EXTS(imm) in
+  let (bit[64]) result64 = imm64 + rGPR(rs1) in
+  let (bit[64]) result32 = EXTS(result64[31..0]) in
+  wGPR(rd, result32)
+
+union ast member ((bit[5]), regno, regno, sop) SHIFTW
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI))
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI))
+function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI))
+function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
+    let rs1_val = (rGPR(rs1))[31..0] in
+    let result = switch(op) {
+      case SLLI -> rs1_val >> shamt
+      case SRLI -> rs1_val << shamt
+      case SRAI -> shift_right_arith32(rs1_val, shamt)
+    } in
+    wGPR(rd, EXTS(result))
+
+union ast member (regno, regno, regno, ropw) RTYPEW
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW))
+function clause execute (RTYPEW(rs2, rs1, rd, op)) =
+  let rs1_val = (rGPR(rs1))[31..0] in
+  let rs2_val = (rGPR(rs2))[31..0] in
+  let (bit[32]) result = switch(op) {
+    case ADDW -> rs1_val + rs2_val
+    case SUBW -> rs1_val - rs2_val
+    case SLLW -> rs1_val << (rs2_val[4..0])
+    case SRLW -> rs1_val >> (rs2_val[4..0])
+    case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
+  } in
+  wGPR(rd, EXTS(result))
 
+end ast
 end decode
 end execute
-end ast
-
-val ast -> ast effect pure supported_instructions
-function ast supported_instructions ((ast) instr) = {
-  switch instr {
-    case (Mbar(_)) -> exit unsupported_instruction
-    case (Sync(0b10)) -> exit unsupported_instruction
-    case (Sync(0b11)) -> exit unsupported_instruction
-    case _ -> instr
-   }
-}
-
-val ast -> bit effect pure illegal_instructions_pred
-function bit illegal_instructions_pred ((ast) instr) = {
-     switch instr {
-        case (Bcctr(BO,BI,BH,LK)) -> ~(BO[2])
-        case (Lbzu(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lbzux(RT,RA,_)) ->(RA == 0) | (RA == RT)
-        case (Lhzu(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lhzux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lhau(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lhaux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lwzu(RA,RT,D)) -> (RA == 0) | (RA == RT)
-        case (Lwzux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lwaux(RA,RT,RB)) -> (RA == 0) | (RA == RT)
-        case (Ldu(RT,RA,DS)) -> (RA == 0) | (RA == RT)
-        case (Ldux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Stbu(RS,RA,D)) -> (RA == 0)
-        case (Stbux(RS,RA,RB)) -> (RA == 0)
-        case (Sthu(RS,RA,RB)) -> (RA == 0)
-        case (Sthux(RS,RA,RB)) -> (RA == 0)
-        case (Stwu(RS,RA,D)) -> (RA == 0)
-        case (Stwux(RS,RA,RB)) -> (RA == 0)
-        case (Stdu(RS,RA,DS)) -> (RA == 0)
-        case (Stdux(RS,RA,RB)) -> (RA == 0)
-        case (Lmw(RT,RA,D)) -> (RA == 0) | ((RT <= RA) & (RA <= 31))
-        case (Lswi(RT,RA,NB)) ->
-           let (([|32|]) n) = (if ~(NB == 0) then NB else 32) in
-           let ceil =
-             (if (n mod 4) == 0
-             then n quot 4 else (n quot 4) + 1) in
-           (RT <= RA) & (RA <= ((bit[5]) (((bit[5]) (RT + ceil)) -1)))
-        (* Can't read XER at the time meant, so will need to rethink *)
-       (* case (Lswx(RT,RA,RB)) ->
-           let (([|32|]) n) = (XER[57..63]) in
-           let ceil =
-             (if (n mod 4 == 0)
-             then n quot 4 else (n quot 4) + 1) in
-           let ((bit[5]) upper_bound) = (RT + ceil) in
-           (RT <= RA & RA <= upper_bound) |
-           (RT <= RB & RB <= upper_bound) |
-           (RT == RA) | (RT == RB)*)
-        case (Lfsu(FRT,RA,D)) -> (RA == 0)
-        case (Lfsux(FRT,RA,RB)) -> (RA == 0)
-        case (Lfdu(FRT,RA,D)) -> (RA == 0)
-        case (Lfdux(FRT,RA,RB)) -> (RA == 0)
-        case (Stfsu(FRS,RA,D)) -> (RA == 0)
-        case (Stfsux(FRS,RA,RB)) -> (RA == 0)
-        case (Stfdu(FRS,D,RA)) -> (RA == 0)
-        case (Stfdux(FRS,RA,RB)) -> (RA == 0)
-        case (Lfdp(FRTp,RA,DS)) -> (FRTp mod 2 == 1)
-        case (Stfdp(FRSp,RA,DS)) -> (FRSp mod 2 == 1)
-        case (Lfdpx(FRTp,RA,RB)) -> (FRTp mod 2 == 1)
-        case (Stfdpx(FRSp,RA,RB)) -> (FRSp mod 2 == 1)
-        case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA)
-        case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1)
-        case (Mtspr(RS, spr)) ->
-          ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 256) |
-            (spr == 512) | (spr == 896) | (spr == 898))
-(*One of these causes a stack overflow error, don't want to debug why now*)
-        (*case (Mfspr(RT, spr)) ->
-           ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 136) |
-           (spr == 256) | (spr == 259) | (spr == 260) | (spr == 261) |
-           (spr == 262) | (spr == 263) | (spr == 268) | (spr == 268) |
-           (spr == 269) | (spr == 512) | (spr == 526) | (spr == 526) |
-           (spr == 527) | (spr == 896) | (spr == 898))
-        case (Se_illegal) -> true
-        case (E_lhau(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_Lhzu(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_lwzu(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_stbu(RS,RA,D8)) -> (RA == 0)
-        case (E_sthu(RS,RA,D8)) -> (RA == 0)
-        case (E_stwu(RS,RA,D8)) -> (RA == 0)
-        case (E_lmw(RT,RA,D8)) -> (RT <= RA & RA <= 31)*)
-        case _ -> false
-     }
-}
-
-val ast -> ast effect pure illegal_instructions
-function ast illegal_instructions ((ast) instr) =
-  if (illegal_instructions_pred ((ast) instr))
-  then exit illegal_instruction else instr
-
-(* fetch-decode-execute *)
-function unit fde () = {
-  NIA := CIA + 4;
-  instr := decode(MEMr(CIA, 4));
-  instr := supported_instructions(instr);
-  execute(instr);
-  CIA := NIA;
-}*)