mulRecFNToRaw

in hardfloat_sys

extern entity mulRecFNToRaw<#uint expWidth, #uint sigWidth>(
    control: uint<1>,
    a: uint<{expWidth + sigWidth + 1}>,
    b: uint<{expWidth + sigWidth + 1}>,
    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 multiplication 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.