FVM：一种降低VHDL设计形式化验证采用障碍的创新方法

《IEEE Open Journal of the Computer Society》：FVM: A Formal Verification Methodology for VHDL Designs

本文针对数字设计复杂度上升导致功能验证难以管理、VHDL团队在形式化验证采用率低的现状，提出了一种创新的形式化验证方法学（FVM）。该方法学结合自动化工具与属性检查，通过PSL序列实现形式化事务级建模，并提供了辅助工具drom2psl简化属性编写流程。研究结果表明，FVM在可管理的设计复杂度和验证生产力方面取得了显著成效，为空间领域及其他依赖VHDL的工业部门提供了实用的验证解决方案。

　　

随着数字设计的复杂度不断攀升，功能验证已成为工程师面临的重要挑战。那些在验证过程中"幸存"下来的设计缺陷往往会导致功能、性能、安全和经济方面的严重问题，这种现象在当前FPGA和ASIC设计中尤为普遍。更令人担忧的是，这些缺陷往往在开发后期甚至产品部署后才被发现，造成了不可估量的损失。

在这一背景下，形式化验证（Formal Verification）作为对当前最主流的仿真验证方法的有力补充，正逐渐展现出其独特价值。通过数学方法证明设计的各种属性，形式化验证能够以高度可信的方式验证设计正确性。然而，这一技术要求设计人员具备深厚的方法学、技术和工具专业知识，导致其在实际项目中的采用率远低于其实际价值所能达到的水平，特别是在以VHDL为主要设计语言的团队中更为明显。

最新研究数据显示，形式化验证在ASIC设计中的采用率已超过50%，但在FPGA项目中仍低于25%。更值得关注的是，在属性规范语言方面，SVA（SystemVerilog Assertions）的使用率远高于PSL（Property Specification Language），而PSL恰好包含VHDL版本。这种语言偏好差异在欧洲空间领域尤为突出，由于VHDL在欧洲的普遍偏好，该领域可能成为形式化验证技术的晚期采用者，面临效率低下、进入门槛高等挑战。

针对这一现状，发表在《IEEE Open Journal of the Computer Society》上的研究提出了一种创新的形式化验证方法学（FVM），专门旨在降低VHDL设计形式化验证的采用障碍。据研究者所知，这是首个通用、开源的形式化验证方法学，为VHDL设计团队提供了一条系统化的验证路径。

该方法学采用了渐进式系统方法，从基础到高级验证任务逐步展开。其核心创新在于将自动化形式化工具与属性检查相结合，使设计人员能够在编写特定属性的同时，利用自动化工具发现设计中的潜在问题。FVM还引入了形式化的事务级建模（Transaction-Level Modeling）概念，通过参数化PSL序列抽象底层复杂性，同时保持形式化语义。

为了进一步降低使用门槛，研究团队开发了drom2psl辅助工具，该工具能够将WaveDrom波形描述转换为PSL序列，有效桥接了人类可读的波形规范与机器可处理的形式化属性之间的鸿沟。这一创新使得设计人员能够基于熟悉的波形描述快速生成形式化验证所需的技术规范。

在验证复杂设计时，FVM提供了系统的复杂度管理策略，包括证明复杂度降低和混合验证策略。方法学通过具体示例展示了多种复杂度降低技术的应用，如切点（Cutpoint）、黑盒化（Blackboxing）、计数器抽象、存储器抽象等，为用户应对中等复杂度设计提供了实用参考。

研究团队还开发了配套的Python框架，作为用户与形式化工具之间的抽象层。该框架支持最小化配置，用户仅需添加设计源文件即可开始基础验证，随着熟练度的提升，可以逐步使用更高级的设置选项。框架自动生成工具特定脚本，运行验证流程，并以多种格式（包括控制台输出、HTML报告和CI系统兼容的JUnit XML）呈现结果。

为验证方法学的有效性，研究团队构建了一个包含不同复杂度设计实例的代码库，涵盖了从简单计数器到复杂IPv6收发器的多种设计。这些实例来自开源库和自主开发，按复杂度分为五个等级：简单、容易、中等、中级和困难。通过对这些设计应用FVM，研究团队获得了令人鼓舞的结果。

在验证生产力方面，方法学表现出色。8个示例设计（包括优先级仲裁器、AXI4-Lite从设备、SDRAM控制器等）由一名初级工程师在约两个月的兼职时间内完成验证，估计验证工作量约为200小时。更令人印象深刻的是，即使在已经通过仿真验证的设计中，FVM仍发现了多个潜在问题，如异步FIFO在特定时钟频率关系下可能出现的下溢问题、IPv6收发器中头部值错误等，充分展示了形式化验证作为仿真补充的强大能力。

对于超大规模设计，研究团队还将FVM应用于欧洲空间局提供的SpaceFibre IP核。这一复杂设计包含接口层、通道层和数据链路层，涉及多时钟域、8b10b编码、QoS机制等复杂功能。通过分层验证和复杂度降低技术的组合应用，研究团队成功发现了设计中存在的多个潜在问题，包括不符合SpaceFibre标准的行为、CRC损坏可能性等，证明了方法学在处理现实世界复杂设计时的实用性。

关键技术方法包括：基于PSL的属性规范与序列生成、自动化形式化工具集成（静态检查、形式友好度评估、规则检查等）、复杂度降低技术应用（结构简化、数据独立性利用等）、混合验证策略（结合形式化验证与仿真）以及分层验证方法。研究使用了来自开放源代码库（OpenLogic、GRLIB、PoC）和自主开发的设计实例作为验证样本。

研究结果方面，通过系统化的验证流程，FVM在各个复杂度级别的设计上都取得了显著成效：

自动化设计分析结果显示，大多数示例设计的形^式友好度评分超过80%，表明它们适合进行形式化验证。这一评分通过加权计算设计元素（时钟域、复位域、控制点比特、状态比特等）的复杂度得出，为设计人员提供了直观的复杂度评估。

属性检查与覆盖率收集表明，FVM能够有效验证设计的正确性。在UART发送器设计中，形式化覆盖率达到了100%，仿真覆盖率为94.06%，验证过程仅需1分钟。即使在复杂如IPv6收发器的设计中，仍能达到88.8%的形式化签署覆盖率和91.91%的仿真覆盖率，验证时间为9分28秒。

复杂度管理技术应用证明，通过属性简化、结构缩减等技术，可以显著提高验证效率。在线性插值器示例中，通过将单一复杂属性分解为13个简单属性，验证时间从11分53秒减少到1分3秒，提升了一个数量级。

框架效能评估显示，FVM框架能够有效管理验证流程，提供清晰的结果反馈。框架生成的多格式报告（控制台、HTML、JUnit XML）满足了不同场景下的需求，特别是基于Allure框架的HTML报告提供了可视化的验证结果和趋势分析。

研究结论指出，FVM方法学成功填补了VHDL设计形式化验证领域的空白，为设计团队提供了一套系统化、实用的验证解决方案。通过降低采用门槛、提高验证生产力，该方法学有望促进形式化验证技术在VHDL社区的广泛应用。特别是对于欧洲空间部门等偏好VHDL的领域，FVM提供了一条避免成为形式化验证晚期采用者的可行路径。

讨论部分强调，虽然当前方法学主要支持Siemens EDA的Questa工具链，但其架构设计允许轻松扩展支持其他形式化工具。未来的工作方向包括应用于更多现实世界设计、增加Verilog/SystemVerilog支持、集成开源工具链以及改进形式友好度度量指标等。

这项研究的重要意义在于，它不仅是技术上的创新，更是对整个VHDL设计验证生态的积极推动。通过提供开源、通用的验证方法学，FVM有望改变VHDL团队在形式化验证方面的落后状况，为提高数字设计的可靠性和安全性做出实质性贡献。随着形式化验证技术的普及和优化，我们有理由期待未来数字设计领域将迎来更高效、更可靠的验证新时代。