Statistical Equivalence Checking Using Partial Haar Spectral Diagrams

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

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.