将SystemVerilog声明延迟转换为invarspec

Question

我想将延迟的SystemVerilog声明转换为正式验证者的invarspec。合成器在下面的代码行中给出## 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));