whitespace cleanup on ls006, remove duplication,
authorLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Wed, 22 Mar 2023 16:06:18 +0000 (16:06 +0000)
committerLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Wed, 22 Mar 2023 16:06:29 +0000 (16:06 +0000)
add "special registers altered" section

openpower/sv/rfc/ls006.mdwn

index a25d148432cdd4591697f2858ee34c7fdfb6a8e9..1d7b3bb49c95031e50bea3dec40a1857ee753643 100644 (file)
@@ -56,56 +56,23 @@ Instructions added
 
 **Motivation**
 
-CPUs without VSX/VMX lack a way to efficiently transfer data between FPRs and GPRs, they need to go through memory, this proposal adds more efficient data transfer (both bitwise copy and Integer <-> FP conversion) instructions that transfer directly between FPRs and GPRs without needing to go through memory.
-
-IEEE 754 doesn't specify what results are obtained when converting a NaN or out-of-range floating-point value to integer, so different programming languages and ISAs have made different choices.  Below is an overview
+CPUs without VSX/VMX lack a way to efficiently transfer data between
+FPRs and GPRs, they need to go through memory, this proposal adds more
+efficient data transfer (both bitwise copy and Integer <-> FP conversion)
+instructions that transfer directly between FPRs and GPRs without needing
+to go through memory.
+
+IEEE 754 doesn't specify what results are obtained when converting a NaN
+or out-of-range floating-point value to integer, so different programming
+languages and ISAs have made different choices.  Below is an overview
 of the different variants, listing the languages and hardware that
 implements each variant.
 
-For convenience, we will give those different conversion semantics names based on which common ISA or programming language uses them, since there may not be an established name for them:
-
-* **Standard OpenPOWER-style conversion**
-
-This conversion, performs "saturation with NaN converted to minimum valid integer". This
-is also exactly the same as the x86 ISA conversion semantics.
-OpenPOWER has instructions for this conversion semantic for both:
-
-* rounding mode read from FPSCR
-* rounding mode always set to truncate
-
-* **Java/Saturating conversion**
-
-For the sake of simplicity, the FP -> Integer conversion semantics generalized from those used by Java's semantics (and Rust's `as` operator) will be referred to as
-[Java/Saturating conversion semantics](#fp-to-int-java-saturating-conversion-semantics).
-
-Those same semantics are used in some way by all of the following languages (not necessarily for the default conversion method):
-
-* Java's
-  [FP -> Integer conversion](https://docs.oracle.com/javase/specs/jls/se16/html/jls-5.html#jls-5.1.3) (only for long/int results)
-* Rust's FP -> Integer conversion using the
-  [`as` operator](https://doc.rust-lang.org/reference/expressions/operator-expr.html#semantics)
-* LLVM's
-  [`llvm.fptosi.sat`](https://llvm.org/docs/LangRef.html#llvm-fptosi-sat-intrinsic) and
-  [`llvm.fptoui.sat`](https://llvm.org/docs/LangRef.html#llvm-fptoui-sat-intrinsic) intrinsics
-* SPIR-V's OpenCL dialect's
-  [`OpConvertFToU`](https://www.khronos.org/registry/spir-v/specs/unified1/SPIRV.html#OpConvertFToU) and
-  [`OpConvertFToS`](https://www.khronos.org/registry/spir-v/specs/unified1/SPIRV.html#OpConvertFToS)
-  instructions when decorated with
-  [the `SaturatedConversion` decorator](https://www.khronos.org/registry/spir-v/specs/unified1/SPIRV.html#_a_id_decoration_a_decoration).
-* WebAssembly has also introduced
- [trunc_sat_u](ttps://webassembly.github.io/spec/core/exec/numerics.html#op-trunc-sat-u) and
- [trunc_sat_s](https://webassembly.github.io/spec/core/exec/numerics.html#op-trunc-sat-s)
-
-* **JavaScript conversion**
-
-For the sake of simplicity, the FP -> Integer conversion semantics generalized from those used by JavaScripts's `ToInt32` abstract operation will be referred to as [JavaScript conversion semantics](#fp-to-int-javascript-conversion-semantics).
-
-This instruction is present in ARM assembler as FJCVTZS
-<https://developer.arm.com/documentation/dui0801/g/hko1477562192868>
-
 **Notes and Observations**:
 
-* TODO
+* These instructions are present in many other ISAs.
+* Javascript rounding as one instruction saves 35 instructions including
+  six branches.
 
 **Changes**
 
@@ -170,18 +137,24 @@ Tables that are used by `fmvtg`/`fmvfg`/`fcvttg`/`fcvtfg`:
 | PO  | RT   | 0     | FRB   | XO    | RCS   | X-Form |
 
 ```
-if RCS[0] = 1 then  # if Single mode
-    RT <- [0] * 32 || SINGLE((FRB))  # SINGLE since that's what stfs uses
-else
-    RT <- (FRB)
+    if RCS[0] = 1 then  # if Single mode
+        RT <- [0] * 32 || SINGLE((FRB))  # SINGLE since that's what stfs uses
+    else
+        RT <- (FRB)
 ```
 
-move a 32/64-bit float from a FPR to a GPR, just copying bits of the IEEE 754 representation directly. This is equivalent to `stfs` followed by `lwz` or equivalent to `stfd` followed by `ld`.
-As `fmvtg` is just copying bits, `FPSCR` is not affected in any way.
+Move a 32/64-bit float from a FPR to a GPR, just copying bits of the
+IEEE754 representation directly. This is equivalent to `stfs` followed
+by `lwz` or equivalent to `stfd` followed by `ld`.  As `fmvtg` is just
+copying bits, `FPSCR` is not affected in any way.
 
 Rc=1 tests RT and sets CR0, exactly like all other Scalar Fixed-Point
 operations.
 
+Special Registers altered:
+
+    CR1     (if Rc=1)
+
 ### Assembly Aliases
 
 | Assembly Alias    | Full Instruction   |
@@ -205,17 +178,24 @@ operations.
 | PO  | FRT  | 0     | RB    | XO    | RCS   | X-Form |
 
 ```
-if RCS[0] = 1 then  # if Single mode
-    FRT <- DOUBLE((RB)[32:63])  # DOUBLE since that's what lfs uses
-else
-    FRT <- (RB)
+    if RCS[0] = 1 then  # if Single mode
+        FRT <- DOUBLE((RB)[32:63])  # DOUBLE since that's what lfs uses
+    else
+        FRT <- (RB)
 ```
 
-move a 32/64-bit float from a GPR to a FPR, just copying bits of the IEEE 754 representation directly. This is equivalent to `stw` followed by `lfs` or equivalent to `std` followed by `lfd`. As `fmvfg` is just copying bits, `FPSCR` is not affected in any way.
+move a 32/64-bit float from a GPR to a FPR, just copying bits of the IEEE
+754 representation directly. This is equivalent to `stw` followed by `lfs`
+or equivalent to `std` followed by `lfd`. As `fmvfg` is just copying bits,
+`FPSCR` is not affected in any way.
 
 Rc=1 tests FRT and sets CR1, exactly like all other Scalar Floating-Point
 operations.
 
+Special Registers altered:
+
+    CR1     (if Rc=1)
+
 ### Assembly Aliases
 
 | Assembly Alias    | Full Instruction   |
@@ -238,52 +218,57 @@ operations.
 `fcvtfg FRT, RB, IT, RCS`
 
 ```
-if IT[0] = 0 and RCS[0] = 0 then  # 32-bit int -> 64-bit float
-    # rounding never necessary, so don't touch FPSCR
-    # based off xvcvsxwdp
-    if IT = 0 then  # Signed 32-bit
-        src <- bfp_CONVERT_FROM_SI32((RB)[32:63])
-    else  # IT = 1 -- Unsigned 32-bit
-        src <- bfp_CONVERT_FROM_UI32((RB)[32:63])
-    FRT <- bfp64_CONVERT_FROM_BFP(src)
-else
-    # rounding may be necessary
-    # based off xscvuxdsp
-    reset_xflags()
-    switch(IT)
-        case(0):  # Signed 32-bit
+    if IT[0] = 0 and RCS[0] = 0 then  # 32-bit int -> 64-bit float
+        # rounding never necessary, so don't touch FPSCR
+        # based off xvcvsxwdp
+        if IT = 0 then  # Signed 32-bit
             src <- bfp_CONVERT_FROM_SI32((RB)[32:63])
-        case(1):  # Unsigned 32-bit
+        else  # IT = 1 -- Unsigned 32-bit
             src <- bfp_CONVERT_FROM_UI32((RB)[32:63])
-        case(2):  # Signed 64-bit
-            src <- bfp_CONVERT_FROM_SI64((RB))
-        default:  # Unsigned 64-bit
-            src <- bfp_CONVERT_FROM_UI64((RB))
-    if RCS[0] = 1 then  # Single
-        rnd <- bfp_ROUND_TO_BFP32(FPSCR.RN, src)
-        result32 <- bfp32_CONVERT_FROM_BFP(rnd)
-        cls <- fprf_CLASS_BFP32(result32)
-        result <- DOUBLE(result32)
+        FRT <- bfp64_CONVERT_FROM_BFP(src)
     else
-        rnd <- bfp_ROUND_TO_BFP64(FPSCR.RN, src)
-        result <- bfp64_CONVERT_FROM_BFP(rnd)
-        cls <- fprf_CLASS_BFP64(result)
-
-    if xx_flag = 1 then SetFX(FPSCR.XX)
-
-    FRT <- result
-    FPSCR.FPRF <- cls
-    FPSCR.FR <- inc_flag
-    FPSCR.FI <- xx_flag
+        # rounding may be necessary. based off xscvuxdsp
+        reset_xflags()
+        switch(IT)
+            case(0):  # Signed 32-bit
+                src <- bfp_CONVERT_FROM_SI32((RB)[32:63])
+            case(1):  # Unsigned 32-bit
+                src <- bfp_CONVERT_FROM_UI32((RB)[32:63])
+            case(2):  # Signed 64-bit
+                src <- bfp_CONVERT_FROM_SI64((RB))
+            default:  # Unsigned 64-bit
+                src <- bfp_CONVERT_FROM_UI64((RB))
+        if RCS[0] = 1 then  # Single
+            rnd <- bfp_ROUND_TO_BFP32(FPSCR.RN, src)
+            result32 <- bfp32_CONVERT_FROM_BFP(rnd)
+            cls <- fprf_CLASS_BFP32(result32)
+            result <- DOUBLE(result32)
+        else
+            rnd <- bfp_ROUND_TO_BFP64(FPSCR.RN, src)
+            result <- bfp64_CONVERT_FROM_BFP(rnd)
+            cls <- fprf_CLASS_BFP64(result)
+        if xx_flag = 1 then SetFX(FPSCR.XX)
+        FRT <- result
+        FPSCR.FPRF <- cls
+        FPSCR.FR <- inc_flag
+        FPSCR.FI <- xx_flag
 ```
 
-Convert from a unsigned/signed 32/64-bit integer in RB to a 32/64-bit float in FRT, following the usual 32-bit float in 64-bit float format.
-
-If converting from a unsigned/signed 32-bit integer to a 64-bit float, rounding is never necessary, so `FPSCR` is unmodified and exceptions are never raised. Otherwise, `FPSCR` is modified and exceptions are raised as usual.
+Convert from a unsigned/signed 32/64-bit integer in RB to a 32/64-bit
+float in FRT, following the usual 32-bit float in 64-bit float format.
+If converting from a unsigned/signed 32-bit integer to a 64-bit float,
+rounding is never necessary, so `FPSCR` is unmodified and exceptions are
+never raised. Otherwise, `FPSCR` is modified and exceptions are raised
+as usual.
 
 Rc=1 tests FRT and sets CR1, exactly like all other Scalar Floating-Point
 operations.
 
+Special Registers altered:
+
+    CR1     (if Rc=1)
+    FPCSR   (TODO: which bits?)
+
 ### Assembly Aliases
 
 | Assembly Alias       | Full Instruction       |
@@ -314,30 +299,38 @@ operations.
 
 <div id="fpr-to-gpr-conversion-mode"></div>
 
-IEEE 754 doesn't specify what results are obtained when converting a NaN or out-of-range floating-point value to integer, so different programming languages and ISAs have made different choices.  Below is an overview
+IEEE 754 doesn't specify what results are obtained when converting a NaN
+or out-of-range floating-point value to integer, so different programming
+languages and ISAs have made different choices.  Below is an overview
 of the different variants, listing the languages and hardware that
 implements each variant.
 
-For convenience, we will give those different conversion semantics names based on which common ISA or programming language uses them, since there may not be an established name for them:
+For convenience, we will give those different conversion semantics names
+based on which common ISA or programming language uses them, since there
+may not be an established name for them:
 
 **Standard OpenPower conversion**
 
-This conversion performs "saturation with NaN converted to minimum valid integer". This
-is also exactly the same as the x86 ISA conversion semantics.
-OpenPOWER however has instructions for both:
+This conversion performs "saturation with NaN converted to minimum
+valid integer". This is also exactly the same as the x86 ISA conversion
+semantics.  OpenPOWER however has instructions for both:
 
 * rounding mode read from FPSCR
 * rounding mode always set to truncate
 
 **Java/Saturating conversion**
 
-For the sake of simplicity, the FP -> Integer conversion semantics generalized from those used by Java's semantics (and Rust's `as` operator) will be referred to as
-[Java/Saturating conversion semantics](#fp-to-int-java-saturating-conversion-semantics).
+For the sake of simplicity, the FP -> Integer conversion semantics
+generalized from those used by Java's semantics (and Rust's `as`
+operator) will be referred to as [Java/Saturating conversion
+semantics](#fp-to-int-java-saturating-conversion-semantics).
 
-Those same semantics are used in some way by all of the following languages (not necessarily for the default conversion method):
+Those same semantics are used in some way by all of the following
+languages (not necessarily for the default conversion method):
 
 * Java's
-  [FP -> Integer conversion](https://docs.oracle.com/javase/specs/jls/se16/html/jls-5.html#jls-5.1.3) (only for ling/int results)
+  [FP -> Integer conversion](https://docs.oracle.com/javase/specs/jls/se16/html/jls-5.html#jls-5.1.3)
+  (only for ling/int results)
 * Rust's FP -> Integer conversion using the
   [`as` operator](https://doc.rust-lang.org/reference/expressions/operator-expr.html#semantics)
 * LLVM's
@@ -354,7 +347,10 @@ Those same semantics are used in some way by all of the following languages (not
 
 **JavaScript conversion**
 
-For the sake of simplicity, the FP -> Integer conversion semantics generalized from those used by JavaScripts's `ToInt32` abstract operation will be referred to as [JavaScript conversion semantics](#fp-to-int-javascript-conversion-semantics).
+For the sake of simplicity, the FP -> Integer conversion
+semantics generalized from those used by JavaScripts's `ToInt32`
+abstract operation will be referred to as [JavaScript conversion
+semantics](#fp-to-int-javascript-conversion-semantics).
 
 This instruction is present in ARM assembler as FJCVTZS
 <https://developer.arm.com/documentation/dui0801/g/hko1477562192868>
@@ -387,17 +383,18 @@ Key for pseudo-code:
 | `rint(fp, rounding_mode)` | `fp`        | rounds the floating-point value `fp` to an integer according to rounding mode `rounding_mode`      |
 
 <div id="fp-to-int-openpower-conversion-semantics"></div>
-OpenPower conversion semantics (section A.2 page 1009 (page 1035) of Power ISA v3.1B):
+OpenPower conversion semantics (section A.2 page 1009 (page 1035) of
+Power ISA v3.1B):
 
 ```
-def fp_to_int_open_power<fp, int>(v: fp) -> int:
-    if v is NaN:
-        return int::MIN_VALUE
-    if v >= int::MAX_VALUE:
-        return int::MAX_VALUE
-    if v <= int::MIN_VALUE:
-        return int::MIN_VALUE
-    return (int)rint(v, rounding_mode)
+    def fp_to_int_open_power<fp, int>(v: fp) -> int:
+        if v is NaN:
+            return int::MIN_VALUE
+        if v >= int::MAX_VALUE:
+            return int::MAX_VALUE
+        if v <= int::MIN_VALUE:
+            return int::MIN_VALUE
+        return (int)rint(v, rounding_mode)
 ```
 
 <div id="fp-to-int-java-saturating-conversion-semantics"></div>
@@ -407,28 +404,29 @@ def fp_to_int_open_power<fp, int>(v: fp) -> int:
 (with adjustment to add non-truncate rounding modes):
 
 ```
-def fp_to_int_java_saturating<fp, int>(v: fp) -> int:
-    if v is NaN:
-        return 0
-    if v >= int::MAX_VALUE:
-        return int::MAX_VALUE
-    if v <= int::MIN_VALUE:
-        return int::MIN_VALUE
-    return (int)rint(v, rounding_mode)
+    def fp_to_int_java_saturating<fp, int>(v: fp) -> int:
+        if v is NaN:
+            return 0
+        if v >= int::MAX_VALUE:
+            return int::MAX_VALUE
+        if v <= int::MIN_VALUE:
+            return int::MIN_VALUE
+        return (int)rint(v, rounding_mode)
 ```
 
 <div id="fp-to-int-javascript-conversion-semantics"></div>
 Section 7.1 of the ECMAScript / JavaScript
-[conversion semantics](https://262.ecma-international.org/11.0/#sec-toint32) (with adjustment to add non-truncate rounding modes):
+[conversion semantics](https://262.ecma-international.org/11.0/#sec-toint32)
+(with adjustment to add non-truncate rounding modes):
 
 ```
-def fp_to_int_java_script<fp, int>(v: fp) -> int:
-    if v is NaN or infinite:
-        return 0
-    v = rint(v, rounding_mode)  # assume no loss of precision in result
-    v = v mod int::VALUE_COUNT  # 2^32 for i32, 2^64 for i64, result is non-negative
-    bits = (uint)v
-    return (int)bits
+    def fp_to_int_java_script<fp, int>(v: fp) -> int:
+        if v is NaN or infinite:
+            return 0
+        v = rint(v, rounding_mode)  # assume no loss of precision in result
+        v = v mod int::VALUE_COUNT  # 2^32 for i32, 2^64 for i64, result is non-negative
+        bits = (uint)v
+        return (int)bits
 ```
 
 
@@ -447,123 +445,131 @@ def fp_to_int_java_script<fp, int>(v: fp) -> int:
 `fcvttgo RT, FRB, CVM, IT, RCS`
 
 ```
-# based on xscvdpuxws
-reset_xflags()
-
-if RCS[0] = 1 then  # if Single mode
-    src <- bfp_CONVERT_FROM_BFP32(SINGLE((FRB)))
-else
-    src <- bfp_CONVERT_FROM_BFP64((FRB))
-
-switch(IT)
-    case(0):  # Signed 32-bit
-        range_min <- bfp_CONVERT_FROM_SI32(0x8000_0000)
-        range_max <- bfp_CONVERT_FROM_SI32(0x7FFF_FFFF)
-        js_mask <- 0xFFFF_FFFF
-    case(1):  # Unsigned 32-bit
-        range_min <- bfp_CONVERT_FROM_UI32(0)
-        range_max <- bfp_CONVERT_FROM_UI32(0xFFFF_FFFF)
-        js_mask <- 0xFFFF_FFFF
-    case(2):  # Signed 64-bit
-        range_min <- bfp_CONVERT_FROM_SI64(-0x8000_0000_0000_0000)
-        range_max <- bfp_CONVERT_FROM_SI64(0x7FFF_FFFF_FFFF_FFFF)
-        js_mask <- 0xFFFF_FFFF_FFFF_FFFF
-    default:  # Unsigned 64-bit
-        range_min <- bfp_CONVERT_FROM_UI64(0)
-        range_max <- bfp_CONVERT_FROM_UI64(0xFFFF_FFFF_FFFF_FFFF)
-        js_mask <- 0xFFFF_FFFF_FFFF_FFFF
-
-if CVM[2] = 1 or FPSCR.RN = 0b01 then
-    rnd <- bfp_ROUND_TO_INTEGER_TRUNC(src)
-else if FPSCR.RN = 0b00 then
-    rnd <- bfp_ROUND_TO_INTEGER_NEAR_EVEN(src)
-else if FPSCR.RN = 0b10 then
-    rnd <- bfp_ROUND_TO_INTEGER_CEIL(src)
-else if FPSCR.RN = 0b11 then
-    rnd <- bfp_ROUND_TO_INTEGER_FLOOR(src)
-
-switch(CVM)
-    case(0, 1):  # OpenPower semantics
-        if IsNaN(rnd) then
-            result <- si64_CONVERT_FROM_BFP(range_min)
-        else if bfp_COMPARE_GT(rnd, range_max) then
-            result <- ui64_CONVERT_FROM_BFP(range_max)
-        else if bfp_COMPARE_LT(rnd, range_min) then
-            result <- si64_CONVERT_FROM_BFP(range_min)
-        else if IT[1] = 1 then  # Unsigned 32/64-bit
-            result <- ui64_CONVERT_FROM_BFP(range_max)
-        else  # Signed 32/64-bit
-            result <- si64_CONVERT_FROM_BFP(range_max)
-    case(2, 3):  # Java/Saturating semantics
-        if IsNaN(rnd) then
-            result <- [0] * 64
-        else if bfp_COMPARE_GT(rnd, range_max) then
-            result <- ui64_CONVERT_FROM_BFP(range_max)
-        else if bfp_COMPARE_LT(rnd, range_min) then
-            result <- si64_CONVERT_FROM_BFP(range_min)
-        else if IT[1] = 1 then  # Unsigned 32/64-bit
-            result <- ui64_CONVERT_FROM_BFP(range_max)
-        else  # Signed 32/64-bit
-            result <- si64_CONVERT_FROM_BFP(range_max)
-    default:  # JavaScript semantics
-        # CVM = 6, 7 are illegal instructions
-
-        # this works because the largest type we try to
-        # convert from has 53 significand bits, and the
-        # largest type we try to convert to has 64 bits,
-        # and the sum of those is strictly less than the
-        # 128 bits of the intermediate result.
-        limit <- bfp_CONVERT_FROM_UI128([1] * 128)
-        if IsInf(rnd) or IsNaN(rnd) then
-            result <- [0] * 64
-        else if bfp_COMPARE_GT(bfp_ABSOLUTE(rnd), limit) then
-            result <- [0] * 64
-        else
-            result128 <- si128_CONVERT_FROM_BFP(rnd)
-            result <- result128[64:127] & js_mask
-
-switch(IT)
-    case(0):  # Signed 32-bit
-        result <- EXTS64(result[32:63])
-        result_bfp <- bfp_CONVERT_FROM_SI32(result[32:63])
-    case(1):  # Unsigned 32-bit
-        result <- EXTZ64(result[32:63])
-        result_bfp <- bfp_CONVERT_FROM_UI32(result[32:63])
-    case(2):  # Signed 64-bit
-        result_bfp <- bfp_CONVERT_FROM_SI64(result)
-    default:  # Unsigned 64-bit
-        result_bfp <- bfp_CONVERT_FROM_UI64(result)
-
-if vxsnan_flag = 1 then SetFX(FPSCR.VXSNAN)
-if vxcvi_flag = 1 then SetFX(FPSCR.VXCVI)
-if xx_flag = 1 then SetFX(FPSCR.XX)
-
-vx_flag <- vxsnan_flag | vxcvi_flag
-vex_flag <- FPSCR.VE & vx_flag
-
-if vex_flag = 0 then
-    RT <- result
-    FPSCR.FPRF <- undefined
-    FPSCR.FR <- inc_flag
-    FPSCR.FI <- xx_flag
-    if IsNaN(src) or not bfp_COMPARE_EQ(src, result_bfp) then
-        overflow <- 1  # signals SO only when OE = 1
-else
-    FPSCR.FR <- 0
-    FPSCR.FI <- 0
+    # based on xscvdpuxws
+    reset_xflags()
+
+    if RCS[0] = 1 then  # if Single mode
+        src <- bfp_CONVERT_FROM_BFP32(SINGLE((FRB)))
+    else
+        src <- bfp_CONVERT_FROM_BFP64((FRB))
+
+    switch(IT)
+        case(0):  # Signed 32-bit
+            range_min <- bfp_CONVERT_FROM_SI32(0x8000_0000)
+            range_max <- bfp_CONVERT_FROM_SI32(0x7FFF_FFFF)
+            js_mask <- 0xFFFF_FFFF
+        case(1):  # Unsigned 32-bit
+            range_min <- bfp_CONVERT_FROM_UI32(0)
+            range_max <- bfp_CONVERT_FROM_UI32(0xFFFF_FFFF)
+            js_mask <- 0xFFFF_FFFF
+        case(2):  # Signed 64-bit
+            range_min <- bfp_CONVERT_FROM_SI64(-0x8000_0000_0000_0000)
+            range_max <- bfp_CONVERT_FROM_SI64(0x7FFF_FFFF_FFFF_FFFF)
+            js_mask <- 0xFFFF_FFFF_FFFF_FFFF
+        default:  # Unsigned 64-bit
+            range_min <- bfp_CONVERT_FROM_UI64(0)
+            range_max <- bfp_CONVERT_FROM_UI64(0xFFFF_FFFF_FFFF_FFFF)
+            js_mask <- 0xFFFF_FFFF_FFFF_FFFF
+
+    if CVM[2] = 1 or FPSCR.RN = 0b01 then
+        rnd <- bfp_ROUND_TO_INTEGER_TRUNC(src)
+    else if FPSCR.RN = 0b00 then
+        rnd <- bfp_ROUND_TO_INTEGER_NEAR_EVEN(src)
+    else if FPSCR.RN = 0b10 then
+        rnd <- bfp_ROUND_TO_INTEGER_CEIL(src)
+    else if FPSCR.RN = 0b11 then
+        rnd <- bfp_ROUND_TO_INTEGER_FLOOR(src)
+
+    switch(CVM)
+        case(0, 1):  # OpenPower semantics
+            if IsNaN(rnd) then
+                result <- si64_CONVERT_FROM_BFP(range_min)
+            else if bfp_COMPARE_GT(rnd, range_max) then
+                result <- ui64_CONVERT_FROM_BFP(range_max)
+            else if bfp_COMPARE_LT(rnd, range_min) then
+                result <- si64_CONVERT_FROM_BFP(range_min)
+            else if IT[1] = 1 then  # Unsigned 32/64-bit
+                result <- ui64_CONVERT_FROM_BFP(range_max)
+            else  # Signed 32/64-bit
+                result <- si64_CONVERT_FROM_BFP(range_max)
+        case(2, 3):  # Java/Saturating semantics
+            if IsNaN(rnd) then
+                result <- [0] * 64
+            else if bfp_COMPARE_GT(rnd, range_max) then
+                result <- ui64_CONVERT_FROM_BFP(range_max)
+            else if bfp_COMPARE_LT(rnd, range_min) then
+                result <- si64_CONVERT_FROM_BFP(range_min)
+            else if IT[1] = 1 then  # Unsigned 32/64-bit
+                result <- ui64_CONVERT_FROM_BFP(range_max)
+            else  # Signed 32/64-bit
+                result <- si64_CONVERT_FROM_BFP(range_max)
+        default:  # JavaScript semantics
+            # CVM = 6, 7 are illegal instructions
+
+            # this works because the largest type we try to
+            # convert from has 53 significand bits, and the
+            # largest type we try to convert to has 64 bits,
+            # and the sum of those is strictly less than the
+            # 128 bits of the intermediate result.
+            limit <- bfp_CONVERT_FROM_UI128([1] * 128)
+            if IsInf(rnd) or IsNaN(rnd) then
+                result <- [0] * 64
+            else if bfp_COMPARE_GT(bfp_ABSOLUTE(rnd), limit) then
+                result <- [0] * 64
+            else
+                result128 <- si128_CONVERT_FROM_BFP(rnd)
+                result <- result128[64:127] & js_mask
+
+    switch(IT)
+        case(0):  # Signed 32-bit
+            result <- EXTS64(result[32:63])
+            result_bfp <- bfp_CONVERT_FROM_SI32(result[32:63])
+        case(1):  # Unsigned 32-bit
+            result <- EXTZ64(result[32:63])
+            result_bfp <- bfp_CONVERT_FROM_UI32(result[32:63])
+        case(2):  # Signed 64-bit
+            result_bfp <- bfp_CONVERT_FROM_SI64(result)
+        default:  # Unsigned 64-bit
+            result_bfp <- bfp_CONVERT_FROM_UI64(result)
+
+    if vxsnan_flag = 1 then SetFX(FPSCR.VXSNAN)
+    if vxcvi_flag = 1 then SetFX(FPSCR.VXCVI)
+    if xx_flag = 1 then SetFX(FPSCR.XX)
+
+    vx_flag <- vxsnan_flag | vxcvi_flag
+    vex_flag <- FPSCR.VE & vx_flag
+
+    if vex_flag = 0 then
+        RT <- result
+        FPSCR.FPRF <- undefined
+        FPSCR.FR <- inc_flag
+        FPSCR.FI <- xx_flag
+        if IsNaN(src) or not bfp_COMPARE_EQ(src, result_bfp) then
+            overflow <- 1  # signals SO only when OE = 1
+    else
+        FPSCR.FR <- 0
+        FPSCR.FI <- 0
 ```
 
-Convert from 32/64-bit float in FRB to a unsigned/signed 32/64-bit integer in RT, with the conversion overflow/rounding semantics following the chosen `CVM` value, following the usual 32-bit float in 64-bit float format.
+Convert from 32/64-bit float in FRB to a unsigned/signed 32/64-bit integer
+in RT, with the conversion overflow/rounding semantics following the
+chosen `CVM` value, following the usual 32-bit float in 64-bit float
+format.
 
 `FPSCR` is modified and exceptions are raised as usual.
 
-Both of these instructions have an Rc=1 mode which sets CR0
-in the normal way for any instructions producing a GPR result.
-Additionally, when OE=1, if the numerical value of the FP number
-is not 100% accurately preserved (due to truncation or saturation
-and including when the FP number was NaN) then this is considered
-to be an integer Overflow condition, and CR0.SO, XER.SO and XER.OV
-are all set as normal for any GPR instructions that overflow.
+Both of these instructions have an Rc=1 mode which sets CR0 in the normal
+way for any instructions producing a GPR result.  Additionally, when OE=1,
+if the numerical value of the FP number is not 100% accurately preserved
+(due to truncation or saturation and including when the FP number was
+NaN) then this is considered to be an integer Overflow condition, and
+CR0.SO, XER.SO and XER.OV are all set as normal for any GPR instructions
+that overflow.
+
+Special Registers altered:
+
+    CR0              (if Rc=1)
+    XER SO, OV, OV32 (if OE=1)
 
 ----------
 
@@ -597,7 +603,6 @@ For brevity, `[o]` is used to mean `o` is optional there.
 
 \newpage{}
 
-
 ----------
 
 # Appendices