软件说明
主要特性:
自动化的、一键式检测所有常见的设计缺陷,如状态机的死锁/活锁、运算的异常、X态的传播等;
基于断言的形式验证技术,支持SVA、 PSL、OVL;
集成化的代码和功能覆盖率分析;
可以使用和仿真器同样的调试与纠错环境;
可以在仿真环境下重现由形式验证引擎发现的断言违反事件;
在仿真环境下使用动态形式验证技术,可以增加验证的完备性;
独一无二的4态引擎技术可以避免产生虚假的违反告警;
可以在系统级重用已有的验证环境进行调试和纠错;
利用Questa Formal验证引擎,可以深度穷举分析设计的行为,从而可以探测到响应检查器断言违反的复杂错误和触发条件,发现验证激励的漏洞,提高验证的完备性。 对于关键的控制模块,Questa Formal验证可以确保设计在任何情况下均能正常工作。 其Autocheck 特性无需手动编写任何Assertion,并可以在仿真验证平台准备好之前发现一些设计上的潜在问题,如下图的X态的传播问题。
自动化的、一键式检测所有常见的设计缺陷,如状态机的死锁/活锁、运算的异常、X态的传播等;
基于断言的形式验证技术,支持SVA、 PSL、OVL;
集成化的代码和功能覆盖率分析;
可以使用和仿真器同样的调试与纠错环境;
可以在仿真环境下重现由形式验证引擎发现的断言违反事件;
在仿真环境下使用动态形式验证技术,可以增加验证的完备性;
独一无二的4态引擎技术可以避免产生虚假的违反告警;
可以在系统级重用已有的验证环境进行调试和纠错;