Revert "whitespace cleanup on ls006, remove duplication,"
authorJacob Lifshay <programmerjake@gmail.com>
Wed, 22 Mar 2023 20:10:08 +0000 (13:10 -0700)
committerJacob Lifshay <programmerjake@gmail.com>
Wed, 22 Mar 2023 20:10:08 +0000 (13:10 -0700)
I can't read the commitdiff, so I'm reverting and reapplying it as a set of split-up commits.

This reverts commit d827d9e11ce635d52652f8936a454319fa2ebea9.

openpower/sv/rfc/ls006.mdwn

index 1d7b3bb49c95031e50bea3dec40a1857ee753643..a25d148432cdd4591697f2858ee34c7fdfb6a8e9 100644 (file)
@@ -56,23 +56,56 @@ 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**:
 
-* These instructions are present in many other ISAs.
-* Javascript rounding as one instruction saves 35 instructions including
-  six branches.
+* TODO
 
 **Changes**
 
@@ -137,24 +170,18 @@ 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
-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.
+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.
 
 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   |
@@ -178,24 +205,17 @@ Special Registers altered:
 | 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   |
@@ -218,57 +238,52 @@ Special Registers altered:
 `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
+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
             src <- bfp_CONVERT_FROM_SI32((RB)[32:63])
-        else  # IT = 1 -- Unsigned 32-bit
+        case(1):  # Unsigned 32-bit
             src <- bfp_CONVERT_FROM_UI32((RB)[32:63])
-        FRT <- bfp64_CONVERT_FROM_BFP(src)
+        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
-        # 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
+        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       |
@@ -299,38 +314,30 @@ Special Registers altered:
 
 <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
@@ -347,10 +354,7 @@ languages (not necessarily for the default conversion method):
 
 **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>
@@ -383,18 +387,17 @@ 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>
@@ -404,29 +407,28 @@ Power ISA v3.1B):
 (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
 ```
 
 
@@ -445,131 +447,123 @@ Section 7.1 of the ECMAScript / JavaScript
 `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.
-
-Special Registers altered:
-
-    CR0              (if Rc=1)
-    XER SO, OV, OV32 (if OE=1)
+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.
 
 ----------
 
@@ -603,6 +597,7 @@ For brevity, `[o]` is used to mean `o` is optional there.
 
 \newpage{}
 
+
 ----------
 
 # Appendices