CODEWITHSUNDEEP
constraintsverificationspecmane
Ank
Ank

Reputation: 1

keep has_each for a list in Specman

I am trying to create a keep with this functionality:

extend sys {
    ListA : list of uint;
    keep ListA.size() == 3; // For the example
    keep for each in ListA { // For the example
        it < 10;
    };
    
    ListB : list of uint;
    keep ListB.size() == 8;
};

I want to add a keep "has_each", meaning, I want to ensure that all of the members of ListA are generated in ListB.

One way I know how to do this is the following:

    keep for each in ListB {
        read_only(index < ListA.size()) => it == ListA[index];
    };

The problem with this method is if I have some form of keep that already sets the first index, for example if I also need the keep:

    keep ListB[0] > 10;

which in this case would cause a contradiction.

Another idea I tried that didn't work was:

keep read_only(ListA) in ListB;

Happy to hear any suggestions. Thank you

Upvotes: 0

Views: 118

Answers (2)

user3467290
user3467290

Reputation: 781

do you mean you want ListA to always be generated before ListB? are there other constraints on ListB, rather than on its size?

Upvotes: 0

user3467290
user3467290

Reputation: 781

you can use this

  keep for each in ListA {
    it in ListB;
};

Upvotes: 1

Related Questions