+/* Put physical address into the BAT format */
+#define BAT_PHYS_ADDR(low, high) \
+ (low | PHYS_HIGH_TO_BXPN(high) | PHYS_HIGH_TO_BX(high))
+/* Convert high/low pairs to actual 64-bit value */
+#define PAIRED_PHYS_TO_PHYS(low, high) (low | ((u64)high << 32))
+#else
+/* 32-bit systems just ignore the "high" bits */
+#define BAT_PHYS_ADDR(low, high) (low)
+#define PAIRED_PHYS_TO_PHYS(low, high) (low)
+#endif
+