DESIGN AND VERIFICATION OF PARITY CHECKING CIRCUIT USING HOL4 THEOREM PROVING

被引：0

作者：

Deniz, Elif ^{[1
]}

Aksoy, Kubra ^{[1
]}

Tahar, Sofiene ^{[2
]}

Zeren, Yusuf ^{[1
]}

机构：

[1] Yildiz Tech Univ, Dept Math, Istanbul, Turkey

[2] Concordia Univ, Dept Elect & Comp Engn, Montreal, PQ, Canada

来源：

SIGMA JOURNAL OF ENGINEERING AND NATURAL SCIENCES-SIGMA MUHENDISLIK VE FEN BILIMLERI DERGISI | 2019年 / 10卷 / 02期

关键词：

Parity checking; formal verification; reliability; higher-order logic; theorem proving; HOL4;

D O I：

暂无

中图分类号：

T [工业技术];

学科分类号：

08 ;

摘要：

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.

引用

页码：245 / 252

页数：8

共 13 条

[1]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[2]

Gordon M.J., 1989, Current Trends in Hardware Verification and Automated Theorem Proving, P387, DOI [10.1007/978-1-4612-3658-0_10, DOI 10.1007/978-1-4612-3658-0_10]

[3]

Gordon Michael JC, 1993, Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic

[4]

Hall A, 2007, J UNIVERS COMPUT SCI, V13, P669

[5]

Hamming R. W., 2005, ART DOING SCI ENG

[6]

Harrison J., 1996, FORMALIZED MATH

[7]

Hasan O., 2008, THESIS

[8]

Hasan Osman, 2015, Encyclopedia of Information Science and Technology, P7162, DOI DOI 10.4018/978-1-4666-5888-2.CH705

[9]

Jensen LS, 2016, PROC INT DESIGN CONF, P821

[10]

Mano M.M., 2004, DIGITAL LOGIC COMPUT

← 1 2 →