Article

Free access

Equivalence checking of datapaths based on canonical arithmetic expressions

Authors:

Zheng Zhou,

Wayne BurlesonAuthors Info & Claims

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

Pages 546 - 551

https://doi.org/10.1145/217474.217585

Published: 01 January 1995 Publication History

PDF eReader

References

[1]

A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison- Wesley, Reading,Mass., 1974.

Digital Library

Google Scholar

[2]

A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

Digital Library

Google Scholar

[3]

R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. Technical report, University of Colorado, 1993.

Google Scholar

[4]

R.E. Bryant. Graph-based algorithms for boolean functions. IEEE Trans. on Computers, C-35(8):677-691, 1986.

Digital Library

Google Scholar

[5]

R.E. Bryant and Y.A. Chen. Verification of arithmetic functions with binary moment diagrams. Technical Report CMU-CS-94- 160, Carnegie Mellon University, 1994.

Digital Library

Google Scholar

[6]

E. Cardoza, R. Lipton, and A.R. Meyer. Exponential space complete problems for petri nets and communtative semigroups. In A CM Symp. on Theory of Computing, 1976.

Digital Library

Google Scholar

[7]

V. Chaiyakul, D. Gajski, and L. Ramachandran. High-level transformations for minimizing syntactic variances. In 30th Design Automation Conference, pages 413-418, 1993.

Digital Library

Google Scholar

[8]

E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang. Spectral transforms for large boolean functions with applications to technology mapping. In 30th A CM/IEEE Design Automation Conference, pages 54-60, 1993.

Digital Library

Google Scholar

[9]

N. Dershowitz. Rewrite systems. In Handbook of Theoretical Computer Science, pages 243-320. Elsevier Science Publishers B.V., 1990.

Digital Library

Google Scholar

[10]

P.J. Downey, R. Sethi, and R.E. Tarjan. Variations on the common subexpression problem. Journal of the A CM, 27(4):758- 771, 1980.

Digital Library

Google Scholar

[11]

J. Ferrante and C.W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

Google Scholar

[12]

D.D. Gajski, N.D. Dutt, A.C. Wu, and S.Y. Lin. High-Level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.

Digital Library

Google Scholar

[13]

M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Illustration of the sfg-tracing multi-level behavioral verification methodolgy, by the correctness proof of a high to low level synthesis application in CATHEDRAL-II. In Proc. ICCD- 91, pages 338-341, 1991.

Digital Library

Google Scholar

[14]

N. Immerman. Decision problems for first-order logical languages. Personal Mail, 1993.

Google Scholar

[15]

U. Kebschull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In European Design Automation Conference, pages 43-47, 1992.

Crossref

Google Scholar

[16]

D.E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2:127-163, 1968.

Crossref

Google Scholar

[17]

D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In ed. J. Leech, editor, Computational Problems in Abstract Algebras, pages 263-297. Pergamon Press, Oxford, England, 1970.

Google Scholar

[18]

Y.T. Lai and S. Sastry. Edge-valued binary decision diagrams for hierarchical verification. In 29th A CM/IEEE Design Automation Conference, pages 608-613, 1992.

Digital Library

Google Scholar

[19]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[20]

M. Potkonjak and J. Rabaey. Optimizing resource utilization using transformations. IEEE Trans. on CAD, 13(3):277-292, 1994.

Digital Library

Google Scholar

[21]

F.J. Taylor. Digital Filter Design Handbook. Marcel Dekker,Inc., 1983.

Digital Library

Google Scholar

[22]

Z. Zhou and W. Burleson. A canonical representation of algebraic expressions in high-level synthesis. Technical Report TR-94-CSE-9, ECE Dept., U. of Mass. at Amherst, 1994.

Google Scholar

[23]

Z. Zhou and W. Burleson. Selecting canonical representations for formal verification of arithmetic computations. Technical Report TR-94-CSE-10, ECE Dept., U. of Mass. at Amherst, 1994.

Google Scholar

[24]

Z. Zhou and W. Burleson. Formal verification of arithmetic expressions with applications in dsp synthesis. Submitted to Conference on Computer-Aided Verification (CAV'95), 1995.

Google Scholar

Cited By

View all

Farahmandi FAlizadeh B(2015)Groebner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extractionMicroprocessors & Microsystems10.1016/j.micpro.2015.01.00739:2(83-96)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1016/j.micpro.2015.01.007
Viswanath VVasudevan SAbraham J(2009)Dedicated RewritingProceedings of the 2009 22nd International Conference on VLSI Design10.1109/VLSI.Design.2009.85(77-82)Online publication date: 5-Jan-2009
https://dl.acm.org/doi/10.1109/VLSI.Design.2009.85
Vasudevan SViswanath VSumners RAbraham J(2007)Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting SystemsIEEE Transactions on Computers10.1109/TC.2007.107356:10(1401-1414)Online publication date: 1-Oct-2007
https://dl.acm.org/doi/10.1109/TC.2007.1073
Show More Cited By

Index Terms

Equivalence checking of datapaths based on canonical arithmetic expressions
1. Hardware

Recommendations

Optimizing equivalence checking for behavioral synthesis
DATE '10: Proceedings of the Conference on Design, Automation and Test in Europe

Behavioral synthesis is the compilation of an Electronic system-level (ESL) design into an RTL implementation. We present a suite of optimizations for equivalence checking of RTL generated through behavioral synthesis. The optimizations exploit the high-...
Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths

In this article, we present techniques for comparison between behavioral level and register transfer level (RTL) design descriptions by mapping the designs into virtual controllers and virtual datapaths. We also discuss about how the equivalence between ...
Equivalence checking of arithmetic expressions with applications in dsp synthesis

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

January 1995

760 pages

ISBN:0897917251

DOI:10.1145/217474

Chairman:
Bryan T. Preas
Xerox Parc, Palo Alto, CA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC95

Sponsor:

EDAC
SIGDA

DAC95: The 32nd Design Automation Conference

June 12 - 16, 1995

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
347
Total Downloads

Downloads (Last 12 months)46
Downloads (Last 6 weeks)8

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Farahmandi FAlizadeh B(2015)Groebner basis based formal verification of large arithmetic circuits using Gaussian elimination and cone-based polynomial extractionMicroprocessors & Microsystems10.1016/j.micpro.2015.01.00739:2(83-96)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1016/j.micpro.2015.01.007
Viswanath VVasudevan SAbraham J(2009)Dedicated RewritingProceedings of the 2009 22nd International Conference on VLSI Design10.1109/VLSI.Design.2009.85(77-82)Online publication date: 5-Jan-2009
https://dl.acm.org/doi/10.1109/VLSI.Design.2009.85
Vasudevan SViswanath VSumners RAbraham J(2007)Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting SystemsIEEE Transactions on Computers10.1109/TC.2007.107356:10(1401-1414)Online publication date: 1-Oct-2007
https://dl.acm.org/doi/10.1109/TC.2007.1073
Ciesielski MKalla PAskar S(2006)Taylor Expansion DiagramsIEEE Transactions on Computers10.1109/TC.2006.15355:9(1188-1201)Online publication date: 1-Sep-2006
https://dl.acm.org/doi/10.1109/TC.2006.153
Ghodrat MGivargis TNicolau AConte TFaraboschi PMangione-Smith BNajjar W(2005)Equivalence checking of arithmetic expressions using fast evaluationProceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems10.1145/1086297.1086317(147-156)Online publication date: 24-Sep-2005
https://dl.acm.org/doi/10.1145/1086297.1086317
Shekhar NKalla PGopalakrishnan SEnescu F(2005)Exploiting Vanishing Polynomials for Equivalence Veri.cation of Fixed-Size Arithmetic DatapathsProceedings of the 2005 International Conference on Computer Design10.1109/ICCD.2005.52(215-220)Online publication date: 2-Oct-2005
https://dl.acm.org/doi/10.1109/ICCD.2005.52
Shekhar NKalla PEnescu FGopalakrishnan S(2005)Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebraICCAD-2005. IEEE/ACM International Conference on Computer-Aided Design, 2005.10.1109/ICCAD.2005.1560081(291-296)Online publication date: 2005
https://doi.org/10.1109/ICCAD.2005.1560081
Chang YTing KAckland B(2002)Self-referential verification of gate-level implementations of arithmetic circuitsProceedings of the 39th annual Design Automation Conference10.1145/513918.513998(311-316)Online publication date: 10-Jun-2002
https://dl.acm.org/doi/10.1145/513918.513998
Ciesielski MKalla PZhihong Zheng Rouzeyre B(2002)Taylor expansion diagrams: a compact, canonical representation with applications to symbolic verificationProceedings 2002 Design, Automation and Test in Europe Conference and Exhibition10.1109/DATE.2002.998286(285-289)Online publication date: 2002
https://doi.org/10.1109/DATE.2002.998286
Ciesielski MKalla PZhihong Zeng Rouzeyre B(2001)Taylor expansion diagrams: a new representation for RTL verificationSixth IEEE International High-Level Design Validation and Test Workshop10.1109/HLDVT.2001.972810(70-75)Online publication date: 2001
https://doi.org/10.1109/HLDVT.2001.972810

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Optimizing equivalence checking for behavioral synthesis

Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths

Equivalence checking of arithmetic expressions with applications in dsp synthesis