Article

Mining global constraints for improving bounded sequential equivalence checking

Authors:

Michael S. HsiaoAuthors Info & Claims

DAC '06: Proceedings of the 43rd annual Design Automation Conference

Pages 743 - 748

https://doi.org/10.1145/1146909.1147098

Published: 24 July 2006 Publication History

Abstract

In this paper, we propose a novel technique on mining relationships in a sequential circuit to discover global constraints. In contrast to the traditional learning methods, our mining algorithm can find important relationships among several nodes efficiently. The nodes involved may often span several time-frames, thus improving the deductibility of the problem instance. Experimental results demonstrate that the application of these global constraints to SAT-based bounded sequential equivalence checking can achieve one to two orders of magnitude speedup. In addition, because it is orthogonal to the underlying SAT solver, it can help to enhance the efficacy of typical SAT based verification flows.

References

[1]

M. H. Schulz, E. Trischler and T. M. Sarfert. SOCRATES: A highly efficient automatic test pattern generation system. IEEE Trans. CAD, vol. 7, no. 1, Jan. 1988, pp. 126--137.

Digital Library

[2]

W. Kunz and D. K. Pradhan. Accelerated dynamic learning for test pattern generation in combinational circuits. IEEE Trans. CAD, vol. 12, no. 5, May 1993, pp. 684--694.

Digital Library

[3]

H. Ichihara and K. Kinoshita. On acceleration of logic circuits optimization using implication relations. In Proc. Asian Test Symp., 1997, pp. 222--227.

Digital Library

[4]

W. Kunz, D. Stoffel and P. R. Menon. Logic optimization and equivalence checking by implication analysis. IEEE Trans. CAD, Vol. 16, no. 3, Mar. 1997, pp.266--281.

Digital Library

[5]

S. Kajihara, K. K. Saluja and S. M. Reddy. Enhanced 3-valued logic/fault simulation for full scan circuits using implicit logic values. Proc. European Test Symp., 2004, pp. 108--113.

Digital Library

[6]

M. E. Amyeen, W. K. Fuch, I. Pomeranz and V. Boppana. Implication and evaluation techniques for proving fault equivalence. Proc. VLSI Test Symp., 1999, pp. 201--207.

Digital Library

[7]

W. Kunz, D. Pradhan and S. Reddy. A Novel Framework for Logic Verification in a Synthesis Environment. IEEE Trans. CAD, vol. 15, no. 1, Jan. 1996, pp. 20--32.

Digital Library

[8]

M. lyer and M. Abramovici. FIRE: A Fault-independent Combinational Redundancy Identification Algorithm. IEEE Trans. VLSI Systems., vol. 4, no. 2, Jun. 1996, pp. 295--301.

Digital Library

[9]

J. K. Zhao, M. Rudnick and J. Patel. Static Logic Implication with Application to Fast Redundancy Identification. Proc. VLSI Test Symp., 1997, pp. 288--293.

Digital Library

[10]

M. H. Schulz and E. Auth. Improved deterministic test pattern generation with applications to redundancy identification. IEEE Trans. CAD, vol. 8, no. 7, Jul. 1989, pp. 811--816.

Digital Library

[11]

Y. Novikov. Local search for Boolean relations on the basis of unit propagation, Proc. Design, Automation and Test in Europe Conf., 2003, pp. 810--815.

Digital Library

[12]

J. Rajski and H. Kox. A Method to Calculate Necessary Assignments in ATPG. Proc. Int'l. Test Conf., 1990, pp. 25--34.

[13]

S.T. Chakradhar and V. D. Agrawal. A transitive closure algorithm for test generation. IEEE Trans. CAD., 1993, pp. 1015 -- 1028.

Digital Library

[14]

W. Kunz and D. K. Pradhan. Recursive Learning: A new Implication Technique for Efficient Solutions to CAD problems test, verification, and optimization. IEEE Trans. CAD., 1993, pp.1149--1158.

[15]

J. Zhao, J. A. Newquist and J. Patel. A graph traversal based framework for sequential logic implication with an application to c-cycle redundancy identification. Proc. VLSI Design Conf., 2001, pp. 163--169.

Digital Library

[16]

K. Gulrajani and M. S. Hsiao. Multi-node static logic implications for redundancy identification. Proc. Design, Automation, and Test in Europe Conf., 2000, pp. 729--733.

Digital Library

[17]

M. Syal, R. Arora and M. S. Hsiao. Extended forward implications and dual recurrence relations to identify sequentially untestable faults. Proc. Int'l Conf. Computer Design, 2005, pp. 453--460.

Digital Library

[18]

D. J. Hand, H. Mannila and P. Smyth. Principles of Data Mining. MIT Press, Aug. 2001.

Digital Library

[19]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita and Y. Zhu Symbolic model checking using SAT procedures instead of BDDs. Proc. Design Automation Conf., 1999, pp. 317--320.

Digital Library

[20]

A. Kuehlmann. Dynamic Transition Relation Simplification for Bounded Property Checking. Proc. Int. Conf. Computer-Aided Design., 2004, pp. 50--57.

Digital Library

[21]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik. Chaff: Engineering an efficient SAT solver. Proc. Design Automation Conf., 2001, pp. 530--535.

Digital Library

[22]

E. Goldberg and Y. Novikov. BerkMin: A fast and robust Sat Solver. Proc. European Design and Test Conf., 2002, pp. 142--149.

Digital Library

[23]

F. Lu, L. C. Wang and K. T. Cheng. A circuit SAT solver with signal correlation guided learning. Proc. European Design and Test Conf., 2003, pp. 892--897.

Digital Library

[24]

R. Agrawal, T. Imielinski and A. Swami. Mining association rules between sets of items in large databases. Proc. Conf. Management of Data, 1993, pp. 207--216.

Digital Library

[25]

R. Agrawal, T. Imielinski and A. Swami. Database mining: A performance perspective. IEEE Trans. Knowledge and Data Engineering, vol. 5, No. 6, 1993, pp. 914--925.

Digital Library

Cited By

Mukherjee RJoshi SGriesmayer AKroening DMelham T(2016)Equivalence Checking of a Floating-Point Unit Against a High-Level C ModelFM 2016: Formal Methods10.1007/978-3-319-48989-6_33(551-558)Online publication date: 8-Nov-2016
https://doi.org/10.1007/978-3-319-48989-6_33
Mukherjee RKroening DMelham TSrivas M(2015)Equivalence Checking Using Trace Partitioning2015 IEEE Computer Society Annual Symposium on VLSI10.1109/ISVLSI.2015.110(13-18)Online publication date: Jul-2015
https://doi.org/10.1109/ISVLSI.2015.110
Nguyen HHsiao M(2012)Sequential equivalence checking of hard instances with targeted inductive invariants and efficient filtering strategies2012 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2012.6418236(1-8)Online publication date: Nov-2012
https://doi.org/10.1109/HLDVT.2012.6418236
Show More Cited By

Index Terms

Mining global constraints for improving bounded sequential equivalence checking
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Mining Global Constraints With Domain Knowledge for Improving Bounded Sequential Equivalence Checking

We present a novel technique on mining relationships in a sequential circuit to discover global constraints. We utilize domain knowledge to prune the search space for our mining process, via which the mined relations may often span several time frames, ...
Improving SAT using 2SAT

Propositional satisfiability (SAT) is a fundamental problem of immense practical importance. While SAT is NP-complete when clauses can contain 3 literals or more, the problem can be solved in linear time when the given formula contains only binary ...
Improving SAT using 2SAT
ACSC '02: Proceedings of the twenty-fifth Australasian conference on Computer science - Volume 4

Propositional satisfiability (SAT) is a fundamental problem of immense practical importance. While SAT is NP-complete when clauses can contain 3 literals or more, the problem can be solved in linear time when the given formula contains only binary ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '06: Proceedings of the 43rd annual Design Automation Conference

July 2006

1166 pages

ISBN:1595933816

DOI:10.1145/1146909

General Chair:
Ellen M. Sentovich
Cadence Berkeley Labs, Berkeley, CA

Copyright © 2006 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: 24 July 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC06

Sponsor:

DAC06: The 43rd Annual Design Automation Conference 2006

July 24 - 28, 2006

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

13
Total Citations
View Citations
256
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mukherjee RJoshi SGriesmayer AKroening DMelham T(2016)Equivalence Checking of a Floating-Point Unit Against a High-Level C ModelFM 2016: Formal Methods10.1007/978-3-319-48989-6_33(551-558)Online publication date: 8-Nov-2016
https://doi.org/10.1007/978-3-319-48989-6_33
Mukherjee RKroening DMelham TSrivas M(2015)Equivalence Checking Using Trace Partitioning2015 IEEE Computer Society Annual Symposium on VLSI10.1109/ISVLSI.2015.110(13-18)Online publication date: Jul-2015
https://doi.org/10.1109/ISVLSI.2015.110
Nguyen HHsiao M(2012)Sequential equivalence checking of hard instances with targeted inductive invariants and efficient filtering strategies2012 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2012.6418236(1-8)Online publication date: Nov-2012
https://doi.org/10.1109/HLDVT.2012.6418236
Goel NHsiao MRamakrishnan NZaki M(2010)Mining Complex Boolean Expressions for Sequential Equivalence CheckingProceedings of the 2010 19th IEEE Asian Test Symposium10.1109/ATS.2010.81(442-447)Online publication date: 1-Dec-2010
https://dl.acm.org/doi/10.1109/ATS.2010.81
Chang CWen CBhadra J(2009)Speeding up bounded sequential equivalence checking with cross-timeframe state-pair constraints from data learning2009 International Test Conference10.1109/TEST.2009.5355713(1-8)Online publication date: Nov-2009
https://doi.org/10.1109/TEST.2009.5355713
Cheng XHsiao MSciuto D(2008)Simulation-directed invariant mining for software verificationProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403541(682-687)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403541
Weixin Wu Hsiao M(2008)SAT-based State Justification with Adaptive Mining of Invariants2008 IEEE International Test Conference10.1109/TEST.2008.4700567(1-10)Online publication date: Oct-2008
https://doi.org/10.1109/TEST.2008.4700567
Wu WHsiao M(2008)Mining Global Constraints With Domain Knowledge for Improving Bounded Sequential Equivalence CheckingIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2007.90724027:1(197-201)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.1109/TCAD.2007.907240
Chang LWen C(2008)Mining Unreachable Cross-Timeframe State-Pairs for Bounded Sequential Equivalence CheckingProceedings of the 2008 Ninth International Workshop on Microprocessor Test and Verification10.1109/MTV.2008.23(33-38)Online publication date: 8-Dec-2008
https://dl.acm.org/doi/10.1109/MTV.2008.23
Cheng XHsiao M(2008)Simulation-Directed Invariant Mining for Software Verification2008 Design, Automation and Test in Europe10.1109/DATE.2008.4484757(682-687)Online publication date: Mar-2008
https://doi.org/10.1109/DATE.2008.4484757
Show More Cited By

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.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten