From cf997974a85e6bee6be19895cce43670e0256102 Mon Sep 17 00:00:00 2001
From: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Date: Tue, 13 Aug 2019 09:25:17 +1000
Subject: [PATCH] hardware_gen: Always specify kernel devices

The kernel device IRQs and Frame mappings generated by this script will
only come from nodes specified in the seL4,kernel-devices property of
the chosen node.  Previously these devices were inferred by the script
but this led to false matching and didn't support easily overriding
which devices to match under different configurations or across
different platforms.

Explicitly specifying which devices from the device tree will be used in
the kernel makes it easier to check which devices the kernel is actually
using and makes it easier to change on a per platform or per
configuration basis.
---
 .../allwinnerA20/overlay-allwinnerA20.dts     |  10 +-
 src/plat/am335x/overlay-am335x.dts            |   8 +-
 src/plat/apq8064/overlay-apq8064.dts          |   7 ++
 src/plat/bcm2837/overlay-rpi3.dts             |   8 ++
 src/plat/exynos4/overlay-exynos4.dts          |   8 ++
 src/plat/exynos5/overlay-exynos5250.dts       |   5 +
 src/plat/exynos5/overlay-exynos5410.dts       |   5 +
 src/plat/exynos5/overlay-exynos5422.dts       |   5 +
 src/plat/fvp/config.cmake                     |   1 +
 src/plat/fvp/overlay-fvp.dts                  |  20 ++++
 src/plat/hifive/config.cmake                  |   1 +
 src/plat/hifive/overlay-hifive.dts            |  18 +++
 src/plat/hikey/overlay-hikey.dts              |   4 +
 src/plat/imx31/overlay-kzm.dts                |   5 +
 src/plat/imx6/overlay-sabre.dts               |   7 ++
 src/plat/imx6/overlay-wandq.dts               |   7 ++
 src/plat/imx7/overlay-imx7sabre.dts           |   6 +
 src/plat/imx8m-evk/overlay-imx8mm-evk.dts     |   6 +
 src/plat/imx8m-evk/overlay-imx8mq-evk.dts     |   8 +-
 src/plat/odroidc2/config.cmake                |   1 +
 src/plat/odroidc2/overlay-odroidc2.dts        |  20 ++++
 src/plat/omap3/overlay-omap3.dts              |   5 +-
 src/plat/spike/config.cmake                   |   1 +
 src/plat/spike/overlay-spike.dts              |  17 +++
 src/plat/tk1/overlay-tk1.dts                  |   7 ++
 src/plat/tx1/overlay-tx1.dts                  |   7 ++
 src/plat/tx2/overlay-tx2.dts                  |   4 +
 src/plat/zynq7000/config.cmake                |   1 +
 src/plat/zynq7000/overlay-zynq7000.dts        |  21 ++++
 src/plat/zynqmp/config.cmake                  |   1 +
 src/plat/zynqmp/overlay-zynqmp.dts            |  20 ++++
 tools/hardware.yml                            |   2 -
 tools/hardware_gen.py                         | 106 +++++++++---------
 tools/hardware_schema.yml                     |  28 -----
 34 files changed, 290 insertions(+), 90 deletions(-)
 create mode 100644 src/plat/fvp/overlay-fvp.dts
 create mode 100644 src/plat/hifive/overlay-hifive.dts
 create mode 100644 src/plat/odroidc2/overlay-odroidc2.dts
 create mode 100644 src/plat/spike/overlay-spike.dts
 create mode 100644 src/plat/zynq7000/overlay-zynq7000.dts
 create mode 100644 src/plat/zynqmp/overlay-zynqmp.dts

diff --git a/src/plat/allwinnerA20/overlay-allwinnerA20.dts b/src/plat/allwinnerA20/overlay-allwinnerA20.dts
index dd2921578..a6a58e4d6 100644
--- a/src/plat/allwinnerA20/overlay-allwinnerA20.dts
+++ b/src/plat/allwinnerA20/overlay-allwinnerA20.dts
@@ -11,7 +11,11 @@
  */
 
 / {
-
-	/* This platform doesn't use the arm generic timer for the kernel timer. */
-	/delete-node/ timer;
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/soc@1c00000/interrupt-controller@1c81000},
+		    /* This platform doesn't use the arm generic timer for the kernel timer. */
+		    &{/soc@1c00000/timer@1c20c00};
+	};
 };
diff --git a/src/plat/am335x/overlay-am335x.dts b/src/plat/am335x/overlay-am335x.dts
index 8c70dc73c..33196ce6a 100644
--- a/src/plat/am335x/overlay-am335x.dts
+++ b/src/plat/am335x/overlay-am335x.dts
@@ -12,7 +12,13 @@
 
 / {
 	chosen {
-		seL4,timer = &dmtimer0;
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/ocp/interrupt-controller@48200000},
+		    /* The following devices are used to support the timer used by the kernel */
+		    &dmtimer0, /* OMAP Dual-Mode timer */
+		    &{/ocp/l4_wkup@44c00000/prcm@200000}, /* Power reset and clock manager */
+		    &{/ocp/wdt@44e35000}; /* Watchdog timer */
 	};
 
 	ocp {
diff --git a/src/plat/apq8064/overlay-apq8064.dts b/src/plat/apq8064/overlay-apq8064.dts
index 879851662..49b0d1088 100644
--- a/src/plat/apq8064/overlay-apq8064.dts
+++ b/src/plat/apq8064/overlay-apq8064.dts
@@ -11,6 +11,13 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/soc/interrupt-controller@2000000},
+		    &{/soc/timer@200a000};
+	};
+
 	memory@80000000 {
 		device_type = "memory";
 		/* skip one page to avoid overflow */
diff --git a/src/plat/bcm2837/overlay-rpi3.dts b/src/plat/bcm2837/overlay-rpi3.dts
index 39ee72cfa..e3219d302 100644
--- a/src/plat/bcm2837/overlay-rpi3.dts
+++ b/src/plat/bcm2837/overlay-rpi3.dts
@@ -11,6 +11,14 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial1",
+		    &{/soc/interrupt-controller@7e00b200},
+		    &{/soc/local_intc@40000000},
+		    &{/timer};
+	};
+
 	memory {
 		/* This is configurable in the Pi's config.txt, but we use 128MiB of RAM by default. */
 		reg = <0x00 0x08000000>;
diff --git a/src/plat/exynos4/overlay-exynos4.dts b/src/plat/exynos4/overlay-exynos4.dts
index d97d27f14..ece5d960e 100644
--- a/src/plat/exynos4/overlay-exynos4.dts
+++ b/src/plat/exynos4/overlay-exynos4.dts
@@ -11,6 +11,14 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial1",
+		    &{/soc/interrupt-controller@10490000},
+		    &{/soc/l2-cache-controller@10502000},
+		    &{/soc/mct@10050000};
+	};
+
 	/delete-node/ memory;
 	memory@40000000 {
 		device_type = "memory";
diff --git a/src/plat/exynos5/overlay-exynos5250.dts b/src/plat/exynos5/overlay-exynos5250.dts
index 4dc2d4e74..510b269a3 100644
--- a/src/plat/exynos5/overlay-exynos5250.dts
+++ b/src/plat/exynos5/overlay-exynos5250.dts
@@ -14,6 +14,11 @@
 	/* Pick serial console */
 	chosen {
 		stdout-path = "serial2:115200n8";
+		seL4,kernel-devices =
+		    "serial2",
+		    &{/soc/interrupt-controller@10481000},
+		    &{/soc/mct@101c0000},
+		    &{/soc/timer};
 	};
 
 	/* HACK: 0xe0000000..0xff000000 is the largest contiguous region
diff --git a/src/plat/exynos5/overlay-exynos5410.dts b/src/plat/exynos5/overlay-exynos5410.dts
index c213f80a5..d673defd5 100644
--- a/src/plat/exynos5/overlay-exynos5410.dts
+++ b/src/plat/exynos5/overlay-exynos5410.dts
@@ -14,6 +14,11 @@
 	/* pick the right boot CPU */
 	chosen {
 		seL4,boot-cpu = <&{/cpus/cpu@0}>;
+		seL4,kernel-devices =
+		    "serial2",
+		    &{/soc/interrupt-controller@10481000},
+		    &{/soc/mct@101c0000},
+		    &{/timer};
 	};
 	/* The architecture timer on exynos5 depends on the MCT, but it is there. */
 	timer {
diff --git a/src/plat/exynos5/overlay-exynos5422.dts b/src/plat/exynos5/overlay-exynos5422.dts
index 04aca04d3..46999dee2 100644
--- a/src/plat/exynos5/overlay-exynos5422.dts
+++ b/src/plat/exynos5/overlay-exynos5422.dts
@@ -20,6 +20,11 @@
 	 */
 	chosen {
 		seL4,boot-cpu = <&{/cpus/cpu@100}>;
+		seL4,kernel-devices =
+		    "serial2",
+		    &{/soc/interrupt-controller@10481000},
+		    &{/soc/mct@101c0000},
+		    &{/timer};
 	};
 
 	/* The architecture timer on exynos5 depends on the MCT, but it is there. */
diff --git a/src/plat/fvp/config.cmake b/src/plat/fvp/config.cmake
index 321576fee..add8d9681 100644
--- a/src/plat/fvp/config.cmake
+++ b/src/plat/fvp/config.cmake
@@ -20,6 +20,7 @@ if(KernelPlatformFVP)
     set(KernelArchArmV8a ON)
     config_set(KernelARMPlatform PLAT "fvp")
     list(APPEND KernelDTSList "tools/dts/fvp.dts")
+    list(APPEND KernelDTSList "src/plat/fvp/overlay-fvp.dts")
     declare_default_headers(
         TIMER_FREQUENCY 100000000llu
         MAX_IRQ 207
diff --git a/src/plat/fvp/overlay-fvp.dts b/src/plat/fvp/overlay-fvp.dts
new file mode 100644
index 000000000..61fbc2619
--- /dev/null
+++ b/src/plat/fvp/overlay-fvp.dts
@@ -0,0 +1,20 @@
+/*
+ * 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)
+ */
+
+/ {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@2f000000},
+		    &{/timer};
+	};
+};
diff --git a/src/plat/hifive/config.cmake b/src/plat/hifive/config.cmake
index d77a0ee76..f32da1a73 100644
--- a/src/plat/hifive/config.cmake
+++ b/src/plat/hifive/config.cmake
@@ -21,6 +21,7 @@ if(KernelPlatformHifive)
     config_set(KernelRiscVPlatform RISCV_PLAT "hifive")
     config_set(KernelPlatformFirstHartID FIRST_HART_ID 1)
     list(APPEND KernelDTSList "tools/dts/hifive.dts")
+    list(APPEND KernelDTSList "src/plat/hifive/overlay-hifive.dts")
     declare_default_headers(
         TIMER_FREQUENCY 10000000llu PLIC_MAX_NUM_INT 53
         INTERRUPT_CONTROLLER drivers/irq/hifive.h
diff --git a/src/plat/hifive/overlay-hifive.dts b/src/plat/hifive/overlay-hifive.dts
new file mode 100644
index 000000000..13d425a5a
--- /dev/null
+++ b/src/plat/hifive/overlay-hifive.dts
@@ -0,0 +1,18 @@
+/*
+ * 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)
+ */
+
+/ {
+	chosen {
+		seL4,kernel-devices =
+		    &{/soc/interrupt-controller@c000000};
+	};
+};
diff --git a/src/plat/hikey/overlay-hikey.dts b/src/plat/hikey/overlay-hikey.dts
index d00edf702..89b41726e 100644
--- a/src/plat/hikey/overlay-hikey.dts
+++ b/src/plat/hikey/overlay-hikey.dts
@@ -13,6 +13,10 @@
 / {
 	chosen {
 		stdout-path = "serial0:115200n8";
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@f6801000},
+		    &{/timer};
 	};
 
 	pmu {
diff --git a/src/plat/imx31/overlay-kzm.dts b/src/plat/imx31/overlay-kzm.dts
index 3f925b7e6..96d37bf7e 100644
--- a/src/plat/imx31/overlay-kzm.dts
+++ b/src/plat/imx31/overlay-kzm.dts
@@ -14,6 +14,11 @@
 	/* Pick serial console */
 	chosen {
 		stdout-path = "serial0";
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@68000000},
+		    &{/l2cc@30000000},
+		    &{/soc/aips@53f00000/timer@53f94000};
 	};
 
 	/* Upstream bug: the memory node doesn't have a device_type,
diff --git a/src/plat/imx6/overlay-sabre.dts b/src/plat/imx6/overlay-sabre.dts
index cfd2e11ee..5e4d63eea 100644
--- a/src/plat/imx6/overlay-sabre.dts
+++ b/src/plat/imx6/overlay-sabre.dts
@@ -11,6 +11,13 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial1",
+		    &{/soc/interrupt-controller@a01000},
+		    &{/soc/l2-cache@a02000},
+		    &{/soc/timer@a00600};
+	};
 	/* Upstream bug: the memory node doesn't have a device_type,
 	 * but there is an empty memory node with a device_type. */
 	/delete-node/ memory;
diff --git a/src/plat/imx6/overlay-wandq.dts b/src/plat/imx6/overlay-wandq.dts
index 854afe354..6952a9243 100644
--- a/src/plat/imx6/overlay-wandq.dts
+++ b/src/plat/imx6/overlay-wandq.dts
@@ -11,6 +11,13 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/soc/interrupt-controller@a01000},
+		    &{/soc/l2-cache@a02000},
+		    &{/soc/timer@a00600};
+	};
 	/* Upstream bug: the memory node doesn't have a device_type,
 	 * but there is an empty memory node with a device_type. */
 	/delete-node/ memory;
diff --git a/src/plat/imx7/overlay-imx7sabre.dts b/src/plat/imx7/overlay-imx7sabre.dts
index 339e7f220..c910b0d04 100644
--- a/src/plat/imx7/overlay-imx7sabre.dts
+++ b/src/plat/imx7/overlay-imx7sabre.dts
@@ -11,6 +11,12 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/soc/interrupt-controller@31001000},
+		    &{/timer};
+	};
 	/* Upstream bug: the memory node doesn't have a device_type,
 	 * but there is an empty memory node with a device_type. */
 	/delete-node/ memory;
diff --git a/src/plat/imx8m-evk/overlay-imx8mm-evk.dts b/src/plat/imx8m-evk/overlay-imx8mm-evk.dts
index 9d527cf81..abc2596fa 100644
--- a/src/plat/imx8m-evk/overlay-imx8mm-evk.dts
+++ b/src/plat/imx8m-evk/overlay-imx8mm-evk.dts
@@ -11,6 +11,12 @@
  */
 
 / {
+    chosen {
+        seL4,kernel-devices =
+            "serial1",
+            &{/interrupt-controller@38800000},
+            &{/timer};
+    };
 
     /* These devices exists in the SOC documentation, but not in the DTS from Linux */
     gpt@302d0000 {
diff --git a/src/plat/imx8m-evk/overlay-imx8mq-evk.dts b/src/plat/imx8m-evk/overlay-imx8mq-evk.dts
index 342046e99..0ef1fe5ff 100644
--- a/src/plat/imx8m-evk/overlay-imx8mq-evk.dts
+++ b/src/plat/imx8m-evk/overlay-imx8mq-evk.dts
@@ -11,6 +11,12 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+			"serial0",
+			&{/interrupt-controller@38800000},
+			&{/timer};
+	};
 
 	/* This device exists in the SOC documentation, but not in the DTS from Linux */
 	gpt@302e0000 {
@@ -22,4 +28,4 @@
 		status = "disabled";
 	};
 
-};
\ No newline at end of file
+};
diff --git a/src/plat/odroidc2/config.cmake b/src/plat/odroidc2/config.cmake
index 39cef8254..4362903ef 100644
--- a/src/plat/odroidc2/config.cmake
+++ b/src/plat/odroidc2/config.cmake
@@ -21,6 +21,7 @@ if(KernelPlatformOdroidc2)
     config_set(KernelARMPlatform ARM_PLAT odroidc2)
     set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
     list(APPEND KernelDTSList "tools/dts/odroidc2.dts")
+    list(APPEND KernelDTSList "src/plat/odroidc2/overlay-odroidc2.dts")
     declare_default_headers(
         TIMER_FREQUENCY 24000000llu
         MAX_IRQ 250
diff --git a/src/plat/odroidc2/overlay-odroidc2.dts b/src/plat/odroidc2/overlay-odroidc2.dts
new file mode 100644
index 000000000..d00b10763
--- /dev/null
+++ b/src/plat/odroidc2/overlay-odroidc2.dts
@@ -0,0 +1,20 @@
+/*
+ * 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)
+ */
+
+/ {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/soc/interrupt-controller@c4301000},
+		    &{/timer};
+	};
+};
diff --git a/src/plat/omap3/overlay-omap3.dts b/src/plat/omap3/overlay-omap3.dts
index b4946349a..d80883782 100644
--- a/src/plat/omap3/overlay-omap3.dts
+++ b/src/plat/omap3/overlay-omap3.dts
@@ -12,7 +12,10 @@
 
 / {
 	chosen {
-		seL4,timer = <&{/ocp@68000000/timer@49040000}>;
 		stdout-path = "serial2";
+		seL4,kernel-devices =
+		    "serial2",
+		    &{/ocp@68000000/interrupt-controller@48200000},
+		    &{/ocp@68000000/timer@49040000};
 	};
 };
diff --git a/src/plat/spike/config.cmake b/src/plat/spike/config.cmake
index bedf95a69..fb202d734 100644
--- a/src/plat/spike/config.cmake
+++ b/src/plat/spike/config.cmake
@@ -35,6 +35,7 @@ if(KernelPlatformSpike)
     else()
         list(APPEND KernelDTSList "tools/dts/spike.dts")
     endif()
+    list(APPEND KernelDTSList "src/plat/spike/overlay-spike.dts")
     declare_default_headers(
         TIMER_FREQUENCY 10000000llu PLIC_MAX_NUM_INT 0
         INTERRUPT_CONTROLLER arch/machine/plic.h
diff --git a/src/plat/spike/overlay-spike.dts b/src/plat/spike/overlay-spike.dts
new file mode 100644
index 000000000..4eb63e2be
--- /dev/null
+++ b/src/plat/spike/overlay-spike.dts
@@ -0,0 +1,17 @@
+/*
+ * 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)
+ */
+
+/ {
+	chosen {
+		seL4,kernel-devices;
+	};
+};
diff --git a/src/plat/tk1/overlay-tk1.dts b/src/plat/tk1/overlay-tk1.dts
index 9d75c10fe..d15579796 100644
--- a/src/plat/tk1/overlay-tk1.dts
+++ b/src/plat/tk1/overlay-tk1.dts
@@ -11,6 +11,13 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@50041000},
+		    &{/timer};
+	};
+
 	memory@80000000 {
 		/* 1MiB carveout at 0xa7f00000 for the elfloader's monitor mode hooks */
 		reg = <0x0 0x80000000 0x0 0x27f00000>;
diff --git a/src/plat/tx1/overlay-tx1.dts b/src/plat/tx1/overlay-tx1.dts
index e16759098..733aec786 100644
--- a/src/plat/tx1/overlay-tx1.dts
+++ b/src/plat/tx1/overlay-tx1.dts
@@ -11,6 +11,13 @@
  */
 
 / {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@50041000},
+		    &{/timer};
+	};
+
 	pmu {
 		compatible = "arm,armv8-pmuv3";
 		interrupts = <0x00 0x90 0x04>,
diff --git a/src/plat/tx2/overlay-tx2.dts b/src/plat/tx2/overlay-tx2.dts
index 37145a49a..8d2ca5286 100644
--- a/src/plat/tx2/overlay-tx2.dts
+++ b/src/plat/tx2/overlay-tx2.dts
@@ -14,6 +14,10 @@
 	/* seL4 on the TX2 boots on the first non-NVIDIA core */
 	chosen {
 		seL4,boot-cpu = <&{/cpus/cpu@2}>;
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/interrupt-controller@3881000},
+		    &{/timer};
 	};
 
 
diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake
index d16a4e4f6..f1bd33d81 100644
--- a/src/plat/zynq7000/config.cmake
+++ b/src/plat/zynq7000/config.cmake
@@ -21,6 +21,7 @@ if(KernelPlatformZynq7000)
     config_set(KernelARMPlatform ARM_PLAT zynq7000)
     config_set(KernelArmMach MACH "zynq")
     list(APPEND KernelDTSList "tools/dts/zynq7000.dts")
+    list(APPEND KernelDTSList "src/plat/zynq7000/overlay-zynq7000.dts")
     declare_default_headers(
         TIMER_FREQUENCY 400000000llu
         MAX_IRQ 92
diff --git a/src/plat/zynq7000/overlay-zynq7000.dts b/src/plat/zynq7000/overlay-zynq7000.dts
new file mode 100644
index 000000000..7eae7b894
--- /dev/null
+++ b/src/plat/zynq7000/overlay-zynq7000.dts
@@ -0,0 +1,21 @@
+/*
+ * 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)
+ */
+
+/ {
+	chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/amba/interrupt-controller@f8f01000},
+		    &{/amba/cache-controller@f8f02000},
+		    &{/amba/timer@f8f00600};
+	};
+};
diff --git a/src/plat/zynqmp/config.cmake b/src/plat/zynqmp/config.cmake
index 571e1c0ff..398d4a960 100644
--- a/src/plat/zynqmp/config.cmake
+++ b/src/plat/zynqmp/config.cmake
@@ -41,6 +41,7 @@ if(KernelPlatformZynqmp)
     if(NOT KernelPlatformUltra96)
         list(APPEND KernelDTSList "tools/dts/zynqmp.dts")
     endif()
+    list(APPEND KernelDTSList "src/plat/zynqmp/overlay-zynqmp.dts")
 
     declare_default_headers(
         TIMER_FREQUENCY 100000000llu
diff --git a/src/plat/zynqmp/overlay-zynqmp.dts b/src/plat/zynqmp/overlay-zynqmp.dts
new file mode 100644
index 000000000..00b276df2
--- /dev/null
+++ b/src/plat/zynqmp/overlay-zynqmp.dts
@@ -0,0 +1,20 @@
+/*
+ * 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)
+ */
+
+/ {
+    chosen {
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/amba_apu@0/interrupt-controller@f9010000},
+		    &{/timer};
+    };
+};
diff --git a/tools/hardware.yml b/tools/hardware.yml
index 59081fe3b..200be1f10 100644
--- a/tools/hardware.yml
+++ b/tools/hardware.yml
@@ -196,7 +196,6 @@ devices:
         kernel: TIMER_PPTR
     interrupts:
       KERNEL_TIMER_IRQ: 0
-    chosen: seL4,timer
   # TI prcm (arm/omap/prcm.txt)
   - compatible:
     - ti,am3-prcm
@@ -227,7 +226,6 @@ devices:
     - snps,dw-apb-uart
     - ti,omap3-uart
     - xlnx,xuartps
-    chosen: stdout-path
     regions:
       - executeNever: true
         index: 0
diff --git a/tools/hardware_gen.py b/tools/hardware_gen.py
index c040a3017..921fc4483 100644
--- a/tools/hardware_gen.py
+++ b/tools/hardware_gen.py
@@ -548,30 +548,6 @@ class Config:
 
         return self.aliases[name].strings[0]
 
-    def _is_chosen(self, device, rule, by_phandle):
-        if 'chosen' not in rule:
-            return True
-        if self.chosen is None:
-            return False
-
-        prop = rule['chosen']
-        if prop not in self.chosen:
-            return False
-
-        val = self.chosen[prop]
-        # a "chosen" field will either have a phandle, or
-        # a path or an alias, then a ":", then other data.
-        # the path/alias may not contain a ":".
-        if isinstance(val, pyfdt.pyfdt.FdtPropertyWords):
-            return 'phandle' in device and device['phandle'].words[0] == val.words[0]
-        val = val.strings[0].split(':')[0]
-
-        # path starts with '/'.
-        if val[0] == '/':
-            return device.name == val
-        else:
-            return device.name == self._lookup_alias(val)
-
     def split_regions(self, device, by_phandle):
         """
         @brief      Wraps Device.regions() and splits into user, kernel groups
@@ -597,8 +573,6 @@ class Config:
             default_user = True
             for rule in self.devices[compatible]:
                 regs = []
-                if not self._is_chosen(device, rule, by_phandle):
-                    continue
                 if 'regions' in rule:
                     for reg_rule in rule['regions']:
                         if 'index' not in reg_rule:
@@ -638,10 +612,8 @@ class Config:
                 continue
 
             for rule in self.devices[compatible]:
-                if self._is_chosen(device, rule, by_phandle):
-                    self.matched_devices.add(compatible)
 
-                if 'interrupts' not in rule or not self._is_chosen(device, rule, by_phandle):
+                if 'interrupts' not in rule:
                     continue
 
                 irqs = device.get_interrupts(by_phandle)
@@ -688,8 +660,43 @@ class Config:
                 break
         return ret
 
-    def get_matched_devices(self):
-        return sorted(self.matched_devices)
+    def get_chosen_devices(self, devices):
+        """
+        @brief      Returns a list of device nodes that were specified by `seL4,kernel-devices`
+
+        @param      self     The Config object
+        @param      devices  All of the devices in the device tree
+
+        @return     The chosen devices matched from `seL4,kernel-devices`.
+        """
+        seL4_device_paths = self.chosen['seL4,kernel-devices']
+        kernel_chosen_devices = []
+        if not isinstance(seL4_device_paths, pyfdt.pyfdt.FdtPropertyStrings):
+            # seL4_device_paths is an empty property
+            return []
+
+        for device_path in seL4_device_paths:
+            val = device_path.split(':')[0]
+            # path starts with '/'.
+            if val[0] == '/':
+                device_path = val
+            else:
+                device_path = self._lookup_alias(val)
+
+            assert device_path in devices, "get_chosen_devices: %s is not a valid device path" % device_path
+            device = devices[device_path]
+            compat = device['compatible']
+            for compatible in compat.strings:
+                if compatible not in self.devices:
+                    continue
+                self.matched_devices.add(compatible)
+                break
+            else:
+                assert False, "The kernel isn't aware of this device type: %s" % "\\0".join(
+                    device['compatible'])
+
+            kernel_chosen_devices.append(device)
+        return kernel_chosen_devices
 
 
 @memoize()
@@ -1025,40 +1032,31 @@ def main(args):
     fdt = pyfdt.pyfdt.FdtBlobParse(args.dtb).to_fdt()
     devices, by_phandle = find_devices(fdt, cfg)
 
+    # Handle kernel devices
+    kernel_chosen_devices = cfg.get_chosen_devices(devices)
+    kernel_irqs = []
+    for device in kernel_chosen_devices:
+        kernel_irqs.extend(cfg.get_irqs(device, by_phandle))
+        _, kernel_mappings = cfg.split_regions(device, by_phandle)
+        kernel.update(kernel_mappings)
+    kernel = fixup_device_regions(kernel, 1 << args.page_bits)
+
+
     rsvmem = []
     if '/reserved-memory' in devices:
         rsvmem = parse_reserved_memory(devices['/reserved-memory'].node, devices, cfg, by_phandle)
     rsvmem += fdt.reserve_entries
-    kernel_irqs = set()
     for d in devices.values():
-        kernel_irqs.update(cfg.get_irqs(d, by_phandle))
         if d.is_memory():
             for e in d.regions():
                 memory.update(e.remove_subregions(rsvmem))
+        elif d in kernel_chosen_devices:
+            user_mappings, _ = cfg.split_regions(d, by_phandle)
+            user.update(user_mappings)
         else:
-            (u, k) = cfg.split_regions(d, by_phandle)
-            user.update(u)
-            kernel.update(k)
-
-    irq_dict = {}
-    for el in kernel_irqs:
-        if el.name in irq_dict:
-            irq_dict[el.name].append(el)
-        else:
-            irq_dict[el.name] = [el]
-
-    kernel_irqs = []
-    for el in irq_dict:
-
-        irq_dict[el].sort(key=lambda a: a.priority, reverse=True)
-        max_prio = irq_dict[el][0].priority
-        for irq in irq_dict[el]:
-            if irq.priority != max_prio:
-                break
-            kernel_irqs.append(irq)
+            user.update(set(d.regions()))
 
     user = fixup_device_regions(user, 1 << args.page_bits, merge=True)
-    kernel = fixup_device_regions(kernel, 1 << args.page_bits)
     output_regions(args, user, memory, kernel, kernel_irqs, args.output)
 
     # generate cmake
diff --git a/tools/hardware_schema.yml b/tools/hardware_schema.yml
index a3f567a33..66900cf9f 100644
--- a/tools/hardware_schema.yml
+++ b/tools/hardware_schema.yml
@@ -45,34 +45,6 @@ definitions:
         patternProperties:
           '^[A-Za-z_][A-Za-z0-9_]*$':
             $ref: '#/definitions/interrupt'
-      chosen:
-        description: >
-          Apply this rule only to the device referenced by the correspondingly named
-          property in the chosen node. For instance, a dts like this
-
-          aliases {
-            serial0 = &serial_0;
-          };
-
-          chosen {
-            stdout-path = "serial0";
-          };
-
-          serial_0: serial@13800000 {
-            compatible = "samsung,exynos4210-uart";
-            reg = <0x13800000 0x100>;
-            /* etc */
-          };
-
-          serial_1: serial@13810000 {
-            compatible = "samsung,exynos4210-uart";
-            reg = <0x13810000 0x100>;
-            /* etc */
-          };
-
-          and a device with the property chosen set to stdout-path will only match the serial@13800000
-          device and not any other device with the samsung,exynos4210-uart compatible.
-        type: string
     required: [compatible]
   region:
     type: object
-- 
GitLab