如何手动或使用（开源）工具自动将PSL或SVA的liveness断言转换为verilog？我可以做简单的安全属性，但我对生命属性一无所知。我知道一些商业工具有这个功能来检查Verilog的设计，但我无法访问它们。
例如，我想将类似assert always req -> eventually! ack;的PSL中的liveness断言转换为等效的Verilog电路，这样我就可以使用一些工具来建模检查这个属性是否存在。
- 编辑是为了将措辞从"有可能翻译吗…"改为"我如何翻译"谢谢ira
真正的问题应该是"我如何将静态形式属性（如liveness或安全性）转换为可以使用动态模拟器检查的断言？答案是：你不能。或者你不能实际地将其转换为等效断言。
在模拟中尝试近似liveness断言的问题是，您还需要为断言的执行提供详尽的刺激。然后你需要证明刺激措施是彻底的。对于一些简单的情况，你可能可以做到这一点，但随着更多信号的加入，它会迅速爆炸。