微信服务号

微信订阅号

2025-5-15- 15
Home > Archive>Volume 32, Issue 6, 2021 >1799-1817. DOI:10.13328/j.cnki.jos.006250
PDF HTML XML Export Cite reminder
Formal Method of Functional Verification for Chip Development
Author:
Affiliation:

Fund Project:

National Key Research and Development Program of China (2018AAA0103202); National Natural Science Foundation of China (61751207, 61732013); Key Science and Technology Innovation Team of Shaanxi Province(2019TD-001)

  • Article
    • | |
  • Metrics
    • |
  • Reference [18]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    In the field of chip design, the use of model-driven FPGA design methods is currently a safer and more reliable method. However, model-driven FPGA design needs to prove the consistency of the FPGA design model and the generated Verilog/VHDL code. Further, the chip design correctness, performance, reliability, and safety are critical. At present, simulation methods are often used to verify the consistency of models and codes. It is difficult to ensure the reliability and safety of the design, and there are problems such as low verification efficiency and heavy workload. This study proposes a new method to verify the consistency of the design model and the generated code. This method uses the MSVL language to model the system, and propositional projection temporal logic (PPTL) formula to describe the properties of the system, then based on the principle of unified model checking, verifies whether the model meets the validity of the property. Furthermore, a signal light control system is used as a verification example to verify and explain the verification method.

    Reference
    [1] Alexander MJ, Cohoon JP, Ganley JL, Robins G. Performance-Oriented placement and routing for field-programmable gate arrays. In:Proc. of the European Design Automation Conf. (EURO-DAC). IEEE, 1995. 80-85.
    [2] Andraka R. A survey of CORDIC algorithms for FPGA based computers. In:Proc. of the 1998 ACM/SIGDA 6th Int'l Symp. on Field Programmable Gate Arrays. New York:Association for Computing Machinery, 1998. 191-200.
    [3] Parsons S, Taylor DE, Schuehler DV, Franklin MA, Chamberlain RD. High speed processing of financial information using FPGA devices. United States Patent US8655764 B2. 2013.
    [4] Guan Y, Yuan Z, Sun G, Cong J. FPGA-Based accelerator for long short-term memory recurrent neural networks. In:Proc. of the 22nd Asia and South Pacific Design Automation Conf. IEEE, 2017. 629-634.
    [5] Ma YF, Suda N, Cao Y, Seo J, Vrudhula S. Scalable and modularized RTL compilation of convolutional neural networks onto FPGA. In:Proc. of the 26th Int'l Conf. on Field Programmable Logic and Applications. IEEE, 2016. 1-8.
    [6] Tolba MF, AbdelAty AM, Soliman NS, Said LA, Madian AH, Azar AT, Radwan AG, et al. FPGA implementation of two fractional order chaotic systems. AEU-Int'l Journal of Electronics and Communications, 2017,78:162-172.
    [7] Hu J, Li T, Li S. Equivalence checking between SLM and RTL using machine learning techniques. In:Proc. of the 17th Int'l Symp. on Quality Electronic Design. Santa Clara:IEEE, 2016. 129-134.
    [8] Vasudevan S, Abraham JA, Viswanath V, Tu JJ. Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In:Proc. of the 4th ACM and IEEE Int'l Conf. on Formal Methods and Models for Co-design. Napa:IEEE, 2006. 71-80.
    [9] Marquez CIC, Strum M, Chau WJ. Formal equivalence checking between high-level and RTL hardware designs. In:Proc. of the 14th Latin American Test Workshop (LATW). Cordoba:IEEE, 2013. 1-6.
    [10] Yang Z. Scalable equivalence checking for behavioral synthesis[Ph.D. Thesis]. Broadway:Portland State University, 2015.
    [11] Wang Z, Li C, Hu S, Man J. A framework on runtime verification for software behavior. In:Proc. of the 2nd Int'l Conf. on Intelligent System Design and Engineering Application. Sanya:IEEE, 2012. 20-23.
    [12] Duan ZH, Yang X, Koutny M. Framed temporal logic programming. Science of Computer Programming, 2008,70(1):31-61.
    [13] Duan ZH, Koutny M. A framed temporal logic programming language. Journal of Computer Science and Technology, 2004,19(3):341-351.
    [14] Duan ZH. Temporal logic and temporal logic programming. Beijing:Science Press, 2005.
    [15] Duan ZH, Tian C, Zhang N. A canonical form based decision procedure and model checkingapproach for propositional projection temporal logic. Theoretical Computer Science, 2016,609:544-560.
    [16] Yang K, Duan ZH, Tian C, Zhang N. A compiler for MSVL and its applications. Theoretical Computer Science, 2018,749:2-16.
    [17] Duan ZH, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical Computer Science, 2014,554:169-190.
    [18] Duan ZH, Tian C. A unified model checking approach with projection temporal logic. In:Proc. of the Int'l Conf. on Formal Engineering Methods. Berlin, Heidelberg:Springer-Verlag, 2008. 167-186.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

姚广宇,张南,田聪,段振华,刘灵敏,孙风津.芯片开发功能验证的形式化方法.软件学报,2021,32(6):1799-1817

Copy
Share
Article Metrics
  • Abstract:2136
  • PDF: 6051
  • HTML: 3771
  • Cited by: 0
History
  • Received:August 30,2020
  • Revised:October 26,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044671Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063