Havacılık ve uzay endüstrilerinde I2C iletişim protokolünün formal doğrulaması

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.