PHDD: an efficient graph representation for floating point circuit verification

ABSTRACT

Data structures such as *BMDs, HDDs, and K*BMDs provide compact representations for functions which map Boolean vectors into integer values, but not floating point values. In this paper, we propose a new data structure, called Multiplicative Power Hybrid Decision Diagrams (*PHDDs), to provide a compact representation for functions that map Boolean vectors into integer or floating point values. The size of the graph to represent the IEEE floating point encoding is linear with the word size. The complexity of floating point multiplication grows linearly with the word size. The complexity of floating point addition grows exponentially with the size of the exponent part, but linearly with the size of the mantissa part. We applied *PHDDs to verify integer multipliers and floating point multipliers before the rounding stage, based on a hierarchical verification approach. For integer multipliers, our results are at least 6 times faster than *BMDs. Previous attempts at verifying floating point multipliers required manual intervention. We verified floating point multipliers before the rounding stage automatically.

REFERENCES

• 1: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 2: Randy E. Bryant , Yirng Chen, Verification of Arithmetic Functions with Binary Moment Diagrams, Carnegie Mellon University, Pittsburgh, PA, 1994
• 3: 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]
• 4: Yirng-An Chen , Randal E. Bryant, ACV: an arithmetic circuit verifier, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.361-365, November 10-14, 1996, San Jose, California, United States
• 5: CHEN, Y.-A., AND BRYANT, R. E. *PBHD: An efficient graph representation for floating point circuit verification. Tech. Rep. CMU-CS-97-134, School of Computer Science, Carnegie Mellon University, 1997.
• 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: E. M. Clarke , M. Fujita , X. Zhao, Hybrid decision diagrams, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.159-163, November 05-09, 1995, San Jose, California, United States
• 8: E. M. Clarke , M. Khaira , X. Zhao, Word level model checking—avoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240640]
• 9: 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]
• 10: Rolf Drechsler , Bernd Becker , Stefan Ruppertz, K*BMDs: A New Data Structure for Verification, Proceedings of the 1996 European conference on Design and Test, p.2, March 11-14, 1996
• 11: R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196444]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

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

  E. Data

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification

Keywords:
BDD, FDD, KFDD, BMD, *BMD, HDD, K*BMD, Floating Point, Verification, Formal Verifications