diff --git a/include/plat/default/plat/machine.h b/include/plat/default/plat/machine.h
new file mode 100644
index 000000000..8cb9b5e4b
--- /dev/null
+++ b/include/plat/default/plat/machine.h
@@ -0,0 +1,14 @@
+/*
+ * 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 <plat/machine/devices_gen.h>
+#include <plat/platform_gen.h>
\ No newline at end of file
diff --git a/include/plat/default/plat/machine/hardware.h b/include/plat/default/plat/machine/hardware.h
new file mode 100644
index 000000000..27452a0d6
--- /dev/null
+++ b/include/plat/default/plat/machine/hardware.h
@@ -0,0 +1,21 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#ifndef __PLAT_MACHINE_HARDWARE_H
+#define __PLAT_MACHINE_HARDWARE_H
+#include <config.h>
+#include <types.h>
+#include <basic_types.h>
+#include <linker.h>
+#include <machine/io.h>
+
+#endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/default/plat/machine/timer.h b/include/plat/default/plat/machine/timer.h
new file mode 100644
index 000000000..b65d1c6cd
--- /dev/null
+++ b/include/plat/default/plat/machine/timer.h
@@ -0,0 +1,17 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#ifndef __PLAT_MACHINE_TIMER_H
+#define __PLAT_MACHINE_TIMER_H
+
+
+#endif /* !__PLAT_MACHINE_TIMER_H */
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index f82d4ebaf..835c33977 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -66,6 +66,18 @@ elseif(KernelSel4ArchAarch64)
     set_kernel_64()
 endif()
 
+function(declare_default_headers timer_frequency max_irq irq_header timer_header)
+    set(CONFIGURE_TIMER_FREQUENCY "${timer_frequency}")
+    set(CONFIGURE_MAX_IRQ "${max_irq}")
+    set(CONFIGURE_INTERRUPT_CONTROLLER "${irq_header}")
+    set(CONFIGURE_TIMER "${timer_header}")
+    configure_file(
+        src/arch/arm/platform_gen.h.in ${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/platform_gen.h
+        @ONLY
+    )
+    include_directories(include/plat/default)
+endfunction()
+
 # Include all the platforms. For all of the common variables we set a default value here
 # and let the platforms override them.
 set(KernelArmMachFeatureModifiers "" CACHE INTERNAL "")
diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in
new file mode 100644
index 000000000..e2653cf26
--- /dev/null
+++ b/src/arch/arm/platform_gen.h.in
@@ -0,0 +1,25 @@
+/*
+ * 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)
+ */
+
+#ifndef __ARM_PLAT_H
+#define __ARM_PLAT_H
+
+#define TIMER_CLOCK_HZ @CONFIGURE_TIMER_FREQUENCY@
+enum IRQConstants {
+    maxIRQ                      = @CONFIGURE_MAX_IRQ@
+} platform_interrupt_t;
+
+
+#include <@CONFIGURE_INTERRUPT_CONTROLLER@>
+#include <@CONFIGURE_TIMER@>
+
+#endif /* !__ARM_PLAT_H */