Abstraction techniques for verification of digital designs

textIndustrial designs are becoming more complicated as technology advances and demand for higher performance increases. The growing complexity poses an increasingly serious challenge towards avoiding design errors. Consequently, design verification forms an important task in the product development cycle. It is desirable to attain an acceptable level of confidence in a design as early in the development cycle as possible. This makes automatic verification methods quite popular as they are effective in discovering bugs with relatively low turn around time. However, as the design size grows, most techniques are adversely affected by the design state explosion problem. The main contribution of this dissertation is the development of automated abstraction techniques that serve to alleviate the state explosion problem. The fundamental idea is to formulate the behavior of a system in an abstracted, hence simplified, model with fewer states and verify the system by analyzing the model. This dissertation presents two abstraction techniques to address design verification problems. In the first, we use data abstraction to automatically abstract away much of the data path of a design that, in some cases, is responsible for state explosion. We then present a technique to generate witnesses that enable the original design to exercise interesting control behavior. The second technique presented in the dissertation deals with verification of custom memories. We present a technique to abstract behaviors of switch level devices using regular expressions and an automatic method for constructing state machines that are useful in verifying equivalence between a register transfer language level description of a custom memory and a switch level description of the same, augmented with an abstraction of the memory core. The effectiveness of the techniques presented in the dissertation has been demonstrated on real life industrial designs.Electrical and Computer Engineerin