Prove that a faulty multiplier is faulty!?

ABSTRACT

Formal verification of integer multipliers was an open problem for a long time as the size of any reduced ordered binary decision diagram (BDD) [1] which represents integer multiplication is exponential in the width of the operands [2]. In 1995, Bryant and Chen [4] introduced multiplicative binary moment diagrams (*BMD) which are a canonical data structure for pseudo Boolean functions allowing a linear representation of integer multipliers. Based on this data structure, Bryant/Chen [4] and Hamaguchi et.al. [5] experimentally showed that integer multipliers up to a word size of 64 bits can be formally verified. However, all these results only handle the problem of proving a faultless integer multiplier to be correct. But, what happens if the multiplier is faulty? Does the backward construction method of Hamaguchi et.al. stop after a short time? After what time can I be sure that the integer multiplier under consideration is faulty? In this paper, we show that these questions are relevant in practice. In particular, we investigate simple add-step multipliers and show that simple design errors can lead to exponential growth of the *BMDS occuring during backward construction. This proves that the backward construction method can only be applied as filter during formal logic combinational verification unless sharp upper bounds for the sizes of the *BMDs occuring during the backward construction have been proven for the various circuit types as Keim et.al. [6] did it for Wallace Tree multipliers.

REFERENCES

• 1: 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]
• 2: 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]
• 3: Randy E. Bryant , Yirng Chen, Verification of Arithmetic Functions with Binary Moment Diagrams, Carnegie Mellon University, Pittsburgh, PA, 1994
• 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: 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
• 6: 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

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
  B.6 LOGIC DESIGN

General Terms:
Theory, Verification