A decision procedure for bit-vector arithmetic

ABSTRACT

Bit-v ector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in suc h a theory is NP-hard, our implementation is efficient for many practical examples. We believ e this to be the first such implementation which is efficient, automatic, and complete.

REFERENCES

• 1: Laurent Arditi, BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.34-48, November 06-08, 1996
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 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: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 5: David Cyrluk , Patrick Lincoln , Natarajan Shankar, On Shostak's Decision Procedure for Combinations of Theories, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.463-477, August 03, 1996
• 6: David Cyrluk , M. Oliver Möller , Harald Rueß, An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors, Proceedings of the 9th International Conference on Computer Aided Verification, p.60-71, June 22-25, 1997
• 7: Joseph A. Gallian. Contemporary Abstract Algebra. D. C. Heath and Company, second edition, 1990.
• 8: Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
• 9: Robert B. Jones , David L. Dill , Jerry R. Burch, Efficient validity checking for processor verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.2-6, November 05-09, 1995, San Jose, California, United States
• 10: Leo G. Marcus. SOVS 13 Users'Manual. The Aerospace Corporation, E1 Segundo, CA 90245, October 1994. Aerospace Report ATR-94(4778)-5.
• 11: Michael D. Smith , Monica S. Lam , Mark A. Horowitz, Boosting beyond static scheduling in a superscalar processor, Proceedings of the 17th annual international symposium on Computer Architecture, p.344-354, May 28-31, 1990, Seattle, Washington, United States
• 12: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, November 1996
• 13: Wai Wong, Modelling Bit Vectors in HOL: the word library, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.371-384, August 11-13, 1993

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Measurement, Performance, Theory

Keywords:
MPEG4, codec, design automatian, flip-flops, level converters, low power, placement, synthesis, voltage scaling