芯片开发功能验证的形式化方法

摘要：

在芯片设计领域,采用模型驱动的FPGA设计方法是目前较为安全可靠的一种方法.但是,基于模型驱动的FPGA设计需要证明FPGA设计模型和生成Verilog/VHDL代码的一致性;同时,芯片设计的正确性、可靠性和安全性也至关重要.目前,多采用仿真方法对模型和代码的一致性进行验证,很难保证设计的可靠性和安全性,并存在验证效率低、工作量大等问题.提出一种新型验证设计模型和生成代码一致性的方法,该方法利用MSVL语言进行系统建模,并通过模型提取命题投影时序逻辑公式描述的系统的性质,通过统一模型检测的原理,验证模型是否满足性质的有效性.进而,应用信号灯控制电路系统作为验证实例,对验证方法做了检验和说明.

关键词：芯片设计、模型驱动、功能一致性、MSVL建模、命题投影时序逻辑

所属期刊栏目：32

分类号：TP311(计算技术、计算机技术)

资助基金：国家重点研发计划;国家自然科学基金;国家自然科学基金;陕西省重点科技创新团队项目

在线出版日期：2021-07-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共19页

页码：1799-1817