Statistical Equivalence Checking Using Partial Haar Spectral Diagrams

组合逻辑等价检验广泛应用于各种形式验证方法中。当候选函数太大而无法在计算机内存中表示时，可能会遇到问题。这激发了对等效性检查的概率方法的需求。这个项目是一个基于两个部分表示函数的哈尔谱进行概率等价检验的探索。从部分哈尔谱图中有效地得到哈尔谱系数子集。两个逻辑函数不同的概率可以迭代细化为计算相等数值的附加哈尔谱系数对。通过使用部分哈尔谱图来解决非常大的函数的表示问题，并通过使用迭代地改进误差概率来发现更多的匹配谱系数对，从而产生概率方面的问题。与其他变换相比，哈尔小波的使用是可取的，因为系数的某些子集是相互独立的，这大大降低了概率计算的复杂性。

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.