Clever Geek Handbook

Specman e: How to restrict "all_different" to a list of structures?

I have my_list

one that is defined like this:

struct my_struct {
    comparator[2] : list of int(bits:16);
    something_else[2] : list of uint(bits:16);
};
...
my_list[10] : list of my_struct;

It is forbidden comparators

with the same index (0 or 1) to be the same in the entire list. When I restrict it this way (for example for index 0):

 keep my_list.all_different(it.comparator[0]);

I am getting compile error:

*** Error: GEN_NO_GENERATABLE_NOTIF: 

    Constraint without any generatable element.
    ... 
    keep my_list.all_different(it.comparator[0]);

How can I generate them all differently? Appreciate any help

+3


source to share


2 answers


It also works in one go:



keep for each (elem) in my_list {
  elem.comparator[0] not in my_list[0..max(0, index-1)].apply(.comparator[0]);
  elem.comparator[1] not in my_list[0..max(0, index-1)].apply(.comparator[1]);      
};
+2


source


When you link to my_list.comparator

, it doesn't do what you think it does. It happens that it concatenates all the lists comparator

into one list of list items. Try this by removing the constraint and printing it:

extend sys {
  my_list[10] : list of my_struct;

  run() is also {
    print my_list.comparator;
  };
};

In this case, you can create your own list of items comparator[0]

:



extend sys {
  comparators0 : list of int;
  keep comparators0.size() == my_list.size();
  keep for each (comp) in comparators0 {
    comp == my_list.comparator[index * 2];
  };
  keep comparators0.all_different(it);

  // just to make sure that we've sliced the appropriate elements
  run() is also {
    print my_list[0].comparator[0], comparators0[0];
    print my_list[1].comparator[0], comparators0[1];
    print my_list[2].comparator[0], comparators0[2];
  };
};

You can apply restriction all_different()

on this new list. To make sure this works, adding the following constraint should be inconsistent:

extend sys {
  // this constraint should cause a contradiction
  keep my_list[0].comparator[0] == my_list[1].comparator[0];
};
+2


source






More articles:


All Articles