time: Revise state abstraction
Make abstract state `State` of HW.Time.Timer, that's used to derive the
Hz value for instance, External. This helps to fix flow issues in the
mutime implementation and also matches real hardware better: The clock
rate may be derived from the hardware state.
HW.Time.Timer.Hz had to be made a volatile function, therefore.
Change-Id: I35af2d0db1acbf9652ea00763aa288545746bb79
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/c/libhwbase/+/26838
Tested-by: Nico Huber <nico.h@gmx.de>
Reviewed-by: Reto Buerki <reet@codelabs.ch>
diff --git a/ada/mutime/hw-time-timer.adb b/ada/mutime/hw-time-timer.adb
index 272289c..c683d6f 100644
--- a/ada/mutime/hw-time-timer.adb
+++ b/ada/mutime/hw-time-timer.adb
@@ -17,8 +17,8 @@
with Muschedinfo;
package body HW.Time.Timer
- with Refined_State => (Timer_State => null,
- Abstract_Time => (Sinfo, Sched_Info))
+ with Refined_State => (Timer_State => (Sinfo),
+ Abstract_Time => (Sched_Info))
is
Sinfo_Base_Address : constant := 16#000e_0000_0000#;
Sinfo_Page_Size : constant
@@ -27,6 +27,8 @@
Sinfo : Musinfo.Subject_Info_Type
with
+ Volatile,
+ Async_Writers,
Address => System'To_Address (Sinfo_Base_Address);
Sched_Info : Muschedinfo.Scheduling_Info_Type
@@ -51,9 +53,11 @@
return T (TSC_Schedule_End);
end Raw_Value_Max;
- function Hz return T is
+ function Hz return T
+ is
+ Khz : constant T := T (Sinfo.TSC_Khz);
begin
- return T (Sinfo.TSC_Khz) * 1000;
+ return Khz * 1000;
end Hz;
end HW.Time.Timer;