| 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. |
