This section shows the requirements and e code for the packet data item.
The specification for the packet data items is described in "Data Packet Description" on page 224. Requirements for the packet data item are as follows:
Since the packet data item is expected to be generated on the fly, it should be defined as a struct.
Define an enumerated type to describe the payload. The values for that enumerated type are SMALL, MEDIUM, and LARGE. Create a field payload_size of that enumerated type.
Define an 8-bit field uid.
The field addr is two bits wide and its values should be constrained between 0 and 2 because there are only three output channels. This should be a soft constraint as another channel may be added later.
When payload_size is SMALL, the len field is constrained between [1..20]; when payload_size is MEDIUM, the len field is constrained between [21..44]; and when payload_size is LARGE, the len field is constrained between [45..63].
The field data item is a list of bytes. The length of the data list is equal to the len field.
The first byte of the data list is equal to the uid field.
Define an enumerated type to describe the type of parity. The values for that enumerated type are GOOD and BAD. Create a field packet_kind of that enumerated type.
When packet_kind is GOOD, the parity field is constrained to the correct value of parity, and when packet_kind is BAD, the parity field is constrained to the incorrect value of parity.
Parity is computed by means of a parity_calc() method.
Example 13-1 presents an e code for the packet data item.
Definition : Fields and constraints defining the packet <' -- Define the enumerated types type sbt_payload_size_t : [SMALL, MEDIUM, LARGE]; type sbt_packet_kind_t : [GOOD, BAD]; struct sbt_packet { payload_size : sbt_payload_size_t; -- Control field for the -- payload size uid : byte; -- Unique id field %addr : uint(bits : 2); keep soft addr in [0..2]; -- Only 3 port addresses, soft in -- case need to change in future %len : uint(bits : 6); -- Constrain the len according the payload_size control -- field keep payload_size == SMALL => len in [1..20]; keep payload_size == MEDIUM => len in [21..44]; keep payload_size == LARGE => len in [45..63]; %data[len] : list of byte; -- Constrain length of list == len -- Constrain the first data byte to be equal to the uid keep data[0] == uid; packet_kind : sbt_packet_kind_t; -- Control field for GOOD/BAD -- parity keep soft packet_kind == GOOD; -- Default: GOOD parity_computed : byte; -- Correct value of parity -- Assign the calculated parity to parity_computed keep parity_computed == parity_calc(len, addr, data); %parity : byte; -- May be assigned either a good or bad value -- Assign the correct parity value to the parity field when GOOD sbt_packet { keep parity == parity_computed; }; -- Do NOT assign the correct parity value to the parity field -- (random) when BAD sbt_packet { keep parity != parity_computed; }; -------------------------------------------------------------- -- parity_calc() -- -- Return the byte resulting from xor-ing among all data bytes -- and the byte resulting from concatenating addr and len -------------------------------------------------------------- parity_calc( len : uint(bits : 6), addr: uint(bits : 2), data: list of byte): byte is { result = %{len, addr}; -- Concatenation for each (data_byte) in data do { -- Iterate through the -- data list result ^= data_byte ; -- Same as: --result = result^data_byte; }; }; -- end parity_calc }; -- end sbt_packet '>