+ v = (uint64_t)a0 * (uint64_t)b0;
+ *plow = v;
+ *phigh = 0;
+
+ v = (uint64_t)a0 * (uint64_t)b1;
+ add128(plow, phigh, v << 32, v >> 32);
+
+ v = (uint64_t)a1 * (uint64_t)b0;
+ add128(plow, phigh, v << 32, v >> 32);
+
+ v = (uint64_t)a1 * (uint64_t)b1;
+ *phigh += v;