--
-- Copyright (C) 2015-2018 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
-- the Free Software Foundation; either version 2 of the License, or
-- (at your option) any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--

with HW.Config;
with HW.Time;
with HW.PCI;
with HW.Port_IO;
with HW.GFX.Framebuffer_Filler;

package HW.GFX.GMA
with
   Abstract_State =>
     (State,
      Init_State,
      Config_State,
      (Device_State with External)),
   Initializes => Init_State
is

   GTT_Page_Size : constant := 4096;
   type GTT_Address_Type is mod 2 ** 39;
   subtype GTT_Range is Natural range 0 .. 16#8_0000# - 1;
   GTT_Rotation_Offset : constant GTT_Range := GTT_Range'Last / 2 + 1;

   type Generation is (G45, Ironlake, Haswell, Broxton, Skylake);

   type CPU_Type is
     (G45,
      GM45,
      Ironlake,
      Sandybridge,
      Ivybridge,
      Haswell,
      Broadwell,
      Broxton,
      Skylake,
      Kabylake);

   type CPU_Variant is (Normal, ULT, ULX);

   type Port_Type is
     (Disabled,
      Internal,
      DP1,
      DP2,
      DP3,
      HDMI1, -- or DVI
      HDMI2, -- or DVI
      HDMI3, -- or DVI
      Analog);
   subtype Active_Port_Type is Port_Type
      range Port_Type'Succ (Disabled) .. Port_Type'Last;

   type Cursor_Mode is (No_Cursor, ARGB_Cursor);
   type Cursor_Size is (Cursor_64x64, Cursor_128x128, Cursor_256x256);
   Cursor_Width : constant array (Cursor_Size) of Width_Type := (64, 128, 256);

   subtype Cursor_Pos is Int32 range Int32'First / 2 .. Int32'Last / 2;

   type Cursor_Type is record
      Mode        : Cursor_Mode;
      Size        : Cursor_Size;
      Center_X    : Cursor_Pos;
      Center_Y    : Cursor_Pos;
      GTT_Offset  : GTT_Range;
   end record;
   Default_Cursor : constant Cursor_Type :=
     (Mode        => No_Cursor,
      Size        => Cursor_Size'First,
      Center_X    => 0,
      Center_Y    => 0,
      GTT_Offset  => 0);

   type Pipe_Config is record
      Port        : Port_Type;
      Framebuffer : Framebuffer_Type;
      Cursor      : Cursor_Type;
      Mode        : Mode_Type;
   end record;
   type Pipe_Index is (Primary, Secondary, Tertiary);
   type Pipe_Configs is array (Pipe_Index) of Pipe_Config;

   -- Special framebuffer offset to indicate legacy VGA plane.
   -- Only valid on primary pipe.
   VGA_PLANE_FRAMEBUFFER_OFFSET : constant := 16#ffff_ffff#;

   pragma Warnings (GNATprove, Off, "unused variable ""Write_Delay""",
      Reason => "Write_Delay is used for debugging only");
   procedure Initialize
     (Write_Delay : in     Word64 := 0;
      Clean_State : in     Boolean := False;
      Success     :    out Boolean)
   with
      Global =>
        (In_Out => (Device_State, Port_IO.State),
         Output => (State, Init_State, Config_State),
         Input  => (Time.State)),
      Post => Success = Is_Initialized;
   function Is_Initialized return Boolean
   with
      Global => (Input => Init_State);
   pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");

   procedure Power_Up_VGA
   with
      Global =>
        (Input => (State, Config_State, Time.State),
         In_Out => (Device_State),
         Proof_In => (Init_State)),
      Pre => Is_Initialized;

   ----------------------------------------------------------------------------

   procedure Update_Outputs (Configs : Pipe_Configs)
   with
      Global =>
        (Input => (Config_State, Time.State),
         In_Out => (State, Device_State, Port_IO.State),
         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 =>
        (Input => (Config_State),
         In_Out => (State, Device_State),
         Proof_In => (Init_State)),
      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;
      X : Cursor_Pos;
      Y : Cursor_Pos)
   with
      Global =>
        (Input => (Config_State),
         In_Out => (State, Device_State),
         Proof_In => (Init_State)),
      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;
      X : Cursor_Pos;
      Y : Cursor_Pos)
   with
      Global =>
        (Input => (Config_State),
         In_Out => (State, Device_State),
         Proof_In => (Init_State)),
      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.");

   ----------------------------------------------------------------------------

   procedure Write_GTT
     (GTT_Page       : GTT_Range;
      Device_Address : GTT_Address_Type;
      Valid          : Boolean)
   with
      Global =>
        (Input => Config_State,
         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 =>
        (Input => Config_State,
         In_Out => Device_State, Proof_In => Init_State),
      Pre => Is_Initialized;

   procedure Setup_Default_FB
     (FB       : in     Framebuffer_Type;
      Clear    : in     Boolean := True;
      Success  :    out Boolean)
   with
      Global =>
        (Input => Config_State,
         In_Out =>
           (State, Device_State,
            Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
         Proof_In => (Init_State)),
      Pre => Is_Initialized and HW.Config.Dynamic_MMIO;

   procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
   with
      Global =>
        (Input => Config_State,
         In_Out => (State, Device_State),
         Proof_In => (Init_State)),
      Pre => Is_Initialized and HW.Config.Dynamic_MMIO,
      Annotate =>
        (GNATprove, Intentional,
         "global input ""GMA.Config_State"" of ""Map_Linear_FB"" not read",
         "Reading of Config_State depends on the platform configuration.");
   pragma Warnings (GNATprove, On, "no check message justified by this");

   ----------------------------------------------------------------------------

   pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
                    Reason => "It's only used for debugging");
   procedure Dump_Configs (Configs : Pipe_Configs);

private

   PCI_Usable : Boolean with Part_Of => State;
   use type HW.PCI.Index;
   procedure PCI_Read16 (Value : out Word16; Offset : HW.PCI.Index)
   with
      Pre => PCI_Usable and Offset mod 2 = 0;

   ----------------------------------------------------------------------------

   -- For the default framebuffer setup (see below) with 90 degree rotations,
   -- we expect the offset which is used for the final scanout to be above
   -- `GTT_Rotation_Offset`. So we can use `Offset - GTT_Rotation_Offset` for
   -- the physical memory location and aperture mapping.
   function Phys_Offset (FB : Framebuffer_Type) return Word32 is
     (if Rotation_90 (FB)
      then FB.Offset - Word32 (GTT_Rotation_Offset) * GTT_Page_Size
      else FB.Offset);

   ----------------------------------------------------------------------------
   -- State tracking for the currently configured pipes

   Cur_Configs : Pipe_Configs with Part_Of => State;

   function Requires_Scaling (Pipe_Cfg : Pipe_Config) return Boolean is
     (Requires_Scaling (Pipe_Cfg.Framebuffer, Pipe_Cfg.Mode));

   function Scaling_Type (Pipe_Cfg : Pipe_Config) return Scaling_Aspect is
     (Scaling_Type (Pipe_Cfg.Framebuffer, Pipe_Cfg.Mode));

   ----------------------------------------------------------------------------
   -- Internal representation of a single pipe's configuration

   type GPU_Port is (DIGI_A, DIGI_B, DIGI_C, DIGI_D, DIGI_E, LVDS, VGA);

   subtype Digital_Port is GPU_Port range DIGI_A .. DIGI_E;
   subtype GMCH_DP_Port is GPU_Port range DIGI_B .. DIGI_D;
   subtype GMCH_HDMI_Port is GPU_Port range DIGI_B .. DIGI_C;

   type PCH_Port is
     (PCH_DAC, PCH_LVDS,
      PCH_HDMI_B, PCH_HDMI_C, PCH_HDMI_D,
      PCH_DP_B, PCH_DP_C, PCH_DP_D);

   subtype PCH_HDMI_Port is PCH_Port range PCH_HDMI_B .. PCH_HDMI_D;
   subtype PCH_DP_Port is PCH_Port range PCH_DP_B .. PCH_DP_D;

   type Port_Config is
      record
         Port     : GPU_Port;
         PCH_Port : GMA.PCH_Port;
         Display  : Display_Type;
         Mode     : Mode_Type;
         Is_FDI   : Boolean;
         FDI      : DP_Link;
         DP       : DP_Link;
      end record;

   type FDI_Training_Type is (Simple_Training, Full_Training, Auto_Training);

   ----------------------------------------------------------------------------

   type DP_Port is (DP_A, DP_B, DP_C, DP_D);

   ----------------------------------------------------------------------------

   subtype DDI_HDMI_Buf_Trans_Range is Integer range 0 .. 11;

   ----------------------------------------------------------------------------

   Tile_Width : constant array (Tiling_Type) of Width_Type :=
     (Linear => 16, X_Tiled => 128, Y_Tiled => 32);
   Tile_Rows : constant array (Tiling_Type) of Height_Type :=
     (Linear => 1, X_Tiled => 8, Y_Tiled => 32);

   function FB_Pitch (Px : Pos_Pixel_Type; FB : Framebuffer_Type) return Natural
      is (Natural (Div_Round_Up
           (Pixel_To_Bytes (Px, FB), Tile_Width (FB.Tiling) * 4)));

   function Valid_Stride (FB : Framebuffer_Type) return Boolean is
     (FB.Width + FB.Start_X <= FB.Stride and
      Pixel_To_Bytes (FB.Stride, FB) mod (Tile_Width (FB.Tiling) * 4) = 0 and
      FB.Height + FB.Start_Y <= FB.V_Stride and
      FB.V_Stride mod Tile_Rows (FB.Tiling) = 0);

end HW.GFX.GMA;