Digital systems are becoming very large and complex making the process of  finding bugs and design validation in early stages of the design cycle a must. As a contribution towards catching this goal, we propose an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and are mainly used for modeling hardware systems. Both ASM and MDG are based on a subset of many-sorted first order logic, making it appealing to link these two concepts. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models.We consider both structural and behavioral models of hardware in our implementation. We have applied this transformation schema on some examples and case studies where our tool generates the corresponding MDG-HDL models automatically.

Download PDF file (PDF File)

Download ASM, MDG, and verification files.

Send comments and suggestions to: amjad@ece.concordia.ca