Article

Free access

Tight integration of combinational verification methods

Authors:

Jerry R. Burch,

Vigyan SinghalAuthors Info & Claims

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

Pages 570 - 576

https://doi.org/10.1145/288548.289088

Published: 01 November 1998 Publication History

PDF eReader

References

[1]

C. L. Berman and L. H. Trevillyan. Functional Comparison of Logic Designs for VLSI Circuits. In Proc. Intl. Conf. on Computer-Aided Design, pages 456-459, 1989.

Crossref

Google Scholar

[2]

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

Digital Library

Google Scholar

[3]

R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35:677- 691, August 1986.

Digital Library

Google Scholar

[4]

J. Gu, P. W. Purdom, j. V. Franco, and B. W. Wah. Algorithms for the Satisfiability (SAT) Problem: A Survey. In D. Du, J. Gu, and P. M. Pardalos, editors, Satisfiability Problems: Theory and Applications. American Mathematical Society, 1997.

Google Scholar

[5]

A. Gupta and P. Ashar. Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. In Proc. Intl. Conf. on VLSI Design, pages 222-225, Chennai, India, 1998.

Digital Library

Google Scholar

[6]

J. Jain, R. Mukherjee, and M. Fujita. Advanced Verification Techniques Based on Learning. In Proc. Design Automation Conf., pages 420-426, 1995.

Digital Library

Google Scholar

[7]

A. Kuehlmann and F. Krohm. Equivalence Checking using Cuts and Heaps. In Proc. Design Automation Conf., pages 263-268, 1997.

Digital Library

Google Scholar

[8]

W. Kunz, D. K. Pradhan, and S. Reddy. A Novel Framework for Logic Verification in a Synthesis Environment. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 15(I):20-36, January 1996.

Digital Library

Google Scholar

[9]

David E. Long. BDD Manipulation Library. Public software. Carnegie Mellon University, Pittsburgh, PA, June 1993. ftp : / / emc. cs. cmu. edu/pub/bdd/bddlib, tar. Z.

Google Scholar

[10]

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

Digital Library

Google Scholar

[11]

R. Mu "kherjee, J. Jain, K. Takayama, M. Fujita, J. A. Abraham, and D. S. Fussell. FLOVER: Flitering Oriented Combinational Verification Approach. In Workshop Notes of International Workshop on Logic Synthesis, Tahoe City, CA, 1997.

Google Scholar

[12]

D. K. Pradhan, D. Paul, and M. Chatterjee. VERILAT: Verification Using Logic Augmentation and Transformations. in Proc. Intl. Conf. on Computer-Aided Design, pages 88-95, 1996.

Digital Library

Google Scholar

[13]

B. Selman, H. Leveque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proc. of AAAI, pages 440--446, 1992.

Google Scholar

[14]

E.M. Sentovich, K. J. Singh, C. Moon, H. Savoj, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Sequential Circuit Design Using Synthesis and Optimization. In Proc. intl. Conf. on Computer Design, pages 328--333, Cambridge, MA, October 1992.

Digital Library

Google Scholar

[15]

C.A.J. van Eijk. Formal Methods for the Verification of Digital Circuits. PhD thesis, Eindhoven University of Technology, Dept. of Electrical Engineering, Eindhoven, Netherlands, 1997.

Google Scholar

Cited By

View all

Kuehlmann ASomenzi FHsu CBustan D(2016)Equivalence CheckingElectronic Design Automation for IC Implementation, Circuit Design, and Process Technology10.1201/b19714-6(77-108)Online publication date: 14-Apr-2016
https://doi.org/10.1201/b19714-6
Fedyukovich GGurfinkel ASharygina N(2016)Property Directed Equivalence via Abstract SimulationComputer Aided Verification10.1007/978-3-319-41540-6_24(433-453)Online publication date: 13-Jul-2016
https://doi.org/10.1007/978-3-319-41540-6_24
Li LThornton M(2010)Digital System Verification: A Combined Formal Methods and Simulation FrameworkSynthesis Lectures on Digital Circuits and Systems10.2200/S00257ED1V01Y201002DCS0275:1(1-93)Online publication date: Jan-2010
https://doi.org/10.2200/S00257ED1V01Y201002DCS027
Show More Cited By

Index Terms

Tight integration of combinational verification methods

Recommendations

Formal Verification of Combinational Circuit
VLSID '97: Proceedings of the Tenth International Conference on VLSI Design: VLSI in Multimedia Applications

With the increase in the complexity of present day systems, proving the correctness of a design has become a major concern. Simulation based methodologies are generally inadequate to validate the correctness of a design with a reasonable confidence. ...
Quaternary CMOS Combinational Logic Circuits
ICIMT '09: Proceedings of the 2009 International Conference on Information and Multimedia Technology

Good Characteristics and advantages of multi-valued logic (MVL) electronic systems and circuits are created great interest for its practical implementation. This paper presents voltage mode quaternary CMOS circuit design using 90nm technology. Basic ...
A Library for Combinational Circuit Verification Using the HOL Theorem Prover

Interactive theorem provers can overcome the scalability limitations of model checking and automated theorem provers by verifying generic circuits and universally quantified properties but they require explicit user guidance, which makes them quite ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

November 1998

704 pages

ISBN:1581130082

DOI:10.1145/288548

Chairman:
Hiroto Yasuura
Kyushu Univ., Fukuoka, Japan

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: 01 November 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICCAD '98

Sponsor:

IEEE-EDS
SIGDA
IEEE-CAS
IEEE-CS

ICCAD '98: International Conference on Computer-Aided Design - 1998

November 8 - 12, 1998

California, San Jose, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
238
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kuehlmann ASomenzi FHsu CBustan D(2016)Equivalence CheckingElectronic Design Automation for IC Implementation, Circuit Design, and Process Technology10.1201/b19714-6(77-108)Online publication date: 14-Apr-2016
https://doi.org/10.1201/b19714-6
Fedyukovich GGurfinkel ASharygina N(2016)Property Directed Equivalence via Abstract SimulationComputer Aided Verification10.1007/978-3-319-41540-6_24(433-453)Online publication date: 13-Jul-2016
https://doi.org/10.1007/978-3-319-41540-6_24
Li LThornton M(2010)Digital System Verification: A Combined Formal Methods and Simulation FrameworkSynthesis Lectures on Digital Circuits and Systems10.2200/S00257ED1V01Y201002DCS0275:1(1-93)Online publication date: Jan-2010
https://doi.org/10.2200/S00257ED1V01Y201002DCS027
Goldberg ENovikov Y(2008)BerkMin: A Fast and Robust Sat-SolverDesign, Automation, and Test in Europe10.1007/978-1-4020-6488-3_34(465-478)Online publication date: 2008
https://doi.org/10.1007/978-1-4020-6488-3_34
Lajaunie RHsiao MLach JQu GIsmail Y(2005)An effective and efficient ATPG-based combinational equivalence checkerProceedings of the 15th ACM Great Lakes symposium on VLSI10.1145/1057661.1057722(248-253)Online publication date: 17-Apr-2005
https://dl.acm.org/doi/10.1145/1057661.1057722
Goldberg ELach JQu GIsmail Y(2005)On equivalence checking and logic synthesis of circuits with a common specificationProceedings of the 15th ACM Great Lakes symposium on VLSI10.1145/1057661.1057687(102-107)Online publication date: 17-Apr-2005
https://dl.acm.org/doi/10.1145/1057661.1057687
Li XLi GShao M(2005)Formal Verification Techniques Based on Boolean Satisfiability ProblemJournal of Computer Science and Technology10.1007/s11390-005-0004-620:1(38-47)Online publication date: Jan-2005
https://doi.org/10.1007/s11390-005-0004-6
Anastasakis DMcIlwain LPilarski SMalik SFix LKahng A(2004)Efficient equivalence checking with partitions and hierarchical cut-pointsProceedings of the 41st annual Design Automation Conference10.1145/996566.996714(539-542)Online publication date: 7-Jun-2004
https://dl.acm.org/doi/10.1145/996566.996714
Radecka KZilic Z(2004)Design Verification by Test Vectors and Arithmetic Transform Universal Test SetIEEE Transactions on Computers10.1109/TC.2004.127530153:5(628-640)Online publication date: 1-May-2004
https://dl.acm.org/doi/10.1109/TC.2004.1275301
Jin HSomenzi F(2004)CirCUsProceedings of the 7th international conference on Theory and Applications of Satisfiability Testing10.1007/11527695_17(211-223)Online publication date: 10-May-2004
https://dl.acm.org/doi/10.1007/11527695_17
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

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

Formal Verification of Combinational Circuit

Quaternary CMOS Combinational Logic Circuits

A Library for Combinational Circuit Verification Using the HOL Theorem Prover