形式化方法验证FPGA设计模型与代码一致性

"本文探讨了一种芯片开发功能验证的新方法，主要关注模型驱动的FPGA设计中的形式化验证。文章指出，传统的FPGA设计方法依赖于Verilog或VHDL代码，但模型和代码的一致性验证往往面临挑战，且仿真验证方法在确保设计正确性、可靠性和安全性方面存在不足。为此，作者提出了一种基于MSVL（Modeling and Specification Language）语言的系统建模和验证方案。 在芯片设计过程中，模型驱动的方法可以提高设计的安全性和可靠性，但需要确保设计模型与生成的硬件描述语言（如Verilog或VHDL）代码之间的一致性。现有的仿真验证手段虽然常见，但在面对复杂的系统设计时，可能会导致验证不充分，效率低下，且工作量巨大。为解决这些问题，研究者利用MSVL构建系统模型，并通过模型提取命题投影时序逻辑公式来描述系统的行为和属性。这种方法结合了统一模型检测的概念，能够有效地验证模型是否满足预定的性质，从而确保设计的正确性。 论文中，作者具体以信号灯控制电路系统为例，实际应用了提出的验证方法，展示了其有效性和实用性。通过这个例子，读者可以更直观地理解如何运用该方法进行设计验证，以及它在功能一致性验证方面的优势。 该研究对于提升芯片设计的质量和安全性具有重要意义，特别是在对安全性有严格要求的领域，如自动驾驶、航空航天等。通过形式化的验证方法，可以减少潜在的错误，提高设计的可靠性，降低后期修复的成本。此外，该方法也有助于优化验证流程，提高工作效率，减轻设计人员的工作负担。 关键词：芯片设计；模型驱动；功能一致性；MSVL建模；命题投影时序逻辑。 分类号：TP311 引用格式：姚广宇，张南，田聪，段振华，刘灵敏，孙风津.芯片开发功能验证的形式化方法.软件学报,2021,32(6):1799−1817. 英文引用格式：YaoGY,ZhangN,TianC,DuanZH,LiuLM,SunFJ.Formalmethodoffunctionalverificationforchip development." 这篇研究不仅提供了新的芯片设计验证思路，也为后续的FPGA设计和验证工作提供了理论基础和技术支持。通过深入理解和应用该方法，设计者可以更好地保证设计的正确性和安全性，同时提高设计验证的效率。