Article

An effective and efficient ATPG-based combinational equivalence checker

Authors:

Ronald P. Lajaunie,

Michael S. HsiaoAuthors Info & Claims

GLSVLSI '05: Proceedings of the 15th ACM Great Lakes symposium on VLSI

Pages 248 - 253

https://doi.org/10.1145/1057661.1057722

Published: 17 April 2005 Publication History

Get Access

Abstract

An effective and efficient ATPG-based combinational equivalence checker.

References

[1]

R. Arora and M. Hsiao. Enhancing sat-based equivalence checking with static logic implications. In Proc. High-Level Design Validation and Test Workshop, pages 12--14, November 2003.

Digital Library

Google Scholar

[2]

C. Berman and L. Trevillyan. Functional comparison of logic designs for vlsi circuits. In Proc. International Conference on Computer-Aided Design, pages 456--459, November 1989.

Crossref

Google Scholar

[3]

D. Brand. Verification of large synthesized designs. In Proc. International Conference on Computer-Aided Design, pages 534--537, November 1993.

Digital Library

Google Scholar

[4]

R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677--691, August 1986.

Digital Library

Google Scholar

[5]

J. Burch and V. Singhal. Tight integration of combinational verification methods. In Proc. International Conference on Computer-Aided Design, pages 570--576, November 1998.

Digital Library

Google Scholar

[6]

P. Goel and B. Rosales. Podem-x: An automatic test generation system for vlsi logic structures. In Proc. Design Automation Conference, pages 260--268, June 1981.

Digital Library

Google Scholar

[7]

E. Goldberg and Y. Novikov. Berkmin: a fast and robust sat-solver. In Proc. Design, Automation and Test in Europe Conference, pages 142--149, March 2002.

Digital Library

Google Scholar

[8]

E. Goldberg, M. Prasad, and R. Brayton. Using sat for combinational equivalence checking. In Proc. Design, Automation and Test in Europe Conference, pages 114--121, March 2001.

Digital Library

Google Scholar

[9]

L. Goldstein and E. Thigpen. Scoap: Sandia controllability/observability analysis program. In Proc. Design Automation Conference, pages 190--196, June 1980.

Digital Library

Google Scholar

[10]

A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In Proc. Design Automation Conference, pages 263--268, June 1997.

Digital Library

Google Scholar

[11]

W. Kunz. Hannibal: An efficient tool for logic verification based on recursive learning. In Proc. International Conference on Computer-Aided Design, pages 538--543, November 1993.

Digital Library

Google Scholar

[12]

F. Lu, L. Wang, K. Cheng, and R. Huang. A circuit sat solver with signal correlation guided learning. In Proc. Design, Automation and Test in Europe Conference, pages 892--897, March 2003.

Digital Library

Google Scholar

[13]

J. P. Marques-Silva and K. A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506--521, May 1999.

Digital Library

Google Scholar

[14]

Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proc. Design Automation Conference, pages 629--634, June 1996.

Digital Library

Google Scholar

[15]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In Proc. Design Automation Conference, pages 629--634, June 2001.

Digital Library

Google Scholar

[16]

S. Reda and A. Salem. Combinational equivalence checking using boolean satisfiability and binary decision diagrams. In Proc. Design, Automation and Test in Europe Conference, pages 122--126, March 2001.

Digital Library

Google Scholar

[17]

S. Reda, A. Wahba, and A. Salem. M-check: A multiple engine combinational equivalence checker. In Proc. International Symposium on Circuits and Systems, pages 613--616, May 2000.

Crossref

Google Scholar

[18]

S. Reddy, W. Kunz, and D. Pradhan. Novel verification framework combining structural and obdd methods in a synthesis environment. In Proc. Design Automation Conference, pages 414--419, June 1995.

Digital Library

Google Scholar

[19]

J. Roth. Diagnosis of automata failures: A calculus and a method. IBM Journal of Research and Development, 10:278--291, July 1996.

Digital Library

Google Scholar

[20]

E. Sentovich, K. Singh, C. Moon, H. Savoj, R. Brayton, and A. Sangiovanni-Vincentelli. Sequential circuit design using synthesis and optimization. In Proc. International Conference on Computer Design, pages 328--333, October 1992.

Digital Library

Google Scholar

[21]

C. Weng, S. Reddy, I. Pomeranz, X. Lin, and J.Rajski. Conflict driven techniques for improving deterministic test pattern generation. In Proc. International Conference on Computer-Aided Design, pages 87--93, November 2002.

Digital Library

Google Scholar

Cited By

View all

Fugate JStitt GMasna NDasgupta ABhunia SDorairaj NKehlet D(2023)An Exploration of ATPG Methods for Redacted IP and Reconfigurable Hardware2023 IEEE 41st VLSI Test Symposium (VTS)10.1109/VTS56346.2023.10139957(1-7)Online publication date: 24-Apr-2023
https://doi.org/10.1109/VTS56346.2023.10139957

Index Terms

An effective and efficient ATPG-based combinational equivalence checker
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)...
An Efficient Logic Equivalence Checker for Industrial Circuits
Special issue on microprocessor test and verification

We present our formal combinational logic equivalence checking methods for industry-sized circuits. Our methods employ functional (OBDDs) algorithms for decisions on logic equivalence and structural (ATPG) algorithms to quickly identify inequivalence. The ...
Formal Verification ATPG Search Engine Emulator (Abstract Only)
FPGA '15: Proceedings of the 2015 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays

Bounded Model Checking (BMC), as a formal method of verifying VLSI circuits, shows violation of a given circuit property by finding a counter-example to the property along bounded state paths of the circuit. In this paper, we present an emulation ...

Comments

Information & Contributors

Information

Published In

GLSVLSI '05: Proceedings of the 15th ACM Great Lakes symposium on VLSI

April 2005

518 pages

ISBN:1595930574

DOI:10.1145/1057661

General Chair:
John Lach
University of Virginia
,
Program Chairs:
Gang Qu
University of Maryland, College Park
,
Yehea Ismail
Northwestern University

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: 17 April 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

GLSVLSI05

Sponsor:

GLSVLSI05: Great Lakes Symposium on VLSI 2005

April 17 - 19, 2005

Illinois, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 312 of 1,156 submissions, 27%

Upcoming Conference

GLSVLSI '25

Sponsor:
sigda

Great Lakes Symposium on VLSI 2025

June 30 - July 2, 2025

New Orleans , LA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
276
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Fugate JStitt GMasna NDasgupta ABhunia SDorairaj NKehlet D(2023)An Exploration of ATPG Methods for Redacted IP and Reconfigurable Hardware2023 IEEE 41st VLSI Test Symposium (VTS)10.1109/VTS56346.2023.10139957(1-7)Online publication date: 24-Apr-2023
https://doi.org/10.1109/VTS56346.2023.10139957

View Options

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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking

An Efficient Logic Equivalence Checker for Industrial Circuits

Formal Verification ATPG Search Engine Emulator (Abstract Only)

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations