Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Increase range of our main Frequency_Type
Increase `Frequency_Type` to 1MHz .. 2.5Ghz. We used to adapt it whenever necessary, e.g. when a new generation supported higher frequencies. But that got a little annoying. So let's choose a broader range that will hopefully lower the noise for some time.
1MHz is low enough for VGA resolution at 24p, and 2.5GHz is high enough for 8K at 60p. That should give us some margin.
Some corner cases required refactoring of some calculations and proofs. And, admittedly, the calculation in `HW.GFX.GMA.PCH.VGA` can in theory overflow, indeed. But our PLL calculations should ensure that this never happens.
Change-Id: I3a159bc11ccadcaba8ad04e126e6feadfd46008e Signed-off-by: Nico Huber nico.h@gmx.de --- M common/hw-gfx-dp_info.adb M common/hw-gfx-gma-pch-vga.adb M common/hw-gfx.ads 3 files changed, 8 insertions(+), 25 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/50/35750/1
diff --git a/common/hw-gfx-dp_info.adb b/common/hw-gfx-dp_info.adb index 7ac4556..d45826d 100644 --- a/common/hw-gfx-dp_info.adb +++ b/common/hw-gfx-dp_info.adb @@ -93,28 +93,11 @@ 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; + Lane_Pixel_Per_Second : constant Pos64 := + (((DP_Symbol_Rate (Link.Bandwidth) * 8) / 3) / Mode.BPC); + Count : constant Pos64 := + Div_Round_Up (Mode.Dotclock, Lane_Pixel_Per_Second); 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; @@ -184,8 +167,8 @@ 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 Calc_M_Type is Int64 range 0 .. 2 ** 38; + subtype Calc_N_Type is Int64 range 0 .. 2 ** 38; subtype N_Rounded_Type is Int64 range 0 .. Int64'Max (DATA_N_MAX, LINK_N_MAX);
diff --git a/common/hw-gfx-gma-pch-vga.adb b/common/hw-gfx-gma-pch-vga.adb index fd82740..eb7f9a0 100644 --- a/common/hw-gfx-gma-pch-vga.adb +++ b/common/hw-gfx-gma-pch-vga.adb @@ -135,7 +135,7 @@ Mask => SBI_SSCCTL_DISABLE);
Aux_Div := 16#0000_0000#; - Div_Sel := Word32 (Refclock / Mode.Dotclock - 2); + Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2; Phase_Inc := Word32 ((Refclock * 64) / Mode.Dotclock) and 16#0000_003f#; Phase_Dir := 16#0000_0000#;
diff --git a/common/hw-gfx.ads b/common/hw-gfx.ads index 93a3684..2cfc017 100644 --- a/common/hw-gfx.ads +++ b/common/hw-gfx.ads @@ -66,7 +66,7 @@ Rotation => No_Rotation, Offset => 0);
- subtype Frequency_Type is Pos64 range 19_200_000 .. 624_000_000; + subtype Frequency_Type is Pos64 range 1_000_000 .. 2_500_000_000;
type DP_Lane_Count is (DP_Lane_Count_1, DP_Lane_Count_2, DP_Lane_Count_4); subtype DP_Lane_Count_Type is Pos64 range 1 .. 4;
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 1: Verified+1
Arthur Heymans has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2: Code-Review+2
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2; Why is this change needed here?
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2:
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2;
Why is this change needed here?
It's the truth I tried to avoid. With `Mode.Dotclock` being possibly nearly as high as `Refclock` (see above), the division could result in 1, that minus 2, gives us -1 which can't be converted to a `Word32`. However the overflow of the subtraction is well defined in the modulo type `Word32`. So the change avoids the undefined behaviour, not the overflow itself.
A more elegant but also much more tedious solution would be to add preconditions all the way back to Update_Outputs() where we could prove that we wouldn't ever have such a high `Mode.Dotclock`. More precisely, in Fill_Port_Config, we'd need 12 FDI lanes to reach `Refclock / 2` :)
Angel Pons has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2:
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2;
It's the truth I tried to avoid. With `Mode.Dotclock` being possibly […]
I would prefer if this were to be proven rather than relying on overflow handling behavior
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2:
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2;
I would prefer if this were to be proven rather than relying on overflow handling behavior
What we rely on is not the behaviour of the numbers here but that this code is never called to enable a VGA port with an order-of-magnitude too high frequency. Which we know that we don't do.
But if you want to prove it, be my guest :)
What makes it difficult to get it proved with GNATprove is also the assumption that this code is only called for FDI connections (which will always be the case). So we'd need the precondition here that `Dotclock < 1_350_000_000`. A level up add `Display = VGA and` and another level up add `Gen = Haswell and` because then we know that VGA is al- ways used with FDI. And finally, in Fill_Port_Config() prove that `Display = VGA and Gen = Haswell => FDI` and that FDI config only succeeds if `Dotclock < X` (X is depends on the BPC also). That prove might need some refactoring so that would result in another (small) patch train... As all that wouldn't change the program behaviour, it's really just an academic excercise. Sure, we could prove correct behaviour of this program, but so far proving absence of runtime errors alone adds enough burden oO
Angel Pons has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2: Code-Review+2
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2;
What we rely on is not the behaviour of the numbers here but […]
I see, so it's far from trivial...
I would leave a comment or something just in case somebody else runs into this later on, if you want.
Hello Angel Pons, Arthur Heymans,
I'd like you to reexamine a change. Please visit
https://review.coreboot.org/c/libgfxinit/+/35750
to look at the new patch set (#3).
Change subject: Increase range of our main Frequency_Type ......................................................................
Increase range of our main Frequency_Type
Increase `Frequency_Type` to 1MHz .. 2.5Ghz. We used to adapt it whenever necessary, e.g. when a new generation supported higher frequencies. But that got a little annoying. So let's choose a broader range that will hopefully lower the noise for some time.
1MHz is low enough for VGA resolution at 24p, and 2.5GHz is high enough for 8K at 60p. That should give us some margin.
Some corner cases required refactoring of some calculations and proofs. And, admittedly, the calculation in `HW.GFX.GMA.PCH.VGA` can in theory overflow. We prove absence of runtime errors by deferring the potential overflow to the modular `Word32` type. This is not perfect, but overflow or not, we have to expect to be called with a sane frequency anyway.
Change-Id: I3a159bc11ccadcaba8ad04e126e6feadfd46008e Signed-off-by: Nico Huber nico.h@gmx.de --- M common/hw-gfx-dp_info.adb M common/hw-gfx-gma-pch-vga.adb M common/hw-gfx.ads 3 files changed, 8 insertions(+), 25 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/50/35750/3
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 3: Verified+1
Nico Huber has submitted this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Increase range of our main Frequency_Type
Increase `Frequency_Type` to 1MHz .. 2.5Ghz. We used to adapt it whenever necessary, e.g. when a new generation supported higher frequencies. But that got a little annoying. So let's choose a broader range that will hopefully lower the noise for some time.
1MHz is low enough for VGA resolution at 24p, and 2.5GHz is high enough for 8K at 60p. That should give us some margin.
Some corner cases required refactoring of some calculations and proofs. And, admittedly, the calculation in `HW.GFX.GMA.PCH.VGA` can in theory overflow. We prove absence of runtime errors by deferring the potential overflow to the modular `Word32` type. This is not perfect, but overflow or not, we have to expect to be called with a sane frequency anyway.
Change-Id: I3a159bc11ccadcaba8ad04e126e6feadfd46008e Signed-off-by: Nico Huber nico.h@gmx.de Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35750 Reviewed-by: Arthur Heymans arthur@aheymans.xyz Reviewed-by: Angel Pons th3fanbus@gmail.com --- M common/hw-gfx-dp_info.adb M common/hw-gfx-gma-pch-vga.adb M common/hw-gfx.ads 3 files changed, 8 insertions(+), 25 deletions(-)
Approvals: Nico Huber: Verified Arthur Heymans: Looks good to me, approved Angel Pons: Looks good to me, approved
diff --git a/common/hw-gfx-dp_info.adb b/common/hw-gfx-dp_info.adb index 7ac4556..d45826d 100644 --- a/common/hw-gfx-dp_info.adb +++ b/common/hw-gfx-dp_info.adb @@ -93,28 +93,11 @@ 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; + Lane_Pixel_Per_Second : constant Pos64 := + (((DP_Symbol_Rate (Link.Bandwidth) * 8) / 3) / Mode.BPC); + Count : constant Pos64 := + Div_Round_Up (Mode.Dotclock, Lane_Pixel_Per_Second); 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; @@ -184,8 +167,8 @@ 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 Calc_M_Type is Int64 range 0 .. 2 ** 38; + subtype Calc_N_Type is Int64 range 0 .. 2 ** 38; subtype N_Rounded_Type is Int64 range 0 .. Int64'Max (DATA_N_MAX, LINK_N_MAX);
diff --git a/common/hw-gfx-gma-pch-vga.adb b/common/hw-gfx-gma-pch-vga.adb index fd82740..eb7f9a0 100644 --- a/common/hw-gfx-gma-pch-vga.adb +++ b/common/hw-gfx-gma-pch-vga.adb @@ -135,7 +135,7 @@ Mask => SBI_SSCCTL_DISABLE);
Aux_Div := 16#0000_0000#; - Div_Sel := Word32 (Refclock / Mode.Dotclock - 2); + Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2; Phase_Inc := Word32 ((Refclock * 64) / Mode.Dotclock) and 16#0000_003f#; Phase_Dir := 16#0000_0000#;
diff --git a/common/hw-gfx.ads b/common/hw-gfx.ads index 93a3684..2cfc017 100644 --- a/common/hw-gfx.ads +++ b/common/hw-gfx.ads @@ -66,7 +66,7 @@ Rotation => No_Rotation, Offset => 0);
- subtype Frequency_Type is Pos64 range 19_200_000 .. 624_000_000; + subtype Frequency_Type is Pos64 range 1_000_000 .. 2_500_000_000;
type DP_Lane_Count is (DP_Lane_Count_1, DP_Lane_Count_2, DP_Lane_Count_4); subtype DP_Lane_Count_Type is Pos64 range 1 .. 4;
-
Angel Pons (Code Review) -
Arthur Heymans (Code Review)
-
Nico Huber (Code Review)