Use correct inttypes.h format specifier

The type here is uint32_t which should use PRIx32, not plain %x which is
for an int, we've just gotten away with it so far.

Signed-off-by: David Gibson <david@gibson.dropbear.id.au>