On the accurate reliability analysis of combinational circuits using theorem proving

Reliability analysis of combinational circuits has become imperative these days due to the extensive usage of nanotechnologies in their fabrication. Traditionally, reliability analysis is done using simulation or paper-and-pencil proof methods. But, these techniques do not ensure accurate results and thus may lead to disastrous consequences when dealing with safety critical applications. In this paper, we mainly tackle the accuracy problem of reliability analysis by presenting a formal approach that is based on higher-order-logic theorem proving. The paper presents formal definitions of gate fault and reliability and utilizes them to formally verify some key reliability properties in a theorem prover. This formal infrastructure can be used to formally analyze the reliability of any combinational circuit. For illustration purposes, we utilize the proposed framework to analyze the reliability of a comparator and a full adder.