PCI_MSR_HI32
hi = (uint32_t)pci_conf_read(glxbase_pc, glxbase_tag, PCI_MSR_HI32);
pci_conf_write(glxbase_pc, glxbase_tag, PCI_MSR_HI32, value >> 32);