[sv-ec] RE: Mantis 3028, constraints for unique array elements

Ray,

As I mentioned in the meeting I do not support unique constraints on heterogeneous collections. No matter what semantics we try to dream up to make it work, the outcome will very likely be perceived as bugs by users. Furthermore, because it all happens inside the solver, with no apparent solver failures, users will have little recourse for debugging the problem.

I particularly dislike the idea of solving the constraint using maximal bit-width. Consider using your proposed semantics on the following example:

       bit [0:1] a;

       bit [0:2] b;

       int c;

       constraint X { unique { a, b, c } };

The solver would ignore the individual bit width while solving the above problem and solve all 3 values as 32-bits (the signdedness may be unimportant for equality). Then, a valid solution would be { 12, 8, 0 }, which after truncation would yield a=0, b=0, and c=0. Since a unique constrain is a request for mutually exclusive values, the user would expect a,b,c to have the different values.

Consider what happens if any of those variables are used in other constraints. For example, constraint { mem[b] == 5 }. Which 'b' value should the solver use? The one prior to truncation (8) or the one following truncation (0) ? Depending on the answer, an assertion post-constraint solving with the same expression may fail (assert mem[b] == 5).

Another approach would be for the solver to auto-insert additional constraints related to the bit-widths. In the example above this would mean the solver would add the following 2 constraints on top of the user-specified unique constraint:

       a inside {0:3};

       b inside {0:7};

This would result in a better solution (at least matching the users intent of mutually exclusive values). However, the additional constrains will make the distribution appear to be skewed (towards larger values on c) and users will probably not understand the reasons for the distribution change.

If we stick to arrays, its much simpler since they guarantee type homogeneity without the need to do any additional checking. But, I can live with the variable set as long as the homogeneous type is a hard restriction.

As for Chris' questions, here are my two cents:

- What about the case where there are more elements in the unique constraint than values?

       Constraints will fail in this case. Need not be done at compile time.

- Would randc variables be allowed in the unique constraint?

       I don't see the restriction as absolutely necessary, but it would surely simplify things.

- What if there are additional constraints on elements of the unique constraint?

       Those constraints should be honored by the solver. If they lead to a contradiction then the solver will fail.

As for sorted collections, I believe these are best handled in the procedural context - perhaps using the built-in array manipulation methods. Otherwise, they create very complex constrains that may fail or take too long to solve.

       Arturo

-----Original Message-----
From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of Chris Spear
Sent: Friday, August 20, 2010 9:31 AM
To: Ryan, Ray; sv-ec@eda.org
Subject: [sv-ec] RE: Mantis 3028, constraints for unique array elements

Hi Ray,

- What about the case where there are more elements in the unique constraint than values?

       bit a, b, c;

       constraint none_left {

              unique {a, b, c};

       }

This could be determined by analysis at compile time, and create an error.

- Would randc variables be allowed in the unique constraint? Probably not as they are solved before rand variables.

- What if there are additional constraints on elements of the unique constraint?

       bit [1:0] a, b, c;

       constraint four { unique {a, b, c}; }

       constraint at_least {

              a > 2; // unsolvable

              b > 2;

       }

- Once you have these issues worked out, is there any interest in sort and rsort constraints? These would put all elements in a sorted order, similar to the constraint:

       foreach (array[i])

              if (i > 0)

                     array[i] > array[i-1];

Thanks!

Chris

-----Original Message-----

From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of Ryan, Ray

Sent: Friday, August 20, 2010 12:11 PM

To: sv-ec@eda.org

Subject: [sv-ec] Mantis 3028, constraints for unique array elements

For mantis I'd suggest a grammar something like:

       constraint_expression ::=

              expression_or_dist ;

              | expression -> constraint_set

              | if ( expression ) constraint_set [ else constraint_set

]

              | foreach ( ps_or_hierarchical_array_identifier [

loop_variables ] ) constraint_set

              | unique { random_variable_list }

where "solve_before_list" is re-named to "random_variable_list" and

used in both "constraint_expression"

and "constraint_block_item" as in:

       constraint_block_item ::=

              solve random_variable_list before random_variable_list ;

              | constraint_expression

       random_variable_list ::= random_variable_primary { ,

random_variable_primary }

       random_variable_primary ::= [ implicit_class_handle . |

class_scope ] hierarchical_identifier select

The description of a 'unique' constraint would be something like:

       In a 'unique' constraint each random variable in the

random_variable_list must be of an integral type or an unpacked array,

associative array or queue where the element type is an integral type.

For unpacked random variables, the 'unique' constraint applies to each

packed element of the variable.

<unique can't be applied to a class handle.>

       A 'unique' constraint requires that each random variable in the

random_variable_list is assigned a unique random value.

       For the unique value comparison:

              - If any value is unsigned, all comparisons are unsigned

otherwise all are signed.

              - Each value is extended to the maximum width of any of

the values.

Some concerns I have about 'unique' constraints.

1) The construct needs to be a 'constraint_expression' and NOT a general

expression. If there is a kind of 'unique' expression then the following

constraints would be syntactically allowed:

       if ( <unique_expression> ) { <constraint> }

       <expression> || !<unique_expression>

I don't think it is meaningful (or what would it mean) to write a

constraint that a set of variable are NOT unique.

The same kind of syntactic restriction is there today for distribution,

implication, if-then-else and foreach constraints. That is, you can't

write a constraint requiring that a variable does NOT have a specific

distribution. I believe the same should apply to the unique constraint.

2) In defining the 'unique' construct as a kind of constraint, 'unique'

is only a keyword (a part of the constraint grammar). It does not become

a operator and so don't need to included in the other sections regarding

operators.

3) The above syntax would still allow a conditional 'unique' constraint.

That is,

       if (condition) { unique { A, B } }

If this is undesirable, the unique constraint could be defined as a

"constraint_block_item" rather than a "expression_constraint".

Solve-before constraint are defined this way so that they cannot be

conditional.

Regards,

Ray

--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.