Pisini, Vijay Kumar (2000) Integration of HOL and MDG for hardware verification. Masters thesis, Concordia University.
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 > Faculty of Engineering and Computer Science > Electrical and Computer Engineering|
|Item Type:||Thesis (Masters)|
|Authors:||Pisini, Vijay Kumar|
|Pagination:||ix, 71 leaves ; 29 cm.|
|Degree Name:||Theses (M.A.Sc.)|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Tahar, Sofiene|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 17:16|
|Last Modified:||08 Dec 2010 15:18|
Repository Staff Only: item control page