# A.1 Floating-Point Round to Single-Precision Model

The following describes algorithmically the operation of the Floating
Round to Single-Precision instruction.

<!-- OPF_PowerISA_v3.1B.pdf Book I Section A.1 page 1005-1008(1031-1034) -->

    def FRSP(FRB):
        if ((FRB)[1:11] <u 897) & ((FRB)[1:63] >u 0) then
            if FPSCR[UE] = 0 then
                return FRSP_Disabled_Exponent_Underflow(FRB)
            if FPSCR[UE] = 1 then
                return FRSP_Enabled_Exponent_Underflow(FRB)

        if ((FRB)[1:11] >u 1150) & ((FRB)[1:11] <u 2047) then
            if FPSCR[OE] = 0 then
                return FRSP_Disabled_Exponent_Overflow(FRB)
            if FPSCR[OE] = 1 then
                return FRSP_Enabled_Exponent_Overflow(FRB)

        if ((FRB)[1:11] >u 896) & ((FRB)[1:11] <u 1151) then
            return FRSP_Normal_Operand(FRB)

        if (FRB)[1:63] = 0 then
            return FRSP_Zero_Operand(FRB)

        if (FRB)[1:11] = 2047 then
            if (FRB)[12:63] = 0 then
                return FRSP_Infinity_Operand(FRB)
            if (FRB)[12] = 1 then
                return FRSP_QNaN_Operand(FRB)
            if ((FRB)[12] = 0) & ((FRB)[13:63] >u 0) then
                return FRSP_SNaN_Operand(FRB)

    def FRSP_Disabled_Exponent_Underflow(FRB):
        sign <- (FRB)[0]
        frac[0:52] <- 0
        exp <- 0
        if (FRB)[1:11] = 0 then
            exp <- -1022
            frac[0:52] <- 0b0 || (FRB)[12:63]
        if (FRB)[1:11] >u 0 then
            exp <- (FRB)[1:11] - 1023
            frac[0:52] <- 0b1 || (FRB)[12:63]

        # Denormalize operand:
        G <- 0b0
        R <- 0b0
        X <- 0b0
        do while exp < -126
            exp <- exp + 1
            X <- X | R
            R <- G
            G <- frac[52]
            frac[0:52] <- 0b0 || frac[0:51]

        FPSCR[UX] <- (frac[24:52] || G || R || X) >u 0
        exp, frac <- Round_Single(sign, exp, frac[0:52], G, R, X)
        FPSCR[XX] <- FPSCR[XX] | FPSCR[FI]
        FRT <- [0b0] * 64
        if frac[0:52] = 0 then
            FRT[0] <- sign
            FRT[1:63] <- 0
            if sign = 0 then FPSCR[FPRF] <- '+ zero'
            if sign = 1 then FPSCR[FPRF] <- '- zero'
        if frac[0:52] >u 0 then
            if frac[0] = 1 then
                if sign = 0 then FPSCR[FPRF] <- '+ normal number'
                if sign = 1 then FPSCR[FPRF] <- '- normal number'
            if frac[0] = 0 then
                if sign = 0 then FPSCR[FPRF] <- '+ denormalized number'
                if sign = 1 then FPSCR[FPRF] <- '- denormalized number'

            # Normalize operand:
            do while frac[0] = 0
                exp <- exp-1
                frac[0:52] <- frac[1:52] || 0b0

            FRT[0] <- sign
            FRT[1:11] <- exp + 1023
            FRT[12:63] <- frac[1:52]
        return FRT

    def FRSP_Enabled_Exponent_Underflow(FRB):
        FPSCR[UX] <- 1
        sign <- (FRB)[0]
        frac <- [0b0] * 53
        exp <- 0
        if (FRB)[1:11] = 0 then
            exp <- -1022
            frac[0:52] <- 0b0 || (FRB)[12:63]
        if (FRB)[1:11] >u 0 then
            exp <- (FRB)[1:11] - 1023
            frac[0:52] <- 0b1 || (FRB)[12:63]

        # Normalize operand:
        do while frac[0] = 0
            exp <- exp - 1
            frac[0:52] <- frac[1:52] || 0b0

        exp, frac <- Round_Single(sign, exp, frac[0:52], 0b0, 0b0, 0b0)
        FPSCR[XX] <- FPSCR[XX] | FPSCR[FI]
        exp <- exp + 192
        FRT <- [0b0] * 64
        FRT[0] <- sign
        FRT[1:11] <- exp + 1023
        FRT[12:63] <- frac[1:52]
        if sign = 0 then FPSCR[FPRF] <- '+ normal number'
        if sign = 1 then FPSCR[FPRF] <- '- normal number'
        return FRT

    def FRSP_Disabled_Exponent_Overflow(FRB):
        FPSCR[OX] <- 1
        FRT <- [0b0] * 64
        if FPSCR[RN] = 0b00 then             # Round to Nearest
            if (FRB)[0] = 0 then FRT <- 0x7FF0_0000_0000_0000
            if (FRB)[0] = 1 then FRT <- 0xFFF0_0000_0000_0000
            if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ infinity'
            if (FRB)[0] = 1 then FPSCR[FPRF] <- '- infinity'
        if FPSCR[RN] = 0b01 then             # Round toward Zero
            if (FRB)[0] = 0 then FRT <- 0x47EF_FFFF_E000_0000
            if (FRB)[0] = 1 then FRT <- 0xC7EF_FFFF_E000_0000
            if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ normal number'
            if (FRB)[0] = 1 then FPSCR[FPRF] <- '- normal number'
        if FPSCR[RN] = 0b10 then             # Round toward +Infinity
            if (FRB)[0] = 0 then FRT <- 0x7FF0_0000_0000_0000
            if (FRB)[0] = 1 then FRT <- 0xC7EF_FFFF_E000_0000
            if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ infinity'
            if (FRB)[0] = 1 then FPSCR[FPRF] <- '- normal number'
        if FPSCR[RN] = 0b11 then             # Round toward -Infinity
            if (FRB)[0] = 0 then FRT <- 0x47EF_FFFF_E000_0000
            if (FRB)[0] = 1 then FRT <- 0xFFF0_0000_0000_0000
            if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ normal number'
            if (FRB)[0] = 1 then FPSCR[FPRF] <- '- infinity'
        FPSCR[FR] <- undefined(0) # FIXME: figure out what values POWER9 uses
        FPSCR[FI] <- 1
        FPSCR[XX] <- 1
        return FRT

    def FRSP_Enabled_Exponent_Overflow(FRB):
        sign <- (FRB)[0]
        exp <- (FRB)[1:11] - 1023
        frac <- [0b0] * 53
        frac[0:52] <- 0b1 || (FRB)[12:63]
        exp, frac <- Round_Single(sign, exp, frac[0:52], 0b0, 0b0, 0b0)
        FPSCR[XX] <- FPSCR[XX] | FPSCR[FI]
        # Enabled Overflow:
        FPSCR[OX] <- 1
        exp <- exp - 192
        FRT <- [0b0] * 64
        FRT[0] <- sign
        FRT[1:11] <- exp + 1023
        FRT[12:63] <- frac[1:52]
        if sign = 0 then FPSCR[FPRF] <- '+ normal number'
        if sign = 1 then FPSCR[FPRF] <- '- normal number'
        return FRT

    def FRSP_Zero_Operand(FRB):
        FRT <- (FRB)
        if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ zero'
        if (FRB)[0] = 1 then FPSCR[FPRF] <- '- zero'
        FPSCR[FRFI] <- 0b00
        return FRT

    def FRSP_Infinity_Operand(FRB):
        FRT <- (FRB)
        if (FRB)[0] = 0 then FPSCR[FPRF] <- '+ infinity'
        if (FRB)[0] = 1 then FPSCR[FPRF] <- '- infinity'
        FPSCR[FRFI] <- 0b00
        return FRT

    def FRSP_QNaN_Operand(FRB):
        FRT <- (FRB)[0:34] || [0b0] * 29
        FPSCR[FPRF] <- 'QNaN'
        FPSCR[FR] <- 0b0
        FPSCR[FI] <- 0b0
        return FRT

    def FRSP_SNaN_Operand(FRB):
        FPSCR[VXSNAN] <- 1
        FRT <- [0b0] * 64
        if FPSCR[VE] = 0 then
            FRT[0:11] <- (FRB)[0:11]
            FRT[12] <- 1
            FRT[13:63] <- (FRB)[13:34] || [0b0] * 29
            FPSCR[FPRF] <- 'QNaN'
        FPSCR[FR] <- 0b0
        FPSCR[FI] <- 0b0
        return FRT

    def FRSP_Normal_Operand(FRB):
        sign <- (FRB)[0]
        exp <- (FRB)[1:11] - 1023
        frac <- [0b0] * 53
        frac[0:52] <- 0b1 || (FRB)[12:63]
        exp, frac <- Round_Single(sign, exp, frac[0:52], 0b0, 0b0, 0b0)
        FPSCR[XX] <- FPSCR[XX] | FPSCR[FI]
        if (exp > 127) & (FPSCR[OE] = 0) then
            return FRSP_Disabled_Exponent_Overflow(FRB)
        if (exp > 127) & (FPSCR[OE] = 1) then
            return FRSP_Enabled_Overflow(FRB)
        FRT <- [0b0] * 64
        FRT[0] <- sign
        FRT[1:11] <- exp + 1023
        FRT[12:63] <- frac[1:52]
        if sign = 0 then FPSCR[FPRF] <- '+ normal number'
        if sign = 1 then FPSCR[FPRF] <- '- normal number'
        return FRT

    def Round_Single(sign, exp, frac, G, R, X):
        inc <- 0
        lsb <- frac[23]
        gbit <- frac[24]
        rbit <- frac[25]
        xbit <- (frac[26:52]||G||R||X) != 0
        if FPSCR[RN] = 0b00 then                       # Round to Nearest
            # comparisons ignore u bits
            if (lsb || gbit) = 0b11 then inc <- 1
            if (lsb || gbit || rbit) = 0b011 then inc <- 1
            if (lsb || gbit || xbit) = 0b011 then inc <- 1
        if FPSCR[RN] = 0b10 then                       # Round toward + Infinity
            # comparisons ignore u bits
            if (sign || gbit) = 0b01 then inc <- 1
            if (sign || rbit) = 0b01 then inc <- 1
            if (sign || xbit) = 0b01 then inc <- 1
        if FPSCR[RN] = 0b11 then                       # Round toward - Infinity
            # comparisons ignore u bits
            if (sign || gbit) = 0b11 then inc <- 1
            if (sign || rbit) = 0b11 then inc <- 1
            if (sign || xbit) = 0b11 then inc <- 1
        frac[0:23] <- frac[0:23] + inc
        if (inc = 1) & (frac[0:23] = 0) then
            frac[0:23] <- 0b1 || frac[0:22]
            exp <- exp + 1
        frac[24:52] <- [0b0] * 29
        FPSCR[FR] <- inc
        FPSCR[FI] <- gbit | rbit | xbit
        return exp, frac

<!-- Power ISA v3.0B p140 section 4.6.2 -->

    def DOUBLE(WORD):
        exp <- [0] * 11
        frac <- [0] * 53
        sign <- 0b0
        FRT <- [0] * 64
        # Normalized Operand
        if (WORD[1:8] >u 0) & (WORD[1:8] <u 255) then
            FRT[0:1] <- WORD[0:1]
            FRT[2] <- ¬WORD[1]
            FRT[3] <- ¬WORD[1]
            FRT[4] <- ¬WORD[1]
            FRT[5:63] <- WORD[2:31] || [0]*29
        # Denormalized Operand
        if (WORD[1:8] = 0) & (WORD[9:31] != 0) then
            sign <- WORD[0]
            exp <- -126
            frac[0:52] <- 0b0 || WORD[9:31] || [0]*29
            #normalize the operand
            do while frac[0] = 0
                frac[0:52] <- frac[1:52] || 0b0
                exp <- exp - 1
            FRT[0] <- sign
            FRT[1:11] <- exp + 1023
            FRT[12:63] <- frac[1:52]
        # Zero / Infinity / NaN
        if (WORD[1:8] = 255) | (WORD[1:31] = 0) then
            FRT[0:1] <- WORD[0:1]
            FRT[2] <- WORD[1]
            FRT[3] <- WORD[1]
            FRT[4] <- WORD[1]
            FRT[5:63] <- WORD[2:31] || [0]*29
        return FRT