diff options
| author | Alasdair Armstrong | 2018-07-30 19:16:34 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-08-01 16:42:33 +0100 |
| commit | 1479ae359fd3afebf9c3dfb6e58a77254e8140ea (patch) | |
| tree | ffcfd96409467a5c41009f68afe1f65a2c7a3d49 /src/test/power.sail | |
| parent | 0b70a9d7464d6c30534d2f511cb8c9879c76b1e5 (diff) | |
Remove old test directory in src/test
Diffstat (limited to 'src/test/power.sail')
| -rw-r--r-- | src/test/power.sail | 4543 |
1 files changed, 0 insertions, 4543 deletions
diff --git a/src/test/power.sail b/src/test/power.sail deleted file mode 100644 index 87a81ab9..00000000 --- a/src/test/power.sail +++ /dev/null @@ -1,4543 +0,0 @@ - -(* XXX binary coded decimal *) -(*function bit[12] DEC_TO_BCD ( (bit[10]) declet ) = { - (bit[4]) hundreds := 0; - (bit[4]) tens := 0; - (bit[4]) ones := 0; - foreach (i from 0 to 9) { - if hundreds >= 5 then hundreds := hundreds + 3; - if tens >= 5 then tens := tens + 3; - if ones >= 5 then ones := ones + 3; - hundreds := hundreds << 1; - hundreds[3] := tens[0]; - tens := tens << 1; - tens[3] := ones[0]; - ones := ones << 1; - ones[3] := declet[i] }; - hundreds:tens:ones }*) - -function bit[12] DEC_TO_BCD ( (bit[10]) [p,q,r,s,t,u,v,w,x,y]) = { - a := ((~(s) & v & w) | (t & v & w & s) | (v & w & ~(x))); - b := ((p & s & x & ~(t)) | (p & ~(w)) | (p & ~(v))); - c := ((q & s & x & ~(t)) | (q & ~(w)) | (q & ~(v))); - d := r; - - e := ((v & ~(w) & x) | (s & v & w & x) | (~(t) & v & x & w)); - f := ((p & t & v & w & x & ~(s)) | (s & ~(x) & v) | (s & ~(v))); - g := ((q & t & w & v & x & ~(s)) | (t & ~(x) & v) | (t & ~(v))); - h := u; - - i := ((t & v & w & x) | (s & v & w & x) | (v & ~(w) & ~(x))); - j := ((p & ~(s) & ~(t) & w & v) | (s & v & ~(w) & x) | (p & w & ~(x) & v) | (w & ~(v))); - k := ((q & ~(s) & ~(t) & v & w) | (t & v & ~(w) & x) | (q & v & w & ~(x)) | (x & ~(v))); - m := y; - [a,b,c,d,e,f,g,h,i,j,k,m] -} - -(*function bit[10] BCD_TO_DEC ( (bit[12]) bcd ) = - (bit[10]) (([|2** 10|]) (bcd[0..3] * 100)) + ([|2** 7|]) ((([|2** 7|]) (bcd[4..7] * 10)) + bcd[8..11]) -*) - -function bit[10] BCD_TO_DEC ( (bit[12]) [a,b,c,d,e,f,g,h,i,j,k,m] ) = { - p := ((f & a & i & ~(e)) | (j & a & ~(i)) | (b & ~(a))); - q := ((g & a & i & ~(e)) | (k & a & ~(i)) | (c & ~(a))); - r := d; - s := ((j & ~(a) & e & ~(i)) | (f & ~(i) & ~(e)) | (f & ~(a) & ~(e)) | (e & i)); - t := ((k & ~(a) & e & ~(i)) | (g & ~(i) & ~(e)) | (g & ~(a) & ~(e)) | (a & i)); - u := h; - v := (a | e | i); - w := ((~(e) & j & ~(i)) | (e & i) | a); - x := ((~(a) & k & ~(i)) | (a & i) | e); - y := m; - [p,q,r,s,t,u,v,w,x,y] -} - -(* 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]) SPRG3 -register (bit[64]) SPRG4 -register (bit[64]) SPRG5 -register (bit[64]) SPRG6 -register (bit[64]) SPRG7 - -let (vector <0, 1024, inc, (register<(bit[64])>) >) SPR = - [ 1=XER, 8=LR, 9=CTR(*, 256=VRSAVE (*32 bit, so not 64, caught by type checker at last*)*), 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7 - ] - -(* 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, 1024, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR = - [ 0=DCR0, 1=DCR1 ; default=undefined] - -(* 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 - -(* Pair-wise access to FPR registers *) - -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 ] - - -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[1:11]) 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[11]) 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. (implicit<'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 'n, Nat 'm. (bit['m]) Chop(x, y) = x[0..y] - -val forall Nat 'o, Nat 'n, Nat 'm, Nat 'k, 'n <= 0. - (implicit<'k>, [:'o:], [:'n:], [|'m|]) -> bit['k] effect { wreg } Clamp - -function forall Nat 'o,Nat 'n, Nat 'm, Nat 'k, 'n <= 0. (bit['k]) -Clamp(([:'o:]) 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 { wmv } 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 { wmv } MEMw_conditional - -(* announce write address for plain write *) -val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA - -(* announce write address for write conditional *) -val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA_cond - -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 - -val extern unit -> unit effect { depend } recalculate_dependency - -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 -} - -(* XXX effect for trap? *) -val extern unit -> unit effect {escape} 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) = { - m:= 0; - (bit[3]) c:= 0; - (bit[64]) zero := 0; - (if mode64bit - then m := 0 - else m := 32); - (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); -} - -function forall Nat 'n. (bit['n]) zero_or_undef ((bit['n]) x) = { - (bit['n]) out := 0; - foreach (i from 0 to ((length(x)) - 1)) { - out[i] := if x[i] then undefined else 0 - }; - out -} - -scattered function unit execute -scattered typedef ast = const union - -val bit[32] -> option<ast> effect pure decode - -scattered function option<ast> decode - -union ast member (bit[24], bit, bit) B - -function clause decode (0b010010 : (bit[24]) LI : [AA] : [LK] as instr) = Some(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) = - Some(Bc(BO,BI,BD,AA,LK)) - -function clause execute (Bc (BO, BI, BD, AA, LK)) = - { - if mode64bit then M := 0 else M := 32; - (bit[64]) 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) = - Some(Bclr(BO,BI,BH,LK)) - -function clause execute (Bclr (BO, BI, BH, LK)) = - { - if mode64bit then M := 0 else M := 32; - (bit[64]) 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) = - Some(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[5], bit[5], bit[5]) Crand - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0100000001 : -(bit[1]) _ as instr) = - Some(Crand(BT,BA,BB)) - -function clause execute (Crand (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] & CR[BB + 32]) - -union ast member (bit[5], bit[5], bit[5]) Crnand - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0011100001 : -(bit[1]) _ as instr) = - Some(Crnand(BT,BA,BB)) - -function clause execute (Crnand (BT, BA, BB)) = CR[BT + 32] := ~(CR[BA + 32] & CR[BB + 32]) - -union ast member (bit[5], bit[5], bit[5]) Cror - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0111000001 : -(bit[1]) _ as instr) = - Some(Cror(BT,BA,BB)) - -function clause execute (Cror (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] | CR[BB + 32]) - -union ast member (bit[5], bit[5], bit[5]) Crxor - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0011000001 : -(bit[1]) _ as instr) = - Some(Crxor(BT,BA,BB)) - -function clause execute (Crxor (BT, BA, BB)) = CR[BT + 32] := CR[BA + 32] ^ CR[BB + 32] - -union ast member (bit[5], bit[5], bit[5]) Crnor - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0000100001 : -(bit[1]) _ as instr) = - Some(Crnor(BT,BA,BB)) - -function clause execute (Crnor (BT, BA, BB)) = CR[BT + 32] := ~(CR[BA + 32] | CR[BB + 32]) - -union ast member (bit[5], bit[5], bit[5]) Creqv - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0100100001 : -(bit[1]) _ as instr) = - Some(Creqv(BT,BA,BB)) - -function clause execute (Creqv (BT, BA, BB)) = CR[BT + 32] := CR[BA + 32] ^ ~(CR[BB + 32]) - -union ast member (bit[5], bit[5], bit[5]) Crandc - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0010000001 : -(bit[1]) _ as instr) = - Some(Crandc(BT,BA,BB)) - -function clause execute (Crandc (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] & ~(CR[BB + 32])) - -union ast member (bit[5], bit[5], bit[5]) Crorc - -function clause decode (0b010011 : -(bit[5]) BT : -(bit[5]) BA : -(bit[5]) BB : -0b0110100001 : -(bit[1]) _ as instr) = - Some(Crorc(BT,BA,BB)) - -function clause execute (Crorc (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] | ~(CR[BB + 32])) - -union ast member (bit[3], bit[3]) Mcrf - -function clause decode (0b010011 : -(bit[3]) BF : -(bit[2]) _ : -(bit[3]) BFA : -(bit[2]) _ : -(bit[5]) _ : -0b0000000000 : -(bit[1]) _ as instr) = - Some(Mcrf(BF,BFA)) - -function clause execute (Mcrf (BF, BFA)) = - CR[4 * BF + 32..4 * BF + 35] := CR[4 * BFA + 32 .. 4 * BFA + 35] - -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) = - Some(Sc(LEV)) - -function clause execute (Sc (LEV)) = () - -union ast member (bit[7]) Scv - -function clause decode (0b010001 : -(bit[5]) _ : -(bit[5]) _ : -(bit[4]) _ : -(bit[7]) LEV : -(bit[3]) _ : -0b0 : -0b1 as instr) = - Some(Scv(LEV)) - -function clause execute (Scv (LEV)) = () - -union ast member (bit[5], bit[5], bit[16]) Lbz - -function clause decode (0b100010 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Lbz(RT,RA,D)) - -function clause execute (Lbz (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] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1) - } - -union ast member (bit[5], bit[5], bit[5]) Lbzx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0001010111 : -(bit[1]) _ as instr) = - Some(Lbzx(RT,RA,RB)) - -function clause execute (Lbzx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1) - } - -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) = - Some(Lbzu(RT,RA,D)) - -function clause execute (Lbzu (RT, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - GPR[RA] := EA; - GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1) - } - -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) = - Some(Lbzux(RT,RA,RB)) - -function clause execute (Lbzux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1) - } - -union ast member (bit[5], bit[5], bit[16]) Lhz - -function clause decode (0b101000 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Lhz(RT,RA,D)) - -function clause execute (Lhz (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] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2) - } - -union ast member (bit[5], bit[5], bit[5]) Lhzx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0100010111 : -(bit[1]) _ as instr) = - Some(Lhzx(RT,RA,RB)) - -function clause execute (Lhzx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2) - } - -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) = - Some(Lhzu(RT,RA,D)) - -function clause execute (Lhzu (RT, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - GPR[RA] := EA; - GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2) - } - -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) = - Some(Lhzux(RT,RA,RB)) - -function clause execute (Lhzux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2) - } - -union ast member (bit[5], bit[5], bit[16]) Lha - -function clause decode (0b101010 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Lha(RT,RA,D)) - -function clause execute (Lha (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] := EXTS(MEMr(EA,2)) - } - -union ast member (bit[5], bit[5], bit[5]) Lhax - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0101010111 : -(bit[1]) _ as instr) = - Some(Lhax(RT,RA,RB)) - -function clause execute (Lhax (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := EXTS(MEMr(EA,2)) - } - -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) = - Some(Lhau(RT,RA,D)) - -function clause execute (Lhau (RT, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - GPR[RA] := EA; - GPR[RT] := EXTS(MEMr(EA,2)) - } - -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) = - Some(Lhaux(RT,RA,RB)) - -function clause execute (Lhaux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := EXTS(MEMr(EA,2)) - } - -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) = - Some(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[5]) Lwzx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000010111 : -(bit[1]) _ as instr) = - Some(Lwzx(RT,RA,RB)) - -function clause execute (Lwzx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - 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) = - Some(Lwzu(RT,RA,D)) - -function clause execute (Lwzu (RT, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - GPR[RA] := EA; - GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4) - } - -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) = - Some(Lwzux(RT,RA,RB)) - -function clause execute (Lwzux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4) - } - -union ast member (bit[5], bit[5], bit[14]) Lwa - -function clause decode (0b111010 : -(bit[5]) RT : -(bit[5]) RA : -(bit[14]) DS : -0b10 as instr) = - Some(Lwa(RT,RA,DS)) - -function clause execute (Lwa (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] := EXTS(MEMr(EA,4)) - } - -union ast member (bit[5], bit[5], bit[5]) Lwax - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0101010101 : -(bit[1]) _ as instr) = - Some(Lwax(RT,RA,RB)) - -function clause execute (Lwax (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := EXTS(MEMr(EA,4)) - } - -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) = - Some(Lwaux(RT,RA,RB)) - -function clause execute (Lwaux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := EXTS(MEMr(EA,4)) - } - -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) = - Some(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[5]) Ldx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000010101 : -(bit[1]) _ as instr) = - Some(Ldx(RT,RA,RB)) - -function clause execute (Ldx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - 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) = - Some(Ldu(RT,RA,DS)) - -function clause execute (Ldu (RT, RA, DS)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(DS : 0b00); - GPR[RA] := EA; - GPR[RT] := MEMr(EA,8) - } - -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) = - Some(Ldux(RT,RA,RB)) - -function clause execute (Ldux (RT, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - GPR[RA] := EA; - GPR[RT] := MEMr(EA,8) - } - -union ast member (bit[5], bit[5], bit[16]) Stb - -function clause decode (0b100110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Stb(RS,RA,D)) - -function clause execute (Stb (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(EA,1); - MEMw(EA,1) := (GPR[RS])[56 .. 63] - } - -union ast member (bit[5], bit[5], bit[5]) Stbx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0011010111 : -(bit[1]) _ as instr) = - Some(Stbx(RS,RA,RB)) - -function clause execute (Stbx (RS, 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(EA,1); - MEMw(EA,1) := (GPR[RS])[56 .. 63] - } - -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) = - Some(Stbu(RS,RA,D)) - -function clause execute (Stbu (RS, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - MEMw_EA(EA,1); - GPR[RA] := EA; - MEMw(EA,1) := (GPR[RS])[56 .. 63] - } - -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) = - Some(Stbux(RS,RA,RB)) - -function clause execute (Stbux (RS, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - MEMw_EA(EA,1); - GPR[RA] := EA; - MEMw(EA,1) := (GPR[RS])[56 .. 63] - } - -union ast member (bit[5], bit[5], bit[16]) Sth - -function clause decode (0b101100 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Sth(RS,RA,D)) - -function clause execute (Sth (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(EA,2); - MEMw(EA,2) := (GPR[RS])[48 .. 63] - } - -union ast member (bit[5], bit[5], bit[5]) Sthx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0110010111 : -(bit[1]) _ as instr) = - Some(Sthx(RS,RA,RB)) - -function clause execute (Sthx (RS, 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(EA,2); - MEMw(EA,2) := (GPR[RS])[48 .. 63] - } - -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) = - Some(Sthu(RS,RA,D)) - -function clause execute (Sthu (RS, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - MEMw_EA(EA,2); - GPR[RA] := EA; - MEMw(EA,2) := (GPR[RS])[48 .. 63] - } - -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) = - Some(Sthux(RS,RA,RB)) - -function clause execute (Sthux (RS, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - MEMw_EA(EA,2); - GPR[RA] := EA; - MEMw(EA,2) := (GPR[RS])[48 .. 63] - } - -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) = - Some(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(EA,4); - MEMw(EA,4) := (GPR[RS])[32 .. 63] - } - -union ast member (bit[5], bit[5], bit[5]) Stwx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0010010111 : -(bit[1]) _ as instr) = - Some(Stwx(RS,RA,RB)) - -function clause execute (Stwx (RS, 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(EA,4); - 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) = - Some(Stwu(RS,RA,D)) - -function clause execute (Stwu (RS, RA, D)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(D); - MEMw_EA(EA,4); - GPR[RA] := EA; - MEMw(EA,4) := (GPR[RS])[32 .. 63] - } - -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) = - Some(Stwux(RS,RA,RB)) - -function clause execute (Stwux (RS, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - MEMw_EA(EA,4); - GPR[RA] := EA; - MEMw(EA,4) := (GPR[RS])[32 .. 63] - } - -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) = - Some(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(EA,8); - MEMw(EA,8) := GPR[RS] - } - -union ast member (bit[5], bit[5], bit[5]) Stdx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0010010101 : -(bit[1]) _ as instr) = - Some(Stdx(RS,RA,RB)) - -function clause execute (Stdx (RS, 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(EA,8); - 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) = - Some(Stdu(RS,RA,DS)) - -function clause execute (Stdu (RS, RA, DS)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + EXTS(DS : 0b00); - MEMw_EA(EA,8); - GPR[RA] := EA; - MEMw(EA,8) := GPR[RS] - } - -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) = - Some(Stdux(RS,RA,RB)) - -function clause execute (Stdux (RS, RA, RB)) = - { - (bit[64]) EA := 0; - EA := GPR[RA] + GPR[RB]; - MEMw_EA(EA,8); - GPR[RA] := EA; - MEMw(EA,8) := GPR[RS] - } - -union ast member (bit[5], bit[5], bit[12], bit[4]) Lq - -function clause decode (0b111000 : -(bit[5]) RTp : -(bit[5]) RA : -(bit[12]) DQ : -(bit[4]) PT as instr) = - Some(Lq(RTp,RA,DQ,PT)) - -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) = - Some(Stq(RSp,RA,DS)) - -function clause execute (Stq (RSp, 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(EA,16); - (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 - } - -union ast member (bit[5], bit[5], bit[5]) Lhbrx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b1100010110 : -(bit[1]) _ as instr) = - Some(Lhbrx(RT,RA,RB)) - -function clause execute (Lhbrx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - load_data := MEMr(EA,2); - GPR[RT] := - 0b000000000000000000000000000000000000000000000000 : load_data[8 .. 15] : load_data[0 .. 7] - } - -union ast member (bit[5], bit[5], bit[5]) Sthbrx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1110010110 : -(bit[1]) _ as instr) = - Some(Sthbrx(RS,RA,RB)) - -function clause execute (Sthbrx (RS, 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(EA,2); - MEMw(EA,2) := (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55] - } - -union ast member (bit[5], bit[5], bit[5]) Lwbrx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b1000010110 : -(bit[1]) _ as instr) = - Some(Lwbrx(RT,RA,RB)) - -function clause execute (Lwbrx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - load_data := MEMr(EA,4); - GPR[RT] := - 0b00000000000000000000000000000000 : - load_data[24 .. 31] : load_data[16 .. 23] : load_data[8 .. 15] : load_data[0 .. 7] - } - -union ast member (bit[5], bit[5], bit[5]) Stwbrx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1010010110 : -(bit[1]) _ as instr) = - Some(Stwbrx(RS,RA,RB)) - -function clause execute (Stwbrx (RS, 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(EA,4); - MEMw(EA,4) := - (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55] : (GPR[RS])[40 .. 47] : (GPR[RS])[32 .. 39] - } - -union ast member (bit[5], bit[5], bit[5]) Ldbrx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b1000010100 : -(bit[1]) _ as instr) = - Some(Ldbrx(RT,RA,RB)) - -function clause execute (Ldbrx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - load_data := MEMr(EA,8); - GPR[RT] := - load_data[56 .. 63] : - load_data[48 .. 55] : - load_data[40 .. 47] : - load_data[32 .. 39] : - load_data[24 .. 31] : load_data[16 .. 23] : load_data[8 .. 15] : load_data[0 .. 7] - } - -union ast member (bit[5], bit[5], bit[5]) Stdbrx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1010010100 : -(bit[1]) _ as instr) = - Some(Stdbrx(RS,RA,RB)) - -function clause execute (Stdbrx (RS, 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(EA,8); - MEMw(EA,8) := - (GPR[RS])[56 .. 63] : - (GPR[RS])[48 .. 55] : - (GPR[RS])[40 .. 47] : - (GPR[RS])[32 .. 39] : - (GPR[RS])[24 .. 31] : (GPR[RS])[16 .. 23] : (GPR[RS])[8 .. 15] : (GPR[RS])[0 .. 7] - } - -union ast member (bit[5], bit[5], bit[16]) Lmw - -function clause decode (0b101110 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Lmw(RT,RA,D)) - -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[5], bit[5], bit[16]) Stmw - -function clause decode (0b101111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) D as instr) = - Some(Stmw(RS,RA,D)) - -function clause execute (Stmw (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); - size := ([|32|]) (32 - RS) * 4; - MEMw_EA(EA,size); - (bit[994]) buffer := [0 = 0,993 = 0; default=0]; - i := 0; - foreach (r from RS to 31 by 1 in inc) - { - buffer[i..i + 31] := (GPR[r])[32 .. 63]; - i := i + 32 - }; - MEMw(EA,size) := buffer[0 .. size * 8] - } - -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) = - Some(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]; - ([|31|]) 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 := ([|31|]) (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[5], bit[5], bit[5]) Lswx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b1000010101 : -(bit[1]) _ as instr) = - Some(Lswx(RT,RA,RB)) - -function clause execute (Lswx (RT, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - ([|31|]) r := 0; - EA := b + GPR[RB]; - r := RT - 1; - i := 32; - ([|128|]) n_top := XER[57 .. 63]; - recalculate_dependency(()); - if n_top == 0 - then GPR[RT] := undefined - else { - (bit[512]) membuffer := MEMr(EA,n_top); - j := 0; - n_r := n_top quot 4; - n_mod := n_top mod 4; - n_r := if n_mod == 0 then n_r else n_r + 1; - foreach (n from n_r to 1 by 1 in dec) - { - r := ([|32|]) (r + 1) mod 32; - (bit[64]) temp := 0; - if n == 1 - then switch n_mod { - case 0 -> temp[32..63] := membuffer[j .. j + 31] - case 1 -> temp[32..39] := membuffer[j .. j + 7] - case 2 -> temp[32..47] := membuffer[j .. j + 15] - case 3 -> temp[32..55] := membuffer[j .. j + 23] - } - else temp[32..63] := membuffer[j .. j + 31]; - j := j + 32; - GPR[r] := temp - } - } - } - -union ast member (bit[5], bit[5], bit[5]) Stswi - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) NB : -0b1011010101 : -(bit[1]) _ as instr) = - Some(Stswi(RS,RA,NB)) - -function clause execute (Stswi (RS, RA, NB)) = - { - (bit[64]) EA := 0; - if RA == 0 then EA := 0 else EA := GPR[RA]; - ([|31|]) r := 0; - r := RS - 1; - ([|32|]) size := if NB == 0 then 32 else NB; - MEMw_EA(EA,size); - (bit[256]) membuffer := [0 = 0,255 = 0; default=0]; - 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 else (); - membuffer[j..j + 7] := (GPR[r])[i .. i + 7]; - j := j + 8; - i := i + 8; - if i == 64 then i := 32 else () - }; - MEMw(EA,size) := membuffer[0 .. size * 8] - } - -union ast member (bit[5], bit[5], bit[5]) Stswx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1010010101 : -(bit[1]) _ as instr) = - Some(Stswx(RS,RA,RB)) - -function clause execute (Stswx (RS, RA, RB)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - ([|31|]) r := 0; - EA := b + GPR[RB]; - r := RS - 1; - i := 32; - ([|128|]) n_top := XER[57 .. 63]; - recalculate_dependency(()); - MEMw_EA(EA,n_top); - (bit[512]) membuffer := [0 = 0,511 = 0; default=0]; - j := 0; - foreach (n from n_top to 1 by 1 in dec) - { - if i == 32 then r := ([|32|]) (r + 1) mod 32 else (); - membuffer[j..j + 7] := (GPR[r])[i .. i + 7]; - i := i + 8; - j := j + 8; - if i == 64 then i := 32 else () - }; - if ~(n_top == 0) then MEMw(EA,n_top) := membuffer[0 .. n_top * 8] else () - } - -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) = - Some(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) = - Some(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) = - Some(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 { - (bit) 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) = - Some(Subf(RT,RA,RB,OE,Rc)) - -function clause execute (Subf (RT, RA, RB, OE, Rc)) = - let (t1, o1, _) = (~(GPR[RA]) +_s GPR[RB]) in - let (t2, o2, _) = (t1 +_s (bit) 1) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - GPR[RT] := temp; - if Rc - then { - (bit) 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[16]) Addic - -function clause decode (0b001100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) SI as instr) = - Some(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) = - Some(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 | XER.SO) - } - -union ast member (bit[5], bit[5], bit[16]) Subfic - -function clause decode (0b001000 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) SI as instr) = - Some(Subfic(RT,RA,SI)) - -function clause execute (Subfic (RT, RA, SI)) = - let (t1, o1, c1) = (~(GPR[RA]) +_s EXTS(SI)) in - let (t2, o2, c2) = (t1 +_s (bit) 1) in - { - (bit[64]) temp := t2; - GPR[RT] := temp; - CA := (c1 | c2) - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Addc - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b000001010 : -[Rc] as instr) = - Some(Addc(RT,RA,RB,OE,Rc)) - -function clause execute (Addc (RT, RA, RB, OE, Rc)) = - let (temp, overflow, carry) = (GPR[RA] +_s GPR[RB]) in - { - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Subfc - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b000001000 : -[Rc] as instr) = - Some(Subfc(RT,RA,RB,OE,Rc)) - -function clause execute (Subfc (RT, RA, RB, OE, Rc)) = - let (t1, o1, c1) = (~(GPR[RA]) +_s GPR[RB]) in - let (t2, o2, c2) = (t1 +_s (bit) 1) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - carry := (c1 | c2); - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Adde - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b010001010 : -[Rc] as instr) = - Some(Adde(RT,RA,RB,OE,Rc)) - -function clause execute (Adde (RT, RA, RB, OE, Rc)) = - let (t1, o1, c1) = (GPR[RA] +_s GPR[RB]) in - let (t2, o2, c2) = (t1 +_s (bit) CA) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - carry := (c1 | c2); - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Subfe - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b010001000 : -[Rc] as instr) = - Some(Subfe(RT,RA,RB,OE,Rc)) - -function clause execute (Subfe (RT, RA, RB, OE, Rc)) = - let (t1, o1, c1) = (~(GPR[RA]) +_s GPR[RB]) in - let (t2, o2, c2) = (t1 +_s (bit) CA) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - carry := (c1 | c2); - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit, bit) Addme - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) _ : -[OE] : -0b011101010 : -[Rc] as instr) = - Some(Addme(RT,RA,OE,Rc)) - -function clause execute (Addme (RT, RA, OE, Rc)) = - let (t1, o1, c1) = (GPR[RA] +_s CA) in - let (t2, o2, c2) = (t1 +_s 0b1111111111111111111111111111111111111111111111111111111111111111) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - carry := (c1 | c2); - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit, bit) Subfme - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) _ : -[OE] : -0b011101000 : -[Rc] as instr) = - Some(Subfme(RT,RA,OE,Rc)) - -function clause execute (Subfme (RT, RA, OE, Rc)) = - let (t1, o1, c1) = (~(GPR[RA]) +_s CA) in - let (t2, o2, c2) = (t1 +_s 0b1111111111111111111111111111111111111111111111111111111111111111) in - { - (bit[64]) temp := t2; - overflow := (o1 | o2); - carry := (c1 | c2); - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit, bit) Addze - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) _ : -[OE] : -0b011001010 : -[Rc] as instr) = - Some(Addze(RT,RA,OE,Rc)) - -function clause execute (Addze (RT, RA, OE, Rc)) = - let (temp, overflow, carry) = (GPR[RA] +_s CA) in - { - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit, bit) Subfze - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) _ : -[OE] : -0b011001000 : -[Rc] as instr) = - Some(Subfze(RT,RA,OE,Rc)) - -function clause execute (Subfze (RT, RA, OE, Rc)) = - let (temp, overflow, carry) = (~(GPR[RA]) +_s CA) in - { - GPR[RT] := temp; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(temp,xer_so) - } - else (); - CA := carry; - if OE then set_SO_OV(overflow) else () - } - -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) = - Some(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 (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[16]) Mulli - -function clause decode (0b000111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[16]) SI as instr) = - Some(Mulli(RT,RA,SI)) - -function clause execute (Mulli (RT, RA, SI)) = - { - (bit[128]) prod := GPR[RA] *_s EXTS(SI); - GPR[RT] := prod[64 .. 127] - } - -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) = - Some(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 { - (bit) 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[5], bit[5], bit[5], bit) Mulhw - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[1]) _ : -0b001001011 : -[Rc] as instr) = - Some(Mulhw(RT,RA,RB,Rc)) - -function clause execute (Mulhw (RT, RA, RB, Rc)) = - { - (bit[64]) prod := 0; - (bit) overflow := 0; - let (p, o, _) = ((GPR[RA])[32 .. 63] *_s (GPR[RB])[32 .. 63]) in - { - prod := p; - overflow := o - }; - (GPR[RT])[32..63] := prod[0 .. 31]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if mode64bit - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(prod,xer_so) - } - else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Mulhwu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[1]) _ : -0b000001011 : -[Rc] as instr) = - Some(Mulhwu(RT,RA,RB,Rc)) - -function clause execute (Mulhwu (RT, RA, RB, Rc)) = - { - (bit[64]) prod := (GPR[RA])[32 .. 63] * (GPR[RB])[32 .. 63]; - (GPR[RT])[32..63] := prod[0 .. 31]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if mode64bit - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(prod,xer_so) - } - else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divw - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111101011 : -[Rc] as instr) = - Some(Divw(RT,RA,RB,OE,Rc)) - -function clause execute (Divw (RT, RA, RB, OE, Rc)) = - { - (bit[32]) dividend := (GPR[RA])[32 .. 63]; - (bit[32]) divisor := (GPR[RB])[32 .. 63]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot_s divisor) in - { - divided[32..63] := d; - overflow := o - }; - (GPR[RT])[32..63] := divided[32 .. 63]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if mode64bit | overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided,xer_so) - } - else (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divwu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111001011 : -[Rc] as instr) = - Some(Divwu(RT,RA,RB,OE,Rc)) - -function clause execute (Divwu (RT, RA, RB, OE, Rc)) = - { - (bit[32]) dividend := (GPR[RA])[32 .. 63]; - (bit[32]) divisor := (GPR[RB])[32 .. 63]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot divisor) in - { - divided[32..63] := d; - overflow := o - }; - (GPR[RT])[32..63] := divided[32 .. 63]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if mode64bit | overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided,xer_so) - } - else (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divwe - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110101011 : -[Rc] as instr) = - Some(Divwe(RT,RA,RB,OE,Rc)) - -function clause execute (Divwe (RT, RA, RB, OE, Rc)) = - { - (bit[64]) dividend := (GPR[RA])[32 .. 63] : 0b00000000000000000000000000000000; - (bit[32]) divisor := (GPR[RB])[32 .. 63]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot_s divisor) in - { - divided[32..63] := d[32 .. 63]; - overflow := o - }; - (GPR[RT])[32..63] := divided[32 .. 63]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if mode64bit | overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided,xer_so) - } - else (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divweu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110001011 : -[Rc] as instr) = - Some(Divweu(RT,RA,RB,OE,Rc)) - -function clause execute (Divweu (RT, RA, RB, OE, Rc)) = - { - (bit[64]) dividend := (GPR[RA])[32 .. 63] : 0b00000000000000000000000000000000; - (bit[32]) divisor := (GPR[RB])[32 .. 63]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot divisor) in - { - divided[32..63] := d[32 .. 63]; - overflow := o - }; - (GPR[RT])[32..63] := divided[32 .. 63]; - (GPR[RT])[0..31] := undefined; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if mode64bit | overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided,xer_so) - } - else (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Mulld - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b011101001 : -[Rc] as instr) = - Some(Mulld(RT,RA,RB,OE,Rc)) - -function clause execute (Mulld (RT, RA, RB, OE, Rc)) = - { - (bit[128]) prod := 0; - (bit) overflow := 0; - let (p, o, _) = (GPR[RA] *_s GPR[RB]) in - { - prod := p; - overflow := o - }; - GPR[RT] := prod[64 .. 127]; - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - set_overflow_cr0(prod[64 .. 127],xer_so) - } - else (); - if OE then set_SO_OV(overflow) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Mulhd - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[1]) _ : -0b001001001 : -[Rc] as instr) = - Some(Mulhd(RT,RA,RB,Rc)) - -function clause execute (Mulhd (RT, RA, RB, Rc)) = - { - (bit[128]) prod := GPR[RA] *_s GPR[RB]; - GPR[RT] := prod[0 .. 63]; - if Rc then set_overflow_cr0(prod[0 .. 63],XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Mulhdu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[1]) _ : -0b000001001 : -[Rc] as instr) = - Some(Mulhdu(RT,RA,RB,Rc)) - -function clause execute (Mulhdu (RT, RA, RB, Rc)) = - { - (bit[128]) prod := GPR[RA] * GPR[RB]; - GPR[RT] := prod[0 .. 63]; - if Rc then set_overflow_cr0(prod[0 .. 63],XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divd - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111101001 : -[Rc] as instr) = - Some(Divd(RT,RA,RB,OE,Rc)) - -function clause execute (Divd (RT, RA, RB, OE, Rc)) = - { - (bit[64]) dividend := GPR[RA]; - (bit[64]) divisor := GPR[RB]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot_s divisor) in - { - divided := d; - overflow := o - }; - GPR[RT] := divided; - if OE then set_SO_OV(overflow) else (); - if Rc then set_overflow_cr0(divided,overflow | XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divdu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111001001 : -[Rc] as instr) = - Some(Divdu(RT,RA,RB,OE,Rc)) - -function clause execute (Divdu (RT, RA, RB, OE, Rc)) = - { - (bit[64]) dividend := GPR[RA]; - (bit[64]) divisor := GPR[RB]; - (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit) overflow := 0; - let (d, o, _) = (dividend quot divisor) in - { - divided := d; - overflow := o - }; - GPR[RT] := divided; - if OE then set_SO_OV(overflow) else (); - if Rc then set_overflow_cr0(divided,overflow | XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divde - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110101001 : -[Rc] as instr) = - Some(Divde(RT,RA,RB,OE,Rc)) - -function clause execute (Divde (RT, RA, RB, OE, Rc)) = - { - (bit[128]) dividend := - GPR[RA] : 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) divisor := GPR[RB]; - (bit[128]) divided := 0; - (bit) overflow := 0; - let (d, o, _) = (dividend quot_s divisor) in - { - divided := d; - overflow := o - }; - GPR[RT] := divided[64 .. 127]; - if OE then set_SO_OV(overflow) else (); - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided[64 .. 127],xer_so) - } - else () - } - -union ast member (bit[5], bit[5], bit[5], bit, bit) Divdeu - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110001001 : -[Rc] as instr) = - Some(Divdeu(RT,RA,RB,OE,Rc)) - -function clause execute (Divdeu (RT, RA, RB, OE, Rc)) = - { - (bit[128]) dividend := - GPR[RA] : 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) divisor := GPR[RB]; - (bit[128]) divided := 0; - (bit) overflow := 0; - let (d, o, _) = (dividend quot divisor) in - { - divided := d; - overflow := o - }; - GPR[RT] := divided[64 .. 127]; - if OE then set_SO_OV(overflow) else (); - if Rc - then { - (bit) xer_so := XER.SO; - if OE & overflow then xer_so := overflow else (); - if overflow - then CR.CR0 := [undefined,undefined,undefined,xer_so] - else set_overflow_cr0(divided[64 .. 127],xer_so) - } - 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) = - Some(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) = - Some(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[3], bit, bit[5], bit[16]) Cmpli - -function clause decode (0b001010 : -(bit[3]) BF : -(bit[1]) _ : -[L] : -(bit[5]) RA : -(bit[16]) UI as instr) = - Some(Cmpli(BF,L,RA,UI)) - -function clause execute (Cmpli (BF, L, RA, UI)) = - { - (bit[64]) a := 0; - (bit[3]) c := 0; - if L == 0 then a := 0b00000000000000000000000000000000 : (GPR[RA])[32 .. 63] else a := GPR[RA]; - if a <_u 0b000000000000000000000000000000000000000000000000 : UI - then c := 0b100 - else if a >_u 0b000000000000000000000000000000000000000000000000 : UI - 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]) Cmpl - -function clause decode (0b011111 : -(bit[3]) BF : -(bit[1]) _ : -[L] : -(bit[5]) RA : -(bit[5]) RB : -0b0000100000 : -(bit[1]) _ as instr) = - Some(Cmpl(BF,L,RA,RB)) - -function clause execute (Cmpl (BF, L, RA, RB)) = - { - (bit[64]) a := 0; - (bit[64]) b := 0; - (bit[3]) c := 0; - if L == 0 - then { - a := 0b00000000000000000000000000000000 : (GPR[RA])[32 .. 63]; - b := 0b00000000000000000000000000000000 : (GPR[RB])[32 .. 63] - } - else { - a := GPR[RA]; - b := GPR[RB] - }; - if a <_u b then c := 0b100 else if a >_u 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[5], bit[5]) Isel - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[5]) BC : -0b01111 : -(bit[1]) _ as instr) = - Some(Isel(RT,RA,RB,BC)) - -function clause execute (Isel (RT, RA, RB, BC)) = - { - (bit[64]) a := 0; - if RA == 0 then a := 0 else a := GPR[RA]; - if CR[BC + 32] == 1 - then { - GPR[RT] := a; - discard := GPR[RB] - } - else GPR[RT] := GPR[RB] - } - -union ast member (bit[5], bit[5], bit[16]) Andi - -function clause decode (0b011100 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) UI as instr) = - Some(Andi(RS,RA,UI)) - -function clause execute (Andi (RS, RA, UI)) = - { - (bit[64]) temp := (GPR[RS] & 0b000000000000000000000000000000000000000000000000 : UI); - GPR[RA] := temp; - set_overflow_cr0(temp,XER.SO) - } - -union ast member (bit[5], bit[5], bit[16]) Andis - -function clause decode (0b011101 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) UI as instr) = - Some(Andis(RS,RA,UI)) - -function clause execute (Andis (RS, RA, UI)) = - { - (bit[64]) temp := (GPR[RS] & 0b00000000000000000000000000000000 : UI : 0b0000000000000000); - GPR[RA] := temp; - set_overflow_cr0(temp,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) = - Some(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) = - Some(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) = - Some(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[16]) Xoris - -function clause decode (0b011011 : -(bit[5]) RS : -(bit[5]) RA : -(bit[16]) UI as instr) = - Some(Xoris(RS,RA,UI)) - -function clause execute (Xoris (RS, RA, UI)) = - GPR[RA] := GPR[RS] ^ 0b00000000000000000000000000000000 : UI : 0b0000000000000000 - -union ast member (bit[5], bit[5], bit[5], bit) And - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0000011100 : -[Rc] as instr) = - Some(And(RS,RA,RB,Rc)) - -function clause execute (And (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[5], bit) Xor - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0100111100 : -[Rc] as instr) = - Some(Xor(RS,RA,RB,Rc)) - -function clause execute (Xor (RS, RA, RB, Rc)) = - { - (bit[64]) temp := 0; - if RS == RB - then { - temp := GPR[RS]; - temp := 0; - GPR[RA] := 0 - } - else { - 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[5], bit) Nand - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0111011100 : -[Rc] as instr) = - Some(Nand(RS,RA,RB,Rc)) - -function clause execute (Nand (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[5], bit) Or - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0110111100 : -[Rc] as instr) = - Some(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[5], bit) Nor - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0001111100 : -[Rc] as instr) = - Some(Nor(RS,RA,RB,Rc)) - -function clause execute (Nor (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[5], bit) Eqv - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0100011100 : -[Rc] as instr) = - Some(Eqv(RS,RA,RB,Rc)) - -function clause execute (Eqv (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[5], bit) Andc - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0000111100 : -[Rc] as instr) = - Some(Andc(RS,RA,RB,Rc)) - -function clause execute (Andc (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[5], bit) Orc - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0110011100 : -[Rc] as instr) = - Some(Orc(RS,RA,RB,Rc)) - -function clause execute (Orc (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) Extsb - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b1110111010 : -[Rc] as instr) = - Some(Extsb(RS,RA,Rc)) - -function clause execute (Extsb (RS, RA, Rc)) = - { - (bit[64]) temp := 0; - s := (GPR[RS])[56]; - temp[56..63] := (GPR[RS])[56 .. 63]; - (GPR[RA])[56..63] := temp[56 .. 63]; - temp[0..55] := s ^^ 56; - (GPR[RA])[0..55] := temp[0 .. 55]; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit) Extsh - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b1110011010 : -[Rc] as instr) = - Some(Extsh(RS,RA,Rc)) - -function clause execute (Extsh (RS, RA, Rc)) = - { - (bit[64]) temp := 0; - s := (GPR[RS])[48]; - temp[48..63] := (GPR[RS])[48 .. 63]; - (GPR[RA])[48..63] := temp[48 .. 63]; - temp[0..47] := s ^^ 48; - (GPR[RA])[0..47] := temp[0 .. 47]; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit) Cntlzw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0000011010 : -[Rc] as instr) = - Some(Cntlzw(RS,RA,Rc)) - -function clause execute (Cntlzw (RS, RA, Rc)) = - { - temp := (bit[64]) (countLeadingZeroes(GPR[RS],32)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5]) Cmpb - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0111111100 : -(bit[1]) _ as instr) = - Some(Cmpb(RS,RA,RB)) - -function clause execute (Cmpb (RS, RA, RB)) = - foreach (n from 0 to 7 by 1 in inc) - if (GPR[RS])[8 * n .. 8 * n + 7] == (GPR[RB])[8 * n .. 8 * n + 7] - then (GPR[RA])[8 * n..8 * n + 7] := 0b11111111 - else (GPR[RA])[8 * n..8 * n + 7] := (bit[8]) 0 - -union ast member (bit[5], bit[5]) Popcntb - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0001111010 : -(bit[1]) _ as instr) = - Some(Popcntb(RS,RA)) - -function clause execute (Popcntb (RS, RA)) = - foreach (i from 0 to 7 by 1 in inc) - { - ([|64|]) n := 0; - foreach (j from 0 to 7 by 1 in inc) if (GPR[RS])[i * 8 + j] == 1 then n := n + 1 else (); - (GPR[RA])[i * 8..i * 8 + 7] := (bit[8]) n - } - -union ast member (bit[5], bit[5]) Popcntw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0101111010 : -(bit[1]) _ as instr) = - Some(Popcntw(RS,RA)) - -function clause execute (Popcntw (RS, RA)) = - foreach (i from 0 to 1 by 1 in inc) - { - ([|64|]) n := 0; - foreach (j from 0 to 31 by 1 in inc) if (GPR[RS])[i * 32 + j] == 1 then n := n + 1 else (); - (GPR[RA])[i * 32..i * 32 + 31] := (bit[32]) n - } - -union ast member (bit[5], bit[5]) Prtyd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0010111010 : -(bit[1]) _ as instr) = - Some(Prtyd(RS,RA)) - -function clause execute (Prtyd (RS, RA)) = - { - s := 0; - foreach (i from 0 to 7 by 1 in inc) s := s ^ (GPR[RS])[i * 8 + 7]; - GPR[RA] := 0b000000000000000000000000000000000000000000000000000000000000000 : [s] - } - -union ast member (bit[5], bit[5]) Prtyw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0010011010 : -(bit[1]) _ as instr) = - Some(Prtyw(RS,RA)) - -function clause execute (Prtyw (RS, RA)) = - { - s := 0; - t := 0; - foreach (i from 0 to 3 by 1 in inc) s := s ^ (GPR[RS])[i * 8 + 7]; - foreach (i from 4 to 7 by 1 in inc) t := t ^ (GPR[RS])[i * 8 + 7]; - (GPR[RA])[0..31] := 0b0000000000000000000000000000000 : [s]; - (GPR[RA])[32..63] := 0b0000000000000000000000000000000 : [t] - } - -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) = - Some(Extsw(RS,RA,Rc)) - -function clause execute (Extsw (RS, RA, Rc)) = - { - s := (GPR[RS])[32]; - (bit[64]) temp := 0; - temp[32..63] := (GPR[RS])[32 .. 63]; - temp[0..31] := s ^^ 32; - if Rc then set_overflow_cr0(temp,XER.SO) else (); - GPR[RA] := temp - } - -union ast member (bit[5], bit[5], bit) Cntlzd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0000111010 : -[Rc] as instr) = - Some(Cntlzd(RS,RA,Rc)) - -function clause execute (Cntlzd (RS, RA, Rc)) = - { - temp := (bit[64]) (countLeadingZeroes(GPR[RS],0)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5]) Popcntd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0111111010 : -(bit[1]) _ as instr) = - Some(Popcntd(RS,RA)) - -function clause execute (Popcntd (RS, RA)) = - { - ([|64|]) n := 0; - foreach (i from 0 to 63 by 1 in inc) if (GPR[RS])[i] == 1 then n := n + 1 else (); - GPR[RA] := (bit[64]) n - } - -union ast member (bit[5], bit[5], bit[5]) Bpermd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0011111100 : -(bit[1]) _ as instr) = - Some(Bpermd(RS,RA,RB)) - -function clause execute (Bpermd (RS, RA, RB)) = - { - (bit[8]) perm := 0; - foreach (i from 0 to 7 by 1 in inc) - { - index := (GPR[RS])[8 * i .. 8 * i + 7]; - if index <_u (bit[8]) 64 - then perm[i] := (GPR[RB])[index] - else { - perm[i] := 0; - discard := GPR[RB] - } - }; - GPR[RA] := 0b00000000000000000000000000000000000000000000000000000000 : perm[0 .. 7] - } - -union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwinm - -function clause decode (0b010101 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) SH : -(bit[5]) MB : -(bit[5]) ME : -[Rc] as instr) = - Some(Rlwinm(RS,RA,SH,MB,ME,Rc)) - -function clause execute (Rlwinm (RS, RA, SH, MB, ME, Rc)) = - { - n := SH; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n); - m := MASK(MB + 32,ME + 32); - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwnm - -function clause decode (0b010111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -(bit[5]) MB : -(bit[5]) ME : -[Rc] as instr) = - Some(Rlwnm(RS,RA,RB,MB,ME,Rc)) - -function clause execute (Rlwnm (RS, RA, RB, MB, ME, Rc)) = - { - n := (GPR[RB])[59 .. 63]; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n); - m := MASK(MB + 32,ME + 32); - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwimi - -function clause decode (0b010100 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) SH : -(bit[5]) MB : -(bit[5]) ME : -[Rc] as instr) = - Some(Rlwimi(RS,RA,SH,MB,ME,Rc)) - -function clause execute (Rlwimi (RS, RA, SH, MB, ME, Rc)) = - { - n := SH; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n); - m := MASK(MB + 32,ME + 32); - (bit[64]) temp := (r & m | GPR[RA] & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicl - -function clause decode (0b011110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -(bit[6]) mb : -0b000 : -(bit[1]) _ : -[Rc] as instr) = - Some(Rldicl(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc)) - -function clause execute (Rldicl (RS, RA, sh, mb, Rc)) = - { - n := [sh[5]] : sh[0 .. 4]; - r := ROTL(GPR[RS],n); - b := [mb[5]] : mb[0 .. 4]; - m := MASK(b,63); - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -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) = - Some(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[5], bit[6], bit[6], bit) Rldic - -function clause decode (0b011110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -(bit[6]) mb : -0b010 : -(bit[1]) _ : -[Rc] as instr) = - Some(Rldic(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc)) - -function clause execute (Rldic (RS, RA, sh, mb, Rc)) = - { - n := [sh[5]] : sh[0 .. 4]; - r := ROTL(GPR[RS],n); - b := [mb[5]] : mb[0 .. 4]; - m := MASK(b,(bit[6]) (~(n))); - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit[6], bit) Rldcl - -function clause decode (0b011110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -(bit[6]) mb : -0b1000 : -[Rc] as instr) = - Some(Rldcl(RS,RA,RB,mb,Rc)) - -function clause execute (Rldcl (RS, RA, RB, mb, Rc)) = - { - n := (GPR[RB])[58 .. 63]; - r := ROTL(GPR[RS],n); - b := [mb[5]] : mb[0 .. 4]; - m := MASK(b,63); - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit[6], bit) Rldcr - -function clause decode (0b011110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -(bit[6]) me : -0b1001 : -[Rc] as instr) = - Some(Rldcr(RS,RA,RB,me,Rc)) - -function clause execute (Rldcr (RS, RA, RB, me, Rc)) = - { - n := (GPR[RB])[58 .. 63]; - 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[5], bit[6], bit[6], bit) Rldimi - -function clause decode (0b011110 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -(bit[6]) mb : -0b011 : -(bit[1]) _ : -[Rc] as instr) = - Some(Rldimi(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc)) - -function clause execute (Rldimi (RS, RA, sh, mb, Rc)) = - { - n := [sh[5]] : sh[0 .. 4]; - r := ROTL(GPR[RS],n); - b := [mb[5]] : mb[0 .. 4]; - m := MASK(b,(bit[6]) (~(n))); - (bit[64]) temp := (r & m | GPR[RA] & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Slw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0000011000 : -[Rc] as instr) = - Some(Slw(RS,RA,RB,Rc)) - -function clause execute (Slw (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[59 .. 63]; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n); - if (GPR[RB])[58] == 0 - then m := MASK(32,63 - n) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Srw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1000011000 : -[Rc] as instr) = - Some(Srw(RS,RA,RB,Rc)) - -function clause execute (Srw (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[59 .. 63]; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n); - if (GPR[RB])[58] == 0 - then m := MASK(n + 32,63) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Srawi - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) SH : -0b1100111000 : -[Rc] as instr) = - Some(Srawi(RS,RA,SH,Rc)) - -function clause execute (Srawi (RS, RA, SH, Rc)) = - { - n := SH; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n); - m := MASK(n + 32,63); - s := (GPR[RS])[32]; - (bit[64]) temp := (r & m | s ^^ 64 & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else (); - XER.CA := if n >_u (bit[5]) 0 then s & ~((r & ~(m)) == 0) else 0 - } - -union ast member (bit[5], bit[5], bit[5], bit) Sraw - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1100011000 : -[Rc] as instr) = - Some(Sraw(RS,RA,RB,Rc)) - -function clause execute (Sraw (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[59 .. 63]; - r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n); - if (GPR[RB])[58] == 0 - then m := MASK(n + 32,63) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - s := (GPR[RS])[32]; - (bit[64]) temp := (r & m | s ^^ 64 & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else (); - XER.CA := if n >_u (bit[5]) 0 then s & ~((r & ~(m)) == 0) else 0 - } - -union ast member (bit[5], bit[5], bit[5], bit) Sld - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0000011011 : -[Rc] as instr) = - Some(Sld(RS,RA,RB,Rc)) - -function clause execute (Sld (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[58 .. 63]; - r := ROTL(GPR[RS],n); - if (GPR[RB])[57] == 0 - then m := MASK(0,63 - n) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[5], bit) Srd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1000011011 : -[Rc] as instr) = - Some(Srd(RS,RA,RB,Rc)) - -function clause execute (Srd (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[58 .. 63]; - r := ROTL(GPR[RS],64 - n); - if (GPR[RB])[57] == 0 - then m := MASK(n,63) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - (bit[64]) temp := (r & m); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else () - } - -union ast member (bit[5], bit[5], bit[6], bit) Sradi - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b110011101 : -(bit[1]) _ : -[Rc] as instr) = - Some(Sradi(RS,RA,instr[16 .. 20] : instr[30 .. 30],Rc)) - -function clause execute (Sradi (RS, RA, sh, Rc)) = - { - n := [sh[5]] : sh[0 .. 4]; - r := ROTL(GPR[RS],64 - n); - m := MASK(n,63); - s := (GPR[RS])[0]; - (bit[64]) temp := (r & m | s ^^ 64 & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else (); - XER.CA := if n >_u (bit[6]) 0 then s & ~((r & ~(m)) == 0) else 0 - } - -union ast member (bit[5], bit[5], bit[5], bit) Srad - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1100011010 : -[Rc] as instr) = - Some(Srad(RS,RA,RB,Rc)) - -function clause execute (Srad (RS, RA, RB, Rc)) = - { - n := (GPR[RB])[58 .. 63]; - r := ROTL(GPR[RS],64 - n); - if (GPR[RB])[57] == 0 - then m := MASK(n,63) - else m := 0b0000000000000000000000000000000000000000000000000000000000000000; - s := (GPR[RS])[0]; - (bit[64]) temp := (r & m | s ^^ 64 & ~(m)); - GPR[RA] := temp; - if Rc then set_overflow_cr0(temp,XER.SO) else (); - XER.CA := if n >_u (bit[6]) 0 then s & ~((r & ~(m)) == 0) else 0 - } - -union ast member (bit[5], bit[5]) Cdtbcd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0100011010 : -(bit[1]) _ as instr) = - Some(Cdtbcd(RS,RA)) - -function clause execute (Cdtbcd (RS, RA)) = - foreach (i from 0 to 1 by 1 in inc) - { - n := i * 32; - (GPR[RA])[n + 0..n + 7] := (bit[8]) 0; - (GPR[RA])[n + 8..n + 19] := DEC_TO_BCD((GPR[RS])[n + 12 .. n + 21]); - (GPR[RA])[n + 20..n + 31] := DEC_TO_BCD((GPR[RS])[n + 22 .. n + 31]) - } - -union ast member (bit[5], bit[5]) Cbcdtd - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) _ : -0b0100111010 : -(bit[1]) _ as instr) = - Some(Cbcdtd(RS,RA)) - -function clause execute (Cbcdtd (RS, RA)) = - foreach (i from 0 to 1 by 1 in inc) - { - n := i * 32; - (GPR[RA])[n + 0..n + 11] := (bit[12]) 0; - (GPR[RA])[n + 12..n + 21] := BCD_TO_DEC((GPR[RS])[n + 8 .. n + 19]); - (GPR[RA])[n + 22..n + 31] := BCD_TO_DEC((GPR[RS])[n + 20 .. n + 31]) - } - -union ast member (bit[5], bit[5], bit[5]) Addg6s - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -(bit[1]) _ : -0b001001010 : -(bit[1]) _ as instr) = - Some(Addg6s(RT,RA,RB)) - -function clause execute (Addg6s (RT, RA, RB)) = - { - (bit[16]) dc := 0; - foreach (i from 0 to 15 by 1 in inc) - let (v, _, co) = ((GPR[RA])[4 * i .. 63] + (GPR[RB])[4 * i .. 63]) in dc[i] := carry_out(v,co); - c := - (dc[0] ^^ 4) : - (dc[1] ^^ 4) : - (dc[2] ^^ 4) : - (dc[3] ^^ 4) : - (dc[4] ^^ 4) : - (dc[5] ^^ 4) : - (dc[6] ^^ 4) : - (dc[7] ^^ 4) : - (dc[8] ^^ 4) : - (dc[9] ^^ 4) : - (dc[10] ^^ 4) : - (dc[11] ^^ 4) : - (dc[12] ^^ 4) : (dc[13] ^^ 4) : (dc[14] ^^ 4) : (dc[15] ^^ 4); - GPR[RT] := (~(c) & 0b0110011001100110011001100110011001100110011001100110011001100110) - } - -union ast member (bit[5], bit[10]) Mtspr - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[10]) spr : -0b0111010011 : -(bit[1]) _ as instr) = - Some(Mtspr(RS,spr)) - -function clause execute (Mtspr (RS, spr)) = - { - n := spr[5 .. 9] : spr[0 .. 4]; - if n == 13 - then trap(()) - else if n == 1 - then { - (bit[64]) reg := GPR[RS]; - (bit[32]) front := zero_or_undef(reg[0 .. 31]); - (bit) xer_so := reg[32]; - (bit) xer_ov := reg[33]; - (bit) xer_ca := reg[34]; - (bit[22]) mid := zero_or_undef(reg[35 .. 56]); - (bit[7]) bot := reg[57 .. 63]; - XER := front : [xer_so] : [xer_ov] : [xer_ca] : mid : bot - } - else if length(SPR[n]) == 64 - then SPR[n] := GPR[RS] - else if n == 152 then CTRL := (GPR[RS])[32 .. 63] else () - } - -union ast member (bit[5], bit[10]) Mfspr - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[10]) spr : -0b0101010011 : -(bit[1]) _ as instr) = - Some(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) = - Some(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) = - Some(Mfcr(RT)) - -function clause execute (Mfcr (RT)) = GPR[RT] := 0b00000000000000000000000000000000 : CR - -union ast member (bit[5], bit[8]) Mtocrf - -function clause decode (0b011111 : -(bit[5]) RS : -0b1 : -(bit[8]) FXM : -(bit[1]) _ : -0b0010010000 : -(bit[1]) _ as instr) = - Some(Mtocrf(RS,FXM)) - -function clause execute (Mtocrf (RS, FXM)) = - { - ([|7|]) n := 0; - count := 0; - foreach (i from 0 to 7 by 1 in inc) - if FXM[i] == 1 - then { - n := i; - count := count + 1 - } - else (); - if count == 1 - then CR[4 * n + 32..4 * n + 35] := (GPR[RS])[4 * n + 32 .. 4 * n + 35] - else CR := undefined - } - -union ast member (bit[5], bit[8]) Mfocrf - -function clause decode (0b011111 : -(bit[5]) RT : -0b1 : -(bit[8]) FXM : -(bit[1]) _ : -0b0000010011 : -(bit[1]) _ as instr) = - Some(Mfocrf(RT,FXM)) - -function clause execute (Mfocrf (RT, FXM)) = - { - ([|7|]) n := 0; - count := 0; - foreach (i from 0 to 7 by 1 in inc) - if FXM[i] == 1 - then { - n := i; - count := count + 1 - } - else (); - if count == 1 - then { - (bit[64]) temp := undefined; - temp[4 * n + 32..4 * n + 35] := CR[4 * n + 32 .. 4 * n + 35]; - GPR[RT] := temp - } - else GPR[RT] := undefined - } - -union ast member (bit[3]) Mcrxr - -function clause decode (0b011111 : -(bit[3]) BF : -(bit[2]) _ : -(bit[5]) _ : -(bit[5]) _ : -0b1000000000 : -(bit[1]) _ as instr) = - Some(Mcrxr(BF)) - -function clause execute (Mcrxr (BF)) = - { - CR[4 * BF + 32..4 * BF + 35] := XER[32 .. 35]; - XER[32..35] := 0b0000 - } - -union ast member (bit[5], bit[5], bit[5], bit) Dlmzb - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0001001110 : -[Rc] as instr) = - Some(Dlmzb(RS,RA,RB,Rc)) - -function clause execute (Dlmzb (RS, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Macchw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b010101100 : -[Rc] as instr) = - Some(Macchw(RT,RA,RB,OE,Rc)) - -function clause execute (Macchw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Macchws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b011101100 : -[Rc] as instr) = - Some(Macchws(RT,RA,RB,OE,Rc)) - -function clause execute (Macchws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Macchwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b010001100 : -[Rc] as instr) = - Some(Macchwu(RT,RA,RB,OE,Rc)) - -function clause execute (Macchwu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Macchwsu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b011001100 : -[Rc] as instr) = - Some(Macchwsu(RT,RA,RB,OE,Rc)) - -function clause execute (Macchwsu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Machhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b000101100 : -[Rc] as instr) = - Some(Machhw(RT,RA,RB,OE,Rc)) - -function clause execute (Machhw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Machhws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b001101100 : -[Rc] as instr) = - Some(Machhws(RT,RA,RB,OE,Rc)) - -function clause execute (Machhws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Machhwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b000001100 : -[Rc] as instr) = - Some(Machhwu(RT,RA,RB,OE,Rc)) - -function clause execute (Machhwu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Machhwsu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b001001100 : -[Rc] as instr) = - Some(Machhwsu(RT,RA,RB,OE,Rc)) - -function clause execute (Machhwsu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110101100 : -[Rc] as instr) = - Some(Maclhw(RT,RA,RB,OE,Rc)) - -function clause execute (Maclhw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111101100 : -[Rc] as instr) = - Some(Maclhws(RT,RA,RB,OE,Rc)) - -function clause execute (Maclhws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110001100 : -[Rc] as instr) = - Some(Maclhwu(RT,RA,RB,OE,Rc)) - -function clause execute (Maclhwu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhwsu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111001100 : -[Rc] as instr) = - Some(Maclhwsu(RT,RA,RB,OE,Rc)) - -function clause execute (Maclhwsu (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mulchw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0010101000 : -[Rc] as instr) = - Some(Mulchw(RT,RA,RB,Rc)) - -function clause execute (Mulchw (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mulchwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0010001000 : -[Rc] as instr) = - Some(Mulchwu(RT,RA,RB,Rc)) - -function clause execute (Mulchwu (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mulhhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000101000 : -[Rc] as instr) = - Some(Mulhhw(RT,RA,RB,Rc)) - -function clause execute (Mulhhw (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mulhhwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000001000 : -[Rc] as instr) = - Some(Mulhhwu(RT,RA,RB,Rc)) - -function clause execute (Mulhhwu (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mullhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0110101000 : -[Rc] as instr) = - Some(Mullhw(RT,RA,RB,Rc)) - -function clause execute (Mullhw (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit) Mullhwu - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0110001000 : -[Rc] as instr) = - Some(Mullhwu(RT,RA,RB,Rc)) - -function clause execute (Mullhwu (RT, RA, RB, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmacchw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b010101110 : -[Rc] as instr) = - Some(Nmacchw(RT,RA,RB,OE,Rc)) - -function clause execute (Nmacchw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmacchws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b011101110 : -[Rc] as instr) = - Some(Nmacchws(RT,RA,RB,OE,Rc)) - -function clause execute (Nmacchws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmachhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b000101110 : -[Rc] as instr) = - Some(Nmachhw(RT,RA,RB,OE,Rc)) - -function clause execute (Nmachhw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmachhws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b001101110 : -[Rc] as instr) = - Some(Nmachhws(RT,RA,RB,OE,Rc)) - -function clause execute (Nmachhws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmaclhw - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b110101110 : -[Rc] as instr) = - Some(Nmaclhw(RT,RA,RB,OE,Rc)) - -function clause execute (Nmaclhw (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5], bit[5], bit, bit) Nmaclhws - -function clause decode (0b000100 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -[OE] : -0b111101110 : -[Rc] as instr) = - Some(Nmaclhws(RT,RA,RB,OE,Rc)) - -function clause execute (Nmaclhws (RT, RA, RB, OE, Rc)) = () - -union ast member (bit[5], bit[5]) Icbi - -function clause decode (0b011111 : -(bit[5]) _ : -(bit[5]) RA : -(bit[5]) RB : -0b1111010110 : -(bit[1]) _ as instr) = - Some(Icbi(RA,RB)) - -function clause execute (Icbi (RA, RB)) = () - -union ast member (bit[4], bit[5], bit[5]) Icbt - -function clause decode (0b011111 : -(bit[1]) _ : -(bit[4]) CT : -(bit[5]) RA : -(bit[5]) RB : -0b0000010110 : -(bit[1]) _ as instr) = - Some(Icbt(CT,RA,RB)) - -function clause execute (Icbt (CT, RA, RB)) = () - -union ast member (bit[5], bit[5]) Dcba - -function clause decode (0b011111 : -(bit[5]) _ : -(bit[5]) RA : -(bit[5]) RB : -0b1011110110 : -(bit[1]) _ as instr) = - Some(Dcba(RA,RB)) - -function clause execute (Dcba (RA, RB)) = () - -union ast member (bit[5], bit[5], bit[5]) Dcbt - -function clause decode (0b011111 : -(bit[5]) TH : -(bit[5]) RA : -(bit[5]) RB : -0b0100010110 : -(bit[1]) _ as instr) = - Some(Dcbt(TH,RA,RB)) - -function clause execute (Dcbt (TH, RA, RB)) = () - -union ast member (bit[5], bit[5], bit[5]) Dcbtst - -function clause decode (0b011111 : -(bit[5]) TH : -(bit[5]) RA : -(bit[5]) RB : -0b0011110110 : -(bit[1]) _ as instr) = - Some(Dcbtst(TH,RA,RB)) - -function clause execute (Dcbtst (TH, RA, RB)) = () - -union ast member (bit[5], bit[5]) Dcbz - -function clause decode (0b011111 : -(bit[5]) _ : -(bit[5]) RA : -(bit[5]) RB : -0b1111110110 : -(bit[1]) _ as instr) = - Some(Dcbz(RA,RB)) - -function clause execute (Dcbz (RA, RB)) = () - -union ast member (bit[5], bit[5]) Dcbst - -function clause decode (0b011111 : -(bit[5]) _ : -(bit[5]) RA : -(bit[5]) RB : -0b0000110110 : -(bit[1]) _ as instr) = - Some(Dcbst(RA,RB)) - -function clause execute (Dcbst (RA, RB)) = () - -union ast member (bit[2], bit[5], bit[5]) Dcbf - -function clause decode (0b011111 : -(bit[3]) _ : -(bit[2]) L : -(bit[5]) RA : -(bit[5]) RB : -0b0001010110 : -(bit[1]) _ as instr) = - Some(Dcbf(L,RA,RB)) - -function clause execute (Dcbf (L, RA, RB)) = () - -union ast member Isync - -function clause decode (0b010011 : -(bit[5]) _ : -(bit[5]) _ : -(bit[5]) _ : -0b0010010110 : -(bit[1]) _ as instr) = - Some(Isync()) - -function clause execute Isync = I_Sync(()) - -union ast member (bit[5], bit[5], bit[5], bit) Lbarx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000110100 : -[EH] as instr) = - Some(Lbarx(RT,RA,RB,EH)) - -function clause execute (Lbarx (RT, RA, RB, EH)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr_reserve(EA,1) - } - -union ast member (bit[5], bit[5], bit[5], bit) Lharx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0001110100 : -[EH] as instr) = - Some(Lharx(RT,RA,RB,EH)) - -function clause execute (Lharx (RT, RA, RB, EH)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr_reserve(EA,2) - } - -union ast member (bit[5], bit[5], bit[5], bit) Lwarx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0000010100 : -[EH] as instr) = - Some(Lwarx(RT,RA,RB,EH)) - -function clause execute (Lwarx (RT, RA, RB, EH)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := 0b00000000000000000000000000000000 : MEMr_reserve(EA,4) - } - -union ast member (bit[5], bit[5], bit[5]) Stbcx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1010110110 : -0b1 as instr) = - Some(Stbcx(RS,RA,RB)) - -function clause execute (Stbcx (RS, 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_cond(EA,1); - status := MEMw_conditional(EA,1,(GPR[RS])[56 .. 63]); - CR0 := 0b00 : [status] : [XER.SO] - } - -union ast member (bit[5], bit[5], bit[5]) Sthcx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b1011010110 : -0b1 as instr) = - Some(Sthcx(RS,RA,RB)) - -function clause execute (Sthcx (RS, 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_cond(EA,2); - status := MEMw_conditional(EA,2,(GPR[RS])[48 .. 63]); - CR0 := 0b00 : [status] : [XER.SO] - } - -union ast member (bit[5], bit[5], bit[5]) Stwcx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0010010110 : -0b1 as instr) = - Some(Stwcx(RS,RA,RB)) - -function clause execute (Stwcx (RS, 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_cond(EA,4); - status := MEMw_conditional(EA,4,(GPR[RS])[32 .. 63]); - CR0 := 0b00 : [status] : [XER.SO] - } - -union ast member (bit[5], bit[5], bit[5], bit) Ldarx - -function clause decode (0b011111 : -(bit[5]) RT : -(bit[5]) RA : -(bit[5]) RB : -0b0001010100 : -[EH] as instr) = - Some(Ldarx(RT,RA,RB,EH)) - -function clause execute (Ldarx (RT, RA, RB, EH)) = - { - (bit[64]) b := 0; - (bit[64]) EA := 0; - if RA == 0 then b := 0 else b := GPR[RA]; - EA := b + GPR[RB]; - GPR[RT] := MEMr_reserve(EA,8) - } - -union ast member (bit[5], bit[5], bit[5]) Stdcx - -function clause decode (0b011111 : -(bit[5]) RS : -(bit[5]) RA : -(bit[5]) RB : -0b0011010110 : -0b1 as instr) = - Some(Stdcx(RS,RA,RB)) - -function clause execute (Stdcx (RS, 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_cond(EA,8); - status := MEMw_conditional(EA,8,GPR[RS]); - CR0 := 0b00 : [status] : [XER.SO] - } - -union ast member (bit[2]) Sync - -function clause decode (0b011111 : -(bit[3]) _ : -(bit[2]) L : -(bit[5]) _ : -(bit[5]) _ : -0b1001010110 : -(bit[1]) _ as instr) = - Some(Sync(L)) - -function clause execute (Sync (L)) = - switch L { case 0b00 -> { H_Sync(()) } case 0b01 -> { LW_Sync(()) } } - -union ast member Eieio - -function clause decode (0b011111 : -(bit[5]) _ : -(bit[5]) _ : -(bit[5]) _ : -0b1101010110 : -(bit[1]) _ as instr) = - Some(Eieio()) - -function clause execute Eieio = EIEIO_Sync(()) - -union ast member (bit[5]) Mbar - -function clause decode (0b011111 : -(bit[5]) MO : -(bit[5]) _ : -(bit[5]) _ : -0b1101010110 : -(bit[1]) _ as instr) = - Some(Mbar(MO)) - -function clause execute (Mbar (MO)) = () - -union ast member (bit[2]) Wait - -function clause decode (0b011111 : -(bit[3]) _ : -(bit[2]) WC : -(bit[5]) _ : -(bit[5]) _ : -0b0000111110 : -(bit[1]) _ as instr) = - Some(Wait(WC)) - -function clause execute (Wait (WC)) = () - - -typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction } - -function clause decode _ = None - -end decode -end execute -end ast - -val ast -> option<ast> effect pure supported_instructions -function option<ast> supported_instructions ((ast) instr) = { - switch instr { - case (Mbar(_)) -> None - case (Sync(0b10)) -> None - case (Sync(0b11)) -> None - case _ -> Some(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)*) -(*Floating point instructions*) -(* 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 -> option<ast> effect pure illegal_instructions -function option<ast> illegal_instructions instr = - if (illegal_instructions_pred (instr)) - then None else Some(instr) - -(* old fetch-decode-execute *) -(*function unit fde () = { - NIA := CIA + 4; - instr := decode(MEMr(CIA, 4)); - instr := supported_instructions(instr); - execute(instr); - CIA := NIA; -}*) |