我想将延迟的 SystemVerilog 断言转换为形式验证器的 invarspec。合成器在下面的代码行中给出 ##1 的语法错误。
assert property ( ( req1 == 0 ) ##1( req1 == 1 ) ##1 !( req2 == 1 ) || ( gnt1 == 0 ) );
有几个属性需要验证并且有延迟。我目前正在尝试使用合成器将它们转换为正式(SMV)模型规范,该合成器适用于不涉及延迟的属性。我可以为这个正式的验证工具建模延迟吗?如果是这样,怎么做?