Accessibility Tools

Breadcrumb

 
 

Hardware Verification Group Home > Research > Application >

Formal Verification of a Telecom System Block using MDGs

 

Members

  • M. Hasan Zobair
  • Dr. Sofiène Tahar

External Collaborators

  • Jean Lamarche, PMC-Sierra , Inc, Montreal
  • Dr. Xiaoyu Song, Portland State University, USA.

Description

The objective of this project is to apply the Multiway Decision Graphs (MDG) tools for the modeling and formal verification of a Telecom System Block (TSB) from PMC-Sierra, Inc. The TSB under investigation is a Receive Automatic Protection Switch (APS) Control, Synchronization Status Extraction, and Bit Error Rate Monitor (RASE) which processes a portion of the SONET Line Overhead of a received SONET data stream. In this project, we will first translate the original VHDL design description to an MDG-HDL structural model. From the TSB documentation, a behavioral specification as an Abstract State Machine (ASM) will also be derived. The formal verification of the RASE TSB will then be performed by property checking and equivalence checking provided by the MDG tools. In order to handle the complexity of the RASE TSB design, we will adopt a hierarchical proof methodology based on module abstraction.

Publications

  1. S. Tahar, M.H. Zobair, and X. Song: On the Formal Verification of a SONET Data Stream Processor ; IEE Proceedings - Computers and Digital Techniques, Vol. 151, No. 1, pp. 71-81, January 2004.
  2. M.H. Zobair and S. Tahar: Formal Verification of a SONET Telecom System Block; In: C. George and H. Miao (Eds.), Formal Methods in Software Engineering, Lecture Notes in Computer Science 2495, Springer Verlag, 2002, pp. 447-458. [Proc. International Conference on Formal Engineering Methods (ICFEM'02), Shanghai, China, October 2002.]
  3. M.H. Zobair and S. Tahar: Modeling and Formal Verification of a Telecom System Block using MDGs; Proc. 2001 Micronet Annual Workshop, Alymer, Canada, April 2001, pp. 161-162.
  4. M.H. Zobair, S. Tahar, and P. Curzon: Impact of Design Changes on Verification Using MDGs; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000.
  5. M. H.Zobair and S. Tahar: On the Modeling and Verification of a Telecom System Block Using MDGs ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2000. [33 pages]
  6. M.H. Zobair, S. Tahar, and P. Curzon: Impact on Design Changes on Verification using MDG; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 1999. [15 pages]
  7. M. H. Zobair: Modeling and Formal Verification of a Telecom System Block using MDGs; MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, December 2000.


 
 

Concordia University