diff --git a/common/hw-gfx-gma-registers.adb b/common/hw-gfx-gma-registers.adb
index 9b14a3b..838afed 100644
--- a/common/hw-gfx-gma-registers.adb
+++ b/common/hw-gfx-gma-registers.adb
@@ -69,7 +69,7 @@
       Index_T     => GTT_Range,
       Array_T     => GTT_Registers_64);
 
-   GTT_PTE_Valid : constant Word32 := 1;
+   GTT_PTE_Valid : constant := 1;
 
    ----------------------------------------------------------------------------
 
@@ -174,6 +174,33 @@
       end if;
    end Write_GTT;
 
+   procedure Read_GTT
+     (Device_Address :    out GTT_Address_Type;
+      Valid          :    out Boolean;
+      GTT_Page       : in     GTT_Range)
+   is
+   begin
+      if not Config.Has_64bit_GTT then
+         declare
+            PTE : GTT_PTE_32;
+         begin
+            GTT_32.Read (PTE, GTT_Page);
+            Valid := (PTE and GTT_PTE_Valid) /= 0;
+            Device_Address := GTT_Address_Type
+              (Shift_Left (Word64 (PTE and 16#07f0#), 32 - 4) or
+               Word64 (PTE and 16#ffff_f000#));
+         end;
+      else
+         declare
+            PTE : GTT_PTE_64;
+         begin
+            GTT_64.Read (PTE, GTT_Page);
+            Valid := (PTE and GTT_PTE_Valid) /= 0;
+            Device_Address := GTT_Address_Type (PTE and 16#7f_ffff_f000#);
+         end;
+      end if;
+   end Read_GTT;
+
    ----------------------------------------------------------------------------
 
    package Rep is
diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index 99efba9..3be2ec7 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -1720,17 +1720,21 @@
 
    procedure Remove_Fence (First_Page, Last_Page : GTT_Range);
 
-   pragma Warnings (Off, "declaration of ""Write_GTT"" hides one at *");
    procedure Write_GTT
      (GTT_Page       : GTT_Range;
       Device_Address : GTT_Address_Type;
       Valid          : Boolean)
    with
       Global  => (In_Out => GTT_State),
-      Depends => (GTT_State =>+ (GTT_Page, Device_Address, Valid)),
-      Pre     => True,
-      Post    => True;
-   pragma Warnings (On, "declaration of ""Write_GTT"" hides one at *");
+      Depends => (GTT_State =>+ (GTT_Page, Device_Address, Valid));
+
+   procedure Read_GTT
+     (Device_Address :    out GTT_Address_Type;
+      Valid          :    out Boolean;
+      GTT_Page       : in     GTT_Range)
+   with
+      Global  => (In_Out => GTT_State),
+      Depends => ((Device_Address, Valid, GTT_State) => (GTT_State, GTT_Page));
 
    procedure Set_Register_Base (Base : Word64; GTT_Base : Word64 := 0)
    with
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index baa7e6c..abd19b1 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -601,6 +601,15 @@
       Registers.Write_GTT (GTT_Page, Device_Address, Valid);
    end Write_GTT;
 
+   procedure Read_GTT
+     (Device_Address :    out GTT_Address_Type;
+      Valid          :    out Boolean;
+      GTT_Page       : in     GTT_Range)
+   is
+   begin
+      Registers.Read_GTT (Device_Address, Valid, GTT_Page);
+   end Read_GTT;
+
    procedure Setup_Default_GTT (FB : Framebuffer_Type; Phys_Base : Word32)
    with
       Pre => Is_Initialized and Valid_Phys_FB (FB, Phys_Base)
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 7f44a0f..dcb3975 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -163,6 +163,14 @@
       Global => (In_Out => Device_State, Proof_In => Init_State),
       Pre => Is_Initialized;
 
+   procedure Read_GTT
+     (Device_Address :    out GTT_Address_Type;
+      Valid          :    out Boolean;
+      GTT_Page       : in     GTT_Range)
+   with
+      Global => (In_Out => Device_State, Proof_In => Init_State),
+      Pre => Is_Initialized;
+
    procedure Setup_Default_FB
      (FB       : in     Framebuffer_Type;
       Clear    : in     Boolean := True;