Browsing by Author "Berik, Merve"

Now showing 1 - 2 of 2

Formal Verification for I2C Communication Protocol in Aerospace and Aviation Industries
(Elsevier B.V., 2026) Berik, Merve; Baykal, Yahya
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.
Havacılık ve Uzay Endüstrilerinde I2c İletişim Protokolünün Formal Doğrulaması
(2024) Berik, Merve; Baykal, Yahya Kemal
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.