Breadcrumb

 
 

Syntactic model reduction for hardware verification

Title:

Syntactic model reduction for hardware verification

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

[img]
Preview
PDF
2607Kb

Abstract

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 > Faculty 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:Theses (M.A.Sc.)
Program:Electrical and Computer Engineering
Date:2003
Thesis Supervisor(s):Tahar, Sofiene
ID Code:2074
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:25
Last Modified:08 Dec 2010 10:24
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

Document Downloads

More statistics for this item...

Concordia University - Footer