-if(xpr64)
- RD = (uint128_t(RS1) * uint128_t(RS2)) >> 64;
+require_extension('M');
+if (xlen == 64)
+ WRITE_RD(mulhu(RS1, RS2));
else
- RD = sext32(((uint64_t)(uint32_t)RS1 * (uint64_t)(uint32_t)RS2) >> 32);
+ WRITE_RD(sext32(((uint64_t)(uint32_t)RS1 * (uint64_t)(uint32_t)RS2) >> 32));