--- src/kernel/sel4/include/plat/pc99/plat/machine.h
+++ src/kernel/sel4/include/plat/pc99/plat/machine.h
@@ -51,8 +51,11 @@ typedef enum _irq_t {
 #define BIOS_PADDR_END   0x100000
 
 #define BIOS_PADDR_VIDEO_RAM_START 0x000A0000
+#define BIOS_PADDR_VIDEO_RAM_END   0x000B0000
 /* The text mode framebuffer exists part way into the video ram region */
 #define BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START 0x000B8000
 #define BIOS_PADDR_IVDEO_RAM_END 0x000C0000
+#define BIOS_PADDR_VIDEO_BIOS_START 0x000C0000
+#define BIOS_PADDR_VIDEO_BIOS_END   0x000CF000
 
 #endif
--- src/kernel/sel4/src/arch/x86/kernel/boot_sys.c
+++ src/kernel/sel4/src/arch/x86/kernel/boot_sys.c
@@ -286,6 +286,40 @@ add_mem_p_regs(p_region_t reg)
 }
 
 /*
+ * Checks whether there are overlaps between the area _reg_ and _trim_area_.
+ * If there are overlaps, trim the _trim_area_ and if there is some rest left,
+ * store it in _tail_.
+ */
+static BOOT_CODE void
+trim_region(p_region_t *reg, p_region_t *trim_area, p_region_t *tail, bool_t add)
+{
+    bool_t const inside_start = trim_area->start <= reg->start && reg->start < trim_area->end;
+    bool_t const inside_end   = trim_area->start < reg->end && reg->end <= trim_area->end;
+
+    if (reg->start >= reg->end)
+        return;
+
+    /* trim BIOS area if we detect overlaps */
+    if (!inside_start && !inside_end &&
+        (reg->start <= trim_area->start && trim_area->start < reg->end))
+        trim_area->start = trim_area->end;
+    else
+    if (inside_start && inside_end) {
+        tail->start = reg->end;
+        tail->end   = trim_area->end;
+        trim_area->end = reg->start;
+    } else {
+        if (inside_start)
+            trim_area->end = reg->start;
+        if (inside_end)
+            trim_area->start = reg->end;
+    }
+
+    if (add)
+        insert_dev_p_reg(*reg);
+}
+
+/*
  * the code relies that the GRUB provides correct information
  * about the actual physical memory regions.
  */
@@ -295,9 +329,17 @@ parse_mem_map(uint32_t mmap_length, uint32_t mmap_addr)
     multiboot_mmap_t *mmap = (multiboot_mmap_t *)((word_t)mmap_addr);
     printf("Parsing GRUB physical memory map\n");
 
+    /*
+     * Legacy regions required by ACPI driver, VESA driver and graphic drivers
+     * (Intel)
+     */
+    p_region_t legacy_area = { .start = BIOS_PADDR_VIDEO_RAM_START, .end = BIOS_PADDR_END };
+    /* optimistic approach that the area splits at most only one time ;-( */
+    p_region_t legacy_split = { .start = 0, .end = 0 };
+
     while ((word_t)mmap < (word_t)(mmap_addr + mmap_length)) {
-        uint64_t mem_start = mmap->base_addr;
-        uint64_t mem_length = mmap->length;
+        uint64_t mem_start = mmap->base_addr & ~0xFFFUL;
+        uint64_t mem_length = (mmap->length + (mmap->base_addr & 0xFFFUL)) & ~0xFFFUL;
         uint32_t type = mmap->type;
         if (mem_start != (uint64_t)(word_t)mem_start) {
             printf("\tPhysical memory region not addressable\n");
@@ -308,9 +350,38 @@ parse_mem_map(uint32_t mmap_length, uint32_t mmap_addr)
                     mem_start, mem_start + mem_length
                 });
             }
+            if (type == MULTIBOOT_MMAP_RESERVED_TYPE ||
+                type == MULTIBOOT_MMAP_ACPI_TYPE ||
+                type == MULTIBOOT_MMAP_ACPI_NVS_TYPE) {
+
+                p_region_t reg = { .start = mem_start, .end = mem_start + mem_length};
+                p_region_t tail = { .start = 0, .end = 0 };
+
+                trim_region(&reg, &legacy_area, &tail, true);
+                if (tail.start < tail.end) {
+                    assert(!(legacy_split.start < legacy_split.end));
+                    legacy_split = tail;
+                }
+
+                tail.start = 0; tail.end = 0;
+                trim_region(&reg, &legacy_split, &tail, false);
+                if (tail.start < tail.end) {
+                    assert(!(legacy_split.start < legacy_split.end));
+                    legacy_split = tail;
+                }
+            }
         }
         mmap++;
     }
+
+    /* first physical page - required by acpi drivers and vesa drivers */
+    insert_dev_p_reg((p_region_t) { .start = 0, .end = 0x1000 });
+
+    /* legacy area - required by acpi drivers */
+    if (legacy_area.start < legacy_area.end) {
+        insert_dev_p_reg(legacy_area);
+        insert_dev_p_reg(legacy_split);
+    }
 }
 
 static BOOT_CODE bool_t
@@ -349,6 +420,9 @@ try_boot_sys(
     /* copy CPU bootup code to lower memory */
     memcpy((void*)BOOT_NODE_PADDR, boot_cpu_start, boot_cpu_end - boot_cpu_start);
 
+    /* Prepare for accepting device regions from here on */
+    boot_state.dev_p_regs.count = 0;
+
     boot_state.mem_p_regs.count = 0;
     if (mbi->flags & MULTIBOOT_INFO_MMAP_FLAG) {
         parse_mem_map(mbi->mmap_length, mbi->mmap_addr);
@@ -378,9 +452,6 @@ try_boot_sys(
         pic_disable();
     }
 
-    /* Prepare for accepting device regions from here on */
-    boot_state.dev_p_regs.count = 0;
-
     /* get ACPI root table */
     acpi_rsdt = acpi_init();
     if (!acpi_rsdt) {
--- src/kernel/sel4/src/plat/pc99/machine/hardware.c
+++ src/kernel/sel4/src/plat/pc99/machine/hardware.c
@@ -26,11 +26,6 @@ void platAddDevices(void)
     /* discover PCI devices and their regions */
     /* pci_scan() calls insert_dev_p_reg() for each device region */
     pci_scan();
-    /* Add the text mode (EGA) frame buffer. 1 frame is enough for the
-     * standard 80x25 text mode. This whole thing is a bit of a hack */
-    insert_dev_p_reg( (p_region_t) {
-        BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START, BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START + 0x1000
-    } );
 }
 
 /* ============================== interrupts/IRQs ============================== */