Integration of HOL and MDG for hardware verification

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