Article

On equivalence checking and logic synthesis of circuits with a common specification

Author:

Eugene GoldbergAuthors Info & Claims

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

Pages 102 - 107

https://doi.org/10.1145/1057661.1057687

Published: 17 April 2005 Publication History

Get Access

Abstract

In this paper we develop a theory of equivalence checking (EC) and logic synthesis of circuits with a common specification (CS). We show that two combinational circuits N₁ N₂ have a CS iff they can be partitioned into subcircuits that are connected "in the same way" and are toggle equivalent. This fact allows one to represent a specification of a circuit implicitly as a partitioning into subcircuits. We give an efficient procedure for checking if circuits N₁, N₂ have the same predefined specification. As a "by-product", this procedure performs EC of N₁ and N₂. We show how, given a circuit N₁ with a predefined specification, one can efficiently build a circuit N₂ satisfying the same specification. We give experimental evidence that EC of N₁ N₂ is hard if their CS is unknown.

References

[1]

Berman,C.L., and Trevillyan,L.H. Functional comparison of logic designs for VLSI circuits. ICCAD-89, pp.456--459.

Google Scholar

[2]

Brand,D. Verification of large synthesized designs. ICCAD-93, pp.534--537.

Digital Library

Google Scholar

[3]

Burch, J.R., and Singhal,V. Tight integration of combi-national verification methods. ICCAD-98, pp.570--576.

Digital Library

Google Scholar

[4]

Goldberg, E. Equivalence Checking of Dissimilar Circuits II. Technical report. CDNL-TR-2004-0830, August 2004, available at http://eigold.tripod.com/papers.html

Google Scholar

[5]

Goldberg, E. Equivalence checking and logic synthesis of circuits with a common specification. Technical report. CDNL-TR-2004--1220, August 2004.

Google Scholar

[6]

Goldberg, E., and Novikov, Y. Equivalence Checking of Dissimilar Circuits, IWLS-2003. May 28-30, USA. Available at http://eigold.tripod.com/papers/dissim-iwls.zip

Google Scholar

[7]

van Eijk, C. and Janssen, G. Exploiting structural similarities in a BDD-based verification method. Proceedings of 2nd International Conference on Theorem Provers in Circuit Design, pp. 110--125, 1995.

Digital Library

Google Scholar

[8]

Kuehlmann, A. and Krohm, F. Equivalence checking using cuts and heaps, DAC-98, pp.263--268.

Digital Library

Google Scholar

Cited By

View all

Goldberg EGulati K(2007)On Complexity of Internal and External Equivalence Checking10th Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD 2007)10.1109/DSD.2007.4341469(197-206)Online publication date: Aug-2007
https://doi.org/10.1109/DSD.2007.4341469
Andrade FOliveira MFernandes ACoelho C(2007)SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse2007 IEEE Design and Diagnostics of Electronic Circuits and Systems10.1109/DDECS.2007.4295319(1-6)Online publication date: Apr-2007
https://doi.org/10.1109/DDECS.2007.4295319

Index Terms

On equivalence checking and logic synthesis of circuits with a common specification
1. Hardware
  1. Electronic design automation
    1. High-level and register-transfer level synthesis
    2. Logic synthesis
      1. Circuit optimization
  2. Hardware validation
    1. Functional verification

Recommendations

Equivalence Checking for Superconducting RSFQ Logic Circuits
GLSVLSI '21: Proceedings of the 2021 Great Lakes Symposium on VLSI

Equivalence checking is a key component of the verification methodology for digital circuit designs. In this paper, we propose an equivalence checking framework for superconducting rapid single-flux-quantum (RSFQ) logic circuits which include acyclic ...
Synthesis of skewed logic circuits

Skewed logic circuits belong to a noise-tolerant high-performance static circuit family. Skewed logic circuits can achieve performance comparable to that of Domino logic circuits but with much lower power consumption. Two factors contribute to the ...
Checking Combinational Equivalence of Speed-Independent Circuits

We introduce the notion of combinational equivalence to relate two speed-independent asynchronous (sequential) circuits: a golden hazard-free circuit C_1 and a target circuit C_2 that can be derived from C_1 through only combinational decomposition and ...

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

2
Total Citations
View Citations
156
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Goldberg EGulati K(2007)On Complexity of Internal and External Equivalence Checking10th Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD 2007)10.1109/DSD.2007.4341469(197-206)Online publication date: Aug-2007
https://doi.org/10.1109/DSD.2007.4341469
Andrade FOliveira MFernandes ACoelho C(2007)SAT-Based Equivalence Checking Based on Circuit Partitioning and Special Approaches for Conflict Clause Reuse2007 IEEE Design and Diagnostics of Electronic Circuits and Systems10.1109/DDECS.2007.4295319(1-6)Online publication date: Apr-2007
https://doi.org/10.1109/DDECS.2007.4295319

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

Equivalence Checking for Superconducting RSFQ Logic Circuits

Synthesis of skewed logic circuits

Checking Combinational Equivalence of Speed-Independent Circuits

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