Login | Register

Syntactic model reduction for hardware verification


Syntactic model reduction for hardware verification

Hussein, Mohamed H. Zaki (2003) Syntactic model reduction for hardware verification. Masters thesis, Concordia University.

[thumbnail of MQ77694.pdf]
Text (application/pdf)


Microelectronics systems become more and more complex, making the detection of errors extremely difficult. Model checking, as a formal hardware verification technique, can potentially catch subtle hardware design errors. It is used to automatically verify temporal properties on finite state systems. However, model checking tools suffer from the state explosion problem; when the number of states representing the program under verification grows exponentially. state explosion problem. The main idea of model reduction is to suppress the techniques that involve both approaches can greatly reduce the design under techniques in which, variables not influencing the property's variables are removed and the values domains of state variables in the system model are values according to their dependency to the property to be verified. 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 successfully applied our tool on the verification of a number of simple Verilog programs.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Hussein, Mohamed H. Zaki
Pagination:xiv, 95 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:TK 7874.75 H87 2003
ID Code:2074
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:25
Last Modified:13 Jul 2020 19:51
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top