Formal verification of pipeline conflicts in RISC processors

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal verification of pipeline conflicts in RISC processors

Full text

Pdf (696 KB)

Source

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

Grenoble, France

Pages: 284 - 289

Year of Publication: 1994

ISBN:0-89791-685-9

Authors

Ramayya Kumar	Forschungszentrum Informatik, Department of Automation in Circuit Design, Haid-und-Neu, Straβe 10-14, 76131 Karlsruhe, Germany
Sofiène Tahar	University of Karlsruhe, Institute of Computer Design and Fault Tolerance (Prof. D. Schmid), P.O. Box 6980, 76128 Karlsruhe, Germany

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society Press Los Alamitos, CA, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 13, 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	Francois Anceau, The architecture of microprocessors, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
	2	Cohn, A.: A Proof of the Viper Microprocessor: The First Level; In: Birtwistle, G. and Subrahmanyam, P. (Eds.). VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.
	3	M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
	4	David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
	5	Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
	6	Joyce, J.: Multi-Level Verification of Microprocessor-Based Systems; Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989.
	7	Kogge. P.: The Architecture of Pipelined Computers; McGraw-Hill, 1981.
	8	Ramayya Kumar , Klaus Schneider , Thomas Kropf, Structuring and automating hardware proofs in a higher-order theorem-proving environment, Formal Methods in System Design, v.2 n.2, p.165-223, April 1993 [doi>10.1007/BF01383880]
	9	Mandayam Srivas , Mark Bickford, Formal Verification of a Pipelined Microprocessor, IEEE Software, v.7 n.5, p.52-64, September 1990 [doi>10.1109/52.57892 ]
	10	Tahar, S.; Kumar. R.: A Formalization of a Hierarchical Model for RISC Processors; In: Spies, P. (Ed.), Proc. European lnformatics Congress Computing Systems Architecture (Euro-ARCH93), Munich, October 1993. lnformatik Aktuell, Springer Verlag, pp. 591-602.
	11	Tahar, S.; Kumar, R.: Towards a Methodology for the Formal Hierarchical Verification of RISC Processors; Proc. IEEE International Conference on Computer Design (ICCD93), Cambridge, Massachusetts, October 1993, pp. 58-62.
	12	Sofiène Tahar , Ramayya Kumar, Implementing a Methodology for Formally Verifying RISC Processors in HOL, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.281-294, August 11-13, 1993
	13	Phillip John Windley, The formal verification of generic interpreters, 1990