Probabilistic equivalence checking of multiple-valued functions

This paper describes a probabilistic method for verifying the equivalence of two multiple-valued functions. Each function is hashed to an integer code by transforming it to a integer-valued polynomial and evaluating it for values of variables taken independently and uniformly at random from a finite field. Since the polynomial is unique for a given function, if two hash codes are different, then the functions are not equivalent. However, if two hash codes are the same, the functions may or may not be equivalent, because different polynomials may happen to hash to the same code. Thus, the method presented in this paper determines the equivalence of two functions with a known (small) probability of error, arising from collisions between inequivalent functions. Such a method seems to be an attractive alternative for verifying functions that are too large to be handled by deterministic equivalence checking methods.