, Soene Tahar

cation Abstract. We describe a hybrid formal hardware veri-cation tool that links the HOL interactive proof system and the MDG automated hardware verication tool. It supports a hierarchical verication approach that mir-rors the hierarchical structure of designs. We obtain ad-vantages of both verication paradigms. We illustrate its use by considering a component of a communications chip. Verication with the hybrid tool is signicantly faster and more tractable than using either tool alone.