Design of data abstraction structure for MDG-HOL hybrid tool
SM Musabbir Hasan · Spectrum Research Repository (Concordia University) · 2005
We have proposed design and implementation of a data abstraction structure that will result in extension to an existing Hybrid hardware verification tool so that it empowers to handle larger data paths automatically. Interactive and user-expertise-dependent theorem proving techniques are well suited to handle large and complex data path dominated systems. However, they are complicated and difficult to handle when highly complex real-life designs are considered. On the other hand, automated state-space-exploration based techniques can verify trivial systems automatically, whereas they lack in the ability to verify practical designs due to state space explosion problems. To bring about a solution to the dilemma, hybrid approaches are under study, which widely vary in the tradeoff between the expressiveness of interactive approaches and automation and speed of the exploration based methodologies. In the thesis we have described the design of an abstract data structure that allows natural numbers as the operands in addition to bit level descriptions. As a case study, we specified and implemented a generic computer processor using the abstract data structure. We implemented a parser that would be used to parse the specification and implementation of the design to be verified. With the parser, and the data abstraction structure, it would be the perfect launch-pad for the implementation of a powerful and largely automatic tool that should be able to verify most practical hardware designs