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

Question

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

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

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

Answer 1

Один из подходов состоит в том, чтобы явно моделировать задержанную версию сигналов в 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));