将带延迟的SystemVerilog断言转换为不变规格

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 ) );