Specman e: How to constrain 'all_different' to list of structs?

988 views Asked by At

I have my_list that defined this way:

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 to comparators at the same index (0 or 1) to be the same in all the list. When I constrain it this way (e.g. for index 0):

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

I get compilation 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 different? Appreciate any help

2

There are 2 answers

0
Thorsten On BEST ANSWER

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]);      
};
0
Tudor Timi On

When you reference my_list.comparator it doesn't do what you think it does. What happens is that it concatenates all comparator lists into one bit 20 element list. Try it out by removing your constraint and printing it:

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

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

What you can do in this case is construct your own list of comparator[0] elements:

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 an all_different() constraint on this new list. To make sure it's working, adding the following constraint should cause a contradiction:

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