On the formal verification of ATM switches

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