[SVA]: Есть ли способ пропустить первую оценку SVA?

У меня есть следующее свойство:

property p_0;
 $rose(signal_a) |-> $rose(signal_b) ;
endproperty

моя проблема в том, что после HW RST сигнал_b повышается (нормальное поведение), но утверждение не выполняется, и я хочу, чтобы эта проверка оценивалась только позже.

Я хотел работать с first_match() примерно так:

p_0_a : assert property ( ! first_match(p_0)) else `uvm_fatal(...)

поэтому я пропускаю первое совпадение этого свойства, но компилятор выдает синтаксическую ошибку.

Есть ли способ пропустить оценку SVA после определенного количества итераций?

Спасибо


uvm system-verilog-assertions
person El_Gahaf    schedule 26.03.2018    source источник
comment
Хороший вопрос, на который, я думаю, у меня есть решение (каскадное следствие). Однако, прежде чем я отвечу, я кое-чего не понимаю: если сброс приводит к повышению signal_b, почему это может привести к сбою утверждения? Тест на рост signal_b находится в следствии, а не в антецеденте, поэтому рост signal_b в какое-то другое время никогда не должен приводить к ошибке вашего утверждения. Вы имеете в виду, что после HW RST сигнал_a повышается (нормальное поведение)?   -  person Matthew Taylor    schedule 26.03.2018
comment
Привет, Мэтью, спасибо за общение. В свойстве есть другой механизм, который отслеживает, повысилось ли значение signal_b без утверждения signal_a. Сообщение об ошибке похоже на Неожиданный нарастающий фронт сигнала_b. Итак, я упростил свойство только ради вопроса.   -  person El_Gahaf    schedule 26.03.2018

Ответы (1)


arrow_upward
0
arrow_downward

Вам могут помочь Каскадные операторы импликации, например, что-то вроде:

assert property (reset |-> p_0);

По сути, |=> и |-> правоассоциативны:

A |=> B |=> C

означает

A |=> ( B |=> C )

т.е. если происходит A, сразу после этого проверьте (B |=> C). Если A не происходит, не проверяйте (B |=> C).

person Matthew Taylor    schedule 26.03.2018