diff options
Diffstat (limited to 'src/test/power.sail')
| -rw-r--r-- | src/test/power.sail | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 232f542a..7a66cb20 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -163,7 +163,8 @@ let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 ] -register (bit[32:63]) VRSAVE +(* adapted to make type checker accept SPR definition *) +register (bit[(* 32 *) 0:63]) VRSAVE register (bit[64]) SPRG3 register (bit[64]) SPRG4 @@ -172,7 +173,7 @@ 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 + [ 1=XER, 8=LR, 9=CTR, 256=VRSAVE, 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7 ] (* XXX DCR is implementation-dependent; also, some DCR are only 32 bits @@ -1421,6 +1422,7 @@ function clause execute (Stdux (RS, RA, RB)) = MEMw(EA,8) := GPR[RS] } +(* union ast member (bit[5], bit[5], bit[12], bit[4]) Lq function clause decode (0b111000 : @@ -1448,7 +1450,9 @@ function clause execute (Lq (RTp, RA, DQ, PT)) = GPR[RTp + 1] := bytereverse[64 .. 127] } } +*) +(* union ast member (bit[5], bit[5], bit[14]) Stq function clause decode (0b111110 : @@ -1458,6 +1462,7 @@ function clause decode (0b111110 : 0b10 as instr) = Stq (RSp,RA,DS) + function clause execute (Stq (RSp, RA, DS)) = { (bit[64]) b := 0; @@ -1476,6 +1481,7 @@ function clause execute (Stq (RSp, RA, DS)) = EA := b + EXTS (DS : 0b00); MEMw(EA,8) := RSp } +*) union ast member (bit[5], bit[5], bit[5]) Lhbrx @@ -2223,6 +2229,7 @@ function clause execute (Mullw (RT, RA, RB, OE, Rc)) = if OE then set_SO_OV (overflow) else () } +(* union ast member (bit[5], bit[5], bit[5], bit) Mulhw function clause decode (0b011111 : @@ -2254,7 +2261,9 @@ function clause execute (Mulhw (RT, RA, RB, Rc)) = } else () } +*) +(* union ast member (bit[5], bit[5], bit[5], bit) Mulhwu function clause decode (0b011111 : @@ -2280,7 +2289,9 @@ function clause execute (Mulhwu (RT, RA, RB, Rc)) = } else () } +*) +(* union ast member (bit[5], bit[5], bit[5], bit, bit) Divw function clause decode (0b011111 : @@ -2318,6 +2329,7 @@ function clause execute (Divw (RT, RA, RB, OE, Rc)) = if OE then set_SO_OV (overflow) else () } + union ast member (bit[5], bit[5], bit[5], bit, bit) Divwu function clause decode (0b011111 : @@ -2430,6 +2442,7 @@ function clause execute (Divweu (RT, RA, RB, OE, Rc)) = else (); if OE then set_SO_OV (overflow) else () } +*) union ast member (bit[5], bit[5], bit[5], bit, bit) Mulld @@ -2732,6 +2745,7 @@ function clause execute (Cmpl (BF, L, RA, RB)) = CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO] } +(* union ast member (bit[5], bit[5], bit[16]) Twi function clause decode (0b000011 : @@ -2770,6 +2784,7 @@ function clause execute (Tw (TO, RA, RB)) = if a <_u b & TO[3] then trap () else (); if a >_u b & TO[4] then trap () else () } +*) union ast member (bit[5], bit[5], bit[16]) Tdi @@ -5905,6 +5920,7 @@ function clause decode (0b011111 : function clause execute (Lvsr (VRT, RA, RB)) = () +(* union ast member (bit[5], bit[5], bit[5]) Vpkpx function clause decode (0b000100 : @@ -5927,6 +5943,7 @@ function clause execute (Vpkpx (VRT, VRA, VRB)) = (VR[VRT])[i + 75..i + 79] := (VR[VRB])[i * 2 + 24 .. i * 2 + 28] } + union ast member (bit[5], bit[5], bit[5]) Vpkshss function clause decode (0b000100 : @@ -6005,6 +6022,7 @@ function clause execute (Vpkswus (VRT, VRA, VRB)) = 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuhum function clause decode (0b000100 : @@ -6021,6 +6039,7 @@ function clause execute (Vpkuhum (VRT, VRA, VRB)) = (VR[VRT])[i + 64..i + 71] := (VR[VRB])[i * 2 + 8 .. i * 2 + 15] } + union ast member (bit[5], bit[5], bit[5]) Vpkuhus function clause decode (0b000100 : @@ -6039,6 +6058,7 @@ function clause execute (Vpkuhus (VRT, VRA, VRB)) = (Clamp (EXTZ ((VR[VRB])[i * 2 .. i * 2 + 15]),0,255))[24 .. 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuwum function clause decode (0b000100 : @@ -6055,6 +6075,7 @@ function clause execute (Vpkuwum (VRT, VRA, VRB)) = (VR[VRT])[i + 64..i + 79] := (VR[VRB])[i * 2 + 16 .. i * 2 + 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuwus function clause decode (0b000100 : @@ -10355,6 +10376,8 @@ function clause decode (0b011111 : Dcbf (L,RA,RB) function clause execute (Dcbf (L, RA, RB)) = () +*) + union ast member Isync @@ -10617,8 +10640,8 @@ function bit illegal_instructions_pred ((ast) instr) = { 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 (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)) |