Solve order of randsz_list_t size constraints within foreach incorrect [v0.8.8]

[alwilson]

I was looking into adding a randsz_list_t example to the docs and I think I ran into a bug with size constraints within foreach loops. Also I had fun digging around for this, so I might be making a mountain out of mole hill. ;)

In this example I constrain the random list size to be 1 to 5, all elements less than list size, and all elements unique. I expect the list size to be random between 1 to 5, but it's always 5. I can constrain the size to be equal to values between 1 and 4, which works, but distributions and solve-before don't change it.

import vsc

@vsc.randobj
class my_cls(object):

    def __init__(self):
        self.l = vsc.randsz_list_t(vsc.uint8_t())

    @vsc.constraint
    def l_c(self):
        self.l.size > 0
        self.l.size <= 5

        with vsc.foreach(self.l, it=True) as it:
            it < self.l.size
        
        vsc.unique(self.l)

my_i = my_cls()
hist = [0] * 6
for _ in range(100):
    my_i.randomize()
    hist[len(my_i.l)] += 1
print(hist)

---------------------------------
Output
---------------------------------
[0, 0, 0, 0, 0, 100]

Looking at the debug output's final model I think it makes sense. The foreach constraining all elements to be less than list size also means the list size must be greater than all elements, regardless of whether those elements end up in the final list. So I think the constraints as generated by pyvsc will always result in a max sized list.

Debug output final model:

Final Model:
  <anonymous> {
    rand unsigned [32] l.size
    l {
        rand unsigned [8] l.l[0]
        rand unsigned [8] l.l[1]
        rand unsigned [8] l.l[2]
        rand unsigned [8] l.l[3]
        rand unsigned [8] l.l[4]
    }
    constraint l_c {
        (l.size > 0);
        (l.size <= 5);
        (l.l[0] < l.size);
        (l.l[1] < l.size);
        (l.l[2] < l.size);
        (l.l[3] < l.size);
        (l.l[4] < l.size);
        unique [l];  # I have a local fix to print unique constraints
     }
}

LRM Section 18.5.8.1 "foreach iterative constraints" and 18.5.13 "Constraint guards" go into more detail, but I believe it boils down to array size needs to be considered a state variable when within a foreach loop on the corresponding array. Although part of 18.5.8.1 also mentions that users must explicitly exclude indices that would be invalid or out-of-bounds. When I tried the first example in SV though it doesn't need an conditional on the bounds b/c I think it's implicit?

So I think either pyvsc users need to wrap up foreach constraints involving that list's size in a conditional, or pyvsc needs to wrap them up when creating/expanding constraints, or pyvsc needs to partition the array size constrains in scenarios where the array size should be a state variable.

Going with the first solution (workaround?), this kind of works, although it differs in distribution for list size b/c it's solved alongside the list elements rather than in a previous partition. Using vsc.solve_order(self.l.size, self.l) helps with that though.

        vsc.solve_order(self.l.size, self.l)

        with vsc.foreach(self.l, idx=True, it=True) as (i, it):
            with vsc.if_then(i < self.l.size):
                it < self.l.size

---------------------------------
Final Model with new constraints
---------------------------------
    constraint l_c {
        (l.size > 0);
        (l.size <= 5);
        solve size before l
        if ((0 < l.size)) {
            (l.l[0] < l.size);
        }
        if ((1 < l.size)) {
            (l.l[1] < l.size);
        }
        if ((2 < l.size)) {
            (l.l[2] < l.size);
        }
        if ((3 < l.size)) {
            (l.l[3] < l.size);
        }
        if ((4 < l.size)) {
            (l.l[4] < l.size);
        }
        unique [l];
     }
---------------------------------
Output
---------------------------------
[0, 24, 15, 16, 22, 23]

I started playing with detecting randsz lists when expanding foreach constraints to wrap them in the above constraint, but I'm still thinking about it and curious what pyvsc's actual strategy here should be.

[mballance]

Hi Al,
As far as I can tell, PyVSC's behavior is correct in this case. As you note, the element-bound and unique constraints combine to force the size to always be 5. It's well-worth trying to remove the unique constraint to see if you get a (more) random distribution on size. It's always possible that more work needs to be put into getting better distribution over random-list sizes.

[alwilson]

Removing unique does allow other list sizes, but I'm less concerned about distribution and more concerned that it doesn't match up with SV.

These would be the equivalent SV constraints, and when randomized it has sizes 1 to 5:

    rand bit [8:0] l[$];

    constraint l_c {
        l.size() > 0;
        l.size() <= 5;
        foreach(l[i]) {
            l[i] < l.size();
        }
        unique {l};
    }

SV solves size before the foreach and unique constraints there's no need to wrap either in if/implies statements to prevent invalid access. Pyvsc creates all possible list elements and expands constraints for those elements regardless of list membership, so to get the equivalent/closer to SV you would need to add if/implies.

Also, with constraints like unique I think you would need to roll you own unique constraint with 2 foreach loops and implies. I'm sure there are other examples where unexpected things happen b/c all elements have entered constraint like this.

[alwilson]

Well, I tried to come up with some more examples, but some of them aren't always solvable in SV b/c the size happens before other constraints get considered, but then solvable by pyvsc b/c it's all part of the same partition. Maybe this is a weird corner for both SV and pyvsc.

While thinking of examples I think I stumbled across a re-randomization issue with array sums. If the sum constraint for a list comes before the size, then on subsequent randomization the sum constraint will use the size of the previous array. I can file a different issue for that though.

[mballance]

Hi Alex,
Just getting a chance to look at and think about this again. My understanding is that PyVSC only unrolls constraints for array elements it intends to use. Consequently, the fact that it's unrolling 5 times indicates that there is a PyVSC bug in array-size distribution. Can you confirm by omitting the foreach constraint? I suspect that the array size will still be fixed to 5.

Also, yes, please find an additional issue on the sum constraint.

[alwilson]

When I remove the foreach constraint I get a dist on size from 1-5:

[0, 19, 19, 22, 24, 16]

But when I remove the foreach constraint the array size is solved by itself in a separate RandSet:

RandSet[0]
  Field: l.size is_rand=True [[1, 5]]
  Constraint: (l.size > 0);
  Constraint: (l.size <= 5);

The problem in my example is that foreach(l[i]) { l[i] < l.size(); } ties array size and all other constraints involving the array into a single RandSet. PyVSC builds foreach constraints using the default/worst case array size which, with the unique constraint, creates 4 < l.size() and pins array size to 5.

This is what the RandSet looks like with the foreach. The unique constraint means at least one array element is 4, which pins l.size to 5.

RandSet[0]
  Field: l.size is_rand=True [[1, 5]]
  Field: l.l[0] is_rand=True [[0, 4]]
  Field: l.l[1] is_rand=True [[0, 4]]
  Field: l.l[2] is_rand=True [[0, 4]]
  Field: l.l[3] is_rand=True [[0, 4]]
  Field: l.l[4] is_rand=True [[0, 4]]
  Constraint: (l.size > 0);
  Constraint: (l.size <= 5);
  Constraint: (l.l[0] < l.size);
  Constraint: (l.l[1] < l.size);
  Constraint: (l.l[2] < l.size);
  Constraint: (l.l[3] < l.size);
  Constraint: (l.l[4] < l.size);
  Constraint: unique(l)