Fitting formal methods into the design cycle

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Fitting formal methods into the design cycle

Full text

Pdf (326 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 31st annual Design Automation Conference table of contents

San Diego, California, United States

Pages: 314 - 319

Year of Publication: 1994

ISBN:0-89791-653-0

Author

K. L. McMillan

AT&T Bell Laboratories, Murray Hill, NJ

Sponsors

IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation
EDAC : Electronic Design Automation Consortium

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 13, Citation Count: 10

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/196244.196392 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	Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
	2	William R. Bevier , Warren A. Hunt, Jr. , J. Strother Moore , William D. Young, An approach to systems verification, Journal of Automated Reasoning, v.5 n.4, p.411-428, Dec. 1989
	3	S. Bose and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In IEEE International Conference on Computer Design, 1989.
	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	R. E. Bryant. Boolean analysis of MOS circuits, lEE Trans. CAD, 6(4):634-649, July 1987.
	6	Randal E. Bryant, Verifying a static RAM design by logic simulation, Proceedings of the fifth MIT conference on Advanced research in VLSI, p.335-349, January 1988, Cambridge, Massachusetts, United States
	7	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	8	Paul N. Loewenstein , David L. Dill, Verification of a multiprocessor cache protocol using simulation relations and higher-order logic, Formal Methods in System Design, v.1 n.4, p.355-383, Dec. 1992 [doi>10.1007/BF00709156]
	9	Aarti Gupta, Formal hardware verification methods: a survey, Formal Methods in System Design, v.1 n.2-3, p.151-238, Oct. 1992 [doi>10.1007/BF00121125]
	10	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	11	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	12	K.L. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistency protocol. In International Symposium on Shared Memory Multiprocessors, 1991.
	13	A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
	14	Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990 [doi>10.1109/2.58215]

CITED BY 10

	Massimo Bombana , Patrizia Cavalloro , Salvatore Conigliaro , Roger B. Hughes , Gerry Musgrave , Giuseppe Zaza, Design-flow and synthesis for ASICs: a case study, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.292-297, June 12-16, 1995, San Francisco, California, United States
	Jörg Bormann , Jörg Lohse , Michael Payer , Gerd Venzl, Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.298-303, June 12-16, 1995, San Francisco, California, 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
	D. Knapp , T. Ly , D. MacMillen , R. Miller, Behavioral synthesis methodology for HDL-based specification and validation, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.286-291, June 12-16, 1995, San Francisco, California, United States
	Jeremy Levitt , Kunle Olukotun, A scalable formal verification methodology for pipelined microprocessors, Proceedings of the 33rd annual conference on Design automation, p.558-563, June 03-07, 1996, Las Vegas, Nevada, United States
	Jeremy Levitt , Kunle Olukotun, Verifying correct pipeline implementation for microprocessors, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.162-169, November 09-13, 1997, San Jose, California, United States
	Gagan Hasteer , Anmol Mathur , Prithviraj Banerjee, An efficient assertion checker for combinational properties, Proceedings of the 34th annual conference on Design automation, p.734-739, June 09-13, 1997, Anaheim, California, United States
	William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
	J. W. G. Fleurkens , C. A. J. van Eijk , J. A. G. Jess, Run-time consistency checking in discrete simulation models, Proceedings of the 1995 European conference on Design and Test, p.223, March 06-09, 1995
	Yasushi Umezawa , Takeshi Shimizu, A Formal Verification Methodology for Checking Data Integrity, Proceedings of the conference on Design, Automation and Test in Europe, p.284-289, March 07-11, 2005