[REQUIREMENTS][PATCH v2 6/6] reqs: add GICv4 direct-delivery requirements

[Mykola Kvach <mykola_kvach@xxxxxxxx>]

Add software requirements for Xen's Arm GICv4 and GICv4.1 direct-delivery
support.

The host GICv4 requirements cover backend state such as vPE lifetime,
residency, doorbells, direct vLPI mappings and GICv4 ITS command handling.

The vGIC direct-delivery requirements cover guest-visible direct SGI
capability, request control and direct-vSGI state handling.

These requirements do not expose GICv4 as a guest interrupt-controller
architecture and do not replace the existing GICv3, ITS, vITS or common
interrupt-management requirements.

Signed-off-by: Mykola Kvach <mykola_kvach@xxxxxxxx>
---
 .../arm64/index.rst                           |   1 +
 .../arm64/vgic_direct_delivery.rst            | 166 ++++++
 .../physical_resources/arm64/gicv4.rst        | 515 ++++++++++++++++++
 .../physical_resources/arm64/index.rst        |   1 +
 4 files changed, 683 insertions(+)
 create mode 100644 
software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/vgic_direct_delivery.rst
 create mode 100644 
software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/gicv4.rst

diff --git 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
index 7896770..9d83bbf 100644
--- 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
+++ 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/index.rst
@@ -10,4 +10,5 @@ Arm64
    gicv3
    its
    tee
+   vgic_direct_delivery
    viommu
diff --git 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/vgic_direct_delivery.rst
 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/vgic_direct_delivery.rst
new file mode 100644
index 0000000..dc364b1
--- /dev/null
+++ 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/vgic_direct_delivery.rst
@@ -0,0 +1,166 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+vGIC direct-delivery requirements
+=================================
+
+The following requirements define guest-visible vGIC behavior that can be 
backed
+by GICv4 direct-delivery mechanisms [1].
+
+These requirements do not expose GICv4 as a guest interrupt-controller
+architecture. GICv4 remains a Xen backend used to implement selected
+guest-visible vGIC behavior when the required host capabilities are available.
+
+Direct vSGI backend selection
+-----------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_backend_selection~1`
+
+Description:
+Xen shall enable a direct-vSGI backend for a selected domain only when the
+domain uses the virtual GICv3 model, the GICv4 vLPI backend is available, a
+GICv4.1 host ITS is available, and the selected domain has initialized
+per-domain GICv4 direct-delivery state.
+
+Rationale:
+Direct vSGI delivery requires GICv4.1 support and vPE state. Enabling the
+backend without the required host capabilities would expose a direct delivery
+mode that Xen cannot safely provide.
+
+Covers:
+ - `XenPRQ~intc~1`
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest direct SGI capability exposure
+------------------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_cap_exposure~1`
+
+Description:
+Xen shall derive the guest-visible ``GICD_TYPER2.nASSGIcap`` capability from
+direct-vSGI backend availability for the selected domain.
+
+Rationale:
+``GICD_TYPER2.nASSGIcap`` is a guest-visible virtual Distributor capability. A
+guest uses this field to determine whether it may request the direct SGI
+active-state model through ``GICD_CTLR.nASSGIreq``. Xen derives this capability
+from the virtual GICv3 domain model and the GICv4.1 direct-vSGI backend
+available for that domain.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Guest direct SGI active-state request control
+---------------------------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_active_state_request_control~1`
+
+Description:
+Xen shall accept a guest direct SGI active-state request through
+``GICD_CTLR.nASSGIreq`` only when ``GICD_TYPER2.nASSGIcap`` is exposed for the
+selected domain.
+
+Rationale:
+``GICD_CTLR.nASSGIreq`` is the guest-visible control that selects the SGI
+active-state model when direct SGI capability is exposed. Xen uses this control
+to switch the domain between software-emulated SGI delivery and direct-vSGI
+delivery while preserving the guest-visible virtual GIC state.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vSGI configuration source
+--------------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_conf_source~1`
+
+Description:
+Xen shall derive direct-vSGI hardware configuration from the authoritative
+guest-visible virtual GIC software state.
+
+Rationale:
+Direct-vSGI hardware state is a delivery backend, not the guest-visible GIC
+model. Xen needs guest register readback, software/direct mode switching and
+partial configuration updates to observe one coherent SGI model for enable,
+priority, group and pending-state semantics.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vSGI pending-state preservation
+--------------------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_pending_state_preservation~1`
+
+Description:
+Xen shall preserve guest-visible SGI pending state when switching a vCPU
+between software-emulated SGI delivery and direct-vSGI delivery.
+
+Rationale:
+SGIs are used for inter-vCPU communication. Losing pending state can hang a
+guest, while duplicating pending state can break guest synchronization
+assumptions. When leaving direct-vSGI mode, Xen needs completed hardware
+pending-state information before reinjecting pending SGIs into the software
+vGIC model.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vSGI pending-state readback
+----------------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_pending_state_readback~1`
+
+Description:
+Xen shall consume direct-vSGI pending-state readback only after the
+Redistributor reports that the query has completed and the queried vPEID and
+Redistributor are still the serialized target of the query.
+
+Rationale:
+Direct-vSGI pending-state readback observes Redistributor-side state indexed by
+vPEID. Consuming a busy, stale or ambiguously targeted readback can lose a
+pending vSGI, inject a spurious or duplicate vSGI, or transfer pending state
+from the wrong vPE.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vSGI send mediation
+--------------------------
+
+`XenSSR~arm64_gicv4_direct_vsgi_send_mediation~1`
+
+Description:
+Xen shall mediate guest SGI generation through the selected domain's virtual
+CPU topology before issuing any direct-vSGI hardware operation.
+
+Rationale:
+Guest SGI generation contains guest-controlled affinity, target-list, group and
+SGI INTID fields. Xen translates those fields through the domain's virtual CPU
+topology and issues direct-vSGI operations only for vPEIDs owned by the sending
+domain and selected by that topology.
+
+Covers:
+ - `XenPRQ~virtual_interrupt_controller~1`
+
+Needs:
+ - XenVerTestCase
+
+| [1] Arm Generic Interrupt Controller Architecture Specification (GIC 
architecture version 3 and version 4)
diff --git 
a/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/gicv4.rst
 
b/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/gicv4.rst
new file mode 100644
index 0000000..8224a5c
--- /dev/null
+++ 
b/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/gicv4.rst
@@ -0,0 +1,515 @@
+.. SPDX-License-Identifier: CC-BY-4.0
+
+Host GICv4 requirements
+=======================
+
+The following requirements are related to Xen's host-side support for the
+Arm Generic Interrupt Controller version 4 (GICv4) architecture [1].
+
+The GICv4 requirements describe Xen's direct-delivery backend state. In the
+current vITS command path, guest ITS commands are exposed to the hardware
+domain.
+
+
+GICv4 direct-delivery backend selection
+---------------------------------------
+
+`XenSSR~arm64_gicv4_direct_delivery_backend_selection~1`
+
+Description:
+Xen shall use a GICv4 direct-delivery backend only when the required host ITS
+and Redistributor capabilities are available for the selected domain, vPE or
+device-event mapping.
+
+Rationale:
+GICv4 direct delivery is a Xen backend choice. A vPE can become resident on
+different Redistributors during execution, and a device event is programmed
+through the host ITS associated with the physical DeviceID and EventID. Using a
+direct-delivery backend when a required host component lacks the corresponding
+capability can make interrupt delivery depend on unsupported runtime placement
+or unsupported ITS command semantics.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+GICv4 ITS virtual command capability gating
+-------------------------------------------
+
+`XenSSR~arm64_gicv4_its_virtual_command_capability_gating~1`
+
+Description:
+Xen shall issue GICv4 ITS virtual interrupt commands only through a host ITS
+that reports virtual LPI support, and shall issue GICv4.1-only commands or
+fields only through a host ITS that reports GICv4.1 support. This shall include
+use of:
+
+ - ``VMAPP``
+ - ``VMAPTI`` and ``VMAPI``
+ - ``VMOVP`` and ``VMOVI``
+ - ``VINVALL``
+ - ``VSYNC``
+ - ``VSGI``
+ - ``INVDB``
+
+Rationale:
+GICv4 virtual interrupt commands depend on host ITS virtual LPI capability.
+GICv4.1 commands and fields, including ``INVDB``, ``VSGI`` and GICv4.1
+``VMAPP`` lifetime and default-doorbell fields, are valid only on a GICv4.1
+ITS.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+GICv4 command completion
+------------------------
+
+`XenSSR~arm64_gicv4_command_completion~1`
+
+Description:
+Xen shall treat a GICv4 direct-delivery state transition as successful only
+after the required host ITS command sequence has been issued and completed
+successfully.
+
+Rationale:
+GICv4 ITS commands can create, update or remove hardware-visible virtual
+interrupt state asynchronously. If a required command cannot be issued or does
+not complete, the dependent direct-delivery state cannot be treated as
+committed.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPEID allocation and lifetime
+-----------------------------
+
+`XenSSR~arm64_gicv4_vpeid_allocation_and_lifetime~1`
+
+Description:
+Xen shall allocate a unique vPEID for each GICv4 vPE and shall release that
+vPEID only after the hardware-visible vPE mapping that uses it has been
+removed.
+
+Rationale:
+A vPEID indexes hardware-visible virtual interrupt state. Reusing a vPEID
+before old ITS and Redistributor references have been removed can deliver a
+virtual interrupt to stale or wrong vPE state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPE table entry readiness
+-------------------------
+
+`XenSSR~arm64_gicv4_vpe_table_entry_readiness~1`
+
+Description:
+Xen shall allocate and initialize host GICv4 vPE table backing storage for a
+vPEID before programming a host ITS mapping that can reference that vPEID.
+
+Rationale:
+The host ITS can use the vPEID to locate vPE table state. If the backing table
+entry or its second-level storage is missing or uninitialized, direct delivery
+can consume invalid vPE state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+GICv4.1 shared vPE table common-affinity sharing
+------------------------------------------------
+
+`XenSSR~arm64_gicv4_1_shared_vpe_table_common_affinity_sharing~1`
+
+Description:
+Xen shall share a GICv4.1 vPE table between host ITS or Redistributor
+components only when their computed common LPI affinity matches.
+
+Rationale:
+A shared vPE table can be consumed by multiple Redistributors or ITS
+instances. Sharing outside the compatible common-LPI-affinity scope can make
+different GIC components consume different vPE configuration state for the same
+vPEID.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+GICv4.1 VMAPP lifetime
+----------------------
+
+`XenSSR~arm64_gicv4_1_vmapp_lifetime~1`
+
+Description:
+Xen shall encode GICv4.1 ``VMAPP`` lifetime state according to the
+architectural lifetime of each vPEID mapping.
+
+Rationale:
+In GICv4.1, ``VMAPP`` lifetime fields identify first-map and last-unmap
+operations for virtual pending and configuration table state. Incorrect
+lifetime programming can leave the interrupt routing infrastructure accessing
+stale vPE table, virtual pending table or virtual configuration table state
+after Xen has removed the software owner.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPE publication after initialization
+------------------------------------
+
+`XenSSR~arm64_gicv4_vpe_publication_after_initialization~1`
+
+Description:
+Xen shall make a GICv4 vPE available to direct-vLPI, doorbell and direct-vSGI
+paths only after the vPEID, virtual pending table, vPE table entry, host
+VMAPP mappings and doorbell state required for that vPE have been
+initialized successfully.
+
+Rationale:
+A published vPE can be used by direct-vLPI, doorbell and direct-vSGI paths.
+Making the vPE available before required backing state is ready can allow later
+direct-delivery operations to consume partial or invalid vPE state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Single vPE residency
+--------------------
+
+`XenSSR~arm64_gicv4_single_vpe_residency~1`
+
+Description:
+Xen shall keep each GICv4 vPE resident on at most one Redistributor at any
+time.
+
+Rationale:
+A vPE represents one hardware-visible virtual CPU interrupt context. Making the
+same vPE resident on more than one Redistributor can cause duplicate delivery,
+cross-CPU delivery or ambiguous ownership of pending virtual interrupt state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPE residency synchronization
+-----------------------------
+
+`XenSSR~arm64_gicv4_vpe_residency_synchronization~1`
+
+Description:
+Xen shall rely on a vPE residency transition only after the architectural
+completion state for that transition has been observed.
+
+Rationale:
+The Redistributor can update or consume virtual pending state asynchronously
+during vPE residency transitions. Reusing a Redistributor, reusing vPE pending
+state, or freeing old vPE resources before synchronization can lose pending
+virtual interrupts, duplicate virtual interrupts, corrupt the wrong pending
+table, or make doorbell decisions from stale state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPE movement serialization
+--------------------------
+
+`XenSSR~arm64_gicv4_vpe_movement_serialization~1`
+
+Description:
+Xen shall serialize vPE movement with GICv4 operations that depend on the
+vPE's current Redistributor target.
+
+Rationale:
+vPE movement changes the Redistributor that owns the vPE. Register-based
+invalidation, doorbell handling, virtual LPI operations and direct-vSGI
+pending-state readback can target Redistributor-resident state. Issuing such
+operations against a stale Redistributor can leave cached state unchanged or
+operate on the wrong state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Doorbell LPI ownership
+----------------------
+
+`XenSSR~arm64_gicv4_doorbell_lpi_ownership~1`
+
+Description:
+Xen shall reserve physical LPIs used as GICv4 doorbells for Xen use and shall
+associate each doorbell with the owning domain and vCPU.
+
+Rationale:
+Doorbells are hypervisor wakeup signals for non-resident vPEs. Guest ownership
+or reuse of a doorbell LPI can suppress, spoof or misroute hypervisor wakeups.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Doorbell invalidation and readiness
+-----------------------------------
+
+`XenSSR~arm64_gicv4_doorbell_invalidation_and_readiness~1`
+
+Description:
+Xen shall update and invalidate GICv4 doorbell state through the
+architecture-supported backend path before relying on the updated doorbell
+state.
+
+Rationale:
+Doorbell state can be cached by the GIC. Xen uses GICv4.1 ``INVDB``,
+Redistributor register invalidation, or a proxy-device invalidation path
+depending on the selected backend.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Doorbell LPI observation
+------------------------
+
+`XenSSR~arm64_gicv4_doorbell_lpi_observation~1`
+
+Description:
+Xen shall mark the vPE as having pending virtual interrupt work and kick
+the owning vCPU when Xen receives a GICv4 doorbell LPI for a non-resident vPE.
+
+Rationale:
+A doorbell is a hypervisor wakeup signal for a non-resident vPE. Marking the
+vPE pending state and kicking the vCPU makes the wakeup visible to Xen's
+scheduler.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+GICv4.1 non-resident pending-state indication
+---------------------------------------------
+
+`XenSSR~arm64_gicv4_1_non_resident_pending_state_indication~1`
+
+Description:
+Xen shall record the architectural ``PendingLast`` indication reported by
+``GICR_VPENDBASER`` before relying on the vPE non-resident state when making
+a GICv4.1 vPE non-resident
+
+Rationale:
+``PendingLast`` reports whether pending enabled virtual interrupts remain after
+the non-resident transition. Xen uses this state as part of its scheduling and
+wakeup handling for the vPE.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI mapping ownership
+-----------------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_mapping_ownership~1`
+
+Description:
+Xen shall install a hardware-forwarded vLPI mapping only when the target
+virtual INTID is valid for the selected domain and the mapping has one
+domain/device/event/vPE/vINTID owner.
+
+Rationale:
+GICv4 virtual LPI mappings are keyed by device events and vPE state. Reusing a
+DeviceID/EventID mapping, aliasing vPEID/vINTID ownership, or using an
+out-of-range virtual INTID can cause wrong-owner delivery, duplicate delivery,
+missed invalidation or constrained unpredictable GIC behaviour.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI setup recovery
+--------------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_setup_recovery~1`
+
+Description:
+Xen shall restore the previous safe host LPI mapping or otherwise keep the
+event unavailable when a direct vLPI setup operation fails after the previous
+mapping has been removed.
+
+Rationale:
+Direct vLPI setup can discard the previous mapping before ``VMAPTI`` succeeds.
+If ``VMAPTI`` fails and the event is left without a safe mapping, subsequent
+device events can be lost or delivered through stale state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI unmap ordering
+--------------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_unmap_ordering~1`
+
+Description:
+Xen shall remove a direct vLPI mapping, restore the host physical LPI mapping,
+invalidate the affected event state and then release the software vLPI mapping
+state.
+
+Rationale:
+A mapped event can remain visible to the host ITS and Redistributor until the
+hardware mapping and cached state have been updated. Releasing software mapping
+state before restoring and invalidating the host mapping can leave hardware
+delivery targeting stale domain state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI movement
+--------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_movement~1`
+
+Description:
+Xen shall move a direct vLPI mapping to another vPE using the GICv4 virtual
+movement operation and shall synchronize the old vPE before relying on a later
+movement of the same event.
+
+Rationale:
+GICv4 movement updates the vPEID associated with the event and can move
+pending state. The architecture requires synchronization between repeated moves
+of the same virtual interrupt to prevent pending-state loss or delivery to the
+old vPE.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI property update
+---------------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_property_update~1`
+
+Description:
+Xen shall update the virtual LPI property table and perform the required
+direct-delivery invalidation before relying on updated virtual LPI enable or
+priority state.
+
+Rationale:
+The GIC can cache virtual LPI property state. Updating the virtual property
+table without completing the corresponding invalidation can make direct
+delivery use stale enable or priority state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+Direct vLPI doorbell update
+---------------------------
+
+`XenSSR~arm64_gicv4_direct_vlpi_doorbell_update~1`
+
+Description:
+Xen shall update the doorbell setting for an existing direct vLPI mapping using
+a GICv4 movement operation that preserves the existing event mapping.
+
+Rationale:
+Re-issuing a mapping command for an already mapped DeviceID and EventID has
+unpredictable architectural behaviour. Xen changes the doorbell association for
+an existing mapping through a virtual movement operation targeting the same
+vPE.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vLPI invalidation
+-----------------
+
+`XenSSR~arm64_gicv4_vlpi_invalidation~1`
+
+Description:
+Xen shall perform GICv4 virtual interrupt invalidation through the
+architecture-supported path for the affected event or vPE and shall wait for
+completion before relying on the invalidated state.
+
+Rationale:
+GICv4 virtual interrupt state can be cached in Redistributors or ITS-visible
+state. Xen uses ITS virtual invalidation, GICv4.1 register invalidation or
+proxy invalidation according to backend capability. Relying on updated virtual
+interrupt state before invalidation completion can preserve stale delivery
+state.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+vPE teardown ordering
+---------------------
+
+`XenSSR~arm64_gicv4_vpe_teardown_ordering~1`
+
+Description:
+Xen shall unmap a vPE from every host ITS that can reference the vPE before
+freeing the vPEID or virtual pending table used by that vPE.
+
+Rationale:
+A host ITS can retain hardware-visible references to vPEID and virtual pending
+table state until the corresponding ``VMAPP`` unmap operation has completed.
+Freeing the vPEID or virtual pending table before the vPE has been unmapped
+can create stale hardware-visible references.
+
+Covers:
+ - `XenPRQ~intc~1`
+
+Needs:
+ - XenVerTestCase
+
+| [1] Arm Generic Interrupt Controller Architecture Specification (GIC 
architecture version 3 and version 4)
diff --git 
a/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/index.rst
 
b/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/index.rst
index cd1aaca..da8cd1e 100644
--- 
a/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/index.rst
+++ 
b/software_safety_reqs/domain_creation_and_runtime/physical_resources/arm64/index.rst
@@ -7,6 +7,7 @@ Arm64
    :maxdepth: 1
 
    gicv3
+   gicv4
    its
    p2m
    pci_host_rcar
-- 
2.43.0