Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions

M
MEMOCODE
2003
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)
Abstract - Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Sudarshan K. Srinivasan Articles by Miroslav N. Velev

First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)

Mont Saint-Michel, France

June 24-June 26

ISBN: 0-7695-1923-7

	ASCII Text	x
	Sudarshan K. Srinivasan, Miroslav N. Velev, "Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions," Formal Methods and Models for Co-Design, ACM/IEEE International Conference on, pp. 65, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003.

	BibTex	x
	@article{ 10.1109/MEMCOD.2003.1210090, author = {Sudarshan K. Srinivasan and Miroslav N. Velev}, title = {Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions}, journal ={Formal Methods and Models for Co-Design, ACM/IEEE International Conference on}, volume = {0}, year = {2003}, isbn = {0-7695-1923-7}, pages = {65}, doi = {http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210090}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on TI - Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions SN - 0-7695-1923-7 SP EP A1 - Sudarshan K. Srinivasan, A1 - Miroslav N. Velev, PY - 2003 KW - null VL - 0 JA - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on ER -

Sudarshan K. Srinivasan, Georgia Institute of Technology, Atlanta

Miroslav N. Velev, Georgia Institute of Technology, Atlanta

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210090

We present the formal verification of an Intel Xscale processor model. The Xscale is a superpipelined RISC processor with 7-stage integer, 8-stage memory, and variable-latency multiply-and-accumulate execution pipelines. The processor uses scoreboarding to track data dependencies, and implements both precise and imprecise exceptions. Such set of features had not been modeled, and formally verified previously. The formal verification was done with an automatic toll flow that consists of the term-level symbolic simulator TLSim, the decision procedure EVC, and an efficient SAT-checker.

Citation:

Sudarshan K. Srinivasan, Miroslav N. Velev, "Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions," memocode, pp.65, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.