Members

• Mohamed Zaki
• Sofiène Tahar
• Yassine Mokhtari

Description

Model checking is a fully automatic approach to verify a Finite state machine against its temporal specifications. However, its application is limited by the size of the system to be verified. Model reduction is one of the methods to tackle this problem. An implementation of a model reduction approach which is based on syntactic analysis of programs is the subject of this project.

In our proposed approach, a system under verification is considered as a program for which abstract syntax and semantics are defined. The approach analyzes the syntactic and semantic structure of the programs.

Throughout the analysis, the value domains of the state variables are extracted based on the control diagram, and the values of state variables in the program are partitioned into active values, and deactive values according to their dependency to the properties. The deactive values then can be replaced by a typical abstract value, and thus the value domains of the variables are much smaller than the original ones. After the above procedures are done, the state space of the reduced program is smaller than that of the original one, while the correctness of the properties are preserved.

We have developed a tool called SynAbs which accepts a subset of the Verilog hardware description language and universally quantified computation tree logic (CTL) temporal properties, and generates a reduced Verilog code which can be fed into a CTL model checker. We have applied our tool on the verification of a number of case studies. Experimental results showed the superiority of our approach compared to existing model reduction tools.

Publications

1. M. Zaki, Y. Mokhtari and S. Tahar: SynAbs: Model Reduction Tool for Verilog Verification; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 57-60.
2. A. Abdel-Hamid, M. Zaki, and S. Tahar: A tool for Converting Finite State Machine to VHDL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'04), Niagara Falls, Ontario, Canada, May 2004, Vol. 4, pp. 1907-1910.
3. M.Zaki, Y. Mokhtari, and S. Tahar: A Path Dependency Graph for Verilog Program Analysis; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'03), Montreal, Quebec, Canada, June 2003.
4. M. Zaki and S. Tahar: Syntax Code Analysis and Generation for Verilog; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003.
5. M. Zaki: Syntactic Model Reduction for Hardware Verification. MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, April 2003.