diff --git a/include/arch/arm/arch/32/mode/machine/registerset.h b/include/arch/arm/arch/32/mode/machine/registerset.h
index 1ef0dfb06..e3eb0174b 100644
--- a/include/arch/arm/arch/32/mode/machine/registerset.h
+++ b/include/arch/arm/arch/32/mode/machine/registerset.h
@@ -106,6 +106,8 @@ enum _register {
 #endif
 };
 
+#define NEXT_PC_REG LR_svc
+
 compile_assert(sp_offset_correct, SP *sizeof(word_t) == PT_SP)
 compile_assert(lr_svc_offset_correct, LR_svc *sizeof(word_t) == PT_LR_svc)
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
diff --git a/include/arch/arm/arch/64/mode/machine/registerset.h b/include/arch/arm/arch/64/mode/machine/registerset.h
index 4b2100382..5498fe9bf 100644
--- a/include/arch/arm/arch/64/mode/machine/registerset.h
+++ b/include/arch/arm/arch/64/mode/machine/registerset.h
@@ -147,6 +147,8 @@ enum _register {
     n_contextRegisters          = 36,
 };
 
+#define NEXT_PC_REG ELR_EL1
+
 compile_assert(sp_offset_correct, SP_EL0 *sizeof(word_t) == PT_SP_EL0)
 compile_assert(lr_svc_offset_correct, ELR_EL1 *sizeof(word_t) == PT_ELR_EL1)
 compile_assert(faultinstruction_offset_correct, FaultInstruction *sizeof(word_t) == PT_FaultInstruction)
diff --git a/src/arch/arm/32/config.cmake b/src/arch/arm/32/config.cmake
index 8736765c5..48f130aac 100644
--- a/src/arch/arm/32/config.cmake
+++ b/src/arch/arm/32/config.cmake
@@ -17,7 +17,6 @@ add_sources(
     PREFIX src/arch/arm/32
     CFILES
         object/objecttype.c
-        machine/hardware.c
         machine/registerset.c
         machine/fpu.c
         model/statedata.c
diff --git a/src/arch/arm/64/config.cmake b/src/arch/arm/64/config.cmake
index 84058bcc4..f40e26a5a 100644
--- a/src/arch/arm/64/config.cmake
+++ b/src/arch/arm/64/config.cmake
@@ -18,7 +18,6 @@ add_sources(
     CFILES
         object/objecttype.c
         machine/capdl.c
-        machine/hardware.c
         machine/registerset.c
         machine/fpu.c
         model/statedata.c
diff --git a/src/arch/arm/64/machine/hardware.c b/src/arch/arm/64/machine/hardware.c
deleted file mode 100644
index 52d2eb6bb..000000000
--- a/src/arch/arm/64/machine/hardware.c
+++ /dev/null
@@ -1,57 +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)
- */
-
-#include <types.h>
-#include <machine/registerset.h>
-#include <arch/machine.h>
-#include <plat/machine/hardware.h>
-
-word_t PURE getRestartPC(tcb_t *thread)
-{
-    return getRegister(thread, FaultInstruction);
-}
-
-void setNextPC(tcb_t *thread, word_t v)
-{
-    setRegister(thread, ELR_EL1, v);
-}
-
-BOOT_CODE int get_num_avail_p_regs(void)
-{
-    return sizeof(avail_p_regs) / sizeof(p_region_t);
-}
-
-BOOT_CODE int get_num_dev_p_regs(void)
-{
-    return sizeof(dev_p_regs) / sizeof(p_region_t);
-}
-
-BOOT_CODE p_region_t get_dev_p_reg(word_t i)
-{
-    return dev_p_regs[i];
-}
-
-BOOT_CODE const p_region_t* get_avail_p_regs(void)
-{
-    return avail_p_regs;
-}
-
-BOOT_CODE void map_kernel_devices(void)
-{
-    for (int i = 0; i < ARRAY_SIZE(kernel_devices); i++) {
-        map_kernel_frame(kernel_devices[i].paddr,
-                         kernel_devices[i].pptr,
-                         VMKernelOnly,
-                         vm_attributes_new(kernel_devices[i].armExecuteNever,
-                                           false, false));
-    }
-}
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index acf96c134..14a3d4de2 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -444,6 +444,7 @@ add_sources(
         machine/cache.c
         machine/errata.c
         machine/debug.c
+        machine/hardware.c
         object/interrupt.c
         object/tcb.c
         object/iospace.c
diff --git a/src/arch/arm/32/machine/hardware.c b/src/arch/arm/machine/hardware.c
similarity index 96%
rename from src/arch/arm/32/machine/hardware.c
rename to src/arch/arm/machine/hardware.c
index 0cbd2bd3a..1a5fa54c4 100644
--- a/src/arch/arm/32/machine/hardware.c
+++ b/src/arch/arm/machine/hardware.c
@@ -20,7 +20,7 @@ word_t PURE getRestartPC(tcb_t *thread)
 
 void setNextPC(tcb_t *thread, word_t v)
 {
-    setRegister(thread, LR_svc, v);
+    setRegister(thread, NEXT_PC_REG, v);
 }
 
 BOOT_CODE int get_num_avail_p_regs(void)