Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs

	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/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by S. Tahar Articles by Z. Zhou Articles by X. Song Articles by E. Cerny Articles by Michel Langevin

6th Great Lakes Symposium on VLSI

Ames, IA

March 22-March 23

ISBN: 0-8186-7502-0

	ASCII Text	x
	S. Tahar, Z. Zhou, X. Song, E. Cerny, Michel Langevin, "Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs," Great Lakes Symposium on VLSI, pp. 0106, 6th Great Lakes Symposium on VLSI, 1996.

	BibTex	x
	@article{ 10.1109/GLSV.1996.497603, author = {S. Tahar and Z. Zhou and X. Song and E. Cerny and Michel Langevin}, title = {Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs}, journal ={Great Lakes Symposium on VLSI}, volume = {0}, year = {1996}, isbn = {0-8186-7502-0}, pages = {0106}, doi = {http://doi.ieeecomputersociety.org/10.1109/GLSV.1996.497603}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Great Lakes Symposium on VLSI TI - Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs SN - 0-8186-7502-0 SP EP A1 - S. Tahar, A1 - Z. Zhou, A1 - X. Song, A1 - E. Cerny, A1 - Michel Langevin, PY - 1996 KW - Hardware Verification KW - ATM Switch Fabric KW - Multiway Decision Graphs KW - Safety Property Checking KW - Abstract State Machines VL - 0 JA - Great Lakes Symposium on VLSI ER -

S. Tahar, University of Montreal

Z. Zhou, University of Montreal

X. Song, University of Montreal

E. Cerny, University of Montreal

Michel Langevin, GMD-SET, Shloss Birlinghoven, 53757 St. Augustin, Germany

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/GLSV.1996.497603

In this paper we present our results on formally verifying the implementation of an Asynchronous Transfer Mode (ATM) network switching fabric using a new class of decision graphs, called Multiway Decision Graphs (MDG). The design we consider is in use for real applications in the Cambridge Fairisle network. We produced the description of the hardware implementation at different levels of abstraction. We then performed the verification of an abstract description model against the description of the gate-level implementation. Using this abstract model, we accomplished the verification of specific properties that reflect the behavior of the Fairisle ATM switch fabric.

Index Terms:

Hardware Verification, ATM Switch Fabric, Multiway Decision Graphs, Safety Property Checking, Abstract State Machines

Citation:

S. Tahar, Z. Zhou, X. Song, E. Cerny, Michel Langevin, "Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs," glsvlsi, pp.0106, 6th Great Lakes Symposium on VLSI, 1996

Peer Review Notice | Give Us Feedback

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