Article

Verification of integer multipliers on the arithmetic bit level

Authors:

Dominik Stoffel,

Wolfgang KunzAuthors Info & Claims

ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design

Pages 183 - 189

Published: 04 November 2001 Publication History

Get Access

Abstract

One of the most severe short-comings of currently available equivalence checkers is their inability to verify integer multipliers. In this paper, we present a bit level reverse-engineering technique that can be integrated into standard equivalence checking flows. We propose a Boolean mapping algorithm that extracts a network of half adders from the gate netlist of an addition circuit. Once the arithmetic bit level representation of the circuit is obtained, equivalence checking can be performed using simple arithmetic operations. Experimental results show the promise of our approach.

References

[1]

J. R. Bitner, J. Jain, M. S. Abadir, J. A. Abraham, and D. S. Fussell, "Efficient Algorithmic Circuit Verification Using Indexed BDDs," in Proc. Fault Tolerant Computing Symposium (FTCS-94), pp. 266-275, 1994.

Crossref

Google Scholar

[2]

D. Brand, "Verification of Large Synthesized Designs," in Proc. Intl. Conf. on Computer-Aided Design (ICCAD-93), pp. 534-537, 1993.

Digital Library

Google Scholar

[3]

R. Bryant and Y. A. Chen, "Verification of Arithmetic Functions by Binary Moment Diagrams," in Proc. Design Automation Conference (DAC-95), pp. 535-541, 1995.

Digital Library

Google Scholar

[4]

Y.-A. Chen and J.-C. Chen, "Equivalence Checking of Integer Multipliers," in Proc. Asia and South Pacific Design Automation Conference (ASPDAC-01), (Yokohama, Japan), 2001.

Digital Library

Google Scholar

[5]

M. Fujita, "Verification of Arithmetic Circuits by Comparing Two Similar Circuits," in Proc. International Conference on Computer Aided Verification (CAV '96).

Digital Library

Google Scholar

[6]

K. Hamaguchi, A. Morita, and S. Yajima, "Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits," in Proc. Internation Conference on Computer-Aided Design (ICCAD-95), pp. 78-82, November 1995.

Digital Library

Google Scholar

[7]

J. Jain, R. Mukherjee, and M. Fujita, "Advanced Verification Techniques Based on Learning," in Proc. 32nd ACM/IEEE Design Automation Conference (DAC-95), pp. 420-426, June 1995.

Digital Library

Google Scholar

[8]

M. Keim, M. Martin, B. Becker, R. Drechsler, and P. Molitor, "Polynomial Formal Verification of Multipliers," in VLSI Test Symp., pp. 150-155, 1997.

Digital Library

Google Scholar

[9]

A. Kühlmann and F. Krohm, "Equivalence Checking Using Cuts and Heaps," in Proc. Design Automation Conference (DAC-97), pp. 263-268, Nov. 1997.

Digital Library

Google Scholar

[10]

W. Kunz, "An Efficient Tool for Logic Verification Based on Recursive Learning," in Proc. Intl. Conference on Computer-Aided Design (ICCAD-93), pp. 538-543, Nov. 1993.

Digital Library

Google Scholar

[11]

W. Kunz and D. Stoffel, Reasoning in Boolean Networks - Logic Synthesis and Verification Using Testing Techniques. Boston: Kluwer Academic Publishers, 1997.

Digital Library

Google Scholar

[12]

Y. Matsunaga, "An Efficient Equivalence Checker for Combinational Circuits," in Proc. Design Automation Conference (DAC-96), pp. 629-634, June 1996.

Digital Library

Google Scholar

[13]

T. Stanion, "Implicit Verification of Structurally Dissimilar Arithmetic Circuits," in Proc. International Conference on Computer Design (ICCD-99), pp. 46-50, October 1999.

Digital Library

Google Scholar

Cited By

View all

Wei XDiao YLam TWu YNebel WAtienza D(2015)A universal macro block mapping scheme for arithmetic circuitsProceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition10.5555/2755753.2757190(1629-1634)Online publication date: 9-Mar-2015
https://dl.acm.org/doi/10.5555/2755753.2757190
Krautz UWedler MKunz WWeber KJacobi CPflanz MKyung CChoi KHa S(2008)Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proofProceedings of the 2008 Asia and South Pacific Design Automation Conference10.5555/1356802.1356902(398-403)Online publication date: 21-Jan-2008
https://dl.acm.org/doi/10.5555/1356802.1356902
Lai CHuang CKhoo KSciuto D(2008)Improving constant-coefficient multiplier verification by partial product identificationProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403575(813-818)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403575
Show More Cited By

Index Terms

Verification of integer multipliers on the arithmetic bit level
1. Hardware
  1. Integrated circuits
    1. Logic circuits
      1. Arithmetic and datapath circuits
      2. Combinational circuits
  2. Very large scale integration design
    1. Application-specific VLSI designs

Recommendations

Bit-Serial Multipliers and Squarers

Traditional bit-serial multipliers present one or more clock cycles of data-latency. In some situations, it is desirable to obtain the output after only a combinational delay, as in serial adders and subtracters. A serial multiplier and a squarer with ...
Equivalence checking of arithmetic circuits on the arithmetic bit level

One of the most severe shortcomings of currently available equivalence checkers is their inability to verify arithmetic circuits and multipliers, in particular. In this paper, we present a bit-level reverse-engineering technique that complements standard ...
32-bit superconductor integer and floating-point multipliers

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design

November 2001

656 pages

ISBN:0780372492

Conference Chair:
Rolf Ernst
Tech. Univ. of Braunschweig, Braunschweig, Germany

Publisher

IEEE Press

Publication History

Published: 04 November 2001

Check for updates

Qualifiers

Article

Conference

ICCAD01

Sponsor:

SIGDA

ICCAD01: International Conference on Computer Aided Design

November 4 - 8, 2001

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
223
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wei XDiao YLam TWu YNebel WAtienza D(2015)A universal macro block mapping scheme for arithmetic circuitsProceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition10.5555/2755753.2757190(1629-1634)Online publication date: 9-Mar-2015
https://dl.acm.org/doi/10.5555/2755753.2757190
Krautz UWedler MKunz WWeber KJacobi CPflanz MKyung CChoi KHa S(2008)Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proofProceedings of the 2008 Asia and South Pacific Design Automation Conference10.5555/1356802.1356902(398-403)Online publication date: 21-Jan-2008
https://dl.acm.org/doi/10.5555/1356802.1356902
Lai CHuang CKhoo KSciuto D(2008)Improving constant-coefficient multiplier verification by partial product identificationProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403575(813-818)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403575
(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
Wedler MStoffel DKunz WJoyner WMartin GKahng A(2005)Normalization at the arithmetic bit levelProceedings of the 42nd annual Design Automation Conference10.1145/1065579.1065699(457-462)Online publication date: 13-Jun-2005
https://dl.acm.org/doi/10.1145/1065579.1065699
Jacobi CWeber KParuthi VBaumgartner J(2005)Automatic Formal Verification of Fused-Multiply-Add FPUsProceedings of the conference on Design, Automation and Test in Europe - Volume 210.1109/DATE.2005.75(1298-1303)Online publication date: 7-Mar-2005
https://dl.acm.org/doi/10.1109/DATE.2005.75
Winkelmann KTrylus HStoffel DFey G(2004)Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate CoprocessorProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969050Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969050
Wedler MStoffel DKunz W(2004)Arithmetic Reasoning in DPLL-Based SAT SolvingProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969005Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969005

View Options

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

Bit-Serial Multipliers and Squarers

Equivalence checking of arithmetic circuits on the arithmetic bit level

32-bit superconductor integer and floating-point multipliers