Article

Free access

Equivalence verification of arithmetic datapaths with multiple word-length operands

Authors:

Namrata Shekhar,

Florian EnescuAuthors Info & Claims

DATE '06: Proceedings of the conference on Design, automation and test in Europe: Proceedings

Pages 824 - 829

Published: 06 March 2006 Publication History

Abstract

This paper addresses the problem of equivalence verification of RTL descriptions that implement arithmetic computations (add, mult, shift) over bit-vectors that have differing bit-widths. Such designs are found in many DSP applications where the widths of input and output bit-vectors are dictated by the desired precision. A bit-vector of size n can represent integer values from 0 to 2ⁿ -- 1; i. e. integers reduced modulo 2ⁿ. Therefore, to verify bit-vector arithmetic over multiple word-length operands, we model the RTL datapath as a polynomial function from Z²ⁿ¹ XZ ²ⁿ² X . . . X . . . Z^2nd to Z^2m. Subsequently, RTL equivalence f ≡ g is solved by proving whether (f -- g) ≡ 0 over such mappings. Exploiting concepts from number theory and commutative algebra, a systematic, complete algorithmic procedure is derived for this purpose. Experimentally, we demonstrate how this approach can be applied within a practical CAD setting. Using our approach, we verify a set of arithmetic datapaths at RTL where contemporary approaches prove to be infeasible.

References

[1]

A. Peymandoust and G. DeMicheli, "Application of Symbolic Computer Algebra in High-Level Data-Flow Synthesis", IEEE Trans. CAD, vol. 22, pp. 1154--11656, 2003.

Digital Library

[2]

M. Ciesielski, P. Kalla, Z. Zheng, and B. Rouzyere, "Taylor Expansion Diagrams: A Compact Canonical Representation with Applications to Symbolic Verification", in Proc. Design Automation and Test in Europe, DATE'02, Mar 2002.

Digital Library

[3]

V. J. Mathews and G. L. Sicuranza, Polynomial Signal Processing, Wiley-Interscience, 2000.

[4]

D. Menard, D Chillet, F Charot, and O. Sentieys, "Automatic Floating-point to Fixed-point Conversion for DSP Code Generation", in Intl. Conf. Compiler, Architecture, Synthesis Embedded Sys., CASES, 2002.

Digital Library

[5]

I. A. Groute and K. Keane, "M(VH)DL: A MATLAB to VHDL Conversion Toolbox for Digital Control", in IFAC Symp. on Computer-Aided Control System Design, Sept. 2000.

[6]

Z. Chen, "On polynomial functions from Zn1 XZn2 x . . . xZnr to Zm", Discrete Math., vol. 162, pp. 67--76, 1996.

Digital Library

[7]

O. H. Ibarra and S. Moran, "Probabilistic Algorithms for Deciding Equivalence of Straight-Line Programs", Journal of the Association for Computing Machinery, vol. 30, pp. 217--228, Jan. 1983.

Digital Library

[8]

R. E. Bryant, "Graph Based Algorithms for Boolean Function Manipulation", IEEE Trans. on Computers, vol. C-35, pp. 677--691, August 1986.

Digital Library

[9]

R. E. Bryant and Y-A. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams", in DAC, 95.

[10]

R. Dreschler, B. Becker, and S. Ruppertz, "The K*BMD: A Verification Data Structure", IEEE Design & Test, pp. 51--59, 1997.

Digital Library

[11]

A. Jabir and Pradhan D., "MODD: A New Decision Diagram and Representation for Multiple Output Binary Functions", in Design, Automation and Test in Europe, DATE, 2004.

Digital Library

[12]

K. Radecka and Z. Zilic, "Specifying and verifying imprecise sequential datapaths by arithmetic transforms", in Intl. Conf. Computer-Aided Design, 2002.

Digital Library

[13]

D. Cyrluk, O. Moller, and H. Ruess, "An Efficient Procedure for the Theory of Fixed-Size Bitvectors", in LCNS, CAV, vol. 1254, 1997.

Digital Library

[14]

C. W. Barlett, D. L. Dill, and J. R. Levitt, "A Decision Procedure for bit-Vector Arithmetic", in DAC, June 1998.

Digital Library

[15]

C.-Y. Huang and K.-T. Cheng, "Using Word-Level ATPG and Modular Arithmetic Constraint Solving Techniques for Assertion Property Checking", IEEE Trans. CAD, vol. 20, pp. 381--391, 2001.

Digital Library

[16]

R. Brinkmann and R. Drechsler, "RTL-Datapath Verification using Integer Linear Programming", in Proc. ASP-DAC, 2002.

Digital Library

[17]

M. Wedler, D. Stoffel, and W. Kunz, "Normalization at the Arithmetic Bit-Level", in Design Automation Conf., 2005.

Digital Library

[18]

Z. Zhou and W. Burleson, "Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions", in DAC, 95.

[19]

V. Paruthi, N. Mansouri, and R. Vemuri, "Automatic datapath abstraction for verification of large scale designs", in Intl. Conf. on Computer Design, 1998.

Digital Library

[20]

T. Raudvere, A. K. Singh, I. Sander, and Jantsch. A, "System level verification of digital signal processing applications based on the polynomial abstraction technique", in Intl. Conf. on Computer Aided Design, Nov 2005.

Digital Library

[21]

T. Becker and V. Weispfenning, Grobner Bases: A Computational Approach to Commutative Algebra, Springer-Verlag, 1993.

Digital Library

[22]

J. Grabmeier, E. Kaltofen, and V. Weispfenning, Computer Algebra Handbook, Springer-Verlag, 2003.

Digital Library

[23]

N. Shekhar, P. Kalla, F. Enescu, and S. Gopalakrishnan, "Exploiting Vanishing Polynomials for Equivalence Verification of Fixed-Size Arithmetic Datapaths", in Intl. Conf. Computer Design, 2005.

Digital Library

[24]

N. Shekhar, P. Kalla, F. Enescu, and S. Gopalakrishnan, "Equivalence Verification of Polynomial Datapaths with Fixed-Size Bit-Vectors using Finite Ring Algebra", in Intl. Conf. on Computer-Aided Design, ICCAD, 2005.

Digital Library

[25]

F. Smarandache, "A function in number theory", Analele Univ. Timisoara, Fascicle 1, vol. XVII, pp. 79--88, 1980.

[26]

D. Power, S. Tabirca, and T. Tabirca, "Java Concurrent Program for the Smarandache Function", Smarandache Notions Journal, vol. 13, pp. 72--84, 2002.

Digital Library

[27]

Maple,", http://www.maplesoft.com.

[28]

A. K. Verma and P. Ienne, "Improved use of the Carry-save Representation for the Synthesis of Complex Arithmetic Circuits", in Proceedings of the International Conference on Computer Aided Design, 2004.

Digital Library

[29]

M. R. Guthaus, J. S. Ringenberg, D. Ernst, T. M. Austin, T. Mudge, and R. B. Brown, "Mibench: A Free, Commercially Representative Embedded Benchmark Suite", in IEEE 4th Annual Workshop on Workload Characterization, Dec 2001.

Digital Library

[30]

Universite' de Bretagne Sud LESTER, "Gaut, Architectural Synthesis Tool", http://lester.univ-ubs.fr:8080, vol., 2004.

[31]

R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vencentelli, F. Somenzi, A. Aziz, S-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, G. Shiple, S. Swamy, and T. Villa, "VIS: A System for Verification and Synthesis", in Computer aided Verification, 1996.

Digital Library

[32]

M. Moskewicz, C. Madigan, L. Zhao, and S. Malik, "CHAFF: Engineering and Efficient SAT Solver", in In Proc. Design Automation Conference, pp. 530--535, June 2001.

Digital Library

Cited By

(2008)Arithmetic Circuits Verification without Looking for Internal EquivalencesProceedings of the Sixth ACM/IEEE International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2008.4547681(7-16)Online publication date: 1-Jun-2008
https://dl.acm.org/doi/10.1109/MEMCOD.2008.4547681
Wienand OWedler MStoffel DKunz WGreuel G(2008)An Algebraic Approach for Proving Data Correctness in Arithmetic Data PathsProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_45(473-486)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_45
Gopalakrishnan SKalla P(2007)Optimization of polynomial datapaths using finite ring algebraACM Transactions on Design Automation of Electronic Systems10.1145/1278349.127836212:4(49-es)Online publication date: 1-Sep-2007
https://dl.acm.org/doi/10.1145/1278349.1278362

Recommendations

Optimization of Arithmetic Datapaths with Finite Word-Length Operands
ASP-DAC '07: Proceedings of the 2007 Asia and South Pacific Design Automation Conference

This paper presents an approach to area optimization of arithmetic datapaths that perform polynomial computations over bit-vectors with finite widths. Examples of such designs abound in DSP for audio, video and multimedia computations where the input ...
Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands
FMCAD '06: Proceedings of the Formal Methods in Computer Aided Design

This paper addresses simulation-based verification of highlevel descriptions of arithmetic datapaths. Instances of such designs are commonly found in DSP for audio, video and multimedia applications, where the word-lengths of input/output bit-vectors ...
Reliable Floating-Point Arithmetic Algorithms for Error-Coded Operands

Reliable floating-point arithmetic is vital for dependable computing systems. It is also important for future high-density VLSI realizations that are vulnerable to soft-errors. However, the direct checking of floating-point arithmetic is still an open ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

DATE '06: Proceedings of the conference on Design, automation and test in Europe: Proceedings

March 2006

1390 pages

ISBN:3981080106

General Chair:
Georges Gielen
KU Leuven, BE

Sponsors

EDAA: European Design Automation Association
The EDA Consortium
IEEE-CS\DATC: The IEEE Computer Society

Publisher

European Design and Automation Association

Leuven, Belgium

Publication History

Published: 06 March 2006

Qualifiers

Article

Acceptance Rates

DATE '06 Paper Acceptance Rate 267 of 834 submissions, 32%;

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
244
Total Downloads

Downloads (Last 12 months)69
Downloads (Last 6 weeks)14

Reflects downloads up to 17 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

(2008)Arithmetic Circuits Verification without Looking for Internal EquivalencesProceedings of the Sixth ACM/IEEE International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2008.4547681(7-16)Online publication date: 1-Jun-2008
https://dl.acm.org/doi/10.1109/MEMCOD.2008.4547681
Wienand OWedler MStoffel DKunz WGreuel G(2008)An Algebraic Approach for Proving Data Correctness in Arithmetic Data PathsProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_45(473-486)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_45
Gopalakrishnan SKalla P(2007)Optimization of polynomial datapaths using finite ring algebraACM Transactions on Design Automation of Electronic Systems10.1145/1278349.127836212:4(49-es)Online publication date: 1-Sep-2007
https://dl.acm.org/doi/10.1145/1278349.1278362

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten