int32_t __int32_mul_16x16(int16_t muliplicand, int16_t multiplier);
this multiplies multiplicand by multiplier and returns the 32-bit signed product as the result.