Scalable solutions to specification and verification of large designs

The requirements on time to market pose an immovable constraint on design and validation. These requirements are a direct consequence of technological advances and increase in design complexities that make it difficult to reduce the gap between product concept and volume shipments. The time spent on validation constitutes almost as large a fraction of this time as the development itself. Therefore it is not only required to streamline the design process but also to contain the validation time within the permissible constraints. Moreover, modern designs with their multiple and complex features raise the need for a faster and more scalable validation process that could provide the desired degree of confidence in the correctness of the design within the time allocated for verification.; Though many methods and techniques are now available to verify designs automatically, it is hard to find a way to combine the benefits of completeness and automation at the same time. The reason for this is the fact that most mathematical methods that ensure completeness are restricted in their capacity for being automated, because of the specification process that is essentially manual. The specification task is not only cumbersome but is also expensive and takes a large amount of time. Being a subjective task the specification process is highly prone to errors.; While the specification process cannot be fully automated, this thesis strives towards a reduction in the time and effort required in developing the specifications. It aims at producing robust specifications that are consistent with fewer redundancies. A causality based method of diagnosis of the bug, in case the specification is found faulty, is also proposed. Furthermore, the thesis presents a method of making the verification process more flexible through the integrated use of simulation and model checking; it provides solutions to some of the key issues in combining the two methodologies. One of the main contributions in this part is the automatic biasing or generation of directed test cases based on the specifications. This method utilizes signal relationships and their usage in the specification to decide on the nature of the test cases. It is shown that the proposed methods help make the verification problem more manageable and scalable. The techniques are tried and tested on the GL85 microprocessor design which is a clone of Intel's 8085 microprocessor. This design was verified as a whole, without partitioning into subunits, so that the advantages and efficiency of the proposed methods could be observed on a model with a large number of latches.