Formal verification for I2C communication protocol in aerospace and aviation industries

Aerospace Industry has many aviation applications that involve vast number of subsystems. Therefore, the need of reliable data communication between devices and components is a critical subject. In this context, I2C communication protocol is widely preferred over other protocols in terms of high speed, flexibility, low power consumption and reliability. However, issues such as data corruption, data loss, slow data transmission may occur in I2C data transmission. These problems can lead to serious consequences in the aviation industry, such as safety risks at multiple levels, electronic problems, air traffic management issues, and incorrect navigation information. Therefore, it is an important requirement that the I2C RTL design be written completely and without errors and also verified. The I2C master design in this thesis was downloaded from OpenCores. There are several verification methods for digital design verification. Formal Verification, which will be used for this thesis, is one of the most precise and reliable methods, especially in critical systems. This method is a significant method that mathematically proves that the design complies with certain features and requirements by saving time. This method checks and proves that the design meets specific features and requirements, providing a mathematical proof while saving time and costs. Yosys, an open source, easily integrated, flexible, synthesis framework that offers comprehensive Verilog support, and the Yosys-based Symbiyosys tool were used to implement this method. In this thesis, using the SystemVerilog Hardware Verification Language and SystemVerilog Assertion supported by Symbiyosys, design errors have been detected according to the design requirements. Thanks to Formal Verification, it prevents problems by ensuring that avionic operations with I2C designs continue smoothly.