Article

Free access

Model checking in industrial hardware design

Authors:

Gerd VenzlAuthors Info & Claims

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

Pages 298 - 303

https://doi.org/10.1145/217474.217545

Published: 01 January 1995 Publication History

First page of PDF

References

[1]

A. Aziz, F. Balarin, S.-T. Cheng, R. Hoyati, T. Kam, S.C. Krishnan, R.K. Ranjan, T.R. Shiple, V. Singhal, S. Tasiran, H.-Y. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. HSIS: A BDD-based environment for formal verification. In 31st ACM/IEEE Design Automation Conference, pages 454-459, June 1994.

Digital Library

[2]

J. Bormann, T. Filkorn, J. Lohse, M. Payer, G. Venzl, and P. Warkentin. CVE: An industrial formal verification environment. Internal report, 1994.

[3]

J. Bormann, H. Nusser-Wehlan, and G. Venzl. Formal design in an industrial research laboratory: lessons andperspectives. In Designing Correct Circuits. 2nd IFIP WGIO.2/WGIO. 5 Workshop, pages 193- 213, 1992.

Digital Library

[4]

R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.

Digital Library

[5]

H. Busch and G. Venzl. Proof-aided design of verified hardware. In 28th ACM/IEEE Design Automation Conference, pages 391 - 196, 1991.

Digital Library

[6]

H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal. In 30th A CM/IEEE Design Automation Conference, pages 25- 30, 1993.

Digital Library

[7]

E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Conference Record of the 19th Annual A CM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 343- 354, 1992.

Digital Library

[8]

W. Datum, B. Josko, and R. Schl6r. Specification and verification of VHDL-based hardware designs. In E. B6rger, editor, Specification and validation methods for programming languages and systems. Oxford University Press, 1994. To appear.

Digital Library

[9]

A. Debreil and P. Oddo. Synchronous designs in VHDL. In Proceedings Euro-DA C'93 with Euro- VHDL '93, pages 486-491. IEEE Computer Society Press, September 1993.

Digital Library

[10]

A. J. Hu and D. L. Dill. Reducing BDD size by exploiting functional dependencies. In 30th A CM/IEEE Design Automation Conference, pages 266 - 271, 1993.

Digital Library

[11]

J. Lohse, J. Bormann, M. Payer, and G. Venzl. VHDL-translation for BDD-based formal verification. Internal report, 1994.

[12]

IEEE Standard VHDL Language Reference Manual. The Institute of Electrical and Electronical Engineers, Inc., New York, IEEE Std 1076-1987 edition, 1988.

[13]

K. L. McMillan and J. Schwalbe. Formal verification of the encore gigamax cache consistency protocol. In International Symposium on Shared Memory Mulitprocessors, April 1991.

[14]

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

Digital Library

[15]

K.L. McMillan. Fitting formal methods into the design cycle. In 31st ACM/IEEE Design Automation Conference, pages 314-319, June 1994.

Digital Library

[16]

P. Stanford and P. Mancuso. EDIF Electronic Design Interchange Format, Reference Manual for Version 2 00. Electronic Industries Association, Washington D.C., 1989.

Cited By

Ecker WMrva M(2022)Object Orientation: Modeling and Design Paradigms for the Year 2000?Object-Oriented Modeling10.1007/978-1-4613-1349-6_1(1-14)Online publication date: 6-Jul-2022
https://doi.org/10.1007/978-1-4613-1349-6_1
Zhang CSun MLi JSu TPu G(2021)Feedback-Guided Circuit Structure Mutation for Testing Hardware Model Checkers2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643509(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643509
Mashkoor AJacquot J(2017)Validation of formal specifications through transformation and animationRequirements Engineering10.1007/s00766-016-0246-622:4(433-451)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s00766-016-0246-6
Show More Cited By

Index Terms

Model checking in industrial hardware design
1. Hardware
  1. Electronic design automation
    1. Hardware description languages and compilation
  2. Hardware validation
    1. Functional verification
      1. Simulation and emulation

Recommendations

A Meta Hardware Description Language Melasy for Model-Checking Systems
ITNG '08: Proceedings of the Fifth International Conference on Information Technology: New Generations

Model-checking tools such as Symbolic Model Verifier (SMV) and NuSMVare available for checking hardware designs. These tools can automatically check the formal legitimacy of a design. However, NuSMV is too low level for describing a complete hardware ...
Industrial applications of model checking
Modeling and verification of parallel processes

Formal methods have a great potential of application in the development of industrial critical systems. In certain application fields, formal methods are even becoming part of standards. Among formal methods, Model Checking is proving particularly ...
Efficient Model Checking of Hardware Using Conditioned Slicing

In this work, we present an abstraction based property verification technique for hardware using conditioned slicing. We handle safety property specifications of the form G(antecedent@?consequent). We use the antecedent of the properties to create our ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

January 1995

760 pages

ISBN:0897917251

DOI:10.1145/217474

Chairman:
Bryan T. Preas
Xerox Parc, Palo Alto, CA

Copyright © 1995 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

EDAC: Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DAC95

Sponsor:

EDAC
SIGDA

DAC95: The 32nd Design Automation Conference

June 12 - 16, 1995

California, 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

28
Total Citations
View Citations
424
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)5

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ecker WMrva M(2022)Object Orientation: Modeling and Design Paradigms for the Year 2000?Object-Oriented Modeling10.1007/978-1-4613-1349-6_1(1-14)Online publication date: 6-Jul-2022
https://doi.org/10.1007/978-1-4613-1349-6_1
Zhang CSun MLi JSu TPu G(2021)Feedback-Guided Circuit Structure Mutation for Testing Hardware Model Checkers2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643509(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643509
Mashkoor AJacquot J(2017)Validation of formal specifications through transformation and animationRequirements Engineering10.1007/s00766-016-0246-622:4(433-451)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s00766-016-0246-6
Della Penna G(2014)Model checking XSL transformationsComputer Languages, Systems & Structures10.1016/j.cl.2014.03.00340:2(73-97)Online publication date: Jul-2014
https://doi.org/10.1016/j.cl.2014.03.003
Cheng BEder KGogolla MGrunske LLitoiu MMüller HPelliccione PPerini AQureshi NRumpe BSchneider DTrollmann FVillegas N(2014)Using Models at Runtime to Address Assurance for Self-Adaptive Systems[email protected]10.1007/978-3-319-08915-7_4(101-136)Online publication date: 2014
https://doi.org/10.1007/978-3-319-08915-7_4
Peled DPelliccione PSpoletini P(2009)Model CheckingWiley Encyclopedia of Computer Science and Engineering10.1002/9780470050118.ecse247(1904-1920)Online publication date: 16-Mar-2009
https://doi.org/10.1002/9780470050118.ecse247
Khlif MShawky M(2008)Observability Checking to Enhance Diagnosis of Real Time Electronic SystemsProceedings of the 2008 12th IEEE/ACM International Symposium on Distributed Simulation and Real-Time Applications10.1109/DS-RT.2008.18(69-74)Online publication date: 27-Oct-2008
https://dl.acm.org/doi/10.1109/DS-RT.2008.18
Borrione DBouamama HDeharbe DLe Faou CWahba A(2005)HDL-based integration of formal methods and CAD tools in the PREVAIL environmentFormal Methods in Computer-Aided Design10.1007/BFb0031827(450-467)Online publication date: 25-Jun-2005
https://doi.org/10.1007/BFb0031827
Lerda FVisser W(2001)Addressing dynamic issues of program model checkingProceedings of the 8th international SPIN workshop on Model checking of software10.5555/380921.380931(80-102)Online publication date: 2-May-2001
https://dl.acm.org/doi/10.5555/380921.380931
Bormann JSpalinger C(2001)Formale Verifikation für Nicht-Formalisten (Formal Verification for Non-Formalists)it - Information Technology10.1524/itit.2001.43.1.2243:1Online publication date: 1-Jan-2001
https://doi.org/10.1524/itit.2001.43.1.22
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents