In order to overcome the limitations of automated tools and the cumbersome proof process of interactive theorem proving, we adopt a hybrid approach for formal hardware verification which uses the strengths of theorem proving (HOL) with powerful mathematical tools such as induction and abstraction, and the advantages of automated tools (MDG) which support equivalence checking and model checking.  The MDG system is a decision diagram based verification tool, primarily designed for hardware verification.  HOL is a theorem prover built on higher-order logic. The methodology used to link the tools and the functioning of the interface are described in detail.  We use the timing block of the 4 by 4 Fairisle ATM switch fabric to illustrate the verification using this hybrid tool.