addRecFNToRaw

in hardfloat_sys

extern entity addRecFNToRaw<#uint expWidth, #uint sigWidth>(
    control: uint<1>,
    subOp: bool,
    a: uint<{expWidth + sigWidth + 1}>,
    b: uint<{expWidth + sigWidth + 1}>,
    roundingMode: uint<3>,
    invalidExc: inv &bool,
    out_isNaN: inv &bool,
    out_isInf: inv &bool,
    out_isZero: inv &bool,
    out_sign: inv &bool,
    out_sExp: inv &int<{expWidth + 2}>,
    out_sig: inv &uint<{sigWidth + 3}>
);

Description taken from the Berkeley Hardfloat documentation:

Returns the intermediate result of addition or subtraction before rounding, as a “raw” deconstructed floating-point value with two extra bits of significand. Boolean output invalidExc is true if the operation should raise an invalid exception. Module roundRawFNToRecFN can be used to round the intermediate result in conformance with the IEEE Standard.