我们可以使用JasperGold做功能验证吗？

Question

任何人都可以告诉我如何使用JasperGold进行功能验证吗？ 我是这个工具的新手。

Answer 1

JasperGold是一个正式的验证工具。功能验证通常使用仿真和功能覆盖进行。

正式工具的输入是你的设计加上一套ASSUME属性。 ASSUME属性通常会限制输入激励的合法范围。给定输入的正式工具可以证明其他属性。

E.g.如果你的设计是一个完整的加法器，并且设置了输入介于0和5之间的ASSUME属性，那么形式也应该能够证明输出始终在0和10之间。它还应该能够证明输出是总是等于输入的总和。这最后一个属性可以被看作是“功能验证”。你已经验证你的HDL代码和你的财产在功能上是平等的。

Answer 2

是的，您可以使用JasperGold进行功能验证。 JasperGold是一个正式的财产检查工具。

功能验证是验证设计功能的过程。传统模拟（定向或随机）可用于执行功能验证。正式的财产检查工具执行功能验证。还有正式的等价性检查工具（如Synopsys的Hector）进行功能验证。

有一些正式的工具，不执行功能验证。例如Formality。

要使用JasperGold，您需要使用属性检查语言来创建合适的属性。 SystemVerilog断言（或SVA）现在是行业标准。您可以从Internet上下载（令人惊讶的可读）SystemVerilog LRM。