Members

• Mohammed Hazanuzzaman
• Sofiène Tahar
• Ali Habibi

External Collaborators

• HVG group in Cambridge

Description

In this project, we aim at interfacing the hybrid MDG-HOL tool with Verilog HDL. This will enable an automatic input of RTL models written in Verilog into the tool rather than doing a hand-translation of such models to MDG-HDL, which can be error prone. In a first stage, we intend to implement a parser from a synthesizable subset of Verilog to our MDG system in that we first generate a control and data flow graph from Verilog, then translate it into HOL terms (formulas), which would comply with the MDG-HDL library of components and Tables. Next, we will use the existing hybrid tool to translate the obtained HOL description into MDG for model or equivalence checking. For the design of the lexical and syntactical analyzer and parser, we will use the SML language, which is the implementation language of HOL. We aim at building this Verilog-HOL-MDG translator based on a generic approach developed at Cambridge U., which defines an intermediate HDL, called VV, that can be synthesized from either Verilog or VHDL and describe models as finite state machines.