diff --git a/include/plat/spike/plat/32/plat_mode/machine/hardware.h b/include/plat/spike/plat/32/plat_mode/machine/hardware.h
index 56be4e5f6..f21f6eadb 100644
--- a/include/plat/spike/plat/32/plat_mode/machine/hardware.h
+++ b/include/plat/spike/plat/32/plat_mode/machine/hardware.h
@@ -19,5 +19,6 @@
 #define PPTR_BASE  seL4_UserTop
 /* This is the mapping of the kernel (mapped above the kernel window currently) */
 #define KERNEL_BASE 0xFF800000lu
+#define KERNEL_ELF_BASE KERNEL_BASE
 
 #endif
diff --git a/include/plat/spike/plat/64/plat_mode/machine/hardware.h b/include/plat/spike/plat/64/plat_mode/machine/hardware.h
index 635b9c1bd..73df13462 100644
--- a/include/plat/spike/plat/64/plat_mode/machine/hardware.h
+++ b/include/plat/spike/plat/64/plat_mode/machine/hardware.h
@@ -26,7 +26,8 @@
 /* This is the base of the kernel window, which is directly mapped to PADDR_BASE */
 #define PPTR_BASE        0xFFFFFFC000000000lu
 /* This is the mapping of the kernel (mapped above the kernel window currently) */
-#define KERNEL_BASE      0xFFFFFFFF84000000lu
+#define KERNEL_BASE      0xFFFFFFFF80000000lu
+#define KERNEL_ELF_BASE  0xFFFFFFFF84000000lu
 #else
 #error Only PT_LEVELS == 3 is supported
 #endif
diff --git a/include/plat/spike/plat/machine/hardware.h b/include/plat/spike/plat/machine/hardware.h
index d914373ea..da0df155b 100644
--- a/include/plat/spike/plat/machine/hardware.h
+++ b/include/plat/spike/plat/machine/hardware.h
@@ -45,10 +45,10 @@
 #define PADDR_TOP (KERNEL_BASE - PPTR_BASE + PADDR_BASE)
 /* The highest valid physical address that can be used for the kernel image. We offset by
  * PADDR_LOAD as the window for the kernel image is mapped started at PADDR_LOAD */
-#define PADDR_HIGH_TOP (-KERNEL_BASE + PADDR_LOAD)
+#define PADDR_HIGH_TOP (-KERNEL_ELF_BASE + PADDR_LOAD)
 
 /* Translates from a physical address and a value in the kernel image */
-#define KERNEL_BASE_OFFSET (KERNEL_BASE - PADDR_LOAD)
+#define KERNEL_BASE_OFFSET (KERNEL_ELF_BASE - PADDR_LOAD)
 
 /* Convert our values into general values expected by the common code */
 #define kernelBase KERNEL_BASE
diff --git a/src/arch/riscv/kernel/boot.c b/src/arch/riscv/kernel/boot.c
index e3d1d2157..90f25fe57 100644
--- a/src/arch/riscv/kernel/boot.c
+++ b/src/arch/riscv/kernel/boot.c
@@ -140,7 +140,7 @@ static BOOT_CODE bool_t try_init_kernel(
     cap_t it_ap_cap;
     cap_t ipcbuf_cap;
     p_region_t boot_mem_reuse_p_reg = ((p_region_t) {
-        kpptr_to_paddr((void *)KERNEL_BASE), kpptr_to_paddr(ki_boot_end)
+        kpptr_to_paddr((void *)KERNEL_ELF_BASE), kpptr_to_paddr(ki_boot_end)
     });
     region_t boot_mem_reuse_reg = paddr_to_pptr_reg(boot_mem_reuse_p_reg);
     region_t ui_reg = paddr_to_pptr_reg((p_region_t) {
diff --git a/src/arch/riscv/kernel/vspace.c b/src/arch/riscv/kernel/vspace.c
index 91dea1867..63311f99a 100644
--- a/src/arch/riscv/kernel/vspace.c
+++ b/src/arch/riscv/kernel/vspace.c
@@ -108,7 +108,7 @@ BOOT_CODE VISIBLE void map_kernel_window(void)
 
     /* first we map in memory from PADDR_BASE */
     word_t paddr = PADDR_BASE;
-    while (pptr < ROUND_DOWN(KERNEL_BASE, RISCV_GET_LVL_PGSIZE_BITS(1))) {
+    while (pptr < KERNEL_BASE) {
         assert(IS_ALIGNED(pptr, RISCV_GET_LVL_PGSIZE_BITS(1)));
         assert(IS_ALIGNED(paddr, RISCV_GET_LVL_PGSIZE_BITS(1)));
 
@@ -118,7 +118,7 @@ BOOT_CODE VISIBLE void map_kernel_window(void)
         paddr += RISCV_GET_LVL_PGSIZE(1);
     }
     /* now we should be mapping the 1GiB kernel base */
-    assert(pptr == ROUND_DOWN(KERNEL_BASE, RISCV_GET_LVL_PGSIZE_BITS(1)));
+    assert(pptr == KERNEL_BASE);
     paddr = ROUND_DOWN(PADDR_LOAD, RISCV_GET_LVL_PGSIZE_BITS(1));
 
 #if __riscv_xlen == 32
@@ -134,8 +134,7 @@ BOOT_CODE VISIBLE void map_kernel_window(void)
         pte_next(kpptr_to_paddr(kernel_image_level2_pt), false);
     kernel_root_pageTable[RISCV_GET_PT_INDEX(pptr, 1)] =
         pte_next(kpptr_to_paddr(kernel_image_level2_pt), false);
-    while (pptr < ROUND_DOWN(KERNEL_BASE, RISCV_GET_LVL_PGSIZE_BITS(1)) +
-           RISCV_GET_LVL_PGSIZE(1)) {
+    while (pptr < KERNEL_BASE + RISCV_GET_LVL_PGSIZE(1)) {
         kernel_image_level2_pt[index] = pte_next(paddr, true);
         index++;
         pptr += RISCV_GET_LVL_PGSIZE(2);
diff --git a/src/plat/spike/linker.lds b/src/plat/spike/linker.lds
index ea6bc06e3..5ab3a0491 100644
--- a/src/plat/spike/linker.lds
+++ b/src/plat/spike/linker.lds
@@ -22,9 +22,9 @@ ENTRY(_start)
 #include <config.h>
 
 #if CONFIG_PT_LEVELS == 2
-KERNEL_BASE  = 0xFF800000;
+KERNEL_ELF_BASE  = 0xFF800000;
 #elif CONFIG_PT_LEVELS == 3
-KERNEL_BASE  = 0xFFFFFFFF84000000;
+KERNEL_ELF_BASE  = 0xFFFFFFFF84000000;
 #elif CONFIG_PT_LEVELS == 4
 #error PT_LEVELS == 4 is not supported yet
 #endif
@@ -35,11 +35,11 @@ PADDR_LOAD     = 0x0000000088000000;
 #else
 PADDR_LOAD     = 0x0000000084000000;
 #endif
-KERNEL_OFFSET = KERNEL_BASE - PADDR_LOAD;
+KERNEL_OFFSET = KERNEL_ELF_BASE - PADDR_LOAD;
 
 SECTIONS
 {
-    . = KERNEL_BASE;
+    . = KERNEL_ELF_BASE;
 
     .boot . : AT(ADDR(.boot) - KERNEL_OFFSET)
     {