[LinuxBIOS] usage of pci_write_config32()?