It turned out that the result of calling ticks_us() was always either odd
or even, depending on some internal state during boot. So the us-counter
was set to a 2 MHz input and the result shifted by 1. The counting period
is still long enough, since internally a (now) 63 bit value is used for us.
4160ec087b