diff --git a/include/arch/arm/arch/64/mode/machine/gic_v3.bf b/include/arch/arm/arch/64/mode/machine/gic_v3.bf
new file mode 100644
index 000000000..31675b665
--- /dev/null
+++ b/include/arch/arm/arch/64/mode/machine/gic_v3.bf
@@ -0,0 +1,68 @@
+--
+-- Copyright 2019, Data61
+-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+-- ABN 41 687 119 230.
+--
+-- This software may be distributed and modified according to the terms of
+-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
+-- See "LICENSE_GPLv2.txt" for details.
+--
+-- @TAG(DATA61_GPL)
+--
+
+#include <config.h>
+-- Default base size: uint64_t
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+base 64(48,0)
+
+block virq_inactive {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_pending {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_active {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_pending_active {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pinitid       10
+    field vintid        32
+}
+
+tagged_union virq virqType {
+    tag virq_inactive       0
+    tag virq_pending        1
+    tag virq_active         2
+    tag virq_pending_active 3
+}
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h
index 7175cddd1..92fd0913c 100644
--- a/include/arch/arm/arch/machine/gic_v3.h
+++ b/include/arch/arm/arch/machine/gic_v3.h
@@ -20,6 +20,7 @@
 #include <mode/smp/smp.h>
 #include <model/statedata.h>
 #include <armv/machine.h>
+#include <mode/machine/gic_v3_gen.h>
 
 #include "gic_common.h"
 
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index 0afe9d8c8..6ccdba289 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -266,5 +266,11 @@ add_bf_source_old(
     "include/arch/arm/arch/${KernelWordSize}"
     "mode/machine"
 )
+add_bf_source_old(
+    "KernelArmHypervisorSupport;Kernel64"
+    "gic_v3.bf"
+    "include/arch/arm/arch/${KernelWordSize}"
+    "mode/machine"
+)
 
 include(src/arch/arm/${KernelWordSize}/config.cmake)