DESIGN AND VERIFICATION OF PARITY CHECKING CIRCUIT USING HOL4 THEOREM PROVING

---

Atıf İçin Kopyala

Deniz E., Aksoy K., Tahar S., ZEREN Y.

SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI, cilt.10, sa.2, ss.245-252, 2019 (ESCI)

• Yayın Türü: Makale / Tam Makale
• Cilt numarası: 10 Sayı: 2
• Basım Tarihi: 2019
• Dergi Adı: SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI
• Derginin Tarandığı İndeksler: Emerging Sources Citation Index (ESCI), Academic Search Premier, Directory of Open Access Journals
• Sayfa Sayıları: ss.245-252
• Yıldız Teknik Üniversitesi Adresli: Evet

Özet

Digital data transmission is the most widely used way of modern communication. The data transmission from source to destination should be without loss of information. This is possible by using the method of parity generator and parity checker. A parity check is the process that ensures accurate data transmission between nodes during communication. In this paper, we present the design and formal verification of a parity checking circuit using Higher-Order Logic theorem proving. We use the HOL4 theorem prover to mathematically describe the parity checking specification as well as mathematical model of the circuit implementation. The formal verification of reliability shows that the circuit implementation satisfies the parity checking specification for all inputs and outputs.