I've defined the following struct :
struct my_struct {
var_a : bit;
var_b : bit;
};
In another struct, I've instantiated a list of this struct :
struct another_struct {
my_list : list of my_struct;
list_size : uint;
keep list_size >= 4;
};
What I want to do is to constraint my_list to have at least all the possible iterations of both var_a and var_b but not only, i.e. to combine both constraints :
extend another_struct {
keep my_list.is_all_iterations(.var_a, .var_b);
keep my_list.size() == list_size;
};
Is there any way to achieve that ?
Thanks
I suggest to create a helper list and constrain it to be a sublist of my_list:
Not sure if that works, but I expect the last constraint to be bi-directional.