Formal Verification for I2C Communication Protocol in Aerospace and Aviation Industries

Abstract

The aerospace industry comprises many safety-critical applications that involve a vast number of interacting subsystems. Reliable data communication between devices and components is therefore essential. In this context, Inter-Integrated Circuit (I2C) communication protocol is widely preferred due to its simplicity, flexibility, low power consumption, and reliability. However, issues such as data corruption, data loss, and increased latency may still occur and can lead to serious consequences in aviation, including safety risks, electronic malfunctions, air traffic management problems, and incorrect navigation information. To avoid such failures, the I2C RegisterTransfer Level (RTL) design must be both correctly implemented and rigorously verified. There are several verification methods for digital design verification. Among several digital design verification approaches, Formal Verification (FV) is one of the most precise and reliable methods for safety- critical systems, as it provides mathematical proofs of conformance to specified properties. In this work, an open-source, Yosys-based formal verification flow is applied to an open-source I2C master design using the SymbiYosys framework. The verification environment is developed in SystemVerilog with SystemVerilog Assertions, enabling the detection of design errors directly against the protocol requirements. By combining bounded model checking, cover analysis, and theorem-proving, the proposed flow systematically verifies all five finite-state-machine (FSM) states and nine transitions of the I2C master. The results demonstrate that formal verification can systematically ensure robust and fault-tolerant I2C operation for avionics applications.