RE: [sv-ec] Can an ordering constraint cause the solver to fail ?


Subject: RE: [sv-ec] Can an ordering constraint cause the solver to fail ?
From: David W. Smith (David.Smith@synopsys.com)
Date: Mon Dec 15 2003 - 09:31:34 PST


Michael,
I would recommend that you raise this as a motion with the suggested wording
during the meeting. We can then discuss it, refine it, and approve it as
appropriate.

Regards
David

-----Original Message-----
From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of Michael
Burns
Sent: Monday, December 15, 2003 8:23 AM
To: Ray_Ryan@mentorg.com
Cc: Arturo.Salz@Synopsys.COM; sv-ec@eda.org
Subject: Re: [sv-ec] Can an ordering constraint cause the solver to fail ?

Hi folks,

I think we need to have some clarification in the LRM for this issue.
How about we add some words a few lines down from the part of section
12.4.8 referred to by Ray originally - specifically, where it now says
this:

  "Variable ordering can be used to force selected corner cases to
  occur more frequently than they would otherwise."

I'd like to add this:

  "Variable ordering can be used to force selected corner cases to
  occur more frequently than they would otherwise. However, a "solve
  ... before ..." constraint does not change the solution space, and
  so cannot introduce the possiblility of a constraint solver failure
  where such a possiblity did not exist without the "solve ... before"
  constraint."

(I'll leave it to those more versed in technical writing to decide on
the lexical conventions that should be used to refer to the "solve
... before ..." constraints)

Also, I think we should add something to 12.4.10 to explicitly
differentiate its behavior from that of 12.4.8. How about, after
this:

  "Thus, constraint D is solved separately before constraint C, which
  uses the values of y and F(y) as a state variables."

we add this:

  "Note that the behavior for variable ordering implied by function
  arguments differs from the behavior for ordering specified using the
  "solve ... before ..." constraint; function argument variable
  ordering can change the solution space, since constraints on
  higher-priority variables are solved without considering
  lower-priority constraints at all."

Overall, I'd agree with Ray that it would be useful to allow user
control over the "hard" ordering - we've found a need for that
internally in Motorola. However, it's a bit late for that in 3.1a -
can we add it as a request for future enhancement?

Thanks,

Mike

>Arturo,
>
>In the new section 12.4.10 (Functions in Constraints) there is a
>different definition or usage of 'variable ordering' and 'solve before'.
>The 5th bullit at the end of the section states:
>
>Random variables used as function arguments shall establish an implicit
>variable ordering or priority. Constraints that include only variables
>with higher priority are solved before other, lower priority,
>constraints. Random variables solved as part of a higher priority set of
>constraints become state variables to the remaining set of constraints.
>For example:
> class B;
> rand int x, y;
> constraint C { x <= F(y); }
> constraint D { y inside {2, 4, 8 } };
> endclass;
>Forces y to be solved before x. Thus, constraint D is solved separately
>before constraint C, which uses the values of y and F(y) as a state
>variables.
>Within each prioritized set of constrained, cyclical (randc) variables
>are solved first.
>
>This section rather clearly states the behavior I expected for ordering
>of variables. Specifically:
> (a) Constraints that include only variables with higher priority are
>solved before other, lower priority constraints.
> (b) Random variables solved as part of a higher priority set of
>constraints become state variables to the remaining set of constraints.
>
>In the above example, if we change "F(y)" to simply "y" and explicitly
>add the constraint "solve y before x", then:
> - First y is solved using only constraint D - as per (a).
> - Second x is solved using constraint C with y as a state variable - as
>per (b).
>If constraint C were like the constraint in my original email, x might
>not be solveable.
>
>Although this section does not specifically state that an "implicit
>variable ordering" is the same as an "explicit variable ordering" (ie a
>solve-before constraint), it would seem intuitive that this is the case.
>Furthermore, I believe it is very useful for the User to be able to
>specify a solve ordering (possibly in addition to distribution ordering)
>to reduce constraint complexity (ie potentially reduce solver time).
>
>Ray
>
>
>-----Original Message-----
>From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of
>Arturo Salz
>Sent: Tuesday, December 02, 2003 6:15 PM
>To: Ryan, Ray; sv-ec@eda.org
>Subject: Re: [sv-ec] Can an ordering constraint cause the solver to fail
>?
>
>
>Ray,
>
>The short answer is no. Ordering constraints affects only the
>distribution, not the
>solution space. Hence, a "solve before" constraint can never cause a
>failure.
>
>Note that the statement in question:
> "The constraints provide a mechanism for ordering variables so that
>s can be
> chosen independently of d."
>Uses the word "chosen", not "solved". This choice is intended to mean
>that the
>selection (i.e., the distribution) of s is independent of d. The
>solution space is
>still constrained by both s and d.
>
>Using your example, the ordering constraint does not change the solution
>space.
>Therefore, x can only have even values. With the ordering constraint all
>even
>values of x have the same probablity (1/128). Without the ordering
>constraint, the
>cross-product of all possible values of x and y would have the same
>probability.
>
>Perhaps that sentence should state:
> "The constraints provide a mechanism for ordering variables so that
>s can be
> chosen with a distribution that is independent of d."
>
> Arturo
>
>
>----- Original Message -----
>From: "Ryan, Ray" < <mailto:Ray_Ryan@mentorg.com> Ray_Ryan@mentorg.com>
>To: < <mailto:sv-ec@eda.org> sv-ec@eda.org>
>Sent: Tuesday, December 02, 2003 4:02 PM
>Subject: [sv-ec] Can an ordering constraint cause the solver to fail ?
>
>
>
>In section 12.4.8 Variable ordering, referring to ordering constraints,
>the
>LRM states that:
>
>"The constraints provide a mechanism for ordering variables so that s
>can be
>chosen independently of d."
>
>This statement is referring to the constraint "solve s before d".
>
>Since s is "chosen independently of d", can the choice for 's' result in
>a
>constraint for 'd' than that cannot be met. For example:
>
>class B
> rand bit[7:0] x, y;
> constraint c1 { 2*y == x; }
> constraint ord { solve x before y; }
>end class
>
>When 'x' is solved before 'y', if an even value is choosen for 'x', then
>when 'y' is
>solved there is a solution. However, if an odd value is choosen, then
>the solver
>cannot choose a value for 'y' that meets constraint 'c1'.
>
>My expectation is case is unstable / over-constrainted and it is valid
>for
>the solver to sometimes fail.
>
>Thanks,
>Ray
>
>
>
>------_=_NextPart_001_01C3B9CE.FC202A39--



This archive was generated by hypermail 2b28 : Mon Dec 15 2003 - 09:34:22 PST