diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index a17a1ac..dae8d27 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -437,19 +437,17 @@
       Registers.Write_GTT (GTT_Page, Device_Address, Valid);
    end Write_GTT;
 
-   procedure Setup_Default_GTT (FB : Framebuffer_Type; Phys_FB : Word32)
+   procedure Setup_Default_GTT (FB : Framebuffer_Type; Phys_Base : Word32)
    is
-      FB_Size : constant Pos32 :=
-         FB.Stride * FB.Height * Pos32 (((FB.BPC * 4) / 8));
-      Phys_Addr : GTT_Address_Type := GTT_Address_Type (Phys_FB);
+      Phys_Addr : GTT_Address_Type :=
+         GTT_Address_Type (Phys_Base) + GTT_Address_Type (FB.Offset);
    begin
-      for Idx in GTT_Range range 0 .. GTT_Range (((FB_Size + 4095) / 4096) - 1)
-      loop
+      for Idx in FB_First_Page (FB) .. FB_Last_Page (FB) loop
          Registers.Write_GTT
            (GTT_Page       => Idx,
             Device_Address => Phys_Addr,
             Valid          => True);
-         Phys_Addr := Phys_Addr + 4096;
+         Phys_Addr := Phys_Addr + GTT_Page_Size;
       end loop;
    end Setup_Default_GTT;
 
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 75dde9e..a91c83b 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -1,5 +1,6 @@
 --
 -- Copyright (C) 2015-2017 secunet Security Networks AG
+-- Copyright (C) 2017 Nico Huber <nico.h@gmx.de>
 --
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -12,6 +13,7 @@
 -- GNU General Public License for more details.
 --
 
+with HW.Config;
 with HW.Time;
 with HW.Port_IO;
 
@@ -84,14 +86,40 @@
                     Reason => "It's only used for debugging");
    procedure Dump_Configs (Configs : Pipe_Configs);
 
+   GTT_Page_Size : constant := 4096;
    type GTT_Address_Type is mod 2 ** 39;
-   type GTT_Range is range 0 .. 16#8_0000# - 1;
+   subtype GTT_Range is Natural range 0 .. 16#8_0000# - 1;
    procedure Write_GTT
      (GTT_Page       : GTT_Range;
       Device_Address : GTT_Address_Type;
       Valid          : Boolean);
 
-   procedure Setup_Default_GTT (FB : Framebuffer_Type; Phys_FB : Word32);
+   ----------------------------------------------------------------------------
+
+   function FB_First_Page (FB : Framebuffer_Type) return Natural is
+     (Natural (FB.Offset / GTT_Page_Size));
+   function FB_Pages (FB : Framebuffer_Type) return Natural is
+     (Natural (Div_Round_Up (FB_Size (FB), GTT_Page_Size)));
+   function FB_Last_Page (FB : Framebuffer_Type) return Natural is
+     (FB_First_Page (FB) + FB_Pages (FB) - 1);
+
+   -- Check basics and that it fits in GTT
+   function Valid_FB (FB : Framebuffer_Type) return Boolean is
+     (FB.Width <= FB.Stride and FB_Last_Page (FB) <= GTT_Range'Last);
+
+   -- Also check that we don't overflow the GTT's 39-bit space
+   -- (always true with a 32-bit base)
+   function Valid_Phys_FB (FB : Framebuffer_Type; Phys_Base : Word32)
+      return Boolean is
+     (Valid_FB (FB) and
+      Int64 (Phys_Base) + Int64 (FB.Offset) + Int64 (FB_Size (FB)) <=
+         Int64 (GTT_Address_Type'Last))
+   with
+      Ghost;
+
+   procedure Setup_Default_GTT (FB : Framebuffer_Type; Phys_Base : Word32)
+   with
+      Pre => Is_Initialized and Valid_Phys_FB (FB, Phys_Base);
 
 private
 
diff --git a/common/hw-gfx.ads b/common/hw-gfx.ads
index 051b326..daf648d 100644
--- a/common/hw-gfx.ads
+++ b/common/hw-gfx.ads
@@ -1,5 +1,6 @@
 --
 -- Copyright (C) 2015-2016 secunet Security Networks AG
+-- Copyright (C) 2017 Nico Huber <nico.h@gmx.de>
 --
 -- This program is free software; you can redistribute it and/or modify
 -- it under the terms of the GNU General Public License as published by
@@ -35,6 +36,9 @@
       Offset : Word32;
    end record;
 
+   function FB_Size (FB : Framebuffer_Type) return Pos32 is
+     (FB.Stride * FB.Height * Pos32 (FB.BPC) / (8 / 4));
+
    Default_FB : constant Framebuffer_Type := Framebuffer_Type'
       (Width  => 1,
        Height => 1,