verilog - 我如何将 PSL 或 SVA 活性断言/属性翻译成 Verilog？

Question

如何手动或使用（开源）工具自动将 PSL 或 SVA 活性断言翻译成 verilog？我可以做简单的安全属性，但我对活性属性一无所知。我知道一些商业工具有这个功能来检查 Verilog 设计，但我无权访问它们。

例如，我想将 PSL 中的活性断言翻译assert always req -> eventually! ack;成等效的 Verilog 电路，以便我可以使用一些工具来模型检查该属性是否存在。

• 进行了编辑，将“是否可以翻译...”改写为“我如何翻译”，谢谢 ira！

Answer 1

问题实际上应该是“我如何将静态形式属性（如活性或安全性）转换为可以用动态模拟器检查的断言？答案是：你不能。或者你不能将它实际转换为等价物断言。

尝试在模拟中逼近活性断言的问题在于，您还需要为断言的执行提供详尽的刺激。然后你需要证明刺激是详尽的。对于一些简单的情况，您可能可以这样做，但随着更多信号的参与，它会迅速爆发。