Formal Verification of Circuit Design

doi:10.3981/j.issn.2097-0781.2023.01.002

Science and Technology Foresight ›› 2023, Vol. 2 ›› Issue (1): 23-32.DOI: 10.3981/j.issn.2097-0781.2023.01.002

• Review and Commentary • Previous Articles Next Articles

Formal Verification of Circuit Design

ZHAN Bohua(), WU Zhilin^†()

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China

Received:2022-12-31 Revised:2023-01-30 Online:2023-03-20 Published:2023-03-24
Contact: ^†

芯片设计形式验证

詹博华(), 吴志林^†()

中国科学院软件研究所计算机科学国家重点实验室，北京 100190

通讯作者: ^†
作者简介:詹博华，副研究员。中国计算机学会形式化方法专业委员会执行委员。主要研究方向为交互式定理证明、嵌入式系统的建模和验证。在形式化方法领域的主要会议和期刊发表论文30余篇。电子信箱：bzhan@ios.ac.cn。
吴志林，研究员，博士研究生导师。中国计算机学会形式化方法专业委员会副秘书长。主要研究方向为计算逻辑、自动机理论、计算机软硬件系统的形式验证。先后承担国家重点研发计划、中国科学院A类战略性先导科技专项、中央军委装备发展部预研领域基金、国家自然科学基金等项目10余项。获CCF-IEEE CS青年科学家奖。发表论文40余篇。电子信箱：wuzl@ios.ac.cn。
基金资助:
国家重点研发计划(2021ZD0113300)

Abstract

Abstract:

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.

Key words: circuit design, correctness and safety, electronic design automation, equivalence checking, assertion-based formal verification, satisfiability problem (SAT) solving, model checking

摘要：

芯片设计验证是对芯片设计是否正确与安全进行检查，在芯片设计流程中具有非常重要的地位，占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段，已经成功用于芯片设计验证。全世界三大电子设计自动化（EDA）软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。文章总结了芯片设计形式验证发展现状，分析了面临的挑战，展望了发展趋势，并对其在中国的发展提出建议。

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

ZHAN Bohua, WU Zhilin. Formal Verification of Circuit Design[J]. Science and Technology Foresight, 2023, 2(1): 23-32.

詹博华, 吴志林. 芯片设计形式验证[J]. 前瞻科技, 2023, 2(1): 23-32.

References 43

[1]	Bryant R E. Graph-based algorithms for Boolean function manipulation[J]. IEEE Transaction on Computers, 1986, 35(8): 677-691.
[2]	Somenzi F. CUDD: CU decision diagram package release 2.5.0[EB/OL]. [2022-12-20]. ftp://vlsi.colorado.edu/pub/.
[3]	Lind-Nielsen J. BuDDy—A binary decision diagram package[EB/OL]. [2022-12-20]. http://buddy.sourceforge.net.
[4]	Cook S A. The complexity of theorem-proving procedures[C]// Proceedings of the Third Annual ACM Symposium on Theory of Computing. New York: ACM Press, 1971: 151-158.
[5]	Davis M, Logemann G, Loveland D. A machine program for theorem proving[J]. Communications of the ACM, 1962, 5(7): 394-397. DOI URL
[6]	Marques-Silva J P, Sakallah K A. Grasp: A search algorithm for propositional satisfiability[J]. IEEE Transactions on Computers, 1999, 48(5): 506-521. DOI URL
[7]	Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications[J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244-263. DOI URL
[8]	Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR[C]// Proceedings of the International Symposium on Programming. Berlin, Heidelberg: Springer, 1982: 337-351.
[9]	Vardi M Y, Wolper P. An automata-theoretic approach to automatic program verification (preliminary report)[C]// Proceedings of the Logic in Computer Science (LICS). Piscataway:IEEE Press, 1986: 332-344.
[10]	Peled D. All from one, one for all: On model checking using representatives[C]// Courcoubetis C. Proceedings of the 5th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 1993: 409-423.
[11]	Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020 states and beyond[J]. Information and Computation, 1992, 98(2): 142-170. DOI URL
[12]	McMillan K L. Symbolic model checking[M]. Boston: Kluwer Academic Publishers, 1993.
[13]	Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs[C]// Cleavelond W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 1999: 193-207.
[14]	Sheeran M, Singh S, Stålmarck G. Checking safety properties using induction and a SAT-solver[C]// Hunt W A, Jr Johnson S D.Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design. Berlin, Heidelberg: Springer, 2000: 108-125.
[15]	McMillan K L. Interpolation and SAT-based model checking[C]// Hunt W A, Jr.Somenzi F.Proceedings of the 15th International Conference on Computer Aided Verification. Cham: Springer, 2003: 1-13.
[16]	Bradley A R. SAT-based model checking without unrolling[C]// Jhala R, Schmidt D.Proceedings of the 12th International Conference on Verification Model Checking and Abstract Interpretation. Berlin, Heidelberg: Springer, 2011, 70-87.
[17]	Eén N, Mishchenko A, Brayton R. Efficient implementation of property directed reachability[C]// Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Piscataway: IEEE Press, 2011: 125-134.
[18]	Chauhan P, Clarke E M, Kukula J H, et al. Automated abstraction refinement for model checking large state spaces using SAT-based conflict analysis[C]// Aagaard M D, O’Leary J W.Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Berlin, Heidelberg: Springer, 2002: 33-51.
[19]	Graf S, Saidi H. Construction of abstract state graphs with PVS[C]// Grumberg O. Proceedings of the 9th International Conference on Computer Aided Verification. Cham: Springer, 1997: 72-83.
[20]	Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement for symbolic model checking[J]. Journal of the ACM, 2003, 50(5): 752-794. DOI URL
[21]	McMillan K L. A methodology for hardware verification using compositional model checking[J]. Science of Computer Programming, 2000, 37(1/3): 279-309. DOI URL
[22]	McMillan K L. Parameterized verification of the FLASH cache coherence protocol by compositional model checking[C]// Margaria T, Melham T.Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Berlin, Heidelberg: Springer, 2001: 179-195.
[23]	Beatty D L, Bryant R E, Seger C J. Formal hardware verification by symbolic ternary trajectory evaluation[C]// Proceedings of the 28th ACM/IEEE Design Automation Conference (DAC). New York:ACM Press, 1991: 397-402.
[24]	Aagaard M, Jones R B, Seger C J H. Lifted-FL: A pragmatic implementation of combined model checking and theorem proving[C]// Bertot Y, DowekG, HirschowitzA, et al. Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Berlin, Heidelberg: Springer, 1999: 323-340.
[25]	Kaivola R, Ghughal R, Narasimhan N, et al. Replacing testing with formal verification in Intel Core^TM i7 processor execution engine validation[C]// Bouajjani A, Maler O. Proceedings of the 21st International Conference on Computer Aided Verification. Cham: Springer, 2009: 414-429.
[26]	Hogan J. Cadence, Mentor, OneSpin, Real Intent, Synopsys formal[EB/OL]. [2022-12-20]. http://www.deepchip.com/items/0558-05.html.
[27]	IEEE Standard 1850-2010. Property specification language (PSL)[S]. Piscataway: IEEE Press, 2010.
[28]	IEEE Standard 1800-2009. SystemVerilog—Unified hardware design, specification, and verification language[S]. Piscataway: IEEE Press, 2009.
[29]	Lin C C, Chen K C, Marek-Sadowska M. Logic synthesis for engineering change[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1999, 18(3): 282-292. DOI URL
[30]	Goel A, Sakallah K A. AVR: Abstractly Verifying Reachability[C]// Biere A, Parker D.Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2020: 413-422.
[31]	Mann M, Irfan A, Lonsing F, et al. Pono: A flexible and extensible SMT-based model checker[C]// Silva A, Leino K R M.Proceedings of the 33rd International Conference on Computer Aided Verification. Cham: Springer, 2021: 461-474.
[32]	Vizel Y, Gurfinkel A. Interpolating property directed reachability[C]// Biere A, Bloem R.Proceedings of the the 26th International Conference on Computer Aided Verification. Cham: Springer, 2014: 260-276.
[33]	Lee S, Sakallah K A. Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction[C]// Proceedings of Computer Aided Verification, Lecture Notes in Computer Science. Cham: Springer, 2014: 849-865.
[34]	Welp T, Kuehlmann A. QF_BV model checking with property directed reachability[C]// Proceedings of Design, Automation & Test in Europe Conference (DATE). San Jose, CA: EDA Consortium, 2013: 791-796.
[35]	Goel A, Sakallah K A. Model checking of Verilog RTL using IC3 with syntax-guided abstraction[C]// Bodger J M, Rozier K Y.Proceedings of the 11th International Symposium on NASA Formal Methods. Cham: Springer Nature Switzerland AG, 2019: 166-185.
[36]	Zhang H, Gupta A, Malik S. Syntax-guided synthesis for lemma generation in hardware model checking[C]// Beyer D, Zufferey D.Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation. Cham: Springer, 2021: 325-349.
[37]	Luo C, Hoos H H, Cai S. PbO-CCSAT: Boosting local search for satisfiability using programming by optimisation[C]// Bäck T, PreussM, DeutzA, et al.Proceedigns of the 16th International Conference on Parallel Problem Solving from Nature—PPSN XVI. Cham: Springer, 2020: 373-389.
[38]	Xu L, Hutter F, Hoos H H, et al. SATzilla: Portfolio-based algorithm selection for SAT[J]. Journal of Artificial Intelligence Research, 2008, 32: 565-606. DOI URL
[39]	Zhu H, Magill S, Jagannathan S. A data-driven CHC solver[C]// Proceedings of ACM-SIGPLAN Symposium on Programming Language Design and Implementation (PLDI). New York:ACM Press, 2018: 707-721.
[40]	Si X, Naik Aa, Dai H, et al. Code2Inv: A deep learning framework for program verification[C]// Lahiri S K, Wang C.Proceedings of the 32nd International Conference on Computer Aided Verification. Cham: Springer, 2020: 151-164.
[41]	Bachrach J, Vo H, Richards B C, et al. Chisel: Constructing hardware in a scala embedded language[C]// Proceedings of Design Automation Conference 2012. Piscataway: IEEE Press, 2012: 1216-1225.
[42]	CIRCT[EB/OL]. [2022-12-20]. https://circt.llvm.org/.
[43]	Liu S, Du Z, Tao J, et al. Cambricon: An instruction set architecture for neural networks[C]// Proceedings of the 2016 ACM/IEEE 43rd Annual International Symposium on Computer Architecture. Piscataway: IEEE Press, 2016: 393-405.

Formal Verification of Circuit Design

芯片设计形式验证

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

References 43

Related Articles 1

Recommended Articles

Metrics

Access Statistics

Links

Contact Us

WeChat