微信服务号

微信订阅号

2025-4-3- 20
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
    • |
  • 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
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
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 firstVisitors
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