Преобразование утверждения SystemVerilog с задержкой в ​​invarspec

Я хочу преобразовать утверждение SystemVerilog с задержкой в ​​invarspec формального верификатора. Синтезатор выдает синтаксическую ошибку для ##1 в строке кода ниже.

assert property ( ( req1 == 0 ) ##1( req1 == 1 ) ##1 !( req2 == 1 ) || ( gnt1 == 0 ) );

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


delay formal-verification system-verilog-assertions model-checking
person mii9    schedule 22.11.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

Для вашего примера:

assert property ( ( req1 == 0 ) ##1( req1 == 1 ) ##1 !( req2 == 1 ) || ( gnt1 == 0 ) );

становится:

reg req1_r,req1_rr;

always @(posedge clk) begin
   req1_rr <= req1_r;
   req1_r <= req1;
end

assert property ( !(( req1_rr == 0 ) && ( req1_r == 1 )) 
               || !( req2 == 1 ) || ( gnt1 == 0 ) );
person Peter de Rivaz    schedule 17.02.2017