Members

• Mohamed Zaki
• Sofiène Tahar
• Yassine Mokhtari

Description

This project is concerned with the syntax and semantic analysis of Verilog programs. The Verilog syntax is very large and defining its full semantic is a very complex task. We start by identifying the main Verilog subset used for hardware behavioral modelling , then we describe a small-step operational semantics suitable for static analysis and program verification. By using the semantical functions Reachability Condition and State transformations, we build an abstract state transition graph (ASTG) which models the behavior of Verilog designs. The ASTG can be used in static analysis techniques such as data flow analysis and model abstract ion, where it can models synchronous as well as asynchronous concurrent designs.

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. PDF File
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.