DESIGN AND VERIFICATION OF PARITY CHECKING CIRCUIT USING HOL4 THEOREM PROVING

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.