Breadcrumb

 
 

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.

[img]
Preview
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 > Faculty 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:Theses (M.A.Sc.)
Program:Dept. of Electrical and Computer Engineering
Date:1999
Thesis Supervisor(s):Tahar, Sofiene
ID Code:868
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:14
Last Modified:08 Dec 2010 10:17
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

Document Downloads

More statistics for this item...

Concordia University - Footer