Model checking in industrial hardware design

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Model checking in industrial hardware design

Full text

Pdf (207 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 32nd annual ACM/IEEE Design Automation Conference table of contents

San Francisco, California, United States

Pages: 298 - 303

Year of Publication: 1995

ISBN:0-89791-725-1

Authors

Jörg Bormann	Siemens Corporate R&D, D-81730 Munich, Germany
Jörg Lohse	Siemens Corporate R&D, D-81730 Munich, Germany
Michael Payer	Siemens Corporate R&D, D-81730 Munich, Germany
Gerd Venzl	Siemens Corporate R&D, D-81730 Munich, Germany

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 12, Citation Count: 7

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/217474.217545 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	A. Aziz , F. Balarin , S.-T. Cheng , R. Hojati , T. Kam , S. C. Krishnan , R. K. Ranjan , T. R. Shiple , V. Singhal , S. Tasiran , H.-Y. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, HSIS: a BDD-based environment for formal verification, Proceedings of the 31st annual conference on Design automation, p.454-459, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196467]
	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örg Bormann , H. Nusser-Wehlan , Gerd Venzl, Invited Talk: Formal Design in an Industrial Research Laboratory: Lessons and Perspectives, Proceedings of the Second IFIP WG10.2/WG10.5 Workshop on Designing Correct Circuits, p.193-213, January 06-08, 1992
	4	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	5	Holger Busch , Gerd Venzl, Proof-aided design of verified hardware, Proceedings of the 28th conference on ACM/IEEE design automation, p.391-396, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127700]
	6	Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164555]
	7	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
	8	Werner Damm , Bernhard Josko , Rainer Schlör, Specification and verification of VHDL-based system-level hardware designs, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
	9	Alain Debreil , Philippe Oddo, Synchronous design in VHDL, Proceedings of the conference on European design automation, p.680-681, November 1992, Congress Centrum Hamburg, Hamburg, Germany
	10	Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
	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	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	15	K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196392]
	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 7

	Flavio Lerda , Willem Visser, Addressing dynamic issues of program model checking, Proceedings of the 8th international SPIN workshop on Model checking of software, p.80-102, May 2001, Toronto, Ontario, Canada
	Ronald Herrmann , Thomas Reielts, Verification of a production cell using an automatic verification environment for VHDL, Proceedings of the conference on European design automation, p.542-547, September 18-22, 1995, Brighton, England
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Avner Landver, RuleBase: an industry-oriented formal verification tool, Proceedings of the 33rd annual conference on Design automation, p.655-660, June 03-07, 1996, Las Vegas, Nevada, United States
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	W. Baker , A. Newton, The maximal VHDL subset with a cycle-level abstraction, Proceedings of the conference on European design automation, p.470-475, September 1996, Geneva, Switzerland
	Hoon Choi , Byeongwhee Yun , Yuntae Lee , Hyunglae Roh, Model checking of S3C2400X industrial embedded SOC product, Proceedings of the 38th conference on Design automation, p.611-616, June 2001, Las Vegas, Nevada, United States
	Manel Khlif , Mohamed Shawky, Observability Checking to Enhance Diagnosis of Real Time Electronic Systems, Proceedings of the 2008 12th IEEE/ACM International Symposium on Distributed Simulation and Real-Time Applications, p.69-74, October 27-29, 2008