Abstract

Nowadays, the formal verification of hardware is gaining a lot of importance in the design flow of micro-electronics systems. There exists several formal hardware verification approaches each with its own advantages and drawbacks. Hence, the idea of linking different approaches to benefit from their advantages has emerged as a potential ultimate solution. In this thesis, we describe a hybrid tool for formal hardware verification that links the HOL (Higher-Order Logic) theorem prover and the MDG (Multiway Decision function symbols available in MDG, allowing the verification of high level specifications. For this purpose, we embedded in HOL the grammar of the hardware description language, MDG-HDL, used to represent models to be verified. Furthermore, we provided an embedding of the first-order temporal logic [Special characters omitted.] used to express properties for the MDG model checker. Furthermore, we have developed an interface which reads a HOL goal, generates the required MDG files, calls the MDG model checker, and generates the HOL theorem on successful verification. Our tool also handles design hierarchies by reducing the model to its subsystem according to the property to be verified. Verification with the hybrid tool is faster and more tractable than using either tool separately. This has been illustrated via a number of simple hardware benchmark examples as well as a more elaborated design case study.