gma tgl: Add connector programming

This patch adds support for enabling displays on both combo PHY ports
and Type-C ports over DP-Alt mode.

Verified eDP, HDMI (not Type-C),  and DP Alt mode on google/delbin.

Change-Id: I908e8bef8451d21eecde9ce6defddc2b3df7f738
Signed-off-by: Tim Wawrzynczak <twawrzynczak@chromium.org>
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.sourcearcade.org/c/libgfxinit/+/469
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Tested-by: Nico Huber <nico.h@gmx.de>
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 1def7e9..d1fb7b1 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -678,12 +678,15 @@
      (GNATprove, Off, """Registers.Register_State"" * is not modified*",
       Reason => "Power_Up_VGA is only effective in certain configurations.");
    pragma Warnings
+     (GNATprove, Off, """PCode.Mailbox_Ready"" * is not modified*",
+      Reason => "Pcode is only used in certain configurations.");
+   pragma Warnings
      (GNATprove, Off, "no check message justified*", Reason => "see below");
    procedure Power_Up_VGA
    with
       Refined_Global =>
         (Input => (Cur_Configs, Config.Variable, Time.State),
-         In_Out => (Registers.Register_State),
+         In_Out => (Registers.Register_State, PCode.Mailbox_Ready),
          Proof_In => (Initialized))
    is
       Fake_Config : constant Pipe_Configs :=
@@ -703,6 +706,8 @@
    pragma Annotate
      (GNATprove, Intentional, "unused global",
       "Power_Up_VGA is only effective in certain configurations.");
+   pragma Warnings
+     (GNATprove, On, """PCode.Mailbox_Ready"" * is not modified*");
    pragma Warnings (GNATprove, On, "no check message justified*");
    pragma Warnings
      (GNATprove, On, """Registers.Register_State"" * is not modified*");