Article

Free access

Enhancing simulation with BDDs and ATPG

Authors:

Malay K. Ganai,

Adnan Aziz,

Andreas KuehlmannAuthors Info & Claims

DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference

Pages 385 - 390

https://doi.org/10.1145/309847.309965

Published: 01 June 1999 Publication History

PDF eReader

References

[1]

Felice Balarin and A. L. Sangiovanni-Vincentelli. An Iterative Approach to Language Containment. In Proc. oJ the Computer Aided Verification Conf., June 1993.

Digital Library

Google Scholar

[2]

R. Kurshan. Formal Verification in a Commercial Setting. In Proc. of the Design Automation Conf., June 1997.

Digital Library

Google Scholar

[3]

J. Yuan, J. Shen, J. Abraham, and A. Aziz. On Combining Formal and Informal Verification. In Proc. of the Computer Aided Verification Conf., July 1997.

Digital Library

Google Scholar

[4]

R. K. Brayton etal. VIS: A System for Verification and Synthesis. In Proc. of the Computer Aided Verification Conf., July 1996.

Digital Library

Google Scholar

[5]

B. Chen, M. Yamazaki, and M. Fujita. Bug Identification of a Real Chip Design by Symbolic Model Checking. In Proc. European Conf. on Design Automation, March 1994.

Crossref

Google Scholar

[6]

H. Cho, G. Hatchel, E. Macii, M. Poncino, and F. Somenzi. A State Space Decomposition Algorithm for Approximate FSM Traversal Based on Circuit Structural Analysis. Technical report, ECE/VLSI, Univ. of Colorado at Boulder, 1993.

Google Scholar

[7]

S. Devadas, A. Ghosh, and K. Keutzer. An Observability-Based Code Coverage Metric for Functional Simulation. In Proc. Intl. Conj. on Computer-Aided Design, November 1996.

Digital Library

Google Scholar

[8]

David L. Dill. Embedded Tutorial: What's between Simulation and Formal Verification? In Proc. of the Design Automation Conf., San Francisco, CA, June 1998.

Digital Library

Google Scholar

[9]

A. El-Maleh, T. Marchok, J. Rajski, and W. Maly. Behavior and Testability Preservation Under the Retiming Transformation. IEEE Transactions on Computer-Aided Design of Integrated Circuit, May 1997.

Digital Library

Google Scholar

[10]

D. Grist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur, and Y. Wolfsthal. Coverage Directed Test Generation Using Formal Verification. In Proc. of the Formal Methods in CAD Conj., November 1996.

Digital Library

Google Scholar

[11]

Daniel Grist and Ilan Beer. Efficient Model Checking by Automated Ordering of Transition Relation Partitions. In Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 52-71. Springer-Verlag, 1994.

Digital Library

Google Scholar

[12]

P. Goel. An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits. IEEE Transactions on Computers, 1981.

Digital Library

Google Scholar

[13]

R. Ho and M. Horowitz. Validation Coverage Analysis for Complex Digital Designs. In Proc. Intl. Conj. on Computer-Aided Design, November 1996.

Digital Library

Google Scholar

[14]

Richard C. Ho, C. Hart Yang, Mark A. Horowitz, and David L. Dill. Architectural Validation for Processors. In Proceedings of the International Symposium on Computer Architecture, June 1995.

Digital Library

Google Scholar

[15]

Y. Hoskote, D. Moundanos, and J. Abraham. Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. In Proc. Intl. Conf. on Computer Design, Austin, TX, October 1995.

Digital Library

Google Scholar

[16]

Andreas Kuehlmann and Florian Krohm. Equivalence Checking Using Cuts and Heaps. In Proc. of the Design Automation Conj., June 1997.

Digital Library

Google Scholar

[17]

W. Lee, A. Pardo, G. D. Hachtel, J. Jang, A. Pardo, and F. Somenzi. Tearing Based Automatic Abstraction for CTL Model Checking. In Proc. Intl. Conf. on Computer-Aided Design, 1996.

Digital Library

Google Scholar

[18]

Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[19]

K. L. McMillan. Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. In Proc. of the Computer Aided Verification Conj., Vancouver, BC, Canada, June 1998.

Digital Library

Google Scholar

[20]

D. Moundanos, J. Abraham, and Y. Hoskote. A Unified Framework for Design Validation and Manufacturing Test. in Proc. Intl. Test Conj., 1996.

Digital Library

Google Scholar

[21]

R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. A. Abraham, and D. S. Fussell. Efficient Combination Verification Using Cuts and Overlapping BDDs. In Proc. intl. Workshop on Logic Synthesis, May 1997.

Google Scholar

[22]

K. Ravi and F. Somenzi. High Density Reachability Analysis. In Proc. Intl. Conj. on Computer-Aided Design, Santa Clara, CA, November 1995.

Digital Library

Google Scholar

[23]

R. Rudell. Dynamic Variable Ordering for Binary Decision Diagrams. In Proc. Intl. Conj. on Computer-Aided Design, November 1993.

Digital Library

Google Scholar

[24]

P. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Combination Test Generation using Satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits, September 1996.

Digital Library

Google Scholar

[25]

U. Stern and D. L. Dill. Using Magnetic Disk instead of Main Memory in the Murphi Verifier. In Proc. of the Computer Aided Verification Conf., June 1998.

Digital Library

Google Scholar

[26]

D. Xiang, S. Venkataraman, W. K. Fuchs, and J. H. Patei. Partial Scan Design Based on Circuit State Information. In Proc. of the Design Automation Conf., Las Vegas, NV, June 1996.

Digital Library

Google Scholar

[27]

C. H. Yang and D. L. Dill. Validation with Guided Search of the State Space. In Proc. of the Design Automation Conf., June 1998.

Digital Library

Google Scholar

[28]

UC Berkeley. mlv.cad.eecs.bsrkslsy.sdu/'vis.

Google Scholar

Cited By

View all

Quer S(2014)Model checking evaluation of airplane landing trajectoriesInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0273-216:6(753-773)Online publication date: 1-Nov-2014
https://dl.acm.org/doi/10.1007/s10009-013-0273-2
Benouhiba TCheriet H(2011)A semi-formal approach for Java programs verification2011 10th International Symposium on Programming and Systems10.1109/ISPS.2011.5898887(169-176)Online publication date: Apr-2011
https://doi.org/10.1109/ISPS.2011.5898887
Agbaria SCarmi DCohen OKorchemny DLifshits MNadel ABloem RSharygina N(2010)SAT-based semiformal verification of hardwareProceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998505(25-32)Online publication date: 20-Oct-2010
https://dl.acm.org/doi/10.5555/1998496.1998505
Show More Cited By

Index Terms

Enhancing simulation with BDDs and ATPG
1. Hardware
  1. Hardware validation
    1. Functional verification
      1. Simulation and emulation

Recommendations

Can BDDs compete with SAT solvers on bounded model checking?
DAC '02: Proceedings of the 39th annual Design Automation Conference

The usefulness of Bounded Model Checking (BMC) based on propositional satisfiability (SAT) methods has recently proven its efficacy for bug hunting. BDD based tools are able to verify broader sets of properties (e.g. CTL formulas) but recent ...
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
An industrially effective environment for formal hardware verification

The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference

June 1999

1000 pages

ISBN:1581131097

DOI:10.1145/309847

Editor:
Mary Jane Irwin

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 June 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC99

Sponsor:

EDAC
SIGDA
IEEE-CAS

DAC99: The 36th ACM/IEEE-CAS/EDAC Design Automation Conference

June 21 - 25, 1999

Louisiana, New Orleans, USA

Acceptance Rates

DAC '99 Paper Acceptance Rate 154 of 451 submissions, 34%;

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

30
Total Citations
View Citations
318
Total Downloads

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

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Quer S(2014)Model checking evaluation of airplane landing trajectoriesInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0273-216:6(753-773)Online publication date: 1-Nov-2014
https://dl.acm.org/doi/10.1007/s10009-013-0273-2
Benouhiba TCheriet H(2011)A semi-formal approach for Java programs verification2011 10th International Symposium on Programming and Systems10.1109/ISPS.2011.5898887(169-176)Online publication date: Apr-2011
https://doi.org/10.1109/ISPS.2011.5898887
Agbaria SCarmi DCohen OKorchemny DLifshits MNadel ABloem RSharygina N(2010)SAT-based semiformal verification of hardwareProceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998505(25-32)Online publication date: 20-Oct-2010
https://dl.acm.org/doi/10.5555/1998496.1998505
Alizadeh BFujita MLin Y(2010)Guided gate-level ATPG for sequential circuits using a high-level test generation approachProceedings of the 2010 Asia and South Pacific Design Automation Conference10.5555/1899721.1899824(425-430)Online publication date: 18-Jan-2010
https://dl.acm.org/doi/10.5555/1899721.1899824
Tiwari PMitra R(2007)Hybrid Verification of Protocol BridgesIEEE Design & Test10.1109/MDT.2007.4724:2(124-131)Online publication date: 1-Mar-2007
https://dl.acm.org/doi/10.1109/MDT.2007.47
Bhadra JAbadir MWang LRay S(2007)A Survey of Hybrid Techniques for Functional VerificationIEEE Design & Test10.1109/MDT.2007.3024:2(112-122)Online publication date: 1-Mar-2007
https://dl.acm.org/doi/10.1109/MDT.2007.30
Majumdar RSen K(2007)Hybrid Concolic TestingProceedings of the 29th international conference on Software Engineering10.1109/ICSE.2007.41(416-426)Online publication date: 24-May-2007
https://dl.acm.org/doi/10.1109/ICSE.2007.41
Shyam SBertacco VGielen G(2006)Distance-guided hybrid verification with GUIDOProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131816(1211-1216)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131816
Maurer PGielen G(2006)Using conjugate symmetries to enhance gate-level simulationsProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131661(638-643)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131661
Hsu YTsai FJong WChang YSentovich E(2006)Visibility enhancement for silicon debugProceedings of the 43rd annual Design Automation Conference10.1145/1146909.1146917(13-18)Online publication date: 24-Jul-2006
https://dl.acm.org/doi/10.1145/1146909.1146917
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

Can BDDs compete with SAT solvers on bounded model checking?

Conditional model checking: a technique to pass information between verifiers

An industrially effective environment for formal hardware verification