Implication/if-else style constraints are bi-directional. What does this mean?
typedef enum {little,big,medium} e_mode;
bit [10:0] len;
e_mode mode;
constraint c1 {mode == little -> len == 10 ;
Does it mean 1)when mode =little ,len should be 10
2) when len = 10 mode= little?
I expected tool to give above results but tool is generating a packet which had mode = big, len =10
The ‘->’ is an implication operator which means that when mode is equal to ‘little’, then len will be constrained to be 10. However, if mode is not equal to ‘little’, there is no constraint on what len can be. Therefore, mode = big and len = 10 satisfy the constraint provided.
In reply to cgales:
All expression operators are treated bidirectionally, including the implication operator (->)
This is written in LRM. What does this mean?
The use of the word “bidirectional” is a poor choice of words. Section 18.5.10 Variable ordering explains this a little better, but the rest of the LRM still needs lots of work.
The LRM is trying to say that although an expression has a precedence order of evaluation, that ordering does not apply to the choice of values for each value. Every combination of valid solutions has equal probability.
So even though the expression A → B reads as if the value of A determines the value of B, the value of B can also determine the value of A. If B is false, then A cannot be true !B → !A. This implicit constraint is where the bidirectional term came from. Without any other variable ordering, the values A and B are determined together.