基于属性的形式验证技术及应用

为了提高产品的验证覆盖率和首次流片成功率，越来越多的验证技术和衡量标准被采纳。传统的仿真验证技术很难达到验证的快速收敛，而静态验证技术采用数学穷举的方法，利用断言对cornerco．se进行快速验证，有效避免了一些设计缺陷。Mentor公司的QuestaFormal工具可以对代码进行常规的功能检查，并可用Formal引擎证明设计代码及其断言的一致性，可极大地提高复杂设计的验证效率和鲁棒性。