diff --git a/common/hw-gfx-gma-config.ads.template b/common/hw-gfx-gma-config.ads.template
index 2667333..8711e54 100644
--- a/common/hw-gfx-gma-config.ads.template
+++ b/common/hw-gfx-gma-config.ads.template
@@ -155,7 +155,7 @@
    Has_Plane_Control             : <genbool> := Broxton_On;
    Has_DSP_Linoff                : <genbool> := Up_To_Ironlake;
    Has_PF_Pipe_Select            : <ilkhswbool> := CPU_Ivybridge or CPU_Haswell;
-   Has_Cursor_FBC_Control        : <ilkbool> := Ivybridge_On;
+   Has_Ivybridge_Cursors         : <ilkbool> := Ivybridge_On;
    VGA_Plane_Workaround          : <ilkbool> := CPU_Ivybridge;
    Has_GMCH_DP_Transcoder        : <genbool> := Gen_G45;
    Has_GMCH_VGACNTRL             : <genbool> := Gen_G45;
diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index bb7b989..000c536 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -15,7 +15,6 @@
 with HW.Debug;
 with GNAT.Source_Info;
 
-with HW.GFX.GMA.Config;
 with HW.GFX.GMA.Transcoder;
 
 package body HW.GFX.GMA.Pipe_Setup is
@@ -352,7 +351,7 @@
       -- on some platforms writing CUR_CTL disables self-arming of CUR_POS
       -- so keep it first
       Registers.Write
-        (Register => Controllers (Pipe).CUR_CTL,
+        (Register => Cursors (Pipe).CTL,
          Value    => CUR_CTL_PIPE_SELECT (Pipe) or
                      CUR_CTL_MODE (Cursor.Mode, Cursor.Size));
       Place_Cursor (Pipe, FB, Cursor);
@@ -376,11 +375,11 @@
          Y := -Width;
       end if;
       Registers.Write
-        (Register => Controllers (Pipe).CUR_POS,
+        (Register => Cursors (Pipe).POS,
          Value    => CUR_POS_Y (Y) or CUR_POS_X (X));
       -- write to CUR_BASE always arms other CUR_* registers
       Registers.Write
-        (Register => Controllers (Pipe).CUR_BASE,
+        (Register => Cursors (Pipe).BASE,
          Value    => Shift_Left (Word32 (Cursor.GTT_Offset), 12));
    end Place_Cursor;
 
@@ -699,11 +698,13 @@
 
    ----------------------------------------------------------------------------
 
-   procedure Planes_Off (Controller : Controller_Type) is
+   procedure Planes_Off (Controller : Controller_Type; CUR : Cursor_Regs)
+   is
+      use type Registers.Registers_Invalid_Index;
    begin
-      Registers.Write (Controller.CUR_CTL, 16#0000_0000#);
-      if Config.Has_Cursor_FBC_Control then
-         Registers.Write (Controller.CUR_FBC_CTL, 16#0000_0000#);
+      Registers.Write (CUR.CTL, 16#0000_0000#);
+      if CUR.FBC_CTL /= Registers.Invalid_Register then
+         Registers.Write (CUR.FBC_CTL, 16#0000_0000#);
       end if;
       Registers.Unset_Mask (Controller.SPCNTR, DSPCNTR_ENABLE);
       if Config.Has_Plane_Control then
@@ -720,7 +721,7 @@
    begin
       pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
 
-      Planes_Off (Controllers (Pipe));
+      Planes_Off (Controllers (Pipe), Cursors (Pipe));
       Transcoder.Off (Pipe);
       Panel_Fitter_Off (Controllers (Pipe));
       Transcoder.Clk_Off (Pipe);
@@ -746,7 +747,7 @@
       Legacy_VGA_Off;
 
       for Pipe in Pipe_Index loop
-         Planes_Off (Controllers (Pipe));
+         Planes_Off (Controllers (Pipe), Cursors (Pipe));
          Transcoder.Off (Pipe);
          Panel_Fitter_Off (Controllers (Pipe));
          Transcoder.Clk_Off (Pipe);
diff --git a/common/hw-gfx-gma-pipe_setup.ads b/common/hw-gfx-gma-pipe_setup.ads
index fe877ad..0edb0c9 100644
--- a/common/hw-gfx-gma-pipe_setup.ads
+++ b/common/hw-gfx-gma-pipe_setup.ads
@@ -12,6 +12,7 @@
 -- GNU General Public License for more details.
 --
 
+with HW.GFX.GMA.Config;
 with HW.GFX.GMA.Registers;
 
 use type HW.Int32;
@@ -78,10 +79,6 @@
          DSPSURF           : Registers.Registers_Index;
          DSPTILEOFF        : Registers.Registers_Index;
          SPCNTR            : Registers.Registers_Index;
-         CUR_CTL           : Registers.Registers_Index;
-         CUR_BASE          : Registers.Registers_Index;
-         CUR_POS           : Registers.Registers_Index;
-         CUR_FBC_CTL       : Registers.Registers_Index;
          -- Skylake registers (partially aliased)
          PLANE_CTL         : Registers.Registers_Index;
          PLANE_OFFSET      : Registers.Registers_Index;
@@ -117,10 +114,6 @@
          DSPSURF           => Registers.DSPASURF,
          DSPTILEOFF        => Registers.DSPATILEOFF,
          SPCNTR            => Registers.SPACNTR,
-         CUR_CTL           => Registers.CUR_CTL_A,
-         CUR_BASE          => Registers.CUR_BASE_A,
-         CUR_POS           => Registers.CUR_POS_A,
-         CUR_FBC_CTL       => Registers.CUR_FBC_CTL_A,
          PLANE_CTL         => Registers.DSPACNTR,
          PLANE_OFFSET      => Registers.DSPATILEOFF,
          PLANE_POS         => Registers.PLANE_POS_1_A,
@@ -166,10 +159,6 @@
          DSPSURF           => Registers.DSPBSURF,
          DSPTILEOFF        => Registers.DSPBTILEOFF,
          SPCNTR            => Registers.SPBCNTR,
-         CUR_CTL           => Registers.CUR_CTL_B,
-         CUR_BASE          => Registers.CUR_BASE_B,
-         CUR_POS           => Registers.CUR_POS_B,
-         CUR_FBC_CTL       => Registers.CUR_FBC_CTL_B,
          PLANE_CTL         => Registers.DSPBCNTR,
          PLANE_OFFSET      => Registers.DSPBTILEOFF,
          PLANE_POS         => Registers.PLANE_POS_1_B,
@@ -215,10 +204,6 @@
          DSPSURF           => Registers.DSPCSURF,
          DSPTILEOFF        => Registers.DSPCTILEOFF,
          SPCNTR            => Registers.SPCCNTR,
-         CUR_CTL           => Registers.CUR_CTL_C,
-         CUR_BASE          => Registers.CUR_BASE_C,
-         CUR_POS           => Registers.CUR_POS_C,
-         CUR_FBC_CTL       => Registers.CUR_FBC_CTL_C,
          PLANE_CTL         => Registers.DSPCCNTR,
          PLANE_OFFSET      => Registers.DSPCTILEOFF,
          PLANE_POS         => Registers.PLANE_POS_1_C,
@@ -252,4 +237,40 @@
                               Registers.CUR_WM_C_6,
                               Registers.CUR_WM_C_7)));
 
+   type Cursor_Regs is record
+      CTL      : Registers.Registers_Index;
+      BASE     : Registers.Registers_Index;
+      POS      : Registers.Registers_Index;
+      FBC_CTL  : Registers.Registers_Invalid_Index;
+   end record;
+
+   function Cursors (Pipe : Pipe_Index) return Cursor_Regs is
+     (if not Config.Has_Ivybridge_Cursors then
+        (if Pipe = Primary then
+           (CTL      => Registers.CURACNTR,
+            BASE     => Registers.CURABASE,
+            POS      => Registers.CURAPOS,
+            FBC_CTL  => Registers.Invalid_Register)
+         else
+           (CTL      => Registers.CURBCNTR,
+            BASE     => Registers.CURBBASE,
+            POS      => Registers.CURBPOS,
+            FBC_CTL  => Registers.Invalid_Register))
+      else
+        (if Pipe = Primary then
+           (CTL      => Registers.CUR_CTL_A,
+            BASE     => Registers.CUR_BASE_A,
+            POS      => Registers.CUR_POS_A,
+            FBC_CTL  => Registers.CUR_FBC_CTL_A)
+         elsif Pipe = Secondary then
+           (CTL      => Registers.CUR_CTL_B,
+            BASE     => Registers.CUR_BASE_B,
+            POS      => Registers.CUR_POS_B,
+            FBC_CTL  => Registers.CUR_FBC_CTL_B)
+         else
+           (CTL      => Registers.CUR_CTL_C,
+            BASE     => Registers.CUR_BASE_C,
+            POS      => Registers.CUR_POS_C,
+            FBC_CTL  => Registers.CUR_FBC_CTL_C)));
+
 end HW.GFX.GMA.Pipe_Setup;
diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index ac0f023..5cffe76 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -473,6 +473,9 @@
       CUR_BASE_A,
       CUR_POS_A,
       CUR_FBC_CTL_A,
+      CURBCNTR,
+      CURBBASE,
+      CURBPOS,
       CUR_WM_A_0,
       CUR_WM_A_1,
       CUR_WM_A_2,
@@ -927,6 +930,9 @@
       PS_CTRL_2_B           => 16#06_8a80# / Register_Width,
 
       -- cursor control
+      CURBCNTR              => 16#07_00c0# / Register_Width,   -- <= SNB
+      CURBBASE              => 16#07_00c4# / Register_Width,   -- <= SNB
+      CURBPOS               => 16#07_00c8# / Register_Width,   -- <= SNB
       CUR_CTL_B             => 16#07_1080# / Register_Width,
       CUR_BASE_B            => 16#07_1084# / Register_Width,
       CUR_POS_B             => 16#07_1088# / Register_Width,
@@ -1632,6 +1638,9 @@
    GMCH_ADPA            : constant Registers_Index := FDI_TX_CTL_B;
    GMCH_HDMIB           : constant Registers_Index := GMCH_SDVOB;
    GMCH_HDMIC           : constant Registers_Index := GMCH_SDVOC;
+   CURACNTR             : constant Registers_Index := CUR_CTL_A;
+   CURABASE             : constant Registers_Index := CUR_BASE_A;
+   CURAPOS              : constant Registers_Index := CUR_POS_A;
 
    ---------------------------------------------------------------------------
 
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 8b1c85a..f9444e8 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -129,12 +129,19 @@
          Proof_In => (Init_State)),
       Pre => Is_Initialized;
 
+   pragma Warnings (GNATprove, Off, "no check message justified by this",
+                    Reason => "see Annotate aspects.");
    procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Update_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    procedure Place_Cursor
      (Pipe : Pipe_Index;
@@ -142,9 +149,14 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Place_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    procedure Move_Cursor
      (Pipe : Pipe_Index;
@@ -152,9 +164,14 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Move_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    ----------------------------------------------------------------------------
 
@@ -191,8 +208,6 @@
          Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
-   pragma Warnings (GNATprove, Off, "no check message justified by this",
-                    Reason => "see Annotate aspects.");
    procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
    with
       Global =>