cubedos-lib-tc_frames.ads

1--------------------------------------------------------------------------------
2-- FILE : cubedos-lib-tc_frames.ads
3-- SUBJECT: Specification of a package containing CCSDS space packet encoding/decoding logic.
4-- AUTHOR : (C) Copyright 2024 by Vermont State University
5--
6--------------------------------------------------------------------------------
7pragma SPARK_Mode(On);
8
9package CubedOS.Lib.TC_Frames is
10
11 subtype Primary_Header is Octet_Array(1 .. 6);
12
13 subtype Packet_Data_Index_Type is
14 Natural range 1 .. 65536; -- TODO: Should this upper limit be generic?
15 subtype Packet_Data_Size_Type is
16 Natural range Packet_Data_Index_Type'First .. Packet_Data_Index_Type'Last;
17 type Packet_Data is array(Packet_Data_Index_Type range <>) of Octet;
18
19 type APID_Type is mod 2**11;
20 type Packet_Type_Type is (Telemetry, Telecommand);
21 type Segementation_Flag_Type is (Continuation_Segment, First_Segment, Last_Segment, Unsegmented);
22 type Sequence_Count_Type is mod 2**14;
23
24 -- Space Packet Decoding
25 ------------------------
26 -- ToDo: Change for TC Frames
27
28 function Extract_Packet_Type(Header : in Primary_Header) return Packet_Type_Type is
29 (case (Header(1) and 16#10#) is
30 when 16#00# => Telemetry,
31 when 16#10# => Telecommand,
32 when others => Telecommand) -- Should never occur!
33 with Inline;
34
35
36 function Extract_Secondary_Header_Flag(Header : in Primary_Header) return Boolean is
37 ((Header(1) and 16#08#) = 16#08#)
38 with Inline;
39
40
41 function Extract_APID(Header : in Primary_Header) return APID_Type is
42 (APID_Type
43 (Shift_Left(Double_Octet(Header(1) and 16#07#), 8) or Double_Octet(Header(2))))
44 with Inline;
45
46
47 function Extract_Segementation_Flags(Header : in Primary_Header) return Segementation_Flag_Type is
48 (case (Header(3) and 16#C0#) is
49 when 16#00# => Continuation_Segment,
50 when 16#40# => First_Segment,
51 when 16#80# => Last_Segment,
52 when 16#C0# => Unsegmented,
53 when others => Unsegmented) -- Should never occur!
54 with Inline;
55
56
57 function Extract_Sequence_Count(Header : in Primary_Header) return Sequence_Count_Type is
58 (Sequence_Count_Type
59 (Shift_Left(Double_Octet(Header(3) and 16#3F#), 8) or Double_Octet(Header(4))))
60 with Inline;
61
62
63 function Extract_Data_Length(Header : in Primary_Header) return Packet_Data_Size_Type is
64 (Packet_Data_Size_Type
65 (Natural(Shift_Left(Double_Octet(Header(5)), 8) or Double_Octet(Header(6))) + 1))
66 with Inline;
67
68
69 -- TC Frames Encoding
70 ------------------------
71 -- Non-urgent, to be implemented later
72
73 function Format_Primary_Header
74 (APID : in APID_Type;
75 Packet_Type : in Packet_Type_Type;
76 Sequence_Count : in Sequence_Count_Type;
77 Data_Length : in Packet_Data_Size_Type;
78 Secondary_Header_Flag : in Boolean := False;
79 Segementation_Flags : in Segementation_Flag_Type := Unsegmented) return Primary_Header
80 with
81 Post =>
82 ((Format_Primary_Header'Result(1) and 16#E0#) = 16#00#) and
83 (Extract_Packet_Type(Format_Primary_Header'Result) = Packet_Type) and
84 ((Extract_Secondary_Header_Flag(Format_Primary_Header'Result) and Secondary_Header_Flag)
85 or (not Extract_Secondary_Header_Flag(Format_Primary_Header'Result) and not Secondary_Header_Flag)) and
86 (Extract_APID(Format_Primary_Header'Result) = APID) and
87 (Extract_Segementation_Flags(Format_Primary_Header'Result) = Segementation_Flags) and
88 (Extract_Sequence_Count(Format_Primary_Header'Result) = Sequence_Count);
89
90end CubedOS.Lib.TC_Frames;