Specman На Fly Generation: Как ограничить список, значения которого отличаются друг от друга по крайней мере, 2

Question

мне нужно генерировать случайные значения списка со следующим Constrain:

my_list[i] not in [my_list[i-1] .. my_list[i-1] + 1] 

т.е. всех значений в списке отличаются друг от друга и, по меньшей мере, с разницей между собой. Все варианты кода, которые я пробовал, не удалось, например:

var prev_val : uint = 0; 
    gen my_list keeping { 
     it.size() == LIST_SIZE; 
     it.all_different(it); 

     for each (val) in it { 
       val not in [prev_val .. prev_val + 1]; 
       prev_val = val; 
     }; 
    }; 

Как такой список может быть сгенерирован? Спасибо за вашу помощь

Answer 1

Я не уверен, я полностью понимаю запрос, но следующий код:

gen my_list keeping { 
    it.size() == LIST_SIZE; 
    it.all_different(it); 
    keep for each (val) in it { 
     val != prev; 
     val != prev + 1; 
    }; 
}; 

Это будет генерировать список (все элементы будут генерировать вместе) в соответствии с вашим правилом:

my_list[i] not in [my_list[i-1] .. my_list[i-1] + 1] 

Но следующий список является допустимым решением: 0,2,1,3,5,4,6,8,7,9,11,10,12, ... , который не соответствует «всем значениям в список отличается и, по крайней мере, с разницей между двумя ».

Для создания списка в соответствии с «Текст запроса» на, вы должны использовать двойной держать для каждого и абс:

gen my_list keeping { 
    it.size() == LIST_SIZE; 
    for each (val1) using index (i1) in it { 
     for each (val2) using index (i2) in it { 
      i1 < i2 => abs(val1-val2) >= 2; 
    }; 
}; 

Если вы хотите my_list быть отсортированы (и будет решаться быстрее):

gen my_list keeping { 
    it.size() == LIST_SIZE; 
    it.size() == LIST_SIZE; 
    it.all_different(it); 
    for each (val) in it { 
     val >= prev + 2; 
    }; 
}; 

Answer 2

Вы можете попробовать следующее:

gen my_list keeping { 
    it.size() == 10; 
    it.all_different(it); 

    for each (val) in it { 
    index > 0 => 
     val not in [value(it[index - 1]) .. value(it[index - 1]) + 1]; 
    }; 
}; 

Решатель требует it[index - 1] выражения в ограничении быть «фиксированным» в точке поколения, следовательно, использование value(...). Это означает, что список будет генерироваться по элементу.

Если это проблема, вы могли бы изменить, чтобы:

index > 0 => 
     val != it[index - 1] + 1; 

Это должно быть эквивалентно, так как all_different(...) ограничение следует убедиться, что элемент не имеет такое же значение, как и предыдущий. Естественно, это не сработает, если у вас есть более широкий набор.