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 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; } register (vector <0, 64, inc, bit>) GPR0 register (vector <0, 64, inc, bit>) GPR1 register (vector <0, 64, inc, bit>) GPR2 register (vector <0, 64, inc, bit>) GPR3 register (vector <0, 64, inc, bit>) GPR4 register (vector <0, 64, inc, bit>) GPR5 register (vector <0, 64, inc, bit>) GPR6 register (vector <0, 64, inc, bit>) GPR7 register (vector <0, 64, inc, bit>) GPR8 register (vector <0, 64, inc, bit>) GPR9 register (vector <0, 64, inc, bit>) GPR10 register (vector <0, 64, inc, bit>) GPR11 register (vector <0, 64, inc, bit>) GPR12 register (vector <0, 64, inc, bit>) GPR13 register (vector <0, 64, inc, bit>) GPR14 register (vector <0, 64, inc, bit>) GPR15 register (vector <0, 64, inc, bit>) GPR16 register (vector <0, 64, inc, bit>) GPR17 register (vector <0, 64, inc, bit>) GPR18 register (vector <0, 64, inc, bit>) GPR19 register (vector <0, 64, inc, bit>) GPR20 register (vector <0, 64, inc, bit>) GPR21 register (vector <0, 64, inc, bit>) GPR22 register (vector <0, 64, inc, bit>) GPR23 register (vector <0, 64, inc, bit>) GPR24 register (vector <0, 64, inc, bit>) GPR25 register (vector <0, 64, inc, bit>) GPR26 register (vector <0, 64, inc, bit>) GPR27 register (vector <0, 64, inc, bit>) GPR28 register (vector <0, 64, inc, bit>) GPR29 register (vector <0, 64, inc, bit>) GPR30 register (vector <0, 64, inc, bit>) GPR31 let (vector <0, 32, inc, (register<(vector<0, 64, inc, bit>)>) >) 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[64]) NIA (* next instruction address *) register (bit[64]) CIA (* current instruction address *) register (bit[32 : 63]) CR register (bit[64]) CTR register (bit[64]) LR typedef xer = register bits [ 0 : 63 ] { 32 : SO; 33 : OV; 34 : CA; } register (xer) XER (* XXX bogus, length should be 1024 with many more values - cf. mfspr definition *) let (vector <0, 10, inc, (register<(vector<0, 64, inc, bit>)>) >) 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 ] 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 scattered function ast decode union ast member (vector<0, 2, inc, bit> , vector<0, 5, inc, bit> , vector<0, 5, inc, bit> , bit) BranchConditionaltoLinkRegister function clause decode ([0 = bitzero, 1 = bitone, 2 = bitzero, 3 = bitzero, 4 = bitone, 5 = bitone, 21 = bitzero, 22 = bitzero, 23 = bitzero, 24 = bitzero, 25 = bitzero, 26 = bitone, 27 = bitzero, 28 = bitzero, 29 = bitzero, 30 = bitzero] as instr) = BranchConditionaltoLinkRegister (instr[19 .. 20],instr[11 .. 15],instr[6 .. 10],instr[31]) function clause execute (BranchConditionaltoLinkRegister (BH, BI, BO, 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 (vector<0, 16, inc, bit> , vector<0, 5, inc, bit> , vector<0, 5, inc, bit> ) LoadWordandZero function clause decode ([0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitzero, 4 = bitzero, 5 = bitzero] as instr) = LoadWordandZero (instr[16 .. 31],instr[11 .. 15],instr[6 .. 10]) function clause execute (LoadWordandZero (D, RA, RT)) = { (vector<0, 64, inc, bit> ) EA := 0; (vector<0, 64, inc, bit> ) 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 (vector<0, 16, inc, bit> , vector<0, 5, inc, bit> , vector<0, 5, inc, bit> ) StoreWord function clause decode ([0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitone, 4 = bitzero, 5 = bitzero] as instr) = StoreWord (instr[16 .. 31],instr[11 .. 15],instr[6 .. 10]) function clause execute (StoreWord (D, RA, RS)) = { (vector<0, 64, inc, bit> ) EA := 0; (vector<0, 64, inc, bit> ) 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 (vector<0, 16, inc, bit> , vector<0, 5, inc, bit> , vector<0, 5, inc, bit> ) StoreWordwithUpdate function clause decode ([0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitone, 4 = bitzero, 5 = bitone] as instr) = StoreWordwithUpdate (instr[16 .. 31],instr[11 .. 15],instr[6 .. 10]) function clause execute (StoreWordwithUpdate (D, RA, RS)) = { (vector<0, 64, inc, bit> ) EA := 0; EA := GPR[RA] + exts (D); MEM(EA,4) := (GPR[RS])[32 .. 63]; GPR[RA] := EA } union ast member (vector<0, 5, inc, bit> , vector<0, 5, inc, bit> , vector<0, 16, inc, bit> ) AddImmediate function clause decode ([0 = bitzero, 1 = bitzero, 2 = bitone, 3 = bitone, 4 = bitone, 5 = bitzero] as instr) = AddImmediate (instr[11 .. 15],instr[6 .. 10],instr[16 .. 31]) function clause execute (AddImmediate (RA, RT, SI)) = if RA == 0 then GPR[RT] := exts (SI) else GPR[RT] := GPR[RA] + exts (SI) union ast member (vector<0, 5, inc, bit> , vector<0, 5, inc, bit> , vector<0, 5, inc, bit> , bit) OR function clause decode ([0 = bitzero, 1 = bitone, 2 = bitone, 3 = bitone, 4 = bitone, 5 = bitone, 21 = bitzero, 22 = bitone, 23 = bitone, 24 = bitzero, 25 = bitone, 26 = bitone, 27 = bitone, 28 = bitone, 29 = bitzero, 30 = bitzero] as instr) = OR (instr[11 .. 15],instr[16 .. 20],instr[6 .. 10],instr[31]) function clause execute (OR (RA, RB, RS, 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; }