Hybrid tool integrating HOL theorem proving with MDG model checking

We describe a hybrid tool for hardware formal verification that links the HOL theorem prover and the MDG (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-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic L_mdg used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.