Calculating probability for solve x,y before z

SystemVerilog
, , ,
1

Hi Forum,
I am trying to calculate the probability of each possible output using solve before constraint

Solve before using 2 random variables solve x before y

rand bit x;
rand bit [1:0] y;

constraint a2 { (x == 0) -> (y==0);

                solve x before y; }

Within solve x before y as x appears first, I calculate the probability starting with x

As x could be either 0 or 1 i.e probability of each would be (1/2)

When x is 1 , y could be 0/1/2/3.
Hence the probability of y == 0/1/2/3 ( when x is 1 ) would be (1/2) divided into 4 equal parts

x y Probability
0 0 1/2
0 1 0
0 2 0
0 3 0
1 0 1/8
1 1 1/8
1 2 1/8
1 3 1/8

On enhancing the solve before using 3 random variables solve x,y before z

rand bit x;
rand bit [1:0] y,z;

constraint a3 { (x == 0) -> { (y==0); (z==0); }

                solve x,y before z; }
x y z Probability
0 0 0 ?
0 0 1 0
0 0 2 0
0 0 3 0
0 1 0 0
0 1 1 0
0 1 2 0
0 1 3 0
0 2 0 0
0 2 1 0
0 2 2 0
0 2 3 0
0 3 0 0
0 3 1 0
0 3 2 0
0 3 3 0
1 0 0 ?
1 0 1 ?
1 0 2 ?
1 0 3 ?
1 1 0 ?
1 1 1 ?
1 1 2 ?
1 1 3 ?
1 2 0 ?
1 2 1 ?
1 2 2 ?
1 2 3 ?
1 3 0 ?
1 3 1 ?
1 3 2 ?
1 3 3 ?

How do I calculate the probability of each valid combination ?

My intuition is that out of the 5 valid combinations of {x,y} as {0,0} / {1,0} / {1,1} / {1,2} / {1,3}
the probability of each combination would be same i.e equal to (1/5).
Hence probability of 1st row ( x == 0 and y == 0 and z == 0 ) would be (1/5)
For the remaining 4 combinations of {x,y} there are 4 possible values of z.
Hence the probability of each of the last 16 rows would be (1/5) x (1/4) i.e (1/20)

(Q) Is my understanding correct ?

2

The probability would be easier to comprehend if you removed the rows with zero probability. In that case, you would observe that the probability of y having the values 1/2/3 would be 1/5 each. However, since y==0 appears twice, it has a probability of 2/5.

Similarly, in the second example, there would be 17 rows. For each variable y and z, the values 1/2/3 appear four times, so their probability would be 4/17. The value 0 appears five times, so its probability is 5/17.

3

Dave,
I am confused with the probability you have mentioned.
As my understanding the above probability is without using solve before

rand bit x;
rand bit [1:0] y;

constraint a0 { (x == 0) -> (y==0); } //  No solve before

With a0 the probability of each combination would be same i.e (1/5)

x y Probability
0 0 1/5
1 0 1/5
1 1 1/5
1 2 1/5
1 3 1/5

(Q) On adding solve x before y (constraint a2 ) wouldn’t the probability change to ::

x y Probability
0 0 1/2
1 0 1/8
1 1 1/8
1 2 1/8
1 3 1/8

If I were to use solve y before x I believe the probability would be

x y Probability
0 0 1/8
1 0 1/8
1 1 1/4
1 2 1/4
1 3 1/4
4

Sorry I posted before finishing my answer. You are correct in the first example when adding solve x before y, the probability of y==0 becomes 1/2 + 1/8, or 5/8. For solve y before x, the probability of x==0 becomes 1/8.

For the second example, I think you meant to say solve x before y,z as solving x and y together doesn’t make any sense with the constraints you have. Then the probability of y==0 becomes 1/2+1/16 or 9/16