Login | Register

Integration of HOL and MDG for hardware verification

Title:

Integration of HOL and MDG for hardware verification

Pisini, Vijay Kumar (2000) Integration of HOL and MDG for hardware verification. Masters thesis, Concordia University.

[thumbnail of MQ47830.pdf]
Preview
Text (application/pdf)
MQ47830.pdf
2MB

Abstract

With the ever increasing complexity of the design of digital systems and the size of the circuits in VLSI technology, the role of design verification has gained a lot of importance. Theorem Proving based verification and Decision Diagram based verification are now-a-days the two main techniques used for formal verification. Each of them has its own advantages and disadvantages. In this thesis, we propose a hybrid approach for formal hardware verification which uses the strengths of the theorem prover HOL (Higher-Order Logic) with of the automated tool MDG (Multiway Decision Graphs) which supports equivalence checking and model checking. We developed a linkage tool between HOL and MDG which uses the specification and implementation of a circuit written in HOL to automatically generate all required MDG files. It then calls the MDG equivalence checking procedure and reports the MDG verification result back to HOL. To illustrate the proposed HOL-MDG hybrid verification we use the Cambridge Fairisle ATM switch fabric as an example.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Pisini, Vijay Kumar
Pagination:ix, 71 leaves ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:2000
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:TK 7874.75 P57 2000
ID Code:1092
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:16
Last Modified:13 Jul 2020 19:48
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