diff --git a/common/hw-gfx-gma-connector_info.ads b/common/hw-gfx-gma-connector_info.ads
index 0de8ba0..171b558 100644
--- a/common/hw-gfx-gma-connector_info.ads
+++ b/common/hw-gfx-gma-connector_info.ads
@@ -26,14 +26,18 @@
    procedure Preferred_Link_Setting
      (Port_Cfg : in out Port_Config;
       Success  :    out Boolean)
-      with
-         Post => (Port_Cfg.Port = Port_Cfg.Port'Old);
+   with
+      Post =>
+         Port_Cfg.Port = Port_Cfg.Port'Old and
+         Port_Cfg.Mode = Port_Cfg.Mode'Old;
 
    procedure Next_Link_Setting
      (Port_Cfg : in out Port_Config;
       Success  :    out Boolean)
-      with
-         Post => (Port_Cfg.Port = Port_Cfg.Port'Old);
+   with
+      Post =>
+         Port_Cfg.Port = Port_Cfg.Port'Old and
+         Port_Cfg.Mode = Port_Cfg.Mode'Old;
 
    function Default_BPC (Port_Cfg : Port_Config) return BPC_Type;
 
diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index b51795b..e1960ce 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -21,7 +21,6 @@
 
 use type HW.Word64;
 use type HW.Pos16;
-use type HW.Int32;
 use type HW.GFX.GMA.Registers.Registers_Invalid_Index;
 
 package body HW.GFX.GMA.Pipe_Setup is
diff --git a/common/hw-gfx-gma-pipe_setup.ads b/common/hw-gfx-gma-pipe_setup.ads
index 42bd85d..b696934 100644
--- a/common/hw-gfx-gma-pipe_setup.ads
+++ b/common/hw-gfx-gma-pipe_setup.ads
@@ -14,6 +14,8 @@
 
 with HW.GFX.GMA.Registers;
 
+use type HW.Int32;
+
 private package HW.GFX.GMA.Pipe_Setup
 is
 
@@ -29,7 +31,11 @@
      (Controller  : Controller_Type;
       Head        : Head_Type;
       Port_Cfg    : Port_Config;
-      Framebuffer : Framebuffer_Type);
+      Framebuffer : Framebuffer_Type)
+   with
+      Pre =>
+         Framebuffer.Width <= Pos32 (Port_Cfg.Mode.H_Visible) and
+         Framebuffer.Height <= Pos32 (Port_Cfg.Mode.V_Visible);
 
    procedure Off
      (Controller : Controller_Type;
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 691b775..f8b0e7b 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -150,7 +150,8 @@
    procedure Configure_FDI_Link
      (Port_Cfg : in out Port_Config;
       Success  :    out Boolean)
-   with Pre => True
+   with
+      Post => Port_Cfg.Mode = Port_Cfg.Mode'Old
    is
       procedure Limit_Lane_Count
       is
@@ -182,7 +183,11 @@
       Port_Cfg    : Port_Config;
       I           : Config_Index)
       return Boolean
-   with Global => null
+   with
+      Post =>
+        (if Validate_Config'Result then
+            Framebuffer.Width <= Pos32 (Port_Cfg.Mode.H_Visible) and
+            Framebuffer.Height <= Pos32 (Port_Cfg.Mode.V_Visible))
    is
    begin
       -- No downscaling
@@ -576,7 +581,9 @@
                end if;
 
                while Success loop
-                  pragma Loop_Invariant (New_Config.Port in Active_Port_Type);
+                  pragma Loop_Invariant
+                    (New_Config.Port in Active_Port_Type and
+                     Port_Cfg.Mode = Port_Cfg.Mode'Loop_Entry);
 
                   PLLs.Alloc
                     (Port_Cfg => Port_Cfg,