core->dbg_regs.dr7 = 0x0000000000000400LL;
 
 
-    /** THESE NEED TO BE MOVED TO GLOBAL LOCATION **/
-    v3_init_svm_io_map(core->vm_info);
     ctrl_area->IOPM_BASE_PA = (addr_t)V3_PAddr(core->vm_info->io_map.arch_data);
     ctrl_area->instrs.IOIO_PROT = 1;
-
-    v3_init_svm_msr_map(core->vm_info);
+           
     ctrl_area->MSRPM_BASE_PA = (addr_t)V3_PAddr(core->vm_info->msr_map.arch_data);
-    ctrl_area->instrs.MSR_PROT = 1;
-    /** *** **/
+    ctrl_area->instrs.MSR_PROT = 1;   
 
 
     PrintDebug("Exiting on interrupts\n");
 
 #include <palacios/vmm_dev_mgr.h>
 #include <palacios/vmm_cpuid.h>
 #include <palacios/vmm_xml.h>
+#include <palacios/vmm_io.h>
+#include <palacios/vmm_msr.h>
 
-#include <palacios/svm.h>
-#include <palacios/vmx.h>
 
 #ifdef CONFIG_SYMBIOTIC
 #include <palacios/vmm_sym_iface.h>
 #endif
 
 
+#ifdef CONFIG_SVM
+#include <palacios/svm.h>
+#include <palacios/svm_io.h>
+#include <palacios/svm_msr.h>
+#endif
+
+#ifdef CONFIG_VMX
+#include <palacios/vmx.h>
+#include <palacios/vmx_io.h>
+#include <palacios/vmx_msr.h>
+#endif
+
+
 #include <palacios/vmm_host_events.h>
 #include <palacios/vmm_socket.h>
 
 }
 
 static int pre_config_vm(struct v3_vm_info * vm, v3_cfg_tree_t * vm_cfg) {
+    v3_cpu_arch_t cpu_type = v3_get_cpu_type(v3_get_cpu_id());
+
     char * memory_str = v3_cfg_val(vm_cfg, "memory");
     char * schedule_hz_str = v3_cfg_val(vm_cfg, "schedule_hz");
     char * vm_class = v3_cfg_val(vm_cfg, "class");
     v3_init_sym_swap(vm);
 #endif
 
+
+       // init SVM/VMX
+#ifdef CONFIG_SVM
+       if ((cpu_type == V3_SVM_CPU) || (cpu_type == V3_SVM_REV3_CPU)) {
+           v3_init_svm_io_map(vm);
+           v3_init_svm_msr_map(vm);
+       }
+#endif
+#ifdef CONFIG_VMX
+       else if ((cpu_type == V3_VMX_CPU) || (cpu_type == V3_VMX_EPT_CPU)) {
+           v3_init_vmx_io_map(vm);
+           v3_init_vmx_msr_map(vm);
+       }
+#endif
+       else {
+           PrintError("Invalid CPU Type\n");
+           return -1;
+       }
+
    if (schedule_hz_str) {
        sched_hz = atoi(schedule_hz_str);
     }