diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index 1aa2f58..1fa1413 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -123,22 +123,22 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         goto read_as_zero;
     case GICR_SETLPIR:
         /* WO. Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_CLRLPIR:
         /* WO. Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_PROPBASER:
         /* LPI's not implemented */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_PENDBASER:
         /* LPI's not implemented */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_INVLPIR:
         /* WO. Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_INVALLR:
         /* WO. Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
         return 0;
     case GICR_SYNCR:
         if ( dabt.size != DABT_WORD ) goto bad_width;
@@ -147,10 +147,10 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         return 1;
     case GICR_MOVLPIR:
         /* WO Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_MOVALLR:
         /* WO Read as zero */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICR_PIDR0:
         if ( dabt.size != DABT_WORD ) goto bad_width;
         *r = GICV3_GICR_PIDR0;
@@ -184,13 +184,9 @@ bad_width:
     domain_crash_synchronous();
     return 0;
 
-read_as_zero_64:
-    if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
-    *r = 0;
-    return 1;
-
 read_as_zero:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG, "vGICR: read as zero width, %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicr_reg);
     *r = 0;
     return 1;
 }
@@ -199,8 +195,6 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
                                           uint32_t gicr_reg)
 {
     struct hsr_dabt dabt = info->dabt;
-    struct cpu_user_regs *regs = guest_cpu_user_regs();
-    register_t *r = select_user_reg(regs, dabt.reg);
 
     switch ( gicr_reg )
     {
@@ -212,7 +206,7 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
         goto write_ignore;
     case GICR_TYPER:
         /* RO */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_STATUSR:
         /* Not implemented */
         goto write_ignore;
@@ -221,31 +215,31 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
         goto write_ignore;
     case GICR_SETLPIR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_CLRLPIR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_PROPBASER:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_PENDBASER:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_INVLPIR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_INVALLR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_SYNCR:
         /* RO */
         goto write_ignore;
     case GICR_MOVLPIR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_MOVALLR:
         /* LPI is not implemented */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICR_PIDR7... GICR_PIDR0:
         /* RO */
         goto write_ignore;
@@ -253,18 +247,9 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
         printk("vGICR: write r%d offset %#08x\n not found", dabt.reg, gicr_reg);
         return 0;
     }
-bad_width:
-    printk("vGICR: bad write width %d r%d=%"PRIregister" offset %#08x\n",
-           dabt.size, dabt.reg, *r, gicr_reg);
-    domain_crash_synchronous();
-    return 0;
-
-write_ignore_64:
-    if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
-    return 1;
-
 write_ignore:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG, "vGICR: ignore write width %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicr_reg);
     return 1;
 }
 
@@ -364,7 +349,9 @@ bad_width:
     return 0;
 
 read_as_zero:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG,
+             "vGIC{D,R}: read as zero width, %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, reg);
     *r = 0;
     return 1;
 }
@@ -477,7 +464,9 @@ bad_width:
     return 0;
 
 write_ignore:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG,
+             "vGIC{D,R}: ignore write width %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, reg);
     return 1;
 }
 
@@ -538,7 +527,9 @@ bad_width:
     return 0;
 
 read_as_zero:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG,
+             "vGICR: SGI: read as zero width, %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicr_reg);
     *r = 0;
     return 1;
 }
@@ -603,7 +594,8 @@ bad_width:
     return 0;
 
 write_ignore:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG, "vGICR: SGI: ignore write width %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicr_reg);
     return 1;
 }
 
@@ -732,7 +724,7 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info)
         return __vgic_v3_distr_common_mmio_read(v, info, gicd_reg);
     case GICD_IROUTER ... GICD_IROUTER31:
         /* SGI/PPI is RES0 */
-        goto read_as_zero_64;
+        goto read_as_zero;
     case GICD_IROUTER32 ... GICD_IROUTERN:
         if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
         rank = vgic_rank_offset(v, 64, gicd_reg - GICD_IROUTER,
@@ -797,8 +789,6 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info)
     case 0xf30 ... 0x5fcc:
     case 0x8000 ... 0xbfcc:
         /* These are reserved register addresses */
-        printk("vGICv3: vGICD: read unknown 0x00c .. 0xfcc r%d offset %#08x\n",
-               dabt.reg, gicd_reg);
         goto read_as_zero;
     default:
         printk("vGICv3: vGICD: unhandled read r%d offset %#08x\n",
@@ -812,13 +802,9 @@ bad_width:
     domain_crash_synchronous();
     return 0;
 
-read_as_zero_64:
-    if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
-    *r = 0;
-    return 1;
-
 read_as_zero:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG, "vGICD: read as zero width, %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicd_reg);
     *r = 0;
     return 1;
 }
@@ -891,12 +877,12 @@ static int vgic_v3_distr_mmio_write(struct vcpu *v, mmio_info_t *info)
         return __vgic_v3_distr_common_mmio_write(v, info, gicd_reg);
     case GICD_IROUTER ... GICD_IROUTER31:
         /* SGI/PPI is RES0 */
-        goto write_ignore_64;
+        goto write_ignore;
     case GICD_IROUTER32 ... GICD_IROUTERN:
         if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
         rank = vgic_rank_offset(v, 64, gicd_reg - GICD_IROUTER,
                                 DABT_DOUBLE_WORD);
-        if ( rank == NULL ) goto write_ignore_64;
+        if ( rank == NULL ) goto write_ignore;
         BUG_ON(v->domain->max_vcpus > 8);
         new_irouter = *r;
         vgic_lock_rank(v, rank, flags);
@@ -977,11 +963,8 @@ bad_width:
     return 0;
 
 write_ignore:
-    if ( dabt.size != DABT_WORD ) goto bad_width;
-    return 1;
-
-write_ignore_64:
-    if ( dabt.size != DABT_DOUBLE_WORD ) goto bad_width;
+    gdprintk(XENLOG_DEBUG, "vGICD: ignore write width %d r%d offset %#08x\n",
+             dabt.size, dabt.reg, gicd_reg);
     return 1;
 }
 
