Previous Section Next Section

13.1 Defining the Packet Data Item

This section shows the requirements and e code for the packet data item.

13.1.1 Requirements 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:

13.1.2 e Code for the Packet Data Item

Example 13-1 presents an e code for the packet data item.

Example 13-1 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
'>
Previous Section Next Section