diff --git a/Makefile.target b/Makefile.target
index e88b896e38..8d2b2323c1 100644
--- a/Makefile.target
+++ b/Makefile.target
@@ -366,6 +366,7 @@ obj-arm-y += cadence_uart.o
 obj-arm-y += cadence_ttc.o
 obj-arm-y += cadence_gem.o
 obj-arm-y += xilinx_zynq.o zynq_slcr.o
+obj-arm-y += arm_gic.o
 obj-arm-y += realview_gic.o realview.o arm_sysctl.o arm11mpcore.o a9mpcore.o
 obj-arm-y += exynos4210_gic.o exynos4210_combiner.o exynos4210.o
 obj-arm-y += exynos4_boards.o exynos4210_uart.o exynos4210_pwm.o
diff --git a/hw/a15mpcore.c b/hw/a15mpcore.c
index 71142e51f5..5a7b365548 100644
--- a/hw/a15mpcore.c
+++ b/hw/a15mpcore.c
@@ -20,36 +20,38 @@
 
 #include "sysbus.h"
 
-/* Configuration for arm_gic.c:
- * max number of CPUs, how to ID current CPU
- */
-#define NCPU 4
-
-static inline int gic_get_current_cpu(void)
-{
-  return cpu_single_env->cpu_index;
-}
-
-#include "arm_gic.c"
-
 /* A15MP private memory region.  */
 
 typedef struct A15MPPrivState {
-    gic_state gic;
+    SysBusDevice busdev;
     uint32_t num_cpu;
     uint32_t num_irq;
     MemoryRegion container;
+    DeviceState *gic;
 } A15MPPrivState;
 
+static void a15mp_priv_set_irq(void *opaque, int irq, int level)
+{
+    A15MPPrivState *s = (A15MPPrivState *)opaque;
+    qemu_set_irq(qdev_get_gpio_in(s->gic, irq), level);
+}
+
 static int a15mp_priv_init(SysBusDevice *dev)
 {
-    A15MPPrivState *s = FROM_SYSBUSGIC(A15MPPrivState, dev);
+    A15MPPrivState *s = FROM_SYSBUS(A15MPPrivState, dev);
+    SysBusDevice *busdev;
 
-    if (s->num_cpu > NCPU) {
-        hw_error("a15mp_priv_init: num-cpu may not be more than %d\n", NCPU);
-    }
+    s->gic = qdev_create(NULL, "arm_gic");
+    qdev_prop_set_uint32(s->gic, "num-cpu", s->num_cpu);
+    qdev_prop_set_uint32(s->gic, "num-irq", s->num_irq);
+    qdev_init_nofail(s->gic);
+    busdev = sysbus_from_qdev(s->gic);
 
-    gic_init(&s->gic, s->num_cpu, s->num_irq);
+    /* Pass through outbound IRQ lines from the GIC */
+    sysbus_pass_irq(dev, busdev);
+
+    /* Pass through inbound GPIO lines to the GIC */
+    qdev_init_gpio_in(&s->busdev.qdev, a15mp_priv_set_irq, s->num_irq - 32);
 
     /* Memory map (addresses are offsets from PERIPHBASE):
      *  0x0000-0x0fff -- reserved
@@ -60,8 +62,10 @@ static int a15mp_priv_init(SysBusDevice *dev)
      *  0x6000-0x7fff -- GIC virtual CPU interface (not modelled)
      */
     memory_region_init(&s->container, "a15mp-priv-container", 0x8000);
-    memory_region_add_subregion(&s->container, 0x1000, &s->gic.iomem);
-    memory_region_add_subregion(&s->container, 0x2000, &s->gic.cpuiomem[0]);
+    memory_region_add_subregion(&s->container, 0x1000,
+                                sysbus_mmio_get_region(busdev, 0));
+    memory_region_add_subregion(&s->container, 0x2000,
+                                sysbus_mmio_get_region(busdev, 1));
 
     sysbus_init_mmio(dev, &s->container);
     return 0;
@@ -85,7 +89,7 @@ static void a15mp_priv_class_init(ObjectClass *klass, void *data)
     SysBusDeviceClass *k = SYS_BUS_DEVICE_CLASS(klass);
     k->init = a15mp_priv_init;
     dc->props = a15mp_priv_properties;
-    /* We currently have no savable state outside the common GIC state */
+    /* We currently have no savable state */
 }
 
 static TypeInfo a15mp_priv_info = {
diff --git a/hw/a9mpcore.c b/hw/a9mpcore.c
index 03b128ce5b..c2ff74d4b6 100644
--- a/hw/a9mpcore.c
+++ b/hw/a9mpcore.c
@@ -10,32 +10,19 @@
 
 #include "sysbus.h"
 
-/* Configuration for arm_gic.c:
- * max number of CPUs, how to ID current CPU
- */
-#define NCPU 4
-
-static inline int
-gic_get_current_cpu(void)
-{
-  return cpu_single_env->cpu_index;
-}
-
-#include "arm_gic.c"
-
 /* A9MP private memory region.  */
 
 typedef struct a9mp_priv_state {
-    gic_state gic;
+    SysBusDevice busdev;
     uint32_t scu_control;
     uint32_t scu_status;
     uint32_t old_timer_status[8];
     uint32_t num_cpu;
-    qemu_irq *timer_irq;
     MemoryRegion scu_iomem;
     MemoryRegion ptimer_iomem;
     MemoryRegion container;
     DeviceState *mptimer;
+    DeviceState *gic;
     uint32_t num_irq;
 } a9mp_priv_state;
 
@@ -124,18 +111,9 @@ static const MemoryRegionOps a9_scu_ops = {
     .endianness = DEVICE_NATIVE_ENDIAN,
 };
 
-static void a9mpcore_timer_irq_handler(void *opaque, int irq, int level)
-{
-    a9mp_priv_state *s = (a9mp_priv_state *)opaque;
-    if (level && !s->old_timer_status[irq]) {
-        gic_set_pending_private(&s->gic, irq >> 1, 29 + (irq & 1));
-    }
-    s->old_timer_status[irq] = level;
-}
-
 static void a9mp_priv_reset(DeviceState *dev)
 {
-    a9mp_priv_state *s = FROM_SYSBUSGIC(a9mp_priv_state, sysbus_from_qdev(dev));
+    a9mp_priv_state *s = FROM_SYSBUS(a9mp_priv_state, sysbus_from_qdev(dev));
     int i;
     s->scu_control = 0;
     for (i = 0; i < ARRAY_SIZE(s->old_timer_status); i++) {
@@ -143,17 +121,29 @@ static void a9mp_priv_reset(DeviceState *dev)
     }
 }
 
+static void a9mp_priv_set_irq(void *opaque, int irq, int level)
+{
+    a9mp_priv_state *s = (a9mp_priv_state *)opaque;
+    qemu_set_irq(qdev_get_gpio_in(s->gic, irq), level);
+}
+
 static int a9mp_priv_init(SysBusDevice *dev)
 {
-    a9mp_priv_state *s = FROM_SYSBUSGIC(a9mp_priv_state, dev);
-    SysBusDevice *busdev;
+    a9mp_priv_state *s = FROM_SYSBUS(a9mp_priv_state, dev);
+    SysBusDevice *busdev, *gicbusdev;
     int i;
 
-    if (s->num_cpu > NCPU) {
-        hw_error("a9mp_priv_init: num-cpu may not be more than %d\n", NCPU);
-    }
+    s->gic = qdev_create(NULL, "arm_gic");
+    qdev_prop_set_uint32(s->gic, "num-cpu", s->num_cpu);
+    qdev_prop_set_uint32(s->gic, "num-irq", s->num_irq);
+    qdev_init_nofail(s->gic);
+    gicbusdev = sysbus_from_qdev(s->gic);
 
-    gic_init(&s->gic, s->num_cpu, s->num_irq);
+    /* Pass through outbound IRQ lines from the GIC */
+    sysbus_pass_irq(dev, gicbusdev);
+
+    /* Pass through inbound GPIO lines to the GIC */
+    qdev_init_gpio_in(&s->busdev.qdev, a9mp_priv_set_irq, s->num_irq - 32);
 
     s->mptimer = qdev_create(NULL, "arm_mptimer");
     qdev_prop_set_uint32(s->mptimer, "num-cpu", s->num_cpu);
@@ -175,7 +165,8 @@ static int a9mp_priv_init(SysBusDevice *dev)
     memory_region_init_io(&s->scu_iomem, &a9_scu_ops, s, "a9mp-scu", 0x100);
     memory_region_add_subregion(&s->container, 0, &s->scu_iomem);
     /* GIC CPU interface */
-    memory_region_add_subregion(&s->container, 0x100, &s->gic.cpuiomem[0]);
+    memory_region_add_subregion(&s->container, 0x100,
+                                sysbus_mmio_get_region(gicbusdev, 1));
     /* Note that the A9 exposes only the "timer/watchdog for this core"
      * memory region, not the "timer/watchdog for core X" ones 11MPcore has.
      */
@@ -183,15 +174,20 @@ static int a9mp_priv_init(SysBusDevice *dev)
                                 sysbus_mmio_get_region(busdev, 0));
     memory_region_add_subregion(&s->container, 0x620,
                                 sysbus_mmio_get_region(busdev, 1));
-    memory_region_add_subregion(&s->container, 0x1000, &s->gic.iomem);
+    memory_region_add_subregion(&s->container, 0x1000,
+                                sysbus_mmio_get_region(gicbusdev, 0));
 
     sysbus_init_mmio(dev, &s->container);
 
-    /* Wire up the interrupt from each watchdog and timer. */
-    s->timer_irq = qemu_allocate_irqs(a9mpcore_timer_irq_handler,
-                                      s, (s->num_cpu + 1) * 2);
-    for (i = 0; i < s->num_cpu * 2; i++) {
-        sysbus_connect_irq(busdev, i, s->timer_irq[i]);
+    /* Wire up the interrupt from each watchdog and timer.
+     * For each core the timer is PPI 29 and the watchdog PPI 30.
+     */
+    for (i = 0; i < s->num_cpu; i++) {
+        int ppibase = (s->num_irq - 32) + i * 32;
+        sysbus_connect_irq(busdev, i * 2,
+                           qdev_get_gpio_in(s->gic, ppibase + 29));
+        sysbus_connect_irq(busdev, i * 2 + 1,
+                           qdev_get_gpio_in(s->gic, ppibase + 30));
     }
     return 0;
 }
diff --git a/hw/arm11mpcore.c b/hw/arm11mpcore.c
index ba6a89d3ed..c528d7aa01 100644
--- a/hw/arm11mpcore.c
+++ b/hw/arm11mpcore.c
@@ -10,28 +10,18 @@
 #include "sysbus.h"
 #include "qemu-timer.h"
 
-#define NCPU 4
-
-static inline int
-gic_get_current_cpu(void)
-{
-  return cpu_single_env->cpu_index;
-}
-
-#include "arm_gic.c"
-
 /* MPCore private memory region.  */
 
 typedef struct mpcore_priv_state {
-    gic_state gic;
+    SysBusDevice busdev;
     uint32_t scu_control;
     int iomemtype;
     uint32_t old_timer_status[8];
     uint32_t num_cpu;
-    qemu_irq *timer_irq;
     MemoryRegion iomem;
     MemoryRegion container;
     DeviceState *mptimer;
+    DeviceState *gic;
     uint32_t num_irq;
 } mpcore_priv_state;
 
@@ -81,18 +71,16 @@ static const MemoryRegionOps mpcore_scu_ops = {
     .endianness = DEVICE_NATIVE_ENDIAN,
 };
 
-static void mpcore_timer_irq_handler(void *opaque, int irq, int level)
+static void mpcore_priv_set_irq(void *opaque, int irq, int level)
 {
     mpcore_priv_state *s = (mpcore_priv_state *)opaque;
-    if (level && !s->old_timer_status[irq]) {
-        gic_set_pending_private(&s->gic, irq >> 1, 29 + (irq & 1));
-    }
-    s->old_timer_status[irq] = level;
+    qemu_set_irq(qdev_get_gpio_in(s->gic, irq), level);
 }
 
 static void mpcore_priv_map_setup(mpcore_priv_state *s)
 {
     int i;
+    SysBusDevice *gicbusdev = sysbus_from_qdev(s->gic);
     SysBusDevice *busdev = sysbus_from_qdev(s->mptimer);
     memory_region_init(&s->container, "mpcode-priv-container", 0x2000);
     memory_region_init_io(&s->iomem, &mpcore_scu_ops, s, "mpcore-scu", 0x100);
@@ -102,31 +90,47 @@ static void mpcore_priv_map_setup(mpcore_priv_state *s)
      */
     for (i = 0; i < (s->num_cpu + 1); i++) {
         target_phys_addr_t offset = 0x100 + (i * 0x100);
-        memory_region_add_subregion(&s->container, offset, &s->gic.cpuiomem[i]);
+        memory_region_add_subregion(&s->container, offset,
+                                    sysbus_mmio_get_region(gicbusdev, i + 1));
     }
     /* Add the regions for timer and watchdog for "current CPU" and
      * for each specific CPU.
      */
-    s->timer_irq = qemu_allocate_irqs(mpcore_timer_irq_handler,
-                                      s, (s->num_cpu + 1) * 2);
     for (i = 0; i < (s->num_cpu + 1) * 2; i++) {
         /* Timers at 0x600, 0x700, ...; watchdogs at 0x620, 0x720, ... */
         target_phys_addr_t offset = 0x600 + (i >> 1) * 0x100 + (i & 1) * 0x20;
         memory_region_add_subregion(&s->container, offset,
                                     sysbus_mmio_get_region(busdev, i));
     }
-    memory_region_add_subregion(&s->container, 0x1000, &s->gic.iomem);
-    /* Wire up the interrupt from each watchdog and timer. */
-    for (i = 0; i < s->num_cpu * 2; i++) {
-        sysbus_connect_irq(busdev, i, s->timer_irq[i]);
+    memory_region_add_subregion(&s->container, 0x1000,
+                                sysbus_mmio_get_region(gicbusdev, 0));
+    /* Wire up the interrupt from each watchdog and timer.
+     * For each core the timer is PPI 29 and the watchdog PPI 30.
+     */
+    for (i = 0; i < s->num_cpu; i++) {
+        int ppibase = (s->num_irq - 32) + i * 32;
+        sysbus_connect_irq(busdev, i * 2,
+                           qdev_get_gpio_in(s->gic, ppibase + 29));
+        sysbus_connect_irq(busdev, i * 2 + 1,
+                           qdev_get_gpio_in(s->gic, ppibase + 30));
     }
 }
 
 static int mpcore_priv_init(SysBusDevice *dev)
 {
-    mpcore_priv_state *s = FROM_SYSBUSGIC(mpcore_priv_state, dev);
+    mpcore_priv_state *s = FROM_SYSBUS(mpcore_priv_state, dev);
+
+    s->gic = qdev_create(NULL, "arm_gic");
+    qdev_prop_set_uint32(s->gic, "num-cpu", s->num_cpu);
+    qdev_prop_set_uint32(s->gic, "num-irq", s->num_irq);
+    qdev_init_nofail(s->gic);
+
+    /* Pass through outbound IRQ lines from the GIC */
+    sysbus_pass_irq(dev, sysbus_from_qdev(s->gic));
+
+    /* Pass through inbound GPIO lines to the GIC */
+    qdev_init_gpio_in(&s->busdev.qdev, mpcore_priv_set_irq, s->num_irq - 32);
 
-    gic_init(&s->gic, s->num_cpu, s->num_irq);
     s->mptimer = qdev_create(NULL, "arm_mptimer");
     qdev_prop_set_uint32(s->mptimer, "num-cpu", s->num_cpu);
     qdev_init_nofail(s->mptimer);
diff --git a/hw/arm_gic.c b/hw/arm_gic.c
index 6b34c06a8f..72298b4b41 100644
--- a/hw/arm_gic.c
+++ b/hw/arm_gic.c
@@ -8,13 +8,29 @@
  */
 
 /* This file contains implementation code for the RealView EB interrupt
-   controller, MPCore distributed interrupt controller and ARMv7-M
-   Nested Vectored Interrupt Controller.  */
+ * controller, MPCore distributed interrupt controller and ARMv7-M
+ * Nested Vectored Interrupt Controller.
+ * It is compiled in two ways:
+ *  (1) as a standalone file to produce a sysbus device which is a GIC
+ *  that can be used on the realview board and as one of the builtin
+ *  private peripherals for the ARM MP CPUs (11MPCore, A9, etc)
+ *  (2) by being directly #included into armv7m_nvic.c to produce the
+ *  armv7m_nvic device.
+ */
+
+#include "sysbus.h"
 
 /* Maximum number of possible interrupts, determined by the GIC architecture */
 #define GIC_MAXIRQ 1020
 /* First 32 are private to each CPU (SGIs and PPIs). */
 #define GIC_INTERNAL 32
+/* Maximum number of possible CPU interfaces, determined by GIC architecture */
+#ifdef NVIC
+#define NCPU 1
+#else
+#define NCPU 8
+#endif
+
 //#define DEBUG_GIC
 
 #ifdef DEBUG_GIC
@@ -50,7 +66,7 @@ typedef struct gic_irq_state
     unsigned trigger:1; /* nonzero = edge triggered.  */
 } gic_irq_state;
 
-#define ALL_CPU_MASK ((1 << NCPU) - 1)
+#define ALL_CPU_MASK ((unsigned)(((1 << NCPU) - 1)))
 #if NCPU > 1
 #define NUM_CPU(s) ((s)->num_cpu)
 #else
@@ -105,7 +121,7 @@ typedef struct gic_state
     int current_pending[NCPU];
 
 #if NCPU > 1
-    int num_cpu;
+    uint32_t num_cpu;
 #endif
 
     MemoryRegion iomem; /* Distributor */
@@ -119,6 +135,16 @@ typedef struct gic_state
     uint32_t num_irq;
 } gic_state;
 
+static inline int gic_get_current_cpu(gic_state *s)
+{
+#if NCPU > 1
+    if (s->num_cpu > 1) {
+        return cpu_single_env->cpu_index;
+    }
+#endif
+    return 0;
+}
+
 /* TODO: Many places that call this routine could be optimized.  */
 /* Update interrupt status after enabled or pending bits have been changed.  */
 static void gic_update(gic_state *s)
@@ -134,7 +160,7 @@ static void gic_update(gic_state *s)
         cm = 1 << cpu;
         s->current_pending[cpu] = 1023;
         if (!s->enabled || !s->cpu_enabled[cpu]) {
-	    qemu_irq_lower(s->parent_irq[cpu]);
+            qemu_irq_lower(s->parent_irq[cpu]);
             return;
         }
         best_prio = 0x100;
@@ -159,8 +185,8 @@ static void gic_update(gic_state *s)
     }
 }
 
-static void __attribute__((unused))
-gic_set_pending_private(gic_state *s, int cpu, int irq)
+#ifdef NVIC
+static void gic_set_pending_private(gic_state *s, int cpu, int irq)
 {
     int cm = 1 << cpu;
 
@@ -171,24 +197,45 @@ gic_set_pending_private(gic_state *s, int cpu, int irq)
     GIC_SET_PENDING(irq, cm);
     gic_update(s);
 }
+#endif
 
 /* Process a change in an external IRQ input.  */
 static void gic_set_irq(void *opaque, int irq, int level)
 {
+    /* Meaning of the 'irq' parameter:
+     *  [0..N-1] : external interrupts
+     *  [N..N+31] : PPI (internal) interrupts for CPU 0
+     *  [N+32..N+63] : PPI (internal interrupts for CPU 1
+     *  ...
+     */
     gic_state *s = (gic_state *)opaque;
-    /* The first external input line is internal interrupt 32.  */
-    irq += GIC_INTERNAL;
-    if (level == GIC_TEST_LEVEL(irq, ALL_CPU_MASK))
+    int cm, target;
+    if (irq < (s->num_irq - GIC_INTERNAL)) {
+        /* The first external input line is internal interrupt 32.  */
+        cm = ALL_CPU_MASK;
+        irq += GIC_INTERNAL;
+        target = GIC_TARGET(irq);
+    } else {
+        int cpu;
+        irq -= (s->num_irq - GIC_INTERNAL);
+        cpu = irq / GIC_INTERNAL;
+        irq %= GIC_INTERNAL;
+        cm = 1 << cpu;
+        target = cm;
+    }
+
+    if (level == GIC_TEST_LEVEL(irq, cm)) {
         return;
+    }
 
     if (level) {
-        GIC_SET_LEVEL(irq, ALL_CPU_MASK);
-        if (GIC_TEST_TRIGGER(irq) || GIC_TEST_ENABLED(irq, ALL_CPU_MASK)) {
-            DPRINTF("Set %d pending mask %x\n", irq, GIC_TARGET(irq));
-            GIC_SET_PENDING(irq, GIC_TARGET(irq));
+        GIC_SET_LEVEL(irq, cm);
+        if (GIC_TEST_TRIGGER(irq) || GIC_TEST_ENABLED(irq, cm)) {
+            DPRINTF("Set %d pending mask %x\n", irq, target);
+            GIC_SET_PENDING(irq, target);
         }
     } else {
-        GIC_CLEAR_LEVEL(irq, ALL_CPU_MASK);
+        GIC_CLEAR_LEVEL(irq, cm);
     }
     gic_update(s);
 }
@@ -278,7 +325,7 @@ static uint32_t gic_dist_readb(void *opaque, target_phys_addr_t offset)
     int cm;
     int mask;
 
-    cpu = gic_get_current_cpu();
+    cpu = gic_get_current_cpu(s);
     cm = 1 << cpu;
     if (offset < 0x100) {
 #ifndef NVIC
@@ -413,7 +460,7 @@ static void gic_dist_writeb(void *opaque, target_phys_addr_t offset,
     int i;
     int cpu;
 
-    cpu = gic_get_current_cpu();
+    cpu = gic_get_current_cpu(s);
     if (offset < 0x100) {
 #ifdef NVIC
         goto bad_reg;
@@ -575,7 +622,7 @@ static void gic_dist_writel(void *opaque, target_phys_addr_t offset,
         int irq;
         int mask;
 
-        cpu = gic_get_current_cpu();
+        cpu = gic_get_current_cpu(s);
         irq = value & 0x3ff;
         switch ((value >> 24) & 3) {
         case 0:
@@ -658,14 +705,14 @@ static uint64_t gic_thiscpu_read(void *opaque, target_phys_addr_t addr,
                                  unsigned size)
 {
     gic_state *s = (gic_state *)opaque;
-    return gic_cpu_read(s, gic_get_current_cpu(), addr);
+    return gic_cpu_read(s, gic_get_current_cpu(s), addr);
 }
 
 static void gic_thiscpu_write(void *opaque, target_phys_addr_t addr,
                               uint64_t value, unsigned size)
 {
     gic_state *s = (gic_state *)opaque;
-    gic_cpu_write(s, gic_get_current_cpu(), addr, value);
+    gic_cpu_write(s, gic_get_current_cpu(s), addr, value);
 }
 
 /* Wrappers to read/write the GIC CPU interface for a specific CPU.
@@ -702,8 +749,9 @@ static const MemoryRegionOps gic_cpu_ops = {
 };
 #endif
 
-static void gic_reset(gic_state *s)
+static void gic_reset(DeviceState *dev)
 {
+    gic_state *s = FROM_SYSBUS(gic_state, sysbus_from_qdev(dev));
     int i;
     memset(s->irq_state, 0, GIC_MAXIRQ * sizeof(gic_irq_state));
     for (i = 0 ; i < NUM_CPU(s); i++) {
@@ -813,6 +861,10 @@ static void gic_init(gic_state *s, int num_irq)
 
 #if NCPU > 1
     s->num_cpu = num_cpu;
+    if (s->num_cpu > NCPU) {
+        hw_error("requested %u CPUs exceeds GIC maximum %d\n",
+                 num_cpu, NCPU);
+    }
 #endif
     s->num_irq = num_irq + GIC_BASE_IRQ;
     if (s->num_irq > GIC_MAXIRQ) {
@@ -828,7 +880,18 @@ static void gic_init(gic_state *s, int num_irq)
                  num_irq);
     }
 
-    qdev_init_gpio_in(&s->busdev.qdev, gic_set_irq, s->num_irq - GIC_INTERNAL);
+    i = s->num_irq - GIC_INTERNAL;
+#ifndef NVIC
+    /* For the GIC, also expose incoming GPIO lines for PPIs for each CPU.
+     * GPIO array layout is thus:
+     *  [0..N-1] SPIs
+     *  [N..N+31] PPIs for CPU 0
+     *  [N+32..N+63] PPIs for CPU 1
+     *   ...
+     */
+    i += (GIC_INTERNAL * num_cpu);
+#endif
+    qdev_init_gpio_in(&s->busdev.qdev, gic_set_irq, i);
     for (i = 0; i < NUM_CPU(s); i++) {
         sysbus_init_irq(&s->busdev, &s->parent_irq[i]);
     }
@@ -851,6 +914,54 @@ static void gic_init(gic_state *s, int num_irq)
     }
 #endif
 
-    gic_reset(s);
     register_savevm(NULL, "arm_gic", -1, 2, gic_save, gic_load, s);
 }
+
+#ifndef NVIC
+
+static int arm_gic_init(SysBusDevice *dev)
+{
+    /* Device instance init function for the GIC sysbus device */
+    int i;
+    gic_state *s = FROM_SYSBUS(gic_state, dev);
+    gic_init(s, s->num_cpu, s->num_irq);
+    /* Distributor */
+    sysbus_init_mmio(dev, &s->iomem);
+    /* cpu interfaces (one for "current cpu" plus one per cpu) */
+    for (i = 0; i <= NUM_CPU(s); i++) {
+        sysbus_init_mmio(dev, &s->cpuiomem[i]);
+    }
+    return 0;
+}
+
+static Property arm_gic_properties[] = {
+    DEFINE_PROP_UINT32("num-cpu", gic_state, num_cpu, 1),
+    DEFINE_PROP_UINT32("num-irq", gic_state, num_irq, 32),
+    DEFINE_PROP_END_OF_LIST(),
+};
+
+static void arm_gic_class_init(ObjectClass *klass, void *data)
+{
+    DeviceClass *dc = DEVICE_CLASS(klass);
+    SysBusDeviceClass *sbc = SYS_BUS_DEVICE_CLASS(klass);
+    sbc->init = arm_gic_init;
+    dc->props = arm_gic_properties;
+    dc->reset = gic_reset;
+    dc->no_user = 1;
+}
+
+static TypeInfo arm_gic_info = {
+    .name = "arm_gic",
+    .parent = TYPE_SYS_BUS_DEVICE,
+    .instance_size = sizeof(gic_state),
+    .class_init = arm_gic_class_init,
+};
+
+static void arm_gic_register_types(void)
+{
+    type_register_static(&arm_gic_info);
+}
+
+type_init(arm_gic_register_types)
+
+#endif
diff --git a/hw/armv7m_nvic.c b/hw/armv7m_nvic.c
index 3210129c3f..986a6bbd0c 100644
--- a/hw/armv7m_nvic.c
+++ b/hw/armv7m_nvic.c
@@ -15,16 +15,8 @@
 #include "arm-misc.h"
 #include "exec-memory.h"
 
-#define NCPU 1
 #define NVIC 1
 
-/* Only a single "CPU" interface is present.  */
-static inline int
-gic_get_current_cpu(void)
-{
-    return 0;
-}
-
 static uint32_t nvic_readl(void *opaque, uint32_t offset);
 static void nvic_writel(void *opaque, uint32_t offset, uint32_t value);
 
@@ -83,6 +75,14 @@ static void systick_timer_tick(void * opaque)
     }
 }
 
+static void systick_reset(nvic_state *s)
+{
+    s->systick.control = 0;
+    s->systick.reload = 0;
+    s->systick.tick = 0;
+    qemu_del_timer(s->systick.timer);
+}
+
 /* The external routines use the hardware vector numbering, ie. the first
    IRQ is #16.  The internal GIC routines use #32 as the first IRQ.  */
 void armv7m_nvic_set_pending(void *opaque, int irq)
@@ -378,6 +378,13 @@ static const VMStateDescription vmstate_nvic = {
     }
 };
 
+static void armv7m_nvic_reset(DeviceState *dev)
+{
+    nvic_state *s = FROM_SYSBUSGIC(nvic_state, sysbus_from_qdev(dev));
+    gic_reset(&s->gic.busdev.qdev);
+    systick_reset(s);
+}
+
 static int armv7m_nvic_init(SysBusDevice *dev)
 {
     nvic_state *s= FROM_SYSBUSGIC(nvic_state, dev);
@@ -407,6 +414,7 @@ static void armv7m_nvic_class_init(ObjectClass *klass, void *data)
 
     sdc->init = armv7m_nvic_init;
     dc->vmsd  = &vmstate_nvic;
+    dc->reset = armv7m_nvic_reset;
     dc->props = armv7m_nvic_properties;
 }
 
diff --git a/hw/exynos4210.c b/hw/exynos4210.c
index f904370505..afc4bdc7e0 100644
--- a/hw/exynos4210.c
+++ b/hw/exynos4210.c
@@ -25,6 +25,7 @@
 #include "sysemu.h"
 #include "sysbus.h"
 #include "arm-misc.h"
+#include "loader.h"
 #include "exynos4210.h"
 
 #define EXYNOS4210_CHIPID_ADDR         0x10000000
@@ -64,6 +65,35 @@
 static uint8_t chipid_and_omr[] = { 0x11, 0x02, 0x21, 0x43,
                                     0x09, 0x00, 0x00, 0x00 };
 
+void exynos4210_write_secondary(CPUARMState *env,
+        const struct arm_boot_info *info)
+{
+    int n;
+    uint32_t smpboot[] = {
+        0xe59f3024, /* ldr r3, External gic_cpu_if */
+        0xe59f2024, /* ldr r2, Internal gic_cpu_if */
+        0xe59f0024, /* ldr r0, startaddr */
+        0xe3a01001, /* mov r1, #1 */
+        0xe5821000, /* str r1, [r2] */
+        0xe5831000, /* str r1, [r3] */
+        0xe320f003, /* wfi */
+        0xe5901000, /* ldr     r1, [r0] */
+        0xe1110001, /* tst     r1, r1 */
+        0x0afffffb, /* beq     <wfi> */
+        0xe12fff11, /* bx      r1 */
+        EXYNOS4210_EXT_GIC_CPU_BASE_ADDR,
+        0,          /* gic_cpu_if: base address of Internal GIC CPU interface */
+        0           /* bootreg: Boot register address is held here */
+    };
+    smpboot[ARRAY_SIZE(smpboot) - 1] = info->smp_bootreg_addr;
+    smpboot[ARRAY_SIZE(smpboot) - 2] = info->gic_cpu_if_addr;
+    for (n = 0; n < ARRAY_SIZE(smpboot); n++) {
+        smpboot[n] = tswap32(smpboot[n]);
+    }
+    rom_add_blob_fixed("smpboot", smpboot, sizeof(smpboot),
+                       info->smp_loader_start);
+}
+
 Exynos4210State *exynos4210_init(MemoryRegion *system_mem,
         unsigned long ram_size)
 {
diff --git a/hw/exynos4210.h b/hw/exynos4210.h
index c112e03bfb..f7c7027302 100644
--- a/hw/exynos4210.h
+++ b/hw/exynos4210.h
@@ -97,6 +97,9 @@ typedef struct Exynos4210State {
     MemoryRegion bootreg_mem;
 } Exynos4210State;
 
+void exynos4210_write_secondary(CPUARMState *env,
+        const struct arm_boot_info *info);
+
 Exynos4210State *exynos4210_init(MemoryRegion *system_mem,
         unsigned long ram_size);
 
diff --git a/hw/exynos4210_combiner.c b/hw/exynos4210_combiner.c
index 6110c19d5d..80af22cc33 100644
--- a/hw/exynos4210_combiner.c
+++ b/hw/exynos4210_combiner.c
@@ -184,11 +184,6 @@ exynos4210_combiner_read(void *opaque, target_phys_addr_t offset, unsigned size)
     uint32_t reg_n;              /* Register number inside the quad */
     uint32_t val;
 
-    if (s->external && (offset > 0x3c && offset != 0x100)) {
-        hw_error("exynos4210.combiner: unallowed read access at offset 0x"
-                TARGET_FMT_plx "\n", offset);
-    }
-
     req_quad_base_n = offset >> 4;
     grp_quad_base_n = req_quad_base_n << 2;
     reg_n = (offset - (req_quad_base_n << 4)) >> 2;
@@ -281,11 +276,6 @@ static void exynos4210_combiner_write(void *opaque, target_phys_addr_t offset,
     uint32_t grp_quad_base_n;    /* Base of group quad */
     uint32_t reg_n;              /* Register number inside the quad */
 
-    if (s->external && (offset > 0x3c && offset != 0x100)) {
-        hw_error("exynos4210.combiner: unallowed write access at offset 0x"
-                TARGET_FMT_plx "\n", offset);
-    }
-
     req_quad_base_n = offset >> 4;
     grp_quad_base_n = req_quad_base_n << 2;
     reg_n = (offset - (req_quad_base_n << 4)) >> 2;
diff --git a/hw/exynos4210_gic.c b/hw/exynos4210_gic.c
index ec13140f9f..e1b215eff0 100644
--- a/hw/exynos4210_gic.c
+++ b/hw/exynos4210_gic.c
@@ -174,7 +174,6 @@ combiner_grp_to_gic_id[64-EXYNOS4210_MAX_EXT_COMBINER_OUT_IRQ][8] = {
 };
 
 #define EXYNOS4210_GIC_NIRQ 160
-#define NCPU                EXYNOS4210_NCPUS
 
 #define EXYNOS4210_EXT_GIC_CPU_REGION_SIZE     0x10000
 #define EXYNOS4210_EXT_GIC_DIST_REGION_SIZE    0x10000
@@ -263,33 +262,44 @@ uint32_t exynos4210_get_irq(uint32_t grp, uint32_t bit)
 
 /********* GIC part *********/
 
-static inline int
-gic_get_current_cpu(void)
-{
-    return cpu_single_env->cpu_index;
-}
-
-#include "arm_gic.c"
-
 typedef struct {
-    gic_state gic;
+    SysBusDevice busdev;
     MemoryRegion cpu_container;
     MemoryRegion dist_container;
-    MemoryRegion cpu_alias[NCPU];
-    MemoryRegion dist_alias[NCPU];
+    MemoryRegion cpu_alias[EXYNOS4210_NCPUS];
+    MemoryRegion dist_alias[EXYNOS4210_NCPUS];
     uint32_t num_cpu;
+    DeviceState *gic;
 } Exynos4210GicState;
 
+static void exynos4210_gic_set_irq(void *opaque, int irq, int level)
+{
+    Exynos4210GicState *s = (Exynos4210GicState *)opaque;
+    qemu_set_irq(qdev_get_gpio_in(s->gic, irq), level);
+}
+
 static int exynos4210_gic_init(SysBusDevice *dev)
 {
-    Exynos4210GicState *s = FROM_SYSBUSGIC(Exynos4210GicState, dev);
+    Exynos4210GicState *s = FROM_SYSBUS(Exynos4210GicState, dev);
     uint32_t i;
     const char cpu_prefix[] = "exynos4210-gic-alias_cpu";
     const char dist_prefix[] = "exynos4210-gic-alias_dist";
     char cpu_alias_name[sizeof(cpu_prefix) + 3];
     char dist_alias_name[sizeof(cpu_prefix) + 3];
+    SysBusDevice *busdev;
 
-    gic_init(&s->gic, s->num_cpu, EXYNOS4210_GIC_NIRQ);
+    s->gic = qdev_create(NULL, "arm_gic");
+    qdev_prop_set_uint32(s->gic, "num-cpu", s->num_cpu);
+    qdev_prop_set_uint32(s->gic, "num-irq", EXYNOS4210_GIC_NIRQ);
+    qdev_init_nofail(s->gic);
+    busdev = sysbus_from_qdev(s->gic);
+
+    /* Pass through outbound IRQ lines from the GIC */
+    sysbus_pass_irq(dev, busdev);
+
+    /* Pass through inbound GPIO lines to the GIC */
+    qdev_init_gpio_in(&s->busdev.qdev, exynos4210_gic_set_irq,
+                      EXYNOS4210_GIC_NIRQ - 32);
 
     memory_region_init(&s->cpu_container, "exynos4210-cpu-container",
             EXYNOS4210_EXT_GIC_CPU_REGION_SIZE);
@@ -301,7 +311,7 @@ static int exynos4210_gic_init(SysBusDevice *dev)
         sprintf(cpu_alias_name, "%s%x", cpu_prefix, i);
         memory_region_init_alias(&s->cpu_alias[i],
                                  cpu_alias_name,
-                                 &s->gic.cpuiomem[0],
+                                 sysbus_mmio_get_region(busdev, 1),
                                  0,
                                  EXYNOS4210_GIC_CPU_REGION_SIZE);
         memory_region_add_subregion(&s->cpu_container,
@@ -311,7 +321,7 @@ static int exynos4210_gic_init(SysBusDevice *dev)
         sprintf(dist_alias_name, "%s%x", dist_prefix, i);
         memory_region_init_alias(&s->dist_alias[i],
                                  dist_alias_name,
-                                 &s->gic.iomem,
+                                 sysbus_mmio_get_region(busdev, 0),
                                  0,
                                  EXYNOS4210_GIC_DIST_REGION_SIZE);
         memory_region_add_subregion(&s->dist_container,
@@ -321,8 +331,6 @@ static int exynos4210_gic_init(SysBusDevice *dev)
     sysbus_init_mmio(dev, &s->cpu_container);
     sysbus_init_mmio(dev, &s->dist_container);
 
-    gic_cpu_write(&s->gic, 1, 0, 1);
-
     return 0;
 }
 
@@ -361,7 +369,7 @@ type_init(exynos4210_gic_register_types)
 typedef struct {
     SysBusDevice busdev;
 
-    qemu_irq pic_irq[NCPU]; /* output IRQs to PICs */
+    qemu_irq pic_irq[EXYNOS4210_NCPUS]; /* output IRQs to PICs */
     uint32_t gpio_level[EXYNOS4210_IRQ_GATE_NINPUTS]; /* Input levels */
 } Exynos4210IRQGateState;
 
@@ -426,7 +434,7 @@ static int exynos4210_irq_gate_init(SysBusDevice *dev)
             EXYNOS4210_IRQ_GATE_NINPUTS);
 
     /* Connect SysBusDev irqs to device specific irqs */
-    for (i = 0; i < NCPU; i++) {
+    for (i = 0; i < EXYNOS4210_NCPUS; i++) {
         sysbus_init_irq(dev, &s->pic_irq[i]);
     }
 
diff --git a/hw/exynos4210_uart.c b/hw/exynos4210_uart.c
index 73a9c18f30..ccc47804f9 100644
--- a/hw/exynos4210_uart.c
+++ b/hw/exynos4210_uart.c
@@ -246,7 +246,7 @@ static uint32_t exynos4210_uart_Tx_FIFO_trigger_level(Exynos4210UartState *s)
     uint32_t level = 0;
     uint32_t reg;
 
-    reg = (s->reg[I_(UFCON)] && UFCON_Tx_FIFO_TRIGGER_LEVEL) >>
+    reg = (s->reg[I_(UFCON)] & UFCON_Tx_FIFO_TRIGGER_LEVEL) >>
             UFCON_Tx_FIFO_TRIGGER_LEVEL_SHIFT;
 
     switch (s->channel) {
@@ -275,9 +275,9 @@ static void exynos4210_uart_update_irq(Exynos4210UartState *s)
      * The Tx interrupt is always requested if the number of data in the
      * transmit FIFO is smaller than the trigger level.
      */
-    if (s->reg[I_(UFCON)] && UFCON_FIFO_ENABLE) {
+    if (s->reg[I_(UFCON)] & UFCON_FIFO_ENABLE) {
 
-        uint32_t count = (s->reg[I_(UFSTAT)] && UFSTAT_Tx_FIFO_COUNT) >>
+        uint32_t count = (s->reg[I_(UFSTAT)] & UFSTAT_Tx_FIFO_COUNT) >>
                 UFSTAT_Tx_FIFO_COUNT_SHIFT;
 
         if (count <= exynos4210_uart_Tx_FIFO_trigger_level(s)) {
diff --git a/hw/exynos4_boards.c b/hw/exynos4_boards.c
index 553a02b910..ea32c51dcc 100644
--- a/hw/exynos4_boards.c
+++ b/hw/exynos4_boards.c
@@ -70,6 +70,7 @@ static struct arm_boot_info exynos4_board_binfo = {
     .loader_start     = EXYNOS4210_BASE_BOOT_ADDR,
     .smp_loader_start = EXYNOS4210_SMP_BOOT_ADDR,
     .nb_cpus          = EXYNOS4210_NCPUS,
+    .write_secondary_boot = exynos4210_write_secondary,
 };
 
 static QEMUMachine exynos4_machines[EXYNOS4_NUM_OF_BOARDS];
diff --git a/hw/realview_gic.c b/hw/realview_gic.c
index 071ef13c9e..5bc37a7120 100644
--- a/hw/realview_gic.c
+++ b/hw/realview_gic.c
@@ -9,39 +9,45 @@
 
 #include "sysbus.h"
 
-#define NCPU 1
-
-/* Only a single "CPU" interface is present.  */
-static inline int
-gic_get_current_cpu(void)
-{
-  return 0;
-}
-
-#include "arm_gic.c"
-
 typedef struct {
-    gic_state gic;
+    SysBusDevice busdev;
+    DeviceState *gic;
     MemoryRegion container;
 } RealViewGICState;
 
-static void realview_gic_map_setup(RealViewGICState *s)
+static void realview_gic_set_irq(void *opaque, int irq, int level)
 {
-    memory_region_init(&s->container, "realview-gic-container", 0x2000);
-    memory_region_add_subregion(&s->container, 0, &s->gic.cpuiomem[0]);
-    memory_region_add_subregion(&s->container, 0x1000, &s->gic.iomem);
+    RealViewGICState *s = (RealViewGICState *)opaque;
+    qemu_set_irq(qdev_get_gpio_in(s->gic, irq), level);
 }
 
 static int realview_gic_init(SysBusDevice *dev)
 {
-    RealViewGICState *s = FROM_SYSBUSGIC(RealViewGICState, dev);
-
+    RealViewGICState *s = FROM_SYSBUS(RealViewGICState, dev);
+    SysBusDevice *busdev;
     /* The GICs on the RealView boards have a fixed nonconfigurable
      * number of interrupt lines, so we don't need to expose this as
      * a qdev property.
      */
-    gic_init(&s->gic, 96);
-    realview_gic_map_setup(s);
+    int numirq = 96;
+
+    s->gic = qdev_create(NULL, "arm_gic");
+    qdev_prop_set_uint32(s->gic, "num-cpu", 1);
+    qdev_prop_set_uint32(s->gic, "num-irq", numirq);
+    qdev_init_nofail(s->gic);
+    busdev = sysbus_from_qdev(s->gic);
+
+    /* Pass through outbound IRQ lines from the GIC */
+    sysbus_pass_irq(dev, busdev);
+
+    /* Pass through inbound GPIO lines to the GIC */
+    qdev_init_gpio_in(&s->busdev.qdev, realview_gic_set_irq, numirq - 32);
+
+    memory_region_init(&s->container, "realview-gic-container", 0x2000);
+    memory_region_add_subregion(&s->container, 0,
+                                sysbus_mmio_get_region(busdev, 1));
+    memory_region_add_subregion(&s->container, 0x1000,
+                                sysbus_mmio_get_region(busdev, 0));
     sysbus_init_mmio(dev, &s->container);
     return 0;
 }