Havacılık ve Uzay Endüstrilerinde I2c İletişim Protokolünün Formal Doğrulaması

Abstract

Havacılık sektörü, birçok alt sistem içeren havacılık uygulamalarına sahiptir. Bu nedenle cihazlar ve bileşenler arasında doğru ve güvenilir veri iletişimi kritik bir gerekliliktir. Bu bağlamda, yüksek hız, esneklik, düşük güç tüketimi ve güvenilirlik açısından I2C haberleşme protokolü diğer protokollere göre yaygın bir şekilde tercih edilir. Ancak, I2C veri iletiminde veri bozulması, veri kaybı, yavaş veri iletimi gibi sorunlar ortaya çıkabilir. Bu sorunlar havacılık sektöründe uçuş güvenliği riskleri, elektronik ve mekanik sorunlar, hava trafik yönetimi sorunları, yanlış navigasyon bilgileri gibi ciddi sonuçlara yol açabilir. Bu nedenle, I2C RTL tasarımının eksiksiz ve hatasız bir şekilde yazılması ve ayrıca doğrulanması önemli bir gerekliliktir. Bu tezdeki I2C Master Tasarımı OpenCores'dan indirilmiştir. Sayısal Tasarım Doğrulamada birçok doğrulama yöntemi vardır. Formal Doğrulama en kritik sistemlerde en kesin ve güvenilir doğrulama sağlayan yöntemlerden biridir. Bu yöntem, zamandan ve maliyetten tasarruf sağlayarak tasarımın belirli özelliklere ve gereksinimlere uygun olduğunu matematiksel olarak kontrol eder ve kanıtlar. Bu yöntemin uygulanabilmesi için açık kaynaklı, kolay entegre edilebilir, esnek, geniş kapsamlı Verilog desteği sunan bir sentez çerçevesi olan Yosys ile Yosys tabanlı Symbiyosys aracı kullanılmıştır. Bu tezde tasarım gereksinimlerine göre uygun, Symbiyosys'in kullanım desteği olan SystemVerilog Donanım Doğrulama Dili ve SystemVerilog Assertion kullanılarak tasarımdaki hatalar tespit edilmiştir. Formal Doğrulama sayesinde, I2C tasarımlarının olduğu havacılık operasyonlarının sorunsuz bir şekilde devam etmesini sağlayarak sorunların yaşanmasını engeller.

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.