diff --git a/include/l4/arch/arm/v5/mm.h b/include/l4/arch/arm/v5/mm.h
index 35b763b..d0ff6d2 100644
--- a/include/l4/arch/arm/v5/mm.h
+++ b/include/l4/arch/arm/v5/mm.h
@@ -40,6 +40,9 @@
 #define PMD_ENTRY_TOTAL				256
 #define PMD_MAP_SIZE				SZ_1MB
 
+/* We need this as printascii.S is including this file */
+#ifndef __ASSEMBLY__
+
 /* Type-checkable page table elements */
 typedef u32 pgd_t;
 typedef u32 pmd_t;
@@ -157,4 +160,5 @@ void remove_section_mapping(unsigned long vaddr);
 void copy_pgds_by_vrange(pgd_table_t *to, pgd_table_t *from,
 			 unsigned long start, unsigned long end);
 
+#endif /* __ASSEMBLY__ */
 #endif /* __V5_MM_H__ */
diff --git a/include/l4/drivers/irq/gic/gic.h b/include/l4/drivers/irq/gic/gic.h
index 65adb79..ac27118 100644
--- a/include/l4/drivers/irq/gic/gic.h
+++ b/include/l4/drivers/irq/gic/gic.h
@@ -1,56 +1,35 @@
 /*
- * PL190 Primecell Vectored Interrupt Controller offsets
+ * Generic Interrupt Controller offsets
  *
  * Copyright (C) 2007 Bahadir Balban
  *
  */
 
-#ifndef __PL190_VIC_H__
-#define __PL190_VIC_H__
+#ifndef __ARM_GIC_H__
+#define __ARM_GIC_H__
 
 #include INC_PLAT(platform.h)
 
-#define PL190_BASE				PLATFORM_IRQCTRL_BASE
-#define PL190_SIC_BASE				PLATFORM_SIRQCTRL_BASE
+/* GIC CPU register offsets */
+#define ARM_GIC_CPU_ICR		0x00 /* Interface Control */
+#define ARM_GIC_CPUPMR		0x04 /* Interrupt Priority Mask */
+#define ARM_GIC_CPU_BPR		0x08 /* Binary Point */
+#define ARM_GIC_CPU_IAR		0x0c /* Interrupt Acknowledge */
+#define ARM_GIC_CPU_EOIR	0x10 /* End of Interrupt */
+#define ARM_GIC_CPU_RRI		0x14 /* Running Priority */
+#define ARM_GIC_CPU_HPIR	0x18 /* Highest Priority Interrupt*/
 
-/* VIC register offsets */
-#define PL190_VIC_IRQSTATUS			(PL190_BASE + 0x00)
-#define PL190_VIC_FIQSTATUS			(PL190_BASE + 0x04)
-#define PL190_VIC_RAWINTR			(PL190_BASE + 0x08)
-#define PL190_VIC_INTSELECT			(PL190_BASE + 0x0C)
-#define PL190_VIC_INTENABLE			(PL190_BASE + 0x10)
-#define PL190_VIC_INTENCLEAR			(PL190_BASE + 0x14)
-#define PL190_VIC_SOFTINT			(PL190_BASE + 0x18)
-#define PL190_VIC_SOFTINTCLEAR			(PL190_BASE + 0x1C)
-#define PL190_VIC_PROTECTION			(PL190_BASE + 0x20)
-#define PL190_VIC_VECTADDR			(PL190_BASE + 0x30)
-#define PL190_VIC_DEFVECTADDR			(PL190_BASE + 0x34)
-#define PL190_VIC_VECTADDR0			(PL190_BASE + 0x100)
-/* 15 PIC_VECTADDR registers up to	0x13C */
-#define PL190_VIC_VECTCNTL0			(PL190_BASE + 0x200)
-/* 15 PIC_VECTCNTL registers up to	0x23C */
+/* Distributor register map */
+#define ARM_GIC_DIST_CR		0x000 /* Control Register */
+#define ARM_GIC_DIST_ICTR	0x004 /* Interface Controller Type */
+#define ARM_GIC_DIST_ISER	0x100 /* Interrupt Set Enable */
+#define ARM_GIC_DIST_ICER	0x180 /* Interrupt Clear Enable */
+#define ARM_GIC_DIST_ISPR	0x200 /* Interrupt Set Pending */
+#define ARM_GIC_DIST_ICPR	0x280 /* Interrupt Clear Pending*/
+#define ARM_GIC_DIST_ABR	0x300 /* Active Bit */
+#define ARM_GIC_DIST_IPR	0x400 /* Interrupt Priority */
+#define ARM_GIC_DIST_IPTR	0x800 /* Interrupt Processor Target */
+#define ARM_GIC_DIST_ICR	0xc00 /* Interrupt Configuration */
+#define ARM_GIC_DIST_SGIR	0xf00 /* Software Generated Interrupt */
 
-#define PL190_SIC_STATUS			(PL190_SIC_BASE + 0x0)
-#define PL190_SIC_RAWSTAT			(PL190_SIC_BASE + 0x04)
-#define PL190_SIC_ENABLE			(PL190_SIC_BASE + 0x08)
-#define PL190_SIC_ENSET				(PL190_SIC_BASE + 0x08)
-#define PL190_SIC_ENCLR				(PL190_SIC_BASE + 0x0C)
-#define PL190_SIC_SOFTINTSET			(PL190_SIC_BASE + 0x10)
-#define PL190_SIC_SOFTINTCLR			(PL190_SIC_BASE + 0x14)
-#define PL190_SIC_PICENABLE			(PL190_SIC_BASE + 0x20)
-#define PL190_SIC_PICENSET			(PL190_SIC_BASE + 0x20)
-#define PL190_SIC_PICENCLR			(PL190_SIC_BASE + 0x24)
-
-void pl190_vic_init(void);
-void pl190_ack_irq(int irq);
-void pl190_mask_irq(int irq);
-void pl190_unmask_irq(int irq);
-int pl190_read_irq(void);
-
-int pl190_sic_read_irq(void);
-void pl190_sic_mask_irq(int irq);
-void pl190_sic_mask_irq(int irq);
-void pl190_sic_ack_irq(int irq);
-void pl190_sic_unmask_irq(int irq);
-void pl190_sic_init(void);
-#endif /* __PL190_VIC_H__ */
+#endif /* __ARM_GIC_H__ */
diff --git a/include/l4/platform/eb/irq.h b/include/l4/platform/eb/irq.h
index ecfad92..3c17bee 100644
--- a/include/l4/platform/eb/irq.h
+++ b/include/l4/platform/eb/irq.h
@@ -1,27 +1,31 @@
 #ifndef __PLATFORM_IRQ_H__
 #define __PLATFORM_IRQ_H__
 
-#define IRQ_CHIPS_MAX				2
-#define IRQS_MAX				64
+/* TODO: Not sure about this, need to check */
+#define IRQ_CHIPS_MAX			4
+#define IRQS_MAX			96
 
-/* IRQ indices. */
+/*
+ * IRQ indices,
+ * GIC 0 and 1 are for logic tile 1
+ * GIC 2 and 3 are for logic tile 2
+ */
 #define IRQ_TIMER01			4
 #define IRQ_TIMER23			5
 #define IRQ_RTC				10
 #define IRQ_UART0			12
 #define IRQ_UART1			13
 #define IRQ_UART2			14
-#define IRQ_SIC				31
-
-/* Cascading definitions */
-
-#define PIC_IRQS_MAX			31 /* Total irqs on PIC */
-/* The local irq line of the dummy peripheral on this chip */
-#define LOCALIRQ_DUMMY			15
-/* The irq index offset of this chip, is the maximum of previous chip + 1 */
-#define SIRQ_CHIP_OFFSET		(PIC_IRQS_MAX + 1)
-/* The global irq number of dummy is the local irq line + it's chip offset */
-#define IRQ_DUMMY			(LOCALIRQ_DUMMY + SIRQ_CHIP_OFFSET)
-
+#define IRQ_UART3                       15
 
+/*
+ * TODO: Seems like GIC0 and GIC1 are cascaded for logic tile1
+ * and GIC2 and GIC3 are cascaded for logic tile 2.
+ * Interrupt Distribution:
+ * 0-31: Used as SI provided by distributed interrupt controller
+ * 32-63: Externel Peripheral Interrupts
+ * 64-71: Interrupts from tile site 1
+ * 72-79: Interrupts from tile site 2
+ * 80-95: PCI and reserved Interrupts
+ */
 #endif /* __PLATFORM_IRQ_H__ */
diff --git a/include/l4/platform/eb/offsets.h b/include/l4/platform/eb/offsets.h
index 4a49729..4d6f3fd 100644
--- a/include/l4/platform/eb/offsets.h
+++ b/include/l4/platform/eb/offsets.h
@@ -1,15 +1,15 @@
 /*
- * Describes physical memory layout of pb926 platform.
+ * Describes physical memory layout of EB platform.
  *
  * Copyright (C) 2007 Bahadir Balban
  */
 
-#ifndef __PLATFORM_PB926_OFFSETS_H__
-#define __PLATFORM_PB926_OFFSETS_H__
+#ifndef __PLATFORM_EB_OFFSETS_H__
+#define __PLATFORM_EB_OFFSETS_H__
 
 /* Physical memory base */
 #define	PHYS_MEM_START			0x00000000 /* inclusive */
-#define	PHYS_MEM_END			0x08000000 /* 128 MB, exclusive */
+#define	PHYS_MEM_END			0x10000000 /* 256 MB, exclusive */
 
 /*
  * These bases taken from where kernel is `physically' linked at,
@@ -20,18 +20,23 @@
 #define	PHYS_ADDR_BASE			0x100000
 
 /* Device memory base */
-#define	PB926_DEV_PHYS			0x10000000
+#define	EB_DEV_PHYS			0x10000000
 
 /* Device offsets in physical memory */
-#define	PB926_SYSTEM_REGISTERS		0x10000000 /* System registers */
-#define	PB926_SYSCTRL_BASE		0x101E0000 /* System controller */
-#define	PB926_WATCHDOG_BASE		0x101E1000 /* Watchdog */
-#define	PB926_TIMER01_BASE		0x101E2000 /* Timers 0 and 1 */
-#define	PB926_TIMER23_BASE		0x101E3000 /* Timers 2 and 3 */
-#define	PB926_RTC_BASE			0x101E8000 /* Real Time Clock */
-#define	PB926_VIC_BASE			0x10140000 /* Primary Vectored IC */
-#define	PB926_SIC_BASE			0x10003000 /* Secondary IC */
-#define	PB926_UART0_BASE		0x101F1000 /* Console port (UART0) */
+#define	EB_SYSTEM_REGISTERS		0x10000000 /* System registers */
+#define	EB_SYSCTRL_BASE			0x10001000 /* System controller */
+#define EB_UART0_BASE           	0x10009000 /* UART 0 */
+#define EB_UART1_BASE           	0x1000A000 /* UART 1 */
+#define EB_UART2_BASE           	0x1000B000 /* UART 2 */
+#define EB_UART3_BASE           	0x1000C000 /* UART 3 */
+#define EB_WATCHDOG0_BASE       	0x10010000 /* WATCHDOG */
+#define EB_TIMER01_BASE         	0x10011000 /* TIMER 0-1 */
+#define EB_TIMER23_BASE         	0x10012000 /* TIMER 2-3 */
+#define EB_RTC_BASE			0x10017000 /* RTC interface */
+#define EB_GIC0_BASE            	0x10040000 /* GIC 0 */
+#define EB_GIC1_BASE            	0x10050000 /* GIC 1 */
+#define EB_GIC2_BASE            	0x10060000 /* GIC 2 */
+#define EB_GIC3_BASE            	0x10070000 /* GIC 3 */
 
 /*
  * Uart virtual address until a file-based console access
@@ -44,17 +49,23 @@
  * device base address. Each page on this virtual base is consecutively
  * allocated to devices. Nice and smooth.
  */
-#define PB926_TIMER01_VOFFSET			0x00000000
-#define PB926_UART0_VOFFSET			0x00001000
-#define	PB926_VIC_VOFFSET			0x00002000
-#define	PB926_SIC_VOFFSET			0x00003000
-#define PB926_SYSREGS_VOFFSET			0x00005000
-#define PB926_SYSCTRL_VOFFSET			0x00006000
+#define EB_SYSREGS_VOFFSET	0x00000000
+#define EB_SYSCTRL_VOFFSET	0x00001000
+#define EB_UART0_VOFFSET	0x00002000
+#define EB_TIMER01_VOFFSET	0x00003000
+#define EB_GIC0_VOFFSET		0x00004000
+#define EB_GIC1_VOFFSET       	0x00005000
+#define EB_GIC2_VOFFSET       	0x00006000
+#define EB_GIC3_VOFFSET       	0x00007000
 
-#define PB926_UART0_VBASE			(IO_AREA0_VADDR + PB926_UART0_VOFFSET)
-#define PB926_TIMER01_VBASE			(IO_AREA0_VADDR + PB926_TIMER01_VOFFSET)
-#define PB926_SYSCTRL_VBASE			(IO_AREA0_VADDR + PB926_SYSCTRL_VOFFSET)
-#define PB926_VIC_VBASE				(IO_AREA0_VADDR + PB926_VIC_VOFFSET)
-#define PB926_SIC_VBASE				(IO_AREA0_VADDR + PB926_SIC_VOFFSET)
-#endif /* __PLATFORM_PB926_OFFSETS_H__ */
+#define EB_SYSREGS_VBASE	(IO_AREA0_VADDR + EB_SYSREGS_VOFFSET)
+#define EB_SYSCTRL_VBASE	(IO_AREA0_VADDR + EB_SYSCTRL0_VOFFSET)
+#define EB_UART0_VBASE		(IO_AREA0_VADDR + EB_UART0_VOFFSET)
+#define EB_TIMER01_VBASE	(IO_AREA0_VADDR + EB_TIMER01_VOFFSET)
+#define EB_GIC0_VBASE         	(IO_AREA0_VADDR + EB_GIC0_VOFFSET)
+#define EB_GIC1_VBASE         	(IO_AREA0_VADDR + EB_GIC1_VOFFSET)
+#define EB_GIC2_VBASE         	(IO_AREA0_VADDR + EB_GIC2_VOFFSET)
+#define EB_GIC3_VBASE         	(IO_AREA0_VADDR + EB_GIC3_VOFFSET)
+
+#endif /* __PLATFORM_EB_OFFSETS_H__ */
 
diff --git a/include/l4/platform/eb/platform.h b/include/l4/platform/eb/platform.h
index dd4f4cb..85896db 100644
--- a/include/l4/platform/eb/platform.h
+++ b/include/l4/platform/eb/platform.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM_PB926_PLATFORM_H__
-#define __PLATFORM_PB926_PLATFORM_H__
+#ifndef __PLATFORM_EB_PLATFORM_H__
+#define __PLATFORM_EB_PLATFORM_H__
 /*
  * Platform specific ties between drivers and generic APIs used by the kernel.
  * E.g. system timer and console.
@@ -10,13 +10,19 @@
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
-#define PLATFORM_TIMER_BASE			PB926_TIMER01_VBASE
-#define PLATFORM_SP810_BASE			PB926_SYSCTRL_VBASE
-#define PLATFORM_IRQCTRL_BASE			PB926_VIC_VBASE
-#define PLATFORM_SIRQCTRL_BASE			PB926_SIC_VBASE
+#define PLATFORM_CONSOLE0_BASE			EB_UART0_VBASE
+#define PLATFORM_TIMER0_BASE			EB_TIMER01_VBASE
+#define PLATFORM_SP810_BASE			EB_SYSCTRL_VBASE
+
+/* Total number of timers present in this platform */
+#define	TOTAL_TIMERS			4
+
+#define PLATFORM_TIMER0	0
+#define PLATFORM_TIMER1	1
+#define PLATFORM_TIMER2	2
+#define PLATFORM_TIMER3	3
 
 void platform_irq_enable(int irq);
 void platform_irq_disable(int irq);
 void timer_start(void);
-#endif /* __PLATFORM_PB926_PLATFORM_H__ */
+#endif /* __PLATFORM_EB_PLATFORM_H__ */
diff --git a/include/l4/platform/eb/printascii.h b/include/l4/platform/eb/printascii.h
index 0d0be28..3a55df4 100644
--- a/include/l4/platform/eb/printascii.h
+++ b/include/l4/platform/eb/printascii.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM__PB926__PRINTASCII__H__
-#define __PLATFORM__PB926__PRINTASCII__H__
+#ifndef __PLATFORM__EB__PRINTASCII__H__
+#define __PLATFORM__EB__PRINTASCII__H__
 
 #define	dprintk(str, val)		\
 {					\
@@ -12,4 +12,4 @@
 void printascii(char *str);
 void printhex8(unsigned int);
 
-#endif /* __PLATFORM__PB926__PRINTASCII__H__ */
+#endif /* __PLATFORM__EB__PRINTASCII__H__ */
diff --git a/include/l4/platform/eb/uart.h b/include/l4/platform/eb/uart.h
index 366590f..69bb0da 100644
--- a/include/l4/platform/eb/uart.h
+++ b/include/l4/platform/eb/uart.h
@@ -5,16 +5,16 @@
  *
  */
 
-#ifndef __PLATFORM_PB926_UART_H__
-#define __PLATFORM_PB926_UART_H__
+#ifndef __PLATFORM_EB_UART_H__
+#define __PLATFORM_EB_UART_H__
 
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
+#define PLATFORM_CONSOLE_BASE			EB_UART0_VBASE
 #include <l4/drivers/uart/pl011/pl011_uart.h>
 
 void uart_init(void);
 void uart_putc(char c);
 
-#endif /* __PLATFORM_PB926_UART_H__ */
+#endif /* __PLATFORM_EB_UART_H__ */
diff --git a/include/l4/platform/pb11mpcore/irq.h b/include/l4/platform/pb11mpcore/irq.h
index ecfad92..9773759 100644
--- a/include/l4/platform/pb11mpcore/irq.h
+++ b/include/l4/platform/pb11mpcore/irq.h
@@ -1,27 +1,27 @@
 #ifndef __PLATFORM_IRQ_H__
 #define __PLATFORM_IRQ_H__
 
-#define IRQ_CHIPS_MAX				2
-#define IRQS_MAX				64
+/* TODO: Not sure about this, need to check */
+#define IRQ_CHIPS_MAX			4
+#define IRQS_MAX			96
 
 /* IRQ indices. */
-#define IRQ_TIMER01			4
-#define IRQ_TIMER23			5
-#define IRQ_RTC				10
-#define IRQ_UART0			12
-#define IRQ_UART1			13
-#define IRQ_UART2			14
-#define IRQ_SIC				31
-
-/* Cascading definitions */
-
-#define PIC_IRQS_MAX			31 /* Total irqs on PIC */
-/* The local irq line of the dummy peripheral on this chip */
-#define LOCALIRQ_DUMMY			15
-/* The irq index offset of this chip, is the maximum of previous chip + 1 */
-#define SIRQ_CHIP_OFFSET		(PIC_IRQS_MAX + 1)
-/* The global irq number of dummy is the local irq line + it's chip offset */
-#define IRQ_DUMMY			(LOCALIRQ_DUMMY + SIRQ_CHIP_OFFSET)
+#define IRQ_TIMER01			36
+#define IRQ_TIMER23			37
+#define IRQ_TIMER45                     73
+#define IRQ_TIMER67                     74
+#define IRQ_RTC				42
+#define IRQ_UART0			44
+#define IRQ_UART1			45
+#define IRQ_UART2			46
+#define IRQ_UART3                       47
 
+/*
+ * Interrupt Distribution:
+ * 0-31: SI, provided by distributed interrupt controller
+ * 32-63: Externel peripheral interrupts
+ * 64-71: Tile site interrupt
+ * 72-95: Externel peripheral interrupts
+ */
 
 #endif /* __PLATFORM_IRQ_H__ */
diff --git a/include/l4/platform/pb11mpcore/offsets.h b/include/l4/platform/pb11mpcore/offsets.h
index 4a49729..61c23ae 100644
--- a/include/l4/platform/pb11mpcore/offsets.h
+++ b/include/l4/platform/pb11mpcore/offsets.h
@@ -1,15 +1,15 @@
 /*
- * Describes physical memory layout of pb926 platform.
+ * Describes physical memory layout of PB11MPCORE platform.
  *
  * Copyright (C) 2007 Bahadir Balban
  */
 
-#ifndef __PLATFORM_PB926_OFFSETS_H__
-#define __PLATFORM_PB926_OFFSETS_H__
+#ifndef __PLATFORM_PB11MPCORE_OFFSETS_H__
+#define __PLATFORM_PB11MPCORE_OFFSETS_H__
 
 /* Physical memory base */
 #define	PHYS_MEM_START			0x00000000 /* inclusive */
-#define	PHYS_MEM_END			0x08000000 /* 128 MB, exclusive */
+#define	PHYS_MEM_END			0x10000000 /* 256 MB, exclusive */
 
 /*
  * These bases taken from where kernel is `physically' linked at,
@@ -20,18 +20,27 @@
 #define	PHYS_ADDR_BASE			0x100000
 
 /* Device memory base */
-#define	PB926_DEV_PHYS			0x10000000
+#define	PB11MPCORE_DEV_PHYS		0x10000000
 
 /* Device offsets in physical memory */
-#define	PB926_SYSTEM_REGISTERS		0x10000000 /* System registers */
-#define	PB926_SYSCTRL_BASE		0x101E0000 /* System controller */
-#define	PB926_WATCHDOG_BASE		0x101E1000 /* Watchdog */
-#define	PB926_TIMER01_BASE		0x101E2000 /* Timers 0 and 1 */
-#define	PB926_TIMER23_BASE		0x101E3000 /* Timers 2 and 3 */
-#define	PB926_RTC_BASE			0x101E8000 /* Real Time Clock */
-#define	PB926_VIC_BASE			0x10140000 /* Primary Vectored IC */
-#define	PB926_SIC_BASE			0x10003000 /* Secondary IC */
-#define	PB926_UART0_BASE		0x101F1000 /* Console port (UART0) */
+#define	PB11MPCORE_SYSTEM_REGISTERS	0x10000000 /* System registers */
+#define	PB11MPCORE_SYSCTRL0_BASE	0x10001000 /* System controller 0 */
+#define PB11MPCORE_UART0_BASE           0x10009000 /* UART 0 */
+#define PB11MPCORE_UART1_BASE           0x1000A000 /* UART 1 */
+#define PB11MPCORE_UART2_BASE           0x1000B000 /* UART 2 */
+#define PB11MPCORE_UART3_BASE           0x1000C000 /* UART 3 */
+#define PB11MPCORE_WATCHDOG0_BASE       0x1000F000 /* WATCHDOG 0 */
+#define PB11MPCORE_WATCHDOG1_BASE       0x10010000 /* WATCHDOG 1 */
+#define PB11MPCORE_TIMER01_BASE         0x10011000 /* TIMER 0-1 */
+#define PB11MPCORE_TIMER23_BASE         0x10012000 /* TIMER 2-3 */
+#define PB11MPCORE_RTC_BASE		0x10017000 /* RTC interface */
+#define PB11MPCORE_TIMER45_BASE         0x10018000 /* TIMER 4-5 */
+#define PB11MPCORE_TIMER67_BASE         0x10019000 /* TIMER 6-7 */
+#define PB11MPCORE_SYSCTRL1_BASE        0x1001A000 /* System controller 1 */
+#define PB11MPCORE_GIC0_BASE            0x1E000000 /* GIC 0 */
+#define PB11MPCORE_GIC1_BASE            0x1E010000 /* GIC 1 */
+#define PB11MPCORE_GIC2_BASE            0x1E020000 /* GIC 2 */
+#define PB11MPCORE_GIC3_BASE            0x1E030000 /* GIC 3 */
 
 /*
  * Uart virtual address until a file-based console access
@@ -44,17 +53,25 @@
  * device base address. Each page on this virtual base is consecutively
  * allocated to devices. Nice and smooth.
  */
-#define PB926_TIMER01_VOFFSET			0x00000000
-#define PB926_UART0_VOFFSET			0x00001000
-#define	PB926_VIC_VOFFSET			0x00002000
-#define	PB926_SIC_VOFFSET			0x00003000
-#define PB926_SYSREGS_VOFFSET			0x00005000
-#define PB926_SYSCTRL_VOFFSET			0x00006000
+#define PB11MPCORE_SYSREGS_VOFFSET	0x00000000
+#define PB11MPCORE_SYSCTRL0_VOFFSET	0x00001000
+#define PB11MPCORE_SYSCTRL1_VOFFSET	0x00002000
+#define PB11MPCORE_UART0_VOFFSET	0x00003000
+#define PB11MPCORE_TIMER01_VOFFSET	0x00004000
 
-#define PB926_UART0_VBASE			(IO_AREA0_VADDR + PB926_UART0_VOFFSET)
-#define PB926_TIMER01_VBASE			(IO_AREA0_VADDR + PB926_TIMER01_VOFFSET)
-#define PB926_SYSCTRL_VBASE			(IO_AREA0_VADDR + PB926_SYSCTRL_VOFFSET)
-#define PB926_VIC_VBASE				(IO_AREA0_VADDR + PB926_VIC_VOFFSET)
-#define PB926_SIC_VBASE				(IO_AREA0_VADDR + PB926_SIC_VOFFSET)
-#endif /* __PLATFORM_PB926_OFFSETS_H__ */
+#define PB11MPCORE_GIC0_VOFFSET		0x00005000
+#define PB11MPCORE_GIC1_VOFFSET         0x00006000
+#define PB11MPCORE_GIC2_VOFFSET         0x00007000
+#define PB11MPCORE_GIC3_VOFFSET         0x00008000
+#define PB11MPCORE_SYSREGS_VBASE	(IO_AREA0_VADDR + PB11MPCORE_SYSREGS_VOFFSET)
+#define PB11MPCORE_SYSCTRL0_VBASE	(IO_AREA0_VADDR + PB11MPCORE_SYSCTRL0_VOFFSET)
+#define PB11MPCORE_SYSCTRL1_VBASE       (IO_AREA0_VADDR + PB11MPCORE_SYSCTRL1_VOFFSET)
+#define PB11MPCORE_UART0_VBASE		(IO_AREA0_VADDR + PB11MPCORE_UART0_VOFFSET)
+#define PB11MPCORE_TIMER01_VBASE	(IO_AREA0_VADDR + PB11MPCORE_TIMER01_VOFFSET)
+#define PB11MPCORE_GIC0_VBASE           (IO_AREA0_VADDR + PB11MPCORE_GIC0_VOFFSET)
+#define PB11MPCORE_GIC1_VBASE           (IO_AREA0_VADDR + PB11MPCORE_GIC1_VOFFSET)
+#define PB11MPCORE_GIC2_VBASE           (IO_AREA0_VADDR + PB11MPCORE_GIC2_VOFFSET)
+#define PB11MPCORE_GIC3_VBASE           (IO_AREA0_VADDR + PB11MPCORE_GIC3_VOFFSET)
+
+#endif /* __PLATFORM_PB11MPCORE_OFFSETS_H__ */
 
diff --git a/include/l4/platform/pb11mpcore/platform.h b/include/l4/platform/pb11mpcore/platform.h
index dd4f4cb..76c8db4 100644
--- a/include/l4/platform/pb11mpcore/platform.h
+++ b/include/l4/platform/pb11mpcore/platform.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM_PB926_PLATFORM_H__
-#define __PLATFORM_PB926_PLATFORM_H__
+#ifndef __PLATFORM_PB11MPCORE_PLATFORM_H__
+#define __PLATFORM_PB11MPCORE_PLATFORM_H__
 /*
  * Platform specific ties between drivers and generic APIs used by the kernel.
  * E.g. system timer and console.
@@ -10,13 +10,25 @@
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
-#define PLATFORM_TIMER_BASE			PB926_TIMER01_VBASE
-#define PLATFORM_SP810_BASE			PB926_SYSCTRL_VBASE
-#define PLATFORM_IRQCTRL_BASE			PB926_VIC_VBASE
-#define PLATFORM_SIRQCTRL_BASE			PB926_SIC_VBASE
+#define PLATFORM_CONSOLE0_BASE			PB11MPCORE_UART0_VBASE
+#define PLATFORM_TIMER0_BASE			PB11MPCORE_TIMER01_VBASE
+/* Need to add syscntrl1 here */
+#define PLATFORM_SP810_BASE			PB11MPCORE_SYSCTRL0_VBASE
+
+/* Total number of timers present in this platform */
+#define	TOTAL_TIMERS			8
+
+#define PLATFORM_TIMER0	0
+#define PLATFORM_TIMER1	1
+#define PLATFORM_TIMER2	2
+#define PLATFORM_TIMER3	3
+#define PLATFORM_TIMER3	4
+#define PLATFORM_TIMER3	5
+#define PLATFORM_TIMER3	6
+#define PLATFORM_TIMER3	7
 
 void platform_irq_enable(int irq);
 void platform_irq_disable(int irq);
 void timer_start(void);
-#endif /* __PLATFORM_PB926_PLATFORM_H__ */
+
+#endif /* __PLATFORM_PB11MPCORE_PLATFORM_H__ */
diff --git a/include/l4/platform/pb11mpcore/printascii.h b/include/l4/platform/pb11mpcore/printascii.h
index 0d0be28..600866e 100644
--- a/include/l4/platform/pb11mpcore/printascii.h
+++ b/include/l4/platform/pb11mpcore/printascii.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM__PB926__PRINTASCII__H__
-#define __PLATFORM__PB926__PRINTASCII__H__
+#ifndef __PLATFORM__PB11MPCORE__PRINTASCII__H__
+#define __PLATFORM__PB11MPCORE__PRINTASCII__H__
 
 #define	dprintk(str, val)		\
 {					\
@@ -12,4 +12,4 @@
 void printascii(char *str);
 void printhex8(unsigned int);
 
-#endif /* __PLATFORM__PB926__PRINTASCII__H__ */
+#endif /* __PLATFORM__PB11MPCORE__PRINTASCII__H__ */
diff --git a/include/l4/platform/pb11mpcore/uart.h b/include/l4/platform/pb11mpcore/uart.h
index 366590f..fb37ce9 100644
--- a/include/l4/platform/pb11mpcore/uart.h
+++ b/include/l4/platform/pb11mpcore/uart.h
@@ -5,16 +5,16 @@
  *
  */
 
-#ifndef __PLATFORM_PB926_UART_H__
-#define __PLATFORM_PB926_UART_H__
+#ifndef __PLATFORM_PB11MPCORE_UART_H__
+#define __PLATFORM_PB11MPCORE_UART_H__
 
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
+#define PLATFORM_CONSOLE_BASE			PB11MPCORE_UART0_VBASE
 #include <l4/drivers/uart/pl011/pl011_uart.h>
 
 void uart_init(void);
 void uart_putc(char c);
 
-#endif /* __PLATFORM_PB926_UART_H__ */
+#endif /* __PLATFORM_PB11MPCORE_UART_H__ */
diff --git a/include/l4/platform/pba8/irq.h b/include/l4/platform/pba8/irq.h
index ecfad92..ac74940 100644
--- a/include/l4/platform/pba8/irq.h
+++ b/include/l4/platform/pba8/irq.h
@@ -1,27 +1,25 @@
 #ifndef __PLATFORM_IRQ_H__
 #define __PLATFORM_IRQ_H__
 
-#define IRQ_CHIPS_MAX				2
-#define IRQS_MAX				64
+/* TODO: Not sure about this, need to check */
+#define IRQ_CHIPS_MAX			4
+#define IRQS_MAX			96
 
-/* IRQ indices. */
-#define IRQ_TIMER01			4
-#define IRQ_TIMER23			5
-#define IRQ_RTC				10
-#define IRQ_UART0			12
-#define IRQ_UART1			13
-#define IRQ_UART2			14
-#define IRQ_SIC				31
-
-/* Cascading definitions */
-
-#define PIC_IRQS_MAX			31 /* Total irqs on PIC */
-/* The local irq line of the dummy peripheral on this chip */
-#define LOCALIRQ_DUMMY			15
-/* The irq index offset of this chip, is the maximum of previous chip + 1 */
-#define SIRQ_CHIP_OFFSET		(PIC_IRQS_MAX + 1)
-/* The global irq number of dummy is the local irq line + it's chip offset */
-#define IRQ_DUMMY			(LOCALIRQ_DUMMY + SIRQ_CHIP_OFFSET)
+/*
+ * IRQ indices, 32-63 and 72-89 index
+ * available for external sources
+ * 0-32: used for SI, provided by
+ * distributed interrupt controller
+ */
+#define IRQ_TIMER01			36
+#define IRQ_TIMER23			37
+#define IRQ_TIMER45                     73
+#define IRQ_TIMER67                     74
+#define IRQ_RTC				42
+#define IRQ_UART0			44
+#define IRQ_UART1			45
+#define IRQ_UART2			46
+#define IRQ_UART3                       47
 
 
 #endif /* __PLATFORM_IRQ_H__ */
diff --git a/include/l4/platform/pba8/offsets.h b/include/l4/platform/pba8/offsets.h
index 4a49729..483e988 100644
--- a/include/l4/platform/pba8/offsets.h
+++ b/include/l4/platform/pba8/offsets.h
@@ -4,12 +4,12 @@
  * Copyright (C) 2007 Bahadir Balban
  */
 
-#ifndef __PLATFORM_PB926_OFFSETS_H__
-#define __PLATFORM_PB926_OFFSETS_H__
+#ifndef __PLATFORM_PBA8_OFFSETS_H__
+#define __PLATFORM_PBA8_OFFSETS_H__
 
 /* Physical memory base */
 #define	PHYS_MEM_START			0x00000000 /* inclusive */
-#define	PHYS_MEM_END			0x08000000 /* 128 MB, exclusive */
+#define	PHYS_MEM_END			0x10000000 /* 256 MB, exclusive */
 
 /*
  * These bases taken from where kernel is `physically' linked at,
@@ -20,18 +20,27 @@
 #define	PHYS_ADDR_BASE			0x100000
 
 /* Device memory base */
-#define	PB926_DEV_PHYS			0x10000000
+#define	PBA8_DEV_PHYS			0x10000000
 
 /* Device offsets in physical memory */
-#define	PB926_SYSTEM_REGISTERS		0x10000000 /* System registers */
-#define	PB926_SYSCTRL_BASE		0x101E0000 /* System controller */
-#define	PB926_WATCHDOG_BASE		0x101E1000 /* Watchdog */
-#define	PB926_TIMER01_BASE		0x101E2000 /* Timers 0 and 1 */
-#define	PB926_TIMER23_BASE		0x101E3000 /* Timers 2 and 3 */
-#define	PB926_RTC_BASE			0x101E8000 /* Real Time Clock */
-#define	PB926_VIC_BASE			0x10140000 /* Primary Vectored IC */
-#define	PB926_SIC_BASE			0x10003000 /* Secondary IC */
-#define	PB926_UART0_BASE		0x101F1000 /* Console port (UART0) */
+#define	PBA8_SYSTEM_REGISTERS		0x10000000 /* System registers */
+#define	PBA8_SYSCTRL0_BASE		0x10001000 /* System controller 0 */
+#define PBA8_UART0_BASE           	0x10009000 /* UART 0 */
+#define PBA8_UART1_BASE           	0x1000A000 /* UART 1 */
+#define PBA8_UART2_BASE           	0x1000B000 /* UART 2 */
+#define PBA8_UART3_BASE           	0x1000C000 /* UART 3 */
+#define PBA8_WATCHDOG0_BASE       	0x1000F000 /* WATCHDOG 0 */
+#define PBA8_WATCHDOG1_BASE       	0x10010000 /* WATCHDOG 1 */
+#define PBA8_TIMER01_BASE         	0x10011000 /* TIMER 0-1 */
+#define PBA8_TIMER23_BASE         	0x10012000 /* TIMER 2-3 */
+#define PBA8_RTC_BASE			0x10017000 /* RTC interface */
+#define PBA8_TIMER45_BASE         	0x10018000 /* TIMER 4-5 */
+#define PBA8_TIMER67_BASE         	0x10019000 /* TIMER 6-7 */
+#define PBA8_SYSCTRL1_BASE        	0x1001A000 /* System controller 1 */
+#define PBA8_GIC0_BASE            	0x1E000000 /* GIC 0 */
+#define PBA8_GIC1_BASE            	0x1E010000 /* GIC 1 */
+#define PBA8_GIC2_BASE            	0x1E020000 /* GIC 2 */
+#define PBA8_GIC3_BASE            	0x1E030000 /* GIC 3 */
 
 /*
  * Uart virtual address until a file-based console access
@@ -44,17 +53,25 @@
  * device base address. Each page on this virtual base is consecutively
  * allocated to devices. Nice and smooth.
  */
-#define PB926_TIMER01_VOFFSET			0x00000000
-#define PB926_UART0_VOFFSET			0x00001000
-#define	PB926_VIC_VOFFSET			0x00002000
-#define	PB926_SIC_VOFFSET			0x00003000
-#define PB926_SYSREGS_VOFFSET			0x00005000
-#define PB926_SYSCTRL_VOFFSET			0x00006000
+#define PBA8_SYSREGS_VOFFSET	0x00000000
+#define PBA8_SYSCTRL0_VOFFSET	0x00001000
+#define PBA8_SYSCTRL1_VOFFSET	0x00002000
+#define PBA8_UART0_VOFFSET	0x00003000
+#define PBA8_TIMER01_VOFFSET	0x00004000
+#define PBA8_GIC0_VOFFSET	0x00005000
+#define PBA8_GIC1_VOFFSET       0x00006000
+#define PBA8_GIC2_VOFFSET       0x00007000
+#define PBA8_GIC3_VOFFSET       0x00008000
 
-#define PB926_UART0_VBASE			(IO_AREA0_VADDR + PB926_UART0_VOFFSET)
-#define PB926_TIMER01_VBASE			(IO_AREA0_VADDR + PB926_TIMER01_VOFFSET)
-#define PB926_SYSCTRL_VBASE			(IO_AREA0_VADDR + PB926_SYSCTRL_VOFFSET)
-#define PB926_VIC_VBASE				(IO_AREA0_VADDR + PB926_VIC_VOFFSET)
-#define PB926_SIC_VBASE				(IO_AREA0_VADDR + PB926_SIC_VOFFSET)
-#endif /* __PLATFORM_PB926_OFFSETS_H__ */
+#define PBA8_SYSREGS_VBASE	(IO_AREA0_VADDR + PBA8_SYSREGS_VOFFSET)
+#define PBA8_SYSCTRL0_VBASE	(IO_AREA0_VADDR + PBA8_SYSCTRL0_VOFFSET)
+#define PBA8_SYSCTRL1_VBASE     (IO_AREA0_VADDR + PBA8_SYSCTRL1_VOFFSET)
+#define PBA8_UART0_VBASE	(IO_AREA0_VADDR + PBA8_UART0_VOFFSET)
+#define PBA8_TIMER01_VBASE	(IO_AREA0_VADDR + PBA8_TIMER01_VOFFSET)
+#define PBA8_GIC0_VBASE         (IO_AREA0_VADDR + PBA8_GIC0_VOFFSET)
+#define PBA8_GIC1_VBASE         (IO_AREA0_VADDR + PBA8_GIC1_VOFFSET)
+#define PBA8_GIC2_VBASE         (IO_AREA0_VADDR + PBA8_GIC2_VOFFSET)
+#define PBA8_GIC3_VBASE         (IO_AREA0_VADDR + PBA8_GIC3_VOFFSET)
+
+#endif /* __PLATFORM_PBA8_OFFSETS_H__ */
 
diff --git a/include/l4/platform/pba8/platform.h b/include/l4/platform/pba8/platform.h
index dd4f4cb..c4b8736 100644
--- a/include/l4/platform/pba8/platform.h
+++ b/include/l4/platform/pba8/platform.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM_PB926_PLATFORM_H__
-#define __PLATFORM_PB926_PLATFORM_H__
+#ifndef __PLATFORM_PBA8_PLATFORM_H__
+#define __PLATFORM_PBA8_PLATFORM_H__
 /*
  * Platform specific ties between drivers and generic APIs used by the kernel.
  * E.g. system timer and console.
@@ -10,13 +10,23 @@
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
-#define PLATFORM_TIMER_BASE			PB926_TIMER01_VBASE
-#define PLATFORM_SP810_BASE			PB926_SYSCTRL_VBASE
-#define PLATFORM_IRQCTRL_BASE			PB926_VIC_VBASE
-#define PLATFORM_SIRQCTRL_BASE			PB926_SIC_VBASE
+#define PLATFORM_CONSOLE0_BASE			PBA8_UART0_VBASE
+#define PLATFORM_TIMER0_BASE			PBA8_TIMER01_VBASE
+#define PLATFORM_SP810_BASE			PBA8_SYSCTRL0_VBASE
+
+/* Total number of timers present in this platform */
+#define	TOTAL_TIMERS			8
+
+#define PLATFORM_TIMER0	0
+#define PLATFORM_TIMER1	1
+#define PLATFORM_TIMER2	2
+#define PLATFORM_TIMER3	3
+#define PLATFORM_TIMER3	4
+#define PLATFORM_TIMER3	5
+#define PLATFORM_TIMER3	6
+#define PLATFORM_TIMER3	7
 
 void platform_irq_enable(int irq);
 void platform_irq_disable(int irq);
 void timer_start(void);
-#endif /* __PLATFORM_PB926_PLATFORM_H__ */
+#endif /* __PLATFORM_PBA8_PLATFORM_H__ */
diff --git a/include/l4/platform/pba8/printascii.h b/include/l4/platform/pba8/printascii.h
index 0d0be28..d60aacc 100644
--- a/include/l4/platform/pba8/printascii.h
+++ b/include/l4/platform/pba8/printascii.h
@@ -1,5 +1,5 @@
-#ifndef __PLATFORM__PB926__PRINTASCII__H__
-#define __PLATFORM__PB926__PRINTASCII__H__
+#ifndef __PLATFORM__PBA8__PRINTASCII__H__
+#define __PLATFORM__PBA8__PRINTASCII__H__
 
 #define	dprintk(str, val)		\
 {					\
@@ -12,4 +12,4 @@
 void printascii(char *str);
 void printhex8(unsigned int);
 
-#endif /* __PLATFORM__PB926__PRINTASCII__H__ */
+#endif /* __PLATFORM__PBA8__PRINTASCII__H__ */
diff --git a/include/l4/platform/pba8/uart.h b/include/l4/platform/pba8/uart.h
index 366590f..3734ddf 100644
--- a/include/l4/platform/pba8/uart.h
+++ b/include/l4/platform/pba8/uart.h
@@ -5,13 +5,13 @@
  *
  */
 
-#ifndef __PLATFORM_PB926_UART_H__
-#define __PLATFORM_PB926_UART_H__
+#ifndef __PLATFORM_PBA8_UART_H__
+#define __PLATFORM_PBA8_UART_H__
 
 #include INC_PLAT(offsets.h)
 #include INC_GLUE(memlayout.h)
 
-#define PLATFORM_CONSOLE_BASE			PB926_UART0_VBASE
+#define PLATFORM_CONSOLE_BASE			PBA8_UART0_VBASE
 #include <l4/drivers/uart/pl011/pl011_uart.h>
 
 void uart_init(void);
diff --git a/src/platform/eb/irq.c b/src/platform/eb/irq.c
index 7b63abf..a1fae4b 100644
--- a/src/platform/eb/irq.c
+++ b/src/platform/eb/irq.c
@@ -41,7 +41,7 @@ struct irq_chip irq_chip_array[IRQ_CHIPS_MAX] = {
 
 static int platform_timer_handler(void)
 {
-	sp804_irq_handler();
+	sp804_irq_handler(PLATFORM_TIMER0_BASE);
 	return do_timer_irq();
 }
 
diff --git a/src/platform/eb/platform.c b/src/platform/eb/platform.c
index d59c955..fd98fca 100644
--- a/src/platform/eb/platform.c
+++ b/src/platform/eb/platform.c
@@ -1,5 +1,5 @@
 /*
- * PB926 platform-specific initialisation and setup
+ * EB platform-specific initialisation and setup
  *
  * Copyright (C) 2007 Bahadir Balban
  */
@@ -21,7 +21,7 @@
 
 void init_platform_console(void)
 {
-	add_boot_mapping(PB926_UART0_BASE, PL011_BASE, PAGE_SIZE,
+	add_boot_mapping(EB_UART0_BASE, PLATFORM_CONSOLE0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 
 	/*
@@ -29,7 +29,7 @@ void init_platform_console(void)
 	 * userspace printf can work. Note, this raw mapping is to be
 	 * removed in the future, when file-based io is implemented.
 	 */
-	add_boot_mapping(PB926_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
+	add_boot_mapping(EB_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
 		    MAP_USR_IO_FLAGS);
 
 	uart_init();
@@ -37,20 +37,22 @@ void init_platform_console(void)
 
 void init_platform_timer(void)
 {
-	add_boot_mapping(PB926_TIMER01_BASE, PLATFORM_TIMER_BASE, PAGE_SIZE,
+	add_boot_mapping(EB_TIMER01_BASE, PLATFORM_TIMER0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
-	add_boot_mapping(PB926_SYSCTRL_BASE,	PB926_SYSCTRL_VBASE, PAGE_SIZE,
+	add_boot_mapping(EB_SYSCTRL_BASE, PB926_SYSCTRL_VBASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	timer_init();
 }
 
 void init_platform_irq_controller()
 {
+#if 0
 	add_boot_mapping(PB926_VIC_BASE, PLATFORM_IRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	add_boot_mapping(PB926_SIC_BASE, PLATFORM_SIRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	irq_controllers_init();
+#endif
 }
 
 void platform_init(void)
diff --git a/src/platform/eb/printascii.S b/src/platform/eb/printascii.S
index e727537..6aaa574 100644
--- a/src/platform/eb/printascii.S
+++ b/src/platform/eb/printascii.S
@@ -3,19 +3,24 @@
  */
 #include INC_ARCH(asm.h)
 #include INC_GLUE(memlayout.h)
+#include INC_PLAT(offsets.h)
+#include INC_SUBARCH(mm.h)
 
 #define UART_DATA_OFFSET		0x0
 
+/* Physical base address of UART0 */
+uart0_phys_base_addr:
+	.word   EB_UART0_BASE
+
+/* Virtual base address of UART0 */
+uart0_virtual_base_addr:
+	.word   EB_UART0_VBASE
+
 	.macro uart_address rx
 	mrc	p15, 0, \rx, c1, c0
 	tst	\rx, #1		@ MMU enabled?
-	moveq	\rx, #0x10000000
-	orreq	\rx, \rx, #0x001F0000
-	orreq	\rx, \rx, #0x00001000
-	/* FIXME: This offset is incorrect */
-	movne	\rx,      #0xf9000000 @#IO_AREA0_VADDR
-	addne	\rx, \rx, #PB926_UART0_VOFFSET	@ UART0 page offset from
-						@ virtual io area base.
+	moveq	\rx, #uart0_phys_base_addr
+	movne	\rx, #uart0_virtual_base_addr
 	.endm
 
 	.macro uart_send, ry, rx
diff --git a/src/platform/eb/timer.c b/src/platform/eb/timer.c
index fc290af..477bbea 100644
--- a/src/platform/eb/timer.c
+++ b/src/platform/eb/timer.c
@@ -13,16 +13,17 @@
 void timer_init(void)
 {
 	/* Set timer 0 to 1MHz */
-	sp810_set_timclk(0, 1);
+	sp810_set_timclk(PLATFORM_TIMER0, 1);
 
 	/* Initialise timer */
-	sp804_init();
+	sp804_init(PLATFORM_TIMER0_BASE, SP804_TIMER_RUNMODE_PERIODIC, \
+		   SP804_TIMER_WRAPMODE_WRAPPING, SP804_TIMER_WIDTH32BIT, \
+		   SP804_TIMER_IRQENABLE);
 }
 
 void timer_start(void)
 {
 	irq_enable(IRQ_TIMER01);
-	sp804_set_irq(0, 1);	/* Enable timer0 irq */
-	sp804_enable(0, 1);	/* Enable timer0 */
+	sp804_enable(PLATFORM_TIMER0_BASE, 1);	/* Enable timer0 */
 }
 
diff --git a/src/platform/eb/uart.c b/src/platform/eb/uart.c
index 35d94f5..ae1fd76 100644
--- a/src/platform/eb/uart.c
+++ b/src/platform/eb/uart.c
@@ -12,8 +12,9 @@ extern struct pl011_uart uart;
 
 void uart_init()
 {
-	uart.base = PL011_BASE;
-	uart.ops.initialise(&uart);
+	/* We are using UART0 for kernel */
+	uart.base = PLATFORM_CONSOLE0_BASE;
+	pl011_initialise_device(&uart);
 }
 
 /* Generic uart function that lib/putchar.c expects to see implemented */
@@ -22,7 +23,7 @@ void uart_putc(char c)
 	int res;
 	/* Platform specific uart implementation */
 	do {
-		res = uart.ops.tx_char(c);
+		res = pl011_tx_char(uart.base, c);
 	} while (res < 0);
 }
 
diff --git a/src/platform/pb11mpcore/irq.c b/src/platform/pb11mpcore/irq.c
index 7b63abf..a1fae4b 100644
--- a/src/platform/pb11mpcore/irq.c
+++ b/src/platform/pb11mpcore/irq.c
@@ -41,7 +41,7 @@ struct irq_chip irq_chip_array[IRQ_CHIPS_MAX] = {
 
 static int platform_timer_handler(void)
 {
-	sp804_irq_handler();
+	sp804_irq_handler(PLATFORM_TIMER0_BASE);
 	return do_timer_irq();
 }
 
diff --git a/src/platform/pb11mpcore/platform.c b/src/platform/pb11mpcore/platform.c
index d59c955..eab404a 100644
--- a/src/platform/pb11mpcore/platform.c
+++ b/src/platform/pb11mpcore/platform.c
@@ -1,5 +1,5 @@
 /*
- * PB926 platform-specific initialisation and setup
+ * PB11MPCORE platform-specific initialisation and setup
  *
  * Copyright (C) 2007 Bahadir Balban
  */
@@ -21,7 +21,7 @@
 
 void init_platform_console(void)
 {
-	add_boot_mapping(PB926_UART0_BASE, PL011_BASE, PAGE_SIZE,
+	add_boot_mapping(PB11MPCORE_UART0_BASE, PLATFORM_CONSOLE0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 
 	/*
@@ -29,7 +29,7 @@ void init_platform_console(void)
 	 * userspace printf can work. Note, this raw mapping is to be
 	 * removed in the future, when file-based io is implemented.
 	 */
-	add_boot_mapping(PB926_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
+	add_boot_mapping(PBMPCORE_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
 		    MAP_USR_IO_FLAGS);
 
 	uart_init();
@@ -37,20 +37,23 @@ void init_platform_console(void)
 
 void init_platform_timer(void)
 {
-	add_boot_mapping(PB926_TIMER01_BASE, PLATFORM_TIMER_BASE, PAGE_SIZE,
+	add_boot_mapping(PBMPCORE_TIMER01_BASE, PLATFORM_TIMER0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
-	add_boot_mapping(PB926_SYSCTRL_BASE,	PB926_SYSCTRL_VBASE, PAGE_SIZE,
+	add_boot_mapping(PB926_SYSCTRL_BASE,	PB926_SYSCTRL0_VBASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
+	/* TODO: SYSCTRL1 mapping may be needed */
 	timer_init();
 }
 
 void init_platform_irq_controller()
 {
+#if 0
 	add_boot_mapping(PB926_VIC_BASE, PLATFORM_IRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	add_boot_mapping(PB926_SIC_BASE, PLATFORM_SIRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	irq_controllers_init();
+#endif
 }
 
 void platform_init(void)
diff --git a/src/platform/pb11mpcore/printascii.S b/src/platform/pb11mpcore/printascii.S
index e727537..25e6260 100644
--- a/src/platform/pb11mpcore/printascii.S
+++ b/src/platform/pb11mpcore/printascii.S
@@ -3,19 +3,24 @@
  */
 #include INC_ARCH(asm.h)
 #include INC_GLUE(memlayout.h)
+#include INC_PLAT(offsets.h)
+#include INC_SUBARCH(mm.h)
 
 #define UART_DATA_OFFSET		0x0
 
+/* Physical base address of UART0 */
+uart0_phys_base_addr:
+	.word   PB11MPCORE_UART0_BASE
+
+/* Virtual base address of UART0 */
+uart0_virtual_base_addr:
+	.word   PB11MPCORE_UART0_VBASE
+
 	.macro uart_address rx
 	mrc	p15, 0, \rx, c1, c0
 	tst	\rx, #1		@ MMU enabled?
-	moveq	\rx, #0x10000000
-	orreq	\rx, \rx, #0x001F0000
-	orreq	\rx, \rx, #0x00001000
-	/* FIXME: This offset is incorrect */
-	movne	\rx,      #0xf9000000 @#IO_AREA0_VADDR
-	addne	\rx, \rx, #PB926_UART0_VOFFSET	@ UART0 page offset from
-						@ virtual io area base.
+	moveq	\rx, #uart0_phys_base_addr
+	movne	\rx, #uart0_virtual_base_addr
 	.endm
 
 	.macro uart_send, ry, rx
diff --git a/src/platform/pb11mpcore/timer.c b/src/platform/pb11mpcore/timer.c
index fc290af..85ae3d8 100644
--- a/src/platform/pb11mpcore/timer.c
+++ b/src/platform/pb11mpcore/timer.c
@@ -13,16 +13,18 @@
 void timer_init(void)
 {
 	/* Set timer 0 to 1MHz */
-	sp810_set_timclk(0, 1);
+	sp810_set_timclk(PLATFORM_TIMER0_BASE, 1);
 
 	/* Initialise timer */
-	sp804_init();
+	sp804_init(PLATFORM_TIMER0_BASE, SP804_TIMER_RUNMODE_PERIODIC, \
+		   SP804_TIMER_WRAPMODE_WRAPPING, SP804_TIMER_WIDTH32BIT, \
+		   SP804_TIMER_IRQENABLE);
+
 }
 
 void timer_start(void)
 {
 	irq_enable(IRQ_TIMER01);
-	sp804_set_irq(0, 1);	/* Enable timer0 irq */
-	sp804_enable(0, 1);	/* Enable timer0 */
+	sp804_enable(PLATFORM_TIMER0_BASE, 1);	/* Enable timer0 */
 }
 
diff --git a/src/platform/pb11mpcore/uart.c b/src/platform/pb11mpcore/uart.c
index 35d94f5..ae1fd76 100644
--- a/src/platform/pb11mpcore/uart.c
+++ b/src/platform/pb11mpcore/uart.c
@@ -12,8 +12,9 @@ extern struct pl011_uart uart;
 
 void uart_init()
 {
-	uart.base = PL011_BASE;
-	uart.ops.initialise(&uart);
+	/* We are using UART0 for kernel */
+	uart.base = PLATFORM_CONSOLE0_BASE;
+	pl011_initialise_device(&uart);
 }
 
 /* Generic uart function that lib/putchar.c expects to see implemented */
@@ -22,7 +23,7 @@ void uart_putc(char c)
 	int res;
 	/* Platform specific uart implementation */
 	do {
-		res = uart.ops.tx_char(c);
+		res = pl011_tx_char(uart.base, c);
 	} while (res < 0);
 }
 
diff --git a/src/platform/pb926/printascii.S b/src/platform/pb926/printascii.S
index e727537..f940749 100644
--- a/src/platform/pb926/printascii.S
+++ b/src/platform/pb926/printascii.S
@@ -3,19 +3,24 @@
  */
 #include INC_ARCH(asm.h)
 #include INC_GLUE(memlayout.h)
+#include INC_PLAT(offsets.h)
+#include INC_SUBARCH(mm.h)
 
 #define UART_DATA_OFFSET		0x0
 
+/* Physical base address of UART0 */
+uart0_phys_base_addr:
+	.word	PB926_UART0_BASE
+
+/* Virtual base address of UART0 */
+uart0_virtual_base_addr:
+	.word 	PB926_UART0_VBASE
+
 	.macro uart_address rx
 	mrc	p15, 0, \rx, c1, c0
 	tst	\rx, #1		@ MMU enabled?
-	moveq	\rx, #0x10000000
-	orreq	\rx, \rx, #0x001F0000
-	orreq	\rx, \rx, #0x00001000
-	/* FIXME: This offset is incorrect */
-	movne	\rx,      #0xf9000000 @#IO_AREA0_VADDR
-	addne	\rx, \rx, #PB926_UART0_VOFFSET	@ UART0 page offset from
-						@ virtual io area base.
+	moveq	\rx, #uart0_phys_base_addr
+	movne	\rx, #uart0_virtual_base_addr
 	.endm
 
 	.macro uart_send, ry, rx
diff --git a/src/platform/pb926/uart.c b/src/platform/pb926/uart.c
index b350388..ae1fd76 100644
--- a/src/platform/pb926/uart.c
+++ b/src/platform/pb926/uart.c
@@ -23,7 +23,7 @@ void uart_putc(char c)
 	int res;
 	/* Platform specific uart implementation */
 	do {
-		res =pl011_tx_char(uart.base, c);
+		res = pl011_tx_char(uart.base, c);
 	} while (res < 0);
 }
 
diff --git a/src/platform/pba8/irq.c b/src/platform/pba8/irq.c
index 7b63abf..a1fae4b 100644
--- a/src/platform/pba8/irq.c
+++ b/src/platform/pba8/irq.c
@@ -41,7 +41,7 @@ struct irq_chip irq_chip_array[IRQ_CHIPS_MAX] = {
 
 static int platform_timer_handler(void)
 {
-	sp804_irq_handler();
+	sp804_irq_handler(PLATFORM_TIMER0_BASE);
 	return do_timer_irq();
 }
 
diff --git a/src/platform/pba8/platform.c b/src/platform/pba8/platform.c
index d59c955..82f507b 100644
--- a/src/platform/pba8/platform.c
+++ b/src/platform/pba8/platform.c
@@ -1,5 +1,5 @@
 /*
- * PB926 platform-specific initialisation and setup
+ * PBA8 platform-specific initialisation and setup
  *
  * Copyright (C) 2007 Bahadir Balban
  */
@@ -21,7 +21,7 @@
 
 void init_platform_console(void)
 {
-	add_boot_mapping(PB926_UART0_BASE, PL011_BASE, PAGE_SIZE,
+	add_boot_mapping(PBA8_UART0_BASE, PLATFORM_CONSOLE0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 
 	/*
@@ -29,7 +29,7 @@ void init_platform_console(void)
 	 * userspace printf can work. Note, this raw mapping is to be
 	 * removed in the future, when file-based io is implemented.
 	 */
-	add_boot_mapping(PB926_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
+	add_boot_mapping(PBA8_UART0_BASE, USERSPACE_UART_BASE, PAGE_SIZE,
 		    MAP_USR_IO_FLAGS);
 
 	uart_init();
@@ -37,20 +37,23 @@ void init_platform_console(void)
 
 void init_platform_timer(void)
 {
-	add_boot_mapping(PB926_TIMER01_BASE, PLATFORM_TIMER_BASE, PAGE_SIZE,
+	add_boot_mapping(PBA8_TIMER01_BASE, PLATFORM_TIMER0_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
-	add_boot_mapping(PB926_SYSCTRL_BASE,	PB926_SYSCTRL_VBASE, PAGE_SIZE,
+	add_boot_mapping(PBA8_SYSCTRL_BASE, PB926_SYSCTRL0_VBASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
+	/* TODO: May need mapping for SYSCTRL1 */
 	timer_init();
 }
 
 void init_platform_irq_controller()
 {
+#if 0
 	add_boot_mapping(PB926_VIC_BASE, PLATFORM_IRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	add_boot_mapping(PB926_SIC_BASE, PLATFORM_SIRQCTRL_BASE, PAGE_SIZE,
 		    MAP_IO_DEFAULT_FLAGS);
 	irq_controllers_init();
+#endif
 }
 
 void platform_init(void)
diff --git a/src/platform/pba8/printascii.S b/src/platform/pba8/printascii.S
index e727537..2d88e10 100644
--- a/src/platform/pba8/printascii.S
+++ b/src/platform/pba8/printascii.S
@@ -3,19 +3,24 @@
  */
 #include INC_ARCH(asm.h)
 #include INC_GLUE(memlayout.h)
+#include INC_PLAT(offsets.h)
+#include INC_SUBARCH(mm.h)
 
 #define UART_DATA_OFFSET		0x0
 
+/* Physical base address of UART0 */
+uart0_phys_base_addr:
+	.word   PBA8_UART0_BASE
+
+/* Virtual base address of UART0 */
+uart0_virtual_base_addr:
+	.word   PBA8_UART0_VBASE
+
 	.macro uart_address rx
 	mrc	p15, 0, \rx, c1, c0
 	tst	\rx, #1		@ MMU enabled?
-	moveq	\rx, #0x10000000
-	orreq	\rx, \rx, #0x001F0000
-	orreq	\rx, \rx, #0x00001000
-	/* FIXME: This offset is incorrect */
-	movne	\rx,      #0xf9000000 @#IO_AREA0_VADDR
-	addne	\rx, \rx, #PB926_UART0_VOFFSET	@ UART0 page offset from
-						@ virtual io area base.
+	moveq	\rx, #uart0_phys_base_addr
+	movne	\rx, #uart0_virtual_base_addr
 	.endm
 
 	.macro uart_send, ry, rx
diff --git a/src/platform/pba8/timer.c b/src/platform/pba8/timer.c
index fc290af..0ec384b 100644
--- a/src/platform/pba8/timer.c
+++ b/src/platform/pba8/timer.c
@@ -13,16 +13,18 @@
 void timer_init(void)
 {
 	/* Set timer 0 to 1MHz */
-	sp810_set_timclk(0, 1);
+	sp810_set_timclk(PLATFORM_TIMER0, 1);
 
 	/* Initialise timer */
-	sp804_init();
+	sp804_init(PLATFORM_TIMER0_BASE, SP804_TIMER_RUNMODE_PERIODIC, \
+		   SP804_TIMER_WRAPMODE_WRAPPING, SP804_TIMER_WIDTH32BIT, \
+		   SP804_TIMER_IRQENABLE);
+
 }
 
 void timer_start(void)
 {
 	irq_enable(IRQ_TIMER01);
-	sp804_set_irq(0, 1);	/* Enable timer0 irq */
-	sp804_enable(0, 1);	/* Enable timer0 */
+	sp804_enable(PLATFORM_TIMER0, 1);	/* Enable timer0 */
 }
 
diff --git a/src/platform/pba8/uart.c b/src/platform/pba8/uart.c
index 35d94f5..ae1fd76 100644
--- a/src/platform/pba8/uart.c
+++ b/src/platform/pba8/uart.c
@@ -12,8 +12,9 @@ extern struct pl011_uart uart;
 
 void uart_init()
 {
-	uart.base = PL011_BASE;
-	uart.ops.initialise(&uart);
+	/* We are using UART0 for kernel */
+	uart.base = PLATFORM_CONSOLE0_BASE;
+	pl011_initialise_device(&uart);
 }
 
 /* Generic uart function that lib/putchar.c expects to see implemented */
@@ -22,7 +23,7 @@ void uart_putc(char c)
 	int res;
 	/* Platform specific uart implementation */
 	do {
-		res = uart.ops.tx_char(c);
+		res = pl011_tx_char(uart.base, c);
 	} while (res < 0);
 }