Formal hardware verification by integrating HOL and MDG
Vijay Kumar Pisini, Sofiène Tahar, Paul Curzon, O. Ait-Mohamed, Xiaoyu Song · 2000
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.