Article

A new approach to the use of satisfiability in false path detection

Authors:

Felipe S. Marques,

Renato P. Ribas,

Sachin Sapatnekar,

André I. ReisAuthors Info & Claims

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

Pages 308 - 311

https://doi.org/10.1145/1057661.1057735

Published: 17 April 2005 Publication History

Get Access

Abstract

This paper presents a novel method for false path detection using satisfiability. It is based on circuit node properties that are related to non-testable stuck-at faults as well as to false path detection. When compared to traditional satisfiability methods that generate sat instances associated to paths, the proposed method is more efficient. This efficiency derives from the fact that most digital circuits have a number of nodes that is smaller than the number of paths.

References

[1]

Marques-Silva, P.J., and Sakallah, K.A., Boolean Satisfiability in Electronic Design Automation, Design Automation Conference, 2000, pp. 675--680.

Digital Library

Google Scholar

[2]

Larrabee, T., Test pattern generation using Boolean satisfiability, IEEE Transactions on CAD, Vol. 11, Issue: 1, January 1992, pp. 4--15.

Digital Library

Google Scholar

[3]

Ringe, M., Lindenkreuz, T., and Barke, E., Path verification using Boolean satisfiability, Design, Automation and Test in Europe, Feb. 1998, pp. 965--966.

Digital Library

Google Scholar

[4]

Brayton, R.K., Hachtel, G.D., McMullen, C.T., and Sangiovanni-Vincentelli, A.L.M., Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Boston, 1984.

Digital Library

Google Scholar

[5]

Fu, Z., Mahajan, Y., and Malik, S., zChaff Solver, http://www.princeton.edu/~chaff/zchaff.html

Google Scholar

[6]

Saldanha, A., Brayton, R.K., and Sangiovanni-Vincentelli, A.L.M., Circuit structure relations to redundancy and delay, IEEE Transactions on CAD, Vol. 13, issue 7, July 1994, pp. 875--883.

Digital Library

Google Scholar

[7]

Keutzer, K., Malik, S., and Saldanha, A., Is redundancy necessary to reduce delay?, IEEE Transactions on CAD, vol. 10, issue 4, 1991, pp. 453--469.

Digital Library

Google Scholar

Cited By

View all

Matrosova AOstanin SChernyshov S(2018)Finding False Paths for Sequential Circuits Using Operations on ROBDDs2018 IEEE 24th International Symposium on On-Line Testing And Robust System Design (IOLTS)10.1109/IOLTS.2018.8474213(240-242)Online publication date: Jul-2018
https://doi.org/10.1109/IOLTS.2018.8474213
Marques FMartinello ORibas RReis AMartino JAraújo GOrailoglu AKlein F(2010)Improvements on the detection of false paths by using unateness and satisfiabilityProceedings of the 23rd symposium on Integrated circuits and system design10.1145/1854153.1854201(192-197)Online publication date: 6-Sep-2010
https://dl.acm.org/doi/10.1145/1854153.1854201
Coudert OSapatnekar S(2010)An efficient algorithm to verify generalized false pathsProceedings of the 47th Design Automation Conference10.1145/1837274.1837321(188-193)Online publication date: 13-Jun-2010
https://dl.acm.org/doi/10.1145/1837274.1837321
Show More Cited By

Index Terms

A new approach to the use of satisfiability in false path detection
1. Hardware
  1. Electronic design automation
    1. Logic synthesis
      1. Circuit optimization
  2. Integrated circuits
    1. Digital switches
      1. Logic families

Recommendations

Improvements on the detection of false paths by using unateness and satisfiability
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system design

This paper presents improvements on a previous methodology for false path detection using satisfiability. As the previous methodology, which is referred as node-sat, it is based on circuit node properties that are related to non-testable stuck-at faults ...
A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiability

We present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSAT_CNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...
Path verification using Boolean satisfiability
DATE '98: Proceedings of the conference on Design, automation and test in Europe

The importance of identifying false paths in a combinational circuit cannot be overstated since they may mask the true delay. We present a fast algorithm based on boolean satisfiability for solving this problem. We also present extensions to this per-...

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

5
Total Citations
View Citations
231
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Matrosova AOstanin SChernyshov S(2018)Finding False Paths for Sequential Circuits Using Operations on ROBDDs2018 IEEE 24th International Symposium on On-Line Testing And Robust System Design (IOLTS)10.1109/IOLTS.2018.8474213(240-242)Online publication date: Jul-2018
https://doi.org/10.1109/IOLTS.2018.8474213
Marques FMartinello ORibas RReis AMartino JAraújo GOrailoglu AKlein F(2010)Improvements on the detection of false paths by using unateness and satisfiabilityProceedings of the 23rd symposium on Integrated circuits and system design10.1145/1854153.1854201(192-197)Online publication date: 6-Sep-2010
https://dl.acm.org/doi/10.1145/1854153.1854201
Coudert OSapatnekar S(2010)An efficient algorithm to verify generalized false pathsProceedings of the 47th Design Automation Conference10.1145/1837274.1837321(188-193)Online publication date: 13-Jun-2010
https://dl.acm.org/doi/10.1145/1837274.1837321
Bayrakci ADemir ATasiran S(2010)Fast Monte Carlo estimation of timing yield with importance sampling and transistor-level circuit simulationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2010.204904229:9(1328-1341)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.1109/TCAD.2010.2049042
Long Fei Loa Mize Cho Moon Mullen BSinghal S(2010)Constraint analysis and debugging for multi-million instance SoC designs2010 11th International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED.2010.5450540(422-427)Online publication date: Mar-2010
https://doi.org/10.1109/ISQED.2010.5450540

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

Improvements on the detection of false paths by using unateness and satisfiability

A satisfiability procedure for quantified boolean formulae

Path verification using Boolean satisfiability

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