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

введите здесь описание изображенияСледующее — это свойство утверждения. Когда o_dc_mode = 1, тогда o_mod_c_c == rego_dc_c_c. Как видно из формы сигнала, когда ASK_MOD_DC_MODE_PROPERTY попадает в сценарий, он остается в «завершенном» состоянии и никогда не переходит в неактивное состояние, даже если o_dc_mode = 0.

property ASK_MOD_DC_MODE; 
@(posedge OSC64MHZ) 
o_dc_mode |->  (o_mod_c_c == rego_dc_c_c);
endproperty

ASK_MOD_DC_MODE_PROPERTY: assert property (ASK_MOD_DC_MODE)
$info("Assertion ASK_MOD_DC_MODE passed");
else
$error("Assertion ASK_MOD_DC_MODE failed");

verification verilog system-verilog system-verilog-assertions
person nandeesh v    schedule 05.11.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

Например, в вопросе:

property ASK_MOD_DC_MODE; 
@(posedge OSC64MHZ)
o_dc_mode |-> ( (o_mod_a_c == rego_dc_a_c) &&  (o_mod_b_c == rego_dc_b_c) && (o_mod_c_c == rego_dc_c_c));
endproperty
ASK_MOD_DC_MODE_PROPERTY: assert property (ASK_MOD_DC_MODE)
$info("Assertion ASK_MOD_DC_MODE passed");
else
$error("Assertion ASK_MOD_DC_MODE failed");

Fig.1 В приведенном выше утверждении, как только симулятор достигает свойства, он обновляет finish_count = 1 (рис. 1) и никогда не обновляет состояние (также Finish_count), если нет отказ. Рис.2 Эту оптимизацию можно отключить с помощью параметра компиляции "-abvevalnochange". Вы можете увидеть эффект на рис.2.

person nandeesh v    schedule 08.11.2019