diff --git a/xen/arch/arm/gic-v2.c b/xen/arch/arm/gic-v2.c
index 0fcb894..02db5f2 100644
--- a/xen/arch/arm/gic-v2.c
+++ b/xen/arch/arm/gic-v2.c
@@ -685,6 +685,35 @@ static void __init gicv2_dt_init(void)
 }
 
 #ifdef CONFIG_ACPI
+static u32 gicv2_make_hwdom_madt(const struct domain *d, u32 offset)
+{
+    struct acpi_subtable_header *header;
+    struct acpi_madt_generic_interrupt *host_gicc, *gicc;
+    u32 i, size, table_len = 0;
+    u8 *base_ptr = d->arch.efi_acpi_table + offset;
+
+    header = acpi_table_get_entry_madt(ACPI_MADT_TYPE_GENERIC_INTERRUPT, 0);
+    if ( !header )
+        panic("Can't get GICC entry");
+    host_gicc = container_of(header, struct acpi_madt_generic_interrupt,
+                             header);
+
+    size = sizeof(struct acpi_madt_generic_interrupt);
+    /* Add Generic Interrupt */
+    for ( i = 0; i < d->max_vcpus; i++ )
+    {
+        gicc = (struct acpi_madt_generic_interrupt *)(base_ptr + table_len);
+        ACPI_MEMCPY(gicc, host_gicc, size);
+        gicc->cpu_interface_number = i;
+        gicc->uid = i;
+        gicc->flags = ACPI_MADT_ENABLED;
+        gicc->arm_mpidr = vcpuid_to_vaffinity(i);
+        table_len += size;
+    }
+
+    return table_len;
+}
+
 static int __init
 gic_acpi_parse_madt_cpu(struct acpi_subtable_header *header,
                         const unsigned long end)
@@ -776,6 +805,10 @@ static void __init gicv2_acpi_init(void)
 }
 #else
 static void __init gicv2_acpi_init(void) { }
+static u32 gicv2_make_hwdom_madt(const struct domain *d, u32 offset)
+{
+    return 0;
+}
 #endif
 
 static int __init gicv2_init(void)
@@ -868,6 +901,7 @@ const static struct gic_hw_operations gicv2_ops = {
     .read_vmcr_priority  = gicv2_read_vmcr_priority,
     .read_apr            = gicv2_read_apr,
     .make_hwdom_dt_node  = gicv2_make_hwdom_dt_node,
+    .make_hwdom_madt     = gicv2_make_hwdom_madt,
 };
 
 /* Set up the GIC */
diff --git a/xen/arch/arm/gic-v3.c b/xen/arch/arm/gic-v3.c
index f83fd88..d9fce4b 100644
--- a/xen/arch/arm/gic-v3.c
+++ b/xen/arch/arm/gic-v3.c
@@ -1236,6 +1236,48 @@ static void __init gicv3_dt_init(void)
 }
 
 #ifdef CONFIG_ACPI
+static u32 gicv3_make_hwdom_madt(const struct domain *d, u32 offset)
+{
+    struct acpi_subtable_header *header;
+    struct acpi_madt_generic_interrupt *host_gicc, *gicc;
+    struct acpi_madt_generic_redistributor *gicr;
+    u8 *base_ptr = d->arch.efi_acpi_table + offset;
+    u32 i, table_len = 0, size;
+
+    /* Add Generic Interrupt */
+    header = acpi_table_get_entry_madt(ACPI_MADT_TYPE_GENERIC_INTERRUPT, 0);
+    if ( !header )
+        panic("Can't get GICC entry");
+    host_gicc = container_of(header, struct acpi_madt_generic_interrupt,
+                             header);
+
+    size = sizeof(struct acpi_madt_generic_interrupt);
+    for ( i = 0; i < d->max_vcpus; i++ )
+    {
+        gicc = (struct acpi_madt_generic_interrupt *)(base_ptr + table_len);
+        ACPI_MEMCPY(gicc, host_gicc, size);
+        gicc->cpu_interface_number = i;
+        gicc->uid = i;
+        gicc->flags = ACPI_MADT_ENABLED;
+        gicc->arm_mpidr = vcpuid_to_vaffinity(i);
+        table_len += size;
+    }
+
+    /* Add Generic Redistributor */
+    size = sizeof(struct acpi_madt_generic_redistributor);
+    for ( i = 0; i < d->arch.vgic.nr_regions; i++ )
+    {
+        gicr = (struct acpi_madt_generic_redistributor *)(base_ptr + table_len);
+        gicr->header.type = ACPI_MADT_TYPE_GENERIC_REDISTRIBUTOR;
+        gicr->header.length = size;
+        gicr->base_address = d->arch.vgic.rdist_regions[i].base;
+        gicr->length = d->arch.vgic.rdist_regions[i].size;
+        table_len += size;
+    }
+
+    return table_len;
+}
+
 static int __init
 gic_acpi_parse_madt_cpu(struct acpi_subtable_header *header,
                         const unsigned long end)
@@ -1380,6 +1422,10 @@ static void __init gicv3_acpi_init(void)
 }
 #else
 static void __init gicv3_acpi_init(void) { }
+static u32 gicv3_make_hwdom_madt(const struct domain *d, u32 offset)
+{
+    return 0;
+}
 #endif
 
 /* Set up the GIC */
@@ -1474,6 +1520,7 @@ static const struct gic_hw_operations gicv3_ops = {
     .read_apr            = gicv3_read_apr,
     .secondary_init      = gicv3_secondary_cpu_init,
     .make_hwdom_dt_node  = gicv3_make_hwdom_dt_node,
+    .make_hwdom_madt     = gicv3_make_hwdom_madt,
 };
 
 static int __init gicv3_dt_preinit(struct dt_device_node *node, const void *data)
diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index fbbe37f..6d32432 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -739,6 +739,11 @@ int gic_make_hwdom_dt_node(const struct domain *d,
     return gic_hw_ops->make_hwdom_dt_node(d, gic, fdt);
 }
 
+u32 gic_make_hwdom_madt(const struct domain *d, u32 offset)
+{
+    return gic_hw_ops->make_hwdom_madt(d, offset);
+}
+
 /*
  * Local variables:
  * mode: C
diff --git a/xen/include/asm-arm/gic.h b/xen/include/asm-arm/gic.h
index 7bd06e1..4cf003d 100644
--- a/xen/include/asm-arm/gic.h
+++ b/xen/include/asm-arm/gic.h
@@ -358,12 +358,15 @@ struct gic_hw_operations {
     /* Create GIC node for the hardware domain */
     int (*make_hwdom_dt_node)(const struct domain *d,
                               const struct dt_device_node *gic, void *fdt);
+    /* Create MADT table for the hardware domain */
+    u32 (*make_hwdom_madt)(const struct domain *d, u32 offset);
 };
 
 void register_gic_ops(const struct gic_hw_operations *ops);
 int gic_make_hwdom_dt_node(const struct domain *d,
                            const struct dt_device_node *gic,
                            void *fdt);
+u32 gic_make_hwdom_madt(const struct domain *d, u32 offset);
 
 #endif /* __ASSEMBLY__ */
 #endif
