Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

In this paper, we address on equivalence checking of integer multipliers, especially for the multipliers without structure similarity. Our approach is based on Hamaguchi's backward substitution method with the following improvements: (1) automatic identification of components to form proper cut points and thus dramatically improve the backward substitution process, (2) a layered-backward substitution algorithm to reduce the number of substitutions, and (3) Multiplicative Power Hybrid Decision Diagrams(*PHDDs) as our word-level representation rather than *BMD in Hamaguchi's approach. Experimental results show that our approach can efficiently check the equivalence of two integer multipliers. To verify the equivalence of a 32 x 32 array multiplier versus a 32 x 32 Wallace tree multiplier, our approach takes about 57 CPU seconds using 11 Mbytes, while Stanion's approach took 21027 seconds using 130 MBytes. We also show that the complexity of our approach grows cubically O(n3).

REFERENCES

• 1: A. D. Booth. A signed binary multiplication technique. In Journal of Mechanics and Applied Mathematics, pages 236-240, 1951.
• 2: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 3: Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
• 4: Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217583]
• 5: Yirng-An Chen , Randal E. Bryant, PHDD: an efficient graph representation for floating point circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.2-7, November 09-13, 1997, San Jose, California, United States
• 6: Yirng-An Chen , Edmund M. Clarke , Pei-Hsin Ho , Yatin Vasant Hoskote , Timothy Kam , Manpreet Khaira , John W. O'Leary , Xudong Zhao, Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.19-33, November 06-08, 1996
• 7: T. Coe. Inside the Pentium Fdiv bug. Dr. Dobbs Journal, pages pp. 129-135, April 1996.
• 8: Kiyoharu Hamaguchi , Akihito Morita , Shuzo Yajima, Efficient construction of binary moment diagrams for verifying arithmetic circuits, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.78-82, November 05-09, 1995, San Jose, California, United States
• 9: Jawahar Jain , James Bitner , Magdy S. Abadir , Jacob A. Abraham , Donald S. Fussell, Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions, IEEE Transactions on Computers, v.46 n.11, p.1230-1245, November 1997 [doi>10.1109/12.644298]
• 10: Martin Keim , Michael Martin , Bernd Becker , Rolf Drechsler , Paul Molitor, Polynomial Formal Verification of Multipliers, Proceedings of the 15th IEEE VLSI Test Symposium (VTS'97), p.150, April 27-May 01, 1997
• 11: T. Mainelli. Intel 820 owners could get free upgrade. In PC World, May 2000.
• 12: Implicit Verification of Structurally Dissimilar Arithmetic Circuits, Proceedings of the 1999 IEEE International Conference on Computer Design, p.46, October 10-13, 1999
• 13: B. Yang, Y.-A. Chen, R. E. Bryant, and D. R. O'Hallaron. Space- and time-efficient bdd construction via working set control. In Proceedings of ASP-DAC '98, pages 423-432, Yokohoma, Japan, Feb. 1998.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

Additional Classification:
  B. Hardware

  G. Mathematics of Computing

General Terms:
Algorithms, Design, Performance, Theory