openpower/isafunctions/bfp.mdwn

   1 # binary-floating-point helper functions
   2
   3 `bfp_*` and related functions as needed by fcvt* from PowerISA v3.1B Book I
   4 section 7.6.2.2
   5
   6     def reset_xflags():
   7         vxsnan_flag <- 0
   8         vximz_flag <- 0
   9         vxidi_flag <- 0
  10         vxisi_flag <- 0
  11         vxzdz_flag <- 0
  12         vxsqrt_flag <- 0
  13         vxcvi_flag <- 0
  14         vxvc_flag <- 0
  15         ox_flag <- 0
  16         ux_flag <- 0
  17         xx_flag <- 0
  18         zx_flag <- 0
  19
  20     def bfp_CONVERT_FROM_BFP64(x):
  21         # x is a binary floating-point value represented in
  22         # double-precision format.
  23         exponent <- x[1:11]
  24         fraction <- x[12:63]
  25
  26         result <- BFPState()
  27         result.sign <- 0
  28         result.exponent <- 0
  29         result.significand <- 0
  30         result.class.SNaN <- 0
  31         result.class.QNaN <- 0
  32         result.class.Infinity <- 0
  33         result.class.Zero <- 0
  34         result.class.Denormal <- 0
  35         result.class.Normal <- 0
  36         if (exponent = 2047) & (fraction[0] = 0) & (fraction != 0) then
  37             # x is a SNaN
  38             result.class.SNaN <- 1
  39             result.sign <- x[0]
  40             result.significand[0] <- 0
  41             result.significand[1:52] <- fraction
  42         else if (exponent = 2047) & (fraction[0] != 0) & (fraction != 0) then
  43             # x is a QNaN
  44             result.class.QNaN <- 1
  45             result.sign <- x[0]
  46             result.significand[0] <- 0
  47             result.significand[1:52] <- fraction
  48         else if (exponent = 2047) & (fraction = 0) then
  49             # is an Infinity
  50             result.class.Infinity <- 1
  51             result.sign <- x[0]
  52         else if (exponent = 0) & (fraction = 0) then
  53             # x is a Zero
  54             result.class.Zero <- 1
  55             result.sign <- x[0]
  56         else if (exponent = 0) & (fraction != 0) then
  57             # x is a Denormal
  58             result.class.Denormal <- 1
  59             result.sign <- x[0]
  60             result.exponent <- -1022
  61             result.significand[0] <- 0
  62             result.significand[1:52] <- fraction
  63             do while result.significand[0] != 1
  64                 result.significand <- result.significand * 2
  65                 result.exponent <- result.exponent - 1
  66         else
  67             result.class.Normal <- 1
  68             result.sign <- x[0]
  69             result.exponent <- exponent
  70             # have to do the subtraction separately since SelectableInt won't
  71             # give negative results
  72             result.exponent <- result.exponent - 1023
  73             result.significand[0] <- 1
  74             result.significand[1:52] <- fraction
  75         return result
  76
  77     def bfp_CONVERT_FROM_SI32(x):
  78         # x is an integer value represented in signed word integer format.
  79
  80         result <- BFPState()
  81         result.sign <- 0
  82         result.exponent <- 0
  83         result.significand <- 0
  84         result.class.SNaN <- 0
  85         result.class.QNaN <- 0
  86         result.class.Infinity <- 0
  87         result.class.Zero <- 0
  88         result.class.Denormal <- 0
  89         result.class.Normal <- 0
  90
  91         if x = 0x0000_0000 then
  92             result.class.Zero <- 1
  93         else
  94             result.class.Normal <- 1
  95             result.sign <- x[0]
  96             result.exponent <- 32
  97             result.significand[0:32] <- EXTS(x)
  98
  99             if result.significand[0] = 1 then
 100                 result.sign <- 1
 101                 result.significand[0:32] <- -result.significand[0:32]
 102             do while result.significand[0] = 0
 103                 result.significand <- result.significand * 2
 104                 result.exponent <- result.exponent - 1
 105         return result
 106
 107     def bfp_CONVERT_FROM_SI64(x):
 108         # x is an integer value represented in signed double-word integer
 109         # format.
 110
 111         result <- BFPState()
 112         result.sign <- 0
 113         result.exponent <- 0
 114         result.significand <- 0
 115         result.class.SNaN <- 0
 116         result.class.QNaN <- 0
 117         result.class.Infinity <- 0
 118         result.class.Zero <- 0
 119         result.class.Denormal <- 0
 120         result.class.Normal <- 0
 121
 122         if x = 0x0000_0000_0000_0000 then
 123             result.class.Zero <- 1
 124         else
 125             result.class.Normal <- 1
 126             result.sign <- x[0]
 127             result.exponent <- 64
 128             result.significand[0:64] <- EXTS(x)
 129
 130             if result.significand[0] = 1 then
 131                 result.sign <- 1
 132                 result.significand[0:64] <- -result.significand[0:64]
 133             do while result.significand[0] = 0
 134                 result.significand <- result.significand * 2
 135                 result.exponent <- result.exponent - 1
 136         return result
 137
 138     def bfp_CONVERT_FROM_SI128(x):
 139         # x is a 128-bit signed integer value.
 140
 141         result <- BFPState()
 142         result.sign <- 0
 143         result.exponent <- 0
 144         result.significand <- 0
 145         result.class.SNaN <- 0
 146         result.class.QNaN <- 0
 147         result.class.Infinity <- 0
 148         result.class.Zero <- 0
 149         result.class.Denormal <- 0
 150         result.class.Normal <- 0
 151
 152         if x = 0x0000_0000_0000_0000_0000_0000_0000_0000 then
 153             result.class.Zero <- 1
 154         else
 155             result.class.Normal <- 1
 156             result.sign <- x[0]
 157             result.exponent <- 128
 158             result.significand[0:128] <- EXTS(x)
 159
 160             if result.significand[0] = 1 then
 161                 result.sign <- 1
 162                 result.significand[0:128] <- -result.significand[0:128]
 163             do while result.significand[0] = 0
 164                 result.significand <- result.significand * 2
 165                 result.exponent <- result.exponent - 1
 166         return result
 167
 168     def bfp_CONVERT_FROM_UI32(x):
 169         # x is an integer value represented in unsigned word integer
 170         # format.
 171
 172         result <- BFPState()
 173         result.sign <- 0
 174         result.exponent <- 0
 175         result.significand <- 0
 176         result.class.SNaN <- 0
 177         result.class.QNaN <- 0
 178         result.class.Infinity <- 0
 179         result.class.Zero <- 0
 180         result.class.Denormal <- 0
 181         result.class.Normal <- 0
 182
 183         if x = 0x0000_0000 then
 184             result.class.Zero <- 1
 185         else
 186             result.class.Normal <- 1
 187             result.sign <- 0
 188             result.exponent <- 32
 189             result.significand[0:32] <- 0b0 || x
 190             do while result.significand[0] = 0
 191                 result.significand <- result.significand * 2
 192                 result.exponent <- result.exponent - 1
 193         return result
 194
 195     def bfp_CONVERT_FROM_UI64(x):
 196         # x is an integer value represented in unsigned double-word integer
 197         # format.
 198
 199         result <- BFPState()
 200         result.sign <- 0
 201         result.exponent <- 0
 202         result.significand <- 0
 203         result.class.SNaN <- 0
 204         result.class.QNaN <- 0
 205         result.class.Infinity <- 0
 206         result.class.Zero <- 0
 207         result.class.Denormal <- 0
 208         result.class.Normal <- 0
 209
 210         if x = 0x0000_0000_0000_0000 then
 211             result.class.Zero <- 1
 212         else
 213             result.class.Normal <- 1
 214             result.sign <- 0
 215             result.exponent <- 64
 216             result.significand[0:64] <- 0b0 || x
 217             do while result.significand[0] = 0
 218                 result.significand <- result.significand * 2
 219                 result.exponent <- result.exponent - 1
 220         return result
 221
 222     def bfp_CONVERT_FROM_UI128(x):
 223         # x is a 128-bit unsigned integer value.
 224
 225         result <- BFPState()
 226         result.sign <- 0
 227         result.exponent <- 0
 228         result.significand <- 0
 229         result.class.SNaN <- 0
 230         result.class.QNaN <- 0
 231         result.class.Infinity <- 0
 232         result.class.Zero <- 0
 233         result.class.Denormal <- 0
 234         result.class.Normal <- 0
 235
 236         if x = 0x0000_0000_0000_0000_0000_0000_0000_0000 then
 237             result.class.Zero <- 1
 238         else
 239             result.class.Normal <- 1
 240             result.sign <- 0
 241             result.exponent <- 128
 242             result.significand[0:128] <- 0b0 || x
 243             do while result.significand[0] = 0
 244                 result.significand <- result.significand * 2
 245                 result.exponent <- result.exponent - 1
 246         return result
 247
 248     def bfp_ROUND_TO_INTEGER(rmode, x):
 249         # x is a binary floating-point value that is represented in the
 250         # binary floating-point working format and has
 251         # unbounded exponent range and significand precision.
 252
 253         if IsSNaN(x) then vxsnan_flag <- 1
 254         if IsNaN(x) & ¬IsSNaN(x) then return x
 255         if IsSNaN(x) then
 256             result <- x
 257             result.class.SNaN <- 0
 258             result.class.QNaN <- 1
 259             return result
 260         if IsInf(x) | IsZero(x) then return x
 261         result <- x
 262         result.class.Denormal <- 0
 263         result.class.Normal <- 0
 264         exact <- 0b0
 265         halfway <- 0b0
 266         more_than_halfway <- 0b0
 267         even <- 0b0
 268         if result.exponent < -1 then
 269             # all values have magnitude < 0.5
 270             result.significand <- 0
 271             result.exponent <- 0
 272             even <- 0b1
 273         else if result.exponent = -1 then
 274             if result.significand[0] = 1 then
 275                 result.significand[0] <- 0
 276                 if result.significand = 0 then halfway <- 0b1
 277                 else more_than_halfway <- 0b1
 278             result.significand <- 0
 279             result.exponent <- 0
 280             even <- 0b1
 281         else
 282             result.significand <- 0
 283             int_part <- x.significand[0:x.exponent]
 284             result.significand[0:x.exponent] <- int_part
 285             even <- ¬int_part[x.exponent]
 286             temp <- x.significand
 287             temp[0:x.exponent] <- 0
 288             if temp = 0 then exact <- 0b1
 289             if temp[x.exponent + 1] = 1 then
 290                 temp[x.exponent + 1] <- 0
 291                 if temp = 0 then halfway <- 0b1
 292                 else more_than_halfway <- 0b1
 293         if rmode = 0b000 then  # Round to Nearest Even
 294             round_up <- (¬even & halfway) | more_than_halfway
 295         if rmode = 0b001 then  # Round towards Zero
 296             round_up <- 0b0
 297         if rmode = 0b010 then  # Round towards +Infinity
 298             round_up <- (x.sign = 0) & ¬exact
 299         if rmode = 0b011 then  # Round towards -Infinity
 300             round_up <- (x.sign = 1) & ¬exact
 301         if rmode = 0b100 then  # Round to Nearest Away
 302             round_up <- halfway | more_than_halfway
 303         if round_up then
 304             inc_flag <- 1
 305             temp <- BFPState()
 306             temp.significand <- 0
 307             temp.significand[result.exponent] <- 1
 308             result.significand <- result.significand + temp.significand
 309             if result.significand >= 2 then
 310                 result.significand <- truediv(result.significand, 2)
 311                 result.exponent <- result.exponent + 1
 312         else inc_flag <- 0  # TODO: does the spec specify this?
 313         if result.significand = 0 then result.class.Zero <- 1
 314         else result.class.Normal <- 1
 315         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 316         else xx_flag <- 0  # TODO: does the spec specify this?
 317         return result
 318
 319     def bfp_ROUND_TO_INTEGER_NEAR_EVEN(x):
 320         return bfp_ROUND_TO_INTEGER(0b000, x)
 321
 322     def bfp_ROUND_TO_INTEGER_TRUNC(x):
 323         return bfp_ROUND_TO_INTEGER(0b001, x)
 324
 325     def bfp_ROUND_TO_INTEGER_CEIL(x):
 326         return bfp_ROUND_TO_INTEGER(0b010, x)
 327
 328     def bfp_ROUND_TO_INTEGER_FLOOR(x):
 329         return bfp_ROUND_TO_INTEGER(0b011, x)
 330
 331     def bfp_ROUND_TO_INTEGER_NEAR_AWAY(x):
 332         return bfp_ROUND_TO_INTEGER(0b100, x)
 333
 334     def bfp_COMPARE_EQ(x, y):
 335         # x is a binary floating-point value represented in the
 336         # binary floating-point working format.
 337         # y is a binary floating-point value represented in the
 338         # binary floating-point working format.
 339
 340         if IsNaN(x) | IsNaN(y) then
 341             return 0b0
 342         if IsZero(x) & IsZero(y) then
 343             return 0b1
 344
 345         if IsInf(x) & IsInf(y) then
 346             return x.sign = y.sign
 347         if IsInf(x) | IsInf(y) then
 348             return 0b0
 349         if IsZero(x) | IsZero(y) then
 350             return 0b0
 351         if x.sign != y.sign then
 352             return 0b0
 353         if x.exponent > 0 then xs <- x.significand * pow(2, x.exponent)
 354         else xs <- truediv(x.significand, pow(2, -x.exponent))
 355         if y.exponent > 0 then ys <- y.significand * pow(2, y.exponent)
 356         else ys <- truediv(y.significand, pow(2, -y.exponent))
 357         return xs = ys
 358
 359     def bfp_COMPARE_GT(x, y):
 360         # x is a binary floating-point value represented in the
 361         # binary floating-point working format.
 362         # y is a binary floating-point value represented in the
 363         # binary floating-point working format.
 364
 365         if IsNaN(x) | IsNaN(y) then
 366             return 0b0
 367         if IsZero(x) & IsZero(y) then
 368             return 0b0
 369
 370         if IsInf(x) & IsInf(y) then
 371             return ¬IsNeg(x) & IsNeg(y)
 372         if IsInf(x) then
 373             return ¬IsNeg(x)
 374         if IsInf(y) then
 375             return IsNeg(y)
 376         if IsZero(x) then
 377             return IsNeg(y)
 378         if IsZero(y) then
 379             return ¬IsNeg(x)
 380         if x.sign != y.sign then
 381             return IsNeg(y)
 382         if x.exponent > 0 then xs <- x.significand * pow(2, x.exponent)
 383         else xs <- truediv(x.significand, pow(2, -x.exponent))
 384         if y.exponent > 0 then ys <- y.significand * pow(2, y.exponent)
 385         else ys <- truediv(y.significand, pow(2, -y.exponent))
 386         if x.sign = 1 then return xs < ys
 387         return xs > ys
 388
 389     def bfp_COMPARE_LT(x, y):
 390         # x is a binary floating-point value represented in the
 391         # binary floating-point working format.
 392         # y is a binary floating-point value represented in the
 393         # binary floating-point working format.
 394
 395         if IsNaN(x) | IsNaN(y) then
 396             return 0b0
 397         if IsZero(x) & IsZero(y) then
 398             return 0b0
 399
 400         if IsInf(x) & IsInf(y) then
 401             return IsNeg(x) & ¬IsNeg(y)
 402         if IsInf(x) then
 403             return IsNeg(x)
 404         if IsInf(y) then
 405             return ¬IsNeg(y)
 406         if IsZero(x) then
 407             return ¬IsNeg(y)
 408         if IsZero(y) then
 409             return IsNeg(x)
 410         if x.sign != y.sign then
 411             return IsNeg(x)
 412         if x.exponent > 0 then xs <- x.significand * pow(2, x.exponent)
 413         else xs <- truediv(x.significand, pow(2, -x.exponent))
 414         if y.exponent > 0 then ys <- y.significand * pow(2, y.exponent)
 415         else ys <- truediv(y.significand, pow(2, -y.exponent))
 416         if x.sign = 1 then return xs > ys
 417         return xs < ys
 418
 419     def bfp_ABSOLUTE(x):
 420         # x is a binary floating-point value represented in the
 421         # binary floating-point working format.
 422         result <- x
 423         result.sign <- 0
 424         return result
 425
 426     def si32_CONVERT_FROM_BFP(x):
 427         # x is an integer value represented in the
 428         # binary floating-point working format.
 429
 430         if IsNaN(x) then
 431             vxcvi_flag <- 1
 432             if IsSNaN(x) then vxsnan_flag <- 1
 433             return 0x8000_0000
 434         else
 435             temp_xx <- xx_flag
 436             temp_inc <- inc_flag
 437             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 438             # TODO: does the spec say these are preserved?
 439             xx_flag <- temp_xx
 440             inc_flag <- temp_inc
 441             exponent <- rnd.exponent
 442             significand <- rnd.significand
 443             si32max <- bfp_CONVERT_FROM_SI32(0b0 || [1] * 31)
 444             si32min <- bfp_CONVERT_FROM_SI32(0b1 || [0] * 31)
 445             if bfp_COMPARE_GT(rnd, si32max) then
 446                 vxcvi_flag <- 1
 447                 return 0x7FFF_FFFF
 448             if bfp_COMPARE_LT(rnd, si32min) then
 449                 vxcvi_flag <- 1
 450                 return 0x8000_0000
 451             else
 452                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 453                 else xx_flag <- 0  # TODO: does the spec specify this?
 454                 inc_flag <- 0
 455                 # TODO: spec says this is logical shift right:
 456                 significand <- significand[0:31] / pow(2, 31 - exponent)
 457                 if IsNeg(rnd) then significand <- -significand
 458                 return significand[0:31]
 459
 460     def si64_CONVERT_FROM_BFP(x):
 461         # x is an integer value represented in the
 462         # binary floating-point working format.
 463
 464         if IsNaN(x) then
 465             vxcvi_flag <- 1
 466             if IsSNaN(x) then vxsnan_flag <- 1
 467             return 0x8000_0000_0000_0000
 468         else
 469             temp_xx <- xx_flag
 470             temp_inc <- inc_flag
 471             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 472             # TODO: does the spec say these are preserved?
 473             xx_flag <- temp_xx
 474             inc_flag <- temp_inc
 475             exponent <- rnd.exponent
 476             significand <- rnd.significand
 477             si64max <- bfp_CONVERT_FROM_SI64(0b0 || [1] * 63)
 478             si64min <- bfp_CONVERT_FROM_SI64(0b1 || [0] * 63)
 479             if bfp_COMPARE_GT(rnd, si64max) then
 480                 vxcvi_flag <- 1
 481                 return 0x7FFF_FFFF_FFFF_FFFF
 482             if bfp_COMPARE_LT(rnd, si64min) then
 483                 vxcvi_flag <- 1
 484                 return 0x8000_0000_0000_0000
 485             else
 486                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 487                 else xx_flag <- 0  # TODO: does the spec specify this?
 488                 inc_flag <- 0
 489                 # TODO: spec says this is logical shift right:
 490                 significand <- significand[0:63] / pow(2, 63 - exponent)
 491                 if IsNeg(rnd) then significand <- -significand
 492                 return significand[0:63]
 493
 494     def si128_CONVERT_FROM_BFP(x):
 495         # x is an integer value represented in the
 496         # binary floating-point working format.
 497
 498         if IsNaN(x) then
 499             vxcvi_flag <- 1
 500             if IsSNaN(x) then vxsnan_flag <- 1
 501             return 0x8000_0000_0000_0000_0000_0000_0000_0000
 502         else
 503             temp_xx <- xx_flag
 504             temp_inc <- inc_flag
 505             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 506             # TODO: does the spec say these are preserved?
 507             xx_flag <- temp_xx
 508             inc_flag <- temp_inc
 509             exponent <- rnd.exponent
 510             significand <- rnd.significand
 511             si128max <- bfp_CONVERT_FROM_SI128(0b0 || [1] * 127)
 512             si128min <- bfp_CONVERT_FROM_SI128(0b1 || [0] * 127)
 513             if bfp_COMPARE_GT(rnd, si128max) then
 514                 vxcvi_flag <- 1
 515                 return 0x7FFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
 516             if bfp_COMPARE_LT(rnd, si128min) then
 517                 vxcvi_flag <- 1
 518                 return 0x8000_0000_0000_0000_0000_0000_0000_0000
 519             else
 520                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 521                 else xx_flag <- 0  # TODO: does the spec specify this?
 522                 inc_flag <- 0
 523                 # TODO: spec says this is logical shift right:
 524                 significand <- significand[0:127] / pow(2, 127 - exponent)
 525                 if IsNeg(rnd) then significand <- -significand
 526                 return significand[0:127]
 527
 528     def ui32_CONVERT_FROM_BFP(x):
 529         # x is an integer value represented in the
 530         # binary floating-point working format.
 531
 532         if IsNaN(x) then
 533             vxcvi_flag <- 1
 534             if IsSNaN(x) then vxsnan_flag <- 1
 535             return 0x0000_0000
 536         else
 537             temp_xx <- xx_flag
 538             temp_inc <- inc_flag
 539             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 540             # TODO: does the spec say these are preserved?
 541             xx_flag <- temp_xx
 542             inc_flag <- temp_inc
 543             exponent <- rnd.exponent
 544             significand <- rnd.significand
 545             ui32max <- bfp_CONVERT_FROM_UI32([1] * 32)
 546             if bfp_COMPARE_GT(rnd, ui32max) then
 547                 vxcvi_flag <- 1
 548                 return 0xFFFF_FFFF
 549             if IsNeg(rnd) then
 550                 vxcvi_flag <- 1
 551                 return 0x0000_0000
 552             else
 553                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 554                 else xx_flag <- 0  # TODO: does the spec specify this?
 555                 inc_flag <- 0
 556                 # TODO: spec says this is logical shift right:
 557                 significand <- significand[0:31] / pow(2, 31 - exponent)
 558                 return significand[0:31]
 559
 560     def ui64_CONVERT_FROM_BFP(x):
 561         # x is an integer value represented in the
 562         # binary floating-point working format.
 563
 564         if IsNaN(x) then
 565             vxcvi_flag <- 1
 566             if IsSNaN(x) then vxsnan_flag <- 1
 567             return 0x0000_0000_0000_0000
 568         else
 569             temp_xx <- xx_flag
 570             temp_inc <- inc_flag
 571             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 572             # TODO: does the spec say these are preserved?
 573             xx_flag <- temp_xx
 574             inc_flag <- temp_inc
 575             exponent <- rnd.exponent
 576             significand <- rnd.significand
 577             ui64max <- bfp_CONVERT_FROM_UI64([1] * 64)
 578             if bfp_COMPARE_GT(rnd, ui64max) then
 579                 vxcvi_flag <- 1
 580                 return 0xFFFF_FFFF_FFFF_FFFF
 581             if IsNeg(rnd) then
 582                 vxcvi_flag <- 1
 583                 return 0x0000_0000_0000_0000
 584             else
 585                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 586                 else xx_flag <- 0  # TODO: does the spec specify this?
 587                 inc_flag <- 0
 588                 # TODO: spec says this is logical shift right:
 589                 significand <- significand[0:63] / pow(2, 63 - exponent)
 590                 return significand[0:63]
 591
 592     def ui128_CONVERT_FROM_BFP(x):
 593         # x is an integer value represented in the
 594         # binary floating-point working format.
 595
 596         if IsNaN(x) then
 597             vxcvi_flag <- 1
 598             if IsSNaN(x) then vxsnan_flag <- 1
 599             return 0x0000_0000_0000_0000_0000_0000_0000_0000
 600         else
 601             temp_xx <- xx_flag
 602             temp_inc <- inc_flag
 603             rnd <- bfp_ROUND_TO_INTEGER_TRUNC(x)
 604             # TODO: does the spec say these are preserved?
 605             xx_flag <- temp_xx
 606             inc_flag <- temp_inc
 607             exponent <- rnd.exponent
 608             significand <- rnd.significand
 609             ui128max <- bfp_CONVERT_FROM_UI128([1] * 128)
 610             if bfp_COMPARE_GT(rnd, ui128max) then
 611                 vxcvi_flag <- 1
 612                 return 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF
 613             if IsNeg(rnd) then
 614                 vxcvi_flag <- 1
 615                 return 0x0000_0000_0000_0000_0000_0000_0000_0000
 616             else
 617                 if ¬bfp_COMPARE_EQ(rnd, x) then xx_flag <- 1
 618                 else xx_flag <- 0  # TODO: does the spec specify this?
 619                 inc_flag <- 0
 620                 # TODO: spec says this is logical shift right:
 621                 significand <- significand[0:127] / pow(2, 127 - exponent)
 622                 return significand[0:127]
 623
 624     def bfp64_CONVERT_FROM_BFP(x):
 625         # x is a floating-point value represented in the binary floating-point
 626         # working format.
 627
 628         result <- [0] * 64
 629         if x.class.QNaN = 1 then
 630             result[0] <- x.sign
 631             result[1:11] <- 0b111_1111_1111
 632             result[12:63] <- x.significand[1:52]
 633         else if x.class.Infinity = 1 then
 634             result[0] <- x.sign
 635             result[1:11] <- 0b111_1111_1111
 636             result[12:63] <- 0
 637         else if x.class.Zero = 1 then
 638             result[0] <- x.sign
 639             result[1:63] <- 0
 640         else if (x.exponent < -1022) & (FPSCR.UE = 0) then
 641             result[0] <- x.sign
 642             sh_cnt <- -1022 - x.exponent
 643             result[1:11] <- 0b000_0000_0000
 644             # TODO: spec says this is shift right
 645             result[12:63] <- x.significand[1:52] / pow(2, sh_cnt)
 646         else if (x.exponent < -1022) & (FPSCR.UE = 1) then
 647             result[0:63] <- undefined(0)  # TODO: which undefined value to use?
 648         else if (x.exponent > 1023) & (FPSCR.OE = 1) then
 649             result[0:63] <- undefined(0)  # TODO: which undefined value to use?
 650         else
 651             result[0] <- x.sign
 652             result[1:11] <- x.exponent + 1023
 653             result[12:63] <- x.significand[1:52]
 654         return result
 655
 656     def bfp_ROUND_TO_BFP64(ro, rmode, x):
 657         # x is a normalized binary floating-point value that is represented in
 658         # the binary floating-point working format and has unbounded exponent
 659         # range and significand precision.
 660         # ro is a 1-bit unsigned integer and rmode is a 2-bit unsigned integer,
 661         # together specifying one of five rounding modes to be used in
 662         # rounding x.
 663         #
 664         # ro=0 rmode=0b00  Round to Nearest Even
 665         # ro=0 rmode=0b01  Round towards Zero
 666         # ro=0 rmode=0b10  Round towards +Infinity
 667         # ro=0 rmode=0b11  Round towards -Infinity
 668         # ro=1             Round to Odd
 669         #
 670         # Return the value x rounded to double-precision under control of the
 671         # specified rounding mode.
 672
 673         if x.class.QNaN then return x
 674         if x.class.Infinity then return x
 675         if x.class.Zero then return x
 676         if bfp_COMPARE_LT(bfp_ABSOLUTE(x), bfp_NMIN_BFP64()) then
 677             if FPSCR.UE=0 then
 678                 x <- bfp_DENORM(-1022, x)
 679                 if (ro=0) & (rmode=0b00) then r <- bfp_ROUND_NEAR_EVEN(53, x)
 680                 if (ro=0) & (rmode=0b01) then r <- bfp_ROUND_TRUNC(53, x)
 681                 if (ro=0) & (rmode=0b10) then r <- bfp_ROUND_CEIL(53, x)
 682                 if (ro=0) & (rmode=0b11) then r <- bfp_ROUND_FLOOR(53, x)
 683                 if  ro=1                 then r <- bfp_ROUND_ODD(53, x)
 684                 ux_flag <- xx_flag
 685                 return r
 686             else
 687                 x.exponent <- x.exponent + 1536
 688                 ux_flag <- 1
 689         if (ro=0) & (rmode=0b00) then r <- bfp_ROUND_NEAR_EVEN(53, x)
 690         if (ro=0) & (rmode=0b01) then r <- bfp_ROUND_TRUNC(53, x)
 691         if (ro=0) & (rmode=0b10) then r <- bfp_ROUND_CEIL(53, x)
 692         if (ro=0) & (rmode=0b11) then r <- bfp_ROUND_FLOOR(53, x)
 693         if  ro=1                 then r <- bfp_ROUND_ODD(53, x)
 694         if bfp_COMPARE_GT(bfp_ABSOLUTE(r), bfp_NMAX_BFP64()) then
 695             if FPSCR.OE=0 then
 696                 if x.sign then
 697                     if (ro=0) & (rmode=0b00) then r <- bfp_INFINITY()
 698                     if (ro=0) & (rmode=0b01) then r <- bfp_NMAX_BFP64()
 699                     if (ro=0) & (rmode=0b10) then r <- bfp_NMAX_BFP64()
 700                     if (ro=0) & (rmode=0b11) then r <- bfp_INFINITY()
 701                     if  ro=1                 then r <- bfp_NMAX_BFP64()
 702                 else
 703                     if (ro=0) & (rmode=0b00) then r <- bfp_INFINITY()
 704                     if (ro=0) & (rmode=0b01) then r <- bfp_NMAX_BFP64()
 705                     if (ro=0) & (rmode=0b10) then r <- bfp_INFINITY()
 706                     if (ro=0) & (rmode=0b11) then r <- bfp_NMAX_BFP64()
 707                     if  ro=1                 then r <- bfp_NMAX_BFP64()
 708                 r.sign <- x.sign
 709                 ox_flag <- 0b1
 710                 xx_flag <- 0b1
 711                 inc_flag <- undefined(0)  # TODO: which undefined value to use?
 712                 return r
 713             else
 714                 r.exponent <- r.exponent - 1536
 715                 ox_flag <- 1
 716         return r
 717
 718     def bfp_INFINITY():
 719         # The value +Infinity represented in the binary floating-point working
 720         # format.
 721         r <- BFPState()
 722         r.class.Infinity <- 1
 723         return r
 724
 725     def bfp_NMAX_BFP32():
 726         # Return the largest finite single-precision floating-point value
 727         # (i.e., 2^128 - 2^(128-24)) in the binary floating-point working
 728         # format.
 729         return bfp_CONVERT_FROM_BFP32(0x7F7F_FFFF)
 730
 731     def bfp_NMAX_BFP64():
 732         # Return the largest finite double-precision floating-point value
 733         # (i.e., 2^1024 - 2^(1024-53)) in the binary floating-point working
 734         # format.
 735         return bfp_CONVERT_FROM_BFP64(0x7FEF_FFFF_FFFF_FFFF)
 736
 737     def bfp_NMIN_BFP32():
 738         # Return the smallest positive normalized single-precision
 739         # floating-point value, 2^-126, represented in the binary
 740         # floating-point working format.
 741         return bfp_CONVERT_FROM_BFP32(0x0080_0000)
 742
 743     def bfp_NMIN_BFP64():
 744         # Return the smallest positive normalized double-precision
 745         # floating-point value, 2^-1022, represented in the binary
 746         # floating-point working format.
 747         return bfp_CONVERT_FROM_BFP64(0x0010_0000_0000_0000)
 748
 749     def bfp_ROUND_HELPER(p, ro, rmode, x):
 750         # not part of the PowerISA v3.1B specification.
 751         # helper function for the bfp_ROUND_* functions.
 752         # doesn't set inc_flag or xx_flag.
 753         #
 754         # x is a binary floating-point value that is represented in the binary
 755         # floating-point working format and has unbounded exponent range and
 756         # significand precision. x must be rounded as presented, without
 757         # prenormalization.
 758         #
 759         # p is an integer value specifying the precision (i.e., number of bits)
 760         # the significand is rounded to.
 761         #
 762         # ro is a 1-bit unsigned integer and rmode is a 3-bit unsigned integer,
 763         # together specifying one of six rounding modes to be used in
 764         # rounding x.
 765         #
 766         # ro=0 rmode=0b000  Round to Nearest Even
 767         # ro=0 rmode=0b001  Round towards Zero
 768         # ro=0 rmode=0b010  Round towards +Infinity
 769         # ro=0 rmode=0b011  Round towards -Infinity
 770         # ro=0 rmode=0b100  Round to Nearest Away
 771         # ro=1              Round to Odd
 772
 773         if IsInf(x) | IsNaN(x) | IsZero(x) then
 774             inc_flag <- 0  # TODO: does the spec specify this?
 775             xx_flag <- 0  # TODO: does the spec specify this?
 776             return x
 777
 778         result <- x
 779         result.significand <- 0
 780         result.significand[0:p - 1] <- x.significand[0:p - 1]
 781         exact <- x.significand = result.significand
 782         halfway <- 0b0
 783         more_than_half <- 0b0
 784         if x.significand[p] then
 785             t <- x
 786             t.significand <- 0
 787             t.significand[0:p] <- x.significand[0:p]
 788             if t.significand = x.significand then halfway <- 0b1
 789             else more_than_half <- 0b1
 790         even <- ¬result.significand[p - 1]
 791
 792         if (ro=0) & (rmode=0b000) then  # Round to Nearest Even
 793             round_up <- (halfway & ¬even) | more_than_half
 794         if (ro=0) & (rmode=0b001) then  # Round towards Zero
 795             round_up <- 0b0
 796         if (ro=0) & (rmode=0b010) then  # Round towards +Infinity
 797             round_up <- (x.sign = 0) & ¬exact
 798         if (ro=0) & (rmode=0b011) then  # Round towards -Infinity
 799             round_up <- (x.sign = 1) & ¬exact
 800         if (ro=0) & (rmode=0b100) then  # Round to Nearest Away
 801             round_up <- halfway | more_than_half
 802         if  ro=1                  then  # Round to Odd
 803             round_up <- ¬exact & even
 804
 805         if round_up then
 806             result.significand[0:p-1] <- result.significand[0:p-1] + 1
 807             if result.significand[0:p-1] = 0 then
 808                 result.significand[0] <- 1
 809                 result.exponent <- result.exponent + 1
 810
 811         if result.significand != 0 then
 812             do while result.significand[0] != 1
 813                 result.significand <- result.significand * 2
 814                 result.exponent <- result.exponent - 1
 815             result.class.Normal <- 1
 816             result.class.Denormal <- 0
 817             result.class.Zero <- 0
 818         else
 819             result.class.Normal <- 0
 820             result.class.Denormal <- 0
 821             result.class.Zero <- 1
 822
 823         return result
 824
 825     def bfp_ROUND_NEAR_EVEN(p, x):
 826         # x is a binary floating-point value that is represented in the binary
 827         # floating-point working format and has unbounded exponent range and
 828         # significand precision. x must be rounded as presented, without
 829         # prenormalization.
 830         #
 831         # p is an integer value specifying the precision (i.e., number of bits)
 832         # the significand is rounded to.
 833
 834         result <- bfp_ROUND_HELPER(p, 0b0, 0b000, x)
 835
 836         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 837             inc_flag <- 1
 838         else inc_flag <- 0  # TODO: does the spec specify this?
 839         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 840         else xx_flag <- 0  # TODO: does the spec specify this?
 841
 842         return result
 843
 844     def bfp_ROUND_TRUNC(p, x):
 845         # x is a binary floating-point value that is represented in the binary
 846         # floating-point working format and has unbounded exponent range and
 847         # significand precision. x must be rounded as presented, without
 848         # prenormalization.
 849         #
 850         # p is an integer value specifying the precision (i.e., number of bits)
 851         # the significand is rounded to.
 852
 853         result <- bfp_ROUND_HELPER(p, 0b0, 0b001, x)
 854
 855         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 856             inc_flag <- 1
 857         else inc_flag <- 0  # TODO: does the spec specify this?
 858         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 859         else xx_flag <- 0  # TODO: does the spec specify this?
 860
 861         return result
 862
 863     def bfp_ROUND_CEIL(p, x):
 864         # x is a binary floating-point value that is represented in the binary
 865         # floating-point working format and has unbounded exponent range and
 866         # significand precision. x must be rounded as presented, without
 867         # prenormalization.
 868         #
 869         # p is an integer value specifying the precision (i.e., number of bits)
 870         # the significand is rounded to.
 871
 872         result <- bfp_ROUND_HELPER(p, 0b0, 0b010, x)
 873
 874         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 875             inc_flag <- 1
 876         else inc_flag <- 0  # TODO: does the spec specify this?
 877         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 878         else xx_flag <- 0  # TODO: does the spec specify this?
 879
 880         return result
 881
 882     def bfp_ROUND_FLOOR(p, x):
 883         # x is a binary floating-point value that is represented in the binary
 884         # floating-point working format and has unbounded exponent range and
 885         # significand precision. x must be rounded as presented, without
 886         # prenormalization.
 887         #
 888         # p is an integer value specifying the precision (i.e., number of bits)
 889         # the significand is rounded to.
 890
 891         result <- bfp_ROUND_HELPER(p, 0b0, 0b011, x)
 892
 893         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 894             inc_flag <- 1
 895         else inc_flag <- 0  # TODO: does the spec specify this?
 896         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 897         else xx_flag <- 0  # TODO: does the spec specify this?
 898
 899         return result
 900
 901     def bfp_ROUND_NEAR_AWAY(p, x):
 902         # not part of the PowerISA v3.1B specification.
 903         #
 904         # x is a binary floating-point value that is represented in the binary
 905         # floating-point working format and has unbounded exponent range and
 906         # significand precision. x must be rounded as presented, without
 907         # prenormalization.
 908         #
 909         # p is an integer value specifying the precision (i.e., number of bits)
 910         # the significand is rounded to.
 911
 912         result <- bfp_ROUND_HELPER(p, 0b0, 0b100, x)
 913
 914         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 915             inc_flag <- 1
 916         else inc_flag <- 0  # TODO: does the spec specify this?
 917         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 918         else xx_flag <- 0  # TODO: does the spec specify this?
 919
 920         return result
 921
 922     def bfp_ROUND_ODD(p, x):
 923         # x is a binary floating-point value that is represented in the binary
 924         # floating-point working format and has unbounded exponent range and
 925         # significand precision. x must be rounded as presented, without
 926         # prenormalization.
 927         #
 928         # p is an integer value specifying the precision (i.e., number of bits)
 929         # the significand is rounded to.
 930
 931         result <- bfp_ROUND_HELPER(p, 0b1, 0b000, x)
 932
 933         if bfp_COMPARE_GT(bfp_ABSOLUTE(result), bfp_ABSOLUTE(x)) then
 934             inc_flag <- 1
 935         else inc_flag <- 0  # TODO: does the spec specify this?
 936         if ¬bfp_COMPARE_EQ(result, x) then xx_flag <- 1
 937         else xx_flag <- 0  # TODO: does the spec specify this?
 938
 939         return result
 940
 941     def fprf_CLASS_BFP64(x):
 942         # x is a floating-point value represented in double-precision format.
 943         #
 944         # Return the 5-bit code that specifies the sign and class of x.
 945
 946         v <- bfp_CONVERT_FROM_BFP64(x)
 947         if v.class.QNaN then return 0b10001
 948         if (v.sign = 1) & v.class.Infinity then return 0b01001
 949         if (v.sign = 0) & v.class.Infinity then return 0b00101
 950         if (v.sign = 1) & v.class.Zero then return 0b10010
 951         if (v.sign = 0) & v.class.Zero then return 0b00010
 952         if (v.sign = 1) & v.class.Denormal then return 0b11000
 953         if (v.sign = 0) & v.class.Denormal then return 0b10100
 954         if (v.sign = 1) & v.class.Normal then return 0b01000
 955         if (v.sign = 0) & v.class.Normal then return 0b00100