Members

• Hong Peng
• Yassine Mokhtari
• Sofiène Tahar

External Collaborators

• Dr. Ferhat Khendek, Concordia University

Description

In this project we aim at enabling the model checking of large designs by integrating compositional verification and model reduction. In a compositional verification, properties are only true under certain environments. In our approach, we provide the environment assumptions as temporal logic formulas and then synthesize an executable hardware description language module from it. Compared with existing related work, the proposed environment has a smaller state space, which is a key factor in compositional verification. The synthesized modules are composed with the design block under verification and then fed into a model checking tool

In case the size of the composed module is still beyond the capability of model checking, we use a novel syntactic model reduction algorithm, which analyzes the source code and removes the redundant variables and values. The reduction is based on the static analysis of control flow diagram of the program, where values of state variables are partitioned into active and deactive values according to their dependency to the properties. Compared with existing related work, the proposed approach is automatic and has better performance in the reduction of datapath intensive designs. In order to demonstrate the application of the proposed techniques, we verified an industrial size ATM (Asynchronous Transfer Mode) switch fabric from Nortel Networks which complexity is beyond the capability of plain model checking tools.

Publications

1. H. Peng, S. Tahar and F. Khendek: Comparison of SPIN and VIS for Protocol Verification; International Journal on Software Tools for Technology Transfer, Vol. 4, No. 2, pp. 234-245, February 2003, Springer Verlag.
2. H. Peng, Y. Mokhtari, and S. Tahar: Environment Synthesis for Compositional Model Checking; Proc. IEEE International Conference on Computer Design (ICCD'02), Freiburg, Germany, September 2002, IEEE Computer Society Press, pp 70-75.
3. H. Peng: Improving Compositional Verification Environment Synthesis and Syntactic Model Reduction. Ph.D. Electrical Engineer, Concordia University, Department of Electrical and Computer Engineering, Fall 2002.
4. H. Peng, Y. Mokhtari, and S. Tahar: Model Reduction Based on Value Dependency; Proc. IEEE International ASCI/SOC Conference (ASIC'2001), Washigton, DC, USA, September 2001.
5. H. Peng, Yassine Mokhtari and Sofiene Tahar: Improving Cone of Influence Reduction; Technical Report, Concordia University, Department of Electrical and Computer Engineering, April 2001. [12 pages]
6. H. Peng, S. Tahar, and F. Khendek: SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol; IEEE International Conference on Formal Engineering Methods (ICFEM'2000), York, UK, September 2000, pp. 79-88.
7. H. Peng and S. Tahar: Hardware Modeling and Verification of an ATM Ring MAC Protocol; IEEE 12th International Conference on Microelectronics (ICM'00), Teheran, Iran, November 2000.
8. H. Peng and S. Tahar: Compositional Verification of IP Based Designs; Proc. IFIP International Worshop on IP Based Synthesis and System Design, Grenoble, France, December 1999, pp. 189-193.
9. H. Peng and S. Tahar: Formal Verification of an Asynchronous MAC Layer Protocol in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 1999. [14 pages]
10. H. Peng, S. Tahar and F. Khendek: Comparison of SPIN and VIS for Protocol Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 1999. [15 pages]
11. H. Peng and S. Tahar: Compositional Verification of an ATM Bit Error Rate Monitor Circuit; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 1999. [23 pages]
12. H. Peng and S. Tahar: A Survey on Compositional Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1998. [17 pages]