Towards verifying VHDL descriptions of processors

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Towards verifying VHDL descriptions of processors

Full text

Pdf (627 KB)

Source

European Design Automation Conference archive
Proceedings of the conference on European design automation table of contents

Brighton, England

Pages: 414 - 419

Year of Publication: 1995

ISBN:0-8186-7156-4

Authors

Laurent Arditi	Université de Nice, Sophia Antipolis, 13S, CNRS-URA 1376
Hélène Collavizza	Université de Nice, Sophia Antipolis, 13S, CNRS-URA 1376

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society Press Los Alamitos, CA, USA

Bibliometrics

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

Additional Information:

references cited by index terms collaborative colleagues

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

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	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]
	2	M. Gordon, "HOL, a machine oriented formulation of higher order logic," Tech. Rep. 68, University of Cambridge, Computer Laboratory, 1985.
	3	A. Cohn, "A proof of correctness of the Viper microprocessor: the first level," in VLSI Specification, Verification and Synthesis, (Calgary), Jan. 1987.
	4	Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
	5	D. Borrione, P. Camurati, J. Paillet, and P. Prinetto, "A functional approach to formal hardware verification: The MTI experience," in ICCD'88, (Port Chester, New-York), Oct. 1988.
	6	Phillip John Windley, The formal verification of generic interpreters, 1990
	7	Laurent Arditi , Hélène Collavizza, An Object-Oriented Framework for the Formal Verification of Processors, Proceedings of the 9th European Conference on Object-Oriented Programming, p.215-234, August 07-11, 1995
	8	J. P. van Tassel, Femto-VHDL: The Semantics of a Subset of VHDL and its Embedding in the HOL Proof Assistant. PhD thesis, Univ. of Cambridge, July 1993.
	9	P. T. Breuer, L. S. Fernandez, and C. Delgado Kloos, "Clean formal semantics for VHDL," in European Design Automation Conference, (Paris, France), 1994.
	10	Dominique D. Borrione , Laurence V. Pierre , Ashrak M. Salem, Formal Verification of VHDL Descriptions in the Prevail Environment, IEEE Design & Test, v.9 n.2, p.42-56, April 1992 [doi>10.1109/54.143145]
	11	F. Nicoli and L. Pierre, "From VHDL to formal verification," in EURO-VHDL Conference, (Grenoble, France), Sept. 1994.
	12	P. J. Ashenden, The VHDL Cookbook. Dept. Computer Science, Univ. of Adelaide, July 1990.
	13	E. Gallesio, "STklos: a Scheme object oriented system dealing with the TK toolkit," in Xhibition 9~, (San Jose), ICS, Jul. 1994.
	14	Francois Anceau, The architecture of microprocessors, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
	15	V. Stavridou, Formal methods in circuit design, Cambridge University Press, New York, NY, 1993
	16	Michel Allemand, A Rewriting Based Method for the Formal Verification of Microprocessors, 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.115-122, April 26-28, 1993