Probabilistic verification of Boolean functions |
| |
Authors: | Jawahar Jain Jacob A. Abraham James Bitner Donald S. Fussell |
| |
Affiliation: | (1) Computer Engineering Research Center and Department of Electrical and Computer Engineering, The University of Texas at Austin, 78712 Austin, TX;(2) Computer Engineering Research Center, The University of Texas at Austin, 78758 Austin, TX;(3) Computer Engineering Research Center and Department of Computer Science, The University of Texas at Austin, 78712 Austin, TX |
| |
Abstract: | We present a novel method for verifying the equivalence of two Boolean functions. Each function is hashed to an integer code by assigning random integer values to the input variables and evaluating an integer-valued transformation of the original function. The hash codes for two equivalent functions are always equal. Thus the equivalence of two functions can be verified with a very low probability of error, which arises from unlikely collisions between inequivalent functions. An upper bound, , on the probability of error is known a priori. The bound can be decreased exponentially by making multiple runs. Results indicate significant time and space advantages for this method over techniques that represent each function as a single OBDD. Some functions known to require space (and time) exponential in the number of input variables for these techniques require only polynomial resources using our method. Experimental results indicate that probabilistic verification can provide an attractive alternative for verifying functions too large to be handled using these OBDD-based techniques. |
| |
Keywords: | probabilistic verification Boolean functions algebraic transforms seminumeric decision diagrams orthogonal partitioning decomposed representation function representation BDDs |
本文献已被 SpringerLink 等数据库收录! |
|