Предположения / утверждения SVA для непрерывного ввода данных

Полагая, что вы говорите о методологии формальной проверки.

Для формальной проверки вам не нужно создавать какой-либо модуль, управляющий стимулом. Но вместо этого стимул будет управляться самим инструментом, и вы можете направить инструмент с помощью предполагаемых свойств для создания юридического стимула.

Если вы не предоставляете никаких предположений, инструмент может обрабатывать любые случайные данные и оценивать утверждения, и в этом случае вы можете получить ложную фальсификацию. Этот сценарий известен как «Ограничено».

Точно так же, если вы предоставите слишком много предположений, вы можете пропустить некоторые допустимые комбинации входных данных. Этот сценарий известен как «Превышение ограничений».

Поэтому очень важно предоставлять точные предположения.

В вашем случае ваше предположение может выглядеть примерно так:

property channel_change;
  // To check the next consecutive ID, after data transfer
  @(posedge clk)
  (id) throughout (valid [=3]) |=> valid && (id == $past(id) + 1)
endproperty

assume property (channel_change);

Для получения более подробной информации о методологии формальной проверки посетите мой блог: Что такое формальная проверка? [1/2] и Что такое формальная проверка? [2/2]

Приведенный вами пример не перекрывается. После трех выборок с одним и тем же идентификатором, как только появится еще одна выборка данных со следующим идентификатором, будет совпадать консеквент, и все свойство будет сохранено.

В любом случае, совпадение попыток - это факт жизни. Инструмент всегда оценивает (заявленные или предполагаемые) свойства в каждом тактовом цикле, чтобы выяснить, возможно ли совпадение. Если он решает, что это так, он начинает новую попытку; если нет, то идет дальше. Невозможно сказать «не пытайтесь рассматривать это утверждение, пока оно уже предпринимается», потому что вы никогда не знаете, завершится ли попытка совпадением или нет.

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

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

assume property (
  sample_with_some_id_came |->
    came_out_of_reset_and_no_samples_were_sent.triggered or
      one_or_two_samples_with_same_id_sent_after_reset.triggered or
      three_samples_with_the_previous_id_sent.triggered
);

Я также не уверен, не вызовет ли ваше предположение какое-то «бесконечное» поведение, поскольку вы говорите, что всегда должен быть следующий образец после 3 образцов с тем же идентификатором.

Я определю три sequence для определения того же идентификатора на следующем действующем (same_id); для обнаружения изменения id на следующем действительном (change_id); и для обнаружения действительного пакета (packet_id). Тогда у меня будет одно свойство для мониторинга в пределах четырех valid, есть только три возможных случая: т.е.

case1: (id, id,   id,   id+1) OR 
case2: (id, id+1, id+1, id+1) OR
case3: (id, id,   id+1, id+1) 

Пожалуйста, смотрите мои коды ниже. Я не тестировал, это только из моих мыслей. Надеюсь, это сработает. Хорошо то, что property будет работать только в течение 4 тактов часов, и в каждом такте часов есть только один поток. Так мы можем избежать взрыва потока.

// To detect same id within two non-consecutive valid,
// (a,a)
sequence same_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence


// To detect valid packet
// (a,a,a)
sequence packet_id;
  int prev_id;
  @(posedge clk)
  same_id, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence   

// To detect any change of ID
// any (a,b)
sequence change_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id+1;
endsequence

// Put all together, in any four non-consecutive valid, there are only three cases: a,b,b,b OR b,b,b,c OR a,a,b,b
property next_id;
  int prev_id;
  @(posedge clk)
  (change_id ##0 packet_id) or         // a,b,b,b
  (packet_id ##0 change_id) or         // b,b,b,c
  (same_id ##0 change_id ##0 same_id); // a,a,b,b
endproperty

assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> (valid[->1] ##0 id == $past(id,,valid))[*2] ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));

Разрушение: предшествующий импликации либо действительный, произошел дважды, и текущий идентификатор во время временного шага, на котором действительный завершился, повышаясь дважды ([->] вместо [=]), отличается от идентификатора последнего времени, когда действительное повышалось:

((valid[->2] ##0 id != $past(id,,valid))

или действительный стал высоким сразу после первого:

($fell(rst) ##0 valid[->1])

Последствие импликации (запуск через один такт после совпадения предшествующего | =>) начинается с двух совпадений с действительным повышением уровня и id == предыдущим идентификатором (когда действительный был высоким). Это ДОЛЖНО совпадать дважды [*].

(valid[->1] ##0 id == $past(id,,valid))[*2]

и заканчивается следующим циклом, в какой-то момент действительный становится высоким, и когда это происходит, идентификатор должен быть равен предыдущему идентификатору (когда действительный был высоким) + 1.

##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1))

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

Если вы хотите, чтобы идентификатор был стабильным на протяжении всего времени действия, вы можете использовать это:

assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> ($stable(id) throughout valid[->2]) ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));