Article

Efficient equivalence checking with partitions and hierarchical cut-points

Authors:

Demosthenes Anastasakis,

Slawomir PilarskiAuthors Info & Claims

DAC '04: Proceedings of the 41st annual Design Automation Conference

Pages 539 - 542

https://doi.org/10.1145/996566.996714

Published: 07 June 2004 Publication History

Abstract

Previous results show that both flat and hierarchical methodologies present obstacles to effectively completing combinational equivalence checking. A new approach that combines the benefits while effectively dealing with the pitfalls of both styles of equivalence checking is presented.

References

[1]

"Digital Systems Testing and Testable Design", M. Abramovici, M.A. Breuer, A. D. Friedman, Computer Science Press, 1990.]]

[2]

"A Practical and Efficient Method for Compare-Point Matching", D. Anastasakis, R. Damiano, T. Ma, T. Stanion, Proc. Design Automation Conf., pages 305--310, 2002.]]

Digital Library

[3]

"Verification of Large Synthesized Designs", D. Brand, Proc. Intl. Conf. on Computer-Aided Design, pages 534--537, 1993.]]

Digital Library

[4]

"Graph-based algorithms for Boolean function manipulation", R.E. Bryant, IEEE Trans. on CAD, 1986.]]

[5]

"Robust Latch Mapping for Combinational Equivalence Checking", J. R. Burch, V. Singhal, Proc. Intl. Conf. on Computer-Aided Design, pages 563--569, 1998.]]

Digital Library

[6]

"Tight Integration of Combinational Verification Methods", J. R. Burch, V. Singhal, Proc. Intl. Conf. on Computer-Aided Design, pages 570--576, 1998.]]

Digital Library

[7]

"Apparatus and method for deriving correspondence between storage elements of a first circuit model and storage elements of a second circuit model", H. Cho, C. Pixley, U. S. Patent 5,638,381, June 1997.]]

[8]

"Equivalence Checking Using Cuts and Heaps", A. Kuehlman, F. Krohm,. Proc. Design Automation Conf., pages 263--268, 1997.]]

Digital Library

[9]

"An Efficient Equivalence Checker for Combinational Circuits", Y. Matsunaga, Proc. Design Automation Conf., pages 629--634, 1996.]]

Digital Library

[10]

"Hierarchical Verification for Equivalence Checking of Designs", L. McIlwain, D. Anastasakis, S. Pilarski, U.S. Patent 6,668,362, December, 2003.]]

[11]

"CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination", J. Moondanos, Carl Seger, Ziyad Hanna, Daher Kaiss, 13th Conf. on Computer-Aided Verification, Jul. 2001.]]

Digital Library

[12]

"An Efficient Filter-based Approach for Combinational Verification", R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. A. Abraham, D. S. Fussell, IEEE Trans. On CAD, pages 1542--1557, 1999.]]

[13]

"A Verification Algorithm for Logic Circuits with Internal Variables", T. Nakaoka, S. Wakabayashi, T. Koide, N. Yoshida, ISCAS 1995, pages 1920--1923.]]

[14]

"Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment," S. M. Reddy, W. Kunz and D. K. Pradhan, Proc. Design Automation Conf., pp. 414--419, 1995.]]

Digital Library

[15]

"Circuit synthesis verification method and apparatus", T. Stanion, U. S. Patent 6,056,784, May 2000.]]

[16]

"Equivalence Checking of Hierarchical Combinational Circuits", P. F. Williams, H. Hulgaard, H.R. Andersen, 6th IEEE Intl. Conf. Electronics, Circuits and Systems, Sep. 1999.]]

Cited By

Wu GXu YWu DRagupathy MMo YChu C(2016)Flip-flop clustering by weighted K-means algorithmProceedings of the 53rd Annual Design Automation Conference10.1145/2897937.2898025(1-6)Online publication date: 5-Jun-2016
https://dl.acm.org/doi/10.1145/2897937.2898025
Wu GSun YJiang J(2016)Design partitioning for large-scale equivalence checking and functional correctionProceedings of the 53rd Annual Design Automation Conference10.1145/2897937.2898004(1-6)Online publication date: 5-Jun-2016
https://dl.acm.org/doi/10.1145/2897937.2898004
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

Efficient equivalence checking with partitions and hierarchical cut-points
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking
ICST '09: Proceedings of the 2009 International Conference on Software Testing Verification and Validation

Bounded model checking---as well as symbolic equivalence checking---are highly successful techniques in the hardware domain. Recently, bit-vector bounded model checkers like CBMC have been developed that are able to check properties of (mostly low-level)...
Semantic program alignment for equivalence checking
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

We introduce a robust semantics-driven technique for program equivalence checking. Given two functions we find a trace alignment over a set of concrete executions of both programs and construct a product program particularly amenable to checking ...
Using complete-1-distinguishability for FSM equivalence checking

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '04: Proceedings of the 41st annual Design Automation Conference

June 2004

1002 pages

ISBN:1581138288

DOI:10.1145/996566

General Chair:
Sharad Malik
Princeton University, Princeton, NJ
,
Program Chairs:
Limor Fix
Intel Semiconductors Ltd., Haifa, Israel
,
Andrew B. Kahng
University of California at San Diego, La Jolla, CA

Copyright © 2004 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 June 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC04

Sponsor:

DAC04: The 41st Annual Design Automation Conference 2004

June 7 - 11, 2004

CA, San Diego, 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

4
Total Citations
View Citations
277
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wu GXu YWu DRagupathy MMo YChu C(2016)Flip-flop clustering by weighted K-means algorithmProceedings of the 53rd Annual Design Automation Conference10.1145/2897937.2898025(1-6)Online publication date: 5-Jun-2016
https://dl.acm.org/doi/10.1145/2897937.2898025
Wu GSun YJiang J(2016)Design partitioning for large-scale equivalence checking and functional correctionProceedings of the 53rd Annual Design Automation Conference10.1145/2897937.2898004(1-6)Online publication date: 5-Jun-2016
https://dl.acm.org/doi/10.1145/2897937.2898004
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
Mony HBaumgartner JParuthi VKanzelman RJoyner WMartin GKahng A(2005)Exploiting suspected redundancy without proving itProceedings of the 42nd annual Design Automation Conference10.1145/1065579.1065700(463-466)Online publication date: 13-Jun-2005
https://dl.acm.org/doi/10.1145/1065579.1065700

View Options

Get Access

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents