Значение SystemVerilog Assertion (SVA) с преимущественным запуском - PullRequest
Новая
       93

Значение SystemVerilog Assertion (SVA) с преимущественным запуском

0 голосов
/ 08 октября 2018

Я новичок в SVA.У меня есть вопрос о причастности SVA.

1: sequence s1;
2:   start ##[1:$] !start;
3: endsequence: s1
4:
5: sequence s2;
6:   ready && (!start);
7: endsequence: s2;
8: 
9: assert_ready: assert property (@(posedge clk) s1 |-> ##5 s2);

Целью этого утверждения является проверка свойства синхронизации:

  • , когда переключается «старт», «готово» активируется после 5 тактов.
  • Но при наличии преждевременного «запуска», то есть другого переключателя «Пуск» до активации «готовности», это свойство синхронизации должно быть сброшено, а «готовность» должна быть отключена.

Я пытался проверить это свойство, используя инструмент формальной проверки, VC Synopsys.Что это показывает, что это утверждение не выполняется, потому что последовательность s2 равна нулю, когда происходит преждевременное «начало».

Я думаю, что у меня неправильное описание в строке 6, которое является настоящим кодом новичка.Не могли бы вы дать мне знать, как правильно описать утверждение для начала?

1 Ответ

0 голосов
/ 08 октября 2018

Я думаю, что вы хотите 

sequence s1;
   start ##1 !start [*5]
endsequence: s1
sequence s2;
  ready;
endsequence: s2;

assert_ready: assert property (@(posedge clk) s1 |->  s2);

Хотя вам, возможно, придется скорректировать это в зависимости от ваших требований относительно того, что происходит, когда start совпадает с ready в 5-м цикле.

...