Questa Formal基于断言的形式验证工具

Questa Formal是一款代码覆盖率检查工具，可以深度穷举分析设计的行为，从而可以探测到响应检查器断言违反的复杂错误和触发条件，发现验证激励的漏洞，提高验证的完备性。对于关键的控制模块，Questa Formal验证可以确保设计在任何情况下均能正常工作。 其Autocheck 特性无需手动编写任何Assertion，并可以在仿真验证平台准备好之前发现一些设计上的潜在问题。