Accessibility Tools

Breadcrumb

 
 

Hardware Verification Group Home > Research > Application >

ATM Switch Verification

 

Members

  • Jianping Lu
  • Dr. Sofiène Tahar

External Collaborators

  • Dr. Xiaoyu Song and Dan Voicu, University of Montreal
  • Dr. Paul Curzon, Middlesex University, UK

Description

Since the current ATM switch has reached 50G bps or even higher bit rate, very complicated modules are making the verification of an ATM switch as the bottle neck in the ATM switch design phase. However, although formal verification has been used in microprocessor or computer design, there is a little application on the verification of ATM switch. Our research is to apply model checking and equivalence checking for the formal verification of ATM switches. Model checking is used in verifying the global properties of an ATM switch. In order to handle a larger ATM design, we apply compositional reasoning to establish a set of environments for various ATM switch components. In addition, we propose and apply property division to verify some global properties to enhance the model checking of certain properties. Equivalence checking is applied to check the sequential equivalence between two different design levels, e.g. RTL and gate-level. Unfortunately, current sequential equivalence checking tools cannot handle medium size designs, therefore, we only used it for submodule verification in our examples, and it may be used for block level verification for a larger design. We have applied model checking and equivalence checking to verify the 4 by 4 Fairisle ATM switch which is in use at Cambridge University, UK. We also partially verified RCMP-800 which was developed according to the PMC-Sierra product documentation. In addition, we applied equivalence checking to verify the architecture of KNOCKOUT ATM switch which has been proven to be quite efficient in many applications. In these verification examples, we established verification strategies which are easy to apply and very efficient in real applications. The methods we illustrated can also be applied to similar ATM switch components.

Publications

  1. J. Lu and S. Tahar: Modeling and Verification of an ATM Port Controller in VIS ; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 1, pp. 241-245.
  2. J. Lu and S. Tahar: On the Model Checking of the RCMP-800 Input FIFO ; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 1, pp. 578-583.
  3. J. Lu and S. Tahar: Design and Verification of a Knockout ATM Concentrator; Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001.
  4. S. Tahar, P. Curzon and J. Lu: Three Approaches to Hardware Verification: HOL, MDG and VIS Compared ; In Gopalakrishnan, G. and Windley, P. (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1522, Springer Verlag, 1998, pp. 433-450. Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), Palo Alto, California, USA, November 1998.
  5. J. Lu, S. Tahar, D. Voicu and X. Song: Model Checking of a real ATM Switch ; Proc. IEEE International Conference on Computer Design (ICCD'98), Austin, Texas, USA, October 1998, IEEE Computer Society Press, pp. 195-198.
  6. J. Lu and S. Tahar: Practical Approaches to the Automatic Verification of an ATM Switch Fabric using VIS; Proc. IEEE 8th Great Lakes Symposium on VLSI (GLS-VLSI'98), Lafayette, Louisiana, USA, February 1998, IEEE Computer Society Press, pp. 368-373.
  7. J. Lu and S. Tahar: Modeling and Verification of the Fairisle ATM Null Port Controller in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [18 pages]
  8. J. Lu and S. Tahar: Model Checking of the RCMP-800 Input FIFO in VIS ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [9 pages]
  9. J. Lu, D. Voicu, S. Tahar, and X. Song: Model Checking of the Fairisle ATM Switch ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 1998. [22 pages]
  10. J. Lu and S. Tahar: On the Formal Verification and Reimplementation of an ATM Switch Fabric Using VIS ; Technical Report No. 401, Concordia University, Department of Electrical and Computer Engineering, September 1997. [19 pages]
  11. J. Lu: On the Formal Verification of ATM Switches; MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, May 1999.


 
 

Concordia University