Multiplication: set t1 to the upper 32 bits of t2*t3 using signed multiplication