Previous Section Next Section

5.3 Implication Constraints

Implication constraints set up constraints on fields or list members based on another boolean expression being true. Implication constraints are specified using the => operator (Note that X => Y is equivalent to not X or (X and Y) ). Example 5-3 shows how the implication operator can be used in the context of a list. Each member of the list can be constrained separately based on the implicit index operator.

Example 5-3 Implication Constraints
Example to show implication constraints on a single field
as well as for constraining a list.
<'
type packet_size_t : [SHORT, MEDIUM, LONG]; //Defined enumerated type

struct packet { // Example shows implication constraint on field.
    size: packet_size_t; //Define a field of type packet_size_t.
                         //The generator picks a value for size.
                         //The size field is defined to control the
                         //generation of the len field.

    address: uint(bits:8); //Define an address 8 bits wide
    len: uint(bits:8); //Define a len field 8 bits wide
         keep size == SHORT => len < 10; //If size value picked is
                                         //SHORT, then a constraint
                                         //len < 10 applies.
         keep size == MEDIUM => len in [11..19];
                                         //If size value picked is
                                         //MEDIUM, then a constraint
                                         //len in [11..19] applies.
         keep size == LONG => len < 20; //If size value picked is
                                         //SHORT, then a constraint
                                         //len < 20 applies.

}; //End of struct packet

extend sys {
    packets: list of packet;
        keep for each (p) in packets {//Implication constraint on list
                                      //items, index is an implicit
                                      //iterator value.
            index == 0 => p.addr == 0; //For first packet, addr == 0.
            index == 1 => p.addr == 1; //For second packet, addr == 1.
           index > 2 => p.addr in [2..15]; //For other packets,
                                            // addr is in [2..15].
        };
}; //End of sys
'>
Previous Section Next Section