[coreboot] Device number to use with testbios & lspci output difference between Commercial BIOS and coreboot