diff --git a/xen/include/asm-arm/arm_vgic.h b/xen/include/asm-arm/arm_vgic.h
new file mode 100644
index 0000000000..865e9ee5bc
--- /dev/null
+++ b/xen/include/asm-arm/arm_vgic.h
@@ -0,0 +1,269 @@
+/*
+ * Copyright (C) 2015, 2016 ARM Ltd.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License version 2 as
+ * published by the Free Software Foundation.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef __KVM_ARM_VGIC_H
+#define __KVM_ARM_VGIC_H
+
+#include <asm/atomic.h>
+#include <asm/mmio.h>
+#include <xen/spinlock.h>
+#include <xen/list.h>
+
+#define VGIC_V3_MAX_CPUS        255
+#define VGIC_V2_MAX_CPUS        8
+#define VGIC_NR_IRQS_LEGACY     256
+#define VGIC_NR_SGIS            16
+#define VGIC_NR_PPIS            16
+#define VGIC_NR_PRIVATE_IRQS    (VGIC_NR_SGIS + VGIC_NR_PPIS)
+#define VGIC_MAX_PRIVATE        (VGIC_NR_PRIVATE_IRQS - 1)
+#define VGIC_MAX_SPI            1019
+#define VGIC_MAX_RESERVED       1023
+#define VGIC_MIN_LPI            8192
+
+#define irq_is_ppi(irq) ((irq) >= VGIC_NR_SGIS && (irq) < VGIC_NR_PRIVATE_IRQS)
+#define irq_is_spi(irq) ((irq) >= VGIC_NR_PRIVATE_IRQS && \
+                         (irq) <= VGIC_MAX_SPI)
+
+enum vgic_type {
+    VGIC_V2,        /* Good ol' GICv2 */
+    VGIC_V3,        /* New fancy GICv3 */
+};
+
+#define VGIC_V2_MAX_LRS         (1 << 6)
+#define VGIC_V3_MAX_LRS         16
+#define VGIC_V3_LR_INDEX(lr)    (VGIC_V3_MAX_LRS - 1 - lr)
+
+enum vgic_irq_config {
+    VGIC_CONFIG_EDGE = 0,
+    VGIC_CONFIG_LEVEL
+};
+
+struct vgic_irq {
+    spinlock_t irq_lock;        /* Protects the content of the struct */
+    struct list_head lpi_list;  /* Used to link all LPIs together */
+    struct list_head ap_list;
+
+    struct vcpu *vcpu;          /*
+                                 * SGIs and PPIs: The VCPU
+                                 * SPIs and LPIs: The VCPU whose ap_list
+                                 * this is queued on.
+                                 */
+
+    struct vcpu *target_vcpu;   /*
+                                 * The VCPU that this interrupt should
+                                 * be sent to, as a result of the
+                                 * targets reg (v2) or the affinity reg (v3).
+                                 */
+
+    u32 intid;                  /* Guest visible INTID */
+    bool line_level;            /* Level only */
+    bool pending_latch;         /*
+                                 * The pending latch state used to
+                                 * calculate the pending state for both
+                                 * level and edge triggered IRQs.
+                                 */
+    bool active;                /* not used for LPIs */
+    bool enabled;
+    bool hw;                    /* Tied to HW IRQ */
+    atomic_t refcount;          /* Used for LPIs */
+    u32 hwintid;                /* HW INTID number */
+    union
+    {
+        u8 targets;             /* GICv2 target VCPUs mask */
+        u32 mpidr;              /* GICv3 target VCPU */
+    };
+    u8 source;                  /* GICv2 SGIs only */
+    u8 priority;
+    enum vgic_irq_config config;    /* Level or edge */
+};
+
+struct vgic_register_region;
+struct vgic_its;
+
+enum iodev_type {
+    IODEV_CPUIF,
+    IODEV_DIST,
+    IODEV_REDIST,
+    IODEV_ITS
+};
+
+struct vgic_io_device {
+    paddr_t base_addr;
+    union
+    {
+        struct vcpu *redist_vcpu;
+        struct vgic_its *its;
+    };
+    const struct vgic_register_region *regions;
+    enum iodev_type iodev_type;
+    int nr_regions;
+};
+
+struct vgic_its {
+    /* The base address of the ITS control register frame */
+    paddr_t     vgic_its_base;
+
+    bool        enabled;
+    struct vgic_io_device       iodev;
+
+    /* These registers correspond to GITS_BASER{0,1} */
+    u64         baser_device_table;
+    u64         baser_coll_table;
+
+    /* Protects the command queue */
+    spinlock_t  cmd_lock;
+    u64         cbaser;
+    u32         creadr;
+    u32         cwriter;
+
+    /* migration ABI revision in use */
+    u32         abi_rev;
+
+    /* Protects the device and collection lists */
+    spinlock_t  its_lock;
+    struct list_head            device_list;
+    struct list_head            collection_list;
+};
+
+struct vgic_dist {
+    bool                ready;
+    bool                initialized;
+
+    /* vGIC model the kernel emulates for the guest (GICv2 or GICv3) */
+    u32                 version;
+
+    /* Do injected MSIs require an additional device ID? */
+    bool                msis_require_devid;
+
+    int                 nr_spis;
+
+    /* base addresses in guest physical address space: */
+    paddr_t             vgic_dist_base;     /* distributor */
+    union
+    {
+        /* either a GICv2 CPU interface */
+        paddr_t         vgic_cpu_base;
+        /* or a number of GICv3 redistributor regions */
+        struct
+        {
+            paddr_t     vgic_redist_base;
+            paddr_t     vgic_redist_free_offset;
+        };
+    };
+
+    /* distributor enabled */
+    bool                enabled;
+
+    struct vgic_irq     *spis;
+    unsigned long       *allocated_irqs; /* bitmap of IRQs allocated */
+
+    struct vgic_io_device   dist_iodev;
+
+    bool                has_its;
+
+    /*
+     * Contains the attributes and gpa of the LPI configuration table.
+     * Since we report GICR_TYPER.CommonLPIAff as 0b00, we can share
+     * one address across all redistributors.
+     * GICv3 spec: 6.1.2 "LPI Configuration tables"
+     */
+    u64                 propbaser;
+
+    /* Protects the lpi_list and the count value below. */
+    spinlock_t          lpi_list_lock;
+    struct list_head    lpi_list_head;
+    int                 lpi_list_count;
+};
+
+struct vgic_v2_cpu_if {
+    u32     vgic_hcr;
+    u32     vgic_vmcr;
+    u64     vgic_elrsr; /* Saved only */
+    u32     vgic_apr;
+    u32     vgic_lr[VGIC_V2_MAX_LRS];
+};
+
+struct vgic_v3_cpu_if {
+    u32     vgic_hcr;
+    u32     vgic_vmcr;
+    u32     vgic_sre;   /* Restored only, change ignored */
+    u32     vgic_elrsr; /* Saved only */
+    u32     vgic_ap0r[4];
+    u32     vgic_ap1r[4];
+    u64     vgic_lr[VGIC_V3_MAX_LRS];
+};
+
+struct vgic_cpu {
+    /* CPU vif control registers for world switch */
+    union
+    {
+        struct vgic_v2_cpu_if   vgic_v2;
+        struct vgic_v3_cpu_if   vgic_v3;
+    };
+
+    unsigned int used_lrs;
+    struct vgic_irq private_irqs[VGIC_NR_PRIVATE_IRQS];
+
+    spinlock_t ap_list_lock;    /* Protects the ap_list */
+
+    /*
+     * List of IRQs that this VCPU should consider because they are either
+     * Active or Pending (hence the name; AP list), or because they recently
+     * were one of the two and need to be migrated off this list to another
+     * VCPU.
+     */
+    struct list_head ap_list_head;
+
+    /*
+     * Members below are used with GICv3 emulation only and represent
+     * parts of the redistributor.
+     */
+    struct vgic_io_device   rd_iodev;
+    struct vgic_io_device   sgi_iodev;
+
+    /* Contains the attributes and gpa of the LPI pending tables. */
+    u64 pendbaser;
+
+    bool lpis_enabled;
+
+    /* Cache guest priority bits */
+    u32 num_pri_bits;
+
+    /* Cache guest interrupt ID bits */
+    u32 num_id_bits;
+};
+
+extern struct static_key_false vgic_v2_cpuif_trap;
+extern struct static_key_false vgic_v3_cpuif_trap;
+
+#define vgic_initialized(k) ((k)->arch.vgic.initialized)
+#define vgic_ready(k)       ((k)->arch.vgic.ready)
+#define vgic_valid_spi(k, i)    (((i) >= VGIC_NR_PRIVATE_IRQS) && \
+            ((i) < (k)->arch.vgic.nr_spis + VGIC_NR_PRIVATE_IRQS))
+
+bool vgic_emulate(struct cpu_user_regs *regs, union hsr hsr);
+bool vgic_v3_emulate(struct cpu_user_regs *regs, union hsr hsr);
+
+void vgic_clear_pending_irqs(struct vcpu *v);
+
+void vgic_v2_setup_hw(paddr_t dbase, paddr_t cbase, paddr_t csize,
+                      paddr_t vbase, void __iomem *hbase,
+                      uint32_t aliased_offset);
+struct rdist_region;
+void vgic_v3_setup_hw(paddr_t dbase, unsigned int nr_rdist_regions,
+                      const struct rdist_region *regions,
+                      unsigned int intid_bits);
+
+#endif /* __KVM_ARM_VGIC_H */
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index 968ffb0c81..e8f2917140 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -198,7 +198,11 @@ struct arch_vcpu
     union gic_state_data gic;
     uint64_t lr_mask;
 
+#ifdef CONFIG_NEW_VGIC
+    struct vgic_cpu vgic_cpu;
+#else
     struct vgic_cpu vgic;
+#endif
 
     /* Timer registers  */
     uint32_t cntkctl;
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 85ad2aca79..96b99f5c85 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -18,6 +18,10 @@
 #ifndef __ASM_ARM_VGIC_H__
 #define __ASM_ARM_VGIC_H__
 
+#ifdef CONFIG_NEW_VGIC
+#include <asm/arm_vgic.h>
+#else
+
 #include <xen/bitops.h>
 #include <xen/radix-tree.h>
 #include <xen/rbtree.h>
@@ -313,6 +317,8 @@ void vgic_v3_setup_hw(paddr_t dbase,
                       unsigned int intid_bits);
 #endif
 
+#endif /* !CONFIG_NEW_VGIC */
+
 /*** Common VGIC functions used by Xen arch code ****/
 
 /*
