Index: /trunk/include/VBox/gic.h
===================================================================
--- /trunk/include/VBox/gic.h	(revision 107983)
+++ /trunk/include/VBox/gic.h	(revision 107984)
@@ -162,4 +162,5 @@
 # define GIC_DIST_REG_TYPER_ESPI_RANGE                  (  RT_BIT_32(27) | RT_BIT_32(28) | RT_BIT(29) \
                                                          | RT_BIT_32(30) | RT_BIT_32(31))
+# define GIC_DIST_REG_TYPER_ESPI_RANGE_BIT              27
 # define GIC_DIST_REG_TYPER_ESPI_RANGE_SET(a_Range)     (((a_Range) << 27) & GIC_DIST_REG_TYPER_ESPI_RANGE)
 
Index: /trunk/src/VBox/VMM/VMMAll/GICAll.cpp
===================================================================
--- /trunk/src/VBox/VMM/VMMAll/GICAll.cpp	(revision 107983)
+++ /trunk/src/VBox/VMM/VMMAll/GICAll.cpp	(revision 107984)
@@ -407,5 +407,6 @@
             break;
         case GIC_DIST_REG_TYPER_OFF:
-            *puValue =   GIC_DIST_REG_TYPER_NUM_ITLINES_SET(pThis->uItLinesNumber)
+            Assert(pThis->uMaxSpi > 0 && pThis->uMaxSpi < GIC_DIST_REG_TYPER_NUM_ITLINES);
+            *puValue =   GIC_DIST_REG_TYPER_NUM_ITLINES_SET(pThis->uMaxSpi)
                        | GIC_DIST_REG_TYPER_NUM_PES_SET(0)      /* 1 PE */ /** @todo r=ramshankar: Should this be pVCpu->cCpus? Currently it means 'ARE' must always be used? */
                        /*| GIC_DIST_REG_TYPER_ESPI*/            /** @todo */
Index: /trunk/src/VBox/VMM/VMMR3/GICR3.cpp
===================================================================
--- /trunk/src/VBox/VMM/VMMR3/GICR3.cpp	(revision 107983)
+++ /trunk/src/VBox/VMM/VMMR3/GICR3.cpp	(revision 107984)
@@ -398,6 +398,8 @@
     PDMDEV_VALIDATE_CONFIG_RETURN(pDevIns, "DistributorMmioBase|RedistributorMmioBase|ItsMmioBase"
                                            "|ArchRev"
-                                           "|ArchExtNmi"
-                                           "|ItLinesNumber", "");
+                                           "|Nmi"
+                                           "|MaxSpi"
+                                           "|MaxExtSpi"
+                                           "|PpiNum", "");
 
 #if 0
@@ -422,33 +424,61 @@
     else
         return PDMDevHlpVMSetError(pDevIns, VERR_INVALID_PARAMETER, RT_SRC_POS,
-                                   N_("Configuration error: \"ArchRev\" %u is not supported"), pGicDev->uArchRev);
-
-    /** @devcfgm{gic, ArchExtNmi, bool, false}
+                                   N_("Configuration error: \"ArchRev\" value %u is not supported"), pGicDev->uArchRev);
+
+    /** @devcfgm{gic, Nmi, bool, false}
      * Configures whether NMIs are supported (GICD_TYPER.NMI). */
-    rc = pHlp->pfnCFGMQueryBoolDef(pCfg, "ArchExtNmi", &pGicDev->fNmi, false);
-    AssertLogRelRCReturn(rc, rc);
-    if (   !pGicDev->fNmi
-        || pGicDev->uArchRev >= 3)
+    rc = pHlp->pfnCFGMQueryBoolDef(pCfg, "Nmi", &pGicDev->fNmi, false);
+    AssertLogRelRCReturn(rc, rc);
+
+    /** @devcfgm{gic, ExtSpi, bool, false}
+     * Configures whether extended SPIs are supported (GICD_TYPER.ESPI). */
+    rc = pHlp->pfnCFGMQueryBoolDef(pCfg, "ExtSpi", &pGicDev->fExtSpi, false);
+    AssertLogRelRCReturn(rc, rc);
+
+    /** @devcfgm{gic, MaxSpi, uint16_t, 1}
+     * Configures GICD_TYPER.ItLinesNumber.
+     *
+     * For the INTID range [32,1023], configures the maximum SPI supported. Valid values
+     * are [1,31] which equates to interrupt IDs [63,1023]. A value of 0 implies SPIs
+     * are supported. We don't allow configuring this value as it's expected that
+     * most guests would assume support for SPIs. */
+    AssertCompile(GIC_DIST_REG_TYPER_NUM_ITLINES == 31);
+    rc = pHlp->pfnCFGMQueryU16Def(pCfg, "MaxSpi", &pGicDev->uMaxSpi, 1 /* 63 INTIDs */);
+    AssertLogRelRCReturn(rc, rc);
+    if (pGicDev->uMaxSpi - 1 < 31)
     { /* likely */ }
     else
         return PDMDevHlpVMSetError(pDevIns, VERR_INVALID_PARAMETER, RT_SRC_POS,
-                                   N_("Configuration error: \"ArchExtNmi\" requires architecture revision v3 or newer"));
-
-    /** @devcfgm{gic, ItLinesNumber, uint16_t, 1}
-     * Configures GICD_TYPER.ItLinesNumber, bits [4:0].
+                                   N_("Configuration error: \"MaxSpi\" must be in the range [1,%u]"),
+                                   GIC_DIST_REG_TYPER_NUM_ITLINES);
+
+    /** @devcfgm{gic, MaxExtSpi, uint16_t, 31}
+     * Configures GICD_TYPER.ESPI_range.
      *
-     * For the INTID range 32-1023, configures the maximum SPI supported. Valid values
-     * are [1, 31] which equates to interrupt IDs [63, 1023]. A value of 0 indicates no
-     * SPIs are supported. We do not allow configuring this value as it's expected most
-     * guests would assume support for SPIs. */
-    rc = pHlp->pfnCFGMQueryU16Def(pCfg, "ItLinesNumber", &pGicDev->uItLinesNumber, 1 /* 63 interrupt IDs */);
-    AssertLogRelRCReturn(rc, rc);
-    if (   pGicDev->uItLinesNumber
-        && !(pGicDev->uItLinesNumber & ~GIC_DIST_REG_TYPER_NUM_ITLINES))
+     * For the extended SPI range [4096,5119], configures the maximum extended SPI
+     * supported. Valid values are [0,31] which equates to extended SPI INTIDs
+     * [4096,5119]. This is ignored (set to 0) when extended SPIs are disabled. */
+    AssertCompile(GIC_DIST_REG_TYPER_ESPI_RANGE >> GIC_DIST_REG_TYPER_ESPI_RANGE_BIT == 31);
+    rc = pHlp->pfnCFGMQueryU16Def(pCfg, "MaxExtSpi", &pGicDev->uMaxExtSpi, 31);
+    AssertLogRelRCReturn(rc, rc);
+    if (pGicDev->uMaxExtSpi <= 31)
     { /* likely */ }
     else
         return PDMDevHlpVMSetError(pDevIns, VERR_INVALID_PARAMETER, RT_SRC_POS,
-                                   N_("Configuration error: \"ItLinesNumber\" must be in the range [1,%u]"),
-                                   GIC_DIST_REG_TYPER_NUM_ITLINES);
+                                   N_("Configuration error: \"MaxExtSpi\" must be in the range [0,31]"));
+
+    /** @devcfgm{gic, MaxExtPpi, uint16_t, 0}
+     * Configures GICR_TYPER.PPInum.
+     *
+     * For the extended PPI INTIDs [31,1056,1119], configures the maximum extended
+     * PPI supported. Valid values are [0,1,2] which equates [31,1087,1119]. A value of
+     * 0 implies extended PPIs are not supported. */
+    rc = pHlp->pfnCFGMQueryU8Def(pCfg, "PpiNum", &pGicDev->fPpiNum, 0);
+    AssertLogRelRCReturn(rc, rc);
+    if (pGicDev->fPpiNum <= GIC_REDIST_REG_TYPER_PPI_NUM_MAX_1119)
+    { /* likely */ }
+    else
+        return PDMDevHlpVMSetError(pDevIns, VERR_INVALID_PARAMETER, RT_SRC_POS,
+                                   N_("Configuration error: \"PpiNum\" must be in the range [0,2]"));
 
     /*
Index: /trunk/src/VBox/VMM/include/GICInternal.h
===================================================================
--- /trunk/src/VBox/VMM/include/GICInternal.h	(revision 107983)
+++ /trunk/src/VBox/VMM/include/GICInternal.h	(revision 107984)
@@ -105,10 +105,16 @@
     /** @name Configurables.
      * @{ */
-    /** The maximum SPI supported (GICD_TYPER.ItsLinesNumber). */
-    uint16_t                    uItLinesNumber;
     /** The GIC architecture (GICD_PIDR2.ArchRev and GICR_PIDR2.ArchRev). */
     uint8_t                     uArchRev;
+    /** Extended PPIs supported (GICR_TYPER.PpiNum). */
+    uint8_t                     fPpiNum;
+    /** Whether extended SPIs are supported (GICD_TYPER.ESPI). */
+    bool                        fExtSpi;
     /** Whether NMIs are supported (GICD_TYPER.NMI). */
     bool                        fNmi;
+    /** The maximum SPI supported (GICD_TYPER.ItsLinesNumber). */
+    uint16_t                    uMaxSpi;
+    /** Maximum extended SPI supported (GICR_TYPER.ESPI_range).  */
+    uint16_t                    uMaxExtSpi;
     /** @} */
 } GICDEV;
