From 0fac956e9f5fc336959aba0cb470f71a9a1226c5 Mon Sep 17 00:00:00 2001
From: Simon Shields <simon.shields@data61.csiro.au>
Date: Tue, 29 Jan 2019 14:53:29 +1100
Subject: [PATCH] ARM platforms: use auto-generated kernel_devices

Note that the auto-generated kernel_devices will differ slightly from
the ones present in the kernel until now. When devices have
registers that aren't page-aligned we now always set the appropriate
PPTR to be the start address of the device, while previously the PPTR
was sometimes page-aligned.

Specifically, this change to PPTRs affects:
- bcm2837 intc
- bcm2837 uart
- allwinnerA20 timer
---
 include/arch/arm/arch/64/mode/hardware.h      |   1 -
 .../plat/allwinnerA20/plat/machine/devices.h  |  48 ---
 .../plat/allwinnerA20/plat/machine/hardware.h |  24 --
 include/plat/am335x/plat/machine/devices.h    |  39 ---
 include/plat/am335x/plat/machine/hardware.h   |  36 ---
 include/plat/apq8064/plat/machine/devices.h   | 245 ---------------
 include/plat/apq8064/plat/machine/hardware.h  |  29 --
 .../plat/32/plat_mode/machine/devices.h       |  22 --
 .../plat/64/plat_mode/machine/devices.h       |  22 --
 include/plat/bcm2837/plat/machine.h           |   3 +-
 include/plat/bcm2837/plat/machine/devices.h   |  38 ---
 include/plat/bcm2837/plat/machine/hardware.h  |  26 --
 include/plat/exynos4/plat/machine/devices.h   | 188 ------------
 include/plat/exynos4/plat/machine/hardware.h  |  34 ---
 include/plat/exynos5/plat/machine/devices.h   | 280 ------------------
 include/plat/exynos5/plat/machine/hardware.h  |  35 ---
 .../hikey/plat/32/plat_mode/machine/devices.h |  22 --
 .../hikey/plat/64/plat_mode/machine/devices.h |  21 --
 include/plat/hikey/plat/machine/devices.h     |  48 ---
 include/plat/hikey/plat/machine/hardware.h    |  23 --
 include/plat/imx31/plat/machine/devices.h     |  15 -
 include/plat/imx31/plat/machine/hardware.h    |  31 --
 include/plat/imx6/plat/machine/devices.h      | 192 ------------
 include/plat/imx6/plat/machine/hardware.h     |  31 --
 include/plat/imx7/plat/machine/devices.h      | 185 ------------
 include/plat/imx7/plat/machine/hardware.h     |  31 --
 include/plat/omap3/plat/machine/devices.h     | 142 ---------
 include/plat/omap3/plat/machine/hardware.h    |  24 --
 include/plat/omap3/plat/machine/interrupt.h   |   1 -
 include/plat/tk1/plat/machine/devices.h       | 128 --------
 include/plat/tk1/plat/machine/hardware.h      |  38 ---
 include/plat/tx1/plat/machine/devices.h       | 117 --------
 include/plat/tx1/plat/machine/hardware.h      |  30 --
 include/plat/tx2/plat/machine/devices.h       |  66 -----
 include/plat/tx2/plat/machine/hardware.h      |  30 --
 include/plat/zynq7000/plat/machine/devices.h  |  92 ------
 include/plat/zynq7000/plat/machine/hardware.h |  30 --
 include/plat/zynqmp/plat/machine.h            |   1 -
 include/plat/zynqmp/plat/machine/devices.h    | 216 --------------
 include/plat/zynqmp/plat/machine/hardware.h   |  23 --
 src/plat/allwinnerA20/machine/hardware.c      |   5 +-
 src/plat/allwinnerA20/machine/io.c            |   2 +-
 src/plat/am335x/machine/hardware.c            |   4 +-
 src/plat/am335x/machine/io.c                  |   2 +-
 src/plat/apq8064/machine/hardware.c           |   1 -
 src/plat/apq8064/machine/io.c                 |   1 -
 src/plat/bcm2837/machine/io.c                 |  19 +-
 src/plat/exynos4/machine/hardware.c           |   1 -
 src/plat/exynos5/machine/hardware.c           |   2 +-
 src/plat/exynos_common/io.c                   |   1 -
 src/plat/hikey/machine/io.c                   |   2 +-
 src/plat/imx31/machine/hardware.c             |   1 +
 src/plat/imx31/machine/io.c                   |   2 +-
 src/plat/imx6/machine/io.c                    |   2 +-
 src/plat/imx7/machine/io.c                    |   2 +-
 src/plat/omap3/machine/hardware.c             |   4 +-
 src/plat/omap3/machine/io.c                   |   2 +-
 src/plat/tk1/machine/io.c                     |   2 +-
 src/plat/tx1/machine/io.c                     |   2 +-
 src/plat/tx2/machine/io.c                     |   2 +-
 src/plat/zynq7000/machine/io.c                |   2 +-
 src/plat/zynqmp/machine/io.c                  |   2 +-
 62 files changed, 29 insertions(+), 2641 deletions(-)
 delete mode 100644 include/plat/allwinnerA20/plat/machine/devices.h
 delete mode 100644 include/plat/am335x/plat/machine/devices.h
 delete mode 100644 include/plat/apq8064/plat/machine/devices.h
 delete mode 100644 include/plat/bcm2837/plat/32/plat_mode/machine/devices.h
 delete mode 100644 include/plat/bcm2837/plat/64/plat_mode/machine/devices.h
 delete mode 100644 include/plat/bcm2837/plat/machine/devices.h
 delete mode 100644 include/plat/exynos4/plat/machine/devices.h
 delete mode 100644 include/plat/exynos5/plat/machine/devices.h
 delete mode 100644 include/plat/hikey/plat/32/plat_mode/machine/devices.h
 delete mode 100644 include/plat/hikey/plat/64/plat_mode/machine/devices.h
 delete mode 100644 include/plat/hikey/plat/machine/devices.h
 delete mode 100644 include/plat/imx6/plat/machine/devices.h
 delete mode 100644 include/plat/imx7/plat/machine/devices.h
 delete mode 100644 include/plat/omap3/plat/machine/devices.h
 delete mode 100644 include/plat/tk1/plat/machine/devices.h
 delete mode 100644 include/plat/tx1/plat/machine/devices.h
 delete mode 100644 include/plat/tx2/plat/machine/devices.h
 delete mode 100644 include/plat/zynq7000/plat/machine/devices.h
 delete mode 100644 include/plat/zynqmp/plat/machine/devices.h

diff --git a/include/arch/arm/arch/64/mode/hardware.h b/include/arch/arm/arch/64/mode/hardware.h
index 590f8498b..9932bf9cb 100644
--- a/include/arch/arm/arch/64/mode/hardware.h
+++ b/include/arch/arm/arch/64/mode/hardware.h
@@ -15,7 +15,6 @@
 
 #include <config.h>
 #include <arch/machine/hardware.h>
-#include <plat/machine/hardware.h>
 #include <plat/api/constants.h>
 
 
diff --git a/include/plat/allwinnerA20/plat/machine/devices.h b/include/plat/allwinnerA20/plat/machine/devices.h
deleted file mode 100644
index 06d71f333..000000000
--- a/include/plat/allwinnerA20/plat/machine/devices.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*
- * Copyright 2015, DornerWorks, Ltd.
- *
- * 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(GD_GPL)
- */
-
-/*
- definitions for memory addresses of allwinner A20 platform
- listed in the order of ascending memory address, similar to the datasheet
- the size must all be powers of 2 and page aligned (4k or 1M).
-*/
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                  0xfff01000
-#define TIMER0_PPTR                 0xfff02000
-#define GIC_DISTRIBUTOR_PPTR        0xfff03000
-#define GIC_CONTROLLER_PPTR         0xfff04000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff05000
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       GIC_PADDR + 0x1000
-#define GIC_CONTROLLER0_PADDR       GIC_PADDR + 0x2000
-
-
-
-#define UART0_PADDR                 0x01C28000
-
-/* CCU, Interrupt, Timer, OWA */
-/* Timer = PPTR + 0xC00 */
-#define TIMER0_PADDR                0x01C20000
-
-#define GIC_PADDR                   0x01C80000
-
-/* TODO: Add other devices PADDRs */
-
-#define SPI0_PADDR  0x01C05000
-#define SPI1_PADDR  0x01C06000
-
-#endif
diff --git a/include/plat/allwinnerA20/plat/machine/hardware.h b/include/plat/allwinnerA20/plat/machine/hardware.h
index 7736ed2d1..012e323d9 100755
--- a/include/plat/allwinnerA20/plat/machine/hardware.h
+++ b/include/plat/allwinnerA20/plat/machine/hardware.h
@@ -15,32 +15,8 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    /*  GP Timer 11 */
-    {
-        TIMER0_PADDR,
-        TIMER0_PPTR,
-        true  /* armExecuteNever */
-    },
-    /*  GIC */
-    {
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART0_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/am335x/plat/machine/devices.h b/include/plat/am335x/plat/machine/devices.h
deleted file mode 100644
index 8767e429f..000000000
--- a/include/plat/am335x/plat/machine/devices.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the kernel. */
-#define INTC_PPTR                       0xfff01000
-#define UART_PPTR                      0xfff02000
-#define DMTIMER0_PPTR                   0xfff03000
-#define WDT1_PPTR                       0xfff04000
-#define CMPER_PPTR                      0xfff05000
-#define ARM_DEBUG_MMAPPING_PPTR         0xfff06000
-
-
-/* Other devices on the SoC. */
-#define INTC_PADDR      0x48200000
-#define UART0_PADDR     0x44E09000
-#define DMTIMER0_PADDR  0x44E05000
-#define DMTIMER2_PADDR  0x48040000
-#define DMTIMER3_PADDR  0x48042000
-#define DMTIMER4_PADDR  0x48044000
-#define DMTIMER5_PADDR  0x48046000
-#define DMTIMER6_PADDR  0x48048000
-#define DMTIMER7_PADDR  0x4804A000
-#define WDT1_PADDR      0x44e35000
-#define CMPER_PADDR     0x44e00000
-#define CTRL_PADDR      0x44E10000
-#define PRCM_PADDR      0x44E00000
-#define CPSW_PADDR      0x4A100000
-
-#endif
diff --git a/include/plat/am335x/plat/machine/hardware.h b/include/plat/am335x/plat/machine/hardware.h
index f215aeb75..f5f9e035a 100644
--- a/include/plat/am335x/plat/machine/hardware.h
+++ b/include/plat/am335x/plat/machine/hardware.h
@@ -14,43 +14,7 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <plat/machine/interrupt.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  DM Timer 0 */
-        DMTIMER0_PADDR,
-        DMTIMER0_PPTR,
-        true  /* armExecuteNever */
-    },
-    /*  INTC */
-    {
-        INTC_PADDR,
-        INTC_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  WDT1 */
-        WDT1_PADDR,
-        WDT1_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  CMPER */
-        CMPER_PADDR,
-        CMPER_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART0_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 #endif
diff --git a/include/plat/apq8064/plat/machine/devices.h b/include/plat/apq8064/plat/machine/devices.h
deleted file mode 100644
index c5731b6f2..000000000
--- a/include/plat/apq8064/plat/machine/devices.h
+++ /dev/null
@@ -1,245 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                   0xfff01000
-#define TIMER_PPTR                  0xfff02000
-#define GIC_DISTRIBUTOR_PPTR        0xfff04000
-#define GIC_CONTROLLER_PPTR         0xfff05000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff06000
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       APCS_QGIC2_PADDR + 0x0000
-#define GIC_CONTROLLER0_PADDR       APCS_QGIC2_PADDR + 0x2000
-
-#define UART_PADDR                  GSBI7_UART_DM_PADDR
-#define TIMER_PADDR                 APCS_TMR_PADDR
-
-/* Other devices on the SoC */
-#define RPM_PADDR                 0x00000000 /* RPM */
-#define RPM_TIMERS_PADDR          0x00062000 /* RPM */
-#define RPM_MSG_RAM_XPU_PADDR     0x00100000 /* RPM */
-#define MPM_PADDR                 0x00200000 /* RPM */
-#define PA1_SSBI2_CFG_PADDR       0x00300000 /* RPM */
-#define PA1_XPU_PADDR             0x00400000 /* RPM */
-#define PA1_SSBI2_CMD_PADDR       0x00500000 /* RPM */
-#define PA2_SSBI2_CFG_PADDR       0x00600000 /* RPM */
-#define SEC_CTRL_PADDR            0x00700000 /* Security */
-#define TLMM_PADDR                0x00800000 /* chip_core_top */
-#define CLK_CTL_PADDR             0x00900000 /* Clock_Controller */
-#define EBI1_CH0_PADDR            0x00A00000 /* LPDDR */
-#define SYS_IMEM_PADDR            0x00B00000 /* chip_core_top */
-#define PA2_SSBI2_CMD_PADDR       0x00C00000 /* RPM */
-#define EBI1_CH1_PADDR            0x00D00000 /* LPDDR */
-#define SFPB_WRAPPER_XPU_PADDR    0x00E00000 /* SFPB_Wrapper */
-#define SFPB_WRAPPER_PADDR        0x00F00000 /* SFPB_Wrapper */
-#define SPDM_PADDR                0x01000000 /* chip_core_top */
-#define SPDM_SECURE_PADDR         0x01100000 /* chip_core_top */
-#define SFPB_WRAPPER_MUTEX_PADDR  0x01200000 /* SFPB_Wrapper */
-#define SFAB_PADDR                0x01300000 /* Fabrics */
-#define AFAB_PADDR                0x01400000 /* Fabrics */
-#define DAY_CFG_PADDR             0x01500000 /* Fabrics */
-#define SFPB_WRAPPER_1x2_PADDR    0x01600000 /* SFPB_Wrapper */
-#define SFPB_WRAPPER_2x1_PADDR    0x01800000 /* SFPB_Wrapper */
-#define QDSS_DAPROM_PADDR         0x01A00000 /* Debug_Sub_System */
-#define QDSS_ETB_PADDR            0x01A01000 /* Debug_Sub_System */
-#define QDSS_CTI1_PADDR           0x01A02000 /* Debug_Sub_System */
-#define QDSS_TPIU_PADDR           0x01A03000 /* Debug_Sub_System */
-#define QDSS_TFUNNEL_PADDR        0x01A04000 /* Debug_Sub_System */
-#define QDSS_ITM_PADDR            0x01A05000 /* Debug_Sub_System */
-#define QDSS_STM_PADDR            0x01A06000 /* Debug_Sub_System */
-#define QDSS_DAPM2VMT_PADDR       0x01A80000 /* Debug_Sub_System */
-#define APCS_QGIC2_PADDR          0x02000000 /* KraitMP_Sub_System */
-#define APCS_ACC_PADDR            0x02008000 /* KraitMP_Sub_System */
-#define APCS_SAW2_PADDR           0x02009000 /* KraitMP_Sub_System */
-#define APCS_TMR_PADDR            0x0200A000 /* KraitMP_Sub_System */
-#define PCS_GLB_PADDR             0x02010000 /* KraitMP_Sub_System */
-#define APCS_GCC_PADDR            0x02011000 /* KraitMP_Sub_System */
-#define APCS_L2_GDHS_PADDR        0x02012000 /* KraitMP_Sub_System */
-#define APCS_L2_MPU_PADDR         0x02013000 /* KraitMP_Sub_System */
-#define CPU0_APCS_ACC_PADDR       0x02088000 /* KraitMP_Sub_System */
-#define CPU0_APCS_SAW2_PADDR      0x02089000 /* KraitMP_Sub_System */
-#define CPU0_APCS_TMR_PADDR       0x0208A000 /* KraitMP_Sub_System */
-#define EXT_APCS_GLB_PADDR        0x02090000 /* KraitMP_Sub_System */
-#define EXT_APCS_GCC_PADDR        0x02091000 /* KraitMP_Sub_System */
-#define EXT_APCS_L2_GDHS_PADDR    0x02092000 /* KraitMP_Sub_System */
-#define EXT_APCS_L2_MPU_PADDR     0x02093000 /* KraitMP_Sub_System */
-#define CPU1_APCS_ACC_PADDR       0x02098000 /* KraitMP_Sub_System */
-#define CPU1_APCS_SAW2_PADDR      0x02099000 /* KraitMP_Sub_System */
-#define CPU1_APCS_TMR_PADDR       0x0209A000 /* KraitMP_Sub_System */
-#define CPU2_APCS_ACC_PADDR       0x020A8000 /* KraitMP_Sub_System */
-#define CPU2_APCS_SAW2_PADDR      0x020A9000 /* KraitMP_Sub_System */
-#define CPU2_APCS_TMR_PADDR       0x020AA000 /* KraitMP_Sub_System */
-#define CPU3_APCS_ACC_PADDR       0x020B8000 /* KraitMP_Sub_System */
-#define CPU3_APCS_SAW2_PADDR      0x020B9000 /* KraitMP_Sub_System */
-#define CPU3_APCS_TMR_PADDR       0x020BA000 /* KraitMP_Sub_System */
-#define APCS_HSEL_PADDR           0x02100000 /* KraitMP_Sub_System */
-#define RIVA_PADDR                0x03000000 /* RIVA */
-#define MMSS_CC_PADDR             0x04000000 /* Multi_Media_Sub_System */
-#define OXILI_PADDR               0x04300000 /* Multi_Media_Sub_System */
-#define MFC_PADDR                 0x04400000 /* Multi_Media_Sub_System */
-#define VFE_PADDR                 0x04500000 /* Multi_Media_Sub_System */
-#define GEMINI_PADDR              0x04600000 /* Multi_Media_Sub_System */
-#define MIPI_DSI_1_PADDR          0x04700000 /* Multi_Media_Sub_System */
-#define CSID_PADDR                0x04800000 /* Multi_Media_Sub_System */
-#define HDMI_TX_PADDR             0x04A00000 /* Multi_Media_Sub_System */
-#define IMEM_MMSS_PADDR           0x04B00000 /* Multi_Media_Sub_System */
-#define ROTATOR_PADDR             0x04E00000 /* Multi_Media_Sub_System */
-#define TV_ENC_PADDR              0x04F00000 /* Multi_Media_Sub_System */
-#define JPEGD_PADDR               0x05000000 /* Multi_Media_Sub_System */
-#define MDP_PADDR                 0x05100000 /* Multi_Media_Sub_System */
-#define FABRIC_MMSS_PADDR         0x05200000 /* Fabrics */
-#define VPE_PADDR                 0x05300000 /* Multi_Media_Sub_System */
-#define MSS_APU_PADDR             0x05400000 /* Multi_Media_Sub_System */
-#define MMSS_SFPB_CFG_PADDR       0x05700000 /* Multi_Media_Sub_System */
-#define MIPI_DSI_2_PADDR          0x05800000 /* Multi_Media_Sub_System */
-#define VCAP_PADDR                0x05900000 /* Multi_Media_Sub_System */
-#define SMMU_VCAP_PADDR           0x07200000 /* Multi_Media_Sub_System */
-#define SMMU_JPEGD_PADDR          0x07300000 /* Multi_Media_Sub_System */
-#define SMMU_VPE_PADDR            0x07400000 /* Multi_Media_Sub_System */
-#define SMMU_MDP4_0_PADDR         0x07500000 /* Multi_Media_Sub_System */
-#define SMMU_MDP4_1_PADDR         0x07600000 /* Multi_Media_Sub_System */
-#define SMMU_ROTATOR_PADDR        0x07700000 /* Multi_Media_Sub_System */
-#define SMMU_JPEG_PADDR           0x07800000 /* Multi_Media_Sub_System */
-#define SMMU_VFE_PADDR            0x07900000 /* Multi_Media_Sub_System */
-#define SMMU_SS1080P_0_PADDR      0x07A00000 /* Multi_Media_Sub_System */
-#define SMMU_SS1080P_1_PADDR      0x07B00000 /* Multi_Media_Sub_System */
-#define SMMU_GFX3D_PADDR          0x07C00000 /* Multi_Media_Sub_System */
-#define SMMU_GFX3D1_PADDR         0x07D00000 /* Multi_Media_Sub_System */
-#define SMMU_SFPB_CFG_DUMMY_PADDR 0x07F00000 /* Multi_Media_Sub_System */
-#define GSS_A5_CSR_PADDR          0x10000000 /* GSS */
-#define GSS_A5_SPM_PADDR          0x10001000 /* GSS */
-#define GSS_A5_TIMERS_PADDR       0x10002000 /* GSS */
-#define GSS_A5_SSBI_PADDR         0x10003000 /* GSS */
-#define GSS_A5_QGIC2_PADDR        0x10008000 /* GSS */
-#define NAV_PADDR                 0x10100000 /* GSS */
-#define CE3_CRYPTO4_PADDR         0x11000000 /* Security */
-#define PPSS_PADDR                0x12080000 /* Daytona_SPS */
-#define PPSS_SLP_TIMERS_PADDR     0x12081000 /* Daytona_SPS */
-#define SIC_PADDR                 0x120C0000 /* Daytona_SPS */
-#define SIC_APU_PADDR             0x120C2000 /* Daytona_SPS */
-#define SIC_NON_SECURE_PADDR      0x12100000 /* Daytona_SPS */
-#define INTCTL0_PADDR             0x12100000 /* Daytona_SPS */
-#define INTCTL1_PADDR             0x12100800 /* Daytona_SPS */
-#define INTCTL2_PADDR             0x12101000 /* Daytona_SPS */
-#define INTCTL3_PADDR             0x12101800 /* Daytona_SPS */
-#define INTCTL4_PADDR             0x12102000 /* Daytona_SPS */
-#define INTCTL5_PADDR             0x12102800 /* Daytona_SPS */
-#define INTCTL6_PADDR             0x12103000 /* Daytona_SPS */
-#define INTCTL7_PADDR             0x12103800 /* Daytona_SPS */
-#define SDC2_PADDR                0x12140000 /* Daytona_SPS */
-#define SDC2_DML_PADDR            0x12140800 /* Daytona_SPS */
-#define SDC2_BAM_PADDR            0x12142000 /* Daytona_SPS */
-#define SDC3_PADDR                0x12180000 /* Daytona_SPS */
-#define SDC3_DML_PADDR            0x12180800 /* Daytona_SPS */
-#define SDC3_BAM_PADDR            0x12182000 /* Daytona_SPS */
-#define SDC4_PADDR                0x121C0000 /* Daytona_SPS */
-#define SDC4_DML_PADDR            0x121C0800 /* Daytona_SPS */
-#define SDC4_BAM_PADDR            0x121C2000 /* Daytona_SPS */
-#define BAM_DMA_PADDR             0x12240000 /* Daytona_SPS */
-#define BAM_DMA_BAM_PADDR         0x12244000 /* Daytona_SPS */
-#define BAM_DMA_BAM_XPU_PADDR     0x12246000 /* Daytona_SPS */
-#define SDC1_PADDR                0x12400000 /* Daytona_SPS */
-#define SDC1_DML_PADDR            0x12400800 /* Daytona_SPS */
-#define SDC1_BAM_PADDR            0x12402000 /* Daytona_SPS */
-#define SPS_GSBI1_PADDR           0x12440000 /* Daytona_SPS */
-#define SPS_UART1_DM_PADDR        0x12450000 /* Daytona_SPS */
-#define SPS_QUP1_PADDR            0x12460000 /* Daytona_SPS */
-#define SPS_GSBI2_PADDR           0x12480000 /* Daytona_SPS */
-#define SPS_UART2_DM_PADDR        0x12490000 /* Daytona_SPS */
-#define SPS_QUP2_PADDR            0x124A0000 /* Daytona_SPS */
-#define USB1_HS_PADDR             0x12500000 /* Daytona_SPS */
-#define USB1_HS_BAM_PADDR         0x12502000 /* Daytona_SPS */
-#define USB2_HSIC_PADDR           0x12510000 /* Daytona_SPS */
-#define USB3_HS_PADDR             0x12520000 /* Daytona_SPS */
-#define USB3_HS_BAM_PADDR         0x12522000 /* Daytona_SPS */
-#define USB4_HS_PADDR             0x12530000 /* Daytona_SPS */
-#define USB4_HS_BAM_PADDR         0x12532000 /* Daytona_SPS */
-#define CE2_CRYPTO4_PADDR         0x12560000 /* Security */
-#define GSBI3_PADDR               0x16200000 /* GSBIs */
-#define GSBI3_UART_DM_PADDR       0x16240000 /* GSBIs */
-#define QUP3_PADDR                0x16280000 /* GSBIs */
-#define GSBI4_PADDR               0x16300000 /* GSBIs */
-#define GSBI4_UART_DM_PADDR       0x16340000 /* GSBIs */
-#define QUP4_PADDR                0x16380000 /* GSBIs */
-#define GSBI6_PADDR               0x16500000 /* GSBIs */
-#define GSBI6_UART_DM_PADDR       0x16540000 /* GSBIs */
-#define QUP6_PADDR                0x16580000 /* GSBIs */
-#define GSBI7_PADDR               0x16600000 /* GSBIs */
-#define GSBI7_UART_DM_PADDR       0x16640000 /* GSBIs */
-#define QUP7_PADDR                0x16680000 /* GSBIs */
-#define LPASS_XPU_PADDR           0x17000000 /* chip_core_top_XPUs */
-#define KPSS_XPU_PADDR            0x17100000 /* chip_core_top_XPUs */
-#define GSS_XPU_PADDR             0x17200000 /* chip_core_top_XPUs */
-#define CFPB2_XPU_CFG_PADDR       0x17300000 /* chip_core_top_Peripherals */
-#define CSYSFPB2_PADDR            0x17400000 /* chip_core_top_Peripherals */
-#define CE3_XPU_CFG_PADDR         0x17500000 /* chip_core_top_XPUs */
-#define CSYSFPB_SPL_PADDR         0x17F00000 /* chip_core_top_Peripherals */
-#define USB1_FS_PADDR             0x18000000 /* chip_core_top_Peripherals */
-#define TSIF_PADDR                0x18200000 /* chip_core_top_Peripherals */
-#define TSPP_PADDR                0x18202000 /* chip_core_top_Peripherals */
-#define TSIF_BAM_PADDR            0x18204000 /* chip_core_top_Peripherals */
-#define ADM3_0_PADDR              0x18300000 /* chip_core_top_Peripherals */
-#define CE1_CRYPTO4_PADDR         0x18500000 /* Security */
-#define TSSC_PADDR                0x18600000 /* chip_core_top_Peripherals */
-#define TSSC_SSBI_PADDR           0x18600000 /* chip_core_top_Peripherals */
-#define MSM_PDM_PADDR             0x18700000 /* chip_core_top_Peripherals */
-#define CSYSFPB_MST_PADDR         0x18D00000 /* chip_core_top_Peripherals */
-#define CFPB1_XPU_CFG_PADDR       0x18E00000 /* chip_core_top_Peripherals */
-#define CSYSFPB1_PADDR            0x18F00000 /* chip_core_top_Peripherals */
-#define GSBI5_PADDR               0x1A200000 /* GSBIs */
-#define GSBI5_UART_DM_PADDR       0x1A240000 /* GSBIs */
-#define QUP5_PADDR                0x1A280000 /* GSBIs */
-#define PMEM_PADDR                0x1A300000 /* chip_core_top_Peripherals */
-#define MSM_TCSR_PADDR            0x1A400000 /* chip_core_top_Peripherals */
-#define PRNG_PADDR                0x1A500000 /* chip_core_top_Peripherals */
-#define DIM_D00_REG_PADDR         0x1A700000 /* LPDDR */
-#define DIM_BD0_REG_PADDR         0x1A780000 /* EBI1_DIM */
-#define DIM_D01_REG_PADDR         0x1A800000 /* LPDDR */
-#define DIM_D02_REG_PADDR         0x1A900000 /* LPDDR */
-#define DIM_D03_REG_PADDR         0x1AA00000 /* LPDDR */
-#define DIM_C00_REG_PADDR         0x1AB00000 /* LPDDR */
-#define DIM_BC0_REG_PADDR         0x1AB40000 /* EBI1_DIM */
-#define DIM_C01_REG_PADDR         0x1AB80000 /* EBI1_DIM */
-#define DIM_D10_REG_PADDR         0x1AC00000 /* LPDDR */
-#define DIM_BD1_REG_PADDR         0x1AC80000 /* EBI1_DIM */
-#define DIM_D11_REG_PADDR         0x1AD00000 /* LPDDR */
-#define DIM_D12_REG_PADDR         0x1AE00000 /* LPDDR */
-#define DIM_D13_REG_PADDR         0x1AF00000 /* LPDDR */
-#define DIM_C10_REG_PADDR         0x1B000000 /* LPDDR */
-#define DIM_BC1_REG_PADDR         0x1B040000 /* EBI1_DIM */
-#define DIM_C11_REG_PADDR         0x1B080000 /* EBI1_DIM */
-#define CFPB0_XPU_CFG_PADDR       0x1B100000 /* chip_core_top_Peripherals */
-#define CSYSFPB0_PADDR            0x1B200000 /* chip_core_top_Peripherals */
-#define SATA_XPU_CFG_PADDR        0x1B300000 /* chip_core_top_XPUs */
-#define SATA_PHY_PADDR            0x1B400000 /* SATA */
-#define PCIE20_PADDR              0x1B500000 /* PCIE20 */
-#define PCIE20_ELBI_PADDR         0x1B502000 /* PCIE20 */
-#define PCIE20_PARF_PADDR         0x1B600000 /* PCIE20 */
-#define LPASS_CSR_PADDR           0x28000000 /* LP_Audio_Sub_System */
-#define LPASS_M2VMT_PADDR         0x28002000 /* LP_Audio_Sub_System */
-#define LPASS_M2VMT_Q6SS_PADDR    0x28003000 /* LP_Audio_Sub_System */
-#define LPASS_AHBTM_PADDR         0x2800A000 /* LP_Audio_Sub_System */
-#define LPASS_SLIMBUS_PADDR       0x28080000 /* LP_Audio_Sub_System */
-#define LPASS_BAM_LITE_PADDR      0x28084000 /* LP_Audio_Sub_System */
-#define LPA_IF_PADDR              0x28100000 /* LP_Audio_Sub_System */
-#define MIDI_PADDR                0x28200000 /* LP_Audio_Sub_System */
-#define LPASS_QDSP6SS_PUB_PADDR   0x28800000 /* LP_Audio_Sub_System */
-#define LPASS_QDSP6SS_CSR_PADDR   0x28880000 /* LP_Audio_Sub_System */
-#define LPASS_QDSP6SS_L2VIC_PADDR 0x28890000 /* LP_Audio_Sub_System */
-#define LPASS_QDSP6SS_SAW_PADDR   0x288B0000 /* LP_Audio_Sub_System */
-#define SATA_PADDR                0x29000000 /* SATA */
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/apq8064/plat/machine/hardware.h b/include/plat/apq8064/plat/machine/hardware.h
index 5a1499048..c2da5c965 100644
--- a/include/plat/apq8064/plat/machine/hardware.h
+++ b/include/plat/apq8064/plat/machine/hardware.h
@@ -14,37 +14,8 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const BOOT_RODATA kernel_frame_t kernel_devices[] = {
-    {
-        /*  timer used as PIT */
-        TIMER_PADDR,
-        TIMER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC */
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/bcm2837/plat/32/plat_mode/machine/devices.h b/include/plat/bcm2837/plat/32/plat_mode/machine/devices.h
deleted file mode 100644
index 3f98a89d1..000000000
--- a/include/plat/bcm2837/plat/32/plat_mode/machine/devices.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * 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_MODE_MACHINE_DEVICES_H
-#define __PLAT_MODE_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                   0xFFF01000
-#define INTC_PPTR                   0xFFF02000
-#define TIMER_PPTR                  0xFFF03000
-#define ARM_LOCAL_PPTR              0xFFF04000
-
-#endif /* __PLAT_MODE_MACHINE_DEVICES_H */
diff --git a/include/plat/bcm2837/plat/64/plat_mode/machine/devices.h b/include/plat/bcm2837/plat/64/plat_mode/machine/devices.h
deleted file mode 100644
index 97ae0f617..000000000
--- a/include/plat/bcm2837/plat/64/plat_mode/machine/devices.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * 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_MODE_MACHINE_DEVICES_H
-#define __PLAT_MODE_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                   0xFFFFFFFFFFF01000
-#define INTC_PPTR                   0xFFFFFFFFFFF02000
-#define TIMER_PPTR                  0xFFFFFFFFFFF03000
-#define ARM_LOCAL_PPTR              0xFFFFFFFFFFF04000
-
-#endif /* __PLAT_MODE_MACHINE_DEVICES_H */
diff --git a/include/plat/bcm2837/plat/machine.h b/include/plat/bcm2837/plat/machine.h
index de211048e..da5d5d29d 100644
--- a/include/plat/bcm2837/plat/machine.h
+++ b/include/plat/bcm2837/plat/machine.h
@@ -12,7 +12,7 @@
 
 #ifndef __PLAT_MACHINE_H
 #define __PLAT_MACHINE_H
-#include <plat_mode/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 #include <machine/io.h>
 
 #define BASIC_IRQ_OFFSET                32
@@ -86,7 +86,6 @@ enum IRQConstants {
 #define FIQCTRL_FIQ_SRC(src)                 (FIQCTRL_FIQ_SRC_##src)
 
 volatile struct intc_regs {
-    uint8_t  res[0x200];
     uint32_t bfIRQBasicPending;  /* 0x200 R     */
     uint32_t bfGPUIRQPending[2]; /* 0x204 R     */
     uint32_t FIQ_control;        /* 0x20C R/W   */
diff --git a/include/plat/bcm2837/plat/machine/devices.h b/include/plat/bcm2837/plat/machine/devices.h
deleted file mode 100644
index 97c289699..000000000
--- a/include/plat/bcm2837/plat/machine/devices.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*
- * 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_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define BUS_ADDR_OFFSET             0x7E000000
-#define PADDR_OFFSET                0x3F000000
-
-#define INTC_BUSADDR                0x7E00B000
-#define UART_BUSADDR                0x7E215000
-#define SDHC_BUSADDR                0x7E300000
-#define USB2_BUSADDR                0x7E980000
-#define SYSTEM_TIMER_BUSADDR        0x7E003000
-#define ARM_TIMER_BUSADDR           0x7E00B000
-
-#define ARM_LOCAL_PADDR             0x40000000
-
-/* We convert from the VC CPU BUS addresses to ARM Physical addresses due to the extra
-    VC (Video controller) MMU */
-#define INTC_PADDR                  (INTC_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-#define UART_PADDR                  (UART_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-#define SDHC_PADDR                  (SDHC_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-#define USB2_PADDR                  (USB2_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-#define SYSTEM_TIMER_PADDR          (SYSTEM_TIMER_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-#define TIMER_PADDR                 (ARM_TIMER_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/bcm2837/plat/machine/hardware.h b/include/plat/bcm2837/plat/machine/hardware.h
index 6ec77138a..b90a585a0 100644
--- a/include/plat/bcm2837/plat/machine/hardware.h
+++ b/include/plat/bcm2837/plat/machine/hardware.h
@@ -16,34 +16,8 @@
 #include <types.h>
 #include <basic_types.h>
 #include <linker.h>
-#include <plat/machine.h>
-#include <plat/machine/devices.h>
-#include <plat/machine/devices_gen.h>
 #include <machine/io.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /* BCM2837 Interrupt controller */
-        INTC_PADDR,
-        INTC_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  ARM Interrupt controller ? */
-        ARM_LOCAL_PADDR,
-        ARM_LOCAL_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 void initL2Cache(void);
 
 static inline void plat_cleanL2Range(paddr_t start, paddr_t end) {}
diff --git a/include/plat/exynos4/plat/machine/devices.h b/include/plat/exynos4/plat/machine/devices.h
deleted file mode 100644
index ee10ecd2e..000000000
--- a/include/plat/exynos4/plat/machine/devices.h
+++ /dev/null
@@ -1,188 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                   0xfff01000
-#define MCT_PPTR                    0xfff02000
-#define L2CC_PPTR                   0xfff03000
-#define GIC_CONTROLLER_PPTR         0xfff04000
-#define GIC_DISTRIBUTOR_PPTR        0xfff05000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff06000
-
-#define L2CC_L2C310_PPTR            L2CC_PPTR
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define EXYNOS_MCT_MHZ              24
-#define EXYNOS_MCT_PPTR             MCT_PPTR
-
-/* Other devices on the SoC */
-#define CHIPID_PADDR                0x10000000
-#define SYSREG_PADDR                0x10010000
-#define PMU_PADDR                   0x10020000
-#define CMU_TOP_PART_PADDR          0x10030000
-#define CMU_DMC_PART_PADDR          0x10040000
-#define MCT_PADDR                   0x10050000
-#define WDT_PADDR                   0x10060000
-#define RTC_PADDR                   0x10070000
-#define KEYIF_PADDR                 0x100A0000
-#define HDMI_CEC_PADDR              0x100B0000
-#define TMU_PADDR                   0x100C0000
-#define SECKEY_PADDR                0x10100000
-#define TZPC0_PADDR                 0x10110000
-#define TZPC1_PADDR                 0x10120000
-#define TZPC2_PADDR                 0x10130000
-#define TZPC3_PADDR                 0x10140000
-#define TZPC4_PADDR                 0x10150000
-#define TZPC5_PADDR                 0x10160000
-#define DMC0_PADDR                  0x10400000
-#define DMC1_PADDR                  0x10410000
-#define INT_COMBINER_PADDR          0x10440000
-#define IEM_IEC_PADDR               0x10460000
-#define IEM_APC_PADDR               0x10470000
-#define GIC_CONTROLLER0_PADDR       0x10480000
-#define GIC_CONTROLLER1_PADDR       0x10488000
-#define GIC_DISTRIBUTOR_PADDR       0x10490000
-#define CORE_TIMERS_PADDR           0x104C0000
-#define MPCORE_PRIV_REG_PADDR       0x10500000
-#define L2CC_PADDR                  0x10502000
-#define AXI_DMCD_PADDR              0x10600000
-#define AXI_DMCSFRX_PADDR           0x10620000
-#define ASYNCAXI_GDL_DMCD_PADDR     0x10640000
-#define ASYNCAXI_GDR_DMCD_PADDR     0x10650000
-#define QECPU_PADDR                 0x10680000
-#define SMDMA0_PADDR                0x10800000
-#define NSMDMA0_PADDR               0x10810000
-#define SSS_PADDR                   0x10830000
-#define CORESIGHT_PADDR             0x10880000
-#define AXI_ACPX_PADDR              0x10A00000
-#define SMMUMDMA_PADDR              0x10A40000
-#define SMMUSSS_PADDR               0x10A50000
-#define QEMDMA_PADDR                0x10AA0000
-#define QESSS_PADDR                 0x10AB0000
-#define AXI_MAUDIOX_PADDR           0x10E00000
-#define GPIO_RIGHT_PADDR            0x11000000
-#define AXI_GDR_PADDR               0x11200000
-#define AXI_GPR_PADDR               0x11210000
-#define ASYNCAXI_CAMIF_PADDR        0x11240000
-#define ASYNCAXI_LCD0_PADDR         0x11250000
-#define ASYNCAXI_LCD1_PADDR         0x11260000
-#define ASYNCAXI_FSYSD_PADDR        0x11270000
-#define ASYNCAXI_MAUDIO_PADDR       0x11290000
-#define GPIO_LEFT_PADDR             0x11400000
-#define AXI_GDL_PADDR               0x11600000
-#define AXI_GPL_PADDR               0x11610000
-#define ASYNCAXI_IMAGE_PADDR        0x11640000
-#define ASYNCAXI_TV_PADDR           0x11650000
-#define ASYNCAXI_MFC_L_PADDR        0x11660000
-#define FIMC0_PADDR                 0x11800000
-#define FIMC1_PADDR                 0x11810000
-#define FIMC2_PADDR                 0x11820000
-#define FIMC3_PADDR                 0x11830000
-#define JPEG_PADDR                  0x11840000
-#define MIPI_CSI0_PADDR             0x11880000
-#define MIPI_CSI1_PADDR             0x11890000
-#define AXI_CAMX_PADDR              0x11A00000
-#define SMMUFIMC0_PADDR             0x11A20000
-#define SMMUFIMC1_PADDR             0x11A30000
-#define SMMUFIMC2_PADDR             0x11A40000
-#define SMMUFIMC3_PADDR             0x11A50000
-#define SMMUJPEG_PADDR              0x11A60000
-#define QEFIMC0_PADDR               0x11A70000
-#define QEFIMC1_PADDR               0x11A80000
-#define QEFIMC2_PADDR               0x11A90000
-#define QEFIMC3_PADDR               0x11AA0000
-#define FIMD0_PADDR                 0x11C00000
-#define MIE0_PADDR                  0x11C20000
-#define MIPI_DSI0_PADDR             0x11C80000
-#define AXI_LCD0_PADDR              0x11E00000
-#define SMMUFIMD0_PADDR             0x11E20000
-#define FIMD1_PADDR                 0x12000000
-#define MIE1_PADDR                  0x12020000
-#define MIPI_DSI1_PADDR             0x12080000
-#define AXI_LCD1X_PADDR             0x12200000
-#define SMMUFIMD1_PADDR             0x12220000
-#define PPMU_LCD1_PADDR             0x12240000
-#define PCIE_PADDR                  0x12400000
-#define USBDEV_LINK_PADDR           0x12480000
-#define TSI_PADDR                   0x12500000
-#define SDMMC0_PADDR                0x12510000
-#define SDMMC1_PADDR                0x12520000
-#define SDMMC2_PADDR                0x12530000
-#define SDMMC3_PADDR                0x12540000
-#define SDMMC4_PADDR                0x12550000
-#define SATA_PADDR                  0x12560000
-#define SROMC_PADDR                 0x12570000
-#define USBHOST_EHCI_PADDR          0x12580000
-#define USBHOST_OHCI_PADDR          0x12590000
-#define USBPHY_CON_PADDR            0x125B0000
-#define PCIEPHY_PADDR               0x125C0000
-#define SATA_PHY_PADDR              0x125D0000
-#define AXI_FSYSD_PADDR             0x12600000
-#define AXI_FSYSS_PADDR             0x12610000
-#define SMMUPCIE_PADDR              0x12620000
-#define PDMA0_PADDR                 0x12680000
-#define PDMA1_PADDR                 0x12690000
-#define PCIEPHY_CTRL_PADDR          0x126A0000
-#define SATAPHY_CTRL_PADDR          0x126B0000
-#define SMDMA2_PADDR                0x12840000
-#define NSMDMA2_PADDR               0x12850000
-#define AXI_IMGX_PADDR              0x12A00000
-#define SMMUG2D_PADDR               0x12A20000
-#define SMMUROTATOR_PADDR           0x12A30000
-#define SMMUMDMA2_PADDR             0x12A40000
-#define QEG2D_PADDR                 0x12A60000
-#define QEROTATOR_PADDR             0x12A70000
-#define QEMDMA2_PADDR               0x12A80000
-#define VP_PADDR                    0x12C00000
-#define MIXER_PADDR                 0x12C10000
-#define TVENC_PADDR                 0x12C20000
-#define HDMI0_PADDR                 0x12D00000
-#define HDMI1_PADDR                 0x12D10000
-#define HDMI2_PADDR                 0x12D20000
-#define HDMI3_PADDR                 0x12D30000
-#define HDMI4_PADDR                 0x12D40000
-#define HDMI5_PADDR                 0x12D50000
-#define HDMI6_PADDR                 0x12D60000
-#define AXI_TVX_PADDR               0x12E00000
-#define SMMUTV_PADDR                0x12E20000
-#define SMMUMFC_L_PADDR             0x13620000
-#define SMMUMFC_R_PADDR             0x13630000
-#define UART0_PADDR                 0x13800000
-#define UART1_PADDR                 0x13810000
-#define UART2_PADDR                 0x13820000
-#define UART3_PADDR                 0x13830000
-#define UART4_PADDR                 0x13840000
-#define I2C0_PADDR                  0x13860000
-#define I2C1_PADDR                  0x13870000
-#define I2C2_PADDR                  0x13880000
-#define I2C3_PADDR                  0x13890000
-#define I2C4_PADDR                  0x138A0000
-#define I2C5_PADDR                  0x138B0000
-#define I2C6_PADDR                  0x138C0000
-#define I2C7_PADDR                  0x138D0000
-#define I2CHDMI_PADDR               0x138E0000
-#define TSADC_PADDR                 0x13910000
-#define SPI0_PADDR                  0x13920000
-#define SPI1_PADDR                  0x13930000
-#define SPI2_PADDR                  0x13940000
-#define I2S1_PADDR                  0x13960000
-#define I2S2_PADDR                  0x13970000
-#define PCM1_PADDR                  0x13980000
-#define PCM2_PADDR                  0x13990000
-#define AC97_PADDR                  0x139A0000
-#define SPDIF_PADDR                 0x139B0000
-#define PWMTIMER_PADDR              0x139D0000
-#define MODEMIF_PADDR               0x13A00000
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/exynos4/plat/machine/hardware.h b/include/plat/exynos4/plat/machine/hardware.h
index c170fd00f..c2da5c965 100644
--- a/include/plat/exynos4/plat/machine/hardware.h
+++ b/include/plat/exynos4/plat/machine/hardware.h
@@ -14,42 +14,8 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  Watch dog timer used as PIT */
-        MCT_PADDR,
-        MCT_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC */
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  L2CC */
-        L2CC_PADDR,
-        L2CC_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        UART1_PADDR,
-        UART_PPTR,
-        true
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/exynos5/plat/machine/devices.h b/include/plat/exynos5/plat/machine/devices.h
deleted file mode 100644
index 3caf5d976..000000000
--- a/include/plat/exynos5/plat/machine/devices.h
+++ /dev/null
@@ -1,280 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <config.h>
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                   0xfff01000
-#define MCT_PPTR                    0xfff02000
-#define L2CC_PPTR                   0xfff03000
-#define GIC_DISTRIBUTOR_PPTR        0xfff04000
-#define GIC_CONTROLLER_PPTR         0xfff05000
-#define GIC_VCPUCTRL_PPTR           0xfff06000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff07000
-
-/* HYP mode kernel devices */
-#define GIC_PL400_VCPUCTRL_PPTR     GIC_VCPUCTRL_PPTR
-
-#define L2CC_L2C310_PPTR            L2CC_PPTR
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       (GIC_PADDR + 0x1000)
-#define GIC_CONTROLLER0_PADDR       (GIC_PADDR + 0x2000)
-#define GIC_VCPUCTRL_PADDR          (GIC_PADDR + 0x4000)
-#define GIC_VCPU_PADDR              (GIC_PADDR + 0x6000)
-
-#define EXYNOS_MCT_MHZ              24
-#define EXYNOS_MCT_PPTR             MCT_PPTR
-
-/* Generic devices */
-#define SECURE_FIRMWARE       0x02070000
-#define CHIP_ID_PADDR         0x10000000
-#define CMU_CPU_PADDR         0x10010000
-#define CMU_CORE_PADDR        0x10014000
-#define CMU_ACP_PADDR         0x10018000
-#define CMU_ISP_PADDR         0x1001C000
-#define CMU_TOP_PADDR         0x10020000
-#define CMU_LEX_PADDR         0x10024000
-#define CMU_R0X_PADDR         0x10028000
-#define CMU_R1X_PADDR         0x1002C000
-#define CMU_CDREX_PADDR       0x10030000
-#define CMU_MEM_PADDR         0x10038000
-#define ALIVE_PADDR           0x10040000
-#define SYSREG_PADDR          0x10050000
-#define TMU0_PADDR            0x10060000
-#define TMU1_PADDR            0x10064000
-#define TMU2_PADDR            0x10068000
-#define TMU3_PADDR            0x1006C000
-#define TMU_GPU_PADDR         0x100A0000
-#define MONOTONIC_CNT_PADDR   0x100C0000
-#define HDMI_CEC_PADDR        0x101B0000
-#define MCT_PADDR             0x101C0000
-#define WDT_PADDR             0x101D0000
-#define RTC_PADDR             0x101E0000
-#define INT_COMB_CPU_PADDR    0x10440000
-#define INT_COMB_IOP_PADDR    0x10450000
-#define GIC_PADDR             0x10480000
-#define GIC_IOPC_PADDR        0x104A0000
-#define GIC_IOPD_PADDR        0x104B0000
-#define MPCORE_PRIV_REG_PADDR 0x10500000
-#define NS_MDMA0_PADDR        0x10800000
-#define SSS_PADDR             0x10830000
-#define SSS_KEY_PADDR         0x10840000
-#define ENGINE_2D_PADDR       0x10850000
-#define CSSYS_PADDR           0x10880000
-#define A15_EAGLE_PADDR       0x10890000
-#define A5_IOP_PADDR          0x108A0000
-#define A5_ISP_PADDR          0x108B0000
-#define SYSMMU_MDMA_PADDR     0x10A40000
-#define SYSMMU_SSS_PADDR      0x10A50000
-#define SYSMMU_2D_PADDR       0x10A60000
-#define DREXII_PHY0_PADDR     0x10C00000
-#define DREXII_PHY1_PADDR     0x10C10000
-#define AS_A_3D_PADDR         0x10CC0000
-#define AS_A_C2C_PADDR        0x10CD0000
-#define AS_A_LEFT_BUS_PADDR   0x10CE0000
-#define AS_A_RIGHT0_BUS_PADDR 0x10CF0000
-#define AS_A_DISP1_BUS_PADDR  0x10D00000
-#define DREXII_PADDR          0x10DD0000
-#define AS_A_EFCON_PADDR      0x10DE0000
-#define AP_C2C_PADDR          0x10E00000
-#define CP_C2C_PADDR          0x10E40000
-#define AS_A_ACP_BLK_PADDR    0x10E80000
-#define AS_A_CPU_P_BLK_PADDR  0x10E90000
-#define AS_A_LBX_BUS_PADDR    0x10F00000
-#define AS_A_R1BX_BUS_PADDR   0x10F10000
-#define AS_A_R0BX_BUS_PADDR   0x10F20000
-#define AS_A_CPU_PADDR        0x10F30000
-#define MFC_PADDR             0x11000000
-#define SYSMMU_MFC0_PADDR     0x11200000
-#define SYSMMU_MFC1_PADDR     0x11210000
-#define AS_A_MFC_PADDR        0x11680000
-#define AS_A_GENX_PADDR       0x116A0000
-#define ENGINE_3D_PADDR       0x11800000
-#define ROTATOR_PADDR         0x11C00000
-#define NS_MDMA1_PADDR        0x11C10000
-#define SYSMMU_ROTATOR_PADDR  0x11D40000
-#define SYSMMU_MDMA1_PADDR    0x11D50000
-#define AS_A_FILE_PADDR       0x11DA0000
-#define AS_A_GPS_PADDR        0x11DB0000
-#define AS_A_JPEG_PADDR       0x11DC0000
-#define JPEG_PADDR            0x11E00000
-#define SYSMMU_JPEG_PADDR     0x11F20000
-#define USB3_DEV_LINK_PADDR   0x12000000
-#define USB3_DEV_CTRL_PADDR   0x12100000
-#define USB2_HOST_EHCI_PADDR  0x12110000
-#define USB2_HOST_OHCI_PADDR  0x12120000
-#define USB2_HOST_CTRL_PADDR  0x12130000
-#define USB2_DEV_LINK_PADDR   0x12140000
-#define MIPI_HSI_PADDR        0x12160000
-#define SATA_PHY_CTRL_PADDR   0x12170000
-#define MCUCTL_IOP_PADDR      0x12180000
-#define WDT_IOP_PADDR         0x12190000
-#define PDMA0_PADDR           0x121A0000
-#define PDMA1_PADDR           0x121B0000
-#define RTIC_PADDR            0x121C0000
-#define SATA_I2CPHYCTRL_PADDR 0x121D0000
-#define MSH0_PADDR            0x12200000
-#define MSH1_PADDR            0x12210000
-#define MSH2_PADDR            0x12220000
-#define MSH3_PADDR            0x12230000
-#define SROMC_PADDR           0x12250000
-#define SATA_PADDR            0x122F0000
-#define AXI_FILE_D64_PADDR    0x12300000
-// #define AXI_FILE_D64_PADDR    0x12310000
-#define AXI_USBSATA_D64_PADDR 0x12320000
-// #define AXI_USBSATA_D64_PADDR 0x12330000
-#define SYSMMU_IOPROC_PADDR   0x12360000
-#define SYSMMU_RTIC_PADDR     0x12370000
-#define AS_A_IOP_FD64X_PADDR  0x12380000
-#define AS_A_AUDIO_PADDR      0x12390000
-#define USB_PADDR             0x12400000
-#define USB3_PHY1_PADDR       0x12500000
-#define AXI_GPS_PADDR         0x12600000
-// #define AXI_GPS_PADDR         0x12610000
-#define AS_A_GPSCPU_PADDR     0x12620000
-#define SYSMMU_GPS_PADDR      0x12630000
-#define UART0_PADDR           0x12C00000
-#define UART1_PADDR           0x12C10000
-#define UART2_PADDR           0x12C20000
-#define UART3_PADDR           0x12C30000
-#define USI0_PADDR            0x12C50000
-#define I2C0_PADDR            0x12C60000
-#define I2C1_PADDR            0x12C70000
-#define I2C2_PADDR            0x12C80000
-#define I2C3_PADDR            0x12C90000
-#define I2C4_PADDR            0x12CA0000
-#define I2C5_PADDR            0x12CB0000
-#define I2C6_PADDR            0x12CC0000
-#define I2C7_PADDR            0x12CD0000
-#define I2C_HDMI_PADDR        0x12CE0000
-#define USI1_PADDR            0x12D00000
-#define TSADC_PADDR           0x12D10000
-#define SPI0_PADDR            0x12D20000
-#define SPI1_PADDR            0x12D30000
-#define SPI2_PADDR            0x12D40000
-#define USI2_PADDR            0x12D50000
-#define I2S1_PADDR            0x12D60000
-#define I2S2_PADDR            0x12D70000
-#define PCM1_PADDR            0x12D80000
-#define PCM2_PADDR            0x12D90000
-#define AC97_PADDR            0x12DA0000
-#define SPDIF_PADDR           0x12DB0000
-#define PWM_PADDR             0x12DD0000
-#define USI3_PADDR            0x12DE0000
-#define FIMC_ISP_PADDR        0x13000000
-#define FIMC_DRC_TOP_PADDR    0x13010000
-#define FIMC_SCALERC_PADDR    0x13020000
-#define FIMC_SCALERP_PADDR    0x13030000
-#define FIMC_FD_TOP_PADDR     0x13040000
-#define FIMC_ODC_PADDR        0x13050000
-#define FIMC_DIS_PADDR        0x13060000
-#define FIMC_3DNR_PADDR       0x13070000
-#define ASYNC_AXI_M_PADDR     0x130F0000
-#define MPWM_ISP_PADDR        0x13110000
-#define I2C2_ISP_PADDR        0x13120000
-#define I2C0_ISP_PADDR        0x13130000
-#define I2C1_ISP_PADDR        0x13140000
-#define MTCADC_ISP_PADDR      0x13150000
-#define PWM_ISP_PADDR         0x13160000
-#define WDT_ISP_PADDR         0x13170000
-#define MCUCTL_ISP_PADDR      0x13180000
-#define UART_ISP_PADDR        0x13190000
-#define SPI0_ISP_PADDR        0x131A0000
-#define SPI1_ISP_PADDR        0x131B0000
-#define GIC_C_ISP_PADDR       0x131E0000
-#define GIC_D_ISP_PADDR       0x131F0000
-#define SYSMMU_FIMCISP_PADDR  0x13260000
-#define SYSMMU_FIMCDRC_PADDR  0x13270000
-#define SYSMMU_FIMCSCLC_PADDR 0x13280000
-#define SYSMMU_FIMCSCLP_PADDR 0x13290000
-#define SYSMMU_FIMCFD_PADDR   0x132A0000
-#define SYSMMU_ISPCPU_PADDR   0x132B0000
-#define SYSMMU_FIMCODC_PADDR  0x132C0000
-#define SYSMMU_FIMCDIS0_PADDR 0x132D0000
-#define SYSMMU_FIMCDIS1_PADDR 0x132E0000
-#define SYSMMU_FIMC3DNR_PADDR 0x132F0000
-#define AS_A_MFC0_PADDR       0x13620000
-#define AS_A_ISP0_PADDR       0x13640000
-#define AS_A_ISP1_PADDR       0x13650000
-#define AS_A_RIGHT1_PADDR     0x13670000
-#define FIMCLT0_PADDR         0x13C00000
-#define FIMCLT1_PADDR         0x13C10000
-#define MIPI_CSI0_PADDR       0x13C20000
-#define MIPI_CSI1_PADDR       0x13C30000
-#define SYSMMU_FIMCLT0_PADDR  0x13C40000
-#define SYSMMU_FIMCLT1_PADDR  0x13C50000
-#define FIMCLT2_PADDR         0x13C90000
-#define SYSMMU_FIMCLT2_PADDR  0x13CA0000
-#define GSCALER0_PADDR        0x13E00000
-#define GSCALER1_PADDR        0x13E10000
-#define GSCALER2_PADDR        0x13E20000
-#define GSCALER3_PADDR        0x13E30000
-#define AS_A_GS0_PADDR        0x13E40000
-#define AS_A_GS1_PADDR        0x13E50000
-#define AS_A_GS2_PADDR        0x13E60000
-#define AS_A_GS3_PADDR        0x13E70000
-#define SYSMMU_GSCALER0_PADDR 0x13E80000
-#define SYSMMU_GSCALER1_PADDR 0x13E90000
-#define SYSMMU_GSCALER2_PADDR 0x13EA0000
-#define SYSMMU_GSCALER3_PADDR 0x13EB0000
-#define AS_A_GSCALER_PADDR    0x14220000
-#define DISP1_MIX_PADDR       0x14400000
-#define DISP1_ENH_PADDR       0x14410000
-#define DISP1_CTRL_PADDR      0x14420000
-#define MIE_PADDR             0x14430000
-#define TV_MIXER_PADDR        0x14450000
-#define MIPI_DSI1_PADDR       0x14500000
-#define DP1_PADDR             0x14510000
-#define HDMI_0_PADDR          0x14530000
-#define HDMI_1_PADDR          0x14540000
-#define HDMI_2_PADDR          0x14550000
-#define HDMI_3_PADDR          0x14560000
-#define HDMI_4_PADDR          0x14570000
-#define HDMI_5_PADDR          0x14580000
-#define HDMI_6_PADDR          0x14590000
-#define DP1_1_PADDR           0x145B0000
-#define HDMI_0_PHY_PADDR      0x145D0000
-#define SYSMMU_DISP1_PADDR    0x14640000
-#define SYSMMU_TV_PADDR       0x14650000
-#define AS_A_TV_PADDR         0x146D0000
-#define AES0EF0_PADDR         0x18000000
-#define EFCON0_SFR_PADDR      0x18200000
-#define AES0_SFR_PADDR        0x18300000
-#define AES1EF1_PADDR         0x18400000
-#define EFCON1_SFR_PADDR      0x18600000
-#define NS_NDMA_PADDR         0x18680000
-#define S_NDMA_PADDR          0x18690000
-#define AES1_SFR_PADDR        0x18700000
-
-#define AUDSS_PADDR           0x03810000
-
-/* SoC specific devices */
-#if defined(CONFIG_PLAT_EXYNOS5250)   /* Arndale */
-#define GPIO_LEFT_PADDR       0x11400000
-#define GPIO_RIGHT_PADDR      0x13400000
-#define C2C_GPIO_PADDR        0x10D10000
-#define AUDIO_GPIO_PADDR      0x03860000
-
-#elif defined(CONFIG_PLAT_EXYNOS54XX) /* Odroid XU and XU3 */
-#define GPIO_LEFT_PADDR       0x14000000
-#define GPIO_RIGHT_PADDR      0x13400000
-#define C2C_GPIO_PADDR        0x10D10000
-#define AUDIO_GPIO_PADDR      0x03860000
-
-#else  /* PLAT_EXYNOS5XXX */
-#error Unidentified EXYNOS5 SoC
-#endif /* PLAT_EXYNOS5XXX */
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/exynos5/plat/machine/hardware.h b/include/plat/exynos5/plat/machine/hardware.h
index e2cdc589c..8613e9155 100644
--- a/include/plat/exynos5/plat/machine/hardware.h
+++ b/include/plat/exynos5/plat/machine/hardware.h
@@ -16,43 +16,8 @@
 #include <linker.h>
 #include <arch/object/vcpu.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  Watch dog timer used as PIT */
-        MCT_PADDR,
-        MCT_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC */
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-    },
-    {
-        GIC_VCPUCTRL_PADDR,
-        GIC_VCPUCTRL_PPTR,
-        false, /* armExecuteNever */
-#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        UART2_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/hikey/plat/32/plat_mode/machine/devices.h b/include/plat/hikey/plat/32/plat_mode/machine/devices.h
deleted file mode 100644
index 9516d17b6..000000000
--- a/include/plat/hikey/plat/32/plat_mode/machine/devices.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * 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_MODE_MACHINE_DEVICES_H
-#define __PLAT_MODE_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                  0xfff01000
-#define GIC_DISTRIBUTOR_PPTR        0xfff03000
-#define GIC_CONTROLLER_PPTR         0xfff04000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff05000
-
-#endif /* __PLAT_MODE_MACHINE_DEVICES_H */
diff --git a/include/plat/hikey/plat/64/plat_mode/machine/devices.h b/include/plat/hikey/plat/64/plat_mode/machine/devices.h
deleted file mode 100644
index 9a2bf2af0..000000000
--- a/include/plat/hikey/plat/64/plat_mode/machine/devices.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * 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_MODE_MACHINE_DEVICES_H
-#define __PLAT_MODE_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                  0xffffffffffff0000
-#define GIC_DISTRIBUTOR_PPTR        0xffffffffffff3000
-#define GIC_CONTROLLER_PPTR         0xffffffffffff4000
-
-#endif /* __PLAT_MODE_MACHINE_DEVICES_H */
diff --git a/include/plat/hikey/plat/machine/devices.h b/include/plat/hikey/plat/machine/devices.h
deleted file mode 100644
index b6899ce01..000000000
--- a/include/plat/hikey/plat/machine/devices.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*
- * Copyright 2016, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-/*
- definitions for memory addresses of HiSilicon hi6220 platform
- listed in the order of ascending memory address, similar to the datasheet
- the size must all be powers of 2 and page aligned (4k or 1M).
-*/
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <plat_mode/machine/devices.h>
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       GIC_PADDR + 0x1000
-#define GIC_CONTROLLER0_PADDR       GIC_PADDR + 0x2000
-
-
-#define UART0_PADDR                 0xF8015000
-#define UART1_PADDR                 0xF7111000
-#define UART2_PADDR                 0xF7112000
-#define UART3_PADDR                 0xF7113000
-#define UART4_PADDR                 0xF7114000
-#define GIC_PADDR                   0xf6800000
-#define RTC0_PADDR                  0xF8003000
-#define RTC1_PADDR                  0xF8004000
-#define DMTIMER0_PADDR              0xF8008000
-#define DMTIMER1_PADDR              0xF8009000
-#define DMTIMER2_PADDR              0xF800A000
-#define DMTIMER3_PADDR              0xF800B000
-#define DMTIMER4_PADDR              0xF800C000
-#define DMTIMER5_PADDR              0xF800D000
-#define DMTIMER6_PADDR              0xF800E000
-#define DMTIMER7_PADDR              0xF800F000
-#define DMTIMER8_PADDR              0xF8010000
-
-
-#endif
diff --git a/include/plat/hikey/plat/machine/hardware.h b/include/plat/hikey/plat/machine/hardware.h
index dfa719336..cad9016ad 100755
--- a/include/plat/hikey/plat/machine/hardware.h
+++ b/include/plat/hikey/plat/machine/hardware.h
@@ -15,31 +15,8 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  GIC */
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART0_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/imx31/plat/machine/devices.h b/include/plat/imx31/plat/machine/devices.h
index cfc5234ad..c7aa59670 100644
--- a/include/plat/imx31/plat/machine/devices.h
+++ b/include/plat/imx31/plat/machine/devices.h
@@ -14,21 +14,6 @@
 #include <stdint.h>
 
 /* kernel devices */
-
-#define EPIT_PADDR                  0x53f94000
-#define EPIT_PPTR                   0xfff00000
-
-#define AVIC_PADDR                  0x68000000
-#define AVIC_PPTR                   0xfff01000
-
-#define L2CC_PADDR                  0x30000000
-#define L2CC_PPTR                   0xfff02000
-
-#define UART_PADDR                  0x43f90000
-#define UART_PPTR                   0xfff03000
-
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff04000
-
 struct imx31_l2cc_id {
     uint32_t id;           /* 000 */
     uint32_t type;         /* 004 */
diff --git a/include/plat/imx31/plat/machine/hardware.h b/include/plat/imx31/plat/machine/hardware.h
index ea7d11cd5..f5f9e035a 100644
--- a/include/plat/imx31/plat/machine/hardware.h
+++ b/include/plat/imx31/plat/machine/hardware.h
@@ -14,38 +14,7 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <plat/machine/interrupt.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  EPIT */
-        EPIT_PADDR,
-        EPIT_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  AVIC */
-        AVIC_PADDR,
-        AVIC_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  L2CC */
-        L2CC_PADDR,
-        L2CC_PPTR,
-        true  /* armExecuteNever */
-
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 #endif
diff --git a/include/plat/imx6/plat/machine/devices.h b/include/plat/imx6/plat/machine/devices.h
deleted file mode 100644
index df3ab708f..000000000
--- a/include/plat/imx6/plat/machine/devices.h
+++ /dev/null
@@ -1,192 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <config.h>
-
-/* These devices are used by the seL4 kernel. */
-#ifdef CONFIG_PLAT_SABRE
-#define UART_PADDR                  UART2_PADDR
-#elif defined(CONFIG_PLAT_WANDQ)
-#define UART_PADDR                  UART1_PADDR
-#else
-#error "unknown imx6 platform selected!"
-#endif
-
-#define UART_PPTR                   0xfff01000
-#define WDT_PPTR                    0xfff02000
-#define L2CC_PL310_PPTR             0xfff03000
-#define ARM_MP_PPTR1                0xfff04000
-#define ARM_MP_PPTR2                0xfff05000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff06000
-
-#define L2CC_L2C310_PPTR            (L2CC_PL310_PPTR      )
-#define ARM_MP_PRIV_TIMER_PPTR      (ARM_MP_PPTR1 + 0x600 )
-#define ARM_MP_GLOBAL_TIMER_PPTR    (ARM_MP_PPTR1 + 0x200 )
-#define GIC_PL390_CONTROLLER_PPTR   (ARM_MP_PPTR1 + 0x100 )
-#define GIC_PL390_DISTRIBUTOR_PPTR  (ARM_MP_PPTR2         )
-
-
-/* All devices */
-#define EIM_CS0_PADDR             0x08000000 /* 128 MB    */
-//#define RESERVED_PADDR          0x02C00000 /*  84 MB    */
-#define IPU2_PADDR                0x02800000 /*   4 MB    */
-#define IPU1_PADDR                0x02400000 /*   4 MB    */
-//#define RESERVED_PADDR          0x0220C000 /*   1 MB    */
-#define MIPI_HSI_PADDR            0x02208000 /*   4 pages */
-#define OPENVG_PADDR              0x02204000 /*   4 pages */
-#define SATA_PADDR                0x02200000 /*   4 pages */
-//#define RESERVED_PADDR          0x021FC000 /*   4 pages */
-//#define RESERVED_PADDR          0x021F8000 /*   4 pages */
-#define UART5_PADDR               0x021F4000 /*   4 pages */
-#define UART4_PADDR               0x021F0000 /*   4 pages */
-#define UART3_PADDR               0x021EC000 /*   4 pages */
-#define UART2_PADDR               0x021E8000 /*   4 pages */
-#define VDOA_PADDR                0x021E4000 /*   4 pages */
-#define MIPI_DSI_PADDR            0x021E0000 /*   4 pages */
-#define MIPI_CSI_PADDR            0x021DC000 /*   4 pages */
-#define AUDMUX_PADDR              0x021D8000 /*   4 pages */
-#define TZASC2_PADDR              0x021D4000 /*   4 pages */
-#define TZASC1_PADDR              0x021D0000 /*   4 pages */
-//#define RESERVED_PADDR          0x021CC000 /*   4 pages */
-//#define RESERVED_PADDR          0x021C8000 /*   4 pages */
-//#define RESERVED_PADDR          0x021C4000 /*   4 pages */
-#define CSU_PADDR                 0x021C0000 /*   4 pages */
-#define OCOTP_CTRL_PADDR          0x021BC000 /*   4 pages */
-#define EIM_PADDR                 0x021B8000 /*   4 pages */
-#define MMDC1_PADDR               0x021B4000 /*   4 pages */
-#define MMDC0_PADDR               0x021B0000 /*   4 pages */
-#define ROMCP_PADDR               0x021AC000 /*   4 pages */
-#define I2C3_PADDR                0x021A8000 /*   4 pages */
-#define I2C2_PADDR                0x021A4000 /*   4 pages */
-#define I2C1_PADDR                0x021A0000 /*   4 pages */
-#define USDHC4_PADDR              0x0219C000 /*   4 pages */
-#define USDHC3_PADDR              0x02198000 /*   4 pages */
-#define USDHC2_PADDR              0x02194000 /*   4 pages */
-#define USDHC1_PADDR              0x02190000 /*   4 pages */
-#define MLB150_PADDR              0x0218C000 /*   4 pages */
-#define ENET_PADDR                0x02188000 /*   4 pages */
-#define USBOH3_PADDR              0x02184000 /*   4 pages */
-//#define RESERVED_PADDR          0x02180000 /*   4 pages */
-#define AIPS2_CONFIG_PADDR        0x0217C000 /*   4 pages */
-#define ARM_MPCORE_PADDR          0x02161000 /*  27 pages */
-#define PLATFORM_CONTROL_PADDR    0x02160000 /*   1 page  */
-#define PTM3_PADDR                0x0215F000 /*   1 page  */
-#define PTM2_PADDR                0x0215E000 /*   1 page  */
-#define PTM1_PADDR                0x0215D000 /*   1 page  */
-#define PTM0_PADDR                0x0215C000 /*   1 page  */
-#define CTI3_PADDR                0x0215B000 /*   1 page  */
-#define CTI2_PADDR                0x0215A000 /*   1 page  */
-#define CTI1_PADDR                0x02159000 /*   1 page  */
-#define CTI0_PADDR                0x02158000 /*   1 page  */
-#define CPU3_PMU_PADDR            0x02157000 /*   1 page  */
-#define CPU3_DEBUG_PADDR          0x02156000 /*   1 page  */
-#define CPU2_PMU_PADDR            0x02155000 /*   1 page  */
-#define CPU2_DEBUG_PADDR          0x02154000 /*   1 page  */
-#define CPU1_PMU_PADDR            0x02153000 /*   1 page  */
-#define CPU1_PADDR                0x02152000 /*   1 page  */
-#define CPU0_PMU_PADDR            0x02151000 /*   1 page  */
-#define CPU0_DEBUG_PADDR          0x02150000 /*   1 page  */
-#define CA9_INTEG_PADDR           0x0214F000 /*   1 page  */
-//#define RESERVED_PADDR          0x02145000 /*  10 pages */
-#define FUNNEL_PADDR              0x02144000 /*   1 page  */
-#define TPIU_PADDR                0x02143000 /*   1 page  */
-#define CTI_PADDR                 0x02142000 /*   1 page  */
-#define ETB_PADDR                 0x02141000 /*   1 page  */
-#define DAP_ROM_TABLE_PADDR       0x02140000 /*   1 page  */
-//#define RESERVED_PADDR          0x02110000 /*  48 pages */
-#define CAAM_PADDR                0x02100000 /*  16 pages */
-//#define RESERVED_PADDR          0x020FC000 /*   4 pages */
-//#define RESERVED_PADDR          0x020F8000 /*   4 pages */
-//#define RESERVED_PADDR          0x020F4000 /*   4 pages */
-//#define RESERVED_PADDR          0x020F0000 /*   4 pages */
-#define SDMA_PADDR                0x020EC000 /*   4 pages */
-#define DCIC2_PADDR               0x020E8000 /*   4 pages */
-#define DCIC1_PADDR               0x020E4000 /*   4 pages */
-#define IOMUXC_PADDR              0x020E0000 /*   4 pages */
-//#define RESERVED_PADDR          0x020DD000 /*   3 pages */
-#define GPC_PADDR                 0x020DC000 /*   1 page  */
-#define SRC_PADDR                 0x020D8000 /*   4 pages */
-#define EPIT2_PADDR               0x020D4000 /*   4 pages */
-#define EPIT1_PADDR               0x020D0000 /*   4 pages */
-#define SNVS_HP_PADDR             0x020CC000 /*   4 pages */
-//#define RESERVED_PADDR          0x020CB000 /*   1 page  */
-#define USBPHY2_PADDR             0x020CA000 /*   1 page  */
-#define USBPHY1_PADDR             0x020C9000 /*   1 page  */
-#define ANALOG_PADDR              0x020C8000 /*   1 page  */
-#define CCM_PADDR                 0x020C4000 /*   4 pages */
-#define WDOG2_PADDR               0x020C0000 /*   4 pages */
-#define WDOG1_PADDR               0x020BC000 /*   4 pages */
-#define KPP_PADDR                 0x020B8000 /*   4 pages */
-#define GPIO7_PADDR               0x020B4000 /*   4 pages */
-#define GPIO6_PADDR               0x020B0000 /*   4 pages */
-#define GPIO5_PADDR               0x020AC000 /*   4 pages */
-#define GPIO4_PADDR               0x020A8000 /*   4 pages */
-#define GPIO3_PADDR               0x020A4000 /*   4 pages */
-#define GPIO2_PADDR               0x020A0000 /*   4 pages */
-#define GPIO1_PADDR               0x0209C000 /*   4 pages */
-#define GPT_PADDR                 0x02098000 /*   4 pages */
-#define CAN2_PADDR                0x02094000 /*   4 pages */
-#define CAN1_PADDR                0x02090000 /*   4 pages */
-#define PWM4_PADDR                0x0208C000 /*   4 pages */
-#define PWM3_PADDR                0x02088000 /*   4 pages */
-#define PWM2_PADDR                0x02084000 /*   4 pages */
-#define PWM1_PADDR                0x02080000 /*   4 pages */
-#define AIPS1_CONFIG_PADDR        0x0207C000 /*   4 pages */
-#define VPU_PADDR                 0x02040000 /*  60 pages */
-#define AIPS1_SPBA_PADDR          0x0203C000 /*   4 pages */
-//#define RESERVED_FOR_SDMA_PADDR 0x02038000 /*   4 pages */
-#define ASRC_PADDR                0x02034000 /*   4 pages */
-#define SSI3_PADDR                0x02030000 /*   4 pages */
-#define SSI2_PADDR                0x0202C000 /*   4 pages */
-#define SSI1_PADDR                0x02028000 /*   4 pages */
-#define ESAI_PADDR                0x02024000 /*   4 pages */
-#define UART1_PADDR               0x02020000 /*   4 pages */
-//#define RESERVED_FOR_SDMA_PADDR 0x0201C000 /*   4 pages */
-#define ECSPI5_PADDR              0x02018000 /*   4 pages */
-#define ECSPI4_PADDR              0x02014000 /*   4 pages */
-#define ECSPI3_PADDR              0x02010000 /*   4 pages */
-#define ECSPI2_PADDR              0x0200C000 /*   4 pages */
-#define ECSPI1_PADDR              0x02008000 /*   4 pages */
-#define SPDIF_PADDR               0x02004000 /*   4 pages */
-//#define RESERVED_FOR_SDMA_PADDR 0x02000000 /*   4 pages */
-#define PCIE_REGISTERS_PADDR      0x01FFC000 /*   4 pages */
-#define PCIE_PADDR                0x01000000 /*  15 MB    */
-//#define RESERVED_PADDR          0x00D00000 /*   3 MB    */
-#define GPV1_PL301_CONFIG_PADDR   0x00C00000 /*   1 MB    */
-#define GPV0_PL301_CONFIG_PADDR   0x00B00000 /*   1 MB    */
-//#define RESERVED_PADDR          0x00A03000 /* 253 pages */
-#define L2CC_PL310_PADDR          0x00A02000 /*   1 page  */
-#define ARM_MP_PADDR              0x00A00000 /*   2 pages */
-#define OCRAM_ALIASED_PADDR       0x00940000 /* 192 pages */
-#define OCRAM_PADDR               0x00900000 /*  64 pages */
-#define GPV4_PL301_CONFIG_PADDR   0x00800000 /*   1 MB    */
-//#define RESERVED_PADDR          0x00400000 /*   4 MB    */
-#define GPV3_PL301_CONFIG_PADDR   0x00300000 /*   1 MB    */
-#define GPV2_PL301_CONFIG_PADDR   0x00200000 /*   1 MB    */
-//#define RESERVED_PADDR          0x0013C000 /* 196 pages */
-#define DTCP_PADDR                0x00138000 /*   4 pages */
-#define GPU2D_PADDR               0x00134000 /*   4 pages */
-#define GPU3D_PADDR               0x00130000 /*   4 pages */
-//#define RESERVED_PADDR          0x00129000 /*   7 pages */
-#define HDMI_PADDR                0x00120000 /*   9 pages */
-//#define RESERVED_PADDR          0x00118000 /*   8 pages */
-#define BCH_PADDR                 0x00114000 /*   4 pages */
-#define GPMI_PADDR                0x00112000 /*   2 pages */
-#define APBH_BRIDGE_DMA_PADDR     0x00110000 /*   2 pages */
-//#define RESERVED_PADDR          0x00104000 /*  12 pages */
-#define CAAM_SECURE_RAM_PADDR     0x00100000 /*   4 pages */
-//#define RESERVED_PADDR          0x00018000 /* 232 pages */
-#define BOOT_ROM_PADDR            0x00000000 /*  24 pages */
-
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/imx6/plat/machine/hardware.h b/include/plat/imx6/plat/machine/hardware.h
index af4997744..89f72ea90 100644
--- a/include/plat/imx6/plat/machine/hardware.h
+++ b/include/plat/imx6/plat/machine/hardware.h
@@ -15,40 +15,9 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <arch/benchmark_overflowHandler.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  GIC controller and private timers */
-        ARM_MP_PADDR,
-        ARM_MP_PPTR1,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC distributor */
-        ARM_MP_PADDR + BIT(PAGE_BITS),
-        ARM_MP_PPTR2,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  L2CC */
-        L2CC_PL310_PADDR,
-        L2CC_PL310_PPTR,
-        true  /* armExecuteNever */
-
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 static inline void
 handleReservedIRQ(irq_t irq)
 {
diff --git a/include/plat/imx7/plat/machine/devices.h b/include/plat/imx7/plat/machine/devices.h
deleted file mode 100644
index 2958398a1..000000000
--- a/include/plat/imx7/plat/machine/devices.h
+++ /dev/null
@@ -1,185 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PADDR                  UART1_PADDR
-
-#define UART_PPTR                   0xfff01000
-#define WDT_PPTR                    0xfff02000
-#define ARM_MP_PPTR1                0xfff03000
-#define ARM_MP_PPTR2                0xfff04000
-#define ARM_MP_PPTR3                0xfff05000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff06000
-
-
-#define ARM_MP_PRIV_TIMER_PPTR      (ARM_MP_PPTR1 + 0x600 )
-#define ARM_MP_GLOBAL_TIMER_PPTR    (ARM_MP_PPTR1 + 0x200 )
-
-#define GIC_PL390_CONTROLLER_PPTR   (ARM_MP_PPTR3)
-#define GIC_PL390_DISTRIBUTOR_PPTR  (ARM_MP_PPTR2)
-
-
-#define ARM_SCU_PADDR               0x31000000
-
-/* All devices */
-#define ARM_MP_PADDR              (ARM_SCU_PADDR) /*   2 pages */
-
-/* addresses from Linux device tree */
-#define CAAM_PADDR                0x00100000      /* 32  KiB secure RAM                     */
-#define TCML_PADDR                0x007f8000      /* 32  KiB                                */
-#define TCMU_PADDR                0x00800000      /* 32  KiB                                */
-#define OCRAM_PADDR               0x00900000      /* 128 KiB                                */
-#define OCRAM_EPDC_PADDR          0x00920000      /* 128 KiB                                */
-#define OCRAM_PXP_PADDR           0x00940000      /* 32  KiB                                */
-#define EIM_PADDR                 0x28000000      /* 128 MiB    NOR/SRAM                    */
-/*--------------------------------- DAP memory map ---------------------------------------- */
-#define DAP_ROM_PADDR             0x30000000      /* 4   KiB DAP ROM table                  */
-#define CA7_DEBUG_ROM_PADDR       0x30040000      /* 4   KiB CA7 Debug ROM table            */
-#define CA7_ATB_FUNNEL_PADDR      0x30041000      /* 4   KiB CA7 ATB Funnel                 */
-#define CA7_ROM_PADDR             0x30060000      /* 4   KiB CA7 ROM table                  */
-#define CPU0_DEBUG_PADDR          0x30070000      /* 4   KiB CPU0 debug                     */
-#define CPU0_PMU_PADDR            0x30071000      /* 4   KiB CPU0 PMU                       */
-#define CPU1_DEBUG_PADDR          0x30072000      /* 4   KiB CPU1 debug                     */
-#define CPU1_PMU_PDDR             0x30073000      /* 4   KiB CPU1 PMU                       */
-#define CPU0_CTI_PADDR            0x30078000      /* 4   KiB CPU0 CTI                       */
-#define CPU1_CTI_PADDR            0x30079000      /* 4   KiB CPU1 CTI                       */
-#define CPU0_ETM_PADDR            0x3007c000      /* 4   KiB CPU0 ETM                       */
-#define CPU1_ETM_PADDR            0x3007d000      /* 4   KiB CPU1 ETM                       */
-#define CS_HUGO_ROM_PADDR         0x30080000      /* 4   KiB CoreSight Hugo ROM table       */
-#define TSGEN_CTRL_PADDR          0x30081000      /* 4   KiB                                */
-#define TSGEN_READ_PADDR          0x30082000      /* 4   KiB                                */
-#define ATB_FUNNEL_PADDR          0x30083000      /* 4   KiB                                */
-#define TMC_ETB_PADDR             0x30084000      /* 4   KiB                                */
-#define CS_HUGO_ATP_PADDR         0x30085000      /* 4   KiB CoreSight Hugo ATP replicator  */
-#define TMC_ETR_PADDR             0x30086000      /* 4   KiB                                */
-#define TPIU_PADDR                0x30087000      /* 4   KiB                                */
-#define CS_HUGO_CTI0_PADDR        0x30088000      /* 4   KiB                                */
-#define CS_HUGO_CTI1_PADDR        0x30089000      /* 4   KiB                                */
-
-/*------------------------------- AIPS-1 memory map ----------------------------------------*/
-#define AIPS1_CFG_PADDR           0x301f0000      /* 64  KiB                                */
-#define GPIO1_PADDR               0x30200000      /* 64  KiB                                */
-#define GPIO2_PADDR               0x30210000      /* 64  KiB                                */
-#define GPIO3_PADDR               0x30220000      /* 64  KiB                                */
-#define GPIO4_PADDR               0x30230000      /* 64  KiB                                */
-#define GPIO5_PADDR               0x30240000      /* 64  KiB                                */
-#define GPIO6_PADDR               0x30250000      /* 64  KiB                                */
-#define GPIO7_PADDR               0x30260000      /* 64  KiB                                */
-#define IOMUXC_LPSR_GPR_PADDR     0x30270000      /* 64  KiB                                */
-#define WDOG1_PADDR               0x30280000      /* 64  KiB                                */
-#define WDOG2_PADDR               0x30290000      /* 64  KiB                                */
-#define WDOG3_PADDR               0x302a0000      /* 64  KiB                                */
-#define WDOG4_PADDR               0x302b0000      /* 64  KiB                                */
-#define IOMUXC_LPSR_PADDR         0x302c0000      /* 64  KiB                                */
-#define GPT1_PADDR                0x302d0000      /* 64  KiB                                */
-#define GPT2_PADDR                0x302e0000      /* 64  KiB                                */
-#define GPT3_PADDR                0x302f0000      /* 64  KiB                                */
-#define GPT4_PADDR                0x30300000      /* 64  KiB                                */
-#define ROMCP_PADDR               0x30310000      /* 64  KiB                                */
-#define KPP_PADDR                 0x30320000      /* 64  KiB                                */
-#define IOMUXC_PADDR              0x30330000      /* 64  KiB                                */
-#define IOMUXC_GPR_PADDR          0x30340000      /* 64  KiB                                */
-#define OCOTP_CTRL_PADDR          0x30350000      /* 64  KiB                                */
-#define ANALOG_PADDR              0x30360000      /* 64  KiB                                */
-#define SNVS_HP_PADDR             0x30370000      /* 64  KiB                                */
-#define CCM_PADDR                 0x30380000      /* 64  KiB                                */
-#define SRC_PADDR                 0x30390000      /* 64  KiB                                */
-#define GPC_PADDR                 0x303a0000      /* 64  KiB                                */
-#define SEMAPHORE1_PADDR          0x303b0000      /* 64  KiB                                */
-#define SEMAPHORE2_PADDR          0x303c0000      /* 64  KiB                                */
-#define RDC_PADDR                 0x303d0000      /* 64  KiB                                */
-#define CSU_PADDR                 0x303e0000      /* 64  KiB                                */
-/*------------------------------- AIPS-2 mem map -------------------------------------------*/
-#define AIPS2_CFG_PADDR           0x305f0000      /* 64  KiB                                */
-#define ADC1_WRAPPER_PADDR        0x30610000      /* 64  KiB                                */
-#define ADC2_WRAPPER_PADDR        0x30620000      /* 64  KiB                                */
-#define ECSPI4_PADDR              0x30630000      /* 64  KiB                                */
-#define FLEX_TIMER1_PADDR         0x30640000      /* 64  KiB                                */
-#define FLEX_TIMER2_PADDR         0x30650000      /* 64  KiB                                */
-#define PWM1_PADDR                0x30660000      /* 64  KiB                                */
-#define PWM2_PADDR                0x30670000      /* 64  KiB                                */
-#define PWM3_PADDR                0x30680000      /* 64  KiB                                */
-#define PWM4_PADDR                0x30690000      /* 64  KiB                                */
-#define SYS_COUNTER_RD_PADDR      0x306a0000      /* 64  KiB system counter read            */
-#define SYS_COUNTER_CMP_PADDR     0x306b0000      /* 64  KiB system counter compare         */
-#define SYS_COUNTER_CTRL_PADDR    0x306c0000      /* 64  KiB system counter control         */
-#define PCIE_PHY_PADDR            0x306d0000      /* 64  KiB                                */
-#define EDPC_PADDR                0x306f0000      /* 64  KiB                                */
-#define PXP_PADDR                 0x30700000      /* 64  KiB                                */
-#define CSI_PADDR                 0x30710000      /* 64  KiB                                */
-#define LCDIF_PADDR               0x30730000      /* 64  KiB                                */
-#define MIPI_CSI_PADDR            0x30750000      /* 64  KiB                                */
-#define MIPI_DSI_PADDR            0x30760000      /* 64  KiB                                */
-#define TZASC_PADDR               0x30780000      /* 64  KiB                                */
-#define DDR_PHY_PADDR             0x30790000      /* 64  KiB                                */
-#define DDRC_PADDR                0x307a0000      /* 64  KiB                                */
-#define PERFMON1_PADDR            0x307c0000      /* 64  KiB                                */
-#define PERFMON2_PADDR            0x307d0000      /* 64  KiB                                */
-#define AXI_DEBUG_MON_PADDR       0x307e0000      /* 64  KiB                                */
-/*------------------------------- AIPS-3 mem map -------------------------------------------*/
-#define ECSPI1_PADDR              0x30820000      /* 64  KiB                                */
-#define ECSPI2_PADDR              0x30830000      /* 64  KiB                                */
-#define ECSPI3_PADDR              0x30840000      /* 64  KiB                                */
-#define UART1_PADDR               0x30860000      /* 64  KiB                                */
-#define UART2_PADDR               0x30890000      /* 64  KiB                                */
-#define UART3_PADDR               0x30880000      /* 64  KiB                                */
-#define SAI1_PADDR                0x308a0000      /* 64  KiB                                */
-#define SAI2_PADDR                0x308b0000      /* 64  KiB                                */
-#define SAI3_PADDR                0x308c0000      /* 64  KiB                                */
-#define SPBA_PADDR                0x308f0000      /* 64  KiB                                */
-#define AIPS3_CAAM_PADDR          0x30900000      /* 256 KiB                                */
-#define AIPS3_CFG_PADDR           0x309f0000      /* 64  KiB                                */
-#define FLEXCAN1_PADDR            0x30a00000      /* 64  KiB                                */
-#define FLEXCAN2_PADDR            0x30a10000      /* 64  KiB                                */
-#define I2C1_PADDR                0x30a20000      /* 64  KiB                                */
-#define I2C2_PADDR                0x30a30000      /* 64  KiB                                */
-#define I2C3_PADDR                0x30a40000      /* 64  KiB                                */
-#define I2C4_PADDR                0x30a50000      /* 64  KiB                                */
-#define UART4_PADDR               0x30a60000      /* 64  KiB                                */
-#define UART5_PADDR               0x30a70000      /* 64  KiB                                */
-#define UART6_PADDR               0x30a80000      /* 64  KiB                                */
-#define UART7_PADDR               0x30a90000      /* 64  KiB                                */
-#define MU_A_PADDR                0x30aa0000      /* 64  KiB                                */
-#define MU_B_PADDR                0x30ab0000      /* 64  KiB                                */
-#define SEMAPHORE_HS_PADDR        0x30ac0000      /* 64  KiB                                */
-#define USB_PL301_PADDR           0x30ad0000      /* 64  KiB                                */
-#define USB1_OTG_PADDR            0x30b10000      /* 64  KiB                                */
-#define USB2_OTG_PADDR            0x30b20000      /* 64  KiB                                */
-#define USB_HOST_PADDR            0x30b30000      /* 64  KiB                                */
-#define USDHC1_PADDR              0x30b40000      /* 64  KiB                                */
-#define USDHC2_PADDR              0x30b50000      /* 64  KiB                                */
-#define USDHC3_PADDR              0x30b60000      /* 64  KiB                                */
-#define SIM1_PADDR                0x30b90000      /* 64  KiB                                */
-#define SIM2_PADDR                0x30ba0000      /* 64  KiB                                */
-#define QSPI_PADDR                0x30bb0000      /* 64  KiB                                */
-#define EIM_EIM_PADDR             0x30bc0000      /* 64  KiB                                */
-#define SDMA_PADDR                0x30bd0000      /* 64  KiB                                */
-#define ENET1_PADDR               0x30be0000      /* 64  KiB                                */
-#define ENET2_PADDR               0x30bf0000      /* 64  KiB                                */
-#define GPV0_PADDR                0x32000000      /* 1   MiB main cfg port                  */
-#define GPV1_PADDR                0x32100000      /* 1   MiB wakeup cfg port                */
-#define GPV2_PADDR                0x32200000      /* 1   MiB per_s cfg port                 */
-#define GPV3_PADDR                0x32300000      /* 1   MiB per_m cfg port                 */
-#define GPV4_PADDR                0x32400000      /* 1   MiB enet cfg port                  */
-#define GPV5_PADDR                0x32500000      /* 1   MiB display cfg port               */
-#define GPV6_PADDR                0x32600000      /* 1   MiB m4 cfg port                    */
-#define GPV7_PADDR                0x32700000      /* 1   MiB reserved                       */
-#define APBH_DMA_PADDR            0x33000000      /* 32  KiB                                */
-#define QSPI1_RX_PADDR            0x34000000      /* 32  MiB  FLASH RX buffer               */
-#define PCIE1_REG_PADDR           0x33800000      /* 16  KiB                                */
-#define APBH_DMA_PADDR            0x33000000      /* 32  KiB                                */
-#define PCIE1_PADDR               0x40000000      /* 256 MiB                                */
-#define QSPI1_PADDR               0x60000000      /* 256 MiB FLASH                          */
-
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/imx7/plat/machine/hardware.h b/include/plat/imx7/plat/machine/hardware.h
index 43fb9dcb4..c2da5c965 100644
--- a/include/plat/imx7/plat/machine/hardware.h
+++ b/include/plat/imx7/plat/machine/hardware.h
@@ -14,39 +14,8 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  GIC distributor and private timers */
-        ARM_MP_PADDR,
-        ARM_MP_PPTR1,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC controller */
-        ARM_MP_PADDR + BIT(PAGE_BITS),
-        ARM_MP_PPTR2,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC controller */
-        ARM_MP_PADDR + BIT(PAGE_BITS) * 2,
-        ARM_MP_PPTR3,
-        true  /* armExecuteNever */
-
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/omap3/plat/machine/devices.h b/include/plat/omap3/plat/machine/devices.h
deleted file mode 100644
index 5412292c1..000000000
--- a/include/plat/omap3/plat/machine/devices.h
+++ /dev/null
@@ -1,142 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-/*
- definitions for memory addresses of omap3 platform
- currently based on the DM3730 chip as used in the beagleboard-xM
- listed in the order of ascending memory address, similar to the datasheet
- the size must all be powers of 2 and page aligned (4k or 1M).
-*/
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PPTR                     0xfff01000
-#define INTC_PPTR                      0xfff02000
-#define GPTIMER9_PPTR                  0xfff03000
-#define ARM_DEBUG_MMAPPING_PPTR        0xfff04000
-
-/* Boot space */
-/* 0x00000000 - 0x40000000 */
-#define GPMC_PADDR                     0x00000000 /* 1GB */
-
-/* FIXME: This is part of beagleboard, not SoC. Need to differentiate. */
-#define ETHERNET_BASE_PADDR            0x2C000000
-
-/* On-chip memory */
-/* 0x40000000 - 0x48000000 */
-#define BOOT_ROM0_PADDR                0x40000000 /* 20 pages */
-#define BOOT_ROM1_PADDR                0x40014000 /* 8 pages */
-#define SRAM_INTERNAL_PADDR            0x40200000 /* 16 pages */
-
-/* L4 core (2 pages each unless specified) */
-/* 0x48000000 - 0x48300000 */
-#define SYSTEM_CONTROL_MODULE_PADDR    0x48002000
-#define CLOCK_MANAGER_PADDR            0x48004000
-#define L4_CORE_CONFIG_PADDR           0x48040000
-#define DISPLAY_SUBSYSTEM_PADDR        0x4804f000
-#define SDMA_PADDR                     0x48056000
-#define I2C3_PADDR                     0x48060000
-#define USBTLL_PADDR                   0x48062000
-#define HS_USB_HOST_PADDR              0x48064000
-#define UART1_PADDR                    0x4806a000
-#define UART2_PADDR                    0x4806c000
-#define I2C1_PADDR                     0x48070000
-#define I2C2_PADDR                     0x48072000
-#define MCBSP1_PADDR                   0x48074000
-#define GPTIMER10_PADDR                0x48086000
-#define GPTIMER11_PADDR                0x48088000
-#define MAILBOX_PADDR                  0x48094000
-#define MCBSP5_PADDR                   0x48096000
-#define MCSPI1_PADDR                   0x48098000
-#define MCSPI2_PADDR                   0x4809a000
-#define MMC_SD_SDIO1_PADDR             0x4809c000
-#define HS_USB_OTG_PADDR               0x480ab000
-#define MMC_SD_SDIO3_PADDR             0x480ad000
-#define HDQ_TM_1WIRE_PADDR             0x480b2000
-#define MMC_SD_SDIO2_PADDR             0x480b4000
-#define ICR_MPU_PORT_PADDR             0x480b6000
-#define MCSPI3_PADDR                   0x480b8000
-#define MCSPI4_PADDR                   0x480ba000
-#define CAMERA_ISP_PADDR               0x480bc000
-#define SR1_PADDR                      0x480c9000
-#define SR2_PADDR                      0x480cb000
-#define ICR_MODEM_PORT_PADDR           0x480cd000
-#define INTC_PADDR                     0x48200000 /* 1 page - see IRQ chapter */
-#define L4_WAKEUP_INTERCONNECT_A_PADDR 0x48300000
-#define CONTROL_MODULE_ID_CODE_PADDR   0x4830a000
-#define L4_WAKEUP_INTERCONNECT_B_PADDR 0x4830c000
-
-/* L4 Wakeup (2 pages each unless specified) */
-/* 0x48300000 - 0x49000000 */
-#define PWR_AND_RST_MANAGER_PADDR      0x48306000
-#define GPIO1_PADDR                    0x48310000
-#define WDT2_PADDR                     0x48314000
-#define GPTIMER1_PADDR                 0x48318000
-#define TIMER32K_PADDR                 0x48320000
-#define L4_WAKEUP_CONFIG_PADDR         0x48328000
-
-/* L4 peripherals (2 pages each) */
-/* 0x49000000 - 0x50000000 */
-#define L4_PER_CONFIG_PADDR            0x49000000
-#define UART3_PADDR                    0x49020000
-#define MCBSP2_PADDR                   0x49022000
-#define MCBSP3_PADDR                   0x49024000
-#define MCBSP4_PADDR                   0x49026000
-#define MCBSP2_SIDETONE_PADDR          0x49028000
-#define MCBSP3_SIDETONE_PADDR          0x4902a000
-#define WDT3_PADDR                     0x49030000
-#define GPTIMER2_PADDR                 0x49032000
-#define GPTIMER3_PADDR                 0x49034000
-#define GPTIMER4_PADDR                 0x49036000
-#define GPTIMER5_PADDR                 0x49038000
-#define GPTIMER6_PADDR                 0x4903a000
-#define GPTIMER7_PADDR                 0x4903c000
-#define GPTIMER8_PADDR                 0x4903e000
-#define GPTIMER9_PADDR                 0x49040000
-#define UART4_PADDR                    0x49042000
-#define GPIO2_PADDR                    0x49050000
-#define GPIO3_PADDR                    0x49052000
-#define GPIO4_PADDR                    0x49054000
-#define GPIO5_PADDR                    0x49056000
-#define GPIO6_PADDR                    0x49058000
-
-/* SGX */
-/* 0x50000000 - 0x54000000 */
-#define SGX_PADDR                      0x50000000 /* 16 pages */
-
-/* L4 emu (2 pages each unless specified) */
-/* 0x54000000 - 0x58000000 */
-#define EMU_TPIU_PADDR                 0x54019000
-#define EMU_ETB_PADDR                  0x5401b000
-#define EMU_DAPCTL_PADDR               0x5401d000
-#define EMU_SDTI_L4_INTERCONNECT_PADDR 0x5401f000
-#define EMU_SDTI_CONFIG_PADDR          0x54500000
-#define EMU_SDTI_WINDOW_PADDR          0x54600000
-#define EMU_PWR_AND_RST_MANAGER_PADDR  0x54706000
-#define EMU_GPIO1_PADDR                0x54710000
-#define EMU_WDT2_PADDR                 0x54714000
-#define EMU_GPTIMER1_PADDR             0x54718000
-#define EMU_32KTIMER_PADDR             0x54720000
-#define EMU_L4_WAKEUP_CONFIG_PADDR     0x54728000
-
-/* IVA 2.2 Subsystem */
-/* 0x5C000000 - 0x60000000 */
-#define IVA_22_PADDR                   0x5C000000 /* 48 MB */
-
-/* Level 3 Interconnect */
-/* 0x68000000 - 0x69000000 */
-#define L3_CONTROL_PADDR               0x68000000 /* 81KB */
-#define L3_SMS_CONFIG                  0x68C00000 /* 16MB */
-#define L3_SDRC_CONFIG                 0x68D00000 /* 16MB */
-#define L3_GPMC_CONFIG                 0x68E00000 /* 16MB */
-
-#endif
diff --git a/include/plat/omap3/plat/machine/hardware.h b/include/plat/omap3/plat/machine/hardware.h
index 7bc466dc9..b9adf8d89 100644
--- a/include/plat/omap3/plat/machine/hardware.h
+++ b/include/plat/omap3/plat/machine/hardware.h
@@ -15,31 +15,7 @@
 #include <linker.h>
 #include <armv/machine.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <plat/machine/interrupt.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  GP Timer 9 */
-        GPTIMER9_PADDR,
-        GPTIMER9_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  INTC */
-        INTC_PADDR,
-        INTC_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART3_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif
-    }
-};
-
 #endif
diff --git a/include/plat/omap3/plat/machine/interrupt.h b/include/plat/omap3/plat/machine/interrupt.h
index 941a77fd8..e8e789950 100644
--- a/include/plat/omap3/plat/machine/interrupt.h
+++ b/include/plat/omap3/plat/machine/interrupt.h
@@ -17,7 +17,6 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
 
 #define INTCPS_SIR_IRQ_SPURIOUSIRQFLAG 0xFF0000
 
diff --git a/include/plat/tk1/plat/machine/devices.h b/include/plat/tk1/plat/machine/devices.h
deleted file mode 100644
index 1a4feae6d..000000000
--- a/include/plat/tk1/plat/machine/devices.h
+++ /dev/null
@@ -1,128 +0,0 @@
-/*
- * Copyright 2016, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UARTA_PPTR                  0xfff01000
-#define UARTB_PPTR                  0xfff01040
-#define UARTC_PPTR                  0xfff01200
-#define UARTD_PPTR                  0xfff01300
-#define GIC_DISTRIBUTOR_PPTR        0xfff03000
-#define GIC_CONTROLLER_PPTR         0xfff04000
-/* HYP mode kernel devices */
-#define GIC_VCPUCTRL_PPTR           0xfff06000
-/* SMMU registers */
-#define SMMU_PPTR                   0Xfff07000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff08000
-
-
-#define UART_PPTR                   UARTD_PPTR
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       GICD_PADDR
-#define GIC_CONTROLLER0_PADDR       GICI_PADDR
-
-#define GIC_PL400_VCPUCTRL_PPTR     GIC_VCPUCTRL_PPTR
-#define GIC_VCPUCTRL_PADDR          (VGICI_REQ_PADDR)
-/*
- * many of the device regions are not 4K page aligned, so some regions may contain more than
- * one devices. it is the user's responsibilty to figure out how to use these regions
- * */
-
-#define ARM_PERIPHBASE              (0x50040000)                /* 128 KB                       */
-#define GICD_PADDR                  (ARM_PERIPHBASE + 0x1000)   /* interrupt distributor        */
-#define GICI_PADDR                  (ARM_PERIPHBASE + 0x2000)   /* GIC CPU interface            */
-#define VGICI_REQ_PADDR             (ARM_PERIPHBASE + 0x4000)   /* hyp view for requesting CPU  */
-#define VGICI_ALL_PADDR             (ARM_PERIPHBASE + 0x5000)   /* hyp view for all CPUs        */
-#define VGICI_VM_PADDR              (ARM_PERIPHBASE + 0x6000)   /* hyp view for VM view         */
-#define PCIE_0_CFG_PADDR            (0x01000000)                /* PCIE lane 0 config register  */
-#define PCIE_1_CFG_PADDR            (0x01001000)                /* PCIE lane 1 config register  */
-#define PCIE_PCA0_1_PADDR           (0x01002000)                /* PCA 0  and 1                 */
-#define PCIE_PADS_AFI_PADDR         (0x01003000)                /* Pads and AFI                 */
-#define PCIE_A1_PADDR               (0x01000000)                /* 16 MB                        */
-#define PCIE_A2_PADDR               (0x02000000)                /* 224 MB                       */
-#define PCIE_A3_PADDR               (0x10000000)                /* 763 MB                     */
-#define R8169_NIC_PADDR             (0x13000000)                /* r8169 NIC 1 MB               */
-#define GRAPH_HOST_REGS_PADDR       (0x50000000)                /* 208 KB                       */
-#define GRAPH_HOST_PADDR            (0x54000000)                /* 16 MB                        */
-#define GPU_PADDR                   (0x57000000)                /* 144 MB                       */
-#define UP_TAG_PADDR                (0x60000000)                /* 4 KB                         */
-#define RSEM_PADDR                  (0x60001000)                /* 4 KB                         */
-#define ASEM_PADDR                  (0x60002000)                /* 4 KB                         */
-#define ARB_PRI_PADDR               (0x60003000)                /* 4 KB                         */
-#define ICTLR_PADDR                 (0x60004000)                /* 4 KB, includes several       */
-#define TMR_PADDR                   (0x60005000)                /* 4 Kb,  1 KB                  */
-#define CLK_RESET_PADDR             (0x60006000)                /* 4 KB                         */
-#define FLOW_CTRL_PADDR             (0x60007000)                /* 4 KB                         */
-#define AHB_DMA_PADDR               (0x60008000)                /* 8 KB                         */
-#define AHB_DMA_CH_PADDR            (0x60009000)                /* 4 KB 4 channels, 32 bytes    */
-#define APB_DMA_PADDR               (0x60020000)                /* 16 KB                        */
-#define APB_DMA_CH_PADDR            (0x60021000)                /* 4KB 32 channels, 64 bytes    */
-#define SYS_REGS_PADDR              (0x6000c000)                /* 768 bytes + 2 KB             */
-#define GPIO_PADDR                  (0x6000d000)                /* 8 GPIOs, 265 bytes each      */
-#define VCP_PADDR                   (0x6000e000)                /* 4 KB                         */
-#define VPUCQ_PADDR                 (0x60010000)                /* 256 Bytes                    */
-#define BSEA_PADDR                  (0x60011000)                /* 4 KB                         */
-#define IPATCH_PADDR                (0x6001d000)                /* 4 KB offset 0xc00, 1 KB      */
-#define VDE_FRAMEID_PADDR           (0x60030000)                /* 16 KB, multiple              */
-#define MISC_AUX_PADDR              (0x70000000)                /* 12 KB: USB AUX, SATA AUX, etc*/
-#define MISC_PINMUX_PADDR           (0x70003000)                /* 4 KB                         */
-#define UARTA_SYNC_PADDR            (0x70006000)                /* 12 KB, multiple              */
-#define SYNC_NOR_PADDR              (0x70009000)                /* 4 KB                         */
-#define PWM_PADDR                   (0x7000a000)                /* 4 KB, 256 bytes              */
-#define MIPIHSI_PADDR               (0x7000b000)                /* 4 KB                         */
-#define I2C_I2C4_PADDR              (0x7000c000)                /* 4 KB                         */
-#define I2C5_SPI2B_6_PADDR          (0x7000d000)                /* 4 KB                         */
-#define RTC_KFUSE_PADDR             (0x7000e000)                /* 4 KB                         */
-#define FUSE_KFUSE_PADDR            (0x7000f000)                /* 4 KB                         */
-#define LA_PADDR                    (0x70010000)                /* 8 KB                         */
-#define SE_PADDR                    (0x70012000)                /* 8 KB                         */
-#define TSENSOR_PADDR               (0x70014000)                /* 4 KB                         */
-#define CEC_PADDR                   (0x70015000)                /* 4 KB                         */
-#define ATOMICS_PADDR               (0x70016000)                /* 8 KB                         */
-#define MC_PADDR                    (0x70019000)                /* 4 KB                         */
-#define EMC_PADDR                   (0x7001b000)                /* 4 KB                         */
-#define SATA_PADDR                  (0x70020000)                /* 64 KB                        */
-#define HDA_PADDR                   (0x70030000)                /* 64 KB                        */
-#define MIOBFM_PADDR                (0x70200000)                /* 64 KB                        */
-#define AUDIO_PADDR                 (0x70300000)                /* 64 KB                        */
-#define XUSB_HOST_PADDR             (0x70090000)                /* 36 KB                        */
-#define XUSB_PADCTL_PADDR           (0x7009f000)                /* 4  KB                        */
-#define XUSB_DEV_PADDR              (0x700d0000)                /* 40 KB                        */
-#define DDS_PADDR                   (0x700a0000)                /* 8KB 4608 bytes               */
-#define SDMMC_1_PADDR               (0x700b0000)                /* 4KB 512 bytes                */
-#define SDMMC_1B_4_PADDR            (0x700b1000)                /* 60KB 512 bytes    each       */
-#define SPEEDO_PADDR                (0x700c0000)                /* 32 KB                        */
-#define SPEEDO_PMON_PADDR           (0x700c8000)                /* 32 KB                        */
-#define SYSCTR0_PADDR               (0x700f0000)                /* 64 KB                        */
-#define SYSCTR1_PADDR               (0x70100000)                /* 64 KB                        */
-#define DP2_PADDR                   (0x700e0000)                /* 256 Bytes                    */
-#define APB2JTAG_PADDR              (0x700e1000)                /* 512 Bytes                    */
-#define SOC_THERM_PADDR             (0x700e2000)                /* 4 KB                         */
-#define MIPI_CAL_PADDR              (0x700e3000)                /* 265 Bytes                    */
-#define DVFS_PADDR                  (0x70110000)                /* 1 KB                         */
-#define CLUSTER_CLK_PADDR           (0x70040000)                /* 256 KB                       */
-#define CSITE_PADDR                 (0x70800000)                /* 2 MB                         */
-#define PPCS_PADDR                  (0x7c000000)                /* 64 KB                        */
-#define TZRAM_PADDR                 (0x7c010000)                /* 64 KB                        */
-#define USB_PADDR                   (0x7d000000)                /* 8 KB region, 6 KB            */
-#define USB2_PADDR                  (0x7d004000)                /* 8 KB region, 6 KB            */
-#define USB3_PADDR                  (0x7d008000)                /* 8 KB region, 6 KB            */
-#define UARTA_PADDR                 (0x70006000)
-
-/* Additional memory outside the kernel window that we export as a device */
-#define TK1_EXTRA_RAM_START    0xb0000000
-#define TK1_EXTRA_RAM_SIZE     0x40000000
-
-#endif
diff --git a/include/plat/tk1/plat/machine/hardware.h b/include/plat/tk1/plat/machine/hardware.h
index 52d3c37e1..e1c91a1b4 100644
--- a/include/plat/tk1/plat/machine/hardware.h
+++ b/include/plat/tk1/plat/machine/hardware.h
@@ -17,7 +17,6 @@
 #include <linker.h>
 #include <arch/object/vcpu.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <plat/machine/hardware_gen.h>
 #include <plat/machine/smmu.h>
@@ -25,43 +24,6 @@
 #include <mode/api/constants.h>
 #include <arch/benchmark_overflowHandler.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /* map kernel device: GIC */
-        GIC_CONTROLLER0_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-    },
-    {
-        GIC_VCPUCTRL_PADDR,
-        GIC_VCPUCTRL_PPTR,
-        false
-#endif /* CONFIG_ARM_HYPERVISOR */
-#ifdef CONFIG_ARM_SMMU
-    },
-    {
-        MC_PADDR,
-        SMMU_PPTR,
-        false
-#endif /* CONFIG_ARM_SMMU */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /* UART */
-        UARTA_PADDR,
-        UARTA_PPTR,
-        true
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/tx1/plat/machine/devices.h b/include/plat/tx1/plat/machine/devices.h
deleted file mode 100644
index 4e0ea3967..000000000
--- a/include/plat/tx1/plat/machine/devices.h
+++ /dev/null
@@ -1,117 +0,0 @@
-/*
- * 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_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <config.h>
-
-/* These devices are used by the seL4 kernel. */
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-#define KDEV_PPTR                   0x0000ffffffff0000lu
-#else
-#define KDEV_PPTR                   0xffffffffffff0000lu
-#endif
-
-#define UART_PPTR                  (KDEV_PPTR)
-#define GIC_DISTRIBUTOR_PPTR        (KDEV_PPTR + 0x3000)
-#define GIC_CONTROLLER_PPTR         (KDEV_PPTR + 0x4000)
-#define GICH_PPTR                   (KDEV_PPTR + 0x6000)
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       GICD_PADDR
-#define GIC_CONTROLLER_PADDR        GICI_PADDR
-
-#define GIC_PL400_VCPUCTRL_PPTR     GICH_PPTR
-
-
-/* many of the device regions are not 4K page aligned, so some regions may contain more than
- * one devices. it is the user's responsibilty to figure out how to use these regions */
-#define PCIE_A1_PADDR               (0x01000000)                /* 16 MB                      */
-#define PCIE_A2_PADDR               (0x02000000)                /* 480 MB                     */
-#define PCIE_A3_PADDR               (0x20000000)                /* 512 MB                     */
-#define IRAM_A_PADDR                (0x40000000)                /* 64 KB                      */
-#define IRAM_B_PADDR                (0x40010000)                /* 64 KB                      */
-#define IRAM_C_PADDR                (0x40020000)                /* 64 KB                      */
-#define IRAM_D_PADDR                (0x40030000)                /* 64 KB                      */
-#define HOST1X_PADDR                (0x50000000)                /* 256 KB                     */
-#define ARM_PERIPHBASE              (0x50040000)                /* 128 KB                     */
-#define GICD_PADDR                  (ARM_PERIPHBASE + 0x1000)   /* interrupt distributor      */
-#define GICI_PADDR                  (ARM_PERIPHBASE + 0x2000)   /* GIC CPU interface          */
-#define GICH_PADDR                  (ARM_PERIPHBASE + 0x4000)   /* GIC hyp-view register      */
-#define GICV_PADDR                  (ARM_PERIPHBASE + 0x6000)   /* GIC VCPU register          */
-#define MSELECT_PADDR               (0x50060000)                /* 4KB                        */
-#define GRAPHICS_HOST_PADDR         (0x54000000)                /* 16 MB                      */
-#define GPU_PADDR                   (0x57000000)                /* 144 MB                     */
-#define UP_TAG_PADDR                (0x60000000)                /* 4 KB uP-TAG                */
-#define RES_SEM_PADDR               (0x60001000)                /* 4 KB resource semaphore    */
-#define ARB_SEM_PADDR               (0x60002000)                /* 4 KB arbitration semaphore */
-#define ARB_PRI_PADDR               (0x60003000)                /* 4 KB                       */
-#define ICTLR_PADDR                 (0x60004000)
-#define TMR_PADDR                   (0x60005000)                /* 4 KB                       */
-#define CLK_RESET_PADDR             (0x60006000)                /* Clock and Reset            */
-#define FLOW_CTL_PADDR              (0x60007000)                /* Flow Controller            */
-#define APB_DMA_PADDR               (0x60020000)                /* 16 KB                      */
-#define SYS_REG_PADDR               (0x6000c000)                /* System Registers           */
-#define GPIO_PADDR                  (0x6000d000)                /* GPIO-1 to GPIO-8           */
-#define UARTA_SYNC_PADDR            (0x70006000)                /* 12 KB, multiple            */
-#define UARTA_PADDR                 (0x70006000)
-#define I2C1_4_PADDR                (0x7000c000)                /* I2C 1 to 4                */
-#define I2C5_6_SPI2B1_4_PADDR       (0x7000d000)                /* I2C 5 to 6, SPI2B 1 to 4  */
-#define RTC_PMC_PADDR               (0x7000e000)                /* RTC and PMC               */
-#define MISC_PADDR                  (0x70000000)                /* MISC 12 KB                */
-#define PINMUX_AUX_PADDR            (0x70003000)
-#define FUSE_KFUSE_PADDR            (0x7000f000)                /* FUSE and KFUSE            */
-#define SE_PADDR                    (0x70012000)                /* 8 KB                      */
-#define TSENSOR_PADDR               (0x70014000)
-#define CEC_PADDR                   (0x70015000)
-#define ATOMICS_PADDR               (0x70016000)                /* 8 KB                      */
-#define MC_PADDR                    (0x70019000)
-#define EMC_PADDR                   (0x7001b000)
-#define MC0_PADDR                   (0x7001c000)
-#define MC1_PADDR                   (0x7001d000)
-#define EMC0_PADDR                  (0x7001e000)
-#define EMC1_PADDR                  (0x7001f000)
-#define SATA_PADDR                  (0x70020000)                /* 64 KB                      */
-#define HDA_PADDR                   (0x70030000)                /* 64 KB                      */
-#define APE_PADDR                   (0x702c0000)                /* 256 KB                     */
-#define XUSB_PADCTL_PADDR           (0x7009f000)
-#define XUSB_HOST_PADDR             (0x70090000)                /* 40 KB                      */
-#define SDMMC1_4_PADDR              (0x700b0000)
-#define SDMMC1B_PADDR               (0x700b1000)
-#define SDMMC2B_PADDR               (0x700b2000)
-#define SDMMC3B_PADDR               (0x700b3000)
-#define SDMMC4B_PADDR               (0x700b4000)
-#define XUSB_DEV_PADDR              (0x700d0000)                /* 40 KB                      */
-#define DDS_PADDR                   (0x700a0000)                /* 8 KB                       */
-#define SPEEDO_PADDR                (0x700c0000)                /* 32 KB                      */
-#define SPEEDO_PMON_PADDR           (0x700c8000)                /* 32 KB                      */
-#define SYSCTR0_PADDR               (0x700f0000)                /* 64 KB                      */
-#define SYSCTR1_PADDR               (0x70100000)                /* 64 KB                      */
-#define DP2_PADDR                   (0x700e0000)
-#define APB2JTAG_PADDR              (0x700e1000)
-#define SOC_THERM_PADDR             (0x700e2000)
-#define MIPI_CAL_PADDR              (0x700e3000)
-#define DVFS_PADDR                  (0x70110000)
-#define CLUSTER_CLK_PADDR           (0x70040000)                /* 256 KB                      */
-#define QSPI_PADDR                  (0x70410000)
-#define STM_PADDR                   (0x71000000)                /* 16 MB                       */
-#define CSITE_PADDR                 (0x72000000)                /* 32 MB                       */
-#define AHB_A1_PADDR                (0x78000000)                /* 16 MB                       */
-#define PPCS_PADDR                  (0x7c000000)                /* AHB ot MC flush 64 KB       */
-#define TZRAM_PADDR                 (0x7c010000)                /* 64 KB                       */
-#define USB_PADDR                   (0x7d000000)                /* 6 KB round up to 8 KB       */
-#define USB2_PADDR                  (0x7d004000)                /* 6 KB round up to 8 KB       */
-
-#endif /* __PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/tx1/plat/machine/hardware.h b/include/plat/tx1/plat/machine/hardware.h
index d62905b28..25cc839d3 100644
--- a/include/plat/tx1/plat/machine/hardware.h
+++ b/include/plat/tx1/plat/machine/hardware.h
@@ -18,38 +18,8 @@
 #include <linker.h>
 #include <arch/object/vcpu.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /* map kernel device: GIC */
-        GIC_CONTROLLER_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /* UART */
-        UARTA_PADDR,
-        UART_PPTR,
-        true
-#endif /* CONFIG_PRINTING */
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-    },
-    {
-        GICH_PADDR,
-        GICH_PPTR,
-        true
-#endif
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/tx2/plat/machine/devices.h b/include/plat/tx2/plat/machine/devices.h
deleted file mode 100644
index 8c7becf38..000000000
--- a/include/plat/tx2/plat/machine/devices.h
+++ /dev/null
@@ -1,66 +0,0 @@
-/*
- * Copyright 2018, 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_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <config.h>
-
-/* These devices are used by the seL4 kernel. */
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-#define KDEV_PPTR                   0x0000ffffffff0000ull
-#else
-#define KDEV_PPTR                   0xffffffffffff0000lu
-#endif
-
-#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER
-/* Since the AArch64 memory layout leaves a massive (approx) 1GiB hole between
- * the end of PPTR_TOP and the start of KDEV_PPTR, we can just backtrack from
- * KDEV_PPTR to the first 2MiB aligned virtual address and use that as the
- * kernel log vaddr. Basically we backtrack 4MiB from KDEV_PPTR and then force
- * align that address to be 2MiB aligned.
- *
- * This is defined as a platform-specific address so that it can reference
- * KDEV_PPTR (defined above) without having to pollute the arch-specific header
- * (arch/64/mode/hardware.h).
- */
-#define KS_LOG_PPTR ((KDEV_PPTR & ~(0x200000 - 1)) - 0x200000)
-compile_assert(log_buffer_vaddr_2MiB_aligned, (KS_LOG_PPTR & (0x200000 - 1)) == 0)
-#endif
-
-
-#define UART_PPTR                  (KDEV_PPTR)
-#define GIC_DISTRIBUTOR_PPTR        (KDEV_PPTR + 0x3000)
-#define GIC_CONTROLLER_PPTR         (KDEV_PPTR + 0x4000)
-#define GICH_PPTR                   (KDEV_PPTR + 0x6000)
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-#define GIC_DISTRIBUTOR_PADDR       GICD_PADDR
-#define GIC_CONTROLLER_PADDR        GICI_PADDR
-
-#define GIC_PL400_VCPUCTRL_PPTR     GICH_PPTR
-
-
-/*
- * This is a subset of the address map.
- */
-#define ARM_PERIPHBASE              (0x03880000)
-#define ARM_PERIPHBASE_END          (0x038affff)
-#define ARM_PERIPHBASE_SIZE         ((ARM_PERIPHBASE_END+1) - ARM_PERIPHBASE) 	    /* 192KiB */
-#define GICD_PADDR                  (ARM_PERIPHBASE + 0x1000)   /* interrupt distributor      */
-#define GICI_PADDR                  (ARM_PERIPHBASE + 0x2000)   /* GIC CPU interface          */
-#define GICH_PADDR                  (ARM_PERIPHBASE + 0x4000)   /* GIC hyp-view register      */
-#define GICV_PADDR                  (ARM_PERIPHBASE + 0x6000)   /* GIC VCPU register          */
-#define UARTA_PADDR                 (0x03100000)
-#endif /* __PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/tx2/plat/machine/hardware.h b/include/plat/tx2/plat/machine/hardware.h
index b9f9d9e45..f472598cc 100644
--- a/include/plat/tx2/plat/machine/hardware.h
+++ b/include/plat/tx2/plat/machine/hardware.h
@@ -18,38 +18,8 @@
 #include <linker.h>
 #include <arch/object/vcpu.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /* map kernel device: GIC */
-        GIC_CONTROLLER_PADDR,
-        GIC_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        GIC_DISTRIBUTOR_PADDR,
-        GIC_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /* UART */
-        UARTA_PADDR,
-        UART_PPTR,
-        true
-#endif /* CONFIG_PRINTING */
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-    },
-    {
-        GICH_PADDR,
-        GICH_PPTR,
-        true
-#endif
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/zynq7000/plat/machine/devices.h b/include/plat/zynq7000/plat/machine/devices.h
deleted file mode 100644
index 64f653024..000000000
--- a/include/plat/zynq7000/plat/machine/devices.h
+++ /dev/null
@@ -1,92 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * 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(GD_GPL)
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-/* These devices are used by the seL4 kernel. */
-#define UART_PADDR                  UART1_PADDR
-
-#define UART_PPTR                   0xfff01000
-#define L2CC_PL310_PPTR             0xfff02000
-#define ARM_MP_PPTR1                0xfff03000
-#define ARM_MP_PPTR2                0xfff04000
-#define ARM_DEBUG_MMAPPING_PPTR     0xfff05000
-
-#define L2CC_L2C310_PPTR            (L2CC_PL310_PPTR      )
-#define ARM_MP_PRIV_TIMER_PPTR      (ARM_MP_PPTR1 + 0x600 )
-#define ARM_MP_GLOBAL_TIMER_PPTR    (ARM_MP_PPTR1 + 0x200 )
-#define GIC_PL390_CONTROLLER_PPTR   (ARM_MP_PPTR1 + 0x100 )
-#define GIC_PL390_DISTRIBUTOR_PPTR  (ARM_MP_PPTR2         )
-
-
-#define PL_M_AXI_GP0_PADDR         0x40000000
-#define PL_M_AXI_GP1_PADDR         0x80000000
-#define UART0_PADDR                0xE0000000
-#define UART1_PADDR                0xE0001000
-#define USB0_PADDR                 0xE0002000
-#define USB1_PADDR                 0xE0003000
-#define I2C0_PADDR                 0xE0004000
-#define I2C1_PADDR                 0xE0005000
-#define SPI0_PADDR                 0xE0006000
-#define SPI1_PADDR                 0xE0007000
-#define CAN0_PADDR                 0xE0008000
-#define CAN1_PADDR                 0xE0009000
-#define GPIO_PADDR                 0xE000A000
-#define ETH0_PADDR                 0xE000B000
-#define ETH1_PADDR                 0xE000C000
-#define QSPI_PADDR                 0xE000D000
-#define SMC_PADDR                  0xE000E000
-#define SDIO0_PADDR                0xE0100000
-#define SDIO1_PADDR                0xE0101000
-#define SMC_NAND_PADDR             0xE1000000
-#define SMC_NOR0_PADDR             0xE2000000
-#define SMC_NOR1_PADDR             0xE4000000
-#define SMC_SLCR_PADDR             0xF8000000
-#define TRPL_TIMER0_PADDR          0xF8001000
-#define TRPL_TIMER1_PADDR          0xF8002000
-#define DMAC_S_PADDR               0xF8003000
-#define DMAC_NS_PADDR              0xF8004000
-#define SWDT_PADDR                 0xF8005000
-#define DDRC_PADDR                 0xF8006000
-#define DEVCFG_PADDR               0xF8007000
-#define AXI_HP0_PADDR              0xF8008000
-#define AXI_HP1_PADDR              0xF8009000
-#define AXI_HP2_PADDR              0xF800A000
-#define AXI_HP3_PADDR              0xF800B000
-#define OCM_PADDR                  0xF800C000
-#define EFUSE_PADDR                0xF800D000
-#define DEBUG_DAP_ROM_PADDR        0xF8800000
-#define DEBUG_ETB_PADDR            0xF8801000
-#define DEBUG_CTI_ETB_TPIU_PADDR   0xF8802000
-#define DEBUG_TPIU_PADDR           0xF8803000
-#define DEBUG_FUNNEL_PADDR         0xF8804000
-#define DEBUG_ITM_PADDR            0xF8805000
-#define DEBUG_CTI_FTM_PADDR        0xF8809000
-#define DEBUG_FTM_PADDR            0xF880B000
-#define DEBUG_CPU_PMU0_PADDR       0xF8891000
-#define DEBUG_CPU_PMU1_PADDR       0xF8893000
-#define DEBUG_CPU_CTI0_PADDR       0xF8898000
-#define DEBUG_CPU_CTI1_PADDR       0xF8899000
-#define DEBUG_CPU_PTM0_PADDR       0xF889C000
-#define DEBUG_CPU_PTM1_PADDR       0xF889D000
-#define GPV_TRUSTZONE_PADDR        0xF8900000
-#define GPV_QOS301_CPU_PADDR       0xF8946000
-#define GPV_QOS301_DMAC_PADDR      0xF8947000
-#define GPV_QOS301_IOU_PADDR       0xF8948000
-#define MPCORE_PRIV_PADDR          0xF8F00000
-#define GIC_DIST_PADDR             0xF8F01000
-#define L2CC_PL310_PADDR           0xF8F02000
-#define QSPI_LINEAR_PADDR          0xFC000000
-#define OCM_HIGH_PADDR             0xFFFC0000
-
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
-
diff --git a/include/plat/zynq7000/plat/machine/hardware.h b/include/plat/zynq7000/plat/machine/hardware.h
index 3fdedef84..821274dc8 100644
--- a/include/plat/zynq7000/plat/machine/hardware.h
+++ b/include/plat/zynq7000/plat/machine/hardware.h
@@ -15,39 +15,9 @@
 #include <basic_types.h>
 #include <linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <arch/benchmark_overflowHandler.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /*  GIC controller and private timers */
-        MPCORE_PRIV_PADDR,
-        ARM_MP_PPTR1,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  GIC distributor */
-        MPCORE_PRIV_PADDR + BIT(PAGE_BITS),
-        ARM_MP_PPTR2,
-        true  /* armExecuteNever */
-    },
-    {
-        /*  L2CC */
-        L2CC_PL310_PADDR,
-        L2CC_PL310_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/include/plat/zynqmp/plat/machine.h b/include/plat/zynqmp/plat/machine.h
index 9ac70dc73..862e2fe2f 100644
--- a/include/plat/zynqmp/plat/machine.h
+++ b/include/plat/zynqmp/plat/machine.h
@@ -19,7 +19,6 @@
 
 #ifndef __PLAT_MACHINE_H
 #define __PLAT_MACHINE_H
-#include <plat/machine/devices.h>
 #include <machine/io.h>
 
 enum IRQConstants {
diff --git a/include/plat/zynqmp/plat/machine/devices.h b/include/plat/zynqmp/plat/machine/devices.h
deleted file mode 100644
index 845e6b4bd..000000000
--- a/include/plat/zynqmp/plat/machine/devices.h
+++ /dev/null
@@ -1,216 +0,0 @@
-/*
- * Copyright 2017, DornerWorks
- * 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_DORNERWORKS_GPL)
- */
-/*
- *
- * This data was produced by DornerWorks, Ltd. of Grand Rapids, MI, USA under
- * a DARPA SBIR, Contract Number D16PC00107.
- *
- * Approved for Public Release, Distribution Unlimited.
- */
-
-#ifndef __PLAT_MACHINE_DEVICES_H
-#define __PLAT_MACHINE_DEVICES_H
-
-#include <config.h>
-#include <plat_mode/machine/devices.h>
-
-#define GIC_PL390_CONTROLLER_PPTR   GIC_CONTROLLER_PPTR
-#define GIC_PL390_DISTRIBUTOR_PPTR  GIC_DISTRIBUTOR_PPTR
-
-/* These devices are used by the seL4 kernel. */
-#ifdef CONFIG_PLAT_ZYNQMP_ULTRA96
-#define UART_PADDR                  UART1_PADDR
-#else
-#define UART_PADDR                  UART0_PADDR
-#endif
-
-#define ACPU_GIC_PADDR              0xF9000000
-#define ACPU_GIC_DISTRIBUTOR_PADDR  0xF9010000
-#define ACPU_GIC_CONTROLLER_PADDR   0xF9020000
-#define AMS_CTRL_PADDR              0xFFA50000
-#define AMS_PL_SYSMON_PADDR         0xFFA50C00
-#define AMS_PS_SYSMON_PADDR         0xFFA50800
-#define APM_CCI_INTC_PADDR          0xFD490000
-#define APM_DDR_PADDR               0xFD0B0000
-#define APM_INTC_OCM_PADDR          0xFFA00000
-#define APM_LPD_FPD_PADDR           0xFFA10000
-#define APU_PADDR                   0xFD5C0000
-#define AXIPCIE_DMA0_PADDR          0xFD0F0000
-#define AXIPCIE_DMA1_PADDR          0xFD0F0080
-#define AXIPCIE_DMA2_PADDR          0xFD0F0100
-#define AXIPCIE_DMA3_PADDR          0xFD0F0180
-#define AXIPCIE_EGRESS0_PADDR       0xFD0E0C00
-#define AXIPCIE_EGRESS1_PADDR       0xFD0E0C20
-#define AXIPCIE_EGRESS2_PADDR       0xFD0E0C40
-#define AXIPCIE_EGRESS3_PADDR       0xFD0E0C60
-#define AXIPCIE_EGRESS4_PADDR       0xFD0E0C80
-#define AXIPCIE_EGRESS5_PADDR       0xFD0E0CA0
-#define AXIPCIE_EGRESS6_PADDR       0xFD0E0CC0
-#define AXIPCIE_EGRESS7_PADDR       0xFD0E0CE0
-#define AXIPCIE_INGRESS0_PADDR      0xFD0E0800
-#define AXIPCIE_INGRESS1_PADDR      0xFD0E0820
-#define AXIPCIE_INGRESS2_PADDR      0xFD0E0840
-#define AXIPCIE_INGRESS3_PADDR      0xFD0E0860
-#define AXIPCIE_INGRESS4_PADDR      0xFD0E0880
-#define AXIPCIE_INGRESS5_PADDR      0xFD0E08A0
-#define AXIPCIE_INGRESS6_PADDR      0xFD0E08C0
-#define AXIPCIE_INGRESS7_PADDR      0xFD0E08E0
-#define AXIPCIE_MAIN_PADDR          0xFD0E0000
-#define BBRAM_PADDR                 0xFFCD0000
-#define CAN0_PADDR                  0xFF060000
-#define CAN1_PADDR                  0xFF070000
-#define CCI_GPV_PADDR               0xFD6E0000
-#define CCI_REG_PADDR               0xFD5E0000
-#define CORESIGHT_A53_CTI_0_PADDR   0xFEC20000
-#define CORESIGHT_A53_CTI_1_PADDR   0xFED20000
-#define CORESIGHT_A53_CTI_2_PADDR   0xFEE20000
-#define CORESIGHT_A53_CTI_3_PADDR   0xFEF20000
-#define CORESIGHT_A53_DBG_0_PADDR   0xFEC10000
-#define CORESIGHT_A53_DBG_1_PADDR   0xFED10000
-#define CORESIGHT_A53_DBG_2_PADDR   0xFEE10000
-#define CORESIGHT_A53_DBG_3_PADDR   0xFEF10000
-#define CORESIGHT_A53_ETM_0_PADDR   0xFEC40000
-#define CORESIGHT_A53_ETM_1_PADDR   0xFED40000
-#define CORESIGHT_A53_ETM_2_PADDR   0xFEE40000
-#define CORESIGHT_A53_ETM_3_PADDR   0xFEF40000
-#define CORESIGHT_A53_PMU_0_PADDR   0xFEC30000
-#define CORESIGHT_A53_PMU_1_PADDR   0xFED30000
-#define CORESIGHT_A53_PMU_2_PADDR   0xFEE30000
-#define CORESIGHT_A53_PMU_3_PADDR   0xFEF30000
-#define CORESIGHT_A53_ROM_PADDR     0xFEC00000
-#define CORESIGHT_R5_CTI_0_PADDR    0xFEBF8000
-#define CORESIGHT_R5_CTI_1_PADDR    0xFEBF9000
-#define CORESIGHT_R5_DBG_0_PADDR    0xFEBF0000
-#define CORESIGHT_R5_DBG_1_PADDR    0xFEBF2000
-#define CORESIGHT_R5_ETM_0_PADDR    0xFEBFC000
-#define CORESIGHT_R5_ETM_1_PADDR    0xFEBFD000
-#define CORESIGHT_R5_ROM_PADDR      0xFEBE0000
-#define CORESIGHT_SOC_CTI_0_PADDR   0xFE990000
-#define CORESIGHT_SOC_CTI_1_PADDR   0xFE9A0000
-#define CORESIGHT_SOC_CTI_2_PADDR   0xFE9B0000
-#define CORESIGHT_SOC_ETF_1_PADDR   0xFE940000
-#define CORESIGHT_SOC_ETF_2_PADDR   0xFE950000
-#define CORESIGHT_SOC_ETR_PADDR     0xFE970000
-#define CORESIGHT_SOC_FTM_PADDR     0xFE9D0000
-#define CORESIGHT_SOC_FUNN_0_PADDR  0xFE910000
-#define CORESIGHT_SOC_FUNN_1_PADDR  0xFE920000
-#define CORESIGHT_SOC_FUNN_2_PADDR  0xFE930000
-#define CORESIGHT_SOC_REPLIC_PADDR  0xFE960000
-#define CORESIGHT_SOC_ROM_PADDR     0xFE800000
-#define CORESIGHT_SOC_STM_PADDR     0xFE9C0000
-#define CORESIGHT_SOC_TPIU_PADDR    0xFE980000
-#define CORESIGHT_SOC_TSGEN_PADDR   0xFE900000
-#define CRF_APB_PADDR               0xFD1A0000
-#define CRL_APB_PADDR               0xFF5E0000
-#define CSU_PADDR                   0xFFCA0000
-#define CSUDMA_PADDR                0xFFC80000
-#define CSU_WDT_PADDR               0xFFCB0000
-#define DDRC_PADDR                  0xFD070000
-#define DDR_PHY_PADDR               0xFD080000
-#define DDR_QOS_CTRL_PADDR          0xFD090000
-#define DDR_XMPU0_CFG_PADDR         0xFD000000
-#define DDR_XMPU1_CFG_PADDR         0xFD010000
-#define DDR_XMPU2_CFG_PADDR         0xFD020000
-#define DDR_XMPU3_CFG_PADDR         0xFD030000
-#define DDR_XMPU4_CFG_PADDR         0xFD040000
-#define DDR_XMPU5_CFG_PADDR         0xFD050000
-#define DP_PADDR                    0xFD4A0000
-#define DPDMA_PADDR                 0xFD4C0000
-#define EFUSE_PADDR                 0xFFCC0000
-#define FPD_DMA_CH0_PADDR           0xFD500000
-#define FPD_DMA_CH1_PADDR           0xFD510000
-#define FPD_DMA_CH2_PADDR           0xFD520000
-#define FPD_DMA_CH3_PADDR           0xFD530000
-#define FPD_DMA_CH4_PADDR           0xFD540000
-#define FPD_DMA_CH5_PADDR           0xFD550000
-#define FPD_DMA_CH6_PADDR           0xFD560000
-#define FPD_DMA_CH7_PADDR           0xFD570000
-#define FPD_GPV_PADDR               0xFD700000
-#define FPD_SLCR_PADDR              0xFD610000
-#define FPD_SLCR_SECURE_PADDR       0xFD690000
-#define FPD_XMPU_CFG_PADDR          0xFD5D0000
-#define FPD_XMPU_SINK_PADDR         0xFD4F0000
-#define GEM0_PADDR                  0xFF0B0000
-#define GEM1_PADDR                  0xFF0C0000
-#define GEM2_PADDR                  0xFF0D0000
-#define GEM3_PADDR                  0xFF0E0000
-#define GPIO_PADDR                  0xFF0A0000
-#define GPU_PADDR                   0xFD4B0000
-#define I2C0_PADDR                  0xFF020000
-#define I2C1_PADDR                  0xFF030000
-#define IOU_GPV_PADDR               0xFE000000
-#define IOU_SCNTR_PADDR             0xFF250000
-#define IOU_SCNTRS_PADDR            0xFF260000
-#define IOU_SECURE_SLCR_PADDR       0xFF240000
-#define IOU_SLCR_PADDR              0xFF180000
-#define IPI_PADDR                   0xFF300000
-#define LPD_DMA_CH0_PADDR           0xFFA80000
-#define LPD_DMA_CH1_PADDR           0xFFA90000
-#define LPD_DMA_CH2_PADDR           0xFFAA0000
-#define LPD_DMA_CH3_PADDR           0xFFAB0000
-#define LPD_DMA_CH4_PADDR           0xFFAC0000
-#define LPD_DMA_CH5_PADDR           0xFFAD0000
-#define LPD_DMA_CH6_PADDR           0xFFAE0000
-#define LPD_DMA_CH7_PADDR           0xFFAF0000
-#define LPD_GPV_PADDR               0xFE100000
-#define LPD_SLCR_PADDR              0xFF410000
-#define LPD_SLCR_SECURE_PADDR       0xFF4B0000
-#define LPD_XPPU_PADDR              0xFF980000
-#define LPD_XPPU_SINK_PADDR         0xFF9C0000
-#define NAND_PADDR                  0xFF100000
-#define OCM_PADDR                   0xFF960000
-#define OCM_XMPU_CFG_PADDR          0xFFA70000
-#define PCIE_ATTRIB_PADDR           0xFD480000
-#define PMU_GLOBAL_PADDR            0xFFD80000
-#define QSPI_PADDR                  0xFF0F0000
-#define RCPU_GIC_PADDR              0xF9000000
-#define RPU_PADDR                   0xFF9A0000
-#define RSA_PADDR                   0xFFCE002C
-#define RSA_CORE_PADDR              0xFFCE0000
-#define RTC_PADDR                   0xFFA60000
-#define SATA_AHCI_HBA_PADDR         0xFD0C0000
-#define SATA_AHCI_PORT0_CNTRL_PADDR 0xFD0C0100
-#define SATA_AHCI_PORT1_CNTRL_PADDR 0xFD0C0180
-#define SATA_AHCI_VENDOR_PADDR      0xFD0C00A0
-#define SD0_PADDR                   0xFF160000
-#define SD1_PADDR                   0xFF170000
-#define SERDES_PADDR                0xFD400000
-#define SIOU_PADDR                  0xFD3D0000
-#define SMMU_GPV_PADDR              0xFD800000
-#define SMMU_REG_PADDR              0xFD5F0000
-#define SPI0_PADDR                  0xFF040000
-#define SPI1_PADDR                  0xFF050000
-#define SWDT_PADDR                  0xFF150000
-#define S_AXI_HPC_0_FPD_PADDR       0xFD360000
-#define S_AXI_HPC_1_FPD_PADDR       0xFD370000
-#define S_AXI_HP_0_FPD_PADDR        0xFD380000
-#define S_AXI_HP_1_FPD_PADDR        0xFD390000
-#define S_AXI_HP_2_FPD_PADDR        0xFD3A0000
-#define S_AXI_HP_3_FPD_PADDR        0xFD3B0000
-#define S_AXI_LPD_PADDR             0xFF9B0000
-#define TTC0_PADDR                  0xFF110000
-#define TTC1_PADDR                  0xFF120000
-#define TTC2_PADDR                  0xFF130000
-#define TTC3_PADDR                  0xFF140000
-#define UART0_PADDR                 0xFF000000
-#define UART1_PADDR                 0xFF010000
-#define USB3_0_PADDR                0xFF9D0000
-#define USB3_0_XHCI_PADDR           0xFE200000
-#define USB3_1_PADDR                0xFF9E0000
-#define USB3_1_XHCI_PADDR           0xFE300000
-#define VCU_PL_DECODE_PADDR         0xA0020000
-#define VCU_PL_ENCODE_PADDR         0xA0000000
-#define VCU_PL_SLCR_PADDR           0xA0040000
-#define WDT_PADDR                   0xFD4D0000
-
-#endif /* !__PLAT_MACHINE_DEVICES_H */
diff --git a/include/plat/zynqmp/plat/machine/hardware.h b/include/plat/zynqmp/plat/machine/hardware.h
index 0080ae273..e1c7634e6 100644
--- a/include/plat/zynqmp/plat/machine/hardware.h
+++ b/include/plat/zynqmp/plat/machine/hardware.h
@@ -24,32 +24,9 @@
 #include <basic_types.h>
 #include <arch/linker.h>
 #include <plat/machine.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/devices_gen.h>
 #include <machine/io.h>
 
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
-    {
-        /* GIC */
-        ACPU_GIC_CONTROLLER_PADDR,
-        GIC_PL390_CONTROLLER_PPTR,
-        true  /* armExecuteNever */
-    },
-    {
-        ACPU_GIC_DISTRIBUTOR_PADDR,
-        GIC_PL390_DISTRIBUTOR_PPTR,
-        true  /* armExecuteNever */
-#ifdef CONFIG_PRINTING
-    },
-    {
-        /*  UART */
-        UART_PADDR,
-        UART_PPTR,
-        true  /* armExecuteNever */
-#endif /* CONFIG_PRINTING */
-    }
-};
-
 /* Handle a platform-reserved IRQ. */
 static inline void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/allwinnerA20/machine/hardware.c b/src/plat/allwinnerA20/machine/hardware.c
index 031047ebe..d420d6d48 100755
--- a/src/plat/allwinnerA20/machine/hardware.c
+++ b/src/plat/allwinnerA20/machine/hardware.c
@@ -16,18 +16,15 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 #include <plat/machine/timer.h>
 
-#define TIMER0_OFFSET       0xC00
-
 #define TIMER_CTL_EN_FLAG               BIT(0)
 #define TIMER_CTL_RELOAD_FLAG           BIT(1)
 
 #define TMR0_IRQ_EN_FLAG            BIT(0)
 
-timer_t *timer = (timer_t *) TIMER0_PPTR + TIMER0_OFFSET;
+timer_t *timer = (timer_t *) TIMER0_PPTR;
 
 /* Configure gptimer11 as kernel preemption timer */
 BOOT_CODE void
diff --git a/src/plat/allwinnerA20/machine/io.c b/src/plat/allwinnerA20/machine/io.c
index 956ff6f8c..c4f24224f 100755
--- a/src/plat/allwinnerA20/machine/io.c
+++ b/src/plat/allwinnerA20/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR 0x00 /* UART Transmit Holding Register */
 #define ULSR 0x14 /* UART Line Status Register */
diff --git a/src/plat/am335x/machine/hardware.c b/src/plat/am335x/machine/hardware.c
index 94f1fdb73..988e878f8 100644
--- a/src/plat/am335x/machine/hardware.c
+++ b/src/plat/am335x/machine/hardware.c
@@ -16,7 +16,7 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 #include <plat/machine/hardware.h>
 #include <plat/machine/timer.h>
 
@@ -30,7 +30,7 @@
 #define TCLR_COMPAREENABLE BIT(6)
 #define TCLR_STARTTIMER BIT(0)
 
-timer_t *timer = (timer_t *) DMTIMER0_PPTR;
+timer_t *timer = (timer_t *) TIMER_PPTR;
 
 #define WDT_REG(base, off) ((volatile uint32_t *)((base) + (off)))
 #define WDT_REG_WWPS 0x34
diff --git a/src/plat/am335x/machine/io.c b/src/plat/am335x/machine/io.c
index 5617b247e..1b93e0b92 100644
--- a/src/plat/am335x/machine/io.c
+++ b/src/plat/am335x/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR 0x00 /* UART Transmit Holding Register */
 #define ULSR 0x14 /* UART Line Status Register */
diff --git a/src/plat/apq8064/machine/hardware.c b/src/plat/apq8064/machine/hardware.c
index 062c65459..3eeb2a361 100644
--- a/src/plat/apq8064/machine/hardware.c
+++ b/src/plat/apq8064/machine/hardware.c
@@ -17,7 +17,6 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
 void plat_cleanL2Range(paddr_t start, paddr_t end) {}
diff --git a/src/plat/apq8064/machine/io.c b/src/plat/apq8064/machine/io.c
index 474addccb..73b7f38d2 100644
--- a/src/plat/apq8064/machine/io.c
+++ b/src/plat/apq8064/machine/io.c
@@ -12,7 +12,6 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
 
 #define UART_REG(X) ((volatile uint32_t *)(UART_PPTR + (X)))
 
diff --git a/src/plat/bcm2837/machine/io.c b/src/plat/bcm2837/machine/io.c
index a1635d910..7ea6fb6ed 100644
--- a/src/plat/bcm2837/machine/io.c
+++ b/src/plat/bcm2837/machine/io.c
@@ -14,23 +14,22 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
 
 #define UART_REG(x) ((volatile uint32_t *)(UART_PPTR + (x)))
 
 /* When DLAB=1, MU_IO is a baud rate register.
  * Otherwise, write to TX, read to RX */
-#define MU_IO       0x40
+#define MU_IO       0x00
 /* When DLAB=1, MU_IIR is a baud rate register.
  * Otherwise IRQ enable */
-#define MU_IIR      0x44
-#define MU_IER      0x48
-#define MU_LCR      0x4C
-#define MU_MCR      0x50
-#define MU_LSR      0x54
-#define MU_MSR      0x58
-#define MU_SCRATCH  0x5C
-#define MU_CNTL     0x60
+#define MU_IIR      0x04
+#define MU_IER      0x08
+#define MU_LCR      0x0C
+#define MU_MCR      0x10
+#define MU_LSR      0x14
+#define MU_MSR      0x18
+#define MU_SCRATCH  0x1C
+#define MU_CNTL     0x20
 
 
 /* This bit is set if the transmit FIFO can accept at least one byte.*/
diff --git a/src/plat/exynos4/machine/hardware.c b/src/plat/exynos4/machine/hardware.c
index f37180750..a2398a39e 100644
--- a/src/plat/exynos4/machine/hardware.c
+++ b/src/plat/exynos4/machine/hardware.c
@@ -13,7 +13,6 @@
 #include <types.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
 #include <plat/machine/timer.h>
 #include <plat/machine/mct.h>
 
diff --git a/src/plat/exynos5/machine/hardware.c b/src/plat/exynos5/machine/hardware.c
index 8621225b5..b2bd00d99 100644
--- a/src/plat/exynos5/machine/hardware.c
+++ b/src/plat/exynos5/machine/hardware.c
@@ -16,7 +16,7 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 #include <plat/machine/hardware.h>
 #include <arch/machine/generic_timer.h>
 #include <plat/machine/mct.h>
diff --git a/src/plat/exynos_common/io.c b/src/plat/exynos_common/io.c
index 3094b9714..e48b36bb1 100644
--- a/src/plat/exynos_common/io.c
+++ b/src/plat/exynos_common/io.c
@@ -12,7 +12,6 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
 
 #define ULCON       0x0000 /* line control */
 #define UCON        0x0004 /* control */
diff --git a/src/plat/hikey/machine/io.c b/src/plat/hikey/machine/io.c
index 069dfd2b7..6dae9a84e 100644
--- a/src/plat/hikey/machine/io.c
+++ b/src/plat/hikey/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UARTDR                    0x000
 #define UARTFR                    0x018
diff --git a/src/plat/imx31/machine/hardware.c b/src/plat/imx31/machine/hardware.c
index 11115117d..7d5130483 100644
--- a/src/plat/imx31/machine/hardware.c
+++ b/src/plat/imx31/machine/hardware.c
@@ -17,6 +17,7 @@
 #include <plat/machine.h>
 #include <linker.h>
 #include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 #include <plat/machine/hardware.h>
 #include <plat/machine/timer.h>
 #include <plat/machine/hardware_gen.h>
diff --git a/src/plat/imx31/machine/io.c b/src/plat/imx31/machine/io.c
index a60d9183a..098c9e7a1 100644
--- a/src/plat/imx31/machine/io.c
+++ b/src/plat/imx31/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define URXD  0x00 /* UART Receiver Register */
 #define UTXD  0x40 /* UART Transmitter Register */
diff --git a/src/plat/imx6/machine/io.c b/src/plat/imx6/machine/io.c
index 5126ce2f3..017569d72 100644
--- a/src/plat/imx6/machine/io.c
+++ b/src/plat/imx6/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define URXD  0x00 /* UART Receiver Register */
 #define UTXD  0x40 /* UART Transmitter Register */
diff --git a/src/plat/imx7/machine/io.c b/src/plat/imx7/machine/io.c
index acb961e08..967aabb57 100644
--- a/src/plat/imx7/machine/io.c
+++ b/src/plat/imx7/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define URXD  0x00 /* UART Receiver Register */
 #define UTXD  0x40 /* UART Transmitter Register */
diff --git a/src/plat/omap3/machine/hardware.c b/src/plat/omap3/machine/hardware.c
index d2950da9c..8ed84c3ad 100644
--- a/src/plat/omap3/machine/hardware.c
+++ b/src/plat/omap3/machine/hardware.c
@@ -16,7 +16,7 @@
 #include <arch/kernel/vspace.h>
 #include <plat/machine.h>
 #include <linker.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 #include <plat/machine/hardware.h>
 #include <plat/machine/timer.h>
 
@@ -32,7 +32,7 @@
 #define TIER_MATCHENABLE    BIT(0)
 #define TIER_OVERFLOWENABLE BIT(1)
 
-timer_t *timer = (timer_t *) GPTIMER9_PPTR;
+timer_t *timer = (timer_t *) TIMER_PPTR;
 
 BOOT_CODE void
 initTimer(void)
diff --git a/src/plat/omap3/machine/io.c b/src/plat/omap3/machine/io.c
index 995e62a97..11760221b 100644
--- a/src/plat/omap3/machine/io.c
+++ b/src/plat/omap3/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR 0x00 /* UART Transmit Holding Register */
 #define ULSR 0x14 /* UART Line Status Register */
diff --git a/src/plat/tk1/machine/io.c b/src/plat/tk1/machine/io.c
index d6ccca757..f3075909d 100644
--- a/src/plat/tk1/machine/io.c
+++ b/src/plat/tk1/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR        0x0
 #define ULSR        0x14
diff --git a/src/plat/tx1/machine/io.c b/src/plat/tx1/machine/io.c
index ef4b43957..9190bf161 100644
--- a/src/plat/tx1/machine/io.c
+++ b/src/plat/tx1/machine/io.c
@@ -14,7 +14,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR        0x0
 #define ULSR        0x14
diff --git a/src/plat/tx2/machine/io.c b/src/plat/tx2/machine/io.c
index e8c52ceab..6d03e77e1 100644
--- a/src/plat/tx2/machine/io.c
+++ b/src/plat/tx2/machine/io.c
@@ -14,7 +14,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UTHR        0x0
 #define ULSR        0x14
diff --git a/src/plat/zynq7000/machine/io.c b/src/plat/zynq7000/machine/io.c
index f6dd7208f..0f718ba54 100644
--- a/src/plat/zynq7000/machine/io.c
+++ b/src/plat/zynq7000/machine/io.c
@@ -12,7 +12,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define UART_CONTROL                 0x00
 #define UART_MODE                    0x04
diff --git a/src/plat/zynqmp/machine/io.c b/src/plat/zynqmp/machine/io.c
index 99279a36a..ee8c39698 100644
--- a/src/plat/zynqmp/machine/io.c
+++ b/src/plat/zynqmp/machine/io.c
@@ -19,7 +19,7 @@
 #include <stdint.h>
 #include <util.h>
 #include <machine/io.h>
-#include <plat/machine/devices.h>
+#include <plat/machine/devices_gen.h>
 
 #define XUARTPS_SR             0x2C
 #define XUARTPS_FIFO           0x30
-- 
GitLab