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 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 '>