as taking a register number, and that would get multiplied by 4 to make
a register address. But the header file that consumers have to reference
this stuff publishes register addresses, not numbers. So now everything
works in terms of register addresses.
Note that the HDMI init code was writing into the wrong register before
this change. Apparently whatever it wrote to was harmless, and apparently
HDMI was working because uboot had set up the right bits.