Importing mdg verification results into hol

Abstract

Formal hardware verification systems can be split into two categories: theorem proving systems and automatic finite state machine based systems. Each approach has its own complementary advantages and disadvantages. In this paper, we consider the combination of two such systems: HOL (a theorem proving system) and MDG (an automatic system). As HOL hardware verification proofs are based on the hierarchical structure of the design, submodules can be verified using other systems such as MDG. However, the results of MDG are not in the appropriate form for this. We have proved a set of theorems that express how results proved using MDG can be converted into the form used in traditional HOL hardware verification.