diff --git a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
index 4843d3353..0d1feb0c2 100644
--- a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
@@ -48,6 +48,7 @@
 /* Below the main kernel window we have any slots for the TLB bitmap */
 #define TLBBITMAP_PML4_RESERVED (TLBBITMAP_ROOT_ENTRIES * BIT(PML4_INDEX_OFFSET))
 #define TLBBITMAP_PPTR (PPTR_BASE - TLBBITMAP_PML4_RESERVED)
+#define PPTR_TOP TLBBITMAP_PPTR
 
 /* Define PPTR_USER_TOP to be 1 before the last address before sign extension occurs.
  * This ensures that