航空航天和航空工业中I2C通信协议的形式化验证

《Microprocessors and Microsystems》：Formal verification for I2C communication Protocol in aerospace and aviation industries

本文采用基于Yosys/SymbiYosys的开源形式验证流程，针对航空领域I2C主控制器，通过有界模型检查、覆盖分析和定理证明，系统验证了其五个有限状态机状态和九个转换，确保数据通信可靠，降低安全风险。

　　

Merve Berik|Yahya Baykal

TUSA?（土耳其航空航天工业公司），地址：土耳其安卡拉Kahramankazan区Fethiye路Havac?l?k Bulvar? 17号

摘要

航空航天工业包含许多对安全性要求极高的应用，这些应用涉及大量相互作用的子系统。因此，设备与组件之间的可靠数据通信至关重要。在此背景下，Inter-Integrated Circuit (I2C) 通信协议因其简单性、灵活性、低功耗和可靠性而受到广泛青睐。然而，数据损坏、数据丢失和延迟增加等问题仍可能发生，这可能导致航空领域的严重后果，包括安全风险、电子故障、空中交通管理问题以及错误的导航信息。为了避免此类故障，必须正确实现并严格验证I2C寄存器传输层（RTL）设计。有多种数字设计验证方法，其中形式化验证（Formal Verification, FV）是针对安全关键系统最精确和最可靠的方法之一，因为它能够提供符合指定属性的数学证明。在这项工作中，我们使用基于Yosys的开源形式化验证流程和SymbiYosys框架对一个开源的I2C主控制器设计进行了验证。验证环境使用SystemVerilog和SystemVerilog断言（SystemVerilog Assertions）开发，可以直接检测设计是否满足协议要求。通过结合有界模型检查（bounded model checking）、覆盖分析（cover analysis）和定理证明（theorem-proving），该流程系统地验证了I2C主控制器的所有五个有限状态机（FSM）状态和九个状态转换。结果表明，形式化验证可以系统地确保航空电子设备的稳健性和容错性。

引言

现代计算机系统和硬件平台变得越来越复杂，这使得确保其正确性并检测细微的设计错误变得具有挑战性。解决这些挑战的一种有效方法是应用形式化验证（Formal Verification, FV）方法。FV依赖于数学上严格的技术，这些技术根据一组正式指定的属性来推理设计的行为。之前的基于仿真的验证研究[[1], [2], [3], [4]]使用了SystemVerilog断言（SystemVerilog Assertions, SVA）和通用验证方法论（Universal Verification Methodology, UVM）来减少验证时间并提高模块化重用性。这些方法通常依赖于受限随机测试生成和复杂的测试平台，但它们无法穷尽设计的所有可达状态。相比之下，基于模型检查的形式化验证在配置的范围内系统地分析状态空间，并且当与明确定义的属性结合使用时，可以为安全关键应用提供更强的保证。

这些方法对于复杂系统非常重要；然而，它们并不总是能为大型设计节省大量时间，而且需要详细的验证计划。此外，它们无法数学上证明所有可能的状态和转换都满足预期属性，也无法保证寄存器传输层（RTL）实现与合成（synthesis）或扫描（scan）等后续表示形式一致。

此外，所有这些方法都需要手动创建测试环境，包括测试用例、驱动程序、监控程序、模型和控制器等组件，这增加了复杂性和出错的风险。正如[5]中所指出的，因此实现时间节省更加困难。形式化验证（Formal Verification, FV）是用于应对这些挑战的方法之一，它包括定理证明（theorem proving）、等价性检查（equivalence checking）、类型检查（type checking）和模型检查（model checking）等技术。在[6]中，FV与验证方法结合使用，以提高系统质量和可靠性。

在这项工作中，我们采用了基于断言的验证（Assertion-Based Verification, ABV）方法，其中I2C主控制器的预期行为被表示为用SystemVerilog断言（SystemVerilog Assertions, SVA）语言编写的属性。这些SVA属性作为我们基于Yosys/SymbiYosys的模型检查流程的规范，使我们能够结合SVA的表达能力和形式化验证的详尽分析能力，以验证安全关键的I2C协议。

文献中关于形式化验证的最新研究引入了基于断言的验证框架，这些框架使用SystemVerilog断言快速检测I2C模块中的RTL错误，并支持在仿真和形式化验证流程之间的重用[7]。

另一项研究使用模型检查自动为I2C设备合成经过验证的硬件/软件驱动程序，以确保驱动程序和硬件共同满足协议规范[8]。新兴的AI辅助技术也开始从自然语言规范直接生成验证断言，尽管这些方法仍在发展中[[9], [10], [11]]。这些发展凸显了将形式化方法与其他验证范式结合使用以提高覆盖率和效率的日益增长的兴趣。此外，形式化验证工具越来越多地适应特定领域的协议，例如汽车CAN和航空电子I2C[7]，这证明了我们选择的方法的可扩展性。

本文的主要贡献是一个应用于航空航天领域的开源、基于Yosys/SymbiYosys的形式化验证流程的案例研究。该工作记录了：(i) 如何为旨在模拟DO-254/AMC 20-152A风格航空电子设计的开源I2C主控制器构建特定于设计和领域的形式化环境和断言规范；(ii) 如何从文本I2C要求中推导出一组可重用的、与START/STOP时序、ACK处理和FSM进展相关的安全和活性检查，并使用BMC、Prove和Cover模式进行分析；(iii) 如何将得到的PASS、FAIL和UNKNOWN结果以及基于归纳的证明和覆盖情况解释为实际的航空电子场景和开发保证考虑。据作者所知，关于在航空航天领域使用开源形式化验证流程进行安全关键I2C通信的公开经验非常有限，本文旨在填补这一空白，提供一份详细且可复制的经验报告。

本文的其余部分组织如下：第2节介绍了I2C协议在航空航天应用中的背景并阐述了工作目标。第3节描述了提出的形式化验证方法和整体验证流程。第4节总结了正在验证的I2C主控制器数字设计的规范。第5节详细介绍了形式化验证框架，包括形式化核心（Formal Core）、验证方法和基于SymbiYosys的工具配置。第6节报告了I2C主控制器的形式化验证结果，包括BMC、Cover和Prove实验。最后，第7节总结了本文并提出了未来工作的方向。

部分摘录

背景和目标

本节首先提供了有关I2C通信协议及其在航空航天应用中作用的背景信息，然后阐述了本工作的具体目标。

I2C协议是一种串行通信标准，它通过两线总线促进微控制器、电子设备和传感器之间的数据交换。在航空电子和其他嵌入式应用中，由于其简单性、灵活性、易用性和低成本，I2C被广泛采用。

方法论和方法

本节描述了提出的形式化验证方法，包括整体流程、验证环境和基于SymbiYosys的工具链配置。

本研究采用形式化验证（Formal Verification, FV）方法，系统地检查I2C主控制器设计的相关状态空间，直至配置的边界。本文中使用的I2C主控制器设计是用Verilog硬件描述语言（Verilog Hardware Description Language, HDL）编写的，已从OpenCores网站下载。

I2C通信过程

I2C总线是一种串行通信协议，由两条活动线组成：串行时钟线（Serial Clock Line, SCL）和串行数据线（Serial Data Line, SDA）。实际数据在SDA线上传输，而SCL线是一个同步时钟信号。

与其他协议相比，I2C通信协议因其高速度、灵活性、低功耗、灵敏度和可靠性而受到广泛青睐。

主设备根据它将要使用的从设备来决定是发送数据还是请求数据。

形式化验证

本节介绍了形式化验证框架，包括环境、验证模式（BMC、Cover、Prove）、形式化核心（Formal Core）和基于Yosys的SymbiYosys工具。

形式化验证结果

创建了测试场景，目的是验证I2C主控制器的“START”、“STOP”、“WRITE”、“READ”、“IDLE”和“ACK”状态，这些状态基于各自的输入和输出。

对于用SystemVerilog编写的验证代码，首先实现了必要的基础设施，并生成了使状态之间转换成为可能的时钟脉冲。在第一个时钟脉冲时，最初的高电平复位信号被拉低以激活所有其他信号。随后，进行所需的操作。

结论

使用特定于设计的验证框架评估了I2C主控制器的准确操作和可靠的数据通信，这对于航空航天应用至关重要。与传统基于仿真的或混合硬件/软件的方法相比，所提出的方法应用了先进的模型检查技术——有界模型检查（bounded model checking）、覆盖分析（cover analysis）和定理证明（theorem proving）——来系统地探索相关内容。

利益冲突声明

作者声明他们没有已知的可能会影响本文所述工作的竞争性财务利益或个人关系。

Merve Berik获得了土耳其安卡拉?ankaya大学电气电子工程系的硕士学位。她以一等荣誉毕业于土耳其Zonguldak的Bülent Ecevit大学的电气电子工程学士学位。她目前担任土耳其安卡拉TUSA?公司的首席数字设计验证工程师。