Login | Register

A hybrid tool for linking HOL theorem proving with MDG model checking


A hybrid tool for linking HOL theorem proving with MDG model checking

Mizouni, Rabeb (2003) A hybrid tool for linking HOL theorem proving with MDG model checking. Masters thesis, Concordia University.

Text (application/pdf)


Nowadays, the formal verification of hardware is gaining a lot of importance in the design flow of micro-electronics systems. There exists several formal hardware verification approaches each with its own advantages and drawbacks. Hence, the idea of linking different approaches to benefit from their advantages has emerged as a potential ultimate solution. In this thesis, we describe a hybrid tool for formal hardware verification that links the HOL (Higher-Order Logic) theorem prover and the MDG (Multiway Decision function symbols available in MDG, allowing the verification of high level specifications. For this purpose, we embedded in HOL the grammar of the hardware description language, MDG-HDL, used to represent models to be verified. Furthermore, we provided an embedding of the first-order temporal logic [Special characters omitted.] used to express properties for the MDG model checker. Furthermore, we have developed an interface which reads a HOL goal, generates the required MDG files, calls the MDG model checker, and generates the HOL theorem on successful verification. Our tool also handles design hierarchies by reducing the model to its subsystem according to the property to be verified. Verification with the hybrid tool is faster and more tractable than using either tool separately. This has been illustrated via a number of simple hardware benchmark examples as well as a more elaborated design case study.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Mizouni, Rabeb
Pagination:xii, 92 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Tahar, Sofiene
ID Code:2132
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:25
Last Modified:18 Jan 2018 17:18
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

Back to top Back to top