softfloat: define floatx80_round()