using printf to print alt_u32 data

The % format codes are somewhat a C language standard. Although printf() actually is a library function and is not strictly related to the language itself, almost every compiler/C tools defines the printf function and these formats in the exactly same way.

IMHO there is no need for extra formats for alt_xx type, since they are simple integer types.

So you will always use %d or %x depending if you want them displayed in dec or hex. You could possibly use %f for float format but this makes no sense for integers.

Maybe you'd like extra format directives, i.e. %04x for printing 4 digits and padding with zeros on the left.

Example:

alt_u32 a;

a = 100;

printf("%d", a); displays "100"

printf("%x", a); displays "64"

printf("%f", a); displays "64.000000" (I'm not sure)

printf("%06x", a); displays "000064"

Look in any C library manual and you'll find all the format codes.

Cris