diff --git a/include/arch/x86/arch/object/structures.h b/include/arch/x86/arch/object/structures.h
index b15597acd..ed54a4df8 100644
--- a/include/arch/x86/arch/object/structures.h
+++ b/include/arch/x86/arch/object/structures.h
@@ -16,6 +16,7 @@
 #include <arch/machine/hardware.h>
 #include <arch/machine/registerset.h>
 #include <sel4/arch/constants.h>
+#include <sel4/sel4_arch/constants.h>
 
 enum tcb_arch_cnode_index {
 #ifdef CONFIG_VTX
@@ -54,9 +55,9 @@ typedef struct arch_tcb {
 #define VTD_CT_BITS       8
 #define VTD_CT_SIZE_BITS  (VTD_CT_BITS + VTD_CTE_SIZE_BITS)
 
-#define VTD_PTE_SIZE_BITS 3
+#define VTD_PTE_SIZE_BITS seL4_IOPageTableEntryBits
 #define VTD_PTE_PTR(r)    ((vtd_pte_t*)(r))
-#define VTD_PT_INDEX_BITS       9
+#define VTD_PT_INDEX_BITS seL4_IOPageTableIndexBits
 
 compile_assert(vtd_pt_size_sane, VTD_PT_INDEX_BITS + VTD_PTE_SIZE_BITS == seL4_IOPageTableBits)
 
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
index e47e7971b..9d1699db2 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
@@ -38,12 +38,15 @@
 #define seL4_PageDirIndexBits 10
 #define seL4_VSpaceBits seL4_PageDirBits
 
-#define seL4_IOPageTableBits 12
 #define seL4_NumASIDPoolsBits 2
 #define seL4_ASIDPoolBits    12
 #define seL4_ASIDPoolIndexBits 10
 #define seL4_WordSizeBits 2
 
+#define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_HugePageBits    30 /* 1GB */
 #define seL4_PDPTBits         0
 #define seL4_LargePageBits    22 /* 4MB */
@@ -52,6 +55,7 @@
 SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
 SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 #endif
 
 /* Previously large frames were explicitly assumed to be 4M. If not using
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
index ecbcb688b..51f0e007a 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
@@ -53,7 +53,10 @@
 #define seL4_PML4IndexBits      9
 #define seL4_VSpaceBits seL4_PML4Bits
 
-#define seL4_IOPageTableBits    12
+#define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_LargePageBits      21
 #define seL4_HugePageBits       30
 #define seL4_NumASIDPoolsBits    3
@@ -71,6 +74,7 @@ SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits)
 SEL4_SIZE_SANITY(seL4_PDPTEntryBits, seL4_PDPTIndexBits, seL4_PDPTBits);
 SEL4_SIZE_SANITY(seL4_PML4EntryBits, seL4_PML4IndexBits, seL4_PML4Bits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 
 typedef enum {
     seL4_VMFault_IP,