Login | Register

On the formal verification of ATM switches

Title:

On the formal verification of ATM switches

Lu, Jianping (1999) On the formal verification of ATM switches. Masters thesis, Concordia University.

[thumbnail of MQ43654.pdf]
Preview
Text (application/pdf)
MQ43654.pdf
5MB

Abstract

Because of the difficulty of adequately simulating large digital designs, there has been a surge of interest in formal verification, in which a mathematical model of the design is proved to satisfy a precise specification. Model Checking and Equivalence Checking , which have the advantage of automatic verification, are two main formal verification techniques that people are working on. The main problem of model checking and sequential equivalence checking is the state space explosion. Another drawback of model checking is lack of methods on establishing an environment and expressing a property. In this thesis, we propose Property Division techniques which avoid the state space explosion problem by deducing a property from several sub-properties. A number of methods on establishing an environment and expressing a property are illustrated. Although ATM hardware is hard to design due to its high speed and various features. the applications of model checking and equivalence checking on ATM hardware verification are few. In this thesis, Fairisle ATM switch fabric, Fairisle ATM null port controller, Input FIFO of RCMP-800 and Concentrator of Knockout ATM switch are developed. With the techniques we propose, all these ATM hardware designs are formally verified in the formal verification tools called Verification Interacting with Synthesis ( VIS )

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Lu, Jianping
Pagination:viii, 148 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Dept. of Electrical and Computer Engineering
Date:1999
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:TK 5105.35 L82 1999
ID Code:868
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:14
Last Modified:13 Jul 2020 19:47
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top