Design verification is the task of establishing that a given design meets the intended behavior. The growing complexity of verification instances requires new methods that can provide high quality verification coverage for large, complex designs. Probabilistic verification complements existing simulation-based and formal verification techniques by providing a distinct trade-off between coverage and capacity. Probabilistic approach maps two Boolean functions onto hash values and compare these values for equivalence. The major drawback of probabilistic verification is the non-zero probability of collision of hash values of two non-equivalent functions, producing "false positive" verification results. In this paper, we prove the existence of a perfect input assignment which never causes collisions. We show that the equivalence of hash values computed for a perfect input assignment implies the equivalence of functions with 100% probability.
SPIE Digital Library