research-article

Using unsatisfiable cores to debug multiple design errors

Authors:

Andre Suelflow,

Goerschwin Fey,

Roderick Bloem,

Rolf DrechslerAuthors Info & Claims

GLSVLSI '08: Proceedings of the 18th ACM Great Lakes symposium on VLSI

Pages 77 - 82

https://doi.org/10.1145/1366110.1366131

Published: 04 May 2008 Publication History

Abstract

Due to the increasing complexity of today's circuits a high degree of automation in the design process is mandatory. The detection of faults and design errors is supported quite well using simulation or formal verification. But locating the fault site is typically a time consuming manual task. Techniques to automate debugging and diagnosis have been proposed. Approaches based on Boolean Satisfiability (SAT) have been demonstrated to be very effective. In this work debugging on the gate level is considered. Unsatisfiable cores contained in a SAT instance for debugging are used (1) to determine all suspects, and (2) to speed-up the debugging process. In comparison to standard SAT-based debugging, the experimental results show a significant speed-up for debugging multiple faults.

References

[1]

K. Chang, I. Markov, and V. Bertacco. Fixing design errors with counterexamples and resynthesis. In ASP Design Automation Conf., pages 944--949, 2007.

Digital Library

[2]

N. Eén and N. Sörensson. An extensible SAT solver. In SAT 2003, volume 2919 of LNCS, pages 502--518, 2004.

[3]

M. Fahim Ali, S. Safarpour, A. Veneris, M. Abadir, and R. Drechsler. Post--verification debugging of hierarchical designs. In Int'l Conf. on CAD, pages 871--876, 2005.

Digital Library

[4]

E. Goldberg and Y. Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe, pages 886--891, 2003.

Digital Library

[5]

D. W. Hoffmann and T. Kropf. Efficient design error correction of digital circuits. In Int'l Conf. on Comp. Design, pages 465--472, 2000.

Digital Library

[6]

J. Huang. MUP: A minimal unsatisfiability prover. In ASP Design Automation Conf., pages 432--437, 2005.

Digital Library

[7]

S.--Y. Huang. A fading algorithm for sequential fault diagnosis. In IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT), pages 139--147, 2004.

Digital Library

[8]

M. Liffiton and K. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. In Journal of Automated Reasoning, volume Online First. Springer Netherlands, 2007.

Digital Library

[9]

C.--C. Lin, K.--C. Chen, S.--C. Chang, M. Marek--Sadowska, and K.--T. Cheng. Logic synthesis for engineering change. In Design Automation Conf., pages 647--651, 1995.

Digital Library

[10]

J. Marques--Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Comp., 48(5):506--521, 1999.

Digital Library

[11]

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

Digital Library

[12]

Y. Oh, M. N. Mneimneh, Z. S. Andraus, K. A. Sakallah, and I. L. Markov. AMUSE: a minimally--unsatisfiable subformula extractor. In Design Automation Conf., pages 518--523, 2004.

Digital Library

[13]

R. Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32:57--95, 1987.

Digital Library

[14]

O. Shacham and K. Yorav. On--the--fly resolve trace minimization. In Design Automation Conf., pages 594--599, 2007.

Digital Library

[15]

O. Shtrichman. Pruning techniques for the SAT--based bounded model checking problem. In CHARME, volume 2144 of LNCS, pages 58--70, 2001.

Digital Library

[16]

A. Smith, A. Veneris, M. Fahim Ali, and A.Viglas. Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. on CAD, 24(10):1606--1621, 2005.

Digital Library

[17]

S.Safarpour, M.Liffton, H.Mangassarian, A.Veneris, and K.A.Sakallah. Improved design debugging using maximum satisfiability. In Int'l Conf. on Formal Methods in CAD, 2007.

Digital Library

[18]

S. Staber, G. Fey, R. Bloem, and R. Drechsler. Automatic fault localization for property checking. In Haifa Verification Conference, volume 4383 of LNCS, pages 50--64. Springer, 2006.

Digital Library

[19]

A. Veneris and I. N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Trans. on CAD, 18(12):1803--1816, 1999.

Digital Library

[20]

J. Whittemore, J. Kim, and K. Sakallah. SATIRE: A new incremental satisfiability engine. In Design Automation Conf., pages 542--545, 2001.

Digital Library

[21]

L. Zhang and S. Malik. Validating SAT solvers using an independent resolution--based checker: Practical implementations and other applications. In Design, Automation and Test in Europe, pages 880--885, 2003.

Digital Library

Cited By

Vick CKang ETripakis S(2023)Counterexample classificationSoftware and Systems Modeling10.1007/s10270-023-01118-023:2(455-472)Online publication date: 26-Jul-2023
https://doi.org/10.1007/s10270-023-01118-0
Srinivasan SVemuri R(2022)Model Checking Leveraged Error Localization for Complex RTL Designs2022 IEEE 40th International Conference on Computer Design (ICCD)10.1109/ICCD56317.2022.00092(585-592)Online publication date: Oct-2022
https://doi.org/10.1109/ICCD56317.2022.00092
Bjørner NLevatich MLopes NRybalchenko AVuppalapati C(2021)Supercharging Plant Configurations Using Z3Integration of Constraint Programming, Artificial Intelligence, and Operations Research10.1007/978-3-030-78230-6_1(1-25)Online publication date: 17-Jun-2021
https://doi.org/10.1007/978-3-030-78230-6_1
Show More Cited By

Index Terms

Using unsatisfiable cores to debug multiple design errors
1. Hardware
  1. Integrated circuits
    1. Logic circuits

Recommendations

An approach for extracting a small unsatisfiable core

The article addresses the problem of finding a small unsatisfiable core of an unsatisfiable CNF formula. The proposed algorithm, CoreTrimmer , iterates over each internal node d in the resolution graph that `consumes' a large number of clauses M (...
A heuristic local search algorithm for unsatisfiable cores extraction
ICCSA'07: Proceedings of the 2007 international conference on Computational science and its applications - Volume Part III

Explaining the causes of infeasibility of Boolean formulas has many practical applications in various fields. We are generally interested in a small explanation of unsatisfiability that excludes irrelevant information. A small unsatisfiable core ...
Algorithms for maximum satisfiability using unsatisfiable cores
DATE '08: Proceedings of the conference on Design, automation and test in Europe

Many decision and optimization problems in Electronic Design Automation (EDA) can be solved with Boolean Satisfiability (SAT). Moreover, well-known extensions of SAT also find application in EDA, including Pseudo-Boolean Optimization, Quantified Boolean ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

GLSVLSI '08: Proceedings of the 18th ACM Great Lakes symposium on VLSI

May 2008

480 pages

ISBN:9781595939999

DOI:10.1145/1366110

General Chairs:
Vijay Narayanan
Penn State University
,
Zhiyuan Yan
Lehigh University
,
Program Chairs:
Enrico Macii
Politecnico di Torino
,
Sanjukta Bhanja
University of South Florida

Copyright © 2008 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: 04 May 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

GLSVLSI08

Sponsor:

GLSVLSI08: Great Lakes Symposium on VLSI 2008

May 4 - 6, 2008

Florida, Orlando, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

40
Total Citations
View Citations
231
Total Downloads

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

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vick CKang ETripakis S(2023)Counterexample classificationSoftware and Systems Modeling10.1007/s10270-023-01118-023:2(455-472)Online publication date: 26-Jul-2023
https://doi.org/10.1007/s10270-023-01118-0
Srinivasan SVemuri R(2022)Model Checking Leveraged Error Localization for Complex RTL Designs2022 IEEE 40th International Conference on Computer Design (ICCD)10.1109/ICCD56317.2022.00092(585-592)Online publication date: Oct-2022
https://doi.org/10.1109/ICCD56317.2022.00092
Bjørner NLevatich MLopes NRybalchenko AVuppalapati C(2021)Supercharging Plant Configurations Using Z3Integration of Constraint Programming, Artificial Intelligence, and Operations Research10.1007/978-3-030-78230-6_1(1-25)Online publication date: 17-Jun-2021
https://doi.org/10.1007/978-3-030-78230-6_1
Veira NPoulos ZVeneris A(2020)Searching for Bugs using Probabilistic Suspect ImplicationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.2966448(1-1)Online publication date: 2020
https://doi.org/10.1109/TCAD.2020.2966448
Berryhill RVeneris A(2019)Chasing Minimal Inductive Validity Cores in Hardware Model Checking2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894268(19-27)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894268
Kumar BFujita MSingh V(2019)A Methodology for SAT-Based Electrical Error Debugging During Post-Silicon Validation2019 32nd International Conference on VLSI Design and 2019 18th International Conference on Embedded Systems (VLSID)10.1109/VLSID.2019.00085(389-394)Online publication date: Jan-2019
https://doi.org/10.1109/VLSID.2019.00085
Gaber LHussein AMoness M(2019)Improved Automatic Correction for Digital VLSI Circuits2019 31st International Conference on Microelectronics (ICM)10.1109/ICM48031.2019.9021938(18-22)Online publication date: Dec-2019
https://doi.org/10.1109/ICM48031.2019.9021938
Kumar BFujita MSingh V(2019)SAT-based Silicon Debug of Electrical Errors under Restricted Observability EnhancementJournal of Electronic Testing10.1007/s10836-019-05830-yOnline publication date: 19-Nov-2019
https://doi.org/10.1007/s10836-019-05830-y
Vali ANicolici N(2018)Bit-Flip Detection-Driven Selection of Trace SignalsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2017.272945837:5(1076-1089)Online publication date: May-2018
https://doi.org/10.1109/TCAD.2017.2729458
Weissenbacher GMalik S(2018)Post-Silicon Fault Localization with Satisfiability SolversPost-Silicon Validation and Debug10.1007/978-3-319-98116-1_13(255-273)Online publication date: 2-Sep-2018
https://doi.org/10.1007/978-3-319-98116-1_13
Show More Cited By

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