diff --git a/src/arch/armv8m/inc/arch/vtimer.h b/src/arch/armv8m/inc/arch/vtimer.h
index d64277747..23e2737a5 100644
--- a/src/arch/armv8m/inc/arch/vtimer.h
+++ b/src/arch/armv8m/inc/arch/vtimer.h
@@ -13,10 +13,11 @@ struct vtimer {
 };
 
 struct vtimer;
+struct vcpu;
 
 void vtimer_init(struct vtimer* vtimer);
 void vtimer_reset(struct vtimer* vtimer);
 void vtimer_save_state(struct vtimer* vtimer);
-void vtimer_restore_state(struct vtimer* vtimer);
+void vtimer_restore_state(struct vcpu* vcpu, struct vtimer* vtimer);
 
 #endif /* VTIMER_H */
diff --git a/src/arch/armv8m/sau.c b/src/arch/armv8m/sau.c
index 5a5bf1c42..5281db196 100644
--- a/src/arch/armv8m/sau.c
+++ b/src/arch/armv8m/sau.c
@@ -58,12 +58,14 @@ static void sau_entry_set(struct sau_vm* sau_vm, mpid_t mpid, struct mp_region*
     unsigned long rbar = (mpr->base & SAU_RBAR_BADDR_MSK);
     unsigned long rlar = (lim & SAU_RLAR_LADDR_MSK) | mpr->mem_flags.rlar;
 
+    sau_arch_disable();
     sau->rnr = mpid;
     ISB();
     sau->rbar = rbar;
     sau_vm->entry[mpid].rbar = rbar;
     sau->rlar = rlar;
     sau_vm->entry[mpid].rlar = rlar;
+    sau_arch_enable();
 }
 
 static mpid_t sau_entry_allocate(void)
diff --git a/src/arch/armv8m/vm.c b/src/arch/armv8m/vm.c
index 0dc9d3677..40c8f4f8a 100644
--- a/src/arch/armv8m/vm.c
+++ b/src/arch/armv8m/vm.c
@@ -142,7 +142,7 @@ void vcpu_restore_state(struct vcpu* vcpu)
 
     vmpu_restore_state(&vcpu->arch.vmpu);
     // vfp_restore_state(&vcpu->regs.vfp_regs);
-    vtimer_restore_state(&vcpu->arch.vtimer);
+    vtimer_restore_state(vcpu, &vcpu->arch.vtimer);
     sau_restore(&vcpu->arch.sau_vm);
 }
 
diff --git a/src/arch/armv8m/vtimer.c b/src/arch/armv8m/vtimer.c
index a8f0ba539..de98acc66 100644
--- a/src/arch/armv8m/vtimer.c
+++ b/src/arch/armv8m/vtimer.c
@@ -2,6 +2,7 @@
 #include <vm.h>
 #include <arch/sysregs.h>
 #include <arch/systick.h>
+#include <sched.h>
 
 void vtimer_init(struct vtimer* vtimer)
 {
@@ -21,7 +22,7 @@ void vtimer_save_state(struct vtimer* vtimer)
     vtimer->cvr = systick_get_cvr(systick_ns);
 }
 
-void vtimer_restore_state(struct vtimer* vtimer)
+void vtimer_restore_state(struct vcpu* vcpu, struct vtimer* vtimer)
 {
     /* Note: Restoring the CVR implies that we simulate a new count routine, i.e., we need to
     disable the timer, reload the previous CVR value to RVR, start the count and immediately stop
@@ -32,9 +33,20 @@ void vtimer_restore_state(struct vtimer* vtimer)
     // Clear CVR
     systick_set_cvr(systick_ns, 0);
     // Set RVR with the cvr value to be restored
-    systick_set_rvr(systick_ns, vtimer->cvr);
-    // Enable the systick timer to force the reload of the cvr
-    systick_set_csr(systick_ns, systick_get_csr(systick_ns) | SYSTICK_CSR_ENABLE);
+
+    if (vcpu->first_run != 0) {
+        uint32_t vcpu_num = list_size(&cpu()->vcpu_lst);
+        uint32_t elapsed_time = (uint32_t)time_slice * (vcpu_num - 1);
+        if (vtimer->cvr < elapsed_time) {
+            systick_set_rvr(systick_ns, 1);
+        } else {
+            systick_set_rvr(systick_ns, vtimer->cvr - elapsed_time);
+        }
+
+        // Enable the systick timer to force the reload of the cvr
+        systick_set_csr(systick_ns,
+            systick_get_csr(systick_ns) | SYSTICK_CSR_ENABLE | SYSTICK_CSR_CLKSOURCE);
+    }
 
     // Restore the CSR and RVR
     systick_set_csr(systick_ns, vtimer->csr);
diff --git a/src/core/inc/sched.h b/src/core/inc/sched.h
index 541bb2d26..8ef952dcb 100644
--- a/src/core/inc/sched.h
+++ b/src/core/inc/sched.h
@@ -3,6 +3,8 @@
 
 #include <crossconhyp.h>
 
+extern const unsigned long long time_slice;
+
 void sched_start(void);
 void sched_yield(void);
 void sched_init(void);
diff --git a/src/core/sched.c b/src/core/sched.c
index f84da27ae..cf6c11cee 100644
--- a/src/core/sched.c
+++ b/src/core/sched.c
@@ -7,12 +7,14 @@
 #include <vm.h>
 #include <cpu.h>
 
+const unsigned long long time_slice = TIME_MS(10);
+
 void sched_init() { }
 
 static inline timer_value_t sched_next_event_time(void)
 {
     // hardcoded 10 ms time slice
-    return (timer_value_t)(timer_arch_get_count() + TIME_MS(10));
+    return (timer_value_t)(timer_arch_get_count() + time_slice);
 }
 
 static void sched_timer_event_handler(struct timer_event* timer_event);
diff --git a/src/core/vm.c b/src/core/vm.c
index bdb3f891a..bb7e87d0d 100644
--- a/src/core/vm.c
+++ b/src/core/vm.c
@@ -320,7 +320,7 @@ static void vm_init_dev(struct vm* vm, const struct vm_config* vm_config)
     for (size_t i = 0; i < vm_config->platform.dev_num; i++) {
         struct vm_dev_region* dev = &vm_config->platform.devs[i];
         INFO("VM %d adding MMIO region, VA: 0x%lx size: 0x%lx mapped at 0x%lx\n", vm->id, dev->va,
-            dev->va, dev->pa);
+            dev->size, dev->pa);
 
         size_t n = ALIGN(dev->size, PAGE_SIZE) / PAGE_SIZE;