381 lines
12 KiB
Ada
381 lines
12 KiB
Ada
--
|
|
-- Copyright (C) 2015-2016 secunet Security Networks AG
|
|
--
|
|
-- 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; version 2 of the License.
|
|
--
|
|
-- 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 Ada.Unchecked_Conversion;
|
|
|
|
with HW.Debug;
|
|
with GNAT.Source_Info;
|
|
|
|
with HW.GFX.DP_Defs;
|
|
|
|
use type HW.Word8;
|
|
|
|
package body HW.GFX.DP_Info is
|
|
|
|
procedure Read_Caps
|
|
(Link : in out DP_Link;
|
|
Port : in T;
|
|
Success : out Boolean)
|
|
is
|
|
Data : DP_Defs.Aux_Payload;
|
|
Length : DP_Defs.Aux_Payload_Length;
|
|
|
|
Caps_Size : constant := 15;
|
|
begin
|
|
pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
|
|
|
|
Length := Caps_Size;
|
|
Aux_Ch.Aux_Read
|
|
(Port => Port,
|
|
Address => 16#00000#,
|
|
Length => Length,
|
|
Data => Data,
|
|
Success => Success);
|
|
Success := Success and Length = Caps_Size;
|
|
|
|
if Length = Caps_Size then
|
|
Link.Receiver_Caps.Rev := Data (0);
|
|
case Data (1) is
|
|
when 16#06# =>
|
|
Link.Receiver_Caps.Max_Link_Rate := DP_Bandwidth_1_62;
|
|
when 16#0a# =>
|
|
Link.Receiver_Caps.Max_Link_Rate := DP_Bandwidth_2_7;
|
|
when 16#14# =>
|
|
Link.Receiver_Caps.Max_Link_Rate := DP_Bandwidth_5_4;
|
|
when others =>
|
|
if Data (1) > 16#14# then
|
|
Link.Receiver_Caps.Max_Link_Rate := DP_Bandwidth_5_4;
|
|
else
|
|
Link.Receiver_Caps.Max_Link_Rate := DP_Bandwidth_1_62;
|
|
end if;
|
|
end case;
|
|
case Data (2) and 16#1f# is
|
|
when 0 | 1 =>
|
|
Link.Receiver_Caps.Max_Lane_Count := DP_Lane_Count_1;
|
|
when 2 | 3 =>
|
|
Link.Receiver_Caps.Max_Lane_Count := DP_Lane_Count_2;
|
|
when others =>
|
|
Link.Receiver_Caps.Max_Lane_Count := DP_Lane_Count_4;
|
|
end case;
|
|
Link.Receiver_Caps.TPS3_Supported := (Data (2) and 16#40#) /= 0;
|
|
Link.Receiver_Caps.Enhanced_Framing := (Data (2) and 16#80#) /= 0;
|
|
Link.Receiver_Caps.No_Aux_Handshake := (Data (3) and 16#40#) /= 0;
|
|
Link.Receiver_Caps.Aux_RD_Interval := Data (14);
|
|
|
|
pragma Debug (Debug.New_Line);
|
|
pragma Debug (Debug.Put_Line ("DPCD:"));
|
|
pragma Debug (Debug.Put_Reg8 (" Rev ", Data (0)));
|
|
pragma Debug (Debug.Put_Reg8 (" Max_Link_Rate ", Data (1)));
|
|
pragma Debug (Debug.Put_Reg8 (" Max_Lane_Count ", Data (2) and 16#1f#));
|
|
pragma Debug (Debug.Put_Reg8 (" TPS3_Supported ", Data (2) and 16#40#));
|
|
pragma Debug (Debug.Put_Reg8 (" Enhanced_Framing", Data (2) and 16#80#));
|
|
pragma Debug (Debug.Put_Reg8 (" No_Aux_Handshake", Data (3) and 16#40#));
|
|
pragma Debug (Debug.Put_Reg8 (" Aux_RD_Interval ", Data (14)));
|
|
pragma Debug (Debug.New_Line);
|
|
end if;
|
|
end Read_Caps;
|
|
|
|
procedure Minimum_Lane_Count
|
|
(Link : in out DP_Link;
|
|
Mode : in Mode_Type;
|
|
Success : out Boolean)
|
|
with
|
|
Depends => ((Link, Success) => (Link, Mode))
|
|
is
|
|
function Link_Pixel_Per_Second
|
|
(Link_Rate : DP_Bandwidth)
|
|
return Positive
|
|
with
|
|
Post => Pos64 (Link_Pixel_Per_Second'Result) <=
|
|
((DP_Symbol_Rate_Type'Last * 8) / 3) / BPC_Type'First
|
|
is
|
|
begin
|
|
-- Link_Rate is brutto with 8/10 bit symbols; three colors
|
|
pragma Assert (Positive (DP_Symbol_Rate (Link_Rate)) <= (Positive'Last / 8) * 3);
|
|
pragma Assert ((Int64 (DP_Symbol_Rate (Link_Rate)) * 8) / 3
|
|
>= Int64 (BPC_Type'Last));
|
|
return Positive
|
|
(((Int64 (DP_Symbol_Rate (Link_Rate)) * 8) / 3)
|
|
/ Int64 (Mode.BPC));
|
|
end Link_Pixel_Per_Second;
|
|
|
|
Count : Natural;
|
|
begin
|
|
Count := Link_Pixel_Per_Second (Link.Bandwidth);
|
|
Count := (Positive (Mode.Dotclock) + Count - 1) / Count;
|
|
|
|
Success := True;
|
|
case Count is
|
|
when 1 => Link.Lane_Count := DP_Lane_Count_1;
|
|
when 2 => Link.Lane_Count := DP_Lane_Count_2;
|
|
when 3 | 4 => Link.Lane_Count := DP_Lane_Count_4;
|
|
when others => Success := False;
|
|
end case;
|
|
end Minimum_Lane_Count;
|
|
|
|
procedure Preferred_Link_Setting
|
|
(Link : in out DP_Link;
|
|
Mode : in Mode_Type;
|
|
Success : out Boolean)
|
|
is
|
|
begin
|
|
Link.Bandwidth := Link.Receiver_Caps.Max_Link_Rate;
|
|
Link.Enhanced_Framing := Link.Receiver_Caps.Enhanced_Framing;
|
|
|
|
Minimum_Lane_Count (Link, Mode, Success);
|
|
|
|
Success := Success and
|
|
Link.Lane_Count <= Link.Receiver_Caps.Max_Lane_Count;
|
|
|
|
pragma Debug (Success, Debug.Put ("Trying DP settings: Symbol Rate = "));
|
|
pragma Debug (Success, Debug.Put_Int32
|
|
(Int32 (DP_Symbol_Rate (Link.Bandwidth))));
|
|
pragma Debug (Success, Debug.Put ("; Lane Count = "));
|
|
pragma Debug (Success, Debug.Put_Int32
|
|
(Int32 (Lane_Count_As_Integer (Link.Lane_Count))));
|
|
pragma Debug (Success, Debug.New_Line);
|
|
pragma Debug (Success, Debug.New_Line);
|
|
|
|
pragma Debug (not Success, Debug.Put_Line
|
|
("Mode requirements exceed available bandwidth!"));
|
|
end Preferred_Link_Setting;
|
|
|
|
procedure Next_Link_Setting
|
|
(Link : in out DP_Link;
|
|
Mode : in Mode_Type;
|
|
Success : out Boolean)
|
|
is
|
|
begin
|
|
if Link.Bandwidth > DP_Bandwidth'First then
|
|
Link.Bandwidth := DP_Bandwidth'Pred (Link.Bandwidth);
|
|
|
|
Minimum_Lane_Count (Link, Mode, Success);
|
|
|
|
Success := Success and
|
|
Link.Lane_Count <= Link.Receiver_Caps.Max_Lane_Count;
|
|
else
|
|
Success := False;
|
|
end if;
|
|
|
|
pragma Debug (Success, Debug.Put ("Trying DP settings: Symbol Rate = "));
|
|
pragma Debug (Success, Debug.Put_Int32
|
|
(Int32 (DP_Symbol_Rate (Link.Bandwidth))));
|
|
pragma Debug (Success, Debug.Put ("; Lane Count = "));
|
|
pragma Debug (Success, Debug.Put_Int32
|
|
(Int32 (Lane_Count_As_Integer (Link.Lane_Count))));
|
|
pragma Debug (Success, Debug.New_Line);
|
|
pragma Debug (Success, Debug.New_Line);
|
|
end Next_Link_Setting;
|
|
|
|
----------------------------------------------------------------------------
|
|
|
|
procedure Calculate_M_N
|
|
(Link : in DP_Link;
|
|
Mode : in Mode_Type;
|
|
Data_M : out M_Type;
|
|
Data_N : out N_Type;
|
|
Link_M : out M_Type;
|
|
Link_N : out N_Type)
|
|
is
|
|
DATA_N_MAX : constant := 16#800000#;
|
|
LINK_N_MAX : constant := 16#100000#;
|
|
|
|
subtype Calc_M_Type is Int64 range 0 .. 2 ** 36;
|
|
subtype Calc_N_Type is Int64 range 0 .. 2 ** 36;
|
|
subtype N_Rounded_Type is Int64 range
|
|
0 .. Int64'Max (DATA_N_MAX, LINK_N_MAX);
|
|
|
|
M : Calc_M_Type;
|
|
N : Calc_N_Type;
|
|
|
|
procedure Cancel_M_N
|
|
(M : in out Calc_M_Type;
|
|
N : in out Calc_N_Type;
|
|
N_Max : in N_Rounded_Type)
|
|
with
|
|
Depends => ((M, N) => (M, N, N_max)),
|
|
Pre => (N > 0 and M in 0 .. Calc_M_Type'Last / 2),
|
|
Post => (M <= M_N_Max and N <= M_N_Max)
|
|
is
|
|
Orig_N : constant Calc_N_Type := N;
|
|
|
|
function Round_N (N : Calc_N_Type) return N_Rounded_Type
|
|
with
|
|
Post => (Round_N'Result <= N * 2)
|
|
is
|
|
RN : Calc_N_Type;
|
|
RN2 : Calc_N_Type := N_Max;
|
|
begin
|
|
loop
|
|
RN := RN2;
|
|
RN2 := RN2 / 2;
|
|
exit when RN2 < N;
|
|
pragma Loop_Invariant (RN2 = RN / 2 and RN2 in N .. N_Max);
|
|
end loop;
|
|
return RN;
|
|
end Round_N;
|
|
begin
|
|
N := Round_N (N);
|
|
|
|
-- The automatic provers need a little nudge here.
|
|
pragma Assert
|
|
(if M <= Calc_M_Type'Last/2 and
|
|
N <= Orig_N * 2 and
|
|
Orig_N > 0 and
|
|
M > 0
|
|
then
|
|
M * N / Orig_N <= Calc_M_Type'Last);
|
|
|
|
pragma Annotate (GNATprove, False_Positive,
|
|
"assertion might fail",
|
|
"The property cannot be proven automatically. An Isabelle proof is included as an axiom");
|
|
|
|
M := M * N / Orig_N;
|
|
|
|
-- This loop is never hit for sane values (i.e. M <= N) but
|
|
-- we have to make sure returned values are always in range.
|
|
while M > M_N_Max loop
|
|
pragma Loop_Invariant (N <= M_N_Max);
|
|
M := M / 2;
|
|
N := N / 2;
|
|
end loop;
|
|
end Cancel_M_N;
|
|
begin
|
|
pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
|
|
|
|
pragma Assert (3
|
|
* Mode.BPC
|
|
* Mode.Dotclock
|
|
in Pos64);
|
|
M := 3
|
|
* Mode.BPC
|
|
* Mode.Dotclock;
|
|
|
|
pragma Assert (8
|
|
* DP_Symbol_Rate (Link.Bandwidth)
|
|
* Lane_Count_As_Integer (Link.Lane_Count)
|
|
in Pos64);
|
|
N := 8
|
|
* DP_Symbol_Rate (Link.Bandwidth)
|
|
* Lane_Count_As_Integer (Link.Lane_Count);
|
|
|
|
Cancel_M_N (M, N, DATA_N_MAX);
|
|
Data_M := M;
|
|
Data_N := N;
|
|
|
|
-------------------------------------------------------------------
|
|
|
|
M := Pos64 (Mode.Dotclock);
|
|
N := Pos64 (DP_Symbol_Rate (Link.Bandwidth));
|
|
|
|
Cancel_M_N (M, N, LINK_N_MAX);
|
|
Link_M := M;
|
|
Link_N := N;
|
|
end Calculate_M_N;
|
|
|
|
----------------------------------------------------------------------------
|
|
|
|
procedure Read_Link_Status
|
|
(Port : in T;
|
|
Status : out Link_Status;
|
|
Success : out Boolean)
|
|
is
|
|
subtype Status_Index is DP_Defs.Aux_Payload_Index range 0 .. 5;
|
|
subtype Status_Buffer is Buffer (Status_Index);
|
|
function Buffer_As_Status is new Ada.Unchecked_Conversion
|
|
(Source => Status_Buffer, Target => Link_Status);
|
|
|
|
Data : DP_Defs.Aux_Payload;
|
|
Length : DP_Defs.Aux_Payload_Length;
|
|
begin
|
|
pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));
|
|
|
|
Length := Status_Index'Last + 1;
|
|
Aux_Ch.Aux_Read
|
|
(Port => Port,
|
|
Address => 16#00202#,
|
|
Length => Length,
|
|
Data => Data,
|
|
Success => Success);
|
|
Success := Success and Length = Status_Index'Last + 1;
|
|
Status := Buffer_As_Status (Data (Status_Index));
|
|
end Read_Link_Status;
|
|
|
|
function All_CR_Done
|
|
(Status : Link_Status;
|
|
Link : DP_Link)
|
|
return Boolean
|
|
is
|
|
CR_Done : Boolean := True;
|
|
begin
|
|
for Lane in Lane_Index
|
|
range 0 .. Lane_Index (Lane_Count_As_Integer (Link.Lane_Count) - 1)
|
|
loop
|
|
CR_Done := CR_Done and Status.Lanes (Lane).CR_Done;
|
|
end loop;
|
|
return CR_Done;
|
|
end All_CR_Done;
|
|
|
|
function All_EQ_Done
|
|
(Status : Link_Status;
|
|
Link : DP_Link)
|
|
return Boolean
|
|
is
|
|
EQ_Done : Boolean := True;
|
|
begin
|
|
for Lane in Lane_Index
|
|
range 0 .. Lane_Index (Lane_Count_As_Integer (Link.Lane_Count) - 1)
|
|
loop
|
|
EQ_Done := EQ_Done and Status.Lanes (Lane).CR_Done
|
|
and Status.Lanes (Lane).Channel_EQ_Done
|
|
and Status.Lanes (Lane).Symbol_Locked;
|
|
end loop;
|
|
return EQ_Done and Status.Interlane_Align_Done;
|
|
end All_EQ_Done;
|
|
|
|
function Max_Requested_VS
|
|
(Status : Link_Status;
|
|
Link : DP_Link)
|
|
return DP_Voltage_Swing
|
|
is
|
|
VS : DP_Voltage_Swing := DP_Voltage_Swing'First;
|
|
begin
|
|
for Lane in Lane_Index
|
|
range 0 .. Lane_Index (Lane_Count_As_Integer (Link.Lane_Count) - 1)
|
|
loop
|
|
if Status.Adjust_Requests (Lane).Voltage_Swing > VS then
|
|
VS := Status.Adjust_Requests (Lane).Voltage_Swing;
|
|
end if;
|
|
end loop;
|
|
return VS;
|
|
end Max_Requested_VS;
|
|
|
|
function Max_Requested_Emph
|
|
(Status : Link_Status;
|
|
Link : DP_Link)
|
|
return DP_Pre_Emph
|
|
is
|
|
Emph : DP_Pre_Emph := DP_Pre_Emph'First;
|
|
begin
|
|
for Lane in Lane_Index
|
|
range 0 .. Lane_Index (Lane_Count_As_Integer (Link.Lane_Count) - 1)
|
|
loop
|
|
if Status.Adjust_Requests (Lane).Pre_Emph > Emph then
|
|
Emph := Status.Adjust_Requests (Lane).Pre_Emph;
|
|
end if;
|
|
end loop;
|
|
return Emph;
|
|
end Max_Requested_Emph;
|
|
|
|
end HW.GFX.DP_Info;
|