Statistical Equivalence Checking Using Partial Haar Spectral Diagrams

Mississippi State University, Mississippi State MS

Investigators

Abstract

Combinational logic equivalence checking is used extensively in various formal verification approaches. Problems can be encountered when the candidate functions are too large to be represented in the memory of a computer. This motivates the need for probabilistic approaches for equivalence checking. This project is an exploration of performing probabilistic equivalence checking based on the Haar spectrum of two partially represented functions. Subsets of Haar spectral coefficients are obtained from partial Haar spectral diagrams efficiently. The probability that two logic functions differ can be iteratively refined as additional pairs of Haar spectral coefficients with equal numeric value are calculated. The problem of representation of very large functions is addressed through the use of the partial Haar spectral diagram and the probabilistic aspect arises through the use of iteratively refining the error probability as more matching pairs of spectral coefficients are found. The use of the Haar wavelet is desirable as compared to other transforms since certain subsets of the coefficients are mutually independent which greatly reduces the complexity of the probability calculations.