Equivalence checking of arithmetic expressions using fast evaluation

ABSTRACT

Arithmetic expressions are the fundamental building blocks of hardware and software systems. An important problem in computational theory is to decide if two arithmetic expressions are equivalent. However, the general problem of equivalence checking, in digital computers, belongs to the NP Hard class of problems. Moreover, existing general techniques for solving this decision problem are applicable to very simple expressions and impractical when applied to more complex expressions found in programs written in high-level languages. In this paper we propose a method for solving the arithmetic expression equivalence problem using partial evaluation. In particular, our technique is specifically designed to solve the problem of equivalence checking of arithmetic expressions obtained from high-level language descriptions of hardware/software systems, which consists of regular arithmetic operators (+, -, x) and logical operators (and, or, not). In our method, we use interval analysis to substantially prune the domain space of arithmetic expressions and limit the evaluation effort to a sufficiently limited set of subspaces. Our results show that the proposed method is fast enough to be of use in practice.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: S.B. Akers. Binary decision diagrams. IEEE ransactions on Computers, 27(6):509--516, 1978.
• 3: R. Camposano. Path-based scheduling for synthesis. EEE Transactions on Computer-Aided Design of ntegrated Circuits and Systems, 10(1):85--93, 1991.
• 4: Viraphol Chaiyakul , Daniel D. Gajski , Loganath Ramachandran, High-level transformations for minimizing syntactic variances, Proceedings of the 30th international conference on Design automation, p.413-418, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164956]
• 5: Newton Cheung , Sri Parameswaran , Jörg Henkel , Jeremy Chan, MINCE: Matching INstructions Using Combinational Equivalence for Extensible Processor, Proceedings of the conference on Design, automation and test in Europe, p.21020, February 16-20, 2004
• 6: 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]
• 7: N. Dershowitz. Rewrite systems. Handbook of Theoretical Computer Science, Elsevier Science Publishers, 1990.
• 8: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 9: R. Drechsler. Formal verification of circuits. Kluwer Academic Publishers, The Nederlands, 2000.
• 10: Rolf Drechsler, Advanced Formal Verification, Kluwer Academic Publishers, Norwell, MA, 2004
• 11: J. Ferrante and C.W. Rackoff. The computational complexity of logical theories. Lecture Notes in Mathematics, 718, 1979.
• 12: M.A. Ghodrat and T. Givargis. Equivalence checking of arithmetic expressions using fast evaluation. Center for Embedded Computer System Technical Report CECS-05-07, 2005.
• 13: M.A. Ghodrat and T. Givargis. Expression equivalence checking using interval analysis. Center for Embedded Computer System Technical Report CECS-05-06, 2005.
• 14: Antonin Guttman, R-trees: a dynamic index structure for spatial searching, Proceedings of the 1984 ACM SIGMOD international conference on Management of data, June 18-21, 1984, Boston, Massachusetts
• 15: Stefan Höreth , Rolf Drechsler, Formal verification of word-level specifications, Proceedings of the conference on Design, automation and test in Europe, p.11-es, January 1999, Munich, Germany [doi>10.1145/307418.307447]
• 16: Hsiao-ping Juan , Viraphol Chaiyakul , Daniel D. Gajski, Condition graphs for high-quality behavioral synthesis, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.170-174, November 06-10, 1994, San Jose, California, United States
• 17: Chunho Lee , Miodrag Potkonjak , William H. Mangione-Smith, MediaBench: a tool for evaluating and synthesizing multimedia and communicatons systems, Proceedings of the 30th annual ACM/IEEE international symposium on Microarchitecture, p.330-335, December 01-03, 1997, Research Triangle Park, North Carolina, United States
• 18: J. Li , R. K. Gupta, An algorithm to determine mutually exclusive operations in behavioral descriptions, Proceedings of the conference on Design, automation and test in Europe, p.457-465, February 23-26, 1998, Le Palais des Congrés de Paris, France
• 19: Jian Li , Rajesh K. Gupta, HDL presynthesis optimizations using a tabular model, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.8 n.4, p.369-378, Aug. 2000 [doi>10.1109/92.863616]
• 20: Giovanni De Micheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill Higher Education, 1994
• 21: R.E. Moore. Interval analysis. Prentice-Hall, Englewood Cliffs, N. J., 1966.
• 22: William H. Press , Saul A. Teukolsky , William T. Vetterling , Brian P. Flannery, Numerical Recipes in C: The Art of Scientific Computing, Cambridge University Press, New York, NY, 1992
• 23: K. Wakabayashi and T. Yoshimura. A resource sharing and control synthesis method for conditional branches. In International Conference on Computer-Aided Design, pages 62--65, 1989.
• 24: Y. Xie , W. Wolf, Allocation and scheduling of conditional task graph in hardware/software co-synthesis, Proceedings of the conference on Design, automation and test in Europe, p.620-625, March 2001, Munich, Germany
• 25: Zheng Zhou , Wayne Burleson, Equivalence checking of datapaths based on canonical arithmetic expressions, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.546-551, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217585]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS

General Terms:
Algorithms, Verification

Keywords:
expression equivalence, interval analysis, mutual exclusion