软件学报

作者：姚广宇，张南，田聪，段振华，刘灵敏，孙风津

单位：姚广宇，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,张南，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103,段振华，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007104,刘灵敏，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007105,孙风津，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007106

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

基金：国家重点研发计划（2018AAA0103202）；国家自然科学基金（61751207，61732013）；陕西省重点科技创新团队（2019TD-001）

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

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期