In this paper, we describe a hybrid tool for hardware formal verification that links the HOL (higher-order logic) theorem prover and (multiway decision graphs) model checker. Our tool supports abstract datatypes and uninterpreted function symbols available in MDG, allowing the verification of high-level specifications. The hybrid tool, HOL