diff --git a/xen/arch/x86/hvm/svm/svm.c b/xen/arch/x86/hvm/svm/svm.c
index cd6a6b382b..0eac9ce4c6 100644
--- a/xen/arch/x86/hvm/svm/svm.c
+++ b/xen/arch/x86/hvm/svm/svm.c
@@ -627,21 +627,21 @@ static void svm_cpuid_policy_changed(struct vcpu *v)
                       cp->extd.ibpb ? MSR_INTERCEPT_NONE : MSR_INTERCEPT_RW);
 }
 
-static void svm_sync_vmcb(struct vcpu *v, enum vmcb_sync_state new_state)
+void svm_sync_vmcb(struct vcpu *v, enum vmcb_sync_state new_state)
 {
     struct svm_vcpu *svm = &v->arch.hvm.svm;
 
     if ( new_state == vmcb_needs_vmsave )
     {
         if ( svm->vmcb_sync_state == vmcb_needs_vmload )
-            svm_vmload(svm->vmcb);
+            svm_vmload_pa(svm->vmcb_pa);
 
         svm->vmcb_sync_state = new_state;
     }
     else
     {
         if ( svm->vmcb_sync_state == vmcb_needs_vmsave )
-            svm_vmsave(svm->vmcb);
+            svm_vmsave_pa(svm->vmcb_pa);
 
         if ( svm->vmcb_sync_state != vmcb_needs_vmload )
             svm->vmcb_sync_state = new_state;
diff --git a/xen/arch/x86/hvm/svm/svmdebug.c b/xen/arch/x86/hvm/svm/svmdebug.c
index d35e40596b..4293d8dba5 100644
--- a/xen/arch/x86/hvm/svm/svmdebug.c
+++ b/xen/arch/x86/hvm/svm/svmdebug.c
@@ -29,6 +29,15 @@ static void svm_dump_sel(const char *name, const struct segment_register *s)
 
 void svm_vmcb_dump(const char *from, const struct vmcb_struct *vmcb)
 {
+    struct vcpu *curr = current;
+
+    /*
+     * If we are dumping the VMCB currently in context, some guest state may
+     * still be cached in hardware.  Retrieve it.
+     */
+    if ( vmcb == curr->arch.hvm.svm.vmcb )
+        svm_sync_vmcb(curr, vmcb_in_sync);
+
     printk("Dumping guest's current state at %s...\n", from);
     printk("Size of VMCB = %zu, paddr = %"PRIpaddr", vaddr = %p\n",
            sizeof(struct vmcb_struct), virt_to_maddr(vmcb), vmcb);
diff --git a/xen/include/asm-x86/hvm/svm/svmdebug.h b/xen/include/asm-x86/hvm/svm/svmdebug.h
index 658cdd3836..330c1d91aa 100644
--- a/xen/include/asm-x86/hvm/svm/svmdebug.h
+++ b/xen/include/asm-x86/hvm/svm/svmdebug.h
@@ -22,6 +22,7 @@
 #include <asm/types.h>
 #include <asm/hvm/svm/vmcb.h>
 
+void svm_sync_vmcb(struct vcpu *v, enum vmcb_sync_state new_state);
 void svm_vmcb_dump(const char *from, const struct vmcb_struct *vmcb);
 bool svm_vmcb_isvalid(const char *from, const struct vmcb_struct *vmcb,
                       const struct vcpu *v, bool verbose);