基于AI加速的可复用FPV平台库
电子技术应用
商思航，江瑷珲，彭云霞，徐加山
深圳市中兴微电子技术有限公司
摘要： 形式验证FPV可将DUT抽象为状态空间进行遍历，针对动态仿真难以随机到的边界场景、异常场景和复杂组合场景可提高收敛速度，增强验证质量。但高质量Property开发对验证人员能力有较高的要求。面对该挑战，基于Cadence公司Jaspergold ABVIP提出了一种可复用FPV平台库解决方案，可在不同模块之间重用，降低FPV验证平台搭建时间，提升Property质量，同时借助其AI工具Proof Master生成加速Proven效率的database。FPV平台库+AI Database已在中兴微电子某车规项目落地并复用，发现动态仿真遗漏的4个故障。Proof Master可应用于项目全周期内，回归效率平均提升80.17%，FPV平台库+AI database可提升FPV 初次Proven效率44.96%。与此同时对生成式大模型提升Property编写效率做了一定探讨。
中图分类号：TN402 文献标志码：A DOI: 10.16157/j.issn.0258-7998.240801
中文引用格式： 商思航，江瑷珲，彭云霞，等. 基于AI加速的可复用FPV平台库[J]. 电子技术应用，2024，50(8)：37-41.
英文引用格式： Shang Sihang，Jiang Aihui，Peng Yunxia，et al. AI accelerated reusable FPV platform[J]. Application of Electronic Technique，2024，50(8)：37-41.
中文引用格式： 商思航，江瑷珲，彭云霞，等. 基于AI加速的可复用FPV平台库[J]. 电子技术应用，2024，50(8)：37-41.
英文引用格式： Shang Sihang，Jiang Aihui，Peng Yunxia，et al. AI accelerated reusable FPV platform[J]. Application of Electronic Technique，2024，50(8)：37-41.
AI accelerated reusable FPV platform
Shang Sihang，Jiang Aihui，Peng Yunxia，Xu Jiashan
Shenzhen Sanechips Technology Co.， Ltd.
Abstract： Formal Property Verification can abstract DUT into a state space for traversal, enhancing convergence speed and improving verification quality for boundary, exceptional, and complex combination scenarios that are difficult to reach through dynamic simulation. However, developing high-quality properties requires a high level of expertise from verification engineers. In the face of this challenge, this paper proposes a reusable FPV platform solution based on Cadence Jaspergold ABVIP, which can be reused across different modules, reducing FPV verification platform setup time, improving property quality, and leveraging AI tools to generate an accelerated proof efficiency database. The FPV platform library + AI database has been implemented and reused in a certain automotive project at Sanechips, identifying four faults missed by dynamic simulation. Proof Master can be applied throughout the project lifecycle, with an average regression efficiency improvement of 80.17%, and the FPV platform library + AI Database can enhance FPV initial proven efficiency by 44.96%. Meanwhile, this article also discusses the improvement of property writing efficiency using LLM.
Key words : formal；LLM；AI；Jaspergold
引言
与传统的动态仿真相比，属性形式验证（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）
此内容为AET网站原创，未经授权禁止转载。