Improved Boolean function hashing based on multiple-vertex dominators

ABSTRACT

The growing complexity of today's system designs requires fast and robust verification methods. Existing BDD, SAT or ATPG-based techniques do not provide sufficient solutions for many verification instances. Boolean function hashing is a probabilistic verification approach which can complement existing formal methods in a number of applications such as equivalence checking, biased random simulation, power analysis and power optimization. The proposed hashing technique is based on the arithmetic transform, which maps a Boolean function onto a probabilistic hash value for a given input assignment. The presented algorithm uses multiple-vertex dominators in circuit graphs to progressively simplify intermediate hashing steps. The experimental results on benchmark circuits demonstrate the robustness of our approach.

REFERENCES

• 1: Vaughan R. Pratt, Anatomy of the Pentium Bug, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.97-107, May 22-26, 1995
• 2: René Krenz , Elena Dubrova , Andreas Kuehlmann, Fast Algorithm for Computing Spectral Transforms of Boolean and Multiple-Valued Functions on Circuit Representation, Proceedings of the 33rd International Symposium on Multiple-Valued Logic, p.334, May 16-19, 2003
• 3: Edward S. Lowry , C. W. Medlock, Object code optimization, Communications of the ACM, v.12 n.1, p.13-22, Jan. 1969 [doi>10.1145/362835.362838]
• 4: Thomas Lengauer , Robert Endre Tarjan, A fast algorithm for finding dominators in a flowgraph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.121-141, July 1979 [doi>10.1145/357062.357071]
• 5: M. Blum, A. K. Chandra, and M. N. Wegman, "Equivalence of free Boolean graphs can be decided probabilistically in polynomial time," Information Processing Letters, vol. 10, pp. 80--82, March 1980.
• 6: J. Jain, J. Bitner, D. S. Fussell, and J. A. Abraham, "Probabilistic verification of Boolean functions," Formal Methods in System Design, vol. 1, pp. 63--117, 1992.
• 7: Whitney J. Townsend , Mitchell A. Thornton , Rolf Drechsler , D. Michael Miller, Computing walsh, arithmetic, and reed-muller spectral decision diagrams using graph transformations, Proceedings of the 12th ACM Great Lakes symposium on VLSI, April 18-19, 2002, New York, New York, USA [doi>10.1145/505306.505344]
• 8: K. P. Parker and E. J. McCluskey, "Probabilistic treatment of general combinational networks," Transactions on Computers, pp. 668--670, June 1975.
• 9: Rajeev Motwani , Prabhakar Raghavan, Randomized algorithms, Cambridge University Press, New York, NY, 1995
• 10: A. Ghosh , S. Devadas , K. Keutzer , J. White, Estimation of average switching activity in combinational and sequential circuits, Proceedings of the 29th ACM/IEEE conference on Design automation, p.253-259, June 08-12, 1992, Anaheim, California, United States
• 11: Paul W. Purdom, Jr. , Edward F. Moore, Immediate predominators in a directed graph [H], Communications of the ACM, v.15 n.8, p.777-778, Aug. 1972 [doi>10.1145/361532.361566]
• 12: Alfred V. Aho , Jeffrey D. Ullman, The Theory of Parsing, Translation, and Compiling, Prentice Hall Professional Technical Reference, 1972
• 13: Stephen Alstrup , Jens Clausen , Kristian Jørgensen, An OV* E algorithm for finding immediate multiple-vertex dominators, Information Processing Letters, v.59 n.1, p.9-11, July 8, 1996 [doi>10.1016/0020-0190(96)00085-3]
• 14: Rajiv Gupta, Generalized dominators and post-dominators, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.246-257, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143216]
• 15: S. Alstrup, P. W. Lauridsen, and M. Thorup, "Generalized dominators for structured programs," Algorithmica, vol. 27, no. 3, pp. 244--253, 2000.
• 16: E. M. Clarke , K. L. McMillan , X Zhao , M. Fujita , J. Yang, Spectral transforms for large boolean functions with applications to technology mapping, Proceedings of the 30th international conference on Design automation, p.54-60, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164569]
• 17: R. Iris Bahar , Erica A. Frohm , Charles M. Gaona , Gary D. Hachtel , Enrico Macii , Abelardo Pardo , Fabio Somenzi, Algebraic decision diagrams and their applications, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.188-191, November 07-11, 1993, Santa Clara, California, United States
• 18: F. Somenzi, CUDD: CU Decision Diagram Package, Release 2.3.1. University of Colorado at Boulder, 2001.