引言
与传统的动态仿真相比，属性形式验证（Formal Property Verification, FPV）可将RTL代码与使用者编写的Property共同抽象成求解表达式（Conjunctive Normal Form, CNF），使用形式验证工具中不同的SAT求解器（Satisfiability, SAT）对其进行证明。可对状态空间进行遍历，即使结构复杂的设计也能够准确地覆盖边界场景，保证了验证的完备性。
图1为传统FPV流程，其中验证功能点分解、自然语言描述编写、Property编写依赖于使用者对DUT的深入理解以及丰富的形式验证经验，并且会花费使用者较多时间。对于某些状态空间较大的模块，Property证明会花费较多的时间和服务器资源。
图1 传统FPV流程图
为了应对此类挑战，中兴微电子提出了基于AI加速的可复用FPV平台库解决方案。针对功能类似的DUT，开发一套通用的Property代码与配套文档，可实现同一项目内复用与不同项目间复用。并且在Jaspergold Proof Master@Cadence工具的支持下，基于平台库抽象成的CNF记录当前使用的SAT，以AI database的形式存储下来，复用至其余功能类似的DUT。FPV平台库+AI database可以极大减少Property开发时间与运行时间，提升FPV验证效率与质量。
本文详细内容请下载：
http://www.chinaaet.com/resource/share/2000006119
作者信息：
商思航，江瑷珲，彭云霞，徐加山
（深圳市中兴微电子技术有限公司，广东 深圳 518054）
