Как лучше всего проверить событие, произошедшее в прошлом в SVA? - PullRequest
Новая
       38

Как лучше всего проверить событие, произошедшее в прошлом в SVA?

0 голосов
/ 10 июля 2019

Я хочу проверить в своем проекте, что, когда сигнал b получен, тогда сигнал a должен был быть утвержден за 3 - 5 циклов.

Я ищу разные способы проверить это.

В настоящее время я использую следующую логику 

sequence s_test();
##1 $rose(a) ##[3:5] 1;
endsequence

property p_test();
##1 $rose(b) |-> s_test.triggered();

Есть ли способ проверить это свойство, не используя механизм запуска по последовательности? Я думаю, я мог бы также использовать что-то вроде $ past (a, 3) || ... || $ прошлый (а, 5), но это громоздко.

Кроме того, в чем разница между механизмом запуска и согласования последовательности?

Ответы [ 3 ]

1 голос
/ 11 июля 2019

Вы можете использовать $past что-то вроде ниже. 

property test_past;
  @(posedge clk)
    $rose(b) |-> ##[3:5] $past(a);
endproperty
1 голос
/ 12 июля 2019
Методы

triggered & matched различаются для последовательностей с одним и несколькими тактами.

Оба метода показывают конечную точку последовательности, но метод triggered оценивается как true, если последовательность операнда достигла своей конечной точки в это конкретное время, и false в противном случае.

Принимая во внимание, что метод matched обнаруживает конечную точку последовательности, на которую ссылаются в многозамкнутой последовательности. Таким образом, он обеспечивает синхронизацию между двумя последовательностями и оценивает значение true после совпадения, пока не поступит 1-й тактовый такт целевой последовательности.

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

1 голос
/ 11 июля 2019

У нас может быть два подхода: причина, а затем эффект или эффект из-за причины .

Причина, а затем эффект приближения :

Вы можете использовать утверждение на основе времени вперед , утверждающее, что при срабатывании s_test значение b должно возрастать в течение 1-5 тактов временного окна: 

s_test.triggered |-> ##[1:5] $rose(b);

Эффект затем вызывает приближение :

В качестве альтернативы, если s_test является сигналом , тогда вы можете использовать клейкую логику, которая отслеживает последние 5 значенийs_test.После этого утверждение проверяет, что более ранние значения s_test должны иметь по крайней мере 1'b1, когда b возрастает с 0 до 1. 

bit[1:5] earlier; 
always  @(posedge clk) begin
  earlier <= {s_test, earlier[1:5]}; // shift for 5 clocks
end

p1_past20: assert property(@(posedge clk)
 $rose(b) |-> $countones(earlier) >= 1);

Подобное обсуждение доступно здесь и ссылка более здесь .

...