Members

• Leila Barakatain
• Dr. Sofiène Tahar

External Collaborators

• Jean Lamarche, PMC-Sierra , Inc, Montreal
• Jean-Marc Gendreau, PMC-Sierra , Inc, Montreal

Description

The objective of this project is to apply model checking techniques for the formal verification of a SCI-PHY Level 2 protocol (a super set of UTOPIA Level 2 protocol) Engine. In collaboration with PMC-Sierra Inc., we are using FormalCheck (Cadence model checking tool) to formally verify the RTL implementation of the Receive Slave SCI-PHY mode of the Transmit Master/Receive Slave (TMRS) design. We produced an abstracted model of the TMRS block and then provided a number of relevant liveness and safety properties expressible in FormalCheck, which we verified in reasonable CPU time. We found a number of mismatches between the RTL design and the TMRS specification. Currently we are exercising a hierarchical verification methodology to verify the design of a whole chip. One of the concerns of the industrial companies is the time spent for the whole verification process. We are also trying to come up with an answer to this question: What kind of changes in the design flow will make the whole process of verification faster?

Publications

1. L. Barakatain and S. Tahar: Functional Verification of a SCI-PHY Level 2 Protocol Engine; Proc. IEEE International Conference on Information, Communications & Signal Processing (ICICS 2001), Singapore, October 2001.
2. L. Barakatain, S. Tahar, J. Lamarche, and J-M Gendreau: Practical Approaches to the Model Checking of a Telecom Megacell using FormalCheck ; Proc. ACM 11th Great Lakes Symposium on VLSI (GLS-VLSI'01), West Lafayette, Indiana, USA, March 2001, ACM Publications.
3. L. Barakatain, S. Tahar, Jean-Marc Gendreau and Jean Lamarche: Model Checking of the Transmit Master/Receive Slave (TMRS) using FormalCheck ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 1999. [17 pages]
4. L. Barakatain and S. Tahar: Model Checking of the Fairisle ATM Switch Fabric using FormalCheck; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1999. [11 pages]
5. L. Barakatain: Practical Approaches to Model Checking using FormalCheck ; MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, April 2000.