diff --git a/src/plat/allwinnerA20/overlay-allwinnerA20.dts b/src/plat/allwinnerA20/overlay-allwinnerA20.dts
index dd2921578d02c1f190662128bab82db344fa2e41..a6a58e4d6f8c2bfe6691097ba5eff5d83b8272ce 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 8c70dc73c53a568db870e304b75946b6084d24c1..33196ce6a25c3b05792160a639b64ec31a7233c4 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 8798516622ef61abdfe631a5b41c9a69e3d22856..49b0d1088251ad9c6d9c8e96e8251d37cd4809f6 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 39ee72cfa54e88516c95ec9f76d6e1b871b98413..e3219d30250a68cae3ab99301afbd325c9df9737 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 d97d27f14ecedfa94182f7ffce3ff76b53a8cbc4..ece5d960e42d80adc5966c195461aef542792ee5 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 4dc2d4e74283afe9d5c7331145133fe3d03d77c5..510b269a3ce189185bd218d83173a80b2624ca34 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 c213f80a592104e45b0dc2fd1145304ce37c7432..d673defd5a5c58bf24a10fb3f37a105593d169c3 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 04aca04d37e0cb1c4cf33c6bd91126202e3dcfae..46999dee22e760fd3e7c2b76281488c95a8c2c81 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 321576fee7ac40c9a62737673afa8bd6c4cf8a2a..add8d96815b30bcab691859687e1eedace0656b8 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 0000000000000000000000000000000000000000..61fbc2619c3554f557a4b8ebcf7b734f06f0d9e3
--- /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 d77a0ee76a0777bed8b20e97dc02cd2c5d2fe224..f32da1a73ba25796918decc8d559d877ee91eb77 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 0000000000000000000000000000000000000000..13d425a5a9dc2e135007290b86bd3ea286ed142c
--- /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 d00edf702569586873bfe9879741af625513055e..89b41726e8217b61bb91e5d252f66a4d09c9b102 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 3f925b7e62417b19804d6ea0f52d7e11784e88d4..96d37bf7e4451a14223f4d3be04665bf67989975 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 cfd2e11ee3b0ae3a02d42fb197fa871bfe3a7a09..5e4d63eead7949e3a810b16b6d61c01be0333103 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 854afe354df9f6d6f35730ca7a54eaa27b04aa5c..6952a92438b4f0ad6855893c8bf01fd3744be4df 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 339e7f22093f7e69e111965967c29704f5a0e8fd..c910b0d0493514f4aac84c3036b33ce77e625685 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 9d527cf81fc3b745c62e1a522f108ba7d5e29fc5..abc2596fa167885baf525937a75b79e15a87ce43 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 342046e99779f7e050ef02c8f567a83114b05293..0ef1fe5ff27782441d7dc70d65dea48871ced38f 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 39cef825493dca784d77d43698d0bca02d937238..4362903efd329c46c47eaabeb8ba1b9b93cbf333 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 0000000000000000000000000000000000000000..d00b10763c23a9a8378aad784fef247ff2971360
--- /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 b4946349a53c565e2f8f360d1678ecad6549205e..d80883782115d8c3da618aa788b83fdac7391aeb 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 bedf95a692aeb2dafda138966dd46c6231a732d4..fb202d734698bbed4bc9fb035c32f59c66b16f82 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 0000000000000000000000000000000000000000..4eb63e2bef11b21e73f73867ddf53b1056ac91e5
--- /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 9d75c10fec7078c277288dff1a82362ce77ebfa5..d15579796e044b966a5cb9ae907d3a53ef48dc91 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 e167590980a95ca9a16b2bcc71eda11694b58273..733aec786582a0cd483d292c5f631665fa5fb6e1 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 37145a49ac4775735d02e565f3ecaf9c446ab3d1..8d2ca52869d5ac43a68a1159ca8e3dbcc8edc54e 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 d16a4e4f62a46bbbe16bff5231ea97194a8ea05f..f1bd33d8122720aad310ad997117ac1f14634395 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 0000000000000000000000000000000000000000..7eae7b89439caa6930222973b0f1181552790660
--- /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 571e1c0ffbda01bfb87e748009ff6eb132285a04..398d4a96080782db5573b97e83cbbb17b2e5c220 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 0000000000000000000000000000000000000000..00b276df20730d5879bf77703c95541ddc686c2b
--- /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 59081fe3b50eddde58b243ed98c2600b690a4d42..200be1f10ce957185e53e724352bbf271c5b812d 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 c040a3017b45956b892acf138992aed9085bf3ea..921fc448339a7d842a73014cb0ecc34e17364e43 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 a3f567a33b62e09917014bd11d73cf7584a6d180..66900cf9f6b1a2964d9e95347406999f7f273d7b 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