Formal verification of an ATM switch fabric using multiway decision graphs
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 106-111
- https://doi.org/10.1109/glsv.1996.497603
Abstract
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.Keywords
This publication has 5 references indexed in Scilit:
- Bug identification of a real chip design by symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A unified framework for describing and verifying hardware synchronous sequential systemsFormal Methods in System Design, 1993
- Symbolic Model CheckingPublished by Springer Nature ,1993
- FairislePublished by Association for Computing Machinery (ACM) ,1991
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986