芯片设计形式验证  

Formal Verification of Circuit Design

作　　者：詹博华 吴志林[1] ZHAN Bohua;WU Zhilin(State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China)

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室,北京100190

出　　处：《前瞻科技》2023年第1期23-32,共10页Science and Technology Foresight

基　　金：国家重点研发计划(2021ZD0113300)。

摘　　要：芯片设计验证是对芯片设计是否正确与安全进行检查,在芯片设计流程中具有非常重要的地位,占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段,已经成功用于芯片设计验证。全世界三大电子设计自动化(EDA)软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。文章总结了芯片设计形式验证发展现状,分析了面临的挑战,展望了发展趋势,并对其在中国的发展提出建议。The verification of circuit design is to check its correctness and safety,which is vital in the circuit design process and occupies almost half of the cost and time.Formal verification is one of the important ways to guarantee the correctness and safety of software and hardware systems of computers and has been applied to circuit design verification.The electronic design automation(EDA)software from three global EDA giants,i.e.,Cadence,Synopsis,and Siemens,all includes mature formal verification tools for circuit design.This paper summarizes the current status of the formal verification of circuit design,analyzes its challenges,discusses its perspectives and trends,and proposes suggestions on its development in China.

关 键 词：芯片设计 正确性与安全性 电子设计自动化 等价性验证 基于断言的形式验证 命题逻辑可满足性(SAT)求解 模型检测 

分 类 号：TN402[电子电信—微电子学与固体电子学]