New Techniques for Boolean Verification

Computer Engineering Research Center
The University of Texas at Austin

Verifying the equivalence of two Boolean functions is at the heart of all formal verification techniques. Current industry tools are best suited for checking the equivalence of two combinational netlists, or the equivalence of a combinational circuit with a Boolean specification. Approaches for achieving this are generally based on transforming the two functions to a canonical form, and then checking for equivalence. The most popular canonical form in use is the Reduced, Ordered, Binary Decision Diagram (ROBDD, commonly referred to as BDD).

Our work has concentrated on novel techniques for Boolean verification, in particular, the use of Probabilistic techniques. Powerful partitioning techniques for reducing the complexity of verification, such as "functional partitioning", and new data structures such as "Indexed Binary Decision Diagrams (IBDDs)" have also been studied.

Selected Papers

J. Jain, J. Bitner, D. S. Fussell and J. A. Abraham, "A Probabilistic Verification Theory for Boolean Functions," International Journal on Formal Methods in Verification, vol. 1, 1992, pp. 61-115.

Abstract

We present a novel method of 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, e, 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 a 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.

J. Bitner, J. Jain, M. Abadir, J. A. Abraham and D. S. Fussell, "Efficient Algorithmic Circuit Verification Using Indexed BDD's," Proceedings 24th Annual International Symposium on Fault-Tolerant Computing, Austin, TX, June 1994, pp. 266-275.

Abstract

A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), was proposed to provide a compact representation for funcitons whose OBDD representation is intractably large. In this paper, we present more efficient algorithms for satisfiability testing and equivalence checking of IBDDs. Efficient verification of Booth multipliers, as well as practical strategies for polynomial time verification of some classes of unsigned array multipliers, are demonstrated experimentally. Our results show that the verification of many instances of functions whose analysis is intractable using OBDDs, such as multipliers and the hidden-weighted-bit function, can be done efficiently using IBDDs.

J. Jain, J. Bitner, M. Abadir, J. A. Abraham and D. S. Fussell, "Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions," IEEE Transactions on Computers, (to appear).

J. Jain, J. Bitner, J. A. Abraham and D. S. Fussell, "Functional Partitioning for Verification and Related Problems," MIT/Brown Symposium on VLSI, Providence, RI March 25-27, 1992, pp. 210-226.

R. Mukherjee, J. Jain, M. Fujita, J. A. Abraham and D. S. Fussell, "On More Efficient Combinational ATPG using Functional Learning," Proc. 9th International Conference on VLSI Design, January 1996, pp. 107-110.

Back to: