Formal verification along with design for transactional models

Chip complexity has grown to a point where traditional verification techniques are growing difficult and expensive to use. Current research is looking into the use of formal methods along with changes in the design methodology to cope with the problem of implementing complex designs correctly. It is suggested that the formalization of abstract models from the start of the design process can find problem with the design early and reduce the cost of fixing bugs.; The key to successfully using formal verification during the early design stages is to recognize that different verification problems must be approached from different perspectives. Each different perspective answers the question of "Why is the design correct?" using a different reasoning technique. By using different models and tools for each different perspective, a set of perspective can capture the design intuition, thus the models can be made small enough so that they can be constructed, verified, and modified quickly. This methodology was applied to the verification of the Smart Memories Project during the design phase, and it has found corner case bugs early in the design process, reducing the cost of re-design compared to the case when the bugs were not found until later.; One particular perspective that was used in verifying the Cache Controller of the Smart Memories is the transactional model perspective. The tool TDV (transactional diagram verifier) was developed to enable quick model construction and fast formal verification to be performed on models with transaction view. TDV is especially efficient in verifying designs that have problematic corner case situations caused by interacting parallel transactions.; TDV verifies parallel transaction models by producing and verifying a set of lower level assertions from the specification. The way the specifications are modeled and converted into lower level assertions are well suited in verifying transaction model designs.