val extern forall Nat 'n. bit['n] -> bit[64] effect pure EXTS (* XXX binary coded decimal *) function forall Type 'a . 'a DEC_TO_BCD ( x ) = x function forall Type 'a . 'a BCD_TO_DEC ( x ) = x (* XXX carry out *) function bit carry_out ( x ) = bitzero (* XXX length *) function nat length ( x ) = 64 (* 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 := 0; if(start > stop) then { mask[start .. 63] := bitone ^^ (64 - start); mask[0 .. stop] := bitone ^^ (stop + 1); } else { mask[start .. stop ] := bitone ^^ (stop - start + 1); }; mask; } 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; (* LT, GT, EQ, SO -- fixed-point *) 36 .. 39 : CR1; (* FX, FEX, VX, OX -- (decimal) floating-point *) 40 .. 43 : CR2; 44 .. 47 : CR3; 48 .. 51 : CR4; 52 .. 55 : CR5; 56 .. 59 : CR6; (* LT, GT, EQ, SO -- vector *) 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 (* Fixed-point registers *) register (bit[64]) GPR0 register (bit[64]) GPR1 register (bit[64]) GPR2 register (bit[64]) GPR3 register (bit[64]) GPR4 register (bit[64]) GPR5 register (bit[64]) GPR6 register (bit[64]) GPR7 register (bit[64]) GPR8 register (bit[64]) GPR9 register (bit[64]) GPR10 register (bit[64]) GPR11 register (bit[64]) GPR12 register (bit[64]) GPR13 register (bit[64]) GPR14 register (bit[64]) GPR15 register (bit[64]) GPR16 register (bit[64]) GPR17 register (bit[64]) GPR18 register (bit[64]) GPR19 register (bit[64]) GPR20 register (bit[64]) GPR21 register (bit[64]) GPR22 register (bit[64]) GPR23 register (bit[64]) GPR24 register (bit[64]) GPR25 register (bit[64]) GPR26 register (bit[64]) GPR27 register (bit[64]) GPR28 register (bit[64]) GPR29 register (bit[64]) GPR30 register (bit[64]) GPR31 let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = [ GPR0, GPR1, GPR2, GPR3, GPR4, GPR5, GPR6, GPR7, GPR8, GPR9, GPR10, GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 ] register (bit[32:63]) VRSAVE register (bit[64]) SPRG4 register (bit[64]) SPRG5 register (bit[64]) SPRG6 register (bit[64]) SPRG7 (* XXX bogus, length should be 1024 with many more values - cf. mfspr definition - eg. SPRG4 to SPRG7 are at offsets 260 to 263, VRSAVE is 256, etc. *) let (vector <0, 10, inc, (register<(bit[64])>) >) SPR = [ undefined, XER, undefined, undefined, undefined, undefined, undefined, undefined, LR, CTR ] (* XXX bogus, DCR might be numbered with 64-bit values! - and it's 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 (?) *) register (vector <0, 64, inc, bit>) DCR0 register (vector <0, 64, inc, bit>) DCR1 let (vector <0, 2, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR = [ DCR0, DCR1 ] (* Floating-point registers *) register (bit[64]) FPR0 register (bit[64]) FPR1 register (bit[64]) FPR2 register (bit[64]) FPR3 register (bit[64]) FPR4 register (bit[64]) FPR5 register (bit[64]) FPR6 register (bit[64]) FPR7 register (bit[64]) FPR8 register (bit[64]) FPR9 register (bit[64]) FPR10 register (bit[64]) FPR11 register (bit[64]) FPR12 register (bit[64]) FPR13 register (bit[64]) FPR14 register (bit[64]) FPR15 register (bit[64]) FPR16 register (bit[64]) FPR17 register (bit[64]) FPR18 register (bit[64]) FPR19 register (bit[64]) FPR20 register (bit[64]) FPR21 register (bit[64]) FPR22 register (bit[64]) FPR23 register (bit[64]) FPR24 register (bit[64]) FPR25 register (bit[64]) FPR26 register (bit[64]) FPR27 register (bit[64]) FPR28 register (bit[64]) FPR29 register (bit[64]) FPR30 register (bit[64]) FPR31 let (vector <0, 32, inc, (register<(bit[64])>) >) FPR = [ FPR0, FPR1, FPR2, FPR3, FPR4, FPR5, FPR6, FPR7, FPR8, FPR9, FPR10, FPR11, FPR12, FPR13, FPR14, FPR15, FPR16, FPR17, FPR18, FPR19, FPR20, FPR21, FPR22, FPR23, FPR24, FPR25, FPR26, FPR27, FPR28, FPR29, FPR30, FPR31 ] typedef fpscr = register bits [ 0 : 63 ] { 32 : FX; 33 : FEX; 34 : VX; 35 : OX; 36 : UX; 37 : ZX; 38 : XX; 39 : VXSNAN; 40 : VXISI; 41 : VXIDI; 42 : VXZDZ; 43 : VXIMZ; 44 : VXVC; 45 : FR; 46 : FI; 47 .. 51 : FPRF; 47 : C; 48 .. 51 : FPCC; (* the bits of FPCC are named FL, FG, FE and FU, but those names are never used in pseudo-code. *) 53 : VXSOFT; 54 : VXSQRT; 55 : VXCVI; 56 : VE; 57 : OE; 58 : UE; 59 : ZE; 60 : XE; 61 : NI; 62 .. 63 : RN; } register (fpscr) FPSCR (* XXX *) val extern bit[32] -> bit[64] effect pure DOUBLE val extern bit[64] -> bit[32] effect pure SINGLE (* Vector registers *) register (bit[128]) VR0 register (bit[128]) VR1 register (bit[128]) VR2 register (bit[128]) VR3 register (bit[128]) VR4 register (bit[128]) VR5 register (bit[128]) VR6 register (bit[128]) VR7 register (bit[128]) VR8 register (bit[128]) VR9 register (bit[128]) VR10 register (bit[128]) VR11 register (bit[128]) VR12 register (bit[128]) VR13 register (bit[128]) VR14 register (bit[128]) VR15 register (bit[128]) VR16 register (bit[128]) VR17 register (bit[128]) VR18 register (bit[128]) VR19 register (bit[128]) VR20 register (bit[128]) VR21 register (bit[128]) VR22 register (bit[128]) VR23 register (bit[128]) VR24 register (bit[128]) VR25 register (bit[128]) VR26 register (bit[128]) VR27 register (bit[128]) VR28 register (bit[128]) VR29 register (bit[128]) VR30 register (bit[128]) VR31 let (vector <0, 32, inc, (register<(bit[128])>) >) VR = [ VR0, VR1, VR2, VR3, VR4, VR5, VR6, VR7, VR8, VR9, VR10, VR11, VR12, VR13, VR14, VR15, VR16, VR17, VR18, VR19, VR20, VR21, VR22, VR23, VR24, VR25, VR26, VR27, VR28, VR29, VR30, VR31 ] typedef vscr = register bits [ 96 : 127 ] { 111 : NJ; 127 : SAT; } register (vscr) VSCR (* XXX extend with zeroes -- the resulting size in completely unknown and depends of context *) val extern forall Nat 'n, Nat 'm. bit['n] -> bit['m] effect pure EXTZ (* Chop has a very weird definition where the resulting size depends of context, but in practice it is used with the following definition everywhere, except in vaddcuw which probably needs to be patched accordingly. *) val forall Nat 'n, Nat 'm, 'm <= 'n. (bit['n], [|'m|]) -> bit['m] effect pure Chop function forall Nat 'm. (bit['m]) Chop(x, y) = x[0..y] val forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm. (nat, [|'n|], [|'m|]) -> [|'n:'m|] effect { wreg } Clamp function forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm. ([|'n:'m|]) Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = { ([|'n:'m|]) result := 0; if (x z) then { result := z; VSCR.SAT := bitone; } else { result := x; }; 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. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { wmem , rmem } MEM (* XXX effect for trap? *) val extern unit -> unit effect pure trap register (bool) mode64bit scattered function unit execute scattered typedef ast = const union val bit[32] -> ast effect pure decode scattered function ast decode union ast member (bit[5], bit[5], bit[2], bit) Bclr function clause decode ([bitzero, bitone, bitzero, bitzero, bitone, bitone] : (bit[5]) BO : (bit[5]) BI : (bit[3]) _ : (bit[2]) BH : [bitzero, bitzero, bitzero, bitzero, bitzero, bitone, bitzero, bitzero, bitzero, bitzero] : [LK] as instr) = Bclr (BO,BI,BH,LK) function clause execute (Bclr (BO, BI, BH, LK)) = { if mode64bit then M := 0 else M := 32; if ~ (BO[2]) then CTR := CTR - 1; ctr_ok := (BO[2] | (CTR[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; if LK then LR := CIA + 4 } union ast member (bit[5], bit[5], bit[16]) Lwz function clause decode ([bitone, bitzero, bitzero, bitzero, bitzero, bitzero] : (bit[5]) RT : (bit[5]) RA : (bit[16]) D as instr) = Lwz (RT,RA,D) function clause execute (Lwz (RT, RA, D)) = { (bit[64]) b := 0; if RA == 0 then b := 0 else b := GPR[RA]; EA := b + EXTS (D); GPR[RT] := 0b00000000000000000000000000000000 : MEM (EA,4) } union ast member (bit[5], bit[5], bit[16]) Stw function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitzero] : (bit[5]) RS : (bit[5]) RA : (bit[16]) D as instr) = Stw (RS,RA,D) function clause execute (Stw (RS, RA, D)) = { (bit[64]) b := 0; if RA == 0 then b := 0 else b := GPR[RA]; EA := b + EXTS (D); MEM(EA,4) := (GPR[RS])[32 .. 63] } union ast member (bit[5], bit[5], bit[16]) Stwu function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitone] : (bit[5]) RS : (bit[5]) RA : (bit[16]) D as instr) = Stwu (RS,RA,D) function clause execute (Stwu (RS, RA, D)) = { EA := GPR[RA] + EXTS (D); MEM(EA,4) := (GPR[RS])[32 .. 63]; GPR[RA] := EA } union ast member (bit[5], bit[5], bit[16]) Addi function clause decode ([bitzero, bitzero, bitone, bitone, bitone, bitzero] : (bit[5]) RT : (bit[5]) RA : (bit[16]) SI as instr) = Addi (RT,RA,SI) function clause execute (Addi (RT, RA, SI)) = if RA == 0 then GPR[RT] := EXTS (SI) else GPR[RT] := GPR[RA] + EXTS (SI) union ast member (bit[5], bit[5], bit[5], bit) Or function clause decode ([bitzero, bitone, bitone, bitone, bitone, bitone] : (bit[5]) RS : (bit[5]) RA : (bit[5]) RB : [bitzero, bitone, bitone, bitzero, bitone, bitone, bitone, bitone, bitzero, bitzero] : [Rc] as instr) = Or (RS,RA,RB,Rc) function clause execute (Or (RS, RA, RB, Rc)) = GPR[RA] := (GPR[RS] | GPR[RB]) end decode end execute end ast register ast instr (* monitor decoded instructions *) (* fetch-decode-execute *) function unit fde () = { NIA := CIA + 4; instr := decode(MEM(CIA, 4)); execute(instr); CIA := NIA; }