hdmi_get_pixel_clock() returns the pixel clock in Hz, but the pck is
stored as kHz. This means the return value has to be multiplied by 1000,
not by 10000 as the code did.
Signed-off-by: Tomi Valkeinen <tomi.valkeinen@ti.com>