gma config: Make Config.CPU and Config.CPU_Var variable

Introduce CONFIG_GFX_GMA_DYN_CPU that, if set to `y`, makes `Config.CPU`
and `Config.CPU_Var` variables. All other config values derived from
these are turned into expression functions.

Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27068
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Reviewed-by: Patrick Georgi <pgeorgi@google.com>
This commit is contained in:
Nico Huber 2018-06-10 14:59:04 +02:00
parent d9365613ea
commit adfe11fec3
6 changed files with 86 additions and 19 deletions

View File

@ -51,8 +51,36 @@ CONFIG_GFX_GMA_CPU_VARIANT := $(call strip_quotes,$(CONFIG_GFX_GMA_CPU_VARIANT))
CONFIG_GFX_GMA_INTERNAL_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_INTERNAL_PORT))
CONFIG_GFX_GMA_ANALOG_I2C_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_ANALOG_I2C_PORT))
_GEN_NONCONST := $(strip \
$(if $(filter Ironlake,$(CONFIG_GFX_GMA_GENERATION)),ilk, \
$(if $(filter Haswell,$(CONFIG_GFX_GMA_GENERATION)),hsw, \
$(if $(filter Skylake,$(CONFIG_GFX_GMA_GENERATION)),skl))))
# GNATprove (GPL 2017) doesn't realize when a boolean expression
# that depends both on static values and variables can be evalu-
# ated at compile time (e.g. `False and then Variable` is always
# `False` and GNAT acts appropriately). So for now, we generate
# functions instead of constant expressions for these mixed ex-
# pressions.
_GEN_CONST_TARGET := <cpufunc> # set to `constant` to generate constants.
hw-gfx-gma-config-ads := $(subst //,/,$(call src-to-obj,,$(dir)/hw-gfx-gma-config).ads)
ifeq ($(CONFIG_GFX_GMA_DYN_CPU),y)
$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
-e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
-e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
-e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
-e'/constant Gen_CPU\(_Var\)\?/d' \
-e's/<genbool>/constant Boolean/' \
-e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)bool>/<\1var> Boolean/' \
$(if $(_GEN_NONCONST),-e's/<\(...\)\?$(_GEN_NONCONST)\(...\)\?var>/<cpufunc>/') \
-e's/<\(ilk\|hsw\|skl\)\(...\)\?var>/$(_GEN_CONST_TARGET)/' \
-e's/\(.*: *<cpufunc>.*:=\) *\(.*\);/\1\n (\2);/' \
-e's/\([^ ]\+\) *: *<cpufunc> \+\([^ ]*\) *:=/function \1 return \2 is/' \
$< >$@
else
$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
@ -61,9 +89,12 @@ $(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
-e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
-e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
-e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
-e":s$$(printf '\n ')/,$$/{N;s/,\n.*Dyn_CPU\(_Var\)\?[^,)]*//;ts$$(printf '\n ')P;D;}" \
-e'/Dyn_CPU\(_Var\)\?/d' \
-e's/<\(gen\|\(ilk\|hsw\|skl\)\(...\)\?\)bool>/constant Boolean/' \
-e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)var>/constant/' \
$< >$@
endif
gfxinit-gen-y += $(hw-gfx-gma-config-ads)
ifneq ($(filter G45,$(CONFIG_GFX_GMA_CPU)),)

View File

@ -59,16 +59,22 @@ private package HW.GFX.GMA.Config is
type Variable_Config is record
Valid_Port : Valid_Port_Array;
Raw_Clock : Frequency_Type;
Dyn_CPU : Gen_CPU_Type;
Dyn_CPU_Var : Gen_CPU_Variant;
end record;
Initial_Settings : constant Variable_Config :=
(Valid_Port => (others => False),
Raw_Clock => Frequency_Type'First);
Raw_Clock => Frequency_Type'First,
Dyn_CPU => Gen_CPU_Type'First,
Dyn_CPU_Var => Gen_CPU_Variant'First);
Variable : Variable_Config with Part_Of => GMA.Config_State;
Valid_Port : Valid_Port_Array renames Variable.Valid_Port;
Raw_Clock : Frequency_Type renames Variable.Raw_Clock;
CPU : Gen_CPU_Type renames Variable.Dyn_CPU;
CPU_Var : Gen_CPU_Variant renames Variable.Dyn_CPU_Var;
----------------------------------------------------------------------------
@ -303,12 +309,12 @@ private package HW.GFX.GMA.Config is
----------------------------------------------------------------------------
GTT_PTE_Size : <hswvar> := (if Has_64bit_GTT then 8 else 4);
GTT_PTE_Size : <hswvar> Natural := (if Has_64bit_GTT then 8 else 4);
Fence_Base : <ilkvar> :=
Fence_Base : <ilkvar> Natural :=
(if not Sandybridge_On then 16#0000_3000# else 16#0010_0000#);
Fence_Count : <ilkvar> :=
Fence_Count : <ilkvar> Natural :=
(if not Ivybridge_On then 16 else 32);
----------------------------------------------------------------------------

View File

@ -16,8 +16,6 @@ with HW.Time;
with HW.MMIO_Range;
pragma Elaborate_All (HW.MMIO_Range);
with HW.GFX.GMA.Config;
with HW.Debug;
with GNAT.Source_Info;

View File

@ -14,6 +14,7 @@
with System;
with HW.GFX.GMA;
with HW.GFX.GMA.Config;
private package HW.GFX.GMA.Registers
with
@ -1720,21 +1721,39 @@ is
procedure Remove_Fence (First_Page, Last_Page : GTT_Range);
pragma Warnings (GNATprove, Off, "no check message justified by this",
Reason => "see Annotate aspects.");
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));
Global =>
(Input => Config.Variable,
In_Out => GTT_State),
Depends =>
(GTT_State =>+ (Config.Variable, GTT_Page, Device_Address, Valid)),
Annotate =>
(GNATprove, Intentional,
"""GMA.Config_State"" of ""Write_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
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));
Global =>
(Input => Config.Variable,
In_Out => GTT_State),
Depends =>
((Device_Address, Valid, GTT_State) =>
(Config.Variable, GTT_State, GTT_Page)),
Annotate =>
(GNATprove, Intentional,
"""GMA.Config_State"" of ""Read_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
pragma Warnings (GNATprove, On, "no check message justified by this");
procedure Set_Register_Base (Base : Word64; GTT_Base : Word64 := 0)
with

View File

@ -528,11 +528,11 @@ is
pragma Warnings
(GNATprove, Off, """Registers.Register_State"" * is not modified*",
Reason => "Power_Up_VGA is only effective on certain generations.");
Reason => "Power_Up_VGA is only effective in certain configurations.");
procedure Power_Up_VGA
with
Refined_Global =>
(Input => (Cur_Configs, Time.State),
(Input => (Cur_Configs, Config.Variable, Time.State),
In_Out => (Registers.Register_State),
Proof_In => (Initialized))
is
@ -554,7 +554,7 @@ is
(GNATprove, Off, "no check message justified*", Reason => "see below");
pragma Annotate
(GNATprove, Intentional, "unused global",
"Power_Up_VGA is only effective on certain generations.");
"Power_Up_VGA is only effective in certain configurations.");
pragma Warnings (GNATprove, On, "no check message justified*");
pragma Warnings
(GNATprove, On, """Registers.Register_State"" * is not modified*");

View File

@ -111,7 +111,7 @@ is
procedure Power_Up_VGA
with
Global =>
(Input => (State, Time.State),
(Input => (State, Config_State, Time.State),
In_Out => (Device_State),
Proof_In => (Init_State)),
Pre => Is_Initialized;
@ -160,7 +160,9 @@ is
Device_Address : GTT_Address_Type;
Valid : Boolean)
with
Global => (In_Out => Device_State, Proof_In => Init_State),
Global =>
(Input => Config_State,
In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
procedure Read_GTT
@ -168,7 +170,9 @@ is
Valid : out Boolean;
GTT_Page : in GTT_Range)
with
Global => (In_Out => Device_State, Proof_In => Init_State),
Global =>
(Input => Config_State,
In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
procedure Setup_Default_FB
@ -177,18 +181,27 @@ is
Success : out Boolean)
with
Global =>
(In_Out =>
(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;
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 =>
(In_Out => (State, Device_State),
(Input => Config_State,
In_Out => (State, Device_State),
Proof_In => (Init_State)),
Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
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");
----------------------------------------------------------------------------