Subject: Re: [sv-ec] Can an ordering constraint cause the solver to fail ?
From: Arturo Salz (Arturo.Salz@synopsys.com)
Date: Tue Dec 02 2003 - 18:14:56 PST
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" <Ray_Ryan@mentorg.com>
To: <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
This archive was generated by hypermail 2b28 : Tue Dec 02 2003 - 18:16:04 PST