Integrating formal verification methods with a conventional project design flow

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Integrating formal verification methods with a conventional project design flow

Full text

Pdf (49 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 33rd annual Design Automation Conference table of contents

Las Vegas, Nevada, United States

Pages: 666 - 671

Year of Publication: 1996

ISBN:0-89791-779-0

Author

Ásgeir Th. Eiríksson

Silicon Graphics Inc., Mountain View, CA

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): 9, Citation Count: 6

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/240518.240644 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.

	Bai95	Stan Bailes, v2smv, Internal SGI Inc., verilog to smv translator.
	Bry86	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]
	Bry91	Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger, Formal hardware verification by symbolic ternary trajectory evaluation, Proceedings of the 28th conference on ACM/IEEE design automation, p.397-402, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127701]
	Bur91	J.R. Burch, E. M. Clarke, and D. E. Long, "Symbolic Model Checking with Partitioned Transition Relations", VLS191: Proceedings of the IFIP TC 10/WG 10.5 International Conf. on VLSI, Edinburgh, Great Britain, 1991
	Cla93	Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
	Eir95	Ásgeir Th. Eiríksson , Kenneth L. McMillan, Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study, Proceedings of the 7th International Conference on Computer Aided Verification, p.367-380, July 03-05, 1995
	Gor88	M.J.C. Gordon (ed), "HOL: A Proof-Generating System for Higher-Order Logic", Kluwer SECS 35, pp. 73-128, 1988.
	Kur94	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	Len92	Daniel Lenoski , James Laudon , Kourosh Gharachorloo , Wolf-Dietrich Weber , Anoop Gupta , John Hennessy , Mark Horowitz , Monica S. Lam, The Stanford Dash Multiprocessor, Computer, v.25 n.3, p.63-79, March 1992 [doi>10.1109/2.121510]
	Lon93	David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
	McM91	K.L. McMillan, J. Schwalbe, "Formal Verification of the Encore Gigamax cache consistency protocol.", Int. Symposium on Shared Memory Multiprocessors, 1991.
	McM93	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	McM95a	K.L. McMillan, vl2smv: verilog to smv translator, Cadence Berkeley Labs, 1995.
	McM95b	K.L. McMillan, rc: refinement checker, Cadence Berkeley Labs, 1995.
	Seg93	Carl J Seger , Bryant, R , E. al, Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories, University of British Columbia, Vancouver, BC, Canada, 1993
	Tan95	Andrew S. Tanenbaum, Distributed operating systems, Prentice-Hall, Inc., Upper Saddle River, NJ, 1994

CITED BY 6

	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
	Cindy Eisner , Irit Shitsevalov , Russ Hoover , Wayne Nation , Kyle Nelson , Ken Valk, A methodology for formal design of hardware control with application to cache coherence protocols, Proceedings of the 37th conference on Design automation, p.724-729, June 05-09, 2000, Los Angeles, 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
	Steven M. German, Formal Design of Cache Memory Protocols in IBM, Formal Methods in System Design, v.22 n.2, p.133-141, March 2003
	Ásgeir Th. Eiríksson, The Formal Design of 1M-gate ASICs, Formal Methods in System Design, v.16 n.1, p.7-22, Jan 1,2000
	Peter Böhm , Tom Melham, A refinement approach to design and verification of on-chip communication protocols, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon