--
-- Copyright (c) 2023, German Rivera
--
--
-- SPDX-License-Identifier: Apache-2.0
--
with System.Storage_Elements;
package HiRTOS.Separation_Kernel.Partition
with SPARK_Mode => On
is
use HiRTOS_Cpu_Multi_Core_Interface;
use System.Storage_Elements;
use type System.Address;
--
-- Create new partition
--
procedure Create_Partition (Reset_Handler_Address : System.Address;
Interrupt_Vector_Table_Address : System.Address;
TCM_Base_Address : System.Address;
TCM_Size_In_Bytes : System.Storage_Elements.Integer_Address;
SRAM_Base_Address : System.Address;
SRAM_Size_In_Bytes : System.Storage_Elements.Integer_Address;
MMIO_Base_Address : System.Address;
MMIO_Size_In_Bytes : System.Storage_Elements.Integer_Address;
Partition_Id : out Valid_Partition_Id_Type;
Suspended : Boolean := False)
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode
and then
(if TCM_Base_Address /= System.Null_Address then
TCM_Size_In_Bytes /= 0
else
TCM_Size_In_Bytes = 0)
and then
(if SRAM_Base_Address /= System.Null_Address then
SRAM_Size_In_Bytes /= 0
else
SRAM_Size_In_Bytes = 0)
and then
(if MMIO_Base_Address /= System.Null_Address then
MMIO_Size_In_Bytes /= 0
else
MMIO_Size_In_Bytes = 0)
and then
((To_Integer (Reset_Handler_Address) in
To_Integer (TCM_Base_Address) ..
To_Integer (TCM_Base_Address) + TCM_Size_In_Bytes - 1
and then
To_Integer (Interrupt_Vector_Table_Address) in
To_Integer (TCM_Base_Address) ..
To_Integer (TCM_Base_Address) + TCM_Size_In_Bytes - 1)
or else
(To_Integer (Reset_Handler_Address) in
To_Integer (SRAM_Base_Address) ..
To_Integer (SRAM_Base_Address) + SRAM_Size_In_Bytes - 1
and then
To_Integer (Interrupt_Vector_Table_Address) in
To_Integer (SRAM_Base_Address) ..
To_Integer (SRAM_Base_Address) + SRAM_Size_In_Bytes - 1));
--
-- Tell if a parittion is currently suspended
--
function Is_Partition_Suspended (Partition_Id : Valid_Partition_Id_Type) return Boolean
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode;
--
-- Set the "fail-over to" parittion for a given partition
--
procedure Set_Partition_Failover (Partition_Id : Valid_Partition_Id_Type;
Failover_Partition_Id : Valid_Partition_Id_Type)
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode
and then
Is_Partition_Suspended (Failover_Partition_Id);
--
-- Return the Id of the current partition executing on the current CPU core,
-- if that core is running in partition context, or the Id of the last partition
-- prempted by an interrupt handler, if running in interrupt context.
--
function Get_Current_Partition_Id return Partition_Id_Type
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode;
end HiRTOS.Separation_Kernel.Partition;