On the embedding of the MDG specification languages in HOL

Summary form only given. We propose an embedding of the MDG input languages in HOL. The MDG (multiway decision graph) system is a tool for equivalence and model checking. It is based on multiway decision graphs that extend reduced-ordered binary decision diagrams with abstract sorts and uninterpreted functions. The HOL system is a higher-order logic theorem prover. It has an open user-extensible architecture, giving the possibility of adding expressiveness power to the theorem prover by embedding new theories. We have embedded in HOL the grammar of the MDG hardware description language, MDG-HDL, and the first-order temporal logic, /spl Lscr/;/sub mdg/, used to specify properties for the MDG model checker. A hybrid tool for formal verification, linking HOL with the MDG model checker, is proposed as an application of the developed embeddings.