The potential and limitation of probability-based combinational equivalence checking

This paper presents a probability based approach to logic equivalence checking. First, a general probability assignment procedure is proposed to uniquely characterize output probability of a network. Thus, the equivalence of two networks can be asserted by the equality of output probabilities. To improve the efficiency of probability calculation, a new encoding scheme and operations are proposed. These encoding scheme and operations also solve the signal correlation issue during the output probability evaluation. As a result, an exact output probability of a network is successfully derived in one pass. Finally, the equivalence of internal gates between two networks are exploited to reduce the number of required input assignments and improve the efficiency of our approach. In the experiments, our approach is compared with a BDD based approach in terms of CPU time and memory usage. The results disclose the potential and limitation of the probabilistic approach to logic equivalence checking.